plt-amy / 1lab Goto Github PK

We have cowedges and coends, but no wedges and ends. Relevant modules are Cat.Diagram.Coend and Cat.Diagram.Coend.Formula.

I was defining abelianisations last night and I realised that like 80% of the code I had defined to match on the underlying type of the abelianisation was shared with the code for set quotients. But they're both really easy coequalisers to define

Currently, our definition of cartesian only requires binary products, which is somewhat non-standard. We should probably create a new module Cat.Cartesian that exposes this new definition, along with some helpers (agda-categories would be good to look at here).

This will also require some careful proofreading to ensure that we update any prose in other modules.

I'm writing up the beginnings of a section on topos theory at https://github.com/plt-amy/1lab/tree/feature/topoi (specific definition used: A topos is a lex reflective subcategory of a category of presheaves) and ran into a bunch of results we do not have yet. Tracking them here:

• Monadic adjunctions create limits (more generally, C^M is complete when C is)
• Reflective subcategory inclusions are monadic functors
• Limit respects natural isomorphism (i.e. for F ≅ G, we have Limit F → Limit G)
• Reflective subcategories are exponential ideals when the reflector is lex (Elephant, prop A4.3.1)
• Left adjoints preserve colimits (dualises right adjoints preserve limits, which we already have)
• Slices of presheaf categories are presheaf categories: PSh(C)/F ≅ PSh(∫ F)
• Sliced adjoint functors
• Equivalent characterisations of reflective subcategories: right adjoint is fully faithful ←→ counit is a natural isomorphism
• Colimits in functor categories (dualising limits in functor categories, which we already have)

Was reading this and noticed that ~i0 = i1 is listed twice here; I'm guessing one of them should change to ~i1 = i0?

Knee-deep in the #186 refactor, getting all of the Agda to check would be a nightmare. But I still want to make sure my diagrams, TeX, etc look right!

Would it be possible to have a "mode" (like -w) which builds only the Literate Agda pages, directly from the Markdown source?

Just a really big list of requests for an eventual refactoring of the "bootstrap" code (some parts of 1Lab, some parts of Data).

• Proper separation between the data structures and their properties for:
  • List
  • Bool
  • Fin
• Rescue Vec out from under the Reflection module
• Separate reflection primitives and reflection helpers
• Developer documentation in all the reflection modules
• Idiom-syntax, Do-syntax, Alt-syntax for Maybe
• Move <$> from Idiom-syntax to (e.g.) Map-syntax
• Proper fixities for _>>=, _=<<_
• Map-syntax instance for Arg
• Missing "generic" combinators:
  • Idiom-syntax: <*, *>
  • <$
  • Traverse-syntax (traverse, sequence)
  • Fold-syntax (nondet, choice/asum/msum)
• Combinator to abstract away instance search
• Generic term traversals?
• More convenient List ErrorPart combinators?
  • Wrap TC in a reader-style monad to carry around the logging prefix for the current tactic?

See here or here with 'Equations' unticked.

That's what I'm choosing to call what the nlab refers to as monadicity over Sets.

I don't think we'll need modules over noncommutative rings, so let's stick with modules over CRing (needs #87). The definition should mirror the rest of the algebraic hierarchy so we can invoke the univalent record macro.

TODO:

• R-modules
• R as an R-module
• The category R-Mod

The macro implementation I ported always adds extra braces around macros, to prevent future parsing accidents: e.g. if \a expands to \b, we wouldn't want the first expansion pass to expand \a x into \bx. Unfortunately there's also a problem with spacing. Since KaTeX does layout properly, groups are taken into account. Contrast a {\leftarrow} b vs a \leftarrow b.

I have a fix for this... somewhere, which was changing the generated parser for macros not to consume spaces unless it's scanning for an argument. There's bound to be a better way which isn't "Amy writes a proper reimplementation of TeX".

Right now, we have proofs that conservative functors reflect all limits that they preserve, but using this result is a bit annoying as we have to mediate between concrete (co)limits and their (co)limit diagrams. It would be nice if we did something analogous to Cat.Functor.Adjoint.Continuous and provide results specialized to concrete (co)limits.

This is blocked on #82 and #76.

