open import Cat.Instances.Shape.Cospan
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Limit.Cone
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Prelude

module Cat.Diagram.Limit.Pullback {o h} (Cat : Precategory o h) where

We establish the correspondence between Pullback and the Limit of a cospan diagram.

open import Cat.Reasoning Cat

-- Yikes:
open is-pullback
open Terminal
open Cone-hom
open Pullback
open Functor
open Cone

Square→Cone
  : ∀ {x y} {P} {F : Functor (·→·←· {x} {y}) Cat}
  → (p1 : Hom P (F .F₀ cs-a)) (p2 : Hom P (F .F₀ cs-b))
  → F .F₁ {cs-a} {cs-c} _ ∘ p1 ≡ F .F₁ {cs-b} {cs-c} _ ∘ p2
  → Cone F
Square→Cone p1 p2 square .apex = _
Square→Cone p1 p2 square .ψ cs-a = p1
Square→Cone p1 p2 square .ψ cs-b = p2
Square→Cone {F = F} p1 p2 square .ψ cs-c = F .F₁ _ ∘ p1
Square→Cone {F = F} p1 p2 square .commutes {cs-a} {cs-a} _ = eliml (F .F-id)
Square→Cone {F = F} p1 p2 square .commutes {cs-a} {cs-c} _ = refl
Square→Cone {F = F} p1 p2 square .commutes {cs-b} {cs-b} _ = eliml (F .F-id)
Square→Cone {F = F} p1 p2 square .commutes {cs-b} {cs-c} _ = sym square
Square→Cone {F = F} p1 p2 square .commutes {cs-c} {cs-c} _ = eliml (F .F-id)

Pullback→Terminal-cone
  : ∀ {x y} {A B C} {f : Hom A C} {g : Hom B C}
  → Pullback Cat f g
  → Terminal (Cones (cospan→cospan-diagram x y {C = Cat} f g))
Pullback→Terminal-cone {f = f} {g} pb = lim where
  module pb = Pullback pb
  lim : Terminal (Cones _)
  lim .top = Square→Cone _ _ pb.square
  lim .has⊤ cone .centre .hom      = pb.universal (cone .commutes (lift tt) ∙ sym (cone .commutes {cs-b} {cs-c} (lift tt)))
  lim .has⊤ cone .centre .commutes cs-a = pb.p₁∘universal
  lim .has⊤ cone .centre .commutes cs-b = pb.p₂∘universal
  lim .has⊤ cone .centre .commutes cs-c = pullr pb.p₁∘universal ∙ cone .commutes (lift tt)
  lim .has⊤ cone .paths otherhom = Cone-hom-path _ (sym (pb.unique (otherhom .commutes _) (otherhom .commutes _)))

Terminal-cone→Pullback
  : ∀ {x y}
  → {F : Functor (·→·←· {x} {y}) Cat}
  → Terminal (Cones F)
  → Pullback Cat (F .F₁ {cs-a} {cs-c} _) (F .F₁ {cs-b} {cs-c} _)
Terminal-cone→Pullback {F = F} lim = pb where
  module lim = Terminal lim
  pb : Pullback Cat _ _
  pb .apex = lim.top .apex
  pb .p₁ = lim.top .ψ cs-a
  pb .p₂ = lim.top .ψ cs-b
  pb .has-is-pb .square = lim.top .commutes _ ∙ sym (lim.top .commutes {cs-b} {cs-c} _)
  pb .has-is-pb .universal x = lim.has⊤ (Square→Cone _ _ x) .centre .hom
  pb .has-is-pb .p₁∘universal {p = p} = lim.has⊤ (Square→Cone _ _ p) .centre .commutes cs-a
  pb .has-is-pb .p₂∘universal {p = p} = lim.has⊤ (Square→Cone _ _ p) .centre .commutes cs-b
  pb .has-is-pb .unique {p₁' = p₁'} {p₂'} {p} {lim'} a b =
    sym (ap hom (lim.has⊤ (Square→Cone _ _ p) .paths other))
    where
      other : Cone-hom _ _ _
      other .hom = _
      other .commutes cs-a = a
      other .commutes cs-b = b
      other .commutes cs-c =
        lim.top .ψ cs-c ∘ lim'                         ≡˘⟨ pulll (lim.top .commutes _) ⟩≡˘
        F .F₁ {cs-a} {cs-c} _ ∘ lim.top .ψ cs-a ∘ lim' ≡⟨ ap (_ ∘_) a ⟩≡
        F .F₁ {cs-a} {cs-c} _ ∘ p₁'                    ∎

Limit→Pullback
  : ∀ {x y} {a b c} → {f : Hom a c} {g : Hom b c}
  → Limit (cospan→cospan-diagram x y f g)
  → Pullback Cat f g
Limit→Pullback x = Terminal-cone→Pullback (Limit→Terminal-cone _ x)

Pullback→Limit
  : ∀ {x y} {A B C} {f : Hom A C} {g : Hom B C}
  → Pullback Cat f g
  → Limit (cospan→cospan-diagram x y {C = Cat} f g)
Pullback→Limit x = Terminal-cone→Limit _ (Pullback→Terminal-cone x)