From de1d19c442581fe60ef833c371f515431af664e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Feb 2018 11:23:21 +0100 Subject: [PATCH] Readd stuff about the yoneda embedding --- src/Cat/Category/Properties.agda | 34 +++++++------------------------- 1 file changed, 7 insertions(+), 27 deletions(-) diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index a1860dc..f8b60f8 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -72,33 +72,13 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat [ (λ _ x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) ] eqTrans = funExt λ x → funExt λ x → ℂ.ident .proj₂ - eqNat : (λ i → Natural (prshf c) (prshf c) (eqTrans i)) - [(λ _ → funExt (λ _ → ℂ.assoc)) ≡ identityNatural (prshf c)] - eqNat = λ i {A} {B} f → - let - open Category 𝓢 - lemm : (𝓢 [ eqTrans i B ∘ func→ (prshf c) f ]) ≡ - (𝓢 [ func→ (prshf c) f ∘ eqTrans i A ]) - lemm = {!!} - lem : (λ _ → 𝓢 [ Functor.func* (prshf c) A , func* (prshf c) B ]) - [ 𝓢 [ eqTrans i B ∘ func→ (prshf c) f ] - ≡ 𝓢 [ func→ (prshf c) f ∘ eqTrans i A ] ] - lem - = arrowIsSet _ _ lemm _ i - -- (Sets [ eqTrans i B ∘ prshf c .func→ f ]) - -- (Sets [ prshf c .func→ f ∘ eqTrans i A ]) - -- lemm - -- _ i - in - lem - -- eqNat = λ {A} {B} i ℂ[B,A] i' ℂ[A,c] → - -- let - -- k : ℂ [ {!!} , {!!} ] - -- k = ℂ[A,c] - -- in {!ℂ [ ? ∘ ? ]!} - - :ident: : (:func→: (ℂ.𝟙 {c})) ≡ (Category.𝟙 Fun {A = prshf c}) - :ident: = Σ≡ eqTrans eqNat + 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₂ ℂ.ident yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢}) yoneda = record