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

Move propositionality stuff about natural transformations to that module

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-05 15:02:36 +01:00
parent 2b92cee254
commit ddd5f17c05
2 changed files with 25 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -4,47 +4,20 @@ module Cat.Categories.Fun where
open import Agda.Primitive open import Agda.Primitive
open import Data.Product open import Data.Product
open import Data.Nat using (_≤_ ; z≤n ; s≤s)
module Nat = Data.Nat
open import Data.Product
open import Cubical open import Cubical
open import Cubical.Sigma
open import Cubical.NType.Properties open import Cubical.NType.Properties
open import Cat.Category open import Cat.Category
open import Cat.Category.Functor hiding (identity) open import Cat.Category.Functor hiding (identity)
open import Cat.Category.NaturalTransformation open import Cat.Category.NaturalTransformation
open import Cat.Wishlist
open import Cat.Equality
import Cat.Category.NaturalTransformation
open Equality.Data.Product
module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
open Category using (Object ; 𝟙) open Category using (Object ; 𝟙)
module NT = NaturalTransformation ℂ 𝔻 module NT = NaturalTransformation ℂ 𝔻
open NT public open NT public
private private
module 𝔻 = Category 𝔻 module 𝔻 = Category 𝔻
module _ {F G : Functor ℂ 𝔻} where
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l → p l C) (λ l → q l C) i j
naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
naturalIsProp θ θNat θNat' = lem
where
lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i
naturalTransformationIsSets : isSet (NaturalTransformation F G)
naturalTransformationIsSets = sigPresSet transformationIsSet
λ θ → ntypeCommulative
(s≤s {n = Nat.suc Nat.zero} z≤n)
(naturalIsProp θ)
private private
module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B} module _ {A B C D : Functor ℂ 𝔻} {θ' : NaturalTransformation A B}
{η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where {η' : NaturalTransformation B C} {ζ' : NaturalTransformation C D} where
@ -97,7 +70,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
isCategory = record isCategory = record
{ isAssociative = λ {A B C D} → isAssociative {A} {B} {C} {D} { isAssociative = λ {A B C D} → isAssociative {A} {B} {C} {D}
; isIdentity = λ {A B} → isIdentity {A} {B} ; isIdentity = λ {A B} → isIdentity {A} {B}
; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G} ; arrowsAreSets = λ {F} {G} → naturalTransformationIsSet {F} {G}
; univalent = {!!} ; univalent = {!!}
} }

24
src/Cat/Category/NaturalTransformation.agda
View file

@ -21,12 +21,16 @@
module Cat.Category.NaturalTransformation where module Cat.Category.NaturalTransformation where
open import Agda.Primitive open import Agda.Primitive
open import Data.Product open import Data.Product
open import Data.Nat using (_≤_ ; z≤n ; s≤s)
module Nat = Data.Nat
open import Cubical open import Cubical
open import Cubical.Sigma
open import Cubical.NType.Properties open import Cubical.NType.Properties
open import Cat.Category open import Cat.Category
open import Cat.Category.Functor hiding (identity) open import Cat.Category.Functor hiding (identity)
open import Cat.Wishlist
module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level} module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
(ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
@ -96,3 +100,23 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
𝔻 [ H.func→ f ∘ T[ θ ∘ η ] A ] ∎ 𝔻 [ H.func→ f ∘ T[ θ ∘ η ] A ] ∎
where where
open Category 𝔻 open Category 𝔻
module _ {F G : Functor ℂ 𝔻} where
private
open Category using (Object ; 𝟙)
module 𝔻 = Category 𝔻
transformationIsSet : isSet (Transformation F G)
transformationIsSet _ _ p q i j C = 𝔻.arrowsAreSets _ _ (λ l → p l C) (λ l → q l C) i j
naturalIsProp : (θ : Transformation F G) → isProp (Natural F G θ)
naturalIsProp θ θNat θNat' = lem
where
lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ]
lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i
naturalTransformationIsSet : isSet (NaturalTransformation F G)
naturalTransformationIsSet = sigPresSet transformationIsSet
λ θ → ntypeCommulative
(s≤s {n = Nat.suc Nat.zero} z≤n)
(naturalIsProp θ)