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

module Relation.Binary.PropositionalEquality.Subst.Properties where

-- Properties of 'subst' onto binary relations.

open import Level
open import Function using (_$_; flip) renaming (id to idFun; _∘_ to _⊚_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

private
  variable
     ℓ₁ ℓ₂ t t₁ t₂ o : Level

-- Two shorthands:  transport the domain or codomain of a relation along an equality.
module Shorthands {O : Set o} (R : Rel O ) where
  infixr 9 _◂_
  infixl 9 _▸_

  _◂_ :  {A B C}  A  B  R B C  R A C
  p  f = subst (flip R _) (sym p) f

  _▸_ :  {A B C}  R A B  B  C  R A C
  f  p = subst (R _) p f

  -- Some simple properties of transports
module Transport {O : Set o} (R : Rel O ) where
  open Shorthands R public

  ◂-▸-id :  {A} (f : R A A)  refl  f  f  refl
  ◂-▸-id f = refl

  ◂-▸-comm :  {A B C D} (p : A  B) (f : R B C) (q : C  D) 
             (p  (f  q))  ((p  f)  q)
  ◂-▸-comm refl f refl = refl

  ◂-assocˡ :  {A B C D} (p : A  B) {q : B  C} (f : R C D) 
            p  q  f  (trans p q)  f
  ◂-assocˡ refl {refl} f = refl

  ▸-assocʳ :  {A B C D} (f : R A B) {p : B  C} (q : C  D) 
            f  p  q  f  trans p q
  ▸-assocʳ f {refl} refl = refl

-- If we have a relation Q over a relation R, we can transport over that too
module TransportOverQ {O : Set o} (R : Rel O ) (Q : {X Y : O}  Rel (R X Y) t)  where
  open Transport R

  ◂-resp-≈ :  {A B C} (p : A  B) {f g : R B C}  Q f g  Q (p  f) (p  g)
  ◂-resp-≈ refl f≈g = f≈g

  ▸-resp-≈ :  {A B C} {f g : R A B}  Q f g  (p : B  C)  Q (f  p) (g  p)
  ▸-resp-≈ f≈g refl = f≈g

-- Given two relations and a homomorphism between them,
-- congruence properties over subst
module TransportMor {O₁ O₂ : Set o}
  (R₁ : Rel O₁ ) (R₂ : Rel O₂ t)
  (M₀       : O₁  O₂)
  (M₁       :  {A B}  R₁ A B  R₂ (M₀ A) (M₀ B)) where

  open Shorthands R₁
  open Shorthands R₂ renaming (_◂_ to _◃_; _▸_ to _▹_)

  M-resp-▸ :  {A B C} (f : R₁ A B) (p : B  C) 
             M₁ (f  p)  M₁ f  cong M₀ p
  M-resp-▸ f refl = refl

  M-resp-◂ :  {A B C} (p : A  B) (f : R₁ B C) 
             M₁ (p  f)  cong M₀ p  M₁ f
  M-resp-◂ refl f = refl


-- Transports on paths
module TransportStar {O : Set o} (R : Rel O ) where
  open Shorthands (Star R) public renaming
    ( _◂_ to _◂*_
    ; _▸_ to _▸*_
    )
  open Shorthands R

  -- Lemmas relating transports to path operations.

  ◂*-▸*-ε : {A B : O} (p : A  B)  ε ▸* p  p ◂* ε
  ◂*-▸*-ε refl = refl

  ◂*-◅ : {A B C D : O} (p : A  B) (f : R B C) (fs : Star R C D) 
         p ◂* (f  fs)  (p  f)  fs
  ◂*-◅ refl f fs = refl

  ◅-▸* : {A B C D : O} (f : R A B) (fs : Star R B C) (p : C  D) 
         (f  fs) ▸* p  f  (fs ▸* p)
  ◅-▸* f fs refl = refl

  ◅-◂*-▸ : {A B C D : O} (f : R A B) (p : B  C) (fs : Star R C D) 
           _≡_ {_} {Star R A D} (f  (p ◂* fs)) ((f  p)  fs)
  ◅-◂*-▸ f refl fs = refl