---

Step * 1 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. 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)
BY
{ (Assert ⌜(phi(rho)==1) ~ tt⌝⋅ 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))
11. (phi(rho)==1) ~ tt
⊢ u = v ∈ T(rho) supposing u = v ∈ T(rho)

---

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.  u  :  if  (phi(rho)==1)
then  T(rho)
else  \{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)\} 
fi 
9.  v  :  if  (phi(rho)==1)
then  T(rho)
else  \{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)\} 
fi 
10.  phi(rho)  =  1
\mvdash{}  u  =  v  supposing  u  =  v


By

---

Latex:
(Assert  \mkleeneopen{}(phi(rho)==1)  \msim{}  tt\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index