Changed (I was following VV)


On Tue, Sep 3, 2013 at 11:56 PM, Andrej Bauer <notifications@github.com>wrote:

> In theories/hit/epi.v:
>
> >
> > -Lemma uahp `{ua:Univalence}:
> > -  forall P P': hProp, (P->P') -> (P' -> P) -> P = P'.
> > +Section AssumingUA.
> > +(** The univalence axiom for HProp *)
> > +(** We need fs to be able to find hprop_trunc *)
> > +Context `{fs:Funext} `{ua:Univalence}.
> > +Lemma uahp' : forall P P': sigT IsHProp, (P.1<->P'.1) -> P = P'.
>
> These are extremely unhelpful names for lemmas, and they do not seem to be
> commented either.
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/206/files#r6139635>
> .
>