{-# OPTIONS --with-K #-}
module typhet where

{----------------------------------------------------------------------
Agda code accompanying the paper:

Andrew Pitts "Typal Heterogeneous Equality Types",
ACM Trans. Comput. Logic, 2020
----------------------------------------------------------------------}

open import Agda.Primitive

module Axioms where
----------------------------------------------------------------------
-- Section 2: The axioms and their properties
----------------------------------------------------------------------
  infix   ∑ proof_
  infixr  _≡≡[_]_
  infix   _qed
  infix   _≡≡_ _≡_

  --------------------------------------------------------------------
  -- Figure 1: The Axioms
  --------------------------------------------------------------------

  -- Axioms for typal heterogeneous equality satisfying Axiom K
  postulate
    _≡≡_ : ∀{l}{A B : Set l} → A → B → Set l

  -- the derived homogeneous equality
  _≡_ : ∀{l}{A : Set l} → A → A → Set l
  x ≡ y = x ≡≡ y

  postulate
    rfl :
      ∀{l}{A : Set l}
      (x : A)
      → -------------
      x ≡ x
    ctr :
      ∀{l}{A B : Set l}{x : A}{y : B}
      (e : x ≡≡ y)
      → -----------------------------
      rfl x ≡≡ e
    eqt :
      ∀{l}{A B : Set l}{x : A}{y : B}
      → -----------------------------
      x ≡≡ y → A ≡ B
    tpt :
      ∀{l m n}{A : Set l}{B : A → Set m}
      (C : (x : A) → B x → Set n)
      {x x′ : A}{y : B x}{y′ : B x′}
      → --------------------------------
      x ≡ x′ → y ≡≡ y′ → C x y → C x′ y′

  --Axioms for $\Sigma$-types with surjective pairing
  postulate
    ∑ : ∀{l m}(A : Set l)(B : A → Set m) → Set (l ⊔ m)

  module _ {l m}{A : Set l}{B : A → Set m} where
    infix   _,_
    postulate
      _,_ : (x : A) → B x → ∑ A B
      fst : ∑ A B → A
      snd : (z : ∑ A B) → B (fst z)
      fpr :
        (x : A)
        (y : B x)
        → --------------
        fst (x , y) ≡ x
      spr :
        (x : A)
        (y : B x)
        → --------------
        snd (x , y) ≡≡ y
      eta :
        (z : ∑ A B)
        → -----------------
        (fst z , snd z) ≡ z

  -- concrete syntax for ∑-types
  syntax ∑ A (λ x → B) = ∑ x ∶ A , B

  --------------------------------------------------------------------
  -- Figure 2: Equational reasoning for heterogeneous equality
  --------------------------------------------------------------------
  symm :
    ∀{l}{A B : Set l}{x : A}{y : B}
    → -----------------------------
    x ≡≡ y → y ≡≡ x
  symm e = tpt (λ _ y → y ≡≡ _) (eqt e) e (rfl _)

  proof_ :
    ∀ {l}{A B : Set l}{x : A}{y : B}
    → ------------------------------
    x ≡≡ y → x ≡≡ y
  proof p = p

  _≡≡[_]_ :
    ∀ {l}{A B C : Set l}(x : A){y : B}{z : C}
    → ---------------------------------------
    x ≡≡ y  → y ≡≡ z  → x ≡≡ z
  x ≡≡[ e ] f = tpt (λ _ z → x ≡≡ z) (eqt f) f e

  _qed :
    ∀ {l}{A : Set l}
    (x : A)
    → --------------
    x ≡ x
  x qed = rfl x

  cong :
    ∀{l m}{A : Set l}{B : A → Set m}
    (f : (x : A) → B x)
    {x y : A}
    → ------------------------------
    x ≡ y → f x ≡≡ f y
  cong f {x} e = tpt (λ _ z → f x ≡≡ f z) e e (rfl (f x))

  cong₂ :
    ∀{l m n}{A : Set l}{B : A → Set m}
    {C : (x : A) → B x → Set n}
    (f : (x : A)(y : B x) → C x y)
    {x x′ : A}{y : B x}{y′ : B x′}
    → ---------------------------------
    x ≡ x′ → y ≡≡ y′ → f x y ≡≡ f x′ y′
  cong₂ f {x} {y = y} e e′ =
    tpt (λ x′ y′ → f x y ≡≡ f x′ y′) e e′ (rfl (f x y))

  cong₃ :
    ∀{k l m n}{A : Set k}{B : A → Set l}
    {C : (x : A) → B x → Set m}
    {D : (x : A)(y : B x) → C x y → Set n}
    (f : (x : A)(y : B x)(z : C x y) → D x y z)
    {x x′ : A}{y : B x}{y′ : B x′}{z : C x y}{z′ : C x′ y′}
    → -----------------------------------------------------
    x ≡ x′ → y ≡≡ y′ → z ≡≡ z′ → f x y z ≡≡ f x′ y′ z′
  cong₃ f {x} {_} {y} {_} {z} e e′ =
    tpt (λ x′ y′ → ∀{z′} → z ≡≡ z′ → f x y z ≡≡ f x′ y′ z′)
    e e′ (cong₂ (f x) (rfl y))

  ------------------------------------------------------------------
  -- Lemma 2.1 : A regular coercion function via a version of
  -- Lumsdaine's argument
  ------------------------------------------------------------------

  -- functions that are injective mod ≡
  Inj : ∀{l}(A B : Set l) → Set l
  Inj A B = ∑ f ∶ (A → B) , ∀{x y} → f x ≡ f y → x ≡ y

  -- the identity function is one such
  id : ∀{l}{A : Set l} → A → A
  id x = x

  idInj : ∀{l}(A : Set l) → Inj A A
  idInj _ = (id , id)

  -- an injective coercion function
  icoe : ∀{l}{A B : Set l} → A ≡ B → Inj A B
  icoe {l} {A} e = tpt (λ _ C → Inj A C) (rfl (Set l)) e (idInj A)

  fsticoe : ∀{l}{A : Set l}(x : A)(B : Set l)(e : A ≡ B) → Set l
  fsticoe x B e = ∑ y ∶ B  , (fst (icoe (rfl B)) y ≡ fst (icoe e) x)

  -- coercion function
  coe : ∀{l}{A B : Set l} → A ≡ B → A → B
  coe e x = fst (tpt (fsticoe x) e (ctr e) (x , rfl _))

  -- heterogeneous regularity
  coeIsRegular :
    ∀{l}{A B : Set l}
    (e : A ≡ B)
    (x : A)
    → ---------------
    coe e x ≡≡ x
  coeIsRegular {_} {A} e x =
    tpt (λ _ e′ → coe e′ x ≡≡ x) e (ctr  e) coerfl
    where
    coerfl : coe (rfl A) x ≡ x
    coerfl =
      snd (icoe (rfl A)) (snd (
        tpt (fsticoe x) (rfl A) (ctr (rfl A)) (x , rfl _)))

  ------------------------------------------------------------------
  -- Theorem 2.2: UIP and Axiom K
  ------------------------------------------------------------------
  uip :
    ∀{l}{A : Set l}{x y : A}
    (e e′ : x ≡ y)
    → ----------------------
    e ≡ e′
  uip e e′ = tpt (λ _ e′′ → e′′ ≡≡ e′) e (ctr e) (ctr e′)

  axiomK :
    ∀{l m}{A : Set l}{x : A}
    (P : x ≡ x → Set m)
    (p : P (rfl x))(e : x ≡ x)
    → ------------------------
    P e
  axiomK P p e = coe (cong₂ (λ _ → P) (rfl p) (ctr e)) p

  axiomKComp :
    ∀ {l m}{A : Set l}{x : A}
    (P : x ≡ x → Set m)
    (p : P (rfl x))
    → -----------------------
    axiomK P p (rfl x) ≡ p
  axiomKComp P p =
    coeIsRegular (cong₂ (λ _ → P) (rfl p) (ctr (rfl _))) p

  --------------------------------------------------------------------
  -- Theorem 2.3: Elimination and typal computation properties
  --------------------------------------------------------------------
  ≡Elim :
    ∀{l m}{A : Set l}{x : A}
    (P : (y : A) → x ≡ y → Set m)
    (p : P x (rfl x))(y : A)(e : x ≡ y)
    → ---------------------------------
    P y e
  ≡Elim P p _ e = coe (cong₂ P e (ctr e)) p

  ≡Comp :
    ∀{l m}{A : Set l}{x : A}
    (P : (y : A) → x ≡ y → Set m)
    (p : P x (rfl x))
    → ---------------------------
    ≡Elim P p x (rfl x) ≡ p
  ≡Comp P = coeIsRegular (cong₂ P (rfl _) (ctr (rfl _)))

  ≡≡Elim :
    ∀{l m}{A : Set l}{x : A}
    (P : (B : Set l)(y : B) → x ≡≡ y → Set m)
    (p : P A x (rfl x))(B : Set l)
    (y : B)
    (e : x ≡≡ y)
    → ---------------------------------------
    P B y e
  ≡≡Elim P p _ _ e = coe (cong₃ P (eqt e) e (ctr e)) p

  ≡≡Comp :
    ∀{l m}{A : Set l}{x : A}
    (P : (B : Set l)(y : B) → x ≡≡ y → Set m)
    (p : P A x (rfl x))
    → ---------------------------------------
    ≡≡Elim P p A x (rfl x) ≡ p
  ≡≡Comp P =
    coeIsRegular (cong₃ P (eqt (rfl _)) (rfl _) (ctr (rfl _)))
 
  ------------------------------------------------------------------
  -- Remark 2.5: The role of ∑-types
  ------------------------------------------------------------------
  ∑Elim :
    ∀{l m n}{A : Set l}{B : A → Set m}
    (C : ∑ A B → Set n)
    (c : (x : A)(y : B x) → C (x , y))
    (z : ∑ A B)
    → --------------------------------
    C z
  ∑Elim C c z = coe (cong C (eta z)) (c (fst z) (snd z))

  ∑Comp :
    ∀ {l m n}{A : Set l}{B : A → Set m}
    (C : ∑ A B → Set n)
    (c : (x : A)(y : B x) → C (x , y))
    (x : A)
    (y : B x)
    → --------------------------------
    ∑Elim C c (x , y) ≡ c x y
  ∑Comp C c x y =
    let z = (x , y) in
    proof
      coe (cong C (eta z)) (c (fst z) (snd z))
    ≡≡[ coeIsRegular _ _ ]
      c (fst z) (snd z)
    ≡≡[ cong₂ c (fpr x y) (spr x y) ]
      c x y
    qed

-- end module Axioms

module Consistency where
----------------------------------------------------------------------
-- Section 3: Consistency of the axioms
----------------------------------------------------------------------
  infix   _,_
  infix  _≡≡_ _≡_

  -- Inductive definitions of equality types
  data _≡≡_ {l}{A : Set l} : {B : Set l} → A → B → Set l where
    rfl : (x : A) → x ≡≡ x

  -- Inductive definitions of dependent product types
  data ∑ {l m}(A : Set l)(B : A → Set m) : Set (l ⊔ m) where
    _,_ : (x : A) → B x → ∑ A B

  -- The derived homogeneous equality
  _≡_ : ∀{l}{A : Set l} → A → A → Set l
  x ≡ y = x ≡≡ y

  -- Validation of the axioms
  ctr :
    ∀{l}{A B : Set l}{x : A}{y : B}
    (e : x ≡≡ y)
    → -----------------------------
    rfl x ≡≡ e
  ctr (rfl x) = rfl (rfl x)

  eqt :
    ∀{l}{A B : Set l}{x : A}{y : B}
    → -----------------------------
    x ≡≡ y → A ≡ B
  eqt {_} {A} (rfl _) = rfl A

  tpt :
    ∀{l m n}{A : Set l}{B : A → Set m}
    (C : (x : A) → B x → Set n)
    {x x′ : A}{y : B x}{y′ : B x′}
    → --------------------------------
    x ≡ x′ → y ≡≡ y′ → C x y → C x′ y′
  tpt _ (rfl _) (rfl _) y = y
  -- matching on the first rfl _ pattern in the above definition
  -- is a use of the form of pattern-matching that
  -- relies on the validity of Axiom K

  module _ {l m}{A : Set l}{B : A → Set m} where
    fst : ∑ A B → A
    fst (x , _) = x

    snd : (z : ∑ A B) → B (fst z)
    snd (_ , y) = y

    fpr :
      (x : A)
      (y : B x)
      → -------------
      fst (x , y) ≡ x
    fpr x _ = rfl x

    spr :
      (x : A)
      (y : B x)
      → ---------------
      snd (x , y) ≡≡ y
    spr _ y = rfl y

    eta :
      (z : ∑ A B)
      → -----------------
      (fst z , snd z) ≡ z
    eta (x , y) = rfl (x , y)
--end module RelativeConsistency

module Appendix where
----------------------------------------------------------------------
-- Appendix: typal homogeneous equality without K
----------------------------------------------------------------------

  -- Homogeneous equality types
  postulate
    _≡_ : ∀{l}{A : Set l} → A → A → Set l

  -- Inductive definition of dependent product types
  data ∑ {l m}(A : Set l)(B : A → Set m) : Set (l ⊔ m) where
    _,_ : (x : A) → B x → ∑ A B

  -- concrete syntax for ∑-types
  syntax ∑ A (λ x → B) = ∑ x ∶ A , B

  -- The equality axioms
  postulate
    refl :
      ∀{l}{A : Set l}
      (x : A)
      → -------------
      x ≡ x
    cntr :
      ∀{l}{A : Set l}{x y : A}
      (e : x ≡ y)
      → ----------------------
      (x  , refl x) ≡ (y , e)
    sbst :
      ∀{l m}{A : Set l}
      (B : A → Set m)
      {x y : A}
      → ---------------
      x ≡ y → B x → B y

  -- A regular form of sbst via Lumsdaine's trick

  -- dependent product projections
  module _ {l m}{A : Set l}{B : A → Set m} where
    fst : ∑ A B → A
    fst (x , _ ) = x

    snd : (z : ∑ A B) → B (fst z)
    snd (_ , y) = y

  -- Functions that are injective mod ≡
  Inj : ∀{l}(A B : Set l) → Set l
  Inj A B = ∑ f ∶ (A → B) , ∀{x y} → f x ≡ f y → x ≡ y

  -- The identity function is one such
  id : ∀{l}{A : Set l} → A → A
  id x = x

  idInj : ∀{l}(A : Set l) → Inj A A
  idInj _ = (id , id)

  -- Construction of subst and substIsRegular:
  module _ {l m}{A : Set l}(B : A → Set m){x : A} where
    Inj₂ :
      {y z : A}
      → -----------------------------
      x ≡ y → x ≡ z → Inj (B y) (B z)
    Inj₂ {y} p q =
      sbst (λ z' → Inj (B y) (B z')) q
       (sbst (λ y' → Inj (B y') (B x)) p (idInj (B x)))

    sbst₂ :
      {y z : A}
      → -----------------------
      x ≡ y → x ≡ z → B y → B z
    sbst₂ p q = fst (Inj₂ p q)

    C :
      {y : A}
      (p : x ≡ y)
      (b : B x)
      → --------------------------------------------
      ∑ c ∶ B y , (sbst₂ p p c ≡ sbst₂ (refl x) p b)
    C p b = sbst C' (cntr p) (b , refl _)
      where
      C' : ∑ y ∶ A , (x ≡ y) → Set m
      C' (y , p) =
        ∑ c ∶ B y , (sbst₂ p p c ≡ sbst₂ (refl x) p b)

    subst :
      {y : A}
      → ---------------
      x ≡ y → B x → B y
    subst p b = fst (C p b)

    substIsRegular :
      (b : B x)
      → ------------------
      subst (refl x) b ≡ b
    substIsRegular b =
      snd (Inj₂ (refl x) (refl x)) (snd (C (refl x) b))

-- end module Appendix