# Zulip Chat Archive

## 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: Dec 20 2023 at 11:08 UTC