Zulip Chat Archive
Stream: general
Topic: computable function Type 2 -> Type 1
Kenny Lau (Jul 31 2018 at 09:50):
is there any computable non-constant function Type 2 -> Type 1?
Chris Hughes (Jul 31 2018 at 09:53):
def f : Type 2 → Type := λ α , plift (nonempty α)
Kenny Lau (Jul 31 2018 at 09:54):
nice
Gabriel Ebner (Jul 31 2018 at 09:54):
Type != Type 1. You need one more plift.
Last updated: Dec 20 2023 at 11:08 UTC