\begin{code}
module CN where
e : ( X : Set )-> Set -- a convenience
e X = (X -> X)
data G : Set where
zer : G
suc : G → G
{-# BUILTIN NATURAL G #-} -- what does this actually do??
-- some combinators. First the ones in Haskell
id : { X : Set}-> e X
id {X} x = x
const : { X : Set}-> {Y : Set}-> X -> Y -> X
const {X} {Y} x _ = x
_∘_ : {X : Set} {Y : Set} {Z : Set} -> (Y -> Z) -> (X -> Y) -> X -> Z
_∘_ {X} {Y} {Z} f g x = f (g x)
flip : {Z : Set}-> {B : Set} -> {A : Set}->
(A -> B -> Z) -> B -> A -> Z
flip f b a = f a b
-- now the standard "S" combinator
cS : {X : Set}-> {Y : Set}-> {Z : Set}->
(X -> Y -> Z) -> (X -> Y) -> X -> Z
cS z y x = z x (y x)
_▷_ = cS -- some infix notation for S and C S.
_◁_ : {X : Set}-> {Y : Set}-> {Z : Set}->
(X -> Y) -> (X -> Y -> Z) -> X -> Z
_◁_ {X} {Y} {Z} = flip {X -> Z} {X -> Y} {X -> Y -> Z} (cS {X} {Y} {Z})
zero_gen : {X : Set}-> {Y : Set}-> Y -> e X
zero_gen {X} {Y} = const id -- const {X} {Y} (id {X})
CN : Set₁ -- predicative, because not a possible argument to its own quantifier.
CN = {X : Set}-> e (e X)
zero : CN
zero = zero_gen
one : CN
one = id
two : CN
two {X} f = f ∘ f
infixr 2 _+_
infixr 3 _*_
infixr 4 _^_
_+_ _*_ _^_ : CN -> CN -> CN
(a + b) s z = b s (a s z) -- : X
(a * b) s = b (a s) -- : e X
-- (a ^ b) {X} s z = b {e X} (a {X}) s z
(a ^ b) {X} = b {e X} (a {X}) -- : e (e X)
O I : CN
O _ z = z
I s = s
-- sg _ s z as a stream is z,sz,sz,sz,... = 0;rep 1
-- sgbar _ s z (as a stream) is sz,z,z,z... = 1;rep 0
sg sgbar : CN -> CN
-- sgbar b {X} = b {e X} (zero {X}) -- is this right?
sgbar b {X} s z = b {X} (const {X} {X} z) (s z) -- why not this?
sg b {X} s z = b {X} (const {X} {X} (s z)) z -- looks right
pd : CN -> CN
pd b {X} f z = let it : e (e X)
it = b (λ m g _ → g (m f z)) (zero {X})
in it id z
pd' : {X : Set}-> e (e (e (e X))) -> e (e X)
pd' {X} n f z = n (λ m g _ → g (m f z)) (zero {X}) id z
-- cons a f is (\n->if n==0 then a else f (n-1)), ie. [a,f0,f1,f2,...]
-- so pd should be cons 0 id
-- sg should be cons 1 (const 0)
-- sgbar should be cons 0 (const 1)
-- cons 88 df = [88,df0,df1,df2,...]
cons : {X : Set} -> e (e X) -> e (e (e X)) -> e (e (e (e X))) -> e (e X)
cons {X} a f n s z
= let postponent : e (e X) -> X
postponent = (λ x -> x (a s z)) ∘ (λ x -> x id)
iteration : (n : e (e (e X)) → e (e (e X))) → e (e X)
iteration n = n (λ m g _ → g (f m s z)) zero
in postponent (iteration n)
-- this just a way to economise on context
module laws (a : CN) (b : CN) (c : CN) -- introduce a common context.
(X : Set) (s : X -> X) (z : X)
(X' : X -> Set) where
infix 0 _~~_ -- ζ equivalence
_~~_ : CN -> CN -> Set
a ~~ b = X' (a s z) -> X' (b s z)
assoc+ : (a + b) + c ~~ a + (b + c)
assoc+ = id
+unit : a + O ~~ a
+unit = id
unit+ : O + a ~~ a
unit+ = id
assoc* : (a * b) * c ~~ a * (b * c)
assoc* = id
*unit : a * I ~~ a
*unit = id
unit* : I * a ~~ a
unit* = id
dist*+ : a * (b + c) ~~ (a * b) + (a * c)
dist*+ = id
dist*O : a * O ~~ O
dist*O = id
dist^+ : a ^ (b + c) ~~ (a ^ b) * (a ^ c)
dist^+ = id
dist^+O : a ^ O ~~ I
dist^+O = id
dist^B : a ^ (b * c) ~~ (a ^ b) ^ c
dist^B = id
dist^BI : a ^ I ~~ a
dist^BI = id
-- In contrast, the following do not hold definitionally.
-- These are "unreasonable" expectations.
-- WrongO* : O * a ~~ O
-- WrongO* x = {!!} -- x
-- WrongI^ : I ^ a ~~ I
-- WrongI^ x = {!!} -- x
-- These are however characteristic of `numerical' values |a|.
-- this is out of place.
-- Accessibility
Set^ : Set -> Set₁
Set^ A = A -> Set
CNN : CN -> Set₁
CNN a
= {X : Set} -> {X' : Set^ X} ->
(s : X -> X) -> (s' : (x : X)-> X' x -> X' (s x))->
(z : X) -> (z' : X' z)->
X' (a {X} s z)
lemma+ : (a : CN)-> CNN a ->
(b : CN)-> CNN b -> CNN(a + b)
lemma+ a a' b b' s s' z z'
= b' s s' (a s z) (a' s s' z z')
lemmaO : CNN O
lemmaO _ _ _ z' = z'
lemma* : (a : CN)-> CNN a ->
(b : CN)-> CNN b -> CNN(a * b)
lemma* a a' b b' s s'
= b' (a s) (a' s s')
lemmaI : CNN I
lemmaI _ s' = s'
lemma^ : (a : CN)-> (a' : CNN a)->
(b : CN)-> (b' : CNN b)-> CNN(a ^ b)
lemma^ a a' b b' {X} {X'}
= b' {e X} {Cl} (a {X}) aX'
where Cl : Set^ (X → X)
Cl f = (x : X) → X' x → X' (f x)
aX' : (f : X → X) → Cl f → Cl (a {X} f)
aX' = a' {X} {X'}
-- Algebras
data Peano (X : Set) : Set where
S : X -> Peano X
Z : Peano X
--2 algebras as maps
Alg-fun : Set -> Set
Alg-fun X = Peano X -> X
--3 construction
Alg-fun-mk : {X : Set}-> (X -> X) -> X -> Alg-fun X
Alg-fun-mk _ z Z = z
Alg-fun-mk s _ (S x) = s x
--3 selection: s
Alg-fun-s : {X : Set} -> Alg-fun X -> X -> X
Alg-fun-s alg x = alg (S x)
--3 and then z:
Alg-fun-z : {X : Set} -> Alg-fun X -> X
Alg-fun-z alg = alg Z
--2 algebras as a data type
data Alg-data (X : Set) : Set where
mkAlg-data : (X -> X) -> X -> Alg-data X --3 constructor right here
--3 selection
Alg-data-s : {X : Set} -> Alg-data X -> X -> X
Alg-data-s (mkAlg-data s _) = s
Alg-data-z : {X : Set} -> Alg-data X -> X
Alg-data-z (mkAlg-data _ z) = z
--2 algebras as record types. This turns out to be best.
record Alg (X : Set) : Set where
constructor mk
field
s : X -> X
z : X
open Alg public
-- this is out of place. It is the corresponding algebra on predicates.
record Prog (X : Set) (a : Alg X) (X' : Set^ X) : Set where
constructor mkProg
field
ss : (x : X)-> X' x -> X' (a .s x)
zz : X' (a .z)
CN# : Set₁
CN# = {X : Set}-> Alg X -> X
CNN# : CN# -> Set₁
CNN# a
= {X : Set} ->
(alg : Alg X) ->
{X' : Set^ X} ->
((x : X)-> X' x -> X' (alg .s x)) ->
X' (alg .z) ->
X' (a {X} alg)
record Lens : Set₁ where
constructor Lens_
field
L : Set -> Set
U : (X : Set)-> Alg X -> Alg (L X)
D : (X : Set)-> Alg X -> L X -> X
-- interpretation of a Lens as a function
[_] : Lens -> CN -> CN
[ l ] a {X} s z
= let alg : Alg X
alg = mk s z
X' : Set
X' = l .Lens.L X
alg' : Alg X'
alg' = l .Lens.U X alg
s' : X' -> X'
s' = alg' .Alg.s
z' : X'
z' = alg' .Alg.z
d : X' -> X
d = l .Lens.D X alg
in
d (a s' z')
[_]# : Lens -> CN# -> CN#
[ l ]# a {X} alg
= let X' : Set
X' = Lens.L l X
alg' : Alg X'
alg' = Lens.U l X alg
in
Lens.D l X alg (a {X'} alg')
-- simple examples of Lenses
2^lens : Lens
2^lens = Lens_ e
(λ X a → mk two (a .s) )
(λ X a f → f (a .z) )
2*lens : Lens
2*lens = Lens_ (λ X → X)
(λ X a → mk (two (a .s)) (a .z) )
(λ X _ x → x )
2+lens : Lens
2+lens = Lens_ (λ X → X)
(λ X a → mk (a .s) (two (a .s) (a .z)))
(λ X _ x → x )
-- a more interesting example
-- this first forms the sequence (a .s),id,id,id,...
-- then maps application to z across it, to get the
-- sequence 1,0,0,0,...., that we might write (1 ; const 0)
-- this is involved in representing the predecessor function
-- pd = ( 0 |-> 0 , S n |-> n)
-- how to represent ( 0 |-> a , S n |-> f n) ?
-- let x = (0^)n in x * a + (0^)x * f n
0^lens : Lens
0^lens = Lens_ e
(λ X a → mk zero (a .s))
(λ X a f → f (a .z))
sglens : Lens
sglens = Lens_ (λ X → X)
(λ X a → mk (const (a .z)) ((a .s) (a .z)))
(λ X a → id)
-- generalisation to arbitrary left operands
_^lens : CN -> Lens
b ^lens = Lens_ e -- (λ X → X → X)
(λ X a → mk b (a .s))
(λ X a f → f (a .z))
_*lens : CN -> Lens
b *lens = Lens_ (λ X → X)
(λ X a → mk (b (a .s)) (a .z))
(λ X _ x → x)
_+lens : CN -> Lens
b +lens = Lens_ (λ X → X)
(λ X a → mk (a .s) (b (a .s) (a .z)))
(λ X _ x → x)
_^'_ _*'_ _+'_ : CN -> CN -> CN
_^'_ a = [ a ^lens ] -- (a ^)
_*'_ a = [ a *lens ] -- (a *)
_+'_ a = [ a +lens ] -- (a +)
lemma+' : (a : CN)-> CNN a ->
(b : CN)-> CNN b -> CNN(a +' b)
lemma+' a a' b b' {X} {X'} s s' z z'
= b' {X} {X'} s s' (a {X} s z) (a' {X} {X'} s s' z z')
lemma*' : (a : CN)-> CNN a ->
(b : CN)-> CNN b -> CNN(a *' b)
lemma*' a a' b b' {X} {X'} s s'
= b' {X} {X'} (a {X} s) (a' {X} {X'} s s')
lemma^' : (a : CN)-> CNN a ->
(b : CN)-> CNN b -> CNN(a ^' b)
lemma^' a a' b b' {X} {X'}
= b' {e X} {Cl} (a {X}) aX'
where Cl : Set^ (X → X)
Cl f = (x : X) → X' x → X' (f x)
aX' : (f : X → X) → Cl f → Cl (a {X} f)
aX' = a' {X} {X'}
module Lemma:coincidences (a : CN) (b : CN) (X : Set)
(s : X -> X) (z : X) (X' : X -> Set) where
infix 1 _≅_
_≅_ : CN -> CN -> Set
a ≅ b = X' (a s z) -> X' (b s z)
wonder+ : a + b ≅ a +' b
wonder+ x = x
wonder* : a * b ≅ a *' b
wonder* x = x
wonder^ : a ^ b ≅ a ^' b
wonder^ x = x
comp : Lens -> Lens -> Lens
comp φ ψ = let F : Set -> Set
F X = Lens.L ψ (Lens.L φ X)
U : (X : Set)-> Alg X -> Alg (F X)
U X alg = Lens.U ψ (Lens.L φ X) (Lens.U φ X alg)
D : (X : Set)-> Alg X -> F X -> X
D X alg fx = Lens.D φ X alg
(Lens.D ψ (Lens.L φ X) (Lens.U φ X alg) fx)
in Lens_ F U D
Theorem:LensComposition : (φ : Lens)-> (ψ : Lens)-> (a : CN)->
(X : Set)-> (s : X -> X)-> (z : X) -> (X' : Set^ X)->
X' ([ comp φ ψ ] a {X} s z) -> X' ([ φ ] ([ ψ ] a) {X} s z)
Theorem:LensComposition φ ψ a X s z X' x' = x'
conjecture# : (φ : Lens)-> (ψ : Lens)-> (a : CN#)->
(X : Set)-> (alg : Alg X)-> (X' : Set^ X)->
X' ([ comp φ ψ ]# a {X} alg) -> X' ([ φ ]# ([ ψ ]# a) {X} alg)
conjecture# φ ψ a X alg X' x' = x'
^lens# *lens# +lens# : CN# -> Lens
^lens# a = Lens_ (λ X → X → X)
(λ X alg → mk -- {X → X}
(λ f x → a {X} (mk f x))
(alg .s))
(λ X alg f → f (alg .z) )
*lens# a = Lens_ (λ X → X)
(λ X alg → mk -- {X}
(λ x → a {X} (mk (alg .s) x) )
(alg .z) )
(λ X alg x → x)
+lens# a = Lens_ (λ X → X)
(λ X alg → mk -- {X}
(alg .s)
(a {X} alg) )
(λ X alg x → x)
_^#_ _*#_ _+#_ : CN# -> CN# -> CN#
_^#_ a = [ ^lens# a ]#
_*#_ a = [ *lens# a ]#
_+#_ a = [ +lens# a ]#
lemma^# : (a : CN#)-> CNN# a ->
(b : CN#)-> CNN# b -> CNN# (a ^# b)
lemma^# a a' b b' {X} alg {X'} sp
= let aiter : (X -> X) -> X -> X
aiter f x = a {X} (mk f x)
alg' : Alg (X → X)
alg' = mk aiter (alg .s)
Cl : Set^ (X -> X)
Cl f = ( x : X )-> X' x -> X' (f x)
fact : (f : X -> X)-> Cl f -> Cl (aiter f)
fact f clf x = a' {X} (mk f x) {X'} clf
in b' {X -> X} alg' {Cl} fact sp (alg .z)
lemma*# : (a : CN#)-> CNN# a ->
(b : CN#)-> CNN# b -> CNN# (a *# b)
lemma*# a a' b b' {X} alg {X'} sp
= let pa : X -> X
pa x = a {X} (mk (alg .s) x)
alg' : Alg X
alg' = mk pa (alg .z)
fact : (x : X) → X' x → X' (pa x)
fact x = a' {X} (mk (alg .s) x) {X'} sp
in b' {X} alg' {X'} fact
lemma*+ : (a : CN#)-> CNN# a ->
(b : CN#)-> CNN# b -> CNN# (a +# b)
lemma*+ a a' b b' {X} alg {X'} sp zp
= let alg' : Alg X
alg' = Lens.U (+lens# a) X alg
in b' {X} alg' {X'} sp (a' {X} alg {X'} sp zp)
-- explorations
exp2 : CN -> CN
exp2 n {X} = n {e X} (two {X})
t tt ttt tttt : CN
t = two -- actually exp2 (exp2 0) = exp2 1
tt {X} = t {e X} (t {X}) -- 2^2 = 4
ttt {X} = (tt {e X}) (t {X}) -- 2^4 = 16
tttt {X} = (ttt {e X}) (t {X}) -- 2^16 = 65536
-- let us have a universe operator. For any set X
-- this produces a family of sets (U{X},T{X})
-- containing X and closed under e.
-- this might be called the universe of pure sets over X.
mutual
data U {X : Set} : Set where
g : U {X}
e' : U {X} -> U {X}
T : {X : Set} -> U {X} -> Set
T {X} g = X
T (e' u) = e (T u)
mutual
data N : Set where
ze : N
su : N -> N
H : N -> Set -- hierarchy of pure sets on G
H ze = G
H (su n) = e (H n)
-- cn : N -> CN
-- cn ze {X} = two {X}
-- cn (su n) {X} = cn n {e X} (two {X})
scn : Set -- small Church numerals
scn = (n : N)-> H (su (su n))
squidge : scn -> scn
squidge t = λ n → t (su n) two
stwo : scn
stwo = λ n → two { H n }
tetr : (n : CN) -> e (e G)
tetr n = let f : (n : CN)-> (n₁ : N) → e (e (H n₁))
f n = n {scn} squidge stwo
in f n ze
test : CN -> G
test n = tetr n suc zer
at : CN -> CN -> CN -- Note: can't be CN -> e CN
at a b {X} =
let ax : e (e X)
ax = a {X}
bx : e (e (e X))
bx = b {e X}
in bx ax
-- now we can iterate with carrier scn instead of the impredicative type.
-- data Nat : Set where
-- zer : Nat
-- suc : Nat -> Nat
-- -- large iteration
-- Iter : {X : Set₁}-> Nat -> (X -> X) -> X -> X
-- Iter zer = λ f x → x
-- Iter (suc n) = λ f x → f (Iter n f x) -- f (iter f n x)
-- -- dependent recursion
-- rec : {C : Nat -> Set}-> (n : Nat) ->
-- ((n : Nat) → C n → C (suc n)) -> C zer -> --
-- -- (n : Nat)->
-- C n
-- rec zer sc zc = zc
-- rec (suc n) sc zc = sc n (rec n sc zc)
-- -- non-dependent (but small) iteration
-- iter : { C : Set }-> Nat -> e C -> e C
-- iter {C} n f x = rec {λ _ → C} n (λ _ c → f c) x
-- Seq : Set -> Set
-- Seq X = Nat -> X
-- CO : Set₁
-- CO = {X : Set} -> (Seq X -> X) -> (X -> X) -> X -> X
-- COO : CO -> Set₁
-- COO a = {X : Set} -> {X' : Set^ X} ->
-- (l : Seq X -> X) -> ((f : Seq X) -> ((n : Nat) → X' (f n))
-- -> X' (l f)) ->
-- (s : X -> X) -> ((x : X) -> X' x -> X' (s x)) ->
-- (z : X) -> X' z ->
-- X' (a {X} l s z)
-- infixr 2 _+O_
-- infixr 3 _*O_
-- infixr 4 _^O_
-- _^O_ _*O_ _+O_ : CO -> CO -> CO
-- (a ^O b) {X} l = let liftl : Seq (X -> X) -> X -> X
-- liftl sf x = l (λ n → sf n x)
-- in b {X -> X} liftl (a {X} l)
-- (a *O b) l s = b l (a l s)
-- (a +O b) l s z = b l s (a l s z)
-- OO II WW : CO
-- OO {X} _ _ z = z
-- II {X} _ s = s
-- WW {X} l s z = l (λ n → iter {X} n s z)
-- lemmaOO : COO OO
-- lemmaOO {X} {X'} l l' s s' z z' = z'
-- lemmaII : COO II
-- lemmaII {X} {X'} l l' s s' z z' = s' z z'
-- lemmaWW : COO WW
-- lemmaWW {X} {X'} l l' s s' z z'
-- = let seq : Seq X
-- seq n = iter {X} n s z
-- in l' seq (λ n → rec {λ n → X' (seq n)} n
-- (λ n₁ x → s' (seq n₁) x) z')
-- module Olaws (a : CO) (b : CO) (c : CO) -- introduce a common context.
-- (X : Set) (l : Seq X -> X) (s : X -> X) (z : X)
-- (X' : X -> Set) where
-- infix 1 _~~_
-- _~~_ : CO -> CO -> Set
-- a ~~ b = X' (a {X} l s z) -> X' (b {X} l s z)
-- assoc+ : (a +O b) +O c ~~ a +O (b +O c)
-- assoc+ x = x
-- Lunit+ : a +O OO ~~ a
-- Lunit+ x = x
-- Runit+ : OO +O a ~~ a
-- Runit+ x = x
-- assoc* : (a *O b) *O c ~~ a *O (b *O c)
-- assoc* x = x
-- Lunit* : a *O II ~~ a
-- Lunit* x = x
-- Runit* : II *O a ~~ a
-- Runit* x = x
-- distr*+ : a *O (b +O c) ~~ (a *O b) +O (a *O c)
-- distr*+ x = x
-- L*O : a *O OO ~~ OO
-- L*O x = x
-- L^+ : a ^O (b +O c) ~~ (a ^O b) *O (a ^O c)
-- L^+ x = x
-- L^O : a ^O OO ~~ II
-- L^O x = x
-- L^* : a ^O (b *O c) ~~ (a ^O b) ^O c
-- L^* x = x
-- L^I : a ^O II ~~ a
-- L^I x = x
-- -- Just as with the numerical case,
-- -- there are some ``unreasonable'' expectations.
-- lemma+O : (a : CO)-> COO a ->
-- (b : CO)-> COO b -> COO(a +O b)
-- lemma+O a a' b b' {X} {X'} l l' s s' z z'
-- = b' {X} {X'} l l' s s' (a {X} l s z) (a' {X} {X'} l l' s s' z z')
-- lemma*O : (a : CO)-> COO a ->
-- (b : CO)-> COO b -> COO(a *O b)
-- lemma*O a a' b b' {X} {X'} l l' s s'
-- = b' {X} {X'} l l' (a {X} l s) (a' {X} {X'} l l' s s')
-- lemma^O : (a : CO)-> (a' : COO a)->
-- (b : CO)-> (b' : COO b)-> COO(a ^O b)
-- lemma^O a a' b b' {X} {X'} l l'
-- = b' {X → X} {Cl }
-- (λ seq x → l (λ n → seq n x)) t
-- (a {X} l) aX'
-- where Cl : Set^ (X → X)
-- Cl f = (x : X) → X' x → X' (f x)
-- aX' : (f : X → X) → Cl f → Cl (a {X} l f)
-- aX' = a' {X} {X'} l l'
-- t : (f : Seq (X → X)) →
-- ((n : Nat) → Cl (f n)) → Cl (λ x → l (λ n → f n x))
-- t f f' x x' = l' (λ n → f n x) (λ n → f' n x x')
-- record AlgO (X : Set) : Set where
-- constructor mkAlgO
-- field
-- l : Seq X -> X
-- s : X -> X
-- z : X
-- record LensO : Set₁ where
-- constructor mkLensO
-- field
-- L : Set -> Set
-- U : (X : Set)-> AlgO X -> AlgO (L X)
-- D : (X : Set)-> AlgO X -> L X -> X
-- [_]O : LensO -> CO -> CO
-- [ ll ]O a {X} l s z
-- = let alg : AlgO X
-- alg = mkAlgO l s z
-- X' : Set
-- X' = LensO.L ll X
-- alg' : AlgO X'
-- alg' = LensO.U ll X alg
-- l' : Seq X' -> X'
-- l' = AlgO.l alg'
-- s' : X' -> X'
-- s' = AlgO.s alg'
-- z' : X'
-- z' = AlgO.z alg'
-- in
-- LensO.D ll X alg (a {X'} l' s' z')
-- ^Olens : CO -> LensO
-- ^Olens a = mkLensO (λ X → X → X)
-- (λ X alg → mkAlgO -- the carrier here is (X → X)
-- (λ s x → AlgO.l alg (λ n → s n x)) -- limits are pointwise
-- (a {X} (AlgO.l alg)) -- the successor of f is f^a
-- (AlgO.s alg) -- the zero is the original successor function
-- )
-- (λ X alg f → f (AlgO.z alg)) -- (0+(a^b))
-- *Olens : CO -> LensO -- a * b = (+a)^b 0
-- *Olens a = mkLensO (λ X → X)
-- (λ X alg → mkAlgO
-- (AlgO.l alg)
-- (a {X} (AlgO.l alg) (AlgO.s alg)) -- (a X (AlgO.s alg))
-- (AlgO.z alg)
-- )
-- (λ X alg x → x)
-- +Olens : CO -> LensO -- a + b = s^b (s^a 0), ie (+b) = s^b
-- +Olens a = mkLensO (λ X → X)
-- (λ X alg → mkAlgO
-- (AlgO.l alg)
-- (AlgO.s alg)
-- (a {X} (AlgO.l alg) (AlgO.s alg) (AlgO.z alg))
-- )
-- (λ X alg x → x)
-- compO : LensO -> LensO -> LensO
-- compO φ ψ = let F : Set -> Set
-- F X = LensO.L ψ (LensO.L φ X)
-- U : (X : Set)-> AlgO X -> AlgO (F X)
-- U X alg = LensO.U ψ (LensO.L φ X) (LensO.U φ X alg)
-- D : (X : Set)-> AlgO X -> F X -> X
-- D X alg fx = LensO.D φ X alg
-- (LensO.D ψ (LensO.L φ X) (LensO.U φ X alg) fx)
-- in mkLensO F U D
-- conjectureO : (φ : LensO)-> (ψ : LensO)-> (a : CO)->
-- (X : Set)-> (l : Seq X -> X) -> (s : X -> X)-> (z : X) ->
-- (X' : Set^ X)->
-- X' ([ compO φ ψ ]O a {X} l s z) -> X' ([ φ ]O ([ ψ ]O a) {X} l s z)
-- conjectureO φ ψ a X l s z X' x' = x'
-- \end{code}