leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

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: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll