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

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

-- 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 Prelude.Size

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 ^[ 1 + n ] R)  ⊆⟨ map C (1 + 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 ^[ 1 + n ] R              ⊆⟨⟩
    F (F ^[ n ] R)              ⊆⟨ mono (Fⁿ⊆∘F¹⁺ⁿ n) 
    F ( C  (F ^[ 1 + n ] R))  ⊆⟨ comp ⟩∎
     C  (F ^[ 2 + 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       ⊆⟨ 0 ,_ 
  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 4 _<_ _≤_

  _<_ : 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)  )