Function World

def RTPNotes.Worlds.Function.level1 {A : Type} : A → A

Level 1

For a type A, the identity function id : A → A is the function defined by sending and arbitrary element a : A to itself.

Equations

• RTPNotes.Worlds.Function.level1 a = a

def RTPNotes.Worlds.Function.level2 {A B : Type} (a : A) (f : A → B) : B

Level 2

Given a function f : A → B and an element a : A, there is an element f a : B obtained by evaluating the function f at a.

Equations

• RTPNotes.Worlds.Function.level2 a f = f a

def RTPNotes.Worlds.Function.level3 {A B : Type} (a : A) (f : A → B) : B

Level 3

Given a function f : A → B and an element a : A, there is an element f a : B obtained by evaluating the function f at a.

Equations

• RTPNotes.Worlds.Function.level3 a f = f a

def RTPNotes.Worlds.Function.level4 {A B C : Type} (g : B → C) (f : A → B) : A → C

Level 4

Given functions g : B → C and f : A → B, define the composite function g ∘ f : A → C that sends x : A to g (f x).

Equations

• RTPNotes.Worlds.Function.level4 g f x = g (f x)

def RTPNotes.Worlds.Function.level5 {A B : Type} (a : A) : B → A

Level 5

For any types A and B and element a : A, there is a constant function const a : B → A that sends any x : B to the element a : A.

Equations

• RTPNotes.Worlds.Function.level5 a x✝ = a

def RTPNotes.Worlds.Function.level6 {A B C : Type} (a : A) (f : A → B → C) : B → C

Level 6

Given an element a : A and a function of two variables f : A → B → C, define a function from B → C by evaluating the first variable of f at the element a.

Equations

• RTPNotes.Worlds.Function.level6 a f = f a

def RTPNotes.Worlds.Function.level7 {A B C : Type} : (A → B → C) → B → A → C

Level 7

From a function of two variables, define another function of two variables, where the inputs are swapped.

Equations

• RTPNotes.Worlds.Function.level7 f b a = f a b

def RTPNotes.Worlds.Function.level8 {A B C : Type} : (B → C) → (A → B) → A → C

Level 8

Define the composition of two functions as a multivariable function between function types.

Equations

• RTPNotes.Worlds.Function.level8 f g a = f (g a)

def RTPNotes.Worlds.Function.level9 {A B : Type} : A → (A → B) → B

Level 9

Define the evaluation function that takes a : A and f : A → B to f a : B.

Equations

• RTPNotes.Worlds.Function.level9 a f = f a

def RTPNotes.Worlds.Function.level10 {F V : Type} : ((((V → F) → F) → F) → F) → (V → F) → F

Level 10

Given a function of type ((((V → F) → F) → F) → F) there is a canonically defined function of type (V → F) → F.

Equations

• RTPNotes.Worlds.Function.level10 f g = f fun (h : (V → F) → F) => h g