### view universal-mapping.agda @ 790:1e7319868d77

Sets is CCC
author Shinji KONO Fri, 19 Apr 2019 23:42:19 +0900 06a7831cf6ce
line wrap: on
line source
```
module universal-mapping where

-- Shinji KONO <kono@ie.u-ryukyu.ac.jp>

open import Category -- https://github.com/konn/category-agda
open import Level
open import HomReasoning
open import cat-utility
open import Category.Cat

open Functor
open NTrans

--
--   Adjunction yields solution of universal mapping
--
--

Adj2UM : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
_* = solution  ;
isUniversalMapping = record {
universalMapping  = universalMapping;
uniquness = uniqueness
}
} where
U : Functor B A
F : Functor A B
η : NTrans A A identityFunctor ( U ○  F )
ε : NTrans B B  ( F ○  U ) identityFunctor
solution :  { a : Obj A} { b : Obj B} → ( f : Hom A a (FObj U b) ) →  Hom B (FObj F a ) b
solution  {_} {b} f = B [ TMap ε b o FMap F f ]
universalMapping :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } →
A [ A [ FMap U ( solution f) o TMap η a' ]  ≈ f ]
universalMapping {a} {b} {f} =
let open ≈-Reasoning (A) in
begin
FMap U ( solution  f) o TMap η a
≈⟨⟩
FMap U (  B [ TMap ε b o FMap F f ] ) o TMap η a
≈⟨ car (distr U ) ⟩
( (FMap U (TMap ε b))  o (FMap U ( FMap F f )) ) o TMap η a
≈⟨ sym assoc ⟩
(FMap U (TMap ε b))  o ((FMap U ( FMap F f ))  o TMap η a )
≈⟨ cdr (nat η) ⟩
(FMap U (TMap ε b))  o ((TMap η (FObj U b )) o f )
≈⟨ assoc ⟩
((FMap U (TMap ε b))  o (TMap η (FObj U b)))  o f
id (FObj U b) o f
≈⟨  idL  ⟩
f
∎
lemma1 : (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  TMap η a ]  ≈ f ] →
B [  (FMap F (A [ FMap U g o TMap η a ] )) ≈ FMap F f ]
lemma1 a b f g k = IsFunctor.≈-cong (isFunctor F) k
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  TMap η a' ]  ≈ f ] → B [ solution f  ≈ g ]
uniqueness {a} {b} {f} {g} k = let open ≈-Reasoning (B) in
begin
solution f
≈⟨⟩
TMap ε b o FMap F f
≈⟨ cdr (sym ( lemma1 a b f g k )) ⟩
TMap ε b o FMap F ( A [ FMap U g o  TMap η a ] )
≈⟨ cdr (distr F )  ⟩
TMap ε b o ( FMap F ( FMap U g)  o FMap F ( TMap η a ) )
≈⟨ assoc  ⟩
( TMap ε b o  FMap F ( FMap U g) ) o FMap F ( TMap η a )
≈⟨ sym ( car ( nat ε ))  ⟩
( g o TMap ε ( FObj F a) )  o FMap F ( TMap η a )
≈⟨ sym assoc ⟩
g o ( TMap ε ( FObj F a)   o FMap F ( TMap η a ) )
g o id (FObj F a)
≈⟨ idR ⟩
g
∎

--
--
--
--

--
-- F is an functor
--

FunctorF : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
{ U : Functor B A }
→ UniversalMapping A B  U → Functor A B
FunctorF A B {U} um = record {
FObj = F;
FMap = myFMap ;
isFunctor = myIsFunctor
} where
F : Obj A → Obj B
F = UniversalMapping.F um
η : (a : Obj A) → Hom A a ( FObj U (F a) )
η = UniversalMapping.η um
_* : (UniversalMapping A B U ) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
_* _ = UniversalMapping._* um
myFMap : {a b : Obj A} → Hom A a b → Hom B (F a) (F b)
myFMap f = (_* um)  (A [  η (Category.cod A f )   o f ])
lemma-id1 :  {a : Obj A} →  A [ A [ FMap U (id1 B (F a))  o  η a ]  ≈ (A [ (η a) o (id1 A a) ]) ]
lemma-id1 {a} = let open ≈-Reasoning (A) in
begin
FMap U (id1 B (F a))  o  η a
≈⟨ ( car ( IsFunctor.identity ( isFunctor U )))  ⟩
id (FObj U ( F a )) o  η a
≈⟨ idL  ⟩
η a
≈⟨ sym idR  ⟩
η a o id a
∎
lemma-id :  {a : Obj A} →  B [ ( (_* um) (A [ (η a) o (id1 A a)] )) ≈ (id1 B (F a)) ]
lemma-id {a} =   ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) ) lemma-id1
lemma-cong2 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] →
A [ A [ FMap U ((_* um) (A [ η b  o  g ]) ) o  η a ] ≈  A [ η b  o  f ] ]
lemma-cong2 a b f g eq =  let open ≈-Reasoning (A) in
begin
( FMap U ((_* um) (A [ η b  o  g ]) )) o  η a
≈⟨  ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um ))  ⟩
η b  o  g
≈⟨ ( IsCategory.o-resp-≈ ( Category.isCategory A ) (sym eq) (refl-hom)  ) ⟩
η b  o  f
∎
lemma-cong1 : (a b : Obj A) (f g : Hom A a b) → A [ f ≈ g ] → B [ (_* um) (A [ η b  o  f ] ) ≈  (_* um) (A [ η b  o  g ]) ]
lemma-cong1 a b f g eq = ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um ) ) ( lemma-cong2 a b f g eq )
lemma-cong :  {a b : Obj A} {f g : Hom A a b} → A [ f ≈ g ] → B [ myFMap f ≈ myFMap g ]
lemma-cong {a} {b} {f} {g} eq = lemma-cong1 a b f g eq
lemma-distr2 :  (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) →
A [ A [ FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ])  o  η a ] ≈ (A [ η c o A [ g o f ] ]) ]
lemma-distr2 a b c f g = let open ≈-Reasoning (A) in
begin
( FMap U (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ] ) )  o  η a
≈⟨ car (distr U )  ⟩
(( FMap U ((_* um) (A [ η c o g ])) o ( FMap U ((_* um)( A [ η b  o f ])))) )   o  η a
≈⟨ sym assoc ⟩
( FMap U ((_* um) (A [ η c o g ])) o (( FMap U ((_* um)( A [ η b  o f ]))))   o  η a )
≈⟨ cdr ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um ))  ⟩
( FMap U ((_* um) (A [ η c o g ])) o ( η b  o f) )
≈⟨ assoc ⟩
( FMap U ((_* um) (A [ η c o g ])) o  η b)  o f
≈⟨ car ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um ))  ⟩
(  η c o g )  o f
≈⟨ sym assoc  ⟩
η c o ( g o f )
∎
lemma-distr1 :  (a b c : Obj A) (f : Hom A a b) (g : Hom A b c) →
B [ (_* um) (A [ η c o A [ g o f ] ]) ≈ (B [(_* um) (A [ η c o g ]) o (_* um)( A [ η b  o f ]) ] )]
lemma-distr1 a b c f g =  ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um )) (lemma-distr2 a b c f g )
lemma-distr :  {a b c : Obj A} {f : Hom A a b} {g : Hom A b c} → B [ myFMap (A [ g o f ]) ≈ (B [ myFMap g o myFMap f ] )]
lemma-distr {a} {b} {c} {f} {g} = lemma-distr1 a b c f g
myIsFunctor : IsFunctor A B F myFMap
myIsFunctor =
record { ≈-cong   = lemma-cong
; identity = lemma-id
; distr    = lemma-distr
}

--
-- naturality of η
--
nat-η : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
{ U : Functor B A }
→ (um : UniversalMapping A B  U )  →
NTrans  A A identityFunctor ( U ○ FunctorF A B um )
nat-η A B {U} um = record {
TMap = η ; isNTrans = myIsNTrans
} where
F : Obj A → Obj B
F = UniversalMapping.F um
η : (a : Obj A) → Hom A a ( FObj U (F a) )
η = UniversalMapping.η um
F' : Functor A B
F' = FunctorF A B um
_* : (UniversalMapping A B U ) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
_* _ = UniversalMapping._* um
commute :  {a b : Obj A} {f : Hom A a b}
→ 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  ( η a )
≈⟨⟩
(FMap U ((_* um)  (A [  η b  o f ])))   o  ( η a )
≈⟨ (IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um ))  ⟩
(η b ) o f
∎
myIsNTrans : IsNTrans A A identityFunctor ( U ○  F' ) η
myIsNTrans = record { commute = commute }

nat-ε : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
{ U : Functor B A }
→ (um : UniversalMapping A B  U )  →
NTrans B B ( FunctorF A B um ○ U ) identityFunctor
nat-ε A B {U} um = record {
TMap = ε ; isNTrans = myIsNTrans
} where
F : Obj A → Obj B
F = UniversalMapping.F um
η : (a : Obj A) → Hom A a ( FObj U (F a) )
η = UniversalMapping.η um
F' : Functor A B
F' = FunctorF A B um
_* : (UniversalMapping A B U ) →  { a : Obj A} { b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (F a ) b
_* _ = UniversalMapping._* um
ε : ( b : Obj B ) → Hom B ( FObj F' ( FObj U b) ) b
ε b = (_* um) ( id1 A (FObj U b))
lemma-nat1 :  (a b : Obj B) (f : Hom B a b ) →
A [ A [ FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) (A [ η (FObj U b) o FMap U f ])) ] )  o η (FObj U a) ]
≈ A [ FMap U f o id1 A (FObj U a) ] ]
lemma-nat1 a b f = let open ≈-Reasoning (A) in
begin
FMap U ( B [ (um *) (id1 A (FObj U b)) o ((um *) ( η (FObj U b) o FMap U f )) ] )  o η (FObj U a)
≈⟨ car ( distr U  ) ⟩
( FMap U  ((um *) (id1 A (FObj U b))) o FMap U ((um *) ( η (FObj U b) o FMap U f )) )  o η (FObj U a)
≈⟨ sym assoc  ⟩
FMap U  ((um *) (id1 A (FObj U b))) o ( FMap U ((um *) ( η (FObj U b) o FMap U f )))  o η (FObj U a)
≈⟨ cdr ((IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) )  ⟩
FMap U  ((um *) (id1 A (FObj U b))) o ( η (FObj U b) o FMap U f )
≈⟨ assoc  ⟩
(FMap U  ((um *) (id1 A (FObj U b))) o  η (FObj U b)) o FMap U f
≈⟨ car ((IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um )) ) ⟩
id1 A (FObj U b) o FMap U f
≈⟨ idL ⟩
FMap U f
≈⟨ sym idR ⟩
FMap U f o id (FObj U a)
∎
lemma-nat2 : (a b : Obj B) (f : Hom B a b ) → A [ A [ FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ] ) o η (FObj U a) ]
≈ A [ FMap U f o id1 A (FObj U a) ] ]
lemma-nat2 a b f = let open ≈-Reasoning (A) in
begin
FMap U ( B [ f o ((um *) (id1 A (FObj U a ))) ])  o η (FObj U a)
≈⟨ car ( distr U  ) ⟩
(FMap U f o FMap U ((um *) (id1 A (FObj U a ))))  o η (FObj U a)
≈⟨ sym assoc  ⟩
FMap U f o ( FMap U ((um *) (id1 A (FObj U a )))  o η (FObj U a)  )
≈⟨ cdr ( IsUniversalMapping.universalMapping ( UniversalMapping.isUniversalMapping um)) ⟩
FMap U f o id (FObj U a )
∎
commute : {a b : Obj B} {f : Hom B a b }
→  B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F' (FMap U f)) ] ]
commute {a} {b} {f} = let open ≈-Reasoning (B) in
sym ( begin
ε b o (FMap F' (FMap U f))
≈⟨⟩
ε b o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
≈⟨⟩
((_* um) ( id1 A (FObj U b))) o ((_* um) (A [ η (FObj U b) o (FMap U f) ]))
≈⟨ sym ( ( IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um )  (lemma-nat1 a b f))) ⟩
(_* um) ( A [ FMap U f o id1 A (FObj U a) ] )
≈⟨ (IsUniversalMapping.uniquness ( UniversalMapping.isUniversalMapping um )  (lemma-nat2 a b f)) ⟩
f o  ((_* um) ( id1 A (FObj U a)))
≈⟨⟩
f o  (ε a)
∎ )
myIsNTrans : IsNTrans B B ( F' ○ U ) identityFunctor　ε
myIsNTrans = record { commute = commute }

------
--
--   Adjunction Construction from Universal Mapping
--
-----

UMAdjunction : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ') →
( U : Functor B A ) →
(um : UniversalMapping A B U )  →
UMAdjunction A B U um = record {
U = U  ;
F = FunctorF A B um ;
η = nat-η A B um ;
ε = nat-ε A B um ;
}
} where
F' : Obj A → Obj B
F' = UniversalMapping.F um
η' : (a : Obj A) → Hom A a ( FObj U (F' a) )
η' = UniversalMapping.η um
F : Functor A B
F = FunctorF A B um
η : NTrans A A identityFunctor ( U ○  F )
η = nat-η A B um
ε : NTrans B B  ( F ○  U ) identityFunctor
ε = nat-ε A B um
_* : UniversalMapping A B  U  →  { a : Obj A}{ b : Obj B} → ( Hom A a (FObj U b) ) →  Hom B (FObj F a ) b
_* _ = UniversalMapping._* um
isUniversalMapping = UniversalMapping.isUniversalMapping
adjoint1 :   { b : Obj B } →
A [ A [ ( FMap U ( TMap ε b ))  o ( TMap η ( FObj U b )) ]  ≈ id1 A (FObj U b) ]
adjoint1 {b} = let open ≈-Reasoning (A) in
begin
FMap U ( TMap ε b )  o  TMap η ( FObj U b )
≈⟨⟩
FMap U ((_* um) ( id1 A (FObj U b)))  o  η' ( FObj U b )
≈⟨ IsUniversalMapping.universalMapping ( isUniversalMapping um )  ⟩
id (FObj U b)
∎
lemma-adj1 : (a : Obj A) →
A [ A [ FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a ]
≈ (η' a) ]
lemma-adj1 a =  let open ≈-Reasoning (A) in
begin
FMap U ((B [((_* um) ( id1 A (FObj U ( FObj F a )))) o (_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]) ])) o η' a
≈⟨ car (distr U)  ⟩
(FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o FMap U ((_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ]))) o η' a
≈⟨ sym assoc ⟩
FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( FMap U ((_* um) (A [  η' (FObj U ( FObj F a )) o ( η' a ) ])) o η' a )
≈⟨ cdr (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )) o ( η' a ) )
≈⟨ assoc ⟩
(FMap U ((_* um) ( id1 A (FObj U ( FObj F a)))) o ( η' (FObj U ( FObj F a )))) o ( η' a )
≈⟨ car (IsUniversalMapping.universalMapping ( isUniversalMapping um)) ⟩
id (FObj U ( FObj F a)) o ( η' a )
≈⟨ idL ⟩
η' a
∎
lemma-adj2 : (a : Obj A) → A [ A [ FMap U (id1 B (FObj F a)) o η' a ] ≈  η' a ]
lemma-adj2 a = let open ≈-Reasoning (A) in
begin
FMap U (id1 B (FObj F a)) o η' a
≈⟨  car ( IsFunctor.identity ( isFunctor U))  ⟩
id (FObj U (FObj F a)) o η' a
≈⟨ idL ⟩
η' a
∎
adjoint2 :   {a : Obj A} →
B [ B [ ( TMap ε ( FObj F a ))  o ( FMap F ( TMap η a )) ]  ≈ id1 B (FObj F a) ]
adjoint2 {a} = let open ≈-Reasoning (B) in
begin
TMap ε ( FObj F a )  o  FMap F ( TMap η a )
≈⟨⟩
((_* um) ( id1 A (FObj U ( FObj F a ))))  o  (_* um)  (A [  η' (FObj U ( FObj F a ))   o ( η' a ) ])
≈⟨ sym ( ( IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-adj1 a))) ⟩
(_* um)( η' a )
≈⟨  IsUniversalMapping.uniquness ( isUniversalMapping um )  (lemma-adj2 a) ⟩
id1 B (FObj F a)
∎

------
--
--
--   Hom(F(-),-) = Hom(-,U(-))
--       Unity of opposite
-----

--  Assuming
--     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               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₂' ℓ')
( U : Functor B A )
( F : Functor A B )
: Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁' ⊔ c₂' ⊔ ℓ' )) where
field
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 Φ
right-commute1 : {a : Obj A} {b b' : Obj B } →
{ f : Hom B (FObj F a) b }  → { k : Hom B b 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 [ 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  left g ]   ≈ left ( A [ FMap U k o g  ] ) ]
left-commute1 {a} {b} {b'} {g} {k} =  let open ≈-Reasoning (B) in
begin
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) ⟩
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 right ( left g ) ]   ≈  A [ FMap U k o g  ] ]
lemma-1 g k = let open ≈-Reasoning (A) in
begin
FMap U k o right ( left g )
≈⟨ cdr ( left-injective) ⟩
FMap U k o g
∎
left-commute2 : {a a' : Obj A} {b : Obj B } →
{ g : Hom A a (FObj U b) }  → { h : Hom A a' a } →
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
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  ) ⟩
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 [  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₂' ℓ')
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
U : Functor B A
F : Functor A B
η : NTrans A A identityFunctor ( U ○  F )
ε : NTrans B B  ( F ○  U ) identityFunctor
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 ) ⟩
( FMap U (TMap ε b) o FMap U (FMap F f )) o (TMap η a)
≈↑⟨ assoc  ⟩
FMap U (TMap ε b) o ( FMap U (FMap F f ) o (TMap η a) )
≈⟨ cdr ( nat η)  ⟩
FMap U (TMap ε b) o ((TMap η (FObj U b))  o f )
≈⟨ assoc  ⟩
(FMap U (TMap ε b) o (TMap η (FObj U b)))  o f
id1 A (FObj U b) o f
≈⟨ idL  ⟩
f
∎
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 ) ⟩
TMap ε b o ( FMap F (FMap U f) o FMap F (TMap η a))
≈⟨ assoc  ⟩
( TMap ε b o FMap F (FMap U f)) o FMap F (TMap η a)
≈↑⟨ car (nat ε)  ⟩
( f  o TMap ε ( FObj F a )) o ( FMap F ( TMap η a ))
≈↑⟨ assoc  ⟩
f  o ( TMap ε ( FObj F a ) o ( FMap F ( TMap η a )))
f o id1 B (FObj F a)
≈⟨ idR  ⟩
f
∎
right-commute1 : {a : Obj A} {b b' : Obj B } →
{ f : Hom B (FObj F a) b }  → { k : Hom B b b' } →
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
right ( B [ k o  f ] )
≈⟨⟩
FMap U  ( B [ k o  f ] ) o (TMap η a)
≈⟨ car (distr U) ⟩
( FMap U k o  FMap U f ) o (TMap η a)
≈↑⟨ assoc ⟩
FMap U k o  ( FMap U f o (TMap η 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 [ 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
right ( B [ f  o  FMap F h ] )
≈⟨⟩
FMap U (  B [ f  o  FMap F h ] )  o TMap η a
≈⟨ car (distr U ) ⟩
(FMap U f  o  FMap U (FMap F h )) o TMap η a
≈↑⟨ assoc ⟩
FMap U f o  ( FMap U (FMap F h ) o TMap η a )
≈⟨ cdr ( nat η) ⟩
FMap U f o (TMap η a' o h )
≈⟨ assoc ⟩
( FMap U f  o TMap η a') 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 [ 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 [ right f ≈ right g   ]
l-cong eq = let open ≈-Reasoning (A) in ( car ( fcong U  eq ) )

open UnityOfOppsite

--   f                            : a ----------→ U(b)
--   1_F(a)                       :F(a) --------→ F(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 =  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 =  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  [ left uo (id1 A (FObj U b)) o FMap F f ]
left uo f

--     F(ε(b)) o η(F(b))
--     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 )
( F : Functor A B ) →
( uo : UnityOfOppsite A B U F)  → UniversalMapping A B U
UO2UM  A B U F uo = record {
F = FObj F ;
η = uo-η-map A B U F uo ;
_* = uo-solution A B U F uo  ;
isUniversalMapping = record {
universalMapping  = universalMapping;
uniquness = uniqueness
}
} where
universalMapping :   {a' : Obj A} { b' : Obj B } → { f : Hom A a' (FObj U b') } →
A [ A [ FMap U ( uo-solution A B U F uo f) o ( uo-η-map A B U F uo  ) a' ]  ≈ f ]
universalMapping {a} {b} {f}  = let open ≈-Reasoning (A) in
begin
FMap U ( uo-solution A B U F uo f) o ( uo-η-map A B U F uo  ) 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  ⟩
right uo ( left uo f )
≈⟨ left-injective uo ⟩
f
∎ where
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 ]
uniqueness {a} {b} {f} {g} eq = let open ≈-Reasoning (B) in
begin
uo-solution A B U F uo f
≈⟨⟩
left uo  f
≈↑⟨ r-cong uo eq ⟩
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
∎

uo-η  : {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)  → NTrans A A identityFunctor ( U ○  F )
uo-η A B U F uo = record {
TMap = uo-η-map A B U F uo  ; isNTrans = myIsNTrans
} where
η = uo-η-map A B U F uo
commute :  {a b : Obj A} {f : Hom A a b}
→ 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  (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))  ⟩
right uo ( FMap F f )
≈↑⟨ l-cong uo (IsCategory.identityL (Category.isCategory B))  ⟩
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
lemma-1 : B [ B [ (FMap F f)  o  ( id1 B (FObj F a) ) ]  ≈  FMap F f ]
lemma-1 = IsCategory.identityR (Category.isCategory B)
myIsNTrans : IsNTrans A A identityFunctor ( U ○  F ) η
myIsNTrans = record { commute = commute }

uo-ε  : {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)  → NTrans B B  ( F ○  U ) identityFunctor
uo-ε A B U F uo = record {
TMap = ε ; isNTrans = myIsNTrans
} where
ε  = uo-ε-map A B U F uo
commute : {a b : Obj B} {f : Hom B a b }
→  B [ B [ f o (ε a) ] ≈ B [(ε b) o (FMap F (FMap U f)) ] ]
commute {a} {b} {f} = let open ≈-Reasoning (B) in
sym ( begin
ε b o (FMap F (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))  ⟩
left uo (  FMap U f  )
≈↑⟨ r-cong uo (IsCategory.identityR (Category.isCategory 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)
∎  )
myIsNTrans : IsNTrans B B ( F ○ U ) identityFunctor　ε
myIsNTrans = record { commute = commute }

UO2Adj : {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)
UO2Adj A B {U} {F} uo = record {
U =  U ;
F =  F ;
η =  uo-η A B U F uo  ;
ε =  uo-ε A B U F uo ;
}
} where
um = UO2UM A B U F uo
adjoint1 :   { b : Obj B } →
A [ A [ ( FMap U ( TMap (uo-ε A B U F uo) b ))  o ( TMap (uo-η A B U F uo) ( FObj U b )) ]  ≈ id1 A (FObj U b) ]
adjoint1 {b} = let open ≈-Reasoning (A) in
begin
( FMap U ( TMap (uo-ε A B U F uo) b ))  o ( TMap (uo-η A B U F uo) ( 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))) ⟩
right uo ( left uo (id1 A (FObj U b))  )
≈⟨ left-injective uo ⟩
id1 A (FObj U b)
∎
adjoint2 :   {a : Obj A} →
B [ B [ ( TMap (uo-ε A B U F uo) ( FObj F a ))  o ( FMap F ( TMap (uo-η A B U F uo) a )) ]  ≈ id1 B (FObj F a) ]
adjoint2 {a} = let open ≈-Reasoning (B) in
begin
( TMap (uo-ε A B U F uo) ( FObj F a ))  o ( FMap F ( TMap (uo-η A B U F uo) 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))) ⟩
left uo ( right uo (id1 B (FObj F a)))
≈⟨  right-injective uo ⟩
id1 B (FObj F a)
∎

--  done!

```