From 04111561e190485400ba91eb274b2acb1b25a817 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 3 Jan 2009 18:30:01 +0000 Subject: [PATCH] Universe level fixed (litterally). --- .../contribs/formal_topology/overlap/o-basic_topologies.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma index be985a43c..61334e540 100644 --- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma +++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma @@ -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); -- 2.39.2