---

Step * of Lemma glue-morph-id

No Annotations
∀Gamma:j⊢. ∀A:{Gamma ⊢ _}. ∀phi:{Gamma ⊢ _:𝔽}. ∀T:{Gamma, phi ⊢ _}. ∀w:{Gamma, phi ⊢ _:(T ⟶ A)}. ∀I:fset(ℕ).
∀a:Gamma(I). ∀u:glue-cube(Gamma;A;phi;T;w;I;a).
  (glue-morph(Gamma;A;phi;T;w;I;a;I;1;u) = u ∈ glue-cube(Gamma;A;phi;T;w;I;a))
BY
{ (Auto
   THEN (BLemma `equal-glue-cube` THENW Auto)
   THEN Unfold `glue-cube` -1
   THEN Unfold `glue-morph` 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. I : fset(ℕ)
7. a : Gamma(I)
8. u : 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 
9. phi(a) = 1 ∈ Point(face_lattice(I))
⊢ (u a 1) = u ∈ T(a)

2
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. T : {Gamma, phi ⊢ _}
5. w : {Gamma, phi ⊢ _:(T ⟶ A)}
6. I : fset(ℕ)
7. a : Gamma(I)
8. ¬(phi(a) = 1 ∈ Point(face_lattice(I)))
9. u : {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)} 
⊢ let t,a@0 = u 
  in if (phi(1(a))==1) then t I 1 else <λK,g. (t K 1 ⋅ g), (a@0 a 1)> fi 
= u
∈ (J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(a)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(a)) × A(a))

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}A:\{Gamma  \mvdash{}  \_\}.  \mforall{}phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}.  \mforall{}T:\{Gamma,  phi  \mvdash{}  \_\}.  \mforall{}w:\{Gamma,  phi  \mvdash{}  \_:(T  {}\mrightarrow{}  A)\}.
\mforall{}I:fset(\mBbbN{}).  \mforall{}a:Gamma(I).  \mforall{}u:glue-cube(Gamma;A;phi;T;w;I;a).
    (glue-morph(Gamma;A;phi;T;w;I;a;I;1;u)  =  u)


By

---

Latex:
(Auto
  THEN  (BLemma  `equal-glue-cube`  THENW  Auto)
  THEN  Unfold  `glue-cube`  -1
  THEN  Unfold  `glue-morph`  0
  THEN  (BoolCase  \mkleeneopen{}(phi(a)==1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index