Yoneda Lemma Proof under Haskell like Functor

Yoneda.agda

module Yoneda where

open import Function.Base using (_∘_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)

{- specialized Morphism to Haskell function,
   specialized Functor to Haskell Functor,
   Proof of Yoneda Lemma -}
{- 射を Haskell の関数に、
   関手を Haskell の Functor に限定した場合の
   米田の補題の証明 -}

module Covariant where

  module Yoneda
    (f : Set → Set)
    (fmap : ∀ {p q} → (p → q) → f p → f q)  {- covariant functor -} {- 共変ファンクター -}
    (r : Set)
    where

      {- construction of Yoneda map ⟹ -}
      {- 米田写像 ⟹ の構成 -}
      map-⟹ : (∀ (a : Set) → (r → a) → f a) → f r
      map-⟹ Nat = Nat r (λ x → x)

      {- construction of Yoneda map ⟸ -}
      {- 米田写像 ⟸ の構成 -}
      map-⟸ : f r → (∀ (a : Set) → (r → a) → f a)
      map-⟸ x a k = fmap k x

      module Lemma
        (fmap-id : ∀ {p} → fmap {p} {p} (λ x → x) ≡ (λ x → x)) -- fmap id ≡ id
        (Nat-free-thr : ∀ {p q} (g : p → q)
                        (Nat : ∀ (a : Set) → (r → a) → f a)
                        (k : r → p)                            →
                        fmap g (Nat p k) ≡ Nat q (g ∘ k))
        {- Naturality about `a` of Natural Transformation `∀ (a : Set) → (r → a) → f a`
           (Raynolds-abstraction, Parametricity, Free-Theorem) -}
        {- 自然変換 `∀ (a : Set) → (r → a) → f a` で成立する `a` についての自然性条件 -}
        where

          {- proof that composition of Yoneda map (⟹ ∘ ⟸) is identity -}
          {- 米田写像の合成 (⟹ ∘ ⟸) が恒等関数になることの証明 -}
          id-right-left : map-⟹ ∘ map-⟸ ≡ (λ x → x)
          id-right-left = fmap-id

          {- proof that composition of Yoneda map (⟸ ∘ ⟹) is identity -}
          {- 米田写像の合成 (⟸ ∘ ⟹) が恒等関数になることの証明 -}
          id-left-right : ∀ (Nat : ∀ (a : Set) → (r → a) → f a) (b : Set) (k : r → b) →
                    (map-⟸ ∘ map-⟹) Nat b k ≡ Nat b k
          id-left-right Nat b k = Nat-free-thr k Nat (λ z → z)

          {- Since we have shown id-right-left , id-left-right , proof of Yoneda lemma is complete -}
          {- id-right-left , id-left-right を示したので、米田の補題の証明が完了 -}

  {- covariant Yoneda Embedding
       Cᵒᵖ → Sets^C
         s → r : Cᵒᵖ  (morphism of Cᵒᵖ)
         ∀ a . r → a : C → Sets  (covaritant Hom Functor, object of functor category Sets^C)
         ∀ a . (r → a) → (s → a) : C → Sets  (morphism of functor category Sets^C)  -}
  {- 共変米田埋め込み
       Cᵒᵖ → Sets^C
         s → r : Cᵒᵖ  (Cᵒᵖ の射)
         ∀ a . r → a : C → Sets  (共変Hom関手, 関手圏 Sets^C の対象)
         ∀ a . (r → a) → (s → a) : C → Sets  (関手圏 Sets^C の射)  -}
  yonedaEmbedding : ∀ (r : Set) (s : Set) →
                    (s → r) →
                    (∀ (a : Set) → (r → a) → (s → a))
  yonedaEmbedding r s = Yoneda.map-⟸ s→ s→-fmap r
    where
      s→ : Set → Set
      s→ a = s → a
      s→-fmap : ∀ {p q} → (p → q) → (s → p) → (s → q)
      s→-fmap m h = m ∘ h

module Contravariant where

  module Yoneda
    (f : Set → Set)
    (fmap : ∀ {p q} → (q → p) → f p → f q)  -- 反変ファンクター
    (r : Set)
    where

      -- 米田写像 ⟹ の構成
      map-⟹ : (∀ (a : Set) → (a → r) → f a) → f r
      map-⟹ Nat = Nat r (λ x → x)

      -- 米田写像 ⟸ の構成
      map-⟸ : f r → (∀ (a : Set) → (a → r) → f a)
      map-⟸ x a k = fmap k x

      module Lemma
        (fmap-id : ∀ {p} → fmap {p} {p} (λ y → y) ≡ (λ y → y)) -- fmap id ≡ id
        (Nat-free-thr : ∀ {p q} (g : q → p)
                        (Nat : ∀ (a : Set) → (a → r) → f a)
                        (k : p → r)                            →
                        fmap g (Nat p k) ≡ Nat q (k ∘ g))
        -- 自然変換 ∀ (a : Set) → (a → r) → f a で成立する自然性条件
        where

          -- 米田写像の合成 (⟹ ∘ ⟸) が恒等関数になることの証明
          id-right-left : map-⟹ ∘ map-⟸ ≡ (λ x → x)
          id-right-left = fmap-id

          -- 米田写像の合成 (⟸ ∘ ⟹) が恒等関数になることの証明
          id-left-right : ∀ (Nat : ∀ (a : Set) → (a → r) → f a) (b : Set) (k : b → r) →
                    map-⟸ (map-⟹ Nat) b k ≡ Nat b k
          id-left-right Nat b k = Nat-free-thr k Nat (λ z → z)

          -- id-right-left , id-left-right を示したので、米田の補題の証明が完了

  -- 反変米田埋め込み
  -- C → Sets^Cᵒᵖ
  --   r → s : C の射
  --   ∀ a . a → r : Cᵒᵖ → Sets (反変Hom関手) は関手圏 Sets^Cᵒᵖ の対象
  --   ∀ a . (a → r) → (a → s) は関手圏 Sets^Cᵒᵖ の射
  yonedaEmbedding : ∀ (r : Set) (s : Set) →
                    (r → s) →
                    (∀ (a : Set) → (a → r) → (a → s))
  yonedaEmbedding r s = Yoneda.map-⟸ →s →s-fmap r
    where
      →s : Set → Set
      →s a = a → s
      →s-fmap : ∀ {p q} → (q → p) → (p → s) → (q → s)
      →s-fmap m h = h ∘ m

