0 | module BeTTI.Quotient
 1 |
 2 | import System
 3 | import System.File
 4 |
 5 | %default total
 6 |
 7 | {- Definitions are in a strange order to work around bug
 8 |    Potentially #2244, although we're not using interface resolution
 9 |    anywhere.
10 | -}
11 |
12 | export
13 | infixl 6 //
14 |
15 | ||| Quotient type
16 | ||| type   : type to quotient
17 | ||| rel : proof-relevant relation to quotient by
18 | export 0
19 | (//) : (type : Type) -> (rel : type -> type -> Type) -> Type
20 |
21 | ||| Equivalence class of input element
22 | export
23 | class :
24 |   {0 rel : type -> type -> Type} ->
25 |   type -> type // rel
26 |
27 | ||| Eliminator for quotients
28 | ||| f : eliminator for quotiented type
29 | ||| motive: the reason for the elimination (to inhabit motive)
30 | export
31 | (.because) : {0 rel : type -> type -> Type} ->
32 |              (f : type -> motive) ->
33 |              (0 indep : (x, y : type) -> rel x y -> (f x === f y) {a=motive}) ->
34 |              (type // rel) -> motive
35 |
36 | ||| Related elements are equal in the quotient
37 | export 0
38 | quotient : {rel : type -> type -> Type} -> {x,y : type} ->
39 |   rel x y -> ((class {type=type,rel} x) === (class {type,rel} y)) {a = type // rel}
40 | quotient prf = believe_me $ unsafePerformIO (do
41 |      _ <- fPutStrLn stderr "Trying to execute function extensionality"
42 |      exitWith {a = class {type,rel} x === class {type,rel} y} $ ExitFailure 1)
43 |
44 | ----- Don't change the order of these definitions -----
45 |
46 | a // r = a
47 | class x = x
48 | f.because indep x = f x
49 |
50 | -------------------------------------------------------
51 | ||| Dependent eliminator for quotients. Untested
52 | export
53 | (.Because) : {0 rel : a -> a -> Type} ->
54 |              {0 b : (x : a // rel) -> Type} ->
55 |              (f : (x : a) -> b (class {type=a,rel} x)) ->
56 |              (0 indep : (x, y : a) -> r x y ->
57 |              f (class {type=a,rel} x) ~=~ f (class {type=a,rel} y)) ->
58 |              (x : a // r) -> b x
59 | f.Because indep x = f x
60 |