You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: UALib/Relations/Continuous.lagda
+38-19
Original file line number
Diff line number
Diff line change
@@ -32,26 +32,31 @@ We refer to such relations as *dependent continuous relations* (or *dependent re
32
32
33
33
34
34
35
+
#### <a id="continuous-and-dependent-relations">Continuous and dependent relations</a>
35
36
37
+
We now define the type `ContRel` which represents predicates of arbitrary arity over a single type `A`. We call this the type of *continuous relations*.<sup>[1](Relations.Continuous.html#fn1)</sup>)
We now define the type `ContRel` which represents predicates of arbitrary arity over a single type `A`. We call this the type of *continuous relations*.<sup>[1](Relations.Continuous.html#fn1)</sup>)
46
+
We now exploit the full power of dependent types to define a completely general relation type. Specifically, we let the tuples inhabit a dependent function type `𝒜 : I → 𝓤 ̇`, where the codomain may depend upon the input coordinate `i : I` of the domain. Heuristically, think of the inhabitants of the following type as relations from `𝒜 i` to `𝒜 j` to `𝒜 k` to …. (This is only an heuristic since \ab I can represent an uncountable collection.\cref{uncountable}.<sup>[2](Relations.Continuous.html#fn2)</sup>)
We call `DepRel` the type of *dependent relations*.
51
56
52
57
53
58
54
-
#### <a id="compatibility-with-continuous-relations">Compatibility with continuous relations</a>
59
+
#### <a id="compatibility-with-general-relations">Compatibility with general relations</a>
55
60
56
61
We now define some functions that make it easy to assert that a given operation is compatible with a given relation. The first is an *evaluation* function which "lifts" an `I`-ary relation to an `(I → J)`-ary relation. The lifted relation will relate an `I`-tuple of `J`-tuples when the "`I`-slices" (or "rows") of the `J`-tuples belong to the original relation.
57
62
@@ -80,19 +85,6 @@ To readers who find the syntax of the last two definitions nauseating, we recomm
80
85
Now `eval-cont-rel R 𝒶` is defined by `∀ j → R (λ i → 𝒶 i j)` which represents the assertion that each row of the `I` columns shown above belongs to the original relation `R`. Finally, `cont-compatible-op` takes a `J`-ary operation `𝑓 : Op J A` and an `I`-tuple `𝒶 : I → J → A` of `J`-tuples, and determines whether the `I`-tuple `λ i → 𝑓 (𝑎 i)` belongs to `R`.
In this section we exploit the power of dependent types to define a completely general relation type. Specifically, we let the tuples inhabit a dependent function type `𝒜 : I → 𝓤 ̇`, where the codomain may depend upon the input coordinate `i : I` of the domain. Heuristically, think of the inhabitants of the following type as relations from `𝒜 i` to `𝒜 j` to `𝒜 k` to …. (This is only an heuristic since \ab I can represent an uncountable collection.\cref{uncountable}.<sup>[2](Relations.Continuous.html#fn2)</sup>)
We call `DepRel` the type of *dependent relations*.
95
-
96
88
Above we saw lifts of continuous relations and what it means for such relations to be compatible with operations. We conclude this module by defining the (only slightly more complicated) lift of dependent relations, and the type that represents compatibility of a dependent relation with an operation.
97
89
98
90
\begin{code}
@@ -129,3 +121,30 @@ module _ {I J : 𝓥 ̇} {𝒜 : I → 𝓤 ̇} where
The principle of *proposition extensionality* asserts that logically equivalent propositions are equivalent. That is, if `P` and `Q` are propositions and if `P ⊆ Q` and `Q ⊆ P`, then `P ≡ Q`. For our purposes, it will suffice to formalize this notion for general predicates, rather than for propositions (i.e., truncated predicates). As such, we call the next type `pred-ext` (instead of, say, `prop-ext`).
25
23
26
24
\begin{code}
27
25
28
26
pred-ext : (𝓤 𝓦 : Universe) → (𝓤 ⊔ 𝓦) ⁺ ̇
29
27
pred-ext 𝓤 𝓦 = ∀ {A : 𝓤 ̇}{P Q : Pred A 𝓦 } → P ⊆ Q → Q ⊆ P → P ≡ Q
28
+
29
+
\end{code}
30
+
31
+
We also define *relation extensionality* principles which generalize the predicate extensionality princple just defined (though these are not yet needed in other modules of the [UALib][]).
dep-rel-ext 𝓤 𝓥 𝓦 = ∀ {I : 𝓥 ̇}{𝒜 : I → 𝓤 ̇}{P Q : DepRel I 𝒜 𝓦 } → P ⊆ Q → Q ⊆ P → P ≡ Q
40
+
30
41
\end{code}
31
42
43
+
Note that each of the types above merely define an extensionality principle. They do not postulate that the principle holds. If we wish to postulate, say, `pred-ext`, then we do so by assuming that type is inhabited (see, for example, the definition of `block-ext` below).
Recall, we defined a type called `ContRel` in the [Relations.Continuous][] module to represent relations of arbitrary arity. Naturally, we define the corresponding truncated types, the inhabitants of which we will call *continuous propositions*.
83
-
84
-
\begin{code}
85
-
86
-
module general-propositions {𝓤 : Universe}{I : 𝓥 ̇} where
87
-
88
-
open import Relations.Continuous using (ContRel; DepRel)
89
-
90
-
IsContProp : {A : 𝓤 ̇}{𝓦 : Universe} → ContRel I A 𝓦 → 𝓥 ⊔ 𝓤 ⊔ 𝓦 ̇
91
-
IsContProp {A = A} P = Π 𝑎 ꞉ (I → A) , is-subsingleton (P 𝑎)
92
-
93
-
ContProp : 𝓤 ̇ → (𝓦 : Universe) → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺ ̇
94
-
ContProp A 𝓦 = Σ P ꞉ (ContRel I A 𝓦) , IsContProp P
cont-prop-ext A 𝓦 = {P Q : ContProp A 𝓦 } → ∣ P ∣ ⊆ ∣ Q ∣ → ∣ Q ∣ ⊆ ∣ P ∣ → P ≡ Q
98
-
99
-
\end{code}
100
-
101
-
102
-
While we're at it, we might as well take the abstraction one step further and define the type of *truncated dependent relations*, which we call *dependent propositions*.
dep-prop-ext 𝒜 𝓦 = {P Q : DepProp 𝒜 𝓦} → ∣ P ∣ ⊆ ∣ Q ∣ → ∣ Q ∣ ⊆ ∣ P ∣ → P ≡ Q
85
+
block-ext|uip pe buip Req Ruv = to-subtype|uip buip (block-ext pe Req Ruv)
114
86
115
87
\end{code}
116
88
117
89
118
-
-----------------------------------
119
-
120
-
<sup>*</sup><span class="footnote" id="fn0"> Sections marked with an asterisk include new types that are more abstract and general than some of the types defined in other sections. As yet these general types are not used elsewhere in the [UALib][], so sections marked * may be safely skimmed or skipped.</span>
This section defines more general truncated predicates which we call *continuous propositions* and *dependent propositions*. Recall, above (in the [Relations.Continuous][] module) we defined types called `ContRel` and `DepRel` to represent relations of arbitrary arity over arbitrary collections of sorts.
116
+
117
+
Naturally, we define the corresponding *truncated continuous relation type* and *truncated dependent relation type*, the inhabitants of which we will call *continuous propositions* and *dependent propositions*, respectively.
118
+
119
+
\begin{code}
120
+
121
+
module _ {𝓤 : Universe}{I : 𝓥 ̇} where
122
+
123
+
open import Relations.Continuous using (ContRel; DepRel)
124
+
125
+
IsContProp : {A : 𝓤 ̇}{𝓦 : Universe} → ContRel I A 𝓦 → 𝓥 ⊔ 𝓤 ⊔ 𝓦 ̇
126
+
IsContProp {A = A} P = Π 𝑎 ꞉ (I → A) , is-subsingleton (P 𝑎)
127
+
128
+
ContProp : 𝓤 ̇ → (𝓦 : Universe) → 𝓤 ⊔ 𝓥 ⊔ 𝓦 ⁺ ̇
129
+
ContProp A 𝓦 = Σ P ꞉ (ContRel I A 𝓦) , IsContProp P
dep-prop-ext 𝒜 𝓦 = {P Q : DepProp 𝒜 𝓦} → ∣ P ∣ ⊆ ∣ Q ∣ → ∣ Q ∣ ⊆ ∣ P ∣ → P ≡ Q
142
+
143
+
\end{code}
111
144
112
145
113
146
-----------------------------------
114
147
148
+
<sup>*</sup><span class="footnote" id="fn0"> Sections marked with an asterisk include new types that are more abstract and general than some of the types defined in other sections. As yet these general types are not used elsewhere in the [UALib][], so sections marked * may be safely skimmed or skipped.</span>
149
+
150
+
115
151
<sup>1</sup><span class="footnote" id="fn1"> As [Escardó][] explains, "at this point, with the definition of these notions, we are entering the realm of univalent mathematics, but not yet needing the univalence axiom."</span>
116
152
117
153
<sup>2</sup><span class="footnote" id="fn2"> See [https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html\#sigmaequality](www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html\#sigmaequality).</span>
0 commit comments