I know. Do you know why this is preferred?
In this way, when we decide to move the lemma, we can also move the Require.

I don't have strong feelings about this. A better dependency tool might
help here.


On Mon, Sep 2, 2013 at 5:48 PM, Jason Gross <notifications@github.com>wrote:

> In theories/HProp.v:
>
> > -Proof.
> > -  issig BuildhProp propT isp.
> > -Defined.
> > -
> > -Lemma sigma_prop_eq {A} {P : A -> hProp}: forall u v : sigT P, u.1 = v.1 -> u=v.
> > -Proof.
> > -intros ? ? H.
> > -apply path_sigma with H. apply allpath_hprop.
> > -Defined.
> > +(** Every hProp is a subclass of IsHProp *)
> > +Class hProp := hp { hproptype : Type ; isp :> IsHProp hproptype}.
> > +(** Avoid hproptype, isp automatically eating a type *)
> > +Implicit Arguments hproptype.
> > +Implicit Arguments isp.
> > +Coercion hproptype: hProp >-> Sortclass.
> > +Require Import Unit Empty.
>
> Nit: I think it's generally preferred to include all the Require Imports
> at the top of the file (or, at least, that is how I've seen it usually
> done).
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/206/files#r6112803>
> .
>