Chu embeds in Lens

cat.agda

{-# OPTIONS --type-in-type #-}
module functors where
open import prelude

record Category {O : Set} (𝒞[_,_] : O → O → Set) : Set where
  constructor 𝒾:_▸:_𝒾▸:_▸𝒾:
  infixl 8 _▸_
  field
    𝒾 : ∀ {x} → 𝒞[ x , x ]
    _▸_ : ∀ {x y z} → 𝒞[ x , y ] → 𝒞[ y , z ] → 𝒞[ x , z ]
    𝒾▸ : ∀ {x y} (f : 𝒞[ x , y ]) → (𝒾 ▸ f) ≡ f
    ▸𝒾 : ∀ {x y} (f : 𝒞[ x , y ]) → (f ▸ 𝒾) ≡ f
open Category ⦃...⦄ public

record Functor {A : Set} {𝒜[_,_] : A → A → Set}
               {B : Set} {ℬ[_,_] : B → B → Set}
               (f : A → B) : Set where
  constructor φ:_𝒾:_▸:
  field
    ⦃ cat₁ ⦄ : Category {A} 𝒜[_,_]
    ⦃ cat₂ ⦄ : Category {B} ℬ[_,_]
    φ : ∀ {a b} → 𝒜[ a , b ] → ℬ[ f a , f b ]
    functor-id : ∀ {a} → φ {a} 𝒾 ≡ 𝒾
    functor-comp : ∀ {A B C} → (f : 𝒜[ A , B ]) (g : 𝒜[ B , C ])
                 → φ (f ▸ g) ≡ φ f ▸ φ g
open Functor ⦃...⦄ public

chu-lens.agda

{-# OPTIONS --type-in-type #-}
module chu-lens where
open import prelude
open import functors
open import chu
open import lens

→∫ : Chu → ∫
→∫ (A⁺ , A⁻ ! Ω) = A⁺ , λ a⁺ → ∃ (Ω a⁺)
      
→Lens : {A B : Chu} → Chu[ A , B ] → ∫[ →∫ A , →∫ B ]
→Lens (f ↔ fᵗ ! †)  a⁺ = f a⁺ , λ (b⁻ , fa⁺Ωb⁻) → fᵗ b⁻ , subst id († a⁺ b⁻) fa⁺Ωb⁻

module _ {A B C : Chu}
         (F@(f ↔ fᵗ ! _†₁_) : Chu[ A , B ])
         (G@(g ↔ gᵗ ! _†₂_) : Chu[ B , C ]) where

    comp₂ : ∀ a⁺ → π₂  (→Lens (F ▸       G) a⁺)
                 ≡ π₂ ((→Lens  F ▸ →Lens G) a⁺)
    comp₂ a⁺ = extensionality λ ( c⁻ , gfaΩc ) → (λ x → (fᵗ ∘ gᵗ) c⁻ , x) ⟨$⟩
               subst⋯ id (f a⁺ †₂ c⁻) (a⁺ †₁ gᵗ c⁻) gfaΩc

    comp∀ : ∀ a⁺ → →Lens (F ▸ G) a⁺ ≡ (→Lens F ▸ →Lens G) a⁺
    comp∀ a⁺ rewrite comp₂ a⁺ = refl

instance
    open Chu[_,_]
    chu-lens-functor : Functor →∫
    chu-lens-functor = φ: →Lens
                       𝒾: refl
                       ▸: λ F G → extensionality (comp∀ F G)

chu.agda

{-# OPTIONS --type-in-type #-}
module chu where
open import functors
open import prelude
                 
record Chu : Set where
  constructor _,_!_
  field
    _⁺ _⁻ : Set
    _Ω_ : _⁺ → _⁻ → Set

module _ (A@(A⁺ , A⁻ ! _Ω₁_) B@(B⁺ , B⁻ ! _Ω₂_) : Chu) where
    record Chu[_,_] :  Set where -- Morphisms of chu spaces
      constructor _↔_!_
      field
        to : A⁺ → B⁺
        from : B⁻ → A⁻
        adj : ∀ a⁺ b⁻ → to a⁺ Ω₂ b⁻ ≡ a⁺ Ω₁ from b⁻
module _ {A@(A⁺ , A⁻ ! _Ω₁_)
          B@(B⁺ , B⁻ ! _Ω₂_)
          C@(C⁺ , C⁻ ! _Ω₃_) : Chu}
         (F@(f  ↔ fᵗ ! _†₁_) : Chu[ A , B ])
         (G@(g  ↔ gᵗ ! _†₂_) : Chu[ B , C ]) where
    adj-comp : ∀ a⁺ c⁻ → (g ∘ f) a⁺ Ω₃ c⁻ ≡ a⁺ Ω₁ (fᵗ ∘ gᵗ) c⁻
    adj-comp a⁺ c⁻ = trans (f a⁺ †₂    c⁻)  -- g (f a⁺) Ω₃        c⁻
                           (  a⁺ †₁ gᵗ c⁻)  --    f a⁺  Ω₂     gᵗ c⁻
                                            --      a⁺  Ω₁ fᵗ (gᵗ c⁻)

    chu-comp : Chu[ A , C ]
    chu-comp = (g ∘ f) ↔ (fᵗ ∘ gᵗ) ! adj-comp

instance
    chu-cat : Category Chu[_,_]
    chu-cat = 𝒾: (id ↔ id ! λ _ _ → refl)
              ▸: chu-comp
              𝒾▸: (λ (_ ↔ _ ! _†_) → (λ x → _ ↔ _ ! x) ⟨$⟩
                    extensionality2 λ a⁺ b⁻ → trans-refl (a⁺ † b⁻))
              ▸𝒾: (λ _ → refl)

lens.agda

{-# OPTIONS --type-in-type #-}
module lens where
open import functors
open import prelude

_^ : Set → Set -- Presheaf
I ^ = I → Set

∫ : Set -- Arena
∫ = ∃ _^

_⦅_⦆ : ∫ → Set → Set -- Interpret as a polynomial functor
(A⁺ , A⁻) ⦅ y ⦆ = Σ[ a⁺ ∈ A⁺ ] (A⁻ a⁺ → y)

module _ (A@(A⁺ , A⁻) B@(B⁺ , B⁻) : ∫) where
  ∫[_,_] : Set
  ∫[_,_] = (a⁺ : A⁺) → Σ[ b⁺ ∈ B⁺ ] (B⁻ b⁺ → A⁻ a⁺)
module _ {A@(A⁺ , A⁻) B@(B⁺ , B⁻) : ∫} where
  lens : (get : A⁺ → B⁺)
         (set : (a⁺ : A⁺) → B⁻ (get a⁺) → A⁻ a⁺)
       → ∫[ A , B ]
  lens g s = λ a⁺ → g a⁺ , s a⁺
  get : (l : ∫[ A , B ]) → A⁺ → B⁺
  get l = π₁ ∘ l
  set : (A↝B : ∫[ A , B ]) → (a⁺ : A⁺) → B⁻ (get A↝B a⁺) → A⁻ a⁺
  set l = π₂ ∘ l

instance
    lens-cat : Category ∫[_,_]
    lens-cat = 𝒾: (λ a⁺ → a⁺ , id)
               ▸: (λ l1 l2 a⁺ → let b⁺ , setb = l1 a⁺
                                    c⁺ , setc = l2 b⁺
                                in  c⁺ , setb ∘ setc)
               𝒾▸: (λ _ → refl)
               ▸𝒾: (λ _ → refl)

prelude.agda

module prelude where
open import Function using (id; _∘_) public
open import Data.Sum renaming (inj₁ to Σ₁; inj₂ to Σ₂) using (_⊎_) public
open import Data.Product renaming (proj₁ to π₁; proj₂ to π₂) using (Σ; _×_; _,_; ∃; Σ-syntax) public
open import Agda.Builtin.Unit using (⊤; tt) public
open import Data.Empty using (⊥) public
open import Data.Nat as Nat renaming (suc to ℕs; zero to ℕz; _+_ to _ℕ+_) using (ℕ) public
open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_; _≢_; refl; sym; trans; subst) renaming (cong to _⟨$⟩_) public
open Eq.≡-Reasoning using (_≡⟨⟩_; step-≡; _∎) public

postulate
  extensionality : {A : Set} {B : A → Set} {f g : (x : A) → B x}
                 → (∀ x → f x ≡ g x) → f ≡ g
extensionality2 : {A : Set} {B : A → Set} {C : (x : A) → B x → Set} {f g : (x : A) (y : B x) → C x y }
                 → (∀ x y → f x y ≡ g x y) → f ≡ g
extensionality2 λλf≡g = extensionality λ x → extensionality λ y → λλf≡g x y

trans-refl : {A : Set} {x y : A} (p : x ≡ y) → trans p refl ≡ p
trans-refl p rewrite p = refl