module Arrow where

open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Function hiding (id)
open ≡-Reasoning

record Category (_⇒_ : Set -> Set -> Set) : Set1 where
  field
    id : ∀ {a} -> a ⇒ a
    _>>>_ : ∀ {a b c} -> a ⇒ b -> b ⇒ c -> a ⇒ c
    left-id : ∀ {a b} -> (f : a ⇒ b) -> id >>> f ≡ f
    right-id : ∀ {a b : Set} -> {f : a ⇒ b} -> f >>> id ≡ f
    ∘-assoc : ∀ {a b c d} -> {f : a ⇒ b} {g : c ⇒ a} {h : d ⇒ c} -> h >>> (g >>> f) ≡ (h >>> g) >>> f
  
  infixl 4 _>>>_



record Applicative (f : Set -> Set) : Set1 where
  field
    pure : ∀ {a} -> a -> f a
    _<*>_ : ∀ {a b} -> f (a -> b) -> f a -> f b
    identity : ∀ {a} {v : f a} -> pure (λ x -> x) <*> v ≡ v
    composition : ∀ {a b c} {u : f (a -> b)} {v : f _} {w : f c} -> 
                pure (λ f g x -> f (g x)) <*> u <*> v <*> w ≡ u <*> (v <*> w)
    homomorphism : ∀ {a b} {f : a -> b}{x} -> pure f <*> pure x ≡ pure (f x)
    interchange : ∀ {a b} {u : f (a -> b)}{y : a} -> u <*> pure y ≡ pure (λ f -> f y) <*> u
  
  _<$>_ : ∀ {a b} -> (a -> b) -> f a -> f b
  f <$> x = pure f <*> x

  infixl 4 _<*>_ 
  infixl 5 _<$>_

  fmap-∘ : ∀ {a b c} {h : b -> c} {g : a -> b} {m : f a} -> h <$> (g <$> m) ≡ (h ∘ g) <$> m
  fmap-∘ {h = h} {g = g} {m = m} = begin pure (λ x → h x) <*> (pure g <*> m) ≡⟨ sym composition ⟩ _ ≡⟨ cong (λ x -> x <*> pure g <*> m) homomorphism ⟩ _
         ≡⟨ cong (λ x -> x <*> m) homomorphism ⟩ _ ∎

  fmap-∘-2 : ∀ {a b c d} {f : a -> b} {g : c -> d -> _}{m}{n} -> f <$> (g <$> m <*> n) ≡ (λ x y -> f (g x y)) <$> m <*> n
  fmap-∘-2 {f = f} {g = g} {m = m} {n = n} = begin 
           f <$> (g <$> m <*> n) ≡⟨ sym composition ⟩
           (λ f g x -> f (g x)) <$> pure f <*> (g <$> m) <*> n ≡⟨ cong (λ x -> x <*> (g <$> m) <*> n) homomorphism ⟩
           (λ g x -> f (g x)) <$> (g <$> m) <*> n ≡⟨ cong (λ x -> x <*> n) fmap-∘ ⟩
           (λ x y -> f (g x y)) <$> m <*> n ∎

  
assoc : ∀ {a b c} -> (a × b) × c → a × (b × c)
assoc z = a , ( b , c)
  where 
    open Σ z renaming (proj₁ to ab; proj₂ to c)
    open Σ ab renaming (proj₁ to a; proj₂ to b)

