------------------------------------------------------------------------
-- Up-to techniques, compatibility, size-preserving functions, and the
-- companion
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

-- The definitions below are parametrised by an indexed container.

open import Indexed-container

module Up-to {ℓ} {I : Set ℓ} (C : Container I I) where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J as F hiding (id; _∘_)

open import Indexed-container.Combinators
  hiding (id; const) renaming (_∘_ to _⊚_)
open import Relation

------------------------------------------------------------------------
-- Up-to techniques

-- This definition of soundness is based on the definition of
-- "b-soundness" given by Pous and Sangiorgi in "Enhancements of the
-- bisimulation proof method", with the following differences:
--
-- * The property is stated for an indexed container rather than a
--   monotone function on a (particular) complete lattice.
--
-- * The extension ⟦ C ⟧ of the container C takes the place of b.
--
-- * The type-theoretic greatest fixpoint ν takes the place of a
--   set-theoretic greatest fixpoint.

Sound : Container I I → Set ℓ
Sound F = ν (C ⊚ F) ∞ ⊆ ν C ∞

-- A relation transformer F is a (sound) up-to technique if every
-- relation R that is contained in ⟦ C ⟧ (F R) is contained in ν C ∞.

Up-to-technique : Trans ℓ I → Set (lsuc ℓ)
Up-to-technique F = ∀ {R} → R ⊆ ⟦ C ⟧ (F R) → R ⊆ ν C ∞

-- The two definitions above are pointwise logically equivalent, if
-- the second one is restricted to containers (in a certain way).

Sound⇔ : ∀ F → Sound F ⇔ Up-to-technique ⟦ F ⟧
Sound⇔ F = record
  { to = λ sound {R} →

      R ⊆ ⟦ C ⟧ (⟦ F ⟧ R)  ↝⟨ ⊆-congʳ _ (_⇔_.from $ ⟦∘⟧↔ _ C) ⟩

      R ⊆ ⟦ C ⊚ F ⟧ R      ↝⟨ unfold (C ⊚ F) ⟩

      R ⊆ ν (C ⊚ F) ∞      ↝⟨ ⊆-congʳ _ sound ⟩□

      R ⊆ ν C ∞            □

  ; from = λ up-to → up-to (

      ν (C ⊚ F) ∞                  ⊆⟨ ν-out _ ⟩

      ⟦ C ⊚ F ⟧ (ν (C ⊚ F) ∞)      ⊆⟨ ⟦∘⟧↔ _ C ⟩∎

      ⟦ C ⟧ (⟦ F ⟧ (ν (C ⊚ F) ∞))  ∎)

  }

------------------------------------------------------------------------
-- Compatibility

-- Compatibility.
--
-- This definition corresponds to Pous and Sangiorgi's definition of
-- b-compatibility.

Compatible : Trans ℓ I → Set (lsuc ℓ)
Compatible F = ∀ {R} → F (⟦ C ⟧ R) ⊆ ⟦ C ⟧ (F R)

-- If F is monotone and compatible, and R is contained in ⟦ C ⟧ (F R),
-- then F ^ω R is a post-fixpoint of ⟦ C ⟧.
--
-- The proof of Pous and Sangiorgi's Theorem 6.3.9 contains a similar
-- result.

compatible→^ω-post-fixpoint :
  ∀ {F} →
  Monotone F → Compatible F →
  ∀ {R} → R ⊆ ⟦ C ⟧ (F R) → F ^ω R ⊆ ⟦ C ⟧ (F ^ω R)
compatible→^ω-post-fixpoint {F} mono comp {R = R} R⊆ = uncurry λ n →
  F ^[ n ] R              ⊆⟨ Fⁿ⊆∘F¹⁺ⁿ n ⟩
  ⟦ C ⟧ (F ^[  + n ] R)  ⊆⟨ map C ( + n ,_) ⟩∎
  ⟦ C ⟧ (F ^ω R)          ∎
  where
  Fⁿ⊆∘F¹⁺ⁿ : ∀ n → F ^[ n ] R ⊆ ⟦ C ⟧ (F ^[ suc n ] R)
  Fⁿ⊆∘F¹⁺ⁿ zero =
    R            ⊆⟨ R⊆ ⟩∎
    ⟦ C ⟧ (F R)  ∎
  Fⁿ⊆∘F¹⁺ⁿ (suc n) =
    F ^[  + n ] R              ⊆⟨⟩
    F (F ^[ n ] R)              ⊆⟨ mono (Fⁿ⊆∘F¹⁺ⁿ n) ⟩
    F (⟦ C ⟧ (F ^[  + n ] R))  ⊆⟨ comp ⟩∎
    ⟦ C ⟧ (F ^[  + n ] R)      ∎

-- Monotone compatible functions are up-to techniques.
--
-- This is basically Pous and Sangiorgi's Theorem 6.3.9.

monotone→compatible→up-to :
  ∀ {F} → Monotone F → Compatible F → Up-to-technique F
monotone→compatible→up-to {F} mono comp {R = R} R⊆ =
  R       ⊆⟨  ,_ ⟩
  F ^ω R  ⊆⟨ unfold C (compatible→^ω-post-fixpoint mono comp R⊆) ⟩∎
  ν C ∞   ∎

