diff options
| -rw-r--r-- | examples/equality/Pi.obs | 46 | ||||
| -rw-r--r-- | examples/equality/Sigma.obs | 47 | ||||
| -rw-r--r-- | examples/equality/Universe.obs | 31 | ||||
| -rw-r--r-- | examples/equality/template.obs | 22 |
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 |