---

Step * of Lemma cubical-fun-equal2

No Annotations
∀[X:j⊢]. ∀[A,B:{X ⊢ _}]. ∀[f:{X ⊢ _:(A ⟶ B)}].
∀[g:I:fset(ℕ) ⟶ a:X(I) ⟶ J:fset(ℕ) ⟶ h:J ⟶ I ⟶ u:A(h(a)) ⟶ B(h(a))].
  f = g ∈ {X ⊢ _:(A ⟶ B)} 
  supposing ∀[I:fset(ℕ)]. ∀[a:X(I)]. ∀[J:fset(ℕ)]. ∀[h:J ⟶ I]. ∀[u:A(h(a))].  ((f(a) J h u) = (g(a) J h u) ∈ B(h(a)))
BY
{ PresheafMLTTInstance Obid: presheaf-fun-equal2⋅ }

---

Latex:

---

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


By

---

Latex:
PresheafMLTTInstance  Obid:  presheaf-fun-equal2\mcdot{}

---

Home Index