---

Step * of Lemma csm-Kan-cubical-type_wf

∀[Delta,Gamma:CubicalSet]. ∀[s:Delta ⟶ Gamma]. ∀[AK:{Gamma ⊢ _(Kan)}].  ((AK)s ∈ {Delta ⊢ _(Kan)})
BY
{ TACTIC:(Auto
          THEN RepeatFor 2 (DVar `AK')
          THEN Unfold `csm-Kan-cubical-type` 0
          THEN All Reduce
          THEN RenameVar `filler' (-2)
          THEN MemTypeCD
          THEN Reduce 0) }

1
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))

2
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)
⊢ Kan-A-filler(Delta;(A)s;λI,alpha. (filler I (s)alpha)) ∧ uniform-Kan-A-filler(Delta;(A)s;λI,alpha. (filler I (s)alpha)\000C)

3
.....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)
7. p : 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))
⊢ istype(let A,filler = p 
         in Kan-A-filler(Delta;A;filler) ∧ uniform-Kan-A-filler(Delta;A;filler))

---

Latex:

---

Latex:
\mforall{}[Delta,Gamma:CubicalSet].  \mforall{}[s:Delta  {}\mrightarrow{}  Gamma].  \mforall{}[AK:\{Gamma  \mvdash{}  \_(Kan)\}].    ((AK)s  \mmember{}  \{Delta  \mvdash{}  \_(Kan)\})


By

---

Latex:
TACTIC:(Auto
                THEN  RepeatFor  2  (DVar  `AK')
                THEN  Unfold  `csm-Kan-cubical-type`  0
                THEN  All  Reduce
                THEN  RenameVar  `filler'  (-2)
                THEN  MemTypeCD
                THEN  Reduce  0)

---

Home Index