foundations

isContr

def isContr (A : Type) : Type

A type is contractible when it has a center element to which every element is connected by a path.

fiber

def fiber (A : Type) (B : Type) (f : A -> B) (b : B) : Type

The fiber of f over b: the elements of A that f maps to b, each paired with the path f a ≡ b.

isEquiv

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

A function is an equivalence when every fiber is contractible.

Equiv

def Equiv (A : Type) (B : Type) : Type

The type of equivalences from A to B: a function together with a proof that it is an equivalence.

funExt

def funExt (A : Type) (B : Type) (f : A -> B) (g : A -> B) (h : (x : A) -> f x ≡ g x) : f ≡ g

Function extensionality: two functions are equal when they agree pointwise.

idEquiv

def idEquiv (A : Type) : Equiv A A

The identity function as an equivalence from A to itself.

subst

def subst (A : Type) (P : A -> Type) (a : A) (b : A) (p : a ≡ b) (pa : P a) : P b

Substitution: transport an element of P a along a path a ≡ b to get an element of P b.

equivFun

def equivFun {A : Type} {B : Type} (e : Equiv A B) : A -> B

The underlying function of an equivalence.

equivProof

def equivProof {A : Type} {B : Type} (e : Equiv A B) : isEquiv A B (fst e)

The proof that the underlying function of an equivalence is an equivalence.

pathToEquiv

def pathToEquiv {A : Type} {B : Type} (p : A ≡ B) : A -> B

Turn a path between types A ≡ B into a function A -> B by transport.

curryDep

def curryDep {A : Type} {B : A -> Type} {C : Type} (f : ((x : A) × B x) -> C) (a : A) (b : B a) : C

Curry a function on a dependent pair into a function of two arguments.

uncurryDep

def uncurryDep {A : Type} {B : A -> Type} {C : Type} (f : (a : A) -> B a -> C) (p : (x : A) × B x) : C

Uncurry a two-argument dependent function into a function on dependent pairs.

symP

def symP {A : Type} {a : A} {b : A} (p : a ≡ b) : b ≡ a

Path symmetry: reverse a path a ≡ b into b ≡ a (prelude-local copy).

congP

def congP {A : Type} {B : Type} {a : A} {b : A} (f : A -> B) (p : a ≡ b) : f a ≡ f b

Congruence: apply f to a path a ≡ b to get f a ≡ f b (prelude-local copy).

congSymP

def congSymP {A : Type} {B : Type} {a : A} {b : A} (f : A -> B) (p : a ≡ b) : congP f (symP p) ≡ symP (congP f p)

Applying f to a reversed path is the reverse of applying f to the path: congP f (symP p) ≡ symP (congP f p).

Path.refl

def refl {l : Level} {A : Type l} {a : A} : a ≡ a

The constant path at a point; write refl where a path is expected.

sym

def sym {l : Level} {A : Type l} {a b : A} (p : a ≡ b) : b ≡ a

Path inversion: a path from a to b reversed is a path from b to a.

cong

def cong {l : Level} {m : Level} {A : Type l} {B : Type m} {a b : A} (f : A -> B) (p : a ≡ b) : f a ≡ f b

Applies a function to a path, giving a path between the images of its endpoints.

congS

def congS {A : Type} {a b : A} (f : A -> A) (p : a ≡ b) : f a ≡ f b

Applies an endofunction to a path; cong specialised to A -> A.

cong2

def cong2 {A B : Type} {C : Type} {a1 : A} {a2 : A} {b1 : B} {b2 : B} (f : A -> B -> C) (p : a1 ≡ a2) (q : b1 ≡ b2) : f a1 b1 ≡ f a2 b2

Applies a two-argument function to a pair of paths, giving a path between the images.

symInv

def symInv {A : Type} {a b : A} (p : a ≡ b) : sym (sym p) ≡ p

Inverting a path twice gives back the same path.

transportRefl

def transportRefl {l : Level} {A : Type l} (a : A) : transport (fun i => A) a ≡ a