When doing stuff with integers, it's pretty common to see some really gnarly goals involving nats.
For instance, this monster comes up when you try to define integer multiplication

a * x + b * y + (y + a * y + (x + b * x)) ≡ a * y + b * x + (x + a * x + (y + b * y))

A simple commutative monoid solver would make quick work of this, so it would be a nice-to-have.

Design

The basic idea is to reflect expressions in some monoid into the following data type:

data Expr : Type ℓ where
  ε   : Expr
  _⊗_ : Expr → Expr → Expr
  [_↑] : M → Expr

Then, we can do a sort of NbE style proof where we interpret this into some semantic domain.
In our case, this will be sorted lists. Then, we shall define a sort of "readback" function that
takes a sorted list and reflects it back into Expr.

However, this poses some problems! In particular, we will need a notion of decidable ordering on M, which is no good.
However, we can circumvent this by using an ordering on Term! This requires quite a bit of machinery though, so it is probably best to split the work across several PRs.

Should be a super simple theorem to write up. We already have a characterisation of monos as certain squares being pullbacks.
Bonus points: Rex functors preserve epis, after #90 is done.

The way 1Lab.Data as a namespace is currently structured is very conducive to dependency cycles.

For instance, 1Lab.Data.Sum depends on 1Lab.Data.Nat, the former module needs a proof of commutativity of addition to prove sums are closed under h-levels. This is a problem if you want to use coproducts -- something very fundamental! -- in any module that might be imported from Nat.

Proposed solution: The following modules should all be split into Base/Properties, with the current module serving as a place to hang re-exports off of:

• Nat
• Int
• List
• Sum

Look: ' ′. Let's use the Unicode tick for everything (1433 uses of it vs 355 of the ASCII single quote) to make things less confusing.

Mirror the definition of Ab for CRing, so we get univalence of the category of commutative rings for free.

TODO:

• Define commutative rings
• Write a bit about them
• Data.Int has everything we need to provide a CRing of integers. Just needs to be assembled.

• Finitely-complete
• Cartesian-fibration
• Hom[_,-]

E.g. $\sets$, $\Ab$, &co. aren't really single things

Essentially the same thing as Algebra.Group.Subgroup, but for ring/ideal rather than group/normal subgroup. Snarky wording about subsets and evil wizards is mandatory.

• Images of ring homomorphisms
• Kernels of ring homomorphisms
• "im(f)" satisfies the universal property of "R/ker(f)"
• Ideal
• Quotient by an ideal
• Kernel of the quotient map is the ideal we started with

I've been spending some time looking at what the slow bits are of a clean 1lab build:

While there's some things which are always going to be slow (_^Agda), the obvious issue here is KaTeX. During a fresh build, we're spinning up 1.9k KaTeX processes, each of which runs for a fraction of a second!

It would be worth experimenting with creating some sort of build daemon here; just a basic JS program which reads an equation from stdin and writes the resulting SVG to stdout. Our Shake code can then maintain a pool of these, avoiding the cost of spawning a process for each job.

For quick editing! Only recompiles the changed file(s), no Agda links, no neighbourhood graph, no type-on-hover. Please.

Our Shakefile is 600 lines and it's an affront to God. @SquidDev thoughts?

Getting rid of the Python dependency is good for the soul and good for an 80MiB reduction in Docker image size. @SquidDev thoughts?

It would be nice to have a good API for reasoning about (Co)Limits, much like we have with Cat.Reasoning and Cat.Functor.Reasoning.

We merged the displayed category stuff, but the explanations in this module are still WIP.

We have Lan but no Ran.

TODO:

• Definition of Ran
• Computation of Ran as a particular limit in complete categories

The sidebar disappearing is intentional as a feature, which makes sense since it prevents the main content from getting too squished. However, a side-effect of the current implementation is that there is no way to directly access the sidebar while at higher zooms and more importantly no indication that there even is a sidebar (particularly problematic when a user has default page zoom set above 125%).

A solution to both issues here would be perhaps to introduce some sort of dropdown/popup/something (sorry, not a UI designer). Perhaps a "hamburger menu"-esque thing on the top bar? Or maybe a pullout drawer kind of feature.

Thanks!

As you can see the website isn't completely displayed because it's too large.
Chrome provide horizontal scroll but Firefox don't.

