function

idApply

def idApply {A : Type} (a : A) : id a ≡ a

Applying the identity function is a no-op: id a = a.

idApplyFn

def idApplyFn {A B : Type} (f : A -> B) : (fun (x : A) => id (f x)) ≡ f

Post-composing a function with id gives back the function: (fun x => id (f x)) = f.

composeApply

def composeApply {A B C : Type} (g : B -> C) (f : A -> B) (x : A) : compose g f x ≡ g (f x)

Composition unfolds pointwise: (g ∘ f) x = g (f x).

composeAssocFn

def composeAssocFn {A B C D : Type} (h : C -> D) (g : B -> C) (f : A -> B) : compose h (compose g f) ≡ compose (compose h g) f

Function composition is associative: h ∘ (g ∘ f) = (h ∘ g) ∘ f.

composeIdLeft

def composeIdLeft {A B : Type} (f : A -> B) : compose (fun (x : B) => x) f ≡ f

The identity function is a left unit for composition: id ∘ f = f.

composeIdRight

def composeIdRight {A B : Type} (f : A -> B) : compose f (fun (x : A) => x) ≡ f

The identity function is a right unit for composition: f ∘ id = f.

flipApply

def flipApply {A B C : Type} (f : A -> B -> C) (a : A) (b : B) : flip f b a ≡ f a b

Flip swaps the two arguments: flip f b a = f a b.

flipFlip

def flipFlip {A B C : Type} (f : A -> B -> C) : (fun (a : A) => fun (b : B) => flip f b a) ≡ f

Flipping a function twice gives back the original function.

constApply

def constApply {A B : Type} (a : A) (b : B) : const a b ≡ a

A constant function ignores its argument: const a b = a.

constComposeLeft

def constComposeLeft {A B C : Type} (c : C) (f : A -> B) : compose (fun (x : B) => c) f ≡ (fun (x : A) => c)

Composing a constant function after any f is still constant: (fun _ => c) ∘ f = fun _ => c.

constComposeRight

def constComposeRight {A B C : Type} (g : B -> C) (b : B) : compose g (fun (x : A) => b) ≡ (fun (x : A) => g b)

Composing g after a constant function is constant at g b: g ∘ (fun _ => b) = fun _ => g b.

applyFn

def applyFn {A B : Type} (f : A -> B) (x : A) : apply f x ≡ f x

Function application via apply agrees with direct application: apply f x = f x.

applyId

def applyId {A : Type} (x : A) : apply (fun (a : A) => a) x ≡ x

Applying the identity function through apply returns the argument: apply id x = x.

isInjective

def isInjective (A : Type) (B : Type) (f : A -> B) : Type

The proposition that f is injective: equal images imply equal inputs.

isSurjective

def isSurjective (A : Type) (B : Type) (f : A -> B) : Type

The type saying f is surjective: every b in the codomain has a chosen preimage a with f a = b.

isBijective

def isBijective (A : Type) (B : Type) (f : A -> B) : Type

The type saying f is bijective: both injective and surjective.

hasSection

def hasSection (A : Type) (B : Type) (f : A -> B) : Type

A section (right inverse) of f: a map s with f (s b) = b for all b.

hasRetraction

def hasRetraction (A : Type) (B : Type) (f : A -> B) : Type

A retraction (left inverse) of f: a map r with r (f a) = a for all a.

isIso

def isIso (A : Type) (B : Type) (f : A -> B) : Type

A two-sided inverse of f: a map g with f (g b) = b and g (f a) = a.

idInjective

def idInjective (A : Type) : isInjective A A (fun (x : A) => x)

The identity function is injective.

idSurjective

def idSurjective (A : Type) : isSurjective A A (fun (x : A) => x)

The identity function is surjective.

idBijective

def idBijective (A : Type) : isBijective A A (fun (x : A) => x)

The identity function is bijective.

idHasSection

def idHasSection (A : Type) : hasSection A A (fun (x : A) => x)

The identity function is its own section.

