module Cat.Restriction.Total where

# The subcategory of total mapsπ

Let $C$ be a restriction category. We can construct a wide subcategory of $C$ containing only the total maps of $C,$ denoted $Total(C).$

module _ {o β} {C : Precategory o β} (Cβ : Restriction-category C) where open Cat.Restriction.Reasoning Cβ

Total-wide-subcat : Wide-subcat C β Total-wide-subcat .Wide-subcat.P = is-total Total-wide-subcat .Wide-subcat.P-prop = is-total-is-prop Total-wide-subcat .Wide-subcat.P-id = id-total Total-wide-subcat .Wide-subcat.P-β = total-β Total-maps : Precategory o β Total-maps = Wide Total-wide-subcat

module _ {o β} {C : Precategory o β} {Cβ : Restriction-category C} where open Cat.Restriction.Reasoning Cβ

Furthermore, the injection from $Total(C)$ into $C$ is pseudomonic, as all isomorphisms in $C$ are total.

Forget-total : Functor (Total-maps Cβ) C Forget-total = Forget-wide-subcat Forget-total-pseudomonic : is-pseudomonic Forget-total Forget-total-pseudomonic = is-pseudomonic-Forget-wide-subcat invertibleβtotal