---

Step * of Lemma equiv-term-0-subset-1

No Annotations
∀[G:j⊢]. ∀[phi:{G ⊢ _:𝔽}].
  ∀[psi:{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 psi = 1(𝔽) ∈ {G ⊢ _:𝔽} 
  supposing phi = 0(𝔽) ∈ {G ⊢ _:𝔽}
BY
{ (Intros
   THEN (InstLemma `equiv-term-0` [⌜G⌝;⌜phi⌝;⌜A⌝;⌜T⌝;⌜f⌝;⌜a⌝;⌜t⌝;⌜c⌝;⌜cF⌝]⋅ THENA Auto)
   THEN (NthHypEqGen (-1) THEN EqCDA THEN (Assert t ∈ {G, phi ⊢ _:T} BY (SubsumeC ⌜{G, 0(𝔽) ⊢ _:T}⌝⋅ THEN Auto)))
   THEN InstLemma `equiv-term-subset` 
   [⌜G⌝;⌜phi⌝;⌜A⌝;⌜T⌝;⌜f⌝;⌜t⌝;⌜a⌝;⌜c⌝;⌜cF⌝;⌜psi⌝]⋅
   THEN Try (Trivial)) }

1
.....wf..... 
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. phi = 0(𝔽) ∈ {G ⊢ _:𝔽}
4. psi : {G ⊢ _:𝔽}
5. psi = 1(𝔽) ∈ {G ⊢ _:𝔽}
6. A : {G ⊢ _}
7. T : {G ⊢ _}
8. f : {G ⊢ _:Equiv(T;A)}
9. a : {G ⊢ _:A}
10. t : Top
11. c : Top
12. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
13. equiv f [phi ⊢→ (t,  c)] a = transprt(G;(cF)p;contr-center(equiv-contr(f;a))) ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
14. t ∈ {G, phi ⊢ _:T}
⊢ c ∈ {G, phi ⊢ _:(Path_A a app(equiv-fun(f); t))}

2
.....wf..... 
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. phi = 0(𝔽) ∈ {G ⊢ _:𝔽}
4. psi : {G ⊢ _:𝔽}
5. psi = 1(𝔽) ∈ {G ⊢ _:𝔽}
6. A : {G ⊢ _}
7. T : {G ⊢ _}
8. f : {G ⊢ _:Equiv(T;A)}
9. a : {G ⊢ _:A}
10. t : Top
11. c : Top
12. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
13. equiv f [phi ⊢→ (t,  c)] a = transprt(G;(cF)p;contr-center(equiv-contr(f;a))) ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
14. t ∈ {G, phi ⊢ _:T}
⊢ cF ∈ G ⊢ Compositon(Fiber(equiv-fun(f);a))

3
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. phi = 0(𝔽) ∈ {G ⊢ _:𝔽}
4. psi : {G ⊢ _:𝔽}
5. psi = 1(𝔽) ∈ {G ⊢ _:𝔽}
6. A : {G ⊢ _}
7. T : {G ⊢ _}
8. f : {G ⊢ _:Equiv(T;A)}
9. a : {G ⊢ _:A}
10. t : Top
11. c : Top
12. cF : G +⊢ Compositon(Fiber(equiv-fun(f);a))
13. equiv f [phi ⊢→ (t,  c)] a = transprt(G;(cF)p;contr-center(equiv-contr(f;a))) ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}
14. t ∈ {G, phi ⊢ _:T}
15. equiv f [phi ⊢→ (t,  c)] a = equiv f [phi ⊢→ (t,  c)] a ∈ {G, psi ⊢ _:Fiber(equiv-fun(f);a)}
⊢ equiv f [phi ⊢→ (t,  c)] a = equiv f [phi ⊢→ (t,  c)] a ∈ {G ⊢ _:Fiber(equiv-fun(f);a)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[phi:\{G  \mvdash{}  \_:\mBbbF{}\}].
    \mforall{}[psi:\{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  psi  =  1(\mBbbF{}) 
    supposing  phi  =  0(\mBbbF{})


By

---

Latex:
(Intros
  THEN  (InstLemma  `equiv-term-0`  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}cF\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (NthHypEqGen  (-1)
              THEN  EqCDA
              THEN  (Assert  t  \mmember{}  \{G,  phi  \mvdash{}  \_:T\}  BY
                                      (SubsumeC  \mkleeneopen{}\{G,  0(\mBbbF{})  \mvdash{}  \_:T\}\mkleeneclose{}\mcdot{}  THEN  Auto)))
  THEN  InstLemma  `equiv-term-subset` 
  [\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}cF\mkleeneclose{};\mkleeneopen{}psi\mkleeneclose{}]\mcdot{}
  THEN  Try  (Trivial))

---

Home Index