trunc

Stream: maths

[Kenny Lau]

import data.quot

universe u

variables {α : Type u} [group α]

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

[Kenny Lau]

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

[Chris Hughes]

Do you get an error?

[Gabriel Ebner]

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]

Do you get an error?

I don't

[Gabriel Ebner]

/-- `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]

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)