------------------------------------------------------------------------
-- Size-preserving functions (using sized types)

-- F is size-preserving if, for any relation R, if R is contained in
-- ν C i, then F R is contained in ν C i.

Size-preserving : Trans ℓ I → Set (lsuc ℓ)
Size-preserving F = ∀ {R i} → R ⊆ ν C i → F R ⊆ ν C i

-- If a transformer is size-preserving, then it satisfies the
-- corresponding property for ν′, and vice versa.
--
-- Note that this proof uses the size successor function.

size-preserving⇔size-preserving′ :
  ∀ {F} → Size-preserving F ⇔ (∀ {R i} → R ⊆ ν′ C i → F R ⊆ ν′ C i)
force (_⇔_.to size-preserving⇔size-preserving′ pres R⊆ν′Ci x) =
  pres (λ y → force (R⊆ν′Ci y)) x
_⇔_.from size-preserving⇔size-preserving′ pres′ {i = i} R⊆ν′Ci x =
  force (pres′ {i = ssuc i} (λ x → λ { .force → R⊆ν′Ci x }) x)

-- If the relation transformer F is size-preserving, then F is an
-- up-to technique.
--
-- On the other hand, up-to techniques are not necessarily
-- size-preserving, not even for monotone and extensive transformers,
-- see
-- Bisimilarity.Up-to.Counterexamples.∃monotone×extensive×up-to׬size-preserving.
-- Thus the property of being size-preserving is less general than
-- that of being an up-to technique. However, the latter property is
-- not closed under composition (not even for monotone and extensive
-- transformers, see Bisimilarity.Up-to.Counterexamples.¬-∘-closure),
-- whereas the former property is (see ∘-closure below).

size-preserving→up-to : ∀ {F} → Size-preserving F → Up-to-technique F
size-preserving→up-to {F} pres {R = R} R⊆CFR = helper
  where
  helper : ∀ {i} → R ⊆ ⟦ C ⟧ (ν′ C i)
  helper =
    map C (_⇔_.to size-preserving⇔size-preserving′
             pres (λ x → λ { .force → helper x })) ∘
    R⊆CFR

  -- An alternative implementation of helper which might be a bit
  -- easier to follow.

  helper′ : ∀ {i} → R ⊆ ν C i
  helper′ {i} =
    R               ⊆⟨ R⊆CFR ⟩
    ⟦ C ⟧ (F R)     ⊆⟨ map C (_⇔_.to size-preserving⇔size-preserving′
                                pres (λ x → λ { .force → helper′ x })) ⟩
    ⟦ C ⟧ (ν′ C i)  ⊆⟨ id ⟩∎
    ν C i           ∎

-- If F is monotone, then Size-preserving F is logically equivalent to
-- a special case stating that, for any size i, ν C i should be a
-- pre-fixpoint of F.
--
-- Note that size-preserving relation transformers are not necessarily
-- monotone (or extensive), see
-- Bisimilarity.Up-to.Counterexamples.∃size-preserving׬[monotone⊎extensive].
--
-- Furthermore there is a container C such that transformers F that
-- satisfy the property ∀ {i} → F (ν C i) ⊆ ν C i are not necessarily
-- up-to techniques for C, see
-- Bisimilarity.Up-to.Counterexamples.∃special-case-of-size-preserving׬up-to.

monotone→⇔ :
  ∀ {F} →
  Monotone F →
  Size-preserving F ⇔ (∀ {i} → F (ν C i) ⊆ ν C i)
monotone→⇔ mono = record
  { to   = λ pres       → pres id
  ; from = λ pres R⊆νCi → pres ∘ mono R⊆νCi
  }

-- A special case of compatibility.

Compatible′ : Trans ℓ I → Set ℓ
Compatible′ F = ∀ {i} → F (⟦ C ⟧ (ν′ C i)) ⊆ ⟦ C ⟧ (F (ν′ C i))

-- Monotone transformers that satisfy the special case of
-- compatibility are size-preserving.

monotone→compatible′→size-preserving :
  ∀ {F} → Monotone F → Compatible′ F → Size-preserving F
monotone→compatible′→size-preserving {F = F} mono comp =
  _⇔_.from (monotone→⇔ mono) helper
  where

  mutual

    helper : ∀ {i} → F (⟦ C ⟧ (ν′ C i)) ⊆ ⟦ C ⟧ (ν′ C i)
    helper = map C helper′ ∘ comp

    helper′ : ∀ {i} → F (ν′ C i) ⊆ ν′ C i
    force (helper′ x) = helper (mono (λ y → force y) x)

  -- A variant of helper that is perhaps a bit easier to follow.

  helper″ : ∀ {i} → F (ν C i) ⊆ ν C i
  helper″ {i} =
    F (ν C i)           ⊆⟨⟩
    F (⟦ C ⟧ (ν′ C i))  ⊆⟨ comp ⟩
    ⟦ C ⟧ (F (ν′ C i))  ⊆⟨ map C helper′ ⟩
    ⟦ C ⟧ (ν′ C i)      ⊆⟨ id ⟩∎
    ν C i               ∎

  -- This definition is definitionally equal to helper.

  helper″≡helper : (λ {i x} → helper″ {i = i} {x = x}) ≡ helper
  helper″≡helper = refl

