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

\record SetHom (Dom Cod : BaseSet)
  | \coerce func : Dom -> Cod

\instance SetCat : Cat \Set
  | 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))

\sfunc SIP_Set (Str : \Set -> \hType (\suc \lp)) (isHom : \Pi {x y : \Set} -> Str x -> Str y -> (x -> y) -> \hType (\suc \lp))
               (st : \Pi {X : \Set} {S1 S2 : Str X} -> isHom S1 S2 (\lam x => x) -> isHom S2 S1 (\lam x => x) -> S1 = S2)
               {X Y : \Set} (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 {J : \Type} (F : J -> \Set) : 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 {X Y : \Set} (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 => \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 : BicompleteCat
  | Cat => SetCat
  | limit F => \new Limit {
    | apex => Cone F (\Sigma)
    | coneMap j x => coneMap {x} j ()
    | coneCoh h => ext (\lam s => pmap (__ ()) (coneCoh {s}  h))
    | isLimit Z => \new QEquiv {
      | ret c z => \new Cone {
        | coneMap j _ => coneMap {c} j z
        | coneCoh h => ext (\lam _ => pmap (__ z) (coneCoh {c} h ))
      }
      | ret_f => idpe
      | f_sec => idpe
    }
  }
  | colimit {J : Precat} G => limits<=pr+eq {SetCat.op} (\lam J G => SetCoproduct G) (\lam {X} {Y} f g => SetCoequalizer f g) {J.op} (Functor.op {G})
  \where {
    \lemma cone-isLim (c : Cone { | D => SetCat }) (e : Equiv (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 \new QEquiv {
            | ret (c' : Cone) z => e.ret (coneMap z c') ()
            | ret_f h => ext \lam z =>
                \have t => e.ret_f (\lam _ => h z)
                \in path (\lam i => t i ())
            | f_sec (c' : Cone) => exts \lam j => ext \lam z =>
                \have t => e.f_ret (coneMap z c')
                \in path (\lam i => Cone.coneMap {t i} j ())
          }
  }

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

    \lemma ~-cequiv {J : SmallPrecat} {F : Functor J SetCat} {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 {J : JoinSemilattice} {F : Functor J SetCat} {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 {J : SmallPrecat} (F : Functor J SetCat) {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 {J : Poset} {F : Functor J SetCat} {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 {J : Poset} {F : Functor J SetCat} {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 (F n)
      | , (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
  }