sigma

sigmaEtaNonDep

def sigmaEtaNonDep {A B : Type} (p : A × B) : (fst p, snd p) ≡ p

Eta for non-dependent pairs: rebuilding a pair from its projections gives the same pair.

fstBeta

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

Beta for the first projection: fst (a, b) is a.

sndBeta

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

Beta for the second projection: snd (a, b) is b.

mkPair

def mkPair {A : Type} {B : A -> Type} (a : A) (b : B a) : (a : A) × B a

Builds a dependent pair from a base point and an element of its fiber.

mkPairNonDep

def mkPairNonDep {A B : Type} (a : A) (b : B) : A × B

Builds a non-dependent pair from two values.

sigmaPathNonDep

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

A path in A × B built from a path between the first components and a path between the second components.

fstPathSigma

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

The base path of a path in a dependent sum, obtained by projecting the first component.

fstPathNonDep

def fstPathNonDep {A B : Type} {x : A × B} {y : A × B} (p : x ≡ y) : fst x ≡ fst y

The path between first components obtained from a path in A × B.

sndPathNonDep

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

The path between second components obtained from a path in A × B.

sigmaMap

def sigmaMap {A : Type} {A2 : Type} {B : A -> Type} {B2 : A2 -> Type} (f : A -> A2) (g : (a : A) -> B a -> B2 (f a)) (p : (a : A) × B a) : (a : A2) × B2 a

Maps a dependent pair along a base function and a fiberwise function over it.

sigmaMapFstNonDep

def sigmaMapFstNonDep {A A2 B : Type} (f : A -> A2) (p : A × B) : A2 × B

Applies a function to the first component of a non-dependent pair.

sigmaMapNonDepComp

def sigmaMapNonDepComp {A B C D E F : Type} (f1 : A -> C) (f2 : C -> E) (g1 : B -> D) (g2 : D -> F) (p : A × B) : (f2 (f1 (fst p)), g2 (g1 (snd p))) ≡ (f2 (f1 (fst p)), g2 (g1 (snd p)))

Reflexivity at the pair obtained by applying two composed functions componentwise (a trivial statement).

congPairNonDep

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

Paths between the components give a path between the pairs.

fiberMk

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

Builds an element of the fiber of f over b from a point and a path f a = b.

fiberPoint

def fiberPoint {A B : Type} {f : A -> B} {b : B} (fib : fiber A B f b) : A

The point of an element of a fiber.

fiberPath

def fiberPath {A B : Type} {f : A -> B} {b : B} (fib : fiber A B f b) : f (fst fib) ≡ b

The path f a = b carried by an element of a fiber.

fiberAtPoint

def fiberAtPoint {A B : Type} (f : A -> B) (a : A) : fiber A B f (f a)

Every point a lies in the fiber of f over f a, via the constant path.

fiberMapId

def fiberMapId {A B : Type} (f : A -> B) (b : B) (fib : fiber A B f b) : fiber A B f b

The identity map on a fiber.

transportSigmaProdConst

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

Transport along the constant family at A × B is the identity.

transportSndConst

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

Transport along the constant family at A × B leaves the second component unchanged.

isPropProd2

def isPropProd2 {A B : Type} (hA : isProp A) (hB : isProp B) : isProp (A × B)

The product of two propositions is a proposition.

isPropSigmaUnit

def isPropSigmaUnit {A : Type} (hA : isProp A) : isProp (A × Unit)

A × Unit is a proposition when A is.

sigmaAssocFwd

def sigmaAssocFwd {A B C : Type} (p : (A × B) × C) : A × (B × C)

Reassociates a left-nested triple (A × B) × C into the right-nested A × (B × C).

sigmaAssocBwd

def sigmaAssocBwd {A B C : Type} (p : A × (B × C)) : (A × B) × C

Reassociates a right-nested triple A × (B × C) into the left-nested (A × B) × C.

sigmaAssocFwdBwd

def sigmaAssocFwdBwd {A B C : Type} (p : A × (B × C)) : sigmaAssocBwd (sigmaAssocFwd (sigmaAssocBwd p)) ≡ sigmaAssocBwd p

Reassociating forward and back after sigmaAssocBwd returns the same left-nested triple.

sigmaAssocBwdFwd

