Add files using upload-large-folder tool

.gitattributes

@@ -1483,3 +1483,83 @@ backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/proofmode/class
 backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/real_closed/complex.vo filter=lfs diff=lfs merge=lfs -text
 backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/TwoSphere.vo filter=lfs diff=lfs merge=lfs -text
 backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/bi/monpred.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_complete.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Interpreter_correct.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Main.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_complete.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MenhirLib/Validator_safe.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/BasicAst.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/config.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Environment.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentReflect.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/EnvironmentTyping.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Kernames.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/MonadBasicAst.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Reflect.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/uGraph.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/Universes.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Common/UniversesDec.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EArities.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAst.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EAstUtils.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/ECoInductiveToInductive.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EConstructorsAsBlocks.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EDeps.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpanded.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EEtaExpandedFix.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericGlobalMap.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EGenericMapEnv.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EImplementBox.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MetaCoq/Erasure/EInduction.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gfunctor.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/qpoly.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/view.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/spin_lock.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Paths.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/automorphism.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/implementations/semiring_pairs.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Interval/Transcend.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pFiber.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/gseries.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Displayed.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/heap_lang/lib/ticket_lock.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/TwoOneCat.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rationals.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Prod.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Integral_helper.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Card.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_ops.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/algebra/rat.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/base.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/fingroup/fingroup.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/ind.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/algebra/lib/gmap_view.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/deriving/instances/order.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Morphisms.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Shift.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Language/Lang_expr.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/bi/lib/fixpoint.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Yoneda.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/hall.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/NoSelect.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Tactics/Interval_helper.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/RelaxBitwidthAdcSbb.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Sigma.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/No/Addition.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Interval/Float/Specific_stdz.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/iris/program_logic/adequacy.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/.rustup/downloads/371a98be3e239f760a7f0e87793ad0a871cdc2e607590cc47514d91fd8d1383c filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/MathClasses/theory/rings.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pMap.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/alphageometry/meliad_lib/meliad/transformer/vocabs/pg19train_bpe_32000.model filter=lfs diff=lfs merge=lfs -text
+backend/core/.rustup/downloads/8c0a40a5411746ff6600d93acd16652fef56702196bb25b940ff399d7e107f40 filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/DisplayedEquiv.vo filter=lfs diff=lfs merge=lfs -text
+backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/mathcomp/solvable/jordanholder.vo filter=lfs diff=lfs merge=lfs -text

backend/core/.rustup/downloads/371a98be3e239f760a7f0e87793ad0a871cdc2e607590cc47514d91fd8d1383c

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:371a98be3e239f760a7f0e87793ad0a871cdc2e607590cc47514d91fd8d1383c
+size 3805000

backend/core/.rustup/downloads/8c0a40a5411746ff6600d93acd16652fef56702196bb25b940ff399d7e107f40

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:8c0a40a5411746ff6600d93acd16652fef56702196bb25b940ff399d7e107f40
+size 9163172

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/NoSelect.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:9f997e28fe542a0840c686b61edce8af6fa4a4a388c7eba24bc9c34cd15acf08
+size 369181

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Rewriter/Passes/RelaxBitwidthAdcSbb.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:ff1b7ced14aedd5c31c212ce24c392981b2d7b53923131968daa8455e4242702
+size 522748

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Modulo.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:32cba916ed4a7ba98c795207dbc59e6f6ae9f2daad94881930238dcbea70e6dd
+size 273119

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Morphisms.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:af5cb481d146c5672bd4647a1a12116978ac2a74cf32c1e9bc669ab242155490
+size 159937

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/Crypto/Util/ZUtil/Shift.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:0a962a0ce6eb50553bf702355d1e3d1b06e0d2092bce08db3f259a27c4a812d1
+size 114642

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:28322028ba1d17fd8bf3250a915a1ac6399ce227878c06cab3fa2fd7b67dde11
+size 1539801

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:6adb8d3bb8a10d07bbf0e69a75f639da0c029685adfc44b32685e181392964b9
+size 1271043

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:24c7899a221d5106d59cad716070d89155d3069afe39b16d4b07f80f90c4d055
+size 220502

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Sequence.v

@@ -0,0 +1,52 @@
+Require Import Basics.
+Require Import Diagrams.Graph.
+Require Import Diagrams.Diagram.
+
+Local Open Scope nat_scope.
+Local Open Scope path_scope.
+
+(** * Sequence *)
+
+(** A Sequence is a sequence of maps from [X(n)] to [X(n+1)]. *)
+
+Definition sequence_graph : Graph.
+Proof.
+  srapply (Build_Graph nat).
+  intros n m; exact (S n = m).
+Defined.
+
+Definition Sequence := Diagram sequence_graph.
+
+Definition Build_Sequence
+  (X : nat -> Type)
+  (f : forall n, X n -> X n.+1)
+  : Sequence.
+Proof.
+  srapply Build_Diagram.
+  1: exact X.
+  intros ? ? p.
+  destruct p.
+  apply f.
+Defined.
+
+(** A useful lemma to show than two sequences are equivalent. *)
+
+Definition equiv_sequence (D1 D2 : Sequence)
+  (H0 : (D1 0) <~> (D2 0))
+  (Hn: forall n (e: (D1 n) <~> (D2 n)),
+    {e' : (D1 n.+1) <~> (D2 n.+1) & (D2 _f 1) o e == e' o (D1 _f 1)})
+  : D1 ~d~ D2.
+Proof.
+  srapply (Build_diagram_equiv (Build_DiagramMap _ _)); intro n; simpl.
+  - apply equiv_fun.
+    induction n.
+    + apply H0.
+    + exact (Hn n IHn).1.
+  - intros m q; destruct q.
+    induction n; simpl.
+    + exact (Hn 0 H0).2.
+    + simple refine (Hn n.+1 _).2.
+  - induction n; simpl.
+    + apply H0.
+    + apply (Hn n _ ).1.
+Defined.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Diagrams/Span.v

@@ -0,0 +1,36 @@
+Require Import Basics.
+Require Import Types.
+Require Import Diagrams.Graph.
+Require Import Diagrams.Diagram.
+
+(** The underlying graph of a span. *)
+
+Definition span_graph : Graph.
+Proof.
+  srapply (Build_Graph (Unit + Bool)).
+  intros [i|i] [j|j].
+  2: exact Unit.
+  all: exact Empty.
+Defined.
+
+Section Span.
+
+  Context {A B C : Type}.
+
+  (** A span is a diagram:
+         f     g
+      B <-- A --> C     *)
+
+  Definition span (f : A -> B) (g : A -> C) : Diagram span_graph.
+  Proof.
+    srapply Build_Diagram.
+    - intros [i|i].
+      + exact A.
+      + exact (if i then B else C).
+    - intros [i|i] [j|j] u; cbn; try contradiction.
+      destruct j.
+      + exact f.
+      + exact g.
+  Defined.
+
+End Span.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/BiInv.v

