\import Category
\import Category.CartesianClosed
\import Category.Limit
\import Category.Subobj
\import Equiv
\import Function.Meta
\import Logic
\import Logic.Meta
\import Logic.Unique
\import Meta
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set.SetCategory
\open PrecatWithBprod

\class PrecatWithSubobjClassifier \extends FinCompletePrecat {
  | Omega : Ob
  | Omega-true : Subobj Omega
  | Omega-univ {c : Ob} : IsEquiv {Hom c Omega} {Subobj c} (\lam h => subobjPullback h Omega-true)

  \func Omega-char {c : Ob} (s : Subobj c) : Hom c Omega
    => IsEquiv.ret Omega-univ s

  \lemma Omega-char-unique {c : Ob} {h1 h2 : Hom c Omega} (p : subobjPullback h1 Omega-true = subobjPullback h2 Omega-true) : h1 = h2
    => IsEquiv.isInj Omega-univ p

  \sfunc Omega-true-map : Hom terminal Omega
    => char.center.
    \where {
      \protected \lemma char : Contr (\Sigma (t : Hom terminal Omega) (Omega-true = inso~ (point-splitMono {_} {_} {t})))
        => cases (Omega-true arg addPath) \with {
          | in~ m, p =>
            \have term : IsTerminal m.dom => \lam {c} => isProp=>isContr
                    (\lam h1 h2 => m.isMono $ Omega-char-unique $ subobjPullback_o *> subobjPullback-top (subobjPullback-self p) *> inv (subobjPullback-top (subobjPullback-self p)) *> inv subobjPullback_o) $
                    (subobjPullback-char {_} {_} {idIso} p $ IsEquiv.f_ret Omega-univ).center.pbProj2
            \in isProp=>isContr (\lam t t' => ext \case =_<= (inv t. *> t'.) \with {
              | inP r => inv r. *> pmap (_ ∘) terminal-unique *> id-right
            }) (m.f ∘ term.center, <=-antisymmetric (inP (terminalMap, o-assoc *> pmap (_ ∘) (isContr=>isProp term _ _) *> id-right)) (inP (term.center, idp)))
        }
    }

  \lemma Omega-true_Omega-true-map : Omega-true = inso~ (point-splitMono {_} {_} {Omega-true-map})
    => rewrite (\peval Omega-true-map) Omega-true-map.char.center.

  \sfunc Omega-pullback (m : Mono {\this}) : Pullback (Omega-char (inso~ m)) Omega-true-map m.dom m
    => (subobjPullback-char {_} {point-splitMono} Omega-true_Omega-true-map $ IsEquiv.f_ret Omega-univ {inso~ m}).center

  \lemma mono-regular (m : Mono {\this}) : IsRegularMono m.f
    => regularMono_pullback (Omega-pullback m) (splitMono_regular point-splitMono)
}

