## Stream: general

### Topic: help with curry howard correspondence

#### Kind Bubble (Jan 03 2023 at 02:37):

Can someone help me complete my puzzle? I'm trying to jumpstart my Curry-Howard correspondence by proving this theorem

notation "⊛" => Unit
notation "*" => Unit.unit
notation "Π" "(" X ":" A ")" "," F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
variable {p : Prop}
def find_this_bugger : Π(_ : p),⊛-> p := sorry


#### Mario Carneiro (Jan 03 2023 at 02:40):

I think there is likely a precedence issue here

#### Kind Bubble (Jan 03 2023 at 02:40):

Mario Carneiro said:

I think there is likely a precedence issue here

What's that mean?

#### Mario Carneiro (Jan 03 2023 at 02:40):

you should put parentheses in to clarify whether you mean (Π(_ : p),⊛) -> p or Π(_ : p), (⊛ -> p)

#### Mario Carneiro (Jan 03 2023 at 02:41):

With the parentheses as you have placed them, the statement is false

#### Kind Bubble (Jan 03 2023 at 02:41):

Mario Carneiro said:

you should put parentheses in to clarify whether you mean (Π(_ : p),⊛) -> p or Π(_ : p), (⊛ -> p)

Ok I made edits here it is now:

notation "⊛" => Unit
notation "*" => Unit.unit
notation "Π" "(" X ":" A ")" "," F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
variable {p : Prop}
def find_this_bugger : (Π(_ : p),⊛) -> p := sorry


#### Mario Carneiro (Jan 03 2023 at 02:42):

because Π(_ : p),⊛ is always inhabited, by the constant function (x:p) ↦ *, but p is only inhabited sometimes

#### Mario Carneiro (Jan 03 2023 at 02:43):

so if we consider p = false for example then the sorry is false

#### Kind Bubble (Jan 03 2023 at 02:43):

Π(_ : p),⊛ could be ... oh! I wanted dependent sum!

Ok ok...

#### Mario Carneiro (Jan 03 2023 at 02:44):

that would be Sigma fun (X : A) => F

#### Kind Bubble (Jan 03 2023 at 02:47):

notation "⊛" => Unit
notation "*" => Unit.unit
notation "Π" "(" X ":" A ")" "," F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
variable {p : Prop}
def find_this_bugger : (Σ(_ : p ),⊛) -> p := sorry
def and_this_one : p ->  (Σ(_ : p ),⊛) := sorry


#### Mario Carneiro (Jan 03 2023 at 02:47):

fun hp => hp.1 and fun hp => \<hp, *\> respectively

#### Kind Bubble (Jan 03 2023 at 02:48):

poifect thanks a million. oh and one more:

notation "⊛" => Unit
notation "*" => Unit.unit
notation "Π" "(" X ":" A ")" "," F => forall (X : A), F
notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
def uniq : Π(x :⊛ ),Π(y :⊛),(Σ(p:x=y),⊛) := sorry


#### Kind Bubble (Jan 03 2023 at 17:46):

(deleted)

Last updated: Aug 03 2023 at 10:10 UTC