\import Algebra.Ordered
\import Arith.Nat
\import Category
\import Category.Functor
\import Category.Limit
\import Equiv \hiding (Map)
\import Function.Meta ($)
\import Meta
\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.inv (\lam x => path ((e.inv_f @ __) x)) (\lam y => path ((e.f_inv @ __) 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.inv)
  : \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 DirectLimit {A : Nat -> BaseSet} (f : \Pi {n : Nat} -> SetHom (A n) (A (suc n)))
  => Quotient {\Sigma (n : Nat) (A n)} \lam s s' => s' = (suc s., f s.)
  \where {
    \func inDL {f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))} (s : \Sigma (n : Nat) (A n)) : DirectLimit f
      => in~ s

    \func include_+-left (f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))) {n m : Nat} (a : A n) : A (n Nat.+ m) \elim m
      |  => a
      | suc m => f (include_+-left f a)

    \func include_+-right (f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))) {n m : Nat} (a : A m) : A (n Nat.+ m) \elim n
      |  => a
      | suc n => f (include_+-right f a)

    \lemma include_+-left-comm {f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))} {n m : Nat} {a : A n} : include_+-left f (f a) = f (include_+-left f {n} {m} a) \elim m
      |  => idp
      | suc m => pmap f include_+-left-comm

    \lemma include_+-right-comm {f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))} {n m : Nat} {a : A m} : include_+-right f {n} (f a) = f (include_+-right f a) \elim n
      |  => idp
      | suc n => pmap f include_+-right-comm

    \func include (f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))) {n m : Nat} (p : n <= m) (a : A n) : A m
      => rewriteI (<=_exists p) (include_+-left f a)

    \lemma include_refl {f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))} {n : Nat} {p : n <= n} {a : A n} : include f p a = a
      => unfold include {?}

    \lemma dequiv {f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))} {s : \Sigma (n : Nat) (A n)} {a' : A (suc s.)} (p : a' = f s.) : in~ s = {DirectLimit f} in~ (suc s., a')
      => path (\lam i => ~-equiv _ _ (ext (idp,p)) i)

    \lemma dequiv2 {f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))} {s s' : \Sigma (n : Nat) (A n)} (p : s. = s'.) (q : include f (Preorder.=_<= p) s. = s'.) : in~ s = {DirectLimit f} in~ s'
      => Jl (\lam x p' => \Pi {y : A x} -> include f (Preorder.=_<= p') s. = y -> inDL s = inDL (x,y)) (\lam q' => pmap (\lam x => inDL (s.,x)) ({?} *> q')) p q

    \lemma dequiv3 {f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))} {s s' : \Sigma (n : Nat) (A n)} (p : s. <= s'.) (q : include f p s. = s'.) : in~ s = {DirectLimit f} in~ s'
      => {?}
      \where
        \lemma aux {f : \Pi {n : Nat} -> SetHom (A n) (A (suc n))} {s s' : \Sigma (n : Nat) (A n)} (k : Nat) (p : s. Nat.+ k = s'.) (q : include f (transport (s. <=) p (NatSemiring.<=_+ <=-refl zero<=_)) s. = s'.) : in~ s = {DirectLimit f} in~ s' \elim k
          |  => dequiv2 p q
          | suc k => aux k idp idp *> dequiv {_} {s. Nat.+ k, include f (NatSemiring.<=_+ <=-refl zero<=_) s.} idp *> dequiv2 p ({?} *> q)
  }