\import Algebra.Monoid
\import Arith.Nat
\import Category
\import Category.Functor
\import Category.Limit
\import Equiv
\import Function (IsInj)
\import Function.Meta
\import Logic.Unique
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set

\instance SetCat.{u} : Cat (\Set u)
  | Hom X Y => X -> Y
  | id => \lam x => x
  | o g f => \lam x => g (f x)
  | id-left => idp
  | id-right => idp
  | o-assoc => idp
  | univalence => Cat.makeUnivalence $ later \lam (e : Iso) =>
    \let p => path (iso e.f e.hinv (\lam x => path ((e.hinv_f @ __) x)) (\lam y => path ((e.f_hinv @ __) y)))
    \in (p, simp_coe (\lam d => idp))
  \where {
    \lemma mono-char.{u} {X Y : \Set u} {f : X -> Y} : Mono {SetCat.{u}} f <-> IsInj f
      => (\lam fm p => path \lam i => fm.isMono (ext \lam _ => p) i (), \lam fi => \new Mono {
        | isMono p => ext \lam x => fi $ path \lam i => p i x
      })
  }

\sfunc SIP_Set.{u} (Str : \Set u -> \Type) (isHom : \Pi {x y : \Set u} -> Str x -> Str y -> (x -> y) -> \Type)
                   (st : \Pi {X : \Set u} {S1 S2 : Str X} -> isHom S1 S2 (\lam x => x) -> isHom S2 S1 (\lam x => x) -> S1 = S2)
                   {X Y : \Set u} (e : Iso {SetCat} {X} {Y}) (S1 : Str X) (S2 : Str Y) (p : isHom S1 S2 e.f) (q : isHom S2 S1 e.hinv)
  : \Sigma (p : X = Y) (Path (\lam i => Str (p @ i)) S1 S2) (\Pi (x : X) -> transport (\lam Z => Z) p x = e.f x)
  => \have (p,q,s) => SIP SetCat Str isHom st e S1 S2 p q
     \in (p, q, \lam x => inv (transport_pi (\lam _ => X) (\lam Z => Z) p (\lam z => z) x) *> path (\lam i => (s @ i) x))

\instance SetCoproduct.{u} {J : \Type u} (F : J -> \Set u) : Product {J} {SetCat.op} F
  | apex => Trunc0 (\Sigma (j : J) (F j))
  | proj j x => in0 (j,x)
  | tupleMap f (in0 (j,x)) => f j x
  | tupleBeta => idp
  | tupleEq e => ext \case \elim __ \with {
    | in0 (j,x) => pmap (__ x) (e j)
  }

\instance SetCoequalizer.{u} {X Y : \Set u} (f g : X -> Y) : Equalizer {SetCat.op} f g
  | apex => Quotient (\lam y y' => \Sigma (x : X) (f x = y) (g x = y'))
  | eql => in~
  | equal => ext (\lam x => path (~-equiv _ _ (later (x,idp,idp))))
  | isEqualizer Z => inP \new QEquiv {
    | ret (h,p) => \case __ \with {
      | in~ y => h y
      | ~-equiv y y' (x,fx=y,gx=y') => inv (pmap h fx=y) *> pmap (__ x) p *> pmap h gx=y'
    }
    | ret_f h => ext \case \elim __ \with {
      | in~ y => idp
    }
    | f_sec (h,p) => ext idp
  }

