hits

S1

data S1

The circle: a base point with a loop from base to itself.

loop_at_0

def loop_at_0 : S1

The loop of the circle evaluated at interval endpoint 0, which is base.

loop_at_1

def loop_at_1 : S1

The loop of the circle evaluated at interval endpoint 1, which is base.

doubleLoop

def doubleLoop : base ≡ base

The loop of the circle traversed twice.

s1Rec

def s1Rec (B : Type) (b : B) (l : b ≡ b) (x : S1) : B

Non-dependent recursion out of the circle: give a point and a loop at that point.

Susp

data Susp (A : Type)

The suspension of A: two poles with a meridian from north to south for each element of A.

suspRec

def suspRec (A : Type) (B : Type) (n : B) (s : B) (m : A -> n ≡ s) (x : Susp A) : B

Non-dependent recursion out of the suspension: give images of both poles and a path between them for each meridian.

Truncation

data Truncation (A : Type)

Propositional truncation of A: elements of A, with any two elements identified by a path.

truncationIsProp

def truncationIsProp (A : Type) (x : Truncation A) (y : Truncation A) : x ≡ y

Any two elements of a propositional truncation are connected by a path.

merely

def merely (A : Type) (a : A) : Truncation A

Includes an element of A into its propositional truncation.

Interval

data Interval

The interval as a higher inductive type: two endpoints joined by a segment.

intervalContr

def intervalContr (x : Interval) : i0 ≡ x

Every point of the interval is connected to the endpoint i0.

Torus

data Torus

The torus: a base point with two loops.

s1MeridMap

def s1MeridMap (b : Bool) : base ≡ base

Assigns each boolean a loop at the circle’s base: true goes to loop, false to refl.

susp_bool_to_s1

def susp_bool_to_s1 (x : Susp Bool) : S1

Maps the suspension of Bool onto the circle, sending both poles to base and the meridians to loop and refl.

Pushout

data Pushout (A : Type) (B : Type) (C : Type) (f : C -> A) (g : C -> B)

The pushout of a span A <- C -> B: points of A and B, glued by a path for each element of C.

S2

data S2

The 2-sphere: a base point with a 2-dimensional surface from refl to refl.

Join

data Join (A : Type) (B : Type)

The join of A and B: points of A and B, with a path from each point of A to each point of B.

s1Elim

def s1Elim (P : S1 -> Type) (b : P base) (l : PathP (fun i => P (loop i)) b b) (x : S1) : P x

Dependent elimination out of the circle: give a point over base and a dependent path over the loop.

loopCancel

def loopCancel : trans loop (sym loop) ≡ refl

Composing the circle’s loop with its inverse is the constant path.

susp_unit_to_interval

def susp_unit_to_interval (x : Susp Unit) : Interval

Maps the suspension of Unit to the interval, sending poles to endpoints and the meridian to the segment.

truncIsProp

def truncIsProp (A : Type) : isProp (Truncation A)

The propositional truncation of any type is a proposition.

truncMap

def truncMap {A : Type} {B : Type} (f : A -> B) (t : Truncation A) : Truncation B

Applies a function under propositional truncation.

truncBind

def truncBind {A : Type} {B : Type} (t : Truncation A) (f : A -> Truncation B) : Truncation B

Monadic bind for propositional truncation.

interval_isProp

def interval_isProp : isProp Interval

The interval is a proposition: any two of its points are connected.

torusRec

def torusRec (B : Type) (b : B) (la : b ≡ b) (lb : b ≡ b) (x : Torus) : B

Non-dependent recursion out of the torus: give a point and two loops at it.

s1_to_nat

def s1_to_nat (x : S1) : Nat

The constant map from the circle to Nat with value zero.

truncReturn

def truncReturn {A : Type} (a : A) : Truncation A

Monadic return for propositional truncation: includes an element.

intervalRec

def intervalRec (B : Type) (b0 : B) (b1 : B) (p : b0 ≡ b1) (x : Interval) : B

Non-dependent recursion out of the interval: give two points and a path between them.

join_inl_nat

def join_inl_nat : Join Nat Bool

An example point of Join Nat Bool on the left side.

join_inr_bool

def join_inr_bool : Join Nat Bool

An example point of Join Nat Bool on the right side.

susp_bool_to_nat

def susp_bool_to_nat (x : Susp Bool) : Nat

The constant map from the suspension of Bool to Nat with value zero.

susp_unit_north

def susp_unit_north : Susp Unit

The north pole of the suspension of Unit.

susp_unit_south

def susp_unit_south : Susp Unit

The south pole of the suspension of Unit.

susp_empty_north

def susp_empty_north : Susp Empty

The north pole of the suspension of Empty.

susp_empty_south

def susp_empty_south : Susp Empty

The south pole of the suspension of Empty.

trunc_zero

def trunc_zero : Truncation Nat

The truncated element zero of Nat.

trunc_one

def trunc_one : Truncation Nat

The truncated element one of Nat.

trunc_true

def trunc_true : Truncation Bool

The truncated element true of Bool.

trunc_false

def trunc_false : Truncation Bool

The truncated element false of Bool.

PoNB

