Merge pull request #144 from Columbus240/SetsUniverses

Some universes in `Sets` are necessarily equal

Instance/Sets.v

@@ -74,14 +74,14 @@ Qed.
       identity: typical identity of sets
    composition: composition of set maps, preserving equivalence
  *)
-Program Definition Sets@{o h so sh p} : Category@{so sh p} := {|
-  obj     := SetoidObject@{o p} : Type@{so};
-  hom     := λ x y, SetoidMorphism@{o h p} x y : Type@{sh};
-  homset  := @SetoidMorphism_Setoid@{o h p};
-  id      := @setoid_morphism_id@{o h p};
-  compose := @setoid_morphism_compose@{o h p};
-
-  compose_respects := @setoid_morphism_compose_respects@{o h p}
+Program Definition Sets@{o so} : Category@{so o o} := {|
+  obj     := SetoidObject@{o o} : Type@{so};
+  hom     := λ x y, SetoidMorphism@{o o o} x y : Type@{o};
+  homset  := @SetoidMorphism_Setoid@{o o o};
+  id      := @setoid_morphism_id@{o o o};
+  compose := @setoid_morphism_compose@{o o o};
+
+  compose_respects := @setoid_morphism_compose_respects@{o o o}
 |}.
 
 Require Import Category.Theory.Isomorphism.

Theory/Adjunction.v

@@ -36,11 +36,11 @@ Context {U : C ⟶ D}.
 Reserved Notation "⌊ f ⌋".
 Reserved Notation "⌈ f ⌉".
 
-(* o3 h3 p3 are universes larger than either C or D. *)
-Class Adjunction@{o3 h3 p3 so sh sp} := {
+(* o3 p3 are universes larger than either C or D. *)
+Class Adjunction@{o3 p3 so sh sp} := {
   (* adj {x y} : F x ~{C}~> y ≊ x ~{D}~> U y *)
   adj {x y} :
-    @Isomorphism@{so sh p3} Sets@{o3 h3 so sh p3}
+    @Isomorphism@{so sh p3} Sets@{o3 so}
       {| carrier := @hom C (F x) y; is_setoid := @homset C (F x) y |}
       {| carrier := @hom D x (U y); is_setoid := @homset D x (U y) |}
     where "⌊ f ⌋" := (to   adj f)