| 12345678910111213141516171819202122232425262728 |
- module Pullback where
- open import Logic.Equivalence
- open import Logic.Relations
- open import Logic.Base
- open import Category
- open import Unique
- module Pull (ℂ : Cat) where
- private open module CC = Category.Category ℂ
- private open module U = Uniq ℂ
- record isPull {A B C D A' : Obj}(f : A ─→ B)(g : A ─→ C)(f' : C ─→ D)(g' : B ─→ D)(h₁ : A' ─→ C)(h₂ : A' ─→ B)(commut : f' ∘ h₁ == g' ∘ h₂) : Set1 where
- field unique : ∃! \(h : A' ─→ A) -> (g ∘ h == h₁) /\ (f ∘ h == h₂)
- record pullback {B C D : Obj}(g' : B ─→ D)(f' : C ─→ D) : Set1 where
- field
- A : Obj
- f : A ─→ B
- g : A ─→ C
- comm : g' ∘ f == f' ∘ g
- pull : (forall {A' : Obj}(h₁ : A' ─→ C)(h₂ : A' ─→ B)(commut : f' ∘ h₁ == g' ∘ h₂) -> isPull f g f' g' h₁ h₂ commut)
- record PullCat : Set2 where
- field pull : {B C D : Obj}(g' : B ─→ D)(f' : C ─→ D) -> pullback g' f'
|
