New definitions of displayed and vertical universal elements

[maxsnew]

This is a big refactor of the displayed universal property stuff we have so far:

1. Redefines displayed right adjoint so we don't need RightAdjoint' anymore.
2. Defines the fiber category over an object, and vertical composition between morphisms in the fiber and displayed morphisms.
3. Defines displayed universalElement using IsoOver, which corresponds more directly to the natural thing in eliminators for free categories
4. Give a separate definition of vertical universal elements which uses Iso and vertical composition
5. Changed to a simpler definition of cartesianLift

The code is still a bit of a mess and I think we should do some name changing, but wanted to push so @hejohns and I can discuss

[maxsnew]

@hejohns this is ready

[hejohns]

The new definitions look good. Haven't tried using them yet.
Just had a question in the comments on this PR about why some seemingly automatically generated normalized proof terms are there, when they don't seem necessary.

[hejohns]

note to self: this is to preserve the definitional behavior/ensure the expected definitional behavior of functor composition? Since vertical functor composition involves reindexing.

[maxsnew]

I'm not sure which thing you are asking about:

1. We want this definition funcCompⱽ just because it is useful, e.g., composing with the projection functor for reindexing we usually need to get rid of the composition with the identity functor in the base.
2. reindF' just has better definitional behavior than reindF when the proofs are Eq.refl since reindF does a reindex/transport. reindF' _ Eq.refl Eq.refl is instead like getting the displayed functor to type check by eta expansion but less tedious.

[hejohns]

I was wondering more of the second. As in, which reindex exactly does this do away with. I'll play around with it later.

[hejohns]

Why are these (normalized) implicit arguments here? The file type checks without them, and the supplied {A = ...} type doesn't appear in the opaque type anyways, right?

I ran into something maybe similar where I wanted to make a displayed path opaque, but because the base path the displayed path is over shows up in the type, the two options I had were to 1) fill in the base path with a giant normalized C-c C-s term 2) rectify to be over something nice. I chose 2), but without opaque, usually we just leave the base path as _, and rectify at use sites

[hejohns]

And make succeeds after deleting {A = ...}

[maxsnew]

I think as I was writing the proof, I put them in because othwerise the goal disappears after fromPathP ?. Didn't think to remove them afterwards.

I don't really understand what you are suggesting with 2. If you have a simpler/less manual proof for this and the one for Sets I would love to see it.

[hejohns]

2. wasn't a suggestion. It just looked to me like you had inserted a C-c C-s proof, and thinking about why you might've needed to do that, it reminded me of the situation where I had a displayed path lemma : fᴰ Cᴰ.≡[ _ ] gᴰ and I wanted to just leave the _ and rectify at the use-sites. But because the lemma was opaque, I had to fill in the _ and C-c C-s gave me some horrible 700 line mess. (I might've had to C-u C-u C-c C-s because the C-c C-s'd term further had opaque paths that would've made the lemma unusable without unfolding.) So it took extra work to manually write a nice base proof to rectify the lemma to be over, just so the type of the lemma wasn't massive.

I just didn't think you had written the transp and interval algebra expressions manually, and was wondering how that proof term got generated.