---

Step * of Lemma csm-Kan-id

∀[Gamma:CubicalSet]. ∀[AK:{Gamma ⊢ _(Kan)}].  ((AK)1(Gamma) = AK ∈ {Gamma ⊢ _(Kan)})
BY
{ (Auto
   THEN Symmetry
   THEN D -1
   THEN EqTypeCD
   THEN Try (Trivial)
   THEN Auto
   THEN D 2
   THEN (Assert Gamma ∈ CubicalSet BY
               Trivial)
   THEN RepeatFor 2 (D 1)
   THEN All Reduce
   THEN RepUR ``csm-Kan-cubical-type`` 0
   THEN EqCD
   THEN Auto
   THEN RenameVar `filler' 6) }

1
1. X : L:(Cname List) ⟶ Type
2. G1 : I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J)
3. ∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
     ((G1 I K (f o g)) = ((G1 J K g) o (G1 I J f)) ∈ ((X I) ⟶ (X K)))
4. ∀I:Cname List. ((G1 I I 1) = (λx.x) ∈ ((X I) ⟶ (X I)))
5. A : {<X, G1> ⊢ _}
6. filler : I:(Cname List)
⟶ alpha:<X, G1>(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(<X, G1>;A;I;alpha;J;x;i)
⟶ A(alpha)
7. Kan-A-filler(<X, G1>;A;filler)
8. uniform-Kan-A-filler(<X, G1>;A;filler)
9. <X, G1> ∈ CubicalSet
⊢ filler
= (λI,alpha. (filler I (1(<X, G1>))alpha))
∈ (I:(Cname List)
  ⟶ alpha:<X, G1>(I)
  ⟶ J:(nameset(I) List)
  ⟶ x:nameset(I)
  ⟶ i:ℕ2
  ⟶ A-open-box(<X, G1>;A;I;alpha;J;x;i)
  ⟶ A(alpha))

---

Latex:

---

Latex:
\mforall{}[Gamma:CubicalSet].  \mforall{}[AK:\{Gamma  \mvdash{}  \_(Kan)\}].    ((AK)1(Gamma)  =  AK)


By

---

Latex:
(Auto
  THEN  Symmetry
  THEN  D  -1
  THEN  EqTypeCD
  THEN  Try  (Trivial)
  THEN  Auto
  THEN  D  2
  THEN  (Assert  Gamma  \mmember{}  CubicalSet  BY
                          Trivial)
  THEN  RepeatFor  2  (D  1)
  THEN  All  Reduce
  THEN  RepUR  ``csm-Kan-cubical-type``  0
  THEN  EqCD
  THEN  Auto
  THEN  RenameVar  `filler'  6)

---

Home Index