Give an additional example in Basics/Polymorphism

[DanielRrr]

This part of the tutorial explains Pi-types basically. There is a basic example of Pi type \Pi (b : Bool) -> if b Nat Bool. Most of the examples in the section with Basics are supported by their counterparts in Haskell. I would give a Haskell counterpart of \Pi (b : Bool) -> if b Nat Bool as well to emphasise how dependently typed languages relief dealing with type-level stuff. It could be of help (for a Haskell part of the potential audience) in making a difference between Haskell and Arend stressing that dependent types in Arend are proper.

\Pi (b : Bool) -> if b Nat Bool could be translated via type families and the language extension call DataKinds.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind (Type)

type family Foo (b :: Bool) :: Type where
  Foo 'True = Nat
  Foo 'False = Bool