path

transRefl

def transRefl {l : Level} {A : Type l} {a : A} {b : A} (p : a ≡ b) : trans p refl ≡ p

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

reflTrans

def reflTrans {A : Type} {a : A} {b : A} (p : a ≡ b) : trans refl p ≡ p

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

transportRefl2

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

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

sigmaPath

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

Builds a path between non-dependent pairs from paths between their components.

succPath

def succPath {m : Nat} {n : Nat} (p : succ m ≡ succ n) : m ≡ n

succ is injective on paths: a path from succ m to succ n gives a path from m to n.

notInvol

def notInvol (b : Bool) : not (not b) ≡ b

Boolean negation is an involution: not (not b) is b.

notPath

def notPath {a : Bool} {b : Bool} (p : a ≡ b) : not a ≡ not b

Applies boolean negation to a path.

mapIdPath

def mapIdPath {A : Type} (f : A -> A) (p : (x : A) -> f x ≡ x) (xs : List A) : map f xs ≡ xs

Mapping a function that is pointwise the identity over a list gives back the list.

mapIdNat

def mapIdNat (xs : List Nat) : map (fun (x : Nat) => x) xs ≡ xs

Mapping the identity function over a list of naturals gives back the list.

happly2

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

Turns a path between non-dependent functions into a pointwise path.

transSymR

def transSymR {A : Type} {a : A} {b : A} (p : a ≡ b) : trans p (sym p) ≡ refl

A path composed with its inverse is refl.

transSymL

def transSymL {A : Type} {a : A} {b : A} (p : a ≡ b) : trans (sym p) p ≡ refl

The inverse of a path composed with the path is refl.

congTrans

def congTrans {A : Type} {B : Type} {a : A} {b : A} {c : A} (f : A -> B) (p : a ≡ b) (q : b ≡ c) : cong f (trans p q) ≡ trans (cong f p) (cong f q)

Applying a function to a composite path equals composing the applied paths.

symTransMotive

def symTransMotive {A : Type} {a : A} {b : A} (p : a ≡ b) (x : A) (r : b ≡ x) : Type

Motive for proving symTrans by path induction: inverting p · r equals r⁻¹ · p⁻¹.

symTrans

def symTrans {A : Type} {a : A} {b : A} {c : A} (p : a ≡ b) (q : b ≡ c) : sym (trans p q) ≡ trans (sym q) (sym p)

Inverting a composite path equals composing the inverses in reverse order.

transportTrans

def transportTrans {A B C : Type} (p : A ≡ B) (q : B ≡ C) (x : A) : transport (trans p q) x ≡ transport q (transport p x)

Transport along a composite type path equals transporting along each path in turn.

transAssoc

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

Path composition is associative.

funExtComp

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

Function extensionality from two composed pointwise paths, giving a path from f to h.

ap2

