From 96d4869421082d9e5b029aa64a67cb9f2f4b7b95 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 26 Apr 2023 17:55:46 +0100 Subject: 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. --- yellowsquid/packages/agda.scm | 8 +- .../patches/agda-categories-everything.patch | 445 +++++++++++++++++++++ 2 files changed, 450 insertions(+), 3 deletions(-) create mode 100644 yellowsquid/packages/patches/agda-categories-everything.patch 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 -- cgit v1.2.3