In Cat.Functor.Adjoint.Continuous we show that left adjoints preserve colimits generally, but don't show that they preserve specific colimits (coproducts, coequalisers, etc).

This should be pretty mechanical, and any prospective implementor could look at the limit versions of these proofs right here, so this should make a good beginner issue :)

This is blocked on #78.

Checklist

• Initial Objects
• Coproducts
• Coequalisers
• Pushouts

Dualising the definition of finitely complete categories, the alternative characterisations, and right exact functors.

• Finitely cocomplete categories
• Initial objects + pushouts => coproducts, coequalisers
• Initial objects, coproducts, coequalisers => pushouts
• Left exact functors

Hi all. I am on MacOS 13.2. I cloned this repo into my ~/agda folder and added it to my ~/.agda/libraries file. I am using agda-mode for VSCode with Agda 2.6.3 and am getting this error:

Duplicate binding for built-in thing TYPE, previous binding to
Agda.Primitive.Set
when checking the pragma BUILTIN TYPE Type

when loading in a file with just:

open import 1Lab.Type

and with an agda-lib file in the same folder:

depend: cubical-1lab
include: .

If I downgrade to Agda 2.6.2.2 I get a different error:

Unrecognized option: --no-load-primitives
when scope checking the declaration
  open import 1Lab.Type

It is possible I somehow have some code that conflicts with 1lab from some HoTTest summer school files, but I've removed everything from my ~/.agda/defaults and I am only depending on and importing cubical-1lab in this folder. I am not sure how to debug this issue.

Since some kind of record hierarchy is definitely required for, say, algebra, category theory, topology, and pretty much any other sort of mathematics, the implementation details need some consideration.

Usually, there are at least two separate kinds of records related to a single kind of structure:
One that parameterizes over all the data involved in the structure, e.g.

data isSemigroup (A : Type) (_*_ : A -> A -> A) where
  field is-associative : ...
  ...

which is needed to state that a specific operation does conform to laws required for a structure, as well as another one that parameterizes only over the involved type:

data SemigroupOn (A : Type) where
  field
    _*_ : A -> A -> A
    is-associative : ...
  ...

which is mainly required to avoid clutter in type signatures and allow for more general theorems.

One probably needs both of these types, but which approach should be used primarily?

It does get even more complicated when considering "inheritance"/nested records: given the semigroup definitions above, how exactly would one extend these to monoids? Would MonoidOn A have SemigroupOn A as a field, or would it include the _*_ operator as a field as well as a proof of isMonoid A _*_?

The questions do not stop there - for example, given that it is unique, should the unit of a monoid be included in the type signature of isMonoid? That's why this issue is meant as a place to collect ideas on how to find solutions to all of these topics.

We should augment our call to Pandoc so it also yeets a list of all headings. Then we should add these headings to the search prompt.

When dealing with some displayed category stuff, it's very easy to get owned by a bunch of transports that are stuck on refl. This is really tedious to clean up, so we should automate it!

The most naive solution here is to repeatedly re-traverse the term looking for stuck transports, and then buidling ap calls, but we can probably do better with a single traversal + some sort of zipper structure.

Issue Description

More or less what the title suggests! This should be pretty easy/mindless, so it would be a good beginner issue. See this for what it looks like for a limit diagram.

To do list:

• Coequalisers
• Pushouts
• Coproducts
• Initial objects

Adding a new file while watch mode is running leaves me in a loop of

🔨 src/Cat/Displayed/Cartesian/Indexing.lagda.md has changed. Rebuilding _build/html/Cat.Displayed.Cartesian.Indexing.html.
# agda (for OracleQ (MainCompileQ ()))
Checking Cat.Displayed.Cartesian.Indexing (/home/amelia/default/Projects/1lab.dev/src/Cat/Displayed/Cartesian/Indexing.lagda.md).
Generating HTML for Cat.Displayed.Cartesian.Indexing
❌ Build failed in 1.68s
Error when running Shake build system:
  at need, called at app/Main.hs:276:22 in main:Main
