search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
367 stars 68 forks source link

properties of presheaves #148

Open HuStmpHrrr opened 4 years ago

HuStmpHrrr commented 4 years ago

implement a number of properties of presheaves category.

presheaves are cartesian categories. if the underlying category is cartesian, presheaves are CCC.

HuStmpHrrr commented 4 years ago

missing subobject classifier then we can show presheaves are topoi. finite completeness need a bit from #129