---

Step * of Lemma csm-equiv_comp

No Annotations
∀[H,K:j⊢]. ∀[tau:K j⟶ H]. ∀[A,E:{H ⊢ _}]. ∀[cA:H +⊢ Compositon(A)]. ∀[cE:H +⊢ Compositon(E)].
  ((equiv_comp(H;A;E;cA;cE))tau = equiv_comp(K;(A)tau;(E)tau;(cA)tau;(cE)tau) ∈ K ⊢ Compositon(Equiv((A)tau;(E)tau)))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert (q)p ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _:((((A)tau ⟶ (E)tau))p)p} BY
               Auto)
   THEN ((InstLemma `cubical-fun-p` [⌜K⌝;⌜(A)tau⌝;⌜(E)tau⌝;⌜((A)tau ⟶ (E)tau)⌝]⋅ THENA Auto)
         THEN (InstLemmaIJ `cubical-fun-p` [⌜K.((A)tau ⟶ (E)tau)⌝;⌜((A)tau)p⌝;⌜((E)tau)p⌝;⌜((E)tau)p⌝]⋅ THENA Auto)
         THEN (Assert (q)p ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _:((((A)tau)p)p ⟶ (((E)tau)p)p)} BY
                     ((InferEqualTypeGen THEN Try (Trivial)) THEN EqCDA THEN NthHypEqGen (-1) THEN EqCDA THEN Auto)))
   THEN (RWO "csm-equiv_comp-sq" 0 THENA Auto)
   THEN Unfolds ``equiv_comp cubical-equiv`` 0
   THEN EqCDA
   THEN (GenConcl ⌜fiber-comp(K.((A)tau ⟶ (E)tau).((E)tau)p;(((A)tau)p)p;(((E)tau)p)p;(q)p;q;(((cA)tau)p)p;
                              (((cE)tau)p)p)
                   = v
                   ∈ K.((A)tau ⟶ (E)tau).((E)tau)p +⊢ Compositon(Fiber((q)p;q))⌝⋅
         THENA Auto
         )
   THEN (Enough to prove K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ Fiber((q)p;q)
         = (Fiber((q)p;q))tau++
         ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}
          Because (StrengthenEquation (-1) THEN Symmetry THEN EquationFromHyp (-1)))) }

1
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. A : {H ⊢ _}
5. E : {H ⊢ _}
6. cA : H +⊢ Compositon(A)
7. cE : H +⊢ Compositon(E)
8. (q)p ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _:((((A)tau ⟶ (E)tau))p)p}
9. (((A)tau ⟶ (E)tau))p = (K.((A)tau ⟶ (E)tau) ⊢ ((A)tau)p ⟶ ((E)tau)p) ∈ {K.((A)tau ⟶ (E)tau) ⊢ _}
10. ((((A)tau)p ⟶ ((E)tau)p))p
= (K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ (((A)tau)p)p ⟶ (((E)tau)p)p)
∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}
11. (q)p ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _:((((A)tau)p)p ⟶ (((E)tau)p)p)}
12. v : K.((A)tau ⟶ (E)tau).((E)tau)p +⊢ Compositon(Fiber((q)p;q))
13. fiber-comp(K.((A)tau ⟶ (E)tau).((E)tau)p;(((A)tau)p)p;(((E)tau)p)p;(q)p;q;(((cA)tau)p)p;(((cE)tau)p)p)
= v
∈ K.((A)tau ⟶ (E)tau).((E)tau)p +⊢ Compositon(Fiber((q)p;q))
⊢ K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ Fiber((q)p;q) = (Fiber((q)p;q))tau++ ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}

