P is a universal property if there is a presheaf F : C^op -> Sets such that
P(c) <-> F is representable by c, i.e. there is an isomorphism y(c) \cong F.
Actually, we require something stronger, that
P(c) \cong NatIso(y(c), F)
that is, we have a bijection (isomorphism of setoids) between P(c) and NatIso(y(c), F).
Class IsUniversalProperty (C : Category) (P : C → Type) (eqP : forall c, Setoid (P c)) :=
{
repr_functor : C ⟶ Sets ;
repr_equivalence : forall c : C,
@Isomorphism Sets
(Build_SetoidObject (P c) (eqP c))
(Build_SetoidObject (Isomorphism [Hom c,─] repr_functor) _)
}.
For example, if x and y are two objects in C, then the predicate P z := IsCartesianProduct x y z associates to z the set of pairs of maps (pi1 : z -> x , pi2 : z -> y) such that (z, pi1, pi2) has the universal mapping property of the Cartesian product.
P is a universal property, because a proof of P z corresponds to an isomorphism
Hom(-, z) \cong Hom(- , x) \times Hom(-,y).
We have these useful theorems about universal properties -
if z , z' are isomorphic by j : z \cong z', and P is a universal property, then P(z) -> P(z'), universal properties are isomorphism invariant.
If P is a universal property, then for any z, z', if P(z) and P(z') both hold, then z and z' are isomorphic by a unique isomorphism that respects the structure of P. For example, if z and z' are Cartesian products of x, y, then z and z' are isomorphic by an isomorphism commuting with the projection maps pi1 and pi2.
Warning - there is one "admit" command in here for a subproof. I have a working proof for Coq 8.16 but unfortunately it does not work for Coq 8.15 or 8.14 as it takes advantage of the fact that setoid rewriting in 8.16 supports universe polymorphism. I have not had time to install Coq + Program for a lower version number and try to write it without this.
Let C be a category, and P a predicate on obj(C).
P is a universal property if there is a presheaf F : C^op -> Sets such that P(c) <-> F is representable by c, i.e. there is an isomorphism y(c) \cong F.
Actually, we require something stronger, that P(c) \cong NatIso(y(c), F) that is, we have a bijection (isomorphism of setoids) between P(c) and NatIso(y(c), F).
For example, if x and y are two objects in C, then the predicate P z := IsCartesianProduct x y z associates to z the set of pairs of maps (pi1 : z -> x , pi2 : z -> y) such that (z, pi1, pi2) has the universal mapping property of the Cartesian product.
P is a universal property, because a proof of P z corresponds to an isomorphism Hom(-, z) \cong Hom(- , x) \times Hom(-,y).
We have these useful theorems about universal properties -
Warning - there is one "admit" command in here for a subproof. I have a working proof for Coq 8.16 but unfortunately it does not work for Coq 8.15 or 8.14 as it takes advantage of the fact that setoid rewriting in 8.16 supports universe polymorphism. I have not had time to install Coq + Program for a lower version number and try to write it without this.