Definition: coordinate_name
`Cname ==  {2...}`

Lemma: coordinate_name_wf
`Cname ∈ Type`

Lemma: coordinate_name-value-type
`value-type(Cname)`

Definition: cname_deq
`CnameDeq ==  IntDeq`

Lemma: cname_deq_wf
`CnameDeq ∈ EqDecider(Cname)`

Definition: eq-cname
`eq-cname(x;y) ==  CnameDeq x y`

Lemma: eq-cname_wf
`∀[x,y:Cname].  (eq-cname(x;y) ∈ 𝔹)`

Lemma: assert-eq-cname
`∀[x,y:Cname].  uiff(↑eq-cname(x;y);x = y ∈ Cname)`

Lemma: decidable__equal-coordinate_name
`∀x,y:Cname.  Dec(x = y ∈ Cname)`

Definition: nameset
`nameset(L) ==  {a:Cname| (a ∈ L)} `

Lemma: nameset_wf
`∀[L:Cname List]. (nameset(L) ∈ Type)`

Lemma: nameset-equipollent
`∀L:Cname List. nameset(L) ~ ℕ||remove-repeats(CnameDeq;L)||`

Lemma: member-nameset-diff
`∀[L,X:Cname List]. ∀[x:nameset(L)].  x ∈ nameset(L-X) supposing ¬(x ∈ X)`

Lemma: nameset-value-type
`∀[L:Cname List]. value-type(nameset(L))`

Lemma: nameset_subtype
`∀[L1,L2:Cname List].  nameset(L1) ⊆r nameset(L2) supposing l_subset(Cname;L1;L2)`

Lemma: nameset_subtype_cons_diff
`∀[I:Cname List]. ∀[x:nameset(I)].  (nameset(I) ⊆r nameset([x / I-[x]]))`

Lemma: nameset_subtype_base
`∀[L:Cname List]. (nameset(L) ⊆r Base)`

Lemma: nameset_sq
`∀[L:Cname List]. SQType(nameset(L))`

Lemma: decidable__nameset
`∀L:Cname List. ∀a:Cname.  Dec(a ∈ nameset(L))`

Definition: fresh-cname
`fresh-cname(I) ==  (fst(list-max(x.x;[1 / I]))) + 1`

Lemma: fresh-cname_wf
`∀[I:Cname List]. (fresh-cname(I) ∈ {x:Cname| ¬(x ∈ I)} )`

Lemma: fresh-cname-not-member
`∀[I:Cname List]. (¬(fresh-cname(I) ∈ nameset(I)))`

Lemma: fresh-cname-not-member2
`∀I:Cname List. (¬(fresh-cname(I) ∈ I))`

Lemma: fresh-cname-not-member-list-diff
`∀I:Cname List. ∀[L:Cname List]. (¬(fresh-cname(I) ∈ I-L))`

Lemma: fresh-cname-not-equal
`∀I:Cname List. ∀[x:nameset(I)]. (¬(fresh-cname(I) = x ∈ Cname))`

Lemma: fresh-cname-not-equal2
`∀I:Cname List. ∀[x:nameset(I)]. (¬(x = fresh-cname(I) ∈ Cname))`

`∀I:Cname List. (I = [fresh-cname(I) / I]-[fresh-cname(I)] ∈ (Cname List))`

`∀I:Cname List. ([fresh-cname(I) / I]-[fresh-cname(I)] ~ I)`

`I+ ==  eval m = fresh-cname(I) in [m / I]`

`∀[I:Cname List]. (I+ ∈ Cname List)`

`∀[I:Cname List]. (nameset(I) ⊆r nameset(I+))`

Definition: extd-nameset
`extd-nameset(L) ==  nameset(L) ⋃ ℕ2`

Lemma: extd-nameset_wf
`∀[L:Cname List]. (extd-nameset(L) ∈ Type)`

Lemma: extd-nameset_subtype_base
`∀[L:Cname List]. (extd-nameset(L) ⊆r Base)`

Lemma: extd-nameset-respects-equality
`∀[L:Cname List]. ∀[T:Type].  respects-equality(extd-nameset(L);T)`

Lemma: extd-nameset_subtype_int
`∀[L:Cname List]. (extd-nameset(L) ⊆r ℤ)`

Lemma: extd-nameset_subtype
`∀[L,L':Cname List].  extd-nameset(L) ⊆r extd-nameset(L') supposing l_subset(Cname;L;L')`

Lemma: extd-nameset-nil
`extd-nameset([]) ⊆r ℕ2`

Lemma: nsub2_subtype_extd-nameset
`∀[L:Cname List]. (ℕ2 ⊆r extd-nameset(L))`

Lemma: nameset_subtype_extd-nameset
`∀[L:Cname List]. (nameset(L) ⊆r extd-nameset(L))`

Definition: isname
`isname(z) ==  2 ≤z z`

Lemma: isname_wf
`∀[L:Cname List]. ∀[z:extd-nameset(L)].  (isname(z) ∈ 𝔹)`

Lemma: isname-nameset
`∀[L:Cname List]. ∀[z:nameset(L)].  (isname(z) ~ tt)`

Lemma: isname-name
`∀[z:Cname]. (isname(z) ~ tt)`

Lemma: assert-isname
`∀[L:Cname List]. ∀[z:extd-nameset(L)].  uiff(↑isname(z);z ∈ nameset(L))`

Lemma: not-assert-isname
`∀[L:Cname List]. ∀[z:extd-nameset(L)].  uiff(¬↑isname(z);z ∈ ℕ2)`

Definition: uext
`uext(g) ==  λz.if isname(z) then g z else z fi `

Lemma: uext_wf
`∀[I,J:Cname List]. ∀[g:nameset(I) ⟶ extd-nameset(J)].  (uext(g) ∈ extd-nameset(I) ⟶ extd-nameset(J))`

Definition: name-morph
`name-morph(I;J) ==`
`  {f:nameset(I) ⟶ extd-nameset(J)| `
`   ∀i,j:nameset(I).  ((↑isname(f i)) `` (↑isname(f j)) `` ((f i) = (f j) ∈ extd-nameset(J)) `` (i = j ∈ nameset(I)))} `

Lemma: name-morph_wf
`∀[I,J:Cname List].  (name-morph(I;J) ∈ Type)`

Lemma: name-morph-ap
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[x:nameset(I)].  (f x ∈ extd-nameset(J))`

Lemma: uext-ap-name
`∀[I,J:Cname List]. ∀[g:name-morph(I;J)]. ∀[x:nameset(I)].  ((uext(g) x) = (g x) ∈ extd-nameset(J))`

Lemma: name-morphs-equal
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:nameset(I) ⟶ extd-nameset(J)].`
`  f = g ∈ name-morph(I;J) supposing f = g ∈ (nameset(I) ⟶ extd-nameset(J))`

Lemma: name-morph-ext
`∀[I,J:Cname List]. ∀[f,g:name-morph(I;J)].`
`  f = g ∈ name-morph(I;J) supposing ∀x:nameset(I). ((f x) = (g x) ∈ extd-nameset(J))`

Lemma: name-morph_subtype
`∀[I,J,A,B:Cname List].`
`  (name-morph(I;J) ⊆r name-morph(A;B)) supposing ((nameset(A) ⊆r nameset(I)) and (nameset(J) ⊆r nameset(B)))`

Lemma: name-morph_subtype_remove1
`∀[I,J:Cname List]. ∀[x:Cname]. ∀[f:name-morph(I;J)].`
`  (f ∈ name-morph(I-[x];J-[f x])) supposing ((↑isname(f x)) and (x ∈ I))`

Definition: extend-name-morph
`f[z1:=z2] ==  λx.if eq-cname(x;z1) then z2 else f x fi `

Lemma: extend-name-morph_wf
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[z1,z2:Cname].  f[z1:=z2] ∈ name-morph([z1 / I];[z2 / J]) supposing ¬(z2 ∈ J)`

Definition: name-morph-extend
`(f)+ ==  eval m = fresh-cname(I) in eval m' = fresh-cname(J) in   λx.if CnameDeq x m then m' else f x fi `

Lemma: name-morph-extend_wf
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  ((f)+ ∈ name-morph(I+;J+))`

Definition: name-morph-domain
`name-morph-domain(f;I) ==  nameset(filter(λx.isname(f x);I))`

Lemma: name-morph-domain_wf
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  (name-morph-domain(f;I) ∈ Type)`

Lemma: name-morph-domain_subtype
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  name-morph-domain(f;I) ≡ {x:nameset(I)| ↑isname(f x)} `

Lemma: name-morph-domain-inject
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  Inj(name-morph-domain(f;I);nameset(J);f)`

Lemma: name-morph-one-one
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[x,y:nameset(I)].`
`  (x = y ∈ Cname) supposing (((f x) = (f y) ∈ Cname) and (↑isname(f y)) and (↑isname(f x)))`

Lemma: name-morph_subtype_domain
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  (f ∈ name-morph-domain(f;I) ⟶ nameset(J))`

Definition: name-morph-range
`name-morph-range(f;I) ==  {x:Cname| ∃i:nameset(I). ((↑isname(f i)) ∧ ((f i) = x ∈ Cname))} `

Lemma: name-morph-range_wf
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  (name-morph-range(f;I) ∈ Type)`

Definition: name-morph-inv
`name-morph-inv(I;f) ==  λx.hd(filter(λi.(isname(f i) ∧b (f i =z x));I))`

Lemma: name-morph-inv_wf
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  (name-morph-inv(I;f) ∈ name-morph-range(f;I) ⟶ nameset(I))`

Lemma: name-morph-inv-eq
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[x:nameset(I)].`
`  (name-morph-inv(I;f) (f x)) = x ∈ nameset(I) supposing ↑isname(f x)`

Lemma: name-morph-inv-eq-domain
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[x:name-morph-domain(f;I)].  ((name-morph-inv(I;f) (f x)) = x ∈ nameset(I))`

Definition: id-morph
`1 ==  λx.x`

Lemma: id-morph_wf
`∀[I:Cname List]. (1 ∈ name-morph(I;I))`

Lemma: name-morph-extend-id
`∀[I:Cname List]. ((1)+ = 1 ∈ name-morph(I+;I+))`

Definition: face-map
`(x:=i) ==  λz.if (z =z x) then i else z fi `

Lemma: face-map_wf
`∀[L:Cname List]. ∀[x:Cname]. ∀[p:ℕ2].  ((x:=p) ∈ name-morph([x / L];L))`

Lemma: face-map_wf2
`∀[I:Cname List]. ∀[x:Cname]. ∀[p:ℕ2].  ((x:=p) ∈ name-morph(I;I-[x]))`

Lemma: face-map-property
`∀[L:Cname List]`
`  ∀x:Cname. ∀p:ℕ2. ∀y:nameset([x / L]).`
`    (((↑isname((x:=p) y)) `` ((¬(y = x ∈ Cname)) ∧ (((x:=p) y) = y ∈ nameset(L))))`
`    ∧ ((¬↑isname((x:=p) y)) `` ((y = x ∈ Cname) ∧ (((x:=p) y) = p ∈ ℕ2))))`

Definition: degeneracy-map
`degeneracy-map(f) ==  f`

Lemma: degeneracy-map_wf
`∀[I,J:Cname List]. ∀[f:nameset(I) ⟶ nameset(J)].`
`  degeneracy-map(f) ∈ name-morph(I;J) supposing Inj(nameset(I);nameset(J);f)`

Lemma: name-morph-degeneracy-map
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  (degeneracy-map(f) ∈ name-morph(filter(λx.isname(f x);I);J))`

Definition: iota
`iota(x) ==  λz.z`

Lemma: iota_wf
`∀[I:Cname List]. ∀[x:Cname].  (iota(x) ∈ name-morph(I;[x / I]))`

Lemma: iota-wf
`∀[I:Cname List]. ∀[x:nameset(I)].  (iota(x) ∈ name-morph(I-[x];I))`

Definition: iota'
`iota'(I) ==  iota(fresh-cname(I))`

Lemma: iota'_wf
`∀[I:Cname List]. (iota'(I) ∈ name-morph(I;I+))`

Lemma: face-map_wf_fresh-cname
`∀[L:Cname List]. ∀[p:ℕ2].  ((fresh-cname(L):=p) ∈ name-morph(L+;L))`

Definition: name-comp
`(f o g) ==  uext(g) o f`

Lemma: name-comp_wf
`∀[I,J,K:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)].  ((f o g) ∈ name-morph(I;K))`

Lemma: name-comp-id-left
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  ((1 o f) = f ∈ name-morph(I;J))`

Lemma: name-comp-id-right
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  ((f o 1) = f ∈ name-morph(I;J))`

Lemma: name-comp-assoc
`∀[I,J,K,H:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)]. ∀[h:name-morph(K;H)].`
`  (((f o g) o h) = (f o (g o h)) ∈ name-morph(I;H))`

Lemma: name-morph-extend-comp
`∀[I,J,K:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)].  (((f o g))+ = ((f)+ o (g)+) ∈ name-morph(I+;K+))`

Lemma: name-morph-extend-face-map
`∀[I,K:Cname List]. ∀[i:ℕ2]. ∀[f:name-morph(I;K)].`
`  (((fresh-cname(I):=i) o f) = ((f)+ o (fresh-cname(K):=i)) ∈ name-morph(I+;K))`

Lemma: face-map-comp
`∀A,B:Cname List. ∀g:name-morph(A;B). ∀x:nameset(A). ∀i:ℕ2.`
`  (g o (g x:=i)) = ((x:=i) o g) ∈ name-morph(A;B-[g x]) supposing ↑isname(g x)`

Lemma: face-map-comp-id
`∀A,B:Cname List. ∀g:name-morph(A;B). ∀x:nameset(A). ∀i:ℕ2.`
`  ((x:=i) o g) = g ∈ name-morph(A;B) supposing (¬↑isname(g x)) ∧ ((g x) = i ∈ ℕ2)`

Lemma: face-map-comp-trivial
`∀A,B:Cname List. ∀g:name-morph(A;B). ∀x:Cname. ∀i:ℕ2.  ((x:=i) o g) = g ∈ name-morph(A;B) supposing ¬(x ∈ A)`

Lemma: face-map-idempotent
`∀A,B:Cname List. ∀x:nameset(A). ∀g:name-morph(A-[x];B). ∀i:ℕ2.`
`  (((x:=i) o ((x:=i) o g)) = ((x:=i) o g) ∈ name-morph(A;B))`

Lemma: face-map-comp2
`∀A,B:Cname List. ∀g:name-morph(A;B). ∀x,y:nameset(A). ∀i,j:ℕ2.`
`  (g o ((g x:=i) o (g y:=j))) = (((x:=i) o (y:=j)) o g) ∈ name-morph(A;B-[g x; g y]) `
`  supposing ((↑isname(g x)) ∧ (↑isname(g y))) ∧ (¬(x = y ∈ Cname))`

Lemma: face-maps-commute
`∀I:Cname List. ∀x:nameset(I). ∀i:ℕ2. ∀y:nameset(I). ∀j:ℕ2.`
`  ((¬(x = y ∈ Cname)) `` (((x:=i) o (y:=j)) = ((y:=j) o (x:=i)) ∈ name-morph(I;I-[x; y])))`

Lemma: iota-identity
`∀[I:Cname List]. ∀[x:Cname]. ∀[i:ℕ2].  (iota(x) o (x:=i)) = 1 ∈ name-morph(I;I) supposing ¬(x ∈ I)`

Lemma: iota-identity2
`∀[I:Cname List]. ∀[x:Cname]. ∀[i:ℕ2].  ((x:=i) o iota(x)) = 1 ∈ name-morph(I;I) supposing ¬(x ∈ I)`

Lemma: iota-face-map
`∀[I:Cname List]. ∀[x,y:Cname]. ∀[i:ℕ2].`
`  ((x:=i) o iota(y)) = (iota(y) o (x:=i)) ∈ name-morph(I;[y / I-[x]]) supposing ¬(x = y ∈ Cname)`

Lemma: iota-two-face-maps
`∀[I:Cname List]. ∀[x,y,z:Cname]. ∀[i,j:ℕ2].`
`  (((x:=i) o (y:=j)) o iota(z)) = (iota(z) o ((x:=i) o (y:=j))) ∈ name-morph(I;[z / I-[x; y]]) `
`  supposing (¬(x = z ∈ Cname)) ∧ (¬(y = z ∈ Cname))`

Lemma: iota'-identity
`∀[I:Cname List]. ∀[i:ℕ2].  ((iota'(I) o (fresh-cname(I):=i)) = 1 ∈ name-morph(I;I))`

