import Logic open

T Category<A:Type, M:A -> A -> Type>
| mkCategory
  { compose : {a:A, b:A, c:A, g:M(b,c), f:M(a,b)} -> M(a,c)
  , associative : {a:A, b:A, c:A, d:A, f:M(a,b), g:M(b,c), h:M(c,d), x:A} ->
      compose(a,c,d,h,compose(a,b,c,g,f)) == compose(a,b,d,compose(b,c,d,h,g),f)
  , identity : {a:A} ->
      [id:M(a,a)
      , And({b:A, f:M(a,b)} -> compose(a,a,b,f,id) == f
           ,{b:A, g:M(b,a)} -> compose(b,a,a,id,g) == g
           )
      ]
  }

Fun : {A:Type, B:Type} -> Type
  A -> B

compose : {A:Type, B:Type, C:Type, g:Fun(B,C), f:Fun(A,B)} -> Fun(A,C)
  {x : A} g(f(x))

functionEq : {A:Type, B:Type, f:Fun(A,B), g:Fun(A,B)
             , e:{x:A} -> f(x) == g(x)
             , em: Empty
             } -> f == g
  absurd(em, f == g)

associative : {A:Type, B:Type, C:Type, D:Type
              , f:Fun(A,B), g:Fun(B,C), h:Fun(C,D)
              , em:Empty
              } -> compose(A,C,D,h,compose(A,B,C,g,f)) ==
                     compose(A,B,D,compose(B,C,D,h,g),f)
  absurd(em, compose(A,C,D,h,compose(A,B,C,g,f)) ==
               compose(A,B,D,compose(B,C,D,h,g),f)
        )

function.id : {A:Type} -> Fun(A,A)
  {x:A} x

identity : {A:Type, em:Empty} ->
           [id:Fun(A,A)
           , And({B:Type, f:Fun(A,B)} -> compose(A,A,b,f,id) == f
                ,{B:Type, g:Fun(B,A)} -> compose(B,A,A,id,g) == g
                )
           ]
absurd(em
      , [id:Fun(A,A)
           , And({B:Type, f:Fun(A,B)} -> compose(A,A,B,f,id) == f
                ,{B:Type, g:Fun(B,A)} -> compose(B,A,A,id,g) == g
                )
           ]
      )

//type.category : Category(Type, Fun)
//  mkCategory(compose, associative, identity)