{-# OPTIONS --without-K --safe #-}

open import Categories.Category
open import Categories.Functor.Bifunctor

module Categories.Diagram.Wedge {o  e o′ ℓ′ e′} {C : Category o  e} {D : Category o′ ℓ′ e′}
  (F : Bifunctor (Category.op C) C D) where

private
  module C = Category C
  module D = Category D
  open D
  open HomReasoning
  variable
    A : Obj

open import Level

open import Categories.Functor hiding (id)
open import Categories.Functor.Construction.Constant
open import Categories.NaturalTransformation.Dinatural

open Functor F

record Wedge : Set (levelOfTerm F) where
  field
    E         : Obj
    dinatural : DinaturalTransformation (const E) F

  module dinatural = DinaturalTransformation dinatural

Wedge-∘ : (W : Wedge)  A  Wedge.E W  Wedge
Wedge-∘ {A = A} W f = record
  { E         = A
  ; dinatural = extranaturalʳ  X  dinatural.α X  f)
                              (sym-assoc  ∘-resp-≈ˡ (extranatural-commʳ dinatural)  assoc)
  }
  where open Wedge W

record Wedge-Morphism (W₁ W₂ : Wedge) : Set (levelOfTerm F) where
  private
    module W₁ = Wedge W₁
    module W₂ = Wedge W₂
    open DinaturalTransformation
  field
    u : W₁.E  W₂.E
    commute :  {C}  W₂.dinatural.α C  u  W₁.dinatural.α C

Wedge-id :  {W}  Wedge-Morphism W W
Wedge-id {W} = record { u = D.id ; commute = D.identityʳ }

Wedge-Morphism-∘ : {A B C : Wedge}  Wedge-Morphism B C  Wedge-Morphism A B  Wedge-Morphism A C
Wedge-Morphism-∘ M N = record { u = u M  u N ; commute =  sym-assoc  (∘-resp-≈ˡ (commute M)  commute N) }
  where
  open Wedge-Morphism
  open HomReasoning