---

Step * 1 of Lemma unglue-term_wf


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}
⊢ unglue(b) ∈ I:fset(ℕ) ⟶ a:Gamma(I) ⟶ A(a)
BY
{ (RepeatFor 2 ((FunExt THENA Auto))
   THEN RepUR ``unglue-term`` 0
   THEN RenameVar `rho' (-1)
   THEN skip{(BoolCase ⌜(phi(rho)==1)⌝⋅ THENA 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. I : fset(ℕ)
8. rho : Gamma(I)
⊢ if (phi(rho)==1) then w I rho I 1 b(rho) else snd(b(rho)) fi  ∈ A(rho)

---

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\}
\mvdash{}  unglue(b)  \mmember{}  I:fset(\mBbbN{})  {}\mrightarrow{}  a:Gamma(I)  {}\mrightarrow{}  A(a)


By

---

Latex:
(RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  RepUR  ``unglue-term``  0
  THEN  RenameVar  `rho'  (-1)
  THEN  skip\{(BoolCase  \mkleeneopen{}(phi(rho)==1)\mkleeneclose{}\mcdot{}  THENA  Auto)\})

---

Home Index