# Zulip Chat Archive

## 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?

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

(computably)

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

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