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

module container.equality where

open import level
open import sum
open import equality.core
open import function.isomorphism
open import function.extensionality
open import container.core
open import container.fixpoint

module Equality {li la lb lx}
                (c : Container li la lb)
                (fp : Fixpoint c lx) where
  open Container c
  open Fixpoint fp

  substX : {i : I}{a a' : A i}(p : a  a')(b : B a)
          X (r (subst B p b))  X (r b)
  substX refl _ x = x

  substX-β :  {i} {a a' : A i}
             (f : (b : B a)  X (r b))
             (f' : (b : B a')  X (r b))
             (p : a  a')
            (subst  a  (b : B a)  X (r b)) p f  f')
            ((b : B a)  f b  substX p b (f' (subst B p b)))
  substX-β f f' refl = sym≅ strong-funext-iso

  -- structural equality for container fixpoints
  I-≡ : Set (li  lx)
  I-≡ = Σ I λ i  X i × X i

  A-≡ : I-≡  Set la
  A-≡ (_ , u , v) = head u  head v

  B-≡ : {j : I-≡}  A-≡ j  Set lb
  B-≡ {_ , u , _} _ = B (head u)

  r-≡ : {j : I-≡}{p : A-≡ j}  B-≡ p  I-≡
  r-≡ {i , u , v}{p} b = r b , tail u b , substX p b (tail v (subst B p b))

  equality : Container _ _ _
  equality = record
    { I = I-≡
    ; A = A-≡
    ; B = B-≡
    ; r =  {j p}  r-≡ {j} {p}) }