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, 46 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