G. Allais

I see that Peter Dybjer has referenced these notes multiple times. My guess is that your best bet is to email him to ask for a copy. The problem with...

Have you tried emailing Ansten Klev and asking him whether he would be willing to share his notes (& have them uploaded here, ideally)?

[Caveat](https://github.com/pigworker/Bi71/blob/992132e666dda4e2cbb1f053833c4874213780c4/tex/TypesNi.tex#L28): > \section{The 1971 Rules} Let us first see the system which we are about to reorganise. \textbf{Really? Actually, I'm just guessing.} Maybe someone with access to a physical copy...

Good catch. There seems to be two versions of this article: * The one from 2006 in The Computer Journal (cf. the [ACM Digital Library](https://dl.acm.org/citation.cfm?id=1183888)) listed in the bib file...

> In emacs that seems to be the only way to do things Do you know about the command `C-c C-d` to infer the type of an expression?

> m+suc[n]≡suc[m]+n : ∀ m n → m + suc n ≡ suc m + n already exists: `+-suc : ∀ m n → m + suc n ≡ suc...

We do have them in http://agda.github.io/agda-stdlib/Algebra.Construct.NaturalChoice.Min.html http://agda.github.io/agda-stdlib/Algebra.Construct.NaturalChoice.Max.html

In Idris, we have [templates](https://github.com/idris-lang/Idris2/tree/main/tests/templates) for the tests. It may be appropriate to add them here too. The advantage of templates is that we can make them part of the...

> I challenge you to locate this definition in the stdlib. I looked at `Function/`, opened `Function.Definitions` and found that it was re-exporting `Surjective` from `Function.Definitions.Core2`. ```agda Surjective : ∀...

I'd suggest also adding: ```agda induction : ∀ {a b} {A : Set a} (B : (n : ℕ) → Vec A n -> Set b) → (∀ {n} x...