Mercurial > hg > Members > kono > Proof > category
changeset 996:6cd40df80dec
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Mar 2021 11:47:19 +0900 |
| parents | 1d365952dde4 |
| children | d9419216ae0c |
| files | src/yoneda.agda |
| diffstat | 1 files changed, 126 insertions(+), 136 deletions(-) [+] |
line wrap: on
line diff
--- a/src/yoneda.agda Sat Mar 06 23:02:33 2021 +0900 +++ b/src/yoneda.agda Sun Mar 07 11:47:19 2021 +0900 @@ -9,10 +9,10 @@ open import Category -- https://github.com/konn/category-agda open import Level open import Category.Sets -module yoneda { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) where +open import cat-utility +module yoneda { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) (I : Set c₁) ( small : Small A I ) where open import HomReasoning -open import cat-utility open import Relation.Binary.Core open import Relation.Binary open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym ) @@ -23,74 +23,61 @@ -- Obj and Hom of Sets^A^op open Functor - -YObj : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) -YObj = Functor (Category.op A) (Sets {c₂}) -YHom : ( f : YObj ) → (g : YObj ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) -YHom f g = NTrans (Category.op A) (Sets {c₂}) f g +open NTrans -open NTrans -Yid : {a : YObj } → YHom a a -Yid {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where - isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x ) - isNTrans1 {a} = record { commute = refl } +SetsAop : Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) +SetsAop = record { Obj = YObj + ; Hom = YHom + ; _o_ = _+_ + ; _≈_ = _==_ + ; Id = Yid + ; isCategory = record { + isEquivalence = record {refl = refl ; trans = λ {i} {j} {k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1 {_} {_} {i} {j}} + ; identityL = refl + ; identityR = refl + ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} + ; associative = refl + } } where + open ≈-Reasoning (Sets {c₂}) + YObj : Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) + YObj = Functor (Category.op A) (Sets {c₂}) + YHom : ( f : YObj ) → (g : YObj ) → Set (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) + YHom f g = NTrans (Category.op A) (Sets {c₂}) f g -_+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c -_+_ {a} {b} {c} f g = record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; isNTrans = isNTrans1 } where - commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b ) - (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → - Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ - Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] - commute1 a b c f g a₁ b₁ h = let open ≈-Reasoning (Sets {c₂})in begin - Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] - ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩ - Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ] - ≈⟨ car (nat f) ⟩ - Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ] - ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩ - Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ] - ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩ - Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ] - ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩ - Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] - ∎ - isNTrans1 : IsNTrans (Category.op A) (Sets {c₂}) a c (λ x → Sets [ TMap f x o TMap g x ]) - isNTrans1 = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } + Yid : {a : YObj } → YHom a a + Yid {a} = record { TMap = λ a → λ x → x ; isNTrans = isNTrans1 {a} } where + isNTrans1 : {a : YObj } → IsNTrans (Category.op A) (Sets {c₂}) a a (λ a → λ x → x ) + isNTrans1 {a} = record { commute = refl } -_==_ : {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁) -_==_ f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ] - -infix 4 _==_ + _+_ : {a b c : YObj} → YHom b c → YHom a b → YHom a c + _+_ {a} {b} {c} f g = + record { TMap = λ x → Sets [ TMap f x o TMap g x ] ; + isNTrans = record { commute = λ {a₁ b₁ h} → commute1 a b c f g a₁ b₁ h } } where + commute1 : (a b c : YObj ) (f : YHom b c) (g : YHom a b ) + (a₁ b₁ : Obj (Category.op A)) (h : Hom (Category.op A) a₁ b₁) → + Sets [ Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈ + Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ] + commute1 a b c f g a₁ b₁ h = begin + Sets [ FMap c h o Sets [ TMap f a₁ o TMap g a₁ ] ] ≈⟨ assoc {_} {_} {_} {_} {FMap c h } {TMap f a₁} {TMap g a₁} ⟩ + Sets [ Sets [ FMap c h o TMap f a₁ ] o TMap g a₁ ] ≈⟨ car (nat f) ⟩ + Sets [ Sets [ TMap f b₁ o FMap b h ] o TMap g a₁ ] ≈↑⟨ assoc {_} {_} {_} {_} { TMap f b₁} {FMap b h } {TMap g a₁}⟩ + Sets [ TMap f b₁ o Sets [ FMap b h o TMap g a₁ ] ] ≈⟨ cdr {_} {_} {_} {_} {_} { TMap f b₁} (nat g) ⟩ + Sets [ TMap f b₁ o Sets [ TMap g b₁ o FMap a h ] ] ≈↑⟨ assoc {_} {_} {_} {_} {TMap f b₁} {TMap g b₁} { FMap a h} ⟩ + Sets [ Sets [ TMap f b₁ o TMap g b₁ ] o FMap a h ] ∎ -isSetsAop : IsCategory (YObj) (YHom) _==_ _+_ ( Yid ) -isSetsAop = - record { isEquivalence = record {refl = refl ; trans = λ {i j k} → trans1 {_} {_} {i} {j} {k} ; sym = λ {i j} → sym1 {_} {_} {i} {j}} - ; identityL = refl - ; identityR = refl - ; o-resp-≈ = λ{a b c f g h i } → o-resp-≈ {a} {b} {c} {f} {g} {h} {i} - ; associative = refl - } where - open ≈-Reasoning (Sets {c₂}) + _==_ : {a b : YObj} → YHom a b → YHom a b → Set (c₂ ⊔ c₁) + _==_ f g = ∀{x : Obj (Category.op A)} → (Sets {c₂}) [ TMap f x ≈ TMap g x ] + sym1 : {a b : YObj } {i j : YHom a b } → i == j → j == i sym1 {a} {b} {i} {j} eq {x} = sym eq trans1 : {a b : YObj } {i j k : YHom a b} → i == j → j == k → i == k trans1 {a} {b} {i} {j} {k} i=j j=k {x} = trans-hom i=j j=k o-resp-≈ : {A₁ B C : YObj} {f g : YHom A₁ B} {h i : YHom B C} → - f == g → h == i → h + f == i + g + f == g → h == i → (h + f) == (i + g) o-resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i {x} = resp f=g h=i -SetsAop : Category (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (suc ℓ ⊔ (suc (suc c₂) ⊔ suc c₁)) (c₂ ⊔ c₁) -SetsAop = - record { Obj = YObj - ; Hom = YHom - ; _o_ = _+_ - ; _≈_ = _==_ - ; Id = Yid - ; isCategory = isSetsAop - } - -- A is Locally small -postulate ≈-≡ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y +postulate ≈-≡ : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y import Axiom.Extensionality.Propositional -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x ) @@ -115,23 +102,17 @@ } } where lemma-y-obj1 : {b : Obj A } → (x : Hom A b a) → (Category.op A) [ id1 A b o x ] ≡ x - lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} idL + lemma-y-obj1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ A idL lemma-y-obj2 : (a₁ b c : Obj A) (f : Hom A b a₁) (g : Hom A c b ) → (x : Hom A a₁ a )→ Category.op A [ Category.op A [ g o f ] o x ] ≡ (Sets [ _[_o_] (Category.op A) g o _[_o_] (Category.op A) f ]) x - lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin - Category.op A [ Category.op A [ g o f ] o x ] - ≈↑⟨ assoc ⟩ - Category.op A [ g o Category.op A [ f o x ] ] - ≈⟨⟩ - ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) - ∎ ) + lemma-y-obj2 a₁ b c f g x = let open ≈-Reasoning (Category.op A) in ≈-≡ A ( begin + Category.op A [ Category.op A [ g o f ] o x ] ≈↑⟨ assoc ⟩ + Category.op A [ g o Category.op A [ f o x ] ] ≈⟨⟩ + ( λ x → Category.op A [ g o x ] ) ( ( λ x → Category.op A [ f o x ] ) x ) ∎ ) lemma-y-obj3 : {b c : Obj A} {f g : Hom A c b } → (x : Hom A b a ) → A [ f ≈ g ] → Category.op A [ f o x ] ≡ Category.op A [ g o x ] - lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ {_} {_} {_} {A} ( begin - Category.op A [ f o x ] - ≈⟨ resp refl-hom eq ⟩ - Category.op A [ g o x ] - ∎ ) - + lemma-y-obj3 {_} {_} {f} {g} x eq = let open ≈-Reasoning (Category.op A) in ≈-≡ A ( begin + Category.op A [ f o x ] ≈⟨ resp refl-hom eq ⟩ + Category.op A [ g o x ] ∎ ) ---- -- @@ -143,16 +124,14 @@ FObj (y-obj a) x → FObj (y-obj b ) x y-tmap a b f x = λ ( g : Hom A x a ) → A [ f o g ] -- ( h : Hom A x b ) -y-map : {a b : Obj A } → (f : Hom A a b ) → YHom (y-obj a) (y-obj b) +y-map : {a b : Obj A } → (f : Hom A a b ) → NTrans (Category.op A) (Sets {c₂}) (y-obj a) (y-obj b) y-map {a} {b} f = record { TMap = y-tmap a b f ; isNTrans = isNTrans1 {a} {b} f } where lemma-y-obj4 : {a₁ b₁ : Obj (Category.op A)} {g : Hom (Category.op A) a₁ b₁} → {a b : Obj A } → (f : Hom A a b ) → Sets [ Sets [ FMap (y-obj b) g o y-tmap a b f a₁ ] ≈ Sets [ y-tmap a b f b₁ o FMap (y-obj a) g ] ] - lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ {_} {_} {_} {A} ( begin - A [ A [ f o x ] o g ] - ≈↑⟨ assoc ⟩ - A [ f o A [ x o g ] ] - ∎ ) ) + lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f = let open ≈-Reasoning A in extensionality A ( λ x → ≈-≡ A ( begin + A [ A [ f o x ] o g ] ≈↑⟨ assoc ⟩ + A [ f o A [ x o g ] ] ∎ ) ) isNTrans1 : {a b : Obj A } → (f : Hom A a b ) → IsNTrans (Category.op A) (Sets {c₂}) (y-obj a) (y-obj b) (y-tmap a b f ) isNTrans1 {a} {b} f = record { commute = λ{a₁ b₁ g } → lemma-y-obj4 {a₁} {b₁} {g} {a} {b} f } @@ -170,38 +149,53 @@ identity = identity ; distr = distr1 ; ≈-cong = ≈-cong - - } - } where + } } where ≈-cong : {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → SetsAop [ y-map f ≈ y-map g ] ≈-cong {a} {b} {f} {g} eq = let open ≈-Reasoning A in -- (λ x g₁ → A [ f o g₁ ] ) ≡ (λ x g₁ → A [ g o g₁ ] ) - extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin - A [ f o h ] - ≈⟨ resp refl-hom eq ⟩ - A [ g o h ] - ∎ - ) ) + extensionality A ( λ h → ≈-≡ A ( begin + A [ f o h ] ≈⟨ resp refl-hom eq ⟩ + A [ g o h ] ∎ ) ) identity : {a : Obj A} → SetsAop [ y-map (id1 A a) ≈ id1 SetsAop (y-obj a ) ] identity {a} = let open ≈-Reasoning A in -- (λ x g → A [ id1 A a o g ] ) ≡ (λ a₁ x → x) - extensionality A ( λ g → ≈-≡ {_} {_} {_} {A} ( begin - A [ id1 A a o g ] - ≈⟨ idL ⟩ - g - ∎ - ) ) + extensionality A ( λ g → ≈-≡ A ( begin + A [ id1 A a o g ] ≈⟨ idL ⟩ + g ∎ ) ) distr1 : {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → SetsAop [ y-map (A [ g o f ]) ≈ SetsAop [ y-map g o y-map f ] ] distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning A in -- (λ x g₁ → (A [ (A [ g o f] o g₁ ]))) ≡ (λ x x₁ → A [ g o A [ f o x₁ ] ] ) - extensionality A ( λ h → ≈-≡ {_} {_} {_} {A} ( begin - A [ A [ g o f ] o h ] - ≈↑⟨ assoc ⟩ - A [ g o A [ f o h ] ] - ∎ - ) ) - + extensionality A ( λ h → ≈-≡ A ( begin + A [ A [ g o f ] o h ] ≈↑⟨ assoc ⟩ + A [ g o A [ f o h ] ] ∎ ) ) ------ -- --- F : A → Sets ∈ Obj SetsAop +-- Hom(_ , _) : Obj (op A) → Obj A → Sets +-- +-- +------ + +-- module _ where +-- +-- open import Category.Constructions.Product +-- open import Data.Product renaming (_×_ to _*_) +-- +-- HomAAop : Functor ((Category.op A) × A) (Sets {c₂}) +-- HomAAop = record { +-- FObj = λ x → Hom A (proj₁ x) (proj₂ x) +-- -- f : Hom (Category.op A × A) A₁ B +-- -- g : Category.Category.Hom A (proj₁ A₁) (proj₂ A₁) +-- ; FMap = λ f g → A [ A [ proj₂ f o g ] o proj₁ f ] +-- ; isFunctor = record { ≈-cong = λ {a} {b} {f} {g} f=g → extensionality A ( λ h → cong (λ k → A [ A [ proj₂ k o h ] o (proj₁ k) ] ) {!!}) +-- ; distr = {!!} ; identity = {!!} } +-- } where open ≈-Reasoning A + +------ +-- +-- Yoneda Lemma +-- +-- (F : Obj SetsAop) → ( +-- Hom SetsAop (FObj YonedaFunctor a , F ) ≅ FObj F a +-- +-- F : Functor (co A) Sets ∈ Obj SetsAop -- -- F(a) → Nat(h_a,F) -- x ∈ F(a) , (g : Hom A b a) → ( FMap F g ) x @@ -263,24 +257,23 @@ Nat2F→F2Nat : {a : Obj A } → {F : Obj SetsAop } → (ha : Hom SetsAop (y-obj a) F) → SetsAop [ F2Nat {a} {F} (Nat2F {a} {F} ha) ≈ ha ] -Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in - begin - TMap (F2Nat {a} {F} (Nat2F {a} {F} ha)) b - ≡⟨⟩ - (λ g → FMap F g (TMap ha a (Category.Category.Id A))) - ≡⟨ extensionality A (λ g → ( - begin - FMap F g (TMap ha a (Category.Category.Id A)) - ≡⟨ ≡-cong (λ f → f (Category.Category.Id A)) (IsNTrans.commute (isNTrans ha)) ⟩ - TMap ha b (FMap (y-obj a) g (Category.Category.Id A)) - ≡⟨⟩ - TMap ha b ( (A Category.o Category.Category.Id A) g ) - ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ {_} {_} {_} {A} (IsCategory.identityL ( Category.isCategory A ))) ⟩ - TMap ha b g - ∎ - )) ⟩ - TMap ha b - ∎ +Nat2F→F2Nat {a} {F} ha {b} = let open ≡-Reasoning in begin + TMap (F2Nat {a} {F} (Nat2F {a} {F} ha)) b ≡⟨⟩ + (λ g → FMap F g (TMap ha a (id1 A _))) ≡⟨ extensionality A (λ g → ( begin + FMap F g (TMap ha a (id1 A _)) ≡⟨ ≡-cong (λ f → f (id1 A _)) (IsNTrans.commute (isNTrans ha)) ⟩ + TMap ha b (FMap (y-obj a) g (id1 A _)) ≡⟨⟩ + TMap ha b ( A [ id1 A _ o g ] ) ≡⟨ ≡-cong ( TMap ha b ) ( ≈-≡ A (≈-Reasoning.idL A)) ⟩ + TMap ha b g ∎ )) ⟩ + TMap ha b + ∎ + +-- SetAop (Y - , F) ≅ F is set of natural transformation + +Nat2F-ntrans : (a : Obj A) ( F : Obj SetsAop ) → NTrans (Category.op A) Sets (y-obj a) F +Nat2F-ntrans a F = record { TMap = λ b f → TMap (F2Nat {a} {F} (Nat2F {!!}) ) b f ; isNTrans = record { commute = {!!} } } + +F2Nat-ntrans : (a : Obj A) ( F : Obj SetsAop ) → NTrans (Category.op A) Sets F (y-obj a) +F2Nat-ntrans a F = record { TMap = λ b f → TMap (F2Nat {a} {y-obj a} (Nat2F {!!})) b {!!} ; isNTrans = record { commute = {!!} } } -- Yoneda's Lemma -- Yoneda Functor is full and faithfull @@ -311,13 +304,13 @@ -- f ∈ FMap (FObj YonedaFunctor a') a -- --- g f --- b --→ a ------→ a' --- | | --- | | --- ↓ ↓ --- H a ------→ H a' --- H f +-- g f +-- b --→ a ------→ a' +-- | | +-- TMap (H f) b | | TMap (H id) a' +-- o g ↓ ↓ o (f o g) +-- H a ------→ H a' +-- H f -- _^ : {a a' b : Obj A } → (f : Hom A a a' ) → Hom A b a → Hom A b a' _^ {a} {a'} {b} f g = (FMap (FObj YonedaFunctor a') g) f @@ -331,10 +324,16 @@ postulate eqObj0 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A} → Hom A a b ≡ Hom A a' b' → a ≡ a' + eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a a' b b' : Obj A} → Hom A a b ≡ Hom A a' b' → b ≡ b' eqHom0 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → f ≡ f' eqHom1 : {a b c : Obj A } {f f' : Hom A b c } {g g' : Hom A a b } → A [ f o g ] ≡ A [ f' o g' ] → g ≡ g' -- eqTMap : { y b : Obj A} { x z : Obj Sets} → {g h : NTrans (Category.op A) Sets (y-obj b) ? } {w : {!!} } → TMap g x {!!} ≡ TMap h x w → g ≡ h +open import Relation.Binary.HeterogeneousEquality as HE using (_≅_) + +a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B +a1 HE.refl = refl + open import Category.Cat @@ -350,18 +349,11 @@ → [_]_~_ B f g → b ≡ b' ≃→b=b B f g (refl eqv) = refl -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_) - -eqObj1 : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → {a b : Obj A} → Hom A a a ≡ Hom A a b → a ≡ b -eqObj1 A {a} {b} eq = lem (subst (λ k → k) eq (id1 A a)) eq where - lem : (f : Hom A a b ) → f ≅ id1 A a → Hom A a a ≡ Hom A a b → a ≡ b - lem _ HE.refl refl = refl - -- full (injective ) Yoneda-injective : {a b : Obj A } → {x y : Obj SetsAop} → (g h : Hom SetsAop y (FObj YonedaFunctor a)) (f : Hom A a b ) → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ] → SetsAop [ g ≈ h ] -Yoneda-injective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z → ≈-≡ ( begin +Yoneda-injective {a} {b} {x} {y} g h f yg=yh = extensionality A (λ z → ≈-≡ A ( begin TMap g _ z ≈⟨ {!!} ⟩ A [ id1 A _ o TMap g _ z ] ≈⟨ {!!} ⟩ ( Sets [ id1 Sets _ o TMap g _ ] ) z ≈⟨ {!!} ⟩ @@ -398,8 +390,6 @@ -- -- But we cannot prove like this -- FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b -a1 : { c₁ : Level} {A B : Set c₁ } {a : A } { b : B } → a ≅ b → A ≡ B -a1 HE.refl = refl open import Relation.Nullary