* Depends on: _build/html/Cat.Displayed.Cartesian.Indexing.html
  at copyFile', called at app/Main.hs:95:12 in main:Main
  at need, called at src/Development/Shake/Internal/Derived.hs:92:5 in shake-0.19.6-7wpTzbc7Oxe2G9GkWOH0sV:Development.Shake.Internal.Derived
* Depends on: _build/html0/Cat.Displayed.Cartesian.Indexing.html
  at error, called at src/Development/Shake/Internal/Rules/File.hs:179:58 in shake-0.19.6-7wpTzbc7Oxe2G9GkWOH0sV:Development.Shake.Internal.Rules.File
* Raised the exception:
Error, rule finished running but did not produce file:
  _build/html0/Cat.Displayed.Cartesian.Indexing.html

We have 66 163 pages. Only 2 have a description field:

src/1Lab/Univalence/SIP.lagda.md
src/1Lab/Equiv/Biinv.lagda.md

Example description

Here's a to-do list:

• 1Lab.Counterexamples.IsIso - rendered
• 1Lab.Counterexamples.Russell - rendered
• 1Lab.Counterexamples.Sigma - rendered
• 1Lab.Equiv.Embedding - rendered
• 1Lab.Equiv.Fibrewise - rendered
• 1Lab.Equiv.FromPath - rendered
• 1Lab.Equiv.HalfAdjoint - rendered
• 1Lab.Equiv - rendered
• 1Lab.HIT.S1 - rendered
• 1Lab.HIT.Sinfty - rendered
• 1Lab.HIT.Sphere - rendered
• 1Lab.HIT.Suspension - rendered
• 1Lab.HIT.Torus - rendered
• 1Lab.HIT.Truncation - rendered
• 1Lab.HLevel - rendered
• 1Lab.HLevel.Retracts - rendered
• 1Lab.HLevel.Sets - rendered
• 1Lab.HLevel.Universe - rendered
• 1Lab.intro - rendered
• 1Lab.Path.Groupoid - rendered
• 1Lab.Path - rendered
• 1Lab.Type.Dec - rendered
• 1Lab.Type - rendered
• 1Lab.Type.Pi - rendered
• 1Lab.Type.Prop - rendered
• 1Lab.Type.Sigma - rendered
• 1Lab.Univalence - rendered
• Algebra.Group.Ab.Free - rendered
• Algebra.Group.Ab - rendered
• Algebra.Group.Cat.Base - rendered
• Algebra.Group.Cat.FinitelyComplete - rendered
• Algebra.Group.Cayley - rendered
• Algebra.Group.Free - rendered
• Algebra.Group.Homotopy.BAut - rendered
• Algebra.Group.Homotopy - rendered
• Algebra.Group - rendered
• Algebra.Group.Subgroup - rendered
• Algebra.Lattice - rendered
• Algebra.Magma - rendered
• Algebra.Magma.Unital.EckmannHilton - rendered
• Algebra.Magma.Unital - rendered
• Algebra.Monoid.Category - rendered
• Algebra.Monoid - rendered
• Algebra.Ring.Base - rendered
• Algebra.Semigroup - rendered
• Algebra.Semilattice - rendered
• Authors - rendered
• Cat.Abelian.Base - rendered
• Cat.Abelian.Images - rendered
• Cat.Abelian.Limits - rendered
• Cat.Base - rendered
• Cat.CartesianClosed.Base - rendered
• Cat.CartesianClosed.Locally - rendered
• Cat.Diagram.Coequaliser - rendered
• Cat.Diagram.Coequaliser.RegularEpi - rendered
• Cat.Diagram.Colimit.Base - rendered
• Cat.Diagram.Congruence - rendered
• Cat.Diagram.Coproduct.Indexed - rendered
• Cat.Diagram.Coproduct - rendered
• Cat.Diagram.Duals - rendered
• Cat.Diagram.Equaliser.Kernel - rendered
• Cat.Diagram.Equaliser - rendered
• Cat.Diagram.Equaliser.RegularMono - rendered
• Cat.Diagram.Idempotent - rendered
• Cat.Diagram.Image - rendered
• Cat.Diagram.Initial - rendered
• Cat.Diagram.Limit.Base - rendered
• Cat.Diagram.Limit.Equaliser - rendered
• Cat.Diagram.Limit.Finite - rendered
• Cat.Diagram.Limit.Product - rendered
• Cat.Diagram.Limit.Pullback - rendered
• Cat.Diagram.Monad - rendered
• Cat.Diagram.Monad.Limits - rendered
• Cat.Diagram.Product.Indexed - rendered
• Cat.Diagram.Product - rendered
• Cat.Diagram.Pullback - rendered
• Cat.Diagram.Pullback.Properties - rendered
• Cat.Diagram.Pushout - rendered
• Cat.Diagram.Sieve - rendered
• Cat.Diagram.Terminal - rendered
• Cat.Diagram.Zero - rendered
• Cat.Displayed.Base - rendered
• Cat.Displayed.Cartesian - rendered
• Cat.Displayed.Instances.Family - rendered
• Cat.Displayed.Instances.Slice - rendered
• Cat.Displayed.Total - rendered
• Cat.Functor.Adjoint.Compose - rendered
• Cat.Functor.Adjoint.Continuous - rendered
• Cat.Functor.Adjoint.Hom - rendered
• Cat.Functor.Adjoint - rendered
• Cat.Functor.Adjoint.Monadic - rendered
• Cat.Functor.Adjoint.Monad - rendered
• Cat.Functor.Adjoint.Reflective - rendered
• Cat.Functor.Base - rendered
• Cat.Functor.Bifunctor - rendered
• Cat.Functor.Conservative - rendered
• Cat.Functor.Equivalence.Complete - rendered
• Cat.Functor.Equivalence - rendered
• Cat.Functor.FullSubcategory - rendered
• Cat.Functor.Hom - rendered
• Cat.Functor.Kan - rendered
• Cat.Functor.Kan.Nerve - rendered
• Cat.Functor.Pullback - rendered
• Cat.Functor.Reasoning - rendered
• Cat.Functor.Slice - rendered
• Cat.Instances.Comma - rendered
• Cat.Instances.Comma.Univalent - rendered
• Cat.Instances.Delooping - rendered
• Cat.Instances.Discrete - rendered
• Cat.Instances.Elements - rendered
• Cat.Instances.FinSet - rendered
• Cat.Instances.Functor.Duality - rendered
• Cat.Instances.Functor - rendered
• Cat.Instances.Functor.Limits - rendered
• Cat.Instances.Karoubi - rendered
• Cat.Instances.Lift - rendered
• Cat.Instances.Product - rendered
• Cat.Instances.Sets.CartesianClosed - rendered
• Cat.Instances.Sets.Cocomplete - rendered
• Cat.Instances.Sets.Complete - rendered
• Cat.Instances.Sets.Congruences - rendered
• Cat.Instances.Sets - rendered
• Cat.Instances.Shape.Cospan - rendered
• Cat.Instances.Shape.Interval - rendered
• Cat.Instances.Shape.Join - rendered
• Cat.Instances.Shape.Parallel - rendered
• Cat.Instances.Shape.Terminal - rendered
• Cat.Instances.Slice - rendered
• Cat.Instances.Slice.Presheaf - rendered
• Cat.Instances.StrictCat.Cohesive - rendered
• Cat.Instances.StrictCat - rendered
• Cat.Morphism - rendered
• Cat.Reasoning - rendered
• Cat.Solver - rendered
• Cat.Thin.Completion - rendered
• Cat.Thin.Instances.Sub - rendered
• Cat.Thin - rendered
• Cat.Thin.Limits - rendered
• Cat.Univalent.Instances.Algebra - rendered
• Cat.Univalent - rendered
• Cat.Univalent.Rezk - rendered
• Data.Bool - rendered
• Data.Fin.Base - rendered
• Data.Fin.Closure - rendered
• Data.Fin - rendered
• Data.Fin.Properties - rendered
• Data.Int.Inductive - rendered
• Data.Int - rendered
• Data.List - rendered
• Data.Nat.Base - rendered
• Data.Nat - rendered
• Data.Nat.Properties - rendered
• Data.Power - rendered
• Data.Power.Lattice - rendered
• Data.Set.Coequaliser - rendered
• Data.Set.Truncation - rendered
• Data.Sum - rendered
• index - rendered
• Relation.Order - rendered
• Relation.Order.Lexicographic - rendered
• Topoi.Base - rendered
• Topoi.Classifying.Diaconescu - rendered
• Topoi.Reasoning - rendered