def sigmaAssocBwdFwd {A B C : Type} (p : (A × B) × C) : sigmaAssocFwd (sigmaAssocBwd (sigmaAssocFwd p)) ≡ sigmaAssocFwd p

Reassociating back and forward after sigmaAssocFwd returns the same right-nested triple.

sigmaAssocRoundtrip1

theorem sigmaAssocRoundtrip1 {A B C : Type} (p : A × (B × C)) : sigmaAssocFwd (sigmaAssocBwd p) ≡ p

sigmaAssocFwd after sigmaAssocBwd is the identity on right-nested triples.

sigmaAssocRoundtrip2

theorem sigmaAssocRoundtrip2 {A B C : Type} (p : (A × B) × C) : sigmaAssocBwd (sigmaAssocFwd p) ≡ p

sigmaAssocBwd after sigmaAssocFwd is the identity on left-nested triples.

sigmaAssocFwdCompute

theorem sigmaAssocFwdCompute {A B C : Type} (a : A) (b : B) (c : C) : sigmaAssocFwd ((a, b), c) ≡ (a, (b, c))

sigmaAssocFwd ((a, b), c) computes to (a, (b, c)).

sigmaAssocBwdCompute

theorem sigmaAssocBwdCompute {A B C : Type} (a : A) (b : B) (c : C) : sigmaAssocBwd (a, (b, c)) ≡ ((a, b), c)

sigmaAssocBwd (a, (b, c)) computes to ((a, b), c).

sigmaAssocDep3Fwd

def sigmaAssocDep3Fwd {A B C D : Type} (t : (A × B) × (C × D)) : A × (B × (C × D))

Reassociates a pair of pairs (A × B) × (C × D) into the right-nested A × (B × (C × D)).

sigmaAssocDep3Bwd

def sigmaAssocDep3Bwd {A B C D : Type} (t : A × (B × (C × D))) : (A × B) × (C × D)

Reassociates a right-nested quadruple A × (B × (C × D)) into the pair of pairs (A × B) × (C × D).

sigmaAssocDep3Roundtrip1

theorem sigmaAssocDep3Roundtrip1 {A B C D : Type} (t : A × (B × (C × D))) : sigmaAssocDep3Fwd (sigmaAssocDep3Bwd t) ≡ t

sigmaAssocDep3Fwd after sigmaAssocDep3Bwd is the identity on right-nested quadruples.

sigmaAssocDep3Roundtrip2

theorem sigmaAssocDep3Roundtrip2 {A B C D : Type} (t : (A × B) × (C × D)) : sigmaAssocDep3Bwd (sigmaAssocDep3Fwd t) ≡ t

sigmaAssocDep3Bwd after sigmaAssocDep3Fwd is the identity on pairs of pairs.

sigmaSwap

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

Swaps the two components of a pair.

sigmaSwapSwap

theorem sigmaSwapSwap {A B : Type} (p : A × B) : sigmaSwap (sigmaSwap p) ≡ p

Swapping a pair twice gives back the original pair.

sigmaSwapCompute

theorem sigmaSwapCompute {A B : Type} (a : A) (b : B) : sigmaSwap (a, b) ≡ (b, a)

sigmaSwap (a, b) computes to (b, a).

sigmaSwapFst

theorem sigmaSwapFst {A B : Type} (p : A × B) : fst (sigmaSwap p) ≡ snd p

The first component of a swapped pair is the original second component.

sigmaSwapSnd

theorem sigmaSwapSnd {A B : Type} (p : A × B) : snd (sigmaSwap p) ≡ fst p

The second component of a swapped pair is the original first component.

sigmaSwapPath

def sigmaSwapPath {A B : Type} {x y : A × B} (p : x ≡ y) : sigmaSwap x ≡ sigmaSwap y

Swapping is functorial on paths: a path between pairs gives a path between the swapped pairs.

sigmaUnitFwd

def sigmaUnitFwd {A : Type} (p : A × Unit) : A

Forward map of A × Unit ≅ A: drops the unit component.

sigmaUnitBwd

def sigmaUnitBwd {A : Type} (a : A) : A × Unit

Backward map of A × Unit ≅ A: pairs a value with unit.

sigmaUnitRoundtrip1

theorem sigmaUnitRoundtrip1 {A : Type} (a : A) : sigmaUnitFwd (sigmaUnitBwd a) ≡ a

