{-# OPTIONS --prop --rewriting #-}

module lib where

open import Agda.Primitive public

-- We work in observational type theory (OTT)
-- OTT is not natively supported by Agda, so we postulate function extensionality, the coe operator,
-- and its computation rules according to "Observational equality meets CIC" by Leray, Tabareau and
-- Pujet.

infixl  _◼_
infix  _⁻¹
infix  _≡_
infix  _~_
infixl  _,Σ_

data _≡_ {i} {A : Set i} (a : A) : A → Prop i where
  ≡refl : a ≡ a

data _~_ {i} {A : Set i} (a : A) : {B : Set i} → B → Prop i where
  ~refl : a ~ a

~to≡ : ∀ {i} {A : Set i} {a b : A} → a ~ b → a ≡ b
~to≡ ~refl = ≡refl

~to≡ty : ∀ {i} {A B : Set i} {a : A} {b : B} → a ~ b → A ≡ B
~to≡ty ~refl = ≡refl

≡to~ : ∀ {i} {A : Set i} {a b : A} → a ≡ b → a ~ b
≡to~ ≡refl = ~refl

_◼_ : ∀{i}{A B C : Set i}{a : A}{b : B}{c : C} → a ~ b → b ~ c → a ~ c
~refl ◼ e = e

_⁻¹ : ∀{i}{A B : Set i}{a : A}{b : B} → a ~ b → b ~ a
~refl ⁻¹ = ~refl

record ⊤ : Set where
  constructor tt

record ⊤ₚ : Prop where
  constructor ttₚ

record Σ {i}(A : Set i){j}(B : A → Set j) : Set (i ⊔ j) where
  constructor _,Σ_
  field
    π₁ : A
    π₂ : B π₁
open Σ public

data Squash {ℓ} (A : Set ℓ) : Prop ℓ where
  squash : A → Squash A

postulate pi-inj₁ : ∀ {i j} {A B : Set i} {P : A → Set j} {Q : B → Set j}
                      → ((x : A) → P x) ~ ((x : B) → Q x) → A ~ B

postulate pi-inj₂ : ∀ {i j} {A B : Set i} {P : A → Set j} {Q : B → Set j}
                      → ((x : A) → P x) ~ ((x : B) → Q x) → P ~ Q

postulate funext : ∀ {i j} {A B : Set i} {P : A → Set j} {Q : B → Set j} {f : (x : A) → P x} {g : (x : B) → Q x}
                      → ({a : A} → {b : B} → (a ~ b) → f a ~ g b) → f ~ g
postulate funextᵢ : ∀ {i j} {A B : Set i} {P : A → Set j} {Q : B → Set j} {f : {x : A} → P x} {g : {x : B} → Q x}
                      → ({a : A} → {b : B} → (a ~ b) → f {a} ~ g {b}) → (λ {x} → f {x}) ~ (λ {x} → g {x})

postulate coe≡     : ∀{ℓ}{A B : Set ℓ} → A ≡ B → A → B
postulate coerefl : ∀{ℓ}{A : Set ℓ}{e : A ≡ A}{a : A} → coe≡ e a ≡ a
postulate coeₚ     : ∀{ℓ}{A B : Prop ℓ} → A ~ B → A → B

{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE coerefl   #-}

coe≡-eq : ∀ {ℓ} {A B : Set ℓ} (e : A ≡ B) (t : A) → t ~ coe≡ e t
coe≡-eq ≡refl t = ~refl

coe≡-eq₂ : ∀ {ℓ} {A B C : Set ℓ} {e₁ : A ≡ B} {e₂ : A ≡ C} (t : A) → coe≡ e₁ t ~ coe≡ e₂ t
coe≡-eq₂ {e₁ = ≡refl} {e₂ = ≡refl} t = ~refl

coe : ∀{ℓ}{A B : Set ℓ} → A ~ B → A → B
coe e t = coe≡ (~to≡ e) t

coe-eq : ∀ {ℓ} {A B : Set ℓ} (e : A ~ B) (t : A) → t ~ coe e t
coe-eq ~refl t = ~refl

cong : ∀ {i j} {A : Set i} {P : A → Set j} (f : (x : A) → P x)
        → {a : A} → {b : A} → a ~ b → f a ~ f b
cong f ~refl = ~refl

cong₂ : ∀ {i j k} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k} (f : (a : A) (b : B a) → C a b)
        → {a₀ : A} → {a₁ : A} → a₀ ~ a₁ → {b₀ : B a₀} {b₁ : B a₁} → b₀ ~ b₁ → f a₀ b₀ ~ f a₁ b₁
cong₂ f ~refl ~refl = ~refl

cong₃ : ∀ {i j k l} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k} {D : (a : A) → (b : B a) → C a b → Set l}
        → (f : (a : A) (b : B a) (c : C a b) → D a b c)
        → {a₀ : A} → {a₁ : A} → a₀ ~ a₁ → {b₀ : B a₀} {b₁ : B a₁} → b₀ ~ b₁
        → {c₀ : C a₀ b₀} → {c₁ : C a₁ b₁} → c₀ ~ c₁ → f a₀ b₀ c₀ ~ f a₁ b₁ c₁
