fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Universally quantify test object in epi- mono- morphism

Browse source 
Closes #26
This commit is contained in:
Frederik Hanghøj Iversen 2018-07-17 17:02:39 +02:00
parent 188bba6c8d
commit 9ee05e1a36
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Cat/Category.agda
View file

@ -84,11 +84,11 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
_≊_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f) _≊_ A B = Σ[ f ∈ Arrow A B ] (Isomorphism f)
module _ {A B : Object} where module _ {A B : Object} where
Epimorphism : {X : Object } → (f : Arrow A B) → Set ℓb Epimorphism : (f : Arrow A B) → Set _
Epimorphism {X} f = (g₀ g₁ : Arrow B X) → g₀ <<< f ≡ g₁ <<< f → g₀ ≡ g₁ Epimorphism f = ∀ {X} → (g₀ g₁ : Arrow B X) → g₀ <<< f ≡ g₁ <<< f → g₀ ≡ g₁
Monomorphism : {X : Object} → (f : Arrow A B) → Set ℓb Monomorphism : (f : Arrow A B) → Set _
Monomorphism {X} f = (g₀ g₁ : Arrow X A) → f <<< g₀ ≡ f <<< g₁ → g₀ ≡ g₁ Monomorphism f = ∀ {X} → (g₀ g₁ : Arrow X A) → f <<< g₀ ≡ f <<< g₁ → g₀ ≡ g₁
IsInitial : Object → Set (ℓa ⊔ ℓb) IsInitial : Object → Set (ℓa ⊔ ℓb)
IsInitial I = {X : Object} → isContr (Arrow I X) IsInitial I = {X : Object} → isContr (Arrow I X)
@ -175,7 +175,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
-- | Relation between iso- epi- and mono- morphisms. -- | Relation between iso- epi- and mono- morphisms.
module _ {A B : Object} {X : Object} (f : Arrow A B) where module _ {A B : Object} {X : Object} (f : Arrow A B) where
iso→epi : Isomorphism f → Epimorphism {X = X} f iso→epi : Isomorphism f → Epimorphism f
iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
g₀ ≡⟨ sym rightIdentity ⟩ g₀ ≡⟨ sym rightIdentity ⟩
g₀ <<< identity ≡⟨ cong (_<<<_ g₀) (sym right-inv) ⟩ g₀ <<< identity ≡⟨ cong (_<<<_ g₀) (sym right-inv) ⟩
@ -186,7 +186,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
g₁ <<< identity ≡⟨ rightIdentity ⟩ g₁ <<< identity ≡⟨ rightIdentity ⟩
g₁ ∎ g₁ ∎
iso→mono : Isomorphism f → Monomorphism {X = X} f iso→mono : Isomorphism f → Monomorphism f
iso→mono (f- , left-inv , right-inv) g₀ g₁ eq = iso→mono (f- , left-inv , right-inv) g₀ g₁ eq =
begin begin
g₀ ≡⟨ sym leftIdentity ⟩ g₀ ≡⟨ sym leftIdentity ⟩
@ -198,7 +198,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
identity <<< g₁ ≡⟨ leftIdentity ⟩ identity <<< g₁ ≡⟨ leftIdentity ⟩
g₁ ∎ g₁ ∎
iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f iso→epi×mono : Isomorphism f → Epimorphism f × Monomorphism f
iso→epi×mono iso = iso→epi iso , iso→mono iso iso→epi×mono iso = iso→epi iso , iso→mono iso
propIsAssociative : isProp IsAssociative propIsAssociative : isProp IsAssociative