Require Import Category.Core Functor.Core.
Require Import Pseudofunctor.FromFunctor.
Require Import Cat.Core.
Require Import Grothendieck.PseudofunctorToCat.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

Local Open Scope morphism_scope.

Section Grothendieck.
  Context `{Funext}.

  Variable P : PreCategory → Type.
  (*Context `{forall C, IsHProp (P C)}.*)
  Context `{HF : ∀ C D, P C → P D → IsHSet (Functor C D)}.

  Local Notation cat := (@sub_pre_cat _ P HF).

  Variable C : PreCategory.
  Variable F : Functor C cat.

  Definition category : PreCategory
    := category (pseudofunctor_of_functor_to_cat F).

  Definition pr1 : Functor category C
    := pr1 (pseudofunctor_of_functor_to_cat F).
End Grothendieck.