---

Step * of Lemma presheaf-fun-equal2

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}]. ∀[f:{X ⊢ _:(A ⟶ B)}]. ∀[g:I:cat-ob(C)
                                                                                        ⟶ a:X(I)
                                                                                        ⟶ J:cat-ob(C)
                                                                                        ⟶ h:(cat-arrow(C) J I)
                                                                                        ⟶ u:A(h(a))
                                                                                        ⟶ B(h(a))].
  f = g ∈ {X ⊢ _:(A ⟶ B)} 
  supposing ∀[I:cat-ob(C)]. ∀[a:X(I)]. ∀[J:cat-ob(C)]. ∀[h:cat-arrow(C) J I]. ∀[u:A(h(a))].
              ((f(a) J h u) = (g(a) J h u) ∈ B(h(a)))
BY
{ Intros }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
5. f : {X ⊢ _:(A ⟶ B)}
6. g : I:cat-ob(C) ⟶ a:X(I) ⟶ J:cat-ob(C) ⟶ h:(cat-arrow(C) J I) ⟶ u:A(h(a)) ⟶ B(h(a))
7. ∀[I:cat-ob(C)]. ∀[a:X(I)]. ∀[J:cat-ob(C)]. ∀[h:cat-arrow(C) J I]. ∀[u:A(h(a))].
     ((f(a) J h u) = (g(a) J h u) ∈ B(h(a)))
⊢ f = g ∈ {X ⊢ _:(A ⟶ B)}

2
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
5. f : {X ⊢ _:(A ⟶ B)}
6. g : I:cat-ob(C) ⟶ a:X(I) ⟶ J:cat-ob(C) ⟶ h:(cat-arrow(C) J I) ⟶ u:A(h(a)) ⟶ B(h(a))
⊢ istype(∀[I:cat-ob(C)]. ∀[a:X(I)]. ∀[J:cat-ob(C)]. ∀[h:cat-arrow(C) J I]. ∀[u:A(h(a))].
           ((f(a) J h u) = (g(a) J h u) ∈ B(h(a))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A,B:\{X  \mvdash{}  \_\}].  \mforall{}[f:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\}].
\mforall{}[g:I:cat-ob(C)  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  J:cat-ob(C)  {}\mrightarrow{}  h:(cat-arrow(C)  J  I)  {}\mrightarrow{}  u:A(h(a))  {}\mrightarrow{}  B(h(a))].
    f  =  g 
    supposing  \mforall{}[I:cat-ob(C)].  \mforall{}[a:X(I)].  \mforall{}[J:cat-ob(C)].  \mforall{}[h:cat-arrow(C)  J  I].  \mforall{}[u:A(h(a))].
                            ((f(a)  J  h  u)  =  (g(a)  J  h  u))


By

---

Latex:
Intros

---

Home Index