PullbackLemma.agda

{-# OPTIONS --safe #-}
open import Cat.Prelude
import Cat.Morphism
import Cat.Diagram.Pullback

module PullbackLemma {ℓ ℓ′} (Cat : Precategory ℓ ℓ′) where

open Cat.Morphism Cat
open Cat.Diagram.Pullback Cat

pullback-lemma-fwd : ∀ {A B C D E F : Ob}
                       (f : A ⇒ B) (g : B ⇒ C)
                       (h : D ⇒ E) (i : E ⇒ F)
                       (u : A ⇒ D) (v : B ⇒ E) (w : C ⇒ F)
                   → is-pullback f v u h
                   → is-pullback g w v i
                   → is-pullback (g ∘ f) w u (i ∘ h)
pullback-lemma-fwd f g h i u v w pl pr .is-pullback.square =
    assoc f g w ⁻¹
  ∙ ap (_∘ f) (pr .is-pullback.square)
  ∙ assoc f v i
  ∙ ap (i ∘_) (pl .is-pullback.square)
  ∙ assoc u h i ⁻¹
pullback-lemma-fwd {A} {B} f g h i u v w pl pr .is-pullback.has-univ {P′} {p₁′} {p₂′} comm =
  record
   { universal = plu
   ; p₁∘universal =
          assoc plu f g
        ∙ ap (g ∘_) (plhu .universal-for.p₁∘universal)
        ∙ prhu .universal-for.p₁∘universal
   ; p₂∘universal = plhu .universal-for.p₂∘universal
   ; unique = λ {lim′} e1 e2 →
                     plhu .universal-for.unique
                        (prhu .universal-for.unique
                           (  assoc lim′ f g ⁻¹
                            ∙ e1)
                           (  assoc lim′ f v ⁻¹
                            ∙ ap (_∘ lim′) (pl .is-pullback.square)
                            ∙ assoc lim′ u h
                            ∙ ap (h ∘_) e2))
                        e2
   }
  where
  prhu = pr .is-pullback.has-univ {P′} {p₁′ = p₁′} {p₂′ = h ∘ p₂′}
              (comm ∙ assoc p₂′ h i)
  pru : P′ ⇒ B
  pru = prhu .universal-for.universal
  
  plhu = pl .is-pullback.has-univ {P′} {p₁′ = pru} {p₂′ = p₂′}
              (prhu .universal-for.p₂∘universal)
  plu : P′ ⇒ A
  plu = plhu .universal-for.universal

pullback-lemma-bwd : ∀ {A B C D E F : Ob}
                       (f : A ⇒ B) (g : B ⇒ C)
                       (h : D ⇒ E) (i : E ⇒ F)
                       (u : A ⇒ D) (v : B ⇒ E) (w : C ⇒ F)
                   → is-pullback g w v i
                   → is-pullback (g ∘ f) w u (i ∘ h)
                   → v ∘ f ＝ h ∘ u
                   → is-pullback f v u h
pullback-lemma-bwd f g h i u v w pr pb eq .is-pullback.square = eq
pullback-lemma-bwd f g h i u v w pr pb eq .is-pullback.has-univ {P′} {p₁′} {p₂′} comm =
  record {
    universal    = ub
  ; p₁∘universal =
      pr-c .universal-for.unique {lim′ = f ∘ ub}
             (  assoc ub f g ⁻¹
              ∙ pb-c .universal-for.p₁∘universal)
             (  assoc ub f v ⁻¹
              ∙ ap (_∘ ub) eq
              ∙ assoc ub u h
              ∙ ap (h ∘_)
                   (pb-c .universal-for.p₂∘universal))
      ∙ pr-c .universal-for.unique {lim′ = p₁′} refl comm ⁻¹
  ; p₂∘universal = pb-c .universal-for.p₂∘universal
  ; unique = λ {lim′} e1 e2 →
                 pb-c .universal-for.unique
                        (assoc lim′ f g ∙ ap (g ∘_) e1) e2
  }
  where
  eq′ : w ∘ g ∘ p₁′ ＝ (i ∘ h) ∘ p₂′
  eq′ =   assoc p₁′ g w ⁻¹
        ∙ ap (_∘ p₁′) (pr .is-pullback.square)
        ∙ assoc p₁′ v i
        ∙ ap (i ∘_) comm
        ∙ assoc p₂′ h i ⁻¹
  pb-c = pb .is-pullback.has-univ eq′
  pr-c = pr .is-pullback.has-univ (eq′ ∙ assoc p₂′ h i)
  ub   = pb-c .universal-for.universal