2
.....aux..... 
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. A : {H ⊢ _}
5. E : {H ⊢ _}
6. cA : H +⊢ Compositon(A)
7. cE : H +⊢ Compositon(E)
8. (q)p ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _:((((A)tau ⟶ (E)tau))p)p}
9. (((A)tau ⟶ (E)tau))p = (K.((A)tau ⟶ (E)tau) ⊢ ((A)tau)p ⟶ ((E)tau)p) ∈ {K.((A)tau ⟶ (E)tau) ⊢ _}
10. ((((A)tau)p ⟶ ((E)tau)p))p
= (K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ (((A)tau)p)p ⟶ (((E)tau)p)p)
∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}
11. (q)p ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _:((((A)tau)p)p ⟶ (((E)tau)p)p)}
12. v : K.((A)tau ⟶ (E)tau).((E)tau)p +⊢ Compositon(Fiber((q)p;q))
13. fiber-comp(K.((A)tau ⟶ (E)tau).((E)tau)p;(((A)tau)p)p;(((E)tau)p)p;(q)p;q;(((cA)tau)p)p;(((cE)tau)p)p)
= v
∈ K.((A)tau ⟶ (E)tau).((E)tau)p +⊢ Compositon(Fiber((q)p;q))
14. K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ Fiber((q)p;q) = (Fiber((q)p;q))tau++ ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}
15. Z : {z:{K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _}| 
         (z = K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ Fiber((q)p;q) ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _})
         ∧ (z = (Fiber((q)p;q))tau++ ∈ {K.((A)tau ⟶ (E)tau).((E)tau)p ⊢ _})} 
⊢ pi_comp(K.((A)tau ⟶ (E)tau);((E)tau)p;((cE)tau)p;contractible_comp(K.((A)tau ⟶ (E)tau).((E)tau)p;Z;v))
  ∈ K.((A)tau ⟶ (E)tau) +⊢ Compositon(IsEquiv(((A)tau)p;((E)tau)p;q))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K:j\mvdash{}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].  \mforall{}[A,E:\{H  \mvdash{}  \_\}].  \mforall{}[cA:H  +\mvdash{}  Compositon(A)].  \mforall{}[cE:H  +\mvdash{}  Compositon(E)].
    ((equiv\_comp(H;A;E;cA;cE))tau  =  equiv\_comp(K;(A)tau;(E)tau;(cA)tau;(cE)tau))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  (q)p  \mmember{}  \{K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  \_:((((A)tau  {}\mrightarrow{}  (E)tau))p)p\}  BY
                          Auto)
  THEN  ((InstLemma  `cubical-fun-p`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}(A)tau\mkleeneclose{};\mkleeneopen{}(E)tau\mkleeneclose{};\mkleeneopen{}((A)tau  {}\mrightarrow{}  (E)tau)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemmaIJ  `cubical-fun-p`  [\mkleeneopen{}K.((A)tau  {}\mrightarrow{}  (E)tau)\mkleeneclose{};\mkleeneopen{}((A)tau)p\mkleeneclose{};\mkleeneopen{}((E)tau)p\mkleeneclose{};\mkleeneopen{}((E)tau)p\mkleeneclose{}
                          ]\mcdot{}
                          THENA  Auto
                          )
              THEN  (Assert  (q)p  \mmember{}  \{K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  \_:((((A)tau)p)p  {}\mrightarrow{}  (((E)tau)p)p)\}  BY
                                      ((InferEqualTypeGen  THEN  Try  (Trivial))
                                        THEN  EqCDA
                                        THEN  NthHypEqGen  (-1)
                                        THEN  EqCDA
                                        THEN  Auto)))
  THEN  (RWO  "csm-equiv\_comp-sq"  0  THENA  Auto)
  THEN  Unfolds  ``equiv\_comp  cubical-equiv``  0
  THEN  EqCDA
  THEN  (GenConcl  \mkleeneopen{}fiber-comp(K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p;(((A)tau)p)p;(((E)tau)p)p;(q)p;q;
                                                        (((cA)tau)p)p;(((cE)tau)p)p)
                                  =  v\mkleeneclose{}\mcdot{}
              THENA  Auto
              )
  THEN  (Enough  to  prove  K.((A)tau  {}\mrightarrow{}  (E)tau).((E)tau)p  \mvdash{}  Fiber((q)p;q)  =  (Fiber((q)p;q))tau++
                Because  (StrengthenEquation  (-1)  THEN  Symmetry  THEN  EquationFromHyp  (-1))))

---

Home Index