---

Step * 1 of Lemma csm-Kan-id


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))
BY
{ (RepeatFor 2 ((FunExt THENA Auto)) THEN Reduce 0 THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  L:(Cname  List)  {}\mrightarrow{}  Type
2.  G1  :  I:(Cname  List)  {}\mrightarrow{}  J:(Cname  List)  {}\mrightarrow{}  name-morph(I;J)  {}\mrightarrow{}  (X  I)  {}\mrightarrow{}  (X  J)
3.  \mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
          ((G1  I  K  (f  o  g))  =  ((G1  J  K  g)  o  (G1  I  J  f)))
4.  \mforall{}I:Cname  List.  ((G1  I  I  1)  =  (\mlambda{}x.x))
5.  A  :  \{<X,  G1>  \mvdash{}  \_\}
6.  filler  :  I:(Cname  List)
{}\mrightarrow{}  alpha:<X,  G1>(I)
{}\mrightarrow{}  J:(nameset(I)  List)
{}\mrightarrow{}  x:nameset(I)
{}\mrightarrow{}  i:\mBbbN{}2
{}\mrightarrow{}  A-open-box(<X,  G1>A;I;alpha;J;x;i)
{}\mrightarrow{}  A(alpha)
7.  Kan-A-filler(<X,  G1>A;filler)
8.  uniform-Kan-A-filler(<X,  G1>A;filler)
9.  <X,  G1>  \mmember{}  CubicalSet
\mvdash{}  filler  =  (\mlambda{}I,alpha.  (filler  I  (1(<X,  G1>))alpha))


By

---

Latex:
(RepeatFor  2  ((FunExt  THENA  Auto))  THEN  Reduce  0  THEN  EqCD  THEN  Auto)

---

Home Index