---

Step * 2 of Lemma comp-fun-to-comp-op-inverse

.....set predicate..... 
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
5. H : CubicalSet{j}
6. sigma : H.𝕀 j⟶ Gamma
7. phi : {H ⊢ _:𝔽}
8. u : {H, phi.𝕀 ⊢ _:(A)sigma}
9. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
⊢ (u)[1(𝕀)] = (cA H sigma phi u a0) ∈ {H, phi ⊢ _:((A)sigma)[1(𝕀)]}
BY
{ (GenConclTerm ⌜cA H sigma phi u a0⌝⋅ THENA Auto) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : composition-function{j:l,i:l}(Gamma;A)
4. uniform-comp-function{j:l, i:l}(Gamma; A; cA)
5. H : CubicalSet{j}
6. sigma : H.𝕀 j⟶ Gamma
7. phi : {H ⊢ _:𝔽}
8. u : {H, phi.𝕀 ⊢ _:(A)sigma}
9. a0 : {H ⊢ _:((A)sigma)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
10. v : {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}
11. (cA H sigma phi u a0) = v ∈ {H ⊢ _:((A)sigma)[1(𝕀)][phi |⟶ (u)[1(𝕀)]]}
⊢ (u)[1(𝕀)] = v ∈ {H, phi ⊢ _:((A)sigma)[1(𝕀)]}

---

Latex:

---

Latex:
.....set  predicate..... 
1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  cA  :  composition-function\{j:l,i:l\}(Gamma;A)
4.  uniform-comp-function\{j:l,  i:l\}(Gamma;  A;  cA)
5.  H  :  CubicalSet\{j\}
6.  sigma  :  H.\mBbbI{}  j{}\mrightarrow{}  Gamma
7.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
8.  u  :  \{H,  phi.\mBbbI{}  \mvdash{}  \_:(A)sigma\}
9.  a0  :  \{H  \mvdash{}  \_:((A)sigma)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
\mvdash{}  (u)[1(\mBbbI{})]  =  (cA  H  sigma  phi  u  a0)


By

---

Latex:
(GenConclTerm  \mkleeneopen{}cA  H  sigma  phi  u  a0\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index