Lemma: iota'-comp
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  ((iota'(I) o (f)+) = (f o iota'(J)) ∈ name-morph(I;J+))`

Lemma: extend-name-morph-iota
`∀I,K:Cname List. ∀f:name-morph(I;K). ∀z,x:Cname.`
`  (iota(z) o f[z:=x]) = (f o iota(x)) ∈ name-morph(I;[x / K]) supposing (¬(x ∈ K)) ∧ (¬(z ∈ I))`

Lemma: extend-face-map-same
`∀[I:Cname List]. ∀[x,y:Cname]. ∀[i:ℕ2].`
`  (x:=i)[y:=y] = (x:=i) ∈ name-morph([y / I];[y / I]-[x]) supposing (¬(y = x ∈ Cname)) ∧ (¬(y ∈ I))`

Lemma: extend-name-morph-face-map
`∀I,K:Cname List. ∀f:name-morph(I;K). ∀z,x:Cname. ∀i:ℕ2.`
`  (f[z:=x] o (x:=i)) = ((z:=i) o f) ∈ name-morph([z / I];K) supposing (¬(x ∈ K)) ∧ (¬(z ∈ I))`

Lemma: extend-name-morph-irrelevant
`∀I,K:Cname List. ∀f:name-morph(I;K).  (f = f[fresh-cname(I):=fresh-cname(K)] ∈ name-morph(I;K))`

Lemma: lift-reduce-face-map
`∀[I:Cname List]. ∀[x:nameset(I)]. ∀[c,i:ℕ2].`
`  ((iota(fresh-cname(I)) o ((x:=i) o (fresh-cname(I):=c))) = (x:=i) ∈ name-morph(I;I-[x]))`

Definition: swap-names
`swap-names(z1;z2) ==  λx.if eq-cname(x;z1) then z2 if eq-cname(x;z2) then z1 else x fi `

Lemma: swap-names_wf
`∀[I:Cname List]. ∀[z1,z2:nameset(I)].  (swap-names(z1;z2) ∈ name-morph(I;I))`

Definition: rename-one-name
`rename-one-name(z1;z2) ==  λx.if eq-cname(x;z1) then z2 else x fi `

Lemma: rename-one-name_wf
`∀[I:Cname List]. ∀[z1,z2:Cname].`
`  rename-one-name(z1;z2) ∈ name-morph([z1 / I];[z2 / I]) supposing (¬(z1 ∈ I)) ∧ (¬(z2 ∈ I))`

Lemma: rename-one-same
`∀I:Cname List. ∀z:Cname.  rename-one-name(z;z) = 1 ∈ name-morph([z / I];[z / I]) supposing ¬(z ∈ I)`

Lemma: rename-one-iota
`∀I:Cname List. ∀z,z1:Cname.`
`  (iota(z) o rename-one-name(z;z1)) = iota(z1) ∈ name-morph(I;[z1 / I]) supposing (¬(z1 ∈ I)) ∧ (¬(z ∈ I))`

Lemma: rename-one-comp
`∀I:Cname List. ∀z,z1,z2:Cname.`
`  (rename-one-name(z;z1) o rename-one-name(z1;z2)) = rename-one-name(z;z2) ∈ name-morph([z / I];[z2 / I]) `
`  supposing (¬(z2 ∈ I)) ∧ (¬(z1 ∈ I)) ∧ (¬(z ∈ I))`

Lemma: extended-face-map
`∀I:Cname List. ∀x1,x2:nameset(I). ∀i:ℕ2. ∀y1,y2:Cname.`
`  (x2:=i)[y1:=y2] = ((x2:=i) o rename-one-name(y1;y2)) ∈ name-morph([y1 / I-[x1]];[y2 / I-[x1; x2]]) `
`  supposing (¬(y2 ∈ I-[x1; x2])) ∧ (¬(y1 ∈ I))`

Lemma: extended-face-map1
`∀I:Cname List. ∀x:nameset(I). ∀i:ℕ2. ∀y1,y2:Cname.`
`  (x:=i)[y1:=y2] = ((x:=i) o rename-one-name(y1;y2)) ∈ name-morph([y1 / I];[y2 / I-[x]]) `
`  supposing (¬(y2 ∈ I-[x])) ∧ (¬(y1 ∈ I))`

Definition: face-maps-comp
`face-maps-comp(L) ==  reduce(λp,f. (let x,i = p in (x:=i) o f);λt.t;L)`

Lemma: face-maps-comp_wf
`∀[L:(Cname × ℕ2) List]. ∀[I:Cname List].  (face-maps-comp(L) ∈ name-morph(map(λp.(fst(p));L) @ I;I))`

Lemma: face-maps-comp-property
`∀L:(Cname × ℕ2) List`
`  ∀[I:Cname List]`
`    ∀y:nameset(map(λp.(fst(p));L) @ I)`
`      (((↑isname(face-maps-comp(L) y)) `` ((¬(y ∈ map(λp.(fst(p));L))) ∧ ((face-maps-comp(L) y) = y ∈ nameset(I))))`
`      ∧ ((¬↑isname(face-maps-comp(L) y))`
`        `` ((y ∈ map(λp.(fst(p));L)) ∧ ((face-maps-comp(L) y) = outl(apply-alist(CnameDeq;L;y)) ∈ ℕ2))))`

Lemma: extend-name-morph-rename-one
`∀I,K:Cname List. ∀f:name-morph(I;K). ∀z,z1,v:Cname.`
`  ((¬(z1 ∈ I))`
`  `` (¬(z ∈ I))`
`  `` (¬(v ∈ K))`
`  `` (f[z:=v] = (rename-one-name(z;z1) o f[z1:=v]) ∈ name-morph([z / I];[v / K])))`

Lemma: rename-one-extend-name-morph
`∀I,K:Cname List. ∀f:name-morph(I;K). ∀x,y,z:Cname.`
`  ((¬(x ∈ I)) `` (¬(z ∈ K)) `` (¬(y ∈ K)) `` ((f[x:=y] o rename-one-name(y;z)) = f[x:=z] ∈ name-morph([x / I];[z / K])))`

Lemma: extend-name-morph-comp
`∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀z,v,v1:Cname.`
`  ((¬(z ∈ I)) `` (¬(v ∈ K)) `` (¬(v1 ∈ J)) `` ((f o g)[z:=v] = (f[z:=v1] o g[v1:=v]) ∈ name-morph([z / I];[v / K])))`

Lemma: rename-one-extend-id
`∀I:Cname List. ∀z,z1:Cname.`
`  ((¬(z ∈ I)) `` (¬(z1 ∈ I)) `` (rename-one-name(z;z1) = 1[z:=z1] ∈ name-morph([z / I];[z1 / I])))`

Lemma: name-morph-decomp
`∀I,J:Cname List. ∀f:name-morph(I;J).`
`  ∃L:(Cname × ℕ2) List`
`   ∃K:Cname List`
`    (nameset(I) ≡ nameset(map(λp.(fst(p));L) @ K)`
`    ∧ (∃g:nameset(K) ⟶ nameset(J)`
`        (Inj(nameset(K);nameset(J);g) ∧ (f = (face-maps-comp(L) o degeneracy-map(g)) ∈ name-morph(I;J)))))`

Definition: name-cat
`NameCat ==  <Cname List, λI,J. name-morph(I;J), λI.1, λI,J,K,f,g. (f o g)>`

Lemma: name-cat_wf
`NameCat ∈ SmallCategory`

Lemma: name-morph-nil
`∀[I:Cname List]. name-morph(I;[]) ≡ nameset(I) ⟶ ℕ2`

Definition: name-morph-flip
`flip(f;y) ==  λn.if eq-cname(n;y) then 1 - f n else f n fi `

Lemma: name-morph-flip_wf
`∀[I:Cname List]. ∀[y:nameset(I)]. ∀[f:name-morph(I;[])].  (flip(f;y) ∈ name-morph(I;[]))`

Lemma: name-morph-flips-commute
`∀I:Cname List. ∀x:name-morph(I;[]). ∀i,j:nameset(I).  (flip(flip(x;j);i) = flip(flip(x;i);j) ∈ name-morph(I;[]))`

Lemma: name-morph-flip-face-map1
`∀I:Cname List. ∀y:nameset(I). ∀a:ℕ2. ∀f:name-morph(I-[y];[]). ∀v:nameset(I).`
`  ((¬(v = y ∈ Cname)) `` (flip(((y:=a) o f);v) = ((y:=a) o flip(f;v)) ∈ name-morph(I;[])))`

Lemma: name-morph-flip-face-map
`∀I:Cname List. ∀y:nameset(I). ∀a:ℕ2. ∀c1:name-morph(I;[]). ∀v:nameset(I).`
`  ((¬(v = y ∈ Cname)) `` (flip(((y:=a) o c1);v) = ((y:=a) o flip(c1;v)) ∈ name-morph(I;[])))`

Lemma: nsub2-flip
`∀[x,y:ℕ2].  uiff((1 - x) = y ∈ ℕ2;x = (1 - y) ∈ ℕ2)`

Lemma: name-morph-flip-flip
`∀I:Cname List. ∀f:name-morph(I;[]). ∀j:nameset(I).  (flip(flip(f;j);j) = f ∈ name-morph(I;[]))`

Lemma: name-comp-flip
`∀I:Cname List. ∀x:nameset(I). ∀K:Cname List. ∀f:name-morph(I;K). ∀f1:name-morph(K;[]).`
`  (f o flip(f1;f x)) = flip((f o f1);x) ∈ name-morph(I;[]) supposing ↑isname(f x)`

Definition: cubical-set
`CubicalSet ==`
`  {XF:X:L:(Cname List) ⟶ Type × (I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J))| `
`   let X,F = XF `
`   in (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).`
`         ((F I K (f o g)) = ((F J K g) o (F I J f)) ∈ ((X I) ⟶ (X K))))`
`      ∧ (∀I:Cname List. ((F I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))} `

Lemma: cubical-set-eqs-istype
`∀[XF:X:L:(Cname List) ⟶ Type × (I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J))]`
`  istype(let X,F = XF `
`         in (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).`
`               ((F I K (f o g)) = ((F J K g) o (F I J f)) ∈ ((X I) ⟶ (X K))))`
`            ∧ (∀I:Cname List. ((F I I 1) = (λx.x) ∈ ((X I) ⟶ (X I)))))`

Lemma: cubical-set_wf
`CubicalSet ∈ 𝕌'`

Lemma: cubical-set-is-functor
`CubicalSet ≡ Functor(NameCat;TypeCat)`

Definition: cube-set-map
`A ⟶ B ==  nat-trans(NameCat;TypeCat;A;B)`

Lemma: cube-set-map_wf
`∀[A,B:CubicalSet].  (A ⟶ B ∈ 𝕌')`

Definition: csm-comp
`G o F ==  F o G`

Lemma: csm-comp_wf
`∀[A,B,C:CubicalSet]. ∀[F:A ⟶ B]. ∀[G:B ⟶ C].  (G o F ∈ A ⟶ C)`

Lemma: csm-comp-sq
`∀[A,B,C,F,G:Top].  (G o F ~ λA,x. (G A (F A x)))`

Lemma: csm-comp-assoc
`∀[A,B,C,D:CubicalSet]. ∀[F:A ⟶ B]. ∀[G:B ⟶ C]. ∀[H:C ⟶ D].  (H o G o F = H o G o F ∈ A ⟶ D)`

Definition: csm-id
`1(X) ==  identity-trans(NameCat;TypeCat;X)`

Lemma: csm-id_wf
`∀[X:CubicalSet]. (1(X) ∈ X ⟶ X)`

Lemma: csm-id-comp
`∀[A,B:CubicalSet]. ∀[sigma:A ⟶ B].  ((sigma o 1(A) = sigma ∈ A ⟶ B) ∧ (1(B) o sigma = sigma ∈ A ⟶ B))`

Definition: I-cube
`X(I) ==  X I`

Lemma: I-cube_wf
`∀[X:CubicalSet]. ∀[I:Cname List].  (X(I) ∈ Type)`

Lemma: csm-equal
`∀[A,B:CubicalSet]. ∀[f:A ⟶ B]. ∀[g:I:(Cname List) ⟶ A(I) ⟶ B(I)].`
`  f = g ∈ A ⟶ B supposing f = g ∈ (I:(Cname List) ⟶ A(I) ⟶ B(I))`

Lemma: cube-set-map-subtype
`∀[A,B:CubicalSet].  (A ⟶ B ⊆r (I:(Cname List) ⟶ A(I) ⟶ B(I)))`

Definition: csm-ap
`(s)x ==  s I x`

Lemma: csm-ap_wf
`∀[X,Y:CubicalSet]. ∀[s:X ⟶ Y]. ∀[I:Cname List]. ∀[x:X(I)].  ((s)x ∈ Y(I))`

Lemma: csm-ap-csm-comp
`∀Gamma,Delta,Z,s1,s2,I,alpha:Top.  ((s2 o s1)alpha ~ (s2)(s1)alpha)`

Definition: cube-set-restriction
`f(s) ==  (snd(X)) I J f s`

Lemma: cube-set-restriction_wf
`∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[s:X(I)].  (f(s) ∈ X(J))`

Lemma: cube-set-restriction-face-map
`∀[X:CubicalSet]. ∀[I,K:Cname List]. ∀[f:name-morph(I;K)]. ∀[s:X(I)]. ∀[c:ℕ2]. ∀[j:name-morph-domain(f;I)].`
`  ((f j:=c)(f(s)) = f((j:=c)(s)) ∈ X(K-[f j]))`

Lemma: cube-set-restriction-id
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[s:X(I)].  (1(s) = s ∈ X(I))`

Lemma: cube-set-restriction-when-id
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[s:X(I)]. ∀[f:name-morph(I;I)].  f(s) = s ∈ X(I) supposing f = 1 ∈ name-morph(I;I)`

Lemma: cube-set-restriction-comp
`∀X:CubicalSet. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I).  (g(f(a)) = (f o g)(a) ∈ X(K))`

Lemma: cube-set-restriction-comp2
`∀X:CubicalSet. ∀I,J,J2,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I).`
`  g(f(a)) = (f o g)(a) ∈ X(K) supposing J = J2 ∈ (Cname List)`

Lemma: csm-ap-restriction
`∀X,Y:CubicalSet. ∀s:X ⟶ Y. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  (f((s)a) = (s)f(a) ∈ Y(J))`

Lemma: cube-set-map-is
`∀[A,B:CubicalSet].`
`  (A ⟶ B ~ {trans:I:(Cname List) ⟶ A(I) ⟶ B(I)| `
`             ∀I,J:Cname List. ∀g:name-morph(I;J).  ((λs.g(trans I s)) = (λs.(trans J g(s))) ∈ (A(I) ⟶ B(J)))} )`

Definition: unit-cube
`unit-cube(I) ==  <λJ.name-morph(I;J), λJ,K,f,g. (g o f)>`

Lemma: unit-cube_wf
`∀[I:Cname List]. (unit-cube(I) ∈ CubicalSet)`

Lemma: unit-cube-I-cube
`∀[I,L:Top].  (unit-cube(I)(L) ~ name-morph(I;L))`

Lemma: unit-cube-is-yoneda
`∀[I:Cname List]. (unit-cube(I) = rep-pre-sheaf(op-cat(NameCat);I) ∈ CubicalSet)`

Definition: unit-cube-map
`unit-cube-map(f) ==  λK,g. (f o g)`

Lemma: unit-cube-map_wf
`∀[I,J:Cname List]. ∀[f:name-morph(I;J)].  (unit-cube-map(f) ∈ unit-cube(J) ⟶ unit-cube(I))`

Lemma: unit-cube-map-id
`∀I:Cname List. (unit-cube-map(1) = 1(unit-cube(I)) ∈ unit-cube(I) ⟶ unit-cube(I))`

Lemma: unit-cube-map-comp
`∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).`
`  (unit-cube-map((f o g)) = unit-cube-map(f) o unit-cube-map(g) ∈ unit-cube(K) ⟶ unit-cube(I))`

Definition: trivial-cube-set
`() ==  <λJ.Unit, λJ,K,f,x. ⋅>`

Lemma: trivial-cube-set_wf
`() ∈ CubicalSet`

Definition: discrete-cube
`discrete-cube(A) ==  <λJ.A, λJ,K,f,x. x>`

Lemma: discrete-cube_wf
`∀[A:Type]. (discrete-cube(A) ∈ CubicalSet)`

Definition: cubical-interval
`cubical-interval() ==  <λI.(name-morph(I;[]) ⟶ ℕ2), λJ,K,f,L,g. (L (f o g))>`

Lemma: cubical-interval_wf
`cubical-interval() ∈ CubicalSet`

Comment: Rules of MLTT without type formers
`The rules from Figure 1 in Bezem, Coquand, Huber`
`"A model of type theory in cubical sets".`
`(First those without type formers)`

`    Γ ⊢`
`-------------                         this is csm-id_wf`
`  1: σ ⟶ Γ`

`σ: Δ ⟶ Γ    δ: Θ -> Δ`
`------------------------              this is csm-comp_wf`
`     σ δ : Θ ⟶ Γ`

`Γ ⊢ A   σ : Δ ⟶ Γ`
`----------------------                this is csm-ap-type_wf`
`     Δ ⊢ A σ`

`Γ ⊢ t: A   σ: Δ ⟶ Γ`
`-----------------------               this is csm-ap-term_wf`
`     Δ ⊢ t σ: A σ`

`-------------                         this is trivial-cube-set_wf`
`   () ⊢`

`Γ ⊢    Γ ⊢ A`
`-----------------                     this is cube-context-adjoin_wf`
`     Γ.A ⊢ `

`     Γ ⊢ A`
`------------------                    this is cc-fst_wf`
`   p:  Γ.A ⟶ Γ`

`   Γ ⊢ A`
`-----------------                     this is cc-snd_wf`
`   Γ.A ⊢ q: Ap `

`σ:Δ ⟶ Γ  Γ ⊢ A   Δ ⊢ u:A s`
`------------------------------        this is csm-adjoin_wf`
`   (σ,u) ⊢ Δ ⟶ Γ.A`

`1 σ = σ 1 = σ                         this is csm-id-comp`
`(σ δ) ν = σ (δ ν)                     this is csm-comp-assoc`
`[u] = (1,u)                           this is csm-id-adjoin`
`A 1 = A                               this is csm-ap-id-type`
`(A σ) δ = A (σ δ)                     this is csm-ap-comp-type`
`u 1 = 1                               this is csm-ap-id-term`
`(u σ) δ = u (σ δ)                     this is csm-ap-comp-term `
`(σ, u) δ = (σ δ, u δ)                 this is csm-adjoin-ap`
`p (σ, u) = σ                          this is cc-fst-csm-adjoin`
`q (σ, u) = u                          this is cc-snd-csm-adjoin`
`(p,q) = 1                             this is csm-adjoin-fst-snd`

`⋅`

Comment: Rules of MLTT type formers
`The rules about type formers Π and ⌜Σ⌝ from Figure 1 in Bezem, Coquand, Huber`
`"A model of type theory in cubical sets".`

`  Γ.A ⊢ B`
`-------------                         this is cubical-pi_wf`
` Γ ⊢ Π A B `

`  Γ.A ⊢ B   Γ.A ⊢ b:B`
`------------------------              this is cubical-lambda_wf`
`   Γ ⊢ λb : Π A B  `

`  Γ.A ⊢ B`
`-------------                         this is cubical-sigma_wf`
` Γ ⊢ Σ A B`

` Γ.A ⊢ B  Γ ⊢ u:A  Γ ⊢ v:B[u]`
`------------------------------        this is cubical-pair_wf`
`     Γ ⊢ (u,v): Σ A B`

`  Γ ⊢ w: Σ A B`
`----------------                      this is cubical-fst_wf`
`  Γ ⊢ w.1: A`

`  Γ ⊢ w: Σ A B`
`-----------------                     this is cubical-snd_wf`
`  Γ ⊢ w.2: B[w.1]   `

` Γ ⊢ w:Π A B   Γ ⊢ u:A`
`------------------------              this is cubical-app_wf`
` Γ ⊢ app(w,u): B[u]  `

`(Π A B)σ = Π (Aσ) (B(σp,q))           this is csm-cubical-pi`
`(λb)σ = λ(b(σp,q))                    this is csm-ap-cubical-lambda  `
`app(w,u)δ = app(wδ, uδ)               this is csm-ap-cubical-app`
`app(λb, u) = b[u]                     this is cubical-beta`
`w = λ(app(wp,q))                      this is cubical-eta`
`(Σ A B)σ =  (Aσ) (B(σp,q))            this is csm-cubical-sigma`
`(w.1)σ = (wσ).1                       this is csm-ap-cubical-fst`
`(w.2)σ = (wσ).2                       this is csm-ap-cubical-snd`
`(u,v)σ = (uσ, vσ)                     this is csm-ap-cubical-pair`
`(u,v).1 = u                           this is cubical-fst-pair`
`(u,v).2 = v                           this is cubical-snd-pair`
`(w.1,w.2) = w                         this is cubical-pair-eta`
`⋅`

Definition: cubical-type
`{X ⊢ _} ==`
`  {AF:A:I:(Cname List) ⟶ X(I) ⟶ Type × (I:(Cname List)`
`                                         ⟶ J:(Cname List)`
`                                         ⟶ f:name-morph(I;J)`
`                                         ⟶ a:X(I)`
`                                         ⟶ (A I a)`
`                                         ⟶ (A J f(a)))| `
`   let A,F = AF `
`   in (∀I:Cname List. ∀a:X(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))`
`      ∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:X(I). ∀u:A I a.`
`           ((F I K (f o g) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K (f o g)(a))))} `

Lemma: cubical-type_wf
`∀[X:CubicalSet]. (X ⊢  ∈ 𝕌')`

Definition: cubical-type-at
`A(a) ==  (fst(A)) I a`

