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.

4 files changed, 146 insertions, 0 deletions

diff --git a/examples/equality/Pi.obs b/examples/equality/Pi.obs
new file mode 100644
index 0000000..6364e2d
--- /dev/null
+++ b/examples/equality/Pi.obs
@@ -0,0 +1,46 @@
+TypeData : Set 1
+TypeData = (domain : Set) ** (x : domain) -> Set
+
+domain : (type : TypeData) -> Set
+domain = \type => fst type
+
+codomain : (type : TypeData) -> (x : domain type) -> Set
+codomain = \type => snd type
+
+Value : (type : TypeData) -> Set
+Value = \type => (x : domain type) -> codomain type x
+
+Equality : (left : TypeData) -> (right : TypeData) -> Prop
+Equality = \left => \right =>
+  (domainEquality : domain right ~ domain left) **
+  (x : domain right) ->
+  codomain left (cast (domain right) (domain left) domainEquality x) ~ codomain right x
+
+Cast :
+  (oldType : TypeData) ->
+  (newType : TypeData) ->
+  (equality : Equality oldType newType) ->
+  (value : Value oldType) ->
+  Value newType
+Cast = \oldType => \newType => \equality => \value =>
+  \x =>
+    cast
+      (codomain oldType (cast (domain newType) (domain oldType) (fst equality) x))
+      (codomain newType x)
+      (snd equality x)
+      (value (cast (domain newType) (domain oldType) (fst equality) x))
+
+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
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
diff --git a/examples/equality/Universe.obs b/examples/equality/Universe.obs
new file mode 100644
index 0000000..19a8408
--- /dev/null
+++ b/examples/equality/Universe.obs
@@ -0,0 +1,31 @@
+TypeData : Prop
+TypeData = ()
+
+Value : (type : TypeData) -> Set 1
+Value = \type => Set
+
+Equality : (left : TypeData) -> (right : TypeData) -> Prop
+Equality = \left => \right => ()
+
+Cast :
+  (oldType : TypeData) ->
+  (newType : TypeData) ->
+  (equality : Equality oldType newType) ->
+  (value : Value oldType) ->
+  Value newType
+Cast = \oldType => \newType => \equality => \value => 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
diff --git a/examples/equality/template.obs b/examples/equality/template.obs
new file mode 100644
index 0000000..856e05f
--- /dev/null
+++ b/examples/equality/template.obs
@@ -0,0 +1,22 @@
+postulate TypeData : Set 1
+postulate Value : (type : TypeData) -> Set
+postulate Equality : (left : TypeData) -> (right : TypeData) -> Prop
+postulate Cast :
+  (oldType : TypeData) ->
+  (newType : TypeData) ->
+  (equality : Equality oldType newType) ->
+  (value : Value oldType) ->
+  Value newType
+
+postulate EqualityCorrect :
+  (left : TypeData) ->
+  (right : TypeData) ->
+  Equality left right ~ (Value left ~ Value right)
+
+postulate 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