Use Preorder and Preorder^D Less

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory

MIT License

25 stars 5 forks source link

Use Preorder and Preorder^D Less #52

Closed maxsnew closed 8 months ago

maxsnew commented 9 months ago

On https://github.com/maxsnew/multi-poly-cats/pull/51 I've added definitions hasPropHoms and hasContrHoms. It seems more in the spirit of the way the cubical library is structured to use these definitions rather than using Preorder^D. We should probably only use Preorder^D as an interface to define a Category^D that hasPropHoms.

maxsnew commented 8 months ago

This is being handled by @stschaef in the PR