module Arrowish (_⇒_ : Set -> Set -> Set) (category : Category _⇒_) (rapp : ∀ {a} -> Applicative (_⇒_ a)) 
                
  where
  
  open Category category public
  module Dummy {a : Set} where
    open Applicative (rapp {a}) public
  open Dummy public
  S : {a b c : Set} -> (a -> b -> c) -> (a -> b) -> (a -> c)
  S f g x = f x (g x)
  
  postulate
    >>>-fmap : ∀ {a b c d} {f : a -> b} {g : c ⇒ d} {h : d ⇒ a} -> f <$> (g >>> h) ≡ g >>> (f <$> h)
    const-id : ∀ {a b} {f : a ⇒ b} -> const <$> f <*> id ≡ f
    pure->>> : ∀ {a b c d} {f : a ⇒ b} {x : a} {g : c -> d} -> pure x >>> f ≡ (g <$> id) >>> (pure x >>> f)
  pure-id : ∀ {a b} {x : a} -> pure x ≡ const x <$> id {b}
  pure-id = trans (sym const-id) (cong (λ x -> x <*> id) homomorphism)
  <*>-id : ∀ {a b c} {f : a -> b -> c}{g} -> f <$> id <*> g <$> id ≡ S f g <$> id
  <*>-id {f = f} {g = g} = {!!} {-begin (f <$> id) <*> (pure g <*> id) ≡⟨ sym composition ⟩
    pure (λ f g x -> f (g x)) <*> (f <$> id) <*> pure g <*> id  ≡⟨ cong (λ x -> x <*> pure g <*> id) fmap-∘ ⟩
    (((λ f g x -> f (g x)) ∘ f) <$> id) <*> pure g <*> id ≡⟨ cong (λ x -> x <*> id) interchange ⟩
    pure (λ f -> f g) <*> ((λ x g -> const (f x (g x))) <$> id) <*> id ≡⟨ cong (λ x -> x <*> id) fmap-∘ ⟩
    (const ∘ S f g) <$> id <*> id ≡⟨ cong (λ x -> x <*> id) (sym fmap-∘) ⟩
    const <$> (S f g <$> id) <*> id 
    ≡⟨ const-id ⟩ _ ∎-}
  arr-fmap : ∀ {a b c} {f : a -> b} {g : c ⇒ a} -> f <$> g ≡ g >>> (f <$> id)
  arr-fmap {f = f} = {!!} -- begin _ ≡⟨ cong (λ x -> f <$> x) (sym right-id) ⟩ _ ≡⟨ >>>-fmap ⟩ _ ∎ 
  const-<$> : ∀ {a b c} {f : a ⇒ b}{g : _ -> c} -> const <$> f <*> (g <$> id) ≡ f
  const-<$> {f = f} {g = g} = {!!} {-begin _ ≡⟨ sym composition ⟩ 
            pure (λ f g x -> f (g x)) <*> (const <$> f) <*> pure g <*> id ≡⟨ cong (λ x -> x <*> pure g <*> id) fmap-∘ ⟩
            pure (λ x g y -> const x (g y)) <*> f <*> pure g <*> id 
                 ≡⟨ cong (λ x -> x <*> id) interchange ⟩ _ ≡⟨ cong (λ x -> x <*> id) fmap-∘ ⟩
            pure (λ x y -> const x (g y)) <*> f <*> id ≡⟨ refl ⟩
            const <$> f <*> id
            ≡⟨ const-id ⟩ _ ∎-}

  
  arr : ∀ {a b} -> (a -> b) -> a ⇒ b
  arr f = f <$> id

  _&&&_ : ∀ {a b c} -> a ⇒ b -> a ⇒ c -> a ⇒ (b × c)
  f &&& g = _,_ <$> f <*> g
  _***_ : ∀ {a b c d} -> a ⇒ b -> c ⇒ d -> (a × c) ⇒ (b × d)
  f *** g = (arr proj₁ >>> f) &&& (arr proj₂ >>> g)
  first : ∀ {a b c} -> a ⇒ b -> (a × c) ⇒ (b × c)
  first f = f *** id

  apply : ∀ {a b} -> (a -> b) × a -> b
  apply p =  proj₁ p (proj₂ p)
  postulate
    bar : ∀ {a b c} {f : a ⇒ b} {g : b ⇒ (a -> c) }  ->  (f >>> g) <*> id ≡ (f &&& id) >>> first g >>> arr apply
  ap : ∀ {a b c} {f : a ⇒ (b -> c)} {g} -> (f &&& g) >>> arr apply ≡ f <*> g 
  ap {a} {b} {c} {f = f} {g = g} = {!!} {-begin (_,_ <$> f <*> g) >>> arr apply ≡⟨ sym arr-fmap ⟩
    pure apply <*> ((_,_ <$> f) <*> g) ≡⟨ sym composition ⟩
    pure (λ f g x -> f (g x)) <*> pure apply <*> (_,_ <$> f) <*> g 
         ≡⟨ cong (λ x -> x <*> (_,_ {b -> c} {b} <$> f) <*> g) homomorphism ⟩
    pure (λ g x -> apply (g x)) <*> (_,_ <$> f) <*> g ≡⟨ cong (λ x -> x <*> g) (sym composition)⟩
    pure (λ f g x -> f (g x)) <*> pure (λ g x -> apply (g x)) <*> pure _,_ <*> f <*> g 
         ≡⟨ cong (λ x -> x <*> pure (_,_ {b -> c} {b}) <*> f <*> g) homomorphism ⟩ _ ≡⟨ cong (λ x -> x <*> f <*> g) homomorphism ⟩
    pure (λ x y -> apply (x , y) ) <*> f <*> g ≡⟨ refl ⟩
    pure (λ x -> x) <*> f <*> g ≡⟨ cong (λ x -> x <*> g) identity ⟩ _ ∎-}
  
  first-def : ∀ {a b c} {f : a ⇒ b} -> first {c = c} f ≡ _,_ <$> (arr proj₁ >>> f) <*> arr proj₂
  first-def {f = f} = {!!} {-cong (λ x -> _,_ <$> (arr proj₁ >>> f) <*> x) right-id -}

  foo : ∀ {a b c} {f : a ⇒ b } -> first {c = c} f ≡ (λ y x -> y , (proj₂ x)) <$> (arr proj₁ >>> f) <*> id
  foo {f = f} = {!!} {-begin _ ≡⟨ first-def ⟩
    _,_ <$> (arr proj₁ >>> f) <*> (pure proj₂ <*> id) ≡⟨ sym composition ⟩
    pure (λ f g x -> f (g x)) <*> (_,_ <$> (arr proj₁ >>> f)) <*> pure proj₂ <*> id ≡⟨ cong (λ x -> x <*> id) interchange ⟩
    (λ f -> f proj₂) <$> ( (λ f g x -> f (g x)) <$> (_,_ <$> (arr proj₁ >>> f)) ) <*> id 
       ≡⟨ cong (λ x -> x <*> id) fmap-∘ ⟩ 
    ((λ f x -> f (proj₂ x)) <$> (_,_ <$> (arr proj₁ >>> f)) ) <*> id 
       ≡⟨ cong (λ x -> x <*> id) fmap-∘ ⟩
    (λ y x -> y , (proj₂ x)) <$> (arr proj₁ >>> f) <*> id ∎-}


  arr-∘ : ∀ {a b c} {f : a -> b} {g : c -> _} -> arr (f ∘ g) ≡ arr g >>> arr f
  arr-∘ {f = f} {g = g} = {!!} {-begin arr (f ∘ g) ≡⟨ refl ⟩ arr (_∘_ f g) ≡⟨ cong (λ x -> x <*> id) (sym homomorphism) ⟩
        pure (_∘_ f) <*> pure g <*> id ≡⟨ cong (λ x -> x <*> pure g <*> id) (sym homomorphism) ⟩
        pure (λ f g x -> f (g x)) <*> pure f <*> pure g <*> id ≡⟨ composition ⟩
        f <$> arr g  
        ≡⟨ arr-fmap ⟩ _ ∎-}
  map-*** : ∀ {a b c d} {f : a -> b} {g : c -> d} -> arr f *** arr g ≡ arr (map f g)
  map-*** {f = f} {g = g} = {!!} {-begin (arr proj₁ >>> arr f) &&& (arr proj₂ >>> arr g) ≡⟨ cong₂ _&&&_ (sym arr-∘) (sym arr-∘) ⟩
    arr (f ∘ proj₁) &&& arr (g ∘ proj₂)  ≡⟨ refl ⟩
    (_,_ <$> ((f ∘ proj₁) <$> id)) <*> arr (g ∘ proj₂) ≡⟨ cong (λ x -> x <*> arr (g ∘ proj₂)) fmap-∘ ⟩
    arr (_,_ ∘ (f ∘ proj₁)) <*> arr (g ∘ proj₂)
    ≡⟨ <*>-id ⟩ _ ∎-}

  first-arr : ∀ {a b c} {f : a -> b} -> first {c = c} (arr f) ≡ arr (map f (λ x -> x))
  first-arr {f = f} = {!!} {- begin arr f *** id  ≡⟨ cong (λ x -> arr f *** x) (sym identity) ⟩
                            arr f *** arr (λ x -> x)
                            ≡⟨ map-*** ⟩ _ ∎-}
  postulate
    <*>->>> : ∀ {a b c d e a1} {f : a ⇒ b} {g : _ ⇒ c} {h : _ -> d} {i : _ ⇒ e} {l : c -> e -> a1} -> 
         (_,_ <$> f <*> arr h) >>> ((l <$> (arr proj₁ >>> g)) <*> (arr proj₂ >>> i)) ≡ l <$> (f >>> g) <*> (arr h >>> i)
    pure-arr : ∀ {a b c d e}{f : a ⇒ b}{g : c -> d} {h : _ × e -> _} -> 
             pure (λ x y -> x , g y) <*> (arr proj₁ >>> f) <*> arr h ≡ arr (λ p -> proj₁ p , g (h p)) >>> first f

  first->>> : ∀ {a b c d} {f : a ⇒ b} {g : _ ⇒ c} -> first {c = d} (f >>> g) ≡ first f >>> first g
  first->>> {f = f} {g = g} = {!!} {- sym (begin (f *** id) >>> (g *** id) ≡⟨ cong₂ _>>>_ first-def first-def ⟩
    (_,_ <$> (arr proj₁ >>> f) <*> arr proj₂) >>> (_,_ <$> (arr proj₁ >>> g) <*> arr proj₂)
          ≡⟨ cong (λ x -> (_,_ <$> (arr proj₁ >>> f) <*> arr proj₂) >>> (_,_ <$> (arr proj₁ >>> g) <*> x)) (sym right-id) ⟩
    (_,_ <$> (arr proj₁ >>> f) <*> arr proj₂) >>> (_,_ <$> (arr proj₁ >>> g) <*> (arr proj₂ >>> id))
          ≡⟨ <*>->>> ⟩
    _,_ <$> ((arr proj₁ >>> f) >>> g) <*> (arr proj₂ >>> id)
          ≡⟨ cong (λ x -> _,_ <$> ((arr proj₁ >>> f) >>> g) <*> x) right-id ⟩
    _,_ <$> ((arr proj₁ >>> f) >>> g) <*> arr proj₂

    ≡⟨ cong (λ x -> _,_ <$> x <*> arr proj₂) (sym ∘-assoc) ⟩
    _,_ <$> (arr proj₁ >>> (f >>> g)) <*> arr proj₂
    ≡⟨ sym first-def ⟩ first (f >>> g) ∎)
    -}
