---

Step * of Lemma glue-equations_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[phi:{Gamma ⊢ _:𝔽}]. ∀[T:{Gamma, phi ⊢ _}]. ∀[w:{Gamma, phi ⊢ _:(T ⟶ A)}].
∀[I:fset(ℕ)]. ∀[rho:Gamma(I)]. ∀[t:J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho))].
∀[a:A(rho)].
  (glue-equations(Gamma;A;phi;T;w;I;rho;t;a) ∈ ℙ)
BY
{ (RepeatFor 7 (Intro)
   THEN (Assert J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) ∈ Type BY
               Auto)
   THEN Intros
   THEN Unhide
   THEN Unfold `glue-equations` 0
   THEN MemCD) }

1
.....subterm..... T:t
1:n
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. J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) ∈ Type
9. t : J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho))
10. a : A(rho)
⊢ ∀J:fset(ℕ). ∀f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))} . ∀K:fset(ℕ). ∀g:K ⟶ J.
    ((t J f f(rho) g) = (t K f ⋅ g) ∈ T(f ⋅ g(rho))) ∈ ℙ

2
.....subterm..... T:t
2:n
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. J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho)) ∈ Type
9. t : J:fset(ℕ) ⟶ f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))}  ⟶ T(f(rho))
10. a : A(rho)
⊢ ∀J:fset(ℕ). ∀f:{f:J ⟶ I| phi(f(rho)) = 1 ∈ Point(face_lattice(J))} .
    ((w(f(rho)) J 1 (t J f)) = (a rho f) ∈ A(f(rho))) ∈ ℙ

---

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)\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[rho:Gamma(I)].  \mforall{}[t:J:fset(\mBbbN{})
                                                                                                                                      {}\mrightarrow{}  f:\{f:J  {}\mrightarrow{}  I|  phi(f(rho))  =  1\} 
                                                                                                                                      {}\mrightarrow{}  T(f(rho))].  \mforall{}[a:A(rho)].
    (glue-equations(Gamma;A;phi;T;w;I;rho;t;a)  \mmember{}  \mBbbP{})


By

---

Latex:
(RepeatFor  7  (Intro)
  THEN  (Assert  J:fset(\mBbbN{})  {}\mrightarrow{}  f:\{f:J  {}\mrightarrow{}  I|  phi(f(rho))  =  1\}    {}\mrightarrow{}  T(f(rho))  \mmember{}  Type  BY
                          Auto)
  THEN  Intros
  THEN  Unhide
  THEN  Unfold  `glue-equations`  0
  THEN  MemCD)

---

Home Index