Mercurial > hg > Members > kono > Proof > category

view nat.agda @ 30:98b8431a419b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 13 Jul 2013 18:12:57 +0900
parents 87cefecc5663
children 17b8bafebad7
line wrap: on
line source

module nat  where 

-- Monad
-- 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 Functor

--T(g f) = T(g) T(f)

Lemma1 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} (T : Functor A A) →  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
     → A [ ( FMap T (A [ g o f ] ))  ≈ (A [ FMap T g o FMap T f ]) ]
Lemma1 = \t → IsFunctor.distr ( isFunctor t )

--        F(f)
--   F(a) ---→ F(b)
--    |          |
--    |t(a)      |t(b)    G(f)t(a) = t(b)F(f)
--    |          |
--    v          v
--   G(a) ---→ G(b)
--        G(f)

record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′)
                 ( F G : Functor D C )
                 (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A))
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
  field
    naturality : {a b : Obj D} {f : Hom D a b} 
      → C [ C [ (  FMap G f ) o  ( TMap a ) ]  ≈ C [ (TMap b ) o  (FMap F f)  ] ]
--    uniqness : {d : Obj D} 
--      →  C [ TMap d  ≈ TMap d ]


record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain )
       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where
  field
    TMap :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
    isNTrans : IsNTrans domain codomain F G TMap

open NTrans
Lemma2 : {c₁ c₂ l : Level} {A : Category c₁ c₂ l} {F G : Functor A A} 
      → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b }
      → A [ A [  FMap G f o TMap μ a ]  ≈ A [ TMap μ b o  FMap F f ] ]
Lemma2 = \n → IsNTrans.naturality ( isNTrans  n  )

open import Category.Cat

-- η :   1_A → T
-- μ :   TT → T
-- μ(a)η(T(a)) = a
-- μ(a)T(η(a)) = a
-- μ(a)(μ(T(a))) = μ(a)T(μ(a))

record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
                 ( T : Functor A A )
                 ( η : NTrans A A identityFunctor T )
                 ( μ : NTrans A A (T ○ T) T)
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
   field
      assoc  : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈  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) ]
      unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ]

record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T)
       : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
  eta : NTrans A A identityFunctor T
  eta = η
  mu : NTrans A A (T ○ T) T
  mu = μ
  field
    isMonad : IsMonad A T η μ

open Monad
Lemma3 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { a : Obj A } →
                 ( M : Monad A T η μ )
    → A [ A [  TMap μ a o TMap μ ( FObj T a ) ] ≈  A [  TMap μ a o FMap T (TMap μ a) ] ]
Lemma3 = \m → IsMonad.assoc ( isMonad m )


Lemma4 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } { f : Hom A a b}
    → A [ A [ Id {_} {_} {_} {A} b o f ] ≈ f ]
Lemma4 = \a → IsCategory.identityL ( Category.isCategory a )