Transport along a constant line is the identity, up to a path.

substRefl

def substRefl {A : Type} (P : A -> Type) (a : A) (x : P a) : transport (fun i => P a) x ≡ x

Transport in a family along a constant line at a point is the identity, up to a path.

transportConst

def transportConst {A B : Type} (p : A ≡ B) (a : A) : transport (fun i => A) a ≡ a

Transport along the constant line at A returns its argument, up to a path; the given type path is unused.

isProp

def isProp (A : Type) : Type

A type is a proposition when any two of its elements are connected by a path.

isSet

def isSet (A : Type) : Type

A type is a set when any two parallel paths in it are connected by a path.

isPropToIsSet

def isPropToIsSet (A : Type) (h : isProp A) (x : A) (y : A) (p : x ≡ y) (q : x ≡ y) : p ≡ q

Every proposition is a set.

isContrToIsProp

def isContrToIsProp {A : Type} (h : isContr A) : isProp A

Every contractible type is a proposition.

isPropPi

def isPropPi {A : Type} {B : A -> Type} (h : (x : A) -> isProp (B x)) : isProp ((x : A) -> B x)

A dependent function type into a family of propositions is a proposition.

trans

def trans {l : Level} {A : Type l} {a b : A} {c : A} (p : a ≡ b) (q : b ≡ c) : a ≡ c

Path composition: a path from a to b followed by a path from b to c gives a path from a to c.

transIdR

def transIdR {A : Type} {a b : A} (p : a ≡ b) : trans p (fun k => b) ≡ p

Composing a path with the constant path on the right gives back the path.

transIdL

def transIdL {A : Type} {a b : A} (p : a ≡ b) : trans (fun k => a) p ≡ p

Composing a path with the constant path on the left gives back the path.

reflAt

def reflAt {A : Type} (a : A) : a ≡ a

The constant path at an explicitly given point.

rCancel

def rCancel {A : Type} {a b : A} (p : a ≡ b) : trans p (sym p) ≡ reflAt a

A path composed with its inverse is the constant path at its start.

lCancel

def lCancel {A : Type} {a b : A} (p : a ≡ b) : trans (sym p) p ≡ reflAt b

The inverse of a path composed with the path is the constant path at its end.

J

def J {l : Level} {m : Level} {A : Type l} {a : A} (P : (x : A) -> a ≡ x -> Type m) (d : P a (fun i => a)) {b : A} (p : a ≡ b) : P b p

Based path induction: a property of paths out of a, proved for refl, holds for every path out of a.

transportUa

def transportUa (A : Type) (B : Type) (e : Equiv A B) (x : A) : transport (ua e) x ≡ fst e x

Transport along the univalence path of an equivalence applies the equivalence’s function, up to a path.

sigmaMapSnd

def sigmaMapSnd {A : Type} {B : A -> Type} {C : A -> Type} (f : (a : A) -> B a -> C a) (p : (a : A) × B a) : (a : A) × C a

Maps a fiberwise function over the second component of a dependent pair, keeping the first.

happly

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

Turns a path between functions into a pointwise path between their values.

whiskerL

def whiskerL {A : Type} {a b : A} {c : A} (p : a ≡ b) {q : b ≡ c} {r : b ≡ c} (h : q ≡ r) : trans p q ≡ trans p r

Composing a fixed path on the left preserves a path between paths.

whiskerR

def whiskerR {A : Type} {a b : A} {c : A} {p : a ≡ b} {q : a ≡ b} (h : p ≡ q) (r : b ≡ c) : trans p r ≡ trans q r

Composing a fixed path on the right preserves a path between paths.

isDiscrete

def isDiscrete (A : Type) : Type

A type is discrete when paths between any two of its elements are decidable.

isGroupoid

def isGroupoid (A : Type) : Type

A type is a groupoid when any two parallel 2-paths in it are connected by a path.

Acc

data Acc (A : Type) (R : A -> A -> Type) : A -> Type

The accessibility predicate: x is accessible under R when every R-predecessor of x is accessible.

WellFounded

