---

Step * of Lemma glue-type-constraint

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[T:{Gamma, phi ⊢ _}]. ∀[w:{Gamma, phi ⊢ _:(T ⟶ A)}].
  Gamma, phi ⊢ Glue [phi ⊢→ (T;w)] A = T
BY
{ (Auto
   THEN Unfold `same-cubical-type` 0
   THEN BLemma `cubical-type-equal2`
   THEN Try (Complete (Auto))
   THEN ((Assert Gamma, phi ⊢ T BY Trivial) THEN RepeatFor 2 (D 4))
   THEN All Reduce
   THEN Unfold `glue-type` 0
   THEN (EqCD THENA Auto)
   THEN RepeatForAtMost "xx" 5 (((FunExt THENA Auto) THEN Reduce 0))⋅
   THEN Unfolds ``glue-morph glue-cube`` 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. x : Gamma, phi(I)
⊢ if (phi(x)==1)
then <A1, T1>(x)
else {ta:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(x)) = 1 ∈ Point(face_lattice(J))}  ⟶ <A1, T1>(f(x)) × A(x)| 
      let t,a = ta 
      in glue-equations(Gamma;A;phi;<A1, T1>;w;I;x;t;a)} 
fi 
= (A1 I x)
∈ Type

2
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, phi(I)
13. x : glue-cube(Gamma;A;phi;<A1, T1>;w;I;a)
⊢ if (phi(a)==1) 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 \000C fi 
= (T1 I J f a x)
∈ if (phi(f(a))==1)
  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 

---

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)\}].
    Gamma,  phi  \mvdash{}  Glue  [phi  \mvdash{}\mrightarrow{}  (T;w)]  A  =  T


By

---

Latex:
(Auto
  THEN  Unfold  `same-cubical-type`  0
  THEN  BLemma  `cubical-type-equal2`
  THEN  Try  (Complete  (Auto))
  THEN  ((Assert  Gamma,  phi  \mvdash{}  T  BY  Trivial)  THEN  RepeatFor  2  (D  4))
  THEN  All  Reduce
  THEN  Unfold  `glue-type`  0
  THEN  (EqCD  THENA  Auto)
  THEN  RepeatForAtMost  "xx"  5  (((FunExt  THENA  Auto)  THEN  Reduce  0))\mcdot{}
  THEN  Unfolds  ``glue-morph  glue-cube``  0)

---

Home Index