{-# OPTIONS --type-in-type #-}
module Lecture7 where
data Nat : Set where
zero : Nat
succ : Nat -> Nat
data Vec (A : Set) : Nat -> Set where
[] : Vec A zero
_∷_ : A -> ∀ {n} -> Vec A n -> Vec A (succ n)
zeros : ∀ n -> Vec Nat n
zeros zero = []
zeros (succ n) = zero ∷ zeros n
_+_ : Nat -> Nat -> Nat
zero + b = b
succ a + b = succ (a + b)
sum : ∀ {n} -> Vec Nat n -> Nat
sum [] = zero
sum (x ∷ xs) = sum xs + x
data _≡_ {A : Set} (x : A) : A -> Set where
refl : x ≡ x
sum-zeros : ∀ n -> sum (zeros n) ≡ zero
sum-zeros zero = refl
sum-zeros (succ n) = {!!} (sum-zeros n)
≡-cong : {A B : Set} {a b : A} (f : A -> B) -> a ≡ b -> f a ≡ f b
≡-cong f refl = refl
+0 : ∀ m -> m ≡ (m + zero)
+0 zero = refl
+0 (succ m) = ≡-cong succ (+0 m)
+comm : ∀ m n -> (m + n) ≡ (n + m)
+comm zero n = +0 n
+comm (succ m) n = {!!}