def WellFounded (A : Type) (R : A -> A -> Type) : Type

A relation is well-founded when every element is accessible under it.

congId

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

Applying the identity function to a path gives back the path.

congConst

def congConst {A B : Type} {a b : A} (c : B) (p : a ≡ b) : cong (fun (_ : A) => c) p ≡ refl

Applying a constant function to a path gives the constant path.

pathSigmaNonDep

def pathSigmaNonDep {A B : Type} {x : A × B} {y : A × B} (p : fst x ≡ fst y) (q : snd x ≡ snd y) : x ≡ y

Builds a path between pairs from paths between their components.

fstPath

def fstPath {A : Type} {B : A -> Type} {x : (a : A) × B a} {y : (a : A) × B a} (p : x ≡ y) : fst x ≡ fst y

Projects a path between dependent pairs to a path between their first components.

singlContr

def singlContr {A : Type} (x : A) : isContr ((a : A) × (a ≡ x))

The singleton type of elements with a path to x is contractible.

isPropContr

def isPropContr {A : Type} (h : isContr A) : isProp A

Every contractible type is a proposition.

isPropProd

def isPropProd {A B : Type} (ha : isProp A) (hb : isProp B) : isProp (A × B)

The product of two propositions is a proposition.

funExtSym

def funExtSym (A : Type) (B : Type) (f : A -> B) (g : A -> B) (h : (x : A) -> g x ≡ f x) : g ≡ f

Function extensionality with reversed pointwise paths: from g x ≡ f x for all x, get g ≡ f.

substConst

def substConst (A : Type) (B : Type) (a : A) (b : A) (p : a ≡ b) (x : B) : subst A (fun (z : A) => B) a b p x ≡ x

Substitution in a constant family returns the original value, up to a path.

isPropPi_explicit

def isPropPi_explicit (A : Type) (B : A -> Type) (h : (x : A) -> isProp (B x)) : isProp ((x : A) -> B x)

A dependent function type into a family of propositions is a proposition, with explicit type arguments.

isPropFun

def isPropFun (A : Type) (B : Type) (h : isProp B) : isProp (A -> B)

Functions into a proposition form a proposition.

isPropArrow

def isPropArrow (A : Type) (B : Type) (h : isProp B) : isProp (A -> B)

Functions into a proposition form a proposition, proved pointwise.

congSym

def congSym {A B : Type} {a b : A} (f : A -> B) (p : a ≡ b) : cong f (sym p) ≡ sym (cong f p)

Applying a function to an inverted path equals inverting the applied path.

congConst2

def congConst2 {A : Type} {B : Type} {a b : A} (c : B) (p : a ≡ b) : cong (fun (_ : A) => c) p ≡ refl

Applying a constant function to a path gives the constant path.

transportConstPath

def transportConstPath {A : Type} (a : A) : transport (fun (i : I) => A) a ≡ a

Transport along a constant line is the identity, up to a path.

sndPath

def sndPath {A B : Type} {x : A × B} {y : A × B} (p : x ≡ y) : snd x ≡ snd y

Projects a path between pairs to a path between their second components.

fstMk

def fstMk {A : Type} {B : A -> Type} (a : A) (b : B a) : fst (a, b) ≡ a

The first projection of a pair is its first component.

sndMk

def sndMk {A : Type} {B : A -> Type} (a : A) (b : B a) : snd (a, b) ≡ b

The second projection of a pair is its second component.

idFn

def idFn (A : Type) (a : A) : A

The identity function at an explicit type.

constFn

def constFn (A : Type) (B : Type) (a : A) (b : B) : A

The constant function returning its first argument.

compose

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

Function composition: compose g f applies f and then g.

composeIdL

def composeIdL (A : Type) (B : Type) (f : A -> B) (x : A) : compose (idFn B) f x ≡ f x

Composing with the identity on the left does not change a function’s value.

composeIdR

def composeIdR (A : Type) (B : Type) (f : A -> B) (x : A) : compose f (idFn A) x ≡ f x

