{-# OPTIONS --without-K --safe --guardedness --no-sized-types #-}

open import dtt

module equality where


--------------
-- identity --
--------------

open import Agda.Builtin.Equality public
-- ≡ is \equiv or \==

J : {X : Set}
    (C : (x y : X) (eq : x ≡ y) → Set)
    (c : (x : X) → C x x refl)
    (x y : X) (eq : x ≡ y) → C x y eq
J C c x y refl = c x

trans : {X : Set} {x : X} {y : X} {z : X} -> (x ≡ y) -> (y ≡ z) -> x ≡ z
trans {X} {x} {y} {z} eq₁ eq₂ = J (λ x y eq → (y ≡ z → x ≡ z)) (λ z → λ eq → eq) x y eq₁ eq₂
--trans refl eq = eq

sym : {U : Set} {u : U} {v : U} -> u ≡ v -> v ≡ u
sym {U} {u} {v} eq = J (λ u v _ → v ≡ u) (λ u → refl) u v eq
--sym refl = refl

ap : {A : Set} {B : Set} (f : A → B) {x y : A}
  → (x ≡ y → f x ≡ f y)
ap f {x} {y} eq = J (λ x y _ → f x ≡ f y) (λ x → refl) x y eq
--ap f refl = refl

ap-f :  {A : Set} {B : Pow A} {f g : Π A B} (x : A) → (f ≡ g → f x ≡ g x)
ap-f {A} {B} {f} {g} x eq = J (λ f g eq → (x : A) → f x ≡ g x) (λ f → λ x → refl) f g eq x
-- ap-f {f} {g} x refl = refl

-- usual transport
transport : {X : Set} (Y : X → Set)
            {x x' : X}
            (p : x ≡ x') → (Y x → Y x')
transport Y {x} {x'} eq = J (λ x x' _ → Y x → Y x') (λ x y → y) x x' eq
--transport Y refl x = x

-- transport for doubly dependent families
higher-transport : {X : Set} (Y : X → Set) (Z : (x : X) → Y x → Set)
                   {x x' : X}
                   (p : x ≡ x') → (y : Y x) →
                   let y' : Y x'
                       y' = transport Y p y in
                   (Z x y → Z x' y')
higher-transport {X} Y Z {x} {x'} p =
  J (λ x x' p → (y : Y x) →
     let y' : Y x'
         y' = transport Y p y in
     Z x y → Z x' y') (λ x y z → z) x x' p
--higher-transport {X} Y Z refl y z = z



sigma-eq-intro : {X : Set} {Y : X → Set} {x x' : X} {y : Y x} {y' : Y x'}
                 (eq : x ≡ x') → (y' ≡ transport (Y) eq y) → (x , y) ≡ (x' , y')
sigma-eq-intro {X} {Y} {x} {x'} {y} {y'} eq_x eq_y =
            J (λ x x' eq_x → (y : Y x) → (y' : Y x') → (y' ≡ transport Y eq_x y) → (x , y) ≡ (x' , y')) (λ x y y' eq_y →
                 J (λ y y' eq → (x , y') ≡ (x , y)) (λ y → refl) y' (transport Y refl y) eq_y)
            x x' eq_x y y' eq_y
--sigma-eq-intro refl refl = refl

sigma-eq-fst : {X : Set} {Y : Pow X} {p q : Σ X Y} (eq : p ≡ q) → fst p ≡ fst q
sigma-eq-fst {X} {Y} {p} {q} eq = ap fst eq

sigma-eq-snd : {X : Set} {Y : Pow X} {p q : Σ X Y} (eq : p ≡ q) →
               transport Y (sigma-eq-fst eq) (snd p) ≡ snd q
sigma-eq-snd {X} {Y} {p} {q} eq = J (λ p q eq → transport Y (sigma-eq-fst eq) (snd p) ≡ snd q) (λ _ → refl) p q eq
--sigma-eq-snd refl = refl