Pairing with unit and dropping it again gives back the value.

sigmaUnitRoundtrip2

def sigmaUnitRoundtrip2 {A : Type} (p : A × Unit) : sigmaUnitBwd (sigmaUnitFwd p) ≡ p

Dropping the unit component and pairing it back gives the original pair.

unitSigmaFwd

def unitSigmaFwd {A : Type} (p : Unit × A) : A

Forward map of Unit × A ≅ A: drops the unit component.

unitSigmaBwd

def unitSigmaBwd {A : Type} (a : A) : Unit × A

Backward map of Unit × A ≅ A: pairs unit with a value.

unitSigmaRoundtrip1

theorem unitSigmaRoundtrip1 {A : Type} (a : A) : unitSigmaFwd (unitSigmaBwd a) ≡ a

Pairing with unit on the left and dropping it again gives back the value.

unitSigmaRoundtrip2

def unitSigmaRoundtrip2 {A : Type} (p : Unit × A) : unitSigmaBwd (unitSigmaFwd p) ≡ p

Dropping the unit component and pairing it back gives the original pair.

sigmaContrBaseFwd

def sigmaContrBaseFwd {A : Type} {B : A -> Type} (hA : isContr A) (p : (a : A) × B a) : B (fst hA)

Over a contractible base, transports the fiber element of a dependent pair to the fiber at the center.

sigmaContrBaseBwd

def sigmaContrBaseBwd {A : Type} {B : A -> Type} (hA : isContr A) (b : B (fst hA)) : (a : A) × B a

Over a contractible base, puts an element of the fiber at the center into the dependent sum.

sigmaContrBaseBwdFst

def sigmaContrBaseBwdFst {A : Type} {B : A -> Type} (hA : isContr A) (b : B (fst hA)) : fst (sigmaContrBaseBwd hA b) ≡ fst hA

The base point of an element built by sigmaContrBaseBwd is the center.

sigmaContrFiberFwd

def sigmaContrFiberFwd {A : Type} {B : A -> Type} (hB : (a : A) -> isContr (B a)) (p : (a : A) × B a) : A

With contractible fibers, projects a dependent pair to its base point.

sigmaContrFiberBwd

def sigmaContrFiberBwd {A : Type} {B : A -> Type} (hB : (a : A) -> isContr (B a)) (a : A) : (a : A) × B a

With contractible fibers, lifts a base point into the dependent sum using the center of its fiber.

sigmaContrFiberRoundtrip1

def sigmaContrFiberRoundtrip1 {A : Type} {B : A -> Type} (hB : (a : A) -> isContr (B a)) (a : A) : sigmaContrFiberFwd hB (sigmaContrFiberBwd hB a) ≡ a

Lifting a base point with sigmaContrFiberBwd and projecting it back gives the same point.

singlContrR

def singlContrR {A : Type} (x : A) : isContr ((y : A) × (x ≡ y))

The singleton type of points y with a path x = y is contractible.

singlContrL

def singlContrL {A : Type} (x : A) : isContr ((y : A) × (y ≡ x))

The singleton type of points y with a path y = x is contractible.

singlCenter

def singlCenter {A : Type} (x : A) : (y : A) × (x ≡ y)

The center of the singleton type at x: x with the constant path.

singlCenterFst

def singlCenterFst {A : Type} (x : A) : fst (singlCenter x) ≡ x

The point of the singleton center at x is x.

sigmaBimap

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

sigmaBimapComp

theorem sigmaBimapComp {A B C D E F : Type} (f1 : A -> C) (f2 : C -> E) (g1 : B -> D) (g2 : D -> F) (p : A × B) : sigmaBimap f2 g2 (sigmaBimap f1 g1 p) ≡ sigmaBimap (fun (a : A) => f2 (f1 a)) (fun (b : B) => g2 (g1 b)) p

Applying sigmaBimap twice equals applying it once with the composed functions.

sigmaBimapCompute

theorem sigmaBimapCompute {A B C D : Type} (f : A -> C) (g : B -> D) (a : A) (b : B) : sigmaBimap f g (a, b) ≡ (f a, g b)

sigmaBimap f g (a, b) computes to (f a, g b).

sigmaFirst

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

