strictly positive

record SP : Set₁ where
  field
    F    : Set → Set

    mon  : ∀{ρ ρ'} → (ρ → ρ') → (Fρ : F ρ) → F ρ'

    Supp : ∀ {ρ} → F ρ → Set

    mon-Supp : ∀ {ρ ρ'} (f : ρ → ρ') (Fρ : F ρ)
               → Supp (mon f Fρ) → Supp Fρ

    necc  : ∀ {ρ} (Fρ : F ρ) → Supp Fρ → ρ

    suff : ∀ {ρ} → (Fρ : F ρ) → F (Supp Fρ)

    necc-suff : ∀ {ρ} {Fρ : F ρ} →  mon (necc Fρ) (suff Fρ) ≡ Fρ

    suff-necc : ∀ {ρ} {Fρ : F ρ} (p : Supp _) → necc (suff Fρ) (mon-Supp (necc Fρ) (suff Fρ) p) ≡ subst Supp necc-suff p

open SP