open import Cat.Functor.WideSubcategory
open import Cat.Functor.Properties
open import Cat.Restriction.Base
open import Cat.Prelude

import Cat.Restriction.Reasoning

module Cat.Restriction.Total where


# The Subcategory of Total Maps🔗

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

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

  Total-wide-subcat : Wide-subcat {C = 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 $\mathbf{Total}(\mathcal{C})$ into $\mathcal{C}$ is pseudomonic, as all isomorphisms in $\mathcal{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