{-# OPTIONS --safe #-}
module Cubical.Categories.Limits.Pullback where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.PropositionalTruncation.Base
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Cospan
open import Cubical.Categories.Limits.Limits
private
variable
ℓ ℓ' : Level
module _ (C : Category ℓ ℓ') where
open Category C
open Functor
record Cospan : Type (ℓ-max ℓ ℓ') where
constructor cospan
field
l m r : ob
s₁ : C [ l , m ]
s₂ : C [ r , m ]
open Cospan
isPullback : (cspn : Cospan) →
{c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
(H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → Type (ℓ-max ℓ ℓ')
isPullback cspn {c} p₁ p₂ H =
∀ {d} (h : C [ d , cspn .l ]) (k : C [ d , cspn .r ])
(H' : h ⋆ cspn .s₁ ≡ k ⋆ cspn .s₂)
→ ∃![ hk ∈ C [ d , c ] ] (h ≡ hk ⋆ p₁) × (k ≡ hk ⋆ p₂)
isPropIsPullback : (cspn : Cospan) →
{c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
(H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → isProp (isPullback cspn p₁ p₂ H)
isPropIsPullback cspn p₁ p₂ H =
isPropImplicitΠ (λ x → isPropΠ3 λ h k H' → isPropIsContr)
record Pullback (cspn : Cospan) : Type (ℓ-max ℓ ℓ') where
field
pbOb : ob
pbPr₁ : C [ pbOb , cspn .l ]
pbPr₂ : C [ pbOb , cspn .r ]
pbCommutes : pbPr₁ ⋆ cspn .s₁ ≡ pbPr₂ ⋆ cspn .s₂
univProp : isPullback cspn pbPr₁ pbPr₂ pbCommutes
pullbackArrow :
{c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
(H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → C [ c , pbOb ]
pullbackArrow p₁ p₂ H = univProp p₁ p₂ H .fst .fst
pullbackArrowUnique :
{c : ob} {p₁ : C [ c , cspn .l ]} {p₂ : C [ c , cspn .r ]}
{H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂}
{pbArrow' : C [ c , pbOb ]}
(H₁ : p₁ ≡ pbArrow' ⋆ pbPr₁) (H₂ : p₂ ≡ pbArrow' ⋆ pbPr₂)
→ pullbackArrow p₁ p₂ H ≡ pbArrow'
pullbackArrowUnique H₁ H₂ =
cong fst (univProp _ _ _ .snd (_ , (H₁ , H₂)))
open Pullback
pullbackArrowPr₁ :
{cspn : Cospan} (pb : Pullback cspn)
{c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
(H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) →
p₁ ≡ pullbackArrow pb p₁ p₂ H ⋆ pbPr₁ pb
pullbackArrowPr₁ pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .snd .fst
pullbackArrowPr₂ :
{cspn : Cospan} (pb : Pullback cspn)
{c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
(H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) →
p₂ ≡ pullbackArrow pb p₁ p₂ H ⋆ pbPr₂ pb
pullbackArrowPr₂ pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .snd .snd
Pullbacks : Type (ℓ-max ℓ ℓ')
Pullbacks = (cspn : Cospan) → Pullback cspn
hasPullbacks : Type (ℓ-max ℓ ℓ')
hasPullbacks = ∥ Pullbacks ∥₁
module _ {C : Category ℓ ℓ'} where
open Category C
open Functor
open Pullback
open LimCone
open Cone
open Cospan
Cospan→Func : Cospan C → Functor CospanCat C
Cospan→Func (cospan l m r f g) .F-ob ⓪ = l
Cospan→Func (cospan l m r f g) .F-ob ① = m
Cospan→Func (cospan l m r f g) .F-ob ② = r
Cospan→Func (cospan l m r f g) .F-hom {⓪} {①} k = f
Cospan→Func (cospan l m r f g) .F-hom {②} {①} k = g
Cospan→Func (cospan l m r f g) .F-hom {⓪} {⓪} k = id
Cospan→Func (cospan l m r f g) .F-hom {①} {①} k = id
Cospan→Func (cospan l m r f g) .F-hom {②} {②} k = id
Cospan→Func (cospan l m r f g) .F-id {⓪} = refl
Cospan→Func (cospan l m r f g) .F-id {①} = refl
Cospan→Func (cospan l m r f g) .F-id {②} = refl
Cospan→Func (cospan l m r f g) .F-seq {⓪} {⓪} {⓪} φ ψ = sym (⋆IdL _)
Cospan→Func (cospan l m r f g) .F-seq {⓪} {⓪} {①} φ ψ = sym (⋆IdL _)
Cospan→Func (cospan l m r f g) .F-seq {⓪} {①} {①} φ ψ = sym (⋆IdR _)
Cospan→Func (cospan l m r f g) .F-seq {①} {①} {①} φ ψ = sym (⋆IdL _)
Cospan→Func (cospan l m r f g) .F-seq {②} {②} {②} φ ψ = sym (⋆IdL _)
Cospan→Func (cospan l m r f g) .F-seq {②} {②} {①} φ ψ = sym (⋆IdL _)
Cospan→Func (cospan l m r f g) .F-seq {②} {①} {①} φ ψ = sym (⋆IdR _)
LimitsOfShapeCospanCat→Pullbacks : LimitsOfShape CospanCat C → Pullbacks C
pbOb (LimitsOfShapeCospanCat→Pullbacks H cspn) = lim (H (Cospan→Func cspn))
pbPr₁ (LimitsOfShapeCospanCat→Pullbacks H cspn) = limOut (H (Cospan→Func cspn)) ⓪
pbPr₂ (LimitsOfShapeCospanCat→Pullbacks H cspn) = limOut (H (Cospan→Func cspn)) ②
pbCommutes (LimitsOfShapeCospanCat→Pullbacks H cspn) = limOutCommutes (H (Cospan→Func cspn)) {v = ①} tt
∙ sym (limOutCommutes (H (Cospan→Func cspn)) tt)
univProp (LimitsOfShapeCospanCat→Pullbacks H cspn) {d = d} h k H' =
uniqueExists (limArrow (H (Cospan→Func cspn)) d cc)
( sym (limArrowCommutes (H (Cospan→Func cspn)) d cc ⓪)
, sym (limArrowCommutes (H (Cospan→Func cspn)) d cc ②))
(λ _ → isProp× (isSetHom _ _) (isSetHom _ _))
λ a' ha' → limArrowUnique (H (Cospan→Func cspn)) d cc a'
(λ { ⓪ → sym (ha' .fst)
; ① → cong (a' ⋆_) (sym (limOutCommutes (H (Cospan→Func cspn)) {⓪} {①} tt))
∙∙ sym (⋆Assoc _ _ _)
∙∙ cong (_⋆ cspn .s₁) (sym (ha' .fst))
; ② → sym (ha' .snd) })
where
cc : Cone (Cospan→Func cspn) d
coneOut cc ⓪ = h
coneOut cc ① = h ⋆ cspn .s₁
coneOut cc ② = k
coneOutCommutes cc {⓪} {⓪} e = ⋆IdR h
coneOutCommutes cc {⓪} {①} e = refl
coneOutCommutes cc {①} {①} e = ⋆IdR _
coneOutCommutes cc {②} {①} e = sym H'
coneOutCommutes cc {②} {②} e = ⋆IdR k
Limits→Pullbacks : Limits C → Pullbacks C
Limits→Pullbacks H = LimitsOfShapeCospanCat→Pullbacks (H CospanCat)