The Coq mailing list

[roconnor AT theorem.ca]

I have a record structure for metric spaces called MetricSpace.  There is 
a coercion to it's type of universe ms : MetricSpace >-> Sortclass.

I have a record type for uniformly continuous functions between metric 
spaces called UCFunction : MetricSpace -> MetricSpace -> Type. The 
representitives are functions, so there is a coercion declared
ucfun : UCFunction >-> Funclass.

The space of uniformly continuous functions also is a metric space, so I 
can define UCSpace : MetricSpace -> MetricSpace -> MetricSpace.

The problem is that if I make a parameter (f:(UCFunction Y Z)), it isn't 
seen as a metric space so I can't curry them to allow
(g:(UCFunction X (UCFunction Y Z)).  If instead I use UCSpace then if I 
have (f:(ms (UCSpace Y Z)))---I'm showing the coercion here---then I 
cannot treat f as a function and write (f y) for (y:ms Y).

So I suspect that I cannot have a type of uniformly continuous functions 
that is automatically coerced into both a metric space and a Funclass. 
But maybe someone knows a trick using identity coercions and or canonical 
structures that can solve this problem.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''