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

Formatting in yoneda

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-20 16:43:48 +01:00
parent b6a9befd9c
commit 629115661b
1 changed files with 22 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/Cat/Category/Yoneda.agda
View file

@ -12,51 +12,52 @@ open import Cat.Category.Functor
open import Cat.Equality open import Cat.Equality
open import Cat.Categories.Fun open import Cat.Categories.Fun
open import Cat.Categories.Sets open import Cat.Categories.Sets hiding (presheaf)
open import Cat.Categories.Cat
-- There is no (small) category of categories. So we won't use _⇑_ from
-- `HasExponential`
--
-- open HasExponentials (Cat.hasExponentials ℓ unprovable) using (_⇑_)
--
-- In stead we'll use an ad-hoc definition -- which is definitionally equivalent
-- to that other one - even without mentioning the category of categories.
_⇑_ : {ℓ : Level} → Category ℓ ℓ → Category ℓ ℓ → Category ℓ ℓ
_⇑_ = Fun.Fun
module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
private private
𝓢 = Sets ℓ 𝓢 = Sets ℓ
open Fun (opposite ℂ) 𝓢 open Fun (opposite ℂ) 𝓢
prshf = presheaf ℂ presheaf = Cat.Categories.Sets.presheaf ℂ
module ℂ = Category ℂ module ℂ = Category ℂ
-- There is no (small) category of categories. So we won't use _⇑_ from
-- `HasExponential`
--
-- open HasExponentials (Cat.hasExponentials ℓ unprovable) using (_⇑_)
--
-- In stead we'll use an ad-hoc definition -- which is definitionally
-- equivalent to that other one.
_⇑_ = CatExponential.object
module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
fmap : Transformation (prshf A) (prshf B) fmap : Transformation (presheaf A) (presheaf B)
fmap C x = ℂ [ f ∘ x ] fmap C x = ℂ [ f ∘ x ]
fmapNatural : Natural (prshf A) (prshf B) fmap fmapNatural : Natural (presheaf A) (presheaf B) fmap
fmapNatural g = funExt λ _ → ℂ.isAssociative fmapNatural g = funExt λ _ → ℂ.isAssociative
fmapNT : NaturalTransformation (prshf A) (prshf B) fmapNT : NaturalTransformation (presheaf A) (presheaf B)
fmapNT = fmap , fmapNatural fmapNT = fmap , fmapNatural
rawYoneda : RawFunctor ℂ Fun rawYoneda : RawFunctor ℂ Fun
RawFunctor.omap rawYoneda = prshf RawFunctor.omap rawYoneda = presheaf
RawFunctor.fmap rawYoneda = fmapNT RawFunctor.fmap rawYoneda = fmapNT
open RawFunctor rawYoneda hiding (fmap) open RawFunctor rawYoneda hiding (fmap)
isIdentity : IsIdentity isIdentity : IsIdentity
isIdentity {c} = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq isIdentity {c} = lemSig (naturalIsProp {F = presheaf c} {presheaf c}) _ _ eq
where where
eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (presheaf c)
eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
isDistributive : IsDistributive isDistributive : IsDistributive
isDistributive {A} {B} {C} {f = f} {g} isDistributive {A} {B} {C} {f = f} {g}
= lemSig (propIsNatural (prshf A) (prshf C)) _ _ eq = lemSig (propIsNatural (presheaf A) (presheaf C)) _ _ eq
where where
T[_∘_]' = T[_∘_] {F = prshf A} {prshf B} {prshf C} T[_∘_]' = T[_∘_] {F = presheaf A} {presheaf B} {presheaf C}
eqq : (X : ℂ.Object) → (x : ℂ [ X , A ]) eqq : (X : ℂ.Object) → (x : ℂ [ X , A ])
→ fmap (ℂ [ g ∘ f ]) X x ≡ T[ fmap g ∘ fmap f ]' X x → fmap (ℂ [ g ∘ f ]) X x ≡ T[ fmap g ∘ fmap f ]' X x
eqq X x = begin eqq X x = begin