cong₃ f ~refl ~refl ~refl = ~refl

cong₄ : ∀ {i j k l m} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k} {D : (a : A) → (b : B a) → C a b → Set l}
           {E : (a : A) → (b : B a) → (c : C a b) → (d : D a b c) → Set m}
        → (f : (a : A) (b : B a) (c : C a b) (d : D a b c) → E a b c d)
        → {a₀ : A} → {a₁ : A} → a₀ ~ a₁ → {b₀ : B a₀} {b₁ : B a₁} → b₀ ~ b₁
        → {c₀ : C a₀ b₀} → {c₁ : C a₁ b₁} → c₀ ~ c₁ → {d₀ : D a₀ b₀ c₀} → {d₁ : D a₁ b₁ c₁} → d₀ ~ d₁
        → f a₀ b₀ c₀ d₀ ~ f a₁ b₁ c₁ d₁
cong₄ f ~refl ~refl ~refl ~refl = ~refl

cong₅ : ∀ {i j k l m n} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k} {D : (a : A) → (b : B a) → C a b → Set l}
           {E : (a : A) → (b : B a) → (c : C a b) → (d : D a b c) → Set m}
           {F : (a : A) → (b : B a) → (c : C a b) → (d : D a b c) → (e : E a b c d) → Set n}
        → (f : (a : A) (b : B a) (c : C a b) (d : D a b c) (e : E a b c d) → F a b c d e)
        → {a₀ : A} → {a₁ : A} → a₀ ~ a₁ → {b₀ : B a₀} {b₁ : B a₁} → b₀ ~ b₁
        → {c₀ : C a₀ b₀} → {c₁ : C a₁ b₁} → c₀ ~ c₁ → {d₀ : D a₀ b₀ c₀} → {d₁ : D a₁ b₁ c₁} → d₀ ~ d₁
        → {e₀ : E a₀ b₀ c₀ d₀} → {e₁ : E a₁ b₁ c₁ d₁} → e₀ ~ e₁
        → f a₀ b₀ c₀ d₀ e₀ ~ f a₁ b₁ c₁ d₁ e₁
cong₅ f ~refl ~refl ~refl ~refl ~refl = ~refl

congᵣᵣᵣᵢᵣ : ∀ {i j k l m n} {A : Set i} {B : A → Set j} {C : (a : A) → B a → Set k} {D : (a : A) → (b : B a) → C a b → Prop l}
           {E : (a : A) → (b : B a) → (c : C a b) → (d : D a b c) → Set m}
           {F : (a : A) → (b : B a) → (c : C a b) → (d : D a b c) → E a b c d → Set n}
        → (f : (a : A) (b : B a) (c : C a b) (d : D a b c) (e : E a b c d) → F a b c d e)
        → {a₀ : A} → {a₁ : A} → a₀ ~ a₁ → {b₀ : B a₀} {b₁ : B a₁} → b₀ ~ b₁
        → {c₀ : C a₀ b₀} → {c₁ : C a₁ b₁} → c₀ ~ c₁ → {d₀ : D a₀ b₀ c₀} → {d₁ : D a₁ b₁ c₁}
        → {e₀ : E a₀ b₀ c₀ d₀} → {e₁ : E a₁ b₁ c₁ d₁} → e₀ ~ e₁
        → f a₀ b₀ c₀ d₀ e₀ ~ f a₁ b₁ c₁ d₁ e₁
congᵣᵣᵣᵢᵣ f ~refl ~refl ~refl ~refl = ~refl

~cong : ∀ {i j} {A B : Set i} {P : A → Set j} {Q : B → Set j}
         {f : (x : A) → P x} {g : (x : B) → Q x} → (f ~ g)
         → {a : A} → {b : B} → a ~ b → f a ~ g b
~cong {f = f} {g = g} e₁ {a = a} e₂ with (pi-inj₂ (≡to~ (~to≡ty e₁)))
~cong {f = f} {g = g} ~refl {a = a} ~refl | ~refl = ~refl

