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/Universe.obs | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 examples/equality/Universe.obs

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

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
-- 
cgit v1.2.3