open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Everything
open import Cat.Functor.Everything
open import Cat.Instances.Discrete
open import Cat.Instances.Elements
open import Cat.Instances.Functor
open import Cat.Instances.Comma
open import Cat.Instances.Lift
open import Cat.Prelude

open import Data.Fin

open import Topoi.Base

import Cat.Functor.Reasoning as Functor-kit
import Cat.Reasoning

module wip.obj where

open Precategory
open Functor
open _=>_

FinSet : ∀ {ℓ} → Precategory ℓ ℓ
FinSet .Ob = Lift _ Nat
FinSet .Hom (lift n) (lift k) = Lift _ (Fin n → Fin k)
FinSet .Hom-set _ _ = hlevel 
FinSet .id = lift λ x → x
FinSet ._∘_ = λ (lift f) (lift g) → lift λ x → f (g x)
FinSet .idr = λ f → refl
FinSet .idl = λ f → refl
FinSet .assoc = λ f g h → refl

Fin→Sets : ∀ {ℓ κ} → Functor (FinSet {ℓ}) (Sets κ)
Fin→Sets .F₀ n = Lift _ (Fin (Lift.lower n)) , hlevel 
Fin→Sets .F₁ (lift f) (lift x) = lift (f x)
Fin→Sets .F-id = refl
Fin→Sets .F-∘ f g = refl

Obj : Topos lzero _
Obj = Presheaf (FinSet ^op)

-- module Sets-tensoring {o ℓ κ} {C : Precategory o ℓ} (colim : is-cocomplete κ κ C) where
--   private
--     module C = Cat.Reasoning C
--     open Initial
--     open Cocone
--     open Cocone-hom

--   Sets_⊗_ : Set κ → Ob C → Ob C
--   Sets n ⊗ T = colim (Const {C = Disc′ n} T) .bot .coapex

--   Copower-map : ∀ {A B : Set κ} {o}
--               → (∣ A ∣ → ∣ B ∣) → Hom C (Sets A ⊗ o) (Sets B ⊗ o)
--   Copower-map f = colim _ .has⊥ cocone′ .centre .hom
--     where
--       cocone′ : Cocone _
--       cocone′ .coapex = Sets _ ⊗ _
--       cocone′ .ψ x = colim _ .bot .ψ (f x)
--       cocone′ .commutes p =
--         idr C _ ∙ ap (colim (Const _) .bot .ψ ⊙ f) (sym p)

--   Copower-id : ∀ {A : Set κ} {o} → Copower-map {A = A} {o = o} (λ x → x) ≡ id C
--   Copower-id = ap hom $ colim _ .has⊥ _ .paths $
--     cocone-hom (id C) λ o → idl C _

--   Copower-∘ : ∀ {A B C : Set κ} {o} {f : ∣ B ∣ → ∣ C ∣} {g : ∣ A ∣ → ∣ B ∣}
--             → Copower-map {A} {C} {o = o} (λ x → f (g x))
--             ≡ Copower-map {B} f C.∘ Copower-map g
--   Copower-∘ = ap hom $ colim _ .has⊥ _ .paths $
--     cocone-hom _ λ o → C.pullr (colim _ .has⊥ _ .centre .commutes _)
--                      ∙ colim _ .has⊥ _ .centre .commutes _

--   Copower : Ob C → Functor (Sets κ) C
--   Copower x .F₀ = Sets_⊗ x
--   Copower x .F₁ = Copower-map
--   Copower x .F-id = Copower-id
--   Copower x .F-∘ _ _ = Copower-∘