def PoNB : Type

An example pushout of Nat and Bool over Unit, gluing zero to true.

po_inl

def po_inl : PoNB

The left point zero of the example pushout PoNB.

po_inr

def po_inr : PoNB

The right point true of the example pushout PoNB.

joinRec

def joinRec (A : Type) (B : Type) (C : Type) (l : A -> C) (r : B -> C) (p : (a : A) -> (b : B) -> l a ≡ r b) (x : Join A B) : C

Non-dependent recursion out of the join: give maps from both sides and a path between their images for each pair.

join_bb_l_true

def join_bb_l_true : Join Bool Bool

The left point true of Join Bool Bool.

join_bb_l_false

def join_bb_l_false : Join Bool Bool

The left point false of Join Bool Bool.

join_bb_r_true

def join_bb_r_true : Join Bool Bool

The right point true of Join Bool Bool.

join_bb_r_false

def join_bb_r_false : Join Bool Bool

The right point false of Join Bool Bool.

s1_to_bool

def s1_to_bool (x : S1) : Bool

The constant map from the circle to Bool with value true.

s1_const_zero

def s1_const_zero (x : S1) : Nat

The constant map from the circle to Nat with value zero.

interval_to_bool

def interval_to_bool (x : Interval) : Bool

The constant map from the interval to Bool with value false.

s1_to_unit

def s1_to_unit (x : S1) : Unit

The map from the circle to Unit.

s1_const_one

def s1_const_one (x : S1) : Nat

The constant map from the circle to Nat with value one.

s1_double_rec

def s1_double_rec (x : S1) : Nat

Adds the value of s1_to_nat to itself at a point of the circle.

susp_nat_north

def susp_nat_north : Susp Nat

The north pole of the suspension of Nat.

susp_nat_south

def susp_nat_south : Susp Nat

The south pole of the suspension of Nat.

susp_nat_to_nat

def susp_nat_to_nat (x : Susp Nat) : Nat

The constant map from the suspension of Nat to Nat with value zero.

susp_unit_to_nat

def susp_unit_to_nat (x : Susp Unit) : Nat

The constant map from the suspension of Unit to Nat with value zero.

join_nat_nat_l0

def join_nat_nat_l0 : Join Nat Nat

The left point zero of Join Nat Nat.

join_nat_nat_l1

def join_nat_nat_l1 : Join Nat Nat

The left point one of Join Nat Nat.

join_nat_nat_r0

def join_nat_nat_r0 : Join Nat Nat

The right point zero of Join Nat Nat.

join_nat_nat_r1

def join_nat_nat_r1 : Join Nat Nat

The right point one of Join Nat Nat.

join_nat_nat_to_nat

def join_nat_nat_to_nat (x : Join Nat Nat) : Nat

The constant map from Join Nat Nat to Nat with value zero.

torus_to_bool

def torus_to_bool (x : Torus) : Bool

The constant map from the torus to Bool with value true.

torus_to_nat

def torus_to_nat (x : Torus) : Nat

The constant map from the torus to Nat with value zero.

trunc_unit

def trunc_unit : Truncation Unit

The truncated element unit of Unit.

trunc_nil

def trunc_nil : Truncation (List Nat)

The truncated empty list of naturals.

trunc_list1

def trunc_list1 : Truncation (List Nat)

The truncated one-element list [0].

trunc_map_succ_zero

def trunc_map_succ_zero : Truncation Nat

Applies succ under truncation to the truncated zero.

trunc_map_succ_one

def trunc_map_succ_one : Truncation Nat

Applies succ under truncation to the truncated one.

interval_to_nat

def interval_to_nat (x : Interval) : Nat

The constant map from the interval to Nat with value zero.

interval_to_unit

def interval_to_unit (x : Interval) : Unit

The map from the interval to Unit.

s2Rec

def s2Rec (B : Type) (b : B) (s : (refl : b ≡ b) ≡ (refl : b ≡ b)) (x : S2) : B

Non-dependent recursion out of the 2-sphere: give a point and a 2-cell from refl to refl at it.

s2_to_nat

def s2_to_nat (x : S2) : Nat

The constant map from the 2-sphere to Nat with value zero.

s2_to_bool

def s2_to_bool (x : S2) : Bool

The constant map from the 2-sphere to Bool with value true.

s1_const_two

def s1_const_two (x : S1) : Nat

The constant map from the circle to Nat with value two.

s1_const_three

def s1_const_three (x : S1) : Nat

The constant map from the circle to Nat with value three.

s1_const_false

def s1_const_false (x : S1) : Bool

The constant map from the circle to Bool with value false.

s1_to_list

def s1_to_list (x : S1) : List Nat

The constant map from the circle to List Nat with value the empty list.

s1_to_option

def s1_to_option (x : S1) : Option Nat

The constant map from the circle to Maybe Nat with value nothing.

s1_double_nat

def s1_double_nat (x : S1) : Nat

Adds s1_to_nat and s1_const_one at a point of the circle.

susp_bool_to_bool

def susp_bool_to_bool (x : Susp Bool) : Bool

The constant map from the suspension of Bool to Bool with value true.

