-
Notifications
You must be signed in to change notification settings - Fork 1
/
prelB.v
50 lines (23 loc) · 1.18 KB
/
prelB.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
(** ** Pre-lB-systems (unital)
By Vladimir Voevodsky, split off the file prelBsystems.v on March 3, 2015 *)
Unset Automatic Introduction.
Require Export lBsystems.prelB_non_unital.
Require Export lBsystems.dlt.
(** ** pre-lB-systems (unital) *)
(** *** The main layers *)
(** **** The structure formed by operations dlt *)
Definition dlt_layer_0 ( BB : lBsystem_carrier ) :=
total2 ( fun dlt : dlt_ops_type BB => dlt_ax0_type dlt ) .
Definition dlt_layer_0_to_dlt_ops_type ( BB : lBsystem_carrier ) :
dlt_layer_0 BB -> dlt_ops_type BB := pr1 .
Coercion dlt_layer_0_to_dlt_ops_type : dlt_layer_0 >-> dlt_ops_type .
(** **** Complete definition of a (unital) pre-lB-system *)
Definition prelBsystem :=
total2 ( fun BB : prelBsystem_non_unital => dlt_layer_0 BB ) .
Definition prelBsystem_pr1 : prelBsystem -> prelBsystem_non_unital := pr1 .
Coercion prelBsystem_pr1 : prelBsystem >-> prelBsystem_non_unital .
(** *** Access functions for the operation dlt and its zeros axiom *)
Definition dlt_op { BB : prelBsystem } : dlt_ops_type BB := pr2 BB .
Definition dlt_ax0 { BB : prelBsystem } : dlt_ax0_type ( @dlt_op BB ) :=
pr2 ( pr2 BB ) .
(* End of the file prelB.v *)