---

Step * of Lemma cubical-type-equal3

No Annotations
∀[X:j⊢]. ∀[A,B:{X ⊢ _}].
  (A = B ∈ {X ⊢ _}) supposing 
     ((∀I:fset(ℕ). ∀[rho:X(I)]. ∀[J:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[u:A(rho)].  ((u rho f) = (u rho f) ∈ A(f(rho)))) and 
     (∀I:fset(ℕ). ∀[rho:X(I)]. (A(rho) = B(rho) ∈ Type)))
BY
{ PresheafMLTTInstance Obid: presheaf-type-equal3⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A,B:\{X  \mvdash{}  \_\}].
    (A  =  B)  supposing 
          ((\mforall{}I:fset(\mBbbN{})
                  \mforall{}[rho:X(I)].  \mforall{}[J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[u:A(rho)].    ((u  rho  f)  =  (u  rho  f)))  and 
          (\mforall{}I:fset(\mBbbN{}).  \mforall{}[rho:X(I)].  (A(rho)  =  B(rho))))


By

---

Latex:
PresheafMLTTInstance  Obid:  presheaf-type-equal3\mcdot{}

---

Home Index