Lemma: cubical-type-at_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[a:X(I)].  (A(a) ∈ Type)`

Definition: cubical-type-ap-morph
`(u a f) ==  (snd(A)) I J f a u`

Lemma: cubical-type-ap-morph_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[a:X(I)]. ∀[u:A(a)].  ((u a f) ∈ A(f(a)))`

Lemma: cubical-type-ap-morph-comp
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I,J,K:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)]. ∀[a:X(I)]. ∀[u:A(a)].`
`  (((u a f) f(a) g) = (u a (f o g)) ∈ A((f o g)(a)))`

Lemma: cubical-type-ap-morph-id
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[f:name-morph(I;I)]. ∀[a:X(I)]. ∀[u:A(a)].`
`  (u a f) = u ∈ A(a) supposing f = 1 ∈ name-morph(I;I)`

Lemma: cubical-type-ap-rename-one-equal
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[x,y:Cname]. ∀[a:X([x / I])]. ∀[u,v:A(a)].`
`  u = v ∈ A(a) `⇐⇒` (u a rename-one-name(x;y)) = (v a rename-one-name(x;y)) ∈ A(rename-one-name(x;y)(a)) `
`  supposing (¬(y ∈ I)) ∧ (¬(x ∈ I))`

Lemma: cubical-type-equal
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:A:I:(Cname List) ⟶ X(I) ⟶ Type × (I:(Cname List)`
`                                                                      ⟶ J:(Cname List)`
`                                                                      ⟶ f:name-morph(I;J)`
`                                                                      ⟶ a:X(I)`
`                                                                      ⟶ (A I a)`
`                                                                      ⟶ (A J f(a)))].`
`  A = B ∈ {X ⊢ _} `
`  supposing A`
`  = B`
`  ∈ (A:I:(Cname List) ⟶ X(I) ⟶ Type × (I:(Cname List)`
`                                        ⟶ J:(Cname List)`
`                                        ⟶ f:name-morph(I;J)`
`                                        ⟶ a:X(I)`
`                                        ⟶ (A I a)`
`                                        ⟶ (A J f(a))))`

Definition: csm-ap-type
`(AF)s ==  let A,F = AF in <λI,a. (A I (s)a), λI,J,f,a,u. (F I J f (s)a u)>`

Lemma: csm-ap-type_wf
`∀[Gamma,Delta:CubicalSet]. ∀[s:Delta ⟶ Gamma]. ∀[A:{Gamma ⊢ _}].  Delta ⊢ (A)s`

Definition: csm-type-ap
`csm-type-ap(A;s) ==  (A)s`

Lemma: csm-type-ap_wf
`∀[Gamma,Delta:CubicalSet]. ∀[s:Delta ⟶ Gamma]. ∀[A:{Gamma ⊢ _}].  Delta ⊢ csm-type-ap(A;s)`

Lemma: csm-ap-id-type
`∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}].  ((A)1(Gamma) = A ∈ {Gamma ⊢ _})`

Lemma: csm-ap-comp-type
`∀[Gamma,Delta,Z:CubicalSet]. ∀[s1:Z ⟶ Delta]. ∀[s2:Delta ⟶ Gamma]. ∀[A:{Gamma ⊢ _}].`
`  ((A)s2 o s1 = ((A)s2)s1 ∈ {Z ⊢ _})`

Lemma: csm-ap-comp-type-sq
`∀[Gamma:CubicalSet]. ∀[Delta,Z,s1,s2:Top].  ∀A:{Gamma ⊢ _}. ((A)s2 o s1 ~ ((A)s2)s1)`

Lemma: csm-cubical-type-ap-morph
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I,J,f,a,u,s:Top].  ((u a f) ~ (u (s)a f))`

Definition: cubical-term
`{X ⊢ _:AF} ==`
`  {u:I:(Cname List) ⟶ a:X(I) ⟶ ((fst(AF)) I a)| `
`   ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:X(I).  let A,F = AF in (F I J f a (u I a)) = (u J f(a)) ∈ (A J f(a))} `

Lemma: cubical-term_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}].  ({X ⊢ _:A} ∈ Type)`

Definition: cubical-term-at
`u(a) ==  u I a`

Lemma: cubical-term-at_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[a:X(I)].  (u(a) ∈ A(a))`

Lemma: cubical-term-at-morph
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[a:X(I)]. ∀[J:Cname List]. ∀[f:name-morph(I;J)].`
`  ((u(a) a f) = u(f(a)) ∈ A(f(a)))`

Lemma: cubical-term-equal
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[z:I:(Cname List) ⟶ a:X(I) ⟶ ((fst(A)) I a)].`
`  u = z ∈ {X ⊢ _:A} supposing u = z ∈ (I:(Cname List) ⟶ a:X(I) ⟶ ((fst(A)) I a))`

Lemma: cubical-term-equal2
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[u,z:{X ⊢ _:A}].`
`  u = z ∈ {X ⊢ _:A} supposing ∀I:Cname List. ∀a:X(I).  ((u I a) = (z I a) ∈ ((fst(A)) I a))`

Definition: csm-ap-term
`(t)s ==  λI,a. (t I (s)a)`

Lemma: csm-ap-term_wf
`∀[Delta,Gamma:CubicalSet]. ∀[s:Delta ⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[t:{Gamma ⊢ _:A}].  ((t)s ∈ {Delta ⊢ _:(A)s})`

Lemma: csm-ap-id-term
`∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[t:{Gamma ⊢ _:A}].  ((t)1(Gamma) = t ∈ {Gamma ⊢ _:A})`

Lemma: csm-ap-comp-term
`∀[Gamma,Delta,Z:CubicalSet]. ∀[s1:Z ⟶ Delta]. ∀[s2:Delta ⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[t:{Gamma ⊢ _:A}].`
`  ((t)s2 o s1 = ((t)s2)s1 ∈ {Z ⊢ _:(A)s2 o s1})`

`X.A ==  <λI.(alpha:X(I) × A(alpha)), λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>>`

`∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}].  (Gamma.A ∈ CubicalSet)`

`(v;u) ==  <v, u>`

`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀J:Cname List. ∀v:X(J). ∀u:A(v).  ((v;u) ∈ X.A(J))`

`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[J,K,g,v,u:Top].  (g((v;u)) ~ (g(v);(u v g)))`

Definition: cc-fst
`p ==  λI,p. (fst(p))`

Lemma: cc-fst_wf
`∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}].  (p ∈ Gamma.A ⟶ Gamma)`

Definition: cc-snd
`q ==  λI,p. (snd(p))`

Lemma: cc-snd_wf
`∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}].  (q ∈ {Gamma.A ⊢ _:(A)p})`

Lemma: csm-type-at
`∀Gamma:CubicalSet. ∀s:Top. ∀A:{Gamma ⊢ _}. ∀I,alpha:Top.  ((A)s(alpha) ~ A((s)alpha))`

`(s;u) ==  λI,a. <(s)a, u I a>`

`∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:Delta ⟶ Gamma]. ∀[u:{Delta ⊢ _:(A)sigma}].`
`  ((sigma;u) ∈ Delta ⟶ Gamma.A)`

`∀[sigma,u,I,del:Top].  (((sigma;u))del ~ <(sigma)del, (u)del>)`

`[u] ==  (1(X);u)`

`∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[u:{Gamma ⊢ _:A}].  ([u] ∈ Gamma ⟶ Gamma.A)`

`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀u:{X ⊢ _:A}. ∀I:Cname List. ∀a:X(I).  (([u])a = (a;u I a) ∈ X.A(I))`

`∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:Delta ⟶ Gamma]. ∀[u:{Delta ⊢ _:(A)sigma}].`
`  (p o (sigma;u) = sigma ∈ Delta ⟶ Gamma)`

`∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:Delta ⟶ Gamma]. ∀[u:{Delta ⊢ _:(A)sigma}].`
`  ((q)(sigma;u) = u ∈ {Delta ⊢ _:(A)sigma})`

`∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}].  ((p;q) = 1(Gamma.A) ∈ Gamma.A ⟶ Gamma.A)`

Definition: cubical-pi-family
`cubical-pi-family(X;A;B;I;a) ==`
`  {w:J:(Cname List) ⟶ f:name-morph(I;J) ⟶ u:A(f(a)) ⟶ B((f(a);u))| `
`   ∀J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀u:A(f(a)).`
`     ((w J f u (f(a);u) g) = (w K (f o g) (u f(a) g)) ∈ B(g((f(a);u))))} `

Lemma: cubical-pi-family_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[I:Cname List]. ∀[a:X(I)].  (cubical-pi-family(X;A;B;I;a) ∈ Type)`

Lemma: cubical-pi-family-comp
`∀X,Delta:CubicalSet. ∀s:Delta ⟶ X. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:Delta(I). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}.`
`∀w:cubical-pi-family(X;A;B;I;(s)a).`
`  (λK,g. (w K (f o g)) ∈ cubical-pi-family(X;A;B;J;(s)f(a)))`

Lemma: csm-cubical-pi-family
`∀X,Delta:CubicalSet. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta ⟶ X. ∀I:Cname List. ∀a:Delta(I).`
`  (cubical-pi-family(X;A;B;I;(s)a) = cubical-pi-family(Delta;(A)s;(B)(s o p;q);I;a) ∈ Type)`

Definition: cubical-pi
`ΠA B ==  <λI,a. cubical-pi-family(X;A;B;I;a), λI,J,f,a,w,K,g. (w K (f o g))>`

Lemma: cubical-pi_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].  X ⊢ ΠA B`

Lemma: csm-cubical-pi
`∀X,Delta:CubicalSet. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta ⟶ X.  ((ΠA B)s = Delta ⊢ Π(A)s (B)(s o p;q) ∈ {Delta ⊢ _})`

Definition: cubical-lambda
`(λb) ==  λI,a,J,f,u. (b J (f(a);u))`

Lemma: cubical-lambda_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[b:{X.A ⊢ _:B}].  ((λb) ∈ {X ⊢ _:ΠA B})`

Definition: cubical-app
`app(w; u) ==  λI,a. (w I a I 1 (u I a))`

Lemma: cubical-app_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}]. ∀[u:{X ⊢ _:A}].  (app(w; u) ∈ {X ⊢ _:(B)[u]})`

Definition: cubical-sigma
`Σ A B ==  <λI,a. (u:A(a) × B((a;u))), λI,J,f,a,p. <(fst(p) a f), (snd(p) (a;fst(p)) f)>>`

Lemma: cubical-sigma_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].  X ⊢ Σ A B`

Lemma: cubical-sigma-at
`∀[X,A,B,I,a:Top].  (Σ A B(a) ~ u:A(a) × B((a;u)))`

Lemma: csm-cubical-sigma
`∀X,Delta:CubicalSet. ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:Delta ⟶ X.  ((Σ A B)s = Σ (A)s (B)(s o p;q) ∈ {Delta ⊢ _})`

Definition: cubical-fst
`p.1 ==  λI,a. (fst((p I a)))`

Lemma: cubical-fst_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}].  (p.1 ∈ {X ⊢ _:A})`

Lemma: csm-cubical-fst
`∀[p,s:Top].  ((p.1)s ~ (p)s.1)`

Lemma: csm-ap-cubical-fst
`∀[X,Delta:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}]. ∀[s:Delta ⟶ X].`
`  ((p.1)s = (p)s.1 ∈ {Delta ⊢ _:(A)s})`

Definition: cubical-snd
`p.2 ==  λI,a. (snd((p I a)))`

Lemma: cubical-snd_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}].  (p.2 ∈ {X ⊢ _:(B)[p.1]})`

Lemma: csm-ap-cubical-snd
`∀[X,Delta:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}]. ∀[s:Delta ⟶ X].`
`  ((p.2)s = (p)s.2 ∈ {Delta ⊢ _:((B)[p.1])s})`

Definition: cubical-pair
`cubical-pair(u;v) ==  λI,a. <u I a, v I a>`

Lemma: cubical-pair_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[v:{X ⊢ _:(B)[u]}].  (cubical-pair(u;v) ∈ {X ⊢ _:Σ A B})`

Lemma: csm-ap-cubical-pair
`∀[X,Delta:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[v:{X ⊢ _:(B)[u]}]. ∀[s:Delta ⟶ X].`
`  ((cubical-pair(u;v))s = cubical-pair((u)s;(v)s) ∈ {Delta ⊢ _:(Σ A B)s})`

Lemma: csm-ap-cubical-app
`∀[X,Delta:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}]. ∀[u:{X ⊢ _:A}]. ∀[s:Delta ⟶ X].`
`  ((app(w; u))s = app((w)s; (u)s) ∈ {Delta ⊢ _:((B)[u])s})`

Lemma: csm-ap-cubical-lambda
`∀[X,Delta:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}]. ∀[u:{X ⊢ _:A}]. ∀[s:Delta ⟶ X].`
`  ((app(w; u))s = app((w)s; (u)s) ∈ {Delta ⊢ _:((B)[u])s})`

Lemma: cubical-snd-pair
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[v:{X ⊢ _:(B)[u]}].`
`  (cubical-pair(u;v).2 = v ∈ {X ⊢ _:(B)[u]})`

Lemma: cubical-fst-pair
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[u:{X ⊢ _:A}]. ∀[v:{X ⊢ _:(B)[u]}].`
`  (cubical-pair(u;v).1 = u ∈ {X ⊢ _:A})`

Lemma: cubical-pair-eta
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:Σ A B}].  (cubical-pair(w.1;w.2) = w ∈ {X ⊢ _:Σ A B})`

Lemma: cubical-eta
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[w:{X ⊢ _:ΠA B}].  ((λapp((w)p; q)) = w ∈ {X ⊢ _:ΠA B})`

Lemma: cubical-beta
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[b:{X.A ⊢ _:B}]. ∀[u:{X ⊢ _:A}].`
`  (app((λb); u) = (b)[u] ∈ {X ⊢ _:(B)[u]})`

Definition: discrete-cubical-type
`discr(T) ==  <λI,alpha. T, λI,J,f,alpha,x. x>`

Lemma: discrete-cubical-type_wf
`∀[T:Type]. ∀[X:CubicalSet].  X ⊢ discr(T)`

Definition: discrete-cubical-term
`discr(t) ==  λI,alpha. t`

Lemma: discrete-cubical-term_wf
`∀[T:Type]. ∀[t:T]. ∀[X:CubicalSet].  (discr(t) ∈ {X ⊢ _:discr(T)})`

Definition: constant-cubical-type
`(X) ==  <λI,alpha. X(I), λI,J,f,alpha,w. f(w)>`

Lemma: constant-cubical-type_wf
`∀[X,Gamma:CubicalSet].  Gamma ⊢ (X)`

Lemma: constant-cubical-type-at
`∀[X,I,a:Top].  ((X)(a) ~ X(I))`

Lemma: unit-cube-cubical-type
`∀[I:Cname List]`
`  ({unit-cube(I) ⊢ _} ~ {AF:A:L:(Cname List) ⟶ name-morph(I;L) ⟶ Type × (L:(Cname List)`
`                                                                          ⟶ J:(Cname List)`
`                                                                          ⟶ f:name-morph(L;J)`
`                                                                          ⟶ a:name-morph(I;L)`
`                                                                          ⟶ (A L a)`
`                                                                          ⟶ (A J (a o f)))| `
`                         let A,F = AF `
`                         in (∀K:Cname List. ∀a:name-morph(I;K). ∀u:A K a.  ((F K K 1 a u) = u ∈ (A K a)))`
`                            ∧ (∀L,J,K:Cname List. ∀f:name-morph(L;J). ∀g:name-morph(J;K). ∀a:name-morph(I;L). ∀u:A L a.`
`                                 ((F L K (f o g) a u) = (F J K g (a o f) (F L J f a u)) ∈ (A K (a o (f o g)))))} )`

Comment: defining the Kan structure
`First, we define the uniform Kan condition for `
`a cubical set X.  `
`We really need it for the cubical dependent types,`
`but a cubical set with Kan structure becomes`
`a "constant" (i.e. independent of the context) cubical type with Kan structure`
`constant-Kan-type`
`constant-Kan-type_wf.`

`For a given I,`
`we can define the family of I-faces (faces of the I-cubes)`
`indexed by pairs ⌜nameset(I) × ℕ2⌝`
`by I-face = x:nameset(I) × ℕ2 × X(I-[x])`

`Face <y,b,w> is face-compatible with face <z,c,u>`
`if (z:=c)(w) = (y:=b)(u)  in X(I-[y; z])`

`A list of I-faces L is adjacent-compatible if it is`
`pairwise face-compatible.`

`Then we define open_box and the Kan filler, etc.`

`But, what we really need is a Kan structure on a cubical type`
` Γ ⊢ A`

`For that, for a given  I and α in Γ(I)`
`we have a type A(α), and we need to define what an open box in`
`A(α)  is.`
`Here, a face will be x:nameset(I) × i:ℕ2 × A((x:=i)(α)).`
`We call this an A-face and define `
`A-face-compatible`
`A-adjacent-compatible`
`fills-A-faces`
`A-face-image`

`The most tedious proof is to show that`
`the image of A-face-compatible A-faces are`
`A-face-compatible.  A-face-compatible-image.`
`⋅`

`The theorems about Kan structure in the Bezem, Coquand, Huber paper`
`are`
`Theorem 6.1 --that context morphisms (cubical set maps) preserve Kan structure:`
`  csm-Kan-cubical-type_wf`
`  csm-Kan-id`
`  csm-Kan-comp`

`Theorem 6.2 -- Pi type has Kan structure`
`                (that is preserved by context morphisms)`
`    *** not proved yet ***`

`Theorem 6.3 -- Sigma type has Kan structure `
`                (that is preserved by context morphisms)`
`   Kan-cubical-sigma_wf`
`   csm-Kan-cubical-sigma`

`Theorem 7.1  -- Identity type has Kan structure`
`   Kan-cubical-identity_wf`
`   csm-Kan-cubical-identity⋅`

Definition: I-face
`I-face(X;I) ==  x:nameset(I) × ℕ2 × X(I-[x])`

Lemma: I-face_wf
`∀[X:CubicalSet]. ∀[I:Cname List].  (I-face(X;I) ∈ Type)`

Definition: face-dimension
`dimension(f) ==  fst(f)`

Lemma: face-dimension_wf
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f:I-face(X;I)].  (dimension(f) ∈ nameset(I))`

Definition: face-direction
`direction(f) ==  fst(snd(f))`

Lemma: face-direction_wf
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f:I-face(X;I)].  (direction(f) ∈ ℕ2)`

Definition: face-cube
`cube(f) ==  snd(snd(f))`

Lemma: face-cube_wf
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f:I-face(X;I)].  (cube(f) ∈ X(I-[dimension(f)]))`

Definition: A-face
`A-face(X;A;I;alpha) ==  x:nameset(I) × i:ℕ2 × A((x:=i)(alpha))`

Lemma: A-face_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)].  (A-face(X;A;I;alpha) ∈ Type)`

Definition: face-name
`face-name(f) ==  <fst(f), fst(snd(f))>`

Lemma: face-name_wf
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f:I-face(X;I)].  (face-name(f) ∈ nameset(I) × ℕ2)`

Definition: face-name-eq
`face-name-eq(a;b) ==  product-deq(ℤ;ℤ;IntDeq;IntDeq) a b`

