Skip to content

Instantly share code, notes, and snippets.

@oisdk oisdk/lens.agda
Created Oct 16, 2019

What would you like to do?
{-# OPTIONS --safe --without-K #-}
module Bits where
infixr 4 _×_ _,_
record _×_ (A : Set) (B : Set) : Set where
constructor _,_
fst : A
snd : B
open _×_
data _+_ (A : Set) (B : Set) : Set where
inl : A A + B
inr : B A + B
record Lens (S : Set) (T : Set) (A : Set) (B : Set) : Set₁ where
X : Set
Y : X Set
viewˡ : X S
viewʳ : X A
updateˡ : (x : X) T Y x
updateʳ : (x : X) B Y x
open Lens
compose : {S T A B P Q} Lens S T A B Lens A B P Q Lens S T P Q
compose xs ys .X = xs .X × ys .X
compose xs ys .Y (x , y) = xs .Y x + ys .Y y
compose xs ys .viewˡ (x , y) = xs .viewˡ x
compose xs ys .viewʳ (x , y) = ys .viewʳ y
compose xs ys .updateˡ (x , y) t = inl (xs .updateˡ x t)
compose xs ys .updateʳ (x , y) t = inr (ys .updateʳ y t)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.