(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "formal_topology/basic_topologies.ma".

definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).

coercion btop_carr.

definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.

coercion btop_carr'.

definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
 intros; constructor 1;
  [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
    intros; simplify; split; intro; cases H1; cases x; exists [1,3: apply w]
    split; try assumption; [ apply (. H‡#) | apply (. H \sup -1‡#) ] assumption
  | intros; split; intros 2; cases f; exists; [1,3: apply w] cases x; split;
    try assumption; [ apply (. #‡H) | apply (. #‡H \sup -1)] assumption]
qed.

interpretation "downarrow" 'downarrow a = (fun_1 __ (downarrow _) a).

definition ffintersects: ∀S:BTop. binary_morphism1 (Ω \sup S) (Ω \sup S) (Ω \sup S).
 intros; constructor 1;
  [ apply (λU,V. ↓U ∩ ↓V);
  | intros; apply (.= (†H)‡(†H1)); apply refl1]
qed.

interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).

record formal_topology: Type ≝
 { bt:> BTop;
   converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
 }.

definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.

coercion bt'.

definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
 intros; constructor 1;
  [ apply (λb,c:S. (singleton S b) ↓ (singleton S c));
  | intros; apply (.= (†H)‡(†H1)); apply refl1]
qed.

interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).

record formal_map (S,T: formal_topology) : Type ≝
 { cr:> continuous_relation_setoid S T;
   C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;
   C2: extS ?? cr T = S
 }.

definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
 λFT1,FT2,c. cr FT1 FT2 c.

coercion cr'.

definition formal_map_setoid: formal_topology → formal_topology → setoid1.
 intros (S T); constructor 1;
  [ apply (formal_map S T);
  | constructor 1;
     [ apply (λf,f1: formal_map S T.f=f1);
     | simplify; intros 1; apply refl1
     | simplify; intros 2; apply sym1
     | simplify; intros 3; apply trans1]]
qed.

definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
 λFT1,FT2,c.cr ?? c.

coercion cr''.

definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
 λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).

coercion cr'''.

axiom C1':
 ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
  extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.

definition formal_map_composition:
 ∀o1,o2,o3: formal_topology.
  binary_morphism1
   (formal_map_setoid o1 o2)
   (formal_map_setoid o2 o3)
   (formal_map_setoid o1 o3).
 intros; constructor 1;
  [ intros; whd in c c1; constructor 1;
     [ apply (comp1 BTop ??? c c1);
     | intros;
       apply (.= (extS_com ??? c c1 ?));
       apply (.= †(C1 ?????));
       apply (.= (C1' ?????));
       apply (.= ((†((extS_singleton ????) \sup -1))‡(†((extS_singleton ????) \sup -1))));
       apply (.= (extS_com ??????)\sup -1 ‡ (extS_com ??????) \sup -1);
       apply (.= (extS_singleton ????)‡(extS_singleton ????));
       apply refl1;
     | apply (.= (extS_com ??? c c1 ?));
       apply (.= (†(C2 ???)));
       apply (.= (C2 ???));
       apply refl1;]
  | intros; simplify;
    change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
    apply prop1; assumption]
qed.