siddhartha-gadgil

data Σ(A : Set) (B : A → Set) : Set where
  ι : (a : A) → B a → Σ A B

siddhartha-gadgil

data _⊕_ (A B : Set) : Set where
  i₁ : A → A ⊕ B
  i₂ : B → A ⊕ B

siddhartha-gadgil

data _×_ (A B : Set) : Set where
  [_,_] : A → B → A × B

siddhartha-gadgil

open import Nat

-- If f(m+1) = f(m) for all m, then f(n) = f(0) for all n  
constthm : (f : ℕ → ℕ) → ((m : ℕ) → (f (succ m)) == (f m)) → (n : ℕ) → (f n) == (f 0)
constthm f _ 0 = refl (f 0)
constthm f adjEq (succ n) = (adjEq n) transEq (constthm f adjEq n)

siddhartha-gadgil

transport : {A : Set} → {B : Set} → {x y : A} → (f : A → B) → x == y → f(x) == f(y)
transport f (refl a) = refl (f a)

symm : {A : Set} → {x y : A} → x == y → y == x
symm (refl a) = refl a


_transEq_ : {A : Set} → {x y z : A} → x == y → y == z → x == z
(refl a) transEq (refl .a) = refl a

siddhartha-gadgil

data _==_ {A : Set} : A → A → Set where
  refl : (a : A) → a == a

siddhartha-gadgil

1odd : Even 1 → False
1odd ()

siddhartha-gadgil

2even : Even 2
2even = +2even zeroeven

siddhartha-gadgil

data Even : ℕ → Set where
  zeroeven : Even zero
  +2even : {n : ℕ} → Even n → Even (succ (succ n))

siddhartha-gadgil

vacuous : {A : Set} → False → A
vacuous ()