voidex

Ковыряю Agda2

module if where

open import proof
open import bool

open import list

if_then_else_ : ∀ {l} {a : Set l} → (p : bool) → ((p ≡ true) → a) → a → a
if true then t else f = t refl
if false then t else f = f

head₀ : ∀ {l} {a : Set l} → (ls : list a) → (not (empty ls) ≡ true) → a
head₀ {_} {_} null ()
head₀ {_} {_} (cons x xs) p = x

test₁ : ∀ {l} {a : Set l} → list a → a → a
test₁ ls v = if (not (empty ls)) then head₀ ls else v

test₂ : ∀ {l} {a : Set l} → a → a
test₂ v = head₀ (singleton v) refl

record Monad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  field
    F : Endofunctor C
    η : NaturalTransformation id F
    μ : NaturalTransformation (F ∘ F) F

  open Functor F

  field
    .assoc : μ ∘₁ (F ∘ˡ μ) ≡ μ ∘₁ (μ ∘ʳ F)
    .identityˡ : μ ∘₁ (F ∘ˡ η) ≡ idN
    .identityʳ : μ ∘₁ (η ∘ʳ F) ≡ idN

С радостью присоединюсь к команде. Поучаствовать хочется, но одному слишком напряжённо, так что зовите. Умею держать свечку и варить кофе.

Поставил до кучи, заодно решил проверить.