Lemma5 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { a : Obj A } →
                 ( M : Monad A T η μ )
    →  A [ A [ TMap μ a o TMap η ( FObj T a )  ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
Lemma5 = \m → IsMonad.unity1 ( isMonad m )

Lemma6 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { a : Obj A } →
                 ( M : Monad A T η μ )
    →  A [ A [ TMap μ a o (FMap T (TMap η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
Lemma6 = \m → IsMonad.unity2 ( isMonad m )

-- T = M x A
-- nat of η
-- g ○ f = μ(c) T(g) f
-- η(b) ○ f = f
-- f ○ η(a) = f
-- h ○ (g ○ f) = (h ○ g) ○ f

record Kleisli  { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ )
                 ( T : Functor A A )
                 ( η : NTrans A A identityFunctor T )
                 ( μ : NTrans A A (T ○ T) T )
                 ( M : Monad A T η μ ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
     monad : Monad A T η μ 
     monad = M
     -- g ○ f = μ(c) T(g) f
     join : { a b : Obj A } → ( c : Obj A ) →
                      ( Hom A b ( FObj T c )) → (  Hom A a ( FObj T b)) → Hom A a ( FObj T c )
     join c g f = A [ TMap μ c  o A [ FMap T g  o f ] ]



module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
  open import Relation.Binary.Core 

  _o_ :  {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b
  x o y = A [ x o y ]

  _≈_ :  {a b : Obj A }   → Rel (Hom A a b) ℓ
  x ≈ y = A [ x ≈ y ]

  infixr 9 _o_
  infix  4 _≈_

  refl-hom :   {a b : Obj A } { x : Hom A a b }  →  x ≈ x 
  refl-hom =  IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))

  trans-hom :   {a b : Obj A } { x y z : Hom A a b }  →
         x ≈ y →  y ≈ z  →  x ≈ z 
  trans-hom b c = ( IsEquivalence.trans (IsCategory.isEquivalence  ( Category.isCategory A ))) b c

  -- some short cuts

  car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } →
          x ≈ y  → ( x o f ) ≈ ( y  o f )
  car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom  ) eq

  cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } →
          x ≈ y  →  f o x  ≈  f  o y 
  cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom  ) 

  id :  (a  : Obj A ) →  Hom A a a
  id a =  (Id {_} {_} {_} {A} a) 

  idL :  {a b : Obj A } { f : Hom A b a } →  id a o f  ≈ f 
  idL =  IsCategory.identityL (Category.isCategory A)

  idR :  {a b : Obj A } { f : Hom A a b } →  f o id a  ≈ f 
  idR =  IsCategory.identityR (Category.isCategory A)

  sym :  {a b : Obj A } { f g : Hom A a b } →  f ≈ g  →  g ≈ f
  sym   =  IsEquivalence.sym (IsCategory.isEquivalence (Category.isCategory A))

  assoc :   {a b c d : Obj A }  {f : Hom A c d}  {g : Hom A b c} {h : Hom A a b}
                                  →  f o ( g o h )  ≈ ( f o g ) o h
  assoc =  IsCategory.associative (Category.isCategory A)

  distr :  (T : Functor A A) →  {a b c : Obj A} {g : Hom A b c} { f : Hom A a b }
     →   FMap T ( g o f  )  ≈  FMap T g o FMap T f 
  distr T = IsFunctor.distr ( isFunctor T )

  nat : { c₁′ c₂′ ℓ′ : Level}  (D : Category c₁′ c₂′ ℓ′) {a b : Obj D} {f : Hom D a b}  {F G : Functor D A }
      →  (η : NTrans D A F G )
      →   FMap G f  o  TMap η a   ≈ TMap η b  o  FMap F f
  nat _ η  =  IsNTrans.naturality ( isNTrans η  )


  infixr  2 _∎
  infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 
  infix  1 begin_

------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
--  ≈-to-≡ : {a b : Obj A } { x y : Hom A a b }  → A [ x ≈  y ] → x ≡ y
--  ≈-to-≡ refl-hom = refl

  data _IsRelatedTo_ { a b : Obj A } ( x y : Hom A a b ) :
                     Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
      relTo : (x≈y : x ≈ y ) → x IsRelatedTo y

  begin_ : { a b : Obj A } { x y : Hom A a b } →
           x IsRelatedTo y → x ≈ y 
  begin relTo x≈y = x≈y

  _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → 
           x ≈ y → y IsRelatedTo z → x IsRelatedTo z
  _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)

  _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y
  _ ≈⟨⟩ x∼y = x∼y

  _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x
  _∎ _ = relTo refl-hom

lemma12 :  {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } → 
       ( x : Hom L c a ) → ( y : Hom L b c ) → L [ L [ x o y ] ≈ L [ x o y ] ]
lemma12 L x y =  
   let open ≈-Reasoning ( L )  in 
      begin  L [ x o y ]  ∎

Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
                 { a : Obj A } ( b : Obj A ) →
                 ( f : Hom A a b )
                      →  A [ A [ (Id {_} {_} {_} {A} b) o f ]  ≈ f ]
Lemma61 c b g = -- IsCategory.identityL (Category.isCategory c) 
  let open ≈-Reasoning (c) in 
     begin  
          c [ Id {_} {_} {_} {c} b o g ]
     ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
          g
     ∎

open Kleisli
-- η(b) ○ f = f
Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) →
                 ( T : Functor A A )
                 ( η : NTrans A A identityFunctor T )
                 { μ : NTrans A A (T ○ T) T }
                 { a : Obj A } ( b : Obj A ) 
                 ( f : Hom A a ( FObj T b) )
                 ( m : Monad A T η μ )
                 ( k : Kleisli A T η μ m) 
                      → A  [ join k b (TMap η b) f  ≈ f ]