In order to round out our monadicity theorem collection, it would be fun to prove Duskin's Monadicity Theorem. There are a couple of variantions on this, but the following version seems the most elegant:

A conservative right adjoint U: D → C between finitely complete categories is monadic if any congruence in D which has a quotient in C already has a quotient in D, and that quotient that is preserved by U.

Would adding dark mode be valuable enough to justify some extra scss complexity?

I'd be happy to handle it, albeit with no guarantees about whether the alternative color scheme is any good.

Proposal

1. CSS-only solution with prefers-color-scheme and some presumably heavy sass restructuring
2. Add a toggle override and store in localstorage.1lab.dark_mode : 'enabled' | 'disabled'

Usually I have to write a custom CSS that a browser extension lets me inject into web pages. So for example I have a CSS for GitHub that sets serif font as default. For once I am freed from this work!

After #181 landed, we're on Pandoc 3.0, which supports wiki links in the Markdown reader. Wiki links are parsed as normal Link nodes, with a class (I think: please check) of wikilink

We should use wiki links to... link to pages by their titles. Since this will probably require a first pass over the Markdown to collect future link targets, the list of targets should include arbitrary elements with given attributes, e.g. paragraphs. I'm not too sure how that would work, but perhaps a block element with link-target="the description" attribute would (a) get an id if it doesn't have one, (b) be added to the map of link targets?

