Code Snippets Agda

Short texts Agda πŸ§‘β€πŸ’» Code snippets Agda ✍️ Reading lists Agda πŸ‘€

Normalization proof for SK combinator calculus using Agda

{-# OPTIONS –rewriting –type-in-type #-} module sknorm where open import Agda.Primitive open import Relation.Binary.PropositionalEquality {-# BUILTIN REWRITE _≑_ #-} open import Data.Product open import Data.Empty module I where infixr 5 _β‡’_ infixl 5 _$_ postulate Ty : Set Tm : Ty β†’ Set variable A B C : Ty variable t u v : Tm […]

Not Python

data Python : Set where def_β¦…_⦆⦂_ : {A B : Set} β†’ A β†’ B β†’ Python β†’ Python for_inΜ‚_⦂_ : {A B : Set} β†’ A β†’ B β†’ Python β†’ Python if_⦂_ : Python β†’ Python β†’ Python if_⦂_else⦂_ : Python β†’ Python β†’ Python β†’ Python _≕_ : {A B : Set} […]

Axiom Of Choice in DTT

module AOC where open import Agda.Builtin.Sigma open import Relation.Binary.PropositionalEquality using (_≑_;refl) infix 0 _β‰ˆ_ record _β‰ˆ_ (A B : Set) : Set where field to : A β†’ B from : B β†’ A from∘to : βˆ€ (x : A) β†’ from (to x) ≑ x to∘from : βˆ€ (y : B) β†’ to (from […]

The free group in Cubical Agda

{-# OPTIONS –cubical #-} open import Cubical.Foundations.Prelude infix 1 begin_ begin_ : {A : Set} {x y : A} β†’ x ≑ y β†’ x ≑ y begin_ x≑y = x≑y infix 9 _⁻¹ infixl 5 _Β·_ data Group : Set where e : Group _Β·_ : Group β†’ Group β†’ Group _⁻¹ : Group […]

Mokhov is (at least) skew monoidal product, see https://arxiv.org/pdf/1201.4981.pdf

{-# OPTIONS –cubical –type-in-type #-} module Mokhov where open import Cubical.Foundations.Everything open import Cubical.Data.Sum open import Cubical.Data.Prod open import Cubical.Data.Unit record Mokhov (F : Set β†’ Set) (G : Set β†’ Set) (A : Set) : Set where constructor mokhov field X : Set Y : Set h : X β†’ A ⊎ (Y β†’ […]