\import Algebra.Meta
\import Data.Or
\import Function.Meta
\import Logic.Unique
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta

\data Empty

\func absurd {A : \Type} (x : Empty) : A

\func Not (A : \Type) => A -> Empty

\func \infix  /= {A : \Type} (a a' : A) => Not (a = a')

\lemma /=-sym {A : \Type} {a a' : A} (p : a /= a') : a' /= a
  => \lam r => p (inv r)

\data TruncP (A : \Type)
  | inP A
  | truncP (a a' : TruncP A) : a = a'
  \where {
    \use \level levelProp {A : \Type} (a a' : TruncP A) : a = a' => path (truncP a a')

    \lemma remove {A : \Type} (p : isProp A) (t : TruncP A) : A \level p \elim t
      | inP a => a

    \lemma remove' {A : \Prop} (t : TruncP A) : A \elim t
      | inP a => a

    \lemma rec {A B : \Type} (p : isProp B) (t : TruncP A) (f : A -> B) : B \level p \elim t
      | inP a => f a

    \lemma rec-eval {A B : \Type} {p : isProp B} {a : A} {f : A -> B} : rec p (inP a) f = f a \level isProp.=>isSet p _ _
      => p _ _

    \lemma rec-set {A : \Type} {B : \Set} (t : TruncP A) (f : A -> B) (p : \Pi (a a' : A) -> f a = f a')
      : \Sigma (b : B) (∃ (a : A) (f a = b)) \level level p \elim t
      | inP a => (f a, inP (a, idp))
      \where {
        \lemma level (p : \Pi (a a' : A) -> f a = f a') : isProp (\Sigma (b : B) (∃ (a : A) (f a = b)))
          => \lam (b, inP (a,fa=b)) (b', inP (a',fa'=b')) => ext $ inv fa=b *> p a a' *> fa'=b'
      }

    \lemma rec-set-eval {A : \Type} {B : \Set} (a : A) {f : A -> B} {p : \Pi (a a' : A) -> f a = f a'} : (rec-set (inP a) f p). = f a
      => \case (rec-set (inP a) f p). \with {
        | inP (a',q) => inv q *> p a' a
      }

    \func map {A B : \Type} (t : TruncP A) (f : A -> B) : TruncP B \elim t
      | inP a => inP (f a)
  }

\lemma prop-pi {A : \Prop} {a a' : A} : a = a'
  => path \case truncP (inP a) (inP a') __ \with {
    | inP x => x
  }

\lemma prop-isProp {A : \Prop} : isProp A
  => \lam _ _ => prop-pi

\lemma set-pi {A : \Set} {a b : A} {p q : a = b} : p = q
  => prop-pi

\lemma prop-dpi (A : I -> \Prop) (a : A left) (a' : A right) : Path A a a'
  => pathOver (prop-isProp (coe A a right) a')

\lemma setPair-unext2 {A : \Set} {B : A -> \Set} {a : A} {b : B a} {b' : B a} (p : (a,b) = {\Sigma (a : A) (B a)} (a,b')) : b = b'
  => pmap (\lam x => transport B x b) (prop-pi : idp = pmap __. p) *> pmapd __. p

\data ToProp (A : \Type) (p : isProp A)
  | toProp A
  \where {
    \lemma fromProp {A : \Type} {p : isProp A} (t : ToProp A p) : A \level p \elim t
      | toProp a => a

    \use \level levelProp {A : \Type} {p : isProp A} (x y : ToProp A p) : x = y \elim x, y
      | toProp a, toProp a' => pmap toProp (p a a')
  }

\truncated \data \infixr  || (A B : \Type) : \Prop
  | byLeft A
  | byRight B
  \where {
    \lemma rec {A B C : \Type} (p : isProp C) (f : A -> C) (g : B -> C) (t : A || B) : C \level p \elim t
      | byLeft a => f a
      | byRight b => g b

    \lemma rec' {A B : \Type} {C : \Prop} (f : A -> C) (g : B -> C) (t : A || B) : C \elim t
      | byLeft a => f a
      | byRight b => g b

    \func map {A B C D : \Type} (f : A -> C) (g : B -> D) (t : A || B) : C || D \elim t
      | byLeft a => byLeft (f a)
      | byRight b => byRight (g b)

    \lemma fromOr {A B : \Type} (p : Or A B) : A || B \elim p
      | inl a => byLeft a
      | inr b => byRight b

    \lemma toOr {A B : \Type} (p : A || B) : TruncP (Or A B) \elim p
      | byLeft a => inP (inl a)
      | byRight b => inP (inr b)

    \lemma flip {A B : \Type} (e : A || B) : B || A \elim e
      | byLeft a => byRight a
      | byRight b => byLeft b
  }

\func \infix  <-> (P Q : \Prop) => \Sigma (P -> Q) (Q -> P)

\lemma <->_= {P Q : \Prop} : (P <-> Q) <-> (P = Q)
  => (\lam p => ext p, \lam p => rewrite p (\lam x => x, \lam x => x))

\lemma <->refl {P : \Prop} : P <-> P
  => (\lam p => p, \lam p => p)

\lemma <->trans {P Q S : \Prop} (f : P <-> Q) (g : Q <-> S) : P <-> S
  => (\lam p => g. (f. p), \lam s => f. (g. s))

\lemma <->sym {P Q : \Prop} (f : P <-> Q) : Q <-> P
  => (f.,f.)

-- | `Image f` is the set `{ f a | a : A }`.
\type TSetIm {A B : \Type} (f : A -> B) (b : B)
  => ∃ (a : A) (f a = b)

\lemma TSetIm-con {A B : \Type} {f : A -> B} (a : A) : TSetIm f (f a)
  => inP (a,idp)

\lemma TSetIm-elim {A B : \Type} {C : B -> \Prop} {f : A -> B} (c : \Pi (a : A) -> C (f a)) {b : B} (s : TSetIm f b) : C b \elim s
  | inP (a,p) => transport C p (c a)

-- | `SetIm f P` is the set `{ f a | a : A, P a }`.
\type SetIm {A B : \Type} (f : A -> B) (P : A -> \Type) (b : B)
  => TSetIm (\lam (s : Given P) => f s.) b

\lemma SetIm-con {A B : \Type} {f : A -> B} {P : A -> \Type} {a : A} (Pa : P a) : SetIm f P (f a)
  => inP ((a,Pa),idp)

\lemma SetIm-cone {A B : \Type} {f : A -> B} {P : A -> \Type} (a : A) (Pa : P a) : SetIm f P (f a)
  => inP ((a,Pa),idp)

\lemma SetIm-elim {A B : \Type} {C : B -> \Prop} {f : A -> B} {P : A -> \Type} (c : \Pi {a : A} -> P a -> C (f a)) {b : B} (s : SetIm f P b) : C b
  => TSetIm-elim (\lam t => c t.) s

\lemma SetIm_id {A : \Type} {P : A -> \Prop} : SetIm (\lam x => x) P = P
  => ext \lam a => propExt (SetIm-elim \lam p => p) SetIm-con

\lemma SetIm_o {A B C : \Type} {f : A -> B} {g : B -> C} {P : A -> \Prop} : SetIm (\lam x => g (f x)) P = SetIm g (SetIm f P)
  => ext \lam c => ext (SetIm-elim \lam p => SetIm-con $ SetIm-con p, SetIm-elim $ SetIm-elim SetIm-con)

\lemma SetIm_TSetIm {A B C : \Type} {f : A -> B} {g : B -> C} : SetIm g (TSetIm f) = TSetIm (\lam a => g (f a))
  => ext \lam c => propExt (SetIm-elim $ TSetIm-elim TSetIm-con) (TSetIm-elim \lam a => SetIm-con $ TSetIm-con a)

\func OneOf (l : Array \Prop) => ∃ (P : l) P

\func ElemOf (l : Array \Prop) => Given (P : l) P

\type arraySubset {X : \Type} (l : Array X) (x : X) => ∃ (y : l) (y = x)

\lemma propExt {A B : \Prop} (f : A -> B) (g : B -> A) : A = B =>
  path (iso f g (\lam _ => prop-pi) (\lam _ => prop-pi))
  \where {
    \lemma dir {A B : \Prop} (p : A = B) (a : A) : B => transport (\lam X => X) p a

    \lemma conv {A B : \Prop} (p : A = B) (b : B) : A => dir (inv p) b
  }

\meta isProp-prover => \lam x y => cases (x,y) (cong prop-pi <|> contradiction)

\class NegatedProp (P : \Prop)
  | isNegated : Not (Not P) -> P

\instance EmptyNegated : NegatedProp Empty
  | isNegated p => p \lam x => x