Mercurial > hg > Members > kono > Proof > category
changeset 1008:e7b0db851a70
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 11 Mar 2021 12:47:19 +0900 |
| parents | 62c8d989cacb |
| children | a611f59932ef |
| files | src/SetsCompleteness.agda src/stdalone-kleisli.agda src/yoneda.agda |
| diffstat | 3 files changed, 85 insertions(+), 96 deletions(-) [+] |
line wrap: on
line diff
--- a/src/SetsCompleteness.agda Wed Mar 10 09:51:46 2021 +0900 +++ b/src/SetsCompleteness.agda Thu Mar 11 12:47:19 2021 +0900 @@ -202,11 +202,10 @@ open import Relation.Binary.PropositionalEquality open ≡-Reasoning -record cequ {c : Level} (A B : Set c) ( f g : A → B ) : Set c where +record cequ {c : Level} (A B : Set c) : Set c where field - sel : B - modh : (x : A ) → f x ≡ sel - modg : (x : A ) → g x ≡ sel + rev : (A → B) → B → A + surjective : (x : B ) → (g : A → B) → g (rev g x) ≡ x -- λ f₁ x y → (λ x₁ → x (f₁ x₁)) ≡ (λ x₁ → y (f₁ x₁)) → x ≡ y -- λ x y → (λ x₁ → x x₁ ≡ y x₁) → x ≡ y @@ -216,34 +215,41 @@ -- → (x : b ) → ((y : a) → f y ≡ x ) → ( (y : a) → g y ≡ x ) → cequ a b f g -- equc {_} {a} {b} f g x fyx gyx = record { sel = x ; modh = fyx ; modg = gyx } --- SetsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) --- → IsCoEqualizer Sets (λ x → ((y : a) → f y ≡ x ) → ( (y : a) → g y ≡ x ) → cequ a b f g) f g --- SetsIsCoEqualizer {c₂} a b f g = record { --- ef=eg = extensionality Sets (λ x → {!!} ) --- ; k = {!!} --- ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq} --- ; uniqueness = {!!} --- } where --- epi : { c₂ : Level } {a b c : Obj (Sets { c₂})} (f : Hom Sets a b ) → (x y : Hom Sets b c) → Set c₂ --- epi f x y = Sets [ Sets [ x o f ] ≈ Sets [ y o f ] ] → Sets [ x ≈ y ] --- c : Set c₂ --- c = (cequ a b f g ) --- k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets c d --- k {d} h hf=hg = {!!} where --- ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a -- (λ x → h (f x)) ≡ (λ x → h (g x)) --- ca eq = {!!} --- cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d --- cd = {!!} --- ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] } --- → Sets [ Sets [ k h eq o {!!} ] ≈ h ] --- ke=h {d} {h} {eq} = extensionality Sets ( λ x → begin --- k h eq ( {!!}) ≡⟨ {!!} ⟩ --- h (f {!!}) ≡⟨ {!!} ⟩ --- h (g {!!}) ≡⟨ {!!} ⟩ --- h x --- ∎ ) where --- open import Relation.Binary.PropositionalEquality --- open ≡-Reasoning +etsIsCoEqualizer : { c₂ : Level} → (a b : Obj (Sets {c₂}) ) (f g : Hom (Sets {c₂}) a b) + → IsCoEqualizer Sets (λ x → Sets [ cequ.rev x g o ? ] ) f g +etsIsCoEqualizer {c₂} a b f g = record { + ef=eg = extensionality Sets (λ x → {!!} ) + ; k = {!!} + ; ke=h = λ {d} {h} {eq} → ke=h {d} {h} {eq} + ; uniqueness = {!!} + } where + c : Set c₂ + c = cequ a b + d : cequ a b + d = {!!} + ef=eg : (x : a ) → (Sets [ cequ.rev d f o f ]) x ≡ (Sets [ cequ.rev d g o g ]) x + ef=eg x = begin + cequ.rev d f (f x) ≡⟨ ≡-sym (cequ.surjective d x (id1 Sets a)) ⟩ + x ≡⟨ cequ.surjective d x (id1 Sets b) ⟩ + cequ.rev d g (g x) ∎ where open ≡-Reasoning + epi : { c₂ : Level } {a b c : Obj (Sets { c₂})} (e : Hom Sets b c ) → (f g : Hom Sets a b) → Set c₂ + epi e f g = Sets [ Sets [ e o f ] ≈ Sets [ e o g ] ] → Sets [ f ≈ g ] + k : {d : Obj Sets} (h : Hom Sets b d) → Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → Hom Sets c d + k {d} h hf=hg = {!!} where + ca : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] → a -- (λ x → h (f x)) ≡ (λ x → h (g x)) + ca eq = {!!} + cd : ( {y : a} → f y ≡ g y → sequ a b f g ) → d + cd = {!!} + ke=h : {d : Obj Sets } {h : Hom Sets b d } → { eq : Sets [ Sets [ h o f ] ≈ Sets [ h o g ] ] } + → Sets [ Sets [ k h eq o {!!} ] ≈ h ] + ke=h {d} {h} {eq} = extensionality Sets ( λ x → begin + k h eq ( {!!}) ≡⟨ {!!} ⟩ + h (f {!!}) ≡⟨ {!!} ⟩ + h (g {!!}) ≡⟨ {!!} ⟩ + h x + ∎ ) where + open import Relation.Binary.PropositionalEquality + open ≡-Reasoning open Functor
--- a/src/stdalone-kleisli.agda Wed Mar 10 09:51:46 2021 +0900 +++ b/src/stdalone-kleisli.agda Thu Mar 11 12:47:19 2021 +0900 @@ -197,17 +197,18 @@ ; assoc = assoc } } where + open Monad M KleisliHom : (a b : Obj C) → Set l KleisliHom a b = Hom C a ( FObj T b ) join : { a b c : Obj C } → KleisliHom b c → KleisliHom a b → KleisliHom a c join {a} {b} {c} f g = C [ TMap (Monad.μ M) c o C [ FMap T ( f ) o g ] ] - idL : {a b : Obj C} {f : KleisliHom a b} → join (TMap (Monad.η M) b ) f ≡ f + idL : {a b : Obj C} {f : KleisliHom a b} → join (TMap η b ) f ≡ f idL {a} {b} {f} = let open ≡-Reasoning in begin - C [ TMap (Monad.μ M) b o C [ FMap T (TMap (Monad.η M) b) o f ] ] + C [ TMap μ b o C [ FMap T (TMap η b) o f ] ] ≡⟨ ( begin - C [ TMap (Monad.μ M) b o C [ FMap T (TMap (Monad.η M) b) o f ] ] + C [ TMap μ b o C [ FMap T (TMap η b) o f ] ] ≡⟨ IsCategory.assoc ( isCategory C ) ⟩ - C [ C [ TMap (Monad.μ M) b o FMap T (TMap (Monad.η M) b) ] o f ] + C [ C [ TMap μ b o FMap T (TMap η b) ] o f ] ≡⟨ cong ( λ z → C [ z o f ] ) ( IsMonad.unity2 (Monad.isMonad M ) ) ⟩ C [ id C (FObj T b) o f ] ≡⟨ IsCategory.idL ( isCategory C ) ⟩ @@ -215,15 +216,15 @@ ∎ ) ⟩ f ∎ - idR : {a b : Obj C} {f : KleisliHom a b} → join f ( TMap (Monad.η M) a ) ≡ f + idR : {a b : Obj C} {f : KleisliHom a b} → join f ( TMap η a ) ≡ f idR {a} {b} {f} = let open ≡-Reasoning in begin - C [ TMap (Monad.μ M) b o C [ FMap T (f) o TMap (Monad.η M) a ] ] + C [ TMap μ b o C [ FMap T f o TMap η a ] ] ≡⟨ ( begin - C [ TMap (Monad.μ M) b o C [ FMap T (f) o TMap (Monad.η M) a ] ] - ≡⟨ cong ( λ z → C [ TMap (Monad.μ M) b o z ] ) ( IsNTrans.commute (isNTrans (Monad.η M) )) ⟩ - C [ TMap (Monad.μ M) b o C [ TMap (Monad.η M) (FObj T b) o f ] ] + C [ TMap μ b o C [ FMap T f o TMap η a ] ] + ≡⟨ cong ( λ z → C [ TMap μ b o z ] ) ( IsNTrans.commute (isNTrans η )) ⟩ + C [ TMap μ b o C [ TMap η (FObj T b) o f ] ] ≡⟨ IsCategory.assoc ( isCategory C ) ⟩ - C [ C [ TMap (Monad.μ M) b o TMap (Monad.η M) (FObj T b) ] o f ] + C [ C [ TMap μ b o TMap η (FObj T b) ] o f ] ≡⟨ cong ( λ z → C [ z o f ] ) ( IsMonad.unity1 (Monad.isMonad M ) ) ⟩ C [ id C (FObj T b) o f ] ≡⟨ IsCategory.idL ( isCategory C ) ⟩ @@ -232,7 +233,7 @@ f ∎ -- --- TMap (Monad.μ M) d ・ ( FMap T (f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (g) ・ h ) ) ) ) +-- TMap μ d ・ ( FMap T f ・ ( TMap μ c ・ ( FMap T g ・ h ) ) ) ) -- -- h T g μ c -- a -→ T b -----→ T T c ---------------→ T c @@ -250,7 +251,7 @@ -- +--------→ T T d ----------------→ T d -- T (μ d・T f・g) μ d -- --- TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (f) ・ g ) ) ) ・ h ) ) +-- TMap μ d ・ ( FMap T (( TMap μ d ・ ( FMap T f ・ g ) ) ) ・ h ) ) -- _・_ : {a b c : Obj C } ( f : Hom C b c ) ( g : Hom C a b ) → Hom C a c f ・ g = C [ f o g ] @@ -258,41 +259,41 @@ assoc {a} {b} {c} {d} {f} {g} {h} = let open ≡-Reasoning in begin join f (join g h) ≡⟨⟩ - TMap (Monad.μ M) d ・ ( FMap T (f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (g) ・ h ))) + TMap μ d ・ ( FMap T f ・ ( TMap μ c ・ ( FMap T g ・ h ))) ≡⟨ ( begin - ( TMap (Monad.μ M) d ・ ( FMap T (f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (g) ・ h ) ) ) ) + ( TMap μ d ・ ( FMap T f ・ ( TMap μ c ・ ( FMap T g ・ h ) ) ) ) ≡⟨ Right C ( Right C (Assoc C)) ⟩ - ( TMap (Monad.μ M) d ・ ( FMap T (f) ・ ( ( TMap (Monad.μ M) c ・ FMap T (g) ) ・ h ) ) ) + ( TMap μ d ・ ( FMap T f ・ ( ( TMap μ c ・ FMap T g ) ・ h ) ) ) ≡⟨ Assoc C ⟩ - ( ( TMap (Monad.μ M) d ・ FMap T (f) ) ・ ( ( TMap (Monad.μ M) c ・ FMap T (g) ) ・ h ) ) + ( ( TMap μ d ・ FMap T f ) ・ ( ( TMap μ c ・ FMap T g ) ・ h ) ) ≡⟨ Assoc C ⟩ - ( ( ( TMap (Monad.μ M) d ・ FMap T (f) ) ・ ( TMap (Monad.μ M) c ・ FMap T (g) ) ) ・ h ) + ( ( ( TMap μ d ・ FMap T f ) ・ ( TMap μ c ・ FMap T g ) ) ・ h ) ≡⟨ sym ( Left C (Assoc C )) ⟩ - ( ( TMap (Monad.μ M) d ・ ( FMap T (f) ・ ( TMap (Monad.μ M) c ・ FMap T (g) ) ) ) ・ h ) + ( ( TMap μ d ・ ( FMap T f ・ ( TMap μ c ・ FMap T g ) ) ) ・ h ) ≡⟨ Left C ( Right C (Assoc C)) ⟩ - ( ( TMap (Monad.μ M) d ・ ( ( FMap T (f) ・ TMap (Monad.μ M) c ) ・ FMap T (g) ) ) ・ h ) + ( ( TMap μ d ・ ( ( FMap T f ・ TMap μ c ) ・ FMap T g ) ) ・ h ) ≡⟨ Left C (Assoc C)⟩ - ( ( ( TMap (Monad.μ M) d ・ ( FMap T (f) ・ TMap (Monad.μ M) c ) ) ・ FMap T (g) ) ・ h ) - ≡⟨ Left C ( Left C ( Right C ( IsNTrans.commute (isNTrans (Monad.μ M) ) ) )) ⟩ - ( ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (f) ) ) ・ FMap T (g) ) ・ h ) + ( ( ( TMap μ d ・ ( FMap T f ・ TMap μ c ) ) ・ FMap T g ) ・ h ) + ≡⟨ Left C ( Left C ( Right C ( IsNTrans.commute (isNTrans μ ) ) )) ⟩ + ( ( ( TMap μ d ・ ( TMap μ (FObj T d) ・ FMap (T ● T) f ) ) ・ FMap T g ) ・ h ) ≡⟨ sym ( Left C (Assoc C)) ⟩ - ( ( TMap (Monad.μ M) d ・ ( ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (f) ) ・ FMap T (g) ) ) ・ h ) + ( ( TMap μ d ・ ( ( TMap μ (FObj T d) ・ FMap (T ● T) f ) ・ FMap T g ) ) ・ h ) ≡⟨ sym ( Left C ( Right C (Assoc C))) ⟩ - ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ ( FMap (T ● T) (f) ・ FMap T (g) ) ) ) ・ h ) + ( ( TMap μ d ・ ( TMap μ (FObj T d) ・ ( FMap (T ● T) f ・ FMap T g ) ) ) ・ h ) ≡⟨ sym ( Left C ( Right C (Right C (IsFunctor.distr (isFunctor T ) ) ) )) ⟩ - ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap T (( FMap T (f) ・ g )) ) ) ・ h ) + ( ( TMap μ d ・ ( TMap μ (FObj T d) ・ FMap T (( FMap T f ・ g )) ) ) ・ h ) ≡⟨ Left C (Assoc C) ⟩ - ( ( ( TMap (Monad.μ M) d ・ TMap (Monad.μ M) (FObj T d) ) ・ FMap T (( FMap T (f) ・ g )) ) ・ h ) + ( ( ( TMap μ d ・ TMap μ (FObj T d) ) ・ FMap T (( FMap T f ・ g )) ) ・ h ) ≡⟨ Left C (Left C ( IsMonad.assoc (Monad.isMonad M ) ) ) ⟩ - ( ( ( TMap (Monad.μ M) d ・ FMap T (TMap (Monad.μ M) d) ) ・ FMap T (( FMap T (f) ・ g )) ) ・ h ) + ( ( ( TMap μ d ・ FMap T (TMap μ d) ) ・ FMap T (( FMap T f ・ g )) ) ・ h ) ≡⟨ sym ( Left C (Assoc C)) ⟩ - ( ( TMap (Monad.μ M) d ・ ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (f) ・ g )) ) ) ・ h ) + ( ( TMap μ d ・ ( FMap T (TMap μ d) ・ FMap T (( FMap T f ・ g )) ) ) ・ h ) ≡⟨ sym (Assoc C) ⟩ - ( TMap (Monad.μ M) d ・ ( ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (f) ・ g )) ) ・ h ) ) + ( TMap μ d ・ ( ( FMap T (TMap μ d) ・ FMap T (( FMap T f ・ g )) ) ・ h ) ) ≡⟨ sym (Right C ( Left C (IsFunctor.distr (isFunctor T )))) ⟩ - ( TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (f) ・ g ) ) ) ・ h ) ) + ( TMap μ d ・ ( FMap T (( TMap μ d ・ ( FMap T f ・ g ) ) ) ・ h ) ) ∎ ) ⟩ - TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (f) ・ g ) ) ) ・ h ) + TMap μ d ・ ( FMap T (( TMap μ d ・ ( FMap T f ・ g ) ) ) ・ h ) ≡⟨⟩ join (join f g) h ∎ @@ -370,19 +371,19 @@ open Monad distr : {a b c : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) a b} {g : Hom (Kleisli Sets T m) b c} → (λ x → TMap (μ m) c (FMap T ((Kleisli Sets T m [ g o f ])) x)) - ≡ (( (λ x → TMap (μ m) c (FMap T (g) x)) ・ (λ x → TMap (μ m) b (FMap T (f) x)) )) + ≡ (( (λ x → TMap (μ m) c (FMap T g x)) ・ (λ x → TMap (μ m) b (FMap T f x)) )) distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in begin ( TMap (μ m) c ・ FMap T ((Kleisli Sets T m [ g o f ])) ) ≡⟨⟩ ( TMap (μ m) c ・ FMap T ( ( TMap (μ m) c ・ ( FMap T ( g ) ・ f ) ) ) ) ≡⟨ Right Sets {_} {_} {_} {TMap (μ m) c} {_} {_} ( IsFunctor.distr (Functor.isFunctor T) ) ⟩ - ( TMap (μ m) c ・ ( FMap T ( TMap (μ m) c) ・ FMap T ( ( FMap T (g) ・ f ) ) ) ) + ( TMap (μ m) c ・ ( FMap T ( TMap (μ m) c) ・ FMap T ( ( FMap T g ・ f ) ) ) ) ≡⟨ sym ( Left Sets (IsMonad.assoc (isMonad m ))) ⟩ - ( ( TMap (μ m) c ・ TMap (μ m) (FObj T c) ) ・ (FMap T (( FMap T (g) ・ f ))) ) + ( ( TMap (μ m) c ・ TMap (μ m) (FObj T c) ) ・ (FMap T (( FMap T g ・ f ))) ) ≡⟨ Right Sets {_} {_} {_} {TMap (μ m) c} ( Right Sets {_} {_} {_} {TMap (μ m) (FObj T c)} ( IsFunctor.distr (Functor.isFunctor T) ) ) ⟩ - ( ( TMap (μ m) c ・ TMap (μ m) (FObj T c) ) ・ ( FMap T ( FMap T (g)) ・ FMap T ( f ) ) ) + ( ( TMap (μ m) c ・ TMap (μ m) (FObj T c) ) ・ ( FMap T ( FMap T g) ・ FMap T ( f ) ) ) ≡⟨ sym ( Right Sets {_} {_} {_} {TMap (μ m) c} ( Left Sets (IsNTrans.commute ( NTrans.isNTrans (μ m))))) ⟩ - ( ( TMap (μ m) c ・ FMap T (g) ) ・ ( TMap (μ m) b ・ FMap T (f) ) ) + ( ( TMap (μ m) c ・ FMap T g ) ・ ( TMap (μ m) b ・ FMap T f ) ) ∎ @@ -416,7 +417,7 @@ let open Monad in record { left = λ {a} {b} f → f - ; right = λ {a} {b} f x → TMap (μ m) b ( TMap ( η m ) (FObj T b) ( (f) x ) ) + ; right = λ {a} {b} f x → TMap (μ m) b ( TMap ( η m ) (FObj T b) ( f x ) ) ; left-injective = left-injective ; right-injective = right-injective ; right-commute1 = right-commute1 @@ -459,9 +460,9 @@ right-commute2 {a} {a'} {b} {f} {h} = let open ≡-Reasoning in begin TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ ((Kleisli Sets T m [ f o FMap (F T {m}) h ] ))) ≡⟨⟩ - TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ ( (TMap (μ m) b ・ FMap T (f) ) ・ ( TMap (η m) a ・ h ))) + TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ ( (TMap (μ m) b ・ FMap T f ) ・ ( TMap (η m) a ・ h ))) ≡⟨ Left Sets (IsMonad.unity1 ( isMonad m )) ⟩ - (TMap (μ m) b ・ FMap T (f) ) ・ ( TMap (η m) a ・ h ) + (TMap (μ m) b ・ FMap T f ) ・ ( TMap (η m) a ・ h ) ≡⟨ Right Sets {_} {_} {_} {TMap (μ m) b} ( Left Sets ( IsNTrans.commute ( isNTrans (η m) ))) ⟩ TMap (μ m) b ・ (( TMap (η m) (FObj T b)・ f ) ・ h ) ∎
--- a/src/yoneda.agda Wed Mar 10 09:51:46 2021 +0900 +++ b/src/yoneda.agda Thu Mar 11 12:47:19 2021 +0900 @@ -387,35 +387,17 @@ s : CatSurjective A SetsAop YonedaFunctor s = Yoneda-surjective - -data [_]_~_ {c₁ c₂ ℓ} (C : Category c₁ c₂ ℓ) {A B : Obj C} (f : Hom C A B) - : ∀{X Y : Obj C} → Hom C X Y → Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where - refl : {g : Hom C A B} → (eqv : C [ f ≈ g ]) → [ C ] f ~ g - -≃→a=a : {c₁ ℓ : Level} (B : Category c₁ c₁ ℓ ) → {a b a' b' : Obj B } - → ( f : Hom B a b ) - → ( g : Hom B a' b' ) - → [_]_~_ B f g → a ≡ a' -≃→a=a B f g (refl eqv) = refl +--- How to prove it? from smallness? -a2 : {a : Obj A } → [ A ] id1 A a ~ id1 A a -a2 = refl (≈-Reasoning.refl-hom A) +data _~_ {a b : Obj A} (f : Hom A a b) + : ∀{x y : Obj A} → Hom A x y → Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where + refl : {g : Hom A a b} → (eqv : A [ f ≈ g ]) → f ~ g -postule - eqObj1 : {a b a' b' : Obj A } → Hom A a b ≡ Hom A a' b' → b ≡ b' --- eqObj1 = ≃→a=a A ? ? a2 close but ... - -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 +postulate -- ? + eqObj1 : {a b a' b' : Obj A } → Hom A a b ≡ Hom A a' b' → b ≡ b' Yoneda-full-embed : {a b : Obj A } → FObj YonedaFunctor a ≡ FObj YonedaFunctor b → a ≡ b -Yoneda-full-embed {a} {b} eq = eqObj1 A ylem1 where +Yoneda-full-embed {a} {b} eq = eqObj1 ylem1 where ylem1 : Hom A a a ≡ Hom A a b ylem1 = cong (λ k → FObj k a) eq - ylem2 : (x : Obj A) → Category.cod SetsAop (FMap YonedaFunctor (id1 A x)) ≡ FObj YonedaFunctor x - ylem2 x = refl - ylem3 : {a b : Obj A } → Hom A a b → Obj A - ylem3 x = Category.cod A x