Lemma: face-name-eq_wf
`∀[I:Cname List]. ∀[a,b:nameset(I) × ℕ2].  (face-name-eq(a;b) ∈ 𝔹)`

Lemma: assert-face-name-eq
`∀[I:Cname List]. ∀[a,b:nameset(I) × ℕ2].  uiff(↑face-name-eq(a;b);a = b ∈ (nameset(I) × ℕ2))`

Definition: A-face-name
`A-face-name(f) ==  <fst(f), fst(snd(f))>`

Lemma: A-face-name_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[f:A-face(X;A;I;alpha)].`
`  (A-face-name(f) ∈ nameset(I) × ℕ2)`

Definition: face-compatible
`face-compatible(X;I;f1;f2) ==`
`  let y,b,w = f1 in `
`  let z,c,u = f2 in `
`  (¬(y = z ∈ Cname)) `` ((z:=c)(w) = (y:=b)(u) ∈ X(I-[y; z]))`

Lemma: face-compatible_wf
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f1,f2:I-face(X;I)].  (face-compatible(X;I;f1;f2) ∈ ℙ)`

Lemma: sq_stable__face-compatible
`∀X:CubicalSet. ∀I:Cname List. ∀f1,f2:I-face(X;I).  SqStable(face-compatible(X;I;f1;f2))`

Lemma: face-compatible-symmetry
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f1,f2:I-face(X;I)].  (face-compatible(X;I;f1;f2) `` face-compatible(X;I;f2;f1))`

Definition: A-face-compatible
`A-face-compatible(X;A;I;alpha;f1;f2) ==`
`  let y,b,w = f1 in `
`  let z,c,u = f2 in `
`  (¬(y = z ∈ Cname)) `` ((w (y:=b)(alpha) (z:=c)) = (u (z:=c)(alpha) (y:=b)) ∈ A(((z:=c) o (y:=b))(alpha)))`

Lemma: A-face-compatible_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[f1,f2:A-face(X;A;I;alpha)].`
`  (A-face-compatible(X;A;I;alpha;f1;f2) ∈ ℙ)`

`adjacent-compatible(X;I;L) ==  (∀f1,f2∈L.  face-compatible(X;I;f1;f2))`

`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[L:I-face(X;I) List].  (adjacent-compatible(X;I;L) ∈ ℙ)`

`∀[X:CubicalSet]`
`  ∀I:Cname List. ∀L:I-face(X;I) List.`
`    uiff(adjacent-compatible(X;I;L);∀f1,f2:I-face(X;I).`
`                                      ((f1 ∈ L)`
`                                      `` (f2 ∈ L)`
`                                      `` (¬(dimension(f1) = dimension(f2) ∈ Cname))`
`                                      `` ((dimension(f2):=direction(f2))(cube(f1))`
`                                         = (dimension(f1):=direction(f1))(cube(f2))`
`                                         ∈ X(I-[dimension(f1); dimension(f2)]))))`

`A-adjacent-compatible(X;A;I;alpha;L) ==  (∀f1,f2∈L.  A-face-compatible(X;A;I;alpha;f1;f2))`

`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[L:A-face(X;A;I;alpha) List].`
`  (A-adjacent-compatible(X;A;I;alpha;L) ∈ ℙ)`

Definition: is-face
`is-face(X;I;bx;f) ==  (dimension(f):=direction(f))(bx) = cube(f) ∈ X(I-[dimension(f)])`

Lemma: is-face_wf
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[bx:X(I)]. ∀[f:I-face(X;I)].  (is-face(X;I;bx;f) ∈ ℙ)`

Definition: is-A-face
`is-A-face(X;A;I;alpha;bx;f) ==  let y,b,w = f in (bx alpha (y:=b)) = w ∈ A((y:=b)(alpha))`

Lemma: is-A-face_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[bx:A(alpha)]. ∀[f:A-face(X;A;I;alpha)].`
`  (is-A-face(X;A;I;alpha;bx;f) ∈ ℙ)`

Definition: fills-faces
`fills-faces(X;I;bx;L) ==  (∀f∈L.is-face(X;I;bx;f))`

Lemma: fills-faces_wf
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[bx:X(I)]. ∀[L:I-face(X;I) List].  (fills-faces(X;I;bx;L) ∈ ℙ)`

Definition: fills-A-faces
`fills-A-faces(X;A;I;alpha;bx;L) ==  (∀f∈L.is-A-face(X;A;I;alpha;bx;f))`

Lemma: fills-A-faces_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[bx:A(alpha)]. ∀[L:A-face(X;A;I;alpha) List].`
`  (fills-A-faces(X;A;I;alpha;bx;L) ∈ ℙ)`

Definition: face-image
`face-image(X;I;K;f;face) ==  let x,b,w = face in <f x, b, f(w)>`

Lemma: face-image_wf
`∀[X:CubicalSet]. ∀[I,K:Cname List]. ∀[f:name-morph(I;K)]. ∀[face:I-face(X;I)].`
`  face-image(X;I;K;f;face) ∈ I-face(X;K) supposing ↑isname(f (fst(face)))`

Definition: A-face-image
`A-face-image(X;A;I;K;f;alpha;face) ==  let x,b,w = face in <f x, b, (w (x:=b)(alpha) f)>`

Lemma: A-face-image_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I,K:Cname List]. ∀[f:name-morph(I;K)]. ∀[alpha:X(I)]. ∀[face:A-face(X;A;I;alpha)].`
`  A-face-image(X;A;I;K;f;alpha;face) ∈ A-face(X;A;K;f(alpha)) supposing ↑isname(f (fst(face)))`

Lemma: face-compatible-image
`∀X:CubicalSet. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀fc1,fc2:I-face(X;I).`
`  ((↑isname(f (fst(fc1))))`
`  `` (↑isname(f (fst(fc2))))`
`  `` face-compatible(X;I;fc1;fc2)`
`  `` face-compatible(X;K;face-image(X;I;K;f;fc1);face-image(X;I;K;f;fc2)))`

Lemma: A-face-compatible-image
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀alpha:X(I). ∀fc1,fc2:A-face(X;A;I;alpha).`
`  ((↑isname(f (fst(fc1))))`
`  `` (↑isname(f (fst(fc2))))`
`  `` A-face-compatible(X;A;I;alpha;fc1;fc2)`
`  `` A-face-compatible(X;A;K;f(alpha);A-face-image(X;A;I;K;f;alpha;fc1);A-face-image(X;A;I;K;f;alpha;fc2)))`

Lemma: face-name-image
`∀X:CubicalSet. ∀I:Cname List. ∀K,f:Top. ∀face:I-face(X;I).`
`  (face-name(face-image(X;I;K;f;face)) ~ (λp.<f (fst(p)), snd(p)>) face-name(face))`

Lemma: A-face-name-image
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀I:Cname List. ∀alpha:X(I). ∀K,f:Top. ∀face:A-face(X;A;I;alpha).`
`  (A-face-name(A-face-image(X;A;I;K;f;alpha;face)) ~ (λp.<f (fst(p)), snd(p)>) A-face-name(face))`

Definition: open_box
`open_box(X;I;J;x;i) ==`
`  {L:I-face(X;I) List| `
`   adjacent-compatible(X;I;L)`
`   ∧ (¬(x ∈ J))`
`   ∧ l_subset(Cname;J;I)`
`   ∧ ((∀y:nameset(J). ∀c:ℕ2.  (∃f∈L. face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))`
`     ∧ (∃f∈L. face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))`
`     ∧ (∀f∈L.¬(face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))`
`   ∧ (∀f∈L.(fst(f) ∈ [x / J]))`
`   ∧ (∀f1,f2∈L.  ¬(face-name(f1) = face-name(f2) ∈ (nameset(I) × ℕ2)))} `

Lemma: open_box_wf
`∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2].  (open_box(X;I;J;x;i) ∈ Type)`

Lemma: open_box-nil
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`  open_box(X;I;[];x;i) ≡ {L:I-face(X;I) List| (||L|| = 1 ∈ ℤ) ∧ (face-name(hd(L)) = <x, i> ∈ (nameset(I) × ℕ2))} `

Lemma: length-open_box
`∀[X:CubicalSet]. ∀[I:Cname List].`
`  ∀J:nameset(I) List`
`    ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)].  (||box|| = (1 + (||remove-repeats(CnameDeq;J)|| * 2)) ∈ ℤ)`

Lemma: length-open_box-ge-3
`∀[X:CubicalSet]. ∀[I:Cname List].`
`  ∀J:nameset(I) List`
`    ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)].  (3 < ||box|| `` (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname))))`

Lemma: length-open_box-le-3
`∀[X:CubicalSet]. ∀[I:Cname List].`
`  ∀J:nameset(I) List`
`    ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)].  ((¬↑null(J)) `` (||box|| ≤ 3) `` (∀j'∈J.j' = hd(J) ∈ Cname))`

Lemma: non-trivial-open-box
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`  ∀bx:open_box(X;I;J;x;i). ∀y:nameset(J). ∀c:ℕ2.`
`    (¬(filter(λf.((dimension(f) =z y) ∧b (direction(f) =z c));bx)`
`    = []`
`    ∈ ({f:{f:I-face(X;I)| (f ∈ bx)} | ↑((dimension(f) =z y) ∧b (direction(f) =z c))}  List)))`

Definition: get_face
`get_face(y;c;box) ==  hd(filter(λf.((fst(f) =z y) ∧b (fst(snd(f)) =z c));box))`

Lemma: get_face_wf
`∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)]. ∀[y:nameset(J)]. ∀[c:ℕ2].`
`  (get_face(y;c;box) ∈ {f:I-face(X;I)| (f ∈ box) ∧ (face-name(f) = <y, c> ∈ (nameset(I) × ℕ2))} )`

Lemma: get_face-wf
`∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)].`
`  (get_face(x;i;box) ∈ {f:I-face(X;I)| (f ∈ box) ∧ (face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))} )`

Lemma: get_face-dimension
`∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)]. ∀[y:nameset(J)]. ∀[c:ℕ2].`
`  (dimension(get_face(y;c;box)) ~ y)`

Lemma: get_face-direction
`∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(X;I;J;x;i)]. ∀[y:nameset(J)]. ∀[c:ℕ2].`
`  (direction(get_face(y;c;box)) ~ c)`

Lemma: get_face_unique
`∀X:CubicalSet. ∀I:Cname List. ∀f:I-face(X;I). ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀box:open_box(X;I;J;x;i).`
`  ((f ∈ box) `` (get_face(dimension(f);direction(f);box) = f ∈ I-face(X;I)))`

Definition: A-open-box
`A-open-box(X;A;I;alpha;J;x;i) ==`
`  {L:A-face(X;A;I;alpha) List| `
`   A-adjacent-compatible(X;A;I;alpha;L)`
`   ∧ (¬(x ∈ J))`
`   ∧ l_subset(Cname;J;I)`
`   ∧ ((∀y:nameset(J). ∀c:ℕ2.  (∃f∈L. A-face-name(f) = <y, c> ∈ (nameset(I) × ℕ2)))`
`     ∧ (∃f∈L. A-face-name(f) = <x, i> ∈ (nameset(I) × ℕ2))`
`     ∧ (∀f∈L.¬(A-face-name(f) = <x, 1 - i> ∈ (nameset(I) × ℕ2))))`
`   ∧ (∀f∈L.(fst(f) ∈ [x / J]))`
`   ∧ (∀f1,f2∈L.  ¬(A-face-name(f1) = A-face-name(f2) ∈ (nameset(I) × ℕ2)))} `

Lemma: A-open-box_wf
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀I:Cname List. ∀alpha:X(I).`
`  ∀[J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2].  (A-open-box(X;A;I;alpha;J;x;i) ∈ Type)`

Lemma: A-open-box-equal
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀I:Cname List. ∀alpha:X(I).`
`  ∀[J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[bx1:A-open-box(X;A;I;alpha;J;x;i)]. ∀[bx2:A-face(X;A;I;alpha) List].`
`    bx1 = bx2 ∈ A-open-box(X;A;I;alpha;J;x;i) supposing bx1 = bx2 ∈ (A-face(X;A;I;alpha) List)`

Lemma: constant-A-open-box
`∀Gamma,X,I,alpha:Top.  ∀[J,x,i:Top].  (A-open-box(Gamma;(X);I;alpha;J;x;i) ~ open_box(X;I;J;x;i))`

Definition: extend-A-open-box
`extend-A-open-box(bx;f1;f2) ==  [f1; [f2 / bx]]`

Lemma: extend-A-open-box_wf
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀I:Cname List. ∀alpha:X(I).`
`  ∀[J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[bx:A-open-box(X;A;I;alpha;J;x;i)]. ∀[f1,f2:A-face(X;A;I;alpha)].`
`  ∀[z:nameset(I)].`
`    extend-A-open-box(bx;f1;f2) ∈ A-open-box(X;A;I;alpha;[z / J];x;i) `
`    supposing ((¬(z ∈ J))`
`              ∧ (A-face-name(f1) = <z, 0> ∈ (nameset(I) × ℕ2))`
`              ∧ (A-face-name(f2) = <z, 1> ∈ (nameset(I) × ℕ2)))`
`    ∧ (¬(x = z ∈ Cname))`
`    ∧ (∀f∈bx.A-face-compatible(X;A;I;alpha;f1;f) ∧ A-face-compatible(X;A;I;alpha;f2;f))`

Lemma: csm-A-open-box
`∀Delta,Gamma:CubicalSet. ∀s:Delta ⟶ Gamma. ∀A:{Gamma ⊢ _}. ∀I:Cname List. ∀alpha:Delta(I). ∀J:nameset(I) List.`
`∀x:nameset(I). ∀i:ℕ2.`
`  (A-open-box(Delta;(A)s;I;alpha;J;x;i) ⊆r A-open-box(Gamma;A;I;(s)alpha;J;x;i))`

Definition: open_box_image
`open_box_image(X;I;K;f;bx) ==  map(λface.face-image(X;I;K;f;face);bx)`

Lemma: open_box_image_wf
`∀[X:CubicalSet]. ∀[I,J,K:Cname List]. ∀[f:name-morph(I;K)]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`  ∀[bx:open_box(X;I;J;x;i)]. (open_box_image(X;I;K;f;bx) ∈ open_box(X;K;map(f;J);f x;i)) `
`  supposing nameset([x / J]) ⊆r name-morph-domain(f;I)`

Lemma: length-open_box_image
`∀[X,I,K,f,bx:Top].  (||open_box_image(X;I;K;f;bx)|| ~ ||bx||)`

Lemma: get_face_image
`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[bx:open_box(X;I;J;x;i)].`
`∀[K:Cname List]. ∀[f:name-morph(I;K)]. ∀[c:ℕ2]. ∀[y:nameset(J)].`
`  get_face(f y;c;open_box_image(X;I;K;f;bx)) = face-image(X;I;K;f;get_face(y;c;bx)) ∈ I-face(X;K) `
`  supposing nameset([x / J]) ⊆r name-morph-domain(f;I)`

Definition: A-open-box-image
`A-open-box-image(X;A;I;K;f;alpha;bx) ==  map(λface.A-face-image(X;A;I;K;f;alpha;face);bx)`

Lemma: A-open-box-image_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I,J,K:Cname List]. ∀[alpha:X(I)]. ∀[f:name-morph(I;K)]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`  ∀[bx:A-open-box(X;A;I;alpha;J;x;i)]`
`    (A-open-box-image(X;A;I;K;f;alpha;bx) ∈ A-open-box(X;A;K;f(alpha);map(f;J);f x;i)) `
`  supposing nameset([x / J]) ⊆r name-morph-domain(f;I)`

Definition: fills-open_box
`fills-open_box(X;I;bx;cube) ==  fills-faces(X;I;cube;bx)`

Lemma: fills-open_box_wf
`∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`  ∀[bx:open_box(X;I;J;x;i)]. ∀[cube:X(I)].  (fills-open_box(X;I;bx;cube) ∈ ℙ) supposing l_subset(Cname;J;I)`

Definition: fills-A-open-box
`fills-A-open-box(X;A;I;alpha;bx;cube) ==  fills-A-faces(X;A;I;alpha;cube;bx)`

Lemma: fills-A-open-box_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[cube:A(alpha)]. ∀[bx:A-open-box(X;A;I;alpha;J;x;i)].`
`  fills-A-open-box(X;A;I;alpha;bx;cube) ∈ ℙ supposing l_subset(Cname;J;I)`

Lemma: sq_stable_fills-A-open-box
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[cube:A(alpha)].`
`  ∀bx:A-open-box(X;A;I;alpha;J;x;i). SqStable(fills-A-open-box(X;A;I;alpha;bx;cube)) supposing l_subset(Cname;J;I)`

Definition: Kan-A-filler
`Kan-A-filler(X;A;filler) ==`
`  ∀I:Cname List. ∀alpha:X(I). ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(X;A;I;alpha;J;x;i).`
`    fills-A-open-box(X;A;I;alpha;bx;filler I alpha J x i bx)`

Lemma: Kan-A-filler_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[filler:I:(Cname List)`
`                                        ⟶ alpha:X(I)`
`                                        ⟶ J:(nameset(I) List)`
`                                        ⟶ x:nameset(I)`
`                                        ⟶ i:ℕ2`
`                                        ⟶ A-open-box(X;A;I;alpha;J;x;i)`
`                                        ⟶ A(alpha)].`
`  (Kan-A-filler(X;A;filler) ∈ ℙ)`

Lemma: sq_stable_Kan-A-filler
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[filler:I:(Cname List)`
`                                        ⟶ alpha:X(I)`
`                                        ⟶ J:(nameset(I) List)`
`                                        ⟶ x:nameset(I)`
`                                        ⟶ i:ℕ2`
`                                        ⟶ A-open-box(X;A;I;alpha;J;x;i)`
`                                        ⟶ A(alpha)].`
`  SqStable(Kan-A-filler(X;A;filler))`

Definition: uniform-Kan-A-filler
`uniform-Kan-A-filler(X;A;filler) ==`
`  ∀I:Cname List. ∀alpha:X(I). ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(X;A;I;alpha;J;x;i).`
`  ∀K:Cname List. ∀f:name-morph(I;K).`
`    ((∀i:nameset(I). ((i ∈ J) `` (↑isname(f i))))`
`    `` (↑isname(f x))`
`    `` ((filler I alpha J x i bx alpha f)`
`       = (filler K f(alpha) map(f;J) (f x) i A-open-box-image(X;A;I;K;f;alpha;bx))`
`       ∈ A(f(alpha))))`

Lemma: uniform-Kan-A-filler_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[filler:I:(Cname List)`
`                                        ⟶ alpha:X(I)`
`                                        ⟶ J:(nameset(I) List)`
`                                        ⟶ x:nameset(I)`
`                                        ⟶ i:ℕ2`
`                                        ⟶ A-open-box(X;A;I;alpha;J;x;i)`
`                                        ⟶ A(alpha)].`
`  (uniform-Kan-A-filler(X;A;filler) ∈ ℙ)`

Lemma: sq_stable_uniform-Kan-A-filler
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[filler:I:(Cname List)`
`                                        ⟶ alpha:X(I)`
`                                        ⟶ J:(nameset(I) List)`
`                                        ⟶ x:nameset(I)`
`                                        ⟶ i:ℕ2`
`                                        ⟶ A-open-box(X;A;I;alpha;J;x;i)`
`                                        ⟶ A(alpha)].`
`  SqStable(uniform-Kan-A-filler(X;A;filler))`

Definition: Kan-cubical-type
`{X ⊢ _(Kan)} ==`
`  {p:A:{X ⊢ _} × (I:(Cname List)`
`                 ⟶ alpha:X(I)`
`                 ⟶ J:(nameset(I) List)`
`                 ⟶ x:nameset(I)`
`                 ⟶ i:ℕ2`
`                 ⟶ A-open-box(X;A;I;alpha;J;x;i)`
`                 ⟶ A(alpha))| `
`   let A,filler = p `
`   in Kan-A-filler(X;A;filler) ∧ uniform-Kan-A-filler(X;A;filler)} `

Lemma: Kan-cubical-type_wf
`∀[X:CubicalSet]. ({X ⊢ _(Kan)} ∈ 𝕌')`

Definition: Kan-type
`Kan-type(Ak) ==  fst(Ak)`

Lemma: Kan-type_wf
`∀[X:CubicalSet]. ∀[AK:{X ⊢ _(Kan)}].  X ⊢ Kan-type(AK)`

Definition: Kanfiller
`filler(x;i;bx) ==  (snd(A)) I alpha J x i bx`

Lemma: Kanfiller_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _(Kan)}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[bx:A-open-box(X;Kan-type(A);I;alpha;J;x;i)].`
`  (filler(x;i;bx) ∈ {cube:Kan-type(A)(alpha)| fills-A-open-box(X;Kan-type(A);I;alpha;bx;cube)} )`

Lemma: Kanfiller-uniform
`∀[X:CubicalSet]. ∀[A:{X ⊢ _(Kan)}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[bx:A-open-box(X;Kan-type(A);I;alpha;J;x;i)].`
`  ∀K:Cname List. ∀f:name-morph(I;K).`
`    ((∀i:nameset(I). ((i ∈ J) `` (↑isname(f i))))`
`    `` (↑isname(f x))`
`    `` ((filler(x;i;bx) alpha f)`
`       = filler(f x;i;A-open-box-image(X;Kan-type(A);I;K;f;alpha;bx))`
`       ∈ Kan-type(A)(f(alpha))))`

Lemma: Kan-cubical-type-equal
`∀[X:CubicalSet]. ∀[A:{X ⊢ _(Kan)}]. ∀[B:A:{X ⊢ _} × (I:(Cname List)`
`                                                    ⟶ alpha:X(I)`
`                                                    ⟶ J:(nameset(I) List)`
`                                                    ⟶ x:nameset(I)`
`                                                    ⟶ i:ℕ2`
`                                                    ⟶ A-open-box(X;A;I;alpha;J;x;i)`
`                                                    ⟶ A(alpha))].`
`  A = B ∈ {X ⊢ _(Kan)} `
`  supposing A`
`  = B`
`  ∈ (A:{X ⊢ _} × (I:(Cname List)`
`                 ⟶ alpha:X(I)`
`                 ⟶ J:(nameset(I) List)`
`                 ⟶ x:nameset(I)`
`                 ⟶ i:ℕ2`
`                 ⟶ A-open-box(X;A;I;alpha;J;x;i)`
`                 ⟶ A(alpha)))`

Definition: csm-Kan-cubical-type
`(AK)s ==  let A,filler = AK in <(A)s, λI,alpha. (filler I (s)alpha)>`

Lemma: csm-Kan-cubical-type_wf
`∀[Delta,Gamma:CubicalSet]. ∀[s:Delta ⟶ Gamma]. ∀[AK:{Gamma ⊢ _(Kan)}].  ((AK)s ∈ {Delta ⊢ _(Kan)})`

Lemma: type-csm-Kan-cubical-type
`∀[Gamma:CubicalSet]. ∀[s:Top]. ∀[AK:{Gamma ⊢ _(Kan)}].  (Kan-type((AK)s) ~ (Kan-type(AK))s)`

Lemma: csm-Kan-id
`∀[Gamma:CubicalSet]. ∀[AK:{Gamma ⊢ _(Kan)}].  ((AK)1(Gamma) = AK ∈ {Gamma ⊢ _(Kan)})`

Lemma: csm-Kan-comp
`∀[Gamma,Delta,Z:CubicalSet]. ∀[s1:Z ⟶ Delta]. ∀[s2:Delta ⟶ Gamma]. ∀[AK:{Gamma ⊢ _(Kan)}].`
`  ((AK)s2 o s1 = ((AK)s2)s1 ∈ {Z ⊢ _(Kan)})`

Lemma: csm-Kan-unit-cube-id
`∀I:Cname List. ∀x:{unit-cube(I) ⊢ _(Kan)}.  ((x)unit-cube-map(1) = x ∈ {unit-cube(I) ⊢ _(Kan)})`

Lemma: csm-Kan-unit-cube-comp
`∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀x:{unit-cube(I) ⊢ _(Kan)}.`
`  ((x)unit-cube-map((f o g)) = ((x)unit-cube-map(f))unit-cube-map(g) ∈ {unit-cube(K) ⊢ _(Kan)})`

Definition: sigma-box-fst
`sigma-box-fst(bx) ==  map(λfc.<fst(fc), fst(snd(fc)), fst(snd(snd(fc)))>;bx)`

Lemma: sigma-box-fst_wf
`∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀B:{X.Kan-type(A) ⊢ _(Kan)}. ∀I:Cname List. ∀alpha:X(I). ∀J:nameset(I) List.`
`∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i).`
`  (sigma-box-fst(bx) ∈ A-open-box(X;Kan-type(A);I;alpha;J;x;i))`

Definition: sigma-box-snd
`sigma-box-snd(bx) ==  map(λfc.<fst(fc), fst(snd(fc)), snd(snd(snd(fc)))>;bx)`

Lemma: sigma-box-snd_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _(Kan)}]. ∀[B:{X.Kan-type(A) ⊢ _(Kan)}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[J:nameset(I) List].`
`∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[bx:A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)]. ∀[cbA:Kan-type(A)(alpha)].`
`  sigma-box-snd(bx) ∈ A-open-box(X.Kan-type(A);Kan-type(B);I;(alpha;cbA);J;x;i) `
`  supposing fills-A-open-box(X;Kan-type(A);I;alpha;sigma-box-fst(bx);cbA)`

