{-# 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
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}) }