Composing with the identity on the right does not change a function’s value.

composeAssoc

def composeAssoc (A : Type) (B : Type) (C : Type) (D : Type) (f : C -> D) (g : B -> C) (h : A -> B) (x : A) : compose f (compose g h) x ≡ compose (compose f g) h x

Function composition is associative.

Not

def Not (A : Type) : Type

Negation: A implies Empty.

notIntro

def notIntro {A : Type} (f : A -> Empty) : Not A

Turns a function into Empty into a negation.

dn_intro

def dn_intro {A : Type} (a : A) : Not (Not A)

Double negation introduction: an element of A refutes Not A.

isPropEmpty

def isPropEmpty : isProp Empty

Empty is a proposition.

isPropNot

def isPropNot (A : Type) : isProp (Not A)

Every negation is a proposition.

isSetToIsPropPath

def isSetToIsPropPath {A : Type} (h : isSet A) (x : A) (y : A) : isProp (x ≡ y)

In a set, every path space is a proposition.

fiberRefl

def fiberRefl (A : Type) (B : Type) (f : A -> B) (a : A) : fiber A B f (f a)

The point a with the constant path is in the fiber of f over f a.

equivRefl

def equivRefl (A : Type) : Equiv A A

The identity equivalence of a type.

funExtDep

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

Dependent function extensionality: pointwise paths give a path between dependent functions.

funExtSym2

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

Function extensionality reversed: pointwise paths from f to g give a path from g to f.

isContrProd

def isContrProd {A B : Type} (ha : isContr A) (hb : isContr B) : isContr (A × B)

The product of two contractible types is contractible.

isContrToIsSet

def isContrToIsSet {A : Type} (h : isContr A) : isSet A

Every contractible type is a set.

mapDec

def mapDec {A B : Type} (f : A -> B) (g : B -> A) (d : Dec A) : Dec B

Transfers a decision along a pair of maps back and forth between two types.

transportSym

def transportSym {A B : Type} (p : A ≡ B) (b : B) : A

Transports an element backwards along a path between types.

transportConst2

def transportConst2 {A : Type} (a : A) : transport Path.refl a ≡ a

Transport along refl is the identity, up to a path.

doubleComp

def doubleComp {A : Type} {a b : A} {c : A} {d : A} (p : a ≡ b) (q : b ≡ c) (r : c ≡ d) : a ≡ d

Composes three consecutive paths.

etaPair

def etaPair {A : Type} {B : A -> Type} (p : (a : A) × B a) : p ≡ p

Every dependent pair is connected to itself by refl.

cong2Refl

def cong2Refl {A B C : Type} (f : A -> B -> C) (a : A) (b : B) : cong2 f (refl : a ≡ a) (refl : b ≡ b) ≡ refl

Applying a binary function to two constant paths gives the constant path.

congComp

def congComp {A B : Type} {C : Type} {a b : A} (g : B -> C) (f : A -> B) (p : a ≡ b) : cong (fun (x : A) => g (f x)) p ≡ cong g (cong f p)

Applying a composite function to a path equals applying the two functions in turn.

symRefl

def symRefl {A : Type} (a : A) : sym (refl : a ≡ a) ≡ refl

The inverse of the constant path is the constant path.

symCong

def symCong {A B : Type} {a b : A} (f : A -> B) (p : a ≡ b) : sym (cong f p) ≡ cong f (sym p)

Inverting an applied path equals applying the function to the inverted path.

isSetPi

def isSetPi {A : Type} {B : A -> Type} (h : (x : A) -> isSet (B x)) : isSet ((x : A) -> B x)

A dependent function type into a family of sets is a set.

isSetProd

def isSetProd {A B : Type} (ha : isSet A) (hb : isSet B) : isSet (A × B)

The product of two sets is a set.

congCompEq

def congCompEq {A B C : Type} {a b : A} (f : B -> C) (g : A -> B) (p : a ≡ b) : cong (fun (x : A) => f (g x)) p ≡ cong f (cong g p)

Applying a composite function to a path equals applying the two functions in turn.

