[Agda] on "Dependently Typed.."

[Serge D. Mechveliani]

A few notes on  "Dependently Typed Programming in Agda" by Ulf Norell.

* 2.1. 
... type theory developed at Chalmers University ...     
References ?

* 2.1.
...
Functions over Bool can be defined by pattern matching in a for 
Haskell programmers familiar way:
--? -->
... in a way familiar to Haskell programmers:

2.4.
...
Absurd patterns
---------------
... name   the family of numbers  
--typo-?-->
... namely the family ...

Regards,
Sergei