{-
module Sets-powering {o ℓ κ} {C : Precategory o ℓ} (lim : is-complete κ κ C) where
  private
    module C = Cat.Reasoning C
    open Terminal
    open Cone
    open Cone-hom

  Sets_⋔_ : Set κ → Ob C → Ob C
  Sets n ⋔ T = lim (Const {C = Disc′ n} T) .top .apex

  Power-map : ∀ {A B : Set κ} {o}
              → (∣ A ∣ → ∣ B ∣) → Hom C (Sets B ⋔ o) (Sets A ⋔ o)
  Power-map f = lim _ .has⊤ cone′ .centre .hom
    where
      cone′ : Cone _
      cone′ .apex = Sets _ ⋔ _
      cone′ .ψ x = lim _ .top .ψ (f x)
      cone′ .commutes p =
        idl C _ ∙ ap (lim (Const _) .top .ψ ⊙ f) p

  abstract
    Power-id : ∀ {A : Set κ} {o} → Power-map {A = A} {o = o} (λ x → x) ≡ id C
    Power-id = ap hom $ lim _ .has⊤ _ .paths $
      record { hom = _ ; commutes = λ o → C.idr _ }

    Power-∘ : ∀ {A B C : Set κ} {o} {f : ∣ B ∣ → ∣ C ∣} {g : ∣ A ∣ → ∣ B ∣}
              → Power-map {A} {C} {o = o} (λ x → f (g x))
              ≡ Power-map {A} g C.∘ Power-map {B} f
    Power-∘ = ap hom $ lim _ .has⊤ _ .paths $
      record { hom = _ ; commutes = λ o → C.pulll (lim _ .has⊤ _ .centre .commutes _)
                                        ∙ lim _ .has⊤ _ .centre .commutes _
            }

  Power : Ob C → Functor (Sets κ ^op) C
  Power x .F₀ = Sets_⋔ x
  Power x .F₁ = Power-map
  Power x .F-id = Power-id
  Power x .F-∘ _ _ = Power-∘
  -}

  -- Power-continuous : ∀ o → is-continuous {oshape = κ} {κ} (Power o)
  -- Power-continuous o K x y = {!   !}


--   const : ∀ {ℓ} (c : C.Ob) → Functor (Sets ℓ) (PSh (h ⊔ ℓ) C)
--   const c .F₀ A .F₀ d = (∣ A ∣ × C.Hom d c) , ×-is-hlevel 2 (A .is-tr) (hlevel 2)
--   const c .F₀ A .F₁ f (fst , snd) = fst , snd C.∘ f
--   const c .F₀ A .F-id = funext λ _ → Σ-pathp refl (C.idr _)
--   const c .F₀ A .F-∘ f g = funext λ _ → Σ-pathp refl (C.assoc _ _ _)
--   const c .F₁ f = NT (λ { _ (a , b) → (f a , b) }) λ x y f₁ → refl
--   const c .F-id = Nat-path λ _ → refl
--   const c .F-∘ f g = Nat-path λ _ → refl

--   const⊣ev : ∀ {ℓ} (c : C.Ob) → const c ⊣ ev {h ⊔ ℓ} c
--   const⊣ev c = adj where
--     open _⊣_
--     adj : _ ⊣ _
--     adj .unit .η _ s = s , C.id
--     adj .unit .is-natural x y f = refl
--     adj .counit .η x = NT (λ i (f , a) → x .F₁ a f) λ _ _ _ →
--       funext λ _ → happly (x .F-∘ _ _) _
--     adj .counit .is-natural x y f = Nat-path λ _ → funext λ _ →
--       happly (sym (f .is-natural _ _ _)) _
--     adj .zig = Nat-path (λ _ → funext λ _ → Σ-pathp refl (C.idl _))
--     adj .zag {B} = B .F-id

