Redundancy between Displayed.Constructions.PropertyOver and Category.Constructions.FullSubcategory

[maxsnew]

FullSubcategory is exactly the same as the total category of a PropertyOver. Would be sensible to me to refactor it so it's literally the case.

[anshwad10]

I think FullSubcategory should instead use embeddings, it's more general that way and it removes the redundance. Also embeddings are more universe polymorphic for now

[anshwad10]

imo this could also be a good first issue

[maxsnew]

ΣPropCat is also the same construction, but with the unnecessary assumption that the predicate is hProp-valued

[maxsnew]

@anshwad10 I don't really know what you mean about using embeddings, and I don't see how it would be more general.

[anshwad10]

I don't really know what you mean about using embeddings, and I don't see how it would be more general

So currently it looks like this:

module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP) where
  private
    module C = Category C
  open Category
  open Functor

  FullSubcategory : Category (ℓ-max ℓC ℓP) ℓC'
  ob FullSubcategory = Σ[ x ∈ C.ob ] P x
  Hom[_,_] FullSubcategory (x , p) (y , q) = C.Hom[ x , y ]

I am suggesting that we change it to this:

module _ (C : Category ℓC ℓC') (P : Type ℓP) (inc : P → Category.ob C) where
  private
    module C = Category C
  open Category
  open Functor

  FullSubcategory : Category ℓP ℓC'
  ob FullSubcategory = P
  Hom[_,_] FullSubcategory x y = C.Hom[ inc x , inc y ]

By being more general I mean that we can definitionally recover the previous behaviour by using FullSubcategory C (Σ C.ob P) fst instead of FullSubcategory C P. I can think of cases where this is useful, for example when we want the underlying type to be a custom record instead of a Σ-type
It is also more universe polymorphic since the universe level of the subcategory can be any ℓP instead of ℓ-max ℓC ℓP.
Also it doesn't need to be an embedding, inc can actually be any map at all (though it does need to be an embedding if we want univalence)

[maxsnew]

Ah I see what you mean. We've implemented that in cubical-categorical-logic but I didn't notice the connection https://github.com/um-catlab/cubical-categorical-logic/blob/main/Cubical/Categories/Constructions/ChangeOfObjects.agda .