Created
March 7, 2021 22:37
-
-
Save ejconlon/205dfda98f0d78d9cbc0ccade187c2d6 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Inj | |
import Decidable.Equality | |
import Decidable.Order | |
-- These definitions would go in some stdlib | |
public export | |
interface Equivalence ty inj => Inj (ty : Type) (inj : ty -> ty -> Type) where | |
useInj : {x, y: ty} -> inj x y -> x = y | |
mkInj : Inj ty inj => {x, y: ty} -> x = y -> inj x y | |
mkInj {x} Refl = reflexive x | |
-- Unsure if DecEq ty should be a superclass constraint | |
public export | |
interface Inj ty inj => DecInj (ty : Type) (inj : ty -> ty -> Type) where | |
decInj : (x, y: ty) -> Dec (inj x y) | |
-- From this definition... | |
data Foo : Type where | |
Zap : Foo | |
Bar : Int -> Foo | |
Quux : Foo -> Foo | |
-- We should be able to derive this datatype and all that follows | |
data FooInj : (a, b: Foo) -> Type where | |
ZapInj : FooInj Zap Zap | |
BarInj : (x1, x2: Int) -> x1 = x2 -> FooInj (Bar x1) (Bar x2) | |
QuuxInj : (r1, r2: Foo) -> r1 = r2 -> FooInj (Quux r1) (Quux r2) | |
implementation Preorder Foo FooInj where | |
transitive _ _ _ ZapInj ZapInj = ZapInj | |
transitive _ _ _ (BarInj x x Refl) (BarInj x x Refl) = BarInj x x Refl | |
transitive _ _ _ (QuuxInj r r Refl) (QuuxInj r r Refl) = QuuxInj r r Refl | |
reflexive f = | |
case f of | |
Zap => ZapInj | |
Bar x => BarInj x x Refl | |
Quux r => QuuxInj r r Refl | |
implementation Equivalence Foo FooInj where | |
symmetric _ _ ZapInj = ZapInj | |
symmetric _ _ (BarInj x x Refl) = BarInj x x Refl | |
symmetric _ _ (QuuxInj r r Refl) = QuuxInj r r Refl | |
implementation Inj Foo FooInj where | |
useInj ZapInj = Refl | |
useInj (BarInj x x Refl) = Refl | |
useInj (QuuxInj r r Refl) = Refl |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment