Clean-up yoneda embedding
This commit is contained in:
parent
1bf565b87a
commit
7fbca1aeeb
|
@ -5,23 +5,18 @@ module Cat.Category.Yoneda where
|
|||
open import Agda.Primitive
|
||||
open import Data.Product
|
||||
open import Cubical
|
||||
open import Cubical.NType.Properties
|
||||
|
||||
open import Cat.Category
|
||||
open import Cat.Category.Functor
|
||||
open import Cat.Equality
|
||||
open Equality.Data.Product
|
||||
|
||||
-- TODO: We want to avoid defining the yoneda embedding going through the
|
||||
-- category of categories (since it doesn't exist).
|
||||
open import Cat.Categories.Cat using (RawCat)
|
||||
open import Cat.Categories.Fun
|
||||
open import Cat.Categories.Sets
|
||||
open import Cat.Categories.Cat
|
||||
|
||||
module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
|
||||
private
|
||||
open import Cat.Categories.Fun
|
||||
open import Cat.Categories.Sets
|
||||
module Cat = Cat.Categories.Cat
|
||||
open import Cat.Category.Exponential
|
||||
open Functor
|
||||
𝓢 = Sets ℓ
|
||||
open Fun (opposite ℂ) 𝓢
|
||||
prshf = presheaf ℂ
|
||||
|
@ -34,33 +29,31 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
|
|||
--
|
||||
-- In stead we'll use an ad-hoc definition -- which is definitionally
|
||||
-- equivalent to that other one.
|
||||
_⇑_ = Cat.CatExponential.prodObj
|
||||
_⇑_ = CatExponential.prodObj
|
||||
|
||||
module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where
|
||||
:func→: : NaturalTransformation (prshf A) (prshf B)
|
||||
:func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ _ → ℂ.isAssociative
|
||||
|
||||
module _ {c : Category.Object ℂ} where
|
||||
eqTrans : (λ _ → Transformation (prshf c) (prshf c))
|
||||
[ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ]
|
||||
eqTrans = funExt λ x → funExt λ x → ℂ.isIdentity .proj₂
|
||||
rawYoneda : RawFunctor ℂ Fun
|
||||
RawFunctor.func* rawYoneda = prshf
|
||||
RawFunctor.func→ rawYoneda = :func→:
|
||||
open RawFunctor rawYoneda
|
||||
|
||||
open import Cubical.NType.Properties
|
||||
open import Cat.Categories.Fun
|
||||
:ident: : :func→: (ℂ.𝟙 {c}) ≡ Category.𝟙 Fun {A = prshf c}
|
||||
:ident: = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
|
||||
where
|
||||
eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
|
||||
eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
|
||||
isIdentity : IsIdentity
|
||||
isIdentity {c} = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
|
||||
where
|
||||
eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c)
|
||||
eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity
|
||||
|
||||
isDistributive : IsDistributive
|
||||
isDistributive = {!!}
|
||||
|
||||
instance
|
||||
isFunctor : IsFunctor ℂ Fun rawYoneda
|
||||
IsFunctor.isIdentity isFunctor = isIdentity
|
||||
IsFunctor.isDistributive isFunctor = isDistributive
|
||||
|
||||
yoneda : Functor ℂ Fun
|
||||
yoneda = record
|
||||
{ raw = record
|
||||
{ func* = prshf
|
||||
; func→ = :func→:
|
||||
}
|
||||
; isFunctor = record
|
||||
{ isIdentity = :ident:
|
||||
; isDistributive = {!!}
|
||||
}
|
||||
}
|
||||
Functor.raw yoneda = rawYoneda
|
||||
Functor.isFunctor yoneda = isFunctor
|
||||
|
|
Loading…
Reference in a new issue