(**************************************************************************)
(*       ___                                                              *)
(*      ||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_pairs.ma".
include "formal_topology/o-basic_pairs.ma".
include "formal_topology/relations_to_o-algebra.ma".

definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair.
 intro b;
 constructor 1;
  [ apply (POW (concr b));
  | apply (POW (form b));
  | apply (POW⎽⇒ ?); apply (rel b); ]
qed.

definition o_relation_pair_of_relation_pair:
 ∀BP1,BP2. relation_pair BP1 BP2 →
  Orelation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2).
 intros;
 constructor 1;
  [ unfold o_basic_pair_of_basic_pair; simplify; apply (POW⎽⇒ ?); apply (r\sub \c); 
  | apply (map_arrows2 ?? POW (form BP1) (form BP2) (r \sub \f));
  | apply (.= (respects_comp2 ?? POW (concr BP1) (concr BP2) (form BP2)  r\sub\c (⊩\sub BP2) )^-1);
    cut ( ⊩ \sub BP2 ∘ r \sub \c =_12 r\sub\f ∘ ⊩ \sub BP1) as H;
    [ apply (.= †H);
      apply (respects_comp2 ?? POW (concr BP1) (form BP1) (form BP2) (⊩\sub BP1) r\sub\f);
    | apply commute;]]
qed.

lemma o_relation_pair_of_relation_pair_is_morphism : 
  ∀S,T:category2_of_category1 BP.    
  ∀a,b:arrows2 (category2_of_category1 BP) S T.a=b → 
   (eq2 (arrows2 OBP (o_basic_pair_of_basic_pair S) (o_basic_pair_of_basic_pair T))) 
    (o_relation_pair_of_relation_pair S T a) (o_relation_pair_of_relation_pair S T b).
intros 2 (S T);       
      intros (a b Eab); split; unfold o_relation_pair_of_relation_pair; simplify;
       unfold o_basic_pair_of_basic_pair; simplify;
       [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); 
       | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
       | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x);
       | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
       simplify;
       apply (prop12);
       apply (.= (respects_comp2 ?? POW (concr S) (concr T) (form T) (a\sub\c) (⊩\sub T))^-1);
       apply sym2;
       apply (.= (respects_comp2 ?? POW (concr S) (concr T) (form T) (b\sub\c) (⊩\sub T))^-1);
       apply sym2;
       apply prop12;
       apply Eab;
qed.

lemma o_relation_pair_of_relation_pair_morphism : 
  ∀S,T:category2_of_category1 BP.
  unary_morphism2 (arrows2 (category2_of_category1 BP) S T)
   (arrows2 OBP (o_basic_pair_of_basic_pair S) (o_basic_pair_of_basic_pair T)).
intros (S T);
   constructor 1;
     [ apply (o_relation_pair_of_relation_pair S T);
     | apply (o_relation_pair_of_relation_pair_is_morphism S T)]
qed.

lemma o_relation_pair_of_relation_pair_morphism_respects_id:
 ∀o:category2_of_category1 BP.
  o_relation_pair_of_relation_pair_morphism o o (id2 (category2_of_category1 BP) o)
  = id2 OBP (o_basic_pair_of_basic_pair o).
   simplify; intros; whd; split; 
       [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); 
       | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
       | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x);
       | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
    simplify;
    apply prop12;
    apply prop22;[2,4,6,8: apply rule #;]
    apply (respects_id2 ?? POW (concr o));
qed. 

lemma o_relation_pair_of_relation_pair_morphism_respects_comp:
  ∀o1,o2,o3:category2_of_category1 BP.
  ∀f1:arrows2 (category2_of_category1 BP) o1 o2.
  ∀f2:arrows2 (category2_of_category1 BP) o2 o3.
  (eq2 (arrows2 OBP (o_basic_pair_of_basic_pair o1) (o_basic_pair_of_basic_pair o3)))
    (o_relation_pair_of_relation_pair_morphism o1 o3 (f2 ∘ f1))
    (comp2 OBP ???
      (o_relation_pair_of_relation_pair_morphism o1 o2 f1)
      (o_relation_pair_of_relation_pair_morphism o2 o3 f2)).
   simplify; intros; whd; split;
       [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); 
       | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
       | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x);
       | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
    simplify;
    apply prop12;
    apply prop22;[2,4,6,8: apply rule #;]
    apply (respects_comp2 ?? POW (concr o1) (concr o2) (concr o3) f1\sub\c f2\sub\c);
qed.

definition BP_to_OBP: carr3 (arrows3 CAT2 (category2_of_category1 BP) OBP).
 constructor 1;
  [ apply o_basic_pair_of_basic_pair;
  | intros; apply o_relation_pair_of_relation_pair_morphism;
  | apply o_relation_pair_of_relation_pair_morphism_respects_id;
  | apply o_relation_pair_of_relation_pair_morphism_respects_comp;]
qed.

theorem BP_to_OBP_faithful: faithful2 ?? BP_to_OBP.
 intros 5 (S T); change with ( (⊩) ∘ f \sub \c = (⊩) ∘ g \sub \c);
 apply (POW_faithful);
 apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) f \sub \c (⊩ \sub T));
 apply sym2;
 apply (.= respects_comp2 ?? POW (concr S) (concr T) (form T) g \sub \c (⊩ \sub T));
 apply sym2;
 apply e;
qed.

theorem BP_to_OBP_full: full2 ?? BP_to_OBP. 
 intros 3 (S T); 
 cases (POW_full (concr S) (concr T) (Oconcr_rel ?? f)) (gc Hgc);
 cases (POW_full (form S) (form T) (Oform_rel ?? f)) (gf Hgf);
 exists[
   constructor 1; [apply gc|apply gf]
   apply (POW_faithful);
   apply (let xxxx ≝POW in .= respects_comp2 ?? POW (concr S) (concr T) (form T) gc (rel T));
   apply rule (.= Hgc‡#);
   apply (.= Ocommute ?? f);
   apply (.= #‡Hgf^-1);
   apply (let xxxx ≝POW in (respects_comp2 ?? POW (concr S) (form S) (form T) (rel S) gf)^-1)]
 split;
  [ change in match or_f_minus_star_ with (λq,w,x.fun12 ?? (or_f_minus_star q w) x); 
  | change in match or_f_minus_ with (λq,w,x.fun12 ?? (or_f_minus q w) x);
  | change in match or_f_ with (λq,w,x.fun12 ?? (or_f q w) x);
  | change in match or_f_star_ with (λq,w,x.fun12 ?? (or_f_star q w) x);]
 simplify; apply (†(Hgc‡#));
qed.