Lemma7 c T η b f m k = 
  let open ≈-Reasoning (c) 
      μ = mu ( monad k )
  in 
     begin  
         join k b (TMap η b) f 
     ≈⟨ refl-hom ⟩
         c [ TMap μ b  o c [ FMap T ((TMap η b)) o f ] ]  
     ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
        c [ c [ TMap μ b  o  FMap T ((TMap η b)) ] o f ]
     ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) )  ⟩
        c [  id (FObj T b)   o f ]
     ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
        f
     ∎

-- f ○ η(a) = f
Lemma8 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
                 ( T : Functor A A )
                 ( η : NTrans A A identityFunctor T )
                 { μ : NTrans A A (T ○ T) T }
                 ( a  : Obj A )  ( b : Obj A )
                 ( f : Hom A a ( FObj T b) )
                 ( m : Monad A T η μ )
                 ( k : Kleisli A T η μ m) 
                      → A  [ join k b f (TMap η a)  ≈ f ]
Lemma8 c T η a b f m k = 
  begin
     join k b f (TMap η a) 
  ≈⟨ refl-hom ⟩
     c [ TMap μ b  o c [  FMap T f o (TMap η a) ] ]  
  ≈⟨ cdr  ( IsNTrans.naturality ( isNTrans η  )) ⟩
     c [ TMap μ b  o c [ (TMap η ( FObj T b)) o f ] ] 
  ≈⟨ IsCategory.associative (Category.isCategory c) ⟩
     c [ c [ TMap μ b  o (TMap η ( FObj T b)) ] o f ] 
  ≈⟨ car ( IsMonad.unity1 ( isMonad ( monad k )) ) ⟩
     c [ id (FObj T b)  o f ]
  ≈⟨  IsCategory.identityL (Category.isCategory c)  ⟩
     f
  ∎  where 
      open ≈-Reasoning (c) 
      μ = mu ( monad k )

-- h ○ (g ○ f) = (h ○ g) ○ f
Lemma9 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
                 ( T : Functor A A )
                 ( η : NTrans A A identityFunctor T )
                 ( μ : NTrans A A (T ○ T) T )
                 ( a b c d : Obj A )
                 ( f : Hom A a ( FObj T b) )
                 ( g : Hom A b ( FObj T c) ) 
                 ( h : Hom A c ( FObj T d) )
                 ( m : Monad A T η μ )
                 ( k : Kleisli A T η μ m)
                      → A  [ join k d h (join k c g f)  ≈ join k d ( join k d h g) f ]