--  _,_ <$> (arr proj₁ >>> f) <*> (arr proj₂ >>> arr g)
  
  
  first->>>-arr : ∀ {a b c d} {f : a ⇒ b} {g : c -> d} -> first f >>> arr (map (λ x -> x) g) ≡ arr (map (λ x -> x) g) >>> first f
  first->>>-arr {f = f} {g = g} = {!!} {-sym (begin _ ≡⟨ sym pure-arr ⟩
    _,_ <$> (arr proj₁ >>> f) <*> (arr λ x -> g (proj₂ x))
      ≡⟨ cong (λ x -> _,_ <$> (arr proj₁ >>> f) <*> x) arr-∘ ⟩
    _,_ <$> (arr proj₁ >>> f) <*> (arr proj₂ >>> arr g) ≡⟨ cong (λ x -> _,_ <$> x <*> (arr proj₂ >>> arr g)) (sym right-id) ⟩ _
      ≡⟨ sym <*>->>> ⟩ 
    (_,_ <$> (arr proj₁ >>> f) <*> arr proj₂) >>> (_,_ <$> (arr proj₁ >>> id) <*> (arr proj₂ >>> arr g))
    ≡⟨ cong (λ x -> (_,_ <$> (arr proj₁ >>> f) <*> arr proj₂) >>> (_,_ <$> (arr proj₁ >>> x) <*> (arr proj₂ >>> arr g))) (sym identity) ⟩
      (_,_ <$> (arr proj₁ >>> f) <*> arr proj₂) >>> (_,_ <$> (arr proj₁ >>> arr (λ x -> x)) <*> (arr proj₂ >>> arr g))
    ≡⟨ cong₂ _>>>_ (sym first-def) map-*** ⟩ _ ∎)-}

  first-π₁ : ∀ {a b c} {f : a ⇒ b} -> first {c = c} f >>> arr proj₁ ≡ arr proj₁ >>> f
  first-π₁ {a} {b} {c} {f = f} = {!!} {- begin (_,_ <$> (arr proj₁ >>> f) <*> (arr proj₂ >>> id)) >>> arr proj₁ ≡⟨ sym arr-fmap ⟩
           proj₁ <$> (_,_ <$> (arr proj₁ >>> f) <*> (arr proj₂ >>> id)) 
                 ≡⟨ cong (λ x -> proj₁ <$> (_,_ {b} {c} <$> (arr proj₁ >>> f) <*> x)) right-id ⟩
           proj₁ <$> (_,_ <$> (arr proj₁ >>> f) <*> arr proj₂) ≡⟨ sym composition ⟩
           pure (λ f g x -> f (g x)) <*> pure proj₁ <*> (_,_ <$> (arr proj₁ >>> f)) <*> arr proj₂
             ≡⟨ cong (λ x -> x <*> (_,_ {b} {c} <$> (arr proj₁ >>> f)) <*> arr proj₂) homomorphism ⟩
           pure (λ g x -> proj₁ (g x)) <*> (_,_ <$> (arr proj₁ >>> f)) <*> arr proj₂ 
             ≡⟨ cong (λ x -> x <*> arr proj₂) fmap-∘ ⟩
           const <$> (arr proj₁ >>> f) <*> arr proj₂
    ≡⟨ const-<$> ⟩ _ ∎-}
