open import Categories.Category.Core
open import Categories.Category.Distributive
open import Categories.Category.Restriction
open import Categories.Object.Terminal
open import Relation.Binary.Bundles using (Poset)
open import Monad.Helper
open import Data.Product using (_,_)
open import Algebra.Elgot
open import Category.Construction.ElgotAlgebras
open import Categories.FreeObjects.Free
open import Categories.Object.NaturalNumbers
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Category.Construction.F-Algebras

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP

import Monad.Instance.K as MIK
-- The kleisli category of K is enriched over pointed partial orders and strict monotone maps.

module Monad.Instance.K.OrderEnriched {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (MK : MIK.MonadK distributive) where
  open import Category.Distributive.Helper distributive renaming (η to η-prod)
  open Bundles
  
  open MIK distributive

  open MonadK MK
  open Category C
  open Equiv
  open HomReasoning
  open M C
  open MR C
  open MP C
  open kleisliK using (extend; extend-≈)
  open monadK using (μ)
  open import Monad.Instance.K.Strong distributive MK
  open import Monad.Instance.K.Commutative distributive MK
  open import Monad.Instance.K.EquationalLifting distributive MK
  open import Monad.Instance.K.Restriction distributive MK
  open strongK using (strengthen; strength-assoc)
  open Restriction KRestriction renaming (_↓ to _↓'; ↓-denestʳ to ↓-denestʳ'; ↓-cong to ↓-cong'; pidʳ to pidʳ'; ↓-comm to ↓-comm'; ↓-skew-comm to ↓-skew-comm')
  open import Categories.Category.Restriction.Properties.Poset KRestriction
  open import Categories.Category.Restriction.Properties KRestriction renaming (↓-idempotent to ↓-idempotent')
  open import Categories.Object.NaturalNumbers.Parametrized.Properties.F-Algebras C cartesian coproducts
  open import Categories.Monad.Commutative.Properties

  open CommutativeProperties braided KCommutativeMonad
 
  -- NOTE: f ↓' ≈ extend (η _ ∘ π₂) ∘ extend (ψ ∘ (η _ ∘ ! ×₁ η _)) ∘ extend (ψ ∘ (f ×₁ η _)) ∘ η _ ∘ ⟨ id , id ⟩

  _↓ : ∀ {X Y} (f : X ⇒ K.₀ Y) → X ⇒ K.₀ X
  f ↓ = K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩

  ↓-charac : ∀ {X Y} {f : X ⇒ K.₀ Y} → f ↓' ≈ f ↓
  ↓-charac {f = f} = begin 
    extend (η _ ∘ π₂) ∘ extend (ψ ∘ (η _ ∘ ! ×₁ η _)) ∘ extend (ψ ∘ (f ×₁ η _)) ∘ η _ ∘ ⟨ id , id ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ kleisliK.identityʳ ⟩ 
    extend (η _ ∘ π₂) ∘ extend (ψ ∘ (η _ ∘ ! ×₁ η _)) ∘ (ψ ∘ (f ×₁ η _)) ∘ ⟨ id , id ⟩              ≈⟨ refl⟩∘⟨ (extend-≈ (∘-resp-≈ʳ (sym (×₁∘×₁ ○ ×₁-cong₂ refl identityʳ))) ⟩∘⟨refl) ⟩ 
    extend (η _ ∘ π₂) ∘ extend (ψ ∘ (η _ ×₁ η _) ∘ (! ×₁ id)) ∘ (ψ ∘ (f ×₁ η _)) ∘ ⟨ id , id ⟩      ≈⟨ refl⟩∘⟨ (extend-≈ (pullˡ ψ-η) ⟩∘⟨refl) ⟩ 
    extend (η _ ∘ π₂) ∘ extend (η _ ∘ (! ×₁ id)) ∘ (ψ ∘ (f ×₁ η _)) ∘ ⟨ id , id ⟩                   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ψ-τ' ⟩∘⟨refl ⟩ 
    extend (η _ ∘ π₂) ∘ extend (η _ ∘ (! ×₁ id)) ∘ (σ _ ∘ (f ×₁ id)) ∘ ⟨ id , id ⟩                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ ×₁∘Δ ⟩ 
    extend (η _ ∘ π₂) ∘ extend (η _ ∘ (! ×₁ id)) ∘ σ _ ∘ ⟨ f , id ⟩                                 ≈⟨ pullˡ (kleisliK.sym-assoc ○ extend-≈ (pullˡ kleisliK.identityʳ)) ⟩ 
    extend ((η _ ∘ π₂) ∘ (! ×₁ id)) ∘ σ _ ∘ ⟨ f , id ⟩                                              ≈⟨ (extend-≈ (pullʳ (project₂ ○ identityˡ))) ⟩∘⟨refl ⟩ 
    extend (η _ ∘ π₂) ∘ σ _ ∘ ⟨ f , id ⟩                                                            ≈˘⟨ sym (F₁⇒extend monadK π₂) ⟩∘⟨refl ⟩ 
    K.₁ π₂ ∘ (K.₁ swap ∘ τ _ ∘ swap) ∘ ⟨ f , id ⟩                                                   ≈⟨ refl⟩∘⟨ (pullʳ (pullʳ swap∘⟨⟩)) ⟩ 
    K.₁ π₂ ∘ K.₁ swap ∘ τ _ ∘ ⟨ id , f ⟩                                                            ≈⟨ pullˡ (sym K.homomorphism ○ K.F-resp-≈ project₂) ⟩ 
    K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩                                                                       ∎

  pidʳ : ∀ {X Y} {f : X ⇒ K.₀ Y} → extend f ∘ f ↓ ≈ f
  pidʳ {f=f} = ∘-resp-≈ʳ (sym ↓-charac) ○ pidʳ'

  ↓-comm : ∀ {X Y Z} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} → extend (f ↓) ∘ g ↓ ≈ extend (g ↓) ∘ f ↓
  ↓-comm {f=f} {g} = ∘-resp-≈ (extend-≈ (sym ↓-charac)) (sym ↓-charac)
    ○ ↓-comm'
    ○ ∘-resp-≈ (extend-≈ ↓-charac) ↓-charac