-- Monotone, compatible transformers are size-preserving.

monotone→compatible→size-preserving :
  ∀ {F} → Monotone F → Compatible F → Size-preserving F
monotone→compatible→size-preserving mono comp =
  monotone→compatible′→size-preserving mono comp

-- Extensive, size-preserving transformers satisfy the special case of
-- compatibility.

extensive→size-preserving→compatible′ :
  ∀ {F} →
  Extensive F → Size-preserving F → Compatible′ F
extensive→size-preserving→compatible′ {F} extensive pres {i} =
  F (⟦ C ⟧ (ν′ C i))  ⊆⟨⟩
  F (ν C i)           ⊆⟨ pres id ⟩
  ν C i               ⊆⟨⟩
  ⟦ C ⟧ (ν′ C i)      ⊆⟨ map C (extensive _) ⟩∎
  ⟦ C ⟧ (F (ν′ C i))  ∎

-- For monotone and extensive transformers the special case of
-- compatibility is logically equivalent to being size-preserving.
--
-- However, size-preserving transformers are not necessarily
-- compatible, not even if they are monotone and extensive, see
-- Bisimilarity.Up-to.Counterexamples.∃monotone×extensive×size-preserving׬compatible.
-- Thus the property of being size-preserving is more general than the
-- property of being compatible. However, it is more well-behaved than
-- Up-to-technique, because it is closed under composition (see
-- ∘-closure below).

monotone→extensive→size-preserving⇔compatible′ :
  ∀ {F} →
  Monotone F → Extensive F →
  Size-preserving F ⇔ Compatible′ F
monotone→extensive→size-preserving⇔compatible′ mono extensive = record
  { to   = extensive→size-preserving→compatible′ extensive
  ; from = monotone→compatible′→size-preserving mono
  }

-- The following four lemmas correspond to Pous and Sangiorgi's
-- Proposition 6.3.11.

-- The identity function is size-preserving.

id-size-preserving :
  Size-preserving id
id-size-preserving = id

-- If R is contained in ν C ∞, then const R is size-preserving.

const-size-preserving :
  {R : Rel ℓ I} →
  R ⊆ ν C ∞ →
  Size-preserving (const R)
const-size-preserving R⊆∼ _ = R⊆∼

-- If F and G are both size-preserving, then F ∘ G is also
-- size-preserving.

∘-closure :
  ∀ {F G} →
  Size-preserving F → Size-preserving G → Size-preserving (F ∘ G)
∘-closure F-pres G-pres = F-pres ∘ G-pres

private

  -- An alternative implementation of ∘-closure which might be a bit
  -- easier to follow.

  ∘-closure′ :
    ∀ {F G} →
    Size-preserving F → Size-preserving G → Size-preserving (F ∘ G)
  ∘-closure′ {F} {G} F-pres G-pres {R = R} {i = i} =
   R ⊆ ν C i        ↝⟨ G-pres ⟩
   G R ⊆ ν C i      ↝⟨ F-pres ⟩□
   F (G R) ⊆ ν C i  □

-- If F is a family of size-preserving transformers, then ⋃ lzero F is
-- also size-preserving.

⋃-closure :
  {A : Set ℓ} {F : A → Trans ℓ I} →
  (∀ a → Size-preserving (F a)) →
  Size-preserving (⋃ lzero F)
⋃-closure {F = F} pres {R = R} {i = i} =
  R ⊆ ν C i                        ↝⟨ (λ R⊆∼ {_} → uncurry λ a →

      F a R                              ⊆⟨ pres a (λ {_} → R⊆∼ {_}) ⟩∎
      ν C i                              ∎) ⟩□

  (λ b → ∃ λ a → F a R b) ⊆ ν C i  □

-- If F and G are both size-preserving, then
-- λ R → F R ∪ G R is also size-preserving.

∪-closure :
  {F G : Trans ℓ I} →
  Size-preserving F →
  Size-preserving G →
  Size-preserving (λ R → F R ∪ G R)
∪-closure {F} {G} F-pres G-pres {R = R} {i = i} =
  R ⊆ ν C i          ↝⟨ (λ R⊆∼ {_} → [ F-pres (R⊆∼ {_}) , G-pres (R⊆∼ {_}) ]) ⟩□
  F R ∪ G R ⊆ ν C i  □

------------------------------------------------------------------------
-- The companion

-- The companion.
--
-- The name comes from "Coinduction All the Way Up" by Pous, but this
-- definition is based on the one presented by Parrow and Weber in
-- "The Largest Respectful Function".

Companion : Trans ℓ I
Companion R x = ∀ {i} → R ⊆ ν C i → ν C i x

-- Another conservative approximation of "up-to technique": being
-- below the companion. This notion was presented by Pous in
-- "Coinduction All the Way Up".

Below-the-companion : Trans ℓ I → Set (lsuc ℓ)
Below-the-companion F = ∀ {R} → F R ⊆ Companion R

-- A transformer is below the companion iff it is size-preserving.
--
-- This is a generalisation of the following result, which is based on
-- a proposition due to Pous and Rot.

below-the-companion⇔size-preserving :
  ∀ {F} → Below-the-companion F ⇔ Size-preserving F
