From 793fc305348c9c6efa44fdc0e54c5647f6ad6998 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sun, 21 Jan 2018 15:01:01 +0100 Subject: [PATCH] Move properties of categories to Cat.Category.Properties --- src/Cat/Category.agda | 89 +++++++------------------------- src/Cat/Category/Properties.agda | 45 +++++++++++++++- 2 files changed, 63 insertions(+), 71 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 8ccad7e..91e25f3 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -53,68 +53,26 @@ record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where open Category -module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Object } where - private - open module ℂ = Category ℂ - _+_ = ℂ._⊕_ +module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where + module _ { A B : ℂ .Object } where + Isomorphism : (f : ℂ .Arrow A B) → Set ℓ' + Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ ._⊕_ g f ≡ ℂ .𝟙 × ℂ ._⊕_ f g ≡ ℂ .𝟙 - Isomorphism : (f : ℂ.Arrow A B) → Set ℓ' - Isomorphism f = Σ[ g ∈ ℂ.Arrow B A ] g ℂ.⊕ f ≡ ℂ.𝟙 × f + g ≡ ℂ.𝟙 + Epimorphism : {X : ℂ .Object } → (f : ℂ .Arrow A B) → Set ℓ' + Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ ._⊕_ g₀ f ≡ ℂ ._⊕_ g₁ f → g₀ ≡ g₁ - Epimorphism : {X : ℂ.Object } → (f : ℂ.Arrow A B) → Set ℓ' - Epimorphism {X} f = ( g₀ g₁ : ℂ.Arrow B X ) → g₀ + f ≡ g₁ + f → g₀ ≡ g₁ + Monomorphism : {X : ℂ .Object} → (f : ℂ .Arrow A B) → Set ℓ' + Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ ._⊕_ f g₀ ≡ ℂ ._⊕_ f g₁ → g₀ ≡ g₁ - Monomorphism : {X : ℂ.Object} → (f : ℂ.Arrow A B) → Set ℓ' - Monomorphism {X} f = ( g₀ g₁ : ℂ.Arrow X A ) → f + g₀ ≡ f + g₁ → g₀ ≡ g₁ + -- Isomorphism of objects + _≅_ : (A B : Object ℂ) → Set ℓ' + _≅_ A B = Σ[ f ∈ ℂ .Arrow A B ] (Isomorphism f) - iso-is-epi : ∀ {X} (f : ℂ.Arrow A B) → Isomorphism f → Epimorphism {X = X} f - iso-is-epi f (f- , left-inv , right-inv) g₀ g₁ eq = - begin - g₀ ≡⟨ sym (fst ident) ⟩ - g₀ + ℂ.𝟙 ≡⟨ cong (_+_ g₀) (sym right-inv) ⟩ - g₀ + (f + f-) ≡⟨ assoc ⟩ - (g₀ + f) + f- ≡⟨ cong (λ x → x + f-) eq ⟩ - (g₁ + f) + f- ≡⟨ sym assoc ⟩ - g₁ + (f + f-) ≡⟨ cong (_+_ g₁) right-inv ⟩ - g₁ + ℂ.𝟙 ≡⟨ fst ident ⟩ - g₁ ∎ - where - open IsCategory ℂ.isCategory - - iso-is-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Monomorphism {X = X} f - iso-is-mono f (f- , (left-inv , right-inv)) g₀ g₁ eq = - begin - g₀ ≡⟨ sym (snd ident) ⟩ - ℂ.𝟙 + g₀ ≡⟨ cong (λ x → x + g₀) (sym left-inv) ⟩ - (f- + f) + g₀ ≡⟨ sym assoc ⟩ - f- + (f + g₀) ≡⟨ cong (_+_ f-) eq ⟩ - f- + (f + g₁) ≡⟨ assoc ⟩ - (f- + f) + g₁ ≡⟨ cong (λ x → x + g₁) left-inv ⟩ - ℂ.𝟙 + g₁ ≡⟨ snd ident ⟩ - g₁ ∎ - where - open IsCategory ℂ.isCategory - - iso-is-epi-mono : ∀ {X} (f : ℂ.Arrow A B ) → Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f - iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso - -{- -epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f) -epi-mono-is-not-iso f = - let k = f {!!} {!!} {!!} {!!} - in {!!} --} - --- Isomorphism of objects -_≅_ : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) → Set ℓ' -_≅_ {ℂ = ℂ} A B = Σ[ f ∈ ℂ .Arrow A B ] (Isomorphism {ℂ = ℂ} f) - -IsProduct : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ') -IsProduct ℂ {A = A} {B = B} π₁ π₂ - = ∀ {X : ℂ.Object} (x₁ : ℂ.Arrow X A) (x₂ : ℂ.Arrow X B) - → ∃![ x ] (π₁ ℂ.⊕ x ≡ x₁ × π₂ ℂ.⊕ x ≡ x₂) - where - open module ℂ = Category ℂ +module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where + IsProduct : (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ') + IsProduct π₁ π₂ + = ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B) + → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ ._⊕_ π₂ x ≡ x₂) -- Tip from Andrea; Consider this style for efficiency: -- record IsProduct {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'}) @@ -131,19 +89,7 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : ℂ .Object) proj₂ : ℂ .Arrow obj B {{isProduct}} : IsProduct ℂ proj₁ proj₂ --- Two pairs are equal if their components are equal. -eqpair : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} {a a' : A} {b b' : B} - → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b') -eqpair eqa eqb i = eqa i , eqb i - module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where - private - instance - _ : IsCategory (ℂ .Object) (flip (ℂ .Arrow)) (ℂ .𝟙) (flip (ℂ ._⊕_)) - _ = record { assoc = sym assoc ; ident = swap ident } - where - open IsCategory (ℂ .isCategory) - Opposite : Category ℓ ℓ' Opposite = record @@ -151,7 +97,10 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where ; Arrow = flip (ℂ .Arrow) ; 𝟙 = ℂ .𝟙 ; _⊕_ = flip (ℂ ._⊕_) + ; isCategory = record { assoc = sym assoc ; ident = swap ident } } + where + open IsCategory (ℂ .isCategory) -- A consequence of no-eta-equality; `Opposite-is-involution` is no longer -- definitional - i.e.; you must match on the fields: diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index f415fc1..4ff4376 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -2,10 +2,53 @@ module Cat.Category.Properties where +open import Agda.Primitive +open import Data.Product +open import Cubical.PathPrelude + open import Cat.Category open import Cat.Functor open import Cat.Categories.Sets +module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Object } {X : ℂ .Category.Object} (f : ℂ .Category.Arrow A B) where + open Category ℂ + open IsCategory (isCategory) + + iso-is-epi : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f + iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = + begin + g₀ ≡⟨ sym (proj₁ ident) ⟩ + g₀ ⊕ 𝟙 ≡⟨ cong (_⊕_ g₀) (sym right-inv) ⟩ + g₀ ⊕ (f ⊕ f-) ≡⟨ assoc ⟩ + (g₀ ⊕ f) ⊕ f- ≡⟨ cong (λ φ → φ ⊕ f-) eq ⟩ + (g₁ ⊕ f) ⊕ f- ≡⟨ sym assoc ⟩ + g₁ ⊕ (f ⊕ f-) ≡⟨ cong (_⊕_ g₁) right-inv ⟩ + g₁ ⊕ 𝟙 ≡⟨ proj₁ ident ⟩ + g₁ ∎ + + iso-is-mono : Isomorphism {ℂ = ℂ} f → Monomorphism {ℂ = ℂ} {X = X} f + iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq = + begin + g₀ ≡⟨ sym (proj₂ ident) ⟩ + 𝟙 ⊕ g₀ ≡⟨ cong (λ φ → φ ⊕ g₀) (sym left-inv) ⟩ + (f- ⊕ f) ⊕ g₀ ≡⟨ sym assoc ⟩ + f- ⊕ (f ⊕ g₀) ≡⟨ cong (_⊕_ f-) eq ⟩ + f- ⊕ (f ⊕ g₁) ≡⟨ assoc ⟩ + (f- ⊕ f) ⊕ g₁ ≡⟨ cong (λ φ → φ ⊕ g₁) left-inv ⟩ + 𝟙 ⊕ g₁ ≡⟨ proj₂ ident ⟩ + g₁ ∎ + + iso-is-epi-mono : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f × Monomorphism {ℂ = ℂ} {X = X} f + iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso + +{- +epi-mono-is-not-iso : ∀ {ℓ ℓ'} → ¬ ((ℂ : Category {ℓ} {ℓ'}) {A B X : Object ℂ} (f : Arrow ℂ A B ) → Epimorphism {ℂ = ℂ} {X = X} f → Monomorphism {ℂ = ℂ} {X = X} f → Isomorphism {ℂ = ℂ} f) +epi-mono-is-not-iso f = + let k = f {!!} {!!} {!!} {!!} + in {!!} +-} + + module _ {ℓa ℓa' ℓb ℓb'} where Exponential : Category ℓa ℓa' → Category ℓb ℓb' → Category {!!} {!!} Exponential A B = record @@ -13,7 +56,7 @@ module _ {ℓa ℓa' ℓb ℓb'} where ; Arrow = {!!} ; 𝟙 = {!!} ; _⊕_ = {!!} - ; isCategory = ? + ; isCategory = {!!} } _⇑_ = Exponential