transportPath

def transportPath {A : Type} (B : A -> Type) (a b : A) (p : a ≡ b) (x : B a) : B b

Transports an element of a family along a path in the base.

transportPathRefl

def transportPathRefl {A : Type} (B : A -> Type) (a : A) (x : B a) : transportPath B a a (fun k => a) x ≡ x

Transporting along the constant path in the base is the identity, up to a path.

transportConst3

def transportConst3 {A B : Type} (a1 a2 : A) (p : a1 ≡ a2) (b : B) : transportPath (fun (_ : A) => B) a1 a2 p b ≡ b

Transporting in a constant family along any base path is the identity, up to a path.

substConst2

def substConst2 {A B : Type} {a b : A} (p : a ≡ b) (x : B) : transport (fun i => B) x ≡ x

Transport in a constant family is the identity, up to a path; the given path is unused.

transportFunConst

def transportFunConst {A B : Type} (f : A -> B) : transport (fun (i : I) => A -> B) f ≡ f

Transport of a function along the constant function-type line is the identity, up to a path.

funExtSimple

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

Function extensionality for non-dependent functions with explicit arguments.

isPropSigmaNonDep

def isPropSigmaNonDep {A B : Type} (ha : isProp A) (hb : isProp B) : isProp (A × B)

The product of two propositions is a proposition.

isSetSigmaNonDep

def isSetSigmaNonDep {A B : Type} (ha : isSet A) (hb : isSet B) : isSet (A × B)

The product of two sets is a set.

isPropToIsSet2

def isPropToIsSet2 {A : Type} (h : isProp A) : isSet A

Every proposition is a set, with an implicit type argument.

isSetPath2

def isSetPath2 {A : Type} (h : isGroupoid A) (x y : A) : isSet (x ≡ y)

In a groupoid, every path space is a set.

decNeg

def decNeg (A : Type) (d : Dec A) : Dec (Not A)

Turns a decision on A into a decision on Not A.

isPropDecEmpty

def isPropDecEmpty : isProp (Dec Empty)

Dec Empty is a proposition.

cong3

def cong3 {A B C D : Type} {a1 a2 : A} {b1 b2 : B} {c1 c2 : C} (f : A -> B -> C -> D) (p : a1 ≡ a2) (q : b1 ≡ b2) (r : c1 ≡ c2) : f a1 b1 c1 ≡ f a2 b2 c2

Applies a three-argument function to three paths, giving a path between the images.

equivFunApp

def equivFunApp {A B : Type} (e : Equiv A B) (a : A) : B

Applies the forward function of an equivalence.

equivId

def equivId (A : Type) : Equiv A A

The identity equivalence of a type.

equivFiberIsContr

def equivFiberIsContr {A B : Type} (e : Equiv A B) (b : B) : isContr (fiber A B (fst e) b)

Every fiber of an equivalence’s function is contractible.

flip

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

Swaps the two arguments of a binary function.

on

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

Applies a binary function after mapping both arguments through g.

mapFst

def mapFst {A B C : Type} (f : A -> C) (p : A × B) : C × B

Applies a function to the first component of a pair.

mapSnd

def mapSnd {A B C : Type} (f : B -> C) (p : A × B) : A × C

Applies a function to the second component of a pair.

prodMap

def prodMap {A B C D : Type} (f : A -> C) (g : B -> D) (p : A × B) : C × D

Applies one function to each component of a pair.

swap

def swap {A B : Type} (p : A × B) : B × A

Swaps the components of a pair.

diag

def diag {A : Type} (a : A) : A × A

The diagonal: pairs an element with itself.

curry

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

Turns a function on pairs into a curried two-argument function.

uncurry

def uncurry {A B C : Type} (f : A -> B -> C) (p : A × B) : C

Turns a curried two-argument function into a function on pairs.

isPropFun2

def isPropFun2 (A B C : Type) (h : isProp C) : isProp (A -> B -> C)

Two-argument functions into a proposition form a proposition.

isSetFun

