{-

Definition of what it means to be a notion of relational structure

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.RelationalStructure where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Univalence
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Sigma
open import Cubical.HITs.PropositionalTruncation as Trunc
open import Cubical.HITs.SetQuotients
open import Cubical.Relation.Binary.Base
open import Cubical.Relation.ZigZag.Base

open BinaryRelation
open isEquivRel
open isQuasiEquivRel

private
  variable
     ℓ' ℓ'' ℓ''' : Level

-- A notion of structured relation for a structure S assigns a relation on S X and S Y to every relation on X
-- and Y. We require the output to be proposition-valued when the input is proposition-valued.
StrRel : (S : Type   Type ℓ') (ℓ'' : Level)  Type (ℓ-max (ℓ-suc (ℓ-max  ℓ'')) ℓ')
StrRel { = } S ℓ'' =  {A B} (R : Rel A B )  Rel (S A) (S B) ℓ''

-- Given a type A and relation R, a quotient structure is a structure on the set quotient A/R such that
-- the graph of [_] : A → A/R is a structured relation
InducedQuotientStr : (S : Type   Type ℓ') (ρ : StrRel S ℓ'')
  (A : TypeWithStr  S) (R : Rel (typ A) (typ A) )
   Type (ℓ-max ℓ' ℓ'')
InducedQuotientStr S ρ A R =
  Σ[ s  S (typ A / R) ] ρ (graphRel [_]) (A .snd) s

-- A structured equivalence relation R on a structured type A should induce a structure on A/R
InducesQuotientStr : (S : Type   Type ℓ') (ρ : StrRel S ℓ'')  Type _
InducesQuotientStr { = } S ρ =
  (A : TypeWithStr  S) (R : EquivPropRel (typ A) )
   ρ (R .fst .fst) (A .snd) (A .snd)
   ∃![ s  S (typ A / R .fst .fst) ] ρ (graphRel [_]) (A .snd) s

-- The identity should be a structured relation
isReflexiveStrRel : {S : Type   Type ℓ'} (ρ : StrRel S ℓ'')  Type _
isReflexiveStrRel { = } {S = S} ρ =
  {X : Type }  (s : S X)  ρ (idPropRel X .fst) s s

-- The inverse of a structured relation should be structured
isSymmetricStrRel : {S : Type   Type ℓ'} (ρ : StrRel S ℓ'')  Type _
isSymmetricStrRel { = } {S = S} ρ =
  {X Y : Type } (R : PropRel X Y )
  {sx : S X} {sy : S Y}
   ρ (R .fst) sx sy
   ρ (invPropRel R .fst) sy sx

-- The composite of structured relations should be structured
isTransitiveStrRel : {S : Type   Type ℓ'} (ρ : StrRel S ℓ'')  Type _
isTransitiveStrRel { = } {S = S} ρ =
  {X Y Z : Type }
  (R : PropRel X Y ) (R' : PropRel Y Z )
  {sx : S X} {sy : S Y} {sz : S Z}
   ρ (R .fst) sx sy
   ρ (R' .fst) sy sz
   ρ (compPropRel R R' .fst) sx sz

-- The type of structures on a set should be a set
preservesSetsStr : (S : Type   Type ℓ')  Type (ℓ-max (ℓ-suc ) ℓ')
preservesSetsStr S =  {X}  isSet X  isSet (S X)

-- The type of structures on a prop-valued relation should be a prop
preservesPropsStrRel : {S : Type   Type ℓ'} (ρ : StrRel S ℓ'')  Type _
preservesPropsStrRel { = } {S = S} ρ =
  {X Y : Type } {R : Rel X Y }
   (∀ x y  isProp (R x y))
   (sx : S X) (sy : S Y)
   isProp (ρ R sx sy)

record SuitableStrRel (S : Type   Type ℓ') (ρ : StrRel S ℓ'') : Type (ℓ-max (ℓ-max (ℓ-suc ) ℓ') ℓ'')
  where
  field
    quo : InducesQuotientStr S ρ
    symmetric : isSymmetricStrRel ρ
    transitive : isTransitiveStrRel ρ
    set : preservesSetsStr S
    prop : preservesPropsStrRel ρ

open SuitableStrRel public

quotientPropRel :  {} {A : Type } (R : Rel A A )  PropRel A (A / R) 
quotientPropRel R .fst a t = [ a ]  t
quotientPropRel R .snd _ _ = squash/ _ _

-- We can also ask for a notion of structured relations to agree with some notion of structured equivalences.

StrRelMatchesEquiv : {S : Type   Type ℓ'}
   StrRel S ℓ''  StrEquiv S ℓ'''  Type _
StrRelMatchesEquiv {S = S} ρ ι =
  (A B : TypeWithStr _ S) (e : typ A  typ B) 
  ρ (graphRel (e .fst)) (A .snd) (B .snd)  ι A B e

-- Additional conditions for a "positive" notion of structured relation

isDetransitiveStrRel : {S : Type   Type ℓ'} (ρ : StrRel S ℓ'')  Type _
isDetransitiveStrRel { = } {S = S} ρ =
  {X Y Z : Type }
  (R : PropRel X Y ) (R' : PropRel Y Z )
  {sx : S X} {sz : S Z}
   ρ (compPropRel R R' .fst) sx sz
   ∃[ sy  S Y ] ρ (R .fst) sx sy × ρ (R' .fst) sy sz

record StrRelAction {S : Type   Type ℓ'} (ρ : StrRel S ℓ'')
  : Type (ℓ-max (ℓ-suc ) (ℓ-max ℓ' ℓ''))
  where
  field
    actStr :  {X Y}  (X  Y)  S X  S Y
    actStrId :  {X} (s : S X)  actStr (idfun X) s  s
    actRel :  {X₀ Y₀ X₁ Y₁} {f : X₀  X₁} {g : Y₀  Y₁}
      {R₀ : X₀  Y₀  Type } {R₁ : X₁  Y₁  Type }
       (∀ x y  R₀ x y  R₁ (f x) (g y))
        sx sy  ρ R₀ sx sy  ρ R₁ (actStr f sx) (actStr g sy)

open StrRelAction public

strRelQuotientComparison : {S : Type   Type ℓ'} {ρ : StrRel S ℓ''}
  (θ : SuitableStrRel S ρ) (α : StrRelAction ρ)
  {X : Type } (R : EquivPropRel X )
   (S X / ρ (R .fst .fst))  S (X / R .fst .fst)
strRelQuotientComparison θ α R [ s ] = α .actStr [_] s
strRelQuotientComparison {ρ = ρ} θ α R (eq/ s t r i) =
  (sym leftEq  rightEq) i
  where
  ρs : ρ (R .fst .fst) s s
  ρs =
    subst  R'  ρ R' s s)
      (funExt₂ λ x x' 
        hPropExt squash (R .fst .snd x x')
          (Trunc.rec (R .fst .snd x x')
             {(_ , r , r')  R .snd .transitive _ _ _ r (R .snd .symmetric _ _ r')}))
           r   x' , r , R .snd .reflexive x' ))
      (θ .transitive (R .fst) (invPropRel (R .fst)) r (θ .symmetric (R .fst) r))

  leftEq : θ .quo (_ , s) R ρs .fst .fst  α .actStr [_] s
  leftEq =
    cong fst
      (θ .quo (_ , s) R ρs .snd
        ( α .actStr [_] s
        , subst
           s'  ρ (graphRel [_]) s' (α .actStr [_] s))
          (α .actStrId s)
          (α .actRel eq/ s s ρs)
        ))

  rightEq : θ .quo (_ , s) R ρs .fst .fst  α .actStr [_] t
  rightEq =
    cong fst
      (θ .quo (_ , s) R ρs .snd
        ( α .actStr [_] t
        , subst
           s'  ρ (graphRel [_]) s' (α .actStr [_] t))
          (α .actStrId s)
          (α .actRel eq/ s t r)
        ))
strRelQuotientComparison θ α R (squash/ _ _ p q i j) =
  θ .set squash/ _ _
    (cong (strRelQuotientComparison θ α R) p)
    (cong (strRelQuotientComparison θ α R) q)
    i j

record PositiveStrRel {S : Type   Type ℓ'} {ρ : StrRel S ℓ''} (θ : SuitableStrRel S ρ)
  : Type (ℓ-max (ℓ-suc ) (ℓ-max ℓ' ℓ''))
  where
  field
    act : StrRelAction ρ
    reflexive : isReflexiveStrRel ρ
    detransitive : isDetransitiveStrRel ρ
    quo : {X : Type } (R : EquivPropRel X )  isEquiv (strRelQuotientComparison θ act R)

open PositiveStrRel public

posRelReflexive : {S : Type   Type ℓ'} {ρ : StrRel S ℓ''} {θ : SuitableStrRel S ρ}
   PositiveStrRel θ
   {X : Type } (R : EquivPropRel X )
   (s : S X)  ρ (R .fst .fst) s s
posRelReflexive {ρ = ρ} σ R s =
  subst
    (uncurry (ρ (R .fst .fst)))
    (ΣPathP (σ .act .actStrId s , σ .act .actStrId s))
    (σ .act .actRel
       x y 
        Trunc.rec (R .fst .snd _ _)
           p  subst (R .fst .fst x) p (R .snd .reflexive x)))
      s s
      (σ .reflexive s))

-- Given a suitable notion of structured relation, if we have a structured quasi equivalence relation R
-- between structured types A and B, we get induced structures on the quotients A/(R ∙ R⁻¹) and B/(R⁻¹ ∙ R),
-- and the induced equivalence e : A/(R ∙ R⁻¹) ≃ B/(R⁻¹ ∙ R) is structured with respect to those quotient
-- structures.

record QERDescends (S : Type   Type ℓ') (ρ : StrRel S ℓ'')
  (A B : TypeWithStr  S) (R : QuasiEquivRel (typ A) (typ B) ) : Type (ℓ-max ℓ' ℓ'')
  where
  private
    module E = QER→Equiv R

  field
    quoᴸ : InducedQuotientStr S ρ A E.Rᴸ
    quoᴿ : InducedQuotientStr S ρ B E.Rᴿ
    rel : ρ (graphRel (E.Thm .fst)) (quoᴸ .fst) (quoᴿ .fst)

open QERDescends

structuredQER→structuredEquiv : {S : Type   Type ℓ'} {ρ : StrRel S ℓ''}
  (θ : SuitableStrRel S ρ)
  (A B : TypeWithStr  S) (R : QuasiEquivRel (typ A) (typ B) )
   ρ (R .fst .fst) (A .snd) (B .snd)
   QERDescends S ρ A B R
structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .quoᴸ =
  θ .quo (X , s) (QER→EquivRel R)
    (θ .transitive (R .fst) (invPropRel (R .fst)) r (θ .symmetric (R .fst) r))
    .fst

structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .quoᴿ =
  θ .quo (Y , t) (QER→EquivRel (invQER R))
    (θ .transitive (invPropRel (R .fst)) (R .fst) (θ .symmetric (R .fst) r) r)
    .fst

structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .rel =
  subst  R'  ρ R' (quol .fst) (quor .fst)) correction
    (θ .transitive (compPropRel (invPropRel (quotientPropRel E.Rᴸ)) (R .fst)) (quotientPropRel E.Rᴿ)
      (θ .transitive (invPropRel (quotientPropRel E.Rᴸ)) (R .fst)
        (θ .symmetric (quotientPropRel E.Rᴸ) (quol .snd))
        r)
      (quor .snd))
  where
  module E = QER→Equiv R
  quol = structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .quoᴸ
  quor = structuredQER→structuredEquiv {ρ = ρ} θ (X , s) (Y , t) R r .quoᴿ
  [R] = compPropRel (compPropRel (invPropRel (quotientPropRel E.Rᴸ)) (R .fst)) (quotientPropRel E.Rᴿ)

  correction : [R] .fst  graphRel (E.Thm .fst)
  correction =
    funExt₂ λ qx qy 
      (hPropExt squash (squash/ _ _)
        (Trunc.rec (squash/ _ _)
           {(y , qr , py) 
            Trunc.rec
              (squash/ _ _)
               {(x , px , r) 
                (cong (E.Thm .fst) (sym px)
                 E.relToFwd≡ r)
                 py})
              qr}))
        (elimProp {B = λ qx  E.Thm .fst qx  qy  [R] .fst qx qy}
           _  isPropΠ λ _  squash)
           x 
            elimProp {B = λ qy  E.Thm .fst [ x ]  qy  [R] .fst [ x ] qy}
               _  isPropΠ λ _  squash)
               y p   _ ,  _ , refl , E.fwd≡ToRel p  , refl )
              qy)
          qx))