open import Cat.Diagram.Coproduct.Indexed
open import Cat.Functor.FullSubcategory
open import Cat.Thin.Instances.Sub
open import Cat.Diagram.Coproduct
open import Cat.Instances.Slice
open import Cat.Instances.Sets
open import Cat.Morphism
open import Cat.Prelude
open import Cat.Thin

open import Data.Sum

import Cat.Thin.Limits

module wip.test4 {ℓ} where

private variable X : Set ℓ

open Precategory
open /-Hom
open /-Obj

-- _∪_ : Ob (Subobj (Sets ℓ) X) → Ob (Subobj (Sets ℓ) X) → Ob (Subobj (Sets ℓ) X)
-- _∪_ {X = X} Afm Bgm = cut {domain = img} fst , embedding→monic (Subset-proj-embedding λ _ → squash) where
--   A = Af .domain
--   f = Af .map

--   B = Bg .domain
--   g = Bg .map

--   cup→x : ∣ A ∣ ⊎ ∣ B ∣ → ∣ X ∣
--   cup→x (inl x) = f x
--   cup→x (inr x) = g x

--   im = image cup→x
--   img = im , Σ-is-hlevel 2 (X .is-tr) λ _ → is-prop→is-set squash

-- open Coproduct
-- open is-coproduct

-- coprod : ∀ {A B} → Coproduct (Subobj (Sets ℓ) X) A B
-- coprod {A = A} {B} .coapex = A ∪ B
-- coprod {A = A} {B} .in₀ .map x = A .fst .map x , inc (inl x , refl)
-- coprod {A = A} {B} .in₀ .commutes = refl
-- coprod {A = A} {B} .in₁ .map x = B .fst .map x , inc (inr x , refl)
-- coprod {A = A} {B} .in₁ .commutes = refl
-- coprod {X = X} {A = A} {B} .has-is-coproduct .is-coproduct.[_,_] {Q = Q} l r =
--   record
--     { map      = the-map
--     ; commutes = funext λ where
--       (y , p) → ∥-∥-elim (λ x → X .is-tr (Q .fst .map (the-map (y , x))) _)
--         (λ { (inl x , p) → happly (l .commutes) _ ∙ p
--            ; (inr x , p) → happly (r .commutes) _ ∙ p }) p
--     }
--   where
--     the-map : Hom (Sets ℓ) (coprod .coapex .fst .domain) (domain (Q .fst))
--     the-map (y , p) =
--       ∥-∥-elim {P = λ _ → fibre (Q .fst .map) y}
--         (λ _ → monic-between-sets→is-embedding {f = Q .fst .map} (X .is-tr) (λ {C = C} g h p → Q .snd {c = C} g h p) y)
--         (λ { (inl x , p) → l .map x , happly (l .commutes) _ ∙ p
--            ; (inr x , p) → r .map x , happly (r .commutes) _ ∙ p }) p .fst
-- coprod {A = A} {B} .has-is-coproduct .in₀∘factor {Q = Q} =
--   Subobj-is-thin (Sets ℓ) {A = A} {B = Q} _ _
-- coprod {A = A} {B} .has-is-coproduct .in₁∘factor {Q = Q} =
--   Subobj-is-thin (Sets ℓ) {A = B} {B = Q} _ _
-- coprod {A = A} {B} .has-is-coproduct .unique {Q = Q} other _ _ =
--   Subobj-is-thin (Sets ℓ) {A = A ∪ B} {B = Q} other _

module _ {X : Set ℓ} where
  module P = Poset (Subobjects (Sets ℓ) Sets-is-category X)
  open Cat.Thin.Limits {P = Poset.→Proset (Subobjects (Sets ℓ) Sets-is-category X)}

  module _ {I : Type ℓ} {F : I → P.Ob} where
    cup = Σ[ i ∈ I ] ∣ F i .object .domain ∣
    inj : cup → ∣ X ∣
    inj (i , x) = F i .object .map x

    img = image inj
    sub : P.Ob
    sub .object .domain = img , Σ-is-hlevel  (X .is-tr) λ _ → is-prop→is-set squash
    sub .object .map = fst
    sub .witness = embedding→monic (Subset-proj-embedding λ _ → squash)

    injs : ∀ i → P.Hom (F i) sub
    injs i .map x = F i .object .map x , inc ((i , x) , refl)
    injs i .commutes = refl

    is-coprod : is-indexed-coproduct (Subobj (Sets ℓ) X) {S = sub} F injs
    is-coprod = indexed-join→indexed-coproduct injs (λ {B} → proj {B = B}) where
      proj : {B : P.Ob} → (∀ i → F i P.≤ B) → sub P.≤ B
      proj {B = B} f .map (y , p) = ∥-∥-elim {P = λ _ → fibre (B .object .map) y}
        (λ _ → monic-between-sets→is-embedding (X .is-tr)
                (λ {C = C} → B .witness {c = C}) y)
        (λ { ((i , x) , p) → f i .map x , happly (f i .commutes) _ ∙ p })
        p .fst
      proj {B = B} f .commutes = funext λ where
        (y , p) → ∥-∥-elim
          (λ x → X .is-tr (B .object .map (proj {B = B} f .map (y , x))) _)
          (λ { ((i , x) , p) → happly (f i .commutes) _ ∙ p })
          p

open import Agda.Builtin.Maybe

private variable A : Type

just-injective : ∀ {x y} → Path (Maybe A) (just x) (just y) → x ≡ y
just-injective {x = x} p = J (λ y p → x ≡ unjust x y) refl p
  where unjust : A → Maybe A → A
        unjust x (just x₁) = x₁
        unjust x nothing = x