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. Any time you wish to write Fibration p E B, you must write instead !M:A->bool. HLP p E B M. 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