Definition: Kan_sigma_filler
`Kan_sigma_filler(A;B) ==`
`  λI,alpha,J,x,i,bx. let cubeA = filler(x;i;sigma-box-fst(bx)) in`
`                      let cubeB = filler(x;i;sigma-box-snd(bx)) in`
`                      <cubeA, cubeB>`

Lemma: Kan_sigma_filler_wf
`∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀B:{X.Kan-type(A) ⊢ _(Kan)}.`
`  (Kan_sigma_filler(A;B) ∈ {filler:I:(Cname List)`
`                            ⟶ alpha:X(I)`
`                            ⟶ J:(nameset(I) List)`
`                            ⟶ x:nameset(I)`
`                            ⟶ i:ℕ2`
`                            ⟶ A-open-box(X;Σ Kan-type(A) Kan-type(B);I;alpha;J;x;i)`
`                            ⟶ Σ Kan-type(A) Kan-type(B)(alpha)| `
`                            Kan-A-filler(X;Σ Kan-type(A) Kan-type(B);filler)} )`

Lemma: Kan_sigma_filler_uniform
`∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀B:{X.Kan-type(A) ⊢ _(Kan)}.`
`  uniform-Kan-A-filler(X;Σ Kan-type(A) Kan-type(B);Kan_sigma_filler(A;B))`

Definition: Kan-cubical-sigma
`KanΣ A B ==  <Σ Kan-type(A) Kan-type(B), Kan_sigma_filler(A;B)>`

Lemma: Kan-cubical-sigma_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _(Kan)}]. ∀[B:{X.Kan-type(A) ⊢ _(Kan)}].  (KanΣ A B ∈ {X ⊢ _(Kan)})`

Lemma: csm-Kan-cubical-sigma
`∀[X,Delta:CubicalSet]. ∀[s:Delta ⟶ X]. ∀[A:{X ⊢ _(Kan)}]. ∀[B:{X.Kan-type(A) ⊢ _(Kan)}].`
`  ((KanΣ A B)s = KanΣ (A)s (B)(s o p;q) ∈ {Delta ⊢ _(Kan)})`

Definition: Kan-discrete
`Kan-discrete(T) ==  <discr(T), λI,alpha,J,x,i,bx. (snd(snd(hd(bx))))>`

Lemma: Kan-discrete_wf
`∀[X:CubicalSet]. ∀[T:Type].  (Kan-discrete(T) ∈ {X ⊢ _(Kan)})`

Definition: Kan-filler
`Kan-filler(X;filler) ==`
`  ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X;I;J;x;i).`
`    fills-open_box(X;I;bx;filler I J x i bx)`

Lemma: Kan-filler_wf
`∀[X:CubicalSet]. ∀[filler:I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X;I;J;x;i) ⟶ X(I)].`
`  (Kan-filler(X;filler) ∈ ℙ)`

Definition: uniform-Kan-filler
`uniform-Kan-filler(X;filler) ==`
`  ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X;I;J;x;i). ∀K:Cname List. ∀f:name-morph(I;K).`
`    ((∀i:nameset(I). ((i ∈ J) `` (↑isname(f i))))`
`    `` (↑isname(f x))`
`    `` (f(filler I J x i bx) = (filler K map(f;J) (f x) i open_box_image(X;I;K;f;bx)) ∈ X(K)))`

Lemma: uniform-Kan-filler_wf
`∀[X:CubicalSet]. ∀[filler:I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X;I;J;x;i) ⟶ X(I)].`
`  (uniform-Kan-filler(X;filler) ∈ ℙ)`

Definition: Kan-cubical-set
`KanCubicalSet ==`
`  {p:X:CubicalSet × (I:(Cname List) ⟶ J:(nameset(I) List) ⟶ x:nameset(I) ⟶ i:ℕ2 ⟶ open_box(X;I;J;x;i) ⟶ X(I))| `
`   let X,filler = p `
`   in Kan-filler(X;filler) ∧ uniform-Kan-filler(X;filler)} `

Lemma: Kan-cubical-set_wf
`KanCubicalSet ∈ 𝕌'`

Definition: constant-Kan-type
`constant-Kan-type(X) ==  let S,filler = X in <(S), λI,alpha. (filler I)>`

Lemma: constant-Kan-type_wf
`∀[X:KanCubicalSet]. ∀[Gamma:CubicalSet].  (constant-Kan-type(X) ∈ {Gamma ⊢ _(Kan)})`

Definition: cubical-interval-ap
`u(L) ==  u L`

Lemma: cubical-interval-ap_wf
`∀[I:Cname List]. ∀[u:cubical-interval()(I)]. ∀[L:name-morph(I;[])].  (u(L) ∈ ℕ2)`

Lemma: cubical-interval-non-trivial-box
`∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`  ∀bx:open_box(cubical-interval();I;J;x;i). ∀h:name-morph(I;[]).`
`    ((¬(J = [] ∈ (nameset(I) List)))`
`    `` (¬(filter(λf.(h (fst(f)) =z fst(snd(f)));bx)`
`       = []`
`       ∈ ({x:{f:I-face(cubical-interval();I)| (f ∈ bx)} | ↑(h (fst(x)) =z fst(snd(x)))}  List))))`

Definition: cubical-interval-filler
`cubical-interval-filler() ==  λI,J,x,i,bx. if null(J) then cube(hd(bx)) else λL.cube(get_face(hd(J);L hd(J);bx))(L) fi `

Lemma: cubical-interval-filler_wf
`cubical-interval-filler() ∈ I:(Cname List)`
`⟶ J:(nameset(I) List)`
`⟶ x:nameset(I)`
`⟶ i:ℕ2`
`⟶ open_box(cubical-interval();I;J;x;i)`
`⟶ cubical-interval()(I)`

Lemma: cubical-interval-filler-fills
`Kan-filler(cubical-interval();cubical-interval-filler())`

Definition: Kan-interval
`Kan-interval() ==  <cubical-interval(), cubical-interval-filler()>`

Lemma: Kan-interval_wf
`Kan-interval() ∈ KanCubicalSet`

Definition: poset-cat
`poset-cat(J) ==  <name-morph(J;[]), λf,g. ∀x:nameset(J). (↑f x ≤z g x), λf,x. Ax, λf,g,h,p,q,x. Ax>`

Lemma: poset-cat_wf
`∀[J:Cname List]. (poset-cat(J) ∈ SmallCategory)`

Lemma: poset-cat-ob_subtype
`∀[I,J:Cname List].  cat-ob(poset-cat(I)) ⊆r cat-ob(poset-cat(J)) supposing nameset(J) ⊆r nameset(I)`

Lemma: poset-cat-arrow_subtype
`∀[I,J:Cname List].`
`  ∀[x,y:cat-ob(poset-cat(I))].  ((cat-arrow(poset-cat(I)) x y) ⊆r (cat-arrow(poset-cat(J)) x y)) `
`  supposing nameset(J) ⊆r nameset(I)`

Lemma: poset-cat-arrow-unique
`∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))]. ∀[a,b:cat-arrow(poset-cat(I)) x y].`
`  (a = b ∈ (cat-arrow(poset-cat(I)) x y))`

Lemma: poset-cat-arrow-flip
`∀I:Cname List. ∀x:cat-ob(poset-cat(I)). ∀a:nameset(I).  (((x a) = 0 ∈ ℤ) `` (cat-arrow(poset-cat(I)) x flip(x;a)))`

Lemma: poset-cat-arrow-iff
`∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))].  uiff(cat-arrow(poset-cat(I)) x y;{∀i:nameset(I). ((x i) ≤ (y i))})`

Lemma: poset-cat-arrow-equals
`∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))]. ∀[a:cat-arrow(poset-cat(I)) x y].`
`  (a = (λx.Ax) ∈ (cat-arrow(poset-cat(I)) x y))`

Lemma: member-poset-cat-arrow
`∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))].  λx.Ax ∈ cat-arrow(poset-cat(I)) x y supposing cat-arrow(poset-cat(I)) x y`

Lemma: poset-cat-arrow-not-equal
`∀I:Cname List. ∀y:nameset(I). ∀c1,c2:cat-ob(poset-cat(I)).`
`  (c1 y ≠ c2 y `` (∀f:cat-arrow(poset-cat(I)) c1 c2. (((c1 y) = 0 ∈ ℕ2) ∧ ((c2 y) = 1 ∈ ℕ2))))`

Lemma: poset-cat-ob-cases
`∀I:Cname List. ∀c1,c2:cat-ob(poset-cat(I)).  ((c1 = c2 ∈ cat-ob(poset-cat(I))) ∨ (∃y:nameset(I). c1 y ≠ c2 y))`

Lemma: decidable__equal-poset-cat-ob
`∀I:Cname List. ∀c1,c2:cat-ob(poset-cat(I)).  Dec(c1 = c2 ∈ cat-ob(poset-cat(I)))`

Lemma: poset-cat-arrow-cases
`∀I:Cname List. ∀c1,c2:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) c1 c2.`
`  ((c1 = c2 ∈ cat-ob(poset-cat(I)))`
`  ∨ (∃y:{y:nameset(I)| (c1 y) = 0 ∈ ℕ2} . (c2 = flip(c1;y) ∈ cat-ob(poset-cat(I))))`
`  ∨ (∃c3:cat-ob(poset-cat(I))`
`      ∃g:cat-arrow(poset-cat(I)) c1 c3`
`       ∃h:cat-arrow(poset-cat(I)) c3 c2. ((¬(c1 = c3 ∈ cat-ob(poset-cat(I)))) ∧ (¬(c2 = c3 ∈ cat-ob(poset-cat(I)))))))`

Lemma: poset-cat-arrow-filter-nil
`∀I:Cname List. ∀J:nameset(I) List. ∀c1,c2:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) c1 c2.`
`  ((filter(λz.(c1 z =z c2 z);J) = [] ∈ ({x:nameset(J)| ↑(c1 x =z c2 x)}  List))`
`  `` (∀j∈J.((c1 j) = 0 ∈ ℕ2) ∧ ((c2 j) = 1 ∈ ℕ2)))`

Definition: poset-cat-dist
`poset-cat-dist(I;x;y) ==  ||filter(λi.((x i =z 0) ∧b (y i =z 1));I)||`

Lemma: poset-cat-dist_wf
`∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))].  (poset-cat-dist(I;x;y) ∈ ℕ)`

`∀[I:Cname List]. ∀[x,y,z:cat-ob(poset-cat(I))].`
`  (poset-cat-dist(I;x;z) = (poset-cat-dist(I;x;y) + poset-cat-dist(I;y;z)) ∈ ℤ) supposing `
`     ((cat-arrow(poset-cat(I)) x y) and `
`     (cat-arrow(poset-cat(I)) y z))`

Lemma: poset-cat-dist-zero
`∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))].`
`  uiff(x = y ∈ cat-ob(poset-cat(I));poset-cat-dist(I;x;y) ≤ 0) supposing cat-arrow(poset-cat(I)) x y`

Lemma: poset-cat-dist-non-zero
`∀[I:Cname List]. ∀[x,y:cat-ob(poset-cat(I))].`
`  (null(filter(λx1.((x x1 =z 0) ∧b (y x1 =z 1));I)) ~ ff) supposing `
`     ((¬(x = y ∈ cat-ob(poset-cat(I)))) and `
`     (cat-arrow(poset-cat(I)) x y))`

Lemma: poset-cat-dist-flip
`∀I:Cname List. ∀x:cat-ob(poset-cat(I)). ∀a:nameset(I).  (((x a) = 0 ∈ ℤ) `` (1 ≤ poset-cat-dist(I;x;flip(x;a))))`

Definition: poset-functor
`poset-functor(J;K;f) ==  <λg.(f o g), λg,h,p,x. Ax>`

Lemma: poset-functor_wf
`∀[J,K:Cname List]. ∀[f:name-morph(J;K)].  (poset-functor(J;K;f) ∈ Functor(poset-cat(K);poset-cat(J)))`

Lemma: poset-functor-comp
`∀[I,J,K:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)].`
`  (poset-functor(I;K;(f o g))`
`  = functor-comp(poset-functor(J;K;g);poset-functor(I;J;f))`
`  ∈ Functor(poset-cat(K);poset-cat(I)))`

Lemma: poset-id-functor
`∀[I:Cname List]. (poset-functor(I;I;1) = 1 ∈ Functor(poset-cat(I);poset-cat(I)))`

Lemma: poset-functor-id
`∀[I:Cname List]. ∀[f:name-morph(I;I)].`
`  poset-functor(I;I;f) = 1 ∈ Functor(poset-cat(I);poset-cat(I)) supposing f = 1 ∈ name-morph(I;I)`

Lemma: name-morph-flip-id
`∀I:Cname List. ∀x:nameset(I). ∀c2:cat-ob(poset-cat(I)).  (c2 = flip(c2;x) ∈ cat-ob(poset-cat(I-[x])))`

Definition: poset_functor_extend
`poset_functor_extend(C;I;L;E;c1;c2)`
`==r eval d = filter(λx.((c1 x =z 0) ∧b (c2 x =z 1));I) in`
`    if null(d)`
`    then cat-id(C) (L c1)`
`    else cat-comp(C) (L c1) (L flip(c1;hd(d))) (L c2) (E hd(d) c1) poset_functor_extend(C;I;L;E;flip(c1;hd(d));c2)`
`    fi `

Lemma: poset_functor_extend_wf
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[L:name-morph(I;[]) ⟶ cat-ob(C)]. ∀[E:i:nameset(I)`
`                                                                             ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                             ⟶ (cat-arrow(C) (L c) (L flip(c;i)))].`
`∀[c1,c2:name-morph(I;[])].`
`  poset_functor_extend(C;I;L;E;c1;c2) ∈ cat-arrow(C) (L c1) (L c2) supposing ∀x:nameset(I). ((c1 x) ≤ (c2 x))`