below-the-companion⇔size-preserving {F} = record
  { to   = λ below R⊆νCi x → below x R⊆νCi
  ; from = λ pres x R⊆νCi  → pres R⊆νCi x
  }

-- A monotone transformer F is below the companion iff, for all
-- sizes i, ν C i is a pre-fixpoint of F.
--
-- This corresponds roughly to Proposition 5.2 in "Companions,
-- Codensity and Causality" by Pous and Rot.

monotone→below-the-companion⇔size-preserving :
  ∀ {F} →
  Monotone F →
  Below-the-companion F ⇔ (∀ {i} → F (ν C i) ⊆ ν C i)
monotone→below-the-companion⇔size-preserving {F} mono =
  Below-the-companion F        ↝⟨ below-the-companion⇔size-preserving ⟩
  Size-preserving F            ↝⟨ monotone→⇔ mono ⟩□
  (∀ {i} → F (ν C i) ⊆ ν C i)  □

-- The companion is size-preserving.

companion-size-preserving : Size-preserving Companion
companion-size-preserving =
  _⇔_.to below-the-companion⇔size-preserving id

-- The companion is monotone.
--
-- This result corresponds to Lemma 2.13 in "The Largest Respectful
-- Function".

companion-monotone : Monotone Companion
companion-monotone R⊆S f S⊆νCi = f (S⊆νCi ∘ R⊆S)

-- A preservation lemma.

companion-cong :
  ∀ {k R S} →
  Extensionality? ⌊ k ⌋-sym ℓ ℓ →
  (∀ {x} → R x ↝[ ⌊ k ⌋-sym ] S x) →
  (∀ {x} → Companion R x ↝[ ⌊ k ⌋-sym ] Companion S x)
companion-cong {k} {R} {S} ext R↝S {x} =
  (∀ {i} → R ⊆ ν C i → ν C i x)  ↝⟨ implicit-∀-cong (lower-extensionality? ⌊ k ⌋-sym _ lzero ext) (→-cong ext (⊆-cong ext R↝S F.id) F.id) ⟩□
  (∀ {i} → S ⊆ ν C i → ν C i x)  □

-- The companion is an up-to technique.

companion-up-to : Up-to-technique Companion
companion-up-to = size-preserving→up-to companion-size-preserving

-- The following four lemmas correspond to parts of Lemma 3.2 from
-- "Coinduction All the Way Up".

-- The identity function is below the companion.

id-below : Below-the-companion id
id-below x f = f x

private

  -- An alternative implementation that might be a bit easier to
  -- follow.

  id-below′ : Below-the-companion id
  id-below′ {R = R} {x = x} Rx {i} =
    R ⊆ ν C i  ↝⟨ (λ f → f Rx) ⟩□
    ν C i x    □

-- ⟦ C ⟧ is below the companion.

⟦⟧-below : Below-the-companion ⟦ C ⟧
⟦⟧-below x = ν-in C ∘ (λ f → f x) ∘ map C

private

  -- An alternative implementation that might be a bit easier to
  -- follow.

  ⟦⟧-below′ : Below-the-companion ⟦ C ⟧
  ⟦⟧-below′ {R = R} {x = x} CR {i} =
    R ⊆ ν C i                ↝⟨ map C ⟩
    ⟦ C ⟧ R ⊆ ⟦ C ⟧ (ν C i)  ↝⟨ (λ f → f CR) ⟩
    ⟦ C ⟧ (ν C i) x          ↝⟨ ν-in C ⟩□
    ν C i x                  □

-- The companion composed with itself is below the companion.

companion∘companion-below : Below-the-companion (Companion ∘ Companion)
companion∘companion-below =
  _⇔_.from below-the-companion⇔size-preserving
    (∘-closure companion-size-preserving companion-size-preserving)

-- The companion is idempotent (in a certain sense).

companion-idempotent :
  ∀ R {x} → Companion (Companion R) x ⇔ Companion R x
companion-idempotent R = record
  { to   = companion∘companion-below
  ; from = Companion R              ⊆⟨ companion-monotone id-below ⟩∎
           Companion (Companion R)  ∎
  }

-- An example illustrating how some of the lemmas above can be used:
-- If F is below the companion, then ⟦ C ⟧ ∘ F is below
-- Companion ∘ Companion, which is below the companion.

below-the-companion-example :
  ∀ {F} → Below-the-companion F → Below-the-companion (⟦ C ⟧ ∘ F)
below-the-companion-example {F} =
  F Below Companion                          ↝⟨ ∘-cong₂ companion-monotone ⟦⟧-below ⟩
  (⟦ C ⟧ ∘ F) Below (Companion ∘ Companion)  ↝⟨ (λ below {_ _} → companion∘companion-below ∘ below {_}) ⟩□
  (⟦ C ⟧ ∘ F) Below Companion                □
  where
  _Below_ : Trans ℓ I → Trans ℓ I → Set (lsuc ℓ)
  F Below G = ∀ {R} → F R ⊆ G R

  ∘-cong₂ : ∀ {F₁ F₂ G₁ G₂ : Trans ℓ I} →
            Monotone F₂ →
            F₁ Below F₂ → G₁ Below G₂ → (F₁ ∘ G₁) Below (F₂ ∘ G₂)
  ∘-cong₂ {F₁} {F₂} {G₁} {G₂} F₂-mono F₁⊆F₂ G₁⊆G₂ {R} =
    F₁ (G₁ R)  ⊆⟨ F₁⊆F₂ ⟩
    F₂ (G₁ R)  ⊆⟨ F₂-mono G₁⊆G₂ ⟩∎
    F₂ (G₂ R)  ∎

