hitslib/hits.ktt

Propositional truncation and suspensions.

8 declarations, all certified by the kernel · source

1import bool
2 
3-- Propositional truncation
4✓data Trunc (A : U) : U :=
5  | inc (a : A)
6  | squash (x y : Trunc A) (i : I) [i = 0 -> x, i = 1 -> y]
7 
8 
9✓def truncIsProp (A : U) : isProp (Trunc A) := \x y i -> squash x y i
10 
11✓def truncRec {A B : U} (h : isProp B) (f : A -> B) : Trunc A -> B
12  | inc a => f a
13  | squash x y i => h (truncRec h f x) (truncRec h f y) i
14 
15-- Suspension
16✓data Susp (A : U) : U :=
17  | north
18  | south
19  | merid (a : A) (i : I) [i = 0 -> north, i = 1 -> south]
20 
21✓def meridP {A : U} (a : A) : Path (Susp A) north south := \i -> merid a i
22 
23✓def suspMap {A B : U} (f : A -> B) : Susp A -> Susp B
24  | north => north
25  | south => south
26  | merid a i => merid (f a) i
27 
28-- transport in a family of suspensions
29✓def suspNot : Path U (Susp Bool) (Susp Bool) := \i -> Susp (notPath i)
30 
31 
32✓def t2 (i : I) : Trunc Bool := transport (\i -> Trunc (notPath i)) (squash (inc true) (inc false) i)