Open maxsnew opened 1 year ago
It's probably worth doing this "manually" for the disjunction property proof:
But there is a more general method that would get us things like conservativity results:
But we want a variant that takes into account the type-object distinction in a CT structure (should be easy).
I think displayed categories give us a different, possibly simpler way to structure this.
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
.FreCCC(1,-) : FreeCCC -> Set
to get a BiCCC over FreeCCC and then construct a section.Marking this blocked as we need to implement https://github.com/maxsnew/multi-poly-cats/milestone/3 first
Show that the gluing category is biCCC