ps/rr/redefine dpath as transport cleanup proofs

[Alizter]

• Suspension: prove that Susp is a 1-functor
• Join: Join Bool <~> Susp
• simplify various proofs
• Spheres: simplify definition of psphere
• Join: add results about Empty and Spheres
• JoinSusp: include the (-1)-spheres in equiv_join_sphere
• Nat/Core: remove redundant iter (same as nat_iter)
• Nat/Core: make nat_iter a notation and clean up proofs
• Join/Core
• Group
• Sets/Powers: use nat_iter; clean up whole file and imports
• Change Join_power -> iterated_join and Join_power' -> join_power
• Fix coqdoc section titles
• STYLE.md: Add instructions on comments
• More coqdoc/comment fixes
• coqdoc: get rid of warnings about << and >>
• dune: pass same(?) coqdoc options as make does
• coqdoc: add --parse-comments
• Update dead link to things generated with [Scheme] should be automatically picked up by [induction] and [elim] coq/coq#3745 from 84247bb
• Spaces.No: Add "Universe i" to reduce universes variables
• Spaces.No: change InSort@{i} to InSort (cosmetic)
• Spaces.No.Core: move No_Empty_for_admitted earlier
• make sure No uses HIT idiom
• github1759: rebase
• github1759: add comment and a second test that shouldn't pass
• github1759.v: add a third test
• Spaces.No.Core: Use the HIT idiom to make this safe
• Spaces.No.Core: get rid of destruct in No_ind_internal
• Spaces.No.Core: speed up the two slowest lines
• Declare universe variables in Context commands
• etc/emacs/run-etags: also index Notation
• Basics/Contractible: simplify logic
• Fix typo in comment
• Join/JoinSusp: add and use bool_pow for join power of Bool
• Basics/Contractible: a few more minor changes
• WildCat/TwoOneCat: make comment no longer a heading
• Functoriality of the triple join and reln to functor_join
• Make NatEquiv's easier to work with
• JoinAssoc: naturality of trijoin_twist and join_assoc
• Reorganize and add 1-functoriality of functor_trijoin
• wildcat: show Universe is a 2-cat
• Yoneda: add faithfulness of Yoneda embedding & missing dual 0gpd results
• Join/Core: prove naturality of unit laws (unitors) & minor cleanups
• Join: prove triangle and hexagon laws
• Don't Export all of Classes.interfaces.abstract_algebra
• canonical_names: use Module to allow just some notations to be exported
• Join: reverse naming of triangle_v/h and triangle_v/h'
• Join: define trijoin_id_sym and prove that it is natural
• HSpace/Core: Export a few more things from canonical_names
• No/Core: add todo saying to remove workaround when Coq 8.19 is required
• Basics/Equivalences: move equiv_ap earlier
• Basics/Equivalences: various clean-ups
• Update theories/Basics/Equivalences.v
• Colimit_Flattening: speed it up a lot
• Colimit_Flattening: reindent; no changes
• Colimit_Flattening: name variables in set and assert tactics
• ReflectiveSubuniverse: workaround no longer needed
• Modalities: add comments about another work around
• ReflectiveSubuniverse: give term instead of using Proof
• WildCat: reduce universe vars from unused Context vars
• Introduce and use a new simple_path_induction tactic
• Modalitities/Localization: clarify why workaround needed
• Basics/Tactics: remove simple_path_induction
• Join.Core: remove unneeded universe annotations
• tests/bugs/github1791: add tests for universe variables
• Typo Fix in Book.py
• Join/Core: allow joinl B a (= joinl (B:=B) a) and joinr A b (= joinr (A:=A) b)
• PathGroupoids: define ap02 using ap
• TwoSphere: fix whitespace and remove unused Generalizable Variables
• Overture: explain creation of internal_paths_rew; remove paths_rect_r
• Overture: move internal_paths_rew to near transport; fix whitespace
• test/bugs/github1794: check internal_paths_rew(_r) universe vars
• Tactics: rewrite_to_transport replaces internal_paths with transport*
• Overture: add TODO about registering transport for rewrite
• 2-cat of pointed types (2-cat of pointed types #1795)
• Add cancelR_equiv_mapinO; change cancelL to cancelR in various places
• Join/Core: add diamond lemmas for paths
• HSpace/Coherent: use pt instead of _
• EMSpace: use IsCoherent; mv K(G
• Tactics
• HSpace/*: lots of updates related to central types/bands paper
• Trunc: more about trunc_index arithmetic
• Connectedness: add isconnected_pred_add'
• Make pelim more robust
• EMSpace: they are 0-connected coherent H-spaces
• Basics/Trunc: get rid of stray universe variables
• Pointed/Core: slightly simplify pelim tactic
• Pointed/Core: get rid of stray universe variable in pHomotopy
• Adjust pmap_(pre/post)whisker in pHomotopy.v
• pHomotopy: remove redundant pmap_postwhisker/prewhisker
• pHomotopy: remove Funext in phomotopy_hcompose
• pFiber: minor clean-up to main definition
• Pointed/Core: remove stray univ var from phomotopy_refl/symm/trans
• ExactSequence: avoid some WildCat notation to improve univ vars
• pHomotopy: rm unneeded results; make ishprop_phomotopy_hset only use Funext
• Pointed/Core: rm unneeded equiv_path_pmap_1; update comments
• Pointed: merge pHomotopy into Core: lots of reordering of things
• Remove three Local Instances that are already Global Instances
• 1-category of successor structures
• pi_n(S^n) = Z
• HomotopyGroup.v: improve pi_prod
• Miscellaneous clean-up
• HomotopyGroup.v: add pequiv_pi_connmap and pequiv_pi_Tr
• Pi1S1: remove unneeded Requires
• Rename Pi1S1.v to PinSn.v
• Remove a few "Require" commands that aren't needed
• CayleyDickson: some cleanups
• review comments
• Add pmap_from_psphere_iterated_loops
• Adjust to renaming of (p)equiv_pequiv_postcompose
• wildcat: binary products
• rename with cat_ and remove superfluous assumptions
• change to representable definition of binary products
• binary coproducts
• binary coproducts in Type
• binary coproducts for pType
• binary coproducts for category of groups
• address review comments
• leave comment about functoriality of products following from symmetry
• test: wildcat opposite being definitionally involuted
• remove old comment from dune file
• test: move Classes/test/ring_tac to tests folder
• use Quotient in ua library
• use Quotient in Ordinals.v
• symmetry and associativity of products
• slicker proof of associativity for products
• trim whitespace
• WIP: Make IsTrunc an inductive type
• Overture: add a Coercion istrunc_fun : IsTrunc >-> Funclass
• Convert more files to Inductive IsTrunc
• Simplify proof of ishprop_istrunc
• Minor changes in response to review
• Make library build with inductive IsTrunc
• Make compatible with Coq 8.17
• HoTTBookExercises: fix universe error in Book_4_6_iii
• Speed up Algebra/Universal/Algebra and Modalities/Fracture a bit
• Homotopy.Hopf: define the Hopf construction; show Prop 2.19 of BCFR
• Homotopy.Hopf: stronger Freudenthal for H-spaces
• Sets/Hartogs: remove two of the three admits
• Sets/Powers: make hset_power have same signature as before
• Sets/Ordinals: remove redundant Instance
• Sets/Hartogs: remove last admit.
• Overture: update comments
• Equivalences: make make_equiv work with Contr
• Move Contr_ind to Contractible
• Reduce universe variables and other clean-ups
• Free up universe in proofs of IsHSet
• Revert "Free up universe in proofs of IsHSet
• Empty.v: Local Set Universe Minimization ToSet
• Basics/Tactics: improve simple_induction
• Spaces.Nat: get rid of lots of universe variables; adjust Classes
• Apply review suggestions
• Truncations/Connectedness: Universe Min ToSet simplifies two results
• HomotopyGroup.v: fix typo
• add prod_0gpd_corec
• Sets/Hartogs: speed it up by a factor of 2
• Sets/Hartogs
• Sets/Hartogs: use 1-4: notation
• Remove some Global Instances
• Supply some implicit variables
• Truncatedness of pointed maps and pForall
• Various cleanups and minor additions
• BlakersMassey: slight speedup
• Pointed/Core: update comments about ppMap and ppForall
• Prove generalization of Licata-Finster theorem
• EMSpace: reverse some equivalences to be in the natural direction
• Basics/Trunc: add some leq lemmas (currently unused)
• ReflectiveSubuniverse: add a couple of things and simplify one proof
• Homotopy/Hopf: improvements based on review
• Colimit_Pushout: speed up slowest line in library
• TorusHomotopy: simpler proof of loops_torus
• Torus: explicitly record the fact that the loops commute
• TorusEquivCircles: remove Section
• TorusEquivCircles: change indentation
• TorusEquivCircles: use nrefine and nrapply when possible
• ReflectiveSubuniverse: cleaner fix for typeclass oddness
• Torus/*: update comments and naming
• all cube concatenations
• Pullback
• make coproduct definition more definitional
• add op graph involutive test
• symmetry and associativity for coproducts
• Update test/WildCat/Opposite.v
• Wedge of a family of pType
• address review comments for wedge
• simplify definition of indexed wedge
• ReflectiveSubuniverse: simplify extendable_to_O'
• Pointed: fix universe vars in istrunc_pforall
• Pointed: other minor updates
• Use snrefine instead of simple notypeclasses refine
• Add "n" (notypeclasses) to some (s)rapply and (s)refine tactics
• Remove `{Univalence} when it isn't needed
• Change {Univalence} to {Funext} when possible
• Remove `{Funext} when not needed
• ReflectiveSubuniverse: remove Univalence and Funext from a Context line
• Add .Core to many Require Import lines
• WhiteheadsPrinciple: import Groups.Group instead of Groups
• etc/coqcreplace.py: a script for trying search & replace on files
• etc/coqcstriprequires.py: minor updates
• Displayed.v: Displayed wild categories
• Add instances for displayed functor composition
• Notation and formatting (DHom
• Attempt to minimize typeclass constraints
• Make A:Type implicit in displayed cat typeclasses
• Add instances for products of displayed categories
• Displayed.v: simplify typeclass arguments
• Displayed.v: use notypeclasses for slight speedup
• Displayed.v: avoid destructing arguments when not needed
• Make families implicit in Is0DFunctor
• Formatting
• Displayed: minor indentation change
• Displayed: remove redundant typeclass assumptions
• WildCat.v: Export Displayed
• Pointed/Core: slightly speed up pelim tactic
• ReflectiveSubuniverse: simplify universe vars in conn_map_homotopic
• Pointed/Core: fix pelim so pEquiv.v builds
• WildCat/Induced: various minor simplifications
• WildCat/Induced: add and use intros_of_type tactic
• Create Utf8Minimal.v for Classes to use
• Colimits/Pushout
• ReflectiveSubuniverse: add inO_retract_inO: RSU closed under retracts
• Projective: use inO_retract_inO and reduce dependencies
• flattening for pushouts
• Hopf fibration total space is a join
• second coherence for flattening proof
• address review comments
• fixup hopf
• new better proof for PushoutFlattening avoiding coh result
• review comments for Hopf
• better proofs in Colimit_Pushout_Flattening
• add comments about the different kinds of pushout and their flattenings
• fix spelling
• reorder contents of Hopf.v
• add Hopf construction to HoTTBook.v
• Colimit_Pushout: clean up and speed up a bit
• Hopf: slight speed up
• wedge projections
• update alectryon
• pinch map of suspension
• address review comments
• fix typo
• diagonal map into binary product
• Makefile.coq.local: reduce long line warnings in alectryon build
• Makefile.coq.local: use --long-line-threshold=99999
• put hor / notation in module
• various improvements to wedge
• remove universe variables in wedge
• functoriality of binary coproducts
• add comment and name hypotheses
• characterize fiber of loop-susp counit
• add comment about path algebra
• add connectivity of loop_susp_counit
• move simpl
• improve connectivity result
• add transport_arrow_toconst'
• speed up proof slightly
• Flattening lemma for GraphQuotient
• add curried version of equiv_sigma_prod
• transport011: transport over 2 1-paths and lemmas about them
• review comments
• GraphQuotient: rephrase comments; tiny adjustments to proofs
• Apply suggestions from code review
• remove rewrite
• remove leftover rewrite
• Apply suggestions from code review
• functoriality of GraphQuotient
• whisker properly
• simplify proofs
• flattening lemma for Coeq
• flattening lemma for Pushout
• make hopf equivalence computable
• delete PushoutFlattening
• simplify hopf fibration total space proof
• Coeq: simplify the path algebra a bit
• Pushout: simplify flattening by using Coeq_rec instead of Pushout_ind
• Colimits/*
• Notations: remove redundant Declare Scope commands
• Cubical: reduce dependencies
• WildCat/Opposite: simplify; remove eta-expansions
• GraphQuotient: add isequiv_functor_gq instance
• Coeq
• Colimit_Sigma: adjust comment
• Add equivalences for displayed wild categories
• Update naming convention for displayed categories
• WildCat/DisplayedEquiv.v: Show total cat univalent
• nix: update flake
• surpress argument-scope-delimiter warning
• test: move Groups.Presentation tests to test/
• [8.18] bump minimal version to Coq 8.18
• [8.18] surpress -uniform-inheritance warning
• [8.18] update opam and nix versions
• add universe constraints in GraphQuotient
• ordinals: small images with prop-resizing
• GraphQuotient: use a Section to simplify the main definition
• Quotient.v
• Improve make_equiv tactic and illustrate in Groups/Group.v
• Adjust/add usage of make_equiv in other places
• Spaces/Int and Pos: minor cleanups
• Spaces/Int/Spec: more things transparent with Defined
• Add instances isconnected_em' and is_minus_one_connected_pointed
• Pointed/Core: get rid of redundant universe variable
• Classes/theory/groups: make group_cancelL transparent and avoid rewrites
• Pointed/pTrunc: really fix typo in comment
• HIT/quotient: fix universe variables
• Generalize quotient_kernel_factor
• Make universe vars in quotient_kernel_factor work with Coq 8.18/8.19
• Ordinals.v: speed it up a bit
• Set/Ordinals: add a comment about universes
• Group is a pointed WildCat
• Pointedness of fmap loops in two contexts
• Pointed/Core: generalize pfmap_loops to any pointed functor
• AbelianGroup.v: condense proof of ispointedcat_abgroup
• WildCat/Core.v: fix is0functor_compose arguments
• redefine DPath as transport + cleanup proofs