As the 1Lab grows, we should be mindful of properly citing our sources! For instance, #67 pulls quite a bit from multiple sources, and it would be great if we had a nice way of giving credit. Perhaps @SquidDev has some thoughts?

Currently, primitives like primHComp and postulates like PathP don't have types. This is because they aren't compiled, and so, the HTML backend never gets a chance to look at their types. Can we fix this?

Any idea how to solve this?

docker run -it -v $PWD:/workspace docker.io/pltamy/1lab:latest /bin/bash -i
docker: Error response from daemon: OCI runtime create failed: container_linux.go:380: starting container process caused: exec: "/bin/bash": stat /bin/bash: no such file or directory: unknown.

or equivalently, from scratch:

[giuliohome@localhost ~]$ docker run -it -v $PWD:/workspace docker.io/pltamy/1lab:latest /bin/bash -i
Unable to find image 'pltamy/1lab:latest' locally
latest: Pulling from pltamy/1lab
68d3b63725a1: Pull complete 
9a28b0df1b70: Pull complete 
b8df2d40799e: Pull complete 
222dc704eb55: Pull complete 
c134d319b85f: Pull complete 
e8339d147d0b: Pull complete 
1df22868c217: Pull complete 
71e4e4735fa1: Pull complete 
54e6b3b6dbbc: Pull complete 
0e9d80cf9b9f: Pull complete 
Digest: sha256:18a2acfa30c28d83a580d2fef0ca192beecf71cb021a7859b0de133e5f493853
Status: Downloaded newer image for pltamy/1lab:latest
docker: Error response from daemon: OCI runtime create failed: container_linux.go:380: starting container process caused: exec: "/bin/bash": stat /bin/bash: no such file or directory: unknown.
ERRO[0096] error waiting for container: context canceled 

The proof that conservative functors reflect limits that they preserves is quite short and elegant, but unfortunately this comes at the cost of requiring a subst (See here). This can cause issues later down the line, as the limits we get out of it won't quite line up with the ones we want. Luckily, the direct proof isn't so bad, so we should probably just do that. See #76 for what that might look like.

We know how to solve equations in a ring, and we know how to solve equations in a category. Can we somehow combine them, to solve equations in a ringoid? This would essentially be a way of getting rid of annoying distributivity, associativity, identity and zero goals.

Bonus points if we can somehow make the solver involve the word "polynomialoid".

Right now we have a notion of preservation/reflection of (co)limits that works over limit diagrams, but this is often a bit annoying to work with when we are working with some concrete (co)limit, as it involves dancing between limit diagrams + the concrete definitions. It would be a bit more ergonomic if we had some definitions like Preserves-products or Reflects-coequalisers, as well as a good API for moving between the general + specific forms.