-- The greatest fixpoint ν C ∞ is pointwise logically equivalent to
-- the companion applied to an empty relation.
--
-- This corresponds to Theorem 3.3 from "Coinduction All the Way Up".

ν⇔companion-⊥ : ∀ {x} → ν C ∞ x ⇔ Companion (λ _ → ⊥) x
ν⇔companion-⊥ {x} = record
  { to   = λ x _ → x
  ; from = λ f → f (λ ())
  }

-- Every "partial" fixpoint ν C i is a pre-fixpoint of the companion.

companion-ν⊆ν : ∀ {i} → Companion (ν C i) ⊆ ν C i
companion-ν⊆ν {i} =
  (∀ {j} → ν C i ⊆ ν C j → ν C j _)  ↝⟨ (λ hyp → hyp id) ⟩□
  ν C i _                            □

-- Every "partial" fixpoint ν′ C i is a pre-fixpoint of the companion.

companion-ν′⊆ν′ : ∀ {i} → Companion (ν′ C i) ⊆ ν′ C i
force (companion-ν′⊆ν′ hyp) =
  companion-ν⊆ν (companion-monotone (λ x → force x) hyp)

-- The companion applied to the greatest fixpoint ν C ∞ is pointwise
-- logically equivalent to the greatest fixpoint.
--
-- This corresponds to Corollary 3.4 from "Coinduction All the Way
-- Up".

companion-ν⇔ν : ∀ {x} → Companion (ν C ∞) x ⇔ ν C ∞ x
companion-ν⇔ν {x} = record
  { to   = companion-ν⊆ν
  ; from = ν C ∞                ⊆⟨ _⇔_.to ν⇔companion-⊥ ⟩
           Companion (λ _ → ⊥)  ⊆⟨ companion-monotone (λ ()) ⟩∎
           Companion (ν C ∞)    ∎
  }

-- If "one half of f-symmetry" holds for R, for some involution f,
-- then the other half also holds.
--
-- (Pous mentions something similar in "Coinduction All the Way Up".)

other-half-of-symmetry :
  {f : I → I} →
  f ∘ f ≡ id →
  (R : Rel ℓ I) → R ∘ f ⊆ R → R ⊆ R ∘ f
other-half-of-symmetry {f} f-involution R R∘f⊆R =
  R          ⊆⟨ (λ {x} → subst (λ g → R (g x)) (sym f-involution)) ⟩
  R ∘ f ∘ f  ⊆⟨ R∘f⊆R ⟩∎
  R ∘ f      ∎

-- The results in the following module are based on Proposition 7.1 in
-- "Coinduction All the Way Up".

