-
Notifications
You must be signed in to change notification settings - Fork 1
/
lB_carriers.v
111 lines (50 loc) · 2.94 KB
/
lB_carriers.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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
(** * Carriers of the B-systems defined in terms of two sorts and the length function
by Vladimir Voevodsky, file created on Jan. 6, 2015 *)
Unset Automatic Introduction.
Require Export lBsystems.hSet_ltowers.
(** **** lBsystem carriers *)
Definition lBsystem_carrier :=
total2 ( fun B : hSet_pltower =>
total2 ( fun TildeB : hSet =>
total2 ( fun dd : TildeB -> B =>
forall r : TildeB , ll ( dd r ) > 0 ) ) ) .
(** Note: the condition that the carrier of an lB-system is based on an h-set is used for the first
time in the formulation of the condition TT (later an axiom TT of the lBsystems). It is possible to avoid
the use of the h-set condition in the formulation of the TT and other axioms at the cost of making the
domains of applicability of these axioms to have a much longer description or of introducing additional
axioms to ensure that Lemma isover_T_T_2 and similar lemmas needed for the formulation of other axioms
hold. *)
Definition lBsystem_carrier_constr { B : hSet_pltower } { TildeB : hSet }
( dd : TildeB -> B ) ( is : forall r : TildeB, ll ( dd r ) > 0 ) : lBsystem_carrier .
Proof .
intros .
split with B .
split with TildeB .
exact ( tpair _ dd is ) .
Defined.
Definition lBsystem_carrier_to_ltower : lBsystem_carrier -> ltower := fun T => pr1 ( pr1 T ) .
Coercion lBsystem_carrier_to_ltower : lBsystem_carrier >-> ltower .
Definition lBsystem_carrier_pr1 : lBsystem_carrier -> hSet_pltower := pr1 .
Coercion lBsystem_carrier_pr1 : lBsystem_carrier >-> hSet_pltower .
Definition Tilde : lBsystem_carrier -> UU := fun BB => pr1 ( pr2 BB ) .
Definition dd { BB : lBsystem_carrier } : Tilde BB -> BB := pr1 ( pr2 ( pr2 BB ) ) .
Definition Tilde_dd { BB : lBsystem_carrier } ( X : BB ) :=
total2 ( fun r : Tilde BB => dd r = X ) .
Definition Tilde_dd_pr1 { BB : lBsystem_carrier } { X : BB } : Tilde_dd X -> Tilde BB := pr1 .
Coercion Tilde_dd_pr1 : Tilde_dd >-> Tilde .
Definition isasetBt ( BB : lBsystem_carrier ) : isaset ( Tilde BB ) :=
pr2 ( pr1 ( pr2 BB ) ) .
(** We can define a family BBn : nat -> UU by the formula
BBn BB := fun n => total2 ( fun X : BB => ll X = 0 )
The subobject in lBsystem_carrier defined by the condition
iscontr ( BBn BB 0 )
is equivalent to the type of type-and-term structures, i.e. presheaves on the category H
from the paper by Richard Garner, "Combinatorial structure of type dependency".
*)
Definition ll_dd { BB : lBsystem_carrier } ( r : Tilde BB ) : ll ( dd r ) > 0 :=
pr2 ( pr2 ( pr2 BB ) ) r .
(** **** Useful lemmas *)
Definition ll_dd_geh { BB : lBsystem_carrier } ( r : Tilde BB ) : ll ( dd r ) >= 1 :=
natgthtogehsn _ _ ( ll_dd r ) .
(** **** lBsystem carriers over an object *)
(* End of the file lBsystems_carriers.v *)