Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC