The dTT/Narya definition of Kan complexes

kan.ny

` ------------------------------------------------
` Kevin Carlson, Astra Kolomatskaia, Reed Mullanix
` Narya formalisation of Kan complexes
`
` developed 13-18 May 2024 during the
`   Prospects of Formal Mathematics
` trimester program at the
`   Hausdorff Institute for Mathematics
`
` dated 7 June 2024
` modulo whitespace and α-equivalence
`
` to be checked with flags: -dtt -discreteness
` ------------------------------------------------

def ⊥ : Type := data []
def ⊤ : Type := sig #(transparent) ()

def Nat : Type :=
data [
| zero. : Nat
| suc.  : Nat → Nat ]

def Nat.degen (n : Nat) : Nat⁽ᵈ⁾ n :=
match n [
| zero.  ↦ zero.
| suc. n ↦ suc. (Nat.degen n) ]

def SST : Type :=
codata [
| X .z : Type
| X .s : (X .z) → SST⁽ᵈ⁾ X ]

def SST.○ (n : Nat) (A : SST) : Type :=
match n [
| zero.  ↦ ⊤
| suc. n ↦
  sig
    ( pt  : A .z
    , ∂a  : SST.○ n A
    , a   : SST.● n A ∂a
    , ∂a' : SST.○⁽ᵈ⁾ n (Nat.degen n) A (A .s pt) ∂a) ]

and SST.● (n : Nat) (A : SST) (○a : SST.○ n A) : Type :=
match n [
| zero.  ↦ A .z
| suc. n ↦ SST.●⁽ᵈ⁾ n (Nat.degen n) A (A .s (○a .pt)) (○a .∂a) (○a .∂a') (○a .a) ]

def Horn.○ (n k : Nat) (A : SST) (○a : SST.○ n A) : Type :=
match n, k [
| zero.  , zero.         ↦ A .z
| zero.  , suc. zero.    ↦ A .z
| zero.  , suc. (suc. k) ↦ ⊥
| suc. n , zero.         ↦
  sig
    ( pt : A .z
    , Λa : SST.○⁽ᵈ⁾ (suc. n) (Nat.degen (suc. n)) A (A .s pt) ○a)
| suc. n , suc. k        ↦
  sig
    ( Λa  : Horn.○ n k A (○a .∂a)
    , a   : Horn.● n k A (○a .∂a) (○a .a) Λa
    , Λa' : Horn.○⁽ᵈ⁾
      n (Nat.degen n)
      k (Nat.degen k)
      A (A .s (○a .pt))
      (○a .∂a) (○a .∂a')
      Λa) ]

and Horn.● (n k : Nat) (A : SST) (○a : SST.○ n A) (●a : SST.● n A ○a)
  (Λ : Horn.○ n k A ○a) : Type :=
match n, k [
| zero.  , zero.         ↦ A .s Λ .z ●a
| zero.  , suc. zero.    ↦ A .s ●a .z Λ
| zero.  , suc. (suc. k) ↦ ⊥
| suc. n , zero.         ↦
  SST.●⁽ᵈ⁾ (suc. n) (Nat.degen (suc. n)) A (A .s (Λ .pt)) ○a (Λ .Λa) ●a
| suc. n , suc. k        ↦
  Horn.●⁽ᵈ⁾
    n (Nat.degen n)
    k (Nat.degen k)
    A (A .s (○a .pt))
    (○a .∂a) (○a .∂a')
    (○a .a) ●a
    (Λ .Λa) (Λ .Λa')
    (Λ .a) ]

def Horn (n k : Nat) (A : SST) : Type :=
sig
  ( ∂a : SST.○ n A
  , Λa : Horn.○ n k A ∂a)

def Horn.data (n k : Nat) (A : SST) (Λ : Horn n k A) : Type :=
sig
  ( face : SST.● n A (Λ .∂a)
  , filler : Horn.● n k A (Λ .∂a) face (Λ .Λa))

def Kan (A : SST) : Type :=
  (n k : Nat) (Λ : Horn n k A) → Horn.data n k A Λ

def Kan.promote (A : SST) (K : Kan A) (x : A .z) : Kan⁽ᵈ⁾ A (A .s x) K :=
n n' k k' Λ Λ' ↦
  let F := K n k Λ in
  let F' :=
    K (suc. n) (suc. k)
      ( (x, Λ .∂a, F .face, Λ' .∂a)
      , (Λ .Λa, F .filler, Λ' .Λa)) in
  (F' .face , F' .filler)

axiom A : SST
axiom x : A .z
axiom y : A .z
axiom α : A .s x .z y
axiom z : A .z
axiom β : A .s x .z z
axiom γ : A .s y .z z
axiom 𝔣 : A .s x .s y α .z z β γ

def ○αβγ : SST.○ 2 A := (x, (y, (), z, ()), γ, (α, (), β, ()))
def ●αβγ : SST.● 2 A ○αβγ := 𝔣

def Λαβ : Horn 1 0 A := ((y, (), z, ()), (x, (α, (), β, ())))
def Λαγ : Horn 1 1 A := ((x, (), z, ()), (y, γ, α))
def Λβγ : Horn 1 2 A := ((x, (), y, ()), (z, γ, β))

def Λαβ.data : Horn.data 1 0 A Λαβ := (γ, 𝔣)
def Λαγ.data : Horn.data 1 1 A Λαγ := (β, 𝔣)
def Λβγ.data : Horn.data 1 2 A Λβγ := (α, 𝔣)