module Setoid.EqualityType where

open import Prelude

open import Setoid.Definition
open import Setoid.Universes
open import Setoid.Lift

----------------------------------------------------------------------
-- Equality types
----------------------------------------------------------------------
record EQ (l : β„•) : Set where
  field
    ty :
      (X : U l)
      (_ _ : El l X)
      β†’ ------------
      U l

    tyCong :
      {X X' : U l}
      {x y : El l X}
      {x' y' : El l X'}
      (_ : 𝒰 l βˆ‹ X ~ X')
      (_ : ℰ𝓁 l βˆ‹ X βΈ΄ x β‰ˆ X' βΈ΄ x')
      (_ : ℰ𝓁 l βˆ‹ X βΈ΄ y β‰ˆ X' βΈ΄ y')
      β†’ --------------------------
      𝒰 l βˆ‹ ty X x y ~ ty X' x' y'

    rfl :
      {X : U l}
      (x : El l X)
      β†’ -------------
      El l (ty X x x)

    rflCong :
      {X X' : U l}
      {x : El l X}
      {x' : El l X'}
      (_ : 𝒰 l βˆ‹ X ~ X')
      (_ :  ℰ𝓁 l βˆ‹ X βΈ΄ x β‰ˆ X' βΈ΄ x')
      β†’ --------------------------------------------
      ℰ𝓁 l βˆ‹ ty X x x βΈ΄ rfl x β‰ˆ ty X' x' x' βΈ΄ rfl x'

    reflect :
      {X : U l}
      {x y : El l X}
      (_ : El l (ty X x y))
      β†’ -------------------
      ℰ𝓁 l βˆ‹ X βΈ΄ x β‰ˆ X βΈ΄ y

    uip :
      {X : U l}
      {x y : El l X}
      (e e' : El l (ty X x y))
      β†’ ------------------------
      ℰ𝓁 l β€² (ty X x y) βˆ‹ e ~ e'

eq : βˆ€ l β†’ EQ l

EQ.ty      (eq 0) = Eqβ‚€
EQ.tyCong  (eq 0) e e' e'' = (e , e' , e'')
EQ.rfl     (eq 0) {X} = hrflβ‚€ X
EQ.rflCong (eq 0) _ _ = tt
EQ.reflect (eq 0) e = e
EQ.uip     (eq 0) _ _ = tt
EQ.ty      (eq(1+ _)) = Eqβ‚Š
EQ.tyCong  (eq(1+ _)) e e' e'' = (e , e' , e'')
EQ.rfl     (eq(1+ _)) {X} = hrflβ‚Š X
EQ.rflCong (eq(1+ _)) _ _ = tt
EQ.reflect (eq(1+ _)) e = e
EQ.uip     (eq(1+ _)) _ _ = tt

-- Equality types
-- Eq :
--   (n : β„•)
--   (T : U n)
--   (t t' : El n T)
--   β†’ -------------
--   U n

-- Eq n = EQ.ty (eq n)

-- Rfl :
--   (n : β„•)
--   {T : U n}
--   (t : El n T)
--   β†’ ----------
--   El n (Eq n T t t)

-- Rfl n = EQ.rfl (eq n)