\import Algebra.Meta
\import Category
\import Category.CartesianClosed
\import Category.Coreflection
\import Category.Limit
\import Equiv
\import Function (isInj)
\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Set.Category
\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

  \func power \alias P (B : Ob) : Ob => p-exponential B

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

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

  \func 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

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

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

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

  \func 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 internal-equality \alias eq (B : Ob) : Hom (Bprod B B) omega =>
    char-map (diagonal.isSplitMono B)

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

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

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

  \func 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} {singleton B ∘ b} $
    rewrite (prod-id-right _ _, inv o-assoc, inv $ p-transpose-univ _) idp

  \func 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
    \where {
      \func full-square {X : Ob} (b : Hom X B)
        : Pullback {\this} (char-rel b) true-map X (pair (id X) b) => pullback-lemma right-square left-square

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

      \func left-square{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

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

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

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

  \func 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

  \func monic-is-regular  {X Y : Ob} (m : Mono {\this} {X} {Y}) : Equalizer true-over-obj (char-map m) X m =>
    \new Equalizer {
      | 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
      }
    }

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

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

  -- Topos is cartesian closed

  {-
  Consider P (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.
  -}

  \func image {B C : Ob} : Hom (Bprod (P $ Bprod B C) B) (P 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.

  \func is-image-single {B C : Ob} : Hom (Bprod (P $ 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 consisinf of elements of B with singleton images.
  -}

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

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

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

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

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

  \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 comm
    \where {
      \func comm  : 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
        }
    }

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

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

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

  \func exp-adjoint (B : Ob) : RightAdjointCoreflection \this \this (bprodFunctorRight B)
  \cowith
    | coreflection => exp B
    \where {
      \func exp (B : Ob) (C : Ob) : Coreflection (bprodFunctorRight B) C \cowith
        | 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
        }

      \func transpose' {A B C : Ob} (f : Hom (Bprod A B) C) : Hom A (graphs.apex B C) =>
        pbMap terminalMap (h f) (unfold (Pullback.f, Pullback.g) $
        rewrite (step5, step4, step3, step2, step1, eqq-p-transpose-s _, ptranspose-eqq-eq f) idp)
        \where {
          \func step1 : true-over-obj ∘ f = is-singleton ∘ (singleton C ∘ f) =>
            rewriteI o-assoc $ rewrite singleton-is-single idp

          \func step2 : is-image-single ∘ prodMap (h f) (id B) = is-singleton ∘ (image ∘ prodMap (h f) (id B) ) =>
            rewriteI o-assoc $ idp

          \func 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

          \func step4 : true-over-obj {_} {B} ∘ proj2 {_} {A} {B} = true-over-obj ∘ f =>
            unfold true-over-obj $ rewrite (o-assoc, terminate, o-assoc, terminate) idp

          \func step5
            : name (true-over-obj {_} {B}) ∘ terminalMap = p-transpose (true-over-obj {_} {B} ∘ proj2 {_} {A} {B}) =>
            run {
              p-transpose-unique {\this} {_} {_} {true-over-obj {_} {B} ∘ proj2 {_} {A} {B}} {name (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
            }
        }

      \func 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

      \func 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 =>
        pbEta {graphs} 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},
          rewrite step2, rewrite (o-assoc, associator-iso.f_hinv, id-right),
          idp
        })
        \where {
          \func 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

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

  \default exp (B : Ob) : isExponential {\this} B => RightAdjointCoreflection.toAdjointCounit (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
  }