Maps
Table of Contents
1 Maps
module Lib.Data.Map where
This file is deprecated. It provides the definition of composition (that is easier to write directly due to the non-type inference) and injectivity that is usually spelled out more directly.
1.1 Packages imports
1.2 Composition
map/comp (A B C : U) (g : B → C) (f : A → B) : A → C = λx. g (f x)
1.3 Injection
A map f : A \to B is said injective when x = y whenever f x = f y. By contraposition, it also means that if f x \neq f y, then x \neq y.
is-injective (A B : U) (f : A → B) : U = (x y : A) → Path B (f x) (f y) → Path A x y is-injective' (A B : U) (f : A → B) : U = (x y : A) → neg (Path A x y) → neg (Path B (f x) (f y))
We show that these two versions are actually equivalent.
is-injective/is-injective' (A B : U) (f : A → B) (i : is-injective A B f) : is-injective' A B f = λx y np p. np (i x y p)