def isSetFun {A B : Type} (h : isSet B) : isSet (A -> B)

Functions into a set form a set.

transportConstConst

def transportConstConst {A : Type} (a : A) : transport (fun (i : I) => A) (transport (fun (i : I) => A) a) ≡ a

Transporting twice along a constant line is the identity, up to a path.

transportConstPSym

def transportConstPSym {A B : Type} (p : A ≡ B) (a : A) : transport (fun (i : I) => A) a ≡ a

Transport along the constant line at A is the identity, up to a path; the given type path is unused.

transportPathComp

def transportPathComp {A : Type} (B : A -> Type) (a : A) (x : B a) : transportPath B a a (fun k => a) (transportPath B a a (fun k => a) x) ≡ x

Transporting twice along the constant base path is the identity, up to a path.

transportSigmaConst

def transportSigmaConst {A B : Type} (p : A × B) : transport (fun (i : I) => A × B) p ≡ p

Transport of a pair along a constant product line is the identity, up to a path.

transportPairConst

def transportPairConst {A B : Type} (a : A) (b : B) : transport (fun (i : I) => A × B) (a, b) ≡ (a, b)

Transport of an explicit pair along a constant product line returns the pair, up to a path.

transportPairFst

def transportPairFst {A B : Type} (a : A) (b : B) : fst (transport (fun (i : I) => A × B) (a, b)) ≡ a

After transport along a constant product line, the first component is unchanged, up to a path.

transportPairSnd

def transportPairSnd {A B : Type} (a : A) (b : B) : snd (transport (fun (i : I) => A × B) (a, b)) ≡ b

After transport along a constant product line, the second component is unchanged, up to a path.

transportPiConst

def transportPiConst {A : Type} {B : A -> Type} (f : (x : A) -> B x) : transport (fun (i : I) => (x : A) -> B x) f ≡ f

Transport of a dependent function along a constant line is the identity, up to a path.

transportPiApp

def transportPiApp {A B : Type} (f : A -> B) (a : A) : (transport (fun (i : I) => A -> B) f) a ≡ f a

A function transported along a constant line agrees with the original at every argument.

JConst

def JConst {A : Type} (a : A) (B : Type) (d : B) (b : A) (p : a ≡ b) : J (fun (x : A) => fun (_ : a ≡ x) => B) d p ≡ d

Path induction with a motive that ignores the path returns the base case, up to a path.

happlyFunExtDep

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

happly undoes funExtDep: the pointwise paths come back unchanged.

funExtDepHapply

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

funExtDep undoes happly: the path between functions comes back unchanged.

pathIndBase

def pathIndBase {A : Type} {a : A} (P : (x : A) -> a ≡ x -> Type) (d : P a (fun i => a)) : P a (fun i => a)

Returns the base case of path induction at refl.

pathIndTransport

def pathIndTransport {A : Type} {a : A} (P : (x : A) -> a ≡ x -> Type) (d : P a (fun i => a)) {b : A} (p : a ≡ b) : P b p

Transports a base case along a path using J.

substConstConst

def substConstConst {A B : Type} (a b c : A) (p : a ≡ b) (q : b ≡ c) (x : B) : subst A (fun (_ : A) => B) b c q (subst A (fun (_ : A) => B) a b p x) ≡ x

Substituting twice in a constant family returns the original value, up to a path.

substRefl2

def substRefl2 {A : Type} (P : A -> Type) (a : A) (x : P a) : subst A P a a (fun k => a) x ≡ x

Substitution along the constant path is the identity, up to a path.

substCong

def substCong {A B : Type} (Q : B -> Type) (f : A -> B) {a b : A} (p : a ≡ b) (x : Q (f a)) : subst B Q (f a) (f b) (cong f p) x ≡ transport (fun i => Q (f (p i))) x

Substitution along an applied path is transport along the composite family.

congReflAt

def congReflAt {A B : Type} (f : A -> B) (a : A) : cong f (reflAt a) ≡ reflAt (f a)

Applying a function to a constant path gives the constant path at the image.

