{-# 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  1  proof_
  infixr 2 _≡≡[_]_
  infix  3 _qed
  infix  4 _≡≡_ _≡_

  --------------------------------------------------------------------
  -- 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  3 _,_
    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 =
    proof
      coe (cong₂  _  P) (rfl p) (ctr (rfl _))) p
    ≡≡[ cong  e  coe e p) (uip _ _) ]
      coe (rfl _) p
    ≡≡[ coeIsRegular _ p ]
      p
    qed

  --------------------------------------------------------------------
  -- 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 p =
    proof
      coe (cong₂ P (rfl _) (ctr (rfl _))) p
      ≡≡[ cong  e  coe e p) (symm (ctr _)) ]
      coe (rfl _) p
    ≡≡[ coeIsRegular _ p ]
      p
    qed

  ≡≡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 p =
    proof
      coe (cong₃ P (eqt (rfl _)) (rfl _) (ctr (rfl _))) p
    ≡≡[ cong  e  coe e p) (uip _ _) ]
      coe (rfl _) p
    ≡≡[ coeIsRegular _ p ]
      p
    qed

  ------------------------------------------------------------------
  -- 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  3 _,_
  infix 4 _≡≡_ _≡_

  -- 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