I'm pleased that my paper with @MartinEscardo on (counter)examples of injective types is out on arXiv: https://arxiv.org/abs/2601.12536.

This paper took a while to come together, partly because we refined the exposition a few times, partly because we kept coming up with new (counter)examples, and partly because we formalized (nearly) everything in TypeTopology using Agda. But that's okay, because I'm confident that all of these things led to a better paper.

[Abstract in the next post]

#TypeTheory #Agda

I realise there is a lot of momentum behind Lean for maths proofs.

But I'm also aware of a very established community around Agda.

Can someone explain in plain English - and for a complete beginner like me - what the main benefits of Agda are over Lean?

My own small experience with Lean is not advanced at all, I liked what I tried, but what I didn't like was the arbitrariness of finding tactics for your proof step needs. Does Agda do this better?

To elaborate on that - I found that my ability to write proofs depended very much on my ability to know/find tactics - and they don't seem to be organised in a way that makes finding "what you don't know" easier. And the tactic search engines are still not that easy to get working well (or at all, in my case).

#agda #leanprover #proofassistants

Hey, any #idris or #agda people also see that "simple trick" for carrying around the index equalities necessary for a hetrogenous equality?

EDIT (found it!): https://martinescardo.github.io/dependent-equality-lecture/DependentEquality.html

Like, the equality proof I'm building is something like [not real syntax] (x : RVect n Mine) = (y : RVect (n + 0) Mine).

Trying to pattern-match on the recursive proof directly is a K-axoim violation (IIRC), and in any case it's making the type checker unhappy (for, reasons I am _sure_ are good). Trying to apply cong / depCong to the recursive proofs is a type mismatch.

I think it was "as simple" as having as carrying around the equality proof on indexes (?) and I think the presentation I saw also used mixfix to make the syntax look quite nice.

I might be able to recapitulate it myself, but it would be easier and better to just crib from my betters.

Do dependently typed languages (such as #roq or #agda) tend toward coupling more than languages with (less dependently typed) ml-style typing (such as #haskell or #ocaml)?

Does this bear out as you move down spectrum toward less typing?

my real #Agda learning will start with Programming Language Foundations in Agda: https://plfa.github.io/ :blobcat_meltthumbsup:

in 2026 I'll be doing more #Haskell, #Agda, and #SPARK.

got my Haskell and Agda dev environment setup in #FreeBSD, but Ada/SPARK is like pulling teeth, as usual.

To be more specific:

- It's weird to me that when we want to do a proof by induction, we never say so explicitly

- I really don't get what these chained equality things are doing. It's not clear to me what's supposed to be a rewrite rule and what's supposed to just be the same thing repeated

- I don't understand how rewrite rules apply, in that I don't know how to target just one side of an equation, or know what "direction" they're going to run in

I'm wondering if I should work through Certainty by Construction before continuing with PLFA, in the hopes that it will give me a better mental model for how Agda actually works?

#agda

I'm a few chapters into "Programming Language Foundations in Agda" and... I'm still struggling to figure out how to write proofs in it, more than I did when learning Rocq or Isabelle or Lean. Granted, I have been very tired for months, but I'm wondering if it's more than that.

Is Agda somehow trickier to write proofs in? Does PLFA introduce techniques in a way that doesn't match what people do in practice? Do I just have a skill issue here?

#Agda

Readings shared December 29, 2025. https://jaalonso.github.io/vestigium/posts/2025/12/30-readings_shared_12-29-25 #AI #Agda #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #OCaml #Rocq #SMT

NAMOR: a new Agda library for modal extended sequents. ~ Riccardo Borsetto, Margherita Zorzi. https://ceur-ws.org/Vol-4142/paper4.pdf #ITP #Agda

Algebraizing higher-order effects. ~ Martin Andrieux, Alan Schmitt. https://hal.science/hal-05428166/document#page=35 #ITP #Agda

Doing some Agda coding while on the train home. I knew I liked Haskell, but damn, this is even cooler (but also kind of confusing still).

#agda

New pre-print out: "Types, equations, dimensions and the Pi theorem".

We formalized the covariance principle (physical laws must be independent of units) as a homomorphism between the algebra of physical quantities and real numbers.

While the Pi Theorem from Dimensional Analysis (DA) is non-constructive, we introduce a constructive method for applying it. This could enable DA-driven program derivation where the type checker helps identify valid physical laws.

📝 Blog: https://patrikja.owlstown.net/posts/4887
📄 Paper: https://arxiv.org/abs/2308.09481
💻 Repo: https://gitlab.pik-potsdam.de/botta/papers/-/tree/master/2023.Types,%20equations,%20dimensions%20and%20the%20Pi%20theorem

#Idris #Agda #TypeTheory #Math #Physics

Readings shared November 23, 2025. https://jaalonso.github.io/vestigium/posts/2025/11/24-readings_shared_11-23-25 #AI #Agda #AlphaProof #FunctionalProgramming #ITP #IsabelleHOL #LLMs #LeanProver #Math #OCaml #Rocq