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

Update Fun according to new naming policy

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-21 13:40:24 +01:00
parent 57d7eab4cb
commit 9e96e704e8
2 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/Cat/Categories/Fun.agda
View file

@ -21,7 +21,7 @@ open import Cat.Equality
open Equality.Data.Product open Equality.Data.Product
module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
open Category hiding ( _∘_ ; Arrow ) open Category using (Object ; 𝟙)
open Functor open Functor
module _ (F G : Functor ℂ 𝔻) where module _ (F G : Functor ℂ 𝔻) where
@ -70,7 +70,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
where where
module F = Functor F module F = Functor F
F→ = F.func→ F→ = F.func→
module 𝔻 = IsCategory (isCategory 𝔻) module 𝔻 = Category 𝔻
identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F
identityNat F = identityTrans F , identityNatural F identityNat F = identityTrans F , identityNatural F
@ -95,13 +95,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩ 𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
𝔻 [ H.func→ f ∘ (θ ∘nt η) A ] ∎ 𝔻 [ H.func→ f ∘ (θ ∘nt η) A ] ∎
where where
open IsCategory (isCategory 𝔻) open Category 𝔻
NatComp = _:⊕:_ NatComp = _:⊕:_
private private
module _ {F G : Functor ℂ 𝔻} where module _ {F G : Functor ℂ 𝔻} where
module 𝔻 = IsCategory (isCategory 𝔻) module 𝔻 = Category 𝔻
transformationIsSet : isSet (Transformation F G) transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C) (λ l → q l C) i j transformationIsSet _ _ p q i j C = 𝔻.arrowIsSet _ _ (λ l → p l C) (λ l → q l C) i j
@ -139,7 +139,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
:assoc: = lemSig (naturalIsProp {F = A} {D}) :assoc: = lemSig (naturalIsProp {F = A} {D})
L R (funExt (λ x → assoc)) L R (funExt (λ x → assoc))
where where
open IsCategory (isCategory 𝔻) open Category 𝔻
module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where
private private
@ -181,7 +181,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
} }
Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd') Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
raw Fun = RawFun Category.raw Fun = RawFun
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
open import Cat.Categories.Sets open import Cat.Categories.Sets

1
src/Cat/Category/Properties.agda
View file

@ -14,7 +14,6 @@ open Equality.Data.Product
module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
open Category ℂ open Category ℂ
open IsCategory (isCategory)
iso-is-epi : Isomorphism f → Epimorphism {X = X} f iso-is-epi : Isomorphism f → Epimorphism {X = X} f
iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin