---

Step * 1 of Lemma csm-Kan-cubical-type_wf


1. Delta : CubicalSet
2. Gamma : CubicalSet
3. s : Delta ⟶ Gamma
4. A : {Gamma ⊢ _}
5. filler : I:(Cname List)
⟶ alpha:Gamma(I)
⟶ J:(nameset(I) List)
⟶ x:nameset(I)
⟶ i:ℕ2
⟶ A-open-box(Gamma;A;I;alpha;J;x;i)
⟶ A(alpha)
6. Kan-A-filler(Gamma;A;filler) ∧ uniform-Kan-A-filler(Gamma;A;filler)
⊢ <(A)s, λI,alpha. (filler I (s)alpha)> ∈ A:{Delta ⊢ _} × (I:(Cname List)
                                                  ⟶ alpha:Delta(I)
                                                  ⟶ J:(nameset(I) List)
                                                  ⟶ x:nameset(I)
                                                  ⟶ i:ℕ2
                                                  ⟶ A-open-box(Delta;A;I;alpha;J;x;i)
                                                  ⟶ A(alpha))
BY
{ (MemCD
   THENL [TACTIC:Auto
         ; TACTIC:(RepeatFor 6 (FunExt THENL [Id; Auto] ) THEN Reduce 0 THEN RWO "csm-type-at" 0 THEN Auto)
         ; TACTIC:Auto]
) }

---

Latex:

---

Latex:

1.  Delta  :  CubicalSet
2.  Gamma  :  CubicalSet
3.  s  :  Delta  {}\mrightarrow{}  Gamma
4.  A  :  \{Gamma  \mvdash{}  \_\}
5.  filler  :  I:(Cname  List)
{}\mrightarrow{}  alpha:Gamma(I)
{}\mrightarrow{}  J:(nameset(I)  List)
{}\mrightarrow{}  x:nameset(I)
{}\mrightarrow{}  i:\mBbbN{}2
{}\mrightarrow{}  A-open-box(Gamma;A;I;alpha;J;x;i)
{}\mrightarrow{}  A(alpha)
6.  Kan-A-filler(Gamma;A;filler)  \mwedge{}  uniform-Kan-A-filler(Gamma;A;filler)
\mvdash{}  <(A)s,  \mlambda{}I,alpha.  (filler  I  (s)alpha)>  \mmember{}  A:\{Delta  \mvdash{}  \_\}  \mtimes{}  (I:(Cname  List)
                                                                                                    {}\mrightarrow{}  alpha:Delta(I)
                                                                                                    {}\mrightarrow{}  J:(nameset(I)  List)
                                                                                                    {}\mrightarrow{}  x:nameset(I)
                                                                                                    {}\mrightarrow{}  i:\mBbbN{}2
                                                                                                    {}\mrightarrow{}  A-open-box(Delta;A;I;alpha;J;x;i)
                                                                                                    {}\mrightarrow{}  A(alpha))


By

---

Latex:
(MemCD
  THENL  [TACTIC:Auto
              ;  TACTIC:(RepeatFor  6  (FunExt  THENL  [Id;  Auto]  )
                                  THEN  Reduce  0
                                  THEN  RWO  "csm-type-at"  0
                                  THEN  Auto)
              ;  TACTIC:Auto]
)

---

Home Index