Category and Cartesian instances for polymorphic predicates

[AJChapman]

This is a new category in which the objects are predicates (wrapped in a PRED record implicitly containing the underlying type and the predicate) and the morphisms map between these objects. This differs from the Preds instance in Categories.Category.Instance.Preds in that the morphisms can change the underlying type as well as the predicate. I'm tentatively referring to this as 'polymorphic' to distinguish it from the existing instance.

I'm not certain that this fits into this library, and if it does then maybe I need to break it apart into separate files for PRED, Preds and PredsCartesian? I'd be happy to adapt it if you're interested, or just to get feedback on any of it as I'm fairly new to Agda and dependent types.

[JacquesCarette]

Note that I'm away at a conference right now, so won't be able to review in detail for another few days.

Because PRED is essentially isomorphic to 'containers' which is also known as 'polynomial functors', we definitely want this. Though doing it atop 'containers' is likely the way to go.

[TOTBWF]

A better name for this would be Fam(Set); it is precisely the total category of the family fibration on the category of sets.

Containers/Poly would have the maps going "backwards", EG:

record _⇒_ (A B : PRED) : Set o where
  constructor mk⇒
  open PRED
  field
    {f} : U A → U B
    imp : ∀ {u} → P B (f u) → P A u

[TOTBWF]

It might be worth doing Fam in it's generality though; this would give you Fam(Set), Fam(Setoids), and Fam(Setoids^op) all in one go.

[JacquesCarette]

Thanks for catching that I missed the orientation reversal. And yes, it probably is worth doing Fam instead. Do you know what that means @AJChapman ?

[AJChapman]

I don't yet know what it means. My category theory knowledge is quite limited. I'll read up on what a 'family fibration' is at the 1lab link @TOTBWF gave. I see that 1lab already has this implemented, so I can use their code as a guide.