open import Data.Product

Rel : Set → Set → Set₁
Rel A B = A → B → Set

infixl 5 _∘_
_∘_ : ∀ {A B C} → Rel B C → Rel A B → Rel A C
_S_ ∘ _R_ = λ x z → ∃ λ y → x R y × y S z

join : {A B I : Set} → (I → Rel A B) → Rel A B
join S x y = ∃ λ i → S i x y

-- extensional equality
infix 4 _≈_
_≈_ : {A B : Set} → (S R : Rel A B) → Set
_≈_ {A} {B} _S_ _R_ = ∀ {x : A} {y : B} → (x S y → x R y) × (x R y → x S y)

join-continuousₗ : ∀ {A B C I : Set} (S : I → Rel B C) (R : Rel A B) →
  (join S) ∘ R ≈ join λ i → (S i) ∘ R
join-continuousₗ S R .proj₁ (b , xRb , bSy) = bSy .proj₁ , b , xRb , bSy .proj₂
join-continuousₗ S R .proj₂ (i , b , xRb , bSiy) = b , xRb , i , bSiy

join-continuousᵣ : ∀ {A B C I : Set} (S : I → Rel A B) (R : Rel B C) →
   R ∘ (join S) ≈ join λ i →  R ∘ (S i)
join-continuousᵣ S R .proj₂ (i , b , xRb , bSiy) = b , (i , xRb) , bSiy
join-continuousᵣ S R .proj₁ (b , xRb , bSy) = xRb .proj₁ , b , xRb .proj₂ , bSy