\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'
      }

    \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'
  => \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')

\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.)

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

\func ElemOf (l : Array \Type) => 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