Beyond foundation

src/foundation.lagda.md

@@ -10,6 +10,7 @@ open import foundation.0-images-of-maps public
 open import foundation.0-maps public
 open import foundation.1-types public
 open import foundation.2-types public
+open import foundation.action-on-equivalences-type-families public
 open import foundation.action-on-identifications-binary-functions public
 open import foundation.action-on-identifications-dependent-functions public
 open import foundation.action-on-identifications-functions public
@@ -249,6 +250,7 @@ open import foundation.subtype-identity-principle public
 open import foundation.subtypes public
 open import foundation.subuniverses public
 open import foundation.surjective-maps public
+open import foundation.symmetric-binary-relations public
 open import foundation.symmetric-difference public
 open import foundation.symmetric-identity-types public
 open import foundation.symmetric-operations public
@@ -293,6 +295,7 @@ open import foundation.universal-property-coproduct-types public
 open import foundation.universal-property-dependent-pair-types public
 open import foundation.universal-property-empty-type public
 open import foundation.universal-property-fiber-products public
+open import foundation.universal-property-identity-systems public
 open import foundation.universal-property-identity-types public
 open import foundation.universal-property-image public
 open import foundation.universal-property-maybe public

src/foundation/action-on-equivalences-type-families.lagda.md

@@ -0,0 +1,169 @@
+# Action on equivalences of type families
+
+```agda
+module foundation.action-on-equivalences-type-families where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equivalence-induction
+open import foundation.fibers-of-maps
+open import foundation.function-extensionality
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.subuniverses
+open import foundation.transport
+open import foundation.univalence
+open import foundation.universe-levels
+
+open import foundation-core.contractible-types
+open import foundation-core.equality-dependent-pair-types
+open import foundation-core.equivalences
+open import foundation-core.injective-maps
+open import foundation-core.propositions
+open import foundation-core.subtypes
+```
+
+</details>
+
+## Ideas
+
+Given a [subuniverse](foundation.subuniverses.md) `P`, any family of types `B`
+indexed by types of `P` has an **action on equivalences**
+
+```text
+  (A ≃ B) → P A ≃ P B
+```
+
+obtained by [equivalence induction](foundation.equivalence-induction.md). The
+acion on equivalences of a type family `B` on a subuniverse `P` of `𝒰` is such
+that `B id-equiv ＝ id-equiv`, and fits in a
+[commuting square](foundation.commuting-squares-of-maps.md)
+
+```text
+                   ap B
+        (X ＝ Y) --------> (B X ＝ B Y)
+           |                    |
+  equiv-eq |                    | equiv-eq
+           V                    V
+        (X ≃ Y) ---------> (B X ≃ B Y).
+                     B
+```
+
+## Definitions
+
+### The action on equivalences of a family of types over a subuniverse
+
+```agda
+module _
+  { l1 l2 l3 : Level}
+  ( P : subuniverse l1 l2) (B : type-subuniverse P → UU l3)
+  where
+
+  unique-action-on-equivalences-family-of-types-subuniverse :
+    (X : type-subuniverse P) →
+    is-contr (fiber (ev-id-equiv-subuniverse P X {λ Y e → B X ≃ B Y}) id-equiv)
+  unique-action-on-equivalences-family-of-types-subuniverse X =
+    is-contr-map-ev-id-equiv-subuniverse P X (λ Y e → B X ≃ B Y) id-equiv
+
+  action-on-equivalences-family-of-types-subuniverse :
+    (X Y : type-subuniverse P) → pr1 X ≃ pr1 Y → B X ≃ B Y
+  action-on-equivalences-family-of-types-subuniverse X =
+    pr1 (center (unique-action-on-equivalences-family-of-types-subuniverse X))
+
+  compute-id-equiv-action-on-equivalences-family-of-types-subuniverse :
+    (X : type-subuniverse P) →
+    action-on-equivalences-family-of-types-subuniverse X X id-equiv ＝ id-equiv
+  compute-id-equiv-action-on-equivalences-family-of-types-subuniverse X =
+    pr2 (center (unique-action-on-equivalences-family-of-types-subuniverse X))
+```
+
+### The action on equivalences of a family of types over a universe
+
+```agda
+module _
+  {l1 l2 : Level} (B : UU l1 → UU l2)
+  where
+
+  unique-action-on-equivalences-family-of-types-universe :
+    {X : UU l1} →
+    is-contr (fiber (ev-id-equiv (λ Y e → B X ≃ B Y)) id-equiv)
+  unique-action-on-equivalences-family-of-types-universe =
+    is-contr-map-ev-id-equiv (λ Y e → B _ ≃ B Y) id-equiv
+
+  action-on-equivalences-family-of-types-universe :
+    {X Y : UU l1} → (X ≃ Y) → B X ≃ B Y
+  action-on-equivalences-family-of-types-universe {X} {Y} =
+    pr1 (center (unique-action-on-equivalences-family-of-types-universe {X})) Y
+
+  compute-id-equiv-action-on-equivalences-family-of-types-universe :
+    {X : UU l1} →
+    action-on-equivalences-family-of-types-universe {X} {X} id-equiv ＝ id-equiv
+  compute-id-equiv-action-on-equivalences-family-of-types-universe {X} =
+    pr2 (center (unique-action-on-equivalences-family-of-types-universe {X}))
+```
+
+## Properties
+
+### The action on equivalences of a family of types over a subuniverse fits in a commuting square with `equiv-eq`
+
+We claim that the square
+
+```text
+                   ap B
+        (X ＝ Y) --------> (B X ＝ B Y)
+           |                    |
+  equiv-eq |                    | equiv-eq
+           V                    V
+        (X ≃ Y) ---------> (B X ≃ B Y).
+                     B
+```
+
+commutes for any two types `X Y : type-subuniverse P` and any family of types
+`B` over the subuniverse `P`.
+
+```agda
+coherence-square-action-on-equivalences-family-of-types-subuniverse :
+  {l1 l2 l3 : Level} (P : subuniverse l1 l2) (B : type-subuniverse P → UU l3) →
+  (X Y : type-subuniverse P) →
+  coherence-square-maps
+    ( ap B {X} {Y})
+    ( equiv-eq-subuniverse P X Y)
+    ( equiv-eq)
+    ( action-on-equivalences-family-of-types-subuniverse P B X Y)
+coherence-square-action-on-equivalences-family-of-types-subuniverse
+  P B X .X refl =
+  compute-id-equiv-action-on-equivalences-family-of-types-subuniverse P B X
+```
+
+### The action on equivalences of a family of types over a universe fits in a commuting square with `equiv-eq`
+
+We claim that the square
+
+```text
+                   ap B
+        (X ＝ Y) --------> (B X ＝ B Y)
+           |                    |
+  equiv-eq |                    | equiv-eq
+           V                    V
+        (X ≃ Y) ---------> (B X ≃ B Y).
+                     B
+```
+
+commutes for any two types `X Y : 𝒰` and any type family `B` over `𝒰`.
+
+```agda
+coherence-square-action-on-equivalences-family-of-types-universe :
+  {l1 l2 : Level} (B : UU l1 → UU l2) (X Y : UU l1) →
+  coherence-square-maps
+    ( ap B {X} {Y})
+    ( equiv-eq)
+    ( equiv-eq)
+    ( action-on-equivalences-family-of-types-universe B)
+coherence-square-action-on-equivalences-family-of-types-universe B X .X refl =
+  compute-id-equiv-action-on-equivalences-family-of-types-universe B
+```

