{-# OPTIONS --without-K --safe #-}
module Categories.Category.Restriction.Properties where
open import Data.Product using (Ξ£; _,_)
open import Level using (Level; _β_)
open import Categories.Category.Core using (Category)
open import Categories.Category.Restriction using (Restriction)
open import Categories.Category.SubCategory
open import Categories.Morphism using (Mono)
open import Categories.Morphism.Idempotent using (Idempotent)
open import Categories.Morphism.Properties using (Mono-id)
import Categories.Morphism.Reasoning as MR
module _ {o β e : Level} {π : Category o β e} (R : Restriction π) where
open Category π
open Restriction R
open HomReasoning
open MR π using (elimΛ‘; introΚ³)
private
variable
A B C : Obj
f : A β B
g : B β C
βf-idempotent : (A β B) β Idempotent π A
βf-idempotent f = record { idem = f β ; idempotent = βΊ β-denestΚ³ β β-cong pidΚ³ }
β-pidΛ‘-gf : f β β (g β f) β β (g β f) β
β-pidΛ‘-gf {f = f} {g = g} = begin
f β β (g β f) β ββ¨ β-comm β©
(g β f) β β f β βΛβ¨ β-denestΚ³ β©
((g β f) β f β) β ββ¨ β-cong assoc β©
(g β (f β f β)) β ββ¨ β-cong (β-resp-βΚ³ pidΚ³) β©
(g β f) β β
β-denestΛ‘ : (g β β f) β β (g β f) β
β-denestΛ‘ {g = g} {f = f} = begin
(g β β f) β ββ¨ β-cong β-skew-comm β©
(f β (g β f) β) β ββ¨ β-denestΚ³ β©
f β β (g β f) β ββ¨ β-pidΛ‘-gf β©
(g β f) β β
β-idempotent : f β β β f β
β-idempotent {f = f} = begin
f β β βΛβ¨ β-cong identityΚ³ β©
(f β β id) β ββ¨ β-denestΛ‘ β©
(f β id) β ββ¨ β-cong identityΚ³ β©
f β β
ββdenest : (g β β f β) β β g β β f β
ββdenest {g = g} {f = f} = begin
(g β β f β) β ββ¨ β-denestΚ³ β©
g β β β f β ββ¨ (β-idempotent β©ββ¨refl) β©
g β β f β β
Monoβfββid : Mono π f β f β β id
Monoβfββid {f = f} mono = mono (f β) id (pidΚ³ β βΊ identityΚ³)
ββββ : f β g β β f β f β β f β β g β
ββββ {f = f} {g = g} fgββf = βΊ (β-cong fgββf) β β-denestΚ³
MonoβTotal : Mono π f β total f
MonoβTotal = Monoβfββid
β-pres-total : {A B C : Obj} {f : B β C} {g : A β B} β total f β total g β total (f β g)
β-pres-total {f = f} {g = g} tf tg = begin
(f β g) β βΛβ¨ β-denestΛ‘ β©
(f β β g) β ββ¨ β-cong (elimΛ‘ tf) β©
g β ββ¨ tg β©
id β
total-gfβtotal-f : total (g β f) β total f
total-gfβtotal-f {g = g} {f = f} tgf = begin
f β ββ¨ introΚ³ tgf β©
f β β (g β f) β ββ¨ β-pidΛ‘-gf β©
(g β f) β ββ¨ tgf β©
id β
total-SubCat : SubCat π Obj
total-SubCat = record
{ U = Ξ» x β x
; R = total
; Rid = MonoβTotal (Mono-id π)
; _βR_ = β-pres-total
}
Total : Category o (β β e) e
Total = SubCategory π total-SubCat