---

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

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ Compositon(A)].
  (cop-to-cfun(cfun-to-cop(Gamma;A;cA)) = cA ∈ Gamma ⊢ Compositon(A))
BY
{ (Intros
   THEN Symmetry
   THEN D -1
   THEN EqTypeCD
   THEN Auto
   THEN Unfold `composition-function` 0
   THEN RepeatFor 5 ((FunExt THENA Auto))
   THEN (EqTypeCD THENW 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(𝕀)]]}
⊢ (cA H sigma phi u a0) = (cop-to-cfun(cfun-to-cop(Gamma;A;cA)) H sigma phi u a0) ∈ {H ⊢ _:((A)sigma)[1(𝕀)]}

2
.....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(𝕀)]}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  Compositon(A)].
    (cop-to-cfun(cfun-to-cop(Gamma;A;cA))  =  cA)


By

---

Latex:
(Intros
  THEN  Symmetry
  THEN  D  -1
  THEN  EqTypeCD
  THEN  Auto
  THEN  Unfold  `composition-function`  0
  THEN  RepeatFor  5  ((FunExt  THENA  Auto))
  THEN  (EqTypeCD  THENW  Auto))

---

Home Index