Mercurial > hg > Members > kono > Proof > category
changeset 775:06a7831cf6ce
exchange left and right
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 13 Jun 2018 15:27:46 +0900 |
| parents | f3a493da92e8 |
| children | 5a3ca9509fbf |
| files | stdalone-kleisli.agda universal-mapping.agda |
| diffstat | 2 files changed, 253 insertions(+), 253 deletions(-) [+] |
line wrap: on
line diff
--- a/stdalone-kleisli.agda Wed Jun 13 12:56:38 2018 +0900 +++ b/stdalone-kleisli.agda Wed Jun 13 15:27:46 2018 +0900 @@ -179,11 +179,11 @@ open KleisliHom -left : {l : Level} (C : Category {l} ) {a b c : Obj C } {f f' : Hom C b c } {g : Hom C a b } → f ≡ f' → C [ f o g ] ≡ C [ f' o g ] -left {l} C {a} {b} {c} {f} {f'} {g} refl = cong ( λ z → C [ z o g ] ) refl +Left : {l : Level} (C : Category {l} ) {a b c : Obj C } {f f' : Hom C b c } {g : Hom C a b } → f ≡ f' → C [ f o g ] ≡ C [ f' o g ] +Left {l} C {a} {b} {c} {f} {f'} {g} refl = cong ( λ z → C [ z o g ] ) refl -right : {l : Level} (C : Category {l} ) {a b c : Obj C } {f : Hom C b c } {g g' : Hom C a b } → g ≡ g' → C [ f o g ] ≡ C [ f o g' ] -right {l} C {a} {b} {c} {f} {g} {g'} refl = cong ( λ z → C [ f o z ] ) refl +Right : {l : Level} (C : Category {l} ) {a b c : Obj C } {f : Hom C b c } {g g' : Hom C a b } → g ≡ g' → C [ f o g ] ≡ C [ f o g' ] +Right {l} C {a} {b} {c} {f} {g} {g'} refl = cong ( λ z → C [ f o z ] ) refl Assoc : {l : Level} (C : Category {l} ) {a b c d : Obj C } {f : Hom C c d } {g : Hom C b c } { h : Hom C a b } → C [ f o C [ g o h ] ] ≡ C [ C [ f o g ] o h ] @@ -264,35 +264,35 @@ record { KMap = TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ))) } ≡⟨ cong ( λ z → record { KMap = z } ) ( begin ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ ( FMap T (KMap g) ・ KMap h ) ) ) ) - ≡⟨ right C ( right C (Assoc C)) ⟩ + ≡⟨ Right C ( Right C (Assoc C)) ⟩ ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) ) ) ≡⟨ Assoc C ⟩ ( ( TMap (Monad.μ M) d ・ FMap T (KMap f) ) ・ ( ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ・ KMap h ) ) ≡⟨ Assoc C ⟩ ( ( ( TMap (Monad.μ M) d ・ FMap T (KMap f) ) ・ ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ) ・ KMap h ) - ≡⟨ sym ( left C (Assoc C )) ⟩ + ≡⟨ sym ( Left C (Assoc C )) ⟩ ( ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ ( TMap (Monad.μ M) c ・ FMap T (KMap g) ) ) ) ・ KMap h ) - ≡⟨ left C ( right C (Assoc C)) ⟩ + ≡⟨ Left C ( Right C (Assoc C)) ⟩ ( ( TMap (Monad.μ M) d ・ ( ( FMap T (KMap f) ・ TMap (Monad.μ M) c ) ・ FMap T (KMap g) ) ) ・ KMap h ) - ≡⟨ left C (Assoc C)⟩ + ≡⟨ Left C (Assoc C)⟩ ( ( ( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ TMap (Monad.μ M) c ) ) ・ FMap T (KMap g) ) ・ KMap h ) - ≡⟨ left C ( left C ( right C ( IsNTrans.commute (isNTrans (Monad.μ M) ) ) )) ⟩ + ≡⟨ Left C ( Left C ( Right C ( IsNTrans.commute (isNTrans (Monad.μ M) ) ) )) ⟩ ( ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ) ・ FMap T (KMap g) ) ・ KMap h ) - ≡⟨ sym ( left C (Assoc C)) ⟩ + ≡⟨ sym ( Left C (Assoc C)) ⟩ ( ( TMap (Monad.μ M) d ・ ( ( TMap (Monad.μ M) (FObj T d) ・ FMap (T ● T) (KMap f) ) ・ FMap T (KMap g) ) ) ・ KMap h ) - ≡⟨ sym ( left C ( right C (Assoc C))) ⟩ + ≡⟨ sym ( Left C ( Right C (Assoc C))) ⟩ ( ( TMap (Monad.μ M) d ・ ( TMap (Monad.μ M) (FObj T d) ・ ( FMap (T ● T) (KMap f) ・ FMap T (KMap g) ) ) ) ・ KMap h ) - ≡⟨ sym ( left C ( right C (right C (IsFunctor.distr (isFunctor T ) ) ) )) ⟩ + ≡⟨ 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 (KMap f) ・ KMap g )) ) ) ・ KMap h ) - ≡⟨ left C (Assoc C) ⟩ + ≡⟨ Left C (Assoc C) ⟩ ( ( ( TMap (Monad.μ M) d ・ TMap (Monad.μ M) (FObj T d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) - ≡⟨ left C (left C ( IsMonad.assoc (Monad.isMonad M ) ) ) ⟩ + ≡⟨ Left C (Left C ( IsMonad.assoc (Monad.isMonad M ) ) ) ⟩ ( ( ( TMap (Monad.μ M) d ・ FMap T (TMap (Monad.μ M) d) ) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) - ≡⟨ sym ( left C (Assoc C)) ⟩ + ≡⟨ sym ( Left C (Assoc C)) ⟩ ( ( TMap (Monad.μ M) d ・ ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ) ・ KMap h ) ≡⟨ sym (Assoc C) ⟩ ( TMap (Monad.μ M) d ・ ( ( FMap T (TMap (Monad.μ M) d) ・ FMap T (( FMap T (KMap f) ・ KMap g )) ) ・ KMap h ) ) - ≡⟨ sym (right C ( left C (IsFunctor.distr (isFunctor T )))) ⟩ + ≡⟨ sym (Right C ( Left C (IsFunctor.distr (isFunctor T )))) ⟩ ( TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) ) ∎ ) ⟩ record { KMap = ( TMap (Monad.μ M) d ・ ( FMap T (( TMap (Monad.μ M) d ・ ( FMap T (KMap f) ・ KMap g ) ) ) ・ KMap h ) ) } @@ -301,58 +301,58 @@ ∎ -- --- U : Kleisli Sets --- F : Sets Kleisli +-- U : Functor C D +-- F : Functor D C -- --- Hom Klei a b ←---→ Hom Sets a (U●F b ) +-- Hom C a b ←---→ Hom D a (U●F b ) -- --- Hom Klei (F a) (F b) ←---→ Hom Sets a (U●F b ) +-- Hom C (F a) (F b) ←---→ Hom D a (U●F b ) -- --- Hom Klei (F a) b ←---→ Hom Sets a U(b) Hom Klei (F a) b ←---→ Hom Sets a U(b) +-- Hom C (F a) b ←---→ Hom D a U(b) Hom C (F a) b ←---→ Hom D a U(b) -- | | | | -- Ff| f| |f |Uf -- | | | | -- ↓ ↓ ↓ ↓ --- Hom Klei (F (f a)) b ←---→ Hom Sets (f a) U(b) Hom Klei (F a) (f b) ←---→ Hom Sets a U(f b) +-- Hom C (F (f a)) b ←---→ Hom D (f a) U(b) Hom C (F a) (f b) ←---→ Hom D a U(f b) -- -- -record UnityOfOppsite ( Kleisli : Category ) ( U : Functor Kleisli Sets ) ( F : Functor Sets Kleisli ) : Set (suc zero) where +record UnityOfOppsite ( C D : Category ) ( U : Functor C D ) ( F : Functor D C ) : Set (suc zero) where field - hom-right : {a : Obj Sets} { b : Obj Kleisli } → Hom Sets a ( FObj U b ) → Hom Kleisli (FObj F a) b - hom-left : {a : Obj Sets} { b : Obj Kleisli } → Hom Kleisli (FObj F a) b → Hom Sets a ( FObj U b ) - hom-right-injective : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Sets a (FObj U b) } → hom-left ( hom-right f ) ≡ f - hom-left-injective : {a : Obj Sets} { b : Obj Kleisli } → {f : Hom Kleisli (FObj F a) b } → hom-right ( hom-left f ) ≡ f + left : {a : Obj D} { b : Obj C } → Hom D a ( FObj U b ) → Hom C (FObj F a) b + right : {a : Obj D} { b : Obj C } → Hom C (FObj F a) b → Hom D a ( FObj U b ) + left-injective : {a : Obj D} { b : Obj C } → {f : Hom D a (FObj U b) } → right ( left f ) ≡ f + right-injective : {a : Obj D} { b : Obj C } → {f : Hom C (FObj F a) b } → left ( right f ) ≡ f --- naturality of Φ - hom-left-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } → - { f : Hom Kleisli (FObj F a) b } → { k : Hom Kleisli b b' } → - hom-left ( Kleisli [ k o f ] ) ≡ Sets [ FMap U k o hom-left f ] - hom-left-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } → - { f : Hom Kleisli (FObj F a) b } → { h : Hom Sets a' a } → - hom-left ( Kleisli [ f o FMap F h ] ) ≡ Sets [ hom-left f o h ] - hom-right-commute1 : {a : Obj Sets} {b b' : Obj Kleisli } → - { g : Hom Sets a (FObj U b)} → { k : Hom Kleisli b b' } → - Kleisli [ k o hom-right g ] ≡ hom-right ( Sets [ FMap U k o g ] ) - hom-right-commute1 {a} {b} {b'} {g} {k} = let open ≡-Reasoning in begin - Kleisli [ k o hom-right g ] - ≡⟨ sym hom-left-injective ⟩ - hom-right ( hom-left ( Kleisli [ k o hom-right g ] ) ) - ≡⟨ cong ( λ z → hom-right z ) hom-left-commute1 ⟩ - hom-right (Sets [ FMap U k o hom-left (hom-right g) ]) - ≡⟨ cong ( λ z → hom-right ( Sets [ FMap U k o z ] )) hom-right-injective ⟩ - hom-right ( Sets [ FMap U k o g ] ) + right-commute1 : {a : Obj D} {b b' : Obj C } → + { f : Hom C (FObj F a) b } → { k : Hom C b b' } → + right ( C [ k o f ] ) ≡ D [ FMap U k o right f ] + right-commute2 : {a a' : Obj D} {b : Obj C } → + { f : Hom C (FObj F a) b } → { h : Hom D a' a } → + right ( C [ f o FMap F h ] ) ≡ D [ right f o h ] + left-commute1 : {a : Obj D} {b b' : Obj C } → + { g : Hom D a (FObj U b)} → { k : Hom C b b' } → + C [ k o left g ] ≡ left ( D [ FMap U k o g ] ) + left-commute1 {a} {b} {b'} {g} {k} = let open ≡-Reasoning in begin + C [ k o left g ] + ≡⟨ sym right-injective ⟩ + left ( right ( C [ k o left g ] ) ) + ≡⟨ cong ( λ z → left z ) right-commute1 ⟩ + left (D [ FMap U k o right (left g) ]) + ≡⟨ cong ( λ z → left ( D [ FMap U k o z ] )) left-injective ⟩ + left ( D [ FMap U k o g ] ) ∎ - hom-right-commute2 : {a a' : Obj Sets} {b : Obj Kleisli } → - { g : Hom Sets a (FObj U b) } → { h : Hom Sets a' a } → - Kleisli [ hom-right g o FMap F h ] ≡ hom-right ( Sets [ g o h ] ) - hom-right-commute2 {a} {a'} {b} {g} {h} = let open ≡-Reasoning in begin - Kleisli [ hom-right g o FMap F h ] - ≡⟨ sym hom-left-injective ⟩ - hom-right (hom-left (Kleisli [ hom-right g o FMap F h ])) - ≡⟨ cong ( λ z → hom-right z ) hom-left-commute2 ⟩ - hom-right (Sets [ hom-left (hom-right g) o h ]) - ≡⟨ cong ( λ z → hom-right ( Sets [ z o h ] )) hom-right-injective ⟩ - hom-right (Sets [ g o h ]) + left-commute2 : {a a' : Obj D} {b : Obj C } → + { g : Hom D a (FObj U b) } → { h : Hom D a' a } → + C [ left g o FMap F h ] ≡ left ( D [ g o h ] ) + left-commute2 {a} {a'} {b} {g} {h} = let open ≡-Reasoning in begin + C [ left g o FMap F h ] + ≡⟨ sym right-injective ⟩ + left (right (C [ left g o FMap F h ])) + ≡⟨ cong ( λ z → left z ) right-commute2 ⟩ + left (D [ right (left g) o h ]) + ≡⟨ cong ( λ z → left ( D [ z o h ] )) left-injective ⟩ + left (D [ g o h ]) ∎ @@ -370,19 +370,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 (KMap (Kleisli Sets T m [ g o f ])) x)) - ≡ (Sets [ (λ x → TMap (μ m) c (FMap T (KMap g) x)) o (λ x → TMap (μ m) b (FMap T (KMap f) x)) ]) + ≡ (( (λ x → TMap (μ m) c (FMap T (KMap g) x)) ・ (λ x → TMap (μ m) b (FMap T (KMap f) x)) )) distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in begin - Sets [ TMap (μ m) c o FMap T (KMap (Kleisli Sets T m [ g o f ])) ] + ( TMap (μ m) c ・ FMap T (KMap (Kleisli Sets T m [ g o f ])) ) ≡⟨⟩ - Sets [ TMap (μ m) c o FMap T ( Sets [ TMap (μ m) c o Sets [ FMap T ( KMap g ) o KMap f ] ] ) ] - ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} {_} {_} ( IsFunctor.distr (Functor.isFunctor T) ) ⟩ - Sets [ TMap (μ m) c o Sets [ FMap T ( TMap (μ m) c) o FMap T ( Sets [ FMap T (KMap g) o KMap f ] ) ] ] - ≡⟨ sym ( left Sets (IsMonad.assoc (isMonad m ))) ⟩ - Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o (FMap T (Sets [ FMap T (KMap g) o KMap f ])) ] - ≡⟨ right Sets {_} {_} {_} {TMap (μ m) c} ( right Sets {_} {_} {_} {TMap (μ m) (FObj T c)} ( IsFunctor.distr (Functor.isFunctor T) ) ) ⟩ - Sets [ Sets [ TMap (μ m) c o TMap (μ m) (FObj T c) ] o Sets [ FMap T ( FMap T (KMap g)) o FMap T ( KMap f ) ] ] - ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} ( left Sets (IsNTrans.commute ( NTrans.isNTrans (μ m))))) ⟩ - Sets [ Sets [ TMap (μ m) c o FMap T (KMap g) ] o Sets [ TMap (μ m) b o FMap T (KMap f) ] ] + ( TMap (μ m) c ・ FMap T ( ( TMap (μ m) c ・ ( FMap T ( KMap g ) ・ KMap f ) ) ) ) + ≡⟨ Right Sets {_} {_} {_} {TMap (μ m) c} {_} {_} ( IsFunctor.distr (Functor.isFunctor T) ) ⟩ + ( TMap (μ m) c ・ ( FMap T ( TMap (μ m) c) ・ FMap T ( ( FMap T (KMap g) ・ KMap f ) ) ) ) + ≡⟨ sym ( Left Sets (IsMonad.assoc (isMonad m ))) ⟩ + ( ( TMap (μ m) c ・ TMap (μ m) (FObj T c) ) ・ (FMap T (( FMap T (KMap g) ・ KMap 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 (KMap g)) ・ FMap T ( KMap f ) ) ) + ≡⟨ sym ( Right Sets {_} {_} {_} {TMap (μ m) c} ( Left Sets (IsNTrans.commute ( NTrans.isNTrans (μ m))))) ⟩ + ( ( TMap (μ m) c ・ FMap T (KMap g) ) ・ ( TMap (μ m) b ・ FMap T (KMap f) ) ) ∎ @@ -392,18 +392,18 @@ ; isFunctor = record { identity = refl ; distr = distr } } where open Monad - distr : {a b c : Obj Sets} {f : Hom Sets a b} {g : Hom Sets b c} → record { KMap = λ x → TMap (η m) c ((Sets [ g o f ]) x) } ≡ + distr : {a b c : Obj Sets} {f : Hom Sets a b} {g : Hom Sets b c} → record { KMap = λ x → TMap (η m) c ((( g ・ f )) x) } ≡ Kleisli Sets T m [ record { KMap = λ x → TMap (η m) c (g x) } o record { KMap = λ x → TMap (η m) b (f x) } ] distr {a} {b} {c} {f} {g} = let open ≡-Reasoning in ( cong ( λ z → record { KMap = z } ) ( begin - Sets [ TMap (η m) c o Sets [ g o f ] ] - ≡⟨ left Sets {_} {_} {_} {Sets [ TMap (η m) c o g ] } ( sym ( IsNTrans.commute ( NTrans.isNTrans (η m) ) )) ⟩ - Sets [ Sets [ FMap T g o TMap (η m) b ] o f ] + ( TMap (η m) c ・ ( g ・ f ) ) + ≡⟨ Left Sets {_} {_} {_} {( TMap (η m) c ・ g ) } ( sym ( IsNTrans.commute ( NTrans.isNTrans (η m) ) )) ⟩ + ( ( FMap T g ・ TMap (η m) b ) ・ f ) ≡⟨ sym ( IsCategory.idL ( Category.isCategory Sets )) ⟩ - Sets [ ( λ x → x ) o Sets [ Sets [ FMap T g o TMap (η m) b ] o f ] ] - ≡⟨ sym ( left Sets (IsMonad.unity2 (isMonad m ))) ⟩ - Sets [ Sets [ TMap (μ m) c o FMap T (TMap (η m) c) ] o Sets [ FMap T g o Sets [ TMap (η m) b o f ] ] ] - ≡⟨ sym ( right Sets {_} {_} {_} {TMap (μ m) c} {_} ( left Sets {_} {_} {_} { FMap T (Sets [ TMap (η m) c o g ] )} ( IsFunctor.distr (Functor.isFunctor T) ))) ⟩ - Sets [ TMap (μ m) c o ( Sets [ FMap T (Sets [ TMap (η m) c o g ] ) o Sets [ TMap (η m) b o f ] ] ) ] + ( ( λ x → x ) ・ ( ( FMap T g ・ TMap (η m) b ) ・ f ) ) + ≡⟨ sym ( Left Sets (IsMonad.unity2 (isMonad m ))) ⟩ + ( ( TMap (μ m) c ・ FMap T (TMap (η m) c) ) ・ ( FMap T g ・ ( TMap (η m) b ・ f ) ) ) + ≡⟨ sym ( Right Sets {_} {_} {_} {TMap (μ m) c} {_} ( Left Sets {_} {_} {_} { FMap T (( TMap (η m) c ・ g ) )} ( IsFunctor.distr (Functor.isFunctor T) ))) ⟩ + ( TMap (μ m) c ・ ( ( FMap T (( TMap (η m) c ・ g ) ) ・ ( TMap (η m) b ・ f ) ) ) ) ∎ )) -- @@ -411,64 +411,64 @@ -- Hom Kleisli (FObj F a) b = Hom Sets a (T b) -- -lemma→ : ( T : Functor Sets Sets ) → (m : Monad T ) → UnityOfOppsite (Kleisli Sets T m) (U T {m} ) (F T {m}) +lemma→ : ( T : Functor Sets Sets ) → (m : Monad T ) → UnityOfOppsite (Kleisli Sets T m) Sets (U T {m} ) (F T {m}) lemma→ T m = let open Monad in record { - hom-right = λ {a} {b} f → record { KMap = f } - ; hom-left = λ {a} {b} f x → TMap (μ m) b ( TMap ( η m ) (FObj T b) ( (KMap f) x ) ) - ; hom-right-injective = hom-right-injective - ; hom-left-injective = hom-left-injective - ; hom-left-commute1 = hom-left-commute1 - ; hom-left-commute2 = hom-left-commute2 + left = λ {a} {b} f → record { KMap = f } + ; right = λ {a} {b} f x → TMap (μ m) b ( TMap ( η m ) (FObj T b) ( (KMap f) x ) ) + ; left-injective = left-injective + ; right-injective = right-injective + ; right-commute1 = right-commute1 + ; right-commute2 = right-commute2 } where open Monad - hom-right-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} + left-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom Sets a (FObj (U T {m}) b)} → (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (f x))) ≡ f - hom-right-injective {a} {b} {f} = let open ≡-Reasoning in begin - Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o f ] ] - ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩ - Sets [ id Sets (FObj (U T {m}) b) o f ] + left-injective {a} {b} {f} = let open ≡-Reasoning in begin + ( TMap (μ m) b ・ ( TMap (η m) (FObj T b) ・ f ) ) + ≡⟨ Left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩ + ( id Sets (FObj (U T {m}) b) ・ f ) ≡⟨ IsCategory.idL ( isCategory Sets ) ⟩ f ∎ - hom-left-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} + right-injective : {a : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} → record { KMap = λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x)) } ≡ f - hom-left-injective {a} {b} {f} = let open ≡-Reasoning in cong ( λ z → record { KMap = z } ) ( begin - Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o KMap f ] ] - ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩ + right-injective {a} {b} {f} = let open ≡-Reasoning in cong ( λ z → record { KMap = z } ) ( begin + ( TMap (μ m) b ・ ( TMap (η m) (FObj T b) ・ KMap f ) ) + ≡⟨ Left Sets ( IsMonad.unity1 ( isMonad m ) ) ⟩ KMap f ∎ ) - hom-left-commute1 : {a : Obj Sets} {b b' : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {k : Hom (Kleisli Sets T m) b b'} → - (λ x → TMap (μ m) b' (TMap (η m) (FObj T b') (KMap (Kleisli Sets T m [ k o f ]) x))) - ≡ (Sets [ FMap (U T {m}) k o (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) ]) - hom-left-commute1 {a} {b} {b'} {f} {k} = let open ≡-Reasoning in begin - Sets [ TMap (μ m) b' o Sets [ TMap (η m) (FObj T b') o KMap (Kleisli Sets T m [ k o f ] ) ] ] + right-commute1 : {a : Obj Sets} {b b' : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {k : Hom (Kleisli Sets T m) b b'} → + (λ x → TMap (μ m) b' (TMap (η m) (FObj T b') (KMap (Kleisli Sets T m [ k o f ] ) x))) + ≡ (( FMap (U T {m}) k ・ (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) )) + right-commute1 {a} {b} {b'} {f} {k} = let open ≡-Reasoning in begin + ( TMap (μ m) b' ・ ( TMap (η m) (FObj T b') ・ KMap (Kleisli Sets T m [ k o f ] ) ) ) ≡⟨⟩ TMap (μ m) b' ・ ( TMap (η m) (FObj T b') ・ ( TMap (μ m) b' ・ ( FMap T (KMap k) ・ KMap f ))) - ≡⟨ left Sets ( IsMonad.unity1 ( isMonad m )) ⟩ + ≡⟨ Left Sets ( IsMonad.unity1 ( isMonad m )) ⟩ TMap (μ m) b' ・ ( FMap T (KMap k) ・ KMap f ) - ≡⟨ right Sets {_} {_} {_} {TMap ( μ m ) b' ・ FMap T ( KMap k )} ( left Sets ( sym ( IsMonad.unity1 ( isMonad m ) ) ) ) ⟩ + ≡⟨ Right Sets {_} {_} {_} {TMap ( μ m ) b' ・ FMap T ( KMap k )} ( Left Sets ( sym ( IsMonad.unity1 ( isMonad m ) ) ) ) ⟩ ( TMap ( μ m ) b' ・ FMap T ( KMap k ) ) ・ ( TMap (μ m) b ・ ( TMap (η m) (FObj T b) ・ KMap f ) ) ≡⟨⟩ - Sets [ FMap (U T {m}) k o Sets [ TMap (μ m) b o Sets [ TMap (η m) (FObj T b) o KMap f ] ] ] + ( FMap (U T {m}) k ・ ( TMap (μ m) b ・ ( TMap (η m) (FObj T b) ・ KMap f ) ) ) ∎ - hom-left-commute2 : {a a' : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {h : Hom Sets a' a} → - (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ]) x))) - ≡ (Sets [ (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x))) o h ]) - hom-left-commute2 {a} {a'} {b} {f} {h} = let open ≡-Reasoning in begin - TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ]))) + right-commute2 : {a a' : Obj Sets} {b : Obj (Kleisli Sets T m)} {f : Hom (Kleisli Sets T m) (FObj (F T {m}) a) b} {h : Hom Sets a' a} → + (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ] ) x))) + ≡ (( (λ x → TMap (μ m) b (TMap (η m) (FObj T b) (KMap f x)))・ h )) + right-commute2 {a} {a'} {b} {f} {h} = let open ≡-Reasoning in begin + TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ (KMap (Kleisli Sets T m [ f o FMap (F T {m}) h ] ))) ≡⟨⟩ TMap (μ m) b ・ (TMap (η m) (FObj T b) ・ ( (TMap (μ m) b ・ FMap T (KMap f) ) ・ ( TMap (η m) a ・ h ))) - ≡⟨ left Sets (IsMonad.unity1 ( isMonad m )) ⟩ + ≡⟨ Left Sets (IsMonad.unity1 ( isMonad m )) ⟩ (TMap (μ m) b ・ FMap T (KMap f) ) ・ ( TMap (η m) a ・ h ) - ≡⟨ right Sets {_} {_} {_} {TMap (μ m) b} ( left Sets ( IsNTrans.commute ( isNTrans (η m) ))) ⟩ + ≡⟨ Right Sets {_} {_} {_} {TMap (μ m) b} ( Left Sets ( IsNTrans.commute ( isNTrans (η m) ))) ⟩ TMap (μ m) b ・ (( TMap (η m) (FObj T b)・ KMap f ) ・ h ) ∎ -lemma← : ( U F : Functor Sets Sets ) → UnityOfOppsite Sets U F → Monad ( U ● F ) +lemma← : ( U F : Functor Sets Sets ) → UnityOfOppsite Sets Sets U F → Monad ( U ● F ) lemma← U F uo = record { η = η ; μ = μ @@ -480,73 +480,73 @@ } where open UnityOfOppsite T = U ● F - η-comm : {a b : Obj Sets} {f : Hom Sets a b} → Sets [ FMap (U ● F) f o (λ x → hom-left uo (λ x₁ → x₁) x) ] - ≡ Sets [ (λ x → hom-left uo (λ x₁ → x₁) x) o FMap (idFunctor {_} {Sets} ) f ] + η-comm : {a b : Obj Sets} {f : Hom Sets a b} → ( FMap (U ● F) f ・ (λ x → right uo (λ x₁ → x₁) x) ) + ≡ ( (λ x → right uo (λ x₁ → x₁) x) ・ FMap (idFunctor {_} {Sets} ) f ) η-comm {a} {b} {f} = let open ≡-Reasoning in begin - FMap (U ● F) f ・ (hom-left uo (λ x₁ → x₁) ) - ≡⟨ sym (hom-left-commute1 uo) ⟩ - hom-left uo ( FMap F f ・ (λ x₁ → x₁) ) - ≡⟨ hom-left-commute2 uo ⟩ - hom-left uo (λ x₁ → x₁) ・ FMap ( idFunctor {_} {Sets} ) f + FMap (U ● F) f ・ (right uo (λ x₁ → x₁) ) + ≡⟨ sym (right-commute1 uo) ⟩ + right uo ( FMap F f ・ (λ x₁ → x₁) ) + ≡⟨ right-commute2 uo ⟩ + right uo (λ x₁ → x₁) ・ FMap ( idFunctor {_} {Sets} ) f ∎ η : NTrans (idFunctor {_} {Sets}) T - η = record { TMap = λ a x → (hom-left uo) (λ x → x ) x ; isNTrans = record { commute = η-comm } } - μ-comm : {a b : Obj Sets} {f : Hom Sets a b} → (Sets [ FMap T f o (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) ]) - ≡ (Sets [ (λ x → FMap U (hom-right uo (λ x₁ → x₁)) x) o FMap (T ● T) f ]) + η = record { TMap = λ a x → (right uo) (λ x → x ) x ; isNTrans = record { commute = η-comm } } + μ-comm : {a b : Obj Sets} {f : Hom Sets a b} → (( FMap T f ・ (λ x → FMap U (left uo (λ x₁ → x₁)) x) )) + ≡ (( (λ x → FMap U (left uo (λ x₁ → x₁)) x) ・ FMap (T ● T) f )) μ-comm {a} {b} {f} = let open ≡-Reasoning in begin - FMap T f ・ FMap U (hom-right uo (λ x₁ → x₁)) + FMap T f ・ FMap U (left uo (λ x₁ → x₁)) ≡⟨⟩ - FMap U (FMap F f ) ・ FMap U (hom-right uo (λ x₁ → x₁)) + FMap U (FMap F f ) ・ FMap U (left uo (λ x₁ → x₁)) ≡⟨ sym ( IsFunctor.distr ( Functor.isFunctor U)) ⟩ - FMap U (FMap F f ・ hom-right uo (λ x₁ → x₁)) - ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute1 uo) ⟩ - FMap U ( hom-right uo (FMap U (FMap F f) ・ (λ x₁ → x₁) ) ) - ≡⟨ sym ( cong ( λ z → FMap U z ) (hom-right-commute2 uo)) ⟩ - FMap U ((hom-right uo (λ x₁ → x₁)) ・ (FMap F (FMap U (FMap F f )))) + FMap U (FMap F f ・ left uo (λ x₁ → x₁)) + ≡⟨ cong ( λ z → FMap U z ) (left-commute1 uo) ⟩ + FMap U ( left uo (FMap U (FMap F f) ・ (λ x₁ → x₁) ) ) + ≡⟨ sym ( cong ( λ z → FMap U z ) (left-commute2 uo)) ⟩ + FMap U ((left uo (λ x₁ → x₁)) ・ (FMap F (FMap U (FMap F f )))) ≡⟨ IsFunctor.distr ( Functor.isFunctor U) ⟩ - FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (FMap F f ))) + FMap U (left uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (FMap F f ))) ≡⟨⟩ - FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap (T ● T) f + FMap U (left uo (λ x₁ → x₁)) ・ FMap (T ● T) f ∎ μ : NTrans (T ● T) T - μ = record { TMap = λ a x → FMap U ( hom-right uo (λ x → x)) x ; isNTrans = record { commute = μ-comm } } - unity1 : {a : Obj Sets} → (Sets [ TMap μ a o TMap η (FObj (U ● F) a) ]) ≡ id Sets (FObj (U ● F) a) + μ = record { TMap = λ a x → FMap U ( left uo (λ x → x)) x ; isNTrans = record { commute = μ-comm } } + unity1 : {a : Obj Sets} → (( TMap μ a ・ TMap η (FObj (U ● F) a) )) ≡ id Sets (FObj (U ● F) a) unity1 {a} = let open ≡-Reasoning in begin TMap μ a ・ TMap η (FObj (U ● F) a) ≡⟨⟩ - FMap U (hom-right uo (λ x₁ → x₁)) ・ hom-left uo (λ x₁ → x₁) - ≡⟨ sym (hom-left-commute1 uo ) ⟩ - hom-left uo ( hom-right uo (λ x₁ → x₁) ・ (λ x₁ → x₁) ) - ≡⟨ hom-right-injective uo ⟩ + FMap U (left uo (λ x₁ → x₁)) ・ right uo (λ x₁ → x₁) + ≡⟨ sym (right-commute1 uo ) ⟩ + right uo ( left uo (λ x₁ → x₁) ・ (λ x₁ → x₁) ) + ≡⟨ left-injective uo ⟩ id Sets (FObj (U ● F) a) ∎ - unity2 : {a : Obj Sets} → (Sets [ TMap μ a o FMap (U ● F) (TMap η a) ]) ≡ id Sets (FObj (U ● F) a) + unity2 : {a : Obj Sets} → (( TMap μ a ・ FMap (U ● F) (TMap η a) )) ≡ id Sets (FObj (U ● F) a) unity2 {a} = let open ≡-Reasoning in begin TMap μ a ・ FMap (U ● F) (TMap η a) ≡⟨⟩ - FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (hom-left uo (λ x₁ → x₁))) + FMap U (left uo (λ x₁ → x₁)) ・ FMap U (FMap F (right uo (λ x₁ → x₁))) ≡⟨ sym ( IsFunctor.distr (isFunctor U)) ⟩ - FMap U (hom-right uo (λ x₁ → x₁) ・ FMap F (hom-left uo (λ x₁ → x₁))) - ≡⟨ cong ( λ z → FMap U z ) (hom-right-commute2 uo) ⟩ - FMap U (hom-right uo ((λ x₁ → x₁) ・ hom-left uo (λ x₁ → x₁) )) - ≡⟨ cong ( λ z → FMap U z ) (hom-left-injective uo) ⟩ + FMap U (left uo (λ x₁ → x₁) ・ FMap F (right uo (λ x₁ → x₁))) + ≡⟨ cong ( λ z → FMap U z ) (left-commute2 uo) ⟩ + FMap U (left uo ((λ x₁ → x₁) ・ right uo (λ x₁ → x₁) )) + ≡⟨ cong ( λ z → FMap U z ) (right-injective uo) ⟩ FMap U ( id Sets (FObj F a) ) ≡⟨ IsFunctor.identity (isFunctor U) ⟩ id Sets (FObj (U ● F) a) ∎ - assoc : {a : Obj Sets} → (Sets [ TMap μ a o TMap μ (FObj (U ● F) a) ]) ≡ (Sets [ TMap μ a o FMap (U ● F) (TMap μ a) ]) + assoc : {a : Obj Sets} → (( TMap μ a ・ TMap μ (FObj (U ● F) a) )) ≡ (( TMap μ a ・ FMap (U ● F) (TMap μ a) )) assoc {a} = let open ≡-Reasoning in begin TMap μ a ・ TMap μ (FObj (U ● F) a) ≡⟨⟩ - FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (hom-right uo (λ x₁ → x₁)) + FMap U (left uo (λ x₁ → x₁)) ・ FMap U (left uo (λ x₁ → x₁)) ≡⟨ sym ( IsFunctor.distr (isFunctor U )) ⟩ - FMap U (hom-right uo (λ x₁ → x₁) ・ hom-right uo (λ x₁ → x₁)) - ≡⟨ cong ( λ z → FMap U z ) ( hom-right-commute1 uo ) ⟩ - FMap U (hom-right uo ((λ x₁ → x₁) ・ FMap U (hom-right uo (λ x₁ → x₁))) ) - ≡⟨ sym ( cong ( λ z → FMap U z ) ( hom-right-commute2 uo ) ) ⟩ - FMap U (hom-right uo (λ x₁ → x₁) ・ FMap F (FMap U (hom-right uo (λ x₁ → x₁)))) + FMap U (left uo (λ x₁ → x₁) ・ left uo (λ x₁ → x₁)) + ≡⟨ cong ( λ z → FMap U z ) ( left-commute1 uo ) ⟩ + FMap U (left uo ((λ x₁ → x₁) ・ FMap U (left uo (λ x₁ → x₁))) ) + ≡⟨ sym ( cong ( λ z → FMap U z ) ( left-commute2 uo ) ) ⟩ + FMap U (left uo (λ x₁ → x₁) ・ FMap F (FMap U (left uo (λ x₁ → x₁)))) ≡⟨ IsFunctor.distr (isFunctor U ) ⟩ - FMap U (hom-right uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (hom-right uo (λ x₁ → x₁)))) + FMap U (left uo (λ x₁ → x₁)) ・ FMap U (FMap F (FMap U (left uo (λ x₁ → x₁)))) ≡⟨⟩ TMap μ a ・ FMap (U ● F) (TMap μ a) ∎
--- a/universal-mapping.agda Wed Jun 13 12:56:38 2018 +0900 +++ b/universal-mapping.agda Wed Jun 13 15:27:46 2018 +0900 @@ -366,11 +366,11 @@ -- naturality of left (Φ) -- k = Hom A b b' ; f' = k o f h Hom A a' a ; f' = f o h -- left left --- f : Hom A F(a) b -------→ f* : Hom B a U(b) f' : Hom A F(a')b ------→ f'* : Hom B a' U(b) --- | | | | --- |k* |U(k*) |F(h*) |h* --- v v v v --- f': Hom A F(a) b'------→ f'* : Hom B a U(b') f: Hom A F(a) b --------→ f* : Hom B a U(b) +-- f : Hom A F(a) b ←------- f* : Hom B a U(b) f' : Hom A F(a')b ←------ f'* : Hom B a' U(b) +-- | -------→ | | | +-- |k right |U(k) |F(h) |h +-- ↓ ↓ ↓ ↓ +-- f': Hom A F(a) b'←------ f'* : Hom B a U(b') f: Hom A F(a) b ←-------- f* : Hom B a U(b) -- left left record UnityOfOppsite {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') @@ -378,69 +378,69 @@ ( F : Functor A B ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where field - right : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b - left : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b ) - right-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ left ( right f ) ≈ f ] - left-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ right ( left f ) ≈ f ] + left : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b + right : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b ) + left-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ right ( left f ) ≈ f ] + right-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ left ( right f ) ≈ f ] --- naturality of Φ - left-commute1 : {a : Obj A} {b b' : Obj B } → + right-commute1 : {a : Obj A} {b b' : Obj B } → { f : Hom B (FObj F a) b } → { k : Hom B b b' } → - A [ left ( B [ k o f ] ) ≈ A [ FMap U k o left f ] ] - left-commute2 : {a a' : Obj A} {b : Obj B } → + A [ right ( B [ k o f ] ) ≈ A [ FMap U k o right f ] ] + right-commute2 : {a a' : Obj A} {b : Obj B } → { f : Hom B (FObj F a) b } → { h : Hom A a' a } → - A [ left ( B [ f o FMap F h ] ) ≈ A [ left f o h ] ] - r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } → A [ f ≈ g ] → B [ right f ≈ right g ] - l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b } → B [ f ≈ g ] → A [ left f ≈ left g ] - -- naturality of right (Φ-1) - right-commute1 : {a : Obj A} {b b' : Obj B } → + A [ right ( B [ f o FMap F h ] ) ≈ A [ right f o h ] ] + r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } → A [ f ≈ g ] → B [ left f ≈ left g ] + l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b } → B [ f ≈ g ] → A [ right f ≈ right g ] + -- naturality of left (Φ-1) + left-commute1 : {a : Obj A} {b b' : Obj B } → { g : Hom A a (FObj U b)} → { k : Hom B b b' } → - B [ B [ k o right g ] ≈ right ( A [ FMap U k o g ] ) ] - right-commute1 {a} {b} {b'} {g} {k} = let open ≈-Reasoning (B) in + B [ B [ k o left g ] ≈ left ( A [ FMap U k o g ] ) ] + left-commute1 {a} {b} {b'} {g} {k} = let open ≈-Reasoning (B) in begin - k o right g - ≈⟨ sym left-injective ⟩ - right ( left ( k o right g ) ) - ≈⟨ r-cong left-commute1 ⟩ - right ( A [ FMap U k o left ( right g ) ] ) + k o left g + ≈⟨ sym right-injective ⟩ + left ( right ( k o left g ) ) + ≈⟨ r-cong right-commute1 ⟩ + left ( A [ FMap U k o right ( left g ) ] ) ≈⟨ r-cong (lemma-1 g k) ⟩ - right ( A [ FMap U k o g ] ) + left ( A [ FMap U k o g ] ) ∎ where lemma-1 : {a : Obj A} {b b' : Obj B } → ( g : Hom A a (FObj U b)) → ( k : Hom B b b' ) → - A [ A [ FMap U k o left ( right g ) ] ≈ A [ FMap U k o g ] ] + A [ A [ FMap U k o right ( left g ) ] ≈ A [ FMap U k o g ] ] lemma-1 g k = let open ≈-Reasoning (A) in begin - FMap U k o left ( right g ) - ≈⟨ cdr ( right-injective) ⟩ + FMap U k o right ( left g ) + ≈⟨ cdr ( left-injective) ⟩ FMap U k o g ∎ - right-commute2 : {a a' : Obj A} {b : Obj B } → + left-commute2 : {a a' : Obj A} {b : Obj B } → { g : Hom A a (FObj U b) } → { h : Hom A a' a } → - B [ B [ right g o FMap F h ] ≈ right ( A [ g o h ] ) ] - right-commute2 {a} {a'} {b} {g} {h} = let open ≈-Reasoning (B) in + B [ B [ left g o FMap F h ] ≈ left ( A [ g o h ] ) ] + left-commute2 {a} {a'} {b} {g} {h} = let open ≈-Reasoning (B) in begin - right g o FMap F h - ≈⟨ sym left-injective ⟩ - right ( left ( right g o FMap F h )) - ≈⟨ r-cong left-commute2 ⟩ - right ( A [ left ( right g ) o h ] ) + left g o FMap F h + ≈⟨ sym right-injective ⟩ + left ( right ( left g o FMap F h )) + ≈⟨ r-cong right-commute2 ⟩ + left ( A [ right ( left g ) o h ] ) ≈⟨ r-cong ( lemma-2 g h ) ⟩ - right ( A [ g o h ] ) + left ( A [ g o h ] ) ∎ where lemma-2 : {a a' : Obj A} {b : Obj B } → ( g : Hom A a (FObj U b)) → ( h : Hom A a' a ) → - A [ A [ left ( right g ) o h ] ≈ A [ g o h ] ] - lemma-2 g h = let open ≈-Reasoning (A) in car ( right-injective ) + A [ A [ right ( left g ) o h ] ≈ A [ g o h ] ] + lemma-2 g h = let open ≈-Reasoning (A) in car ( left-injective ) Adj2UO : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( adj : Adjunction A B ) → UnityOfOppsite A B (Adjunction.U adj) (Adjunction.F adj) Adj2UO A B adj = record { - right = right ; - left = left ; - right-injective = right-injective ; - left-injective = left-injective ; - left-commute1 = left-commute1 ; - left-commute2 = left-commute2 ; + left = left ; + right = right ; + left-injective = left-injective ; + right-injective = right-injective ; + right-commute1 = right-commute1 ; + right-commute2 = right-commute2 ; r-cong = r-cong ; l-cong = l-cong } where @@ -452,12 +452,12 @@ η = Adjunction.η adj ε : NTrans B B ( F ○ U ) identityFunctor ε = Adjunction.ε adj - right : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b - right {a} {b} f = B [ TMap ε b o FMap F f ] - left : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b ) - left {a} {b} f = A [ FMap U f o (TMap η a) ] - right-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ left ( right f ) ≈ f ] - right-injective {a} {b} {f} = let open ≈-Reasoning (A) in + left : {a : Obj A} { b : Obj B } → Hom A a ( FObj U b ) → Hom B (FObj F a) b + left {a} {b} f = B [ TMap ε b o FMap F f ] + right : {a : Obj A} { b : Obj B } → Hom B (FObj F a) b → Hom A a ( FObj U b ) + right {a} {b} f = A [ FMap U f o (TMap η a) ] + left-injective : {a : Obj A} { b : Obj B } → {f : Hom A a (FObj U b) } → A [ right ( left f ) ≈ f ] + left-injective {a} {b} {f} = let open ≈-Reasoning (A) in begin FMap U (B [ TMap ε b o FMap F f ]) o (TMap η a) ≈⟨ car ( distr U ) ⟩ @@ -473,8 +473,8 @@ ≈⟨ idL ⟩ f ∎ - left-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ right ( left f ) ≈ f ] - left-injective {a} {b} {f} = let open ≈-Reasoning (B) in + right-injective : {a : Obj A} { b : Obj B } → {f : Hom B (FObj F a) b } → B [ left ( right f ) ≈ f ] + right-injective {a} {b} {f} = let open ≈-Reasoning (B) in begin TMap ε b o FMap F ( A [ FMap U f o (TMap η a) ]) ≈⟨ cdr ( distr F ) ⟩ @@ -490,12 +490,12 @@ ≈⟨ idR ⟩ f ∎ - left-commute1 : {a : Obj A} {b b' : Obj B } → + right-commute1 : {a : Obj A} {b b' : Obj B } → { f : Hom B (FObj F a) b } → { k : Hom B b b' } → - A [ left ( B [ k o f ] ) ≈ A [ FMap U k o left f ] ] - left-commute1 {a} {b} {b'} {f} {k} = let open ≈-Reasoning (A) in + A [ right ( B [ k o f ] ) ≈ A [ FMap U k o right f ] ] + right-commute1 {a} {b} {b'} {f} {k} = let open ≈-Reasoning (A) in begin - left ( B [ k o f ] ) + right ( B [ k o f ] ) ≈⟨⟩ FMap U ( B [ k o f ] ) o (TMap η a) ≈⟨ car (distr U) ⟩ @@ -503,14 +503,14 @@ ≈↑⟨ assoc ⟩ FMap U k o ( FMap U f o (TMap η a) ) ≈⟨⟩ - FMap U k o left f + FMap U k o right f ∎ - left-commute2 : {a a' : Obj A} {b : Obj B } → + right-commute2 : {a a' : Obj A} {b : Obj B } → { f : Hom B (FObj F a) b } → { h : Hom A a' a} → - A [ left ( B [ f o FMap F h ] ) ≈ A [ left f o h ] ] - left-commute2 {a'} {a} {b} {f} {h} = let open ≈-Reasoning (A) in + A [ right ( B [ f o FMap F h ] ) ≈ A [ right f o h ] ] + right-commute2 {a'} {a} {b} {f} {h} = let open ≈-Reasoning (A) in begin - left ( B [ f o FMap F h ] ) + right ( B [ f o FMap F h ] ) ≈⟨⟩ FMap U ( B [ f o FMap F h ] ) o TMap η a ≈⟨ car (distr U ) ⟩ @@ -522,12 +522,12 @@ ≈⟨ assoc ⟩ ( FMap U f o TMap η a') o h ≈⟨⟩ - left f o h + right f o h ∎ - r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } → A [ f ≈ g ] → B [ right f ≈ right g ] + r-cong : {a : Obj A} { b : Obj B } → { f g : Hom A a ( FObj U b ) } → A [ f ≈ g ] → B [ left f ≈ left g ] r-cong eq = let open ≈-Reasoning (B) in ( cdr ( fcong F eq ) ) - l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b } → B [ f ≈ g ] → A [ left f ≈ left g ] + l-cong : {a : Obj A} { b : Obj B } → { f g : Hom B (FObj F a) b } → B [ f ≈ g ] → A [ right f ≈ right g ] l-cong eq = let open ≈-Reasoning (A) in ( car ( fcong U eq ) ) @@ -535,32 +535,32 @@ -- f : a ----------→ U(b) -- 1_F(a) :F(a) --------→ F(a) --- ε(b) = right uo (1_F(a)) :UF(b)--------→ a --- η(a) = left uo (1_U(a)) : a ----------→ FU(a) +-- ε(b) = left uo (1_F(a)) :UF(b)--------→ a +-- η(a) = right uo (1_U(a)) : a ----------→ FU(a) uo-η-map : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Functor A B ) → ( uo : UnityOfOppsite A B U F) → (a : Obj A ) → Hom A a (FObj U ( FObj F a )) -uo-η-map A B U F uo a = left uo ( id1 B (FObj F a) ) +uo-η-map A B U F uo a = right uo ( id1 B (FObj F a) ) uo-ε-map : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Functor A B ) → ( uo : UnityOfOppsite A B U F) → (b : Obj B ) → Hom B (FObj F ( FObj U ( b ) )) b -uo-ε-map A B U F uo b = right uo ( id1 A (FObj U b) ) +uo-ε-map A B U F uo b = left uo ( id1 A (FObj U b) ) uo-solution : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) ( F : Functor A B ) → ( uo : UnityOfOppsite A B U F) → {a : Obj A} {b : Obj B } → ( f : Hom A a (FObj U b )) → Hom B (FObj F a) b -uo-solution A B U F uo {a} {b} f = -- B [ right uo (id1 A (FObj U b)) o FMap F f ] - right uo f +uo-solution A B U F uo {a} {b} f = -- B [ left uo (id1 A (FObj U b)) o FMap F f ] + left uo f -- F(ε(b)) o η(F(b)) --- F( right uo (id1 A (FObj U b)) ) o left uo (id1 B (FObj F a)) ] == 1 +-- F( left uo (id1 A (FObj U b)) ) o right uo (id1 B (FObj F a)) ] == 1 UO2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') ( U : Functor B A ) @@ -581,15 +581,15 @@ begin FMap U ( uo-solution A B U F uo f) o ( uo-η-map A B U F uo ) a ≈⟨⟩ - FMap U ( right uo f) o left uo ( id1 B (FObj F a) ) - ≈↑⟨ left-commute1 uo ⟩ - left uo ( B [ right uo f o id1 B (FObj F a) ] ) + FMap U ( left uo f) o right uo ( id1 B (FObj F a) ) + ≈↑⟨ right-commute1 uo ⟩ + right uo ( B [ left uo f o id1 B (FObj F a) ] ) ≈⟨ l-cong uo lemma-1 ⟩ - left uo ( right uo f ) - ≈⟨ right-injective uo ⟩ + right uo ( left uo f ) + ≈⟨ left-injective uo ⟩ f ∎ where - lemma-1 : B [ B [ right uo f o id1 B (FObj F a) ] ≈ right uo f ] + lemma-1 : B [ B [ left uo f o id1 B (FObj F a) ] ≈ left uo f ] lemma-1 = let open ≈-Reasoning (B) in idR uniqueness : {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } → { g : Hom B (FObj F a') b'} → A [ A [ FMap U g o ( uo-η-map A B U F uo ) a' ] ≈ f ] → B [ uo-solution A B U F uo f ≈ g ] @@ -597,12 +597,12 @@ begin uo-solution A B U F uo f ≈⟨⟩ - right uo f + left uo f ≈↑⟨ r-cong uo eq ⟩ - right uo ( A [ FMap U g o left uo ( id1 B (FObj F a) ) ] ) - ≈↑⟨ r-cong uo ( left-commute1 uo ) ⟩ - right uo ( left uo ( g o ( id1 B (FObj F a) ) ) ) - ≈⟨ left-injective uo ⟩ + left uo ( A [ FMap U g o right uo ( id1 B (FObj F a) ) ] ) + ≈↑⟨ r-cong uo ( right-commute1 uo ) ⟩ + left uo ( right uo ( g o ( id1 B (FObj F a) ) ) ) + ≈⟨ right-injective uo ⟩ g o ( id1 B (FObj F a) ) ≈⟨ idR ⟩ g @@ -620,15 +620,15 @@ → A [ A [ (FMap U (FMap F f)) o ( η a ) ] ≈ A [ (η b ) o f ] ] commute {a} {b} {f} = let open ≈-Reasoning (A) in begin - (FMap U (FMap F f)) o (left uo ( id1 B (FObj F a) ) ) - ≈↑⟨ left-commute1 uo ⟩ - left uo ( B [ (FMap F f) o ( id1 B (FObj F a) ) ] ) + (FMap U (FMap F f)) o (right uo ( id1 B (FObj F a) ) ) + ≈↑⟨ right-commute1 uo ⟩ + right uo ( B [ (FMap F f) o ( id1 B (FObj F a) ) ] ) ≈⟨ l-cong uo (IsCategory.identityR (Category.isCategory B)) ⟩ - left uo ( FMap F f ) + right uo ( FMap F f ) ≈↑⟨ l-cong uo (IsCategory.identityL (Category.isCategory B)) ⟩ - left uo ( B [ ( id1 B (FObj F b )) o FMap F f ] ) - ≈⟨ left-commute2 uo ⟩ - (left uo ( id1 B (FObj F b) ) ) o f + right uo ( B [ ( id1 B (FObj F b )) o FMap F f ] ) + ≈⟨ right-commute2 uo ⟩ + (right uo ( id1 B (FObj F b) ) ) o f ≈⟨⟩ (η b ) o f ∎ where @@ -651,15 +651,15 @@ sym ( begin ε b o (FMap F (FMap U f)) ≈⟨⟩ - right uo ( id1 A (FObj U b) ) o (FMap F (FMap U f)) - ≈⟨ right-commute2 uo ⟩ - right uo ( A [ id1 A (FObj U b) o FMap U f ] ) + left uo ( id1 A (FObj U b) ) o (FMap F (FMap U f)) + ≈⟨ left-commute2 uo ⟩ + left uo ( A [ id1 A (FObj U b) o FMap U f ] ) ≈⟨ r-cong uo (IsCategory.identityL (Category.isCategory A)) ⟩ - right uo ( FMap U f ) + left uo ( FMap U f ) ≈↑⟨ r-cong uo (IsCategory.identityR (Category.isCategory A)) ⟩ - right uo ( A [ FMap U f o id1 A (FObj U a) ] ) - ≈↑⟨ right-commute1 uo ⟩ - f o right uo ( id1 A (FObj U a) ) + left uo ( A [ FMap U f o id1 A (FObj U a) ] ) + ≈↑⟨ left-commute1 uo ⟩ + f o left uo ( id1 A (FObj U a) ) ≈⟨⟩ f o (ε a) ∎ ) @@ -689,12 +689,12 @@ begin ( FMap U ( TMap (uo-ε A B U F uo) b )) o ( TMap (uo-η A B U F uo) ( FObj U b )) ≈⟨⟩ - FMap U (right uo (id1 A (FObj U b))) o (left uo (id1 B (FObj F (FObj U b)))) - ≈↑⟨ left-commute1 uo ⟩ - left uo ( B [ right uo (id1 A (FObj U b)) o id1 B (FObj F (FObj U b)) ] ) + FMap U (left uo (id1 A (FObj U b))) o (right uo (id1 B (FObj F (FObj U b)))) + ≈↑⟨ right-commute1 uo ⟩ + right uo ( B [ left uo (id1 A (FObj U b)) o id1 B (FObj F (FObj U b)) ] ) ≈⟨ l-cong uo ((IsCategory.identityR (Category.isCategory B))) ⟩ - left uo ( right uo (id1 A (FObj U b)) ) - ≈⟨ right-injective uo ⟩ + right uo ( left uo (id1 A (FObj U b)) ) + ≈⟨ left-injective uo ⟩ id1 A (FObj U b) ∎ adjoint2 : {a : Obj A} → @@ -703,12 +703,12 @@ begin ( TMap (uo-ε A B U F uo) ( FObj F a )) o ( FMap F ( TMap (uo-η A B U F uo) a )) ≈⟨⟩ - right uo (Category.Category.Id A) o FMap F (left uo (id1 B (FObj F a))) - ≈⟨ right-commute2 uo ⟩ - right uo ( A [ (Category.Category.Id A) o (left uo (id1 B (FObj F a))) ] ) + left uo (Category.Category.Id A) o FMap F (right uo (id1 B (FObj F a))) + ≈⟨ left-commute2 uo ⟩ + left uo ( A [ (Category.Category.Id A) o (right uo (id1 B (FObj F a))) ] ) ≈⟨ r-cong uo ((IsCategory.identityL (Category.isCategory A))) ⟩ - right uo ( left uo (id1 B (FObj F a))) - ≈⟨ left-injective uo ⟩ + left uo ( right uo (id1 B (FObj F a))) + ≈⟨ right-injective uo ⟩ id1 B (FObj F a) ∎