## Stream: Is there code for X?

### Topic: trunc

#### Scott Morrison (Jun 02 2020 at 03:27):

Is

import data.quot

def foo {α : Type*} {Z : α → Type*} (f : Π a, trunc (Z a)) : trunc (Π a, Z a) :=
sorry


definable?

(computably)

Nope

#### Mario Carneiro (Jun 02 2020 at 03:44):

This comes up every once in a while. It has some reasonably obvious computational interpretation, but you can't prove it from lean's axioms

#### Simon Hudon (Jun 02 2020 at 03:45):

I think we could remove the noncomputable keyword by using a vm_override though. Am I wrong? (I haven't used them that way yet)

#### Mario Carneiro (Jun 02 2020 at 03:46):

This is also relevant for the QPF implementation that Jeremy, Simon and I worked on last year. I think @Gabriel Ebner told me that this makes the definitional equality problem much harder because you have to work under binders; I forget the details now. It might end up like cubical type theory reduction

#### Simon Hudon (Jun 02 2020 at 03:49):

To answer my own question: vm_override don't do that yet

#### Mario Carneiro (Jun 02 2020 at 03:51):

Oh, I also remembered a trick that @Chris Hughes pointed out:

def bar {α : Type*} : trunc (trunc α → α) := foo (@id (trunc α))


you can do some really funny things with this function, because the VM representation of this function does not respect equality

#### Mario Carneiro (Jun 02 2020 at 04:00):

Ah, here it is:

import data.quot

meta def foo {α : Type*} {Z : α → Type*} (f : Π a, trunc (Z a)) : trunc (Π a, Z a) :=
unchecked_cast f

meta def bar {α : Type*} : trunc (trunc α → α) := foo (@id (trunc α))

meta def lie : bool :=
(@bar bool).lift (λ f, to_bool (f (trunc.mk tt) = f (trunc.mk ff))) \$ λ f g,
by simp [show trunc.mk tt = trunc.mk ff, from subsingleton.elim _ _]

meta example : lie = tt :=
show trunc.lift _ _ bar = _, begin
generalize : bar = x,
refine trunc.ind (λ x, _) x,
apply to_bool_tt,
rw show trunc.mk tt = trunc.mk ff, from subsingleton.elim _ _
end

#eval lie -- ff


#### Scott Morrison (Jun 02 2020 at 04:03):

Ok, to #xy the problem, what I really wanted was:

import data.fintype.basic

def equiv.sigma_quotient_fin_card
{α : Type*} [fintype α] [decidable_eq α] (s : setoid α) [decidable_rel s.r]:
trunc (α ≃ Σ (q : quotient s), fin (fintype.card {x // ⟦x⟧ = q})) :=


which I can construct using foo, but so far not otherwise.

#### Mario Carneiro (Jun 02 2020 at 04:07):

I think this can be proven. First you fix an ordering of the base type, then this induces an order on every equivalence class and you get the map to fin that way

#### Mario Carneiro (Jun 02 2020 at 04:43):

def equiv.sigma_quotient_fin_card
{α : Type*} [fa : fintype α] [decidable_eq α] (s : setoid α) [decidable_rel s.r] :
trunc (α ≃ Σ (q : quotient s), fin (fintype.card {x // ⟦x⟧ = q})) :=
begin
resetI, rcases fa with ⟨⟨S, hS₁⟩, hS₂⟩,
refine quotient.rec_on_subsingleton S (λ l h₁ h₂, trunc.mk _) hS₁ hS₂, clear hS₂ hS₁ S,
exact (equiv.sigma_preimage_equiv quotient.mk).symm.trans (equiv.sigma_congr_right (λ q,
fintype.equiv_fin_of_forall_mem_list
(λ ⟨x, px⟩, list.mem_pmap.2 ⟨x, list.mem_filter.2 ⟨h₂ _, px⟩, rfl⟩)
(list.nodup_pmap (λ a _ b _, congr_arg subtype.val) (list.nodup_filter _ h₁)))),
end


#### Scott Morrison (Jun 02 2020 at 05:34):

Excellent, thanks. I'll upgrade this to a trunc (Σ' e : α ≃ Σ (q : quotient s), fin (fintype.card {x // ⟦x⟧ = q}), ∀ x, (e x).1 = ⟦x⟧), recording the "fibre-wise" property, and eventually include it in a PR.

#### Mario Carneiro (Jun 02 2020 at 06:22):

That could be a subtype instead of a Sigma'

Last updated: May 16 2021 at 05:21 UTC