Grothendieck forgetful functor

[stschaef]

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]

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]

I think the naming convention is to call this isFaithfulFst

[maxsnew]

Fix the naming and merge this?

[stschaef]

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]

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