---

Step * 2 1 of Lemma glue-type-constraint


1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. A1 : I:fset(ℕ) ⟶ Gamma, phi(I) ⟶ Type
5. T1 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma, phi(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
6. (∀I:fset(ℕ). ∀a:Gamma, phi(I). ∀u:A1 I a.  ((T1 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma, phi(I). ∀u:A1 I a.
     ((T1 I K f ⋅ g a u) = (T1 J K g f(a) (T1 I J f a u)) ∈ (A1 K f ⋅ g(a))))
7. w : {Gamma, phi ⊢ _:(<A1, T1> ⟶ A)}
8. Gamma, phi ⊢ <A1, T1>
9. I : fset(ℕ)
10. J : fset(ℕ)
11. f : J ⟶ I
12. a : Gamma(I)
13. phi(a) = 1 ∈ Point(face_lattice(I))
14. x : glue-cube(Gamma;A;phi;<A1, T1>;w;I;a)
⊢ if tt then (x a f) else let t,a@0 = x in if (phi(f(a))==1) then t J f else <λK,g. (t K f ⋅ g), (a@0 a f)> fi  fi 
= (T1 I J f a x)
∈ if tt
  then <A1, T1>(f(a))
  else {ta:J@0:fset(ℕ) ⟶ f@0:{f@0:J@0 ⟶ J| phi(f@0(f(a))) = 1 ∈ Point(face_lattice(J@0))}  ⟶ <A1, T1>(f@0(f(a)))
        × A(f(a))| 
        let t,a@0 = ta 
        in glue-equations(Gamma;A;phi;<A1, T1>;w;J;f(a);t;a@0)} 
  fi 
BY
{ (Reduce 0 THEN Fold `member` 0) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. phi : {Gamma ⊢ _:𝔽}
4. A1 : I:fset(ℕ) ⟶ Gamma, phi(I) ⟶ Type
5. T1 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:Gamma, phi(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
6. (∀I:fset(ℕ). ∀a:Gamma, phi(I). ∀u:A1 I a.  ((T1 I I 1 a u) = u ∈ (A1 I a)))
∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:Gamma, phi(I). ∀u:A1 I a.
     ((T1 I K f ⋅ g a u) = (T1 J K g f(a) (T1 I J f a u)) ∈ (A1 K f ⋅ g(a))))
7. w : {Gamma, phi ⊢ _:(<A1, T1> ⟶ A)}
8. Gamma, phi ⊢ <A1, T1>
9. I : fset(ℕ)
10. J : fset(ℕ)
11. f : J ⟶ I
12. a : Gamma(I)
13. phi(a) = 1 ∈ Point(face_lattice(I))
14. x : glue-cube(Gamma;A;phi;<A1, T1>;w;I;a)
⊢ T1 I J f a x ∈ A1 J f(a)

---

Latex:

---

Latex:

1.  Gamma  :  CubicalSet\{j\}
2.  A  :  \{Gamma  \mvdash{}  \_\}
3.  phi  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
4.  A1  :  I:fset(\mBbbN{})  {}\mrightarrow{}  Gamma,  phi(I)  {}\mrightarrow{}  Type
5.  T1  :  I:fset(\mBbbN{})  {}\mrightarrow{}  J:fset(\mBbbN{})  {}\mrightarrow{}  f:J  {}\mrightarrow{}  I  {}\mrightarrow{}  a:Gamma,  phi(I)  {}\mrightarrow{}  (A1  I  a)  {}\mrightarrow{}  (A1  J  f(a))
6.  (\mforall{}I:fset(\mBbbN{}).  \mforall{}a:Gamma,  phi(I).  \mforall{}u:A1  I  a.    ((T1  I  I  1  a  u)  =  u))
\mwedge{}  (\mforall{}I,J,K:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}g:K  {}\mrightarrow{}  J.  \mforall{}a:Gamma,  phi(I).  \mforall{}u:A1  I  a.
          ((T1  I  K  f  \mcdot{}  g  a  u)  =  (T1  J  K  g  f(a)  (T1  I  J  f  a  u))))
7.  w  :  \{Gamma,  phi  \mvdash{}  \_:(<A1,  T1>  {}\mrightarrow{}  A)\}
8.  Gamma,  phi  \mvdash{}  <A1,  T1>
9.  I  :  fset(\mBbbN{})
10.  J  :  fset(\mBbbN{})
11.  f  :  J  {}\mrightarrow{}  I
12.  a  :  Gamma(I)
13.  phi(a)  =  1
14.  x  :  glue-cube(Gamma;A;phi;<A1,  T1>w;I;a)
\mvdash{}  if  tt
then  (x  a  f)
else  let  t,a@0  =  x 
          in  if  (phi(f(a))==1)  then  t  J  f  else  <\mlambda{}K,g.  (t  K  f  \mcdot{}  g),  (a@0  a  f)>  fi 
fi 
=  (T1  I  J  f  a  x)


By

---

Latex:
(Reduce  0  THEN  Fold  `member`  0)

---

Home Index