I decided to take a simpler approach.


On Sun, Sep 1, 2013 at 9:17 AM, Bas Spitters <b.a.w.spitters@gmail.com>wrote:

> Thanks for the suggestions. I have now applied them in a new commit.
>
> If it does not make sense, let me think a bit more, I need to run now.
>
>
> On Fri, Aug 30, 2013 at 11:17 PM, Jason Gross <notifications@github.com>wrote:
>
>> In theories/HProp.v:
>>
>> > -Global Existing Instance isp.
>> > -
>> > -Definition issig_hProp
>> > -: { propT : Type & IsHProp propT } <~> hProp.
>> > -Proof.
>> > -  issig BuildhProp propT isp.
>> > +(** We use both the Sigma type of propositions and the record type of propositions.
>> > +The latter allows us to automatically find a proof that a type is a proposition.
>> > +
>> > +Setting things up in this way allows us to define coercions from one type to the other.
>> > +So, a theory stated about one type can be apply to the other. It's not magic, but it is convenient.
>> > +
>> > +We should explore this some more and then apply this to more record types.
>> > +*)
>> > +
>> > +Class total2 {T} (P: T -> Type) := tpair2 { tp1 :> T ; tp2 :> P tp1 }.
>>
>> What does having total2 add? In particular, why do we want it to be a
>> class (i.e., why can't we just use sigT), and why do we want it to be
>> inconvertible with sigT (i.e., why isn't this Class total2 {T} {P : T ->
>> Type} := tpair2 : sigT P)?
>>
>> —
>> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/206/files#r6096467>
>> .
>>
>
>