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))
Lemma: add-remove-fresh-cname
∀I:Cname List. (I = [fresh-cname(I) / I]-[fresh-cname(I)] ∈ (Cname List))
Lemma: add-remove-fresh-sq
∀I:Cname List. ([fresh-cname(I) / I]-[fresh-cname(I)] ~ I)
Definition: add-fresh-cname
I+ == eval m = fresh-cname(I) in [m / I]
Lemma: add-fresh-cname_wf
∀[I:Cname List]. (I+ ∈ Cname List)
Lemma: subtype-add-fresh-cname
∀[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})
Definition: cube-context-adjoin
X.A == <λI.(alpha:X(I) × A(alpha)), λI,J,f,p. <f(fst(p)), (snd(p) fst(p) f)>>
Lemma: cube-context-adjoin_wf
∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}]. (Gamma.A ∈ CubicalSet)
Definition: cc-adjoin-cube
(v;u) == <v, u>
Lemma: cc-adjoin-cube_wf
∀X:CubicalSet. ∀A:{X ⊢ _}. ∀J:Cname List. ∀v:X(J). ∀u:A(v). ((v;u) ∈ X.A(J))
Lemma: cc-adjoin-cube-restriction
∀[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))
Definition: csm-adjoin
(s;u) == λI,a. <(s)a, u I a>
Lemma: csm-adjoin_wf
∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:Delta ⟶ Gamma]. ∀[u:{Delta ⊢ _:(A)sigma}].
((sigma;u) ∈ Delta ⟶ Gamma.A)
Lemma: csm-adjoin-ap
∀[sigma,u,I,del:Top]. (((sigma;u))del ~ <(sigma)del, (u)del>)
Definition: csm-id-adjoin
[u] == (1(X);u)
Lemma: csm-id-adjoin_wf
∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[u:{Gamma ⊢ _:A}]. ([u] ∈ Gamma ⟶ Gamma.A)
Lemma: csm-id-adjoin-ap
∀X:CubicalSet. ∀A:{X ⊢ _}. ∀u:{X ⊢ _:A}. ∀I:Cname List. ∀a:X(I). (([u])a = (a;u I a) ∈ X.A(I))
Lemma: cc-fst-csm-adjoin
∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:Delta ⟶ Gamma]. ∀[u:{Delta ⊢ _:(A)sigma}].
(p o (sigma;u) = sigma ∈ Delta ⟶ Gamma)
Lemma: cc-snd-csm-adjoin
∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:Delta ⟶ Gamma]. ∀[u:{Delta ⊢ _:(A)sigma}].
((q)(sigma;u) = u ∈ {Delta ⊢ _:(A)sigma})
Lemma: csm-adjoin-fst-snd
∀[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.
⋅
Comment: theorems about Kan structure
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) ∈ ℙ)
Definition: adjacent-compatible
adjacent-compatible(X;I;L) == (∀f1,f2∈L. face-compatible(X;I;f1;f2))
Lemma: adjacent-compatible_wf
∀[X:CubicalSet]. ∀[I:Cname List]. ∀[L:I-face(X;I) List]. (adjacent-compatible(X;I;L) ∈ ℙ)
Lemma: adjacent-compatible-iff
∀[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)]))))
Definition: A-adjacent-compatible
A-adjacent-compatible(X;A;I;alpha;L) == (∀f1,f2∈L. A-face-compatible(X;A;I;alpha;f1;f2))
Lemma: A-adjacent-compatible_wf
∀[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) ∈ ℕ)
Lemma: poset-cat-dist-add
∀[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