{-# 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 =
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  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