General Subobjectclassifier

Done. It is all in the new commit.

On Thu, Sep 11, 2014 at 5:40 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/ObjectClassifier.v:
>
> > @@ -88,4 +96,48 @@ simpl in p. by path_induction.
> >  Qed.
> >
> >  End FamPow.
> > +
> > +Section Subobjectclassifier.
> > +(** We prove that hProp is the subobject classifier *)
> > +(** In fact, the proof works for general mere predicates on [Type],
> > +not just [IsHProp], truncations and modalities are important examples.*)
> > +Variable A:Type.
> > +Variable isP:Type -> Type.
> > +Variable ishprop_isP: forall I, IsHProp (isP I).
> > +Definition IsPfibered {I} (f:I->A):=forall i, isP (hfiber f i).
> > +Definition PFam := (sig (fun F:Fam A => IsPfibered (pr2 F))).
> > +(* Bug: abstract should accept more than one tactic.
>
> *nods* Make a feature request for one or both of these on the bug tracker?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/487/files#r17428506>.
>