-- Pullback from product and equalizer -- -- -- Shinji KONO ---- open import Category -- https://github.com/konn/category-agda open import Level module pullback { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ') ( Γ : Functor I A ) where open import HomReasoning open import cat-utility -- -- Pullback from equalizer and product -- f -- a -------> c -- ^ ^ -- π1 | |g -- | | -- ab -------> b -- ^ π2 -- | -- | e = equalizer (f π1) (g π1) -- | -- d <------------------ d' -- k (π1' × π2' ) open Equalizer open Product open Pullback pullback-from : (a b c ab d : Obj A) ( f : Hom A a c ) ( g : Hom A b c ) ( π1 : Hom A ab a ) ( π2 : Hom A ab b ) ( e : Hom A d ab ) ( eqa : {a b c : Obj A} → (f g : Hom A a b) → {e : Hom A c a } → Equalizer A e f g ) ( prod : Product A a b ab π1 π2 ) → Pullback A a b c d f g ( A [ π1 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] ) ( A [ π2 o equalizer ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ){e} ) ] ) pullback-from a b c ab d f g π1 π2 e eqa prod = record { commute = commute1 ; p = p1 ; π1p=π1 = λ {d} {π1'} {π2'} {eq} → π1p=π11 {d} {π1'} {π2'} {eq} ; π2p=π2 = λ {d} {π1'} {π2'} {eq} → π2p=π21 {d} {π1'} {π2'} {eq} ; uniqueness = uniqueness1 } where commute1 : A [ A [ f o A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ≈ A [ g o A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] ] ] commute1 = let open ≈-Reasoning (A) in begin f o ( π1 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) ≈⟨ assoc ⟩ ( f o π1 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) ≈⟨ fe=ge (eqa (A [ f o π1 ]) (A [ g o π2 ])) ⟩ ( g o π2 ) o equalizer (eqa ( f o π1 ) ( g o π2 )) ≈↑⟨ assoc ⟩ g o ( π2 o equalizer (eqa ( f o π1 ) ( g o π2 )) ) ∎ lemma1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → A [ A [ A [ f o π1 ] o (prod × π1') π2' ] ≈ A [ A [ g o π2 ] o (prod × π1') π2' ] ] lemma1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in begin ( f o π1 ) o (prod × π1') π2' ≈↑⟨ assoc ⟩ f o ( π1 o (prod × π1') π2' ) ≈⟨ cdr (π1fxg=f prod) ⟩ f o π1' ≈⟨ eq ⟩ g o π2' ≈↑⟨ cdr (π2fxg=g prod) ⟩ g o ( π2 o (prod × π1') π2' ) ≈⟨ assoc ⟩ ( g o π2 ) o (prod × π1') π2' ∎ p1 : {d' : Obj A} {π1' : Hom A d' a} {π2' : Hom A d' b} → A [ A [ f o π1' ] ≈ A [ g o π2' ] ] → Hom A d' d p1 {d'} { π1' } { π2' } eq = let open ≈-Reasoning (A) in k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) ( lemma1 eq ) π1p=π11 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π1' ] π1p=π11 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in begin ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq ≈⟨⟩ ( π1 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ≈↑⟨ assoc ⟩ π1 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ π1 o (_×_ prod π1' π2' ) ≈⟨ π1fxg=f prod ⟩ π1' ∎ π2p=π21 : {d₁ : Obj A} {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ] o p1 eq ] ≈ π2' ] π2p=π21 {d'} {π1'} {π2'} {eq} = let open ≈-Reasoning (A) in begin ( π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ]) {e} ) ) o p1 eq ≈⟨⟩ ( π2 o e) o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ≈↑⟨ assoc ⟩ π2 o ( e o k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ) ≈⟨ cdr ( ek=h ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} )) ⟩ π2 o (_×_ prod π1' π2' ) ≈⟨ π2fxg=g prod ⟩ π2' ∎ uniqueness1 : {d₁ : Obj A} (p' : Hom A d₁ d) {π1' : Hom A d₁ a} {π2' : Hom A d₁ b} {eq : A [ A [ f o π1' ] ≈ A [ g o π2' ] ]} → {eq1 : A [ A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π1' ]} → {eq2 : A [ A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ] ≈ π2' ]} → A [ p1 eq ≈ p' ] uniqueness1 {d'} p' {π1'} {π2'} {eq} {eq1} {eq2} = let open ≈-Reasoning (A) in begin p1 eq ≈⟨⟩ k ( eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e} ) (_×_ prod π1' π2' ) (lemma1 eq) ≈⟨ Equalizer.uniqueness (eqa ( A [ f o π1 ] ) ( A [ g o π2 ] ) {e}) ( begin e o p' ≈⟨⟩ equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p' ≈↑⟨ Product.uniqueness prod ⟩ (prod × ( π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p') ) ( π2 o (equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) o p')) ≈⟨ ×-cong prod (assoc) (assoc) ⟩ (prod × (A [ A [ π1 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ])) (A [ A [ π2 o equalizer (eqa (A [ f o π1 ]) (A [ g o π2 ])) ] o p' ]) ≈⟨ ×-cong prod eq1 eq2 ⟩ ((prod × π1') π2') ∎ ) ⟩ p' ∎ ------ -- -- Limit -- ----- -- Constancy Functor K : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) → ( a : Obj A ) → Functor I A K I a = record { FObj = λ i → a ; FMap = λ f → id1 A a ; isFunctor = let open ≈-Reasoning (A) in record { ≈-cong = λ f=g → refl-hom ; identity = refl-hom ; distr = sym idL } } open NTrans record Limit { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) ( a0 : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) : Set (suc (c₁' ⊔ c₂' ⊔ ℓ' ⊔ c₁ ⊔ c₂ ⊔ ℓ )) where field limit : ( a : Obj A ) → ( t : NTrans I A ( K I a ) Γ ) → Hom A a a0 t0f=t : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → ∀ { i : Obj I } → A [ A [ TMap t0 i o limit a t ] ≈ TMap t i ] limit-uniqueness : { a : Obj A } → { t : NTrans I A ( K I a ) Γ } → { f : Hom A a a0 } → ∀ ( i : Obj I ) → A [ A [ TMap t0 i o f ] ≈ TMap t i ] → A [ limit a t ≈ f ] -------------------------------- -- -- If we have two limits on c and c', there are isomorphic pair h, h' open Limit iso-l : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ ) ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) → Hom A a0 a0' iso-l I Γ a0 a0' t0 t0' lim lim' = limit lim' a0 t0 iso-r : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ ) ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) → Hom A a0' a0 iso-r I Γ a0 a0' t0 t0' lim lim' = limit lim a0' t0' iso-lr : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) ( a0 a0' : Obj A ) ( t0 : NTrans I A ( K I a0 ) Γ ) ( t0' : NTrans I A ( K I a0' ) Γ ) ( lim : Limit I Γ a0 t0 ) → ( lim' : Limit I Γ a0' t0' ) → ∀{ i : Obj I } → A [ A [ iso-l I Γ a0 a0' t0 t0' lim lim' o iso-r I Γ a0 a0' t0 t0' lim lim' ] ≈ id1 A a0' ] iso-lr I Γ a0 a0' t0 t0' lim lim' {i} = let open ≈-Reasoning (A) in begin limit lim' a0 t0 o limit lim a0' t0' ≈↑⟨ limit-uniqueness lim' i ( begin TMap t0' i o ( limit lim' a0 t0 o limit lim a0' t0' ) ≈⟨ assoc ⟩ ( TMap t0' i o limit lim' a0 t0 ) o limit lim a0' t0' ≈⟨ car ( t0f=t lim' ) ⟩ TMap t0 i o limit lim a0' t0' ≈⟨ t0f=t lim ⟩ TMap t0' i ∎ ) ⟩ limit lim' a0' t0' ≈⟨ limit-uniqueness lim' i idR ⟩ id a0' ∎ open import CatExponetial I A KI : { c₁' c₂' ℓ' : Level} ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I A ) → ( a : Obj A ) → Functor I A KI I Γ a = record { FObj = λ i → a ; FMap = λ f → id1 A a ; isFunctor = let open ≈-Reasoning (A) in record { ≈-cong = λ f=g → refl-hom ; identity = refl-hom ; distr = sym idL } }