Residual representations of `Lens` and `PLens` in Agda, and the canonical embedding of the former into the latter.

Lens.agda

module Lens where
open import Level
open import Function
open import Relation.Binary
open import Data.Product
open import Relation.Binary.Product.Pointwise
open import Data.Sum
open import Relation.Binary.Sum
open import Data.Empty
open import Function.Inverse
open import Function.Equality hiding ( ≡-setoid )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ) renaming ( setoid to ≡-setoid )

record Lens {iℓ sℓ s≈ℓ tℓ t≈ℓ : Level} {Index : Set iℓ} (Source : Index → Setoid sℓ s≈ℓ) (Target : Index → Setoid tℓ t≈ℓ) (rℓ r≈ℓ : Level) : Set (iℓ ⊔ sℓ ⊔ s≈ℓ ⊔ tℓ ⊔ t≈ℓ ⊔ suc (rℓ ⊔ r≈ℓ)) where
  constructor lens
  field
    Residue : Setoid rℓ r≈ℓ
    transition : {ix : Index} → Inverse (Source ix) (Target ix ×-setoid Residue)       

record PLens {iℓ sℓ s≈ℓ tℓ t≈ℓ : Level} {Index : Set iℓ} (Source : Index → Setoid sℓ s≈ℓ) (Target : Index → Setoid tℓ t≈ℓ) (rℓ r≈ℓ r′ℓ r′≈ℓ : Level) : Set (iℓ ⊔ sℓ ⊔ s≈ℓ ⊔ tℓ ⊔ t≈ℓ ⊔ suc (rℓ ⊔ r≈ℓ ⊔ r′ℓ ⊔ r′≈ℓ)) where
  constructor plens
  field
    Residue : Setoid rℓ r≈ℓ
    Residue′ : Setoid r′ℓ r′≈ℓ
    transition : {ix : Index} → Inverse (Source ix) ((Target ix ×-setoid Residue) ⊎-setoid Residue′)

embedding : {iℓ sℓ s≈ℓ tℓ t≈ℓ rℓ r≈ℓ : Level} {Index : Set iℓ} {Source : Index → Setoid sℓ s≈ℓ} {Target : Index → Setoid tℓ t≈ℓ} → Lens Source Target rℓ r≈ℓ → PLens Source Target rℓ r≈ℓ zero zero
embedding {Index = Index} {Source} {Target} (lens Residue transition) = plens Residue (≡-setoid ⊥)
                                                                          (λ {ix} →
                                                                             record {
                                                                             to =
                                                                               record {
                                                                               _⟨$⟩_ = λ x → inj₁ (Inverse.to transition ⟨$⟩ x);
                                                                               cong = λ x → ₁∼₁ (cong (Inverse.to transition) x) };
                                                                             from =
                                                                               record {
                                                                               _⟨$⟩_ = λ x → Inverse.from transition ⟨$⟩ extractˡ x;
                                                                               cong = λ {i} {j} → from-cong ix i j };
                                                                             inverse-of =
                                                                               record {
                                                                               left-inverse-of = λ x → Inverse.left-inverse-of transition x;
                                                                               right-inverse-of =
                                                                                 λ {(inj₁ x) → ₁∼₁ (Inverse.right-inverse-of transition x);
                                                                                    (inj₂ ())} } })
  where
    extractˡ : {a : Level} → {A : Set a} → A ⊎ ⊥ → A
    extractˡ (inj₁ x) = x
    extractˡ (inj₂ ())
    
    module _ (ix : Index) where
      open Setoid (Source ix) public using () renaming ( Carrier to S )
      open Setoid (Target ix) public using () renaming ( Carrier to T )
    module _ {ix : Index} where
      open Setoid (Source ix) public using () renaming ( _≈_ to _S≈_ )
      open Setoid (Target ix) public using () renaming ( _≈_ to _T≈_ )
    open Setoid Residue using () renaming ( Carrier to R ; _≈_ to _R≈_ )
    
    from-cong : (ix : Index) →
                  (i j : T ix × R ⊎ ⊥) →
                  (_T≈_ ×-Rel _R≈_ ⊎-Rel _≡_) i j →
                  Inverse.from transition ⟨$⟩ extractˡ i S≈
                  Inverse.from transition ⟨$⟩ extractˡ j
    from-cong ix (inj₁ _) (inj₁ _) (₁∼₁ p) = cong (Inverse.from transition) p
    from-cong ix (inj₁ _) (inj₂ ()) (₁∼₂ ())
    from-cong ix (inj₂ ()) (inj₁ _) ()
    from-cong ix (inj₂ ()) (inj₂ ()) (₂∼₂ _)