Provide examples of Obs code.HEADmaster

This folder spells out the action of equality and cast for the different
type constructors. Ideally the two correctness proofs should given by
reflexivity.

1 files changed, 47 insertions, 0 deletions

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