---

Step * 1 of Lemma trans-const-path_wf


1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. a : {G ⊢ _:A}
5. ∀[u:{G.𝕀, 0(𝔽) ⊢ _:(A)p}]. ∀[a1:{G ⊢ _:((A)p)[1(𝕀)][0(𝔽) |⟶ u[1]]}].
     (rev_fill_term(G;(cA)p;0(𝔽);u;a1) ∈ {G.𝕀 ⊢ _:(A)p[0(𝔽) |⟶ u]})
6. discr(⋅) ∈ {G.𝕀, 0(𝔽) ⊢ _:(A)p}
7. a ∈ {G ⊢ _:((A)p)[1(𝕀)][0(𝔽) |⟶ discr(⋅)[1]]}
8. rev_fill_term(G;(cA)p;0(𝔽);discr(⋅);a) ∈ {G.𝕀 ⊢ _:(A)p}
⊢ comp rev-type-comp(G;(cA)p) [0(𝔽) ⊢→ (discr(⋅))(p;1-(q))] a = transprt-const(G;cA;a) ∈ {G ⊢ _:A}
BY
{ (Subst' rev-type-comp(G;(cA)p) ~ (cA)p 0 THENA (RepUR ``rev-type-comp`` 0 THEN CsmUnfoldingComp)) }

1
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. cA : G +⊢ Compositon(A)
4. a : {G ⊢ _:A}
5. ∀[u:{G.𝕀, 0(𝔽) ⊢ _:(A)p}]. ∀[a1:{G ⊢ _:((A)p)[1(𝕀)][0(𝔽) |⟶ u[1]]}].
     (rev_fill_term(G;(cA)p;0(𝔽);u;a1) ∈ {G.𝕀 ⊢ _:(A)p[0(𝔽) |⟶ u]})
6. discr(⋅) ∈ {G.𝕀, 0(𝔽) ⊢ _:(A)p}
7. a ∈ {G ⊢ _:((A)p)[1(𝕀)][0(𝔽) |⟶ discr(⋅)[1]]}
8. rev_fill_term(G;(cA)p;0(𝔽);discr(⋅);a) ∈ {G.𝕀 ⊢ _:(A)p}
⊢ comp (cA)p [0(𝔽) ⊢→ (discr(⋅))(p;1-(q))] a = transprt-const(G;cA;a) ∈ {G ⊢ _:A}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  cA  :  G  +\mvdash{}  Compositon(A)
4.  a  :  \{G  \mvdash{}  \_:A\}
5.  \mforall{}[u:\{G.\mBbbI{},  0(\mBbbF{})  \mvdash{}  \_:(A)p\}].  \mforall{}[a1:\{G  \mvdash{}  \_:((A)p)[1(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  u[1]]\}].
          (rev\_fill\_term(G;(cA)p;0(\mBbbF{});u;a1)  \mmember{}  \{G.\mBbbI{}  \mvdash{}  \_:(A)p[0(\mBbbF{})  |{}\mrightarrow{}  u]\})
6.  discr(\mcdot{})  \mmember{}  \{G.\mBbbI{},  0(\mBbbF{})  \mvdash{}  \_:(A)p\}
7.  a  \mmember{}  \{G  \mvdash{}  \_:((A)p)[1(\mBbbI{})][0(\mBbbF{})  |{}\mrightarrow{}  discr(\mcdot{})[1]]\}
8.  rev\_fill\_term(G;(cA)p;0(\mBbbF{});discr(\mcdot{});a)  \mmember{}  \{G.\mBbbI{}  \mvdash{}  \_:(A)p\}
\mvdash{}  comp  rev-type-comp(G;(cA)p)  [0(\mBbbF{})  \mvdash{}\mrightarrow{}  (discr(\mcdot{}))(p;1-(q))]  a  =  transprt-const(G;cA;a)


By

---

Latex:
(Subst'  rev-type-comp(G;(cA)p)  \msim{}  (cA)p  0  THENA  (RepUR  ``rev-type-comp``  0  THEN  CsmUnfoldingComp))

---

Home Index