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. OK, I Understand
 
Top