module VanDoornDissertation.HIT where open import HottBook.Chapter1
3 Higher Inductive Types
3.1 Propositional Truncation
postulate one-step-truncation : Set → Set f : {A : Set} → A → one-step-truncation A e : {A : Set} → (x y : A) → f x ≡ f y -- data one-step-truncation (A : Set) : Set where -- f : A → one-step-truncation A -- e : (x y : A) → f x ≡ f y weakly-constant : {A B : Set} → (g : A → B) → Set weakly-constant {A} g = {x y : A} → g x ≡ g y definition3∙1∙1 : {A : Set} → one-step-truncation A → ℕ → Set definition3∙1∙1 {A} trunc zero = A definition3∙1∙1 {A} trunc (suc n) = one-step-truncation (definition3∙1∙1 trunc n) fs : {A : Set} → one-step-truncation A → (n : ℕ) → Set fs trunc n = (definition3∙1∙1 trunc n) → (definition3∙1∙1 trunc (suc n)) -- lemma3∙1∙3 : {X : Set} → {x : X} → is