open import Cat.Instances.Slice.Presheaf
open import Cat.Diagram.Everything
open import Cat.Functor.Everything
open import Cat.Instances.Elements
open import Cat.Instances.Functor
open import Cat.Instances.Comma
open import Cat.Instances.Slice
open import Cat.Prelude

open import Topoi.Base

import Cat.Reasoning

module wip.slice where

open Functor
open /-Obj
open /-Hom
open _=>_
open _⊣_

-- module _ {o h : _} (C : Precategory o h) where
--   private module C = Cat.Reasoning C
--   open C.HLevel-instance

--   ev : ∀ {ℓ} (c : C.Ob) → Functor (PSh ℓ C) (Sets ℓ)
--   F₀ (ev c) x = F₀ x c
--   F₁ (ev c) x x₁ = η x c x₁
--   F-id (ev c) = refl
--   F-∘ (ev c) f g = refl

-- module
--   _ {o o′ κ} {C : Precategory o κ} {D : Precategory o′ κ}
--     (ct : Topos C κ) (dt : Topos D κ)
--     (F : Functor D C)
--     (cont : is-continuous {oshape = κ} {κ} F)
--     where

--   open Initial
--   open Terminal
--   open Cone
--   open Cone-hom
--   open ↓Hom
--   open ↓Obj

--   private
--     module C = Cat.Reasoning C
--     module D = Cat.Reasoning D
--     module ct = Topos ct
--     module dt = Topos dt
--     module Cs = Cat.Reasoning (ct.site)
--     module Ds = Cat.Reasoning (dt.site)
--     module Pc = Cat.Reasoning (PSh κ (ct.site))
--     module Pd = Cat.Reasoning (PSh κ (dt.site))
--     module F = Functor F
--     abstract
--       dlim : is-complete κ κ D
--       dlim = Topos-is-complete dt

--   univ : ∀ o → Initial (o ↙ F)
--   univ o = init where
--     test′ : Precategory κ κ
--     test′ = ct.ι.₀ o ↙ (ct.ι F∘ (F F∘ (dt.L F∘ よ dt.site)))

--     lc : Limit _
--     lc = dlim {D = test′} ((dt.L F∘ よ dt.site) F∘ Cod _ _)

--     clim : _
--     clim = cont (lc .top) (lc .has⊤)

--     init : Initial (o ↙ F)
--     init .bot .↓Obj.x = tt
--     init .bot .↓Obj.y = lc .top .apex
--     init .bot .↓Obj.map = clim cone′ .centre .hom
--       where
--         cone′ : Cone _
--         cone′ .apex = o
--         cone′ .ψ ob = equiv→inverse ct.has-ff (ob .map)
--         cone′ .commutes f = {!   !}
--     init .has⊥ = {!   !}

-- module _ {o κ} {C : Precategory o κ} (ct : Topos C κ) where
--   private
--     module C = Cat.Reasoning C
--     module ct = Topos ct
--     module Site = Cat.Reasoning (ct.site)
--     module PSh = Cat.Reasoning (PSh κ (ct.site))
--     module ι = Functor (ct.ι)
--     module L = Functor (ct.L)
--     open _⊣_ (ct.L⊣ι)

--   open Functor
--   open _=>_
--   open Terminal
--   open Initial
--   open Cocone

--   generator : C.Ob
--   generator = Topos-is-cocomplete ct {D = ct.site} (ct.L F∘ よ ct.site) .bot .coapex

--   abstract
--     T-fc : Finitely-complete C
--     T-fc = is-complete→finitely C (Topos-is-complete ct)

--   open Finitely-complete T-fc

--   よ-univ : ∀ o → Initial (o ↙ よ C)
--   よ-univ o = init where
--     ob : Precategory.Ob (o ↙ よ C)
--     ob .↓Obj.x = tt
--     ob .↓Obj.y = {!   !}
--     ob .↓Obj.map = {!   !}

--     init : Initial (o ↙ よ C)
--     init .bot = ob
--     init .has⊥ = {!   !}