\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta

\class InjData (f : \Prop -> \Prop) (inj : \Pi {A B : \Prop} -> f A = f B -> A = B) {
  \lemma PropFin (A : \Prop) : f (f A) = A => inj $ propExt
    (\lam p => run {
      aux at p,
      inj at p,
      equals=>true (inv p)
    })
    (\lam p => run {
      rewrite (true=>equals p),
      rewrite (aux p) p
    })

  \lemma aux {P : \Prop} (h : f P) : f (\Sigma) = P
    => propExt (\lam p => equals=>true (inj (true=>equals h *> inv (true=>equals p))))
               (\lam p => transport f (true=>equals p) h)

  \lemma true=>equals {P : \Prop} (h : P) : P = (\Sigma)
    => propExt (\lam p => ()) (\lam _ => h)

  \lemma equals=>true {P : \Prop} (p : P = (\Sigma)) : P
    => rewrite p ()
}