Modal logic

CONTRIBUTORS.toml

@@ -242,3 +242,8 @@ github = "UlrikBuchholtz"
 displayName = "Garrett Figueroa"
 usernames = [ "Garrett Figueroa", "djspacewhale" ]
 github = "djspacewhale"
+
+[[contributors]]
+displayName = "Viktor Yudov"
+usernames = [ "Viktor Yudov" ]
+github = "spcfox"

src/foundation-core/decidable-propositions.lagda.md

@@ -11,13 +11,16 @@ open import foundation.coproduct-types
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.double-negation
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.logical-equivalences
 open import foundation.negation
 open import foundation.propositional-truncations
+open import foundation.small-types
 open import foundation.unit-type
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
-open import foundation-core.empty-types
 open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.propositions
@@ -189,3 +192,33 @@ is-merely-decidable-is-decidable-trunc-Prop A (inl x) =
 is-merely-decidable-is-decidable-trunc-Prop A (inr f) =
   unit-trunc-Prop (inr (f ∘ unit-trunc-Prop))
 ```
+
+### TODO
+
+```agda
+-- TODO: not only for decidable
+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
+
+-- TODO: not only for decidable
+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)
+
+equiv-empty-or-unit-is-decidable-prop :
+  {l : Level} {A : UU l} → is-decidable-prop A → (A ≃ unit) + (A ≃ empty)
+equiv-empty-or-unit-is-decidable-prop {l} {A} H@(_ , is-d) with is-d
+... | inl contra = inl (equiv-unit-is-decidable-prop H contra)
+... | inr a = inr (equiv-empty-is-decidable-prop H a)
+
+-- TODO: move to foundation
+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)
+```

src/foundation-core/injective-maps.lagda.md

@@ -90,6 +90,11 @@ module _
     is-injective h → is-injective g → is-injective (g ∘ h)
   is-injective-comp is-inj-h is-inj-g = is-inj-h ∘ is-inj-g
 
+  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
+
   is-injective-left-map-triangle :
     (f : A → C) (g : B → C) (h : A → B) → f ~ (g ∘ h) →
     is-injective h → is-injective g → is-injective f

src/foundation.lagda.md

@@ -38,6 +38,7 @@ open import foundation.binary-homotopies public
 open import foundation.binary-operations-unordered-pairs-of-types public
 open import foundation.binary-reflecting-maps-equivalence-relations public
 open import foundation.binary-relations public
+open import foundation.binary-relations-transitive-closures public
 open import foundation.binary-relations-with-extensions public
 open import foundation.binary-relations-with-lifts public
 open import foundation.binary-transport public

src/foundation/binary-relations-transitive-closures.lagda.md

@@ -0,0 +1,120 @@
+# Transitive Closures
+
+```agda
+module foundation.binary-relations-transitive-closures where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.binary-relations
+open import foundation.propositional-truncations
+open import foundation.universe-levels
+
+open import foundation-core.function-types
+open import foundation-core.propositions
+```
+
+</details>
+
+## Idea
+
+TODO
+
+## Definition
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1}
+  where
+
+  data transitive-closure (R : Relation l2 A) : Relation (l1 ⊔ l2) A
+    where
+    transitive-closure-base : {x y : A} → R x y → transitive-closure R x y
+    transitive-closure-step :
+      {x y z : A} → R x y → transitive-closure R y z → transitive-closure R x z
+
+  is-transitive-transitive-closure :
+    (R : Relation l2 A) → is-transitive (transitive-closure R)
+  is-transitive-transitive-closure
+    R x y z c-yz (transitive-closure-base r-xy) =
+      transitive-closure-step r-xy c-yz
+  is-transitive-transitive-closure
+    R x y z c-yz (transitive-closure-step {y = u} r-xu c-uy) =
+      transitive-closure-step r-xu
+        ( is-transitive-transitive-closure R u y z c-yz c-uy)
+
+  transitive-closure-preserves-reflexivity :
+    (R : Relation l2 A) →
+    is-reflexive R →
+    is-reflexive (transitive-closure R)
+  transitive-closure-preserves-reflexivity R is-refl x =
+    transitive-closure-base (is-refl x)
+
+  transitive-closure-preserves-symmetry :
+    (R : Relation l2 A) →
+    is-symmetric R →
+    is-symmetric (transitive-closure R)
+  transitive-closure-preserves-symmetry R is-sym x y
+    (transitive-closure-base r) =
+      transitive-closure-base (is-sym x y r)
+  transitive-closure-preserves-symmetry
+    R is-sym x y (transitive-closure-step {y = u} r-xu c-uy) =
+      is-transitive-transitive-closure R y u x
+        ( transitive-closure-base (is-sym x u r-xu))
+        ( transitive-closure-preserves-symmetry R is-sym u y c-uy)
+```
+
+### Transitive closure of a relation valued in propositions
+
+```agda
+  transitive-closure-Prop :
+    (R : Relation-Prop l2 A) → Relation-Prop (l1 ⊔ l2) A
+  transitive-closure-Prop R x y =
+    trunc-Prop (transitive-closure (type-Relation-Prop R) x y)
+
+  is-transitive-transitive-closure-Prop :
+    (R : Relation-Prop l2 A) →
+    is-transitive-Relation-Prop (transitive-closure-Prop R)
+  is-transitive-transitive-closure-Prop R x y z c-yz c-xy =
+    apply-twice-universal-property-trunc-Prop
+      ( c-yz)
+      ( c-xy)
+      ( transitive-closure-Prop R x z)
+      ( λ r-yz r-xy →
+        unit-trunc-Prop
+          ( is-transitive-transitive-closure
+            ( type-Relation-Prop R)
+            ( x)
+            ( y)
+            ( z)
+            ( r-yz)
+            ( r-xy)))
+
+  transitive-closure-Prop-preserves-reflexivity :
+    (R : Relation-Prop l2 A) →
+    is-reflexive-Relation-Prop R →
+    is-reflexive-Relation-Prop (transitive-closure-Prop R)
+  transitive-closure-Prop-preserves-reflexivity R is-refl x =
+    unit-trunc-Prop
+      ( transitive-closure-preserves-reflexivity
+        ( type-Relation-Prop R)
+        ( is-refl)
+        ( x))
+
+  transitive-closure-Prop-preserves-symmetry :
+    (R : Relation-Prop l2 A) →
+    is-symmetric-Relation-Prop R →
+    is-symmetric-Relation-Prop (transitive-closure-Prop R)
+  transitive-closure-Prop-preserves-symmetry R is-sym x y =
+    map-universal-property-trunc-Prop
+      ( transitive-closure-Prop R y x)
+      ( λ r-xy →
+        unit-trunc-Prop
+          ( transitive-closure-preserves-symmetry
+            ( type-Relation-Prop R)
+            ( is-sym)
+            ( x)
+            ( y)
+            ( r-xy)))
+```

src/foundation/decidable-types.lagda.md

@@ -270,3 +270,15 @@ module _
   is-decidable-raise (inl p) = inl (map-raise p)
   is-decidable-raise (inr np) = inr (λ p' → np (map-inv-raise p'))
 ```
+
+### For decidable type `Q` `¬ Q → ¬ P` implies `P → Q`
+
+```agda
+contraposition-is-decidable :
+  {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
+  is-decidable Q →
+  (¬ Q → ¬ P) →
+  P → Q
+contraposition-is-decidable {Q = Q} (inl q) f p = q
+contraposition-is-decidable {Q = Q} (inr nq) f p = ex-falso (f nq p)
+```