pathSigmaNonDepRefl

def pathSigmaNonDepRefl {A B : Type} (x : A × B) : pathSigmaNonDep {A} {B} {x} {x} refl refl ≡ refl

Building a pair path from two constant paths gives the constant path.

isContrPath

def isContrPath {A : Type} (h : isContr A) (x : A) (y : A) : isContr (x ≡ y)

Every path space of a contractible type is contractible.

isContrPi

def isContrPi {A : Type} {B : A -> Type} (h : (x : A) -> isContr (B x)) : isContr ((x : A) -> B x)

A dependent function type into a family of contractible types is contractible.

doubleCompTrans

def doubleCompTrans {A : Type} {a b c d : A} (p : a ≡ b) (q : b ≡ c) (r : c ≡ d) : doubleComp p q r ≡ trans (trans p q) r

Triple composition unfolds to two nested binary compositions.

whiskerLUnfold

def whiskerLUnfold {A : Type} {a b c : A} (p : a ≡ b) {q : b ≡ c} {r : b ≡ c} (h : q ≡ r) : whiskerL p h ≡ (fun j => trans p (h j))

Unfolds left whiskering to its definition.

whiskerRUnfold

def whiskerRUnfold {A : Type} {a b c : A} {p : a ≡ b} {q : a ≡ b} (h : p ≡ q) (r : b ≡ c) : whiskerR h r ≡ (fun j => trans (h j) r)

Unfolds right whiskering to its definition.

isPropPathFromSet

def isPropPathFromSet {A : Type} (hA : isSet A) (x y : A) : isProp (x ≡ y)

In a set, every path space is a proposition.

accEmpty

def accEmpty (A : Type) (x : A) : Acc A (fun (_ : A) => fun (_ : A) => Empty) x

Every element is accessible under the empty relation.

wfEmpty

def wfEmpty (A : Type) : WellFounded A (fun (_ : A) => fun (_ : A) => Empty)

The empty relation is well-founded.

isPropFun3

def isPropFun3 {A B C D : Type} (h : isProp D) : isProp (A -> B -> C -> D)

Three-argument functions into a proposition form a proposition.

isPropProdFun

def isPropProdFun {A B C D : Type} (hC : isProp C) (hD : isProp D) : isProp ((A -> C) × (B -> D))

A pair of functions into propositions forms a proposition.

congCompose

def congCompose {A B C : Type} {a b : A} (g : B -> C) (f : A -> B) (p : a ≡ b) : cong (fun (x : A) => compose g f x) p ≡ cong (fun (x : A) => g (f x)) p

Applying compose g f to a path equals applying the lambda composite.

decProd

def decProd {A B : Type} (dA : Dec A) (dB : Dec B) : Dec (A × B)

Decides a product from decisions on both components.

transportReflFam1

def transportReflFam1 {A : Type} (x : A) : transport (fun i => A) x ≡ x

Transport along a constant line is the identity, up to a path.

transportReflFamTwice

def transportReflFamTwice {A : Type} (a : A) : transport (fun i => A) (transport (fun i => A) a) ≡ a

Transporting twice along a constant line is the identity, up to a path.

transportConstFam

def transportConstFam {A B : Type} (b : B) : transport (fun i => B) b ≡ b

Transport along a constant line is the identity, up to a path.

transportConstFamFull

def transportConstFamFull {A B : Type} (p : A ≡ B) (b : B) : transport (fun i => B) b ≡ b

Transport along the constant line at B is the identity, up to a path; the given type path is unused.

Jsimple

def Jsimple {A : Type} {a : A} (P : A -> Type) (d : P a) {b : A} (p : a ≡ b) : P b

Non-dependent path induction: transports an element of P a to P b along a path.

JsimpleRefl

def JsimpleRefl {A : Type} {a : A} (P : A -> Type) (d : P a) : Jsimple P d (reflAt a) ≡ transport (fun i => P a) d

Non-dependent path induction along a constant path is transport along the constant line.

substReflTwice