Lemma: poset_functor_extend-face-map1
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[L:name-morph(I;[]) ⟶ cat-ob(C)]. ∀[E:i:nameset(I)`
`                                                                             ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                             ⟶ (cat-arrow(C) (L c) (L flip(c;i)))].`
`∀[y:nameset(I)]. ∀[a:ℕ2]. ∀[c1,c2:name-morph(I;[])].`
`  poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))`
`  = poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));c1;c2)`
`  ∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2))) `
`  supposing ∀x:nameset(I). ((c1 x) ≤ (c2 x))`

Lemma: poset_functor_extend-face-map
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[L:name-morph(I;[]) ⟶ cat-ob(C)]. ∀[E:i:nameset(I)`
`                                                                             ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                             ⟶ (cat-arrow(C) (L c) (L flip(c;i)))].`
`∀[y:nameset(I)]. ∀[a:ℕ2]. ∀[c1,c2:name-morph(I-[y];[])].`
`  poset_functor_extend(C;I;L;E;((y:=a) o c1);((y:=a) o c2))`
`  = poset_functor_extend(C;I-[y];L o (λf.((y:=a) o f));λz,f. (E z ((y:=a) o f));c1;c2)`
`  ∈ (cat-arrow(C) (L ((y:=a) o c1)) (L ((y:=a) o c2))) `
`  supposing ∀x:nameset(I-[y]). ((c1 x) ≤ (c2 x))`

Lemma: poset_functor_extend_id
`∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)`
`                                                                      ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                      ⟶ (cat-arrow(C) (L c) (L flip(c;i))).`
`∀x:cat-ob(poset-cat(I)).`
`  (poset_functor_extend(C;I;L;E;x;x) = (cat-id(C) (L x)) ∈ (cat-arrow(C) (L x) (L x)))`

Lemma: poset_functor_extend_same
`∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)`
`                                                                      ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                      ⟶ (cat-arrow(C) (L c) (L flip(c;i))).`
`∀x:cat-ob(poset-cat(I)).`
`  ∀[y:cat-ob(poset-cat(I))]`
`    poset_functor_extend(C;I;L;E;x;y) = (cat-id(C) (L x)) ∈ (cat-arrow(C) (L x) (L x)) `
`    supposing x = y ∈ cat-ob(poset-cat(I))`

Definition: poset-functor-extends
`poset-functor-extends(C;I;L;E;F) ==`
`  (ob(F) = L ∈ (name-morph(I;[]) ⟶ cat-ob(C)))`
`  ∧ (∀i:nameset(I). ∀c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} .`
`       ((F c flip(c;i) (λx.Ax)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i)))))`

Lemma: poset-functor-extends_wf
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[L:name-morph(I;[]) ⟶ cat-ob(C)]. ∀[E:i:nameset(I)`
`                                                                             ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                             ⟶ (cat-arrow(C) (L c) (L flip(c;i)))].`
`∀[F:Functor(poset-cat(I);C)].`
`  (poset-functor-extends(C;I;L;E;F) ∈ ℙ)`

Lemma: poset_functor_extend-extends
`∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)`
`                                                                      ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                      ⟶ (cat-arrow(C) (L c) (L flip(c;i))).`
`  poset-functor-extends(C;I;L;E;<L, λc1,c2,p. poset_functor_extend(C;I;L;E;c1;c2)>)`

Lemma: poset_functor_extend-flip
`∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)`
`                                                                      ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                      ⟶ (cat-arrow(C) (L c) (L flip(c;i))).`
`∀i:nameset(I). ∀c:cat-ob(poset-cat(I)).`
`  poset_functor_extend(C;I;L;E;c;flip(c;i)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i))) supposing (c i) = 0 ∈ ℕ2`

Definition: edge-arrows-commute
`edge-arrows-commute(C;I;L;E) ==`
`  ∀x:name-morph(I;[]). ∀i,j:{i:nameset(I)| (x i) = 0 ∈ ℕ2} .`
`    ((¬(i = j ∈ nameset(I)))`
`    `` ((cat-comp(C) (L x) (L flip(x;i)) (L flip(flip(x;i);j)) (E i x) (E j flip(x;i)))`
`       = (cat-comp(C) (L x) (L flip(x;j)) (L flip(flip(x;j);i)) (E j x) (E i flip(x;j)))`
`       ∈ (cat-arrow(C) (L x) (L flip(flip(x;i);j)))))`

Lemma: edge-arrows-commute_wf
`∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)`
`                                                                      ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                      ⟶ (cat-arrow(C) (L c) (L flip(c;i))).`
`  (edge-arrows-commute(C;I;L;E) ∈ ℙ)`

Lemma: poset_functor_extend-is-functor
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[L:name-morph(I;[]) ⟶ cat-ob(C)]. ∀[E:i:nameset(I)`
`                                                                             ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                             ⟶ (cat-arrow(C) (L c) (L flip(c;i)))].`
`  <L, λc1,c2,p. poset_functor_extend(C;I;L;E;c1;c2)> ∈ Functor(poset-cat(I);C) supposing edge-arrows-commute(C;I;L;E)`

Lemma: poset-extend-unique
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[L:name-morph(I;[]) ⟶ cat-ob(C)]. ∀[E:i:nameset(I)`
`                                                                             ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                             ⟶ (cat-arrow(C) (L c) (L flip(c;i)))].`
`∀[F,G:Functor(poset-cat(I);C)].`
`  (F = G ∈ Functor(poset-cat(I);C)) supposing (poset-functor-extends(C;I;L;E;G) and poset-functor-extends(C;I;L;E;F))`

Lemma: unique-poset-functor
`∀C:SmallCategory. ∀I:Cname List. ∀L:name-morph(I;[]) ⟶ cat-ob(C). ∀E:i:nameset(I)`
`                                                                      ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} `
`                                                                      ⟶ (cat-arrow(C) (L c) (L flip(c;i))).`
`  (edge-arrows-commute(C;I;L;E) `` (∃!F:Functor(poset-cat(I);C). poset-functor-extends(C;I;L;E;F)))`

Lemma: poset-functors-equal
`∀C:SmallCategory. ∀I:Cname List. ∀F,G:Functor(poset-cat(I);C).`
`  (F = G ∈ Functor(poset-cat(I);C)`
`  `⇐⇒` (∀f:name-morph(I;[]). ((F f) = (G f) ∈ cat-ob(C)))`
`      ∧ (∀x:nameset(I). ∀f:{f:name-morph(I;[])| (f x) = 0 ∈ ℕ2} .`
`           ((F f flip(f;x) (λx.Ax)) = (G f flip(f;x) (λx.Ax)) ∈ (cat-arrow(C) (F f) (F flip(f;x))))))`

Definition: cubical-nerve
`cubical-nerve(X) ==  <λJ.Functor(poset-cat(J);X), λI,J,f,F. functor-comp(poset-functor(I;J;f);F)>`

Lemma: cubical-nerve_wf
`∀[X:SmallCategory]. (cubical-nerve(X) ∈ CubicalSet)`

Lemma: cubical-nerve-I-cube
`∀[X,I:Top].  (cubical-nerve(X)(I) ~ Functor(poset-cat(I);X))`

Lemma: face-compatible-cubical-nerve1
`∀[C:SmallCategory]. ∀[I:Cname List].`
`  ∀f1,f2:I-face(cubical-nerve(C);I).`
`    (face-compatible(cubical-nerve(C);I;f1;f2) ~ (¬((fst(f1)) = (fst(f2)) ∈ Cname))`
`    `` (functor-comp(poset-functor(I-[fst(f1)];I-[fst(f1); fst(f2)];(fst(f2):=fst(snd(f2))));snd(snd(f1)))`
`       = functor-comp(poset-functor(I-[fst(f2)];I-[fst(f1); fst(f2)];(fst(f1):=fst(snd(f1))));snd(snd(f2)))`
`       ∈ Functor(poset-cat(I-[fst(f1); fst(f2)]);C)))`

Definition: nerve-box-face
`nerve-box-face(box;L) ==  hd(filter(λf.(direction(f) =z L dimension(f));box))`

Lemma: nerve-box-face_wf
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[L:cat-ob(poset-cat(I))].`
`  nerve-box-face(box;L) ∈ {f:I-face(cubical-nerve(C);I)| (f ∈ box) ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)}  `
`  supposing ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))`

Definition: nerve-box-common-face
`nerve-box-common-face(box;L;z) ==`
`  hd(filter(λf.((direction(f) =z L dimension(f)) ∧b (direction(f) =z flip(L;z) dimension(f)));box))`

Lemma: nerve-box-common-face_wf2
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[L:cat-ob(poset-cat(I))]. ∀[z:nameset(I)].`
`  nerve-box-common-face(box;L;z) ∈ {f:I-face(cubical-nerve(C);I)| `
`                                    (f ∈ box)`
`                                    ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)`
`                                    ∧ (direction(f) = (flip(L;z) dimension(f)) ∈ ℕ2)}  `
`  supposing (∃j∈J. ¬(j = z ∈ Cname)) ∨ (((L x) = i ∈ ℕ2) ∧ (¬↑null(J)))`

Lemma: nerve-box-common-face_wf
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[L:cat-ob(poset-cat(I))]. ∀[z:nameset(I)].`
`  nerve-box-common-face(box;L;z) ∈ {f:I-face(cubical-nerve(C);I)| `
`                                    (f ∈ box)`
`                                    ∧ (direction(f) = (L dimension(f)) ∈ ℕ2)`
`                                    ∧ (direction(f) = (flip(L;z) dimension(f)) ∈ ℕ2)}  `
`  supposing (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname))) ∨ (((L x) = i ∈ ℕ2) ∧ (¬↑null(J)))`

Definition: nerve_box_label
`nerve_box_label(box;L) ==  cube(nerve-box-face(box;L)) L`

Lemma: nerve_box_label_wf
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[L:name-morph(I;[])].`
`  nerve_box_label(box;L) ∈ cat-ob(C) supposing ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))`

Lemma: nerve_box_label_same
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[L:name-morph(I;[])].`
`  ∀f:I-face(cubical-nerve(C);I)`
`    ((cube(f) L) = nerve_box_label(box;L) ∈ cat-ob(C)) supposing ((f ∈ box) and (direction(f) = (L dimension(f)) ∈ ℕ2)) `
`  supposing ((L x) = i ∈ ℕ2) ∨ (¬↑null(J))`

Lemma: same-face-edge-arrows-commute
`∀C:SmallCategory. ∀I:Cname List. ∀f:name-morph(I;[]). ∀a,b:nameset(I). ∀v:I-face(cubical-nerve(C);I).`
`  (((f a) = 0 ∈ ℕ2)`
`  `` ((f b) = 0 ∈ ℕ2)`
`  `` (¬(a = b ∈ nameset(I)))`
`  `` (¬(dimension(v) = a ∈ Cname))`
`  `` (¬(dimension(v) = b ∈ Cname))`
`  `` ((cat-comp(C) (cube(v) f) (cube(v) flip(f;a)) (cube(v) flip(flip(f;a);b)) (cube(v) f flip(f;a) (λx.Ax)) `
`       (cube(v) flip(f;a) flip(flip(f;a);b) (λx.Ax)))`
`     = (cat-comp(C) (cube(v) f) (cube(v) flip(f;b)) (cube(v) flip(flip(f;b);a)) (cube(v) f flip(f;b) (λx.Ax)) `
`        (cube(v) flip(f;b) flip(flip(f;b);a) (λx.Ax)))`
`     ∈ (cat-arrow(C) (cube(v) f) (cube(v) flip(flip(f;a);b)))))`

Definition: nerve_box_edge
`nerve_box_edge(box;c;y) ==  cube(nerve-box-common-face(box;c;y)) c flip(c;y) (λx.Ax)`

Definition: nerve_box_edge'
`nerve_box_edge'(box; c; y) ==  nerve_box_edge(box;c;y)`

Lemma: nerve_box_edge_wf2
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[y:nameset(I)]. ∀[c:{c:name-morph(I;[])| (c y) = 0 ∈ ℕ2} ].`
`  nerve_box_edge(box;c;y) ∈ cat-arrow(C) nerve_box_label(box;c) nerve_box_label(box;flip(c;y)) `
`  supposing (∃j∈J. ¬(j = y ∈ Cname)) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))`

Lemma: nerve_box_edge'_wf
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[y:nameset(I)]. ∀[c:{c:name-morph(I;[])| (c y) = 0 ∈ ℕ2} ].`
`  nerve_box_edge'(box; c; y) ∈ cat-arrow(C) nerve_box_label(box;c) nerve_box_label(box;flip(c;y)) `
`  supposing (∃j∈J. ¬(j = y ∈ Cname)) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))`

Lemma: nerve_box_edge_wf
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[y:nameset(I)]. ∀[c:{c:name-morph(I;[])| (c y) = 0 ∈ ℕ2} ].`
`  nerve_box_edge(box;c;y) ∈ cat-arrow(C) nerve_box_label(box;c) nerve_box_label(box;flip(c;y)) `
`  supposing (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname))) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))`

Lemma: nerve_box_edge_same1
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[y:nameset(I)]. ∀[c:{c:name-morph(I;[])| (c y) = 0 ∈ ℕ2} ].`
`  ∀f:I-face(cubical-nerve(C);I)`
`    (cube(f) c flip(c;y) (λx.Ax))`
`    = nerve_box_edge(box;c;y)`
`    ∈ (cat-arrow(C) nerve_box_label(box;c) nerve_box_label(box;flip(c;y))) `
`    supposing (f ∈ box) ∧ (direction(f) = (c dimension(f)) ∈ ℕ2) ∧ (direction(f) = (flip(c;y) dimension(f)) ∈ ℕ2) `
`  supposing (∃j∈J. ¬(j = y ∈ Cname)) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))`

Lemma: nerve_box_edge_same
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[y:nameset(I)]. ∀[c:{c:name-morph(I;[])| (c y) = 0 ∈ ℕ2} ].`
`  ∀f:I-face(cubical-nerve(C);I)`
`    (cube(f) c flip(c;y) (λx.Ax))`
`    = nerve_box_edge(box;c;y)`
`    ∈ (cat-arrow(C) nerve_box_label(box;c) nerve_box_label(box;flip(c;y))) `
`    supposing (f ∈ box) ∧ (direction(f) = (c dimension(f)) ∈ ℕ2) ∧ (direction(f) = (flip(c;y) dimension(f)) ∈ ℕ2) `
`  supposing (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname))) ∨ (((c x) = i ∈ ℕ2) ∧ (¬↑null(J)))`

Lemma: same-face-edge-arrows-commute0
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)].`
`  ∀f:name-morph(I;[]). ∀a,b:nameset(I).`
`    ∀[v:I-face(cubical-nerve(C);I)]`
`      ((cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b)) `
`        nerve_box_edge(box;f;a) `
`        nerve_box_edge(box;flip(f;a);b))`
`         = (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a)) `
`            nerve_box_edge(box;f;b) `
`            nerve_box_edge(box;flip(f;b);a))`
`         ∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))) supposing `
`         ((v ∈ box) and `
`         (¬(dimension(v) = b ∈ Cname)) and `
`         (¬(dimension(v) = a ∈ Cname)) and `
`         (¬(a = b ∈ nameset(I))) and `
`         ((f b) = 0 ∈ ℕ2) and `
`         (((f a) = 0 ∈ ℕ2) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))) `
`    supposing ((∃j1∈J. ¬(j1 = a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 = b ∈ Cname)))`
`    ∨ ((¬↑null(J)) ∧ ((f x) = i ∈ ℤ) ∧ ((flip(f;a) x) = i ∈ ℤ) ∧ ((flip(f;b) x) = i ∈ ℕ2))`

Lemma: same-face-edge-arrows-commute1
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)].`
`  ∀f:name-morph(I;[]). ∀a,b:nameset(I).`
`    ∀[v:I-face(cubical-nerve(C);I)]`
`      ((cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b)) `
`        nerve_box_edge(box;f;a) `
`        nerve_box_edge(box;flip(f;a);b))`
`         = (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a)) `
`            nerve_box_edge(box;f;b) `
`            nerve_box_edge(box;flip(f;b);a))`
`         ∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))) supposing `
`         ((v ∈ box) and `
`         (¬(dimension(v) = b ∈ Cname)) and `
`         (¬(dimension(v) = a ∈ Cname)) and `
`         (¬(a = b ∈ nameset(I))) and `
`         ((f b) = 0 ∈ ℕ2) and `
`         (((f a) = 0 ∈ ℕ2) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))) `
`    supposing (∃j1∈J. ¬(j1 = a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 = b ∈ Cname))`

Lemma: same-face-edge-arrows-commute4
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)].`
`  ∀f:name-morph(I;[]). ∀a,b:nameset(I).`
`    ((cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b)) `
`      nerve_box_edge(box;f;a) `
`      nerve_box_edge(box;flip(f;a);b))`
`       = (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a)) `
`          nerve_box_edge(box;f;b) `
`          nerve_box_edge(box;flip(f;b);a))`
`       ∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))) supposing `
`       ((¬(a = b ∈ nameset(I))) and `
`       ((f b) = 0 ∈ ℕ2) and `
`       ((f a) = 0 ∈ ℕ2) and `
`       (∃v:I-face(cubical-nerve(C);I)`
`         ((v ∈ box)`
`         ∧ (¬(dimension(v) = b ∈ Cname))`
`         ∧ (¬(dimension(v) = a ∈ Cname))`
`         ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))) and `
`       ((∃j1∈J. ¬(j1 = a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 = b ∈ Cname))))`

