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

open import Topoi.Base

import Cat.Reasoning

open Terminal
open Functor
open ↓Obj
open ↓Hom
open _=>_
open _⊣_

module wip.artin
  {o o′ κ} {C : Precategory o κ} {D : Precategory o′ κ}
  (ct : Topos κ C) (dt : Topos κ D)
  (F : Functor C D)
  (Flex : is-lex F)
  where

private
  open is-lex Flex
  module F = Functor F
  module C = Cat.Reasoning C
  module D = Cat.Reasoning D
  module ct = Topos ct

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

  D-fcc : Finitely-complete (D ^op)
  D-fcc = is-complete→finitely (D ^op) λ f → subst Limit F^op^op≡F $
    Colimit→Co-limit D (Topos-is-cocomplete dt (Functor.op f))

  module Cfc = Finitely-complete C-fc
  module Dfcc = Finitely-complete D-fcc

Glued : Precategory _ _
Glued = Id ↓ F

↓-Inc : Functor Glued C
↓-Inc .F₀ o = o .y
↓-Inc .F₁ f = f .β
↓-Inc .F-id = refl
↓-Inc .F-∘ f g = refl

↓-Inc-radj : Functor C Glued
↓-Inc-radj .F₀ x .x = F.₀ x
↓-Inc-radj .F₀ x .y = x
↓-Inc-radj .F₀ x .map = D.id
↓-Inc-radj .F₁ h .α = F.₁ h
↓-Inc-radj .F₁ h .β = h
↓-Inc-radj .F₁ h .sq = sym D.id-comm
↓-Inc-radj .F-id = ↓Hom-path _ _ F.F-id refl
↓-Inc-radj .F-∘ f g = ↓Hom-path _ _ (F.F-∘ _ _) refl

right-ff : is-fully-faithful ↓-Inc-radj
right-ff {x} {y} = is-iso→is-equiv
  (iso inv (λ x → ↓Hom-path _ _ (D.intror refl ∙ sym (x .sq) ∙ D.eliml refl) refl)
           λ x → refl)
  where
    inv : ↓Hom Id F _ _ → C.Hom x y
    inv x = x .β

-- adjunction :