def substReflTwice {A : Type} (P : A -> Type) (a : A) (x : P a) : transport (fun i => P a) (transport (fun i => P a) x) ≡ x

Transporting twice along a constant line in a family is the identity, up to a path.

substApp

def substApp {A B : Type} (f : A -> B) (a : A) : transport (fun i => B) (f a) ≡ f a

Transport of a function value along a constant line is the identity, up to a path.

funextDep

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

Dependent function extensionality: pointwise paths give a path between dependent functions.

funextNondep

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

Function extensionality: pointwise paths give a path between functions.

happlyV140N

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

Turns a path between dependent functions into a pointwise path.

funEtaN

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

Eta for functions: a function equals its eta-expansion.

funEtaDepN

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

Eta for dependent functions: a function equals its eta-expansion.

funEta2N

def funEta2N {A B C : Type} (f : A -> B -> C) : f ≡ (fun (x : A) => fun (y : B) => f x y)

Eta for two-argument functions: a function equals its eta-expansion.

funEta3N

def funEta3N {A B C D : Type} (f : A -> B -> C -> D) : f ≡ (fun (x : A) => fun (y : B) => fun (z : C) => f x y z)

Eta for three-argument functions: a function equals its eta-expansion.

contrToPropN

def contrToPropN {A : Type} (h : isContr A) : isProp A

Every contractible type is a proposition.

contrPathTrivialN

def contrPathTrivialN {A : Type} (h : isContr A) (x y : A) : x ≡ y

Any two elements of a contractible type are connected by a path.

transportReflFun

def transportReflFun {A B : Type} (f : A -> B) : transport (fun i => A -> B) f ≡ f

Transport of a function along a constant line is the identity, up to a path.

transportReflSigmaPair

def transportReflSigmaPair {A B : Type} (p : (a : A) × B) : transport (fun i => (a : A) × B) p ≡ p

Transport of a pair along a constant line is the identity, up to a path.

transportReflEmpty

def transportReflEmpty (e : Empty) : transport (fun i => Empty) e ≡ e

Transport along the constant line at Empty is the identity.

reflPolyEq

def reflPolyEq {A : Type} (a : A) : reflAt a ≡ reflAt a

The refl and lambda forms of the constant path agree.

reflPolyEq2

def reflPolyEq2 {A : Type} (a : A) : reflAt a ≡ reflAt a

The lambda and reflAt forms of the constant path agree.

reflPolyEq3

def reflPolyEq3 {A : Type} (a : A) : reflAt a ≡ reflAt a

The refl and reflAt forms of the constant path agree.

sigmaPathNondep

def sigmaPathNondep {A B : Type} {p q : (a : A) × B} (fp : fst p ≡ fst q) (sp : snd p ≡ snd q) : p ≡ q

Builds a path between pairs from paths between their components.

sigmaPathReflV140

def sigmaPathReflV140 {A B : Type} (p : (a : A) × B) : p ≡ p

Every pair is connected to itself by refl.

apNV140

def apNV140 {A B : Type} {a b : A} (f : A -> B) (p : a ≡ b) : f a ≡ f b

Applies a function to a path; an alias of cong.

apNRefl

def apNRefl {A B : Type} (f : A -> B) (a : A) : apNV140 f (reflAt a) ≡ reflAt (f a)

Applying a function to a constant path gives the constant path at the image.

apNId

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

Applying the identity function to a path gives back the path.

apNConst

def apNConst {A B : Type} {a b : A} (c : B) (p : a ≡ b) : apNV140 (fun (_ : A) => c) p ≡ reflAt c

Applying a constant function to a path gives the constant path.

fstPairV140

def fstPairV140 {A B : Type} (a : A) (b : B) : fst ((a, b) : (x : A) × B) ≡ a

The first projection of a pair is its first component.

sndPairV140

def sndPairV140 {A B : Type} (a : A) (b : B) : snd ((a, b) : (x : A) × B) ≡ b

The second projection of a pair is its second component.

isPropUnit

def isPropUnit : isProp Unit

The unit type is a proposition: any two elements are equal.