module Cat.Restriction.Total where

The subcategory of total mapsπŸ”—

Let be a restriction category. We can construct a wide subcategory of containing only the total maps of denoted

  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

Furthermore, the injection from into is pseudomonic, as all isomorphisms in 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