{- Set Theory: - Stability and Discretness leads to Set Copyright (c) Groupoid Infinity, 2014-2018. -} module hedberg where import proto import path import iso hedbergLemma (A: U) (a b:A) (f: (x: A) -> Path A a x -> Path A a x) (p: Path A a b): Square A a a a b (refl A a) p (f a (refl A a)) (f b p) = comp ( Square A a a a (p @ i) (<_> a) ( p @ i /\ j) (f a (<_> a)) (f (p @ i) ( p @ i /\ j))) ( f a (<_> a)) [] hedbergStable (A: U) (a b: A) (h: (x: A) -> stable (Path A a x)) (p q: Path A a b): Path (Path A a b) p q = comp (<_> A) a [ (j = 0) -> (hedbergLemma A a b f p) @ i, (j = 1) -> (hedbergLemma A a b f q) @ i, (i = 0) -> ((rem1 a).1) (refl A a), (i = 1) -> (fConst b p q) @ j ] where rem1 (x: A): exConst (Path A a x) = stableConst (Path A a x) (h x) f (x: A): Path A a x -> Path A a x = (rem1 x).1 fConst (x: A): isConst (Path A a x) (f x) = (rem1 x).2 hedbergS (A:U) (h: (a x:A) -> stable (Path A a x)): isSet A = \ (a b: A) -> hedbergStable A a b (h a) hedberg (A:U) (h: discrete A): isSet A = \ (a b: A) -> hedbergStable A a b (\(b : A) -> decStable (Path A a b) (h a b))