Universal properties without funext, and localization

See <http://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/> for a detailed description of the contents of this PR.
Other things being equal, I tend to prefer general solutions, for
consistency and readability, so I'd rather stick with %nat here.
On Nov 9, 2014 2:17 AM, "Jason Gross" <notifications@github.com> wrote:

> In theories/ReflectiveSubuniverse.v:
>
> > -  := (precomp P Q)^-1 f.
> > -
> > -  Local Definition O_rec_beta' {P Q : Type} `{In O Q} (f : P -> Q) (x : P)
> > -  : O_rec' f (to O P x) = f x
> > -  := ap10 (eisretr (precomp P Q) f) x.
> > -
> > -  Local Definition O_indpaths' {P Q : Type} `{In O Q}
> > -        (g h : O P -> Q) (p : g o to O P == h o to O P)
> > -  : g == h.
> > -  Proof.
> > -    apply ap10.
> > -    refine ((eissect (precomp P Q) g)^ @ _ @ eissect (precomp P Q) h).
> > -    apply ap.
> > -    apply path_arrow, p.
> > -  Defined.
> > +  := (fst (extendable_to_O O 1%nat) f).1.
>
> There are insane solutions, such as making 1 a notation for a typeclass
> that can be either a nat or a path...
>
> But, yes, for things you pose, there's probably not really a better way
> than adjusting the overall scope stack, or using %nat. (I still think
> that, in the line this particular comment thread is on, you should use
> Arguments and drop the %nat. It's just not a fully general solution.)
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/603/files#r20057883>.
>