idHasRetraction

def idHasRetraction (A : Type) : hasRetraction A A (fun (x : A) => x)

The identity function is its own retraction.

idIsIso

def idIsIso (A : Type) : isIso A A (fun (x : A) => x)

The identity function is an isomorphism, with itself as inverse.

funExtImpl

def funExtImpl {A B : Type} {f g : A -> B} (h : (x : A) -> f x ≡ g x) : f ≡ g

Function extensionality: functions that agree pointwise are equal as paths.

happlyImpl

def happlyImpl {A B : Type} {f g : A -> B} (p : f ≡ g) (x : A) : f x ≡ g x

Turns a path between functions into pointwise paths: f = g implies f x = g x.

happlyDep

def happlyDep {A : Type} {B : A -> Type} {f g : (x : A) -> B x} (p : f ≡ g) (x : A) : f x ≡ g x

Pointwise paths from a path between dependent functions: f = g implies f x = g x.

compose_injective

def compose_injective (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (gInj : isInjective B C g) (fInj : isInjective A B f) : isInjective A C (compose g f)

The composite of two injective functions is injective.

compose_surjective

def compose_surjective (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (gSurj : isSurjective B C g) (fSurj : isSurjective A B f) : isSurjective A C (compose g f)

The composite of two surjective functions is surjective.

compose_bijective

def compose_bijective (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (gBij : isBijective B C g) (fBij : isBijective A B f) : isBijective A C (compose g f)

The composite of two bijective functions is bijective.

fibIdCenter

def fibIdCenter (A : Type) (b : A) : fiber A A (fun (x : A) => x) b

The canonical element of the fiber of the identity function over b, namely b itself.

fibConstElem

def fibConstElem (A : Type) (B : Type) (a : A) (x : B) : fiber B A (fun (b : B) => a) a

Every x gives an element of the fiber of the constant function at a over a.

precomp

def precomp {A B C : Type} (f : A -> B) : (B -> C) -> (A -> C)

Precomposition with f: sends g to g ∘ f.

postcomp

def postcomp {A B C : Type} (g : B -> C) : (A -> B) -> (A -> C)

Postcomposition with g: sends f to g ∘ f.

precompIdApply

def precompIdApply (A : Type) (C : Type) (g : A -> C) (x : A) : precomp (fun (a : A) => a) g x ≡ g x

Precomposing with the identity leaves a function unchanged at every point.

postcompIdApply

def postcompIdApply (A : Type) (B : Type) (f : A -> B) (x : A) : postcomp (fun (b : B) => b) f x ≡ f x

Postcomposing with the identity leaves a function unchanged at every point.

curryApplyNd

def curryApplyNd {A B C : Type} (f : ((x : A) × B) -> C) (a : A) (b : B) : curry f a b ≡ f (a, b)

Currying computes as expected on non-dependent pairs: curry f a b = f (a, b).

uncurryApplyNd

def uncurryApplyNd {A B C : Type} (f : A -> B -> C) (a : A) (b : B) : uncurry f (a, b) ≡ f a b

Uncurrying computes as expected: uncurry f (a, b) = f a b.

curryUncurryNd

def curryUncurryNd {A B C : Type} (f : A -> B -> C) : (fun (a : A) => fun (b : B) => curry (uncurry f) a b) ≡ f

Currying after uncurrying gives back the original two-argument function.

constEq

def constEq {A B : Type} (a : A) (b1 b2 : B) : const a b1 ≡ const a b2

A constant function returns the same value for any two arguments.

constFunExt

def constFunExt {A B : Type} (a : A) : (fun (b : B) => const a b) ≡ (fun (b : B) => a)

The function fun b => const a b equals the constant function fun _ => a.

flipConstFn

def flipConstFn {A B : Type} : flip (fun (a : A) => fun (b : B) => a) ≡ (fun (b : B) => fun (a : A) => a)

Flipping the first projection gives the second projection: flip (fun a b => a) = fun b a => a.

section_to_surjective

def section_to_surjective (A : Type) (B : Type) (f : A -> B) (sec : hasSection A B f) : isSurjective A B f

A function with a section is surjective.

retraction_to_injective

def retraction_to_injective (A : Type) (B : Type) (f : A -> B) (ret : hasRetraction A B f) : isInjective A B f

A function with a retraction is injective.

iso_to_bijective

def iso_to_bijective (A : Type) (B : Type) (f : A -> B) (iso : isIso A B f) : isBijective A B f

A function with a two-sided inverse is bijective.

hasSection_compose

def hasSection_compose (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (gs : hasSection B C g) (fs : hasSection A B f) : hasSection A C (compose g f)

Sections compose: if g and f have sections, so does g ∘ f.

hasRetraction_compose

def hasRetraction_compose (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (gr : hasRetraction B C g) (fr : hasRetraction A B f) : hasRetraction A C (compose g f)

Retractions compose: if g and f have retractions, so does g ∘ f.

depApply

def depApply {A : Type} {B : A -> Type} {C : A -> Type} (g : (x : A) -> B x -> C x) (f : (x : A) -> B x) (x : A) : C x

Pointwise application of a dependent family of functions g to a dependent function f: x maps to g x (f x).

depConst

def depConst {A : Type} {B : A -> Type} (f : (x : A) -> B x) : (x : A) -> B x

The identity on dependent functions: returns f unchanged.

congIdFn

def congIdFn {A : Type} {a b : A} (p : a ≡ b) : cong (fun (x : A) => x) p ≡ p

Applying the identity function to a path with cong gives back the same path.

compose3

def compose3 {A B C D : Type} (h : C -> D) (g : B -> C) (f : A -> B) : A -> D

Composition of three functions: h ∘ g ∘ f.

compose4

def compose4 {A B C D E : Type} (k : D -> E) (h : C -> D) (g : B -> C) (f : A -> B) : A -> E

Composition of four functions: k ∘ h ∘ g ∘ f.

compose3Assoc

def compose3Assoc {A B C D : Type} (h : C -> D) (g : B -> C) (f : A -> B) : compose3 h g f ≡ compose (compose h g) f

The triple composite equals the left-associated composite: compose3 h g f = (h ∘ g) ∘ f.

onApply

def onApply {A B C : Type} (f : B -> B -> C) (g : A -> B) (x : A) (y : A) : on f g x y ≡ f (g x) (g y)

The on combinator unfolds: on f g x y = f (g x) (g y).

onId

def onId {A C : Type} (f : A -> A -> C) : on f (fun (x : A) => x) ≡ f

Using on with the identity function gives back the binary function: on f id = f.

funPathSym

def funPathSym {A B : Type} {f g : A -> B} (p : f ≡ g) : (fun (x : A) => sym (happlyImpl p x)) ≡ (fun (x : A) => happlyImpl (sym p) x)

Pointwise paths of an inverted function path are the inverses of its pointwise paths.

succ_injective

def succ_injective : isInjective Nat Nat succ

The successor function on natural numbers is injective.

not_injective

def not_injective : isInjective Bool Bool not

Boolean negation is injective.

not_surjective

def not_surjective : isSurjective Bool Bool not

Boolean negation is surjective.

not_bijective

def not_bijective : isBijective Bool Bool not

Boolean negation is bijective.

not_hasSection

def not_hasSection : hasSection Bool Bool not

Boolean negation is its own section.

not_hasRetraction

def not_hasRetraction : hasRetraction Bool Bool not

Boolean negation is its own retraction.

not_isIso

def not_isIso : isIso Bool Bool not

Boolean negation is an isomorphism, with itself as inverse.

pointwiseEq

def pointwiseEq {A B : Type} (f g : A -> B) (h : (x : A) -> f x ≡ g x) : f ≡ g

Builds a path f = g from pointwise paths f x = g x (function extensionality).

pointwiseRefl

def pointwiseRefl {A B : Type} (f : A -> B) : (x : A) -> f x ≡ f x

Pointwise reflexivity: f x = f x for every x.

pointwiseSym

def pointwiseSym {A B : Type} (f g : A -> B) (h : (x : A) -> f x ≡ g x) : (x : A) -> g x ≡ f x

Pointwise symmetry: from f x = g x for all x, get g x = f x for all x.

pointwiseTrans

def pointwiseTrans {A B : Type} (f g h : A -> B) (p : (x : A) -> f x ≡ g x) (q : (x : A) -> g x ≡ h x) : (x : A) -> f x ≡ h x

Pointwise transitivity: from f x = g x and g x = h x for all x, get f x = h x for all x.

funSpaceRefl

def funSpaceRefl {A B : Type} (f : A -> B) : f ≡ f

The reflexivity path on a function.

funSpaceSym

def funSpaceSym {A B : Type} {f g : A -> B} (p : f ≡ g) : g ≡ f

Inverts a path between functions: f = g gives g = f.

funSpaceCong

def funSpaceCong {A B C : Type} {f g : A -> B} (h : B -> C) (p : f ≡ g) : compose h f ≡ compose h g

Postcomposition respects paths: f = g implies h ∘ f = h ∘ g.

funSpaceCongDomain

def funSpaceCongDomain {A B C : Type} {f g : B -> C} (h : A -> B) (p : f ≡ g) : compose f h ≡ compose g h

Precomposition respects paths: f = g implies f ∘ h = g ∘ h.

isEmbedding

def isEmbedding (A : Type) (B : Type) (f : A -> B) : Type

The type saying f is an embedding, here stated as injectivity: f a1 = f a2 implies a1 = a2.

embedding_is_injective

def embedding_is_injective (A : Type) (B : Type) (f : A -> B) (emb : isEmbedding A B f) : isInjective A B f

An embedding is injective.

Retract

def Retract (A : Type) (B : Type) : Type

The type of retractions of A onto B: maps s and r with r (s a) = a, exhibiting A as a retract of B.

retract_id

def retract_id (A : Type) : Retract A A

Every type is a retract of itself via the identity maps.

retract_compose

def retract_compose (A : Type) (B : Type) (C : Type) (rAB : Retract A B) (rBC : Retract B C) : Retract A C

Retracts compose: if A is a retract of B and B of C, then A is a retract of C.

iterateZero

def iterateZero {A : Type} (f : A -> A) (x : A) : iterate zero f x ≡ x

Iterating f zero times is the identity: iterate 0 f x = x.

iterateOne

def iterateOne {A : Type} (f : A -> A) (x : A) : iterate (succ zero) f x ≡ f x

Iterating f once is applying f: iterate 1 f x = f x.

iterateSucc

def iterateSucc {A : Type} (n : Nat) (f : A -> A) (x : A) : iterate (succ n) f x ≡ f (iterate n f x)

One more iteration applies f once more: iterate (n + 1) f x = f (iterate n f x).

iterateId

def iterateId (A : Type) (n : Nat) (x : A) : iterate n (fun (a : A) => a) x ≡ x

Iterating the identity function any number of times returns the input.

isInvolution

def isInvolution (A : Type) (f : A -> A) : Type

The type saying f is an involution: f (f x) = x for every x.

involution_is_iso

def involution_is_iso (A : Type) (f : A -> A) (inv : isInvolution A f) : isIso A A f

An involution is an isomorphism, with itself as inverse.

involution_injective

def involution_injective (A : Type) (f : A -> A) (inv : isInvolution A f) : isInjective A A f

An involution is injective.

involution_surjective

def involution_surjective (A : Type) (f : A -> A) (inv : isInvolution A f) : isSurjective A A f

An involution is surjective.

involution_bijective

def involution_bijective (A : Type) (f : A -> A) (inv : isInvolution A f) : isBijective A A f

An involution is bijective.

not_involution

def not_involution : isInvolution Bool not

Boolean negation is an involution.

isFixedPoint

def isFixedPoint (A : Type) (f : A -> A) (x : A) : Type

The type saying x is a fixed point of f: f x = x.

hasFixedPoint

def hasFixedPoint (A : Type) (f : A -> A) : Type

The type of fixed points of f: some x together with a path f x = x.

idAllFixed

def idAllFixed (A : Type) (x : A) : isFixedPoint A (fun (a : A) => a) x

Every point is a fixed point of the identity function.

constFixed

def constFixed (A : Type) (a : A) : isFixedPoint A (fun (x : A) => a) a

The value a is a fixed point of the constant function at a.

isIdempotent

def isIdempotent (A : Type) (f : A -> A) : Type

The type saying f is idempotent: f (f x) = f x for every x.

constIdempotent

def constIdempotent (A : Type) (a : A) : isIdempotent A (fun (x : A) => a)

Every constant function is idempotent.

idIdempotentFn

def idIdempotentFn (A : Type) : isIdempotent A (fun (x : A) => x)

The identity function is idempotent.

isCommutative

def isCommutative (A : Type) (B : Type) (f : A -> A -> B) : Type

The type saying a binary function is commutative: f x y = f y x.

isAssociative

def isAssociative (A : Type) (f : A -> A -> A) : Type

The type saying a binary operation is associative: f (f x y) z = f x (f y z).

isLeftIdentity

def isLeftIdentity (A : Type) (f : A -> A -> A) (e : A) : Type

The type saying e is a left identity for f: f e x = x.

isRightIdentity

def isRightIdentity (A : Type) (f : A -> A -> A) (e : A) : Type

The type saying e is a right identity for f: f x e = x.

add_commutative

def add_commutative : isCommutative Nat Nat add

Natural-number addition is commutative.

add_associative

def add_associative : isAssociative Nat add

Natural-number addition is associative.

add_left_identity

def add_left_identity : isLeftIdentity Nat add zero

Zero is a left identity for natural-number addition.

add_right_identity

def add_right_identity : isRightIdentity Nat add zero

Zero is a right identity for natural-number addition.

and_commutative

def and_commutative : isCommutative Bool Bool and

Boolean conjunction is commutative.

or_commutative

def or_commutative : isCommutative Bool Bool or

Boolean disjunction is commutative.

isLeftCancellable

def isLeftCancellable (A : Type) (B : Type) (f : A -> B) (a : A) : Type

The type saying f can be cancelled at a: f a = f b implies a = b for every b.

injective_implies_cancellable

def injective_implies_cancellable (A : Type) (B : Type) (f : A -> B) (inj : isInjective A B f) (a : A) : isLeftCancellable A B f a

An injective function is left cancellable at every point.

FnGraph

def FnGraph (A : Type) (B : Type) (f : A -> B) : Type

The graph of f as a type: points a paired with the trivial path f a = f a.

graph_elem

def graph_elem (A : Type) (B : Type) (f : A -> B) (a : A) : FnGraph A B f

The element of the graph of f determined by a point a.

graph_fst

def graph_fst (A : Type) (B : Type) (f : A -> B) (g : FnGraph A B f) : A

Projects a point of the graph of f to its domain coordinate.

compose_injective_implies_f

def compose_injective_implies_f (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (gfInj : isInjective A C (compose g f)) : isInjective A B f

If g ∘ f is injective, then f is injective.

surjective_compose_left

def surjective_compose_left (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (h : isSurjective A C (compose g f)) : isSurjective B C g

If g ∘ f is surjective, then g is surjective.

FnRel

def FnRel (A : Type) (B : Type) : Type 1

The type of binary relations between A and B, valued in types.

isFunctional

def isFunctional (A : Type) (B : Type) (R : FnRel A B) : Type

The type saying a relation is functional: each a is related to at most one b (up to paths).

isTotalRel

def isTotalRel (A : Type) (B : Type) (R : FnRel A B) : Type

The type saying a relation is total: each a is related to some chosen b.

graphRel

def graphRel (A : Type) (B : Type) (f : A -> B) : FnRel A B

The graph relation of f: a is related to b when f a = b.

graphRel_functional

def graphRel_functional (A : Type) (B : Type) (f : A -> B) : isFunctional A B (graphRel A B f)

The graph relation of a function is functional.

graphRel_total

def graphRel_total (A : Type) (B : Type) (f : A -> B) : isTotalRel A B (graphRel A B f)

The graph relation of a function is total.

Pred

def Pred (A : Type) : Type 1

The type of type-valued predicates on A.

preimage_pred

def preimage_pred (A : Type) (B : Type) (f : A -> B) (P : Pred B) : Pred A

The preimage of a predicate P on B along f: holds at a when P (f a) holds.

preimageIdPred

def preimageIdPred (A : Type) (P : Pred A) : preimage_pred A A (fun (x : A) => x) P ≡ P

Pulling back a predicate along the identity function gives the same predicate.

preimageComposePred

def preimageComposePred (A : Type) (B : Type) (C : Type) (g : B -> C) (f : A -> B) (P : Pred C) : preimage_pred A C (compose g f) P ≡ preimage_pred A B f (preimage_pred B C g P)

Pulling back along g ∘ f is pulling back along g and then along f.

endo_compose

def endo_compose {A : Type} (g : A -> A) (f : A -> A) : A -> A

Composition of two endomorphisms of A.

endoComposeAssoc

def endoComposeAssoc {A : Type} (h : A -> A) (g : A -> A) (f : A -> A) : endo_compose h (endo_compose g f) ≡ endo_compose (endo_compose h g) f

Composition of endomorphisms is associative.

endoComposeIdLeft

def endoComposeIdLeft {A : Type} (f : A -> A) : endo_compose (fun (x : A) => x) f ≡ f

The identity is a left unit for endomorphism composition.

endoComposeIdRight

def endoComposeIdRight {A : Type} (f : A -> A) : endo_compose f (fun (x : A) => x) ≡ f

The identity is a right unit for endomorphism composition.

endo_power

def endo_power {A : Type} (f : A -> A) (n : Nat) : A -> A

The n-th power of an endomorphism: f composed with itself n times.

endoPowerZero

def endoPowerZero {A : Type} (f : A -> A) (x : A) : endo_power f zero x ≡ x

The zeroth power of an endomorphism is the identity: f^0 x = x.

endoPowerOne

def endoPowerOne {A : Type} (f : A -> A) (x : A) : endo_power f (succ zero) x ≡ f x

The first power of an endomorphism is the endomorphism itself: f^1 x = f x.

endoPowerSucc

def endoPowerSucc {A : Type} (f : A -> A) (n : Nat) (x : A) : endo_power f (succ n) x ≡ f (endo_power f n x)

The successor power applies f once more: f^(n + 1) x = f (f^n x).

depFunExtSym

def depFunExtSym {A : Type} {B : A -> Type} {f g : (x : A) -> B x} (p : f ≡ g) : g ≡ f

Inverts a path between dependent functions: f = g gives g = f.

depFunExtTrans

def depFunExtTrans {A : Type} {B : A -> Type} {f g h : (x : A) -> B x} (p : f ≡ g) (q : g ≡ h) : f ≡ h

Concatenates paths between dependent functions: f = g and g = h give f = h.

self_compose

def self_compose {A : Type} (f : A -> A) : A -> A

Composes an endomorphism with itself: f ∘ f.

selfComposeApply

def selfComposeApply {A : Type} (f : A -> A) (x : A) : self_compose f x ≡ f (f x)

Self-composition unfolds: (f ∘ f) x = f (f x).

involutionSelfCompose

def involutionSelfCompose (A : Type) (f : A -> A) (inv : isInvolution A f) : (fun (x : A) => self_compose f x) ≡ (fun (x : A) => x)

An involution composed with itself is the identity function.

fixedPointIterate

def fixedPointIterate (A : Type) (f : A -> A) (x : A) (fix : f x ≡ x) (n : Nat) : iterate n f x ≡ x

Iterating f from a fixed point stays there: iterate n f x = x whenever f x = x.

pred_retraction_succ

def pred_retraction_succ : hasRetraction Nat Nat succ

The predecessor function is a retraction of the successor: pred (succ n) = n.

mapComposeFn

def mapComposeFn {A B C : Type} (f : B -> C) (g : A -> B) (xs : List A) : map f (map g xs) ≡ map (compose f g) xs

Mapping over a list respects composition: map f (map g xs) = map (f ∘ g) xs.

CommSquare

def CommSquare (A : Type) (B : Type) (C : Type) (D : Type) (f : A -> B) (g : C -> D) (h : A -> C) (k : B -> D) : Type

The type saying a square of functions commutes: k (f a) = g (h a) for every a.

idCommute

def idCommute (A : Type) (B : Type) (f : A -> B) : CommSquare A B A B f f (fun (x : A) => x) (fun (x : B) => x)

The square with f on two opposite sides and identities on the other two commutes.

flipCommutative

def flipCommutative (A : Type) (B : Type) (f : A -> A -> B) (comm : isCommutative A B f) (x : A) (y : A) : flip f x y ≡ f x y

For a commutative binary function, flipping does not change the result: flip f x y = f x y.

pointwiseCompose

def pointwiseCompose {A B C : Type} (h : B -> C) (f g : A -> B) (pw : (x : A) -> f x ≡ g x) : (x : A) -> h (f x) ≡ h (g x)

Postcomposing preserves pointwise paths: f x = g x for all x gives h (f x) = h (g x).

pointwisePrecompose

def pointwisePrecompose {A B C : Type} (h : A -> B) (f g : B -> C) (pw : (x : B) -> f x ≡ g x) : (x : A) -> f (h x) ≡ g (h x)

Precomposing preserves pointwise paths: f x = g x for all x gives f (h x) = g (h x).

doubleEq

def doubleEq (n : Nat) : add n n ≡ double n

Doubling a natural number is adding it to itself: n + n = double n.

mulTwoEq

def mulTwoEq (n : Nat) : mul (succ (succ zero)) n ≡ add n (add n zero)

Multiplying by two unfolds to repeated addition: 2 * n = n + (n + 0).

composeFlipInteraction

def composeFlipInteraction {A B C D : Type} (f : C -> D) (g : A -> B -> C) : (fun (b : B) => fun (a : A) => f (g a b)) ≡ (fun (b : B) => compose f (fun (a : A) => g a b))

Postcomposing f inside a flipped two-argument function equals composing f with each partial application.

idComposeBoth

def idComposeBoth {A : Type} : compose (fun (x : A) => x) (fun (x : A) => x) ≡ (fun (x : A) => x)

The identity composed with itself is the identity: id ∘ id = id.

succPredSucc

def succPredSucc (n : Nat) : succ (pred (succ n)) ≡ succ n

Predecessor cancels successor under succ: succ (pred (succ n)) = succ n.

predZero

def predZero : pred zero ≡ zero

The predecessor of zero is zero.

andIdempotent

def andIdempotent (a : Bool) : and a a ≡ a

Boolean conjunction is idempotent: a && a = a.

orIdempotent

def orIdempotent (a : Bool) : or a a ≡ a

Boolean disjunction is idempotent: a || a = a.

andTrueRightFn

def andTrueRightFn (a : Bool) : and a true ≡ a

True is a right identity for conjunction: a && true = a.

orFalseRightFn

def orFalseRightFn (a : Bool) : or a false ≡ a

False is a right identity for disjunction: a || false = a.

lengthMapFn

def lengthMapFn {A B : Type} (f : A -> B) (xs : List A) : length (map f xs) ≡ length xs

Mapping a function over a list preserves its length.

appendNilFn

def appendNilFn {A : Type} (xs : List A) : append xs nil ≡ xs

Appending the empty list on the right leaves a list unchanged: xs ++ [] = xs.