Gluing for CCCs

[maxsnew]

Show that the gluing category is biCCC

[maxsnew]

It's probably worth doing this "manually" for the disjunction property proof:

1. If L is the lindenbaum algebra and Cl : L -> Set then the gluing construction is Comma Cl Id_Set.
2. Define the "types" to be ones where the L object is a type.
3. Easy to get general results about Comma F G being biCC when F G are biCC functors
4. Define the exponential manually

[maxsnew]

But there is a more general method that would get us things like conservativity results:

1. Define something like "proof-relevant first-order hyperdoctrines" as basically this but using biCCC rather than Heyting algebra.
2. Construct "base change" for such hyperdoctrines: if F : C -> D is a cartesian functor then any hyperdoctrine on D can be pulled back to a hyperdoctrine on C.
3. Define the Grothendieck construction/total category for such hyperdoctrines
4. Prove a result from Claudio Hermida's thesis (https://era.ed.ac.uk/bitstream/handle/1842/14057/Hermida1993.Pdf): if the base category of such a hyperdoctrine is bi-cartesian closed, then the total category is as well and the projection is a CCC functor.
5. Prove that the slices of any sheaf category form such a hyperdoctrine. This gives us the examples we need for conservativity results, which are all sheaf categories)

But we want a variant that takes into account the type-object distinction in a CT structure (should be easy).

[maxsnew]

I think displayed categories give us a different, possibly simpler way to structure this.

1. Define a "displayed BiCCC", i.e., a BiCCC over a BiCCC
2. Define a (proof relevant) "first-order hyperdoctrine" to be a displayed cat that is a fibration, interprets universal/existential quantifiers, equality and local sums/products is a displayed BiCCC.
3. Show that first-order hyperdoctrines are stable under base-change along product-preserving functors. I.e., if F : C -> D preserves finite products and H is a fo-hyperdoctrine over D then the reindexing F^*H is a fo-hyperdoctrine over C.
4. Show that any proof-relevant first-order hyperdoctrine is a displayed BiCCC.
5. Prove that the free BiCCC supports an eliminator: any displayed BiCCC over the free BiCCC has a section.
6. Show that the displayed cat of dependent sets over sets is a fo hyperdoctrine.
7. Pullback (6) along the global sections FreCCC(1,-) : FreeCCC -> Set to get a BiCCC over FreeCCC and then construct a section.

[maxsnew]

Marking this blocked as we need to implement https://github.com/maxsnew/multi-poly-cats/milestone/3 first

[maxsnew]

unblocked now that @hejohns has finished the cartesian category case (woo!). I think this is the plan:

Semantically:

1. Define lifted exponentials
2. Define fiberwise exponentials
3. Define the "Pi type" as a right adjoint to cartesian lift of a projection.
4. prove that fiberwise exponentials + Pi types are preserved under reindexing.
5. prove that fiberwise exponentials + Pi types imply lifted exponentials

Syntactically:

1. Define free cartesian closed category
2. Construct its eliminator into a displayed CCC

Gluing:

1. For canonicity: prove Set^D has fiberwise exponentials + Pi types glue with interpretation of base types as sets of canonical forms
2. For conservativity: same for Presheaf^D, similar to @hejohns previous proof.