diff options
| -rw-r--r-- | Coeq.agda | 79 | ||||
| -rw-r--r-- | Util.agda | 1 |
2 files changed, 80 insertions, 0 deletions
diff --git a/Coeq.agda b/Coeq.agda new file mode 100644 index 0000000..ad21587 --- /dev/null +++ b/Coeq.agda @@ -0,0 +1,79 @@ +{-# OPTIONS --without-K --safe #-} +module Coeq where + +open import Categories.Category.Core using (Category) +open import Categories.Category.Instance.Nat using (Nat) +open import Categories.Diagram.Coequalizer Nat using (IsCoequalizer) +open import Categories.Object.Coproduct Nat using (Coproduct; IsCoproduct; IsCoproduct⇒Coproduct) + + +open Category Nat + +-- TODO: any category +≈-i₁-i₂ + : {A B A+B C : Obj} + → {i₁ : A ⇒ A+B} + → {i₂ : B ⇒ A+B} + → (f g : A+B ⇒ C) + → IsCoproduct i₁ i₂ + → f ∘ i₁ ≈ g ∘ i₁ + → f ∘ i₂ ≈ g ∘ i₂ + → f ≈ g +≈-i₁-i₂ f g coprod ≈₁ ≈₂ = begin + f ≈⟨ Equiv.sym g-η ⟩ + [ f ∘ i₁ , f ∘ i₂ ] ≈⟨ []-cong₂ ≈₁ ≈₂ ⟩ + [ g ∘ i₁ , g ∘ i₂ ] ≈⟨ g-η ⟩ + g ∎ + where + open Coproduct (IsCoproduct⇒Coproduct coprod) + open HomReasoning + +iterated-coequalizer + : {A B A+B C Q₁ Q₂ : Obj} + → (i₁ : A ⇒ A+B) + → (i₂ : B ⇒ A+B) + → (f g : A+B ⇒ C) + → (q₁ : C ⇒ Q₁) + → (q₂ : Q₁ ⇒ Q₂) + → IsCoproduct i₁ i₂ + → IsCoequalizer (f ∘ i₁) (g ∘ i₁) q₁ + → IsCoequalizer (q₁ ∘ f ∘ i₂) (q₁ ∘ g ∘ i₂) q₂ + → IsCoequalizer f g (q₂ ∘ q₁) +iterated-coequalizer {C = C} {Q₁} {Q₂} i₁ i₂ f g q₁ q₂ coprod coeq₁ coeq₂ = record + { equality = ≈-i₁-i₂ + (q₂ ∘ q₁ ∘ f) + (q₂ ∘ q₁ ∘ g) + coprod + (∘-resp-≈ʳ {g = q₂} X₁.equality) + X₂.equality + ; coequalize = λ {Q} {q} q∘f≈q∘g → let module X = Cocone {Q} {q} q∘f≈q∘g in X.u₂ + ; universal = λ {Q} {q} {q∘f≈q∘g} → let module X = Cocone {Q} {q} q∘f≈q∘g in X.q≈u₂∘q₂∘q₁ + ; unique = λ {Q} {q} {i} {q∘f≈q∘g} q≈i∘q₂∘q₁ → + let module X = Cocone {Q} {q} q∘f≈q∘g in X.q≈i∘q₂∘q₁⇒i≈u₂ q≈i∘q₂∘q₁ + } + where + module X₁ = IsCoequalizer coeq₁ + module X₂ = IsCoequalizer coeq₂ + module Cocone {Q : Obj} {q : C ⇒ Q} (q∘f≈q∘g : q ∘ f ≈ q ∘ g) where + open HomReasoning + u₁ : Q₁ ⇒ Q + u₁ = X₁.coequalize (∘-resp-≈ˡ q∘f≈q∘g) + q≈u₁∘q₁ : q ≈ u₁ ∘ q₁ + q≈u₁∘q₁ = X₁.universal + u₁∘q₁∘f∘i₂≈u₁∘q₁∘g∘i₂ : u₁ ∘ q₁ ∘ f ∘ i₂ ≈ u₁ ∘ q₁ ∘ g ∘ i₂ + u₁∘q₁∘f∘i₂≈u₁∘q₁∘g∘i₂ = begin + u₁ ∘ q₁ ∘ f ∘ i₂ ≈⟨ ∘-resp-≈ˡ (Equiv.sym q≈u₁∘q₁) ⟩ + q ∘ f ∘ i₂ ≈⟨ ∘-resp-≈ˡ q∘f≈q∘g ⟩ + q ∘ g ∘ i₂ ≈⟨ ∘-resp-≈ˡ q≈u₁∘q₁ ⟩ + u₁ ∘ q₁ ∘ g ∘ i₂ ∎ + u₂ : Q₂ ⇒ Q + u₂ = X₂.coequalize u₁∘q₁∘f∘i₂≈u₁∘q₁∘g∘i₂ + u₁≈u₂∘q₂ : u₁ ≈ u₂ ∘ q₂ + u₁≈u₂∘q₂ = X₂.universal + q≈u₂∘q₂∘q₁ : q ≈ u₂ ∘ q₂ ∘ q₁ + q≈u₂∘q₂∘q₁ = begin + q ≈⟨ q≈u₁∘q₁ ⟩ + u₁ ∘ q₁ ≈⟨ ∘-resp-≈ˡ u₁≈u₂∘q₂ ⟩ + u₂ ∘ q₂ ∘ q₁ ∎ + q≈i∘q₂∘q₁⇒i≈u₂ : {i : Q₂ ⇒ Q} → q ≈ i ∘ q₂ ∘ q₁ → i ≈ u₂ + q≈i∘q₂∘q₁⇒i≈u₂ q≈i∘q₂∘q₁ = X₂.unique (Equiv.sym (X₁.unique q≈i∘q₂∘q₁)) @@ -1,3 +1,4 @@ +{-# OPTIONS --without-K --safe #-} module Util where open import Data.Fin using (Fin; toℕ) |