--    arr f >>> (g <*> h) = arr f >>> g <*> arr f >>> h
--    pure (λ x y -> x , g y) <*> (arr proj₁ >>> f) <*> arr h ≡ arr (λ p -> proj₁ p , g (h p)) >>> first f   
  first-assoc : ∀ {a b c d} {f : a ⇒ b} -> first {c = c} (first {c = d} f) >>> arr assoc ≡ arr assoc >>> first f
  first-assoc {f = f} = begin first f *** id >>> arr assoc  ≡⟨ sym arr-fmap ⟩
    assoc <$> (_,_ <$> (arr proj₁ >>> first f) <*> (arr proj₂ >>> id)) ≡⟨ fmap-∘-2 ⟩
    (λ x y -> assoc (x , y)) <$> (arr proj₁ >>> first f) <*> (arr proj₂ >>> id) ≡⟨ cong (λ x -> x <*> (arr proj₂ >>> id)) (>>>-fmap) ⟩
    (arr proj₁ >>> ((λ x y -> assoc (x , y)) <$> first f)) <*> (arr proj₂ >>> id)
   ≡⟨ cong (λ x -> (arr proj₁ >>> x) <*> (arr proj₂ >>> id)) fmap-∘-2  ⟩
     ?
    ≡⟨ {!!} ⟩ _ ∎
  second : ∀ {a b c} -> a ⇒ b -> (c × a) ⇒ (c × b)
  second f = arr swap >>> first f >>> arr swap