Introduction to Agda playground: https://serokell.io/blog/agda-in-nutshell

Intro.agda

module Intro where

-- Types

data Writers : Set where
  Wilde Shelley Byron Sartre Camus : Writers

data Literature : Set where
  DorianGrey Alastor ChildeHarold LaNausée L’Étranger : Literature

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

infixr 100 _∷_

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

[_] : {A : Set} → A → List A
[ x ] = x ∷ []

_++_ : {A : Set} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (succ n)

Vec-length : {n : ℕ} {A : Set} → Vec A n → ℕ
Vec-length {n} v = n

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (succ n)
  succ : {n : ℕ} → Fin n → Fin (succ n)

-- Functions

bookToWriter : Literature → Writers
bookToWriter DorianGrey = Wilde
bookToWriter Alastor = Shelley
bookToWriter ChildeHarold = Byron
bookToWriter LaNausée = Sartre
bookToWriter L’Étranger = Camus

const₁ : (A B : Set) → A → B → A
const₁ A B x y = x

const₂ : {A B : Set} → A → B → A
const₂ x y = x

data Ireland : Set where
  Dublin : Ireland

data England : Set where
  London : England

data France : Set where
  Paris : France

WriterToCountry : Writers → Set
WriterToCountry Wilde = Ireland
WriterToCountry Shelley = England
WriterToCountry Byron = England
WriterToCountry Sartre = France
WriterToCountry Camus = France

WriterToCity : (w : Writers) → WriterToCountry w
WriterToCity Wilde = Dublin
WriterToCity Shelley = London
WriterToCity Byron = London
WriterToCity Sartre = Paris
WriterToCity Camus = Paris

data IsReverse {A : Set} : (xs ys : List A) → Set where
  reverse[] : IsReverse [] []
  reverse∷ : (x : A) (xs ys : List A) → IsReverse xs ys → IsReverse (x ∷ xs) (ys ++ [ x ])

open import Agda.Primitive using (_⊔_)

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ

infixr 4 _,_

theoremReverse₁ : {A : Set} (xs : List A) → Σ (List A) (λ ys → IsReverse xs ys)
theoremReverse₁ [] = [] , reverse[]
theoremReverse₁ (z ∷ zs) =
  let ys = fst (theoremReverse₁ zs) in
  ys ++ [ z ] , reverse∷ z zs ys (snd (theoremReverse₁ zs))

-- Universes

s : {A B C : Set} → (A → B → C) → (A → B) → A → C
s f g x = f x (g x)

open import Agda.Primitive using (Level)

s₁ : {a : Level} → {A B C : Set a} → (A → B → C) → (A → B) → A → C
s₁ f g x = f x (g x)

s₂ : {a b c : Level} → {A : Set a} {B : Set b} {C : Set c} → (A → B → C) → (A → B) → A → C
s₂ f g x = f x (g x)

S : {a b c : Level}
  → {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c}
  → (f : (x : A) → (y : B x) → C x y)
  → (g : (x : A) → B x)
  → (x : A)
  → C x (g x)
S f g x = f x (g x)

-- Records

open import Agda.Builtin.Int using (Int)
open import Agda.Builtin.String using (String)

record Person : Set where
  field
    name : String
    country : String
    age : Int

open import Agda.Primitive using (lsuc)

record Functor {a} (F : Set a → Set a) : Set (lsuc a) where
  field
    map : ∀ {A B} → (A → B) → F A → F B

open Functor

List-map : {A B : Set} → (A → B) → List A → List B
List-map f [] = []
List-map f (x ∷ xs) = f x ∷ List-map f xs

instance
  ListFunctor₁ : Functor List
  ListFunctor₁ = record { map = List-map }

-- Propositional Equality

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  instance refl : x ≡ x

open import Data.Nat using (_+_; _*_; suc)
open import Data.Nat.Properties using (+-assoc)
open import Relation.Binary.PropositionalEquality using (cong; sym)
open import Relation.Binary.PropositionalEquality.Properties

-- *-+-distr : ∀ a b c → (b + c) * a ≡ b * a + c * a
-- *-+-distr a zero c = refl
-- *-+-distr a (suc b) c =
--     begin
--     (suc b + c) * a     ≡⟨ refl ⟩
--     a + (b + c) * a     ≡⟨ cong (_+_ a) (*-+-distr a b c) ⟩
--     a + (b * a + c * a) ≡⟨ sym (+-assoc a (b * a) (c * a)) ⟩
--     suc b * a + c * a
--     ∎
--     where open ≡-Reasoning

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

exFalso : {A : Set} → ⊥ → A
exFalso ()

exContr : {A B : Set} → ¬ A → A → B
exContr f x = exFalso (f x)

_∘_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
f ∘ g = λ x → f (g x)

contraposition : {A B : Set} → (A → B) → (¬ B → ¬ A)
contraposition f g = g ∘ f

¬-intro : {A B : Set} → (A → B) → (A → ¬ B) → ¬ A
¬-intro f g x = g x (f x)

open import Data.Sum using (_⊎_; inj₁; inj₂)

disjImpl : {A B : Set} → ¬ A ⊎ B → A → B
disjImpl (inj₁ x) a = exContr x a
disjImpl (inj₂ y) a = y

postulate
  ¬¬-elim : ∀ {A} → ¬ ¬ A → A

open import Function using (_$_)

lem : ∀ {A} → A ⊎ ¬ A
lem = ¬¬-elim $ λ f → f $ inj₂ $ λ x → f $ inj₁ x

λto⊎ : ∀ {A B} → (A → B) → ¬ A ⊎ B
λto⊎ f = ¬¬-elim λ x → x $ inj₁ λ y → x $ inj₂ $ f y

contraposition' : ∀ {A B} → (¬ A → ¬ B) → B → A
contraposition' f x = ¬¬-elim λ a → f a x

open import Data.Product using (_×_; _,_)

deMorgan₁ : ∀ {A B} → ¬ (A × B) → ¬ A ⊎ ¬ B
deMorgan₁ f = ¬¬-elim λ g → g $ inj₁ $ λ a → g $ inj₂ λ b → f (a , b)

deMorgan₂ : ∀ {A B} → ¬ (A ⊎ B) → ¬ A × ¬ B
deMorgan₂ f = (λ a → f (inj₁ a)) , (λ b → f (inj₂ b))

-- pierce : ∀ {A B} → ((A → B) → A) → A
-- pierce f = {!   !}