{-
  module _ {D : Precategory κ κ} (F : Functor D C) (flat : Flat cocompl F) where
    private
      module DC = Cat.Reasoning Cat[ D , C ]
      module D = Cat.Reasoning D
      module F = Functor F

    diinv : Diaconescu⁻¹ (Diaconescu F flat) DC.≅ F
    diinv = DC.invertible→iso to (componentwise-invertible→invertible to inv)
      where
        cocone′ : ∀ x → Cocone _
        cocone′ x = cocone (F.₀ x) (λ x → F.₁ (x .section))
          λ f → sym (F.F-∘ _ _) ∙ ap F.₁ (f .commute)

        to : Diaconescu⁻¹ (Diaconescu F flat) => F
        to .η x = cocompl _ .has⊥ (cocone′ x) .centre .hom
        to .is-natural x y f = ap hom $
          is-contr→is-prop
            (cocompl (F F∘ πₚ _ _) .has⊥ (cocone (F.F₀ y) (λ x → F.₁ (f D.∘ x .section)) λ p → sym (F.F-∘ _ _) ∙ ap F.₁ (D.pullr (p .commute))))
            (cocone-hom _ (λ _ → C.pullr (cocompl _ .has⊥ _ .centre .commutes _) ∙ cocompl _ .has⊥ _ .centre .commutes _))
            (cocone-hom _ λ _ → C.pullr (cocompl _ .has⊥ _ .centre .commutes _) ∙ sym (F.F-∘ _ _))

        inv : ∀ x → C.is-invertible (to .η x)
        inv ob = C.make-invertible (cocompl _ .bot .ψ (elem ob D.id))
          (cocompl _ .has⊥ _ .centre .commutes _ ∙ F.F-id)
          (ap hom $ is-contr→is-prop (cocompl _ .has⊥ (cocompl _ .bot))
            (cocone-hom _ (λ o → C.pullr (cocompl _ .has⊥ _ .centre .commutes _) ∙ cocompl _ .bot .commutes (elem-hom (o .section) (D.idl _))))
            (cocone-hom _ (λ _ → C.idl _)))

  -- open Finitely-complete
  -- test : {D : Precategory κ κ} → Finitely-complete D → (F : Functor D C) → is-lex F → Flat cocompl F
  -- test f-c F F-lex .is-lex.pres-⊤ {T} x ob = contr map unique
  --   where
  --     map : C.Hom ob (₀ (Realisation cocompl F) T)
  --     map = cocompl _ .bot .ψ (elem (f-c .terminal .top)
  --           (x (Const (Lift _ ⊤ , λ _ _ _ _ _ _ → lift tt)) .centre .η (f-c .terminal .top) (lift tt)))
  --       C.∘ F-lex .is-lex.pres-⊤ (f-c .terminal .has⊤) ob .centre

  --     unique : ∀ h → map ≡ h
  --     unique h = {! ap (_ C.∘_) ? ∙ cocompl _ .bot .commutes _ ∙ ?!}
  -- test f-c F F-lex .is-lex.pres-pullback = {!   !}

  -- test : C.Ob → Functor (FinSet {κ} ^op) C
  -- test o = Power o F∘ Functor.op Fin→Sets

  -- test′ : C.Ob → Functor (PSh κ (FinSet ^op)) C
  -- test′ ob = Realisation {κ = κ} cocompl (test ob)

  -- object→map : C.Ob → Geom[ C , PSh κ (FinSet {κ} ^op) ]
  -- object→map ob = g where
  --   g : Geom[ _ , _ ]
  --   Inv[ g ] = test′ ob
  --   Dir[ g ] = RHom cocompl (test ob)
  --   g .Inv-lex = {!   !}
  --   g .Inv⊣Dir = よext⊣RH cocompl (test ob)


--   {-
--   Global-sections : Geom[ C , Sets κ ]
--   Inv[ Global-sections ] = Copower (fc.terminal .top)
--   Dir[ Global-sections ] = hom' where
--     hom' : Functor C (Sets κ)
--     hom' .F₀ ob′ = C.Hom (fc.terminal .top) ob′ , C.Hom-set _ _
--     hom' .F₁ f = f C.∘_
--     hom' .F-id = funext C.idl
--     hom' .F-∘ f g = funext λ _ → sym (C.assoc _ _ _)
--   Global-sections .Inv-lex .is-lex.pres-⊤ term obj =
--     is-terminal-iso C isom (fc.terminal .has⊤) obj
--     where
--       isom : _ C.≅ _
--       isom = C.make-iso
--         (cocompl _ .bot .ψ (term (Lift κ ⊤ , λ _ _ _ _ _ _ → lift tt) .centre _))
--         (cocompl _ .has⊥ (cocone (fc.terminal .top) (λ _ → C.id) λ _ → C.idl _) .centre .hom)
--         (ap hom (is-contr→is-prop (cocompl _ .has⊥ (cocone _ (λ _ → cocompl _ .bot .ψ _) λ _ → C.idr _))
--           (cocone-hom _ λ o → C.pullr (cocompl _ .has⊥ _ .centre .commutes _) ∙ C.idr _)
--           (cocone-hom _ λ o → C.idl _ ∙ ap (cocompl _ .bot .ψ) (sym (happly (term _ .paths _) _)))))
--         (!-unique₂ fc.terminal _ _)

--   Global-sections .Inv-lex .is-lex.pres-pullback {P = P} {X} {p1 = p1} {p2} {f} {g} x = {!   !}
--     -- open is-pullback
--     -- pb′ : is-pullback C _ _ _ _
--     -- pb′ .square = sym Copower-∘ ∙ ap Copower-map (x .square) ∙ Copower-∘
--     -- pb′ .limiting {P'} {p1'} {p2'} p = Copower-map {!   !} C.∘ {!   !}
--     -- pb′ .p₁∘limiting = C.pulll (sym Copower-∘ ∙ ap Copower-map (x .p₁∘limiting))
--     --                  ∙ {! !}
--     -- pb′ .p₂∘limiting = {!   !}
--     -- pb′ .unique = {!   !}
--   Global-sections .Inv⊣Dir = adj₂
--     where
--       open _⊣_

--       adj₂ : Copower (fc.terminal .top) ⊣ _
--       adj₂ .unit .η x i = cocompl _ .bot .ψ i
--       adj₂ .unit .is-natural x y f = funext λ _ → sym (cocompl _ .has⊥ _ .centre .commutes _)
--       adj₂ .counit .η x = cocompl _ .has⊥ cocone′ .centre .hom
--         where
--           cocone′ : Cocone (Const (fc.terminal .top))
--           cocone′ .coapex = x
--           cocone′ .ψ f = f
--           cocone′ .commutes f = C.idr _ ∙ sym f
--       adj₂ .counit .is-natural x y f = ap hom $ is-contr→is-prop
--         (cocompl _ .has⊥ (cocone y (λ g → f C.∘ g) (λ p → C.pullr (C.elimr refl ∙ sym p))))
--         (cocone-hom _ (λ o → C.pullr (cocompl _ .has⊥ _ .centre .commutes _) ∙ cocompl _ .has⊥ _ .centre .commutes _))
--         (cocone-hom _ (λ o → C.pullr (cocompl _ .has⊥ _ .centre .commutes _)))
--       adj₂ .zig = ap hom $ is-contr→is-prop
--         (cocompl _ .has⊥ (cocone (cocompl (Const (fc.terminal .top)) .bot .coapex) _ λ f → C.idr _ ∙ ap (cocompl _ .bot .ψ) (sym f)))
--         (cocone-hom _ λ o → C.pullr (cocompl _ .has⊥ _ .centre .commutes _) ∙ cocompl _ .has⊥ _ .centre .commutes _)
--         (cocone-hom C.id (λ o → C.idl _))
--       adj₂ .zag = funext λ x → cocompl _ .has⊥ _ .centre .commutes _
--   -}

--   {-
--   map→object : Geom[ C , PSh κ (FinSet ^op) ] → C.Ob
--   map→object gm = Inv[ gm ] .F₀ Fin→Sets

--   object→map : C.Ob → Geom[ C , PSh κ (FinSet ^op) ]
--   Inv[ object→map ob ] = Copower ob F∘ ev (FinSet ^op) 1
--   Dir[ object→map ob ] = const′ F∘ hom' where
--     hom' : Functor C (Sets κ)
--     hom' .F₀ ob′ = C.Hom ob ob′ , C.Hom-set _ _
--     hom' .F₁ f = f C.∘_
--     hom' .F-id = funext C.idl
--     hom' .F-∘ f g = funext λ _ → sym (C.assoc _ _ _)

--     const′ : Functor (Sets κ) (PSh κ (FinSet ^op))
--     const′ .F₀ c = Const c
--     const′ .F₁ f = NT (λ _ → f) (λ _ _ _ → refl)
--     const′ .F-id = Nat-path λ _ → refl
--     const′ .F-∘ f g = Nat-path λ _ → refl
--   object→map ob .Inv-lex = F∘-is-lex (record { pres-⊤ = {!   !} ; pres-pullback = {!   !} }) (right-adjoint→lex (const⊣ev _ _))
--   object→map ob .Inv⊣Dir = LF⊣GR adj₁ adj₂
--     where
--       open _⊣_
--       adj₁ : ev _ _ ⊣ _
--       adj₁ .unit .η x .η n o = x .F₁ (λ _ → fzero) o
--       adj₁ .unit .η x .is-natural y z f = funext λ _ →
--         sym (happly (x .F-∘ _ _) _) ∙ refl
--       adj₁ .unit .is-natural x y f = Nat-path λ _ → funext λ _ →
--         happly (sym (f .is-natural _ _ _)) _
--       adj₁ .counit .η _ o = o
--       adj₁ .counit .is-natural = λ _ _ _ → refl
--       adj₁ .zig {A} = funext λ x → ap (λ e → A .F₁ e x) (funext λ { fzero → refl })
--                                  ∙ happly (A .F-id) _
--       adj₁ .zag = Nat-path (λ _ → refl)

--       adj₂ : Copower ob ⊣ _
--       adj₂ .unit .η x i = cocompl _ .bot .ψ i
--       adj₂ .unit .is-natural x y f = funext λ _ → sym (cocompl _ .has⊥ _ .centre .commutes _)
--       adj₂ .counit .η x = cocompl _ .has⊥ cocone′ .centre .hom
--         where
--           cocone′ : Cocone (Const ob)
--           cocone′ .coapex = x
--           cocone′ .ψ f = f
--           cocone′ .commutes f = C.idr _ ∙ sym f
--       adj₂ .counit .is-natural x y f = ap hom $ is-contr→is-prop
--         (cocompl _ .has⊥ (cocone y (λ g → f C.∘ g) (λ p → C.pullr (C.elimr refl ∙ sym p))))
--         (cocone-hom _ (λ o → C.pullr (cocompl _ .has⊥ _ .centre .commutes _) ∙ cocompl _ .has⊥ _ .centre .commutes _))
--         (cocone-hom _ (λ o → C.pullr (cocompl _ .has⊥ _ .centre .commutes _)))
--       adj₂ .zig = ap hom $ is-contr→is-prop
--         (cocompl _ .has⊥ (cocone (cocompl (Const ob) .bot .coapex) _ λ f → C.idr _ ∙ ap (cocompl _ .bot .ψ) (sym f)))
--         (cocone-hom _ λ o → C.pullr (cocompl _ .has⊥ _ .centre .commutes _) ∙ cocompl _ .has⊥ _ .centre .commutes _)
--         (cocone-hom C.id (λ o → C.idl _))
--       adj₂ .zag = funext λ x → cocompl _ .has⊥ _ .centre .commutes _

--   test : ∀ x → map→object (object→map x) C.≅ x
--   test x = C.make-iso
--     (cocompl _ .has⊥ (cocone x (λ _ → C.id) (λ _ → C.idl _)) .centre .hom)
--     (cocompl _ .bot .ψ (lift fzero)) (cocompl _ .has⊥ _ .centre .commutes _)
--     $ ap hom $ is-contr→is-prop
--       (cocompl _ .has⊥ (cocompl _ .bot))
--       (cocone-hom _ (λ o → C.pullr (cocompl _ .has⊥ _ .centre .commutes _) ∙ C.idr _ ∙ ap (cocompl (Const x) .bot .ψ) (ap lift (p (Lift.lower o)))))
--       (cocone-hom _ (λ o → C.idl _))
--     where
--       p : (o : Fin 1) → fzero ≡ o
--       p fzero = refl
--   -}
-}