]> matita.cs.unibo.it Git - helm.git/commitdiff
Universe level fixed (litterally).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 Jan 2009 18:30:01 +0000 (18:30 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 3 Jan 2009 18:30:01 +0000 (18:30 +0000)
helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma

index be985a43cefd551e01fd6ea942dcc220dea8b622..61334e54080fe84472942e6e88556d3ea02c9efe 100644 (file)
@@ -15,7 +15,7 @@
 include "o-algebra.ma".
 include "o-saturations.ma".
 
-record basic_topology: Type ≝
+record basic_topology: Type2 ≝
  { carrbt:> OA;
    A: carrbt ⇒ carrbt;
    J: carrbt ⇒ carrbt;
@@ -29,7 +29,7 @@ lemma hint: OA → objs2 OA.
 qed.
 coercion hint.
 
-record continuous_relation (S,T: basic_topology) : Type ≝
+record continuous_relation (S,T: basic_topology) : Type2 ≝
  { cont_rel:> arrows2 OA S T;
    (* reduces uses eq1, saturated uses eq!!! *)
    reduced: ∀U. U = J ? U → cont_rel U = J ? (cont_rel U);