Yoneda.v

Module Yoneda.

(* 射を Haskell の関数に、
   関手を Haskell の Functor に限定した場合の
   米田の補題の証明 *)

Section UnderFandFreeT.
  Variable (r : Type).
  Variable (f : Type -> Type) (fmap : forall p q, (p -> q) -> f p -> f q).
  Variable (fmap_id : forall p x, fmap p p (fun y => y) x = x). (* fmap id === id *)
  Variable (Nat_free_thr :
              forall p q (g : p -> q)
                     (Nat : forall (a : Type), (r -> a) -> f a)
                     (k : r -> p),
                fmap p q g (Nat p k) = Nat q (fun z => g (k z))).
  (* forall (a : Type), (r -> a) -> f a で成立する Raynolds-abstraction (free-theorem) *)

  (* 米田写像 "-->" の構成 *)
  Lemma map_lr : (forall (a : Type), (r -> a) -> f a) -> f r.
    intros Nat.
    apply Nat.
    intros y.
    assumption.
  Defined.

  Print map_lr.
  (* map_lr =
       fun (Nat : forall a : Type, (r -> a) -> f a)
         => Nat r (fun y : r => y)
       : (forall a : Type, (r -> a) -> f a) -> f r
   *)

  (* 米田写像 "<--" の構成 *)
  Lemma map_rl : f r -> (forall (a : Type), (r -> a) -> f a).
    intros x a k.
    apply (fmap r a).
    assumption.
    assumption.
  Defined.

  Print map_rl.
  (* map_rl =
       fun (x : f r) (a : Type) (k : r -> a)
         => fmap r a k x
       : f r -> forall a : Type, (r -> a) -> f a
   *)

  (* "-->" ・ "<--" === id *)
  Lemma rr_id : forall (x : f r),
      map_lr (map_rl x) = x. (* map_lr ・ map_rl === id *)
  Proof.
    intros.
    unfold map_rl. (* 米田写像 "<--" の定義 *)
    unfold map_lr. (* 米田写像 "-->" の定義 *)
    now apply fmap_id. (* fmap id === id *)
  Qed.

  Print rr_id.
  (* rr_id =
       fun x : f r
         => fmap_id r x
       : forall x : f r, map_lr (map_rl x) = x
   *)

  (* "<--" ・ "-->" === id *)
  Lemma ll_id : forall
      (Nat : forall (a : Type), (r -> a) -> f a)
      (b : Type) (k : r -> b),
      map_rl (map_lr Nat) b k = Nat b k. (* map_rl ・ map_lr === id *)
  Proof.
    intros.
    unfold map_rl.
    unfold map_lr.
    rewrite Nat_free_thr.
    reflexivity.
  Qed.

  Print ll_id.
  (* ll_id =
       fun (Nat : forall a : Type, (r -> a) -> f a) (b : Type) (k : r -> b)
         => eq_ind_r (fun f0 : f b => f0 = Nat b k) eq_refl
            (Nat_free_thr r b k Nat (fun y : r => y))
       : forall (Nat : forall a : Type, (r -> a) -> f a) (b : Type) (k : r -> b),
         map_rl (map_lr Nat) b k = Nat b k
   *)

  (* 米田写像 "-->", "<--" の構成と、
     その合成が恒等関数になることを証明できたので、
     同型になることの証明が完了。 *)

  Record IsoProperty :=
    { map_lr_ : (forall (a : Type), (r -> a) -> f a) -> f r;
      map_rl_ : f r -> (forall (a : Type), (r -> a) -> f a);
      rr_id_ : forall (x : f r), map_lr_ (map_rl_ x) = x;
      ll_id_ : forall
          (Nat : forall (a : Type), (r -> a) -> f a)
          (b : Type) (k : r -> b),
          map_rl_ (map_lr_ Nat) b k = Nat b k;
    }.

  (* 同型に必要な証明をまとめる *)
  Lemma yoneda_iso : IsoProperty.
  Proof.
    now apply (Build_IsoProperty map_lr map_rl rr_id ll_id).
  Qed.

End UnderFandFreeT.

Print Yoneda.yoneda_iso.