wip.inst

module wip.inst where

open import 1Lab.Prelude
open import Data.Set.Coequaliser
open import Data.Bool
open import Data.Sum

postulate
  sup : ∀ {ℓ} {I : Type (lsuc ℓ)} (T : I → Prop ℓ) → Prop ℓ
  sup-coproj : ∀ {ℓ} {I : Type (lsuc ℓ)} {F : I → Prop ℓ} (i : I) → ∣ F i ∣ → ∣ sup F ∣
  sup-match
    : ∀ {ℓ ℓ′} {I : Type (lsuc ℓ)} {F : I → Prop ℓ} {Q : Prop ℓ′}
    → (∀ i → ∣ F i ∣ → ∣ Q ∣) → ∣ sup F ∣ → ∣ Q ∣

resize : ∀ {ℓ} → Prop (lsuc ℓ) → Prop ℓ
resize P = sup {I = ∣ P ∣} λ _ → Lift _ ⊤ , λ _ _ _ → lift tt

test : ∀ {ℓ} → is-equiv (resize {ℓ})
test {ℓ} = is-iso→is-equiv (iso lift′ p q) where
  lift′ : ∀ {ℓ} → Prop ℓ → Prop (lsuc ℓ)
  lift′ P = Lift _ ∣ P ∣ , Lift-is-hlevel 1 (P .is-tr)

  p : ∀ (x : Prop ℓ) → sup _ ≡ x
  p x = n-ua $ prop-ext (sup _ .is-tr) (x .is-tr)
    (sup-match {I = Lift _ ∣ x ∣} {Q = x} (λ (lift x) _ → x))
    λ x → sup-coproj (lift x) (lift tt)

  q : ∀ (x : Prop (lsuc ℓ)) → _ ≡ x
  q x = n-ua $ prop-ext (Lift-is-hlevel 1 (sup _ .is-tr)) (x .is-tr)
    (λ (lift m) → sup-match {Q = x} (λ i _ → i) m)
    λ o → lift (sup-coproj o (lift tt))

module _ {ℓ} {A : Set ℓ} {P : ∣ A ∣ → Prop ℓ} where
  rel : ∣ A ∣ → Bool → Bool → Type ℓ
  rel a false false = Lift _ ⊤
  rel a false true = ∣ P a ∣
  rel a true false = ∣ P a ∣
  rel a true true = Lift _ ⊤

  open import Cat.Prelude
  open import Cat.Instances.Discrete
  open import Cat.Instances.Sets.Cocomplete
  open import Cat.Instances.Shape.Join
  open import Cat.Instances.Shape.Terminal
  open import Cat.Diagram.Everything

  open Functor
  open Initial
  open Cocone
  open Cocone-hom

  diagram′ : Functor (⊤Cat ⋆ Disc′ A) (Sets ℓ)
  diagram′ .F₀ (inl tt) = Lift _ Bool , Lift-is-hlevel 2 Bool-is-set
  diagram′ .F₀ (inr x) = (Bool / rel x) , squash
  diagram′ .F₁ {inl x} {inl x₁} f a = a
  diagram′ .F₁ {inl x} {inr x₁} f a = inc (Lift.lower a)
  diagram′ .F₁ {inr x} {inr x₁} f a = subst (λ e → Bool / rel e) (Lift.lower f) a
  diagram′ .F-id {inl x} = refl
  diagram′ .F-id {inr x} = funext λ _ → transport-refl _
  diagram′ .F-∘ {inl x} {inl x₁} {inl x₂} f g = refl
  diagram′ .F-∘ {inl x} {inl x₁} {inr x₂} f g = refl
  diagram′ .F-∘ {inl x} {inr x₁} {inr x₂} f g = refl
  diagram′ .F-∘ {inr x} {inr x₁} {inr x₂} f g = funext $ λ a →
    subst-∙ (λ e → Bool / rel e) (Lift.lower g) (Lift.lower f) a

  colim : Colimit diagram′
  colim = Sets-is-cocomplete {o = ℓ} diagram′

  test′ : Bool → ∣ colim .bot .coapex ∣
  test′ x = inc (inl tt , lift x)