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


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

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


Latex:


Latex:

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{}  (cA  H  sigma  phi  u  a0)  =  (cop-to-cfun(cfun-to-cop(Gamma;A;cA))  H  sigma  phi  u  a0)


By


Latex:
(CubicalTermEqual  THENA  Auto)




Home Index