---

Step * of Lemma equal-glue-cube

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}].
  ∀phi:{Gamma ⊢ _:𝔽}
    ∀[T:{Gamma, phi ⊢ _}]. ∀[w:{Gamma, phi ⊢ _:(T ⟶ A)}].
      ∀I:fset(ℕ). ∀rho:Gamma(I). ∀u,v:glue-cube(Gamma;A;phi;T;w;I;rho).
        u = v ∈ glue-cube(Gamma;A;phi;T;w;I;rho) 
        supposing if (phi(rho)==1)
        then u = v ∈ T(rho)
        else u = v ∈ (J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(rho))
        fi 
BY
{ (RepeatFor 9 (Intro) THEN All (Unfold `glue-cube`)⋅ THEN (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. I : fset(ℕ)
7. rho : Gamma(I)
8. u : if (phi(rho)==1)
then T(rho)
else {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(rho)| 
      let t,a = ta 
      in glue-equations(Gamma;A;phi;T;w;I;rho;t;a)} 
fi 
9. v : if (phi(rho)==1)
then T(rho)
else {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(rho)| 
      let t,a = ta 
      in glue-equations(Gamma;A;phi;T;w;I;rho;t;a)} 
fi 
10. phi(rho) = 1 ∈ Point(face_lattice(I))
⊢ u = v ∈ T(rho) supposing u = v ∈ T(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. ¬(phi(rho) = 1 ∈ Point(face_lattice(I)))
9. u : {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(rho)| 
        let t,a = ta 
        in glue-equations(Gamma;A;phi;T;w;I;rho;t;a)} 
10. v : {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(rho)| 
         let t,a = ta 
         in glue-equations(Gamma;A;phi;T;w;I;rho;t;a)} 
⊢ u
  = v
  ∈ {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(rho)| 
     let t,a = ta 
     in glue-equations(Gamma;A;phi;T;w;I;rho;t;a)}  
  supposing u = v ∈ (J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(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{}u,v:glue-cube(Gamma;A;phi;T;w;I;rho).
                u  =  v  supposing  if  (phi(rho)==1)  then  u  =  v  else  u  =  v  fi 


By

---

Latex:
(RepeatFor  9  (Intro)  THEN  All  (Unfold  `glue-cube`)\mcdot{}  THEN  (BoolCase  \mkleeneopen{}(phi(rho)==1)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index