-
Notifications
You must be signed in to change notification settings - Fork 1
/
lB.v
75 lines (40 loc) · 2.13 KB
/
lB.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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
(** * The type of the unital lBsystems
By Vladimir Voevodsky, started on Jan. 18, 2015 *)
Unset Automatic Introduction.
Require Export lBsystems.lB_non_unital.
Require Export lBsystems.lB0.
(** Condition dltT *)
Definition dltT_type { BB : lB_nu } ( dlt : dlt_layer ( @T_op BB ) ) :=
dlt.dltT_type ( @T_ax0 BB ) ( @T_ax1b BB ) ( @Tt_op BB ) ( dlt_ax1 dlt ) .
(** Condition dltS *)
Definition dltS_type { BB : lB_nu } ( dlt : dlt_layer ( @T_op BB ) ) :=
dlt.dltS_type ( @T_ax1b BB ) ( @S_ax0 BB ) ( @St_op BB ) ( dlt_ax1 dlt ) .
(** Condition SdltT *)
Definition SdltT_type { BB : lB_nu } ( dlt : dlt_layer ( @T_op BB ) ) :=
dlt.SdltT_type ( @T_ax0 BB ) ( @T_ax1a BB ) ( dlt_ax1 dlt ) ( @S_op BB ) .
(** Condition StdltTt *)
Definition StdltTt_type { BB : lB_nu } ( dlt : dlt_layer ( @T_op BB ) ) :=
dlt.StdltTt_type ( @T_ax0 BB ) ( @T_ax1a BB ) ( dlt_ax1 dlt ) ( @Tt_ax1 BB ) ( @St_op BB ) .
(** Condition dltSid *)
Definition dltSid_type { BB : lB_nu } ( dlt : dlt_layer ( @T_op BB ) ) :=
dlt.dltSid_type ( @T_ax1b BB ) ( dlt_ax1 dlt ) ( @St_op BB ) .
(** Unital lBsystem *)
Definition lB :=
total2 ( fun BB : lB_nu =>
total2 ( fun dlt : dlt_layer ( @T_op BB ) =>
dirprod
( dirprod
( dirprod ( dltT_type dlt ) ( dltS_type dlt ) )
( dirprod ( SdltT_type dlt ) ( StdltTt_type dlt ) ) )
( dltSid_type dlt ) ) ) .
Definition lB_to_lB_nu : lB -> lB_nu := pr1 .
Coercion lB_to_lB_nu : lB >-> lB_nu .
Definition lB_to_lB0 ( BB : lB ) : lB0system :=
tpair ( fun BB : lB0system_non_unital => dlt_layer ( @T_op BB ) ) BB ( pr1 ( pr2 BB ) ) .
Coercion lB_to_lB0 : lB >-> lB0system .
Definition dltT { BB : lB } : dltT_type BB := pr1 ( pr1 ( pr1 ( pr2 ( pr2 BB ) ) ) ) .
Definition dltS { BB : lB } : dltS_type BB := pr2 ( pr1 ( pr1 ( pr2 ( pr2 BB ) ) ) ) .
Definition SdltT { BB : lB } : SdltT_type BB := pr1 ( pr2 ( pr1 ( pr2 ( pr2 BB ) ) ) ) .
Definition StdltTt { BB : lB } : StdltTt_type BB := pr2 ( pr2 ( pr1 ( pr2 ( pr2 BB ) ) ) ) .
Definition dltSid { BB : lB } : dltSid_type BB := pr2 ( pr2 ( pr2 BB ) ) .
(* End of the file lB.v *)