---

Step * 2 of Lemma equal-glue-cube


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))
BY
{ (D 0 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. ¬(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)} 
11. u = v ∈ (J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) × A(rho))
⊢ 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)} 

---

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.  I  :  fset(\mBbbN{})
7.  rho  :  Gamma(I)
8.  \mneg{}(phi(rho)  =  1)
9.  u  :  \{ta:J:fset(\mBbbN{})  {}\mrightarrow{}  f:\{f:J  {}\mrightarrow{}  I|  phi(f(rho))  =  1\}    {}\mrightarrow{}  T(f(rho))  \mtimes{}  A(rho)| 
                let  t,a  =  ta 
                in  glue-equations(Gamma;A;phi;T;w;I;rho;t;a)\} 
10.  v  :  \{ta:J:fset(\mBbbN{})  {}\mrightarrow{}  f:\{f:J  {}\mrightarrow{}  I|  phi(f(rho))  =  1\}    {}\mrightarrow{}  T(f(rho))  \mtimes{}  A(rho)| 
                  let  t,a  =  ta 
                  in  glue-equations(Gamma;A;phi;T;w;I;rho;t;a)\} 
\mvdash{}  u  =  v  supposing  u  =  v


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index