Zulip Chat Archive

Stream: maths

Topic: trunc


view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 15 2018 at 20:33):

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

view this post on Zulip Chris Hughes (Jul 15 2018 at 20:36):

Do you get an error?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 15 2018 at 20:36):

Do you get an error?

I don't

view this post on Zulip 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. -/

view this post on Zulip 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