1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "formal_topology/basic_pairs_to_o-basic_pairs.ma".
16 include "formal_topology/o-basic_pairs_to_o-basic_topologies.ma".
17 include "formal_topology/basic_pairs.ma".
18 include "formal_topology/basic_topologies.ma".
20 definition basic_topology_of_basic_pair: basic_pair → basic_topology.
22 letin obt ≝ (OR (BP_to_OBP bp));
27 | apply (oA_is_saturation obt);
28 | apply (oJ_is_reduction obt);
29 | apply (Ocompatibility obt); ]
32 definition continuous_relation_of_relation_pair:
33 ∀BP1,BP2.relation_pair BP1 BP2 →
34 continuous_relation (basic_topology_of_basic_pair BP1) (basic_topology_of_basic_pair BP2).
36 letin ocr ≝ (OR⎽⇒ (BP_to_OBP⎽⇒ rp));
39 | apply (Oreduced ?? ocr);
40 | apply (Osaturated ?? ocr); ]
43 alias symbol "compose" (instance 3) = "category1 composition".
44 alias symbol "compose" (instance 3) = "category1 composition".
45 record functor1 (C1: category1) (C2: category1) : Type2 ≝
46 { map_objs1:1> C1 → C2;
47 map_arrows1: ∀S,T. unary_morphism1 (arrows1 ? S T) (arrows1 ? (map_objs1 S) (map_objs1 T));
48 respects_id1: ∀o:C1. map_arrows1 ?? (id1 ? o) =_1 id1 ? (map_objs1 o);
50 ∀o1,o2,o3.∀f1:arrows1 ? o1 o2.∀f2:arrows1 ? o2 o3.
51 map_arrows1 ?? (f2 ∘ f1) =_1 map_arrows1 ?? f2 ∘ map_arrows1 ?? f1}.
54 definition BTop_of_BP: functor1 BP BTop.
56 [ apply basic_topology_of_basic_pair
57 | intros; constructor 1 [ apply continuous_relation_of_relation_pair; ]
62 lemma BBBB_faithful : failthful2 ?? VVV