Lemma9 A T η μ a b c d f g h m k = 
  begin 
     join k d h (join k c g f)  
   ≈⟨⟩
     join k d h (                  ( TMap μ c o ( FMap T g o f ) ) )
   ≈⟨ refl-hom ⟩
     ( TMap μ d  o ( FMap T h  o  ( TMap μ c o ( FMap T g  o f ) ) ) )
   ≈⟨ cdr ( cdr ( assoc )) ⟩
     ( TMap μ d  o ( FMap T h o ( ( TMap μ c o  FMap T g )  o f ) ) )
   ≈⟨ assoc  ⟩    ---   ( f  o  ( g  o  h ) ) = ( ( f  o  g )  o  h )
     (     ( TMap μ d o  FMap T h ) o  ( (TMap μ c   o  FMap T g )    o f ) )
   ≈⟨ assoc  ⟩
     ( ( ( TMap μ d o      FMap T h ) o  (TMap μ c   o  FMap T g ) )  o f )
   ≈⟨ car (sym assoc) ⟩
     ( ( TMap μ d o  ( FMap T h     o   ( TMap μ c   o  FMap T g ) ) ) o f )
   ≈⟨ car ( cdr (assoc) ) ⟩
     ( ( TMap μ d o  ( ( FMap T h o       TMap μ c ) o  FMap T g )   ) o f )
   ≈⟨ car assoc ⟩
     ( ( ( TMap μ d o  ( FMap T h   o   TMap μ c ) ) o  FMap T g ) o f )
   ≈⟨ car (car ( cdr ( begin 
           ( FMap T h o TMap μ c )
       ≈⟨ nat A μ ⟩
           ( TMap μ (FObj T d) o FMap T (FMap T h) )
        ∎ 
   )))  ⟩
      ( ( ( TMap μ d  o  ( TMap μ ( FObj T d)  o FMap T (  FMap T h ) ) )  o FMap T g )  o f )
   ≈⟨ car (sym assoc) ⟩
     ( ( TMap μ d  o  ( ( TMap μ ( FObj T d)   o FMap T (  FMap T h ) )   o FMap T g ) )   o f )
   ≈⟨ car ( cdr (sym assoc) ) ⟩
     ( ( TMap μ d  o  ( TMap μ ( FObj T d)   o ( FMap T (  FMap T h ) o FMap T g ) ) )   o f )
   ≈⟨ car ( cdr (cdr (sym (distr T )))) ⟩
     ( ( TMap μ d  o  ( TMap μ ( FObj T d)     o FMap T ( ( FMap T h  o g ) ) ) )   o f )
   ≈⟨ car assoc ⟩
     ( ( ( TMap μ d  o  TMap μ ( FObj T d)  )  o FMap T ( ( FMap T h  o g ) ) )    o f )
   ≈⟨ car ( car (
      begin
         ( TMap μ d o TMap μ (FObj T d) )
      ≈⟨ IsMonad.assoc ( isMonad m) ⟩
         ( TMap μ d o FMap T (TMap μ d) )
      ∎
   )) ⟩
     ( ( ( TMap μ d  o    FMap T ( TMap μ d) ) o FMap T ( ( FMap T h  o g ) ) )    o f )
   ≈⟨ car (sym assoc) ⟩
     ( ( TMap μ d  o  ( FMap T ( TMap μ d )    o FMap T ( ( FMap T h  o g ) ) ) )  o f )
   ≈⟨ sym assoc ⟩
     ( TMap μ d  o  ( ( FMap T ( TMap μ d )    o FMap T ( ( FMap T h  o g ) ) )  o f ) )
   ≈⟨ cdr ( car ( sym ( distr T )))   ⟩
     ( TMap μ d  o ( FMap T ( ( ( TMap μ d )   o ( FMap T h  o g ) ) ) o f ) )
   ≈⟨ refl-hom ⟩
     join k d ( ( TMap μ d  o ( FMap T h  o g ) ) ) f
   ≈⟨ refl-hom ⟩
     join k d ( join k d h g) f 
  ∎ where open ≈-Reasoning (A) 



-- Kleisli :
-- Kleisli = record { Hom = 
--                 ; Hom = _⟶_
--                  ; Id = IdProd
--                  ; _o_ = _∘_
--                  ; _≈_ = _≈_
--                  ; isCategory = record { isEquivalence = record { refl  = λ {φ} → ≈-refl {φ = φ}
--                                                                 ; sym   = λ {φ ψ} → ≈-symm {φ = φ} {ψ}
--                                                                 ; trans = λ {φ ψ σ} → ≈-trans {φ = φ} {ψ} {σ}
--                                                                 }
--                                        ; identityL = identityL
--                                        ; identityR = identityR
--                                        ; o-resp-≈ = o-resp-≈
--                                        ; associative = associative
--                                        }
--                  }