---

Step * 1 of Lemma glue-unglue


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. b : I:fset(ℕ) ⟶ a:Gamma(I) ⟶ Glue [phi ⊢→ (T;w)] A(a)
7. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).  ((b I a a f) = (b J f(a)) ∈ Glue [phi ⊢→ (T;w)] A(f(a)))
8. I : fset(ℕ)
9. a : Gamma(I)
⊢ (b I a) = (glue [phi ⊢→ b] unglue(b) I a) ∈ Glue [phi ⊢→ (T;w)] A(a)
BY
{ (RepUR ``glue-term unglue-term`` 0
   THEN (Assert b I a ∈ Glue [phi ⊢→ (T;w)] A(a) BY
               Auto)
   THEN RepUR ``glue-type glue-cube`` -1
   THEN RepUR ``glue-type glue-cube cubical-term-at`` 0
   THEN Fold `cubical-term-at` 0
   THEN (BoolCase ⌜(phi(a)==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 : I:fset(ℕ) ⟶ a:Gamma(I) ⟶ Glue [phi ⊢→ (T;w)] A(a)
7. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).  ((b I a a f) = (b J f(a)) ∈ Glue [phi ⊢→ (T;w)] A(f(a)))
8. I : fset(ℕ)
9. a : Gamma(I)
10. b I a ∈ if (phi(a)==1)
    then T(a)
    else {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(a)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(a)) × A(a)| 
          let t,a@0 = ta 
          in glue-equations(Gamma;A;phi;T;w;I;a;t;a@0)} 
    fi 
11. phi(a) = 1 ∈ Point(face_lattice(I))
⊢ b(a) = b(a) ∈ T(a)

2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. b : I:fset(ℕ) ⟶ a:Gamma(I) ⟶ Glue [phi ⊢→ (T;w)] A(a)
7. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).  ((b I a a f) = (b J f(a)) ∈ Glue [phi ⊢→ (T;w)] A(f(a)))
8. I : fset(ℕ)
9. a : Gamma(I)
10. ¬(phi(a) = 1 ∈ Point(face_lattice(I)))
11. b I a ∈ {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(a)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(a)) × A(a)| 
             let t,a@0 = ta 
             in glue-equations(Gamma;A;phi;T;w;I;a;t;a@0)} 
⊢ b(a)
= <λJ,f. b(f(a)), snd(b(a))>
∈ {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(a)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(a)) × A(a)| 
   let t,a@0 = ta 
   in glue-equations(Gamma;A;phi;T;w;I;a;t;a@0)} 

---

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  :  I:fset(\mBbbN{})  {}\mrightarrow{}  a:Gamma(I)  {}\mrightarrow{}  Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A(a)
7.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:Gamma(I).    ((b  I  a  a  f)  =  (b  J  f(a)))
8.  I  :  fset(\mBbbN{})
9.  a  :  Gamma(I)
\mvdash{}  (b  I  a)  =  (glue  [phi  \mvdash{}\mrightarrow{}  b]  unglue(b)  I  a)


By

---

Latex:
(RepUR  ``glue-term  unglue-term``  0
  THEN  (Assert  b  I  a  \mmember{}  Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A(a)  BY
                          Auto)
  THEN  RepUR  ``glue-type  glue-cube``  -1
  THEN  RepUR  ``glue-type  glue-cube  cubical-term-at``  0
  THEN  Fold  `cubical-term-at`  0
  THEN  (BoolCase  \mkleeneopen{}(phi(a)==1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index