Lemma: same-face-edge-arrows-commute2
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List].`
`  ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(cubical-nerve(C);I;J;x;i)].`
`    ∀f:name-morph(I;[]). ∀a,b:nameset(I).`
`      ∀[v:I-face(cubical-nerve(C);I)]`
`        ((cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b)) `
`          nerve_box_edge(box;f;a) `
`          nerve_box_edge(box;flip(f;a);b))`
`           = (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a)) `
`              nerve_box_edge(box;f;b) `
`              nerve_box_edge(box;flip(f;b);a))`
`           ∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b)))) supposing `
`           ((v ∈ box) and `
`           (¬(dimension(v) = b ∈ Cname)) and `
`           (¬(dimension(v) = a ∈ Cname)) and `
`           (¬(a = b ∈ nameset(I))) and `
`           ((f b) = 0 ∈ ℕ2) and `
`           (((f a) = 0 ∈ ℕ2) ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))) `
`  supposing (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))`

Lemma: same-face-edge-arrows-commute3
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List].`
`  ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(cubical-nerve(C);I;J;x;i)].`
`    ∀f:name-morph(I;[]). ∀a,b:nameset(I).`
`      (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;a)) nerve_box_label(box;flip(flip(f;a);b)) `
`       nerve_box_edge(box;f;a) `
`       nerve_box_edge(box;flip(f;a);b))`
`      = (cat-comp(C) nerve_box_label(box;f) nerve_box_label(box;flip(f;b)) nerve_box_label(box;flip(flip(f;b);a)) `
`         nerve_box_edge(box;f;b) `
`         nerve_box_edge(box;flip(f;b);a))`
`      ∈ (cat-arrow(C) nerve_box_label(box;f) nerve_box_label(box;flip(flip(f;a);b))) `
`      supposing (((¬(a = b ∈ nameset(I))) ∧ ((f a) = 0 ∈ ℕ2)) ∧ ((f b) = 0 ∈ ℕ2))`
`      ∧ (∃v:I-face(cubical-nerve(C);I)`
`          ((v ∈ box)`
`          ∧ (¬(dimension(v) = b ∈ Cname))`
`          ∧ (¬(dimension(v) = a ∈ Cname))`
`          ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))) `
`  supposing (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))`

Lemma: same-face-square-commutes
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List].`
`  ∀[x:nameset(I)]. ∀[i:ℕ2]. ∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[f,g,h,k:name-morph(I;[])].`
`    ∀a,b:nameset(I).`
`      nerve_box_edge(box;f;a) o nerve_box_edge(box;g;b) = nerve_box_edge(box;f;b) o nerve_box_edge(box;h;a) `
`      supposing (((¬(a = b ∈ nameset(I))) ∧ ((f a) = 0 ∈ ℕ2))`
`      ∧ ((f b) = 0 ∈ ℕ2)`
`      ∧ (g = flip(f;a) ∈ name-morph(I;[]))`
`      ∧ (h = flip(f;b) ∈ name-morph(I;[]))`
`      ∧ (k = flip(flip(f;a);b) ∈ name-morph(I;[])))`
`      ∧ (∃v:I-face(cubical-nerve(C);I)`
`          ((v ∈ box)`
`          ∧ (¬(dimension(v) = b ∈ Cname))`
`          ∧ (¬(dimension(v) = a ∈ Cname))`
`          ∧ (direction(v) = (f dimension(v)) ∈ ℕ2))) `
`  supposing (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))`

Lemma: same-face-square-commutes2
`∀[C:SmallCategory]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(C);I;J;x;i)]. ∀[f,g,h,k:name-morph(I;[])].`
`  ∀a,b:nameset(I).`
`    (nerve_box_edge(box;f;a) o nerve_box_edge(box;g;b) = nerve_box_edge(box;f;b) o nerve_box_edge(box;h;a)) supposing `
`       (((((¬(a = b ∈ nameset(I))) ∧ ((f a) = 0 ∈ ℕ2))`
`       ∧ ((f b) = 0 ∈ ℕ2)`
`       ∧ (g = flip(f;a) ∈ name-morph(I;[]))`
`       ∧ (h = flip(f;b) ∈ name-morph(I;[]))`
`       ∧ (k = flip(flip(f;a);b) ∈ name-morph(I;[])))`
`       ∧ (∃v:I-face(cubical-nerve(C);I)`
`           ((v ∈ box)`
`           ∧ (¬(dimension(v) = b ∈ Cname))`
`           ∧ (¬(dimension(v) = a ∈ Cname))`
`           ∧ (direction(v) = (f dimension(v)) ∈ ℕ2)))) and `
`       (((∃j1∈J. ¬(j1 = a ∈ Cname)) ∧ (∃j2∈J. ¬(j2 = b ∈ Cname)))`
`       ∨ ((¬↑null(J)) ∧ ((f x) = i ∈ ℤ) ∧ ((flip(f;a) x) = i ∈ ℤ) ∧ ((flip(f;b) x) = i ∈ ℕ2))))`

Lemma: poset-functor-extends-box-faces
`∀G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(cubical-nerve(cat(G));I;J;x;i).`
`  (((¬↑null(J)) ∧ (∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname))))`
`  `` (∀fc∈bx.poset-functor-extends(cat(G);I-[dimension(fc)];λx.nerve_box_label(bx;((dimension(fc):=direction(fc)) o x));`
`                                   λz,f. nerve_box_edge(bx;((dimension(fc):=direction(fc)) o f);z);cube(fc))))`

Lemma: groupoid-edges-commute
`∀G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀box:open_box(cubical-nerve(fst(G));I;J;x;i).`
`  ((∃j1∈J. (∃j2∈J. ¬(j1 = j2 ∈ Cname)))`
`  `` edge-arrows-commute(fst(G);I;λc.nerve_box_label(box;c);λy,c. nerve_box_edge(box;c;y)))`

Definition: nerve_box_edge1
`nerve_box_edge1(G;box;x;i;j;c;y) ==`
`  if (c x =z i) ∨b(¬beq-cname(y;j)) then nerve_box_edge(box;c;y)`
`  if (i =z 0)`
`    then groupoid-square1(G;nerve_box_label(box;flip(c;x));nerve_box_label(box;flip(flip(c;x);y));`
`         nerve_box_label(box;c);nerve_box_label(box;flip(c;y));nerve_box_edge(box;flip(c;x);y);`
`         nerve_box_edge(box;flip(flip(c;x);y);x);nerve_box_edge(box;flip(c;x);x))`
`  else groupoid-square2(G;nerve_box_label(box;c);nerve_box_label(box;flip(c;y));`
`       nerve_box_label(box;flip(c;x));nerve_box_label(box;flip(flip(c;y);x));nerve_box_edge(box;flip(c;y);x);`
`       nerve_box_edge(box;c;x);nerve_box_edge(box;flip(c;x);y))`
`  fi `

Lemma: nerve_box_edge1_wf
`∀[G:Groupoid]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[j:nameset(J)]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(cat(G));I;J;x;i)]. ∀[y:nameset(I)]. ∀[c:{c:name-morph(I;[])| (c y) = 0 ∈ ℕ2} ].`
`  nerve_box_edge1(G;box;x;i;j;c;y) ∈ cat-arrow(cat(G)) nerve_box_label(box;c) nerve_box_label(box;flip(c;y)) `
`  supposing (∀j'∈J.j' = j ∈ Cname)`

Lemma: poset-functor-extends-box-faces-1
`∀G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(cubical-nerve(cat(G));I;J;x;i).`
`  (((¬↑null(J)) ∧ (∀j'∈J.j' = hd(J) ∈ Cname))`
`  `` (∀fc∈bx.poset-functor-extends(cat(G);I-[dimension(fc)];λx.nerve_box_label(bx;((dimension(fc):=direction(fc)) o x));`
`                                   λz,f. nerve_box_edge1(G;bx;x;i;hd(J);((dimension(fc):=direction(fc)) o f);z);cube(fc)\000C)))`

Lemma: groupoid-edges-commute1
`∀G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀j:nameset(I).`
`  ((j ∈ J)`
`  `` (∀j'∈J.j' = j ∈ Cname)`
`  `` (∀x:nameset(I). ∀i:ℕ2. ∀box:open_box(cubical-nerve(fst(G));I;J;x;i).`
`        edge-arrows-commute(fst(G);I;λc.nerve_box_label(box;c);λy,c. nerve_box_edge1(G;box;x;i;j;c;y))))`

Definition: groupoid-nerve-filler0
`groupoid-nerve-filler0(I;x;box) ==  functor-comp(poset-functor(I-[x];I;iota(x));snd(snd(hd(box))))`

Lemma: groupoid-nerve-filler0_wf
`∀[G:Groupoid]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(cat(G));I;J;x;i)].`
`  groupoid-nerve-filler0(I;x;box) ∈ cubical-nerve(cat(G))(I) supposing ↑null(J)`

Definition: groupoid-nerve-filler1
`groupoid-nerve-filler1(G;I;J;x;i;box) ==`
`  <λc.nerve_box_label(box;c)`
`  , λc1,c2,p. poset_functor_extend(cat(G);I;λc.nerve_box_label(box;c);λy,c. nerve_box_edge1(G;box;x;i;hd(J);c;y);c1;c2)`
`  >`

Lemma: groupoid-nerve-filler1_wf
`∀[G:Groupoid]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(cat(G));I;J;x;i)].`
`  groupoid-nerve-filler1(G;I;J;x;i;box) ∈ cubical-nerve(cat(G))(I) supposing (¬↑null(J)) ∧ (||box|| ≤ 3)`

Definition: groupoid-nerve-filler2
`groupoid-nerve-filler2(C;I;J;box) ==`
`  <λc.nerve_box_label(box;c)`
`  , λc1,c2,p. poset_functor_extend(C;I;λc.nerve_box_label(box;c);λy,c. nerve_box_edge(box;c;y);c1;c2)`
`  >`

Lemma: groupoid-nerve-filler2_wf
`∀[G:Groupoid]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(cat(G));I;J;x;i)].`
`  groupoid-nerve-filler2(cat(G);I;J;box) ∈ cubical-nerve(cat(G))(I) supposing 3 < ||box||`

Definition: groupoid-nerve-filler
`groupoid-nerve-filler(G;I;J;x;i;box) ==`
`  if null(J) then groupoid-nerve-filler0(I;x;box)`
`  if 3 <z ||box|| then groupoid-nerve-filler2(cat(G);I;J;box)`
`  else groupoid-nerve-filler1(G;I;J;x;i;box)`
`  fi `

Lemma: groupoid-nerve-filler_wf
`∀[G:Groupoid]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[box:open_box(cubical-nerve(cat(G));I;J;x;i)].`
`  (groupoid-nerve-filler(G;I;J;x;i;box) ∈ cubical-nerve(cat(G))(I))`

Lemma: groupoid-nerve-filler-fills
`∀G:Groupoid. ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(cubical-nerve(cat(G));I;J;x;i).`
`  fills-open_box(cubical-nerve(cat(G));I;bx;(λI,J,x,i,box. groupoid-nerve-filler(G;I;J;x;i;box)) I J x i bx)`

Lemma: groupoid-nerve-functor-flip
`∀[G:Groupoid]. ∀[I:Cname List]. ∀[u:nameset(I)]. ∀[K:Cname List]. ∀[f:name-morph(I;K)]. ∀[f1:name-morph(K;[])].`
`  ∀x1:nameset(I)`
`    ∀[F:Functor(poset-cat(I-[x1]);cat(G))]`
`      (F (f o f1) flip((f o f1);u) (λx.Ax))`
`      = (f(F) f1 flip(f1;f u) (λx.Ax))`
`      ∈ (cat-arrow(cat(G)) (F (f o f1)) (F (f o flip(f1;f u)))) `
`      supposing (↑isname(f u)) ∧ ((f1 (f u)) = 0 ∈ ℕ2)`

Lemma: groupoid-nerve-filler-uniform
`∀G:Groupoid. uniform-Kan-filler(cubical-nerve(cat(G));λI,J,x,i,box. groupoid-nerve-filler(G;I;J;x;i;box))`

Definition: Kan-groupoid-nerve
`Kan-groupoid-nerve(G) ==  <cubical-nerve(cat(G)), λI,J,x,i,box. groupoid-nerve-filler(G;I;J;x;i;box)>`

Lemma: Kan-groupoid-nerve_wf
`∀[G:Groupoid]. (Kan-groupoid-nerve(G) ∈ KanCubicalSet)`

Comment: Theorem 6.2 in Bezem,Coquand,Huber
`We prove theorem 6.2 of the BCH paper.`
`If ⋅`

Comment: The Type (Id_A a b)
`To define the type (Id_A a b) we must define, for each I-cube, alpha of`

`the context X, the "set" (Id_A a b)(alpha).`
`For a new coordinate z, the members of the type`
`   named-path are  z-paths from a(alpha) to b(alpha).`

`We tried to simply use ⌜z = fresh-cname(I)⌝ as the choice for coordinate z.`
`But, when defining the Kan structure on (Id_A a b) this did not work.`
`(Because then, an (y,c)-face of (Id_A a b) has coordinates`
` ⌜[fresh-cname(I-[y]) / I-[y]]⌝ in A,  and that is not the same as`
` ⌜[fresh-cname(I) / I]-[y]⌝ -- since fresh-cname(I-[y]) could be y  ).`

`So, we need to proceed as in the BCH paper with an equivalence class`
`of I-path.`

`The equivalence relation is `
`path-eq`
`path-eq-equiv`
`and the equivalence classes are the quotient type: cubical-path.`

`The morphisms on this type are defined by the operation: I-path-morph,`
`and then we can define the type cubical-identity`
`and prove its typing lemma cubical-identity_wf.`

`To prove that, we have to show that the morphisms are well defined on the`
`quotient type, which is proved in`
`I-path-morph_functionality`
`I-path-morph-id`
`I-path-morph-comp`
` `
`Those proof use lemmas`
`like extend-name-morph-rename-one`
`    rename-one-extend-name-morph`
`    extend-name-morph-comp`
`    rename-one-extend-id`

`The next step is to show that (Id_A a a) is inhabited by the term refl(a)`
`cubical-refl_wf`

`The description of the Kan-structure is here: Kan structure on Id_A a b`
`⋅`

Definition: name-path-endpoints
`name-path-endpoints(X;A;a;b;I;alpha;z;omega) ==`
`  ((omega iota(z)(alpha) (z:=0)) = (a I alpha) ∈ A(alpha)) ∧ ((omega iota(z)(alpha) (z:=1)) = (b I alpha) ∈ A(alpha))`

Lemma: name-path-endpoints_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[z:Cname]. ∀[omega:A(iota(z)(alpha))].`
`  name-path-endpoints(X;A;a;b;I;alpha;z;omega) ∈ ℙ supposing ¬(z ∈ I)`

Definition: named-path
`named-path(X;A;a;b;I;alpha;z) ==  {omega:A(iota(z)(alpha))| name-path-endpoints(X;A;a;b;I;alpha;z;omega)} `

Lemma: named-path_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[z:Cname].`
`  named-path(X;A;a;b;I;alpha;z) ∈ Type supposing ¬(z ∈ I)`

Lemma: named-path-subtype
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[z:Cname].`
`  named-path(X;A;a;b;I;alpha;z) ⊆r A(iota(z)(alpha)) supposing ¬(z ∈ I)`

Lemma: named-path-equal-implies
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[z:Cname].`
`  ∀[p,q:named-path(X;A;a;b;I;alpha;z)].  p = q ∈ A(iota(z)(alpha)) supposing p = q ∈ named-path(X;A;a;b;I;alpha;z) `
`  supposing ¬(z ∈ I)`

Lemma: equal-named-paths
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[z:Cname].`
`  ∀[p:named-path(X;A;a;b;I;alpha;z)]. ∀[q:A(iota(z)(alpha))].`
`    p = q ∈ named-path(X;A;a;b;I;alpha;z) supposing p = q ∈ A(iota(z)(alpha)) `
`  supposing ¬(z ∈ I)`

Definition: named-path-morph
`named-path-morph(X;A;I;K;z;x;f;alpha;w) ==  (w iota(z)(alpha) f[z:=x])`

Lemma: named-path-morph_wf
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀alpha:X(I). ∀z:{z:Cname| ¬(z ∈ I)} .`
`∀w:named-path(X;A;a;b;I;alpha;z). ∀x:{x:Cname| ¬(x ∈ K)} .`
`  (named-path-morph(X;A;I;K;z;x;f;alpha;w) ∈ named-path(X;A;a;b;K;f(alpha);x))`

Definition: I-path
`I-path(X;A;a;b;I;alpha) ==  z:{z:Cname| ¬(z ∈ I)}  × named-path(X;A;a;b;I;alpha;z)`

Lemma: I-path_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)].  (I-path(X;A;a;b;I;alpha) ∈ Type)`

Lemma: equal-I-paths
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[p,q:I-path(X;A;a;b;I;alpha)].`
`  p = q ∈ I-path(X;A;a;b;I;alpha) `
`  supposing ((fst(p)) = (fst(q)) ∈ Cname) ∧ ((snd(p)) = (snd(q)) ∈ A(iota(fst(p))(alpha)))`

Definition: I-path-morph
`I-path-morph(X;A;I;K;f;alpha;p) ==`
`  let z,w = p `
`  in <fresh-cname(K), named-path-morph(X;A;I;K;z;fresh-cname(K);f;alpha;w)>`

Lemma: I-path-morph_wf
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀alpha:X(I). ∀w:I-path(X;A;a;b;I;alpha).`
`  (I-path-morph(X;A;I;K;f;alpha;w) ∈ I-path(X;A;a;b;K;f(alpha)))`

Definition: path-eq
`path-eq(X;A;I;alpha;p;q) ==`
`  let z,w = p `
`  in let z',w' = q `
`     in (w iota(z)(alpha) rename-one-name(z;z')) = w' ∈ A(iota(z')(alpha))`

Lemma: path-eq_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[p,q:I-path(X;A;a;b;I;alpha)].`
`  (path-eq(X;A;I;alpha;p;q) ∈ ℙ)`

Lemma: path-eq-equiv
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)].`
`  EquivRel(I-path(X;A;a;b;I;alpha);p,q.path-eq(X;A;I;alpha;p;q))`

Lemma: path-eq_weakening
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)].`
`  ∀p,q:I-path(X;A;a;b;I;alpha).  path-eq(X;A;I;alpha;p;q) supposing p = q ∈ I-path(X;A;a;b;I;alpha)`

Lemma: path-eq-same-name
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)].`
`  ∀p,q:I-path(X;A;a;b;I;alpha).`
`    path-eq(X;A;I;alpha;p;q) `⇐⇒` p = q ∈ I-path(X;A;a;b;I;alpha) supposing (fst(p)) = (fst(q)) ∈ Cname`

Lemma: I-path-morph_functionality
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀alpha:X(I).`
`∀p,q:I-path(X;A;a;b;I;alpha).`
`  (path-eq(X;A;I;alpha;p;q) `` path-eq(X;A;K;f(alpha);I-path-morph(X;A;I;K;f;alpha;p);I-path-morph(X;A;I;K;f;alpha;q)))`

Definition: cubical-path
`cubical-path(X;A;a;b;I;alpha) ==  p,q:I-path(X;A;a;b;I;alpha)//path-eq(X;A;I;alpha;p;q)`

Lemma: cubical-path_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)].  (cubical-path(X;A;a;b;I;alpha) ∈ Type)`

Lemma: cubical-path-same-name
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[p,q:I-path(X;A;a;b;I;alpha)].`
`  (((fst(p)) = (fst(q)) ∈ Cname) `` (p = q ∈ cubical-path(X;A;a;b;I;alpha)) `` (p = q ∈ I-path(X;A;a;b;I;alpha)))`

