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

open import Categories.Category

module Categories.Category.Construction.Pullbacks {o  e} (C : Category o  e) where

open import Level using (_⊔_)
open import Function using (_$_)
open import Data.Product using (_×_; _,_)

open import Categories.Diagram.Pullback C
open import Categories.Morphism.Reasoning C

open Category C

record PullbackObj W : Set (o    e) where
  field
    {A} {B}  : Obj
    arr₁     : A  W
    arr₂     : B  W
    pullback : Pullback arr₁ arr₂

  module pullback = Pullback pullback

open HomReasoning

record Pullback⇒ W (X Y : PullbackObj W) : Set (o    e) where
  module X = PullbackObj X
  module Y = PullbackObj Y
  field
    mor₁     : X.A  Y.A
    mor₂     : X.B  Y.B
    commute₁ : Y.arr₁  mor₁  X.arr₁
    commute₂ : Y.arr₂  mor₂  X.arr₂

  pbarr : X.pullback.P  Y.pullback.P
  pbarr = Y.pullback.universal $ begin
    Y.arr₁  mor₁  X.pullback.p₁ ≈⟨ pullˡ commute₁ 
    X.arr₁  X.pullback.p₁        ≈⟨ X.pullback.commute 
    X.arr₂  X.pullback.p₂        ≈˘⟨ pullˡ commute₂ 
    Y.arr₂  mor₂  X.pullback.p₂ 

open Pullback⇒

Pullbacks : Obj  Category (o    e) (o    e) e
Pullbacks W = record
  { Obj       = PullbackObj W
  ; _⇒_       = Pullback⇒ W
  ; _≈_       = λ f g  mor₁ f  mor₁ g × mor₂ f  mor₂ g
  ; id        = record
    { mor₁     = id
    ; mor₂     = id
    ; commute₁ = identityʳ
    ; commute₂ = identityʳ
    }
  ; _∘_       = λ f g  record
    { mor₁     = mor₁ f  mor₁ g
    ; mor₂     = mor₂ f  mor₂ g
    ; commute₁ = pullˡ (commute₁ f)  commute₁ g
    ; commute₂ = pullˡ (commute₂ f)  commute₂ g
    }
  ; assoc     = assoc , assoc
  ; sym-assoc = sym-assoc , sym-assoc
  ; identityˡ = identityˡ , identityˡ
  ; identityʳ = identityʳ , identityʳ
  ; identity² = identity² , identity²
  ; equiv     = record
    { refl  = refl , refl
    ; sym   = λ { (eq₁ , eq₂)  sym eq₁ , sym eq₂ }
    ; trans = λ { (eq₁ , eq₂) (eq₃ , eq₄)  trans eq₁ eq₃ , trans eq₂ eq₄ }
    }
  ; ∘-resp-≈  = λ { (eq₁ , eq₂) (eq₃ , eq₄)  ∘-resp-≈ eq₁ eq₃ , ∘-resp-≈ eq₂ eq₄ }
  }
  where open Equiv