Construct the Presheaf of Subobjects

[maxsnew]

The main source of semantic hyperdoctrines comes from constructing the presheaf of subobjects. Terse nlab reference: https://ncatlab.org/nlab/show/poset+of+subobjects

For any category C and object c : C .ob you can define

1. A preorder of subobjects of c Σ [ B ∈ C ] Σ [ f ∈ C [ B , A ] ] isMono f). If C is univalent this should already be a poset but otherwise you'll need to quotient it.
2. If C has pullbacks of monos, then you can define a presheaf on C of subobjects where the action on morphisms is given by pullback. (Useful lemma: monos are preserved under pullback).
3. Further, the poset will always have finite meets, and if you have a terminal object I think you can construct an equality predicate as well.
4. This defines a poset internal to presheaves, and the meets and equality are internal as well.

There is already a decent amount about pullbacks in the library. We should probably port some of that to use representability instead.

There is a whole zoo of what conditions you need on C to get each connective we would want in the hyperdoctrine. We can discuss how to tackle that later.

[maxsnew]

A lot of details are given in this note: https://www.brics.dk/LS/98/2/BRICS-LS-98-2.pdf

[GenericMonkey]

One issue I'm running up against here is that C .ob isn't a set. I was able to prove all the other criterion for a preorder, but showing that the monic funcs defined as the nested sigma type isSet is proving to be tricky.

[maxsnew]

You need to quotient it to get it to be a set

[GenericMonkey]

I think I might be missing something here. The way I thought about approaching this was:

1. First make Mono(X) , i.e. the preorder of monomorphisms into an Preorder. (No isomorphism classes). This currently fails because the isSet criterion of defining a Preorder cannot be satisfied for an arbitrary category.
2. Posetify this using the isomorphism classes to make Sub(X).

My interpretation of what you mean by "quotienting" is going from step 1 -> 2, where hopefully we can make Sub(X) into a proper Poset even if Mono(X) isn't a Preorder (as it fails the isSet condition).

However, looking at the BRICS resource, it seems like even after this quotienting, we aren't guaranteed a set unless we have that C is "well-powered".

Definition 2.1 We say that C is well-powered if Sub(X) is a set for all objects X of C.

Am I missing some assumption I should be making on the base category? Maybe univalence gives you well-powered?

[maxsnew]

I guess we should drop the isSet condition on the objects of a preorder, after all there's no corresponding isGpd condition for categories. Then it should go through no problem.

The "well-powered" thing is irrelevant, it's not the same meaning of "set". There they mean "set vs class" i.e., small vs large. We are just handling all of that with the difference universe levels.

[GenericMonkey]

Ok, that makes sense. This means that we should redefine the PREORDER category to have Σ[ P ∈ Preorder ] isSet (P .fst) as the objects yeah? and trickle up any changes to higher constructions? My understanding is that the category of Preorders only contains "small preorders?"

Also, I'm guessing we should fork off Cubicals definition of Poset to build off of our defnition of Preorder instead of being defined in Binary.Relation.Poset, and that we should lose the isSet condition on the new Poset as well?

[maxsnew]

that's right about the preorder category. monotone functions are only a set if the preorders have a set of elements.

It's hard to map small large terminology directly to universe levels. Don't worry about that.

You can drop isSet from Poset but for a different reason: you can show it's a set from anti-symmetry, just like you can show the objects of a univalent category are a groupoid.

[maxsnew]

This is not needed anymore now that we're switching to displayed cats for this kind of stuff. I already implemented a displayed preorder of subobjects in https://github.com/maxsnew/multi-poly-cats/pull/42