susp_nat_to_bool

def susp_nat_to_bool (x : Susp Nat) : Bool

The constant map from the suspension of Nat to Bool with value true.

susp_unit_to_bool

def susp_unit_to_bool (x : Susp Unit) : Bool

The constant map from the suspension of Unit to Bool with value true.

interval_to_list

def interval_to_list (x : Interval) : List Nat

The constant map from the interval to List Nat with value the empty list.

interval_to_option

def interval_to_option (x : Interval) : Option Nat

The constant map from the interval to Maybe Nat with value nothing.

torus_to_unit

def torus_to_unit (x : Torus) : Unit

The map from the torus to Unit.

torusInvA

def torusInvA : tbase ≡ tbase

The inverse of the torus’s first loop.

join_nat_bool_to_nat

def join_nat_bool_to_nat (x : Join Nat Bool) : Nat

The constant map from Join Nat Bool to Nat with value zero.

join_uu_l

def join_uu_l : Join Unit Unit

The left point of Join Unit Unit.

join_uu_r

def join_uu_r : Join Unit Unit

The right point of Join Unit Unit.

PoUnit

def PoUnit : Type

The pushout of Unit and Unit along identities over Unit, an interval-like type.

torus_to_option

def torus_to_option (x : Torus) : Option Nat

The constant map from the torus to Maybe Nat with value nothing.

s1_to_pair

def s1_to_pair (x : S1) : Pair Nat Bool

The constant map from the circle to Pair Nat Bool with value (zero, true).

s1_const_five

def s1_const_five (x : S1) : Nat

The constant map from the circle to Nat with value five.

s1_to_pair_bb

def s1_to_pair_bb (x : S1) : Pair Bool Bool

The constant map from the circle to Pair Bool Bool with value (true, false).

s1_to_option_bool

def s1_to_option_bool (x : S1) : Option Bool

The constant map from the circle to Maybe Bool with value just true.

susp_bool_to_unit

def susp_bool_to_unit (x : Susp Bool) : Unit

The map from the suspension of Bool to Unit.

susp_nat_to_unit

def susp_nat_to_unit (x : Susp Nat) : Unit

The map from the suspension of Nat to Unit.

susp_bool_to_option

def susp_bool_to_option (x : Susp Bool) : Option Nat

The constant map from the suspension of Bool to Maybe Nat with value nothing.

interval_to_pair

def interval_to_pair (x : Interval) : Pair Nat Bool

The constant map from the interval to Pair Nat Bool with value (zero, true).

torus_to_option_bool

def torus_to_option_bool (x : Torus) : Option Bool

The constant map from the torus to Maybe Bool with value just false.

join_nat_bool_to_bool

def join_nat_bool_to_bool (x : Join Nat Bool) : Bool

The constant map from Join Nat Bool to Bool with value true.

pushoutRec

def pushoutRec (A : Type) (B : Type) (C : Type) (f : C -> A) (g : C -> B) (D : Type) (l : A -> D) (r : B -> D) (p : (c : C) -> l (f c) ≡ r (g c)) (x : Pushout A B C f g) : D

Non-dependent recursion out of a pushout: give maps from both sides that agree by a path on each glued element.

suspMap

def suspMap {A : Type} {B : Type} (h : A -> B) (x : Susp A) : Susp B

The functorial action of suspension: maps poles to poles and each meridian along the given function.

truncJoin

def truncJoin {A : Type} (tt : Truncation (Truncation A)) : Truncation A

Flattens a doubly truncated value into a single truncation.

truncJoinInc

def truncJoinInc {A : Type} (a : A) : truncJoin (inc (inc a)) ≡ inc a

Flattening a doubly included element gives the singly included element.

s1_rec_const

def s1_rec_const (b : Nat) (x : S1) : Nat

The constant map from the circle to Nat with the given value.

join_bool_bool_to_nat

def join_bool_bool_to_nat (x : Join Bool Bool) : Nat

The constant map from Join Bool Bool to Nat with value zero.

join_to_unit

def join_to_unit (A : Type) (B : Type) (x : Join A B) : Unit

The map from any join to Unit.

interval_isContr

def interval_isContr : isContr Interval

The interval is contractible, with center i0.

truncMapIdInc

def truncMapIdInc {A : Type} (a : A) : truncMap (fun (x : A) => x) (inc a) ≡ inc a

Mapping the identity under truncation fixes an included element.

truncBindRightIdInc

def truncBindRightIdInc {A : Type} (a : A) : truncBind (inc a) (fun (x : A) => inc x) ≡ inc a

Right identity of truncation bind on an included element: binding with inclusion returns it.

suspMapNorth

def suspMapNorth {A B : Type} (h : A -> B) : suspMap h north ≡ north

The suspension map sends the north pole to the north pole.

suspMapSouth

def suspMapSouth {A B : Type} (h : A -> B) : suspMap h south ≡ south

The suspension map sends the south pole to the south pole.

suspMapMerid

def suspMapMerid (h : Bool -> Nat) (b : Bool) : (fun i => suspMap h (merid b i)) ≡ merid (h b)

The suspension map sends the meridian at b to the meridian at h b.