On Fri, Jan 18, 2013 at 12:58 PM, Bill Richter <
rich...@math.northwestern.edu> wrote:
> Thanks, Ramana! I think I wasn't clear. As Rob explained, there's a type
> quantification problem: we can't define Fibration p E B.
I think I was just trying to explain why you can't define it (without type
quantification).
> Any time you wish to write Fibration p E B, you must write instead
> !M:A->bool. HLP p E B M.
Though you'll have to be careful when writing that if the type variable A
is already in your context.
> With that in mind, I don't understand your objection
>
> It's not just an annoyance. Suppose the assumption you have to
> drag around was instead the definition of Fibration.
>
> --
> Best,
> Bill
>
------------------------------------------------------------------------------
Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and
much more. Get web development skills now with LearnDevNow -
350+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122812
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