src/foundation/binary-relations.lagda.md

@@ -124,6 +124,17 @@ module _
   is-antisymmetric-Relation-Prop = is-antisymmetric (type-Relation-Prop R)
 ```
 
+### Morphisms of binary relations
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1}
+  where
+
+  hom-Relation : Relation l2 A → Relation l3 A → UU (l1 ⊔ l2 ⊔ l3)
+  hom-Relation R S = (x y : A) → R x y → S x y
+```
+
 ## Properties
 
 ### Characterization of equality of binary relations

src/foundation/commuting-triangles-of-maps.lagda.md

@@ -11,10 +11,12 @@ open import foundation-core.commuting-triangles-of-maps public
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.functoriality-dependent-function-types
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
+open import foundation-core.function-types
 ```
 
 </details>
@@ -50,13 +52,22 @@ module _
 
   equiv-coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) ≃
-    coherence-triangle-maps' right left (map-inv-equiv e)
+    coherence-triangle-maps right left (map-inv-equiv e)
   equiv-coherence-triangle-maps-inv-top =
-    equiv-Π
+    ( equiv-inv-htpy
+      ( left ∘ (map-inv-equiv e))
+      ( right)) ∘e
+    ( equiv-Π
       ( λ b → left (map-inv-equiv e b) ＝ right b)
       ( e)
       ( λ a →
         equiv-concat
           ( ap left (is-retraction-map-inv-equiv e a))
-          ( right (map-equiv e a)))
+          ( right (map-equiv e a))))
+
+  coherence-triangle-maps-inv-top :
+    coherence-triangle-maps left right (map-equiv e) →
+    coherence-triangle-maps right left (map-inv-equiv e)
+  coherence-triangle-maps-inv-top =
+    map-equiv equiv-coherence-triangle-maps-inv-top
 ```

src/foundation/decidable-propositions.lagda.md

@@ -170,6 +170,10 @@ pr2 (iff-universes-Decidable-Prop l l' P) p =
 is-set-Decidable-Prop : {l : Level} → is-set (Decidable-Prop l)
 is-set-Decidable-Prop {l} =
   is-set-equiv bool equiv-bool-Decidable-Prop is-set-bool
+
+Decidable-Prop-Set : (l : Level) → Set (lsuc l)
+pr1 (Decidable-Prop-Set l) = Decidable-Prop l
+pr2 (Decidable-Prop-Set l) = is-set-Decidable-Prop
 ```
 
 ### Extensionality of decidable propositions
@@ -230,6 +234,13 @@ abstract
     is-decidable (type-Prop P) → is-finite (type-Prop P)
   is-finite-is-decidable-Prop P x =
     is-finite-count (count-is-decidable-Prop P x)
+
+is-finite-type-Decidable-Prop :
+  {l : Level} (P : Decidable-Prop l) → is-finite (type-Decidable-Prop P)
+is-finite-type-Decidable-Prop P =
+  is-finite-is-decidable-Prop
+    ( prop-Decidable-Prop P)
+    ( is-decidable-Decidable-Prop P)
 ```
 
 ### The type of decidable propositions of any universe level is finite

src/foundation/equivalence-extensionality.lagda.md

@@ -10,6 +10,7 @@ module foundation.equivalence-extensionality where
 open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.fundamental-theorem-of-identity-types
+open import foundation.identity-systems
 open import foundation.subtype-identity-principle
 open import foundation.type-theoretic-principle-of-choice
 open import foundation.universe-levels
@@ -24,6 +25,7 @@ open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
 open import foundation-core.propositions
+open import foundation-core.sections
 ```
 
 </details>
@@ -88,3 +90,34 @@ module _
     {e e' : A ≃ B} → (map-equiv e) ＝ (map-equiv e') → htpy-equiv e e'
   htpy-eq-map-equiv = htpy-eq
 ```
+
+### Homotopy induction for homotopies between equivalences
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2}
+  where
+
+  abstract
+    Ind-htpy-equiv :
+      {l3 : Level} (e : A ≃ B)
+      (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) →
+      section
+        ( λ (h : (e' : A ≃ B) (H : htpy-equiv e e') → P e' H) →
+          h e (refl-htpy-equiv e))
+    Ind-htpy-equiv e =
+      is-identity-system-is-torsorial e
+        ( refl-htpy-equiv e)
+        ( is-contr-total-htpy-equiv e)
+
+  ind-htpy-equiv :
+    {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3) →
+    P e (refl-htpy-equiv e) → (e' : A ≃ B) (H : htpy-equiv e e') → P e' H
+  ind-htpy-equiv e P = pr1 (Ind-htpy-equiv e P)
+
+  compute-ind-htpy-equiv :
+    {l3 : Level} (e : A ≃ B) (P : (e' : A ≃ B) (H : htpy-equiv e e') → UU l3)
+    (p : P e (refl-htpy-equiv e)) →
+    ind-htpy-equiv e P p e (refl-htpy-equiv e) ＝ p
+  compute-ind-htpy-equiv e P = pr2 (Ind-htpy-equiv e P)
+```