Fiber displayed category.

[anuyts]

No description provided.

[maxsnew]

This can be constructed compositionally using displayed total categories, reindexing and Displayed.Instances.Path. I've already made a similar definition for the fiber up to isomorphism downstream here: https://github.com/maxsnew/cubical-categorical-logic/blob/main/Cubical/Categories/Displayed/Constructions/IsoFiber/Base.agda#L44 . The compositional definition would be preferable because then we get more code reuse.

Also it seems like you're adding a lot of small things to the (displayed) categories library lately, which is great. I think we should have a chat e.g., on Agda zulip about your formalization plans so we can coördinate our efforts a bit better

[anuyts]

Ah yes, I see, using a displayed total category is cleaner indeed.

[jpoiret]

Should this PR be closed then?

[anuyts]

Suppose yes, I won't be coming back to it anytime soon.