Kubus
The library
The standard library, rendered from lib/: hover over a name to see its type, click it to go to its definition. Every declaration is certified by the kernel.
- basic — Paths: reflexivity, symmetry, concatenation, transport, J, function extensionality.
- equiv — Contractible types, fibers, equivalences, univalence as a map ua, isomorphisms are equivalences.
- univalence — The univalence axiom: the type of types equivalent to A is contractible.
- int — Natural numbers and integers; the successor equivalence of the integers.
- bool — Booleans and negation as a path Bool = Bool.
- circle — The circle, its universal cover, and winding numbers.
- loopspace — The loop space of the circle is the integers.
- hits — Propositional truncation and suspensions.
Index of definitions
| name | type | module |
|---|---|---|
| absurd | {A : U} → Empty → A | basic |
| add | Nat → Nat → Nat | int |
| addZero | (n : Nat) → Path Nat (add zero n) n | int |
| base | S1 | circle |
| Bool | U | bool |
| compS1 | Path S1 base base → Path S1 base base → Path S1 base base | circle |
| cong | {A B : U} → (f : A → B) → {a b : A} → Path A a b → Path B (f a) (f b) | basic |
| contrSingl | {A : U} → {a b : A} → (p : Path A a b) → Path (singl a) (a, refl a) (b, p) | basic |
| decode | (x : S1) → helix x → Path S1 base x | loopspace |
| decodeEncode | (x : S1) → (p : Path S1 base x) → Path (Path S1 base x) (decode x (encode x p)) p | loopspace |
| decodeSquare | (n : Int) → PathP (λ i → Path S1 base (loop i)) (intLoop (predInt n)) (intLoop n) | loopspace |
| Empty | U | basic |
| encode | (x : S1) → Path S1 base x → helix x | loopspace |
| encodeDecode | (n : Int) → Path Int (encode base (decode base n)) n | loopspace |
| Equiv | U → U → U | equiv |
| EquivContr | (A : U) → isContr^1 ((T : U) × Equiv T A) | univalence |
| equivCtr | {A B : U} → (e : Equiv A B) → (y : B) → fiber e.1 y | univalence |
| equivCtrPath | {A B : U} → (e : Equiv A B) → (y : B) → (v : fiber e.1 y) → Path (fiber e.1 y) (equivCtr e y) v | univalence |
| false | Bool | bool |
| fiber | {A B : U} → (A → B) → B → U | equiv |
| funext | {A B : U} → {f g : A → B} → ((x : A) → Path B (f x) (g x)) → Path (A → B) f g | basic |
| funextDep | {A : U} → {B : A → U} → {f g : (x : A) → B x} → ((x : A) → Path (B x) (f x) (g x)) → Path ((x : A) → B x) f g | basic |
| GlueI | {A : U} → ((T : U) × Equiv T A) → (i : I) → U | univalence |
| helix | S1 → U | circle |
| id | {A : U} → A → A | basic |
| idEquiv | (A : U) → Equiv A A | equiv |
| idIsEquiv | {A : U} → isEquiv id | equiv |
| inc | {A : U} → A → Trunc A | hits |
| Int | U | int |
| intLoop | Int → Path S1 base base | loopspace |
| intLoopNeg | Nat → Path S1 base base | loopspace |
| intLoopPos | Nat → Path S1 base base | loopspace |
| invLoop | Path S1 base base | circle |
| isContr | U → U | equiv |
| isEquiv | {A B : U} → (A → B) → U | equiv |
| isoToEquiv | {A B : U} → (f : A → B) → (g : B → A) → section f g → retract f g → Equiv A B | equiv |
| isoToPath | {A B : U} → (f : A → B) → (g : B → A) → section f g → retract f g → Path U A B | equiv |
| isProp | U → U | basic |
| isSet | U → U | basic |
| J | {A : U} → {a : A} → (C : (x : A) → Path A a x → U) → C a (refl a) → {x : A} → (p : Path A a x) → C x p | basic |
| JRefl | {A : U} → {a : A} → (C : (x : A) → Path A a x → U) → (d : C a (refl a)) → Path (C a (refl a)) (J C d (refl a)) d | basic |
| lemIso | {A B : U} → {f : A → B} → {g : B → A} → section f g → retract f g → {y : B} → {x0 x1 : A} → (p0 : Path B (f x0) y) → (p1 : Path B (f x1) y) → Path (fiber f y) (x0, p0) (x1, p1) | equiv |
| loop | (i : I) → S1 | circle |
| loopP | Path S1 base base | circle |
| loopSpaceS1 | Path U (Path S1 base base) Int | loopspace |
| lUnit | {A : U} → {a b : A} → (p : Path A a b) → Path (Path A a b) p (trans (refl a) p) | basic |
| merid | {A : U} → A → (i : I) → Susp A | hits |
| meridP | {A : U} → A → Path (Susp A) north south | hits |
| Nat | U | int |
| negsuc | Nat → Int | int |
| north | {A : U} → Susp A | hits |
| not | Bool → Bool | bool |
| notnot | (b : Bool) → Path Bool (not (not b)) b | bool |
| notPath | Path U Bool Bool | bool |
| pos | Nat → Int | int |
| predInt | Int → Int | int |
| predSuc | (z : Int) → Path Int (predInt (sucInt z)) z | int |
| refl | {A : U} → (a : A) → Path A a a | basic |
| retract | {A B : U} → (A → B) → (B → A) → U | equiv |
| rUnit | {A : U} → {a b : A} → (p : Path A a b) → Path (Path A a b) p (trans p (refl b)) | basic |
| S1 | U | circle |
| section | {A B : U} → (A → B) → (B → A) → U | equiv |
| sigmaPath | {A : U} → {B : A → U} → {u v : (x : A) × B x} → (p : Path A u.1 v.1) → PathP (λ i → B (p i)) u.2 v.2 → Path ((x : A) × B x) u v | basic |
| singl | {A : U} → A → U | basic |
| south | {A : U} → Susp A | hits |
| squash | {A : U} → Trunc A → Trunc A → (i : I) → Trunc A | hits |
| substComp | {X : U} → (F : X → U) → {a b : X} → (p : Path X a b) → (u : F a) → {c : X} → (q : Path X b c) → Path (F c) (transport (λ i → F (trans p q i)) u) (transport (λ i → F (q i)) (transport (λ i → F (p i)) u)) | loopspace |
| suc | Nat → Nat | int |
| sucInt | Int → Int | int |
| sucPathInt | Path U Int Int | int |
| sucPred | (z : Int) → Path Int (sucInt (predInt z)) z | int |
| Susp | U → U | hits |
| suspMap | {A B : U} → (A → B) → Susp A → Susp B | hits |
| suspNot | Path U (Susp Bool) (Susp Bool) | hits |
| sym | {A : U} → {a b : A} → Path A a b → Path A b a | basic |
| symInv | {A : U} → {a b : A} → (p : Path A a b) → Path (Path A a b) (sym (sym p)) p | basic |
| t2 | (i : I) → Trunc Bool | hits |
| trans | {A : U} → {a b c : A} → Path A a b → Path A b c → Path A a c | basic |
| transport | {A B : U} → Path U A B → A → B | basic |
| transportInv | {A B : U} → (p : Path U A B) → (x : A) → Path A (transport (λ i → p ~i) (transport p x)) x | loopspace |
| transportInvLoop | (y : Int) → Path Int (transport (λ i → helix (invLoop i)) y) (predInt y) | loopspace |
| transportLoop | (x : Int) → Path Int (sucInt x) (transport (λ i → helix (loopP i)) x) | loopspace |
| transportRefl | {A : U} → (x : A) → Path A (transport (λ i → A) x) x | basic |
| true | Bool | bool |
| Trunc | U → U | hits |
| truncIsProp | (A : U) → isProp (Trunc A) | hits |
| truncRec | {A B : U} → isProp B → (A → B) → Trunc A → B | hits |
| tt | Unit | basic |
| ua | {A B : U} → Equiv A B → Path U A B | equiv |
| uaβ | {A B : U} → (e : Equiv A B) → (x : A) → Path B (e.1 x) (transport (ua e) x) | equiv |
| unglueI | {A : U} → (w : (T : U) × Equiv T A) → (i : I) → GlueI w i → A | univalence |
| unglueIsEquivI | {A : U} → (w : (T : U) × Equiv T A) → (i : I) → isEquiv (unglueI w i) | univalence |
| Unit | U | basic |
| winding | Path S1 base base → Int | circle |
| windingNeg | (n : Nat) → Path Int (winding (intLoopNeg n)) (negsuc n) | loopspace |
| windingPos | (n : Nat) → Path Int (winding (intLoopPos n)) (pos n) | loopspace |
| zero | Nat | int |