-
Notifications
You must be signed in to change notification settings - Fork 69
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Modal logic #1146
base: master
Are you sure you want to change the base?
Modal logic #1146
Conversation
- Add index for variables in formulas - Add soundness for decidable valuation
- Add priorities
- Add me to contributors
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a very nice pull request!
I am very impressed with this pull request. It covers a very substantial amount of modal logic, and many nontrivial theorems. The formalization is well thought-out and most of the coding style is very good. So all in all, this seems to be excellent work!
Since it is a larger pull request, I will review it in parts. I've looked over a couple of files and left a few comments on those. I will continue reviewing it over the coming days.
equiv-empty-is-decidable-prop : | ||
{l : Level} {A : UU l} → is-decidable-prop A → ¬ A → A ≃ empty | ||
equiv-empty-is-decidable-prop {l} {A} (is-p , _) contra = | ||
equiv-iff (A , is-p) empty-Prop contra ex-falso |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This already in the library as equiv-is-empty. Note that any map into the empty type (or indeed into any empty type) is an equivalence.
equiv-unit-is-decidable-prop : | ||
{l : Level} {A : UU l} → is-decidable-prop A → A → A ≃ unit | ||
equiv-unit-is-decidable-prop {l} {A} (is-p , _) a = | ||
equiv-iff (A , is-p) unit-Prop (λ _ → star) (λ _ → a) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few pointers:
- Any proposition equipped with an element is contractible. This is shown here: is-proof-irrelevant-is-prop. The notion of proof irrelevance means
A -> is-contr A
in agda-unimath. - Any contractible type is equivalent to the unit type: equiv-unit-is-contr.
is-small-prop-is-decidable-prop : | ||
{l1 : Level} (l2 : Level) (A : UU l1) → is-decidable-prop A → is-small l2 A | ||
is-small-prop-is-decidable-prop l2 A H | ||
with equiv-empty-or-unit-is-decidable-prop H | ||
... | inl e = is-small-equiv unit e (raise-unit l2 , compute-raise-unit l2) | ||
... | inr e = is-small-equiv empty e (raise-empty l2 , compute-raise-empty l2) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice!
injection-comp : | ||
injection A B → injection B C → injection A C | ||
injection-comp (f , is-inj-f) (g , is-inj-g) = | ||
g ∘ f , is-injective-comp is-inj-f is-inj-g |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would you mind renaming this to comp-injection
? This would fit better with the naming scheme we currently have, which goes comp-pointed-map
, comp-hom-Group
, and so on.
Note that I just found an exception to this naming scheme, which is that we use equiv-comp
. That's probably a mistake on our part, which we missed because we usually use the infix notation for composition of equivalences.
# Transitive Closures | ||
|
||
```agda | ||
module foundation.binary-relations-transitive-closures where |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would you mind renaming this file to transitive-closures-binary-relations
?
We usually name the concept of interest first, and then disambiguate later. For instance, we have several files about the action on identifications files all named action-on-identifications-disambiguation
.
The formula of modal logic is defined inductively as follows: | ||
|
||
- A variable is a formula. | ||
- ⊥ is a formula. | ||
- If `a` and `b` are formulas, then `a → b` is a formula. | ||
- If `a` is a formula, then □`a` is a formula. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The formula of modal logic is defined inductively as follows: | |
- A variable is a formula. | |
- ⊥ is a formula. | |
- If `a` and `b` are formulas, then `a → b` is a formula. | |
- If `a` is a formula, then □`a` is a formula. | |
The type of {{#concept "formulas of modal logic" Agda=modal-formula}} is defined inductively as follows: | |
- A variable is a formula of modal logic. | |
- `⊥` is a formula of modal logic. | |
- If `a` and `b` are formulas of modal logic, then `a → b` is a formula of modal logic. | |
- If `a` is a formula of modal logic, then `□ a` is a formula of modal logic. |
|
||
## Definition | ||
|
||
### Inductive definition of formulas |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
### Inductive definition of formulas | |
### Inductive definition of formulas of modal logic |
@@ -0,0 +1,200 @@ | |||
# Modal logic formulas |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
# Modal logic formulas | |
# Formulas of modal logic |
I would make "Formulas" the first word, so that it doesn't confuse people that something starting with the "M" is listed among the files starting with "F" in an otherwise alphabetically ordered list.
### If formulas are equal, then their subformulas are equal | ||
|
||
```agda | ||
eq-implication-left : {a b c d : modal-formula i} → a →ₘ b = c →ₘ d → a = c | ||
eq-implication-left refl = refl | ||
|
||
eq-implication-right : {a b c d : modal-formula i} → a →ₘ b = c →ₘ d → b = d | ||
eq-implication-right refl = refl | ||
|
||
eq-box : {a b : modal-formula i} → □ₘ a = □ₘ b → a = b | ||
eq-box refl = refl | ||
|
||
eq-diamond : {a b : modal-formula i} → ◇ₘ a = ◇ₘ b → a = b | ||
eq-diamond refl = refl | ||
``` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would place this under ## Properties
is-prop-Eq-modal-formula (□ₘ a) (□ₘ c) = is-prop-Eq-modal-formula a c | ||
``` | ||
|
||
### A formula is a set |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
### A formula is a set | |
### The type of formulas of modal logic is a set |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here is another batch of comments :)
@@ -0,0 +1,338 @@ | |||
# Modal logic deduction |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
# Modal logic deduction | |
# Deductions in modal logic |
I would make the first word of this title "Deductions" so that it starts with the D, because the file titles will be listed by the file names in alphabetic ordering.
### Modal logic predicate | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A sentence explaining this definition informally would be nice. For instance:
### Modal logic predicate | |
### The predicate of being a modal logic | |
A {{#concept "modal logic" Agda=is-modal-logic}} is a theory of modal logic that contains its own deductive closure. |
### Closure of a theory under the deduction system | ||
|
||
```agda | ||
modal-logic-closure : modal-theory l2 i → modal-theory (l1 ⊔ l2) i | ||
modal-logic-closure axioms a = trunc-Prop (axioms ⊢ₘ a) | ||
``` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We try to avoid modules that cross over sections, just because it is harder for the reader to keep track of what is assumed and sections seem a natural breaking point. This approach requires the arguments to be given a few more times, but we find it improves readability.
It also improves maintainability to break modules more often, because it is easier to move code around if it's not in a module that spans a large portion of the file.
### Closure of a theory under the deduction system | |
```agda | |
modal-logic-closure : modal-theory l2 i → modal-theory (l1 ⊔ l2) i | |
modal-logic-closure axioms a = trunc-Prop (axioms ⊢ₘ a) | |
``` | |
### The deductive closure of a theory | |
A modal formula is in the deductive closure of a theory if there [exists](foundation.existence.md) a deduction of the formula from the theory. | |
```agda | |
module _ | |
{l1 l2 : Level} {i : Set l1} | |
where | |
modal-logic-closure : modal-theory l2 i → modal-theory (l1 ⊔ l2) i | |
modal-logic-closure axioms a = trunc-Prop (axioms ⊢ₘ a) | |
``` |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would also suggest:
- Renaming
modal-logic-closure
todeductive-closure-modal-theory
- Adding an entry
is-in-deductive-closure-modal-theory
instead of usingis-in-subtype (modal-logic-closure theory)
later on.
### TODO: Title | ||
|
||
```agda | ||
is-in-modal-logic-closure-deduction : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If my previous renaming suggestions are accepted, then this one could be named is-in-deductive-closure-is-in-modal-theory
.
is-consistent-modal-logic-Prop : modal-theory l2 i → Prop l2 | ||
is-consistent-modal-logic-Prop = neg-Prop ∘ is-contradictory-modal-logic-Prop | ||
|
||
is-consistent-modal-logic : modal-theory l2 i → UU l2 | ||
is-consistent-modal-logic = type-Prop ∘ is-consistent-modal-logic-Prop |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It would make sense if the consistent and inconsistent modal theories each get their own sections ### Inconsistent modal theories
and ### Consistent modal theories
.
is-modal-logic = type-Prop ∘ is-modal-logic-Prop | ||
``` | ||
|
||
### TODO: Title |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
### TODO: Title | |
### Any modal theory is contained in its own deductive closure |
|
||
is-contradictory-modal-logic-Prop : modal-theory l2 i → Prop l2 | ||
is-contradictory-modal-logic-Prop logic = logic ⊥ₘ | ||
|
||
is-contradictory-modal-logic : modal-theory l2 i → UU l2 | ||
is-contradictory-modal-logic = type-Prop ∘ is-contradictory-modal-logic-Prop |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would name this is-inconsistent-modal-theory-Prop
, and the next one is-inconsistent-modal-theory
.
The point is that it is a predicate on modal theories, which isn't currently reflected in the name. I personally find inconsistent
reading a bit better than contradictory
, and it is also more consistent with your use of consistent
of the name for consistent modal theories.
I would also put this in a new section.
One question I have about your definition of contradictory modal logics is that currently it says that a theory is contradictory if it contains falsehood. However, theories are not deductively closed, so wouldn't it be more natural to say that modal theories are inconsistent if their deductive closure contains falsehood?
is-contradictory-modal-logic-Prop : modal-theory l2 i → Prop l2 | |
is-contradictory-modal-logic-Prop logic = logic ⊥ₘ | |
is-contradictory-modal-logic : modal-theory l2 i → UU l2 | |
is-contradictory-modal-logic = type-Prop ∘ is-contradictory-modal-logic-Prop | |
``` | |
### Inconsistent modal theories | |
```agda | |
is-inconsistent-modal-theory-Prop : modal-theory l2 i → Prop l2 | |
is-inconsistent-modal-theory-Prop logic = logic ⊥ₘ | |
is-inconsistent-modal-theory : modal-theory l2 i → UU l2 | |
is-inconsistent-modal-theory = type-Prop ∘ is-contradictory-modal-logic-Prop |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
However, theories are not deductively closed, so wouldn't it be more natural to say that modal theories are inconsistent if their deductive closure contains falsehood?
On the one hand, this would be correct from a definitional point of view. But on the other hand, in proofs this definition is already used in relation to closures, therefore it is convenient to use it in this form. I'll think about how best to determine
Hi Viktor and welcome to agda-unimath! This is very impressive stuff, thanks for the big contribution! |
|
||
```agda | ||
module _ | ||
{l1 l2 : Level} ((Ω , prop-resize) : propositional-resizing l1 l2) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't wish to dogpile on you, but I noticed this one while browsing through the code and thought you might not know about it. Agda implements pattern-matching in module declarations and type declarations via let
-bindings. These don't interact well with Agda's interactive mode, leading to unreadable goal expressions down the line. Therefore we advise against using pattern matching in places such as this one. The principled approach is to define named projection maps for propositional resizing and then use those instead.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, ok, I will fix this. I agree, It's really hard to read in interactive mode
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here is another batch of comments :)
{l1 l2 l3 : Level} {X : UU l1} (P : subtype l2 X) (Q : subtype l3 X) | ||
where | ||
|
||
subtype-intersection-left : P ∩ Q ⊆ P |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A better name for this will be left-inclusion-intersection-subtype
. Note that we build our names exactly the other way around: We first state the name of the operation left-inclusion
and then disambiguate it by intersection-subtype
.
subtype-intersection-left : P ∩ Q ⊆ P | ||
subtype-intersection-left _ = pr1 | ||
|
||
subtype-intersection-right : P ∩ Q ⊆ Q |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A better name for this will be right-inclusion-intersection-subtype
subtype-intersection-right : P ∩ Q ⊆ Q | ||
subtype-intersection-right _ = pr2 | ||
|
||
subtype-both-intersection : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe a better name would be inclusion-intersection-inclusion-subtype
, which would read as the inclusion in the intersection obtained from the inclusion(s) into the subtypes.
Perhaps there are even better suggestions.
{l1 : Level} {X : UU l1} | ||
where | ||
|
||
is-reflexivity-intersection : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This would say that intersection is an idempotent operation, so perhaps is-idempotent-intersection-subtype
would be a more descriptive name.
( refl-leq-subtype P) | ||
( refl-leq-subtype P)) | ||
|
||
is-commutative-subtype-intersection : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would call this inclusion-is-commutative-intersection-subtype
in-concat-left _ l2 (is-in-tail a x l1 in-l1) = | ||
is-in-tail a x (concat-list l1 l2) (in-concat-left l1 l2 in-l1) | ||
|
||
in-concat-right : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would call this in-concat-list-in-right-list
.
in-concat-right (cons x l1) l2 in-l2 = | ||
is-in-tail _ x (concat-list l1 l2) (in-concat-right l1 l2 in-l2) | ||
|
||
in-concat-list : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This one is more tricky to name, but in-concat-list
reads too much like the predicate "to be in a concatenated list". Perhaps we could consider calling it cases-in-concat-list
.
@@ -257,3 +257,27 @@ map-snoc-list : | |||
map-snoc-list f nil a = refl | |||
map-snoc-list f (cons b x) a = ap (cons (f b)) (map-snoc-list f x a) | |||
``` | |||
|
|||
### TODO: maybe another file |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
### TODO: maybe another file | |
### Lists obtained from maps of elements of lists | |
Consider a list `l : list A` of elements of `A`, and consider a function `f : (a : A) → a ∈ l → B`, which assigns to each element of `l` a value in `B`. Then we obtain a list of elements of `B` whose elements are given by `f`. | |
This operation is a generalization of `map-list`, because we only need to assign values in `B` to the elements of the list. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this entry is fine in this file.
### TODO: maybe another file | ||
|
||
```agda | ||
dependent-map-list : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Given what this function does, perhaps map-element-list
is more descriptive. Feel free to disregard this suggestion, if you think dependent-map-list
is better.
|
||
## Idea | ||
|
||
TODO |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Perhaps the "image" of a list would be a good name for this concept. What you describe here is equivalent to the image of the projection map
(Sigma (a : A), a ∈ l) → A
where the first time is the type of all elements of l
. If you agree with this suggestion, we could change the file name to images-lists.lagda.md
and the title to # Images of lists
.
For the ## Idea
section, I have the following suggestion:
TODO | |
For any [list](lists.lists.md) `l : list A` of elements of `A`, the {{#concept "image" Disambiguation="lists"}} of `l` is the least [subtype](foundation.subtypes.md) of `A` that contains all elements of `l`. In other words, it is the subtype of all elements of `A` that are merely elements of `l`, in the sense that the [proposition](foundation-core.propositions.md) | |
```text | |
║a ∈ l║ | |
``` | |
holds, where we applied the [propositional truncation](foundation.propositional-truncations.md) to the elementhood relation of lists. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Changing the concept name to "image of lists" would also trigger some name changes in your entries below. The basic name would be image-list
. Let me know if you want me to go through all of them and make suggestions, or whether you like to come up with names yourself.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here is another couple of comments.
I find myself making suggestions that are dependent on previous suggestions, so perhaps it is best for me to let you work on my current suggestions first, before continuing the review.
Your work is definitely very good, and it would be an amazing addition to the library. The suggestions I made are mostly about what names to choose for certain entries and how to integrate it with the rest of the library better, but the quality of your work is without doubt excellent.
The deduction system of modal logic is defined inductively as follows: | ||
|
||
a ∈ T ------ (AX) T ⊢ a | ||
|
||
T ⊢ a → b T ⊢ a ------------------ (MP) T ⊢ b | ||
|
||
T ⊢ a ------ (NEC) T ⊢ □a | ||
|
||
where `T` is a set of formulas and `a`, `b` are formulas. | ||
|
||
Modal logic generated by a set of axioms is the smallest set of formulas that | ||
contains the axioms and is closed under the deduction system. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The deduction system of modal logic is defined inductively as follows: | |
a ∈ T ------ (AX) T ⊢ a | |
T ⊢ a → b T ⊢ a ------------------ (MP) T ⊢ b | |
T ⊢ a ------ (NEC) T ⊢ □a | |
where `T` is a set of formulas and `a`, `b` are formulas. | |
Modal logic generated by a set of axioms is the smallest set of formulas that | |
contains the axioms and is closed under the deduction system. | |
A {{#concept "theory" Disambiguation="modal logic" Agda=modal-theory}} of modal logic is a [subtype](foundation.subtypes.md) `T : modal-formula i → Prop` of the type of [formulas](modal-logic.formulas.md). | |
Given a theory, a {{#concept "deduction" Disambiguation="modal logic" Agda=_⊢ₘ_}} an element of the type `_⊢ₘ_` inductively generated by: | |
* Axioms: formulas in the theory. | |
* Modus ponens: Given deductions `T ⊢ₘ a →ₘ b` and `T ⊢ₘ a` hold, we obtain a deduction `T ⊢ₘ b`. | |
* Necessity: Given a deduction `T ⊢ₘ a` we obtain a deduction `T ⊢ₘ □a`. | |
In other words, deductions can be formed by combining the following inference rules: | |
```text | |
a ∈ T | |
----------- (AX) | |
T ⊢ a | |
T ⊢ a → b T ⊢ a | |
----------------------- (MP) | |
T ⊢ b | |
T ⊢ a | |
----------- (NEC) | |
T ⊢ □a | |
``` | |
The {{#concept "modal logic"}} generated by a set of axioms is the smallest set of formulas that | |
contains the axioms and is closed under the deduction system, i.e., the modal logic generated by a set of formulas is the deductive closure of that set of formulas. |
Modal logic generated by a set of axioms is the smallest set of formulas that | ||
contains the axioms and is closed under the deduction system. | ||
|
||
## Definition |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
## Definition | |
## Definitions |
|
||
## Definition | ||
|
||
### Theory of modal formulas |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
### Theory of modal formulas | |
### Theories of modal formulas |
modal-theory = subtype l2 (modal-formula i) | ||
``` | ||
|
||
### Deduction system |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
### Deduction system | |
### Deductions of modal logic |
modal-nec : {a : modal-formula i} → axioms ⊢ₘ a → axioms ⊢ₘ □ₘ a | ||
``` | ||
|
||
### Closure of a theory under the deduction system |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
### Closure of a theory under the deduction system | |
### The deductive closure of a theory of modal logic |
ax-1-parameter : | ||
(h : modal-formula i → modal-formula i) → is-injective h → modal-theory l i | ||
pr1 (ax-1-parameter h inj f) = Σ (modal-formula i) (λ a → f = h a) | ||
pr2 (ax-1-parameter h inj f) (a , refl) = | ||
is-prop-is-contr | ||
( is-contr-Σ-is-prop a refl | ||
( λ b → is-set-modal-formula (h a) (h b)) | ||
( λ x → inj)) | ||
( a , refl) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This operation takes an injective map and returns a modal theory. Perhaps an informal sentence explaining this would be helpful. A few things to note: For this construction to work, h
could be any injection X → modal-formula i
where X
is an arbitrary type. This observation leads me to think that a more descriptive name for this construction would be modal-theory-injection-modal-formula
, to say that it is the modal theory obtained from an injection into the type of modal formulas.
One thing to note is that we have a lot more infrastructure for embeddings than for injective maps. A map between sets is injective if and only if it is an embedding, but because the concept of embeddings is better behaved for arbitrary types (types that are not sets), we generally prefer to work with embeddings.
For instance, the fact that any embedding induces a subtype is in the library as fiber-emb-Prop. Admittedly, this name is rather cryptic and could be improved on our part (a better name would be subtype-emb
).
The fact that injective maps between sets are embeddings is is-emb-is-injective, and the fact that injective maps between sets are propositional maps is is-prop-map-is-injective.
Your construction here is essentially combining those constructions without referring to them, so it would be better to use them explicitly.
I wouldn't ask you to change your current approach, which is absolutely fine, but it could be even better if you tried using embeddings more. One benefit of using embeddings is that a potential future generalization to modal theories with an arbitrary type of variables could be easier. We could be less reliant on the fact that modal theories are sets.
One further minor difference between the fibers of an embedding and your type Σ (modal-formula i) (λ a → f = h a)
, is that your type is fiber' h f
, where fiber'
can be found here. In general, it is good to use existing definitions, so that you can also use the existing infrastructure for those definitions. In this case I would also suggest that using fiber
would be better than using fiber'
, because the library has a lot more stuff about the main definition of fibers.
ax-2-parameters : | ||
(h : modal-formula i → modal-formula i → modal-formula i) → | ||
({x x' y y' : modal-formula i} → h x y = h x' y' → x = x') → | ||
({x x' y y' : modal-formula i} → h x y = h x' y' → y = y') → | ||
modal-theory l i | ||
pr1 (ax-2-parameters h inj-1 inj-2 f) = | ||
Σ (modal-formula i) (λ a → Σ (modal-formula i) (λ b → f = h a b)) | ||
pr2 (ax-2-parameters h inj-1 inj-2 f) (a , b , refl) = | ||
is-prop-is-contr | ||
( is-contr-Σ-is-prop a (b , refl) | ||
( λ x → is-prop-type-Prop (ax-1-parameter (h x) inj-2 (h a b))) | ||
( λ x (y , e) → inj-1 e)) | ||
( a , b , refl) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Given the previous discussion, perhaps modal-theory-injection-pair-modal-formula
could be more descriptive? It would describe the modal theory obtained from the injection of pairs of modal formulas.
ax-3-parameters : | ||
(h : | ||
modal-formula i → modal-formula i → modal-formula i → modal-formula i) → | ||
({x x' y y' z z' : modal-formula i} → h x y z = h x' y' z' → x = x') → | ||
({x x' y y' z z' : modal-formula i} → h x y z = h x' y' z' → y = y') → | ||
({x x' y y' z z' : modal-formula i} → h x y z = h x' y' z' → z = z') → | ||
modal-theory l i | ||
pr1 (ax-3-parameters h inj-1 inj-2 inj-3 f) = | ||
Σ ( modal-formula i) | ||
( λ a → | ||
( Σ (modal-formula i) | ||
( λ b → Σ (modal-formula i) ( λ c → f = h a b c)))) | ||
pr2 (ax-3-parameters h inj-1 inj-2 inj-3 f) (a , b , c , refl) = | ||
is-prop-is-contr | ||
( is-contr-Σ-is-prop a (b , c , refl) | ||
( λ x → is-prop-type-Prop (ax-2-parameters (h x) inj-2 inj-3 (h a b c))) | ||
( λ x (y , z , e) → inj-1 e)) | ||
( a , b , c , refl) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Similarly here: perhaps a more descriptive name would be modal-theory-injection-triple-modal-formula
.
Module containing the formalization of normal modal logics. It includes:
The theorems proved are easily generalized to other normal modal logics.
The code is currently being refactored.