{-# OPTIONS --without-K --safe #-} open import Categories.Bicategory module Categories.Bicategory.LocalCoequalizers {o ℓ e t} (𝒞 : Bicategory o ℓ e t) where open import Categories.Diagram.Coequalizer using (Coequalizer; Coequalizers) open import Level using (_⊔_) open import Categories.Functor.Properties using (PreservesCoequalizers) import Categories.Bicategory.Extras as Bicat open Bicat 𝒞 record LocalCoequalizers : Set (o ⊔ ℓ ⊔ e ⊔ t) where field localCoequalizers : (A B : Obj) → Coequalizers (hom A B) precompPreservesCoequalizer : {A B E : Obj} → (f : E ⇒₁ A) → PreservesCoequalizers (-⊚_ {E} {A} {B} f) postcompPreservesCoequalizer : {A B E : Obj} → (f : B ⇒₁ E) → PreservesCoequalizers (_⊚- {B} {E} {A} f) open LocalCoequalizers module _ (localcoeq : LocalCoequalizers) {A B E : Obj} {X Y : A ⇒₁ B} {α β : X ⇒₂ Y} where _coeq-◁_ : (coeq : Coequalizer (hom A B) α β) (f : E ⇒₁ A) → Coequalizer (hom E B) (α ◁ f) (β ◁ f) coeq coeq-◁ f = record { obj = obj ∘₁ f ; arr = arr ◁ f ; isCoequalizer = precompPreservesCoequalizer localcoeq f {coeq = coeq} } where open Coequalizer coeq _▷-coeq_ : (f : B ⇒₁ E) (coeq : Coequalizer (hom A B) α β) → Coequalizer (hom A E) (f ▷ α) (f ▷ β) f ▷-coeq coeq = record { obj = f ∘₁ obj ; arr = f ▷ arr ; isCoequalizer = postcompPreservesCoequalizer localcoeq f {coeq = coeq} } where open Coequalizer coeq