Applies a function to the first component of a pair, keeping the second.

sigmaSecond

def sigmaSecond {A B D : Type} (g : B -> D) (p : A × B) : A × D

Applies a function to the second component of a pair, keeping the first.

sigmaFirstCompute

theorem sigmaFirstCompute {A B C : Type} (f : A -> C) (a : A) (b : B) : sigmaFirst f (a, b) ≡ (f a, b)

sigmaFirst f (a, b) computes to (f a, b).

sigmaSecondCompute

theorem sigmaSecondCompute {A B D : Type} (g : B -> D) (a : A) (b : B) : sigmaSecond g (a, b) ≡ (a, g b)

sigmaSecond g (a, b) computes to (a, g b).

sigmaDiag

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

Diagonal map: duplicates a value into a pair.

sigmaDiagFst

theorem sigmaDiagFst {A : Type} (a : A) : fst (sigmaDiag a) ≡ a

The first component of the diagonal pair is the original value.

sigmaDiagSnd

theorem sigmaDiagSnd {A : Type} (a : A) : snd (sigmaDiag a) ≡ a

The second component of the diagonal pair is the original value.

sigmaDiagCompute

theorem sigmaDiagCompute {A : Type} (a : A) : sigmaDiag a ≡ (a, a)

sigmaDiag a computes to (a, a).

sigmaFanout

