open import Data.Product
open import Agda.Primitive using (_⊔_; lsuc; lzero)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; sym)

left-total : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → B → Set ℓ') → Set (ℓ ⊔ ℓ')
left-total rel = ∀ a → Σ _ λ b → rel a b

functional : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → B → Set ℓ') → Set (ℓ ⊔ ℓ')
functional rel = ∀ a b c → rel a b × rel a c → b ≡ c 

_→ᵣ_ : ∀ {ℓ ℓ'} → Set ℓ → Set ℓ' → Set (ℓ ⊔ (lsuc ℓ'))
_→ᵣ_ {ℓ} {ℓ'} A B = Σ (A → B → Set ℓ') λ rel →
                left-total {A = A} {B = B} rel × functional {A = A} {B = B} rel
                
call : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A →ᵣ B → A → B
call (f , ltot , fun) a = proj₁ (ltot a)

llac : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → B) → A →ᵣ B
llac f = (λ a b → f a ≡ b) ,
          (λ a → (f a) , refl) ,
          λ a b c x → trans (sym (proj₁ x)) (proj₂ x)
  
-- →ᵣ-→-coincide' : ∀ {A B} → A →ᵣ B → (A → B) → Set
-- →ᵣ-→-coincide' fᵣ f = ∀ a → call fᵣ a ≡ f a

→ᵣ-→-coincide : ∀ {A B} → A →ᵣ B → (A → B) → Set
→ᵣ-→-coincide (r , _) f = (∀ {a b} → r a b → f a ≡ b) × (∀ {a} → r a (f a))

→-→ᵣ-coincide : ∀ {A B} →  (A → B) → A →ᵣ B → Set
→-→ᵣ-coincide f fᵣ = →ᵣ-→-coincide fᵣ f

→ᵣ-→-coincide-call : ∀ {A B} (fᵣ : A →ᵣ B) → →ᵣ-→-coincide fᵣ (call fᵣ)
→ᵣ-→-coincide-call {A} {B} (r , ltot , fun) =
  (λ {a} {b} aRb → fun a (proj₁ (ltot a)) b (proj₂ (ltot a) , aRb)) ,
  λ {a} → proj₂ (ltot a)

→ᵣ-→-coincide-llac : ∀ {A B} (f : A → B) → →ᵣ-→-coincide (llac f) f
→ᵣ-→-coincide-llac f = (λ fa≡b → fa≡b) , refl

_∘_ : ∀ {ℓ ℓ' ℓ''} {A : Set ℓ} {B : Set ℓ'} {C : Set ℓ''} → (B → C) → (A → B) → (A → C)
f ∘ g = λ a → f (g a)

_∼_ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → (A → B) → (A → B) → Set (ℓ ⊔ ℓ' )
f ∼ g = ∀ a → f a ≡ g a

call∘llac∼id : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'}
             → (call ∘ llac) ∼ (λ (x : A → B) → x)
call∘llac∼id _ = refl

-- llac∘call∼id : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'}
--              → (llac ∘ call) ∼ (λ (x : A →ᵣ B) → x)
-- llac∘call∼id (r , ltot , fun) = {!!}