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

Grothendieck forgetful functor #37

Closed stschaef closed 1 year ago

stschaef commented 1 year ago

Here is the forgetful functor from Grothendieck D to the category C, and a proof that this is faithful in the case that D is a displayed poset.

maxsnew commented 1 year ago

Code looks good. Some thoughts on naming.

I would call it some variation "first projection" rather than "forgetful" as I think of these Grothendieck constructions as a kind of Sigma type for categories. So just Fst is probably a fine name. You don't need to give things really long names since users can just import it qualified and call it Grothendieck.Fst or something.

maxsnew commented 1 year ago

Fix the naming and merge this?

stschaef commented 1 year ago

Sorry, this slipped my mind while distracted by subobjects/pullbacks

After wrestling with some merge conflicts, this is now mergeable.

This tests are failing, but not because of this code. Upstream cubical has deprecated Cubical.Foundations.Id, so Constructions.Free.Functor (and anything else that imports Id) needs to be refactored to fix the change with this import.

Because the tests aren't blocked on this piece of code, I will merge it and then open an issue for handling the change in cubical. sound reasonable?

maxsnew commented 1 year ago

Sounds good. I'm aware of the change in cubical. It should just be a minor change for us