• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Aug 23rd, 2019 78 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. import Logic open
2.
3. T Category<A:Type, M:A -> A -> Type>
4. | mkCategory
5.   { compose : {a:A, b:A, c:A, g:M(b,c), f:M(a,b)} -> M(a,c)
6.   , associative : {a:A, b:A, c:A, d:A, f:M(a,b), g:M(b,c), h:M(c,d), x:A} ->
7.       compose(a,c,d,h,compose(a,b,c,g,f)) == compose(a,b,d,compose(b,c,d,h,g),f)
8.   , identity : {a:A} ->
9.       [id:M(a,a)
10.       , And({b:A, f:M(a,b)} -> compose(a,a,b,f,id) == f
11.            ,{b:A, g:M(b,a)} -> compose(b,a,a,id,g) == g
12.            )
13.       ]
14.   }
15.
16. Fun : {A:Type, B:Type} -> Type
17.   A -> B
18.
19. compose : {A:Type, B:Type, C:Type, g:Fun(B,C), f:Fun(A,B)} -> Fun(A,C)
20.   {x : A} g(f(x))
21.
22. functionEq : {A:Type, B:Type, f:Fun(A,B), g:Fun(A,B)
23.              , e:{x:A} -> f(x) == g(x)
24.              , em: Empty
25.              } -> f == g
26.   absurd(em, f == g)
27.
28. associative : {A:Type, B:Type, C:Type, D:Type
29.               , f:Fun(A,B), g:Fun(B,C), h:Fun(C,D)
30.               , em:Empty
31.               } -> compose(A,C,D,h,compose(A,B,C,g,f)) ==
32.                      compose(A,B,D,compose(B,C,D,h,g),f)
33.   absurd(em, compose(A,C,D,h,compose(A,B,C,g,f)) ==
34.                compose(A,B,D,compose(B,C,D,h,g),f)
35.         )
36.
37. function.id : {A:Type} -> Fun(A,A)
38.   {x:A} x
39.
40. identity : {A:Type, em:Empty} ->
41.            [id:Fun(A,A)
42.            , And({B:Type, f:Fun(A,B)} -> compose(A,A,b,f,id) == f
43.                 ,{B:Type, g:Fun(B,A)} -> compose(B,A,A,id,g) == g
44.                 )
45.            ]
46. absurd(em
47.       , [id:Fun(A,A)
48.            , And({B:Type, f:Fun(A,B)} -> compose(A,A,B,f,id) == f
49.                 ,{B:Type, g:Fun(B,A)} -> compose(B,A,A,id,g) == g
50.                 )
51.            ]
52.       )
53.
54. //type.category : Category(Type, Fun)
55. //  mkCategory(compose, associative, identity)
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top