{- 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 (<i> Square A a a a (p @ i) (<_> a) (<j> p @ i /\ j)
             (f a (<_> a)) (f (p @ i) (<j> p @ i /\ j))) (<i> 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 =
   <j i> 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))