Table of Contents

• [[Propositional equality]]
• [[Natural numbers]]
• [[Finite type]]
• [2019-08-12] YOW! Lambda Jam 2019 - Philip Wadler: (Programming Languages) in Agda = Programming (Languages in Agda) /r/functionalprogramming [[towatch]] [[agda]]
• [2018-10-10] Agda Beginner(-ish) Tips, Tricks, & Pitfalls - Donnacha Oisín Kidney [[agda]]
• [[A Few Haskell Highlights: Top Haskell Resources of 2019]] [[agda]]
• [2019-04-21] Cubical Agda and Probability Monads /r/agda [[agda]]
• [2018-11-13] good with explanation https://agda.readthedocs.io/en/latest/language/with-abstraction.html#simultaneous-abstraction pull [[agda]]
• [[https://math.stackexchange.com/a/1307770/15108 prove isomorphism?]] [[tostudy]] [[agda]]
• [[Philip Wadler and Wen Kokke publish book on Programming Language Foundations in Agda]]
• [[Tweet from Denis Moskvin (@deniok), at Apr 12, 17:20]] [[agda]]
• [[Agda stuff]]
  • [2018-11-11] agda/Records.agda at master · agda/agda
  • [2018-11-11] agda/Sigma.agda at master · agda/agda
  • [2018-11-13] Abstract Algebra in Agda
  • [2018-11-13] With-Abstraction — Agda 2.6.0 documentation
• [2019-01-26] agda-ring-solver https://oisdk.github.io/agda-ring-solver/README.html

Propositional equality

data _≡_ {A : Set} : A → A → Set where
  refl : {a : A} → a ≡ a

sym : ∀ {A} {a b : A} → a ≡ b -> b ≡ a
sym refl = refl

Natural numbers

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

Finite type

data Fin : ℕ → Set where
  fzero : (n : ℕ) -> Fin (S n)
  fsucc : (n : ℕ) -> Fin n -> Fin (S n)

onlyone : (x : Fin (S Z)) → x ≡ fzero Z
onlyone (fzero .Z) = refl
onlyone (fsucc .Z ())

[2019-08-12] YOW! Lambda Jam 2019 - Philip Wadler: (Programming Languages) in Agda = Programming (Languages in Agda) /r/functionalprogramming [[towatch]] [[agda]]

[2018-10-10] Agda Beginner(-ish) Tips, Tricks, & Pitfalls - Donnacha Oisín Kidney [[agda]]

https://doisinkidney.com/posts/2018-09-20-agda-tips.html

A Few Haskell Highlights: Top Haskell Resources of 2019 [[agda]]

To get to know Agda better, you can read this introductory post by Danya Rogozin.

[2019-04-21] Cubical Agda and Probability Monads /r/agda [[agda]]

[2018-11-13] good with explanation https://agda.readthedocs.io/en/latest/language/with-abstraction.html#simultaneous-abstraction pull [[agda]]

tldr: write multiple with clauses; then pattern match on them to rewrite and eliminate

https://math.stackexchange.com/a/1307770/15108 prove isomorphism? [[tostudy]] [[agda]]

Philip Wadler and Wen Kokke publish book on Programming Language Foundations in Agda

https://www.reddit.com/r/haskell/comments/a2d3pg/_/eax3ml7?context=1000

Tweet from Denis Moskvin (@deniok), at Apr 12, 17:20 [[agda]]

В Агдочку Prop'ов завезли! https://t.co/1s98uSyGd8

<https://twitter.com/deniok/status/1116737917421064192 pull>

Agda stuff

[2018-11-11] agda/Records.agda at master · agda/agda

https://github.com/agda/agda/blob/master/examples/SummerSchool07/Lecture/Records.agda

[2018-11-11] agda/Sigma.agda at master · agda/agda

https://github.com/agda/agda/blob/master/src/data/lib/prim/Agda/Builtin/Sigma.agda

[2018-11-13] Abstract Algebra in Agda

https://people.inf.elte.hu/pgj/agda/tutorial/Application.Algebra.html

[2018-11-13] With-Abstraction — Agda 2.6.0 documentation

https://agda.readthedocs.io/en/latest/language/with-abstraction.html#simultaneous-abstraction pull

[2019-01-26] agda-ring-solver https://oisdk.github.io/agda-ring-solver/README.html