V_______________________________________________________________ *)
include "arithmetics/exp.ma".
+include "basics/core_notation/fact_1.ma".
let rec fact n ≝
match n with
notation "- term 65 a" with precedence 65
for @{ 'uminus $a }.
-notation "a !"
- non associative with precedence 80
-for @{ 'fact $a }.
-
notation "\sqrt a"
non associative with precedence 65
for @{ 'sqrt $a }.
notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
for @{ 'powerset $A }.
+
notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
for @{ 'powerset $A }.
-notation < "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i}. $p)}.
-
-notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
-for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
-for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
-
notation "hvbox(a break ∈ b)" non associative with precedence 45
for @{ 'mem $a $b }.
notation "hvbox(a break ∪ b)" left associative with precedence 55
for @{ 'union $a $b }. (* \cup *)
-notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
-
(* other notations **********************************************************)
notation "hvbox(a break \approx b)" non associative with precedence 45
notation "hvbox(a break # b)" non associative with precedence 45
for @{ 'apart $a $b}.
-
-notation "hvbox(a break \circ b)"
- left associative with precedence 60
-for @{ 'compose $a $b }.
notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }.
notation > "↓ a" with precedence 60 for @{ 'downarrow $a }.
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+(* Core notation *******************************************************)
+
+notation "hvbox(a break \circ b)"
+ left associative with precedence 60
+for @{ 'compose $a $b }.
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+(* Core notation *******************************************************)
+
+notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+(* Core notation *******************************************************)
+
+notation "a !"
+ non associative with precedence 80
+for @{ 'fact $a }.
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+(* Core notation *******************************************************)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A|| This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ \ /
+ V_______________________________________________________________ *)
+
+(* Core notation *******************************************************)
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
V_______________________________________________________________ *)
include "basics/logic.ma".
+include "basics/core_notation/compose_2.ma".
(********** predicates *********)
V_______________________________________________________________ *)
include "basics/logic.ma".
+include "basics/core_notation/singl_1.ma".
(**** a subset of A is just an object of type A→Prop ****)
(* substraction *)
lemma substract_def:∀U.∀A,B:U→Prop. A-B ≐ A ∩ ¬B.
#U #A #B #w normalize /2/
-qed.
\ No newline at end of file
+qed.
(**************************************************************************)
include "formal_topology/cprop_connectives.ma".
+include "basics/core_notation/compose_2.ma".
inductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝
refl: eq A x x.
notation "r \sup ⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
notation > "r⎻" non associative with precedence 90 for @{'OR_f_minus $r}.
-*)
\ No newline at end of file
+*)
(* *)
(**************************************************************************)
+include "basics/core_notation/comprehension_2.ma".
include "formal_topology/categories.ma".
(*
inductive bool : Type[0] := true : bool | false : bool.
(* *)
(**************************************************************************)
+include "basics/core_notation/comprehension_2.ma".
include "formal_topology/subsets.ma".
(*
record binary_relation (A,B: SET) : Type[1] ≝
(**************************************************************************)
include "formal_topology/categories.ma".
+include "basics/core_notation/singl_1.ma".
+include "basics/core_notation/subset_1.ma".
(*
record powerset_carrier (A: objs1 SET) : Type[1] ≝ { mem_operator: A ⇒_1 CPROP }.
interpretation "powerset low" 'powerset A = (powerset_carrier A).
include "hott/types.ma".
+include "basics/core_notation/compose_2.ma".
(* * * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)
notation "- term 65 a" with precedence 65
for @{ 'uminus $a }.
-notation "a !"
- non associative with precedence 80
-for @{ 'fact $a }.
-
notation "\sqrt a"
non associative with precedence 65
for @{ 'sqrt $a }.
notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
for @{ 'powerset $A }.
-notation < "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i | term 19 p })" with precedence 90
-for @{ 'subset (\lambda ${ident i}. $p)}.
-
-notation < "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
-for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
-
-notation > "hvbox({ ident i ∈ term 19 s | term 19 p })" with precedence 90
-for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
-
notation "hvbox(a break ∈ b)" non associative with precedence 45
for @{ 'mem $a $b }.
notation "hvbox(a break ∪ b)" left associative with precedence 55
for @{ 'union $a $b }. (* \cup *)
-notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
-
notation "hvbox(a break \approx b)" non associative with precedence 45
for @{ 'napart $a $b}.
notation "hvbox(a break # b)" non associative with precedence 45
for @{ 'apart $a $b}.
-*)
-
-notation "hvbox(a break \circ b)"
- left associative with precedence 60
-for @{ 'compose $a $b }.
-(*
notation < "↓ \ensp a" with precedence 60 for @{ 'downarrow $a }.
notation > "↓ a" with precedence 60 for @{ 'downarrow $a }.
include "arithmetics/nat.ma".
include "basics/lists/list.ma".
+include "basics/core_notation/singl_1.ma".
interpretation "iff" 'iff a b = (iff a b).
| #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
-*)
\ No newline at end of file
+*)
include "basics/vectors.ma".
include "basics/finset.ma".
+include "basics/core_notation/compose_2.ma".
(* include "basics/relations.ma". *)
record tape (sig:FinSet): Type[0] ≝
include "tutorial/chapter5.ma".
+include "basics/core_notation/singl_1.ma".
(*************************** Naive Set Theory *********************************)