implemented dual monoid, trying axiom of extensionality and embedding…

[johnchandlerburnham]

… setoids into a monoid to prove monoid of endomorphims

I need some help figuring out how to get endo.associative to typecheck. I'm trying to embed a Setoid into the Monoid to try to write proofs when the Monoid is over a type (like functions) that needs extensional equality.

I have written the proofs that the monoid of endomorphisms is associative over function composition and has and identity element as the identity function, I just can't seem to convince the type-checker that the Setoid equality s.eq is the same as FunEq (function equality)

[ERROR]
Type mismatch.
- Found type... FunEq(~A, ~A) == FunEq(~A, ~A)
- Instead of... s.eq == FunEq(~A, ~A)
- When checking refl(~FunEq(~A, ~A))
- On expression (%setoid.FunEq(~A, ~A))(~{s} => {~e : s.eq == FunEq(~A, ~A)} -> Associative({:A} -> A, s, compose(~A, ~A, ~A)), {s.eq, s.equivalence, ~e} => ?n, ~refl(~FunEq(~A, ~A)))
- With the following context:
- A : Type

This is odd because I defined

setoid.FunEq : {~A : Type, ~B : Type} -> Setoid(A -> B)
  setoid(~(A -> B),FunEq(A,B),funeq.equivalence(~A,~B))

So I would have thought this would work.

I also found two strange expressions that validly typecheck:

// funeq.reflexive : {~A : Type} -> Reflexive(A,FunEq(A,sldalakfjsaldfkjas))
//  {f,x} refl(~f(x))

//endo.associative.go :
//  {~A : Type
//  , x : A -> A -> A
//  , y : A -> A -> A
//  , z : A -> A -> A
//  , a : A
//  } -> let cmp = compose(~A,~A,~A)
//       cmp(cmp(x,y),z)(a) == cmp(x,cmp(y,z))(a)
//  refl(~x(y(z(a))))