Skip to content

Instantly share code, notes, and snippets.

@pthariensflame
Last active December 30, 2015 17:39
Show Gist options
  • Save pthariensflame/7862243 to your computer and use it in GitHub Desktop.
Save pthariensflame/7862243 to your computer and use it in GitHub Desktop.
Residual representations of `Lens` and `PLens` in Agda, and the canonical embedding of the former into the latter.
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₂ ()) (₂∼₂ _)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment