Beyond foundation (#751)

In this PR I pulled changes I made in the `foundation` and
`foundation-core` folders in the Beyond finite sets PR #623. The goal is
to create something mergeable without having to wait for the other
unfinished changes in #623. Let's see what monstrosity I created.

src/finite-group-theory/cartier-delooping-sign-homomorphism.lagda.md

@@ -17,7 +17,7 @@ open import finite-group-theory.finite-type-groups
 open import finite-group-theory.sign-homomorphism
 open import finite-group-theory.transpositions
 
-open import foundation.action-on-equivalences-families-over-subuniverses
+open import foundation.action-on-equivalences-type-families-over-subuniverses
 open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
@@ -29,6 +29,7 @@ open import foundation.negation
 open import foundation.propositional-truncations
 open import foundation.raising-universe-levels
 open import foundation.transport-along-identifications
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -69,7 +70,7 @@ module _
         ( star)
         ( transposition Y))
       ( map-equiv
-        ( action-equiv-family-on-subuniverse
+        ( action-equiv-family-over-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( orientation-Complete-Undirected-Graph (n +ℕ 2))
           ( raise l (Fin (n +ℕ 2)) ,
@@ -110,17 +111,19 @@ module _
           preserves-id-equiv-orientation-complete-undirected-graph-equiv
             ( n +ℕ 2)}
         { y =
-          ( action-equiv-family-on-subuniverse
+          ( action-equiv-family-over-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( orientation-Complete-Undirected-Graph (n +ℕ 2))) ,
-          ( preserves-id-equiv-action-equiv-family-on-subuniverse
+          ( compute-id-equiv-action-equiv-family-over-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( orientation-Complete-Undirected-Graph (n +ℕ 2)))}
         ( eq-is-contr
-          ( is-contr-preserves-id-action-equiv-family-on-subuniverse
-            ( mere-equiv-Prop (Fin (n +ℕ 2)))
-            ( orientation-Complete-Undirected-Graph (n +ℕ 2))
-            ( is-set-orientation-Complete-Undirected-Graph (n +ℕ 2)))))
+          ( is-contr-equiv' _
+            ( distributive-Π-Σ)
+            ( is-contr-Π
+              ( unique-action-equiv-family-over-subuniverse
+                ( mere-equiv-Prop (Fin (n +ℕ 2)))
+                ( orientation-Complete-Undirected-Graph (n +ℕ 2)))))))
       ( not-even-difference-orientation-aut-transposition-count
         (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star))
 

src/finite-group-theory/delooping-sign-homomorphism.lagda.md

@@ -18,8 +18,9 @@ open import finite-group-theory.permutations
 open import finite-group-theory.sign-homomorphism
 open import finite-group-theory.transpositions
 
-open import foundation.action-on-equivalences-families-over-subuniverses
+open import foundation.action-on-equivalences-type-families-over-subuniverses
 open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
 open import foundation.commuting-squares-of-maps
 open import foundation.contractible-types
 open import foundation.coproduct-types
@@ -31,6 +32,7 @@ open import foundation.empty-types
 open import foundation.equality-dependent-pair-types
 open import foundation.equivalence-classes
 open import foundation.equivalence-extensionality
+open import foundation.equivalence-induction
 open import foundation.equivalence-relations
 open import foundation.equivalences
 open import foundation.function-extensionality
@@ -129,7 +131,7 @@ module _
           unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))
       ( quotient-aut-succ-succ-Fin n (transposition Y))
       ( map-equiv
-        ( action-equiv-family-on-subuniverse
+        ( action-equiv-family-over-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( D (n +ℕ 2))
           ( raise l1 (Fin (n +ℕ 2)) ,
@@ -146,9 +148,8 @@ module _
 
     eq-counting-equivalence-class-R :
       (n : ℕ) →
-      Id
-        ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2))))
-        ( raise (l2 ⊔ lsuc l3) (Fin 2))
+      equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2))) ＝
+      raise (l2 ⊔ lsuc l3) (Fin 2)
     eq-counting-equivalence-class-R n =
       eq-equiv
         ( equivalence-class (R (n +ℕ 2) (Fin-UU-Fin l1 (n +ℕ 2))))
