import MyNat.Definition
namespace MyNat
open MyNat

Function World

Level 6: (P → (Q → R)) → ((P → Q) → (P → R)).

You can solve this level completely just using intro, apply and exact, but if you want to argue forwards instead of backwards then don't forget that you can do things like

have j : Q → R := f p

if f : P → (Q → R) and p : P. Remember the trick with the colon in have: we could just write have j := f p but this way we can be sure that j is what we actually expect it to be.

We start with intro f rather than intro p because even though the goal starts P → ..., the brackets mean that the goal is not a function from P to anything, it's a function from P → (Q → R) to something. In fact you can save time by starting with intros f h p, which introduces three variables at once, although you'd better then look at your tactic state to check that you called all those new terms sensible things.

After all the intros, you find that the goal is ⊢ R. If you try have j : Q → R := f p now then you can apply j. Alternatively you can apply (f p) directly. What happens if you just try apply f? Can you figure out what just happened? This is a little apply easter egg. Why is it mathematically valid?

Definition

Whatever the sets P and Q and R are, we make an element of \(\operatorname{Hom}(\operatorname{Hom}(P,\operatorname{Hom}(Q,R)), \operatorname{Hom}(\operatorname{Hom}(P,Q),\operatorname{Hom}(P,R)))\).

example: (P Q R : Type) → (P → Q → R) → (P → Q) → P → R
example (
P: Type
P 
Q: Type
Q 
R: Type
R : 
Type: Type 1
Type) : (
P: Type
P → (
Q: Type
Q → 
R: Type
R)) → ((
P: Type
P → 
Q: Type
Q) → (
P: Type
P → 
R: Type
R)) := 
P, Q, R: Type
(P → Q → R) → (P → Q) → P → R

  
P, Q, R: Type
f: P → Q → R
(P → Q) → P → R

  
P, Q, R: Type
f: P → Q → R
h: P → Q
P → R

  
P, Q, R: Type
f: P → Q → R
h: P → Q
p: P
R

  
P, Q, R: Type
f: P → Q → R
h: P → Q
p: P
j: Q → R
R

  
P, Q, R: Type
f: P → Q → R
h: P → Q
p: P
j: Q → R
Q

  
P, Q, R: Type
f: P → Q → R
h: P → Q
p: P
j: Q → R
P

  
Goals accomplished! 🐙

Next up Level 7