---

Step * 1 of Lemma equiv-witness_wf


1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:(T ⟶ A)}
5. iseq : {G ⊢ _:IsEquiv(T;A;f)}
⊢ cubical-pair(f;iseq) ∈ {G ⊢ _:Σ (T ⟶ A) IsEquiv((T)p;(A)p;q)}
BY
{ MemCD }

1
.....implicit subterm..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:(T ⟶ A)}
5. iseq : {G ⊢ _:IsEquiv(T;A;f)}
⊢ G j⊢

2
.....implicit subterm..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:(T ⟶ A)}
5. iseq : {G ⊢ _:IsEquiv(T;A;f)}
⊢ G ⊢ (T ⟶ A)

3
.....implicit subterm..... 
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:(T ⟶ A)}
5. iseq : {G ⊢ _:IsEquiv(T;A;f)}
⊢ G.(T ⟶ A) ⊢ IsEquiv((T)p;(A)p;q)

4
.....subterm..... T:t
1:n
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:(T ⟶ A)}
5. iseq : {G ⊢ _:IsEquiv(T;A;f)}
⊢ f ∈ {G ⊢ _:(T ⟶ A)}

5
.....subterm..... T:t
2:n
1. G : CubicalSet{j}
2. A : {G ⊢ _}
3. T : {G ⊢ _}
4. f : {G ⊢ _:(T ⟶ A)}
5. iseq : {G ⊢ _:IsEquiv(T;A;f)}
⊢ iseq ∈ {G ⊢ _:(IsEquiv((T)p;(A)p;q))[f]}

---

Latex:

---

Latex:

1.  G  :  CubicalSet\{j\}
2.  A  :  \{G  \mvdash{}  \_\}
3.  T  :  \{G  \mvdash{}  \_\}
4.  f  :  \{G  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}
5.  iseq  :  \{G  \mvdash{}  \_:IsEquiv(T;A;f)\}
\mvdash{}  cubical-pair(f;iseq)  \mmember{}  \{G  \mvdash{}  \_:\mSigma{}  (T  {}\mrightarrow{}  A)  IsEquiv((T)p;(A)p;q)\}


By

---

Latex:
MemCD

---

Home Index