module _
  (D : Container I I)
  (f : I → I)
  (f-involution : f ∘ f ≡ id)
  (C⇔⟷D : ∀ {R : Rel ℓ I} {x} → ⟦ C ⟧ R x ⇔ ⟦ D ⊗ reindex f D ⟧ R x)
  where

  mutual

    ν-symmetric : ∀ {i} → ν C i ∘ f ⊆ ν C i
    ν-symmetric {i} =
      ν C i ∘ f                                          ⊆⟨⟩
      ⟦ C ⟧ (ν′ C i) ∘ f                                 ⊆⟨ _⇔_.to C⇔⟷D ⟩
      ⟦ D ⊗ reindex f D ⟧ (ν′ C i) ∘ f                   ⊆⟨ ⟦⊗⟧↔ _ D (reindex f D) ⟩
      ⟦ D ⟧ (ν′ C i) ∘ f ∩ ⟦ reindex f D ⟧ (ν′ C i) ∘ f  ⊆⟨ Σ-map id (⟦reindex⟧↔ _ D) ⟩
      ⟦ D ⟧ (ν′ C i) ∘ f ∩ ⟦ D ⟧ (ν′ C i ∘ f) ∘ f ∘ f    ⊆⟨ (λ {x} → Σ-map id (subst (λ g → ⟦ D ⟧ (ν′ C i ∘ f) (g x)) f-involution)) ⟩
      ⟦ D ⟧ (ν′ C i) ∘ f ∩ ⟦ D ⟧ (ν′ C i ∘ f)            ⊆⟨ Σ-map (map D (other-half-of-symmetry f-involution (ν′ C i) ν′-symmetric))
                                                                  (map D ν′-symmetric) ⟩
      ⟦ D ⟧ (ν′ C i ∘ f) ∘ f ∩ ⟦ D ⟧ (ν′ C i)            ⊆⟨ swap ⟩
      ⟦ D ⟧ (ν′ C i) ∩ ⟦ D ⟧ (ν′ C i ∘ f) ∘ f            ⊆⟨ Σ-map id (_⇔_.from (⟦reindex⟧↔ _ D)) ⟩
      ⟦ D ⟧ (ν′ C i) ∩ ⟦ reindex f D ⟧ (ν′ C i)          ⊆⟨ _⇔_.from (⟦⊗⟧↔ _ D (reindex f D)) ⟩
      ⟦ D ⊗ reindex f D ⟧ (ν′ C i)                       ⊆⟨ _⇔_.from C⇔⟷D ⟩
      ⟦ C ⟧ (ν′ C i)                                     ⊆⟨ id ⟩∎
      ν C i                                              ∎

    ν′-symmetric : ∀ {i} → ν′ C i ∘ f ⊆ ν′ C i
    force (ν′-symmetric x) = ν-symmetric (force x)

  companion-symmetric : ∀ {R} → Companion R ∘ f ⊆ Companion R
  companion-symmetric {R} {x} =
    Companion R (f x)                  ↔⟨⟩
    (∀ {i} → R ⊆ ν C i → ν C i (f x))  ↝⟨ (λ hyp {i} R⊆ν → ν-symmetric (hyp R⊆ν)) ⟩
    (∀ {i} → R ⊆ ν C i → ν C i x)      ↔⟨⟩
    Companion R x                      □

  symmetry-lemma :
    {R S : Rel ℓ I} →
    R ∘ f ⊆ R →
    R ⊆ ⟦ C ⟧ (Companion S) ⇔ R ⊆ ⟦ D ⟧ (Companion S)
  symmetry-lemma {R} {S} R-sym = record { to = to; from = from }
    where
    lemma = λ {x} →
      ⟦ C ⟧ (Companion S) x                                    ↝⟨ C⇔⟷D ⟩
      ⟦ D ⊗ reindex f D ⟧ (Companion S) x                      ↝⟨ ⟦⊗⟧↔ _ D (reindex f D) ⟩
      ⟦ D ⟧ (Companion S) x × ⟦ reindex f D ⟧ (Companion S) x  ↝⟨ ∃-cong (λ _ → ⟦reindex⟧↔ _ D) ⟩□
      ⟦ D ⟧ (Companion S) x × ⟦ D ⟧ (Companion S ∘ f) (f x)    □

    to : R ⊆ ⟦ C ⟧ (Companion S) → R ⊆ ⟦ D ⟧ (Companion S)
    to R⊆CCS =
      R                                                  ⊆⟨ R⊆CCS ⟩
      ⟦ C ⟧ (Companion S)                                ⊆⟨ _⇔_.to lemma ⟩
      ⟦ D ⟧ (Companion S) ∩ ⟦ D ⟧ (Companion S ∘ f) ∘ f  ⊆⟨ proj₁ ⟩∎
      ⟦ D ⟧ (Companion S)                                ∎

    from : R ⊆ ⟦ D ⟧ (Companion S) → R ⊆ ⟦ C ⟧ (Companion S)
    from R⊆DCS =
      R                                                  ⊆⟨ (λ x → x , x) ⟩
      R ∩ R                                              ⊆⟨ Σ-map id (other-half-of-symmetry f-involution R R-sym) ⟩
      R ∩ R ∘ f                                          ⊆⟨ Σ-map R⊆DCS R⊆DCS ⟩
      ⟦ D ⟧ (Companion S) ∩ ⟦ D ⟧ (Companion S) ∘ f      ⊆⟨ Σ-map id (map D (other-half-of-symmetry f-involution
                                                                               (Companion S) companion-symmetric)) ⟩
      ⟦ D ⟧ (Companion S) ∩ ⟦ D ⟧ (Companion S ∘ f) ∘ f  ⊆⟨ _⇔_.from lemma ⟩∎
      ⟦ C ⟧ (Companion S)                                ∎

-- Pous defines the companion in roughly the following way in
-- "Coinduction All the Way Up".
--
-- Note that this definition is large.

Companion₁ : Rel ℓ I → Rel (lsuc ℓ) I
Companion₁ R x = ∃ λ (F : Trans ℓ I) → Monotone F × Compatible F × F R x

-- Pous' variant of the companion is compatible (modulo size issues).
--
-- This corresponds to Lemma 3.2 from "Coinduction All the Way Up".

companion₁-compatible :
  ∀ R → Companion₁ (⟦ C ⟧ R) ⊆ ⟦ C ⟧ (Companion₁ R)
companion₁-compatible R {x} (F , mono , comp , FCR) =
                          $⟨ FCR ⟩
  F (⟦ C ⟧ R) x           ↝⟨ comp ⟩
  ⟦ C ⟧ (F R) x           ↝⟨ map C (λ FR → F , (λ {_ _} → mono) , (λ {_ _} → comp) , FR) ⟩□
  ⟦ C ⟧ (Companion₁ R) x  □

-- Pous' variant of the companion is monotone.

companion₁-monotone : ∀ {R S} → R ⊆ S → Companion₁ R ⊆ Companion₁ S
companion₁-monotone R⊆S =
  ∃-cong λ _ → ∃-cong λ mono → ∃-cong λ _ → mono R⊆S

-- Pous' variant of the companion is contained in Companion.

companion₁⊆companion : ∀ {R} → Companion₁ R ⊆ Companion R
companion₁⊆companion (F , mono , comp , x) =
  _⇔_.from below-the-companion⇔size-preserving
    (monotone→compatible→size-preserving mono comp) x

