From 72feeec46c34c678640341e76958481f4244d8df Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 12 Jan 2023 17:57:06 +0000
Subject: Provide examples of Obs code.

This folder spells out the action of equality and cast for the different
type constructors. Ideally the two correctness proofs should given by
reflexivity.
---
 examples/equality/Sigma.obs | 47 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 examples/equality/Sigma.obs

(limited to 'examples/equality/Sigma.obs')

diff --git a/examples/equality/Sigma.obs b/examples/equality/Sigma.obs
new file mode 100644
index 0000000..f742183
--- /dev/null
+++ b/examples/equality/Sigma.obs
@@ -0,0 +1,47 @@
+TypeData : Set 1
+TypeData = (index : Set) ** (x : index) -> Set
+
+index : (type : TypeData) -> Set
+index = \type => fst type
+
+element : (type : TypeData) -> (x : index type) -> Set
+element = \type => snd type
+
+Value : (type : TypeData) -> Set
+Value = \type => (x : index type) ** element type x
+
+Equality : (left : TypeData) -> (right : TypeData) -> Prop
+Equality = \left => \right =>
+  (indexEquality : index left ~ index right) **
+  (x : index left) ->
+  element left x ~ element right (cast (index left) (index right) indexEquality x)
+
+Cast :
+  (oldType : TypeData) ->
+  (newType : TypeData) ->
+  (equality : Equality oldType newType) ->
+  (value : Value oldType) ->
+  Value newType
+Cast = \oldType => \newType => \equality => \value =>
+  < cast (index oldType) (index newType) (fst equality) (fst value)
+  , cast
+      (element oldType (fst value))
+      (element newType (cast (index oldType) (index newType) (fst equality) (fst value)))
+      (snd equality (fst value))
+      (snd value)
+  >
+
+EqualityCorrect :
+  (left : TypeData) ->
+  (right : TypeData) ->
+  Equality left right ~ (Value left ~ Value right)
+EqualityCorrect = refl Equality
+
+CastCorrect :
+  (oldType : TypeData) ->
+  (newType : TypeData) ->
+  (equality : Equality oldType newType) ->
+  (value : Value oldType) ->
+  Cast oldType newType equality value ~
+  cast (Value oldType) (Value newType) (fst (EqualityCorrect oldType newType) equality) value
+CastCorrect = refl Cast
-- 
cgit v1.2.3