Post #2636105

@mc@mathstodon.xyz @JacquesC2@types.pl Universal Element of a presheaf is an element such that composition with it is an equivalence: https://github.com/agda/cubical/blob/7a4fbe151cc7185b5b782f8257976753317ed176/Cubical/Categories/Presheaf/Representable.agda#L84 PshHom is a natural transformation of presheaves (defined in a way that is universe polymorphic: https://github.com/um-catlab/cubical-categorical-logic/blob/3a1f2fea115ac6a6c1ec7640681ddf2ddfccad96/Cubical/Categories/Presheaf/Morphism/Alt.agda#L87). PshIso is a PshHom that is pointwise an isomorphism (https://github.com/um-catlab/cubical-categorical-logic/blob/3a1f2fea115ac6a6c1ec7640681ddf2ddfccad96/Cubical/Categories/Presheaf/Morphism/Alt.agda#L275). Note that isomorphism and equivalence are equivalent. The Yoneda lemma says that an element P x can be uniquely extended to a PshHom (C [-, x]) P that sends the identity to the specified element. We call this operation "yoRec". Then UniversalElement is just saying that the resulting PshHom you get from the element is a PshIso. This equivalence is proven here: https://github.com/um-catlab/cubical-categorical-logic/blob/3a1f2fea115ac6a6c1ec7640681ddf2ddfccad96/Cubical/Categories/Presheaf/Representable/More.agda#L156