-- The other direction holds iff Companion is compatible.
--
-- However, I don't know if Companion is provably compatible (in
-- predicative, constructive type theory).

companion-compatible⇔companion⊆companion₁ :
  Compatible Companion ⇔ (∀ {R} → Companion R ⊆ Companion₁ R)
companion-compatible⇔companion⊆companion₁ = record
  { to   = λ comp f → (Companion , companion-monotone , comp , f)
  ; from = λ below f →
             let (F , mono , comp , FCR) = below f
             in map C (λ FR {_} →
                         companion₁⊆companion (F , mono , comp , FR))
                      (comp FCR)
  }
  where
  -- An alternative implementation of the from component which might
  -- be a bit easier to follow.

  from′ : (∀ {R} → Companion R ⊆ Companion₁ R) → Compatible Companion
  from′ below {R = R} =
    Companion (⟦ C ⟧ R)      ⊆⟨ below ⟩

    Companion₁ (⟦ C ⟧ R)     ⊆⟨ (λ { (F , mono , comp , x) → (_$ x) (

        F (⟦ C ⟧ R)               ⊆⟨ comp ⟩

        ⟦ C ⟧ (F R)               ⊆⟨ map C (

            F R                        ⊆⟨ (λ y → F , (λ {_ _} → mono) , (λ {_ _} → comp) , y) ⟩
            Companion₁ R               ⊆⟨ companion₁⊆companion ⟩∎
            Companion R                ∎) ⟩∎

        ⟦ C ⟧ (Companion R)        ∎) }) ⟩∎

    ⟦ C ⟧ (Companion R)      ∎

-- Assumptions used by companion-compatible below.

record Companion-compatible-assumptions : Set (lsuc ℓ) where
  field
    -- A strong form of excluded middle, not compatible with
    -- univalence.

    excluded-middle : (P : Set ℓ) → Dec P

  -- The type i < j means that i is a smaller size than j, and i ≤ j
  -- means that i is smaller than or equal to j.

  infix  _<_ _≤_

  _<_ : Size → Size → Set
  _<_ = λ i j → Σ (Size< j) λ { k → i ≡ k }

  _≤_ : Size → Size → Set
  _≤_ = λ i j → i < j ⊎ i ≡ j

  -- Successor sizes: Sizes i for which there is a size j < i such
  -- that every size k < i satisfies k ≤ j.

  Successor : Size → Set
  Successor i = Σ (Size< i) λ { j → (k : Size< i) → k ≤ j }

  field
    -- If i is not smaller than or equal to j, then j is smaller
    -- than i.

    ≰→> : ∀ {i j} → ¬ i ≤ j → j < i

    -- If a predicate from a certain class of predicates is satisfied
    -- for all sizes smaller than i, but not for i itself, then i is a
    -- successor size.

    is-successor :
      {R : Rel ℓ I} →
      let P = λ i → R ⊆ ν C i in
      ∀ i →
      ((j : Size< i) → P j) →
      ¬ P i →
      Successor i

    -- Size elimination. A very similar elimination principle can at
    -- the time of writing be implemented in Agda, but Andreas Abel
    -- has suggested that this implementation should not be allowed.

    size-elim :
      (P : Size → Set ℓ) →
      (∀ i → ((j : Size< i) → P j) → P i) →
      ∀ i → P i

  -- A variant of excluded-middle.

  excluded-middle₀ : (P : Set) → Dec P
  excluded-middle₀ P =
    ⊎-map lower (_∘ lift) $ excluded-middle (↑ ℓ P)

  -- "Not for all" implies "exists not".

  ¬∀→∃¬ : {A : Set} {P : A → Set ℓ} →
          ¬ (∀ x → P x) → ∃ λ x → ¬ P x
  ¬∀→∃¬ {P = P} ¬∀ = case excluded-middle (∃ λ x → ¬ P x) of λ where
    (inj₁ ∃¬P)  → ∃¬P
    (inj₂ ¬∃¬P) → ⊥-elim (¬∀ λ x → case excluded-middle (P x) of λ where
      (inj₁ Px)  → Px
      (inj₂ ¬Px) → ⊥-elim (¬∃¬P (x , ¬Px)))

  -- Given the assumptions above every pair of sizes must be related
  -- by either _<_, _≡_, or flip _<_. However, note that all three
  -- relations hold for ∞ and ∞, so we do not get a law of trichotomy.

  compare : ∀ i j → i < j ⊎ i ≡ j ⊎ j < i
  compare i j = case excluded-middle₀ (i < j) of λ where
    (inj₁ i<j) → inj₁ i<j
    (inj₂ i≮j) → case excluded-middle₀ (i ≡ j) of λ where
      (inj₁ i≡j) → inj₂ (inj₁ i≡j)
      (inj₂ i≢j) → inj₂ (inj₂ (≰→> [ i≮j , i≢j ]))

