open import Cat.Diagram.Everything
open import Cat.Functor.Everything
open import Cat.Prelude
open import Topoi.Classifying.Diaconescu
open import Topoi.Reasoning
open import Topoi.Base
open import Data.Fin

module wip.flat
  {o κ} {C : Precategory κ κ} {E : Precategory o κ}
  (T : Topos κ E)
  where

private
  module E = Sheaf-topos T
  abstract
    colim : is-cocomplete κ κ E
    colim = Topos-is-cocomplete T
open Cocone-hom
open Cone-hom
open Terminal
open Initial
open Functor
open Cocone
open Cone

{-
factor
  : (F : Functor C E) {I : Precategory κ κ} {G : Functor I C}
  → (K : Cone G)
  → E.Hom (F-map-cone F K .apex) (Topos-is-complete T (F F∘ G) .top .apex)
factor F {G = G} K =
  Topos-is-complete T (F F∘ G) .has⊤ (F-map-cone F K) .centre .hom

Internally-flat : Functor C E → Type _
Internally-flat F =
  ∀ {A} {I : Precategory κ κ} {G : Functor I C} {f g : E.Hom _ A}
  → (∀ {K : Cone G} → f E.∘ factor F K ≡ g E.∘ factor F K)
  → f ≡ g

lemma
  : ∀ (F : Functor C E) {X}
  → Realisation colim F .F₀ X E.≅ colim {!   !} .bot .coapex
  -}