def sigmaFanout {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : B × C

Applies two functions to the same input and pairs the results.

sigmaFanoutFst

theorem sigmaFanoutFst {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : fst (sigmaFanout f g a) ≡ f a

The first component of sigmaFanout f g a is f a.

sigmaFanoutSnd

theorem sigmaFanoutSnd {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : snd (sigmaFanout f g a) ≡ g a

The second component of sigmaFanout f g a is g a.

sigmaFanoutCompute

theorem sigmaFanoutCompute {A B C : Type} (f : A -> B) (g : A -> C) (a : A) : sigmaFanout f g a ≡ (f a, g a)

sigmaFanout f g a computes to (f a, g a).

sigmaCurry

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

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

sigmaUncurry

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

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

sigmaCurryUncurry

theorem sigmaCurryUncurry {A : Type} {B : A -> Type} {C : Type} (f : (a : A) -> B a -> C) (a : A) (b : B a) : sigmaCurry (sigmaUncurry f) a b ≡ f a b

Currying an uncurried function gives back the original function pointwise.

sigmaUncurryCurry

theorem sigmaUncurryCurry {A : Type} {B : A -> Type} {C : Type} (f : ((a : A) × B a) -> C) (a : A) (b : B a) : sigmaUncurry (sigmaCurry f) (a, b) ≡ f (a, b)

Uncurrying a curried function gives back the original function on every pair.

sigmaApply

def sigmaApply {A B C D : Type} (fg : (A -> C) × (B -> D)) (p : A × B) : C × D

Applies a pair of functions componentwise to a pair of arguments.

sigmaApplyCompute

theorem sigmaApplyCompute {A B C D : Type} (f : A -> C) (g : B -> D) (a : A) (b : B) : sigmaApply (f, g) (a, b) ≡ (f a, g b)

sigmaApply (f, g) (a, b) computes to (f a, g b).

sigmaDup

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

Applies one function to both components of a homogeneous pair.

sigmaDupCompute

theorem sigmaDupCompute {A B : Type} (f : A -> B) (a1 : A) (a2 : A) : sigmaDup f (a1, a2) ≡ (f a1, f a2)

sigmaDup f (a1, a2) computes to (f a1, f a2).

exists_intro

def exists_intro {A : Type} {P : A -> Type} (a : A) (pa : P a) : (a : A) × P a

Introduces an existential from a witness and a proof that it satisfies the predicate.

exists_witness

def exists_witness {A : Type} {P : A -> Type} (h : (a : A) × P a) : A

The witness of an existential.

exists_proof

def exists_proof {A : Type} {P : A -> Type} (h : (a : A) × P a) : P (fst h)

The proof that the witness of an existential satisfies the predicate.

exists_elim

def exists_elim {A : Type} {P : A -> Type} {C : Type} (h : (a : A) × P a) (f : (a : A) -> P a -> C) : C

Eliminates an existential by a function that works for every witness and proof.

exists_map

def exists_map {A : Type} {P : A -> Type} {Q : A -> Type} (f : (a : A) -> P a -> Q a) (h : (a : A) × P a) : (a : A) × Q a

Maps an existential along a fiberwise implication between predicates, keeping the witness.

existsMapCompute

theorem existsMapCompute {A : Type} {P : A -> Type} {Q : A -> Type} (f : (a : A) -> P a -> Q a) (a : A) (pa : P a) : exists_map f (a, pa) ≡ (a, f a pa)

exists_map f (a, pa) computes to (a, f a pa).

sigmaBoolInjectTrue

def sigmaBoolInjectTrue {P : Bool -> Type} (pt : P true) : (b : Bool) × P b

Puts an element of the fiber at true into the dependent sum over Bool.

sigmaBoolInjectFalse

def sigmaBoolInjectFalse {P : Bool -> Type} (pf : P false) : (b : Bool) × P b

Puts an element of the fiber at false into the dependent sum over Bool.

sigmaBoolInjectTrueFst

theorem sigmaBoolInjectTrueFst {P : Bool -> Type} (pt : P true) : fst (sigmaBoolInjectTrue pt) ≡ true

The base point of sigmaBoolInjectTrue is true.

sigmaBoolInjectFalseFst

theorem sigmaBoolInjectFalseFst {P : Bool -> Type} (pf : P false) : fst (sigmaBoolInjectFalse pf) ≡ false

The base point of sigmaBoolInjectFalse is false.

sigmaNatZero

def sigmaNatZero {P : Nat -> Type} (p0 : P zero) : (n : Nat) × P n

Puts an element of the fiber at zero into the dependent sum over Nat.

sigmaNatSucc

def sigmaNatSucc {P : Nat -> Type} (n : Nat) (ps : P (succ n)) : (k : Nat) × P k

Puts an element of the fiber at succ n into the dependent sum over Nat.

sigmaNatZeroFst

theorem sigmaNatZeroFst {P : Nat -> Type} (p0 : P zero) : fst (sigmaNatZero p0) ≡ zero

The base point of sigmaNatZero is zero.

sigmaNatSuccFst

theorem sigmaNatSuccFst {P : Nat -> Type} (n : Nat) (ps : P (succ n)) : fst (sigmaNatSucc n ps) ≡ succ n

The base point of sigmaNatSucc n is succ n.

sigmaFlip

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

Turns a function on A × B into a function on B × A by swapping the input.

sigmaFlipFlip

theorem sigmaFlipFlip {A B C : Type} (f : A × B -> C) (a : A) (b : B) : sigmaFlip (sigmaFlip f) (a, b) ≡ f (a, b)

Flipping a function on pairs twice gives back the original function on every pair.

sigmaDistrib

def sigmaDistrib {A B C : Type} (p : A × Either B C) : Either (A × B) (A × C)

Distributes a product over a sum: A × (B + C) to (A × B) + (A × C).

sigmaUndistrib

def sigmaUndistrib {A B C : Type} (e : Either (A × B) (A × C)) : A × Either B C

Factors a sum of products: (A × B) + (A × C) to A × (B + C).

sigmaDistribRet

def sigmaDistribRet {A B C : Type} (e : Either (A × B) (A × C)) : sigmaDistrib (sigmaUndistrib e) ≡ e

Distributing after factoring gives back the original sum, so sigmaUndistrib is a section of sigmaDistrib.

sigmaTriple

def sigmaTriple {A B C : Type} (a : A) (b : B) (c : C) : A × (B × C)

Builds a right-nested triple from three values.

sigmaQuad

def sigmaQuad {A B C D : Type} (a : A) (b : B) (c : C) (d : D) : A × (B × (C × D))

Builds a right-nested quadruple from four values.

sigmaTripleFst

theorem sigmaTripleFst {A B C : Type} (a : A) (b : B) (c : C) : fst (sigmaTriple a b c) ≡ a

The first component of sigmaTriple a b c is a.

isPropSigmaConst

def isPropSigmaConst {A B : Type} (hA : isProp A) (hB : isProp B) : isProp (A × B)

The product of two propositions is a proposition.

isSetSigmaNonDep2

def isSetSigmaNonDep2 (A B : Type) (hA : isSet A) (hB : isSet B) : isSet (A × B)

The product of two sets is a set.

sigmaConstProj1

def sigmaConstProj1 {A B : Type} (a : A) (b : B) : fst (a, b) ≡ a

The first projection of a non-dependent pair (a, b) is a.

sigmaConstProj2

def sigmaConstProj2 {A B : Type} (a : A) (b : B) : snd (a, b) ≡ b

The second projection of a non-dependent pair (a, b) is b.

sigmaIdFwd

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

Projects an element of the based path space at b to its point.

sigmaIdBwd

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

Puts a into the based path space at a, using the constant path.

sigmaOfPi_to_piOfSigma

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

Turns a pair of a point and a function into a function returning pairs with that fixed point.

congSigmaPath

def congSigmaPath {A B : Type} {x y z : A × B} (p : x ≡ y) (q : y ≡ z) : sigmaPathNonDep (fun i => fst (trans p q i)) (fun i => snd (trans p q i)) ≡ trans p q

Rebuilding a composite path in A × B from its component paths gives back the composite.

etaMk

theorem etaMk {A : Type} {B : A -> Type} (a : A) (b : B a) : (fst (a, b), snd (a, b)) ≡ (a, b)

Eta after beta: rebuilding (a, b) from its projections gives (a, b).

fstSigmaMapSnd

theorem fstSigmaMapSnd {A : Type} {B : A -> Type} {C : A -> Type} (f : (a : A) -> B a -> C a) (a : A) (b : B a) : fst (sigmaMapSnd f (a, b)) ≡ a

sigmaMapSnd keeps the base point.

sndSigmaMapSnd

theorem sndSigmaMapSnd {A : Type} {B : A -> Type} {C : A -> Type} (f : (a : A) -> B a -> C a) (a : A) (b : B a) : snd (sigmaMapSnd f (a, b)) ≡ f a b

The second component of sigmaMapSnd f (a, b) is f a b.

sigmaEmpty

def sigmaEmpty {B : Empty -> Type} (p : (a : Empty) × B a) : Empty

A dependent sum over Empty is empty.

sigmaEmptyFiber

def sigmaEmptyFiber {A : Type} (p : A × Empty) : Empty

A × Empty is empty.

boolNatPair

def boolNatPair : Bool × Nat

Example pair of a boolean and a natural number, (true, 2).

sigmaPathNested

def sigmaPathNested {A B C : Type} {x : A × (B × C)} {y : A × (B × C)} (p1 : fst x ≡ fst y) (p2 : fst (snd x) ≡ fst (snd y)) (p3 : snd (snd x) ≡ snd (snd y)) : x ≡ y

A path in a right-nested triple built from paths between the three components.

fstPathNested

def fstPathNested {A B C : Type} {x : A × (B × C)} {y : A × (B × C)} (p : x ≡ y) : fst x ≡ fst y

The path between first components obtained from a path in a right-nested triple.

sndFstPathNested

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

The path between second components obtained from a path in a right-nested triple.

sndSndPathNested

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

The path between third components obtained from a path in a right-nested triple.

isPropSinglR

def isPropSinglR {A : Type} (x : A) : isProp ((y : A) × (x ≡ y))

The singleton type of points y with a path x = y is a proposition.

isPropSinglL

def isPropSinglL {A : Type} (x : A) : isProp ((y : A) × (y ≡ x))

The singleton type of points y with a path y = x is a proposition.

sigmaStrengthL

def sigmaStrengthL {A B : Type} (a : A) (b : B) : A × B

Pairs a value with another, the first argument becoming the first component.

sigmaStrengthR

def sigmaStrengthR {A B : Type} (b : B) (a : A) : A × B

Pairs two values with the arguments reversed: the second argument becomes the first component.

sigmaStrengthLFst

theorem sigmaStrengthLFst {A B : Type} (a : A) (b : B) : fst (sigmaStrengthL a b) ≡ a

The first component of sigmaStrengthL a b is a.

sigmaStrengthLSnd

theorem sigmaStrengthLSnd {A B : Type} (a : A) (b : B) : snd (sigmaStrengthL a b) ≡ b

The second component of sigmaStrengthL a b is b.

natTriple1

def natTriple1 : Nat × (Nat × Nat)

Example right-nested triple of natural numbers, (0, (1, 2)).