[Agda] Univalence via Agda's primTrustMe?

[Alan Jeffrey]

Hi everyone,

In the Agda development of Homotopy Type Theory at 
https://github.com/HoTT/HoTT-Agda/ the univalence axiom is given by 
three postulates (the map from (A ≃ B) to (A ≡ B) and its β and η rules).

I wonder whether these postulates could be replaced by uses of primTrustMe?

As a reminder, primTrustMe is a trusted function which inhabits the type 
(M ≡ N) for any M and N. It is possible to introduce contradictions 
(e.g. 0 ≡ 1) in the same way as with postulates, so it has to be handled 
with care. The semantics is as for postulates, but with an extra beta 
reduction:

   primTrustMe M M → refl

In the attached Agda code, primTrustMe is used to define:

   private
     trustme : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (∃ q ∙ ((≡-to-≃ q) ≡ p))
     trustme p = ⟨ primTrustMe , primTrustMe ⟩

from which we get the map from (A ≃ B) to (A ≡ B) and its β rule:

   ≃-to-≡ : ∀ {ℓ} {A B : Set ℓ} → (A ≃ B) → (A ≡ B)
   ≃-to-≡ p with trustme p
   ≃-to-≡ .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl

   ≃-to-≡-β : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (≡-to-≃ (≃-to-≡ p) ≡ p)
   ≃-to-≡-β p with trustme p
   ≃-to-≡-β .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl

Interestingly, the η rule and the coherence property for β and η then 
become trivial:

   ≃-to-≡-η : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → (≃-to-≡ (≡-to-≃ p) ≡ p)
   ≃-to-≡-η refl = refl

   ≃-to-≡-τ : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) →
     (cong ≡-to-≃ (≃-to-≡-η p) ≡ ≃-to-≡-β (≡-to-≃ p))
   ≃-to-≡-τ refl = refl

Note there's some hoop-jumping with private declarations to hide trustme 
from users, because:

   (fst (trustme p)) → refl  (for any p : (A ≃ A))

that is, all proofs of (A ≃ A) would be identified if we were allowed 
unfettered access to trustme. Instead, we only allow (≃-to-≡ p) to 
reduce to refl when (trustme p) reduces to ⟨ refl , refl ⟩, that is not 
only do we have (A ≃ A) but also that p must be the trivial proof that 
(A ≃ A).

Now, this isn't a conservative extension of HOTT because it introduces 
extra beta reductions that were previously just propositional 
equalities, in particular:

   (≃-to-≡ (≡-to-≃ refl)) → refl
   (≃-to-≡-β (≡-to-≃ refl)) → refl
   (≃-to-≡-η refl) → refl
   (≃-to-≡-τ refl) → refl

So questions... a) Is this re-inventing the wheel? b) Is this sound? c) 
Is there a connection between this and a computational interpretation of 
univalence?

Alan.
-------------- next part --------------
{-# OPTIONS --without-K #-}

open import Level

module UnivalenceViaPrimTrustMe where

-- Existential quantification

record Σ {ℓ} {A : Set ℓ} (B : A → Set ℓ) : Set ℓ where
  constructor ⟨_,_⟩
  field a : A
  field b : B a

syntax Σ (λ a → b) = ∃ a ∙ b

-- Propositional equality

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

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

private primitive primTrustMe : ∀ {ℓ} {A : Set ℓ} {a b : A} → (a ≡ b)

cong :  ∀ {ℓ} {A B : Set ℓ} {a b} → (f : A → B) → (a ≡ b) → (f a ≡ f b)
cong f refl = refl

-- Equivalence between types
-- This defn uses half-adjoint equivalences (sec 4.2 of the HOTTBook)

record IsEquiv {ℓ} {A B : Set ℓ} (f : A → B) : Set ℓ where
  constructor ⟨_,_,_,_⟩
  field g : B → A
  field η : ∀ a → g(f a) ≡ a
  field ε : ∀ b → f(g b) ≡ b
  field τ : ∀ a → cong f(η a) ≡ ε(f a)

record _≃_ {ℓ} (A B : Set ℓ) : Set (suc ℓ) where
  constructor ⟨_,_⟩
  field f : A → B
  field f✓ : IsEquiv(f)

-- Equality implies equivalence

id : ∀ {ℓ} {A : Set ℓ} → A → A
id = λ a → a

id✓ : ∀ {ℓ} {A : Set ℓ} → IsEquiv(id {ℓ} {A})
id✓ = ⟨ id , (λ a → refl) , (λ a → refl) , (λ a → refl) ⟩

≡-to-≃ : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) → (A ≃ B)
≡-to-≃ {ℓ} {A} refl = ⟨ id , id✓ ⟩

-- We use primTrustMe twice, in defining the map from (p : A ≃ B) to (∃ q ∙ ((≡-to-≃ q) ≡ p))
-- From this we define ≃-to-≡ and ≃-to-≡-β by pattern-matching on trustme p.
-- Note that both primTrustMe instances have to beta-reduce to refl
-- in order for ≃-to-≡ p to reduce to refl. In particular,
-- if (p : (A ≃ A)) then (≃-to-≡ p) does not reduce to refl in general,
-- only when p is ⟨ id , id✓ ⟩.

private 
  -- trustme is not safe in general, since fst(trustme p)
  -- would beta-reduce to refl for any (p : A ≃ A),
  -- so we define it as private to stop it escaping.
  trustme : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (∃ q ∙ ((≡-to-≃ q) ≡ p))
  trustme p = ⟨ primTrustMe , primTrustMe ⟩

-- Equivalence implies equality

≃-to-≡ : ∀ {ℓ} {A B : Set ℓ} → (A ≃ B) → (A ≡ B)
≃-to-≡ p with trustme p
≃-to-≡ .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl

≃-to-≡-β : ∀ {ℓ} {A B : Set ℓ} (p : A ≃ B) → (≡-to-≃ (≃-to-≡ p) ≡ p)
≃-to-≡-β p with trustme p
≃-to-≡-β .(≡-to-≃ refl) | ⟨ refl , refl ⟩ = refl

≃-to-≡-η : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → (≃-to-≡ (≡-to-≃ p) ≡ p)
≃-to-≡-η refl = refl

≃-to-≡-τ : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → (cong ≡-to-≃ (≃-to-≡-η p) ≡ ≃-to-≡-β (≡-to-≃ p))
≃-to-≡-τ refl = refl

-- These are enough to give univalence

univalence : ∀ {ℓ} {A B : Set ℓ} → IsEquiv(≡-to-≃ {ℓ} {A} {B})
univalence = ⟨ ≃-to-≡ , ≃-to-≡-η , ≃-to-≡-β , ≃-to-≡-τ ⟩

-- In particular, equality is equivalent to equivalence

≡-equiv-≃ : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)
≡-equiv-≃ = ⟨ ≡-to-≃ , univalence ⟩