\import Data.Or
\import Equiv
\import Equiv.Path
\import Equiv.Univalence
\import HLevel
\import Logic
\import Meta
\import Paths
\import Paths.Meta

\lemma Set-lemma' {A : \Type} (R : A -> A -> \Type) (c : \Pi {a a' : A} -> isProp (R a a')) (p : \Pi {a : A} -> R a a) (q : \Pi {a a' : A} -> R a a' -> a = a') : isSet A
  => \lam a a' => transport isProp {R a a'} (inv (univalence.ret (pathEquiv R (\lam {a} {a'} => \new Retraction (rewrite __ p) q (\lam _ => c _ _))))) c

\lemma Set-lemma {A : \Type} (R : A -> A -> \Prop) (p : \Pi {a : A} -> R a a) (q : \Pi {a a' : A} -> R a a' -> a = a') : isSet A
  => Set-lemma' R (\lam {_} {_} => prop-isProp) p q

\lemma Hedberg {A : \Type} (d : \Pi (a a' : A) -> (a = a') `Or` (a /= a')) : isSet A
  => Set-lemma
      (\lam a a' => \case d a a' \with {
        | inl _ => \Sigma
        | inr _ => Empty
      })
      (\lam {a} => cases (d a a) \with {
        | inl _ => ()
        | inr q => q idp
      })
      (\lam {a} {a'} s => cases (d a a', s) \with {
        | inl p, _ => p
        | inr _, s' => absurd s'
      })