[Agda] Re: Builtins

[N. Raghavendra]

At 2015-04-25T18:53:05Z, Kirill Elagin wrote:

> Also note, that in Agda’s stdlib from `a ≡ b` it follows that `a` is
> `b`, as Agda knows that there is no other than `refl` way to
> construct a proof of `a ≡ b`.

Is this related to axiom K and uniqueness of identity proofs?

> You said you are going to do HoTT, so you should be aware that this is
> not true in HoTT (since there are types that are not 0-types).

Is this why all HoTT-Agda files contain the {-# OPTIONS --without-K #-}
pragma?

Thanks and cheers,
Raghu.

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/