Mercurial > hg > Members > kono > Proof > category
changeset 253:24e83b8b81be
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 11 Sep 2013 20:26:48 +0900 |
| parents | e0835b8dd51b |
| children | 45b81fcb8a64 |
| files | HomReasoning.agda cat-utility.agda equalizer.agda kleisli.agda yoneda.agda |
| diffstat | 5 files changed, 87 insertions(+), 68 deletions(-) [+] |
line wrap: on
line diff
--- a/HomReasoning.agda Mon Sep 09 16:15:09 2013 +0900 +++ b/HomReasoning.agda Wed Sep 11 20:26:48 2013 +0900 @@ -159,3 +159,19 @@ ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ g ∎ + +Lemma62 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → + { a b : Obj A } → + ( f g : Hom A a b ) + → A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ A [ (Id {_} {_} {_} {A} b) o g ] ] + → A [ g ≈ f ] +Lemma62 A {a} {b} f g 1g=1f = let open ≈-Reasoning A in + begin + g + ≈↑⟨ idL ⟩ + id b o g + ≈↑⟨ 1g=1f ⟩ + id b o f + ≈⟨ idL ⟩ + f + ∎
--- a/cat-utility.agda Mon Sep 09 16:15:09 2013 +0900 +++ b/cat-utility.agda Wed Sep 11 20:26:48 2013 +0900 @@ -11,6 +11,7 @@ id1 : ∀{c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (a : Obj A ) → Hom A a a id1 A a = (Id {_} {_} {_} {A} a) + -- We cannot make A implicit record IsUniversalMapping {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A )
--- a/equalizer.agda Mon Sep 09 16:15:09 2013 +0900 +++ b/equalizer.agda Wed Sep 11 20:26:48 2013 +0900 @@ -30,6 +30,7 @@ equalizer : Hom A c a equalizer = e + -- -- Burroni's Flat Equational Definition of Equalizer -- @@ -116,7 +117,7 @@ ≈⟨ cdr assoc ⟩ e o (( h-1 o h) o k eqa j eq ) ≈⟨ cdr (car h-1h=1 ) ⟩ - e o (id1 A c o k eqa j eq ) + e o (id c o k eqa j eq ) ≈⟨ cdr idL ⟩ e o k eqa j eq ≈⟨ ek=h eqa ⟩ @@ -139,7 +140,7 @@ ≈⟨ assoc ⟩ (h o h-1 ) o j ≈⟨ car hh-1=1 ⟩ - id1 A c' o j + id c' o j ≈⟨ idL ⟩ j ∎ @@ -194,23 +195,23 @@ e'←e {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa = let open ≈-Reasoning (A) in begin e o c-iso-r eqa eqa' keqa ≈⟨⟩ - e o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) + e o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ≈↑⟨ car (ek=h eqa' ) ⟩ - ( equalizer eqa' o k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) + ( equalizer eqa' o k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ≈⟨⟩ - ( e' o k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) + ( e' o k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ≈↑⟨ assoc ⟩ - e' o (( k eqa' e (fe=ge eqa) ) o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) ) + e' o (( k eqa' e (fe=ge eqa) ) o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ) ≈⟨⟩ - e' o (equalizer keqa o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) ) + e' o (equalizer keqa o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ) ≈⟨ cdr ( ek=h keqa ) ⟩ - e' o id1 A c' + e' o id c' ≈⟨ idR ⟩ e' ∎ --- e←e' e'←e = e --- e'←e e←e = e' is enough for isomorphism but we want to prove l o r = id also. +-- e←e' e'←e e = e +-- e'←e e←e e' = e' is enough for isomorphism but we can prove l o r = id also. c-iso→ : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) → ( keqa : Equalizer A (k eqa' e (fe=ge eqa)) (A [ f o e' ]) (A [ g o e' ]) ) @@ -218,9 +219,9 @@ c-iso→ {c} {c'} {a} {b} {f} {g} eqa eqa' keqa = let open ≈-Reasoning (A) in begin c-iso-l eqa eqa' keqa o c-iso-r eqa eqa' keqa ≈⟨⟩ - equalizer keqa o k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) + equalizer keqa o k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) ≈⟨ ek=h keqa ⟩ - id1 A c' + id c' ∎ c-iso← : { c c' a b : Obj A } {f g : Hom A a b } → {e : Hom A c a } {e' : Hom A c' a} ( eqa : Equalizer A e f g) → ( eqa' : Equalizer A e' f g ) @@ -230,26 +231,26 @@ c-iso← {c} {c'} {a} {b} {f} {g} {e} {e'} eqa eqa' keqa keqa' = let open ≈-Reasoning (A) in begin c-iso-r eqa eqa' keqa o c-iso-l eqa eqa' keqa ≈⟨⟩ - k keqa (id1 A c') ( f1=g1 (fe=ge eqa') (id1 A c') ) o k eqa' e (fe=ge eqa ) + k keqa (id c') ( f1=g1 (fe=ge eqa') (id c') ) o k eqa' e (fe=ge eqa ) ≈⟨⟩ equalizer keqa' o k eqa' e (fe=ge eqa ) ≈⟨ cdr ( begin k eqa' e (fe=ge eqa ) ≈⟨ uniqueness eqa' ( begin - e' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)) + e' o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c)) ≈↑⟨ car (e'←e eqa eqa' keqa ) ⟩ - ( e o equalizer keqa' ) o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c)) + ( e o equalizer keqa' ) o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c)) ≈↑⟨ assoc ⟩ - e o ( equalizer keqa' o k keqa' (id1 A c) (f1=g1 (fe=ge eqa) (id1 A c))) + e o ( equalizer keqa' o k keqa' (id c) (f1=g1 (fe=ge eqa) (id c))) ≈⟨ cdr ( ek=h keqa' ) ⟩ - e o id1 A c + e o id c ≈⟨ idR ⟩ e ∎ )⟩ - k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) ) + k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) ∎ )⟩ - equalizer keqa' o k keqa' (id1 A c) ( f1=g1 (fe=ge eqa) (id1 A c) ) ≈⟨ ek=h keqa' ⟩ - id1 A c + equalizer keqa' o k keqa' (id c) ( f1=g1 (fe=ge eqa) (id c) ) ≈⟨ ek=h keqa' ⟩ + id c ∎ @@ -292,9 +293,9 @@ lemma-b3 : {a b d : Obj A} (f : Hom A a b ) { h : Hom A d a } → A [ A [ equalizer (eqa f f ) o k (eqa f f) (id1 A a) (f1=f1 f) ] ≈ id1 A a ] lemma-b3 {a} {b} {d} f {h} = let open ≈-Reasoning (A) in begin - equalizer (eqa f f) o k (eqa f f) (id1 A a) (f1=f1 f) + equalizer (eqa f f) o k (eqa f f) (id a) (f1=f1 f) ≈⟨ ek=h (eqa f f ) ⟩ - id1 A a + id a ∎ lemma-equ4 : {a b c d : Obj A} → (f : Hom A a b) → (g : Hom A a b ) → (h : Hom A d a ) → A [ A [ f o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ≈ A [ g o A [ h o equalizer (eqa (A [ f o h ]) (A [ g o h ])) ] ] ] @@ -329,13 +330,13 @@ k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') ] cong-δ1 {a} {b} {c} {e} {f} {f'} f=f' = let open ≈-Reasoning (A) in begin - k (eqa {a} {b} {c} f f {e} ) (id1 A a) (f1=f1 f) + k (eqa {a} {b} {c} f f {e} ) (id a) (f1=f1 f) ≈⟨ uniqueness (eqa f f) ( begin - e o k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') + e o k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f') ≈⟨ ek=h (eqa {a} {b} {c} f' f' {e} ) ⟩ - id1 A a + id a ∎ )⟩ - k (eqa {a} {b} {c} f' f' {e} ) (id1 A a) (f1=f1 f') + k (eqa {a} {b} {c} f' f' {e} ) (id a) (f1=f1 f') ∎ lemma-b2 : {d : Obj A} {h : Hom A d a} → A [ @@ -362,19 +363,19 @@ ≈⟨ car ((uniqueness (eqa f g) ( begin equalizer (eqa f g) o j ≈↑⟨ idR ⟩ - (equalizer (eqa f g) o j ) o id1 A d - ≈⟨⟩ -- here we decide e (fej) (gej)' is id1 A d + (equalizer (eqa f g) o j ) o id d + ≈⟨⟩ -- here we decide e (fej) (gej)' is id d ((equalizer (eqa f g) o j) o equalizer (eqa (f o equalizer (eqa f g {e}) o j) (g o equalizer (eqa f g {e}) o j))) ∎ ))) ⟩ j o k (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) (id1 A d) (f1=f1 (( f o ( equalizer (eqa f g) o j ) ))) ≈⟨ cdr ((uniqueness (eqa (( f o ( equalizer (eqa f g) o j ) )) (( f o ( equalizer (eqa f g) o j ) ))) ( begin - equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j)) o id1 A d + equalizer (eqa (f o equalizer (eqa f g {e} ) o j) (f o equalizer (eqa f g {e}) o j)) o id d ≈⟨ idR ⟩ equalizer (eqa (f o equalizer (eqa f g {e}) o j) (f o equalizer (eqa f g {e}) o j)) - ≈⟨⟩ -- here we decide e (fej) (fej)' is id1 A d - id1 A d + ≈⟨⟩ -- here we decide e (fej) (fej)' is id d + id d ∎ ))) ⟩ - j o id1 A d + j o id d ≈⟨ idR ⟩ j ∎ @@ -401,17 +402,17 @@ begin α bur f g e o k1 h eq ≈⟨⟩ - α bur f g e o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id1 A d) (f o h) ) + α bur f g e o ( γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h) ) ≈⟨ assoc ⟩ - ( α bur f g e o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} (id1 A d) (f o h) + ( α bur f g e o γ bur {a} {b} {c} f g h ) o δ bur {d} {b} {d} (id d) (f o h) ≈⟨ car (b2 bur) ⟩ - ( h o ( α bur ( f o h ) ( g o h ) (id1 A d))) o δ bur {d} {b} {d} (id1 A d) (f o h) + ( h o ( α bur ( f o h ) ( g o h ) (id d))) o δ bur {d} {b} {d} (id d) (f o h) ≈↑⟨ assoc ⟩ - h o ((( α bur ( f o h ) ( g o h ) (id1 A d) )) o δ bur {d} {b} {d} (id1 A d) (f o h) ) + h o ((( α bur ( f o h ) ( g o h ) (id d) )) o δ bur {d} {b} {d} (id d) (f o h) ) ≈↑⟨ cdr ( car ( cong-α bur eq)) ⟩ - h o ((( α bur ( f o h ) ( f o h ) (id1 A d)))o δ bur {d} {b} {d} (id1 A d) (f o h) ) - ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id1 A d} ) ⟩ - h o id1 A d + h o ((( α bur ( f o h ) ( f o h ) (id d)))o δ bur {d} {b} {d} (id d) (f o h) ) + ≈⟨ cdr (b3 bur {d} {b} {d} (f o h) {id d} ) ⟩ + h o id d ≈⟨ idR ⟩ h ∎ @@ -421,11 +422,11 @@ begin k1 {d} h eq ≈⟨⟩ - γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id1 A d) (f o h) + γ bur {a} {b} {c} f g h o δ bur {d} {b} {d} (id d) (f o h) ≈↑⟨ car (cong-γ bur {a} {b} {c} {d} ek=h ) ⟩ - γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id1 A d) (f o h) + γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) (f o h) ≈↑⟨ cdr (cong-δ bur (resp ek=h refl-hom )) ⟩ - γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id1 A d) ( f o ( α bur f g e o k') ) + γ bur f g (A [ α bur f g e o k' ]) o δ bur {d} {b} {d} (id d) ( f o ( α bur f g e o k') ) ≈⟨ b4 bur ⟩ k' ∎
--- a/kleisli.agda Mon Sep 09 16:15:09 2013 +0900 +++ b/kleisli.agda Wed Sep 11 20:26:48 2013 +0900 @@ -146,7 +146,7 @@ ( ( TMap μ d o FMap T h ) o ( (TMap μ c o FMap T g ) o f ) ) ≈⟨ assoc ⟩ ( ( ( TMap μ d o FMap T h ) o (TMap μ c o FMap T g ) ) o f ) - ≈⟨ car (sym assoc) ⟩ + ≈↑⟨ car assoc ⟩ ( ( TMap μ d o ( FMap T h o ( TMap μ c o FMap T g ) ) ) o f ) ≈⟨ car ( cdr (assoc) ) ⟩ ( ( TMap μ d o ( ( FMap T h o TMap μ c ) o FMap T g ) ) o f ) @@ -159,11 +159,11 @@ ∎ ))) ⟩ ( ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) ) o FMap T g ) o f ) - ≈⟨ car (sym assoc) ⟩ + ≈↑⟨ car assoc ⟩ ( ( TMap μ d o ( ( TMap μ ( FObj T d) o FMap T ( FMap T h ) ) o FMap T g ) ) o f ) - ≈⟨ car ( cdr (sym assoc) ) ⟩ + ≈↑⟨ car ( cdr assoc ) ⟩ ( ( TMap μ d o ( TMap μ ( FObj T d) o ( FMap T ( FMap T h ) o FMap T g ) ) ) o f ) - ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩ + ≈↑⟨ car ( cdr (cdr (distr T ))) ⟩ ( ( TMap μ d o ( TMap μ ( FObj T d) o FMap T ( ( FMap T h o g ) ) ) ) o f ) ≈⟨ car assoc ⟩ ( ( ( TMap μ d o TMap μ ( FObj T d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) @@ -175,11 +175,11 @@ ∎ )) ⟩ ( ( ( TMap μ d o FMap T ( TMap μ d) ) o FMap T ( ( FMap T h o g ) ) ) o f ) - ≈⟨ car (sym assoc) ⟩ + ≈↑⟨ car assoc ⟩ ( ( TMap μ d o ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) ) o f ) - ≈⟨ sym assoc ⟩ + ≈↑⟨ assoc ⟩ ( TMap μ d o ( ( FMap T ( TMap μ d ) o FMap T ( ( FMap T h o g ) ) ) o f ) ) - ≈⟨ cdr ( car ( sym ( distr T ))) ⟩ + ≈↑⟨ cdr ( car ( distr T )) ⟩ ( TMap μ d o ( FMap T ( ( ( TMap μ d ) o ( FMap T h o g ) ) ) o f ) ) ≈⟨ refl-hom ⟩ join M ( ( TMap μ d o ( FMap T h o g ) ) ) f @@ -289,7 +289,7 @@ begin TMap μ (a) o FMap T (TMap η a) ≈⟨ IsMonad.unity2 (isMonad M) ⟩ - id1 A (FObj T a) + id (FObj T a) ∎ ≈-cong : {a b : Obj A} {f g : KHom a b} → A [ KMap f ≈ KMap g ] → A [ ufmap f ≈ ufmap g ] ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in @@ -361,7 +361,7 @@ ≈⟨ car (sym (nat η)) ⟩ (FMap T g o TMap η (b)) o f ≈⟨ sym idL ⟩ - id1 A (FObj T c) o ((FMap T g o TMap η (b)) o f) + id (FObj T c) o ((FMap T g o TMap η (b)) o f) ≈⟨ sym (car (IsMonad.unity2 (isMonad M))) ⟩ (TMap μ c o FMap T (TMap η c)) o ((FMap T g o TMap η (b)) o f) ≈⟨ sym assoc ⟩ @@ -405,7 +405,7 @@ ≈⟨ assoc ⟩ (TMap μ (b) o FMap T (TMap η (b))) o FMap T f ≈⟨ car (IsMonad.unity2 (isMonad M)) ⟩ - id1 A (FObj T b) o FMap T f + id (FObj T b) o FMap T f ≈⟨ idL ⟩ FMap T f ∎ ) @@ -445,7 +445,7 @@ sym ( begin KMap (( tmap-ε b ) * ( FMap (F_T ○ U_T) f )) ≈⟨⟩ - TMap μ b o ( FMap T ( id1 A (FObj T b) ) o ( KMap (FMap (F_T ○ U_T) f ) )) + TMap μ b o ( FMap T ( id (FObj T b) ) o ( KMap (FMap (F_T ○ U_T) f ) )) ≈⟨ cdr ( cdr ( begin KMap (FMap (F_T ○ U_T) f ) @@ -455,19 +455,19 @@ TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)) ∎ )) ⟩ - TMap μ b o ( FMap T ( id1 A (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) + TMap μ b o ( FMap T ( id (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) ≈⟨ cdr (car (IsFunctor.identity (isFunctor T))) ⟩ - TMap μ b o ( id1 A (FObj T (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) + TMap μ b o ( id (FObj T (FObj T b) ) o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f)))) ≈⟨ cdr idL ⟩ TMap μ b o (TMap η (FObj T b) o (TMap μ (b) o FMap T (KMap f))) ≈⟨ assoc ⟩ (TMap μ b o (TMap η (FObj T b))) o (TMap μ (b) o FMap T (KMap f)) ≈⟨ (car (IsMonad.unity1 (isMonad M))) ⟩ - id1 A (FObj T b) o (TMap μ (b) o FMap T (KMap f)) + id (FObj T b) o (TMap μ (b) o FMap T (KMap f)) ≈⟨ idL ⟩ TMap μ b o FMap T (KMap f) ≈⟨ cdr (sym idR) ⟩ - TMap μ b o ( FMap T (KMap f) o id1 A (FObj T a) ) + TMap μ b o ( FMap T (KMap f) o id (FObj T a) ) ≈⟨⟩ KMap (f * ( tmap-ε a )) ∎ ) @@ -516,9 +516,9 @@ sym ( begin FMap U_T ( TMap nat-ε ( FObj F_T x ) ) ≈⟨⟩ - TMap μ x o FMap T (id1 A (FObj T x) ) + TMap μ x o FMap T (id (FObj T x) ) ≈⟨ cdr (IsFunctor.identity (isFunctor T)) ⟩ - TMap μ x o id1 A (FObj T (FObj T x) ) + TMap μ x o id (FObj T (FObj T x) ) ≈⟨ idR ⟩ TMap μ x ∎ ) @@ -536,13 +536,13 @@ begin ( FMap U_T ( TMap nat-ε b)) o ( TMap nat-η ( FObj U_T b )) ≈⟨⟩ - (TMap μ (b) o FMap T (id1 A (FObj T b ))) o ( TMap η ( FObj T b )) + (TMap μ (b) o FMap T (id (FObj T b ))) o ( TMap η ( FObj T b )) ≈⟨ car ( cdr (IsFunctor.identity (isFunctor T))) ⟩ - (TMap μ (b) o (id1 A (FObj T (FObj T b )))) o ( TMap η ( FObj T b )) + (TMap μ (b) o (id (FObj T (FObj T b )))) o ( TMap η ( FObj T b )) ≈⟨ car idR ⟩ TMap μ (b) o ( TMap η ( FObj T b )) ≈⟨ IsMonad.unity1 (isMonad M) ⟩ - id1 A (FObj U_T b) + id (FObj U_T b) ∎ adjoint2 : {a : Obj A} → KleisliCategory [ KleisliCategory [ ( TMap nat-ε ( FObj F_T a )) o ( FMap F_T ( TMap nat-η a )) ] @@ -551,15 +551,15 @@ begin KMap (( TMap nat-ε ( FObj F_T a )) * ( FMap F_T ( TMap nat-η a )) ) ≈⟨⟩ - TMap μ a o (FMap T (id1 A (FObj T a) ) o ((TMap η (FObj T a)) o (TMap η a))) + TMap μ a o (FMap T (id (FObj T a) ) o ((TMap η (FObj T a)) o (TMap η a))) ≈⟨ cdr ( car ( IsFunctor.identity (isFunctor T))) ⟩ - TMap μ a o ((id1 A (FObj T (FObj T a) )) o ((TMap η (FObj T a)) o (TMap η a))) + TMap μ a o ((id (FObj T (FObj T a) )) o ((TMap η (FObj T a)) o (TMap η a))) ≈⟨ cdr ( idL ) ⟩ TMap μ a o ((TMap η (FObj T a)) o (TMap η a)) ≈⟨ assoc ⟩ (TMap μ a o (TMap η (FObj T a))) o (TMap η a) ≈⟨ car (IsMonad.unity1 (isMonad M)) ⟩ - id1 A (FObj T a) o (TMap η a) + id (FObj T a) o (TMap η a) ≈⟨ idL ⟩ TMap η a ≈⟨⟩
--- a/yoneda.agda Mon Sep 09 16:15:09 2013 +0900 +++ b/yoneda.agda Wed Sep 11 20:26:48 2013 +0900 @@ -305,13 +305,14 @@ -- YondaLemma2 : {a b x : Obj A } → (FObj (FObj YonedaFunctor a) x) ≡ (FObj (FObj YonedaFunctor b ) x) → -- a ≡ b -- YondaLemma2 {a} {b} eq = {!!} +-- N.B = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b -- --- Instead we prove +-- Instead we prove only -- inv ( FObj YonedaFunctor a ) ≡ a inv : {a x : Obj A} ( f : FObj (FObj YonedaFunctor a) x) → Obj A inv {a} f = Category.cod A f -YonedaLemma21 : (a x : Obj A) { f : ( FObj (FObj YonedaFunctor a) x) } → inv f ≡ a -YonedaLemma21 a x {f} = refl +YonedaLemma21 : {a x : Obj A} ( f : ( FObj (FObj YonedaFunctor a) x) ) → inv f ≡ a +YonedaLemma21 {a} {x} f = refl