Gluing for Free cat with terminal objects

[maxsnew]

I got started on implementing some metatheory for free categories with terminal objects. I got up to constructing the eliminator that constructs a local section but see we actually don't have the proof that VerticalTerminal is preserved by reindexing or that it implies LiftedTerminal. @hejohns please add those to this PR

[hejohns]

gah I guess I forgot to graft those over

[hejohns]

Not these?

cubical-categorical-logic/Cubical/Categories/Displayed/Fibration/Properties.agda

Line 86 in 6bb2d8a

Verticalᴰ/𝟙→LiftedTermᴰ : Verticalᴰ/𝟙 → LiftedTerminalᴰ Cᴰ term

cubical-categorical-logic/Cubical/Categories/Displayed/Fibration/Properties.agda

Line 109 in 6bb2d8a

reind-VerticalTerminalsᴰ : VerticalTerminalsᴰ (reindex Dᴰ F)

[maxsnew]

Well they don't have anything to do with fibrations so why would I look there

[hejohns]

I can move these, but I had them under Fibration/ for uniformity.
Or at least Vertical→Lifted in general should be under Fibration/.
I agree (not that you're necessarily saying this) that preservation under reindexing should get moved to Displayed/Limit/Terminal

[maxsnew]

No all of these constructions should be under Constructions.Reindex.Properties

…

On Wed, May 22, 2024, 4:52 PM Johnson He ***@***.***> wrote: I can move these, but I had them under Fibration/ for uniformity. Or at least Vertical→Lifted in general should be under Fibration/. I agree (not that you're necessarily saying this) that preservation under reindexing should get moved to Displayed/Limit/Terminal — Reply to this email directly, view it on GitHub <#95 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AALJIPKW6U2UVQH5DRMTKI3ZDUASXAVCNFSM6AAAAABIELXNA6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMRVG4ZDKMJXHE> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[maxsnew]

If they're already there I'll move them myself

…

On Wed, May 22, 2024, 4:56 PM Max New ***@***.***> wrote: No all of these constructions should be under Constructions.Reindex.Properties On Wed, May 22, 2024, 4:52 PM Johnson He ***@***.***> wrote: > I can move these, but I had them under Fibration/ for uniformity. > Or at least Vertical→Lifted in general should be under Fibration/. > I agree (not that you're necessarily saying this) that preservation under > reindexing should get moved to Displayed/Limit/Terminal > > — > Reply to this email directly, view it on GitHub > <#95 (comment)>, > or unsubscribe > <https://github.com/notifications/unsubscribe-auth/AALJIPKW6U2UVQH5DRMTKI3ZDUASXAVCNFSM6AAAAABIELXNA6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCMRVG4ZDKMJXHE> > . > You are receiving this because you authored the thread.Message ID: > ***@***.***> >

[hejohns]

Looks good to merge.
I think I follow how we want to do these gluing examples.

I don't get at the moment why the uniqueness of normal forms has a path issue while the uniqueness of canonical forms is just fine, but maybe I'll get some idea after doing canonical forms for free cartesian categories.

[maxsnew]

I don't get at the moment why the uniqueness of normal forms has a path issue while the uniqueness of canonical forms is just fine, but maybe I'll get some idea after doing canonical forms for free cartesian categories.

I think it's just cubical nonsense because the NFs are a more complicated data type than sums. It could be a bug in cubical Agda for all we know