---

Step * of Lemma presheaf-fun-as-presheaf-pi

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B:{X ⊢ _}].  ((X ⊢ A ⟶ B) = X ⊢ ΠA (B)p ∈ {X ⊢ _})
BY
{ (Intros THEN (BLemma `presheaf-type-equal2` THENA Auto)) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
⊢ (X ⊢ A ⟶ B)
= X ⊢ ΠA (B)p
∈ (A:I:cat-ob(C) ⟶ X(I) ⟶ Type × (I:cat-ob(C)
                                   ⟶ J:cat-ob(C)
                                   ⟶ f:(cat-arrow(C) J I)
                                   ⟶ a:X(I)
                                   ⟶ (A I a)
                                   ⟶ (A J f(a))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A,B:\{X  \mvdash{}  \_\}].    ((X  \mvdash{}  A  {}\mrightarrow{}  B)  =  X  \mvdash{}  \mPi{}A  (B)p)


By

---

Latex:
(Intros  THEN  (BLemma  `presheaf-type-equal2`  THENA  Auto))

---

Home Index