CoYoneda.agda

module CoYoneda where

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; sym)
open import Data.Product using (_×_; proj₁; proj₂; ∃; _,_)


pattern _⊢_⊗_ a k x = (a , k , x) --  ∃ (λ a → (a → r) × f a)

module CovariantMap
  (r : Set)
  (f : Set → Set)
  (fmap : ∀ p q → (p → q) → f p → f q)  -- 共変ファンクター
  where

  map-⟹ : ∃ (λ a → (a → r) × f a) → f r
  map-⟹ (a ⊢ k ⊗ x) = fmap a r k x

  map-⟸ : f r → ∃ (λ a → (a → r) × f a)
  map-⟸ x = r ⊢ (λ y → y) ⊗ x

module CovariantLemma
  (r : Set)
  (f : Set → Set)
  (fmap : ∀ p q → (p → q) → f p → f q)
  (fmap-id : ∀ p → fmap p p (λ y → y) ≡ (λ y → y)) -- fmap id ≡ id
  (Nat-free-thr : ∀ p q (g : p → q)
                     (x : f p) (k : q → r) →
                     q ⊢ k ⊗ fmap p q g x ≡ p ⊢ k ∘ g ⊗ x
                     -- この全単射は一般には成立しないのでは?
                     -- 例えば fmap に const () を渡した場合が反例になると思う
                     -- 一般的には fmap 適用前の構造を覚えておけないので、戻すことができない
  )
  --  g
  --  p    ∀ (p : Set) (p → r) × f p
  --  ↓             (∘ g) ↑       ↓ fmap g
  --  q    ∀ (q : Set) (q → r) × f q
  where

  map-⟹ : ∃ (λ a → (a → r) × f a) → f r
  map-⟹ = CovariantMap.map-⟹ r f fmap
  map-⟸ : f r → ∃ (λ a → (a → r) × f a)
  map-⟸ = CovariantMap.map-⟸ r f fmap

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

  -- 米田写像の合成 (⟸ ∘ ⟹) が恒等関数になることの証明
  id-left : (Nat : ∃ (λ a → (a → r) × f a)) →
            map-⟸ (map-⟹ Nat) ≡ Nat
  id-left (a ⊢ k ⊗ x) = Nat-free-thr a r k x (λ z → z)
  --  map-⟸ (map-⟹ (a ⊢ k ⊗ x))  =
  --  map-⟸ (fmap a r k x)         =
  --  r ⊢ (λ y → y) ⊗ fmap a r k x