---

Step * of Lemma glue-morph-comp

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[T:{Gamma, phi ⊢ _}]. ∀[w:{Gamma, phi ⊢ _:(T ⟶ A)}].
∀[I:fset(ℕ)]. ∀[rho:Gamma(I)]. ∀[J,K:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[g:K ⟶ J]. ∀[u:glue-cube(Gamma;A;phi;T;w;I;rho)].
  (glue-morph(Gamma;A;phi;T;w;J;f(rho);K;g;glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u))
  = glue-morph(Gamma;A;phi;T;w;I;rho;K;f ⋅ g;u)
  ∈ glue-cube(Gamma;A;phi;T;w;K;f ⋅ g(rho)))
BY
{ (Intros THEN (BLemma `equal-glue-cube` THENW Auto) THEN (BoolCase ⌜(phi(f ⋅ g(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. I : fset(ℕ)
7. rho : Gamma(I)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. u : glue-cube(Gamma;A;phi;T;w;I;rho)
13. phi(f ⋅ g(rho)) = 1 ∈ Point(face_lattice(K))
⊢ glue-morph(Gamma;A;phi;T;w;J;f(rho);K;g;glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u))
= glue-morph(Gamma;A;phi;T;w;I;rho;K;f ⋅ g;u)
∈ T(f ⋅ g(rho))

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. rho : Gamma(I)
8. J : fset(ℕ)
9. K : fset(ℕ)
10. f : J ⟶ I
11. g : K ⟶ J
12. ¬(phi(f ⋅ g(rho)) = 1 ∈ Point(face_lattice(K)))
13. u : glue-cube(Gamma;A;phi;T;w;I;rho)
⊢ glue-morph(Gamma;A;phi;T;w;J;f(rho);K;g;glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u))
= glue-morph(Gamma;A;phi;T;w;I;rho;K;f ⋅ g;u)
∈ (J1:fset(ℕ) ⟶ f1:{f1:J1 ⟶ K| phi(f1(f ⋅ g(rho))) = 1 ∈ Point(face_lattice(J1))}  ⟶ T(f1(f ⋅ g(rho)))
  × A(f ⋅ g(rho)))

---

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{}[rho:Gamma(I)].  \mforall{}[J,K:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].
\mforall{}[g:K  {}\mrightarrow{}  J].  \mforall{}[u:glue-cube(Gamma;A;phi;T;w;I;rho)].
    (glue-morph(Gamma;A;phi;T;w;J;f(rho);K;g;glue-morph(Gamma;A;phi;T;w;I;rho;J;f;u))
    =  glue-morph(Gamma;A;phi;T;w;I;rho;K;f  \mcdot{}  g;u))


By

---

Latex:
(Intros
  THEN  (BLemma  `equal-glue-cube`  THENW  Auto)
  THEN  (BoolCase  \mkleeneopen{}(phi(f  \mcdot{}  g(rho))==1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index