---

Step * 1 1 of Lemma unglue-term-1


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. b : {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
7. unglue(b) = unglue(b) ∈ {Gamma ⊢ _:A}
8. app(w; b) = unglue(b) ∈ {Gamma, phi ⊢ _:A}
9. phi = 1(𝔽) ∈ {Gamma ⊢ _:𝔽}
⊢ unglue(b) = app(w; b) ∈ {Gamma ⊢ _:A}
BY
{ (SubsumeC ⌜{Gamma, phi ⊢ _:A}⌝⋅ THEN Auto) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. b : {Gamma ⊢ _:Glue [phi ⊢→ (T;w)] A}
7. unglue(b) = unglue(b) ∈ {Gamma ⊢ _:A}
8. app(w; b) = unglue(b) ∈ {Gamma, phi ⊢ _:A}
9. phi = 1(𝔽) ∈ {Gamma ⊢ _:𝔽}
10. unglue(b) = app(w; b) ∈ {Gamma, phi ⊢ _:A}
⊢ {Gamma, phi ⊢ _:A} ⊆r {Gamma ⊢ _: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.  b  :  \{Gamma  \mvdash{}  \_:Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A\}
7.  unglue(b)  =  unglue(b)
8.  app(w;  b)  =  unglue(b)
9.  phi  =  1(\mBbbF{})
\mvdash{}  unglue(b)  =  app(w;  b)


By

---

Latex:
(SubsumeC  \mkleeneopen{}\{Gamma,  phi  \mvdash{}  \_:A\}\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index