{- Truncations: - Propositional (-1), Set (0), Groupoid (1). Copyright (c) Groupoid Infinity, 2014-2018. HoTT 6.9 Truncations -} module trunc where import path import prop data pTrunc (A : U) -- (-1)-trunc, mere proposition truncation = inc (a : A) | inh (x y : pTrunc A) [ (i=0) -> x, (i=1) -> y ] pTruncIsProp (A : U) : isProp (pTrunc A) = \ (x y : pTrunc A) -> inh{pTrunc A} x y @ i pTruncRec (A B : U) (pP : isProp B) (f : A -> B) : pTrunc A -> B = split inc a -> f a inh x y @ i -> pP (pTruncRec A B pP f x) (pTruncRec A B pP f y) @ i pTruncElim (A : U) (B : (pTrunc A) -> U) (pP : (x : pTrunc A) -> isProp (B x)) (f : (a : A) -> B (inc a)) : (x : pTrunc A) -> B x = split inc a -> f a inh x y @ i -> lemPropF (pTrunc A) B pP x y ( inh{pTrunc A} x y @ j) (pTruncElim A B pP f x) (pTruncElim A B pP f y) @ i data sTrunc (A : U) -- (0)-trunc, set truncation = inc (a : A) | line (a b: sTrunc A) (p q: Path (sTrunc A) a b) [ (i=0) -> p @ j, (i=1) -> q @ j, (j=0) -> a, (j=1) -> b ] sTr (A : U) (a b : sTrunc A) (p q: Path (sTrunc A) a b) : Path (Path (sTrunc A) a b) p q = line {sTrunc A} a b p q @ i @ j sTruncRec (A: U) (B: U) (bS: isSet B) (f: A -> B): sTrunc A -> B = split inc a -> f a line a b p q @ i j -> (bS (sTruncRec A B bS f a) (sTruncRec A B bS f b) ( sTruncRec A B bS f (p @ k)) ( sTruncRec A B bS f (q @ k))) @ i @ j data gTrunc (A : U) -- (1)-trunc, groupoid truncation = inc (a : A) | squashC (a b : gTrunc A) (p q : Path (gTrunc A) a b) (r s: Path (Path (gTrunc A) a b) p q) [ (i=0) -> r @ j @ k , (i=1) -> s @ j @ k , (j=0) -> p @ k , (j=1) -> q @ k , (k=0) -> a , (k=1) -> b]