agda-categories: bump version.

Upstream have stopped packaging an Everything file. Because guix strips
the git information from the source, the file has to be created
manually.

In future, this should be converted into a build phase.

2 files changed, 450 insertions, 3 deletions

diff --git a/yellowsquid/packages/agda.scm b/yellowsquid/packages/agda.scm
index 7929818..a3c73d7 100644
--- a/yellowsquid/packages/agda.scm
+++ b/yellowsquid/packages/agda.scm
@@ -129,7 +129,7 @@ normalisation performance.")
 (define-public agda-categories
   (package
     (name "agda-categories")
-    (version "0.1.7.1")
+    (version "0.1.7.1a")
     (home-page "https://github.com/agda/agda-categories")
     (source (origin
               (method git-fetch)
@@ -138,9 +138,11 @@ normalisation performance.")
               (file-name (git-file-name name version))
               (sha256
                (base32
-                "1acb693ad2nrmnn6jxsyrlkc0di3kk2ksj2w9wnyfxrgvfsil7rn"))))
+                "1m96f4a98bs4fhwz5lb03dghf195gi7520jhcbrykyp02l7m2p2n"))
+              (patches
+               (search-patches "agda-categories-everything.patch"))))
     (build-system agda-build-system)
-    (inputs (list agda-stdlib-1.7))
+    (inputs (list agda-stdlib-1.7.1))
     (arguments
      '(#:readme "Everything.agda"))
     (synopsis "Categories library for Agda")
diff --git a/yellowsquid/packages/patches/agda-categories-everything.patch b/yellowsquid/packages/patches/agda-categories-everything.patch
new file mode 100644
index 0000000..e059aee
--- /dev/null
+++ b/yellowsquid/packages/patches/agda-categories-everything.patch
@@ -0,0 +1,445 @@
+diff --git a/Everything.agda b/Everything.agda
+new file mode 100644
+index 00000000..8c679a62
+--- /dev/null
++++ b/Everything.agda
+@@ -0,0 +1,439 @@
++import Categories.2-Category
++import Categories.2-Functor
++import Categories.Adjoint
++import Categories.Adjoint.AFT
++import Categories.Adjoint.AFT.SolutionSet
++import Categories.Adjoint.Alternatives
++import Categories.Adjoint.Compose
++import Categories.Adjoint.Construction.CoEilenbergMoore
++import Categories.Adjoint.Construction.CoKleisli
++import Categories.Adjoint.Construction.EilenbergMoore
++import Categories.Adjoint.Construction.Kleisli
++import Categories.Adjoint.Equivalence
++import Categories.Adjoint.Equivalence.Properties
++import Categories.Adjoint.Equivalents
++import Categories.Adjoint.Instance.0-Truncation
++import Categories.Adjoint.Instance.01-Truncation
++import Categories.Adjoint.Instance.Core
++import Categories.Adjoint.Instance.PathsOf
++import Categories.Adjoint.Instance.PosetCore
++import Categories.Adjoint.Instance.StrictCore
++import Categories.Adjoint.Instance.StrictDiscrete
++import Categories.Adjoint.Mate
++import Categories.Adjoint.Monadic
++import Categories.Adjoint.Monadic.Crude
++import Categories.Adjoint.Monadic.Properties
++import Categories.Adjoint.Properties
++import Categories.Adjoint.RAPL
++import Categories.Adjoint.Relative
++import Categories.Adjoint.TwoSided
++import Categories.Adjoint.TwoSided.Compose
++import Categories.Bicategory
++import Categories.Bicategory.Bigroupoid
++import Categories.Bicategory.Construction.1-Category
++import Categories.Bicategory.Construction.LaxSlice
++import Categories.Bicategory.Construction.Spans
++import Categories.Bicategory.Construction.Spans.Properties
++import Categories.Bicategory.Extras
++import Categories.Bicategory.Instance.Cats
++import Categories.Bicategory.Instance.EnrichedCats
++import Categories.Bicategory.Monad
++import Categories.Bicategory.Monad.Properties
++import Categories.Bicategory.Object.Product
++import Categories.Bicategory.Object.Terminal
++import Categories.Bicategory.Opposite
++import Categories.Category
++import Categories.Category.BicartesianClosed
++import Categories.Category.BinaryProducts
++import Categories.Category.CMonoidEnriched
++import Categories.Category.Cartesian
++import Categories.Category.Cartesian.Bundle
++import Categories.Category.Cartesian.Monoidal
++import Categories.Category.Cartesian.Properties
++import Categories.Category.Cartesian.SymmetricMonoidal
++import Categories.Category.CartesianClosed
++import Categories.Category.CartesianClosed.Bundle
++import Categories.Category.CartesianClosed.Canonical
++import Categories.Category.CartesianClosed.Locally
++import Categories.Category.CartesianClosed.Locally.Properties
++import Categories.Category.CartesianClosed.Properties
++import Categories.Category.Closed
++import Categories.Category.Cocartesian
++import Categories.Category.Cocartesian.Bundle
++import Categories.Category.Cocomplete
++import Categories.Category.Cocomplete.Finitely
++import Categories.Category.Cocomplete.Finitely.Properties
++import Categories.Category.Cocomplete.Properties
++import Categories.Category.Complete
++import Categories.Category.Complete.Finitely
++import Categories.Category.Complete.Finitely.Properties
++import Categories.Category.Complete.Properties
++import Categories.Category.Complete.Properties.Construction
++import Categories.Category.Complete.Properties.SolutionSet
++import Categories.Category.Concrete
++import Categories.Category.Concrete.Properties
++import Categories.Category.Construction.0-Groupoid
++import Categories.Category.Construction.Adjoints
++import Categories.Category.Construction.Arrow
++import Categories.Category.Construction.CoEilenbergMoore
++import Categories.Category.Construction.CoKleisli
++import Categories.Category.Construction.Cocones
++import Categories.Category.Construction.Comma
++import Categories.Category.Construction.Cones
++import Categories.Category.Construction.Coproduct
++import Categories.Category.Construction.Core
++import Categories.Category.Construction.Cowedges
++import Categories.Category.Construction.EilenbergMoore
++import Categories.Category.Construction.Elements
++import Categories.Category.Construction.EnrichedFunctors
++import Categories.Category.Construction.F-Algebras
++import Categories.Category.Construction.Fin
++import Categories.Category.Construction.Functors
++import Categories.Category.Construction.Grothendieck
++import Categories.Category.Construction.GroupAsCategory
++import Categories.Category.Construction.Groups
++import Categories.Category.Construction.KanComplex
++import Categories.Category.Construction.KaroubiEnvelope
++import Categories.Category.Construction.KaroubiEnvelope.Properties
++import Categories.Category.Construction.Kleisli
++import Categories.Category.Construction.LT-Models
++import Categories.Category.Construction.MonoidAsCategory
++import Categories.Category.Construction.MonoidalFunctors
++import Categories.Category.Construction.Monoids
++import Categories.Category.Construction.ObjectRestriction
++import Categories.Category.Construction.Path
++import Categories.Category.Construction.PathCategory
++import Categories.Category.Construction.Presheaves
++import Categories.Category.Construction.Properties.CoEilenbergMoore
++import Categories.Category.Construction.Properties.CoKleisli
++import Categories.Category.Construction.Properties.Comma
++import Categories.Category.Construction.Properties.EilenbergMoore
++import Categories.Category.Construction.Properties.Functors
++import Categories.Category.Construction.Properties.Kleisli
++import Categories.Category.Construction.Properties.Presheaves
++import Categories.Category.Construction.Properties.Presheaves.Cartesian
++import Categories.Category.Construction.Properties.Presheaves.CartesianClosed
++import Categories.Category.Construction.Properties.Presheaves.Complete
++import Categories.Category.Construction.Properties.Presheaves.FromCartesianCCC
++import Categories.Category.Construction.Pullbacks
++import Categories.Category.Construction.SetoidDiscrete
++import Categories.Category.Construction.Spans
++import Categories.Category.Construction.StrictDiscrete
++import Categories.Category.Construction.SymmetricMonoidalFunctors
++import Categories.Category.Construction.Thin
++import Categories.Category.Construction.TwistedArrow
++import Categories.Category.Construction.Wedges
++import Categories.Category.Core
++import Categories.Category.Dagger
++import Categories.Category.Dagger.Construction.Discrete
++import Categories.Category.Dagger.Instance.Rels
++import Categories.Category.Diagram.Span
++import Categories.Category.Discrete
++import Categories.Category.Duality
++import Categories.Category.Equivalence
++import Categories.Category.Equivalence.Preserves
++import Categories.Category.Equivalence.Properties
++import Categories.Category.Exact
++import Categories.Category.Extensive
++import Categories.Category.Finite
++import Categories.Category.Finite.Fin
++import Categories.Category.Finite.Fin.Construction.Discrete
++import Categories.Category.Finite.Fin.Construction.Poset
++import Categories.Category.Finite.Fin.Instance.Parallel
++import Categories.Category.Finite.Fin.Instance.Span
++import Categories.Category.Finite.Fin.Instance.Triangle
++import Categories.Category.Groupoid
++import Categories.Category.Groupoid.Properties
++import Categories.Category.Helper
++import Categories.Category.Indiscrete
++import Categories.Category.Instance.Cartesians
++import Categories.Category.Instance.Cats
++import Categories.Category.Instance.EmptySet
++import Categories.Category.Instance.FamilyOfSetoids
++import Categories.Category.Instance.FinCatShapes
++import Categories.Category.Instance.FinSetoids
++import Categories.Category.Instance.Globe
++import Categories.Category.Instance.Groupoids
++import Categories.Category.Instance.KanComplexes
++import Categories.Category.Instance.LawvereTheories
++import Categories.Category.Instance.Monoidals
++import Categories.Category.Instance.Nat
++import Categories.Category.Instance.One
++import Categories.Category.Instance.PartialFunctions
++import Categories.Category.Instance.PointedSets
++import Categories.Category.Instance.Posets
++import Categories.Category.Instance.Preds
++import Categories.Category.Instance.Properties.Cats
++import Categories.Category.Instance.Properties.Posets
++import Categories.Category.Instance.Properties.Setoids
++import Categories.Category.Instance.Properties.Setoids.CCC
++import Categories.Category.Instance.Properties.Setoids.Choice
++import Categories.Category.Instance.Properties.Setoids.Cocomplete
++import Categories.Category.Instance.Properties.Setoids.Complete
++import Categories.Category.Instance.Properties.Setoids.Exact
++import Categories.Category.Instance.Properties.Setoids.Extensive
++import Categories.Category.Instance.Properties.Setoids.LCCC
++import Categories.Category.Instance.Properties.Setoids.Limits.Canonical
++import Categories.Category.Instance.Quivers
++import Categories.Category.Instance.Rels
++import Categories.Category.Instance.Setoids
++import Categories.Category.Instance.Sets
++import Categories.Category.Instance.Simplex
++import Categories.Category.Instance.SimplicialSet
++import Categories.Category.Instance.SimplicialSet.Properties
++import Categories.Category.Instance.SingletonSet
++import Categories.Category.Instance.Span
++import Categories.Category.Instance.StrictCats
++import Categories.Category.Instance.StrictGroupoids
++import Categories.Category.Instance.Zero
++import Categories.Category.Inverse
++import Categories.Category.Lift
++import Categories.Category.Monoidal
++import Categories.Category.Monoidal.Braided
++import Categories.Category.Monoidal.Braided.Properties
++import Categories.Category.Monoidal.Bundle
++import Categories.Category.Monoidal.Closed
++import Categories.Category.Monoidal.Closed.IsClosed
++import Categories.Category.Monoidal.Closed.IsClosed.Diagonal
++import Categories.Category.Monoidal.Closed.IsClosed.Dinatural
++import Categories.Category.Monoidal.Closed.IsClosed.Identity
++import Categories.Category.Monoidal.Closed.IsClosed.L
++import Categories.Category.Monoidal.Closed.IsClosed.Pentagon
++import Categories.Category.Monoidal.CompactClosed
++import Categories.Category.Monoidal.Construction.Minus2
++import Categories.Category.Monoidal.Construction.Product
++import Categories.Category.Monoidal.Core
++import Categories.Category.Monoidal.Instance.Cats
++import Categories.Category.Monoidal.Instance.One
++import Categories.Category.Monoidal.Instance.Rels
++import Categories.Category.Monoidal.Instance.Setoids
++import Categories.Category.Monoidal.Instance.Sets
++import Categories.Category.Monoidal.Instance.StrictCats
++import Categories.Category.Monoidal.Interchange
++import Categories.Category.Monoidal.Interchange.Braided
++import Categories.Category.Monoidal.Interchange.Symmetric
++import Categories.Category.Monoidal.Properties
++import Categories.Category.Monoidal.Reasoning
++import Categories.Category.Monoidal.Rigid
++import Categories.Category.Monoidal.Star-Autonomous
++import Categories.Category.Monoidal.Symmetric
++import Categories.Category.Monoidal.Traced
++import Categories.Category.Monoidal.Utilities
++import Categories.Category.Product
++import Categories.Category.Product.Properties
++import Categories.Category.Regular
++import Categories.Category.Restriction
++import Categories.Category.Restriction.Construction.Trivial
++import Categories.Category.Restriction.Instance.PartialFunctions
++import Categories.Category.Restriction.Properties
++import Categories.Category.RigCategory
++import Categories.Category.Site
++import Categories.Category.Slice
++import Categories.Category.Slice.Properties
++import Categories.Category.Species
++import Categories.Category.Species.Constructions
++import Categories.Category.SubCategory
++import Categories.Category.Topos
++import Categories.Category.Unbundled
++import Categories.Category.Unbundled.Properties
++import Categories.Category.Unbundled.Utilities
++import Categories.CoYoneda
++import Categories.Comonad
++import Categories.Comonad.Relative
++import Categories.Diagram.Cocone
++import Categories.Diagram.Cocone.Properties
++import Categories.Diagram.Coend
++import Categories.Diagram.Coend.Properties
++import Categories.Diagram.Coequalizer
++import Categories.Diagram.Coequalizer.Properties
++import Categories.Diagram.Colimit
++import Categories.Diagram.Colimit.DualProperties
++import Categories.Diagram.Colimit.Lan
++import Categories.Diagram.Colimit.Properties
++import Categories.Diagram.Cone
++import Categories.Diagram.Cone.Properties
++import Categories.Diagram.Cowedge
++import Categories.Diagram.Cowedge.Properties
++import Categories.Diagram.Duality
++import Categories.Diagram.End
++import Categories.Diagram.End.Properties
++import Categories.Diagram.Equalizer
++import Categories.Diagram.Equalizer.Indexed
++import Categories.Diagram.Equalizer.Limit
++import Categories.Diagram.Equalizer.Properties
++import Categories.Diagram.Finite
++import Categories.Diagram.KernelPair
++import Categories.Diagram.Limit
++import Categories.Diagram.Limit.Properties
++import Categories.Diagram.Limit.Ran
++import Categories.Diagram.Pullback
++import Categories.Diagram.Pullback.Limit
++import Categories.Diagram.Pullback.Properties
++import Categories.Diagram.Pushout
++import Categories.Diagram.Pushout.Properties
++import Categories.Diagram.ReflexivePair
++import Categories.Diagram.SubobjectClassifier
++import Categories.Diagram.Wedge
++import Categories.Diagram.Wedge.Properties
++import Categories.Enriched.Category
++import Categories.Enriched.Category.Opposite
++import Categories.Enriched.Category.Underlying
++import Categories.Enriched.Functor
++import Categories.Enriched.NaturalTransformation
++import Categories.Enriched.NaturalTransformation.NaturalIsomorphism
++import Categories.Enriched.Over.One
++import Categories.Enriched.Over.Setoids
++import Categories.FreeObjects.Free
++import Categories.Functor
++import Categories.Functor.Algebra
++import Categories.Functor.Bifunctor
++import Categories.Functor.Bifunctor.Properties
++import Categories.Functor.Cartesian
++import Categories.Functor.Cartesian.Properties
++import Categories.Functor.CartesianClosed
++import Categories.Functor.Coalgebra
++import Categories.Functor.Construction.Constant
++import Categories.Functor.Construction.Diagonal
++import Categories.Functor.Construction.FromDiscrete
++import Categories.Functor.Construction.LiftSetoids
++import Categories.Functor.Construction.Limit
++import Categories.Functor.Construction.ObjectRestriction
++import Categories.Functor.Construction.PathsOf
++import Categories.Functor.Construction.SubCategory
++import Categories.Functor.Construction.SubCategory.Properties
++import Categories.Functor.Construction.Zero
++import Categories.Functor.Core
++import Categories.Functor.Duality
++import Categories.Functor.Equivalence
++import Categories.Functor.Fibration
++import Categories.Functor.Groupoid
++import Categories.Functor.Hom
++import Categories.Functor.Hom.Properties
++import Categories.Functor.Hom.Properties.Contra
++import Categories.Functor.Hom.Properties.Covariant
++import Categories.Functor.IdentityOnObjects
++import Categories.Functor.Instance.0-Truncation
++import Categories.Functor.Instance.01-Truncation
++import Categories.Functor.Instance.ConnectedComponents
++import Categories.Functor.Instance.Core
++import Categories.Functor.Instance.Discrete
++import Categories.Functor.Instance.SetoidDiscrete
++import Categories.Functor.Instance.StrictCore
++import Categories.Functor.Instance.Twisted
++import Categories.Functor.Instance.UnderlyingQuiver
++import Categories.Functor.Limits
++import Categories.Functor.Monoidal
++import Categories.Functor.Monoidal.Braided
++import Categories.Functor.Monoidal.Construction.Product
++import Categories.Functor.Monoidal.PointwiseTensor
++import Categories.Functor.Monoidal.Properties
++import Categories.Functor.Monoidal.Symmetric
++import Categories.Functor.Monoidal.Tensor
++import Categories.Functor.Power
++import Categories.Functor.Power.Functorial
++import Categories.Functor.Power.NaturalTransformation
++import Categories.Functor.Presheaf
++import Categories.Functor.Profunctor
++import Categories.Functor.Profunctor.Cograph
++import Categories.Functor.Profunctor.FormalComposite
++import Categories.Functor.Properties
++import Categories.Functor.Representable
++import Categories.Functor.Restriction
++import Categories.Functor.Slice
++import Categories.GlobularSet
++import Categories.Kan
++import Categories.Kan.Duality
++import Categories.Minus2-Category
++import Categories.Minus2-Category.Construction.Indiscrete
++import Categories.Minus2-Category.Instance.One
++import Categories.Minus2-Category.Properties
++import Categories.Monad
++import Categories.Monad.Duality
++import Categories.Monad.Idempotent
++import Categories.Monad.Morphism
++import Categories.Monad.Relative
++import Categories.Monad.Strong
++import Categories.Morphism
++import Categories.Morphism.Cartesian
++import Categories.Morphism.Duality
++import Categories.Morphism.Extremal
++import Categories.Morphism.Extremal.Properties
++import Categories.Morphism.HeterogeneousEquality
++import Categories.Morphism.HeterogeneousIdentity
++import Categories.Morphism.HeterogeneousIdentity.Properties
++import Categories.Morphism.Idempotent
++import Categories.Morphism.Idempotent.Bundles
++import Categories.Morphism.IsoEquiv
++import Categories.Morphism.Isomorphism
++import Categories.Morphism.Lifts
++import Categories.Morphism.Lifts.Properties
++import Categories.Morphism.Normal
++import Categories.Morphism.Notation
++import Categories.Morphism.Properties
++import Categories.Morphism.Reasoning
++import Categories.Morphism.Reasoning.Core
++import Categories.Morphism.Reasoning.Iso
++import Categories.Morphism.Regular
++import Categories.Morphism.Regular.Properties
++import Categories.Morphism.Universal
++import Categories.Multi.Category.Indexed
++import Categories.NaturalTransformation
++import Categories.NaturalTransformation.Core
++import Categories.NaturalTransformation.Dinatural
++import Categories.NaturalTransformation.Equivalence
++import Categories.NaturalTransformation.Extranatural
++import Categories.NaturalTransformation.Hom
++import Categories.NaturalTransformation.Monoidal
++import Categories.NaturalTransformation.Monoidal.Braided
++import Categories.NaturalTransformation.Monoidal.Symmetric
++import Categories.NaturalTransformation.NaturalIsomorphism
++import Categories.NaturalTransformation.NaturalIsomorphism.Equivalence
++import Categories.NaturalTransformation.NaturalIsomorphism.Functors
++import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal
++import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Braided
++import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric
++import Categories.NaturalTransformation.NaturalIsomorphism.Properties
++import Categories.NaturalTransformation.Properties
++import Categories.Object.Biproduct
++import Categories.Object.Cokernel
++import Categories.Object.Coproduct
++import Categories.Object.Duality
++import Categories.Object.Exponential
++import Categories.Object.Group
++import Categories.Object.Initial
++import Categories.Object.InternalRelation
++import Categories.Object.Kernel
++import Categories.Object.Kernel.Properties
++import Categories.Object.Monoid
++import Categories.Object.NaturalNumber
++import Categories.Object.NaturalNumber.Properties.F-Algebras
++import Categories.Object.Product
++import Categories.Object.Product.Construction
++import Categories.Object.Product.Core
++import Categories.Object.Product.Indexed
++import Categories.Object.Product.Indexed.Properties
++import Categories.Object.Product.Limit
++import Categories.Object.Product.Morphisms
++import Categories.Object.Subobject
++import Categories.Object.Subobject.Properties
++import Categories.Object.Terminal
++import Categories.Object.Terminal.Limit
++import Categories.Object.Zero
++import Categories.Pseudofunctor
++import Categories.Pseudofunctor.Composition
++import Categories.Pseudofunctor.Hom
++import Categories.Pseudofunctor.Identity
++import Categories.Pseudofunctor.Instance.EnrichedUnderlying
++import Categories.Tactic.Category
++import Categories.Theory.Lawvere
++import Categories.Theory.Lawvere.Instance.Identity
++import Categories.Theory.Lawvere.Instance.Triv
++import Categories.Utils.EqReasoning
++import Categories.Utils.Product
++import Categories.Yoneda
++import Categories.Yoneda.Continuous
++import Categories.Yoneda.Properties
++import Data.Quiver
++import Data.Quiver.Morphism
++import Data.Quiver.Paths
++import Relation.Binary.PropositionalEquality.Subst.Properties