open import Cat.Diagram.Pullback.Properties
open import Cat.Diagram.Pullback
open import Cat.Prelude

import Cat.Displayed.Instances.Subobjects as Subobjs
import Cat.Reasoning as Cat

module Cat.Diagram.Pullback.Along where

Pullbacks along an indeterminate morphism🔗

module _ {o ℓ} (C : Precategory o ℓ) where
  open Precategory C

This module defines the auxiliary notion of a map $p_{1} : P \to X$ being the pullback of a map $g : Y \to Z$ along a map $f : X \to Z,$ by summing over the possible maps $P \to Y$ fitting in the diagram below.

While this is a rather artificial notion, it comes up a lot in the context of elementary topos theory, especially in the case where $g$ is the generic subobject $true : ⊤ \to Ω .$

  record is-pullback-along {P X Y Z} (p₁ : Hom P X) (f : Hom X Z) (g : Hom Y Z) : Type (o ⊔ ℓ) where
    no-eta-equality
    field
      top       : Hom P Y
      has-is-pb : is-pullback C p₁ f top g
    open is-pullback has-is-pb public

open is-pullback-along
open is-pullback
open Pullback

module _ {o ℓ} {C : Precategory o ℓ} where
  open Subobjs C
  open Cat C

  private
    unquoteDecl eqv = declare-record-iso eqv (quote is-pullback-along)
    variable
      U V W X Y Z : Ob
      f g h k m n l nm : Hom X Y
  abstract

Warning

Despite the name is-pullback-along, nothing about the definition guarantees that this type is a proposition after fixing the three maps $p_{1},$ $f$ and $g .$ However, we choose to name this auxiliary notion as though it were always a proposition, since it will most commonly be used when $g$ is a monomorphism, and, under this assumption, it is propositional:

    is-monic→is-pullback-along-is-prop
      : ∀ {P X Y Z} {f : Hom P X} {g : Hom X Z} {h : Hom Y Z}
      → is-monic h
      → is-prop (is-pullback-along C f g h)
    is-monic→is-pullback-along-is-prop h-monic = Iso→is-hlevel 1 eqv λ (_ , x) (_ , y) →
      Σ-prop-path! (h-monic _ _ (sym (x .square) ∙ y .square))

Of course, the notion of being a pullback along a map is closed under composition: if $k$ is the pullback of $l$ along $n,$ and $h$ is the pullback of $k$ along $m,$ as in the diagram below, then $h$ is also the pullback of $l$ along $n \circ m .$

  paste-is-pullback-along
    : is-pullback-along C k n l → is-pullback-along C h m k
    → n ∘ m ≡ nm → is-pullback-along C h nm l
  paste-is-pullback-along p q r .top = p .top ∘ q .top
  paste-is-pullback-along p q r .has-is-pb =
    subst-is-pullback refl r refl refl (rotate-pullback (pasting-left→outer-is-pullback
      (rotate-pullback (p .has-is-pb))
      (rotate-pullback (q .has-is-pb))
      ( extendl (sym (p .is-pullback-along.square))
      ∙ pushr (sym (q .is-pullback-along.square)))))