---

Step * 1 of Lemma equiv-term-0-subset-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))}
BY
{ (SubsumeC ⌜{G, 0(𝔽) ⊢ _:(Path_A a app(equiv-fun(f); t))}⌝⋅ THENL [Auto; BLemma `subset-cubical-term`]) }

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}
15. c = c ∈ {G, 0(𝔽) ⊢ _:(Path_A a app(equiv-fun(f); t))}
⊢ G, 0(𝔽) j⊢

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}
15. c = c ∈ {G, 0(𝔽) ⊢ _:(Path_A a app(equiv-fun(f); t))}
⊢ G, phi j⊢

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. c = c ∈ {G, 0(𝔽) ⊢ _:(Path_A a app(equiv-fun(f); t))}
⊢ sub_cubical_set{j:l}(G, phi; G, 0(𝔽))

4
.....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}
15. c = c ∈ {G, 0(𝔽) ⊢ _:(Path_A a app(equiv-fun(f); t))}
⊢ G, 0(𝔽) ⊢ (Path_A a app(equiv-fun(f); t))

---

Latex:

---

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


By

---

Latex:
(SubsumeC  \mkleeneopen{}\{G,  0(\mBbbF{})  \mvdash{}  \_:(Path\_A  a  app(equiv-fun(f);  t))\}\mkleeneclose{}\mcdot{}
  THENL  [Auto;  BLemma  `subset-cubical-term`]
)

---

Home Index