Daniel Rogozin

In Propositions and sets/Mere Proposition, there is the [following example](https://arend-lang.github.io/documentation/tutorial/PartII/hprops#mere-propositions): ``` \func Unit-isProp : isProp Unit => \lam x y => idp ``` which is rejected with ``` [ERROR] Intro.ard:543:48:...

[There is Exercise 5 in the "Propositions and sets" section](https://arend-lang.github.io/documentation/tutorial/PartII/hprops#mere-propositions): ``` Exercise 5: Prove that \Sigma (x : A) (B x) preserves propositions. ``` But the logic of propositions is...

[The tutorial says](https://arend-lang.github.io/documentation/tutorial/PartI/synndef#namespaces-and-modules) ``` Each definition can be accompanied by \where block in the end. In contrast to Haskell, \where block is attached to the whole definition, not to a...

[This part of the tutorial](https://arend-lang.github.io/documentation/tutorial/PartI/synndef#polymorphism) explains Pi-types basically. There is a basic example of Pi type `\Pi (b : Bool) -> if b Nat Bool`. Most of the examples in...