Library HoTT.categories.SetCategory.Core

PreCategories set_cat and prop_cat

Require Import Category.Core Category.Strict.
Require Import HoTT.Basics.Trunc HProp HSet Types.Universe UnivalenceImpliesFunext TruncType.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Notation cat_of obj :=
  (@Build_PreCategory obj
                      (fun x yx y)
                      (fun _ xx)
                      (fun _ _ _ f gf o g)%core
                      (fun _ _ _ _ _ _ _idpath)
                      (fun _ _ _idpath)
                      (fun _ _ _idpath)

There is a category Set, where the objects are sets and the morphisms are set morphisms

Definition prop_cat `{Funext} : PreCategory := cat_of hProp.
Definition set_cat `{Funext} : PreCategory := cat_of hSet.

Prop is a strict category

Global Instance isstrict_prop_cat `{Univalence}
: IsStrictCategory prop_cat
  := _.

Because, e.g., @identity set_cat x x, and we want rewrite to notice this, we must inform it that it can try treating identity as idmap.
Declare Equivalent Keys identity idmap.