open import Category -- https://github.com/konn/category-agda                                                                                     
open import Level
open import Category.Sets
module yoneda { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } where

open import HomReasoning
open import cat-utility
open import Relation.Binary.Core
open import Relation.Binary


-- Contravariant Functor : op A → Sets  ( Obj of Sets^{A^op} )
open Functor

-- A is Locally small
postulate ≈-≡ : {a b : Obj A } { x y : Hom A a b } →  (x≈y : A [ x ≈ y  ]) → x ≡ y

import Relation.Binary.PropositionalEquality
-- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )
postulate extensionality : Relation.Binary.PropositionalEquality.Extensionality c₂ c₂


CF' : (a : Obj A) → Functor A Sets
CF' a = record {
        FObj = λ b → Hom A a b
        ; FMap =   λ {b c : Obj A } → λ ( f : Hom A b c ) → λ (g : Hom A a b ) →  A [ f o g ] 
        ; isFunctor = record {
             identity = identity
             ; distr = λ {a} {b} {c} {f} {g} → distr1 a b c f g
             ; ≈-cong = cong1
        } 
    } where
        lemma-CF1 : {b : Obj A } → (x : Hom A a b) → A [ id1 A b o x ] ≡ x
        lemma-CF1 {b} x = let open ≈-Reasoning (A) in ≈-≡ idL
        identity : {b : Obj A} → Sets [ (λ (g : Hom A a b ) → A [ id1 A b o g ]) ≈ ( λ g → g ) ]
        identity {b} = extensionality lemma-CF1
        lemma-CF2 : (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) → (x : Hom A a a₁ )→ A [ A [ g o f ] o x ] ≡ (Sets [ _[_o_] A g o _[_o_] A f ]) x
        lemma-CF2 a₁ b c f g x = let open ≈-Reasoning (A) in ≈-≡ ( begin
               A [ A [ g o f ] o x ]
             ≈↑⟨ assoc ⟩
               A [ g o A [ f o x ] ] 
             ≈⟨⟩
               ( λ x →  A [ g o x  ]  ) ( ( λ x → A [ f o x ] ) x )
             ∎ )
        distr1 :   (a₁ b c : Obj A) (f : Hom A a₁ b) (g : Hom A b c) →
                Sets [ (λ g₁ → A [ A [ g o f ] o g₁ ]) ≈ Sets [ (λ g₁ → A [ g o g₁ ]) o (λ g₁ → A [ f o g₁ ]) ] ]
        distr1 a b c f g = extensionality ( λ x → lemma-CF2 a b c f g x )
        cong1 :  {A₁ B : Obj A} {f g : Hom A A₁ B} → A [ f ≈ g ] → Sets [ (λ g₁ → A [ f o g₁ ]) ≈ (λ g₁ → A [ g o g₁ ]) ]
        cong1 eq = extensionality ( λ x → ( ≈-≡ (  
                 (IsCategory.o-resp-≈  ( Category.isCategory A )) ( IsEquivalence.refl (IsCategory.isEquivalence  ( Category.isCategory A ))) eq )))

open import Function

CF : (a : Obj A) → Functor (Category.op A) Sets
CF a = record {
        FObj = λ b → Hom (Category.op A) a b  
          ; FMap =   λ {b c : Obj A } → λ ( f : Hom  A c b ) → λ (g : Hom  A b a ) →  (Category.op A) [ f o g ] 
        ; isFunctor = record {
             identity =  \{b} → extensionality ( λ x → lemma-CF1 {b} x )
             ; distr = λ {a} {b} {c} {f} {g} → {!!}
             ; ≈-cong = {!!}
        } 
    }  where
        lemma-CF1 : {b : Obj A } → (x : Hom A b a) →  (Category.op A) [ id1 A b o x ] ≡ x
        lemma-CF1 {b} x = let open ≈-Reasoning (Category.op A) in ≈-≡ idL