---

Step * 2 of Lemma glue-term_wf2


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. t : {Gamma, phi ⊢ _:T}
7. a : {Gamma ⊢ _:A[phi |⟶ app(w; t)]}
8. glue [phi ⊢→ t] a ∈ {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
9. a1 : {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
10. Gamma ⊢ Glue [phi ⊢→ (T;w)] A = T ∈ {Gamma, phi ⊢ _}
⊢ istype(t = a1 ∈ {Gamma, phi ⊢ _:Glue [phi ⊢→ (T;w)] A})
BY
{ EqualityIsType1 }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. t : {Gamma, phi ⊢ _:T}
7. a : {Gamma ⊢ _:A[phi |⟶ app(w; t)]}
8. glue [phi ⊢→ t] a ∈ {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
9. a1 : {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
10. Gamma ⊢ Glue [phi ⊢→ (T;w)] A = T ∈ {Gamma, phi ⊢ _}
⊢ istype({Gamma, phi ⊢ _:Glue [phi ⊢→ (T;w)] A})

2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. t : {Gamma, phi ⊢ _:T}
7. a : {Gamma ⊢ _:A[phi |⟶ app(w; t)]}
8. glue [phi ⊢→ t] a ∈ {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
9. a1 : {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
10. Gamma ⊢ Glue [phi ⊢→ (T;w)] A = T ∈ {Gamma, phi ⊢ _}
⊢ t ∈ {Gamma, phi ⊢ _:Glue [phi ⊢→ (T;w)] A}

3
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. t : {Gamma, phi ⊢ _:T}
7. a : {Gamma ⊢ _:A[phi |⟶ app(w; t)]}
8. glue [phi ⊢→ t] a ∈ {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
9. a1 : {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
10. Gamma ⊢ Glue [phi ⊢→ (T;w)] A = T ∈ {Gamma, phi ⊢ _}
⊢ a1 ∈ {Gamma, phi ⊢ _:Glue [phi ⊢→ (T;w)] A}

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  T  :  \{Gamma,  phi  \mvdash{}  \_\}
5.  w  :  \{Gamma,  phi  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}
6.  t  :  \{Gamma,  phi  \mvdash{}  \_:T\}
7.  a  :  \{Gamma  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  app(w;  t)]\}
8.  glue  [phi  \mvdash{}\mrightarrow{}  t]  a  \mmember{}  \{Gamma  \mvdash{}  \_:Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A\}
9.  a1  :  \{Gamma  \mvdash{}  \_:Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A\}
10.  Gamma  \mvdash{}  Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A  =  T
\mvdash{}  istype(t  =  a1)


By

---

Latex:
EqualityIsType1

---

Home Index