{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Core using (Category)

module Categories.Diagram.Pullback {o  e} (C : Category o  e) where

open Category C
open HomReasoning
open Equiv

open import Level
open import Data.Product using (_,_; )
open import Function using (flip; _$_) renaming (_∘_ to _●_)
open import Categories.Morphism C
open import Categories.Object.Product C hiding (up-to-iso; repack; repack∘; repack-cancel)
open import Categories.Diagram.Equalizer C hiding (up-to-iso)
open import Categories.Morphism.Reasoning C as Square
  renaming (glue to glue-square) hiding (id-unique)

private
  variable
    A B X Y Z : Obj
    f g h h₁ h₂ i i₁ i₂ j k : A  B

-- Proof that a given square is a pullback
record IsPullback {P : Obj} (p₁ : P  X) (p₂ : P  Y) (f : X  Z) (g : Y  Z) : Set (o    e) where
  field
    commute         : f  p₁  g  p₂
    universal       :  {h₁ : A  X} {h₂ : A  Y}  f  h₁  g  h₂  A  P
    p₁∘universal≈h₁ :  {eq : f  h₁  g  h₂} 
                        p₁  universal eq  h₁
    p₂∘universal≈h₂ :  {eq : f  h₁  g  h₂} 
                        p₂  universal eq  h₂
    unique-diagram  : p₁  h  p₁  i 
                      p₂  h  p₂  i 
                      h  i

  unique :  {eq : f  h₁  g  h₂}  p₁  i  h₁  p₂  i  h₂  i  universal eq
  unique p₁∘i≈h₁ p₂∘i≈h₂ =
    unique-diagram
      (p₁∘i≈h₁   p₁∘universal≈h₁)
      (p₂∘i≈h₂   p₂∘universal≈h₂)

  unique′ : (eq eq′ : f  h₁  g  h₂)  universal eq  universal eq′
  unique′ eq eq′ = unique p₁∘universal≈h₁ p₂∘universal≈h₂

  id-unique : id  universal commute
  id-unique = unique identityʳ identityʳ

  universal-resp-≈ :  {eq : f  h₁  g  h₂} {eq′ : f  i₁  g  i₂}  h₁  i₁  h₂  i₂  universal eq  universal eq′
  universal-resp-≈ h₁≈i₁ h₂≈i₂ = unique (p₁∘universal≈h₁  h₁≈i₁) (p₂∘universal≈h₂  h₂≈i₂)

-- Pullback of two arrows with a common codomain
record Pullback (f : X  Z) (g : Y  Z) : Set (o    e) where
  field
    {P} : Obj
    p₁  : P  X
    p₂  : P  Y
    isPullback : IsPullback p₁ p₂ f g

  open IsPullback isPullback public

up-to-iso : (pullback pullback′ : Pullback f g)  Pullback.P pullback  Pullback.P pullback′
up-to-iso pullback pullback′ = record
  { from = repack pullback pullback′
  ; to = repack pullback′ pullback
  ; iso = record
    { isoˡ = repack-cancel pullback′ pullback
    ; isoʳ = repack-cancel pullback pullback′
    }
  }
  where
    open Pullback

    repack : (pullback pullback′ : Pullback f g)  P pullback  P pullback′
    repack pullback pullback′ = universal pullback′ (commute pullback)

    repack∘ : (pullback pullback′ pullback″ : Pullback f g)  repack pullback′ pullback″  repack pullback pullback′  repack pullback pullback″
    repack∘ pullback pullback′ pullback″ =
      unique pullback″
             (glueTrianglesʳ (p₁∘universal≈h₁ pullback″) (p₁∘universal≈h₁ pullback′))
             (glueTrianglesʳ (p₂∘universal≈h₂ pullback″) (p₂∘universal≈h₂ pullback′))

    repack-cancel : (pullback pullback′ : Pullback f g)  repack pullback pullback′  repack pullback′ pullback  id
    repack-cancel pullback pullback′ = repack∘ pullback′ pullback pullback′   (id-unique pullback′)

swap : Pullback f g  Pullback g f
swap p = record
  { p₁              = p₂
  ; p₂              = p₁
  ; isPullback = record
    { commute          =  commute
    ; universal       = universal  
    ; p₁∘universal≈h₁ = p₂∘universal≈h₂
    ; p₂∘universal≈h₂ = p₁∘universal≈h₁
    ; unique-diagram  = flip unique-diagram
    }
  }
  where open Pullback p

glue : (p : Pullback f g)  Pullback h (Pullback.p₁ p)  Pullback (f  h) g
glue {h = h} p q = record
  { p₁              = q.p₁
  ; p₂              = p.p₂  q.p₂
  ; isPullback = record
    { commute         = glue-square p.commute q.commute
    ; universal       = λ eq  q.universal ( (p.p₁∘universal≈h₁ {eq = sym-assoc  eq}))
    ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁
    ; p₂∘universal≈h₂ = assoc  ∘-resp-≈ʳ q.p₂∘universal≈h₂  p.p₂∘universal≈h₂
    ; unique-diagram  = λ {_ j i} eq₁ eq₂ 
        let eq′ : p.p₁  q.p₂  j  p.p₁  q.p₂  i
            eq′ = begin
              p.p₁  q.p₂  j ≈⟨ extendʳ q.commute 
              h  q.p₁  j    ≈⟨ refl⟩∘⟨ eq₁ 
              h  q.p₁  i    ≈⟨ extendʳ q.commute 
              p.p₁  q.p₂  i 
        in q.unique-diagram eq₁ (p.unique-diagram eq′ (sym-assoc  eq₂  assoc))
    }
  }
  where module p = Pullback p
        module q = Pullback q

unglue : (p : Pullback f g)  Pullback (f  h) g  Pullback h (Pullback.p₁ p)
unglue {f = f} {g = g} {h = h} p q = record
  { p₁              = q.p₁
  ; p₂              = p₂′
  ; isPullback = record
    { commute         =  p.p₁∘universal≈h₁
    ; universal       = λ {_ h₁ h₂} eq  q.universal $ begin
      (f  h)  h₁      ≈⟨ pullʳ eq 
      f  p.p₁  h₂     ≈⟨ extendʳ p.commute 
      g  p.p₂  h₂     
    ; p₁∘universal≈h₁ = q.p₁∘universal≈h₁
    ; p₂∘universal≈h₂ = λ {_ _ _ eq} 
      p.unique-diagram ((pullˡ p.p₁∘universal≈h₁)  pullʳ q.p₁∘universal≈h₁  eq)
                       (pullˡ p.p₂∘universal≈h₂  q.p₂∘universal≈h₂)
    ; unique-diagram  = λ {_ j i} eq₁ eq₂ 
        let eq′ : q.p₂  j  q.p₂  i
            eq′ = begin
              q.p₂  j       ≈⟨ pushˡ ( p.p₂∘universal≈h₂) 
              p.p₂  p₂′  j ≈⟨ refl⟩∘⟨ eq₂ 
              p.p₂  p₂′  i ≈⟨ pullˡ p.p₂∘universal≈h₂ 
              q.p₂  i 
        in q.unique-diagram eq₁ eq′
    }
  }
  where module p = Pullback p
        module q = Pullback q
        p₂′ = p.universal (sym-assoc  q.commute) -- used twice above

Product×Equalizer⇒Pullback :
  (p : Product A B)  Equalizer (f  Product.π₁ p) (g  Product.π₂ p) 
  Pullback f g
Product×Equalizer⇒Pullback {f = f} {g = g} p e = record
  { p₁              = π₁  arr
  ; p₂              = π₂  arr
  ; isPullback = record
    { commute         = sym-assoc  equality  assoc
    ; universal       = λ {_ h₁ h₂} eq  equalize $ begin
      (f  π₁)   h₁ , h₂  ≈⟨ pullʳ project₁ 
      f  h₁                ≈⟨ eq 
      g  h₂                ≈˘⟨ pullʳ project₂ 
      (g  π₂)   h₁ , h₂  
    ; p₁∘universal≈h₁ = pullʳ ( e.universal)  project₁
    ; p₂∘universal≈h₂ = pullʳ ( e.universal)  project₂
    ; unique-diagram  = λ eq₁ eq₂ 
      e.unique-diagram (p.unique′ (sym-assoc  eq₁  assoc) (sym-assoc  eq₂  assoc))
    }
  }
  where module p = Product p
        module e = Equalizer e
        open p
        open e

Product×Pullback⇒Equalizer : (p : Product A B)  Pullback f g 
  Equalizer (f  Product.π₁ p) (g  Product.π₂ p)
Product×Pullback⇒Equalizer {f = f} {g = g} p pu = record
  { arr       =  p₁ , p₂ 
  ; isEqualizer = record
    { equality  = begin
      (f  π₁)   p₁ , p₂  ≈⟨ pullʳ project₁ 
      f  p₁                 ≈⟨ commute 
      g  p₂                 ≈˘⟨ pullʳ project₂ 
      (g  π₂)   p₁ , p₂  
    ; equalize  = λ eq  pu.universal (sym-assoc  eq  assoc)
    ; universal = λ {_ h}  begin
      h                      ≈˘⟨ p.unique ( p₁∘universal≈h₁) ( p₂∘universal≈h₂) 
       p₁  _ , p₂  _     ≈⟨ p.unique (pullˡ project₁) (pullˡ project₂) 
       p₁ , p₂   _        
    ; unique    = λ eq  pu.unique (pushˡ ( project₁)   (∘-resp-≈ʳ eq))
                                   (pushˡ ( project₂)   (∘-resp-≈ʳ eq))
  }
  }
  where module p = Product p
        module pu = Pullback pu
        open p
        open pu

module _ (p : Pullback f g) where
  open Pullback p

  Pullback-resp-≈ : h  f  i  g  Pullback h i
  Pullback-resp-≈ eq eq′ = record
    { p₁              = p₁
    ; p₂              = p₂
    ; isPullback = record
      { commute         = ∘-resp-≈ˡ eq  commute   (∘-resp-≈ˡ eq′)
      ; universal       = λ eq″  universal (∘-resp-≈ˡ ( eq)  eq″  ∘-resp-≈ˡ eq′)
      ; p₁∘universal≈h₁ = p₁∘universal≈h₁
      ; p₂∘universal≈h₂ = p₂∘universal≈h₂
      ; unique-diagram  = unique-diagram
      }
    }

  Pullback-resp-Mono : Mono g  Mono p₁
  Pullback-resp-Mono mg h i eq = unique-diagram eq (mg _ _ eq′)
    where eq′ : g  p₂  h  g  p₂  i
          eq′ = begin
            g  p₂  h ≈⟨ extendʳ (sym commute) 
            f  p₁  h ≈⟨ refl⟩∘⟨ eq 
            f  p₁  i ≈⟨ extendʳ commute 
            g  p₂  i 

  Pullback-resp-Iso : Iso g h   λ i  Iso p₁ i
  Pullback-resp-Iso {h = h} iso = universal eq
                                , record
                                { isoˡ = unique-diagram eq₁ eq₂
                                ; isoʳ = p₁∘universal≈h₁
                                }
    where open Iso iso
          eq = begin
            f  id                 ≈⟨ introˡ refl 
            id  f  id            ≈⟨ pushˡ ( isoʳ) 
            g  h  f  id         
          eq₁ = begin
            p₁  universal eq  p₁ ≈⟨ cancelˡ p₁∘universal≈h₁ 
            p₁                     ≈˘⟨ identityʳ 
            p₁  id                
          eq₂ = begin
            p₂  universal eq  p₁ ≈⟨ extendʳ p₂∘universal≈h₂ 
            h  (f  id)  p₁      ≈⟨ refl ⟩∘⟨ identityʳ ⟩∘⟨ refl 
            h  f  p₁             ≈⟨ refl ⟩∘⟨ commute 
            h  g  p₂             ≈⟨ cancelˡ isoˡ 
            p₂                     ≈˘⟨ identityʳ 
            p₂  id