bc transport p := transp (λ i → p i) i0 , and transp (λ i → A) i xis actually transp refl i x, which at i := i0 is transp refl i0 x which is transport refl x

the squares seem to be flipped wrt to their description, i.e. horizontal vs vertical

link to fibrations?

"|" used as syntax, read as either a disjunction or fallthrough… interesting

so this is a difference to haskell, bc + is a defined function occurring in a pattern, not a constructor. Also, the pattern is non-linear. Aha, so this point is addressed later on.

this is the way it's done in "How to keep your neighbors in order"

combine the results of recursive invocations on smaller input

making refactoring more difficult

business logic

via the covariant induced Σ_f postcomposition functor

this is only a Widerspruchsbeweis bc Kontraposition has been applied to the proof obligation 🤨

like a functor for products

unless you defined ana/cata using map…

Not necessarily. If you install the emacs package agda2-mode globally (which e.g. allows you to use the agda-input-method globally), but not agda, it will pick up the local agda executable from the path, which you can set as described below. You might still get a mismatch between your globally installed agda-mode and the agda version on your path, but you can execute C-c + C-x + C-s and pass it an empty string. This calls agda2-set-program-version and tells it to use the agda and agda-mode executables from PATH, which have the correct local versions.

the fact that many readers of this blogposts probably encounter it searching for "agda" and "nix" prbly preselects an audience that almost certainly has quite a big interest in this precise combination of tools

that one would seem to make more sense but it causes green slime. Feel like the tradeoffs should be addressed.

this isn't proven correct. We have lkp x t = x \in t, but not x \nin t <=> lkp x t = nothing. Basically it is only a partial decision procedure for ∈

extrinsic verification

Conor also doesn't have this

does this somehow become an implicit argument? It seems so from later uses, but how do generalized variables decide when to generalize implicitly? More importantly, its type was earlier declared to be A, but it should be [ A ]∞ ?? Ok so it appears that the generalized vars can be instantiated to different things – I don't know if at a term- or module level. Ok so if you look at the next line, already they're instantiated to something else. So apparently you can do this even at the clause level. Btw the source code for this blog can be found at https://github.com/jespercockx/agda2scheme/blob/12ff5dcaebfe38dfbfdb48d4fb97bbbe2aa792d9/test/formalize-all-the-things.agda, there doesn't seem to be a lagda file though.

in the original, [_]∞ is a function to Set

why is it in instance brackets in its own definition by copattern matching?

this means we don't have to pattern-match on the case {m = m}, {n = zero}

Ok so yet another redundancy where you can express your decision procedure in a different format…

Could one also write: agda data Maybe : Set where just : A → Maybe A nothing : Maybe A ? For maximum confusion, as it were

this means metaprogramming, unless one says "programs that are proofs", which is just programming.

this is the sense in which the word is used in "to discharge a proof obligation"

silent failure is never good. Often 'the impossible' happens. Do sanity checks, assertions

First time I've seen someone explicitly point out Hypothes.is! I'm currently trying to find a static site generator that will best suit me (I'm planning to make posts about Haskell and Nix in the beginning). I previously looked into https://utteranc.es/ as a comments system, but I do like the hypothes.is feature of comments being tied to particular text.

semantics

again, undefined? though I suppose one would have to pass it @a as type parameter then, to inform ghc

except for undefined - and couldn't one use it if typeOf matches its argument with an _?

Was ist damit gemeint??