{-# OPTIONS --without-K --safe #-}
open import Categories.Category
open import Data.Product
open import Categories.Morphism
open import Categories.Diagram.Cocone.Properties
open import Categories.Category.Construction.Cocones
open import Categories.Functor

module Helper-Definitions where
open import Level

_[_β‰…_] : {o β„“ e : Level} (π’ž : Category o β„“ e) β†’ (A B : Category.Obj π’ž) β†’ Set _
_[_β‰…_] π’ž A B = _β‰…_ π’ž A B

record Full-β‰ˆ {o β„“ e} {π’ž : Category o β„“ e} {o' β„“' e' : Level} {π’Ÿ : Category o' β„“' e'} (F : Functor π’Ÿ π’ž) : Set (o βŠ” β„“ βŠ” e βŠ” o' βŠ” β„“' βŠ” e') where
  -- A more explicit definition of 'Full'ness of a functor F.
  private
    module π’ž = Category π’ž
    module π’Ÿ = Category π’Ÿ
    module F = Functor F
  field
    preimage : βˆ€ (X Y : π’Ÿ.Obj) β†’ π’ž [ F.β‚€ X , F.β‚€ Y ] β†’ π’Ÿ [ X , Y ]
    preimage-prop : βˆ€ (X Y : π’Ÿ.Obj) β†’ (f : π’ž [ F.β‚€ X , F.β‚€ Y ]) β†’ π’ž [ F.₁ (preimage X Y f) β‰ˆ f ]


record  singleton-hom {o β„“ e} (π’ž : Category o β„“ e) (X Y : Category.Obj π’ž) : Set (β„“ βŠ” e) where
  -- the fact that a hom-setoid (from X to Y) is a singleton (up to β‰ˆ)
  field
    arr : π’ž [ X , Y ]
    unique : βˆ€ (f : π’ž [ X , Y ]) β†’ π’ž [ arr β‰ˆ f ]

  uniqueβ‚‚ : βˆ€ (f g : π’ž [ X , Y ]) β†’ π’ž [ f β‰ˆ g ]
  uniqueβ‚‚ f g =
    let open Category π’ž in
    Equiv.trans (Equiv.sym (unique f)) (unique g)

_[_=βˆƒ!=>_] : {o β„“ e : Level} β†’ (π’ž : Category o β„“ e) (X Y : Category.Obj π’ž) β†’ Set _
_[_=βˆƒ!=>_] = singleton-hom


_<===>_ : βˆ€ {a b : Level} β†’ Set a β†’ Set b β†’ Set (a βŠ” b)
_<===>_ x y = (x β†’ y) Γ— (y β†’ x)
infix -5 _<===>_

private
  variable
    o β„“ e : Level
    C D J Jβ€² : Category o β„“ e

module _ {F : Functor J C} (G : Functor C D) where
  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G
    module CF = Cocone F
    GF = G ∘F F
    module CGF = Cocone GF

  F-map-Cocone-Functor : Functor (Cocones F) (Cocones (G ∘F F))
  F-map-Cocone-Functor = record
     { Fβ‚€ = F-map-CoconeΛ‘ G
     ; F₁ = F-map-Coconeβ‡’Λ‘ G
     ; identity = Ξ» {A} β†’ G.identity
     ; homomorphism = Ξ» {X} {Y} {Z} {f} {g} β†’ G.homomorphism
     ; F-resp-β‰ˆ = G.F-resp-β‰ˆ
     }