{-# OPTIONS --without-K --safe #-}
open import Categories.Category
open import Categories.Functor hiding (id)
module Categories.Category.Construction.Cocones
{o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where
open Category C
private
variable
X : Obj
open HomReasoning
open Functor F
open import Data.Product
open import Relation.Binary using (Rel; IsEquivalence; Setoid)
import Categories.Morphism as Mor
import Categories.Morphism.IsoEquiv as IsoEquiv
open import Categories.Diagram.Cocone F public
open Mor C
open IsoEquiv C
open import Categories.Morphism.Reasoning C
open Cocone
open Coapex
open Cocone⇒
open Equiv
Cocones : Category _ _ _
Cocones = record
{ Obj = Cocone
; _⇒_ = Cocone⇒
; _≈_ = λ f g → arr f ≈ arr g
; id = record { arr = id ; commute = identityˡ }
; _∘_ = λ {A B C} f g → record
{ arr = arr f ∘ arr g
; commute = λ {X} → begin
(arr f ∘ arr g) ∘ ψ A X ≈⟨ pullʳ (commute g) ⟩
arr f ∘ ψ B X ≈⟨ commute f ⟩
ψ C X ∎
}
; assoc = assoc
; sym-assoc = sym-assoc
; identityˡ = identityˡ
; identityʳ = identityʳ
; identity² = identity²
; equiv = record
{ refl = refl
; sym = sym
; trans = trans
}
; ∘-resp-≈ = ∘-resp-≈
}
module Cocones = Category Cocones
private
variable
K K′ : Cocone
module CM = Mor Cocones
module CI = IsoEquiv Cocones
open CM using () renaming (_≅_ to _⇔_)
open CI using () renaming (_≃_ to _↮_)
cocone-resp-iso : ∀ (κ : Cocone) → Cocone.N κ ≅ X → Σ[ κ′ ∈ Cocone ] κ ⇔ κ′
cocone-resp-iso {X = X} κ κ≅X = record
{ coapex = record
{ ψ = λ Y → from ∘ Cocone.ψ κ Y
; commute = λ f → pullʳ (Cocone.commute κ f)
}
} , record
{ from = record
{ arr = from
; commute = refl
}
; to = record
{ arr = to
; commute = cancelˡ isoˡ
}
; iso = record
{ isoˡ = isoˡ
; isoʳ = isoʳ
}
}
where open _≅_ κ≅X
open Cocone
open Coapex
iso-cocone⇒iso-coapex : K ⇔ K′ → N K ≅ N K′
iso-cocone⇒iso-coapex K⇔K′ = record
{ from = arr from
; to = arr to
; iso = record
{ isoˡ = isoˡ
; isoʳ = isoʳ
}
}
where open _⇔_ K⇔K′