@@ -165,34 +166,57 @@ module _
       (n : ℕ) (X X' : UU-Fin l1 n) →
       type-UU-Fin n X ≃ type-UU-Fin n X' → D n X ≃ D n X'
     invertible-action-D-equiv n =
-      action-equiv-family-on-subuniverse (mere-equiv-Prop (Fin n)) (D n)
+      action-equiv-family-over-subuniverse (mere-equiv-Prop (Fin n)) (D n)
 
     preserves-id-equiv-invertible-action-D-equiv :
       (n : ℕ) (X : UU-Fin l1 n) →
       Id (invertible-action-D-equiv n X X id-equiv) id-equiv
     preserves-id-equiv-invertible-action-D-equiv n =
-      preserves-id-equiv-action-equiv-family-on-subuniverse
+      compute-id-equiv-action-equiv-family-over-subuniverse
         ( mere-equiv-Prop (Fin n))
         ( D n)
 
-    preserves-R-invertible-action-D-equiv :
-      ( n : ℕ) →
-      ( X X' : UU-Fin l1 n)
-      ( e : type-UU-Fin n X ≃ type-UU-Fin n X') →
-      ( a a' : D n X) →
-      ( sim-Equivalence-Relation (R n X) a a' ↔
-        sim-Equivalence-Relation
-          ( R n X')
-          ( map-equiv (invertible-action-D-equiv n X X' e) a)
-          ( map-equiv (invertible-action-D-equiv n X X' e) a'))
-    preserves-R-invertible-action-D-equiv n X X' =
-      Ind-action-equiv-family-on-subuniverse (mere-equiv-Prop (Fin n)) (D n) X
-        ( λ Y f →
-          ( a a' : D n X) →
-          ( sim-Equivalence-Relation (R n X) a a' ↔
-            sim-Equivalence-Relation (R n Y) (map-equiv f a) (map-equiv f a')))
-        ( λ a a' → id , id)
-        ( X')
+    abstract
+      preserves-R-invertible-action-D-equiv :
+        ( n : ℕ) →
+        ( X X' : UU-Fin l1 n)
+        ( e : type-UU-Fin n X ≃ type-UU-Fin n X') →
+        ( a a' : D n X) →
+        ( sim-Equivalence-Relation (R n X) a a' ↔
+          sim-Equivalence-Relation
+            ( R n X')
+            ( map-equiv (invertible-action-D-equiv n X X' e) a)
+            ( map-equiv (invertible-action-D-equiv n X X' e) a'))
+      preserves-R-invertible-action-D-equiv n X =
+        ind-equiv-subuniverse
+          ( mere-equiv-Prop (Fin n))
+          ( X)
+          ( λ Y f →
+            ( a a' : D n X) →
+            ( sim-Equivalence-Relation (R n X) a a' ↔
+              sim-Equivalence-Relation
+                ( R n Y)
+                ( map-equiv (invertible-action-D-equiv n X Y f) a)
+                ( map-equiv (invertible-action-D-equiv n X Y f) a')))
+          ( λ a a' →
+            ( binary-tr
+              ( sim-Equivalence-Relation (R n X))
+                ( inv
+                  ( htpy-eq-equiv
+                    ( preserves-id-equiv-invertible-action-D-equiv n X)
+                    ( a)))
+                ( inv
+                  ( htpy-eq-equiv
+                    ( preserves-id-equiv-invertible-action-D-equiv n X)
+                    ( a')))) ,
+            ( binary-tr
+              ( sim-Equivalence-Relation (R n X))
+                ( htpy-eq-equiv
+                  ( preserves-id-equiv-invertible-action-D-equiv n X)
+                  ( a))
+                ( htpy-eq-equiv
+                  ( preserves-id-equiv-invertible-action-D-equiv n X)
+                  ( a'))))
 
     raise-UU-Fin-Fin : (n : ℕ) → UU-Fin l1 n
     pr1 (raise-UU-Fin-Fin n) = raise l1 (Fin n)
@@ -1490,7 +1514,7 @@ module _
             unit-trunc-Prop (compute-raise-Fin l1 (n +ℕ 2))))) →
     ¬ ( x ＝
         ( map-equiv
-          ( action-equiv-family-on-subuniverse
+          ( action-equiv-family-over-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( type-UU-Fin 2 ∘ Q (n +ℕ 2))
             ( raise l1 (Fin (n +ℕ 2)) ,

src/finite-group-theory/simpson-delooping-sign-homomorphism.lagda.md

@@ -21,7 +21,7 @@ open import finite-group-theory.permutations
 open import finite-group-theory.sign-homomorphism
 open import finite-group-theory.transpositions
 
-open import foundation.action-on-equivalences-families-over-subuniverses
+open import foundation.action-on-equivalences-type-families-over-subuniverses
 open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.coproduct-types
@@ -43,6 +43,7 @@ open import foundation.propositional-truncations
 open import foundation.raising-universe-levels
 open import foundation.sets
 open import foundation.transport-along-identifications
+open import foundation.type-theoretic-principle-of-choice
 open import foundation.unit-type
 open import foundation.universe-levels
 
@@ -683,7 +684,7 @@ module _
           unit-trunc-Prop (compute-raise-Fin l (n +ℕ 2))))
       ( sign-comp-aut-succ-succ-Fin n (transposition Y))
       ( map-equiv
-        ( action-equiv-family-on-subuniverse
+        ( action-equiv-family-over-subuniverse
           ( mere-equiv-Prop (Fin (n +ℕ 2)))
           ( λ X → Fin (n +ℕ 2) ≃ pr1 X)
           ( raise l (Fin (n +ℕ 2)) ,
@@ -716,20 +717,19 @@ module _
           simpson-comp-equiv (n +ℕ 2) ,
           preserves-id-equiv-simpson-comp-equiv (n +ℕ 2)}
         { y =
-          ( action-equiv-family-on-subuniverse
+          ( action-equiv-family-over-subuniverse
             ( mere-equiv-Prop (Fin (n +ℕ 2)))
             ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X) ,
-            ( preserves-id-equiv-action-equiv-family-on-subuniverse
+            ( compute-id-equiv-action-equiv-family-over-subuniverse
               ( mere-equiv-Prop (Fin (n +ℕ 2)))
               ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X)))}
         ( eq-is-contr
-          ( is-contr-preserves-id-action-equiv-family-on-subuniverse
-            ( mere-equiv-Prop (Fin (n +ℕ 2)))
-            ( λ X → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) X)
-            ( λ X →
-              is-set-equiv-is-set
-                ( is-set-Fin (n +ℕ 2))
-                ( is-set-type-UU-Fin (n +ℕ 2) X)))))
+          ( is-contr-equiv' _
+            ( distributive-Π-Σ)
+            ( is-contr-Π
+              ( unique-action-equiv-family-over-subuniverse
+                  ( mere-equiv-Prop (Fin (n +ℕ 2)))
+                  ( λ Y → Fin (n +ℕ 2) ≃ type-UU-Fin (n +ℕ 2) Y))))))
       ( not-sign-comp-transposition-count
         (n +ℕ 2 , (compute-raise l (Fin (n +ℕ 2)))) (star))
 

src/foundation.lagda.md

@@ -10,8 +10,10 @@ 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-families-over-subuniverses public
 open import foundation.action-on-equivalences-functions public
+open import foundation.action-on-equivalences-functions-out-of-subuniverses public
+open import foundation.action-on-equivalences-type-families public
+open import foundation.action-on-equivalences-type-families-over-subuniverses 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
@@ -251,6 +253,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
@@ -295,6 +298,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