Why am I doing this?

module type Type = sig
  module type T
end

module Equality = (struct
  module Eq(Typ:Type)(X:Typ.T)(Y:Typ.T) = struct
    module type T = sig end
  end

  module Eq_refl(Typ:Type)(X:Typ.T) = (struct
  end : Eq(Typ)(X)(X).T)
  
  module Eq_trans(Typ:Type)(X:Typ.T)(Y:Typ.T)(Z:Typ.T)
      (E1:Eq(Typ)(X)(Y).T)
      (E2:Eq(Typ)(Y)(Z).T)
    = (struct end : Eq(Typ)(X)(Z).T)
    
  module Eq_symm(Typ:Type)(X:Typ.T)(Y:Typ.T)(E:Eq(Typ)(X)(Y).T) 
    = (struct end : Eq(Typ)(Y)(X).T)

  module Eq_ext(A:Type)(B:Type)(X:A.T)(Y:A.T)(E:Eq(A)(X)(Y).T)
      (F:functor(Arg:A.T)->B.T)
    = (struct end : Eq(B)(F(X))(F(Y)).T)
end : sig
  module Eq(Typ:Type)(X:Typ.T)(Y:Typ.T) : sig
    module type T
  end

  module Eq_refl(Typ:Type)(X:Typ.T) : Eq(Typ)(X)(X).T
  
  module Eq_trans(Typ:Type)(X:Typ.T)(Y:Typ.T)(Z:Typ.T)
      (E1:Eq(Typ)(X)(Y).T)
      (E2:Eq(Typ)(Y)(Z).T)
    : Eq(Typ)(X)(Z).T
    
  module Eq_symm(Typ:Type)(X:Typ.T)(Y:Typ.T)(E:Eq(Typ)(X)(Y).T)
    : Eq(Typ)(Y)(X).T
    
  module Eq_ext(A:Type)(B:Type)(X:A.T)(Y:A.T)(E:Eq(A)(X)(Y).T)
      (F:functor(Arg:A.T)->B.T)
    : Eq(B)(F(X))(F(Y)).T
end)