@@ -0,0 +1,55 @@
+(* -*- mode: coq; mode: visual-line -*- *)
+
+Require Import HoTT.Basics HoTT.Types.
+
+Local Open Scope path_scope.
+Generalizable Variables A B f.
+
+(** * Bi-invertible maps *)
+
+(** A map is "bi-invertible" if it has both a section and a retraction, not necessarily the same.  This definition of equivalence was proposed by Andre Joyal. *)
+
+Definition BiInv `(f : A -> B) : Type
+  := {g : B -> A & g o f == idmap} * {h : B -> A & f o h == idmap}.
+
+(** It seems that the easiest way to show that bi-invertibility is equivalent to being an equivalence is also to show that both are h-props and that they are logically equivalent. *)
+
+Definition isequiv_biinv `(f : A -> B)
+  : BiInv f -> IsEquiv f.
+Proof.
+  intros [[g s] [h r]].
+  exact (isequiv_adjointify f g
+    (fun x => ap f (ap g (r x)^ @ s (h x)) @ r x)
+    s).
+Defined.
+
+Definition biinv_isequiv `(f : A -> B)
+  : IsEquiv f -> BiInv f.
+Proof.
+  intros [g s r adj].
+  exact ((g; r), (g; s)).
+Defined.
+
+Definition iff_biinv_isequiv `(f : A -> B)
+  : BiInv f <-> IsEquiv f.
+Proof.
+  split.
+  - apply isequiv_biinv.
+  - apply biinv_isequiv.
+Defined.
+
+Global Instance ishprop_biinv `{Funext} `(f : A -> B) : IsHProp (BiInv f) | 0.
+Proof.
+  apply hprop_inhabited_contr.
+  intros bif; pose (fe := isequiv_biinv f bif).
+  apply @contr_prod.
+  (* For this, we've done all the work already. *)
+  - by apply contr_retr_equiv.
+  - by apply contr_sect_equiv.
+Defined.
+
+Definition equiv_biinv_isequiv `{Funext} `(f : A -> B)
+  : BiInv f <~> IsEquiv f.
+Proof.
+  apply equiv_iff_hprop_uncurried, iff_biinv_isequiv.
+Defined.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/PathSplit.v

@@ -0,0 +1,126 @@
+(* -*- mode: coq; mode: visual-line -*- *)
+
+Require Import HoTT.Basics HoTT.Types.
+
+Local Open Scope nat_scope.
+Local Open Scope path_scope.
+
+Generalizable Variables A B f.
+
+Section AssumeFunext.
+Context `{Funext}.
+
+(** * n-Path-split maps.
+
+A map is n-path-split if its induced maps on the first n iterated path-spaces are split surjections.  Thus every map is 0-path-split, the 1-path-split maps are the split surjections, and so on.  It turns out that for n>1, being n-path-split is the same as being an equivalence. *)
+
+Fixpoint PathSplit (n : nat) `(f : A -> B) : Type
+  := match n with
+       | 0 => Unit
+       | S n => (forall a, hfiber f a) *
+                forall (x y : A), PathSplit n (@ap _ _ f x y)
+     end.
+
+Definition isequiv_pathsplit (n : nat) `{f : A -> B}
+: PathSplit n.+2 f -> IsEquiv f.
+Proof.
+  intros [g k].
+  pose (h := fun x y p => (fst (k x y) p).1).
+  pose (hs := fun x y => (fun p => (fst (k x y) p).2)
+                         : (ap f) o (h x y) == idmap).
+  clearbody hs; clearbody h; clear k.
+  apply isequiv_contr_map; intros b.
+  apply contr_inhabited_hprop.
+  2:exact (g b).
+  apply hprop_allpath; intros [a p] [a' p'].
+  refine (path_sigma' _ (h a a' (p @ p'^)) _).
+  refine (transport_paths_Fl _ _ @ _).
+  refine ((inverse2 (hs a a' (p @ p'^)) @@ 1) @ _).
+  refine ((inv_pp p p'^ @@ 1) @ _).
+  refine (concat_pp_p _ _ _ @ _).
+  refine ((1 @@ concat_Vp _) @ _).
+  exact ((inv_V p' @@ 1) @ concat_p1 _).
+Defined.
+
+Global Instance contr_pathsplit_isequiv
+           (n : nat) `(f : A -> B) `{IsEquiv _ _ f}
+: Contr (PathSplit n f).
+Proof.
+  generalize dependent B; revert A.
+  simple_induction n n IHn; intros A B f ?.
+  - exact _.
+  - apply contr_prod.
+Defined.
+
+Global Instance ishprop_pathsplit (n : nat) `(f : A -> B)
+: IsHProp (PathSplit n.+2 f).
+Proof.
+  apply hprop_inhabited_contr; intros ps.
+  pose (isequiv_pathsplit n ps).
+  exact _.
+Defined.
+
+Definition equiv_pathsplit_isequiv (n : nat) `(f : A -> B)
+: PathSplit n.+2 f <~> IsEquiv f.
+Proof.
+  refine (equiv_iff_hprop _ _).
+  - apply isequiv_pathsplit.
+  - intros ?; refine (center _).
+Defined.
+
+(** Path-splitness transfers across commutative squares of equivalences. *)
+Lemma equiv_functor_pathsplit (n : nat) {A B C D}
+      (f : A -> B) (g : C -> D) (h : A <~> C) (k : B <~> D)
+      (p : g o h == k o f)
+: PathSplit n f <~> PathSplit n g.
+Proof.
+  destruct n as [|n].
+  1:apply equiv_idmap.
+  destruct n as [|n].
+  - simpl.
+    refine (_ *E equiv_contr_contr).
+    refine (equiv_functor_forall' k^-1 _); intros d.
+    unfold hfiber.
+    refine (equiv_functor_sigma' h _); intros a.
+    refine (equiv_concat_l (p a) d oE _).
+    simpl; apply equiv_moveR_equiv_M.
+  - refine (_ oE equiv_pathsplit_isequiv n f).
+    refine ((equiv_pathsplit_isequiv n g)^-1 oE _).
+    apply equiv_iff_hprop; intros e.
+    + refine (isequiv_commsq f g h k (fun a => (p a)^)).
+    + refine (isequiv_commsq' f g h k p).
+Defined.
+
+(** A map is oo-path-split if it is n-path-split for all n.  This is also equivalent to being an equivalence. *)
+
+Definition ooPathSplit `(f : A -> B) : Type
+  := forall n, PathSplit n f.
+
+Definition isequiv_oopathsplit `{f : A -> B}
+: ooPathSplit f -> IsEquiv f
+  := fun ps => isequiv_pathsplit 0 (ps 2).
+
+Global Instance contr_oopathsplit_isequiv
+           `(f : A -> B) `{IsEquiv _ _ f}
+: Contr (ooPathSplit f).
+Proof.
+  apply contr_forall.
+Defined.
+
+Global Instance ishprop_oopathsplit `(f : A -> B)
+: IsHProp (ooPathSplit f).
+Proof.
+  apply hprop_inhabited_contr; intros ps.
+  pose (isequiv_oopathsplit ps).
+  exact _.
+Defined.
+
+Definition equiv_oopathsplit_isequiv `(f : A -> B)
+: ooPathSplit f <~> IsEquiv f.
+Proof.
+  refine (equiv_iff_hprop _ _).
+  - apply isequiv_oopathsplit.
+  - intros ?; refine (center _).
+Defined.
+
+End AssumeFunext.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Equiv/Relational.v

@@ -0,0 +1,68 @@
+(* -*- mode: coq; mode: visual-line -*- *)
+
+Require Import HoTT.Basics HoTT.Types.
+
+Local Open Scope nat_scope.
+Local Open Scope path_scope.
+
+Generalizable Variables A B f.
+
+(** * Relational equivalences *)
+
+(** This definition is due to Peter LeFanu Lumsdaine on the HoTT mailing list.  This definition gives more judgmental properties, though has the downside of jumping universe levels. *)
+
+Record RelEquiv A B :=
+  { equiv_rel : A -> B -> Type;
+    relequiv_contr_f : forall a, Contr { b : B & equiv_rel a b };
+    relequiv_contr_g : forall b, Contr { a : A & equiv_rel a b } }.
+
+Arguments equiv_rel {A B} _ _ _.
+Global Existing Instance relequiv_contr_f.
+Global Existing Instance relequiv_contr_g.
+
+Definition issig_relequiv {A B}
+  : { equiv_rel : A -> B -> Type
+    | { f : forall a, Contr { b : B & equiv_rel a b }
+      | forall b, Contr { a : A & equiv_rel a b } } }
+      <~> RelEquiv A B.
+Proof.
+  issig.
+Defined.
+
+Definition relequiv_of_equiv {A B} (e : A <~> B) : RelEquiv A B.
+Proof.
+  refine {| equiv_rel a b := e a = b |}.
+  (** The rest is found by typeclass inference! *)
+Defined.
+
+Definition equiv_of_relequiv {A B} (e : RelEquiv A B) : A <~> B.
+Proof.
+  refine (equiv_adjointify
+            (fun a => (center { b : B & equiv_rel e a b}).1)
+            (fun b => (center { a : A & equiv_rel e a b}).1)
+            _ _);
+    intro x; cbn.
+  { refine (ap pr1 (contr _) : _.1 = (x; _).1).
+    exact (center {a : A & equiv_rel e a x}).2. }
+  { refine (ap pr1 (contr _) : _.1 = (x; _).1).
+    exact (center {b : B & equiv_rel e x b}).2. }
+Defined.
+
+Definition RelIsEquiv {A B} (f : A -> B)
+  := { r : RelEquiv A B | forall x, (center { b : B & equiv_rel r x b }).1 = f x }.
+
+(** TODO: Prove [ishprop_relisequiv `{Funext} {A B} f : IsHProp (@RelIsEquiv A B f)] *)
+
+(** * Judgmental property *)
+Definition inverse_relequiv {A B} (e : RelEquiv A B) : RelEquiv B A
+  := {| equiv_rel a b := equiv_rel e b a |}.
+
+Definition reinv_V {A B} (e : RelEquiv A B)
+  : inverse_relequiv (inverse_relequiv e) = e
+  := 1.
+
+(** TODO: Is there a definition of this that makes [inverse_relequiv (relequiv_idmap A)] be [relequiv_idmap A], judgmentally? *)
+Definition relequiv_idmap A : RelEquiv A A
+  := {| equiv_rel a b := a = b |}.
+
+(** TODO: Define composition; we probably need truncation to do this? *)

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Flattening.v

