General Subobjectclassifier

I am not entirely sure that this approach is more readable, but it is
shorter; see the commit.

On Thu, Sep 11, 2014 at 7:04 PM, Mike Shulman <notifications@github.com>
wrote:

> In theories/ObjectClassifier.v:
>
> >  Definition pullback {A0 B C} (f:B-> A0) (g:C->A0):= {b:B & {c:C & f b = g c}}.
> >
> >  Section FamPow.
> > +(** This seems like a useful strengthening of [BiInv].
> > +It is easier to work with than [Equiv]. *)
> > +Definition BiInvPair {A B} (f : A -> B) (g : B -> A) : Type
>
> In the book, we called this qinv. But I don't think it should be
> dignified with a name. Rather than proving PowisoFam and then FamequivPow,
> you should just go directly to FamequivPow, beginning by applying
> equiv_adjointify and then reproduce the current proof of PowisoFam.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/487/files#r17433107>.
>