---

Step * 2 of Lemma unglue-term_wf

.....set predicate..... 
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}
⊢ ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).  ((unglue(b) I a a f) = (unglue(b) J f(a)) ∈ A(f(a)))
BY
{ (Intros THEN RepUR ``unglue-term`` 0) }

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. I : fset(ℕ)
8. J : fset(ℕ)
9. f : J ⟶ I
10. a : Gamma(I)
⊢ (if (phi(a)==1) then w I a I 1 b(a) else snd(b(a)) fi  a f)
= if (phi(f(a))==1) then w J f(a) J 1 b(f(a)) else snd(b(f(a))) fi 
∈ A(f(a))

---

Latex:

---

Latex:
.....set  predicate..... 
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\}
\mvdash{}  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:Gamma(I).    ((unglue(b)  I  a  a  f)  =  (unglue(b)  J  f(a)))


By

---

Latex:
(Intros  THEN  RepUR  ``unglue-term``  0)

---

Home Index