triangular.agda

open import Agda.Builtin.Nat

data Vec (F : Nat → Set) : Nat → Set where
  []  : Vec F 0
  _∷_ : ∀ {n} (xs : Vec F n) (x : F (suc n)) → Vec F (suc n)

map : {!   !}
map f [] = []
map f (xs ∷ x) = (map f xs) ∷ (f x)

reduce : {!   !}
reduce f z []       = z
reduce f z (xs ∷ x) = reduce f (f z x) xs

-- example data
row1 : Vec (\ _ -> Nat) 1
row1 = [] ∷ 1

row2 : Vec (\ _ -> Nat) 2
row2 = ([] ∷ 2) ∷ 3

row3 : Vec (\ _ -> Nat) 3
row3 = (([] ∷ 4) ∷ 5) ∷ 6

xs : Vec (\ i -> Vec (\ _ -> Nat) i) 3
xs = (([] ∷ row1) ∷ row2) ∷ row3

-- apply suc to each element
ys : {!   !}
ys = map (\ row -> map suc row) xs

-- sum up all rows
zs : {!   !}
zs = map (\ row -> reduce (\ x y -> x + y) 0 row) xs