Lemma: I-path-morph_wf2
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I,K:Cname List. ∀f:name-morph(I;K). ∀alpha:X(I).`
`∀w:cubical-path(X;A;a;b;I;alpha).`
`  (I-path-morph(X;A;I;K;f;alpha;w) ∈ cubical-path(X;A;a;b;K;f(alpha)))`

Lemma: I-path-morph-id
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:X(I). ∀w:cubical-path(X;A;a;b;I;alpha).`
`  (I-path-morph(X;A;I;I;1;alpha;w) = w ∈ cubical-path(X;A;a;b;I;alpha))`

Lemma: I-path-morph-comp
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀alpha:X(I).`
`∀u:cubical-path(X;A;a;b;I;alpha).`
`  (I-path-morph(X;A;I;K;(f o g);alpha;u)`
`  = I-path-morph(X;A;J;K;g;f(alpha);I-path-morph(X;A;I;J;f;alpha;u))`
`  ∈ cubical-path(X;A;a;b;K;(f o g)(alpha)))`

Definition: cubical-identity
`(Id_A a b) ==  <λI,alpha. cubical-path(X;A;a;b;I;alpha), λI,K,f,alpha,p. I-path-morph(X;A;I;K;f;alpha;p)>`

Lemma: cubical-identity_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}].  X ⊢ (Id_A a b)`

Lemma: equal-cubical-identity-at
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[p,q:I-path(X;A;a;b;I;alpha)].`
`  p = q ∈ (Id_A a b)(alpha) supposing path-eq(X;A;I;alpha;p;q)`

Definition: set-path-name
`set-path-name(X;A;I;alpha;x;p) ==  let z,w = p in <x, named-path-morph(X;A;I;I;z;x;1;alpha;w)>`

Lemma: set-path-name_wf
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:X(I).`
`  ∀[x:{x:Cname| ¬(x ∈ I)} ]`
`    ∀p:(Id_A a b)(alpha)`
`      (set-path-name(X;A;I;alpha;x;p) ∈ {q:I-path(X;A;a;b;I;alpha)| `
`                                         ((fst(q)) = x ∈ Cname) ∧ (q = p ∈ (Id_A a b)(alpha))} )`

Definition: lift-id-face
`lift-id-face(X;A;I;alpha;face) ==`
`  let y,c,w = face in `
`  <y, c, snd(set-path-name(X;A;I-[y];(y:=c)(alpha);fresh-cname(I);w))>`

Lemma: lift-id-face_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[face:A-face(X;(Id_A a b);I;alpha)].`
`  (lift-id-face(X;A;I;alpha;face) ∈ A-face(X;A;I+;iota'(I)(alpha)))`

Definition: lift-id-faces
`lift-id-faces(X;A;I;alpha;box) ==  map(λface.lift-id-face(X;A;I;alpha;face);box)`

Lemma: lift-id-faces-wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[alpha:X(I)]. ∀[box:A-open-box(X;(Id_A a b);I;alpha;J;x;i)].`
`  (lift-id-faces(X;A;I;alpha;box) ∈ A-open-box(X;A;I+;iota'(I)(alpha);J;x;i))`

Lemma: lift-id-faces_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[alpha:X(I)]. ∀[box:A-open-box(X;(Id_A a b);I;alpha;J;x;i)].`
`  (lift-id-faces(X;A;I;alpha;box) ∈ A-open-box(X;A;[fresh-cname(I) / I];iota(fresh-cname(I))(alpha);J;x;i))`

Definition: term-A-face
`This makes a <y,i>-face  (where y is fresh(I))  that is equal to the`
`given cubical term, a.⋅`

`term-A-face(a;I;alpha;i) ==  <fresh-cname(I), i, a(alpha)>`

Lemma: term-A-face_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[alpha:X(I)]. ∀[i:ℕ2].`
`  (term-A-face(a;I;alpha;i) ∈ A-face(X;A;[fresh-cname(I) / I];iota(fresh-cname(I))(alpha)))`

Definition: cubical-id-box
`cubical-id-box(X;A;a;b;I;alpha;box) ==`
`  extend-A-open-box(lift-id-faces(X;A;I;alpha;box);term-A-face(a;I;alpha;0);term-A-face(b;I;alpha;1))`

Lemma: cubical-id-box_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a,b:{X ⊢ _:A}]. ∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[i:ℕ2].`
`∀[alpha:X(I)]. ∀[box:A-open-box(X;(Id_A a b);I;alpha;J;x;i)].`
`  (cubical-id-box(X;A;a;b;I;alpha;box) ∈ A-open-box(X;A;[fresh-cname(I) / `
`                                                         I];iota(fresh-cname(I))(alpha);[fresh-cname(I) / J];x;i))`

Comment: Kan structure on Id_A a b
`We need the Kan structure on (Id_A a b).`

`If bx is an open box in (Id_A a b)(alpha) then it is a list of faces`
`<y,c,w> with w in ⌜(Id_A a b)((y:=c)(alpha))⌝`

`If we take x = fresh-cname(I) then ⌜¬(x ∈ I)⌝ so `
`trivially,  ⌜¬(x ∈ I-[y])⌝`
`so we can use set-path-name(X;A;I;alpha;x;w)`
`to change w into an equal w' with ⌜(fst(w')) = x⌝.`

`We use this to `
`define lift-id-face`
`that converts an A-face(X;(Id_A a b);I;alpha)`
`to an A-face(X;A;I+;iota'(I)(alpha)).`

`If we do this to each face in bx, we get an open box (with parameters J)`
`  lift-id-faces-wf  (proof is quite long!)`
`in A(iota'(I)(alpha))`

`Now we extend this to an open box with parameters ⌜[fresh-cname(I) / J]⌝`
`by adding the bottom and top faces corresponding to a(alpha) and b(alpha)`
`to get: cubical-id-box`
`        cubical-id-box_wf `

`We can use the Kanfiller for A`
`to fill it with a cube c  `

`Then  the pair <fresh-cname(I),c> fills the original bx in (Id_A a b)(alpha)`
`Kan_id_filler.`
`Kan_id_filler_wf`

`Then we have to show that this filler satisfies the uniformity condition:`
`  Kan_id_filler_uniform   (very long proof!! can it be improved?)`

`Putting these together we get the identity type with uniform Kan structure:`
`Kan-cubical-identity`
`Kan-cubical-identity_wf.⋅`

Definition: Kan_id_filler
`Kan_id_filler(X;A;a;b) ==  λI,alpha,J,x,i,bx. <fresh-cname(I), filler(x;i;cubical-id-box(X;Kan-type(A);a;b;I;alpha;bx))>`

Lemma: Kan_id_filler_wf1
`∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀a,b:{X ⊢ _:Kan-type(A)}.`
`  (Kan_id_filler(X;A;a;b) ∈ I:(Cname List)`
`   ⟶ alpha:X(I)`
`   ⟶ J:(nameset(I) List)`
`   ⟶ x:nameset(I)`
`   ⟶ i:ℕ2`
`   ⟶ A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)`
`   ⟶ I-path(X;Kan-type(A);a;b;I;alpha))`

Lemma: Kan_id_filler_wf
`∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀a,b:{X ⊢ _:Kan-type(A)}.`
`  (Kan_id_filler(X;A;a;b) ∈ {filler:I:(Cname List)`
`                             ⟶ alpha:X(I)`
`                             ⟶ J:(nameset(I) List)`
`                             ⟶ x:nameset(I)`
`                             ⟶ i:ℕ2`
`                             ⟶ A-open-box(X;(Id_Kan-type(A) a b);I;alpha;J;x;i)`
`                             ⟶ (Id_Kan-type(A) a b)(alpha)| `
`                             Kan-A-filler(X;(Id_Kan-type(A) a b);filler)} )`

Lemma: Kan_id_filler_uniform
`∀X:CubicalSet. ∀A:{X ⊢ _(Kan)}. ∀a,b:{X ⊢ _:Kan-type(A)}.`
`  uniform-Kan-A-filler(X;(Id_Kan-type(A) a b);Kan_id_filler(X;A;a;b))`

Definition: Kan-cubical-identity
`Kan(Id_A a b) ==  <(Id_Kan-type(A) a b), Kan_id_filler(X;A;a;b)>`

Lemma: Kan-cubical-identity_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _(Kan)}]. ∀[a,b:{X ⊢ _:Kan-type(A)}].  (Kan(Id_A a b) ∈ {X ⊢ _(Kan)})`

Lemma: csm-I-path
`∀X,Delta:CubicalSet. ∀s:Delta ⟶ X. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:Delta(I).`
`  (I-path(Delta;(A)s;(a)s;(b)s;I;alpha) = I-path(X;A;a;b;I;(s)alpha) ∈ Type)`

Lemma: csm-cubical-identity
`∀X,Delta:CubicalSet. ∀s:Delta ⟶ X. ∀A:{X ⊢ _}. ∀a,b:{X ⊢ _:A}.`
`  (((Id_A a b))s`
`  = (Id_(A)s (a)s (b)s)`
`  ∈ (A:I:(Cname List) ⟶ Delta(I) ⟶ Type × (I:(Cname List)`
`                                            ⟶ J:(Cname List)`
`                                            ⟶ f:name-morph(I;J)`
`                                            ⟶ a:Delta(I)`
`                                            ⟶ (A I a)`
`                                            ⟶ (A J f(a)))))`

Lemma: csm-Kan-cubical-identity
`∀[X,Delta:CubicalSet]. ∀[s:Delta ⟶ X]. ∀[A:{X ⊢ _(Kan)}]. ∀[a,b:{X ⊢ _:Kan-type(A)}].`
`  ((Kan(Id_A a b))s = Kan(Id_(A)s (a)s (b)s) ∈ {Delta ⊢ _(Kan)})`

Definition: refl-path
`refl-path(A;a;I;alpha) ==  <fresh-cname(I), (a I alpha alpha iota'(I))>`

Lemma: refl-path_wf
`∀X:CubicalSet. ∀A:{X ⊢ _}. ∀a:{X ⊢ _:A}. ∀I:Cname List. ∀alpha:X(I).  (refl-path(A;a;I;alpha) ∈ I-path(X;A;a;a;I;alpha))`

Definition: cubical-refl
`refl(a) ==  λI,alpha. refl-path(A;a;I;alpha)`

Lemma: cubical-refl_wf
`∀[X:CubicalSet]. ∀[A:{X ⊢ _}]. ∀[a:{X ⊢ _:A}].  (refl(a) ∈ {X ⊢ _:(Id_A a a)})`

Definition: cubical-universe
`c𝕌 ==  <λI.{unit-cube(I) ⊢ _(Kan)}, λI,J,f,AK. (AK)unit-cube-map(f)>`

Lemma: cubical-universe_wf
`c𝕌 ∈ CubicalSet'`

Lemma: cubical-universe-I-cube
`∀[I:Cname List]`
`  (c𝕌(I) ~ {p:AF:{AF:A:L:(Cname List) ⟶ name-morph(I;L) ⟶ Type × (L:(Cname List)`
`                                                                   ⟶ J:(Cname List)`
`                                                                   ⟶ f:name-morph(L;J)`
`                                                                   ⟶ a:name-morph(I;L)`
`                                                                   ⟶ (A L a)`
`                                                                   ⟶ (A J (a o f)))| `
`                  let A,F = AF `
`                  in (∀K:Cname List. ∀a:name-morph(I;K). ∀u:A K a.  ((F K K 1 a u) = u ∈ (A K a)))`
`                     ∧ (∀L,J,K:Cname List. ∀f:name-morph(L;J). ∀g:name-morph(J;K). ∀a:name-morph(I;L). ∀u:A L a.`
`                          ((F L K (f o g) a u) = (F J K g (a o f) (F L J f a u)) ∈ (A K (a o (f o g)))))} `
`            × (L:(Cname List)`
`              ⟶ f:name-morph(I;L)`
`              ⟶ J:(nameset(L) List)`
`              ⟶ x:nameset(L)`
`              ⟶ i:ℕ2`
`              ⟶ A-open-box(unit-cube(I);AF;L;f;J;x;i)`
`              ⟶ ((fst(AF)) L f))| `
`            let AF,filler = p `
`            in Kan-A-filler(unit-cube(I);AF;filler) ∧ uniform-Kan-A-filler(unit-cube(I);AF;filler)} )`

Definition: cu-cube-family
`cu-cube-family(alpha;L;f) ==  (fst(fst(alpha))) L f`

Lemma: cu-cube-family_wf
`∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[L:Cname List]. ∀[f:name-morph(I;L)].  (cu-cube-family(alpha;L;f) ∈ Type)`

Lemma: cu-cube-family-Kan-type-at
`∀[alpha,L,f:Top].  (cu-cube-family(alpha;L;f) ~ Kan-type(alpha)(f))`

Lemma: cu-cube-family-comp
`∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[J,L,f,g:Top].  (cu-cube-family(alpha;L;(f o g)) ~ cu-cube-family(f(alpha);L;g))`

Definition: cu-cube-restriction
`cu-cube-restriction(alpha;L;J;f;a;T) ==  (snd(fst(alpha))) L J f a T`

Lemma: cu-cube-restriction_wf
`∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[L,J:Cname List]. ∀[f:name-morph(L;J)]. ∀[a:name-morph(I;L)].`
`∀[T:cu-cube-family(alpha;L;a)].`
`  (cu-cube-restriction(alpha;L;J;f;a;T) ∈ cu-cube-family(alpha;J;(a o f)))`

Lemma: cu-cube-restriction-id
`∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[K:Cname List]. ∀[a:name-morph(I;K)]. ∀[T:cu-cube-family(alpha;K;a)].`
`  (cu-cube-restriction(alpha;K;K;1;a;T) = T ∈ cu-cube-family(alpha;K;a))`

Lemma: cu-cube-restriction-comp
`∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[L,J,K:Cname List]. ∀[f:name-morph(L;J)]. ∀[g:name-morph(J;K)]. ∀[a:name-morph(I;L)].`
`∀[T:cu-cube-family(alpha;L;a)].`
`  (cu-cube-restriction(alpha;J;K;g;(a o f);cu-cube-restriction(alpha;L;J;f;a;T))`
`  = cu-cube-restriction(alpha;L;K;(f o g);a;T)`
`  ∈ cu-cube-family(alpha;K;(a o (f o g))))`

Definition: cu-cube-filler
`cu-cube-filler(alpha) ==  snd(alpha)`

Lemma: cu-cube-filler_wf
`∀[I:Cname List]. ∀[alpha:c𝕌(I)].`
`  (cu-cube-filler(alpha) ∈ L:(Cname List)`
`   ⟶ f:name-morph(I;L)`
`   ⟶ J:(nameset(L) List)`
`   ⟶ x:nameset(L)`
`   ⟶ i:ℕ2`
`   ⟶ A-open-box(unit-cube(I);Kan-type(alpha);L;f;J;x;i)`
`   ⟶ cu-cube-family(alpha;L;f))`

Lemma: cu-cube-filler-fills
`∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[L:Cname List]. ∀[f:name-morph(I;L)]. ∀[J:nameset(L) List]. ∀[x:nameset(L)]. ∀[i:ℕ2].`
`∀[box:A-open-box(unit-cube(I);Kan-type(alpha);L;f;J;x;i)].`
`  Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha))`

Lemma: cu-cube-filler-uniform
`∀[I:Cname List]. ∀[alpha:c𝕌(I)]. ∀[L:Cname List]. ∀[f:name-morph(I;L)]. ∀[J:nameset(L) List]. ∀[x:nameset(L)]. ∀[i:ℕ2].`
`∀[box:A-open-box(unit-cube(I);Kan-type(alpha);L;f;J;x;i)].`
`  uniform-Kan-A-filler(unit-cube(I);Kan-type(alpha);cu-cube-filler(alpha))`

Definition: cu-box-in-box
`cu-box-in-box(I;box) ==`
`  {u:i:ℕ||box|| ⟶ cu-cube-family(cube(box[i]);I-[dimension(box[i])];1)| `
`   ∀i,j:ℕ||box||.`
`     ((¬(dimension(box[i]) = dimension(box[j]) ∈ Cname))`
`     `` (cu-cube-restriction(cube(box[i]);I-[dimension(box[i])];I-[dimension(box[i]); dimension(box[j])];`
`                             (dimension(box[j]):=direction(box[j]));1;u i)`
`        = cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];`
`                              (dimension(box[i]):=direction(box[i]));1;u j)`
`        ∈ cu-cube-family(cube(box[i]);I-[dimension(box[i]);`
`                                         dimension(box[j])];(1 o (dimension(box[j]):=direction(box[j]))))))} `

Lemma: cu-box-in-box_wf
`∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[x:nameset(I)]. ∀[d:ℕ2]. ∀[box:open_box(c𝕌;I;J;x;d)].`
`  (cu-box-in-box(I;box) ∈ Type)`

Lemma: cu-filler-cases
`∀I:Cname List. ∀J:nameset(I) List. ∀K:Cname List. ∀x:nameset(I). ∀f:name-morph(I-[x];K). ∀i:ℕ2.`
`∀box:open_box(c𝕌;I;J;x;i).`
`  ((J ∈ nameset(J) List)`
`  ∧ (nameset(J) ⊆r nameset(I-[x]))`
`  ∧ ((∃y:nameset(J) [((y ∈ J) ∧ (↑¬bisname(f y)) ∧ (l-first(y.¬bisname(f y);J) ~ inl y))])`
`    ∨ (((∀y∈J.¬↑¬bisname(f y)) ∧ (↑isr(l-first(y.¬bisname(f y);J))))`
`      ∧ (f[x:=fresh-cname(K)] ∈ name-morph(I;[fresh-cname(K) / K]))`
`      ∧ (nameset([x / J]) ⊆r nameset(I))`
`      ∧ (∀z:nameset([x / J]). (↑isname(f[x:=fresh-cname(K)] z)))`
`      ∧ (f[x:=fresh-cname(K)] ∈ nameset([x / J]) ⟶ nameset([fresh-cname(K) / K]))`
`      ∧ (x ∈ nameset([x / J]))`
`      ∧ (nameset([x / J]) ⊆r name-morph-domain(f[x:=fresh-cname(K)];I)))))`

Definition: cu_filler_1
`cu_filler_1{i:l}(I;J;K;f;x;i;box) ==`
`  case l-first(y.¬bisname(f y);J)`
`   of inl(y) =>`
`   cu-cube-family(cube(get_face(y;f y;box));K;((x:=i) o f))`
`   | inr(_) =>`
`   cu-box-in-box([fresh-cname(K) / K];open_box_image(c𝕌;I;[fresh-cname(K) / K];f[x:=fresh-cname(K)];box))`

Lemma: cu_filler_1_wf
`∀[I:Cname List]. ∀[J:nameset(I) List]. ∀[K:Cname List]. ∀[x:nameset(I)]. ∀[f:name-morph(I-[x];K)]. ∀[i:ℕ2].`
`∀[box:open_box(c𝕌;I;J;x;i)].`
`  (cu_filler_1{i:l}(I;J;K;f;x;i;box) ∈ Type)`

Definition: cu_filler_2
`cu_filler_2(J;K;L;f;g;x;i;box;X) ==`
`  case l-first(y.¬bisname(f y);J)`
`   of inl(y) =>`
`   cu-cube-restriction(cube(get_face(y;f y;box));K;L;g;((x:=i) o f);X)`
`   | inr(_) =>`
`   case l-first(y.¬bisname((f o g) y);J) of inl(y) => 44 | inr(_) => 55`

Home Index