def ap2 {A : Type} {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 two paths, giving a path between the images.

apSym

def apSym {A : Type} {B : Type} {a : 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.

transportConstFamily

def transportConstFamily (B : Type) (b : B) : transport (fun (_ : I) => B) b ≡ b

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

PathOver

def PathOver (A : Type) (P : A -> Type) {x : A} {y : A} (p : x ≡ y) (a : P x) (b : P y) : Type

A path over p from a to b: transporting a along p in the family P gives b.

addSuccPath

def addSuccPath (m : Nat) (n : Nat) : add m (succ n) ≡ succ (add m n)

Adding a successor on the right is the successor of the sum, as a path.

consPath

def consPath {A : Type} {x : A} {y : A} {xs : List A} {ys : List A} (p : x ≡ y) (q : xs ≡ ys) : cons x xs ≡ cons y ys

cons preserves paths: paths between heads and between tails give a path between the lists.

mapIdFn

def mapIdFn {A : Type} (xs : List A) : map (fun (x : A) => x) xs ≡ xs

Mapping the identity function over a list gives back the list.

succAddComm

def succAddComm (m : Nat) (n : Nat) : succ (add m n) ≡ add m (succ n)

The successor of a sum equals adding a successor on the right, as a path.

addCancelL

def addCancelL (k : Nat) (m : Nat) (n : Nat) (p : add k m ≡ add k n) : m ≡ n

Addition is cancellative on the left: a path from k + m to k + n gives a path from m to n.

addZeroRPath

def addZeroRPath (m : Nat) : add m zero ≡ m

Adding zero on the right leaves a natural number unchanged, as a path.

succCong

def succCong {m : Nat} {n : Nat} (p : m ≡ n) : succ m ≡ succ n

Applies succ to a path between naturals.

predCong

def predCong {m : Nat} {n : Nat} (p : m ≡ n) : pred m ≡ pred n

Applies pred to a path between naturals.

addCongL

def addCongL {m : Nat} {n : Nat} (p : m ≡ n) (k : Nat) : add m k ≡ add n k

Addition preserves a path in its left argument.

addCongR

def addCongR (m : Nat) {n : Nat} {k : Nat} (p : n ≡ k) : add m n ≡ add m k

Addition preserves a path in its right argument.

mulCongL

def mulCongL {m : Nat} {n : Nat} (p : m ≡ n) (k : Nat) : mul m k ≡ mul n k

Multiplication preserves a path in its left argument.

mulCongR

def mulCongR (m : Nat) {n : Nat} {k : Nat} (p : n ≡ k) : mul m n ≡ mul m k

Multiplication preserves a path in its right argument.

andCong

def andCong {a : Bool} {b : Bool} {c : Bool} {d : Bool} (p : a ≡ b) (q : c ≡ d) : and a c ≡ and b d

Boolean and preserves paths in both arguments.

orCong

def orCong {a : Bool} {b : Bool} {c : Bool} {d : Bool} (p : a ≡ b) (q : c ≡ d) : or a c ≡ or b d

Boolean or preserves paths in both arguments.

appendCong

def appendCong {A : Type} {xs : List A} {ys : List A} {zs : List A} {ws : List A} (p : xs ≡ ys) (q : zs ≡ ws) : append xs zs ≡ append ys ws

List append preserves paths in both arguments.

mapCong

def mapCong {A : Type} {B : Type} (f : A -> B) {xs : List A} {ys : List A} (p : xs ≡ ys) : map f xs ≡ map f ys

map f preserves a path between lists.

lengthCong

def lengthCong {A : Type} {xs : List A} {ys : List A} (p : xs ≡ ys) : length xs ≡ length ys

length preserves a path between lists.

reverseCong

def reverseCong {A : Type} {xs : List A} {ys : List A} (p : xs ≡ ys) : reverse xs ≡ reverse ys

reverse preserves a path between lists.

congTransSucc

def congTransSucc (p : zero ≡ zero) (q : zero ≡ zero) : cong succ (trans p q) ≡ trans (cong succ p) (cong succ q)

Applying succ to a composite of loops at zero equals composing the applied loops.

transportCong

def transportCong {A B : Type} (f : A -> B) (P : B -> Type) {a b : A} (p : a ≡ b) (x : P (f a)) : transport (fun i => P (f (p i))) x ≡ transport (fun i => P (f (p i))) x

Trivial reflexivity witness for transport along the family P (f (p i)) of an applied path.

congConstFn

def congConstFn {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 refl.

pathSigmaFst

def pathSigmaFst {A : Type} {B : A -> Type} {x 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.

happlyPath

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

Turns a path between non-dependent functions into a pointwise path.

funExtHapply

def funExtHapply {A B : Type} {f g : A -> B} (p : f ≡ g) : funExt A B f g (fun x => happlyPath p x) ≡ p

Function extensionality undoes happly: funExt of the pointwise paths of p is p.

transportReflPath

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

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

transportSymType

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

Transports an element backwards along a path between types.

addCong2

def addCong2 {m1 m2 n1 n2 : Nat} (p : m1 ≡ m2) (q : n1 ≡ n2) : add m1 n1 ≡ add m2 n2

Addition preserves paths in both arguments.

mulCong2

def mulCong2 {m1 m2 n1 n2 : Nat} (p : m1 ≡ m2) (q : n1 ≡ n2) : mul m1 n1 ≡ mul m2 n2

Multiplication preserves paths in both arguments.

congRefl

def congRefl {A B : Type} (f : A -> B) (a : A) : cong f (refl : a ≡ a) ≡ (refl : f a ≡ f a)

Applying a function to refl gives refl.

symReflPath

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

The inverse of refl is refl.

doubleCong

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

Applying g after applying f to a path equals applying their composite.

congAddR

def congAddR (n : Nat) {m1 m2 : Nat} (p : m1 ≡ m2) : add m1 n ≡ add m2 n

Adding a fixed number on the right preserves a path.

congAddL

def congAddL (n : Nat) {m1 m2 : Nat} (p : m1 ≡ m2) : add n m1 ≡ add n m2

Adding a fixed number on the left preserves a path.

transportConstNat

def transportConstNat (n : Nat) : transport (fun (i : I) => Nat) n ≡ n

Transport along the constant Nat line is the identity.

transportConstBool

def transportConstBool (b : Bool) : transport (fun (i : I) => Bool) b ≡ b

Transport along the constant Bool line is the identity.

transportConstList

def transportConstList {A : Type} (xs : List A) : transport (fun (i : I) => List A) xs ≡ xs

Transport along a constant List line is the identity.

transportConstFun

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

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

transportConstSigma

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

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

transportConstUnit

def transportConstUnit (u : Unit) : transport (fun (i : I) => Unit) u ≡ u

Transport along the constant Unit line is the identity.

transportConstPair

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

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

pathConcat

def pathConcat {A : Type} {a b c : A} (p : a ≡ b) (q : b ≡ c) : a ≡ c

Path composition; an alias of trans.

pathInv

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

Path inversion; an alias of sym.

pathConcatReflR

def pathConcatReflR {A : Type} {a b : A} (p : a ≡ b) : pathConcat p refl ≡ p

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

pathConcatReflL

def pathConcatReflL {A : Type} {a b : A} (p : a ≡ b) : pathConcat refl p ≡ p

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

pathInvPathInv

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

Inverting a path twice gives back the path.

pathConcatPathInvR

def pathConcatPathInvR {A : Type} {a b : A} (p : a ≡ b) : pathConcat p (pathInv p) ≡ refl

A path composed with its inverse is refl.

pathConcatPathInvL

def pathConcatPathInvL {A : Type} {a b : A} (p : a ≡ b) : pathConcat (pathInv p) p ≡ refl

The inverse of a path composed with the path is refl.

funExtConst

def funExtConst {A B : Type} (c : B) : (fun (_ : A) => c) ≡ (fun (_ : A) => c)

A constant function is connected to itself by refl.

funExtCompose

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

A composite function is connected to itself by refl.

sigmaPathRefl

def sigmaPathRefl {A B : Type} (x : (a : A) × B) : sigmaPath {A} {B} {x} {x} refl refl ≡ refl

Building a pair path from two refl paths gives refl.

sigmaPathFst

def sigmaPathFst {A B : Type} {x : (a : A) × B} {y : (a : A) × B} (p : fst x ≡ fst y) (q : snd x ≡ snd y) : (fun i => fst (sigmaPath p q i)) ≡ p

The first projection of a pair path built by sigmaPath is the given first-component path.

sigmaPathSnd

def sigmaPathSnd {A B : Type} {x : (a : A) × B} {y : (a : A) × B} (p : fst x ≡ fst y) (q : snd x ≡ snd y) : (fun i => snd (sigmaPath p q i)) ≡ q

The second projection of a pair path built by sigmaPath is the given second-component path.

sigmaPathTrans

def sigmaPathTrans {A B : Type} {x y z : (a : A) × B} (p1 : fst x ≡ fst y) (q1 : snd x ≡ snd y) (p2 : fst y ≡ fst z) (q2 : snd y ≡ snd z) : sigmaPath (trans p1 p2) (trans q1 q2) ≡ trans (sigmaPath p1 q1) (sigmaPath p2 q2)

Composing pair paths is done componentwise.

whiskerLRefl

def whiskerLRefl {A : Type} {a b c : A} (p : a ≡ b) (q : b ≡ c) : whiskerL p (refl : q ≡ q) ≡ refl

Left whiskering the refl 2-path gives refl.

constFunPath

def constFunPath {A B : Type} (b1 b2 : B) (p : b1 ≡ b2) : (fun (_ : A) => b1) ≡ (fun (_ : A) => b2)

A path between two values gives a path between the corresponding constant functions.

composePath

def composePath {A B C : Type} {f1 f2 : A -> B} {g1 g2 : B -> C} (pf : f1 ≡ f2) (pg : g1 ≡ g2) : (fun (x : A) => g1 (f1 x)) ≡ (fun (x : A) => g2 (f2 x))

Paths between two pairs of functions give a path between their composites.

reflRefl

def reflRefl {A : Type} (a : A) : (refl : a ≡ a) ≡ (refl : a ≡ a)

The 2-path from refl to refl given by refl.

transportConstInd

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

Transport in a constant family is the identity, up to a path, whatever the base path.

happlyFunExt

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

happly undoes function extensionality: the pointwise path at x is h x.

addCancelR

def addCancelR (k : Nat) (m : Nat) (n : Nat) (p : add m k ≡ add n k) : m ≡ n

Addition is cancellative on the right: a path from m + k to n + k gives a path from m to n.

xorCong

def xorCong {a b c d : Bool} (p : a ≡ b) (q : c ≡ d) : xor a c ≡ xor b d

Boolean xor preserves paths in both arguments.

notCong

def notCong {a b : Bool} (p : a ≡ b) : not a ≡ not b

Applies boolean negation to a path.

someCongPath

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

Applies just to a path.

mapOptionNonePath

def mapOptionNonePath {A B : Type} (f : A -> B) : Option.map f (none : Option A) ≡ (none : Option B)

Mapping a function over nothing gives nothing.

mapOptionSomePath

def mapOptionSomePath {A B : Type} (f : A -> B) (a : A) : Option.map f (some a) ≡ some (f a)

Mapping a function over just a gives just (f a).

congCong

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

Applying g after applying f to a path equals applying their composite.

symOfCong

def symOfCong {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.

congPreservesSym

def congPreservesSym {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.

fstPairMkPath

def fstPairMkPath {A B : Type} (a : A) (b : B) : fstPair (mkPair a b) ≡ a

The first projection of mkPair a b is a.

sndPairMkPath

def sndPairMkPath {A B : Type} (a : A) (b : B) : sndPair (mkPair a b) ≡ b

The second projection of mkPair a b is b.

transportComposeConst

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

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

apRefl

def apRefl {A B : Type} (f : A -> B) (a : A) : cong f (refl : a ≡ a) ≡ (refl : f a ≡ f a)

Applying a function to refl gives refl.

apSymPath

def apSymPath {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.

apId

def apId {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.

apConst

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

Applying a constant function to a path gives refl.

apCompose

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

Applying g after applying f to a path equals applying their composite.

ap2Refl

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

Applying a binary function to two refl paths gives refl.

pathConcatTrans

def pathConcatTrans {A : Type} {a b c : A} (p : a ≡ b) (q : b ≡ c) : pathConcat p q ≡ trans p q

pathConcat is trans.

pathInvSym

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

pathInv is sym.

symInvol

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

Inverting a path twice gives back the path.

pathOverConst

def pathOverConst {A B : Type} {x y : A} (p : x ≡ y) (a b : B) : PathOver A (fun (_ : A) => B) p a b ≡ (a ≡ b)

A path over p in a constant family is the same type as a plain path.

pathOverRefl

def pathOverRefl {A : Type} (P : A -> Type) (a : A) (x y : P a) : PathOver A P (refl : a ≡ a) x y ≡ (x ≡ y)

A path over refl is the same type as a plain path in the fiber.

appendPathBoth

def appendPathBoth {A : Type} {xs1 xs2 ys1 ys2 : List A} (p : xs1 ≡ xs2) (q : ys1 ≡ ys2) : append xs1 ys1 ≡ append xs2 ys2

List append preserves paths in both arguments.

pathConcat3

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

Composes three consecutive paths.

pathConcat4

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

Composes four consecutive paths.

pathConcat3Refl

def pathConcat3Refl {A : Type} (a : A) : pathConcat3 (refl : a ≡ a) refl refl ≡ refl

The triple composite of refl paths is refl.

apSuccPred

def apSuccPred {m n : Nat} (p : m ≡ n) : cong succ (cong pred p) ≡ cong (fun x => succ (pred x)) p

Applying succ after pred to a path equals applying their composite.

apPredSucc

def apPredSucc {m n : Nat} (p : m ≡ n) : cong pred (cong succ p) ≡ cong (fun x => pred (succ x)) p

Applying pred after succ to a path equals applying their composite.

apAddR

def apAddR (n : Nat) {m1 m2 : Nat} (p : m1 ≡ m2) : cong (fun x => add x n) p ≡ cong (fun x => add x n) p

cong and cong agree for adding a fixed number on the right.

apAddL

def apAddL (n : Nat) {m1 m2 : Nat} (p : m1 ≡ m2) : cong (fun x => add n x) p ≡ cong (fun x => add n x) p

cong and cong agree for adding a fixed number on the left.

congMulR

def congMulR (n : Nat) {m1 m2 : Nat} (p : m1 ≡ m2) : mul m1 n ≡ mul m2 n

Multiplying by a fixed number on the right preserves a path.

congMulL

def congMulL (n : Nat) {m1 m2 : Nat} (p : m1 ≡ m2) : mul n m1 ≡ mul n m2

Multiplying by a fixed number on the left preserves a path.

congSubR

def congSubR (n : Nat) {m1 m2 : Nat} (p : m1 ≡ m2) : sub m1 n ≡ sub m2 n

Subtracting a fixed number preserves a path in the minuend.

congSubL

def congSubL (n : Nat) {m1 m2 : Nat} (p : m1 ≡ m2) : sub n m1 ≡ sub n m2

Subtracting from a fixed number preserves a path in the subtrahend.

congLengthMap

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

A path between lists gives a path between the lengths of their maps.

transportReflOption

def transportReflOption {A : Type} (x : Option A) : transport (fun (i : I) => Option A) x ≡ x

Transport along a constant Maybe line is the identity.

transportReflEither

def transportReflEither {A B : Type} (e : Either A B) : transport (fun (i : I) => Either A B) e ≡ e

Transport along a constant Either line is the identity.

transportReflPair

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

Transport along a constant Pair line is the identity.

transportTripleConst

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

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

subPath

def subPath {m1 m2 n1 n2 : Nat} (p : m1 ≡ m2) (q : n1 ≡ n2) : sub m1 n1 ≡ sub m2 n2

Truncated subtraction preserves paths in both arguments.

minPath

def minPath {m1 m2 n1 n2 : Nat} (p : m1 ≡ m2) (q : n1 ≡ n2) : min m1 n1 ≡ min m2 n2

min preserves paths in both arguments.

maxPath

def maxPath {m1 m2 n1 n2 : Nat} (p : m1 ≡ m2) (q : n1 ≡ n2) : max m1 n1 ≡ max m2 n2

max preserves paths in both arguments.

beqPath

def beqPath {m1 m2 n1 n2 : Nat} (p : m1 ≡ m2) (q : n1 ≡ n2) : Nat.beq m1 n1 ≡ Nat.beq m2 n2

Boolean equality on naturals preserves paths in both arguments.

bltPath

def bltPath {m1 m2 n1 n2 : Nat} (p : m1 ≡ m2) (q : n1 ≡ n2) : Nat.blt m1 n1 ≡ Nat.blt m2 n2

Boolean less-than on naturals preserves paths in both arguments.

leftCongPath

def leftCongPath {A B : Type} {a b : A} (p : a ≡ b) : (left a : Either A B) ≡ (left b : Either A B)

Applies left to a path.

rightCongPath

def rightCongPath {A B : Type} {a b : B} (p : a ≡ b) : (right a : Either A B) ≡ (right b : Either A B)

Applies right to a path.

mapEitherLeftPath

def mapEitherLeftPath {A B C D : Type} (f : A -> C) (g : B -> D) (a : A) : Either.bimap f g (left a : Either A B) ≡ (left (f a) : Either C D)

Either.bimap on left a gives left (f a).

mapEitherRightPath

def mapEitherRightPath {A B C D : Type} (f : A -> C) (g : B -> D) (b : B) : Either.bimap f g (right b : Either A B) ≡ (right (g b) : Either C D)

Either.bimap on right b gives right (g b).

applyPath

def applyPath {A B : Type} {f g : A -> B} {a b : A} (pf : f ≡ g) (pa : a ≡ b) : f a ≡ g b

Applies a path of functions to a path of arguments, giving a path between the results.

pairPath

def pairPath {A B : Type} {a1 a2 : A} {b1 b2 : B} (p : a1 ≡ a2) (q : b1 ≡ b2) : (a1, b1) ≡ (a2, b2)

Builds a path between pairs from paths between their components.

pairPathFst

def pairPathFst {A B : Type} {a1 a2 : A} {b1 b2 : B} (p : a1 ≡ a2) (q : b1 ≡ b2) : (fun i => fst (pairPath p q i)) ≡ p

The first projection of a pair path built by pairPath is the given first-component path.

pairPathSnd

def pairPathSnd {A B : Type} {a1 a2 : A} {b1 b2 : B} (p : a1 ≡ a2) (q : b1 ≡ b2) : (fun i => snd (pairPath p q i)) ≡ q

The second projection of a pair path built by pairPath is the given second-component path.

ap2Sym

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

Applying a binary function to two inverted paths equals inverting the applied path.

ap2ConstOuter

def ap2ConstOuter {A B C : Type} {a1 a2 : A} {b1 b2 : B} (c : C) (p : a1 ≡ a2) (q : b1 ≡ b2) : ap2 (fun (_ : A) (_ : B) => c) p q ≡ refl

Applying a constant binary function to two paths gives refl.

apd2

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

Applies a two-argument function to two paths; the same as ap2.

Loop2

def Loop2 (A : Type) (a : A) : Type

The second loop space of A at a: 2-paths from refl to refl.

loop2Refl

def loop2Refl (A : Type) (a : A) : Loop2 A a

The trivial element of the second loop space.

depPathConst

def depPathConst {A : Type} (B : Type) {x y : A} (p : x ≡ y) (b1 b2 : B) : (transport (fun i => B) b1 ≡ b2) ≡ (b1 ≡ b2)

A transported path in a constant family is the same type as a plain path.

depPathRefl

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

A path from a value transported along a constant line is the same type as a plain path.

liftPath

def liftPath {B : Type} {b1 b2 : B} (p : b1 ≡ b2) : transport (fun (i : I) => B) b1 ≡ b2

Turns a path from b1 to b2 into a path from b1 transported along a constant line to b2.

transReflV2

def transReflV2 {A : Type} {a b : A} (p : a ≡ b) : trans p refl ≡ p

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

reflTransV2

def reflTransV2 {A : Type} {a b : A} (p : a ≡ b) : trans refl p ≡ p

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

congTransV2

def congTransV2 {A B : Type} {a b c : A} (f : A -> B) (p : a ≡ b) (q : b ≡ c) : cong f (trans p q) ≡ trans (cong f p) (cong f q)

Applying a function to a composite path equals composing the applied paths.

symTransV2

def symTransV2 {A : Type} {a b c : A} (p : a ≡ b) (q : b ≡ c) : sym (trans p q) ≡ trans (sym q) (sym p)

Inverting a composite path equals composing the inverses in reverse order.

funExtPointwise

def funExtPointwise {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.

funExtId

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

Function extensionality applied to refl at every point gives refl.

whiskerLeftUnfold

def whiskerLeftUnfold {A : Type} {a b c : A} (q : a ≡ b) (p : b ≡ c) : pathConcat q p ≡ trans q p

pathConcat unfolds to trans.

pathTripleSym

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

Inverting a path three times equals inverting it once.

transportCompose

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

Trivial reflexivity witness for transport along the family P (p i).

transportSymV140

def transportSymV140 {A : Type} (P : A -> Type) {a b : A} (p : a ≡ b) (x : P b) : transport (fun i => P (sym p i)) x ≡ transport (fun i => P (p (1 - i))) x

Transport along the family over sym p is transport along the reversed family.

transportConstWitness

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

Transport in a constant family is the identity, up to a path, whatever the base path.

transportConstNatV140

def transportConstNatV140 {A : Type} {a1 a2 : A} (p : a1 ≡ a2) (n : Nat) : transport (fun i => Nat) n ≡ n

Transport along the constant Nat line is the identity.

transportConstBoolV140

def transportConstBoolV140 {A : Type} {a1 a2 : A} (p : a1 ≡ a2) (b : Bool) : transport (fun i => Bool) b ≡ b

Transport along the constant Bool line is the identity.

transportConstListV140

def transportConstListV140 {A T : Type} {a1 a2 : A} (p : a1 ≡ a2) (xs : List T) : transport (fun i => List T) xs ≡ xs

Transport along a constant List line is the identity.

apSucc

def apSucc {m n : Nat} (p : m ≡ n) : succ m ≡ succ n

Applies succ to a path between naturals.

apSuccRefl

def apSuccRefl (n : Nat) : apSucc (refl : n ≡ n) ≡ (refl : succ n ≡ succ n)

Applying succ to refl gives refl.

apNotRefl

def apNotRefl (b : Bool) : notCong (refl : b ≡ b) ≡ (refl : not b ≡ not b)

Applying boolean negation to refl gives refl.

apAddLRefl

def apAddLRefl (n m : Nat) : congAddL n (refl : m ≡ m) ≡ (refl : add n m ≡ add n m)

Adding a fixed number on the left to refl gives refl.

sigmaPathSndRefl

def sigmaPathSndRefl {A B : Type} {a1 a2 : A} (p : a1 ≡ a2) (b : B) : ((a1, b) : (a : A) × B) ≡ ((a2, b) : (a : A) × B)

A path in the first component gives a path between pairs with the same second component.

sigmaPathFstRefl

def sigmaPathFstRefl {A B : Type} (a : A) {b1 b2 : B} (q : b1 ≡ b2) : ((a, b1) : (x : A) × B) ≡ ((a, b2) : (x : A) × B)

A path in the second component gives a path between pairs with the same first component.

sigmaPathReflPair

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

A pair is connected to itself by refl.

ehRefl

def ehRefl {A : Type} (a : A) : trans (refl : a ≡ a) (refl : a ≡ a) ≡ (refl : a ≡ a)

The composite of refl with refl is refl.

transportNatRefl

def transportNatRefl (n : Nat) : transport (fun i => Nat) n ≡ n

Transport along the constant Nat line is the identity.

transportBoolRefl

def transportBoolRefl (b : Bool) : transport (fun i => Bool) b ≡ b

Transport along the constant Bool line is the identity.

transportListRefl

def transportListRefl {A : Type} (xs : List A) : transport (fun i => List A) xs ≡ xs

Transport along a constant List line is the identity.

transportFunRefl

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

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

transportPairRefl

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

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

congAddLZero

def congAddLZero (m : Nat) : cong (fun (x : Nat) => add zero x) (refl : m ≡ m) ≡ (refl : add zero m ≡ add zero m)

Applying addition of zero on the left to refl gives refl.

congAddRZero

def congAddRZero (m : Nat) : cong (fun (x : Nat) => add x zero) (refl : m ≡ m) ≡ (refl : add m zero ≡ add m zero)

Applying addition of zero on the right to refl gives refl.

congMulLOne

def congMulLOne (m : Nat) : cong (fun (x : Nat) => mul (succ zero) x) (refl : m ≡ m) ≡ (refl : mul (succ zero) m ≡ mul (succ zero) m)

Applying multiplication by one on the left to refl gives refl.

congCons

def congCons {A : Type} (x : A) {xs ys : List A} (p : xs ≡ ys) : cons x xs ≡ cons x ys

Consing a fixed head preserves a path between tails.

congConsRefl

def congConsRefl {A : Type} (x : A) (xs : List A) : congCons x (refl : xs ≡ xs) ≡ (refl : cons x xs ≡ cons x xs)

Consing a fixed head onto refl gives refl.

congLengthCons

def congLengthCons {A : Type} (x : A) {xs ys : List A} (p : xs ≡ ys) : length (cons x xs) ≡ length (cons x ys)

A path between tails gives a path between the lengths of the lists with a fixed head.

toPathPOver

def toPathPOver {X : Type} (B : X -> Type) {a0 : X} {a1 : X} (q : a0 ≡ a1) (b0 : B a0) (b1 : B a1) (p : transport (fun j => B (q j)) b0 ≡ b1) : PathP (fun i => B (q i)) b0 b1

Turns a path from the transport of b0 to b1 into a dependent path from b0 to b1 over q.

isPropToPathPOver

def isPropToPathPOver {X : Type} (B : X -> Type) (h : (x : X) -> isProp (B x)) {a0 : X} {a1 : X} (q : a0 ≡ a1) (b0 : B a0) (b1 : B a1) : PathP (fun i => B (q i)) b0 b1

In a family of propositions, any two points over the ends of a path are joined by a dependent path.