search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
21 stars 5 forks source link

Wide Subcategories #54

Open maxsnew opened 4 months ago

maxsnew commented 4 months ago

We defined full subcategories as displayed categories in the new PR, it would be nice to have the opposite extreme, a "wide" subcategory as well.

maxsnew commented 1 month ago

Naming update: FullSubcategory has been merged upstream and is now called PropertyOver. I guess that means WideSubcategory should be like HomPropertyOver or something

stschaef commented 1 month ago

See #100