\instance SetBicat.{u} : BicompleteCat.{u}
  | Cat => SetCat.{u}
  | limit F => \new Limit {
    | apex => LimitSet F
    | coneMap j l => l. j
    | coneCoh h => ext \lam l => l. h
    | limMap c x => (\lam j => c.coneMap j x, \lam h => path \lam i => c.coneCoh h i x)
    | limBeta c j => idp
    | limUnique r => ext \lam x => exts \lam j => path \lam i => r j i x
  }
  | Bprod X Y => \new Product {
    | apex => \Sigma X Y
    | proj => \case \elim __ \with {
      |  => __.
      |  => __.
    }
    | tupleMap e z => (e  z, e  z)
    | tupleBeta => ext \lam z => mcases idp
    | tupleEq e => ext \lam z => path \lam i => (e  i z, e  i z)
  }
  | pullback {X} {Y} f g => \new Pullback {
    | apex => \Sigma (x : X) (y : Y) (f x = g y)
    | pbProj1 => __.
    | pbProj2 => __.
    | pbCoh => ext __.
    | pbMap p1 p2 c w => (p1 w, p2 w, path \lam i => c i w)
    | pbBeta1 => idp
    | pbBeta2 => idp
    | pbEta c1 c2 => ext \lam w => ext (path \lam i => c1 i w, path \lam i => c2 i w)
  }
  | colimit {J} G => limits<=pr+eq {SetCat.op} (\lam J G => SetCoproduct G) (\lam {X} {Y} f g => SetCoequalizer f g) {Precat.op {J}} (Functor.op {G})
  \where {
    \type LimitSet.{u} {J : Precat.{u,u}} (F : Functor J SetCat.{u}) : \Set u
      => Given (f : \Pi (j : J) -> F j) ∀ {j j' : J} (h : Hom j j') (F.Func h (f j) = f j')

    \lemma cone-isLim.{u} (c : Cone { | D => SetCat.{u} }) (e : IsEquiv (conePullback c (\Sigma))) : Limit { | Cone => c } \cowith
      | isLimit Z =>
        \have coneMap (z : Z) (c' : Cone c.G Z) : Cone c.G (\Sigma) => \new Cone {
          | coneMap j _ => c'.coneMap j z
          | coneCoh h => ext \lam _ => path (\lam i => c'.coneCoh h i z)
        } \in inP \new QEquiv {
          | ret c' z => IsEquiv.ret e (coneMap z c') ()
          | ret_f h => ext \lam z => path (\lam i => IsEquiv.ret_f e i ())
          | f_sec c' => exts \lam j => ext \lam z => path (\lam i => (IsEquiv.f_ret e i).coneMap j ())
        }

    \lemma limit-elem-equals.{u} {C : Cone { | D => SetCat.{u} }} (cl : IsLimitCone C) {x y : C.apex} (p : \Pi (j : C.J) -> C.coneMap j x = C.coneMap j y) : x = y
      => path \lam i => IsEquiv.isInj (cl (\Sigma)) {\lam _ => x} {\lam _ => y} (exts \lam j => ext \lam _ => p j) i ()
  }

\type SetColimit.{u} {J : Precat} (F : Functor J SetCat.{u})
  => Quotient {\Sigma (j : J) (F j)} \lam s s' => \Sigma (p : Hom s. s'.) (F.Func p s. = s'.)
  \where {
    \func inC.{u} {J : Precat} {F : Functor J SetCat.{u}} (s : \Sigma (j : J) (F j)) : SetColimit F => in~ s

    \lemma ~-cequiv {s s' : \Sigma (j : J) (F j)} (f : Hom s. s'.) (p : F.Func f s. = s'.)
      : in~ s = {SetColimit F} in~ s'
      => path (\lam i => ~-equiv s s' (f,p) i)

    \lemma unext-ub.{u} {J : JoinSemilattice} {F : Functor J SetCat.{u}} {s s' : \Sigma (j : J) (F j)} (p : inC s = inC s')
      : ∃ (j : J) (p : s. <= j) (q : s'. <= j) (F.Func p s. = F.Func q s'.)
      => Quotient.equalityClosure (\new Equivalence (\Sigma (j : J) (F j)) _ {
        | ~-transitive => later \lam (inP s) (inP t) => inP (s. ∨ t., s. <=∘ join-left, t. <=∘ join-right, Func-app F *> pmap (F.Func join-left) s. *> inv (Func-app F) *> poset-app *> Func-app F *> pmap (F.Func join-right) t. *> inv (Func-app F))
        | ~-reflexive {x} => later $ inP (x., <=-refl, <=-refl, idp)
        | ~-symmetric => later \lam (inP s) => inP (s., s., s., inv s.)
      }) (later \lam {x} {y} s => inP (x. ∨ y., join-left, join-right, Func-app F *> pmap (F.Func join-right) s.)) (path \lam i => p i)

    \lemma Func-app.{u} {J : Precat} (F : Functor J SetCat.{u}) {j1 j2 j3 : J} {f : Hom j1 j2} {g : Hom j2 j3} {a : F j1} : F.Func (g ∘ f) a = F.Func g (F.Func f a)
      => pmap (__ a) F.Func-o

    \lemma poset-app.{u} {J : Poset} {F : Functor J SetCat.{u}} {j j' : J} {f g : j <= j'} {a : F j} : F.Func f a = F.Func g a
      => pmap (F.Func __ a) prop-pi

    \lemma poset-id.{u} {J : Poset} {F : Functor J SetCat.{u}} {j : J} {p : j <= j} {a : F j} : F.Func p a = a
      => poset-app *> pmap (__ a) F.Func-id

    \func inMap (j : J) (a : F j) : SetColimit F
      => in~ (j,a)

    \lemma inMap-coh {j j' : J} (f : Hom j j') (a : F j) : inMap j a = inMap j' (F.Func f a)
      => ~-cequiv f idp
  }

\func NatFunctor {C : Precat} (F : Nat -> C) (f : \Pi {n : Nat} -> Hom (F n) (F (suc n))) : Functor NatSemiring C \cowith
  | F => F
  | Func p => natHom (_, <=_exists p)
  | Func-id => pmap natHom (sigma-isProp _ (,idp)) *> natHom_id
  | Func-o => pmap natHom (sigma-isProp _ _) *> natHom-comp
  \where {
    \lemma sigma-isProp {n m : Nat} : isProp (\Sigma (k : Nat) (n + k = m))
      => \lam s t => ext $ NatSemiring.cancel-left n $ s. *> inv t.

    \func natHom {n m : Nat} (s : \Sigma (k : Nat) (n + k = m)) : Hom (F n) (F m) \elim m, s
      | _, (, idp) => id
      | , (suc k, ())
      | suc m, (suc k, q) => f ∘ natHom (k, pmap pred q)

    \lemma natHom_id {n : Nat} : natHom (,idp) = id {_} {F n} \elim n
      |  => idp
      | suc n => idp

    \lemma natHom-comp {n m k : Nat} {s : \Sigma (l : Nat) (n + l = m)} {t : \Sigma (l : Nat) (m + l = k)}
      : natHom (s. + t., inv +-assoc *> pmap (+ _) s. *> t.) = natHom t ∘ natHom s \elim k, t
      | , (, idp) => pmap natHom (sigma-isProp _ _) *> inv id-left
      | suc k, (, idp) => pmap natHom (sigma-isProp _ _) *> inv id-left
      | , (suc m, ())
      | suc k, (suc m, q) => pmap (f ∘) (pmap natHom (sigma-isProp _ _) *> natHom-comp) *> inv o-assoc
  }