Sets Properties
Table of Contents
1 Sets properties
module Lib.Prop.Set where
This file contains properties of sets.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Stdlib.Prelude import Lib.Data.Nat import Lib.Prop.Comp
1.2 Axiom K
Axiom K is a notion of proof irrelevance: it states that the only proof of identity for an object is the reflexivity.
axiom-K (A : U) : U = (x : A) → (p : Path A x x) → Path (Path A x x) (refl A x) p
Actually, we show that types are sets iff they satisfy axiom K. A set obviously satisfies axiom K, almost by definition.
is-set/axiom-K (A : U) (s : is-set A) : axiom-K A = λx. s x x (refl A x)
Conversely, if A satisfies axiom K, then for any p, q : Path A x y, we have p ⋅ q-1 = refl. So p = q.
axiom-K/is-set (A : U) (ax : axiom-K A) : is-set A = λx y p q. let a : Path A x y = comp A x y p y (refl A y) b : Path A x y = comp A x y p y (comp A y x (inv A x y q) y q) c : Path A x y = comp A x x (comp A x y p x (inv A x y q)) y q d : Path A x y = comp A x x (refl A x) y q in comp-n (Path A x y) five-Nat p a (refl/comp-r A x y p) b (ap (Path A y y) (Path A x y) (λr. comp A x y p y r) (refl A y) (comp A y x (inv A x y q) y q) (comp/inv-l' A x y q)) c (comp/assoc' A x y p x (inv A x y q) y q) d (ap (Path A x x) (Path A x y) (λr. comp A x x r y q) (comp A x y p x (inv A x y q)) (refl A x) (inv (Path A x x) (refl A x) (comp A x y p x (inv A x y q)) (ax x (comp A x y p x (inv A x y q))))) q (comp/ident-l A x y q)
1.3 Universe of sets
UU-Set : U = Σ U is-set Set/type (A : UU-Set) : U = A.1 Set/is-set (A : UU-Set) : is-set (Set/type A) = A.2 Set/hom (A B : UU-Set) : U = (Set/type A) → (Set/type B)