@@ -0,0 +1,209 @@
+(* -*- mode: coq; mode: visual-line -*- *)
+
+(** * The flattening lemma. *)
+
+Require Import HoTT.Basics.
+Require Import Types.Paths Types.Forall Types.Sigma Types.Arrow Types.Universe.
+Local Open Scope path_scope.
+Require Import HoTT.Colimits.Coeq.
+
+(** The base HIT [W] is just a homotopy coequalizer [Coeq]. *)
+
+(** TODO: Make the names in this file more usable, move it into [Coeq.v], and use it to derive corresponding flattening lemmas for [pushout], etc. *)
+
+(** Now we define the flattened HIT which will be equivalent to the total space of a fibration over [W]. *)
+
+Module Export FlattenedHIT.
+
+Private Inductive Wtil (A B : Type) (f g : B -> A)
+  (C : A -> Type) (D : forall b, C (f b) <~> C (g b))
+  : Type :=
+| cct : forall a, C a -> Wtil A B f g C D.
+
+Arguments cct {A B f g C D} a c.
+
+Axiom ppt : forall {A B f g C D} (b:B) (y:C (f b)),
+  @cct A B f g C D (f b) y = cct (g b) (D b y).
+
+Definition Wtil_ind {A B f g C D} (Q : Wtil A B f g C D -> Type)
+  (cct' : forall a x, Q (cct a x))
+  (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y))
+  : forall w, Q w
+  := fun w => match w with cct a x => fun _ => cct' a x end ppt'.
+
+Axiom Wtil_ind_beta_ppt
+  : forall {A B f g C D} (Q : Wtil A B f g C D -> Type)
+    (cct' : forall a x, Q (cct a x))
+    (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y))
+    (b:B) (y : C (f b)),
+    apD (Wtil_ind Q cct' ppt') (ppt b y) = ppt' b y.
+
+End FlattenedHIT.
+
+Definition Wtil_rec {A B f g C} {D : forall b, C (f b) <~> C (g b)}
+  (Q : Type) (cct' : forall a (x : C a), Q)
+  (ppt' : forall b (y : C (f b)), cct' (f b) y = cct' (g b) (D b y))
+  : Wtil A B f g C D -> Q
+  := Wtil_ind (fun _ => Q) cct' (fun b y => transport_const _ _ @ ppt' b y).
+
+Definition Wtil_rec_beta_ppt
+  {A B f g C} {D : forall b, C (f b) <~> C (g b)}
+  (Q : Type) (cct' : forall a (x : C a), Q)
+  (ppt' : forall (b:B) (y : C (f b)), cct' (f b) y = cct' (g b) (D b y))
+  (b:B) (y: C (f b))
+  : ap (@Wtil_rec A B f g C D Q cct' ppt') (ppt b y) = ppt' b y.
+Proof.
+  unfold Wtil_rec.
+  eapply (cancelL (transport_const (ppt (C:=C) b y) _)).
+  refine ((apD_const
+    (@Wtil_ind A B f g C D (fun _ => Q) cct' _) (ppt b y))^ @ _).
+  refine (Wtil_ind_beta_ppt (fun _ => Q) _ _ _ _).
+Defined.
+
+
+
+(** Now we define the fibration over it that we will be considering the total space of. *)
+
+Section AssumeAxioms.
+Context `{Univalence}.
+
+Context {B A : Type} {f g : B -> A}.
+Context {C : A -> Type} {D : forall b, C (f b) <~> C (g b)}.
+
+Let W' := Coeq f g.
+
+Let P : W' -> Type
+  := Coeq_rec Type C (fun b => path_universe (D b)).
+
+
+
+(** Now we give the total space the same structure as [Wtil]. *)
+
+Let sWtil := { w:W' & P w }.
+
+Let scct (a:A) (x:C a) : sWtil := (exist P (coeq a) x).
+
+Let sppt (b:B) (y:C (f b)) : scct (f b) y = scct (g b) (D b y)
+  := path_sigma' P (cglue b)
+       (transport_path_universe' P (cglue b) (D b)
+         (Coeq_rec_beta_cglue Type C (fun b0 => path_universe (D b0)) b) y).
+
+(** Here is the dependent eliminator *)
+Definition sWtil_ind (Q : sWtil -> Type)
+  (scct' : forall a x, Q (scct a x))
+  (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y))
+  : forall w, Q w.
+Proof.
+  apply sig_ind.
+  refine (Coeq_ind (fun w => forall x:P w, Q (w;x))
+    (fun a x => scct' a x) _).
+  intros b.
+  apply (dpath_forall P (fun a b => Q (a;b)) _ _ (cglue b)
+    (scct' (f b)) (scct' (g b))).
+  intros y.
+  set (q := transport_path_universe' P (cglue b) (D b)
+    (Coeq_rec_beta_cglue Type C (fun b0 : B => path_universe (D b0)) b) y).
+  rewrite transportD_is_transport.
+  refine (_ @ apD (scct' (g b)) q^).
+  refine (moveL_transport_V (fun x => Q (scct (g b) x)) q _ _ _).
+  rewrite transport_compose, <- transport_pp.
+  refine (_ @ sppt' b y).
+  apply ap10, ap.
+  refine (whiskerL _ (ap_exist P (coeq (g b)) _ _ q) @ _).
+  exact ((path_sigma_p1_1p' _ _ _)^).
+Defined.
+
+(** The eliminator computes on the point constructor. *)
+Definition sWtil_ind_beta_cct (Q : sWtil -> Type)
+  (scct' : forall a x, Q (scct a x))
+  (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y))
+  (a:A) (x:C a)
+  : sWtil_ind Q scct' sppt' (scct a x) = scct' a x
+  := 1.
+
+(** This would be its propositional computation rule on the path constructor... *)
+(**
+<<
+Definition sWtil_ind_beta_ppt (Q : sWtil -> Type)
+  (scct' : forall a x, Q (scct a x))
+  (sppt' : forall b y, (sppt b y) # (scct' (f b) y) = scct' (g b) (D b y))
+  (b:B) (y:C (f b))
+  : apD (sWtil_ind Q scct' sppt') (sppt b y) = sppt' b y.
+Proof.
+  unfold sWtil_ind.
+  (** ... but it's a doozy! *)
+Abort.
+>>
+*)
+
+(** Fortunately, it turns out to be enough to have the computation rule for the *non-dependent* eliminator! *)
+
+(** We could define that in terms of the dependent one, as usual...
+<<
+Definition sWtil_rec (P : Type)
+  (scct' : forall a (x : C a), P)
+  (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y))
+  : sWtil -> P
+  := sWtil_ind (fun _ => P) scct' (fun b y => transport_const _ _ @ sppt' b y).
+>>
+*)
+
+(** ...but if we define it diindly, then it's easier to reason about. *)
+Definition sWtil_rec (Q : Type)
+  (scct' : forall a (x : C a), Q)
+  (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y))
+  : sWtil -> Q.
+Proof.
+  apply sig_ind.
+  refine (Coeq_ind (fun w => P w -> Q) (fun a x => scct' a x) _).
+  intros b.
+  refine (dpath_arrow P (fun _ => Q) _ _ _ _).
+  intros y.
+  refine (transport_const _ _ @ _).
+  refine (sppt' b _ @ ap _ _).
+  refine ((transport_path_universe' P (cglue b) (D b) _ _)^).
+  exact (Coeq_rec_beta_cglue _ _ _ _).
+Defined.
+
+Open Scope long_path_scope.
+
+Definition sWtil_rec_beta_ppt (Q : Type)
+  (scct' : forall a (x : C a), Q)
+  (sppt' : forall b (y : C (f b)), scct' (f b) y = scct' (g b) (D b y))
+  (b:B) (y: C (f b))
+  : ap (sWtil_rec Q scct' sppt') (sppt b y) = sppt' b y.
+Proof.
+  unfold sWtil_rec, sppt.
+  refine (@ap_sig_rec_path_sigma W' P Q _ _ (cglue b) _ _ _ _ @ _); simpl.
+  rewrite (@Coeq_ind_beta_cglue B A f g).
+  rewrite (ap10_dpath_arrow P (fun _ => Q) (cglue b) _ _ _ y).
+  repeat rewrite concat_p_pp.
+  (** Now everything cancels! *)
+  rewrite ap_V, concat_pV_p, concat_pV_p, concat_pV_p, concat_Vp.
+  by apply concat_1p.
+Qed.
+
+Close Scope long_path_scope.
+
+(** Woot! *)
+Definition equiv_flattening : Wtil A B f g C D <~> sWtil.
+Proof.
+  (** The maps back and forth are obtained easily from the non-dependent eliminators. *)
+  refine (equiv_adjointify
+    (Wtil_rec _ scct sppt)
+    (sWtil_rec _ cct ppt)
+    _ _).
+  (** The two homotopies are completely symmetrical, using the *dependent* eliminators, but only the computation rules for the non-dependent ones. *)
+  - refine (sWtil_ind _ (fun a x => 1) _). intros b y.
+    apply dpath_path_FFlr.
+    rewrite concat_1p, concat_p1.
+    rewrite sWtil_rec_beta_ppt.
+      by symmetry; apply (@Wtil_rec_beta_ppt A B f g C D).
+  - refine (Wtil_ind _ (fun a x => 1) _). intros b y.
+    apply dpath_path_FFlr.
+    rewrite concat_1p, concat_p1.
+    rewrite Wtil_rec_beta_ppt.
+      by symmetry; apply sWtil_rec_beta_ppt.
+Defined.
+
+End AssumeAxioms.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.v

@@ -0,0 +1,102 @@
+(* -*- mode: coq; mode: visual-line -*- *)
+Require Import HoTT.Basics HoTT.Types.
+Require Import Spaces.Int Spaces.Circle.
+Require Import Colimits.Coeq HIT.Flattening Truncations.Core Truncations.Connectedness.
+
+Local Open Scope path_scope.
+
+(** * Quotients by free actions of [Int] *)
+
+(** We will show that if [Int] acts freely on a set, then the set-quotient of that action can be defined without a 0-truncation, giving it a universal property for mapping into all types. *)
+
+Section FreeIntAction.
+
+  Context `{Univalence}.
+  Context (R : Type) `{IsHSet R}.
+
+  (** A free action by [Int] is the same as a single autoequivalence [f] (the action of [1]) whose iterates are all pointwise distinct. *)
+  Context (f : R <~> R)
+          (f_free : forall (r : R) (n m : Int),
+                      (int_iter f n r = int_iter f m r) -> (n = m)).
+
+  (** We can then define the quotient to be the coequalizer of [f] and the identity map.  This gives it the desired universal property for all types; it remains to show that this definition gives a set. *)
+  Let RmodZ := Coeq f idmap.
+
+  (** Together, [R] and [f] define a fibration over [Circle].  By the flattening lemma, its total space is equivalent to the quotient. *)
+  Global Instance isset_RmodZ : IsHSet RmodZ.
+  Proof.
+    nrefine (istrunc_equiv_istrunc
+              { z : Circle & Circle_rec Type R (path_universe f) z}
+              (_ oE (@equiv_flattening _ Unit Unit idmap idmap
+                                  (fun _ => R) (fun _ => f))^-1
+              oE _));
+    try exact _.
+    - unshelve rapply equiv_adjointify.
+      + simple refine (Wtil_rec _ _ _).
+        * intros u r; exact (coeq r).
+        * intros u r; cbn. exact ((cglue r)^).
+      + simple refine (Coeq_rec _ _ _).
+        * exact (cct tt).
+        * intros r; exact ((ppt tt r)^).
+      + refine (Coeq_ind _ (fun a => 1) _); cbn; intros b.
+        rewrite transport_paths_FlFr, concat_p1, ap_idmap.
+        apply moveR_Vp; rewrite concat_p1.
+        rewrite ap_compose.
+        rewrite (Coeq_rec_beta_cglue
+                   (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
+                   (cct tt) (fun r => (ppt tt r)^) b).
+        rewrite ap_V; symmetry.
+        refine (inverse2
+                  (Wtil_rec_beta_ppt
+                     RmodZ (unit_name (fun r => coeq r))
+                     (unit_name (fun r => (cglue r)^)) tt b) @ inv_V _).
+      + simple refine (Wtil_ind _ _ _); cbn.
+        { intros [] ?; reflexivity. }
+        intros [] r; cbn.
+        rewrite transport_paths_FlFr, concat_p1, ap_idmap.
+        apply moveR_Vp; rewrite concat_p1.
+        rewrite ap_compose.
+        refine (_ @ ap (ap _) (Wtil_rec_beta_ppt
+                   RmodZ (unit_name (fun r => coeq r))
+                   (unit_name (fun r => (cglue r)^)) tt r)^).
+        rewrite ap_V.
+        rewrite (Coeq_rec_beta_cglue
+                   (Wtil Unit Unit idmap idmap (unit_name R) (unit_name f))
+                   (cct tt) (fun r0 : R => (ppt tt r0)^) r).
+        symmetry; apply inv_V.
+    - apply equiv_functor_sigma_id; intros x.
+      apply equiv_path.
+      revert x; refine (Circle_ind _ 1 _); cbn.
+      rewrite transport_paths_FlFr, concat_p1.
+      apply moveR_Vp; rewrite concat_p1.
+      rewrite Circle_rec_beta_loop.
+      unfold loop.
+      exact (Coeq_rec_beta_cglue _ _ _ _).
+    - apply istrunc_S.
+      intros xu yv.
+      nrefine (istrunc_equiv_istrunc (n := -1) _ (equiv_path_sigma _ xu yv)).
+      destruct xu as [x u], yv as [y v]; cbn.
+      apply hprop_allpath.
+      intros [p r] [q s].
+      set (P := Circle_rec Type R (path_universe f)) in *.
+      assert (forall z, IsHSet (P z)).
+      { simple refine (Circle_ind _ _ _); cbn beta.
+        - exact _.
+        - apply path_ishprop. }
+      apply path_sigma_hprop; cbn.
+      assert (t := r @ s^); clear r s.
+      assert (xb := merely_path_is0connected Circle base x).
+      assert (yb := merely_path_is0connected Circle base y).
+      strip_truncations. destruct xb, yb.
+      revert p q t.
+      equiv_intro (equiv_loopCircle_int^-1) n.
+      equiv_intro (equiv_loopCircle_int^-1) m.
+      subst P.
+      rewrite !Circle_action_is_iter.
+      intros p. apply ap.
+      exact (f_free u n m p).
+  Qed.
+
+  (** TODO: Prove that this [RmodZ] is equivalent to the set-quotient of [R] by a suitably defined equivalence relation. *)
+
+End FreeIntAction.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/Interval.v

@@ -0,0 +1,52 @@
+(* -*- mode: coq; mode: visual-line -*- *)
+
+(** * Theorems about the homotopical interval. *)
+
+Require Import Basics.Overture Basics.PathGroupoids.
+Require Import Types.Paths.
+
+Local Open Scope path_scope.
+
+
+Module Export Interval.
+
+Private Inductive interval : Type0 :=
+  | zero : interval
+  | one : interval.
+
+Axiom seg : zero = one.
+
+Definition interval_ind (P : interval -> Type)
+  (a : P zero) (b : P one) (p : seg # a = b)
+  : forall x:interval, P x
+  := fun x => (match x return _ -> P x with
+                | zero => fun _ => a
+                | one  => fun _ => b
+              end) p.
+
+Axiom interval_ind_beta_seg : forall (P : interval -> Type)
+  (a : P zero) (b : P one) (p : seg # a = b),
+  apD (interval_ind P a b p) seg = p.
+
+End Interval.
+
+Definition interval_rec (P : Type) (a b : P) (p : a = b)
+  : interval -> P
+  := interval_ind (fun _ => P) a b (transport_const _ _ @ p).
+
+Definition interval_rec_beta_seg (P : Type) (a b : P) (p : a = b)
+  : ap (interval_rec P a b p) seg = p.
+Proof.
+  refine (cancelL (transport_const seg a) _ _ _).
+  refine ((apD_const (interval_ind (fun _ => P) a b _) seg)^ @ _).
+  refine (interval_ind_beta_seg (fun _ => P) _ _ _).
+Defined.
+
+(** ** The interval is contractible. *)
+
+Global Instance contr_interval : Contr interval | 0.
+Proof.
+  apply (Build_Contr _ zero).
+  refine (interval_ind _ 1 seg _).
+  refine (transport_paths_r _ _ @ concat_1p _).
+Defined.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/SetCone.v

@@ -0,0 +1,16 @@
+(* -*- mode: coq; mode: visual-line -*- *)
+Require Import HoTT.Basics Types.Unit.
+Require Import Colimits.Pushout.
+Require Import Truncations.Core.
+
+(** * Cones of HSets *)
+
+Section SetCone.
+  Context {A B : HSet} (f : A -> B).
+
+  Definition setcone := Trunc 0 (Pushout@{_ _ Set _} f (const_tt A)).
+
+  Global Instance istrunc_setcone : IsHSet setcone := _.
+
+  Definition setcone_point : setcone := tr (push (inr tt)).
+End SetCone.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/epi.v

@@ -0,0 +1,182 @@
+Require Import Basics.
+Require Import Types.
+Require Import TruncType.
+Require Import ReflectiveSubuniverse.
+Require Import Colimits.Pushout Truncations.Core HIT.SetCone.
+
+Local Open Scope path_scope.
+
+Section AssumingUA.
+Context `{ua:Univalence}.
+
+(** We will now prove that for sets, epis and surjections are equivalent.*)
+Definition isepi {X Y} `(f:X->Y) := forall Z: HSet,
+  forall g h: Y -> Z, g o f = h o f -> g = h.
+
+Definition isepi_funext {X Y : Type} (f : X -> Y)
+  := forall Z : HSet, forall g0 g1 : Y -> Z, g0 o f == g1 o f -> g0 == g1.
+
+Definition isepi' {X Y} `(f : X -> Y) :=
+  forall (Z : HSet) (g : Y -> Z), Contr { h : Y -> Z | g o f = h o f }.
+
+Lemma equiv_isepi_isepi' {X Y} f : @isepi X Y f <~> @isepi' X Y f.
+Proof.
+  unfold isepi, isepi'.
+  apply (@equiv_functor_forall' _ _ _ _ _ (equiv_idmap _)); intro Z.
+  apply (@equiv_functor_forall' _ _ _ _ _ (equiv_idmap _)); intro g.
+  unfold equiv_idmap; simpl.
+  refine (transitivity (@equiv_sig_ind _ (fun h : Y -> Z => g o f = h o f) (fun h => g = h.1)) _).
+  (** TODO(JasonGross): Can we do this entirely by chaining equivalences? *)
+  apply equiv_iff_hprop.
+  { intro hepi.
+    nrapply (Build_Contr _ (g; idpath)).
+    intro xy; specialize (hepi xy).
+    apply path_sigma_uncurried.
+    exists hepi.
+    apply path_ishprop. }
+  { intros hepi xy.
+    exact (ap pr1 ((contr (g; 1))^ @ contr xy)). }
+Defined.
+
+Definition equiv_isepi_isepi_funext {X Y : Type} (f : X -> Y)
+  : isepi f <~> isepi_funext f.
+Proof.
+  apply equiv_iff_hprop.
+  - intros e ? g0 g1 h.
+    apply equiv_path_arrow.
+    apply e.
+    by apply path_arrow.
+  - intros e ? g0 g1 p.
+    apply path_arrow.
+    apply e.
+    by apply equiv_path_arrow.
+Defined.
+
+Section cones.
+  Lemma isepi'_contr_cone `{Funext} {A B : HSet} (f : A -> B) : isepi' f -> Contr (setcone f).
+  Proof.
+    intros hepi.
+    apply (Build_Contr _ (setcone_point _)).
+    pose (alpha1 := @pglue A B Unit f (const_tt _)).
+    pose (tot:= { h : B -> setcone f & tr o push o inl o f = h o f }).
+    transparent assert (l : tot).
+    { simple refine (tr o _ o inl; _).
+      { refine push. }
+      { refine idpath. } }
+    pose (r := (@const B (setcone f) (setcone_point _); (ap (fun f => @tr 0 _ o f) (path_forall _ _ alpha1))) : tot).
+    subst tot.
+    assert (X : l = r).
+      { let lem := constr:(fun X push' => hepi (Build_HSet (setcone f)) (tr o push' o @inl _ X)) in
+        pose (lem _ push).
+        refine (path_contr l r). }
+    subst l r.
+
+    pose (I0 b := ap10 (X ..1) b).
+    refine (Trunc_ind _ _).
+    pose (fun a : B + Unit => (match a as a return setcone_point _ = tr (push a) with
+                                 | inl a' => (I0 a')^
+                                 | inr tt => idpath
+                               end)) as I0f.
+    refine (Pushout_ind _ (fun a' => I0f (inl a')) (fun u => (I0f (inr u))) _).
+
+    simpl. subst alpha1. intros.
+    unfold setcone_point.
+    subst I0. simpl.
+    pose (X..2) as p. simpl in p.
+    rewrite (transport_precompose f _ _ X..1) in p.
+    assert (H':=concat (ap (fun x => ap10 x a) p) (ap10_ap_postcompose tr (path_arrow (pushl o f) (pushr o const_tt _) pglue) _)).
+    rewrite ap10_path_arrow in H'.
+    clear p.
+    (** Apparently [pose; clearbody] is only ~.8 seconds, while [pose proof] is ~4 seconds? *)
+    pose (concat (ap10_ap_precompose f (X ..1) a)^ H') as p.
+    clearbody p.
+    simpl in p.
+    rewrite p.
+    rewrite transport_paths_Fr.
+    apply concat_Vp.
+  Qed.
+End cones.
+
+Lemma issurj_isepi {X Y} (f:X->Y): IsSurjection f -> isepi f.
+Proof.
+intros sur ? ? ? ep. apply path_forall. intro y.
+specialize (sur y). pose (center (merely (hfiber f y))).
+apply (Trunc_rec (n:=-1) (A:=(sig (fun x : X => f x = y))));
+  try assumption.
+intros [x p]. set (p0:=apD10 ep x).
+transitivity (g (f x)).
+- by apply ap.
+- transitivity (h (f x));auto with path_hints. by apply ap.
+Qed.
+
+Corollary issurj_isepi_funext {X Y} (f:X->Y) : IsSurjection f -> isepi_funext f.
+Proof.
+  intro s.
+  apply equiv_isepi_isepi_funext.
+  by apply issurj_isepi.
+Defined.
+
+(** Old-style proof using polymorphic Omega. Needs resizing for the isepi proof to live in the
+ same universe as X and Y (the Z quantifier is instantiated with an HSet at a level higher)
+<<
+Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> issurj f.
+Proof.
+  intros epif y.
+  set (g :=fun _:Y => Unit_hp).
+  set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))).
+  assert (X1: g o f = h o f ).
+  - apply path_forall. intro x. apply path_equiv_biimp_rec;[|done].
+    intros _ . apply min1. exists tt. by (exists x).
+  - specialize (epif _ g h).
+    specialize (epif X1). clear X1.
+    set (p:=apD10 epif y).
+    apply (@minus1Trunc_map (sig (fun _ : Unit => sig (fun x : X => y = f x)))).
+    + intros [ _ [x eq]].
+      exists x.
+        by symmetry.
+    + apply (transport hproptype p tt).
+Defined.
+>>
+*)
+
+Section isepi_issurj.
+  Context {X Y : HSet} (f : X -> Y) (Hisepi : isepi f).
+  Definition epif := equiv_isepi_isepi' _ Hisepi.
+  Definition fam (c : setcone f) : HProp.
+  Proof.
+    pose (fib y := hexists (fun x : X => f x = y)).
+    apply (fun f => @Trunc_rec _ _ HProp _ f c).
+    refine (Pushout_rec HProp fib (fun _ => Unit_hp) (fun x => _)).
+    (** Prove that the truncated sigma is equivalent to Unit *)
+    pose (contr_inhabited_hprop (fib (f x)) (tr (x; idpath))) as i.
+    apply path_hprop. simpl. simpl in i.
+    apply (equiv_contr_unit).
+  Defined.
+
+  Lemma isepi_issurj : IsSurjection f.
+  Proof.
+    intros y.
+    pose (i := isepi'_contr_cone _ epif).
+
+    assert (X0 : forall x : setcone f, fam x = fam (setcone_point f)).
+    { intros. apply contr_dom_equiv. apply i. }
+    specialize (X0 (tr (push (inl y)))). simpl in X0.
+    unfold IsConnected.
+    refine (transport (fun A => Contr A) (ap trunctype_type X0)^ _); exact _.
+  Defined.
+End isepi_issurj.
+
+Lemma isepi_isequiv X Y (f : X -> Y) `{IsEquiv _ _ f}
+: isepi f.
+Proof.
+  intros ? g h H'.
+  apply ap10 in H'.
+  apply path_forall.
+  intro x.
+  transitivity (g (f (f^-1 x))).
+  - by rewrite eisretr.
+  - transitivity (h (f (f^-1 x))).
+    * apply H'.
+    * by rewrite eisretr.
+Qed.
+End AssumingUA.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/iso.v

@@ -0,0 +1,41 @@
+Require Import HoTT.Basics.
+Require Import Types.Universe.
+Require Import HSet.
+Require Import HIT.epi HIT.unique_choice.
+
+Local Open Scope path_scope.
+
+(** We prove that [epi + mono <-> IsEquiv] *)
+Section iso.
+  Context `{Univalence}.
+  Variables X Y : HSet.
+  Variable f : X -> Y.
+
+  Lemma atmost1P_isinj (injf : isinj f)
+  : forall y : Y, atmost1P (fun x => f x = y).
+  Proof.
+    unfold isinj, atmost1P in *.
+    intros.
+    apply injf.
+    path_induction.
+    reflexivity.
+  Defined.
+
+  Definition isequiv_isepi_ismono (epif : isepi f) (monof : ismono f)
+  : IsEquiv f.
+  Proof.
+    pose proof (@isepi_issurj _ _ _ f epif) as surjf.
+    pose proof (isinj_ismono _ monof) as injf.
+    pose proof (unique_choice
+                  (fun y x => f x = y)
+                  _
+                  (fun y => (@center _ (surjf y), atmost1P_isinj injf y)))
+      as H_unique_choice.
+    apply (isequiv_adjointify _ H_unique_choice.1).
+    - intro.
+      apply H_unique_choice.2.
+    - intro.
+      apply injf.
+      apply H_unique_choice.2.
+  Defined.
+End iso.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/quotient.v

@@ -0,0 +1,328 @@
+(* -*- mode: coq; mode: visual-line -*-  *)
+Require Import HoTT.Basics HoTT.Types.
+Require Import HSet TruncType.
+Require Import Truncations.Core.
+
+Local Open Scope path_scope.
+
+(** * The set-quotient of a type by an hprop-valued relation
+
+We aim to model:
+<<
+Inductive quotient : Type :=
+   | class_of : A -> quotient
+   | related_classes_eq : forall x y, (R x y), class_of x = class_of y
+   | quotient_set : IsHSet quotient
+>>
+*)
+
+(** TODO:  This development should be further connected with the sections in the book; see below.  And it should be merged with Colimits.Quotient. Currently this file is only used in Classes/implementations/natpair_integers.v and Classes/implementations/field_of_fractions.v, so it shouldn't be too hard to switch to Colimits.Quotient. *)
+
+Module Export Quotient.
+
+  Section Domain.
+
+    Universes i j u.
+    Constraint i <= u, j <= u.
+
+    Context {A : Type@{i}} (R : Relation@{i j} A) {sR: is_mere_relation _ R}.
+
+    (** We choose to let the definition of quotient depend on the proof that [R] is a set-relations.  Alternatively, we could have defined it for all relations and only develop the theory for set-relations.  The former seems more natural.
+
+We do not require [R] to be an equivalence relation, but implicitly consider its transitive-reflexive closure. *)
+
+    (** This definition has a parameter [sR] that shadows the ambient one in the Context in order to ensure that it actually ends up depending on everything in the Context when the section is closed, since its definition doesn't actually refer to any of them.  *)
+    Private Inductive quotient {sR: is_mere_relation _ R} : Type@{u} :=
+    | class_of : A -> quotient.
+
+    (** The path constructors. *)
+    Axiom related_classes_eq
+    : forall {x y : A}, R x y ->
+                        class_of x = class_of y.
+
+    Axiom quotient_set : IsHSet (@quotient sR).
+    Global Existing Instance quotient_set.
+
+    Definition quotient_ind (P : (@quotient sR) -> Type) {sP : forall x, IsHSet (P x)}
+               (dclass : forall x, P (class_of x))
+               (dequiv : (forall x y (H : R x y), (related_classes_eq H) # (dclass x) = dclass y))
+    : forall q, P q
+      := fun q => match q with class_of a => fun _ _ => dclass a end sP dequiv.
+
+    Definition quotient_ind_compute {P sP} dclass dequiv x
+    : @quotient_ind P sP dclass dequiv (class_of x) = dclass x.
+    Proof.
+      reflexivity.
+    Defined.
+
+    (** Again equality of paths needs to be postulated *)
+    Axiom quotient_ind_compute_path
+    : forall P sP dclass dequiv,
+      forall x y (H : R x y),
+        apD (@quotient_ind P sP dclass dequiv) (related_classes_eq H)
+        = dequiv x y H.
+
+  End Domain.
+
+End Quotient.
+
+Section Equiv.
+
+  Context `{Univalence}.
+
+  Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
+          {Htrans : Transitive R} {Hsymm : Symmetric R}.
+
+  Lemma quotient_path2 : forall {x y : quotient R} (p q : x=y), p=q.
+  Proof.
+    apply @hset_path2. apply _.
+  Defined.
+
+  Definition in_class : quotient R -> A -> HProp.
+  Proof.
+    refine (quotient_ind R (fun _ => A -> HProp) (fun a b => Build_HProp (R a b)) _).
+    intros. eapply concat;[apply transport_const|].
+    apply path_forall. intro z. apply path_hprop; simpl.
+    apply @equiv_iff_hprop; eauto.
+  Defined.
+
+  Context {Hrefl : Reflexive R}.
+
+  Lemma in_class_pr : forall x y, (in_class (class_of R x) y : Type) = R x y.
+  Proof.
+    reflexivity.
+  Defined.
+
+  Lemma quotient_ind_prop (P : quotient R -> Type)
+        `{forall x, IsHProp (P x)} :
+    forall dclass : forall x, P (class_of R x),
+    forall q, P q.
+  Proof.
+    intros. apply (quotient_ind R P dclass).
+    intros. apply path_ishprop.
+  Defined.
+
+  Global Instance decidable_in_class `{forall x y, Decidable (R x y)}
+  : forall x a, Decidable (in_class x a).
+  Proof.
+    refine (quotient_ind_prop _ _).
+    intros a b; exact (transport Decidable (in_class_pr a b) _).
+  Defined.
+
+  Lemma class_of_repr : forall q x, in_class q x -> q = class_of R x.
+  Proof.
+    apply (quotient_ind R
+                        (fun q : quotient R => forall x, in_class q x -> q = class_of _ x)
+                        (fun x y H => related_classes_eq R H)).
+    intros.
+    apply path_forall. intro z.
+    apply path_forall;intro H'.
+    apply quotient_path2.
+  Defined.
+
+  Lemma classes_eq_related : forall x y,
+                               class_of R x = class_of R y -> R x y.
+  Proof.
+    intros x y H'.
+    pattern (R x y).
+    eapply transport.
+    - apply in_class_pr.
+    - pattern (class_of R x). apply (transport _ (H'^)).
+      apply Hrefl.
+  Defined.
+
+  (** Thm 10.1.8 *)
+  Theorem sets_exact : forall x y, (class_of R x = class_of R y) <~> R x y.
+    intros ??. apply equiv_iff_hprop.
+    - apply classes_eq_related.
+    - apply related_classes_eq.
+  Defined.
+
+  Definition quotient_rec {B : Type} {sB : IsHSet B}
+             (dclass : (forall x : A, B))
+             (dequiv : (forall x y, R x y -> dclass x = dclass y))
+  : quotient R -> B.
+  Proof.
+    apply (quotient_ind R (fun _ : quotient _ => B)) with dclass.
+    intros ?? H'. destruct (related_classes_eq R H'). by apply dequiv.
+  Defined.
+
+  Definition quotient_rec2 {B : HSet} {dclass : (A -> A -> B)}:
+    forall dequiv : (forall x x', R x x' -> forall y y',  R y y' ->
+                                                          dclass x y = dclass x' y'),
+      quotient R -> quotient R -> B.
+  Proof.
+    intro.
+    assert (dequiv0 : forall x x0 y : A, R x0 y -> dclass x x0 = dclass x y)
+      by (intros ? ? ? Hx; apply dequiv;[apply Hrefl|done]).
+    refine (quotient_rec
+              (fun x => quotient_rec (dclass x) (dequiv0 x)) _).
+    intros x x' Hx.
+    apply path_forall. red.
+    assert (dequiv1 : forall y : A,
+                        quotient_rec (dclass x) (dequiv0 x) (class_of _ y) =
+                        quotient_rec (dclass x') (dequiv0 x') (class_of _ y))
+      by (intros; by apply dequiv).
+    refine (quotient_ind R (fun q =>
+                              quotient_rec (dclass x) (dequiv0 x) q =
+                              quotient_rec (dclass x') (dequiv0 x') q) dequiv1 _).
+    intros. apply path_ishprop.
+  Defined.
+
+  Definition quotient_ind_prop' : forall P : quotient R -> Type,
+                                  forall (Hprop' : forall x, IsHProp (P (class_of _ x))),
+                                    (forall x, P (class_of _ x)) -> forall y, P y.
+  Proof.
+    intros ? ? dclass. apply quotient_ind with dclass.
+    - simple refine (quotient_ind R (fun x => IsHSet (P x)) _ _); cbn beta; try exact _.
+      intros; apply path_ishprop.
+    - intros. apply path_ishprop.
+  Defined.
+
+  (** From Ch6 *)
+  Theorem quotient_surjective: IsSurjection (class_of R).
+  Proof.
+    apply BuildIsSurjection.
+    apply (quotient_ind_prop (fun y => merely (hfiber (class_of R) y))); try exact _.
+    intro x. apply tr. by exists x.
+  Defined.
+
+  (** From Ch10 *)
+  Definition quotient_ump' (B:HSet): (quotient R -> B) ->
+                                     (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))).
+    intro f. exists (compose f (class_of R) ).
+    intros. f_ap. by apply related_classes_eq.
+  Defined.
+
+  Definition quotient_ump'' (B:HSet): (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0)))
+                                      -> quotient R -> B.
+    intros [f H'].
+    apply (quotient_rec _ H').
+  Defined.
+
+  Theorem quotient_ump (B:HSet): (quotient R -> B) <~>
+                                                   (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))).
+  Proof.
+    refine (equiv_adjointify (quotient_ump' B) (quotient_ump'' B) _ _).
+    - intros [f Hf].
+      by apply equiv_path_sigma_hprop.
+    - intros f.
+      apply path_forall.
+      red. apply quotient_ind_prop';[apply _|reflexivity].
+  Defined.
+
+  (** Missing
+
+  The equivalence with VVquotient [A//R].
+
+  This should lead to the unnamed theorem:
+
+  10.1.10. Equivalence relations are effective and there is an equivalence [A/R<~>A//R]. *)
+
+  (**
+  The theory of canonical quotients is developed by C.Cohen:
+  http://perso.crans.org/cohen/work/quotients/
+ *)
+
+End Equiv.
+
+Section Functoriality.
+
+  Definition quotient_functor
+             {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
+             {B : Type} (S : Relation B) {sS: is_mere_relation _ S}
+             (f : A -> B) (fresp : forall x y, R x y -> S (f x) (f y))
+  : quotient R -> quotient S.
+  Proof.
+    refine (quotient_rec R (class_of S o f) _).
+    intros x y r.
+    apply related_classes_eq, fresp, r.
+  Defined.
+
+  Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
+          {B : Type} (S : Relation B) {sS: is_mere_relation _ S}.
+
+  Global Instance quotient_functor_isequiv
+             (f : A -> B) (fresp : forall x y, R x y <-> S (f x) (f y))
+             `{IsEquiv _ _ f}
+  : IsEquiv (quotient_functor R S f (fun x y => fst (fresp x y))).
+  Proof.
+    simple refine (isequiv_adjointify _ (quotient_functor S R f^-1 _)
+                               _ _).
+    - intros u v s.
+      apply (snd (fresp _ _)).
+      abstract (do 2 rewrite eisretr; apply s).
+    - intros x; revert x; simple refine (quotient_ind S _ _ _).
+      + intros b; simpl. apply ap, eisretr.
+      + intros; apply path_ishprop.
+    - intros x; revert x; simple refine (quotient_ind R _ _ _).
+      + intros a; simpl. apply ap, eissect.
+      + intros; apply path_ishprop.
+  Defined.
+
+  Definition quotient_functor_equiv
+             (f : A -> B) (fresp : forall x y, R x y <-> S (f x) (f y))
+             `{IsEquiv _ _ f}
+  : quotient R <~> quotient S
+    := Build_Equiv _ _
+         (quotient_functor R S f (fun x y => fst (fresp x y))) _.
+
+  Definition quotient_functor_equiv'
+             (f : A <~> B) (fresp : forall x y, R x y <-> S (f x) (f y))
+  : quotient R <~> quotient S
+    := quotient_functor_equiv f fresp.
+
+End Functoriality.
+
+Section Kernel.
+
+  (** ** Quotients of kernels of maps to sets give a surjection/mono factorization. *)
+
+  Context {fs : Funext}.
+
+  (** A function we want to factor. *)
+  Context {A B : Type} `{IsHSet B} (f : A -> B).
+
+  (** A mere relation equivalent to its kernel. *)
+  Context (R : Relation A) {sR : is_mere_relation _ R}.
+  Context (is_ker : forall x y, f x = f y <~> R x y).
+
+  Theorem quotient_kernel_factor
+  : exists (C : Type) (e : A -> C) (m : C -> B),
+      IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).
+  Proof.
+    pose (C := quotient R).
+    (* We put this explicitly in the context so that typeclass resolution will pick it up. *)
+    assert (IsHSet C) by (unfold C; apply _).
+    exists C.
+    pose (e := class_of R).
+    exists e.
+    transparent assert (m : (C -> B)).
+    { apply quotient_ind with f; try exact _.
+      intros x y H. transitivity (f x).
+      - apply transport_const.
+      - exact ((is_ker x y) ^-1 H). }
+    exists m.
+    split;[split;[split|]|].
+    - assumption.
+    - apply quotient_surjective.
+    - intro u.
+      apply hprop_allpath.
+      assert (H : forall (x y : C) (p : m x = u) (p' : m y = u), x = y).
+      { simple refine (quotient_ind R _ _ _).
+        - intro a.
+          simple refine (quotient_ind R _ _ _).
+          + intros a' p p'; fold e in p, p'.
+            * apply related_classes_eq.
+              refine (is_ker a a' _).
+              change (m (e a) = m (e a')).
+              exact (p @ p'^).
+          + intros; apply path_ishprop.
+        - intros; apply path_ishprop. }
+      intros [x p] [y p'].
+      apply path_sigma_hprop; simpl.
+      exact (H x y p p').
+    - reflexivity.
+  Defined.
+
+End Kernel.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/surjective_factor.v

@@ -0,0 +1,37 @@
+Require Import
+        HoTT.Types
+        HoTT.Basics
+        HoTT.Truncations.Core Modalities.Modality.
+
+(** Definition by factoring through a surjection. *)
+
+Section surjective_factor.
+  Context `{Funext}.
+  Context {A B C} `{IsHSet C} `(f : A -> C) `(g : A -> B) {Esurj : IsSurjection g}.
+  Variable (Eg : forall x y, g x = g y -> f x = f y).
+
+  Lemma ishprop_surjective_factor_aux : forall b, IsHProp (exists c : C, forall a, g a = b -> f a = c).
+  Proof.
+    intros. apply Sigma.ishprop_sigma_disjoint.
+    intros c1 c2 E1 E2.
+    generalize (@center _ (Esurj b)); apply (Trunc_ind _).
+    intros [a p];destruct p.
+    path_via (f a).
+  Qed.
+
+  Definition surjective_factor_aux :=
+    @conn_map_elim
+      _ _ _ _ Esurj (fun b => exists c : C, forall a, g a = b -> f a = c)
+      ishprop_surjective_factor_aux
+      (fun a => exist (fun c => forall a, _ -> _ = c) (f a) (fun a' => Eg a' a)).
+
+  Definition surjective_factor : B -> C
+    := fun b => (surjective_factor_aux b).1.
+
+  Lemma surjective_factor_pr : f == compose surjective_factor g.
+  Proof.
+    intros a.
+    apply (surjective_factor_aux (g a)).2. trivial.
+  Qed.
+
+End surjective_factor.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/HIT/unique_choice.v

@@ -0,0 +1,31 @@
+Require Import HoTT.Basics HoTT.Truncations.Core.
+
+Definition atmost1 X:=(forall x1 x2:X, (x1 = x2)).
+Definition atmost1P {X} (P:X->Type):=
+    (forall x1 x2:X, P x1 -> P x2 -> (x1 = x2)).
+Definition hunique {X} (P:X->Type):=(hexists P) * (atmost1P P).
+
+Lemma atmost {X} {P : X -> Type}:
+  (forall x, IsHProp (P x)) -> (atmost1P P) -> atmost1 (sig  P).
+intros H H0 [x p] [y q].
+specialize (H0 x y p q).
+induction H0.
+assert (H0: (p =q)) by apply path_ishprop.
+now induction H0.
+Qed.
+
+Lemma iota {X} (P:X-> Type):
+  (forall x, IsHProp (P x)) -> (hunique P) -> sig P.
+Proof.
+intros H1 [H H0].
+apply (@Trunc_rec (-1) (sig P) );auto.
+by apply hprop_allpath, atmost.
+Qed.
+
+Lemma unique_choice {X Y} (R:X->Y->Type) :
+ (forall x y, IsHProp (R x y)) -> (forall x, (hunique (R x)))
+   -> {f : X -> Y & forall x, (R x (f x))}.
+intros X0 X1.
+exists (fun x:X => (pr1 (iota _ (X0 x) (X1 x)))).
+intro x. apply (pr2 (iota _ (X0 x) (X1 x))).
+Qed.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pFiber.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:f24569b0e96de2846b8733568c9546aed28b23136c49dfc7e0abf14fbc7c4af2
+size 199966

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Pointed/pMap.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:c1d5a4c5f776b9c8bce55f80839cbe0fa73869130a2c443e987ea1a7f89646a9
+size 391923

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.v

@@ -0,0 +1,445 @@
+(* -*- mode: coq; mode: visual-line -*-  *)
+Require Import HoTT.Basics HoTT.Types.
+Require Import Constant.
+Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness.
+Require Import Spaces.BAut.
+Require Import Pointed.Core.
+
+Local Open Scope trunc_scope.
+Local Open Scope path_scope.
+Local Open Scope pointed_scope.
+
+(** * BAut(Bool) *)
+
+Section AssumeUnivalence.
+  Context `{Univalence}.
+
+  (** ** Nontrivial central homotopy *)
+
+  (** The equivalence [Bool <~> (Bool <~> Bool)], and particularly its consequence [abelian_aut_bool], implies that [BAut Bool] has a nontrivial center.  *)
+
+  Definition negb_center_baut_bool
+  : forall (Z:BAut Bool), Z = Z.
+  Proof.
+    apply center_baut; try exact _.
+    exists equiv_negb.
+    intros g; apply abelian_aut_bool.
+  Defined.
+
+  Definition nontrivial_negb_center_baut_bool
+  : negb_center_baut_bool <> (fun Z => idpath Z).
+  Proof.
+    intros oops.
+    pose (p := ap10_equiv
+                 ((ap (center_baut Bool))^-1
+                  (oops @ (id_center_baut Bool)^))..1 true).
+    exact (false_ne_true p).
+  Defined.
+
+  (** In particular, every element of [BAut Bool] has a canonical flip automorphism.  *)
+  Definition negb_baut_bool (Z : BAut Bool) : Z <~> Z
+    := equiv_path Z Z (negb_center_baut_bool Z)..1.
+
+  Definition negb_baut_bool_ne_idmap (Z : BAut Bool)
+  : negb_baut_bool Z <> equiv_idmap Z.
+  Proof.
+    intros oops.
+    apply nontrivial_negb_center_baut_bool.
+    apply path_forall; intros Z'.
+    pose (p := merely_path_component Z Z').
+    clearbody p. strip_truncations.
+    destruct p.
+    unfold negb_baut_bool in oops.
+    apply moveL_equiv_V in oops.
+    refine (_ @ ap (equiv_path_sigma_hprop _ _)
+                   (oops @ path_universe_1) @ _).
+    - symmetry.
+      refine (eisretr (equiv_path_sigma_hprop Z Z) _).
+    - apply moveR_equiv_M; reflexivity.
+  Defined.
+
+  (** If [Z] is [Bool], then the flip is the usual one. *)
+  Definition negb_baut_bool_bool_negb
+  : negb_baut_bool pt = equiv_negb.
+  Proof.
+    pose (c := aut_bool_idmap_or_negb (negb_baut_bool pt)).
+    destruct c.
+    - pose (negb_baut_bool_ne_idmap pt p).
+      contradiction.
+    - assumption.
+  Defined.
+
+  Definition ap_pr1_negb_baut_bool_bool
+  : (negb_center_baut_bool pt)..1 = path_universe negb.
+  Proof.
+    apply moveL_equiv_V.
+    apply negb_baut_bool_bool_negb.
+  Defined.
+
+  (** Moreover, we can show that every automorphism of a [Z : BAut Bool] must be either the flip or the identity. *)
+  Definition aut_baut_bool_idmap_or_negb (Z : BAut Bool) (e : Z <~> Z)
+  : (e = equiv_idmap Z) + (e = negb_baut_bool Z).
+  Proof.
+    assert (IsHProp ((e = equiv_idmap Z) + (e = negb_baut_bool Z))).
+    { apply ishprop_sum; try exact _.
+      intros p q; exact (negb_baut_bool_ne_idmap Z (q^ @ p)). }
+    baut_reduce.
+    case (aut_bool_idmap_or_negb e).
+    - intros p; exact (inl p).
+    - intros q; apply inr.
+      exact (q @ negb_baut_bool_bool_negb^).
+  Defined.
+
+  (** ** Connectedness *)
+
+  Global Instance isminusoneconnected_baut_bool `{Funext} (Z : BAut Bool)
+  : IsConnected (-1) Z.
+  Proof.
+    baut_reduce.
+    apply contr_inhabited_hprop; try exact _.
+    exact (tr true).
+  Defined.
+
+  Definition merely_inhab_baut_bool `{Funext} (Z : BAut Bool)
+  : merely Z
+    := center (merely Z).
+
+  (** ** Equivalence types *)
+
+  (** As soon as an element of [BAut Bool] is inhabited, it is (purely) equivalent to [Bool].  (Of course, every element of [BAut Bool] is *merely* inhabited, since [Bool] is.)  In fact, it is equivalent in two canonical ways.
+
+First we define the function that will be the equivalence. *)
+  Definition inhab_baut_bool_from_bool (t : Bool)
+             (Z : BAut Bool) (z : Z)
+  : Bool -> Z
+    := fun b => if t then
+                  if b then z else negb_baut_bool Z z
+                else
+                  if b then negb_baut_bool Z z else z.
+
+  (** We compute this in the case when [Z] is [Bool]. *)
+  Definition inhab_baut_bool_from_bool_bool (t : Bool)
+  : inhab_baut_bool_from_bool t pt =
+    fun (z : point (BAut Bool)) (b : Bool) =>
+      if t then
+        if b then z else negb z
+      else
+        if b then negb z else z.
+  Proof.
+    apply path_forall; intros z'; simpl in z'.
+    apply path_forall; intros b.
+    destruct z', b, t; simpl;
+    try reflexivity;
+    try apply (ap10_equiv negb_baut_bool_bool_negb).
+  Defined.
+
+  (** Now we show that it is an equivalence. *)
+  Global Instance isequiv_inhab_baut_bool_from_bool (t : Bool)
+         (Z : BAut Bool) (z : Z)
+  : IsEquiv (inhab_baut_bool_from_bool t Z z).
+  Proof.
+    baut_reduce.
+    refine (transport IsEquiv (ap10 (inhab_baut_bool_from_bool_bool t)^ z) _).
+    simpl in z; destruct z, t; simpl.
+    - refine (isequiv_homotopic idmap _); intros []; reflexivity.
+    - apply isequiv_negb.
+    - apply isequiv_negb.
+    - refine (isequiv_homotopic idmap _); intros []; reflexivity.
+  Defined.
+
+  Definition equiv_inhab_baut_bool_bool (t : Bool)
+             (Z : BAut Bool) (z : Z)
+  : Bool <~> Z
+    := Build_Equiv _ _ (inhab_baut_bool_from_bool t Z z) _.
+
+  Definition path_baut_bool_inhab (Z : BAut Bool) (z : Z)
+  : (point (BAut Bool)) = Z.
+  Proof.
+    apply path_baut.
+    exact (equiv_inhab_baut_bool_bool true Z z). (** [true] is a choice! *)
+  Defined.
+
+  (** In fact, the map sending [z:Z] to this equivalence [Bool <~> Z] is also an equivalence.  To assist with computing the result when [Z] is [Bool], we prove it with an extra parameter first. *)
+  Definition isequiv_equiv_inhab_baut_bool_bool_lemma
+             (t : Bool) (Z : BAut Bool) (m : merely (pt = Z))
+  : IsEquiv (equiv_inhab_baut_bool_bool t Z).
+  Proof.
+    strip_truncations. destruct m.
+    refine (isequiv_adjointify _ (fun (e : Bool <~> Bool) => e t) _ _).
+    + intros e.
+      apply path_equiv.
+      refine (ap10 (inhab_baut_bool_from_bool_bool t) (e t) @ _).
+      apply path_arrow; intros []; destruct t.
+      * reflexivity.
+      * refine (abelian_aut_bool equiv_negb e false).
+      * refine (abelian_aut_bool equiv_negb e true).
+      * reflexivity.
+    + intros z.
+      refine (ap10 (ap10 (inhab_baut_bool_from_bool_bool t) z) t @ _).
+      destruct t; reflexivity.
+  Defined.
+
+  Global Instance isequiv_equiv_inhab_baut_bool_bool
+         (t : Bool) (Z : BAut Bool)
+  : IsEquiv (equiv_inhab_baut_bool_bool t Z).
+  Proof.
+    exact (isequiv_equiv_inhab_baut_bool_bool_lemma t Z
+            (merely_path_component _ _)).
+  Defined.
+
+  (** The names are getting pretty ridiculous; below we suggest a better name for this. *)
+  Definition equiv_equiv_inhab_baut_bool_bool (t : Bool)
+             (Z : BAut Bool)
+  : Z <~> (Bool <~> Z)
+    := Build_Equiv _ _ (equiv_inhab_baut_bool_bool t Z) _.
+
+  (** We compute its inverse in the case of [Bool]. *)
+  Definition equiv_equiv_inhab_baut_bool_bool_bool_inv (t : Bool)
+             (e : Bool <~> Bool)
+  : equiv_inverse (equiv_equiv_inhab_baut_bool_bool t pt) e = e t.
+  Proof.
+    pose (alt := Build_Equiv _ _ (equiv_inhab_baut_bool_bool t pt)
+                   (isequiv_equiv_inhab_baut_bool_bool_lemma
+                      t pt (tr 1))).
+    assert (p : equiv_equiv_inhab_baut_bool_bool t pt = alt).
+    { apply (ap (fun i => Build_Equiv _ _ _ i)).
+      apply (ap (isequiv_equiv_inhab_baut_bool_bool_lemma t pt)).
+      apply path_ishprop. }
+    exact (ap10_equiv (ap equiv_inverse p) e).
+  Defined.
+
+  (** ** Group structure *)
+
+  (** Homotopically, [BAut Bool] is a [K(Z/2,1)].  In particular, it has a (coherent) abelian group structure induced from that of [Z/2].  With our definition of [BAut Bool], we can construct this operation as follows. *)
+
+  Definition baut_bool_pairing : BAut Bool -> BAut Bool -> BAut Bool.
+  Proof.
+    intros Z W.
+    exists (Z <~> W).
+    baut_reduce; simpl.
+    apply tr, symmetry.
+    exact (path_universe equiv_bool_aut_bool).
+  Defined.
+
+  Declare Scope baut_bool_scope.
+  Notation "Z ** W" := (baut_bool_pairing Z W) : baut_bool_scope.
+  Local Open Scope baut_bool_scope.
+
+  (** Now [equiv_equiv_inhab_baut_bool_bool] is revealed as simply the left unit law of this pairing. *)
+  Definition baut_bool_pairing_1Z Z : pt ** Z = Z.
+  Proof.
+    apply path_baut, equiv_inverse, equiv_equiv_inhab_baut_bool_bool.
+    exact true.                   (** This is a choice! *)
+  Defined.
+
+  (** The pairing is obviously symmetric. *)
+  Definition baut_bool_pairing_symm Z W : Z ** W = W ** Z.
+  Proof.
+    apply path_baut, equiv_equiv_inverse.
+  Defined.
+
+  (** Whence we get the right unit law as well. *)
+  Definition baut_bool_pairing_Z1 Z : Z ** pt = Z
+    := baut_bool_pairing_symm Z pt @ baut_bool_pairing_1Z Z.
+
+  (** Every element is its own inverse. *)
+  Definition baut_bool_pairing_ZZ Z : Z ** Z = pt.
+  Proof.
+    apply symmetry, path_baut_bool_inhab.
+    apply equiv_idmap.            (** A choice!  Could be the flip. *)
+  Defined.
+
+  (** Associativity is easiest to think about in terms of "curried 2-variable equivalences".  We start with some auxiliary lemmas. *)
+  Definition baut_bool_pairing_ZZ_Z_symm_part1 {Y Z W}
+             (e : Y ** (Z ** W)) (z : Z)
+  : Y ** W.
+  Proof.
+    simple refine (equiv_adjointify _ _ _ _).
+    + exact (fun y => e y z).
+    + intros w.
+      destruct (path_baut_bool_inhab W w).
+      destruct (path_baut_bool_inhab Z z).
+      (** It might be tempting to just say [e^-1 (equiv_idmap _)] here, but for the rest of the proof to work, we actually need to choose between [idmap] and [negb] based on whether [z] and [w] are equal or not. *)
+      destruct (dec (z=w)).
+      * exact (e^-1 (equiv_idmap _)).
+      * exact (e^-1 equiv_negb).
+    + intros w.
+      destruct (path_baut_bool_inhab W w).
+      destruct (path_baut_bool_inhab Z z).
+      simpl.
+      destruct z,w; simpl; refine (ap10_equiv (eisretr e _) _).
+    + intros y.
+      destruct (path_baut_bool_inhab Y y).
+      destruct (path_baut_bool_inhab Z z).
+      destruct (path_baut_bool_inhab W (e y z)).
+      simpl.
+      case (dec (z = e y z)); intros p; apply moveR_equiv_V;
+      destruct (aut_bool_idmap_or_negb (e y)) as [q|q].
+      * symmetry; assumption.
+      * case (not_fixed_negb z (p @ ap10_equiv q z)^).
+      * case (p (ap10_equiv q z)^).
+      * symmetry; assumption.
+  Defined.
+
+  Definition baut_bool_pairing_ZZ_Z_symm_lemma {Y Z W}
+             (e : Y ** (Z ** W)) (f : Y ** W)
+  : merely Y -> Z.
+  Proof.
+    pose (k := (fun y => (e y)^-1 (f y))).
+    refine (merely_rec_hset k); intros y1 y2.
+    destruct (path_baut_bool_inhab Y y1).
+    destruct (path_baut_bool_inhab W (f y1)).
+    destruct (path_baut_bool_inhab Z (k y1)).
+    destruct (aut_bool_idmap_or_negb f) as [p|p];
+      refine (ap (e y1)^-1 (ap10_equiv p y1) @ _);
+      refine (_ @ (ap (e y2)^-1 (ap10_equiv p y2))^);
+      clear p f k; simpl.
+    + destruct (dec (y1=y2)) as [p|p].
+      { exact (ap (fun y => (e y)^-1 y) p). }
+      destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1];
+        destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2].
+      * case (p ((ap e)^-1 (q1 @ q2^))).
+      * rewrite q1, q2. exact (negb_ne p).
+      * rewrite q1, q2. symmetry. exact (negb_ne (fun r => p r^)).
+      * case (p ((ap e)^-1 (q1 @ q2^))).
+    + destruct (dec (y1=y2)) as [p|p].
+      { exact (ap (fun y => (e y)^-1 (negb y)) p). }
+      destruct (aut_bool_idmap_or_negb (e y1)) as [q1|q1];
+        destruct (aut_bool_idmap_or_negb (e y2)) as [q2|q2].
+      * case (p ((ap e)^-1 (q1 @ q2^))).
+      * rewrite q1, q2.
+        exact (negb_ne (fun r => p ((ap negb)^-1 r))).
+      * rewrite q1, q2. symmetry.
+        exact (negb_ne (fun r => p ((ap negb)^-1 r)^)).
+      * case (p ((ap e)^-1 (q1 @ q2^))).
+  Defined.
+
+  Definition baut_bool_pairing_ZZ_Z_symm_map Y Z W
+  : Y ** (Z ** W) -> Z ** (Y ** W).
+  Proof.
+    intros e.
+    simple refine (equiv_adjointify (baut_bool_pairing_ZZ_Z_symm_part1 e)
+                             _ _ _).
+    - intros f.
+      exact (baut_bool_pairing_ZZ_Z_symm_lemma e f
+               (merely_inhab_baut_bool Y)).
+    - intros f.
+      apply path_equiv, path_arrow; intros y.
+      change ((e y)
+                (baut_bool_pairing_ZZ_Z_symm_lemma e f
+                  (merely_inhab_baut_bool Y)) = f y).
+      refine (ap (e y o baut_bool_pairing_ZZ_Z_symm_lemma e f)
+                 (path_ishprop _ (tr y)) @ _).
+      simpl. apply eisretr.
+    - intros z.
+      assert (IsHSet Z) by exact _.
+      refine (Trunc_rec _ (merely_inhab_baut_bool Y)); intros y.
+      refine (ap (baut_bool_pairing_ZZ_Z_symm_lemma e _)
+                 (path_ishprop _ (tr y)) @ _).
+      simpl. refine (eissect _ _).
+  Defined.
+
+  Definition baut_bool_pairing_ZZ_Z_symm_inv Y Z W
+  : baut_bool_pairing_ZZ_Z_symm_map Y Z W
+    o baut_bool_pairing_ZZ_Z_symm_map Z Y W
+    == idmap.
+  Proof.
+    intros e.
+    apply path_equiv, path_arrow; intros z.
+    apply path_equiv, path_arrow; intros y.
+    reflexivity.
+  Defined.
+
+  Definition baut_bool_pairing_ZZ_Z_symm Y Z W
+  : Y ** (Z ** W) <~> Z ** (Y ** W).
+  Proof.
+    refine (equiv_adjointify
+              (baut_bool_pairing_ZZ_Z_symm_map Y Z W)
+              (baut_bool_pairing_ZZ_Z_symm_map Z Y W)
+              (baut_bool_pairing_ZZ_Z_symm_inv Y Z W)
+              (baut_bool_pairing_ZZ_Z_symm_inv Z Y W)).
+  Defined.
+
+  (** Finally, we can prove associativity. *)
+  Definition baut_bool_pairing_ZZ_Z Z W Y
+  : (Z ** W) ** Y = Z ** (W ** Y).
+  Proof.
+    refine (baut_bool_pairing_symm (Z ** W) Y @ _).
+    refine (_ @ ap (fun X => Z ** X) (baut_bool_pairing_symm Y W)).
+    apply path_baut, baut_bool_pairing_ZZ_Z_symm.
+  Defined.
+
+  (** Since [BAut Bool] is not a set, we ought to have some coherence for these operations too, but we'll leave that for another time. *)
+
+  (** ** Automorphisms of [BAut Bool] *)
+
+  (** Interestingly, like [Bool] itself, [BAut Bool] is equivalent to its own automorphism group. *)
+
+  (** An initial lemma: every automorphism of [BAut Bool] and its inverse are "adjoint" with respect to the pairing. *)
+  Definition aut_baut_bool_moveR_pairing_V
+             (e : BAut Bool <~> BAut Bool) (Z W : BAut Bool)
+  : (e^-1 Z ** W) = (Z ** e W).
+  Proof.
+    apply path_baut; simpl.
+    refine ((equiv_equiv_path _ _) oE _ oE (equiv_equiv_path _ _)^-1).
+    refine (_ oE (@equiv_moveL_equiv_M _ _ e _ W Z) oE _).
+    - apply equiv_inverse, equiv_path_sigma_hprop.
+    - apply equiv_path_sigma_hprop.
+  Defined.
+
+  Definition equiv_baut_bool_aut_baut_bool
+  : BAut Bool <~> (BAut Bool <~> BAut Bool).
+  Proof.
+    simple refine (equiv_adjointify _ _ _ _).
+    - intros Z.
+      refine (equiv_involution (fun W => Z ** W) _).
+      intros W.
+      refine ((baut_bool_pairing_ZZ_Z Z Z W)^ @ _).
+      refine (_ @ baut_bool_pairing_1Z W).
+      apply (ap (fun Y => Y ** W)).
+      apply baut_bool_pairing_ZZ.
+    - intros e.
+      exact (e^-1 pt).
+    - intros e.
+      apply path_equiv, path_arrow; intros Z; simpl.
+      refine (aut_baut_bool_moveR_pairing_V e pt Z @ _).
+      apply baut_bool_pairing_1Z.
+    - intros Z.
+      apply baut_bool_pairing_Z1.
+  Defined.
+
+  (** ** [BAut (BAut Bool)]  *)
+
+  (** Putting all of this together, we can construct a nontrivial 2-central element of [BAut (BAut Bool)]. *)
+
+  Definition center_baut_bool_central
+             (g : BAut Bool <~> BAut Bool) (W : BAut Bool)
+  : ap g (negb_center_baut_bool W) = negb_center_baut_bool (g W).
+  Proof.
+    revert g; equiv_intro equiv_baut_bool_aut_baut_bool Z.
+    simpl.
+    baut_reduce.
+    refine (_ @ apD negb_center_baut_bool (baut_bool_pairing_1Z pt)^).
+    rewrite transport_paths_lr, inv_V.
+    apply moveL_pV.
+    exact (concat_A1p baut_bool_pairing_1Z (negb_center_baut_bool pt)).
+  Qed.
+
+  Definition negb_center2_baut_baut_bool
+  : forall B : BAut (BAut Bool), (idpath B) = (idpath B).
+  Proof.
+    refine (center2_baut (BAut Bool) _).
+    exists negb_center_baut_bool.
+    apply center_baut_bool_central.
+  Defined.
+
+  Definition nontrivial_negb_center_baut_baut_bool
+  : negb_center2_baut_baut_bool <> (fun Z => idpath (idpath Z)).
+  Proof.
+    intros oops.
+    exact (nontrivial_negb_center_baut_bool
+             (((ap (center2_baut (BAut Bool)))^-1
+                (oops @ (id_center2_baut (BAut Bool))^))..1)).
+  Defined.
+
+End AssumeUnivalence.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:c7c607cb704205feab678f03d1834a68d2fa1172391fb4a6dc92859aae452894
+size 774082

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:198b31d1593267436f37848c33810d3ebcce5546564ee533e6116870a6c5db06
+size 218157

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Card.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:e2c14871cc113b0348353e9439588f0b43043538ce26b0fa0ccb4b875538323b
+size 679382

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/No/Addition.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:9266083f75cc26c616b1d2ca86b7152613302544130103a34b7221ce4f4e8bba
+size 1189062

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Spaces/Universe.v

@@ -0,0 +1,217 @@
+(* -*- mode: coq; mode: visual-line -*-  *)
+Require Import Basics Types.
+Require Import HoTT.Truncations.
+Require Import Spaces.BAut Spaces.BAut.Rigid.
+Require Import ExcludedMiddle.
+
+Local Open Scope trunc_scope.
+Local Open Scope path_scope.
+
+(** * The universe *)
+
+(** ** Automorphisms of the universe *)
+
+(** See "Parametricity, automorphisms of the universe, and excluded middle" by Booij, Escardo, Lumsdaine, Shulman. *)
+
+(** If two inequivalent types have equivalent automorphism oo-groups, then assuming LEM we can swap them and leave the rest of the universe untouched. *)
+Section SwapTypes.
+  (** Amusingly, this does not actually require univalence!  But of course, to verify [BAut A <~> BAut B] in any particular example does require univalence. *)
+  Context `{Funext} `{ExcludedMiddle}.
+  Context (A B : Type) (ne : ~(A <~> B)) (e : BAut A <~> BAut B).
+
+  Definition equiv_swap_types : Type <~> Type.
+  Proof.
+    refine (((equiv_decidable_sum (fun X:Type => merely (X=A)))^-1)
+              oE _ oE
+              (equiv_decidable_sum (fun X:Type => merely (X=A)))).
+    refine ((equiv_functor_sum_l
+               (equiv_decidable_sum (fun X => merely (X.1=B)))^-1)
+              oE _ oE
+              (equiv_functor_sum_l
+                 (equiv_decidable_sum (fun X => merely (X.1=B))))).
+    refine ((equiv_sum_assoc _ _ _)
+              oE _ oE
+              (equiv_sum_assoc _ _ _)^-1).
+    apply equiv_functor_sum_r.
+    assert (q : BAut B <~> {x : {x : Type & ~ merely (x = A)} &
+                                merely (x.1 = B)}).
+    { refine (equiv_sigma_assoc _ _ oE _).
+      apply equiv_functor_sigma_id; intros X.
+      apply equiv_iff_hprop.
+      - intros p.
+        refine (fun q => _ ; p).
+        strip_truncations.
+        destruct q.
+        exact (ne (equiv_path X B p)).
+      - exact pr2. }
+    refine (_ oE equiv_sum_symm _ _).
+    apply equiv_functor_sum'.
+    - exact (e^-1 oE q^-1).
+    - exact (q oE e).
+  Defined.
+
+  Definition equiv_swap_types_swaps : merely (equiv_swap_types A = B).
+  Proof.
+    assert (ea := (e (point _)).2). cbn in ea.
+    strip_truncations; apply tr.
+    unfold equiv_swap_types.
+    apply moveR_equiv_V.
+    rewrite (equiv_decidable_sum_l
+               (fun X => merely (X=A)) A (tr 1)).
+    assert (ne' : ~ merely (B=A))
+      by (intros p; strip_truncations; exact (ne (equiv_path A B p^))).
+    rewrite (equiv_decidable_sum_r
+               (fun X => merely (X=A)) B ne').
+    cbn.
+    apply ap, path_sigma_hprop; cbn.
+    exact ea.
+  Defined.
+
+  Definition equiv_swap_types_not_id
+    : equiv_swap_types <> equiv_idmap.
+  Proof.
+    intros p.
+    assert (q := equiv_swap_types_swaps).
+    strip_truncations.
+    apply ne.
+    apply equiv_path.
+    rewrite p in q; exact q.
+  Qed.
+
+End SwapTypes.
+
+(** In particular, we can swap any two distinct rigid types. *)
+
+Definition equiv_swap_rigid `{Univalence} `{ExcludedMiddle}
+           (A B : Type) `{IsRigid A} `{IsRigid B} (ne : ~(A <~> B))
+  : Type <~> Type.
+Proof.
+  refine (equiv_swap_types A B ne _).
+  apply equiv_contr_contr.
+Defined.
+
+(** Such as [Empty] and [Unit]. *)
+
+Definition equiv_swap_empty_unit `{Univalence} `{ExcludedMiddle}
+  : Type <~> Type
+  := equiv_swap_rigid Empty Unit (fun e => e^-1 tt).
+
+(** In this case we get an untruncated witness of the swapping. *)
+
+Definition equiv_swap_rigid_swaps `{Univalence} `{ExcludedMiddle}
+           (A B : Type) `{IsRigid A} `{IsRigid B} (ne : ~(A <~> B))
+  : equiv_swap_rigid A B ne A = B.
+Proof.
+  unfold equiv_swap_rigid, equiv_swap_types.
+  apply moveR_equiv_V.
+  rewrite (equiv_decidable_sum_l
+             (fun X => merely (X=A)) A (tr 1)).
+  assert (ne' : ~ merely (B=A))
+    by (intros p; strip_truncations; exact (ne (equiv_path A B p^))).
+  rewrite (equiv_decidable_sum_r
+             (fun X => merely (X=A)) B ne').
+  cbn.
+  apply ap, path_sigma_hprop; cbn.
+  exact ((path_contr (center (BAut B)) (point (BAut B)))..1).
+Defined.
+
+(** We can also swap the products of two rigid types with another type [X], under a connectedness/truncatedness assumption. *)
+
+Definition equiv_swap_prod_rigid  `{Univalence} `{ExcludedMiddle}
+           (X A B : Type) (n : trunc_index) (ne : ~(X*A <~> X*B))
+           `{IsRigid A} `{IsConnected n.+1 A}
+           `{IsRigid B} `{IsConnected n.+1 B}
+           `{IsTrunc n.+1 X}
+  : Type <~> Type.
+Proof.
+  refine (equiv_swap_types (X*A) (X*B) ne _).
+  transitivity (BAut X).
+  - symmetry; exact (baut_prod_rigid_equiv X A n).
+  - exact (baut_prod_rigid_equiv X B n).
+Defined.
+
+(** Conversely, from some nontrivial automorphisms of the universe we can deduce nonconstructive consequences. *)
+
+Definition lem_from_aut_type_unit_empty `{Univalence}
+           (f : Type <~> Type) (eu : f Unit = Empty)
+  : ExcludedMiddle_type.
+Proof.
+  apply DNE_to_LEM, DNE_from_allneg; intros P ?.
+  exists (f P); split.
+  - intros p.
+    assert (Contr P) by (apply contr_inhabited_hprop; assumption).
+    assert (q : Unit = P)
+      by (apply path_universe_uncurried, equiv_contr_contr).
+    destruct q.
+    rewrite eu.
+    auto.
+  - intros nfp.
+    assert (q : f P = Empty)
+      by (apply path_universe_uncurried, equiv_to_empty, nfp).
+    rewrite <- eu in q.
+    apply ((ap f)^-1) in q.
+    rewrite q; exact tt.
+Defined.
+
+Lemma equiv_hprop_idprod `{Univalence}
+      (A : Type) (P : Type) (a : merely A) `{IsHProp P}
+  : P <-> (P * A = A).
+Proof.
+  split.
+  - intros p; apply path_universe with snd.
+    apply isequiv_adjointify with (fun a => (p,a)).
+    + intros x; reflexivity.
+    + intros [p' x].
+      apply path_prod; [ apply path_ishprop | reflexivity ].
+  - intros q.
+    strip_truncations.
+    apply equiv_path in q.
+    exact (fst (q^-1 a)).
+Defined.
+
+Definition lem_from_aut_type_inhabited_empty `{Univalence}
+           (f : Type <~> Type)
+           (A : Type) (a : merely A) (eu : f A = Empty)
+  : ExcludedMiddle_type.
+Proof.
+  apply DNE_to_LEM, DNE_from_allneg; intros P ?.
+  exists (f (P * A)); split.
+  - intros p.
+    assert (q := fst (equiv_hprop_idprod A P a) p).
+    apply (ap f) in q.
+    rewrite eu in q.
+    rewrite q; auto.
+  - intros q.
+    apply equiv_to_empty in q.
+    apply path_universe_uncurried in q.
+    rewrite <- eu in q.
+    apply ((ap f)^-1) in q.
+    exact (snd (equiv_hprop_idprod A P a) q).
+Defined.
+
+(** If you can derive a constructive taboo from an automorphism of the universe such that [g X <> X], then you get [X]-many beers; see <https://groups.google.com/d/msg/homotopytypetheory/8CV0S2DuOI8/blCo7x-B7aoJ>. *)
+
+Definition zero_beers `{Univalence}
+           (g : Type <~> Type) (ge : g Empty <> Empty)
+  : ~~ExcludedMiddle_type.
+Proof.
+  pose (f := equiv_inverse g).
+  intros nlem.
+  apply ge.
+  apply path_universe_uncurried, equiv_to_empty; intros gz.
+  apply nlem.
+  apply (lem_from_aut_type_inhabited_empty f (g Empty) (tr gz)).
+  unfold f; apply eissect.
+Defined.
+
+Definition lem_beers `{Univalence}
+           (g : Type <~> Type) (ge : g ExcludedMiddle_type <> ExcludedMiddle_type)
+  : ~~ExcludedMiddle_type.
+Proof.
+  intros nlem.
+  pose (nlem' := equiv_to_empty nlem).
+  apply path_universe_uncurried in nlem'.
+  rewrite nlem' in ge.
+  apply (zero_beers g) in ge.
+  exact (ge nlem).
+Defined.

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Paths.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:4eee41d70e1adcab6668f5b03e740ceaf5aa8177e1a05e93ca1d51bac7c672fc
+size 291077

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Prod.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:ea1d9baa225e7f06c2d4edd131b6ba9dc1f73f00e431c23dc622dabb487f024d
+size 238829

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/Types/Sigma.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:60403f0eb098c40babbad07b97512d756594e58e1145fa714adef9b861adb217
+size 264842

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:087c4ac8fcac3bd4ae96e02abba50b82b5f44cfcee2376daf165024133416471
+size 142313

backend/core/Coq-Platform~8.19~2024.10/lib/coq/user-contrib/HoTT/WildCat/Displayed.vo

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:dd585c4f7cdc6e73587d2f4a294edc868e8269531a0621953b8d97a3fffab0f7
+size 285568