-- Given certain assumptions one can prove that the companion is
-- compatible. (The proof is based on that of Theorem 2.14 in Parrow
-- and Weber's "The Largest Respectful Function".) However, I don't
-- know if these assumptions are consistent with the variant of Agda
-- that is used in this development. I discussed the assumptions with
-- Andreas Abel and Andrea Vezzosi. Some potential problems came up in
-- the discussion:
--
-- * The fact that ∞ : Size< ∞ could perhaps lead to some kind of
--   problem.
--
-- * The assumptions make it possible to define functions that give
--   completely different results for different sizes (assuming that
--   there is more than one size).

companion-compatible :
  Companion-compatible-assumptions → Compatible Companion
companion-compatible assumptions {R} = case lemma R of λ where

    (inj₁ R⊆νC) →
      Companion (⟦ C ⟧ R)  ⊆⟨ _$ map C (λ Rx → λ { .force → R⊆νC Rx }) ⟩
      ν C ∞                ⊆⟨ map C (λ ν′C∞x {_} _ → force ν′C∞x) ⟩∎
      ⟦ C ⟧ (Companion R)  ∎

    (inj₂ (1+i , (i , <1+i→≤i) , <1+i→R⊆νC , R⊈νC[1+i])) →

      let CR⊆νC[1+i] =
            ⟦ C ⟧ R        ⊆⟨ map C (<1+i→R⊆νC i) ⟩
            ⟦ C ⟧ (ν C i)  ⊆⟨ map C (λ x → λ { .force {j} → cast (<1+i→≤i j) x }) ⟩∎
            ν C 1+i        ∎

          νCi⊆CompanionR =
            ν C i                                                ⊆⟨ (λ hyp → λ { j≤i → cast j≤i hyp }) ⟩
            (λ x → ∀ {j} → j ≤ i → ν C j x)                      ⊆⟨ (λ hyp → λ { (j , refl) → hyp (<1+i→≤i j) }) ⟩
            (λ x → ∀ {j} → j < 1+i → ν C j x)                    ⊆⟨ (λ hyp → λ { j<1+i _ → hyp j<1+i }) ⟩
            (λ x → ∀ {j} → j < 1+i → R ⊆ ν C j → ν C j x)        ⊆⟨ (λ hyp → λ { 1+i≰j → hyp (≰→> 1+i≰j) }) ⟩
            (λ x → ∀ {j} → ¬ 1+i ≤ j → R ⊆ ν C j → ν C j x)      ⊆⟨ (λ hyp → λ { {j} → [ (λ 1+i≤j R⊆νCj →
                                                                                            ⊥-elim $ R⊈νC[1+i] (
                R                                                                             ⊆⟨ (λ {x} → R⊆νCj {x}) ⟩
                ν C j                                                                         ⊆⟨ cast 1+i≤j ⟩∎
                ν C 1+i                                                                       ∎))
                                                                                       , hyp
                                                                                       ] }) ⟩
            (λ x → ∀ {j} → Dec (1+i ≤ j) → R ⊆ ν C j → ν C j x)  ⊆⟨ (λ hyp → λ { {_} → hyp (excluded-middle₀ _) }) ⟩
            (λ x → ∀ {j} → R ⊆ ν C j → ν C j x)                  ⊆⟨ id ⟩∎
            Companion R                                          ∎
      in
      Companion (⟦ C ⟧ R)  ⊆⟨ _$ CR⊆νC[1+i] ⟩
      ν C 1+i              ⊆⟨⟩
      ⟦ C ⟧ (ν′ C 1+i)     ⊆⟨ map C (λ x → force x) ⟩
      ⟦ C ⟧ (ν C i)        ⊆⟨ map C νCi⊆CompanionR ⟩∎
      ⟦ C ⟧ (Companion R)  ∎

  where
  open Companion-compatible-assumptions assumptions

  cast : ∀ {j k} → j ≤ k → ν C k ⊆ ν C j
  cast (inj₁ (_ , refl)) x = x
  cast (inj₂ refl)       x = x

  lemma :
    ∀ R → (∀ {i} → R ⊆ ν C i)
            ⊎
          ∃ λ i → Successor i ×
                  ((j : Size< i) → R ⊆ ν C j) ×
                  ¬ R ⊆ ν C i
  lemma R =
    case excluded-middle (∀ {i} → R ⊆ ν C i) of
      ⊎-map id
        (¬ (∀ {i} → R ⊆ ν C i)                                ↝⟨ (λ hyp → ¬∀→∃¬ {P = λ _ → _ ⊆ _} (λ ∀iR⊆νCi → hyp λ {i} → ∀iR⊆νCi i)) ⟩

         (∃ λ i → ¬ R ⊆ ν C i)                                ↝⟨ uncurry $
                                                                   size-elim (λ i → ¬ R ⊆ ν C i → _)
                                                                   (λ i ind-hyp R⊈νCi → case excluded-middle _ of λ where
                                                                        (inj₁ ∀<R⊆νC)  → i , ∀<R⊆νC , R⊈νCi
                                                                        (inj₂ ¬∀<R⊆νC) → let j , R⊈νCj = ¬∀→∃¬ ¬∀<R⊆νC
                                                                                         in ind-hyp j R⊈νCj) ⟩

         (∃ λ i → ((j : Size< i) → R ⊆ ν C j) × ¬ R ⊆ ν C i)  ↝⟨ (λ { (i , hyp) → (i , uncurry (is-successor i) hyp , hyp) }) ⟩□

         (∃ λ i → Successor i ×
                  ((j : Size< i) → R ⊆ ν C j) × ¬ R ⊆ ν C i)  □)