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

Rename distrib to isDistributive

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-23 12:53:35 +01:00
parent 7787a8f0be
commit 4874ed0795
4 changed files with 17 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Cat/Categories/Cat.agda
View file

@ -107,13 +107,13 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
proj₁ : Catt [ :product: , ℂ ] proj₁ : Catt [ :product: , ℂ ]
proj₁ = record proj₁ = record
{ raw = record { func* = fst ; func→ = fst } { raw = record { func* = fst ; func→ = fst }
; isFunctor = record { isIdentity = refl ; distrib = refl } ; isFunctor = record { isIdentity = refl ; isDistributive = refl }
} }
proj₂ : Catt [ :product: , 𝔻 ] proj₂ : Catt [ :product: , 𝔻 ]
proj₂ = record proj₂ = record
{ raw = record { func* = snd ; func→ = snd } { raw = record { func* = snd ; func→ = snd }
; isFunctor = record { isIdentity = refl ; distrib = refl } ; isFunctor = record { isIdentity = refl ; isDistributive = refl }
} }
module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where module _ {X : Object Catt} (x₁ : Catt [ X , ℂ ]) (x₂ : Catt [ X , 𝔻 ]) where
@ -125,7 +125,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where
} }
; isFunctor = record ; isFunctor = record
{ isIdentity = Σ≡ x₁.isIdentity x₂.isIdentity { isIdentity = Σ≡ x₁.isIdentity x₂.isIdentity
; distrib = Σ≡ x₁.distrib x₂.distrib ; isDistributive = Σ≡ x₁.isDistributive x₂.isDistributive
} }
} }
where where
@ -279,14 +279,14 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
ηθ = proj₁ ηθNT ηθ = proj₁ ηθNT
ηθNat = proj₂ ηθNT ηθNat = proj₂ ηθNT
:distrib: : :isDistributive: :
𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ] 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ]
≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ]
:distrib: = begin :isDistributive: = begin
𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ] 𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ]
≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩
𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩ ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩
𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ]
≡⟨ sym isAssociative ⟩ ≡⟨ sym isAssociative ⟩
𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ]
@ -314,7 +314,7 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where
} }
; isFunctor = record ; isFunctor = record
{ isIdentity = λ {o} → :ident: {o} { isIdentity = λ {o} → :ident: {o}
; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y} ; isDistributive = λ {f u n k y} → :isDistributive: {f} {u} {n} {k} {y}
} }
} }

4
src/Cat/Categories/Sets.agda
View file

@ -99,7 +99,7 @@ module _ {ℓa ℓb : Level} where
} }
; isFunctor = record ; isFunctor = record
{ isIdentity = funExt λ _ → proj₂ isIdentity { isIdentity = funExt λ _ → proj₂ isIdentity
; distrib = funExt λ x → sym isAssociative ; isDistributive = funExt λ x → sym isAssociative
} }
} }
where where
@ -114,7 +114,7 @@ module _ {ℓa ℓb : Level} where
} }
; isFunctor = record ; isFunctor = record
{ isIdentity = funExt λ x → proj₁ isIdentity { isIdentity = funExt λ x → proj₁ isIdentity
; distrib = funExt λ x → isAssociative ; isDistributive = funExt λ x → isAssociative
} }
} }
where where

14
src/Cat/Category/Functor.agda
View file

@ -33,8 +33,8 @@ module _ {ℓc ℓc' ℓd ℓd'}
record IsFunctor (F : RawFunctor) : 𝓤 where record IsFunctor (F : RawFunctor) : 𝓤 where
open RawFunctor F public open RawFunctor F public
field field
isIdentity : IsIdentity isIdentity : IsIdentity
distrib : IsDistributive isDistributive : IsDistributive
record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
field field
@ -56,7 +56,7 @@ module _
propIsFunctor : isProp (IsFunctor _ _ F) propIsFunctor : isProp (IsFunctor _ _ F)
propIsFunctor isF0 isF1 i = record propIsFunctor isF0 isF1 i = record
{ isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i { isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i
; distrib = 𝔻.arrowsAreSets _ _ isF0.distrib isF1.distrib i ; isDistributive = 𝔻.arrowsAreSets _ _ isF0.isDistributive isF1.isDistributive i
} }
where where
module isF0 = IsFunctor isF0 module isF0 = IsFunctor isF0
@ -106,8 +106,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ]
dist = begin dist = begin
(F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡⟨ refl ⟩ (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡⟨ refl ⟩
F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (distrib G) ⟩ F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (isDistributive G) ⟩
F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ distrib F ⟩ F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ isDistributive F ⟩
C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎
_∘fr_ : RawFunctor A C _∘fr_ : RawFunctor A C
@ -121,7 +121,7 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)⟩ F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)⟩
F→ (𝟙 B) ≡⟨ isIdentity F ⟩ F→ (𝟙 B) ≡⟨ isIdentity F ⟩
𝟙 C ∎ 𝟙 C ∎
; distrib = dist ; isDistributive = dist
} }
_∘f_ : Functor A C _∘f_ : Functor A C
@ -136,6 +136,6 @@ identity = record
} }
; isFunctor = record ; isFunctor = record
{ isIdentity = refl { isIdentity = refl
; distrib = refl ; isDistributive = refl
} }
} }

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

@ -88,6 +88,6 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
} }
; isFunctor = record ; isFunctor = record
{ isIdentity = :ident: { isIdentity = :ident:
; distrib = {!!} ; isDistributive = {!!}
} }
} }