---

Step * of Lemma equiv-term-0

No Annotations
∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}].
  ∀[A,T:{G ⊢ _}]. ∀[f:{G ⊢ _:Equiv(T;A)}]. ∀[a:{G ⊢ _:A}]. ∀[t,c:Top]. ∀[cF:G +⊢ Compositon(Fiber(equiv-fun(f);a))].
    (equiv f [phi ⊢→ (t,  c)] a = transprt(G;(cF)p;contr-center(equiv-contr(f;a))) ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}) 
  supposing phi = 0(𝔽) ∈ {G ⊢ _:𝔽}
BY
{ (Intros
   THEN RepUR ``equiv-term let`` 0
   THEN (GenConcl ⌜contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top⌝⋅ THENA Auto)
   THEN (InstLemma `equals-transprt` [⌜G⌝;⌜(Fiber(equiv-fun(f);a))p⌝;⌜(cF)p⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜ctr⌝;⌜xx⌝] (-1)⋅ THENA (InferEqualType THEN Auto))
   THEN NthHypEqGen (-1)
   THEN EqCDA) }

1
.....subterm..... T:t
1:n
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. phi = 0(𝔽) ∈ {G ⊢ _:𝔽}
4. A : {G ⊢ _}
5. T : {G ⊢ _}
6. f : {G ⊢ _:Equiv(T;A)}
7. a : {G ⊢ _:A}
8. t : Top
9. c : Top
10. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
11. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
12. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
13. xx : Top
14. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
15. ∀[a@0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}]. ∀[xx:Top].
      (comp (cF)p [0(𝔽) ⊢→ xx] a@0 = transprt(G;(cF)p;a@0) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]})
16. comp (cF)p [0(𝔽) ⊢→ xx] ctr = transprt(G;(cF)p;ctr) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]}
⊢ {G ⊢ _:Fiber(equiv-fun(f);a)} = {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]} ∈ 𝕌{[i | j']}

2
.....subterm..... T:t
2:n
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. phi = 0(𝔽) ∈ {G ⊢ _:𝔽}
4. A : {G ⊢ _}
5. T : {G ⊢ _}
6. f : {G ⊢ _:Equiv(T;A)}
7. a : {G ⊢ _:A}
8. t : Top
9. c : Top
10. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
11. ctr : {G ⊢ _:Fiber(equiv-fun(f);a)}
12. contr-center(equiv-contr(f;a)) = ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
13. xx : Top
14. (contr-path(equiv-contr(f;a);fiber-point(t;c)))p @ q = xx ∈ Top
15. ∀[a@0:{G ⊢ _:((Fiber(equiv-fun(f);a))p)[0(𝕀)]}]. ∀[xx:Top].
      (comp (cF)p [0(𝔽) ⊢→ xx] a@0 = transprt(G;(cF)p;a@0) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]})
16. comp (cF)p [0(𝔽) ⊢→ xx] ctr = transprt(G;(cF)p;ctr) ∈ {G ⊢ _:((Fiber(equiv-fun(f);a))p)[1(𝕀)]}
⊢ comp (cF)p [phi ⊢→ xx] ctr = comp (cF)p [0(𝔽) ⊢→ xx] ctr ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].
    \mforall{}[A,T:\{G  \mvdash{}  \_\}].  \mforall{}[f:\{G  \mvdash{}  \_:Equiv(T;A)\}].  \mforall{}[a:\{G  \mvdash{}  \_:A\}].  \mforall{}[t,c:Top].
    \mforall{}[cF:G  +\mvdash{}  Compositon(Fiber(equiv-fun(f);a))].
        (equiv  f  [phi  \mvdash{}\mrightarrow{}  (t,    c)]  a  =  transprt(G;(cF)p;contr-center(equiv-contr(f;a)))) 
    supposing  phi  =  0(\mBbbF{})


By

---

Latex:
(Intros
  THEN  RepUR  ``equiv-term  let``  0
  THEN  (GenConcl  \mkleeneopen{}contr-center(equiv-contr(f;a))  =  ctr\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(contr-path(equiv-contr(f;a);fiber-point(t;c)))p  @  q  =  xx\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `equals-transprt`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}(Fiber(equiv-fun(f);a))p\mkleeneclose{};\mkleeneopen{}(cF)p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}ctr\mkleeneclose{};\mkleeneopen{}xx\mkleeneclose{}]  (-1)\mcdot{}  THENA  (InferEqualType  THEN  Auto))
  THEN  NthHypEqGen  (-1)
  THEN  EqCDA)

---

Home Index