Merge pull request #1812 from Alizter/ps/branch/add_universe_constrai…

…nts_in_graphquotient

add universe constraints in GraphQuotient

theories/Colimits/GraphQuotient.v

@@ -12,35 +12,40 @@ We use graph quotients to build up all our other non-recursive HITs. Their simpl
 Local Unset Elimination Schemes.
 
 Module Export GraphQuotient.
+ Section GraphQuotient.
 
-  Private Inductive GraphQuotient@{i j u}
-    {A : Type@{i}} (R : A -> A -> Type@{j}) : Type@{u} :=
+  Universes i j u.
+  Constraint i <= u, j <= u.
+  Context {A : Type@{i}}.
+
+  Private Inductive GraphQuotient (R : A -> A -> Type@{j}) : Type@{u} :=
   | gq : A -> GraphQuotient R.
 
-  Arguments gq {A R} a.
+  Arguments gq {R} a.
+
+  Context {R : A -> A -> Type@{j}}.
 
-  Axiom gqglue@{i j u}
-    : forall {A : Type@{i}} {R : A -> A -> Type@{j}} {a b : A},
-    R a b -> paths@{u} (@gq A R a) (gq b).
+  Axiom gqglue : forall {a b : A},
+    R a b -> paths (@gq R a) (gq b).
 
-  Definition GraphQuotient_ind@{i j u k} {A : Type@{i}} {R : A -> A -> Type@{j}}
-    (P : GraphQuotient@{i j u} R -> Type@{k})
-    (gq' : forall a, P (gq@{i j u} a))
-    (gqglue' : forall a b (s : R a b), gqglue@{i j u} s # gq' a = gq' b)
+  Definition GraphQuotient_ind
+    (P : GraphQuotient R -> Type@{k})
+    (gq' : forall a, P (gq a))
+    (gqglue' : forall a b (s : R a b), gqglue s # gq' a = gq' b)
     : forall x, P x := fun x =>
     match x with
     | gq a => fun _ => gq' a
     end gqglue'.
   (** Above we did a match with output type a function, and then outside of the match we provided the argument [gqglue'].  If we instead end with [| gq a => gq' a end.], the definition will not depend on [gqglue'], which would be incorrect.  This is the idiom referred to in ../../test/bugs/github1758.v and github1759.v. *)
 
-  Axiom GraphQuotient_ind_beta_gqglue@{i j u k}
-  : forall  {A : Type@{i}} {R : A -> A -> Type@{j}}
-    (P : GraphQuotient@{i j u} R -> Type@{k})
+  Axiom GraphQuotient_ind_beta_gqglue
+  : forall (P : GraphQuotient R -> Type@{k})
     (gq' : forall a, P (gq a))
     (gqglue' : forall a b (s : R a b), gqglue s # gq' a = gq' b)
     (a b: A) (s : R a b),
     apD (GraphQuotient_ind P gq' gqglue') (gqglue s) = gqglue' a b s.
 
+ End GraphQuotient.
 End GraphQuotient.
 
 Arguments gq {A R} a.

theories/Colimits/Quotient.v

@@ -7,8 +7,7 @@ Require Import Truncations.Core.
 
 Local Open Scope path_scope.
 
-
-(** * Quotient of a Type by an hprop-valued Relation
+(** * Quotient of a type by an hprop-valued relation
 
 We aim to model:
 <<
@@ -17,9 +16,7 @@ Inductive Quotient R : Type :=
    | qglue : forall x y, (R x y) -> class_of R x = class_of R y
    | ishset_quotient : IsHSet (Quotient R)
 >>
-We do this by defining the quotient as a truncated coequalizer.
-
-*)
+We do this by defining the quotient as a 0-truncated graph quotient. *)
 
 Definition Quotient@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : Type@{k}
   := Trunc@{k} 0 (GraphQuotient@{i j k} R).

theories/Sets/Ordinals.v

@@ -742,15 +742,16 @@ Qed.
 
 (** * Ordinal limit *)
 
-Definition image@{i j} {A : Type@{i}} {B : HSet@{j}} (f : A -> B) : Type@{i}
-  := Quotient (fun a a' : A => f a = f a').
+(** We can use PropResizing to resize the image of a function to whatever universe we want. *)
+Definition image@{i j |} `{PropResizing} {A : Type@{i}} {B : HSet@{j}} (f : A -> B) : Type@{i}
+  := Quotient@{i i i} (fun a a' : A => resize_hprop@{j i} (f a = f a')).
 
-Definition factor1 {A} {B : HSet} (f : A -> B)
+Definition factor1 `{PropResizing} {A} {B : HSet} (f : A -> B)
   : A -> image f
   := Quotient.class_of _.
 
-Lemma image_ind_prop {A} {B : HSet} (f : A -> B)
-  (P : image f -> Type) `{forall x, IsHProp (P x)}
+Lemma image_ind_prop@{i j k|} `{PropResizing} {A : Type@{i}} {B : HSet@{j}} (f : A -> B)
+  (P : image f -> Type@{k}) `{forall x, IsHProp (P x)}
   : (forall a : A, P (factor1 f a))
     -> forall x : image f, P x.
 Proof.
@@ -759,23 +760,39 @@ Proof.
   apply step.
 Qed.
 
-Definition image_rec {A} {B : HSet} (f : A -> B)
-      {C : HSet} (step : A -> C)
-  : (forall a a', f a = f a' -> step a = step a')
-    -> image f -> C
-  := Quotient_rec _ _ step.
+Definition image_rec@{i j k|} `{PropResizing} {A : Type@{i}} {B : HSet@{j}} (f : A -> B)
+      {C : HSet@{k}} (step : A -> C)
+  (p : forall a a', f a = f a' -> step a = step a')
+  : image f -> C.
+Proof.
+  snrapply Quotient_rec.
+  - exact _.
+  - exact step.
+  - simpl. intros x y q.
+    apply p.
+    apply (equiv_resize_hprop _)^-1.
+    exact q.
+Defined.
 
-Definition factor2 {A} {B : HSet} (f : A -> B)
-  : image f -> B
-  := Quotient_rec _ _ f (fun a a' fa_fa' => fa_fa').
+Definition factor2@{i j|} `{PropResizing} {A : Type@{i}} {B : HSet@{j}} (f : A -> B)
+  : image f -> B.
+Proof.
+  snrapply image_rec.
+  - exact f.
+  - intros a a' fa_fa'.
+    apply fa_fa'.
+Defined.
 
-Global Instance isinjective_factor2 `{Funext} {A} {B : HSet} (f : A -> B)
+Global Instance isinjective_factor2 `{PropResizing} `{Funext} {A} {B : HSet} (f : A -> B)
   : IsInjective (factor2 f).
 Proof.
   unfold IsInjective, image.
   refine (Quotient_ind_hprop _ _ _); intros x; cbn.
   refine (Quotient_ind_hprop _ _ _); intros y; cbn.
+  simpl; intros p.
   rapply qglue.
+  apply equiv_resize_hprop.
+  exact p.
 Qed.
 
 Definition limit `{Univalence} `{PropResizing}