---

Step * of Lemma csm-revfill

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma.𝕀 ⊢ _}]. ∀[cA:Gamma.𝕀 ⊢ Compositon(A)]. ∀[a1:{Gamma ⊢ _:(A)[1(𝕀)]}]. ∀[Delta:j⊢].
∀[s:Delta j⟶ Gamma].
  ((revfill(Gamma;cA;a1))s+ = revfill(Delta;(cA)s+;(a1)s) ∈ {Delta.𝕀 ⊢ _:(A)s+})
BY
{ ((Intros THEN Unfold `revfill` 0)
   THEN (Assert discr(⋅) ∈ {Gamma.𝕀, (0(𝔽))p ⊢ _:A} BY
               (RWO "csm-face-0" 0 THEN Auto))
   THEN (Assert a1 ∈ {Gamma ⊢ _:(A)[1(𝕀)][0(𝔽) |⟶ ⋅[1]]} BY
               (DoSubsume THEN Auto THEN BLemma `trivial-constrained-term` THEN Auto))
   THEN (InstLemma `csm-rev_fill_term` [⌜Gamma⌝;⌜0(𝔽)⌝;⌜A⌝;⌜cA⌝;⌜discr(⋅)⌝;⌜a1⌝;⌜Delta⌝;⌜s⌝]⋅ THENA Auto)
   THEN (EqTypeHD (-1) THENA Auto)) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma.𝕀 ⊢ _}
3. cA : Gamma.𝕀 ⊢ Compositon(A)
4. a1 : {Gamma ⊢ _:(A)[1(𝕀)]}
5. Delta : CubicalSet{j}
6. s : Delta j⟶ Gamma
7. discr(⋅) ∈ {Gamma.𝕀, (0(𝔽))p ⊢ _:A}
8. a1 ∈ {Gamma ⊢ _:(A)[1(𝕀)][0(𝔽) |⟶ ⋅[1]]}
9. (rev_fill_term(Gamma;cA;0(𝔽);discr(⋅);a1))s+
= rev_fill_term(Delta;(cA)s+;(0(𝔽))s;(discr(⋅))s+;(a1)s)
∈ {Delta.𝕀 ⊢ _:(A)s+}
10. (discr(⋅))s+ = (rev_fill_term(Gamma;cA;0(𝔽);discr(⋅);a1))s+ ∈ {Delta.𝕀, ((0(𝔽))s)p ⊢ _:(A)s+}
⊢ (rev_fill_term(Gamma;cA;0(𝔽);discr(⋅);a1))s+ = rev_fill_term(Delta;(cA)s+;0(𝔽);discr(⋅);(a1)s) ∈ {Delta.𝕀 ⊢ _:(A)s+}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[cA:Gamma.\mBbbI{}  \mvdash{}  Compositon(A)].  \mforall{}[a1:\{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})]\}].
\mforall{}[Delta:j\mvdash{}].  \mforall{}[s:Delta  j{}\mrightarrow{}  Gamma].
    ((revfill(Gamma;cA;a1))s+  =  revfill(Delta;(cA)s+;(a1)s))


By

---

Latex:
((Intros  THEN  Unfold  `revfill`  0)
  THEN  (Assert  discr(\mcdot{})  \mmember{}  \{Gamma.\mBbbI{},  (0(\mBbbF{}))p  \mvdash{}  \_:A\}  BY
                          (RWO  "csm-face-0"  0  THEN  Auto))
  THEN  (Assert  a1  \mmember{}  \{Gamma  \mvdash{}  \_:(A)[1(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  \mcdot{}[1]]\}  BY
                          (DoSubsume  THEN  Auto  THEN  BLemma  `trivial-constrained-term`  THEN  Auto))
  THEN  (InstLemma  `csm-rev\_fill\_term`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}0(\mBbbF{})\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}cA\mkleeneclose{};\mkleeneopen{}discr(\mcdot{})\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}Delta\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (EqTypeHD  (-1)  THENA  Auto))

---

Home Index