---

Step * 2 of Lemma glue-morph-id


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))
BY
{ ((RepeatFor 2 (DVar `u') THEN Reduce 0) THEN (Subst' (phi(1(a))==1) ~ ff 0 THENA Auto) THEN Reduce 0) }

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. ¬(phi(a) = 1 ∈ Point(face_lattice(I)))
9. u1 : J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(a)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(a))
10. u2 : A(a)
11. let t,a@0 = <u1, u2> 
    in glue-equations(Gamma;A;phi;T;w;I;a;t;a@0)
⊢ <λK,g. (u1 K 1 ⋅ g), (u2 a 1)>
= <u1, u2>
∈ (J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(a)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(a)) × A(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.  a  :  Gamma(I)
8.  \mneg{}(phi(a)  =  1)
9.  u  :  \{ta:J:fset(\mBbbN{})  {}\mrightarrow{}  f:\{f:J  {}\mrightarrow{}  I|  phi(f(a))  =  1\}    {}\mrightarrow{}  T(f(a))  \mtimes{}  A(a)| 
                let  t,a@0  =  ta 
                in  glue-equations(Gamma;A;phi;T;w;I;a;t;a@0)\} 
\mvdash{}  let  t,a@0  =  u  in  if  (phi(1(a))==1)  then  t  I  1  else  <\mlambda{}K,g.  (t  K  1  \mcdot{}  g),  (a@0  a  1)>  fi    =  u


By

---

Latex:
((RepeatFor  2  (DVar  `u')  THEN  Reduce  0)
  THEN  (Subst'  (phi(1(a))==1)  \msim{}  ff  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index