.gitignore

@@ -305,4 +305,3 @@ TSWLatexianTemp*
 *.agdai
 MAlonzo/**
 
-*.html

agda/Makefile

@@ -1,25 +0,0 @@
-.PHONY: all clean
-
-all: agda
-	make pandoc
-
-open:
-	firefox ./public/algebra.html
-
-agda: Everything.agda
-	agda --html --html-dir=public algebra.lagda.md --html-highlight=auto -i.
-	rm -f public/Agda.css
-	cp Agda.css public/Agda.css
-
-pandoc: public/*.md
-	@$(foreach file,$^, \
-		pandoc $(file) -s --to=html+TEX_MATH_DOLLARS --mathjax -c Agda.css -o $(file:.md=.html) ; \
-	)
-
-clean:
-	rm -f  Everything.agda
-	rm -rf public/*
-	find . -name '*.agdai' -exec rm \{\} \;
-
-Everything.agda:
-	git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda

agda/algebra.lagda.md

@@ -1,486 +0,0 @@
-```agda
-open import equality
-module algebra where
-```
-
-# Algebra of programming
-
-## Preliminaries (Types, Lemmas, Functions)
-
-```agda
-  id : ∀ {A : Set} → A → A
-  id a = a
-
-  _! : ∀ {A B : Set} → (b : B) → A → B
-  (b !) _ = b
-```
-
-We will need functional extensionality
-
-```agda
-  postulate
-    extensionality : ∀ {A B : Set} (f g : A → B) → (∀ (x : A) → f x ≡ g x) → f ≡ g
-  
-  ext-rev : ∀ {A B : Set} {f g : A → B} → f ≡ g → (∀ (x : A) → f x ≡ g x)
-  ext-rev {A} {B} {f} {g} refl x = refl
-```
-
-Function composition and some facts about it
-
-```agda
-  infixr 9 _∘_
-  _∘_ : ∀ {A B C : Set} (g : B → C) (f : A → B) → A → C
-  (g ∘ f) x = g (f x)
-  {-# INLINE _∘_ #-}
-
-  identityʳ : ∀ {A B : Set} {f : A → B} → f ∘ id ≡ f
-  identityʳ {f} = refl
-
-  identityˡ : ∀ {A B : Set} {f : A → B} → id ∘ f ≡ f
-  identityˡ {f} = refl
-
-  _⟩∘⟨_ : ∀ {A B C : Set} {g i : B → C} {f h : A → B} → g ≡ i → f ≡ h → g ∘ f ≡ i ∘ h
-  refl ⟩∘⟨ refl = refl
-
-  introˡ : ∀ {A B : Set} {f : A → B} {h : B → B} → h ≡ id → f ≡ h ∘ f
-  introˡ {f} {h} eq = trans (sym identityˡ) (sym eq ⟩∘⟨ refl)
-
-  introʳ : ∀ {A B : Set} {f : A → B} {h : A → A} → h ≡ id → f ≡ f ∘ h
-  introʳ {f} {h} eq = trans (sym identityʳ) (refl ⟩∘⟨ sym eq)
-```
-
-## Unit and void type
-
-```agda
-  data ⊤ : Set where
-    unit : ⊤
-
-  data ⊥ : Set where
-
-  ¡ : ∀ {B : Set} → ⊥ → B
-  ¡ ()
-
-  ¡-unique : ∀ {B : Set} → (f : ⊥ → B) → f ≡ ¡
-  ¡-unique f = extensionality f ¡ (λ ())
-```
-
-## Products
-
-```agda
-  infixr 8 _×_
-  infixr 7 _×₁_
-  record _×_ (A B : Set) : Set where
-    constructor _,_
-    field
-      outl : A
-      outr : B
-  open _×_
-
-  ×-cong : ∀ {A B : Set} {x y : A} {u v : B} → x ≡ y → u ≡ v → (x , u) ≡ (y , v)
-  ×-cong refl refl = refl    
-
-  ⟨_,_⟩ : {A B C : Set} → (A → B) → (A → C) → A → B × C
-  ⟨ f , g ⟩ x = (f x) , (g x)
-  project₁ : ∀ {A B C : Set} (f : A → B) (g : A → C) → outl ∘ ⟨ f , g ⟩ ≡ f
-  project₁ _ _ = refl 
-  project₂ : ∀ {A B C : Set} (f : A → B) (g : A → C) → outr ∘ ⟨ f , g ⟩ ≡ g
-  project₂ _ _ = refl 
-
-  ⟨⟩-cong : {A B C : Set} → (f g : A → B) → (h i : A → C) → f ≡ g → h ≡ i → ⟨ f , h ⟩ ≡ ⟨ g , i ⟩
-  ⟨⟩-cong f g h i refl refl = refl
-
-  ⟨⟩-unique : ∀ {A B C : Set} (f : A → B) (g : A → C) (h : A → B × C) → outl ∘ h ≡ f → outr ∘ h ≡ g → h ≡ ⟨ f , g ⟩
-  ⟨⟩-unique f g h refl refl = refl
-
-  _×₁_ : ∀ {A B C D : Set} (f : A → C) (g : B → D) → A × B → C × D
-  _×₁_ f g (x , y) = f x , g y
-```
-
-Composition as function on products
-
-```agda
-  comp : ∀ {A B C : Set} → ((A → B) × (B → C)) → A → C
-  comp (f , g) x = g (f x)
-```
-
-curry, uncurry, eval
-
-```agda
-  curry : ∀ {A B C : Set} → (A × B → C) → (A → B → C)
-  curry f a b = f (a , b)
-
-  uncurry : ∀ {A B C : Set} → (A → B → C) → (A × B → C)
-  uncurry f (a , b) = f a b
-
-  ev : ∀ {A B : Set} → (A → B) × A → B
-  ev (f , a) = f a
-```
-
-**HOMEWORK 1**
-
-```agda
-  curry-uncurry : ∀ {A B C : Set} → curry ∘ uncurry {A} {B} {C} ≡ id
-  curry-uncurry = extensionality (curry ∘ uncurry) id λ _ → refl
-
-  uncurry-curry : ∀ {A B C : Set} → uncurry ∘ curry {A} {B} {C} ≡ id
-  uncurry-curry = extensionality (uncurry ∘ curry) id λ _ → refl
-```
-
-## Naturals
-
-```agda
-  data ℕ : Set where
-    zero : ℕ
-    succ : ℕ → ℕ
-  {-# BUILTIN NATURAL ℕ #-}
-
-  data 𝔹 : Set where
-    true : 𝔹
-    false : 𝔹
-  {-# BUILTIN BOOL 𝔹 #-}
-  
-  succ-inj : ∀ {x y : ℕ} → succ x ≡ succ y → x ≡ y
-  succ-inj refl = refl
-
-  -- todo rewrite foldn to use ugly cartesian product...
-  foldn : ∀ {C : Set} → (C × (C → C)) → ℕ → C
-  foldn (c , h) zero = c
-  foldn (c , h) (succ n) = h (foldn (c , h) n)
-
-  foldn-id : foldn (zero , succ) ≡ id {ℕ}
-  foldn-id = extensionality (foldn (zero , succ)) id helper
-    where
-      helper : (x : ℕ) → foldn (zero , succ) x ≡ id x
-      helper zero = refl
-      helper (succ n) rewrite helper n = refl
-
-  foldn-fusion : ∀ {C C' : Set} (c : C) (h : C → C) (k : C → C') (c' : C') (h' : C' → C') → k c ≡ c' → k ∘ h ≡ h' ∘ k → k ∘ foldn (c , h) ≡ foldn (c' , h')
-  foldn-fusion {C} {C'} c h k c' h' refl eq = extensionality (k ∘ foldn (c , h)) (foldn (k c , h')) helper
-    where
-      helper : (x : ℕ) → (k ∘ foldn (c , h)) x ≡ foldn (k c , h') x
-      helper zero = refl
-      helper (succ x) = begin 
-        (k ∘ h) (foldn (c , h) x)  ≡⟨ ext-rev eq (foldn (c , h) x) ⟩ 
-        (h' ∘ k) (foldn (c , h) x) ≡⟨ cong h' (helper x) ⟩
-        h' (foldn (k c , h') x)  ∎
-```
-
-### proving with the fusion law
-
-```agda
-  add : ℕ → ℕ → ℕ
-  add zero n = n
-  add (succ m) n = succ (add m n)
-
-  plus : ℕ → ℕ → ℕ
-  plus n = foldn (n , succ)
-  plus' : ℕ → ℕ → ℕ
-  plus' = foldn (id , (comp ∘ ⟨ id , succ ! ⟩))
-  plus-test1 : plus 13 19 ≡ 32
-  plus-test1 = refl
-  
-  + : ℕ × ℕ → ℕ
-  + = uncurry (foldn (id , (comp ∘ ⟨ id , succ ! ⟩)))
-  +-test1 : + (3 , 5) ≡ 8
-  +-test1 = refl
-  +-test2 : + (0 , 100) ≡ 100
-  +-test2 = refl
-  +-test3 : + (100 , 0) ≡ 100
-  +-test3 = refl
-  
-  +0 : ∀ (n : ℕ) → + (n , 0) ≡ n
-  +0 zero = refl
-  +0 (succ n) rewrite +0 n = refl
-
-  -- TODO define with fusion la
-  plus-succˡ : ∀ {m n : ℕ} → succ (plus m n) ≡ plus (succ m) n
-  plus-succˡ {m} {zero} = refl
-  plus-succˡ {m} {succ n} rewrite plus-succˡ {m} {n} = refl
-  plus-comm : ∀ {m n : ℕ} → plus m n ≡ plus n m
-  plus-comm {zero} {n} = ext-rev foldn-id n
-  plus-comm {succ m} {n} rewrite plus-comm {n} {m} = sym (plus-succˡ {m} {n})
-
-  plus-comm' : ∀ {m n : ℕ} → (plus m) ∘ (plus n) ≡ (plus n) ∘ (plus m)
-  plus-comm' {m} {n} = begin 
-    (plus m) ∘ (foldn (n , succ)) ≡⟨ commute₁ ⟩ 
-    foldn ((plus m n) , succ)     ≡⟨ extensionality (foldn ((plus m n) , succ)) (foldn ((plus n m) , succ)) helper ⟩
-    foldn ((plus n m) , succ)     ≡⟨ sym commute₂ ⟩
-    (plus n) ∘ (foldn (m , succ)) ∎
-    where
-      helper : (x : ℕ) → foldn ((plus m n) , succ) x ≡ foldn ((plus n m) , succ) x
-      helper x rewrite plus-comm {m} {n} = refl
-      commute₁ = foldn-fusion n succ (plus m) (plus m n) succ refl refl
-      commute₂ = foldn-fusion m succ (plus n) (plus n m) succ refl refl
-```
-
-**HOMEWORK 2**
-
-```agda
-  mul : ℕ → ℕ → ℕ
-  mul zero n = zero
-  mul (succ m) n = plus n (mul m n)
-  mul-test1 : mul 0 3 ≡ 0
-  mul-test1 = refl
-  mul-test2 : mul 3 15 ≡ 45
-  mul-test2 = refl
-
-  mult : (m : ℕ) → ℕ → ℕ
-  mult m = foldn (zero , (plus m))
-
-  times : (ℕ × ℕ) → ℕ
-  times = uncurry times'
-    where
-      times' : ℕ → ℕ → ℕ
-      times' = foldn ((zero !) , (comp ∘ ⟨ curry ⟨ outr , ev ⟩ , + ! ⟩))
-  times-test1 : times (1 , 1) ≡ 1
-  times-test1 = refl
-  times-test2 : times (123 , 15) ≡ 1845
-  times-test2 = refl
-  times-test3 : times (5 , 0) ≡ 0
-  times-test3 = refl
-```
-
-**HOMEWORK 3**
-
-```agda
-  fac2 : ℕ → ℕ
-  fac2 zero = 1
-  fac2 (succ n) = times (n , fac2 n)
-
-  fac : ℕ → ℕ
-  fac = outr ∘ fac'
-    where
-      fac' : ℕ → (ℕ × ℕ)
-      fac' = foldn ((zero , succ zero) , ⟨ succ ∘ outl , times ∘ (succ ×₁ id) ⟩)
-  fac-test1 : fac 5 ≡ 120
-  fac-test1 = refl
-  fac-test2 : fac 0 ≡ 1
-  fac-test2 = refl
-```
-
-Proofs from the script
-
-```agda
-  distrib : ∀ (m n x : ℕ) → mult m (plus n x) ≡ plus (mult m n) (mult m x)
-  distrib m n x = begin 
-    mult m (plus n x)                       ≡⟨ refl ⟩ 
-    mult m (foldn (n , succ) x)                 ≡⟨ ext-rev commute₁ x ⟩ 
-    foldn ((mult m n) , (plus m)) x             ≡⟨ sym (ext-rev commute₂ x) ⟩ 
-    plus (mult m n) (foldn (zero , (plus m)) x) ≡⟨ refl ⟩ 
-    plus (mult m n) (mult m x)              ∎
-    where
-      commute₁ : (mult m) ∘ (foldn (n , succ)) ≡ foldn ((mult m n) , (plus m))
-      commute₁ = foldn-fusion n succ (mult m) (mult m n) (plus m) kc kh
-        where
-          kc : mult m n ≡ mult m n
-          kc = refl
-          kh : mult m ∘ succ ≡ plus m ∘ mult m
-          kh = refl
-      commute₂ : (plus (mult m n)) ∘ (foldn (zero , (plus m))) ≡ foldn ((mult m n) , (plus m))
-      commute₂ = foldn-fusion zero (plus m) (plus (mult m n)) (mult m n) (plus m) kc (kh m n)
-        where
-          kc : plus (mult m n) zero ≡ mult m n
-          kc = refl
-          kh : ∀ (m n : ℕ) → (plus (mult m n)) ∘ (plus m) ≡ (plus m) ∘ (plus (mult m n))
-          kh zero zero = refl
-          kh (succ m) zero = plus-comm'
-          kh m (succ n) = plus-comm'
-
-  induction : ∀ (p : ℕ → 𝔹) → p zero ≡ true → (∀ (n : ℕ) → p (succ n) ≡ p n) → p ≡ true !
-  induction p IS IH = begin 
-    p                          ≡⟨ introʳ foldn-id ⟩ 
-    p ∘ foldn (zero , succ)        ≡⟨ commute₁ ⟩ 
-    foldn (true , id)              ≡⟨ sym commute₂ ⟩ 
-    (true !) ∘ foldn (zero , succ) ≡⟨ identityʳ ⟩
-    true !                     ∎
-    where
-      commute₁ = foldn-fusion zero succ p true id IS (extensionality (p ∘ succ) p IH)
-      commute₂ = foldn-fusion zero succ (true !) true id refl refl
-```
-
-## Lists
-
-```agda
-  data 𝕃 (A : Set) : Set where
-    nil : 𝕃 A
-    cons : (A × 𝕃 A) → 𝕃 A
-
-  foldr : ∀ {A C : Set} → (C × (A × C → C)) → 𝕃 A → C
-  foldr (c , h) nil = c
-  foldr (c , h) (cons (x , xs)) = h (x , foldr (c , h) xs)
-
-  foldr-id : ∀ {A : Set} → foldr (nil , cons) ≡ id {𝕃 A}
-  foldr-id {A} = extensionality (foldr (nil , cons)) id helper
-    where
-      helper : ∀ (x : 𝕃 A) → foldr (nil , cons) x ≡ id x
-      helper nil = refl
-      helper (cons (x , xs)) rewrite helper xs = refl
-
-  foldr-fusion : ∀ {A B B' : Set} (c : B) (h : A × B → B) (k : B → B') (c' : B') (h' : A × B' → B') 
-    → k c ≡ c'
-    → k ∘ h ≡ h' ∘ (id ×₁ k)
-    → k ∘ foldr (c , h) ≡ foldr (c' , h')
-  foldr-fusion {A} c h k c' h' kc kh = extensionality (k ∘ foldr (c , h)) (foldr (c' , h')) helper
-    where
-      helper : ∀ (x : 𝕃 A) → k (foldr (c , h) x) ≡ foldr (c' , h') x
-      helper nil = kc
-      helper (cons (x , xs)) rewrite ext-rev kh (x , foldr (c , h) xs) | helper xs = refl
-
-  length : ∀ {A : Set} → 𝕃 A → ℕ
-  length {A} = foldr (zero , h)
-    where
-      h : A × ℕ → ℕ
-      h = succ ∘ outr
-
-  isempty? : ∀ {A : Set} → 𝕃 A → 𝔹
-  isempty? = foldr (true , (false !))
-
-  cat : ∀ {A : Set} → 𝕃 A × 𝕃 A → 𝕃 A
-  cat = uncurry (foldr (id , curry (cons ∘ ⟨ outl ∘ outl , ev ∘ (outr ×₁ id) ⟩)))
-
-  sum : 𝕃 ℕ → ℕ
-  sum = foldr (0 , +)
-```
-
-**HOMEWORK 4**
-
-```agda
-  take : ∀ {A : Set} → ℕ → 𝕃 A → 𝕃 A
-  take zero = nil !
-  take (succ n) = foldr (nil , (cons ∘ (id ×₁ take n)))
-```
-
-**HOMEWORK 5**
-
-We show that the `list` function is functorial:
-
-```agda
-  list : ∀ {A B : Set} → (A → B) → 𝕃 A → 𝕃 B
-  list f = foldr (nil , (cons ∘ (f ×₁ id)))
-
-  list-id : ∀ {A : Set} → list id ≡ id {𝕃 A}
-  list-id = foldr-id
-
-  list-homomorphism : ∀ {A B C : Set} (f : A → B) (g : B → C) → (list g) ∘ (list f) ≡ list (g ∘ f)
-  list-homomorphism {A} {B} {C} f g = foldr-fusion nil (cons ∘ (f ×₁ id)) (list g) nil (cons ∘ ((g ∘ f) ×₁ id)) refl refl
-```
-
-**HOMEWORK 6**
-
-Ackermann function:
-
-```agda
-  ack : ℕ × ℕ → ℕ
-  ack = uncurry (foldn (succ , h))
-    where
-      -- https://arxiv.org/pdf/1602.05010.pdf
-      -- first look
-      h' : (ℕ → ℕ) → ℕ → ℕ
-      h' f = foldn (f 1 , f)
-      -- pointfree
-      h : (ℕ → ℕ) → ℕ → ℕ
-      h = curry (ev ∘ ((foldn ∘ ⟨ ev ∘ ⟨ id , 1 ! ⟩ , id ⟩) ×₁ id))
-
-  -- pointwise definition for comparison
-  ack' : ℕ → ℕ → ℕ
-  ack' 0 = succ
-  ack' (succ n) zero = ack' n 1
-  ack' (succ n) (succ m) = ack' n (ack' (succ n) m)
-
-  ack-test1 : ack (3 , 3) ≡ ack' 3 3
-  ack-test1 = refl
-  ack-test2 : ack (0 , 3) ≡ ack' 0 3
-  ack-test2 = refl
-  ack-test3 : ack (3 , 2) ≡ ack' 3 2
-  ack-test3 = refl
-  ack-test4 : ack (2 , 2) ≡ ack' 2 2
-  ack-test4 = refl
-```
-
-**HOMEWORK 7**
-
-Trees:
-
-```agda
-  data 𝕋 (A : Set) : Set where
-    leaf : A → 𝕋 A
-    bin : 𝕋 A × 𝕋 A → 𝕋 A
-
-  foldt : ∀ {A C : Set} → ((A → C) × ((C × C) → C)) → 𝕋 A → C
-  foldt (c , h) (leaf a) = c a
-  foldt (c , h) (bin (s , t)) = h (foldt (c , h) s , foldt (c , h) t)
-
-  front : ∀ {A : Set} → 𝕋 A → 𝕃 A
-  front = foldt ((cons ∘ ⟨ id , nil ! ⟩) , cat)
-
-  foldt-id : ∀ {A : Set} → foldt (leaf , bin) ≡ id {𝕋 A}
-  foldt-id {A} = extensionality (foldt (leaf , bin)) id helper
-    where
-      helper : ∀ (x : 𝕋 A) → foldt (leaf , bin) x ≡ id x
-      helper (leaf x) = refl
-      helper (bin (x , y)) rewrite helper x | helper y = refl
-
-  foldt-fusion : ∀ {A C C' : Set} (c : A → C) (h : C × C → C) (k : C → C') (c' : A → C') (h' : C' × C' → C') → k ∘ c ≡ c' → k ∘ h ≡ h' ∘ (k ×₁ k) → k ∘ foldt (c , h) ≡ foldt (c' , h')
-  foldt-fusion {A} {C} {C'} c h k c' h' kc kh = extensionality (k ∘ foldt (c , h)) (foldt (c' , h')) helper
-    where
-      helper : ∀ (x : 𝕋 A) → k (foldt (c , h) x) ≡ foldt (c' , h') x
-      helper (leaf x) = ext-rev kc x
-      helper (bin (s , t)) rewrite ext-rev kh (foldt (c , h) s , foldt (c , h) t) | helper s | helper t = refl
-
-```
-
-**HOMEWORK 8**
-
-```agda
-  sumt : 𝕋 ℕ → ℕ
-  sumt = foldt (id , +)
-
-  front-sum : sumt ≡ sum ∘ front
-  front-sum = sym (foldt-fusion (cons ∘ ⟨ id , nil ! ⟩) cat sum id + (extensionality _ _ triangle) square)
-    where
-      triangle : ∀ x → (sum ∘ (cons ∘ ⟨ id , nil ! ⟩)) x ≡ id x
-      triangle x rewrite +0 x = refl
-      square : sum ∘ cat ≡ + ∘ (sum ×₁ sum)
-      square = extensionality _ _ helper
-        where 
-          helper : (x : 𝕃 ℕ × 𝕃 ℕ) → (sum ∘ cat) x ≡ (+ ∘ (sum ×₁ sum)) x
-          helper = {!   !}
-```
-
-**HOMEWORK 9**
-
-```agda
-  data 𝕋' (A : Set) : Set where
-    leaf' : A → 𝕋' A
-    bin' : A × 𝕋' A × 𝕋' A → 𝕋' A
-
-  foldb : ∀ {A C : Set} → ((A → C) × (A × C × C → C)) → 𝕋' A → C
-  foldb (c , h) (leaf' x) = c x
-  foldb (c , h) (bin' (x , (s , t))) = h (x , (foldb (c , h) s , foldb (c , h) t))
-
-  foldb-id : ∀ {A : Set} → foldb (leaf' , bin') ≡ id {𝕋' A}
-  foldb-id {A} = extensionality (foldb (leaf' , bin')) id helper
-    where
-      helper : ∀ (x : 𝕋' A) → foldb (leaf' , bin') x ≡ id x
-      helper (leaf' x) = refl
-      helper (bin' (x , (t , s))) rewrite helper t | helper s = refl
-
-  foldb-fusion : ∀ {A C C' : Set} (c : A → C) (h : A × C × C → C) (k : C → C') (c' : A → C') (h' : A × C' × C' → C') → k ∘ c ≡ c' → k ∘ h ≡ h' ∘ (id ×₁ k ×₁ k) → k ∘ foldb (c , h) ≡ foldb (c' , h')
-  foldb-fusion {A} {C} {C'} c h k c' h' kc kh = extensionality _ _ helper 
-    where
-      helper : ∀ (x : 𝕋' A) → (k ∘ foldb (c , h)) x ≡ foldb (c' , h') x
-      helper (leaf' x) = ext-rev kc x
-      helper (bin' (x , (s , t))) rewrite ext-rev kh (x , (foldb (c , h) s , foldb (c , h) t)) | helper s | helper t = refl
-
-  size : ∀ {A : Set} → 𝕋' A → ℕ
-  size = foldb ((1 !) , (succ ∘ + ∘ outr))
-
-  flatten : ∀ {A : Set} → 𝕋' A → 𝕃 A
-  flatten = foldb ((cons ∘ ⟨ id , nil ! ⟩) , (cons ∘ (id ×₁ cat)))
-
-  flatten-size : ∀ {A : Set} → length ∘ flatten ≡ size {A}
-  flatten-size {A} = foldb-fusion (cons ∘ ⟨ id , nil ! ⟩) (cons ∘ (id ×₁ cat)) length (1 !) (succ ∘ + ∘ outr) refl square
-    where
-      square : length ∘ (cons ∘ ((id ×₁ cat))) ≡ (succ ∘ + ∘ outr) ∘ (id ×₁ length ×₁ length)
-      square = {!   !}
-```

agda/equality.agda

@@ -1,35 +0,0 @@
-module equality where
-  -- in this module we define propositional equality and some helper syntax.
-
-  infix 4 _≡_
-  data _≡_ {A : Set} (a : A) : A → Set where
-    instance refl : a ≡ a
-  {-# BUILTIN EQUALITY _≡_ #-}
-
-  -- ≡ is a equivalence relation
-  sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
-  sym refl = refl
-
-  trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
-  trans refl refl = refl
-
-  cong : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y
-  cong f refl = refl
-
-  -- Equational reasoning
-  infix 3 _∎
-  infixr 2 _≡⟨⟩_ step-≡
-  infix 1 begin_
-  begin_ : ∀ {A : Set} {x y : A} → x ≡ y → x ≡ y
-  begin x = x
-
-  _≡⟨⟩_ : ∀ {A : Set} (x y : A) → x ≡ y → x ≡ y
-  _ ≡⟨⟩ _ = λ x → x
-
-  _∎ : ∀ {A : Set} (x : A) → x ≡ x
-  _ ∎ = refl
-
-  step-≡ : ∀ {A : Set} (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
-  step-≡ _ y≡z x≡y = trans x≡y y≡z
-
-  syntax step-≡ x eq1 eq2 = x ≡⟨ eq2 ⟩ eq1

tex/.vscode/ltex.dictionary.en-US.txt

@@ -1,4 +0,0 @@
-Vatthauer
-mycase
-Coalgebras
-Coalgebra

tex/.vscode/settings.json

@@ -1,27 +0,0 @@
-{
-  "latex-workshop.latex.tools": [
-    {
-      "name": "latexmk-main",
-      "command": "latexmk",
-      "args": [
-        "-synctex=1",
-        "-interaction=nonstopmode",
-        "-file-line-error",
-        "-shell-escape",
-        "-pdf",
-        "-xelatex",
-        "-outdir=%OUTDIR%",
-        "main.tex"
-      ],
-      "env": {}
-    }
-  ],
-  "latex-workshop.latex.recipes": [
-    {
-      "name": "latexmk-main",
-      "tools": [
-        "latexmk-main"
-      ]
-    }
-  ]
-}

tex/Makefile

@@ -1,15 +0,0 @@
-src = $(wildcard *.tex)
-pdf = $(src:.tex=.pdf)
-
-.PHONY: all clean
-
-all: $(pdf)
-
-%.pdf: %.tex $(wildcard src/*.tex) $(wildcard *.bib)
-	latexmk -pdf -xelatex -shell-escape -file-line-error -synctex=1 -halt-on-error -shell-escape $<
-
-clean:
-	latexmk -C $(src)
-	rm -f $(wildcard *.out *.nls *.nlo *.bbl *.blg *-blx.bib *.run.xml *.bcf *.synctex.gz *.fdb_latexmk *.fls *.toc *.loe *.tdo *.bbl-SAVE-ERROR)
-	rm -f $(wildcard sections/*.aux)
-	rm -rf $(wildcard _minted-main sections/.auctex-auto _region_.prv)

tex/main.tex

@@ -1,117 +0,0 @@
-\documentclass[a4paper,11pt,titlepage]{scrartcl}
-
-%%%% Document Setup
-\usepackage[top=2cm,lmargin=1in,rmargin=1in,bottom=3cm,hmarginratio=1:1]{geometry}
-\usepackage{scrlayer-fancyhdr}
-\usepackage{extramarks}
-\usepackage{anyfontsize}
-\usepackage{unicode-math}
-\usepackage[scale=.85]{noto-mono} % TODO find better unicode mono font
-\usepackage[final]{hyperref}
-\pagestyle{fancy}
-\lhead{\DocTitle}
-\chead{\UniCourse}
-\rhead{\firstxmark}
-\lfoot{\lastxmark}
-\cfoot{\thepage}
-\renewcommand\headrulewidth{0.4pt}
-\renewcommand\footrulewidth{0.4pt}
-%%%%
-
-%%%% Metadata
-\newcommand{\DocTitle}{Lecture notes}
-\newcommand{\UniCourse}{Algebra of Programming}
-\newcommand{\UniProf}{Prof.\ Dr.\ Stefan Milius}
-\author{Leon Vatthauer}
-%%%%
-
-%%%% Title
-\title{
-    \vspace{2in}
-    \textmd{\textbf{\UniCourse\\\DocTitle}}\\
-    \vspace{0.1in}\large{\textit{\UniProf\ }}
-    \vspace{3in}
-}
-%%%%
-
-%%%% Math packages
-\usepackage{amsthm}
-\usepackage{thmtools}
-\usepackage{tikz}
-\usetikzlibrary{cd, quotes}
-\declaretheorem[name=Definition,style=definition,numberwithin=section]{definition}
-\declaretheorem[name=Example,style=definition,sibling=definition]{example}
-\declaretheorem[style=definition,numbered=no]{exercise}
-\declaretheorem[name=Remark,style=definition,sibling=definition]{remark}
-\declaretheorem[name=Assumption,style=definition,sibling=definition]{assumption}
-\declaretheorem[name=Observation,style=definition,sibling=definition]{observation}
-\declaretheorem[name=Theorem,sibling=definition]{theorem}
-\declaretheorem[sibling=definition]{corollary}
-\declaretheorem[name=Fact,sibling=definition]{fact}
-\declaretheorem[sibling=definition]{lemma}
-\declaretheorem[sibling=lemma]{proposition}
-%%%%
-
-\makeatletter
-\hypersetup{
-  pdfauthor={\@author},
-  pdftitle={\@title},
-  % kill those ugly red rectangles around links
-  hidelinks,
-}
-\makeatother
-
-%%%% Custom definitions: Commands and environments
-
-%%% Case distinction environment
-% Defines the `mycase` environment, copied from https://tex.stackexchange.com/questions/251053/how-to-use-case-1-case-2-in-a-proof-ieee-confs
-\newcounter{cases}
-\newcounter{subcases}[cases]
-\newenvironment{mycase}
-{
-    \setcounter{cases}{0}
-    \setcounter{subcases}{0}
-    \newcommand{\case}
-    {
-        \par\indent\stepcounter{cases}\textbf{Case \thecases.}
-    }
-    \newcommand{\subcase}
-    {
-        \par\indent\stepcounter{subcases}\textit{Subcase (\thesubcases):}
-    }
-}
-{
-    \par
-}
-\renewcommand*\thecases{\arabic{cases}}
-\renewcommand*\thesubcases{\roman{subcases}}
-%%%
-
-%%% Custom label command
-\makeatletter
-\newcommand{\customlabel}[2]{%
-  \protected@write \@auxout {}{\string \newlabel {#1}{{#2}{\thepage}{#2}{#1}{}} }% chktex 1
-  \hypertarget{#1}{#2}%
-}
-\makeatother
-%%%
-%%%%
-
-
-\begin{document}
-%% Titlepage
-\maketitle
-\setcounter{page}{1}
-%%
-
-%% TOC
-\tableofcontents
-\pagebreak
-%%
-
-%% Contents
-\include{sections/01_introduction}
-\include{sections/02_categories}
-\include{sections/03_constructions}
-%%
-\end{document}

tex/sections/01_introduction.tex

@@ -1,4 +0,0 @@
-\section{Introduction}
-
-\subsection{Functions}
-\subsection{Data Types}

tex/sections/02_categories.tex

@@ -1,9 +0,0 @@
-\section{Category Theory}
-
-\subsection{Special Objects}
-\subsection{Duality}
-\subsection{Functors}
-\subsection{Natural Transformations}
-\subsection{Functor Algebras}
-\subsection{Functor Coalgebras}
-\subsection{(co)Limits} % chktex 36

tex/sections/02_datatypes.tex

@@ -1 +0,0 @@
-\section{Functions and Data}

tex/sections/03_constructions.tex

@@ -1,4 +0,0 @@
-\section{Constructions}
-\subsection{CPO}
-\subsection{Initial Algebra Construction}
-\subsection{Terminal Coalgebra Construction}