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 )
                 (Trans : (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  ( Trans a ) ]  ≈ C [ (Trans b ) o  (FMap F f)  ] ]
--    uniqness : {d : Obj D} 
--      →  C [ Trans d  ≈ Trans 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
    Trans :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
    isNTrans : IsNTrans domain codomain F G Trans

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 Trans μ a ]  ≈ A [ Trans μ 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 [ Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ a) ] ]
      unity1 : {a : Obj A} -> A [ A [ Trans μ a o Trans η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
      unity2 : {a : Obj A} -> A [ A [ Trans μ a o (FMap T (Trans η 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 [  Trans μ a o Trans μ ( FObj T a ) ] ≈  A [  Trans μ a o FMap T (Trans μ 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 [ Trans μ a o Trans η ( 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 [ Trans μ a o (FMap T (Trans η a )) ] ≈ Id {_} {_} {_} {A} (FObj T a) ]
Lemma6 = \m -> IsMonad.unity2 ( isMonad m )

-- T = M x A
-- nat of η
-- g ○ f = μ(c) T(g) f
-- h ○ (g ○ f) = (h ○ g) ○ f
-- η(b) ○ f = f
-- f ○ η(a) = 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
     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 [ Trans μ c  o A [ FMap T g  o f ] ]


-- open import Relation.Binary.Core  renaming (Trans to Trans1 )

-- module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where

--   -- The code in Relation.Binary.EqReasoning cannot handle                                                                              
--   -- heterogeneous equalities, hence the code duplication here.                                                                         

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

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

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


--   data _IsRelatedTo_ {a} {A1 : Set a} (x : A1) {b} {B : Set b} (y : B) :
--                      Set (suc (c₁ ⊔ c₂ ⊔ ℓ ))  where
--     relTo : (x≈y : A [ x ≈ y ] ) → x IsRelatedTo y

--   begin_ : ∀ {a} {A1 : Set a} {x : A1} {b} {B : Set b} {y : B} →
--            x IsRelatedTo y → A [ x ≈ y ]
--   begin relTo x≈y = x≈y

--   _≈⟨_⟩_ : ∀ {a} {A1 : Set a} (x : A1) {b} {B : Set b} {y : B}
--              {c} {C : Set c} {z : C} →
--            A [ x ≈ y ] → y IsRelatedTo z → x IsRelatedTo z
--   _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)

--   _∎ : ∀ {a} {A1 : Set a} (x : A1) → x IsRelatedTo x
--   _∎ _ = relTo refl-hom

-- --  hoge : {!!} -- {a b : Obj A } -> Rel ( Hom A a b ) (suc  ℓ )
-- --  hoge = IsCategory.identityL (Category.isCategory A) 

--   lemma11 : ? --  {a c : Obj A} { x : Hom A a c } {y : Hom A a c }  -> x IsRelatedTo y
--   lemma11 =  relTo ( IsCategory.identityL (Category.isCategory A)  )

open  import  Relation.Binary.PropositionalEquality
open ≡-Reasoning

lemma60 :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->  ∀{n} ->  ( Set n ) IsRelatedTo ( Set n )
lemma60 c = relTo refl

lemma12 :  {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b c : Obj L } -> 
       ( x : Hom L c a ) -> ( y : Hom L b c ) -> L [ x o y ] ≡ L [ x o y ]
lemma12 L x y =  begin  L [ x o y ]  ∎

lemma13 :  {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } ( c : Obj L ) -> 
       ( x : Hom L c a ) -> L [ x o Id L c ] ≡ L [ x o Id L c ]
lemma13 L c x  =  begin  L [ x o Id L c ]  ∎

lemma14 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } ( c : Obj L ) ->
       ( x : Hom L c a ) -> x ≡ L [ x o Id L c ]
lemma14 L a x = {!!}

lemma15 : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } ( c : Obj L ) ->
       ( x y z : Hom L c a ) -> x ≡ y -> L [ y  ≈  z ] -> x ≡ z
lemma15 L x y z = {!!}

eq-func : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ)  ->
       { a b : Obj L } -> ( x : Hom L a b ) -> { x y : Hom L a b } ->
       L [ x ≈ y ] -> Hom L a b
eq-func c x eq = {!!}

-- ≅-to-≡ : ∀ {a} {A : Set a} {x y : A} → x ≅ y → x ≡ y
-- ≅-to-≡ refl = refl

data _==_  {n} {c₁ c₂ ℓ : Level} {L : Category c₁ c₂ ℓ} { a b : Obj L } : 
           Hom L a b -> Hom L a b -> Set  (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
     reflection : { x : Hom L a b } -> x == x
     identityR :  {f : Hom L a b} → ( L [ f o Id L b ] ) == f
     identityL :  {f : Hom L a b} → ( L [ Id L a o f ] ) == f
     o-resp-≈ : {c : Obj L} {f g : Hom L a c } {h i : Hom L c b } → f == g → h == i → ( L [ h o f ] ) == ( L [ i o g ] )
     associative : {B C : Obj L } {f : Hom L C b  }  {g : Hom L B C  } {h : Hom L a B }
             → ( L [ f o L [ g o h ] ] ) == ( L [ L [ f o g ] o h ] )

cat-== : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } { x y : Hom L a b } -> ( x == y ) -> x ≡ y
cat-== c reflection = ?

cat-eq : {c₁ c₂ ℓ : Level} (L : Category c₁ c₂ ℓ) { a b : Obj L } { x y : Hom L a b } -> L [ x ≈ y ] -> x ≡ y
cat-eq c refl = refl


Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
                 { a : Obj A } ( b : Obj A ) ->
                 ( f : Hom A a b )
                      ->  A [ (Id {_} {_} {_} {A} b) o f ]  ≡ f
Lemma61 c b g = --  IsCategory.identityL (Category.isCategory c) 
     begin  
          c [ Id c b o g ]
     ≡⟨ cat-eq c ( IsCategory.identityL (Category.isCategory c)) ⟩
          g
     ∎

open Kleisli
Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { a b : Obj A } 
                 { f : Hom A a ( FObj T b) } 
                 { M : Monad A T η μ } 
                 ( K : Kleisli A T η μ M) 
                      -> A  [ join K b (Trans η b) f  ≈ f ]
Lemma7 c k = 
--              { a b : Obj c} 
--              { T : Functor c c }
--              { η : NTrans c c identityFunctor T }
--              { f : Hom c a ( FObj T b) }  
         {!!}
     

Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
                 { T : Functor A A }
                 { η : NTrans A A identityFunctor T }
                 { μ : NTrans A A (T ○ T) T }
                 { 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 (Trans η a)  ≈ f ]
Lemma8 k = {!!}

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 k = {!!}





-- 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
--                                        }
--                  }