## Stream: maths

### Topic: trunc

#### Kenny Lau (Jul 15 2018 at 20:32):

import data.quot

universe u

variables {α : Type u} [group α]

def get_one : trunc α → α :=
trunc.lift (λ x, x * x⁻¹) \$ λ x y, by simp


#### Kenny Lau (Jul 15 2018 at 20:33):

Am I doing it right? What is the use of trunc?

#### Chris Hughes (Jul 15 2018 at 20:36):

Do you get an error?

#### Gabriel Ebner (Jul 15 2018 at 20:36):

trunc is the quotient by the universal relation. So for groups, trunc α is always a singleton. You can use it e.g. to define an existential quantifier where you can computably use the witness, but still have (propositional) "proof" irrelevance.

#### Kenny Lau (Jul 15 2018 at 20:36):

Do you get an error?

I don't

#### Gabriel Ebner (Jul 15 2018 at 20:36):

/-- trunc α is the quotient of α by the always-true relation. This
is related to the propositional truncation in HoTT, and is similar
in effect to nonempty α, but unlike nonempty α, trunc α is data,
so the VM representation is the same as α, and so this can be used to
maintain computability. -/


#### Gabriel Ebner (Jul 15 2018 at 20:39):

So trunc { x // x * x != 1 } is a subsingleton like ∃ x, x * x != 1 but you can use the witness x to compute other data (as long as it does not depend on the concrete value of x)

Last updated: May 18 2021 at 07:19 UTC