  ↓-cong : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ≈ g → f ↓ ≈ g ↓
  ↓-cong f≈g = sym ↓-charac ○ ↓-cong' f≈g ○ ↓-charac

  ↓-denestʳ : ∀ {X Y Z} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} → (extend g ∘ f ↓) ↓ ≈ extend (g ↓) ∘ f ↓
  ↓-denestʳ {f = f} {g} = begin 
    (extend g ∘ f ↓) ↓   ≈˘⟨ ↓-charac ○ ↓-cong (∘-resp-≈ʳ ↓-charac) ⟩ 
    (extend g ∘ f ↓') ↓' ≈⟨ ↓-denestʳ' ⟩ 
    extend (g ↓') ∘ f ↓' ≈⟨ extend-≈ ↓-charac ⟩∘⟨ ↓-charac ⟩ 
    extend (g ↓) ∘ f ↓   ∎

  ↓-idempotent : ∀ {X Y} {f : X ⇒ K.₀ Y} → f ↓ ↓ ≈ f ↓
  ↓-idempotent {f = f} = begin 
    f ↓ ↓   ≈˘⟨ ↓-charac ○ ↓-cong ↓-charac ⟩ 
    f ↓' ↓' ≈⟨ ↓-idempotent' ⟩
    f ↓'    ≈⟨ ↓-charac ⟩
    f ↓     ∎

  -- restriction of f to domain of g
  _⇂_ : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (g : X ⇒ K.₀ Z) → X ⇒ K.₀ Y
  f ⇂ g = extend π₁ ∘ τ _ ∘ ⟨ f , g ⟩

  -- lemmas on domain and restriction
  ⇂-cong₂ : ∀ {X Y Z} {f h : X ⇒ K.₀ Y} {g i : X ⇒ K.₀ Z} → f ≈ h → g ≈ i → f ⇂ g ≈ h ⇂ i
  ⇂-cong₂ eq₁ eq₂ = refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ eq₁ eq₂

  restrict-η : ∀ {X Y} {f : X ⇒ K.₀ Y} → η X ⇂ f ≈ f ↓
  restrict-η {X} {Y} {f} = begin 
    extend π₁ ∘ τ _ ∘ ⟨ η X , f ⟩                    ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
    extend π₁ ∘ τ _ ∘ (η X ×₁ id) ∘ ⟨ id , f ⟩       ≈⟨ refl⟩∘⟨ pullˡ (τ-comm-id (η X)) ⟩ 
    extend π₁ ∘ (K.₁ (η X ×₁ id) ∘ τ _) ∘ ⟨ id , f ⟩ ≈⟨ pullˡ (pullˡ (extend∘F₁ monadK π₁ (η X ×₁ id))) ⟩ 
    (extend (π₁ ∘ (η X ×₁ id)) ∘ τ _) ∘ ⟨ id , f ⟩   ≈⟨ (kleisliK.extend-≈ project₁ ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
    (extend (η X ∘ π₁) ∘ τ _) ∘ ⟨ id , f ⟩           ≈⟨ pushˡ ((F₁⇒extend monadK π₁) ⟩∘⟨refl) ⟩ 
    K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩                        ∎

  restrict-law : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (g : X ⇒ K.₀ Z) → f ⇂ g ≈ extend f ∘ g ↓
  restrict-law {X} {Y} {Z} f g = begin 
    extend π₁ ∘ τ (K.₀ Y , Z) ∘ ⟨ f , g ⟩                   ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ 
    extend π₁ ∘ τ (K.₀ Y , Z) ∘ (f ×₁ id) ∘ ⟨ id , g ⟩      ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm-id f)) ⟩ 
    extend π₁ ∘ (K.₁ (f ×₁ id) ∘ τ (X , Z)) ∘ ⟨ id , g ⟩    ≈⟨ (refl⟩∘⟨ assoc) ○ pullˡ (pullʳ (sym K.homomorphism)) ⟩ 
    (μ.η _ ∘ K.₁ (π₁ ∘ (f ×₁ id))) ∘ τ (X , Z) ∘ ⟨ id , g ⟩ ≈⟨ (refl⟩∘⟨ ((K.F-resp-≈ π₁∘×₁) ○ K.homomorphism)) ⟩∘⟨refl ⟩ 
    (μ.η Y ∘ (K.₁ f ∘ K.₁ π₁)) ∘ τ (X , Z) ∘ ⟨ id , g ⟩     ≈⟨ sym-assoc ⟩∘⟨refl ○ assoc ⟩ 
    extend f ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ id , g ⟩                    ∎

  ⇂∘ : ∀ {A X Y Z} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} {h : A ⇒ X} → (f ⇂ g) ∘ h ≈ (f ∘ h) ⇂ (g ∘ h)
  ⇂∘ {A} {X} {Y} {Z} {f} {g} {h} = pullʳ (pullʳ ⟨⟩∘)

  η↓ : ∀ {X Y} (f : X ⇒ K.₀ Y) → (η (K.₀ Y) ∘ f) ↓ ≈ η X
  η↓ {X} {Y} f = begin 
    K.₁ π₁ ∘ τ _ ∘ ⟨ id , η _ ∘ f ⟩         ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩ 
    K.₁ π₁ ∘ τ _ ∘ (id ×₁ η _) ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (τ-η _)) ⟩ 
    K.₁ π₁ ∘ η _ ∘ ⟨ id , f ⟩               ≈⟨ pullˡ (K₁η π₁) ⟩ 
    (η _ ∘ π₁) ∘ ⟨ id , f ⟩                 ≈⟨ cancelʳ project₁ ⟩ 
    η _                                     ∎

  -- f ↓ == M₁ π₁ ∘ σ ∘ ⟨ id , f ⟩
  ⇂-assoc : ∀ {A X Y Z} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} {h : X ⇒ K.₀ A} → (f ⇂ g) ⇂ h ≈ f ⇂ (g ⇂ h)
  ⇂-assoc {A} {X} {Y} {Z} {f} {g} {h} = begin 
    (f ⇂ g) ⇂ h                     ≈⟨ restrict-law _ _ ○ ∘-resp-≈ˡ (extend-≈ (restrict-law _ _)) ⟩ 
    extend (extend f ∘ g ↓) ∘ h ↓   ≈˘⟨ pullˡ (sym kleisliK.assoc) ⟩ 
    extend f ∘ extend (g ↓) ∘ h ↓   ≈˘⟨ refl⟩∘⟨ ↓-denestʳ ⟩ 
    extend f ∘ ((extend g ∘ h ↓) ↓) ≈˘⟨ restrict-law _ _ ○ ∘-resp-≈ʳ (↓-cong (restrict-law _ _)) ⟩ 
    f ⇂ (g ⇂ h)                     ∎

  infixr  _⊑_

  -- This is an alternative definition of the order to the one in `Categories.Category.Restriction.Properties.Poset`
  -- But they are in fact equivalent, which is what we use to get `refl`, `trans` and `antisym`

  _⊑_ : ∀ {X Y} (f g : X ⇒ K.₀ Y) → Set e
  f ⊑ g = f ≈ g ⇂ f

  module PartialOrder where
    private
      _≤_ : ∀ {X Y} (f g : X ⇒ K.₀ Y) → Set e
      _≤_ {X} {Y} = _≤'_
        where open Poset (poset X Y) using () renaming (_≤_ to _≤'_) 
      
      ≤⇔⊑-helper' : ∀ {X Y} {f g : X ⇒ K.₀ Y} → extend g ∘ f ↓ ≈ extend π₁ ∘ τ _ ∘ ⟨ g , f ⟩
      ≤⇔⊑-helper' {X} {Y} {f} {g} = begin 
        extend g ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩         ≈⟨ pullˡ (extend∘F₁ monadK g π₁) ⟩ 
        extend (g ∘ π₁) ∘ τ _ ∘ ⟨ id , f ⟩           ≈˘⟨ (extend-≈ project₁) ⟩∘⟨refl ⟩ 
        extend (π₁ ∘ (g ×₁ id)) ∘ τ _ ∘ ⟨ id , f ⟩   ≈˘⟨ pullˡ ((extend∘F₁ monadK π₁ (g ×₁ id))) ⟩ 
        extend π₁ ∘ K.₁ (g ×₁ id) ∘ τ _ ∘ ⟨ id , f ⟩ ≈˘⟨ refl⟩∘⟨ (extendʳ (strongK.strengthen.commute (g , id))) ⟩ 
        extend π₁ ∘ τ _ ∘ (g ×₁ K.₁ id) ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ (elimˡ K.identity)) ⟩ 
        extend π₁ ∘ τ _ ∘ ⟨ g , f ⟩                  ∎

      ≤⇔⊑-helper : ∀ {X Y} {f g : X ⇒ K.₀ Y} → extend g ∘ f ↓' ≈ extend π₁ ∘ τ _ ∘ ⟨ g , f ⟩
      ≤⇔⊑-helper {X} {Y} {f} {g} = ∘-resp-≈ʳ ↓-charac ○ ≤⇔⊑-helper'

      ≤⇒⊑ : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ≤ g → f ⊑ g
      ≤⇒⊑ {X} {Y} {f} {g} leq = begin 
        f                           ≈⟨ leq ⟩
        extend g ∘ f ↓'             ≈⟨ ≤⇔⊑-helper ⟩ 
        extend π₁ ∘ τ _ ∘ ⟨ g , f ⟩ ∎
      ⊑⇒≤ : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ⊑ g → f ≤ g
      ⊑⇒≤ {X} {Y} {f} {g} sqleq = begin 
        f                           ≈⟨ sqleq ⟩ 
        extend π₁ ∘ τ _ ∘ ⟨ g , f ⟩ ≈˘⟨ ≤⇔⊑-helper ⟩  
        extend g ∘ f ↓'             ∎

    ⊑-refl : ∀ {X Y} {f : X ⇒ K.₀ Y} → f ⊑ f
    ⊑-refl {X} {Y} = ≤⇒⊑ (refl' refl)
      where open Poset (poset X Y) using () renaming (reflexive to refl')

    ⊑-trans : ∀ {X Y} {f g h : X ⇒ K.₀ Y} → f ⊑ g → g ⊑ h → f ⊑ h
    ⊑-trans {X} {Y} f⊑g g⊑h = ≤⇒⊑ (trans' (⊑⇒≤ f⊑g) (⊑⇒≤ g⊑h))
      where open Poset (poset X Y) using () renaming (trans to trans')

    ⊑-antisym : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ⊑ g → g ⊑ f → f ≈ g
    ⊑-antisym {X} {Y} f⊑g g⊑f = antisym' (⊑⇒≤ f⊑g) (⊑⇒≤ g⊑f)
      where open Poset (poset X Y) using () renaming (antisym to antisym')

  open PartialOrder public


  -- right monotonicity of composition
  ⊑∘ʳ : ∀ {A X Y} {f g : X ⇒ K.₀ Y} {h : Y ⇒ K.₀ A} → f ⊑ g → (extend h ∘ f) ⊑ (extend h ∘ g)
  ⊑∘ʳ {A} {X} {Y} {f} {g} {h} leq = begin
    extend h ∘ f                                              ≈⟨ refl⟩∘⟨ leq ⟩
    extend h ∘ (g ⇂ f)                                        ≈⟨ refl⟩∘⟨ (restrict-law g f) ⟩
    extend h ∘ extend g ∘ f ↓                                 ≈⟨ pullˡ kleisliK.sym-assoc ⟩
    extend (extend h ∘ g) ∘ f ↓                               ≈˘⟨ ∘-resp-≈ˡ (extend-≈ pidʳ) ⟩
    extend (extend (extend h ∘ g) ∘ ((extend h ∘ g) ↓)) ∘ f ↓ ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
    extend (extend h ∘ g) ∘ extend ((extend h ∘ g) ↓) ∘ f ↓   ≈˘⟨ refl⟩∘⟨ ↓-denestʳ ⟩
    extend (extend h ∘ g) ∘ (extend (extend h ∘ g) ∘ (f ↓)) ↓ ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
    extend h ∘ extend g ∘ (extend (extend h ∘ g) ∘ (f ↓)) ↓   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ↓-cong (∘-resp-≈ˡ kleisliK.assoc ○ assoc) ⟩
    extend h ∘ extend g ∘ (extend h ∘ extend g ∘ f ↓)↓        ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ↓-cong (refl⟩∘⟨ leq ○ ∘-resp-≈ʳ (restrict-law g f) ) ⟩ -- h g dom(h g dom(f))
    extend h ∘ extend g ∘ (extend h ∘ f)↓                     ≈⟨ pullˡ (kleisliK.sym-assoc) ⟩ -- h g dom(h f)
    extend (extend h ∘ g) ∘ (extend h ∘ f)↓                   ≈˘⟨ restrict-law (extend h ∘ g) (extend h ∘ f) ⟩
    (extend h ∘ g) ⇂ (extend h ∘ f)                           ∎

  -- left monotonocity of composition
  ⊑∘ˡ : ∀ {A X Y} {f g : X ⇒ K.₀ Y} {h : A ⇒ X} → f ⊑ g → (f ∘ h) ⊑ (g ∘ h)
  ⊑∘ˡ {A} {X} {Y} {f} {g} {h} leq = begin 
    f ∘ h               ≈⟨ leq ⟩∘⟨refl ⟩ 
    (g ⇂ f) ∘ h         ≈⟨ ⇂∘ ⟩ 
    ((g ∘ h) ⇂ (f ∘ h)) ∎

  ⊑-cong₂ : ∀ {X Y} {f g h i : X ⇒ K.₀ Y} → f ≈ h → g ≈ i → f ⊑ g → h ⊑ i
  ⊑-cong₂ eq₁ eq₂ leq = (sym eq₁) ○ leq ○ ⇂-cong₂ eq₂ eq₁

  f↓⊑η : ∀ {X Y} {f : X ⇒ K.₀ Y} → f ↓ ⊑ η X
  f↓⊑η {X} {Y} {f} = begin 
    f ↓         ≈˘⟨ ↓-idempotent ⟩ 
    (f ↓)↓      ≈˘⟨ restrict-η ⟩ 
    η X ⇂ (f ↓) ∎


  -- bottom element of restriction order
  bot : ∀ {X} {Y} → X ⇒ K.₀ Y
  bot = i₂ #

  bot∘! : ∀ {X} {Y} → bot {X} {Y} ≈ bot {⊤} {Y} ∘ !
  bot∘! = #-Uniformity (algebras _) inject₂

  bot-absorbs : ∀ {X Y Z} {f : Z ⇒ X} → bot {X} {Y} ∘ f ≈ bot {Z} {Y}
  bot-absorbs {X} {Y} {Z} {f} = begin 
    bot {X} {Y} ∘ f ≈⟨ bot∘! ⟩∘⟨refl ⟩ 
    (bot ∘ !) ∘ f   ≈⟨ pullʳ (sym (!-unique (! ∘ f))) ⟩ 
    bot ∘ !         ≈˘⟨ bot∘! ⟩
    bot {Z} {Y}     ∎

  bot⊑f : ∀ {X} {Y} {f : X ⇒ K.₀ Y} → bot ⊑ f
  bot⊑f {X} {Y} {f} = sym (begin
    extend π₁ ∘ τ _ ∘ ⟨ f , i₂ # ⟩                                       ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩
    extend π₁ ∘ τ _ ∘ (id ×₁ i₂ #) ∘ ⟨ f , id ⟩                          ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm i₂)) ⟩
    extend π₁ ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂))# ∘ ⟨ f , id ⟩ ≈⟨ refl⟩∘⟨ ((#-resp-≈ (algebras (K.₀ Y × Y)) (refl⟩∘⟨ distributeˡ⁻¹-i₂)) ⟩∘⟨refl) ⟩
    extend π₁ ∘ ((τ _ +₁ id) ∘ i₂)# ∘ ⟨ f , id ⟩                         ≈⟨ refl⟩∘⟨ ((#-resp-≈ (algebras (K.₀ Y × Y)) ((inject₂ ○ identityʳ))) ⟩∘⟨refl) ⟩
    extend π₁ ∘ i₂ # ∘ ⟨ f , id ⟩                                        ≈⟨ pullˡ (extend-preserve π₁ i₂) ⟩
    ((extend π₁ +₁ id) ∘ i₂) # ∘ ⟨ f , id ⟩                              ≈⟨ (#-resp-≈ (algebras Y) (inject₂ ○ identityʳ)) ⟩∘⟨refl ⟩
    i₂ # ∘ ⟨ f , id ⟩                                                    ≈˘⟨ #-Uniformity (algebras Y) inject₂ ⟩
    i₂ #                                                                 ∎)

  -- strictness of strength
  τ-strict : ∀ {X Y Z} → τ (X , Y) ∘ (id ×₁ bot {Z} {Y}) ≈ bot
  τ-strict {X} {Y} {Z} = begin
    τ _ ∘ (id ×₁ i₂ #)                           ≈⟨ τ-comm i₂ ⟩
    ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ distributeˡ⁻¹-i₂) ⟩
    ((τ _ +₁ id) ∘ i₂) #                         ≈⟨ #-resp-≈ (algebras _) (inject₂ ○ identityʳ) ⟩
    (i₂ #)                                       ∎

  -- monotonicity of strength
  τ-monotonicity : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ⊑ g → (τ (X , Y) ∘ ⟨ id , f ⟩) ⊑ (τ (X , Y) ∘ ⟨ id , g ⟩)
  τ-monotonicity {f = f} {g} f⊑g = begin
    τ _ ∘ ⟨ id , f ⟩                                                             ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (f⊑g ○ restrict-law g f)) ⟩
    τ _ ∘ ⟨ id , extend g ∘ f ↓ ⟩                                                ≈˘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩
    τ _ ∘ (id ×₁ extend g) ∘ ⟨ id , f ↓ ⟩                                        ≈⟨ pullˡ (sym (τ-extendʳ g)) ○ assoc ⟩
    extend (τ _ ∘ (id ×₁ g)) ∘ τ _ ∘ ⟨ id , K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩ ⟩          ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩
    extend (τ _ ∘ (id ×₁ g)) ∘ τ _ ∘ (id ×₁ K.₁ π₁) ∘ ⟨ id , τ _ ∘ ⟨ id , f ⟩ ⟩  ≈⟨ refl⟩∘⟨ (extendʳ (strengthen.commute (id , π₁))) ⟩
    extend (τ _ ∘ (id ×₁ g)) ∘ K.₁ (id ×₁ π₁) ∘  τ _ ∘ ⟨ id , τ _ ∘ ⟨ id , f ⟩ ⟩ ≈⟨ pullˡ (extend∘F₁ monadK _ _ ○ extend-≈ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² refl))) ⟩
    extend (τ _ ∘ (id ×₁ g ∘ π₁)) ∘ τ _ ∘ ⟨ id , τ _ ∘ ⟨ id , f ⟩ ⟩              ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩
    extend (τ _ ∘ (id ×₁ g ∘ π₁)) ∘ τ _ ∘ (id ×₁ τ _) ∘ ⟨ id , ⟨ id , f ⟩ ⟩      ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟩
    extend (τ _ ∘ (id ×₁ g ∘ π₁)) ∘ τ _ ∘ (id ×₁ τ _) ∘ assocˡ ∘ ⟨ Δ , f ⟩       ≈⟨ refl⟩∘⟨ (sym-assoc ○ pullˡ (assoc ○ sym strength-assoc)) ⟩
    extend (τ _ ∘ (id ×₁ g ∘ π₁)) ∘ (K.₁ assocˡ ∘ τ _) ∘ ⟨ Δ , f ⟩               ≈⟨ pullˡ (pullˡ (extend∘F₁ monadK _ _)) ⟩
    (extend ((τ _ ∘ (id ×₁ g ∘ π₁)) ∘ assocˡ) ∘ τ _) ∘ ⟨ Δ , f ⟩                 ≈⟨ (extend-≈ (pullʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁ ○ identityˡ) (pullʳ project₂ ○ pullʳ project₁))) ⟩∘⟨refl) ⟩∘⟨refl ⟩
    (extend (τ _ ∘ ⟨ π₁ ∘ π₁ , g ∘ π₂ ∘ π₁ ⟩) ∘ τ _) ∘ ⟨ Δ , f ⟩                 ≈˘⟨ ((extend-≈ (∘-resp-≈ʳ (⟨⟩∘ ○ ⟨⟩-cong₂ (∘-resp-≈ˡ identityˡ) assoc))) ⟩∘⟨refl) ⟩∘⟨refl ⟩
    (extend (τ _ ∘ (id ×₁ g) ∘ π₁) ∘ τ _) ∘ ⟨ Δ , f ⟩                            ≈˘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
    (extend (τ _ ∘ (id ×₁ g) ∘ π₁) ∘ τ _) ∘ (Δ ×₁ id) ∘ ⟨ id , f ⟩               ≈⟨ pullʳ (extendʳ (τ-comm-id Δ)) ⟩
    extend (τ _ ∘ (id ×₁ g) ∘ π₁) ∘ K.₁ (Δ ×₁ id) ∘ τ _ ∘ ⟨ id , f ⟩             ≈⟨ pullˡ (extend∘F₁ monadK _ _ ○ extend-≈ (pullʳ (pullʳ project₁ ○ pullˡ ×₁∘Δ))) ⟩
    extend (τ _ ∘ ⟨ id , g ⟩ ∘ π₁) ∘ τ _ ∘ ⟨ id , f ⟩                            ≈˘⟨ pullˡ (extend∘F₁ monadK _ _ ○ extend-≈ assoc) ⟩
    extend (τ _ ∘ ⟨ id , g ⟩) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ id , f ⟩                        ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ project₁ identityˡ) ⟩
    extend (τ _ ∘ ⟨ id , g ⟩) ∘ K.₁ π₁ ∘ τ _ ∘ (π₁ ×₁ id) ∘ ⟨ Δ , f ⟩            ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (τ-comm-id π₁) ⟩
    extend (τ _ ∘ ⟨ id , g ⟩) ∘ K.₁ π₁ ∘ K.₁ (π₁ ×₁ id) ∘ τ _ ∘ ⟨ Δ , f ⟩        ≈⟨ refl⟩∘⟨ pullˡ (sym monadK.F.homomorphism ○ monadK.F.F-resp-≈ project₁) ⟩
    extend (τ _ ∘ ⟨ id , g ⟩) ∘ K.₁ (π₁ ∘ π₁) ∘ τ _ ∘ ⟨ Δ , f ⟩                  ≈˘⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym monadK.F.homomorphism ○ monadK.F.F-resp-≈ project₁)) ○ assoc) ⟩
    extend (τ _ ∘ ⟨ id , g ⟩) ∘ K.₁ π₁ ∘ (K.₁ assocˡ ∘ τ _) ∘ ⟨ Δ , f ⟩          ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○ pullˡ (assoc ○ sym strength-assoc)) ⟩
    extend (τ _ ∘ ⟨ id , g ⟩) ∘ K.₁ π₁ ∘ τ _ ∘ (id ×₁ τ _) ∘ assocˡ ∘ ⟨ Δ , f ⟩  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⟨⟩ ⟩
    extend (τ _ ∘ ⟨ id , g ⟩) ∘ K.₁ π₁ ∘ τ _ ∘ (id ×₁ τ _) ∘ ⟨ id , ⟨ id , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩
    extend (τ _ ∘ ⟨ id , g ⟩) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ id , τ _ ∘ ⟨ id , f ⟩ ⟩         ≈˘⟨ restrict-law _ _ ⟩
    ((τ _ ∘ ⟨ id , g ⟩) ⇂ (τ _ ∘ ⟨ id , f ⟩))                                    ∎

  -- right strictness of composition
  ∘-right-strict : ∀ {X Y Z} (f : X ⇒ K.₀ Y) → extend f ∘ bot {Z} {X} ≈ bot
  ∘-right-strict f = begin
    extend f ∘ bot            ≈⟨ extend-preserve f i₂ ⟩
    ((extend f +₁ id) ∘ i₂) # ≈⟨ #-resp-≈ (algebras _) (inject₂ ○ identityʳ) ⟩
    bot                       ∎

  bot-restrict : ∀ {X Y Z} (f : X ⇒ K.₀ Y) → f ⇂ (bot {X} {Z}) ≈ bot
  bot-restrict f = begin
    extend π₁ ∘ τ _ ∘ ⟨ f , bot ⟩              ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩
    extend π₁ ∘ τ _ ∘ (id ×₁ bot) ∘ ⟨ f , id ⟩ ≈⟨ refl⟩∘⟨ (pullˡ τ-strict) ⟩
    extend π₁ ∘ bot ∘ ⟨ f , id ⟩               ≈⟨ pullˡ (∘-right-strict π₁) ⟩
    bot ∘ ⟨ f , id ⟩                           ≈˘⟨ #-Uniformity (algebras _) inject₂ ⟩
    bot                                        ∎

  -- bottom element is iteration preserving
  bot-preserves : ∀ {X Y Z} {f : X ⇒ K.₀ Y + X} → bot {K.₀ Y} {Z} ∘ f # ≈ ((bot +₁ id) ∘ f)#
  bot-preserves {f = f} = begin 
    bot ∘ f # ≈⟨ bot-absorbs ⟩ 
    bot 
      ≈⟨ ⊑-antisym bot⊑f helper ⟩
    extend bot ∘ ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f))# ∘ Δ
      ≈⟨ pullˡ (extend-preserve bot ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) ○ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²))) ⟩
    ((extend bot ∘ η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f))# ∘ Δ 
      ≈⟨ (#-resp-≈ (algebras _) (∘-resp-≈ˡ (+₁-cong₂ (pullˡ kleisliK.identityʳ ○ bot-absorbs) refl))) ⟩∘⟨refl ⟩
        ((bot +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f))# ∘ Δ ≈⟨ pushˡ (#-Uniformity (algebras _) (begin
          (id +₁ π₂) ∘ (bot +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f) ≈⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ (identityˡ ○ sym bot-absorbs) id-comm ○ sym +₁∘+₁) ⟩
          (bot +₁ id) ∘ (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (id ×₁ f) ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹-π₂  ) ⟩
          (bot +₁ id) ∘ π₂ ∘ (id ×₁ f)                         ≈⟨ ∘-resp-≈ʳ project₂ ○ sym-assoc ⟩
          ((bot +₁ id) ∘ f) ∘ π₂                               ∎)) ⟩
    ((bot +₁ id) ∘ f)# ∘ π₂ ∘ Δ 
      ≈⟨  elimʳ project₂  ⟩
    ((bot +₁ id) ∘ f)# 
      ∎
    where
      ηπ₁-strict : ∀ {X Y Z} (f : Z ⇒ Y + Z) → ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f))# ⊑ (η X ∘ π₁)
      ηπ₁-strict f = begin
        ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) #                                                                  ≈⟨ introʳ (×₁∘Δ ○ ×₁-η) ⟩
        ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) # ∘ (π₁ ×₁ π₂) ∘ Δ                                                 ≈˘⟨ pushˡ (#-Uniformity (algebras _) by-uniformity) ⟩
        ((η _ ∘ π₁ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f)))# ∘ Δ                                  ≈˘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (extendʳ (K₁η (π₁ ∘ π₁)) ○ ∘-resp-≈ʳ (pullʳ (project₁ ○ identityˡ))) refl) ⟩∘⟨refl)) ⟩∘⟨refl ⟩
        ((K.₁ (π₁ ∘ π₁) ∘ η _ ∘ (id ×₁ π₁) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f)))# ∘ Δ               ≈˘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (refl⟩∘⟨ (∘-resp-≈ʳ ( sym (×₁∘×₁ ○ ×₁-cong₂ identity² refl)) ○ pullˡ (τ-η (A×B , _)))) refl) ⟩∘⟨refl)) ⟩∘⟨refl ⟩
        ((K.₁ (π₁ ∘ π₁) ∘ τ _ ∘ (id ×₁ η _ ∘ π₁) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f)))# ∘ Δ         ≈˘⟨ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identity² ))) ⟩∘⟨refl ⟩
        ((K.₁ (π₁ ∘ π₁) ∘ τ _ +₁ id) ∘ ((id ×₁ η _ ∘ π₁) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f)))# ∘ Δ ≈˘⟨ (#-resp-≈ (algebras _) (refl⟩∘⟨ (extendʳ (sym (distributeˡ⁻¹-natural _ _ _) ○ ∘-resp-≈ˡ (+₁-cong₂ refl (⟨⟩-unique id-comm id-comm)))))) ⟩∘⟨refl ⟩
        ((K.₁ (π₁ ∘ π₁) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ (η _ ∘ π₁ +₁ id)) ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f)))# ∘ Δ ≈⟨ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identity² refl)))) ⟩∘⟨refl ⟩
        ((K.₁ (π₁ ∘ π₁) ∘ τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ (η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)))# ∘ Δ         ≈˘⟨ pullˡ (K-preserve _ _ ○ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²))) ⟩
        K.₁ (π₁ ∘ π₁) ∘ ((τ _ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ (η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)))# ∘ Δ         ≈˘⟨ refl⟩∘⟨ (pullˡ (τ-comm _)) ⟩
        K.₁ (π₁ ∘ π₁) ∘ τ _ ∘ (id ×₁ ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) #) ∘ Δ                                ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘Δ ⟩
        K.₁ (π₁ ∘ π₁) ∘ τ _ ∘ ⟨ id , ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) # ⟩                                   ≈˘⟨ pullˡ (extend∘F₁ monadK π₁ _ ○ ∘-resp-≈ʳ (monadK.F.F-resp-≈ (project₁ ○ assoc)) ○ F₁⇒extend monadK (π₁ ∘ π₁)) ⟩
        extend π₁ ∘ K.₁ (η _ ∘ π₁ ×₁ id) ∘ τ _ ∘ ⟨ id , ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) # ⟩                ≈˘⟨ refl⟩∘⟨ (extendʳ (τ-comm-id (η _ ∘ π₁))) ⟩
        extend π₁ ∘ τ _ ∘ (η _ ∘ π₁ ×₁ id) ∘ ⟨ id , ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) # ⟩                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
        extend π₁ ∘ τ _ ∘ ⟨ η _ ∘ π₁ , ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) # ⟩                                 ∎
        where
          by-uniformity : (id +₁ π₁ ×₁ π₂) ∘ (η _ ∘ π₁ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f))
            ≈ ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) ∘ (π₁ ×₁ π₂)
          by-uniformity = begin
            (id +₁ π₁ ×₁ π₂) ∘ (η _ ∘ π₁ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f))  ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ (identityˡ ○ ∘-resp-≈ʳ (sym project₁)) identityʳ) ⟩
            (η _ ∘ π₁ ∘ (π₁ ×₁ π₂) +₁ π₁ ×₁ π₂) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f))       ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityˡ) ⟩
            (η _ ∘ π₁ +₁ id) ∘ (π₁ ×₁ π₂ +₁ π₁ ×₁ π₂) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f)) ≈⟨ refl⟩∘⟨ extendʳ (distributeˡ⁻¹-natural π₁ π₂ π₂) ⟩
            (η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (π₁ ×₁ (π₂ +₁ π₂)) ∘ (id ×₁ distributeˡ⁻¹ ∘ (id ×₁ f))     ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identityʳ refl) ⟩
            (η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (π₁ ×₁ (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (id ×₁ f))             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-cong₂ refl (pullˡ distributeˡ⁻¹-π₂ ○ project₂) ⟩
            (η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (π₁ ×₁ f ∘ π₂)                                             ≈˘⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identityˡ refl)) ⟩
            ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) ∘ (π₁ ×₁ π₂)                                   ∎
      helper : (extend bot ∘ ((η _ ∘ π₁ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ f)) # ∘ Δ) ⊑ bot
      helper =  ⊑-cong₂ refl (begin
        extend bot ∘ (η _ ∘ π₁) ∘ Δ ≈⟨ pullˡ (pullˡ kleisliK.identityʳ) ○ cancelʳ project₁ ⟩
        bot ∎) (⊑∘ʳ (⊑∘ˡ (ηπ₁-strict f)))

  -- strictness of extend
  extend-strict : ∀ {X Y : Obj} → bot {K.₀ X} {Y} ≈ extend bot
  extend-strict {X} {Y} = begin
    bot 
      ≈⟨ FreeObject.*-uniq (freealgebras X) bot (record { h = bot ; preserves = bot-preserves }) bot-absorbs ⟩
    Elgot-Algebra-Morphism.h (((freealgebras X) FreeObject.*) bot) 
      ≈⟨ sym (FreeObject.*-uniq (freealgebras X) {algebras Y} bot (record { h = extend bot ; preserves = extend-preserve bot _ }) kleisliK.identityʳ) ⟩
    extend bot
      ∎

  -- left strictness of composition
  ∘-left-strict : ∀ {X Y Z} (f : X ⇒ K.₀ Y) → extend (bot {Y} {Z}) ∘ f ≈ bot
  ∘-left-strict f =  begin
    extend bot ∘ f ≈˘⟨ extend-strict ⟩∘⟨refl ⟩
    bot ∘ f        ≈⟨ bot-absorbs ⟩
    bot            ∎

  bot∘!-id : bot {⊤} {⊥} ∘ ! {K.₀ ⊥} ≈ id
  bot∘!-id = begin 
    bot ∘ !             ≈⟨ bot-absorbs ⟩
    bot                 ≈˘⟨ ∘-left-strict id ⟩
    extend bot ∘ id     ≈⟨ identityʳ ⟩
    μ.η _ ∘ (K.₁ bot)   ≈⟨ refl⟩∘⟨ K.F-resp-≈ (¡-unique₂ bot (η _)) ⟩
    μ.η _ ∘ (K.₁ (η ⊥)) ≈⟨ monadK.identityˡ ⟩
    id                  ∎

  K⊥⊤ : K.₀ ⊥ ≅ ⊤
  K⊥⊤ = record { from = ! ; to = bot ; iso = record { isoˡ = bot∘!-id ; isoʳ = !-unique₂ } }