Cleanup of @spcfox's modal logic pull request

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,12 @@ 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))
 ```
+
+### Any decidable proposition is small with respect to any universe level
+
+```agda
+is-small-is-decidable-prop :
+ {l1 : Level} (l2 : Level) (A : UU l1) → is-decidable-prop A → is-small l2 A
+is-small-is-decidable-prop l2 A (H , inl a) = is-small-is-contr l2 (is-proof-irrelevant-is-prop H a)
+is-small-is-decidable-prop l2 A (H , inr f) = is-small-is-empty l2 f
+```

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

@@ -42,6 +42,16 @@ is-injective {l1} {l2} {A} {B} f = {x y : A} → f x ＝ f y → x ＝ y
 
 injection : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
 injection A B = Σ (A → B) is-injective
+
+module _
+ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : injection A B)
+ where
+
+ map-injection : A → B
+ map-injection = pr1 f
+
+ is-injective-injection : is-injective map-injection
+ is-injective-injection = pr2 f
 ```
 
 ## Examples
@@ -90,6 +100,12 @@ 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 B C → injection A B → injection A C
+ pr1 (injection-comp g f) = map-injection g ∘ map-injection f
+ pr2 (injection-comp g f) =
+ is-injective-comp (is-injective-injection f) (is-injective-injection 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-core/small-types.lagda.md

@@ -24,6 +24,8 @@ open import foundation.universe-levels
 open import foundation-core.cartesian-product-types
 open import foundation-core.contractible-types
 open import foundation-core.coproduct-types
+open import foundation.empty-types
+open import foundation.function-types
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.identity-types
 open import foundation-core.propositions
@@ -202,6 +204,23 @@ is-small-unit : {l : Level} → is-small l unit
 is-small-unit = is-small-is-contr _ is-contr-unit
 ```
 
+### Any empty type is small with respect to any universe
+
+```agda
+is-small-is-empty :
+ (l : Level) {l1 : Level} {A : UU l1} → is-empty A → is-small l A
+pr1 (is-small-is-empty l H) = raise-empty l
+pr2 (is-small-is-empty l H) = equiv-is-empty H is-empty-raise-empty
+```
+
+### The empty type is small with respect to any universe
+
+```agda
+is-small-empty :
+ (l : Level) → is-small l empty
+is-small-empty l = is-small-is-empty l id
+```
+
 ### Small types are closed under dependent pair types
 
 ```agda

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.transitive-closures-binary-relations 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/decidable-types.lagda.md

@@ -270,3 +270,13 @@ module _
  is-decidable-raise (inl p) = inl (map-raise p)
  is-decidable-raise (inr np) = inr (λ p' → np (map-inv-raise p'))
 ```
+
+### If `Q` is a decidable type, then any implication `P → Q` can be proven by contraposition
+
+```agda
+contraposition-is-decidable :
+ {l1 l2 : Level} {P : UU l1} {Q : UU l2} →
+ is-decidable Q → (¬ Q → ¬ P) → P → Q
+contraposition-is-decidable (inl q) f p = q
+contraposition-is-decidable (inr nq) f p = ex-falso (f nq p)
+```

src/foundation/dependent-reflecting-maps-equivalence-relations.lagda.md

@@ -0,0 +1,229 @@
+# Dependent reflecting maps for equivalence relations
+
+```agda
+module foundation.dependent-reflecting-maps-equivalence-relations where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-pair-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopy-induction
+open import foundation.reflecting-maps-equivalence-relations
+open import foundation.subtype-identity-principle
+open import foundation.type-arithmetic-dependent-pair-types
+open import foundation.type-theoretic-principle-of-choice
+open import foundation.universe-levels
+
+open import foundation-core.dependent-identifications
+open import foundation-core.equivalence-relations
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.propositions
+open import foundation-core.sets
+open import foundation-core.torsorial-type-families
+```
+
+</details>
+
+## Idea
+
+Consider a type `A` equipped with an [equivalence relation](foundation.equivalence-relations.md) `R`, and consider a [reflecting map](foundation.reflecting-maps-equivalence-relations.md) `f : A → B` with
+
+```text
+ ρ : {x y : A} → R x y → f x ＝ f y.
+```
+
+Furthermore, consider a type family `C` over `B`. A dependent function `g : (x : A) → C (f x)` is said to be a {{#concept "dependent reflecting map" Disambiguation="equivalence relations" Agda=reflecting-map-equivalence-relation}} if we there is a [dependent identification](foundation-core.dependent-identifications.md) `dependent-identification C (ρ r) (g x) (g y)` for every `r : R x y` and every `x y : A`.
+
+## Definitions
+
+### The predicate of being a dependent reflecting map
+
+```agda
+module _
+ {l1 l2 l3 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+ {B : UU l3} (f : reflecting-map-equivalence-relation R B)
+ where
+
+ is-dependent-reflecting-map-equivalence-relation :
+ {l4 : Level} (C : B → UU l4) →
+ ((x : A) → C (map-reflecting-map-equivalence-relation R f x)) →
+ UU (l1 ⊔ l2 ⊔ l4)
+ is-dependent-reflecting-map-equivalence-relation C g =
+ {x y : A} (r : sim-equivalence-relation R x y) →
+ dependent-identification C
+ ( reflects-map-reflecting-map-equivalence-relation R f r)
+ ( g x)
+ ( g y)
+```
+
+### Dependent reflecting maps
+
+```agda
+module _
+ {l1 l2 l3 l4 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+ {B : UU l3} (f : reflecting-map-equivalence-relation R B)
+ (C : B → UU l4)
+ where
+
+ dependent-reflecting-map-equivalence-relation : UU (l1 ⊔ l2 ⊔ l4)
+ dependent-reflecting-map-equivalence-relation =
+ Σ ( (x : A) → C (map-reflecting-map-equivalence-relation R f x))
+ ( is-dependent-reflecting-map-equivalence-relation R f C)
+
+ map-dependent-reflecting-map-equivalence-relation :
+ dependent-reflecting-map-equivalence-relation →
+ (x : A) → C (map-reflecting-map-equivalence-relation R f x)
+ map-dependent-reflecting-map-equivalence-relation = pr1
+
+ reflects-map-dependent-reflecting-map-equivalence-relation :
+ (g : dependent-reflecting-map-equivalence-relation) →
+ is-dependent-reflecting-map-equivalence-relation R f C
+ ( map-dependent-reflecting-map-equivalence-relation g)
+ reflects-map-dependent-reflecting-map-equivalence-relation = pr2
+```
+
+## Properties
+
+### Being a dependent reflecting map into a family of sets is a proposition
+
+```agda
+module _
+ {l1 l2 l3 l4 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+ {B : UU l3} (f : reflecting-map-equivalence-relation R B)
+ (C : B → Set l4)
+ (g : (x : A) → type-Set (C (map-reflecting-map-equivalence-relation R f x)))
+ where
+
+ is-prop-is-dependent-reflecting-map-equivalence-relation :
+ is-prop
+ ( is-dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C) g)
+ is-prop-is-dependent-reflecting-map-equivalence-relation =
+ is-prop-implicit-Π
+ ( λ x →
+ is-prop-implicit-Π
+ ( λ y → is-prop-Π (λ r → is-set-type-Set (C _) _ _)))
+
+ is-dependent-reflecting-map-prop-equivalence-relation :
+ Prop (l1 ⊔ l2 ⊔ l4)
+ pr1 is-dependent-reflecting-map-prop-equivalence-relation =
+ is-dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C) g
+ pr2 is-dependent-reflecting-map-prop-equivalence-relation =
+ is-prop-is-dependent-reflecting-map-equivalence-relation 
+```
+
+### Characterizing the identity type of dependent reflecting maps into families of sets
+
+```agda
+module _
+ {l1 l2 l3 l4 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+ {B : UU l3} (f : reflecting-map-equivalence-relation R B)
+ (C : B → Set l4)
+ (g : dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C))
+ where
+
+ htpy-dependent-reflecting-map-equivalence-relation :
+ (h : dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C)) →
+ UU (l1 ⊔ l4)
+ htpy-dependent-reflecting-map-equivalence-relation h =
+ map-dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C) g ~
+ map-dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C) h
+
+ refl-htpy-dependent-reflecting-map-equivalence-relation :
+ htpy-dependent-reflecting-map-equivalence-relation g
+ refl-htpy-dependent-reflecting-map-equivalence-relation = refl-htpy
+
+ htpy-eq-dependent-reflecting-map-equivalence-relation :
+ (h : dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C)) →
+ g ＝ h → htpy-dependent-reflecting-map-equivalence-relation h
+ htpy-eq-dependent-reflecting-map-equivalence-relation h refl =
+ refl-htpy-dependent-reflecting-map-equivalence-relation
+
+ is-torsorial-htpy-dependent-reflecting-map-equivalence-relation :
+ is-torsorial htpy-dependent-reflecting-map-equivalence-relation
+ is-torsorial-htpy-dependent-reflecting-map-equivalence-relation =
+ is-torsorial-Eq-subtype
+ ( is-torsorial-htpy
+ ( map-dependent-reflecting-map-equivalence-relation R f
+ ( type-Set ∘ C)
+ ( g)))
+ ( is-prop-is-dependent-reflecting-map-equivalence-relation R f C)
+ ( map-dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C) g)
+ ( refl-htpy)
+ ( reflects-map-dependent-reflecting-map-equivalence-relation R f
+ ( type-Set ∘ C)
+ ( g))
+
+ is-equiv-htpy-eq-dependent-reflecting-map-equivalence-relation :
+ (h : dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C)) →
+ is-equiv (htpy-eq-dependent-reflecting-map-equivalence-relation h)
+ is-equiv-htpy-eq-dependent-reflecting-map-equivalence-relation =
+ fundamental-theorem-id
+ is-torsorial-htpy-dependent-reflecting-map-equivalence-relation
+ htpy-eq-dependent-reflecting-map-equivalence-relation
+
+ extensionality-dependent-reflecting-map-equivalence-relation :
+ (h : dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C)) →
+ (g ＝ h) ≃ htpy-dependent-reflecting-map-equivalence-relation h
+ pr1 (extensionality-dependent-reflecting-map-equivalence-relation h) =
+ htpy-eq-dependent-reflecting-map-equivalence-relation h
+ pr2 (extensionality-dependent-reflecting-map-equivalence-relation h) =
+ is-equiv-htpy-eq-dependent-reflecting-map-equivalence-relation h
+
+ eq-htpy-dependent-reflecting-map-equivalence-relation :
+ (h : dependent-reflecting-map-equivalence-relation R f (type-Set ∘ C)) →
+ htpy-dependent-reflecting-map-equivalence-relation h → g ＝ h
+ eq-htpy-dependent-reflecting-map-equivalence-relation h =
+ map-inv-is-equiv
+ ( is-equiv-htpy-eq-dependent-reflecting-map-equivalence-relation h)
+```
+
+### The type of dependent reflecting maps into a family `C` is equivalent to the type of reflecting maps into `Σ B C` that give `f` after composing with the first projection
+
+```agda
+module _
+ {l1 l2 l3 l4 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+ {B : UU l3} (f : reflecting-map-equivalence-relation R B)
+ {C : B → UU l4}
+ where
+
+ map-compute-dependent-reflecting-map-equivalence-relation :
+ dependent-reflecting-map-equivalence-relation R f C →
+ Σ ( reflecting-map-equivalence-relation R (Σ B C))
+ ( λ g →
+ pr1 ∘ map-reflecting-map-equivalence-relation R g ~
+ map-reflecting-map-equivalence-relation R f)
+ pr1 (pr1 (map-compute-dependent-reflecting-map-equivalence-relation g)) x =
+ ( map-reflecting-map-equivalence-relation R f x ,
+ map-dependent-reflecting-map-equivalence-relation R f C g x)
+ pr2 (pr1 (map-compute-dependent-reflecting-map-equivalence-relation g)) r =
+ eq-pair-Σ
+ ( reflects-map-reflecting-map-equivalence-relation R f r)
+ ( reflects-map-dependent-reflecting-map-equivalence-relation R f C g r)
+ pr2 (map-compute-dependent-reflecting-map-equivalence-relation g) =
+ refl-htpy
+
+ compute-dependent-reflecting-map-equivalence-relation :
+ Σ ( reflecting-map-equivalence-relation R (Σ B C))
+ ( λ g →
+ pr1 ∘ map-reflecting-map-equivalence-relation R g ~
+ map-reflecting-map-equivalence-relation R f) ≃
+ dependent-reflecting-map-equivalence-relation R f C
+ compute-dependent-reflecting-map-equivalence-relation =
+ {!!} ∘e
+ ( equiv-Σ _
+ ( inv-distributive-Π-Σ)
+ ( λ t → {!equiv-implicit-Π!})) ∘e
+ ( equiv-right-swap-Σ)
+```
+
+## See also
+
+- [Reflecting maps](foundation.reflecting-maps-equivalence-relations.md)