\class PrecatWithPowerObject \extends FinCompletePrecat {
  | Power : Ob -> Ob
  | Power-belongs (a : Ob) : Subobj {\this} (Bprod a (Power a))
  | Power-univ {c a : Ob} : IsEquiv {Hom c (Power a)} {Subobj {\this} (Bprod a c)} (\lam h => subobjPullback (prodMap id h) (Power-belongs a))

  \func Power-char {c a : Ob} (s : Subobj (Bprod a c)) : Hom c (Power a)
    => IsEquiv.ret Power-univ s

  \lemma pullback_Power {c a : Ob} {s : Subobj (Bprod a c)} : subobjPullback (prodMap id (Power-char s)) (Power-belongs a) = s
    => IsEquiv.f_ret Power-univ

  \lemma Power_pullback {c a : Ob} {f : Hom c (Power a)} : Power-char (subobjPullback (prodMap id f) (Power-belongs a)) = f
    => IsEquiv.ret_f Power-univ

  \lemma Power-char_o {a b c : Ob} {f : Hom a b} {s : Subobj (Bprod c b)} : Power-char s ∘ f = Power-char (subobjPullback (prodMap id f) s)
    => IsEquiv.isInj Power-univ $ pmap (subobjPullback __ _) (inv prod-id-left) *> subobjPullback_o *> pmap (subobjPullback _) pullback_Power *> inv pullback_Power

  \lemma Power_lift-char {a b c : Ob} {f : Hom a b} {s : Subobj (Bprod c b)}
    : subobjLifts (prodMap id f) s <-> (Power-char s ∘ f = Power-char subobjTop)
    => rewrite pullback_Power in revered {_} {_} {_} {_} {f} {Power-char s}
    \where {
      \protected \lemma revered {g : Hom b (Power c)}
        : subobjLifts (prodMap id f) (subobjPullback (prodMap id g) (Power-belongs c)) <-> (g ∘ f = Power-char subobjTop)
        => <->trans subobjPullback-lifts $ transportInv (subobjLifts __ _ <-> _) prod-id-left $
            <->trans subobjLifts_top (\lam p => inv Power_pullback *> pmap Power-char p, later \lam p => rewrite p pullback_Power)
    }

  \lemma Power-char_top {c b a : Ob} {f : Hom c b} : Power-char subobjTop ∘ f = Power-char (subobjTop {_} {Bprod a c})
    => IsEquiv.isInj Power-univ $ pmap (subobjPullback __ _) (inv prod-id-left) *> subobjPullback_o *> pmap (subobjPullback _) pullback_Power *> subobjPullback_top *> inv pullback_Power

  \func Power-singleton (c : Ob) : Hom c (Power c)
    => Power-char (subobjEq c)

  \lemma Power-singleton-mono {c : Ob} : Mono (Power-singleton c) \cowith
    | isMono {_} {g} p => subobjEq-lifts. $ transport (subobjLifts _) pullback_Power $ subobjPullback-lifts. $ transport (subobjLifts __ _)
      (pair-unique (inv o-assoc *> pmap (∘ _) (beta1 *> id-left) *> beta1 *> inv (pmap (∘ _) (beta1 *> id-left) *> beta1) *> o-assoc)
                   (inv o-assoc *> pmap (∘ _) beta2 *> o-assoc *> pmap (_ ∘) beta2 *> p *> inv (pmap (∘ _) beta2 *> o-assoc *> pmap (_ ∘) beta2) *> o-assoc)) $
      subobjPullback-lifts. $ transportInv (subobjLifts _) pullback_Power $ subobjEq-lifts. idp

  \sfunc Power-singleton-subobj (c : Ob) : Subobj (Power c)
    => inso~ Power-singleton-mono

  \sfunc PHom (b c : Ob) : Equalizer (Power-char (subobjPullback psmap (Power-singleton-subobj c))) (Power-char subobjTop)
    => equalizer
    \where {
      \protected \func psmap : Hom (Bprod b (Power (Bprod c b))) (Power c)
        => Power-char $ subobjPullback associator-iso.hinv (Power-belongs _)
    }

  \func PHom-eval {b c : Ob} : Hom (Bprod (PHom b c) b) c
    => char.
    \where {
      \protected \sfunc char : \Sigma (eval : Hom (Bprod (PHom b c) b) c) (Power-singleton c ∘ eval = PHom.psmap ∘ pair proj2 (Equalizer.eql ∘ proj1))
        => \have (g,p) => subobjLifts.toMap (\peval Power-singleton-subobj c) $ subobjPullback-lifts. $ (Power_lift-char {_} {_} {_} {b} {(PHom b c).eql}). $ Equalizer.equal *> Power-char_top
           \in (g ∘ swap, inv o-assoc *> pmap (∘ _) p *> o-assoc *> pmap (_ ∘) (pair-unique
                (inv o-assoc *> pmap (∘ _) (beta1 *> id-left) *> beta1 *> inv beta1)
                (inv o-assoc *> pmap (∘ _) beta2 *> o-assoc *> pmap (_ ∘) beta2 *> inv beta2)))
    }

  \lemma PHom-univ {a b c : Ob} : IsEquiv {Hom a (PHom b c)} {Hom (Bprod a b) c} (\lam g => PHom-eval ∘ prodMap g id)
    => IsEquiv.fromInjSurj (\lam {g} {g'} p =>
          \have | t => pmap (subobjPullback (prodMap id swap ∘ associator)) $ subobjPullback_o *> IsEquiv.isInj (IsEquiv.ret-equiv Power-univ)
                        (inv Power-char_o *> inv o-assoc *> pmap (∘ _) (inv PHom-eval.char.) *> o-assoc *> pmap (Power-singleton c ∘) p *> inv o-assoc *> pmap (∘ _) PHom-eval.char. *> o-assoc *> Power-char_o) *> inv subobjPullback_o
                | lem g : associator-iso.hinv ∘ prodMap id (pair proj2 (Equalizer.eql ∘ proj1) ∘ prodMap g id) ∘ (prodMap id swap ∘ associator) = prodMap id (Equalizer.eql ∘ g)
                  => pmap (_ ∘ prodMap _ __ ∘ _) (pair-comp *> pmap2 pair (beta2 *> id-left) (o-assoc *> pmap (_ ∘) beta1)) *> pmap2 (_ ∘ pair __ __ ∘ _) id-left pair-comp *> pmap (∘ _) associator-inv-pair *> pair-comp *> pmap2 pair
                      (pair-comp *> pmap2 pair (inv o-assoc *> pmap (∘ _) beta1 *> pmap (∘ _) id-left *> beta1) (o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) beta2 *> o-assoc *> pmap (_ ∘) beta2) *> inv o-assoc *> pmap (∘ _) beta2 *> beta1) *> inv pair-comp *> pmap (∘ _) pair-eta)
                      (o-assoc *> o-assoc *> pmap (_ ∘) (o-assoc *> pmap (_ ∘) (pmap (_ ∘) (inv o-assoc *> pmap (∘ _) beta2 *> o-assoc) *> inv o-assoc *> pmap2 (∘) beta1 beta2 *> beta2)) *> inv o-assoc)
          \in Equalizer.eqMono $ IsEquiv.isInj Power-univ $ pmap (subobjPullback __ _) (inv (lem g)) *> subobjPullback_o *> t *> inv subobjPullback_o *> pmap (subobjPullback __ _) (lem g'))
        \lam h => inP (Equalizer.eqMap (Power-char (graph h)) (graph-eq h), Power-singleton-mono.isMono $ inv o-assoc *> pmap (∘ _) PHom-eval.char. *> o-assoc *>
          pmap (_ ∘) (pair-comp *> pmap2 pair (beta2 *> id-left) (o-assoc *> pmap (_ ∘) beta1 *> inv o-assoc *> pmap (∘ _) Equalizer.eqBeta)) *>
          IsEquiv.isInj Power-univ (pmap (subobjPullback __ _) (inv prod-id-left) *> subobjPullback_o *> pmap (subobjPullback _) pullback_Power *> inv subobjPullback_o *>
          pmap (subobjPullback __ _) (pmap (_ ∘) (pmap (prodMap _) (inv $ pair-comp *> pmap2 pair (o-assoc *> id-left *> beta1) (o-assoc *> pmap (_ ∘) beta2)) *> inv prod-id-left) *> inv o-assoc *> pmap (∘ _) (inv associator-inv-prod) *> pmap (\lam r => prodMap r _ ∘ _ ∘ _) prod-id *> o-assoc) *>
          subobjPullback_o *> pmap (subobjPullback _) pullback_Power *> inv subobjPullback_o *> pmap (subobjPullback __ _)
            (o-assoc *> pmap (_ ∘) (inv o-assoc *> pmap (∘ _) associator-iso.f_hinv *> id-left) *> prod-id-left *> pmap (prodMap _) (o-assoc *> pmap (h ∘) (swap-pair *> pair-eta) *> id-right)) *>
          pmap (subobjPullback _) (inv pullback_Power) *> inv subobjPullback_o *> pmap (subobjPullback __ _) prod-id-left))
    \where {
      \func graph (h : Hom (Bprod a b) c) : Subobj (Bprod (Bprod c b) a)
        => subobjPullback (prodMap id (h ∘ swap) ∘ associator) (subobjEq c)

      \lemma graph-eq (h : Hom (Bprod a b) c)
        : Power-char (subobjPullback PHom.psmap (Power-singleton-subobj c)) ∘ Power-char (graph h) = Power-char subobjTop ∘ Power-char (graph h)
        => Power_lift-char. (subobjPullback-lifts. $ rewrite (\peval Power-singleton-subobj c) $ inP (h ∘ swap, IsEquiv.isInj Power-univ $
            pmap (subobjPullback __ _) (inv prod-id-left) *> subobjPullback_o *> pmap (subobjPullback _) pullback_Power *>
            inv (pmap (subobjPullback __ _) (inv prod-id-left) *> subobjPullback_o *> pmap (subobjPullback _) pullback_Power *>
            inv subobjPullback_o *> pmap (subobjPullback __ _) (inv associator-inv-prod *> pmap (prodMap __ _ ∘ _) prod-id) *>
            subobjPullback_o *> pmap (subobjPullback _) pullback_Power *> inv subobjPullback_o *>
            pmap (subobjPullback __ _) (o-assoc *> pmap (_ ∘) associator-iso.f_hinv *> id-right)))) *> inv Power-char_top
    }
}

\class ToposPrecat \extends PrecatWithSubobjClassifier, CartesianClosedPrecat, PrecatWithPowerObject
  \where {
    -- TODO: Make constructor classes
    \class FromSubobjClassifier \extends ToposPrecat
      | Power a => CHom a Omega
      | Power-belongs a => subobjPullback (CHom-eval ∘ pair proj2 proj1) Omega-true
      | Power-univ {c} {a} => transport IsEquiv
          (ext \lam h => inv subobjPullback_o *> pmap (subobjPullback __ _) (o-assoc *> pmap (_ ∘) (inv swap-prod) *> inv o-assoc) *> subobjPullback_o) $
          IsEquiv.trans CHom-univ $ IsEquiv.trans (Omega-univ {\this} {Bprod c a}) $ inP (subobjPullback_Iso-equiv swap-iso)

    \class FromPowerObject \extends ToposPrecat
      | Omega => Power terminal
      | Omega-true => subobjPullback (pair terminalMap id) (Power-belongs terminal)
      | Omega-univ => transport IsEquiv
          (ext \lam h => inv subobjPullback_o *> pmap (subobjPullback __ _) (pair-unique terminal-unique $ inv o-assoc *> pmap (∘ _) beta2 *> o-assoc *> pmap (h ∘) beta2 *> id-right *> inv id-left *> pmap (∘ h) (inv beta2) *> o-assoc) *> subobjPullback_o) $
          IsEquiv.trans Power-univ $ inP (subobjPullback_Iso-equiv Bprod_terminal-left)
      | CHom b c => PHom b c
      | CHom-eval => PHom-eval
      | CHom-univ => PHom-univ
  }

\instance SetTopos.{u} : ToposPrecat.FromSubobjClassifier (\Set u)
  | FinCompletePrecat => SetBicat.{u}
  | CartesianClosedPrecat => SetCartesianClosed.{u}
  | Omega => \Prop
  | Omega-true => inso~ \new Mono {
    | dom => \Sigma
    | f _ => \Sigma
    | isMono _ => idpe \lam _ => ()
  }
  | Omega-univ {X} => inP \new QEquiv {
    | ret s x => \case \elim s \with {
      | in~ m => ∃ (y : m.dom) (m.f y = x)
      | ~-equiv m1 m2 r => propExt
        (\lam (inP (y,p)) => inP (r. y, path (\lam i => r. i y) *> p))
        (\lam (inP (y,p)) => inP (r. y, path (\lam i => r. i y) *> p))
    }
    | ret_f P => ext \lam x => propExt (\lam (inP s) => transport P s. $ propExt.conv s.. ()) \lam Px => inP ((x, (), propExt (\lam _ => ()) (\lam _ => Px)), idp)
    | f_sec => \case \elim __ \with {
      | in~ m => <=-antisymmetric (
        \have me {x} (p : ∃ (y : m.dom) (m.f y = x)) : \Sigma (y : m.dom) (m.f y = x) => TruncP.remove (\lam s s' => ext $ SetCat.mono-char. m $ s. *> inv s'.) p
        \in inP (\lam d => (me $ propExt.conv d. ())., ext \lam d => (me $ propExt.conv d. ()).)) (inP (\lam d => (m.f d, (), propExt (\lam _ => ()) (\lam _ => inP (d,idp))), idp))
    }
  }