helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* Project started Wed Oct 12, 2005 ***************************************)
  16
  17 set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs".
  18
  19 include "../../library/logic/connectives.ma".
  20
  21 (* ACZEL CATEGORIES:
  22    - We use typoids with a compatible membership relation
  23    - The category is intended to be the domain of the membership relation
  24    - The membership relation is necessary because we need to regard the
  25      domain of a propositional function (ie a predicative subset) as a
  26      quantification domain and therefore as a category, but there is no
  27      type in CIC representing the domain of a propositional function
  28    - We set up a single equality predicate, parametric on the category,
  29      defined as the reflexive, symmetic, transitive and compatible closure
  30      of the csub1 predicate given inside the category. Then we prove the
  31      properties of the equality that usually are axiomatized inside the
  32      category structure. This makes categories easier to use
  33 *)
  34
  35 record Class: Type \def {
  36    class: Type;
  37    cin  : class \to Prop;
  38    csub1: class \to class \to Prop
  39 }.
  40
  41 coercion class.
  42
  43 inductive eq (C:Class) (c1:C): C \to Prop \def
  44    | eq_refl:   cin ? c1 \to eq ? c1 c1
  45    | eq_sing_r: \forall c2,c3.
  46                 eq ? c1 c2 \to cin ? c3 \to csub1 ? c2 c3 \to eq ? c1 c3
  47    | eq_sing_l: \forall c2,c3.
  48                 eq ? c1 c2 \to cin ? c3 \to csub1 ? c3 c2 \to eq ? c1 c3.
  49
  50 theorem eq_cl: \forall C,c1,c2. eq ? c1 c2 \to cin C c1 \land cin C c2.
  51 intros; elim H; clear H; clear c2;
  52    [ auto | decompose H2; auto | decompose H2; auto ].
  53 qed.
  54
  55 theorem eq_trans: \forall C,c2,c1,c3.
  56                   eq C c2 c3 \to eq ? c1 c2 \to eq ? c1 c3.
  57 intros 5; elim H; clear H; clear c3;
  58    [ auto
  59    | apply eq_sing_r; [||| apply H4 ]; auto
  60    | apply eq_sing_l; [||| apply H4 ]; auto
  61    ].
  62 qed.
  63
  64 theorem eq_conf_rev: \forall C,c2,c1,c3.
  65                      eq C c3 c2 \to eq ? c1 c2 \to eq ? c1 c3.
  66 intros 5; elim H; clear H; clear c2;
  67    [ auto
  68    | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
  69      apply H2; apply eq_sing_l; [||| apply H4 ]; auto
  70    | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
  71      apply H2; apply eq_sing_r; [||| apply H4 ]; auto
  72    ].
  73 qed.
  74
  75 theorem eq_sym: \forall C,c1,c2. eq C c1 c2 \to eq C c2 c1.
  76 intros;
  77 lapply eq_cl; [ decompose Hletin |||| apply H ].
  78 auto.
  79 qed.
  80
  81 theorem eq_conf: \forall C,c2,c1,c3.
  82                  eq C c1 c2 \to eq ? c1 c3 \to eq ? c2 c3.
  83 intros.
  84 lapply eq_sym; [|||| apply H ].
  85 apply eq_trans; [| auto | auto ].
  86 qed.