Sets is CCC
author Shinji KONO Fri, 19 Apr 2019 23:42:19 +0900 a5f2ca67e7c5
line wrap: on
line source
```
-- Category A
-- A = Category
-- Functor T : A → A
--T(a) = t(a)
--T(f) = tf(f)

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

----
--
--
----

open NTrans
open Functor

UεF :  {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
( U : Functor B A )
( F : Functor A B )
( ε : NTrans B B  ( F ○  U ) identityFunctor ) → NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
UεF A B U F ε =  lemma11  (
Functor*Nat A {B} A U {( F ○ U) ○ F} {identityFunctor ○ F} ( Nat*Functor A {B} B { F ○  U} {identityFunctor} ε F)  ) where
lemma11 :   NTrans A A   ( U ○ ((F  ○  U) ○  F )) ( U ○  (identityFunctor ○ F) )
→  NTrans A A  (( U ○  F ) ○ ( U ○  F )) ( U ○  F )
lemma11  n = record { TMap = \a → TMap n a; isNTrans = record { commute = IsNTrans.commute ( isNTrans n ) }}

Adj2Monad : {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁ c₂ ℓ) (B : Category c₁' c₂' ℓ')
T = T ;
η = η ;
μ = μ ;
assoc = assoc1;
unity1 = unity1;
unity2 = unity2
}
}  where
U : Functor B A
F : Functor A B
η : NTrans A A identityFunctor ( U ○  F )
ε : NTrans B B  ( F ○  U ) identityFunctor
T : Functor A A
T = U  ○ F
μ : NTrans A A ( T ○ T ) T
μ = UεF A B U F ε
lemma-assoc1 : {a b : Obj B} → ( f : Hom B a b) →
B [ B [ f o TMap ε a ] ≈ B [ TMap ε b o FMap F (FMap U f ) ] ]
lemma-assoc1 f =  IsNTrans.commute ( isNTrans ε )
assoc1 : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
assoc1 {a} = let open ≈-Reasoning (A) in
begin
TMap μ a o TMap μ ( FObj T a )
≈⟨⟩
(FMap U (TMap ε ( FObj F a ))) o (FMap U (TMap ε ( FObj F ( FObj U (FObj F  a )))))
≈⟨ sym (distr U) ⟩
FMap U (B [ TMap ε ( FObj F a )  o TMap ε ( FObj F ( FObj U (FObj F a ))) ] )
≈⟨  (IsFunctor.≈-cong (isFunctor U)) (lemma-assoc1 ( TMap ε (FObj F a ))) ⟩
FMap U (B [ (TMap ε ( FObj F a )) o FMap F (FMap U (TMap ε ( FObj F a ))) ] )
≈⟨ distr U ⟩
(FMap U (TMap ε ( FObj F a ))) o FMap U (FMap F (FMap U (TMap ε ( FObj F a ))))
≈⟨⟩
TMap μ a o FMap T (TMap μ a)
∎
unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
unity1 {a} = let open ≈-Reasoning (A) in
begin
TMap μ a o TMap η ( FObj T a )
≈⟨⟩
(FMap U (TMap ε ( FObj F a ))) o TMap η ( FObj U ( FObj F  a ))
id (FObj U ( FObj F a ))
≈⟨⟩
id (FObj T a)
∎
unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]
unity2 {a} = let open ≈-Reasoning (A) in
begin
TMap μ a o (FMap T (TMap η a ))
≈⟨⟩
(FMap U (TMap ε ( FObj F a ))) o (FMap U ( FMap F (TMap η a )))
≈⟨ sym (distr U ) ⟩
FMap U ( B [  (TMap ε ( FObj F a )) o ( FMap F (TMap η a )) ])