\import Algebra.Meta
\import Category
--\import Category.Adjoint
\import Category.CartesianClosed
\import Category.Coreflection
\import Category.Limit
--\import Category.Subobj
--\import Category.SubobjectPoset
\import Equiv
\import Function (IsInj)
\import Function.Meta
\import Logic
\import Meta
--\import Order.PartialOrder
\import Paths
\import Paths.Meta
--\import Relation.Equivalence
\import Set.SetCategory
--\import Topology.Locale
\open PrecatWithBprod

\class ToposPrecat \extends FinCompletePrecat, CartesianClosedPrecat {
  -- subobject classifier map

  | subobj-classifier \alias omega : Ob
  | true-map : Hom terminal omega

  -- characteristic maps

  | char-map {S B : Ob} (m : Mono {\this} {S} {B}) : Hom B omega
  | char-pullback {S B : Ob} (m : Mono {\this} {S} {B}) : Pullback {\this} (char-map m) true-map S m terminalMap
  | char-unique {S B : Ob} {m : Mono {\this} {S} {B}} {phi : Hom B omega}
                (phi-pull : Pullback phi true-map S m terminalMap) : phi = char-map m

  -- omega is exponentiable

  | p-exponential : isExponentiable omega

  \default p-exponential => CartesianClosedPrecat.is-exponentiable omega

  \use \func Power (B : Ob) : Ob
    => p-exponential B

  \use \func belongs {B : Ob} : Hom (Bprod (Power B) B) omega
    => corefl-map {p-exponential B}

  \use \func p-transpose {A B : Ob} (f : Hom (Bprod A B) omega) : Hom A (Power B)
    => ret {isCoreflection {p-exponential B}} f

  \use \lemma p-transpose-univ {A B : Ob} (f : Hom (Bprod A B) omega) : f = belongs ∘ (prodMap (p-transpose f) (id B))
    => inv $ Equiv.f_ret {isCoreflection {p-exponential B}} f

  \use \lemma p-transpose-unique {A B : Ob} {f : Hom (Bprod A B) omega} {g : Hom A (Power B)} (comm : f = belongs ∘ prodMap g (id B)) : g = p-transpose f
    => Equiv.adjoint {isCoreflection {p-exponential B}} (inv comm)

  \use \func anti-transpose  {A B : Ob} (g : Hom A (Power B)) : Hom (Bprod A B) omega
    => belongs ∘ (prodMap g (id B))

  \use \lemma antitranspose-eq {A B : Ob} (f : Hom (Bprod B A) omega) : f = anti-transpose (p-transpose f)
    => p-transpose-univ f

  \use \lemma transpose-inj {A B : Ob} {f g : Hom (Bprod A B) omega} (e : p-transpose f = p-transpose g) : f = g
    => p-transpose-univ f *> pmap (belongs ∘ prodMap __ (id B)) e *> (inv $ p-transpose-univ g)

--  \func subobject-equiv (C : Ob) : Equiv {SubobjectPoset C} {Hom C omega} => \new QEquiv {
--    | f => from-subobj
--    | ret m => in~ (from-char-map m)
--    | ret_f sub =>
--      \let equiv => ~-equiv {SubobjPreorder C} {Preorder.EquivRel.~} \in
--      \case\elim sub \with {
--      | in~ a => \case\elim a \with {
--        | subobj sub m => equiv (from-char-map (from-subobj (in~ (subobj sub m)))) (subobj sub m)
--            $ (inP (Iso.hinv {pb-of-char-iso m}, unfold $ unfold Pullback.unique.p-map $
--                                                          \let s => pbBeta1 {char-pullback m} {sub} {Mono.f {m}} {terminalMap} \in
--                                                          unfold at s $ {?}), {?}) -- this is the same as to say that pullbacks are equal
--      }
--  }
--    | f_sec c => inv $ char-unique $ unfold {?}
--  }
--    \where {
--      \func from-subobj (x : SubobjectPoset C) : Hom C omega
--      \elim x
--        | in~ a => \case\elim a \with {
--          | subobj _ m => char-map m
--        }
--        | ~-equiv x y (r1, r2) => \case\elim x, \elim y, \elim r1, \elim r2 \with {
--          | subobj a m1, subobj b m2, eq1, eq2 =>
--            \let | (h1, eq1') => SubobjPreorder.extractMap {_} {C} m2 eq1
--                 | (h2, eq2') => SubobjPreorder.extractMap {_} {C} m1 eq2
--                 | iso => SubobjPreorder.antisymmetric m2 m1 (inP $ (h2, eq2')) (inP $ (h1, eq1'))
--                 | iso-mono => Iso.isMono {iso}
--            \in
--              char-unique (\new Pullback {
--                | pbCoh => rewriteI (eq2', o-assoc) $ rewrite (pbCoh {char-pullback m1}, o-assoc, terminate) idp
--                | pbMap {w} p1 n coh => h1 ∘ pbMap {char-pullback m1} {w} p1 n coh
--                | pbBeta1 => rewriteI o-assoc $ rewrite (eq1', pbBeta1 {char-pullback m1}) idp
--                | pbBeta2 => terminal-unique
--                | pbEta {w} {g} {h} coh _ =>
--                  \let | c => pbEta {char-pullback m1} {w} {h2 ∘ g} {h2 ∘ h} (rewrite (inv o-assoc, eq2', inv o-assoc, eq2') coh) terminal-unique
--                  \in
--                    iso-mono {w} {g} {h} c
--              })
--        }

--      \func pb-of-char-iso {B C : Ob} (m : Mono {\this} {B} {C})
--        => Pullback.unique (char-map m) true-map (char-pullback m) (pullback (char-map m) true-map)
--
--      \func from-char-map (m : Hom C omega) : SubobjPreorder C =>
--        \let
--          | true-mono => global-section true-map
--          | pb-of-mono => Pullback.pullback-of-mono' {_} {_} {_} {_} {_} {true-mono} (pullback m true-map)
--        \in
--          subobj (Pullback.apex {pullback m true-map}) pb-of-mono
--    }

  \use \func internal-equality \alias eq (B : Ob) : Hom (Bprod B B) omega
    => char-map (diagonal.isSplitMono B)

  \use \func singleton (B : Ob) : Hom B (Power B)
    => p-transpose (eq B)

  -- 'char-rel' gives the characteristic map of the functional relation corresponding to f.

  \use \func char-rel {B C : Ob} (f : Hom B C) : Hom (Bprod B C) omega
    => eq C ∘ prodMap f (id C)

  \use \lemma eqq-p-transpose-s {B X : Ob} (b : Hom X B) : singleton B ∘ b = p-transpose (char-rel b)
    => p-transpose-unique {\this} {_} {_} {char-rel b} $ rewrite (prod-id-right _ _, inv o-assoc, inv $ p-transpose-univ _) idp

  \private \use \lemma pbBeta2' {B X : Ob} {b : Hom X B} (w : Ob) (p1 : Hom w (Bprod X B))
                 (p2 : Hom w B) (c : prodMap b (id B) ∘ p1 = diagonal B ∘ p2) : b ∘ (proj1 ∘ p1) = p2 =>
    \let left : proj1 ∘ (diagonal B ∘ p2) = p2 => rewriteI o-assoc $ rewrite (beta1 _ _) equation
         | right : proj1 ∘ (prodMap b (id B) ∘ p1) = b ∘ (proj1 ∘ p1) =>
           rewriteI o-assoc $ rewrite (beta1 _ _) o-assoc
    \in
      inv right *> pmap (proj1 ∘ __) c *> left

  \private \use \func left-square {B X : Ob} {b : Hom X B} : Pullback (prodMap b (id B)) (diagonal B) X (pair (id X) b) b \cowith
    | pbCoh => pair-unique
        (run {
          rewriteI o-assoc,
          rewrite (beta1 _ _, o-assoc, beta1 _ _, id-right),
          rewriteI o-assoc,
          rewrite (beta1 _ _, id-left),
          idp
        })
        (run {
          rewriteI o-assoc,
          rewrite (beta2 _ _),
          rewriteI o-assoc, rewrite (beta2 _ _, o-assoc, beta2 _ _) equation
        })
    | pbMap p1 _ _ => proj1 ∘ p1
    | pbBeta1 {w} {p1} {p2} {c} =>
      \let
        left : proj2 ∘ (diagonal B ∘ p2) = p2 => rewriteI o-assoc $ rewrite (beta2 _ _) equation
        | right : proj2 ∘ (prodMap b (id B) ∘ p1) = proj2 ∘ p1 => rewriteI o-assoc $ rewrite (beta2 _ _) equation \in
        pair-unique
            (run {
              rewriteI o-assoc,
              rewrite (beta1 _ _ ),
              equation
            })
            (run {rewriteI o-assoc,
                  rewrite (beta2 _ _),
                  pbBeta2' w p1 p2 c *> inv left *> pmap (proj2 ∘ __) (inv c) *> right
            })
    | pbBeta2 {w} {p1} {p2} {c} => pbBeta2' w p1 p2 c
    | pbEta {_} {h1} {h2} c _ =>
      \let p2 : h1 = proj1 ∘ (pair (id X) b ∘ h1) => rewriteI o-assoc $ rewrite (beta1 _ _) equation
           | p1 : proj1 ∘ (pair (id X) b ∘ h2) = h2  => rewriteI o-assoc $ rewrite (beta1 _ _) equation
      \in p2 *> pmap (proj1 ∘ __) c *> p1

  \private \use \func right-square {B : Ob} : Pullback {\this} {Bprod B B} {terminal} {omega} (eq B) true-map B (diagonal B) terminalMap
    => char-pullback (diagonal.isSplitMono B)

  \private \use \func full-square {B X : Ob} (b : Hom X B) : Pullback {\this} (char-rel b) true-map X (pair (id X) b)
    => pullback-lemma right-square left-square

  \use \lemma singleton-mono (B : Ob) : Mono (singleton B) \cowith
    | isMono {X} {b} {b'} sb=sb' =>
      \let
        | c : char-rel b = char-rel b' => transpose-inj ((inv $ eqq-p-transpose-s b) *> sb=sb' *> eqq-p-transpose-s b')
        | b-square => full-square b
        | b'-square : Pullback {\this} (char-rel b) true-map X (pair (id X) b') =>
          transport (Pullback {\this} __ true-map X (pair (id X) b')) (inv c) (full-square b')
        | h-iso : Iso {\this} {X} {X} => Pullback.unique (char-rel b) true-map b-square b'-square
        | pb~pb*h : pair (id X) b = pair (id X) b' ∘ h-iso => inv (Pullback.unique.p-beta1 b'-square b-square)
        | c' : proj1 ∘ (pair (id X) b' ∘ h-iso.f) = h-iso.f => rewriteI o-assoc $ rewrite (beta1 _ _) id-left
        | h~1 : id X = h-iso.f => inv (beta1 _ _) *> pmap (proj1 ∘ __) pb~pb*h *> c'
        | b~b'h : b = b' ∘ h-iso.f => inv (beta2 _ _) *> pmap (proj2 ∘ __) pb~pb*h *> (rewriteI o-assoc $ rewrite (beta2 _ _) idp)
      \in b~b'h *> rewriteI h~1 id-right

  \use \func is-singleton {B : Ob} : Hom (Power B) omega => char-map (singleton-mono B)

  \use \func true-over-obj {B : Ob} : Hom B omega => true-map ∘ terminalMap

  \use \lemma monic-is-regular  {X Y : Ob} (m : Mono {\this} {X} {Y}) : Equalizer true-over-obj (char-map m) X m \cowith
    | equal =>
      rewrite (pbCoh {char-pullback m}, o-assoc) $
      rewrite terminal-unique idp
    | isEqualizer _ => \new QEquiv {
      | ret (h, com) => pbMap {char-pullback m} h terminalMap
          (rewriteI com $ rewrite o-assoc $ rewrite terminal-unique idp)
      | ret_f _ => pbEta {char-pullback m} (rewrite (pbBeta1 {char-pullback m}) $ idp)
          (rewrite (pbBeta2 {char-pullback m}) terminal-unique)
      | f_sec (h, com) => exts $ rewrite (pbBeta1 {char-pullback m}) idp
    }

  \use \lemma monic+epi=iso {X Y : Ob} (m : Mono {\this} {X} {Y}) (m-is-epi : isEpi {\this} {X} {Y} m)
    : Iso {\this} {X} {Y} m =>
    \let equalizer => monic-is-regular m
         | true=char-m : true-over-obj = char-map m => m-is-epi (Equalizer.equal {equalizer} : true-over-obj ∘ m.f = char-map m ∘ m)
         | equalizer-f : Equalizer (char-map m) (char-map m) => transport (Equalizer __ (char-map m) X m) true=char-m equalizer
    \in
      Equalizer.equalizer-iso equalizer-f

  \use \func global (X : Ob) => Hom terminal X

  \use \func namePower {A : Ob} (phi : Hom A omega) : global (Power A) => p-transpose (phi ∘ terminal-prod-left.hinv)

  -- Topos is cartesian closed

  {-
  Consider Power (B x C) as the type of binary relations between elements of B and C.
  Then, 'image' takes a relation S and an element b of B and returns the subset of C that corresponds to b.
  -}

  \use \func image {B C : Ob} : Hom (Bprod (Power $ Bprod B C) B) (Power C) =>
    p-transpose $ belongs {_} {Bprod B C} ∘ associator-iso.f

  -- 'single-image-test' takes a relation S and element b of B and tests if the image of relation is a singleton subset.

  \use \func is-image-single {B C : Ob} : Hom (Bprod (Power $ Bprod B C) B) omega => is-singleton ∘ image

  {-
  The idea: a relation S between B and C is functional iff all elements of B have a single image under S.
  'all-with-single-img' returns the subset consising of elements of B with singleton images.
  -}

  \use \func all-with-single-img {B C : Ob} : Hom (Power $ Bprod B C) (Power B) => p-transpose is-image-single

  -- Finally, the apex of the pullback gives the type of functional relations between B and C.

  \use \func graphs {B C : Ob} : Pullback (namePower (true-over-obj {\this} {B})) (all-with-single-img {\this} {B} {C})
    => pullback (namePower (true-over-obj {\this} {B})) (all-with-single-img {\this} {B} {C})
    \where {
      \use \func apex (B C : Ob) : Ob => Pullback.apex {graphs {_} {B} {C} }

      \use \func map {B C : Ob} : Hom (graphs.apex B C) (Power $ Bprod B C) => Pullback.pbProj2 {graphs {_} {B} {C}}
    }

  \use \lemma terminate {B C : Ob} {f : Hom B C} : terminalMap ∘ f = terminalMap => terminal-unique

  \private \use \lemma eval_comm {B C : Ob} : char-map (singleton-mono C) ∘ (image ∘ prodMap graphs.map (id B)) = true-map ∘ terminalMap =>
    run {
      rewriteI o-assoc ,
      rewrite (antitranspose-eq _ : char-map (singleton-mono C) ∘ image = belongs ∘ prodMap all-with-single-img (id B)),
      rewrite o-assoc,
      rewriteI (prod-id-right, pbCoh {graphs}),
      rewrite prod-id-right,
      rewriteI (o-assoc, antitranspose-eq _),
      rewrite (o-assoc, o-assoc, terminate) idp
    }

  \use \func eval {B C : Ob} : Hom (Bprod (graphs.apex B C) B) C
    => pbMap {char-pullback $ singleton-mono C} (image ∘ prodMap graphs.map (id B)) terminalMap eval_comm

  \private \use \func h {A B C : Ob} (f : Hom (Bprod A B) C) : Hom A (Power $ Bprod B C)
    => p-transpose (char-rel f ∘ associator-iso.hinv)

  \use \lemma ptranspose-eqq-eq {A B C : Ob} (f : Hom (Bprod A B) C) : p-transpose (char-rel f) = image ∘ prodMap (h f) (id B)
    => run {
      inv,
      p-transpose-unique {\this} {_} {_} {char-rel f} {_},
      rewrite prod-id-right,
      rewriteI (o-assoc, antitranspose-eq {\this} _),
      rewrite o-assoc,
      rewrite (inv $ associtor-prod _ _ _,  inv o-assoc, prod-id, inv $ antitranspose-eq _),
      rewrite (o-assoc, Iso.hinv_f {associator-iso}, id-right) idp
    }

  \use \lemma singleton-is-single {C : Ob} : is-singleton ∘ singleton C = true-over-obj
    => pbCoh {char-pullback (singleton-mono C)}

  \private \use \func transpose' {A B C : Ob} (f : Hom (Bprod A B) C) : Hom A (graphs.apex B C)
    => \have | step1 => pmap (`∘ f) (inv singleton-is-single) *> o-assoc
             | step2 : is-image-single ∘ prodMap (h f) (id B) = is-singleton ∘ (image ∘ prodMap (h f) (id B)) => o-assoc
             | step3 : all-with-single-img ∘ (h f) = p-transpose (is-image-single ∘ prodMap (h f) (id B))
                     => p-transpose-unique $ unfold $ rewrite prod-id-right $ rewriteI (o-assoc, antitranspose-eq _) idp
             | step4 : true-over-obj {_} {B} ∘ proj2 {_} {A} {B} = true-over-obj ∘ f
                     => unfold true-over-obj $ rewrite (o-assoc, terminate, o-assoc, terminate) idp
             | step5 => run {
                          p-transpose-unique {\this} {_} {_} {true-over-obj {_} {B} ∘ proj2 {_} {A} {B}} {namePower (true-over-obj {_} {B}) ∘ terminalMap},
                          rewrite (prod-id-right, inv o-assoc, inv $ antitranspose-eq _),
                          rewrite (o-assoc, terminate, o-assoc, o-assoc, terminate),
                          idp
                        }
       \in pbMap terminalMap (h f) $ unfold (Pullback.f, Pullback.g) $ rewrite (step5, step4, step3, step2, step1, eqq-p-transpose-s _, ptranspose-eqq-eq f) idp

  \private \use \lemma transpose-univ' {A B C : Ob} (f : Hom (Bprod A B) C) : f = eval ∘ prodMap (transpose' f) (id B) =>
    \let lem  : singleton C ∘ f = image ∘ prodMap (graphs.map ∘ transpose' f) (id B) =>
      rewrite (pbBeta2 {graphs}, eqq-p-transpose-s _) (ptranspose-eqq-eq _)
    \in
      pbEta {char-pullback (singleton-mono C)}
          (rewrite (inv o-assoc, pbBeta1 {char-pullback (singleton-mono C)}) $ rewrite (o-assoc, inv $ prod-id-right _ _) lem)
          terminal-unique

  \private \use \lemma transpose-unique' {A B C : Ob} {f : Hom (Bprod A B) C} {g : Hom A (graphs.apex B C)} (s : f = eval ∘ prodMap g (id B)) : transpose' f = g
    => graphs.pbEta terminal-unique $ run {
      unfold,
      rewrite (pbBeta2 {graphs}),
      unfold h, inv,
      p-transpose-unique {\this} {_} {_} {eq C ∘ prodMap f (id C) ∘ hinv {associator-iso}} {pbProj2 ∘ g},
      \have | step1 : singleton C ∘ f = image ∘ (prodMap (graphs.map {_} {B} {C} ∘ g) (id B))
                    => rewrite (s, inv o-assoc, pbBeta1 {char-pullback (singleton-mono C)}, o-assoc, inv $ prod-id-right _ _) idp
            | step2 : char-rel f = belongs {_} {Bprod B C} ∘ prodMap (graphs.map ∘ g) (id (Bprod B C)) ∘ associator
                    => run {
                      transpose-inj,
                      rewrite (inv $ eqq-p-transpose-s _, step1),
                      p-transpose-unique {\this} {_} {_} {belongs ∘ prodMap (graphs.map ∘ g) (id (Bprod B C)) ∘ associator} {image ∘ prodMap (graphs.map ∘ g) (id B)},
                      rewrite {} (prod-id-right _ _),
                      rewriteI o-assoc,
                      rewrite (inv $ antitranspose-eq _ : belongs ∘ prodMap image (id C) = belongs ∘ associator-iso.f),
                      rewrite {} o-assoc ,
                      rewrite (inv $ associtor-prod _ _ _, prod-id),
                      o-assoc
                    },
      rewrite step2,
      rewrite (o-assoc, associator-iso.f_hinv, id-right),
      idp
    }

  \use \func exp-adjoint (B : Ob) : RightAdjointCoreflection \this \this (bprodFunctorRight B) \cowith
    | coreflection C => \new Coreflection (bprodFunctorRight B) C {
      | Coreflected => graphs.apex B C
      | corefl-map => eval
      | isCoreflection => \new QEquiv {
        | ret => transpose'
        | ret_f _ => transpose-unique' idp
        | f_sec g => inv $ transpose-univ' g
      }
    }

  \default exp (B : Ob) : isExponential {\this} B => RightAdjointCoreflection.toAdjoint (exp-adjoint B)
}

\lemma sigma-prop-ext {A : \Prop} (a : A) : A = (\Sigma) => exts (\lam _ => (), \lam _ => a)

\lemma sigma-prop-ext-inv {A : \Prop} (eq : A = (\Sigma)) : A => propExt.conv eq ()

\open PrecatWithTerminal
\open SetCartesianClosed

\instance SetTopos : ToposPrecat \Set
  | FinCompletePrecat => SetBicat
  | CartesianClosedPrecat => SetCartesianClosed
  | subobj-classifier => \Prop
  | true-map => \lam _ => \Sigma
  | char-map => IsElement
  | char-pullback m => \new Pullback {
    | pbCoh => exts (\lam _ => sigma-prop-ext (SetTopos.isContained _ idp))
    | pbMap {_} p1 _ eq =>
      \lam w1 => cases (isElement-char {_} {_} {_} {_} {p1} {eq} w1) \with {
        | SetTopos.isContained a p => a
      }
    | pbBeta1 {_} {p1} {_} {eq} => ext (\lam w1 => cases (isElement-char {_} {_} {_} {_} {p1} {eq} w1) \with {
      | SetTopos.isContained a p => p
    })
    | pbBeta2 => terminal-unique {SetBicat}
    | pbEta {_} {h1} {h2} eq _ => ext (\lam x => \let s : Mono.f {m} (h1 x) = Mono.f {m} (h2 x) => path (\lam i => (eq @ i) x) \in mono-is-inj m s)
  }
  | char-unique {S} {_} {m} {phi} pullback =>
    ext (\lam b =>
        ext (\lam p =>
                 \let preimage : terminal.apex -> S => pbMap {pullback} (name' b) (terminalMap {SetBicat}) (unfold (unfold name' $ exts (\lam _ => sigma-prop-ext p))) \in
                   SetTopos.isContained (unname' preimage)
                       (\let b-image : Mono.f {m} ∘ {SetBicat} preimage = name' b => pbBeta1 {pullback} \in name-inj
                           (rewriteI (name-f (Mono.f {m})) $ rewrite (global-elements-iso.f_ret preimage) b-image)),
             \let ss : phi ∘ {SetBicat} (Mono.f {m}) = terminalMap ∘ {SetBicat} true-map => pbCoh {pullback}
                  | ss-impl (x : S) : phi (Mono.f {m} x) = (\Sigma) => path (\lam i => (ss @ i) x) \in
               \lam c => cases c \with {
                 | SetTopos.isContained a p => rewriteI p $ sigma-prop-ext-inv (ss-impl a)
               }
        ))
  \where {
    \func mono-is-inj {A B : SetBicat} (m : Mono {SetBicat} {A} {B}) : IsInj m.f => \lam {a} {b} p =>
        run {
          name-inj,
          m.isMono,
          rewrite (name-f m.f a, name-f m.f b),
          pmap name' p
        }

    \data IsElement {A B : SetBicat} (m : Mono {SetBicat} {A} {B}) (b : B)
      | isContained (a : A) (m.f a = b)
      \where {
        \use \level isProp {A B : SetBicat} (m : Mono {SetBicat} {A} {B}) (b : B) (x y : IsElement m b) : x = y
        \elim x, y
          | isContained a p, isContained c p1 =>
            \let a=c : a = c => mono-is-inj m (p *> inv p1)
                 | p=p1 : transport {A} (\lam (x : A) => m.f x = b) a=c p = p1 => prop-isProp _ _
            \in \case\elim a, \elim c, \elim p, \elim p1, \elim a=c, \elim p=p1 \with {
              | a, c, _, _, idp, idp => idp
            }
      }

    \func isElement-char {S B : SetBicat} {m : Mono {SetBicat} {S} {B}} {w : SetBicat} {p1 : w -> B}
                         {eq : (\lam x => IsElement m (p1 x)) = (\lam _ => \Sigma)} (x : w) : IsElement m (p1 x) =>
      \let s : IsElement m (p1 x) = (\Sigma) => path (\lam i => (eq @ i) x) \in
        sigma-prop-ext-inv s
  }