# HG changeset patch # User Shinji KONO # Date 1555470225 -32400 # Node ID bded2347efa46ae86a98d351877f01f704c7118b # Parent db59b8f954aa0df36c3dd09904f713c9333824f4 CCC by equation diff -r db59b8f954aa -r bded2347efa4 CCC.agda --- a/CCC.agda Fri Mar 08 18:09:11 2019 +0900 +++ b/CCC.agda Wed Apr 17 12:03:45 2019 +0900 @@ -4,8 +4,8 @@ open import HomReasoning open import cat-utility -open import Data.Product renaming (_×_ to _∧_) -open import Category.Constructions.Product +-- open import Data.Product renaming (_×_ to _∧_) +-- open import Category.Constructions.Product open import Relation.Binary.PropositionalEquality open Functor @@ -14,14 +14,6 @@ -- ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b ) -- ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c -record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) - : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where - field - ≅→ : Hom A a b → Hom B a' b' - ≅← : Hom B a' b' → Hom A a b - iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] - iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] - data One {c : Level} : Set c where OneObj : One -- () in Haskell ( or any one object set ) @@ -44,14 +36,22 @@ lemma {a} {b} {f} with f ... | OneObj = refl +record IsoS {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') (a b : Obj A) ( a' b' : Obj B ) + : Set ( c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' ) where + field + ≅→ : Hom A a b → Hom B a' b' + ≅← : Hom B a' b' → Hom A a b + iso→ : {f : Hom B a' b' } → B [ ≅→ ( ≅← f) ≈ f ] + iso← : {f : Hom A a b } → A [ ≅← ( ≅→ f) ≈ f ] -record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A) + +record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (１ : Obj A) ( _×_ : {a b c : Obj A ) → Hom A c a → Hom A c b → Hom A (a * b) ) ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where field - ccc-1 : {a : Obj A} → -- Hom A a one ≅ {*} - IsoS A OneCat a one OneObj OneObj + ccc-1 : {a : Obj A} → -- Hom A a １ ≅ {*} + IsoS A OneCat a １ OneObj OneObj ccc-2 : {a b c : Obj A} → -- Hom A c ( a * b ) ≅ ( Hom A c a ) * ( Hom A c b ) - IsoS A (A × A) c (a * b) (c , c) (a , b) + IsoS A A c (a * b) {!!} {!!} ccc-3 : {a b c : Obj A} → -- Hom A a ( c ^ b ) ≅ Hom A ( a * b ) c IsoS A A a (c ^ b) (a * b) c @@ -61,11 +61,77 @@ one : Obj A _*_ : Obj A → Obj A → Obj A _^_ : Obj A → Obj A → Obj A - isCCC : IsCCC A one _*_ _^_ + _×_ : Obj A → Obj A → Obj A + isCCC : IsCCC A one _×_ _*_ _^_ + +open import HomReasoning + +record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( １ : Obj A ) + ( ○ : (a : Obj A ) → Hom A a １ ) + ( _∧_ : Obj A → Obj A → Obj A ) + ( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) ) + ( π : {a b : Obj A } → Hom A (a ∧ b) a ) + ( π' : {a b : Obj A } → Hom A (a ∧ b) b ) + ( _<=_ : (a b : Obj A ) → Obj A ) + ( _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) ) + ( ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a ) + : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where + field + -- cartesian + e2 : {a : Obj A} → ∀ ( f : Hom A a １ ) → A [ f ≈ ○ a ] + e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π o < f , g > ] ≈ f ] + e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } → A [ A [ π' o < f , g > ] ≈ g ] + e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } → A [ < A [ π o h ] , A [ π' o h ] > ≈ h ] + π-congl : {a b c : Obj A} → { f f' : Hom A c a }{ g : Hom A c b } → A [ f ≈ f' ] → A [ < f , g > ≈ < f' , g > ] + π-congr : {a b c : Obj A} → { f : Hom A c a }{ g g' : Hom A c b } → A [ g ≈ g' ] → A [ < f , g > ≈ < f , g' > ] + -- closed + e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } → A [ A [ ε o < A [ (h *) o π ] , π' > ] ≈ h ] + e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } → A [ ( A [ ε o < A [ k o π ] , π' > ] ) * ≈ k ] -record IsEqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (one : Obj A) ( oneT : ( a : Obj A ) → Hom A a one ) - ( _*_ : Obj A → Obj A → Obj A ) ( _^_ : Obj A → Obj A → Obj A ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where + e'2 : A [ ○ １ ≈ id1 A １ ] + e'2 = let open ≈-Reasoning A in begin + ○ １ + ≈↑⟨ e2 (id1 A １ ) ⟩ + id1 A １ + ∎ + e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [ ○ b o f ] ≈ ○ a ] + e''2 {a} {b} {f} = let open ≈-Reasoning A in begin + ○ b o f + ≈⟨ e2 (○ b o f) ⟩ + ○ a + ∎ + distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ] ≈ < A [ f o h ] , A [ g o h ] > ] + distr {a} {b} {c} {d} {f} {g} {h} = let open ≈-Reasoning A in begin + < f , g > o h + ≈↑⟨ e3c ⟩ + < π o < f , g > o h , π' o < f , g > o h > + ≈⟨ π-congl assoc ⟩ + < ( π o < f , g > ) o h , π' o < f , g > o h > + ≈⟨ π-congl (car e3a ) ⟩ + < f o h , π' o < f , g > o h > + ≈⟨ π-congr assoc ⟩ + < f o h , (π' o < f , g > ) o h > + ≈⟨ π-congr (car e3b ) ⟩ + < f o h , g o h > + ∎ + _×_ : { a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e ) + f × g = λ h → < A [ f o A [ π o h ] ] , A [ g o A [ π' o h ] ] > + +record EqCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) : Set ( c₁ ⊔ c₂ ⊔ ℓ ) where field - e2 : {a : Obj A} { f : Hom A a one } → A [ f ≈ oneT a ] - e3a : {!!} + １ : Obj A + ○ : (a : Obj A ) → Hom A a １ + _∧_ : Obj A → Obj A → Obj A + <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b) + π : {a b : Obj A } → Hom A (a ∧ b) a + π' : {a b : Obj A } → Hom A (a ∧ b) b + _<=_ : (a b : Obj A ) → Obj A + _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) + ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a + isEqCCC : IsEqCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε + + + + diff -r db59b8f954aa -r bded2347efa4 applicative.agda --- a/applicative.agda Fri Mar 08 18:09:11 2019 +0900 +++ b/applicative.agda Wed Apr 17 12:03:45 2019 +0900 @@ -9,6 +9,7 @@ open import Relation.Binary.Core open import Relation.Binary open import monoidal +open import Relation.Binary.PropositionalEquality hiding ( [_] ) ----- -- diff -r db59b8f954aa -r bded2347efa4 monad→monoidal.agda --- a/monad→monoidal.agda Fri Mar 08 18:09:11 2019 +0900 +++ b/monad→monoidal.agda Wed Apr 17 12:03:45 2019 +0900 @@ -16,7 +16,7 @@ open import applicative open import Category.Cat open import Category.Sets -import Relation.Binary.PropositionalEquality +open import Relation.Binary.PropositionalEquality hiding ( [_] ) ----- -- diff -r db59b8f954aa -r bded2347efa4 monoid-monad.agda --- a/monoid-monad.agda Fri Mar 08 18:09:11 2019 +0900 +++ b/monoid-monad.agda Wed Apr 17 12:03:45 2019 +0900 @@ -19,16 +19,21 @@ record ≡-Monoid c : Set (suc c) where - infixl 7 _∙_ + infixl 7 _*_ field Carrier : Set c - _∙_ : Op₂ Carrier + _*_ : Op₂ Carrier ε : Carrier -- id in Monoid - isMonoid : IsMonoid _≡_ _∙_ ε + isMonoid : IsMonoid _≡_ _*_ ε postulate M : ≡-Monoid c open ≡-Monoid +infixl 7 _∙_ + +_∙_ : ( m m' : Carrier M ) → Carrier M +_∙_ m m' = _*_ M m m' + A = Sets {c} -- T : A → (M x A) @@ -36,7 +41,7 @@ T : Functor A A T = record { FObj = λ a → (Carrier M) × a - ; FMap = λ f → map ( λ x → x ) f + ; FMap = λ f p → (proj₁ p , f (proj₂ p )) ; isFunctor = record { identity = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets )) ; distr = (IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory Sets ))) @@ -71,7 +76,7 @@ -- μ : (m,(m',a)) → (m*m,a) muMap : (a : Obj A ) → FObj T ( FObj T a ) → Σ (Carrier M) (λ x → a ) -muMap a ( m , ( m' , x ) ) = ( _∙_ M m m' , x ) +muMap a ( m , ( m' , x ) ) = ( m ∙ m' , x ) Lemma-MM2 : {a b : Obj A} {f : Hom A a b} → A [ A [ FMap T f o (λ x → muMap a x) ] ≈ @@ -96,13 +101,13 @@ Lemma-MM33 : {a : Level} {b : Level} {A : Set a} {B : A → Set b} {x : Σ A B } → (((proj₁ x) , proj₂ x ) ≡ x ) Lemma-MM33 = _≡_.refl -Lemma-MM34 : ∀( x : Carrier M ) → ( (M ∙ ε M) x ≡ x ) +Lemma-MM34 : ∀( x : Carrier M ) → ε M ∙ x ≡ x Lemma-MM34 x = (( proj₁ ( IsMonoid.identity ( isMonoid M )) ) x ) -Lemma-MM35 : ∀( x : Carrier M ) → ((M ∙ x) (ε M)) ≡ x +Lemma-MM35 : ∀( x : Carrier M ) → x ∙ ε M ≡ x Lemma-MM35 x = ( proj₂ ( IsMonoid.identity ( isMonoid M )) ) x -Lemma-MM36 : ∀( x y z : Carrier M ) → ((M ∙ (M ∙ x) y) z) ≡ (_∙_ M x (_∙_ M y z ) ) +Lemma-MM36 : ∀( x y z : Carrier M ) → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z ) Lemma-MM36 x y z = ( IsMonoid.assoc ( isMonoid M )) x y z -- Functional Extensionality Axiom (We cannot prove this in Agda / Coq, just assumming ) @@ -115,13 +120,13 @@ (∀ x y z → f x y z ≡ g x y z ) → ( f ≡ g ) extensionality30 eq = extensionality ( λ x → extensionality ( λ y → extensionality (eq x y) ) ) -Lemma-MM9 : ( λ(x : Carrier M) → ( M ∙ ε M ) x ) ≡ ( λ(x : Carrier M) → x ) +Lemma-MM9 : (λ(x : Carrier M) → ( ε M ∙ x )) ≡ ( λ(x : Carrier M) → x ) Lemma-MM9 = extensionality Lemma-MM34 -Lemma-MM10 : ( λ x → ((M ∙ x) (ε M))) ≡ ( λ x → x ) +Lemma-MM10 : ( λ x → (x ∙ ε M)) ≡ ( λ x → x ) Lemma-MM10 = extensionality Lemma-MM35 -Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z)) ≡ (λ x y z → ( _∙_ M x (_∙_ M y z ) )) +Lemma-MM11 : (λ x y z → ((x ∙ y ) ∙ z)) ≡ (λ x y z → ( x ∙ (y ∙ z ) )) Lemma-MM11 = extensionality30 Lemma-MM36 MonoidMonad : Monad A @@ -140,7 +145,7 @@ begin TMap μ a o TMap η ( FObj T a ) ≈⟨⟩ - ( λ x → ((M ∙ ε M) (proj₁ x) , proj₂ x )) + ( λ x → ε M ∙ (proj₁ x) , proj₂ x ) ≈⟨ cong ( λ f → ( λ x → ( ( f (proj₁ x) ) , proj₂ x ))) ( Lemma-MM9 ) ⟩ ( λ (x : FObj T a) → (proj₁ x) , proj₂ x ) ≈⟨⟩ @@ -153,7 +158,7 @@ begin TMap μ a o (FMap T (TMap η a )) ≈⟨⟩ - ( λ x → (M ∙ proj₁ x) (ε M) , proj₂ x ) + ( λ x → ( proj₁ x ∙ (ε M) , proj₂ x )) ≈⟨ cong ( λ f → ( λ x → ( f (proj₁ x) ) , proj₂ x )) ( Lemma-MM10 ) ⟩ ( λ x → (proj₁ x) , proj₂ x ) ≈⟨⟩ @@ -166,11 +171,11 @@ begin TMap μ a o TMap μ ( FObj T a ) ≈⟨⟩ - ( λ x → (M ∙ (M ∙ proj₁ x) (proj₁ (proj₂ x))) (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x))) + ( λ x → (proj₁ x) ∙ (proj₁ (proj₂ x)) ∙ (proj₁ (proj₂ (proj₂ x))) , proj₂ (proj₂ (proj₂ x))) ≈⟨ cong ( λ f → ( λ x → (( f ( proj₁ x ) ((proj₁ (proj₂ x))) ((proj₁ (proj₂ (proj₂ x))) )) , proj₂ (proj₂ (proj₂ x)) ) )) Lemma-MM11 ⟩ - ( λ x → (M ∙ proj₁ x) ((M ∙ proj₁ (proj₂ x)) (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x))) + ( λ x → ( proj₁ x) ∙(( proj₁ (proj₂ x)) ∙ (proj₁ (proj₂ (proj₂ x)))) , proj₂ (proj₂ (proj₂ x))) ≈⟨⟩ TMap μ a o FMap T (TMap μ a) ∎ diff -r db59b8f954aa -r bded2347efa4 system-f.agda --- a/system-f.agda Fri Mar 08 18:09:11 2019 +0900 +++ b/system-f.agda Wed Apr 17 12:03:45 2019 +0900 @@ -12,6 +12,8 @@ T X = λ(x y : X) → x F : {l : Level} (X : Set l) → Bool X + + F X = λ(x y : X) → y D : {l : Level} → {U : Set l} → U → U → Bool U → U @@ -27,7 +29,7 @@ _×_ {l} U V = {X : Set l} → (U → V → X) → X <_,_> : {l : Level} {U V : Set l} → U → V → (U × V) -<_,_> {l} {U} {V} u v = λ X → λ(x : U → V → X) → x u v +<_,_> {l} {U} {V} u v = λ x → x u v π1 : {l : Level} {U V : Set l} → (U × V) → U π1 {l} {U} {V} t = t {U} (λ(x : U) → λ(y : V) → x) @@ -44,8 +46,8 @@ hoge : {l : Level} {U V : Set l} → U → V → (U × V) hoge u v = < u , v > --- lemma08 : {l : Level} {U V : Set l } → {u : U } → (t : U × V) → < π1 t , π2 t > ≡ t --- lemma08 t = refl +--lemma08 : {l : Level} {X U V : Set l } → {x : X } → {u : U } → (t : U × V) → < π1 t , π2 t > x ≡ t x +--lemma08 t = refl -- Emp definision is still wrong... @@ -62,8 +64,8 @@ Emp : {l : Level } → Set (suc l) Emp {l} = {X : Set l} → X --- ε : {l : Level} {U : Set l} → Emp {l} → U --- ε {l} {U} t = t U +ε : {l : Level} {U : Set l} → Emp {l} → U +ε {l} {U} t = t {U} -- lemma103 : {l : Level} {U V : Set l} → (u : U) → (t : Emp {l} ) → (ε {l} {U → V} t) u ≡ ε {l} {V} t -- lemma103 u t = refl @@ -88,10 +90,10 @@ _+_ {l} U V = {X : Set l} → ( U → X ) → (V → X) → X ι1 : {l : Level } {U V : Set l} → U → U + V -ι1 {l} {U} {V} u = λ{X} → λ(x : U → X) → λ(y : V → X ) → x u +ι1 {l} {U} {V} u = λ x y → x u -- λ{X} → λ(x : U → X) → λ(y : V → X ) → x u ι2 : {l : Level } {U V : Set l} → V → U + V -ι2 {l} {U} {V} v = λ{X} → λ(x : U → X) → λ(y : V → X ) → y v +ι2 {l} {U} {V} v = λ x y → y v --λ{X} → λ(x : U → X) → λ(y : V → X ) → y v δ : {l : Level} { U V R S : Set l } → (R → U) → (S → U) → ( R + S ) → U δ {l} {U} {V} {R} {S} u v t = t {U} (λ(x : R) → u x) ( λ(y : S) → v y) @@ -107,7 +109,7 @@ _××_ {l} U V = {X : Set l} → (U → V → X) → X <<_,_>> : {l : Level} {U : Set (suc l) } {V : Set l} → U → V → (U ×× V) -<<_,_>> {l} {U} {V} u v = λ{X} → λ(x : U → V → X) → x u v +<<_,_>> {l} {U} {V} u v = λ x → x u v -- λ{X} → λ(x : U → V → X) → x u v Int : {l : Level } ( X : Set l ) → Set l @@ -143,6 +145,9 @@ ItInt : {l : Level} {X : Set l} → Int X → (X → Int X ) → ( Int X → Int X ) → Int X → Int X ItInt {l} {X} u g f t = λ z s → t (u z s) ( λ (w : X) → (f (g w)) z s ) +copy_int : {l l' : Level } { X X' : Set l } → Int (X → (X → X) → X) → Int X +copy_int {_} {_} {X} {X'} x = It Zero S x + R : {l : Level} { U X : Set l} → U → ( U → Int X → U ) → Int _ → U R {l} {U} {X} u v t = π1 ( It {suc l} {U × Int X} (< u , Zero >) (λ (x : U × Int X) → < v (π1 x) (π2 x) , S (π2 x) > ) t ) @@ -159,6 +164,20 @@ lemma22 : {l : Level} {X : Set l} ( x y : Int X ) → add x y ≡ add'' x y lemma22 x y = refl +lemma21 : {l : Level} {X : Set l} ( x y : Int X ) → add x Zero ≡ x +lemma21 x y = refl + +postulate extensionality : {l : Level } → Relation.Binary.PropositionalEquality.Extensionality l l + +--lemma23 : {l : Level} {X : Set l} ( x y : Int X ) → add x (S y) ≡ S ( add x y ) +--lemma23 x y = extensionality ( λ z → {!!} ) +-- where +-- lemma24 : {!!} +-- lemma24 = {!!} + +-- lemma23 : {l : Level} {X : Set l} ( x y : Int X ) → add x y ≡ add y x +-- lemma23 x y = {!!} + -- bad adder which modifies input type mul' : {l : Level } {X : Set l} → Int X → Int (Int X) → Int X mul' {l} {X} x y = It Zero (add x) y @@ -183,7 +202,7 @@ -- lemma14 : {l : Level} {X : Set l} → (x y : Int X) → mul x y ≡ mul y x --- lemma14 x y = It {!!} {!!} {!!} +-- lemma14 x y = {!!} -- It {!!} {!!} {!!} lemma15 : {l : Level} {X : Set l} (x y : Int X) → mul {l} {X} n2 n3 ≡ mul {l} {X} n3 n2 lemma15 x y = refl diff -r db59b8f954aa -r bded2347efa4 yoneda.agda --- a/yoneda.agda Fri Mar 08 18:09:11 2019 +0900 +++ b/yoneda.agda Wed Apr 17 12:03:45 2019 +0900 @@ -165,7 +165,7 @@ ----- YonedaFunctor : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Functor A (SetsAop A) -YonedaFunctor {_} {c₂} {_} A = record { +YonedaFunctor A = record { FObj = λ a → y-obj A a ; FMap = λ f → y-map A f ; isFunctor = record { @@ -299,10 +299,25 @@ -- -- But we cannot prove like this -- FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b --- YondaLemma2 : {a b x : Obj A } → (FObj (FObj YonedaFunctor a) x) ≡ (FObj (FObj YonedaFunctor b ) x) → --- a ≡ b --- YondaLemma2 {a} {b} eq = {!!} + +open import Relation.Nullary +open import Data.Empty + +--YondaLemma2 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → +-- (a b x : Obj A ) → (FObj (FObj (YonedaFunctor A) a) x) ≡ (FObj (FObj (YonedaFunctor A) b ) x) → a ≡ b +--YondaLemma2 A a bx eq = {!!} + -- N.B = ≡-cong gives you ! a ≡ b, so we cannot cong inv to prove a ≡ b + +--record Category c₁ c₂ ℓ : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where +-- infixr 9 _o_ +-- infix 4 _≈_ +-- field +-- Obj : Set c₁ +-- Hom : Obj → Obj → Set c₂ +--YondaLemma31 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → +-- (a b x : Obj A ) → Hom A a x ≡ Hom A b x → a ≡ b +--YondaLemma31 A a b x eq = {!!} -- -- Instead we prove only -- inv ( FObj YonedaFunctor a ) ≡ a @@ -314,11 +329,19 @@ YonedaLemma21 A {a} {x} f = refl open import Relation.Binary.HeterogeneousEquality --- a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B a1 refl = refl --- --- YonedaInjective : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b x : Obj A} --- → FObj (FObj (YonedaFunctor A ) a ) x ≡ FObj (FObj (YonedaFunctor A ) b ) x --- → a ≡ b --- YonedaInjective A eq = ≡-cong ( λ y → inv A y ) eq + +-- YondaLemma3 : {c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → +-- (a b x : Obj A ) → Hom A a x ≅ Hom A b x → a ≡ b +-- YondaLemma3 A a b x eq = {!!} -- ≡-cong (inv A) ? + +a2 : ( a b : Set ) (f : a → a ) (g : b → a ) -> f ≅ g → a ≡ b +a2 a b f g eq = {!!} + +-- YonedaInjective : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A} +-- → FObj (FObj (YonedaFunctor A ) a ) a ≅ FObj (FObj (YonedaFunctor A ) a ) b +-- → a ≡ b +-- YonedaInjective A {a} {b} eq = {!!} + +