gistfile1.txt

module test where
data _≡_ {A} : A → A → Set where
  refl : {a : A} → a ≡ a

cong : ∀ {A B} {a₁ a₂ : A} → (f : A → B) → (a₁ ≡ a₂) → f a₁ ≡ f a₂
cong _ refl = refl

sym : ∀ {A} {a₁ a₂ : A} → a₁ ≡ a₂ → a₂ ≡ a₁
sym refl = refl

trans : ∀ {A} {a₁ a₂ a₃ : A} → a₁ ≡ a₂ → a₂ ≡ a₃ → a₁ ≡ a₃
trans refl refl = refl

infixl 1 _⇒_
_⇒_ : ∀ {A} {a₁ a₂ a₃ : A} → a₁ ≡ a₂ → a₂ ≡ a₃ → a₁ ≡ a₃
p ⇒ q = trans p q

infixr 2 _≡⟨_⟩_
_≡⟨_⟩_ : ∀ x {y z} → x ≡ y → y ≡ z → x ≡ z
_≡⟨_⟩_ .z {.z} {z} refl refl = refl

begin_ : ∀ {x y} → x ≡ y → x ≡ y
begin refl = refl

_∎ : ∀ x → x ≡ x
_∎ _ = refl

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

_+_ : ℕ → ℕ → ℕ
zero + m = m
n + zero = n
(succ n) + m = succ (n + m)

n+m≡m+n : {n m : ℕ} → (n + m) ≡ (m + n)
n+m≡m+n {zero} {zero} = refl
n+m≡m+n {zero} {succ m} = refl
n+m≡m+n {succ n} {zero} = refl
n+m≡m+n {succ n} {succ m} = begin {!succ (n + succ m) ≡ succ (m + succ n)!}

--open import Relation.Binary.EqReasoning

data Even : ℕ → Set where
  ezero : Even zero
  esucc : (n : ℕ) → Even n → Even (succ (succ n))

twoIsEven : Even (succ (succ zero))
twoIsEven = esucc zero ezero

evenIsEven : (n : ℕ) → Even n → Even (succ (succ n))
evenIsEven = esucc

sumOfEven : (n m : ℕ) → Even n → Even m → Even (n + m)
sumOfEven zero m p q = q
sumOfEven (succ n) .zero p ezero = {!!}
sumOfEven (succ n) .(succ (succ n₁)) p (esucc n₁ q) = {!!}