postulate ~congᵢᵣ : ∀ {i j k} {A B : Set i}
                    {P : A → Set j} {P' : {a : A} → P a → Set k}
                    {Q : B → Set j} {Q' : {b : B} → Q b → Set k}
                    {f : {a : A} → (x : P a) → P' x} {g : {b : B} → (x : Q b) → Q' x}
                    → _~_ {A = {a : A} → (x : P a) → P' x} f {B = {b : B} → (x : Q b) → Q' x} g
                    → {a : A} → {b : B} → a ~ b
                    → {x : P a} → {y : Q b} → x ~ y → f {a} x ~ g {b} y

-- also provable from the injectivity of irrelevant pi's
postulate ~congₚₛ : ∀ {i j} {A B : Prop i} {P : A → Set j} {Q : B → Set j}
                  {f : (x : A) → P x} {g : (x : B) → Q x} → (f ~ g)
                  → {a : A} → {b : B} → f a ~ g b

funextH : ∀ {i j} {A : Set i} {P : A → Set j} {f g : (x : A) → P x} → ((a : A) → f a ~ g a) → f ~ g
funextH {f = f} {g = g} e = funext λ {_} {b} e' → cong f e' ◼ e b

funextHᵢ : ∀ {i j} {A : Set i} {P : A → Set j} {f g : {x : A} → P x} → ({a : A} → f {a} ~ g {a}) → (λ {x} → f {x}) ~ (λ {x} → g {x})
funextHᵢ {f = f} {g = g} e = funextᵢ λ {_} {b} e' → cong (λ x → f {x}) e' ◼ e {b}

funexth : ∀ {i j} {A : Set i} {P : A → Set j} {Q : A → Set j} {f : (x : A) → P x} {g : (x : A) → Q x}
         → ((a : A) → f a ~ g a) → f ~ g
funexth {f = f} {g = g} e = funext λ {_} {b} e' → cong f e' ◼ e b

funexthᵢ : ∀ {i j} {A : Set i} {P : A → Set j} {Q : A → Set j} {f : {x : A} → P x} {g : {x : A} → Q x}
         → ({a : A} → f {a} ~ g {a}) → (λ {x} → f {x}) ~ (λ {x} → g {x})
funexthᵢ {f = f} {g = g} e = funextᵢ λ {_} {b} e' → cong (λ x → f {x}) e' ◼ e {b}

funextHᵢᵣ : ∀ {i j k} {A : Set i} {P : A → Set j} {Q : (a : A) → P a → Set k} {f g : {x : A} → (y : P x) → Q x y}
          → ({a : A} → (p : P a) → f {a} p ~ g {a} p) → (λ {x} y → f {x} y) ~ (λ {x} y → g {x} y)
funextHᵢᵣ H = funextHᵢ λ {a} → funextH λ p → H p

funexthᵢᵣ : ∀ {i j k} {A : Set i} {P : A → Set j} {Q : (a : A) → P a → Set k} {Q' : (a : A) → P a → Set k}
            {f : {x : A} → (y : P x) → Q x y} {g : {x : A} → (y : P x) → Q' x y}
          → ({a : A} → (p : P a) → f {a} p ~ g {a} p) → (λ {x} y → f {x} y) ~ (λ {x} y → g {x} y)
funexthᵢᵣ H = funexthᵢ λ {a} → funexth λ p → H p

~Jᵢ : ∀ {i j} {A : Set i} {a : A} (P : (b : A) → (a ~ b) → Prop j) (Prefl : P a ~refl) (b : A) (e : a ~ b) → P b e
~Jᵢ P Prefl b ~refl = Prefl

~Jeq : ∀ {i j} {A : Set i} {a : A} (P : (b : A) → (a ~ b) → Set j) (b : A) (e : a ~ b) → P a ~refl ~ P b e
~Jeq P b ~refl = ~refl

~Jeq' : ∀ {i j} {A : Set i} {a : A} (P : (b : A) → (b ~ a) → Set j) (b : A) (e : b ~ a) → P a ~refl ~ P b e
~Jeq' P b ~refl = ~refl

~Jeq₂' : ∀ {i j k} {A : Set i} {B : A → Set j} {a : A} {b : B a} (P : (a' : A) → (a' ~ a) → (b' : B a') → (b' ~ b) → Set k)
           (a' : A) (e₁ : a' ~ a) (b' : B a') (e₂ : b' ~ b) → P a ~refl b ~refl ~ P a' e₁ b' e₂
~Jeq₂' P a' ~refl b' ~refl = ~refl

~J : ∀ {i j} {A : Set i} {a : A} (P : (b : A) → (a ~ b) → Set j) (Prefl : P a ~refl) (b : A) (e : a ~ b) → P b e
~J {a = a} P Prefl b e = coe (~Jeq P b e) Prefl