search

maxsnew / cubical-categorical-logic

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

Coend #78

Open bond15 opened 6 months ago

bond15 commented 6 months ago

Should the Set-Coend go in a separate "Instances" file?

bond15 commented 3 months ago

@maxsnew So should I scrap this and use a similar construction to your definition of Ends ?

maxsnew commented 3 months ago

Typically we would have two versions: one concrete like yours which is easy to read and understand and one compositional like mine where it's easier to get common properties. Then we would define a function that goes from the concrete to the compositional one.

bond15 commented 3 months ago

Typically we would have two versions: one concrete like yours which is easy to read and understand and one compositional like mine where it's easier to get common properties. Then we would define a function that goes from the concrete to the compositional one.

I can attempt this once both branches are merged in.