[Agda] Univalence via Agda's primTrustMe again

[Alan Jeffrey]

Hi all,

OK, I made another shot at a computational version of univalence, using 
Agda's primTrustMe to get beta-reduction.

In the attached Agda code, there's a construction of the 2-categorical 
version of univalence such that many of the equivalences are 
beta-reductions. In particular:

   ap(ua(e))(a)  beta reduces to  e(a)

I only did the 2-categorical version, which lifts up the skeletal 
equivalence on Set_0 to a non-skeletal equivalence on Set_1. It would be 
interesting to see if it goes through for any Set_n, to get an 
n-categorical model, but this may require more book-keeping than I am 
capable of.

Let ≣ be the skeletal equivalence satisfying K.

The identity type on Set₀ is (a ≡₀ b) whenever (a ≣ b). From this, we 
can define (A ≃₁ B : Set₀) as per usual (half-adjoint equivalences).

The definition of the identity type on Set₁ is (a ≡₁ b : A) whenever:

- p : (a ≣ b)
- q : ∀ C → (C a ≃₁ C b)
- r : ∀ C D → (q (C ∘ D)) ≣ (≃₁-cong C (q D))

from which we can define (A ≃₂ B : Set₁), and show the 2-categorical 
version of univalence:

   (A ≡₁ B) ≃₂ (A ≃₁ B)

The Agda trick to getting beta-reductions is that from:

   trustMe : ∀ (a b : A) → (a ≣ b)

we can build:

   POSTULATE[_↦_] : ∀ (a : A) (b : B a) → (∀ a → B a)
   POSTULATE[ a ↦ b ] a′ with trustMe a a′
   POSTULATE[ a ↦ b ] .a | refl = b

Since trustMe a a beta-reduces to refl, (POSTULATE[ a ↦ b ] a) 
beta-reduces to b. We can use this to make some of the coherence 
conditions definitional equalities, not just propositional ones. For 
example, the congruence property for equivalence can be defined:

   ≃₁-cong : ∀ {A B} C → (A ≃₁ B) → (C A ≃₁ C B)
   ≃₁-cong = POSTULATE[ id ↦ id ]

which means that (≃₁-cong id e) beta-reduces to e. From this, we get 
that ap(ua(e))(a) beta reduces to e(a).

One restriction is that the only beta-reduction on postulates is the one 
given. This is good because we can't introduce nondeterminism, but bad 
because we only get one beta-reduction per term, so we have to choose 
carefully which propositional equality to make definitional.

Thoughts? Is the construction of ≡₁ as a contextual equivalence 
generated by ≃₁ new?

Alan.
-------------- next part --------------
open import Level using (Level ; zero ; suc ; _⊔_ )

module UnivalenceViaPrimTrustMe2 where

-- Function identity and composition

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

_∘_ : ∀ {ℓ} {A B C : Set ℓ} → (B → C) → (A → B) → (A → C)
(f ∘ g) a = f(g a)

-- Skeletal propositional equality

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

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

≣-uniq : ∀ {ℓ} {A : Set ℓ} {a b : A} → (p q : a ≣ b) → (p ≣ q)
≣-uniq ≣-refl ≣-refl = ≣-refl -- Requires K

≣-sym : ∀ {ℓ} {A : Set ℓ} {a b : A} → (a ≣ b) → (b ≣ a)
≣-sym ≣-refl = ≣-refl

≣-trans : ∀ {ℓ} {A : Set ℓ} {a b c : A} → (a ≣ b) → (b ≣ c) → (a ≣ c)
≣-trans ≣-refl ≣-refl = ≣-refl

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

≣-cong₂ : ∀ {ℓ m n} {A : Set ℓ} {B : Set m} {C : Set n} → (f : A → B → C) → ∀ {a b c d} → (a ≣ b) → (c ≣ d) → (f a c ≣ f b d)
≣-cong₂ f ≣-refl ≣-refl = ≣-refl

≣-cong-id : ∀ {ℓ} {A : Set ℓ} {a b : A} (p : a ≣ b) → (≣-cong id p ≣ p)
≣-cong-id ≣-refl = ≣-refl

≣-cong-dist-∘ : ∀ {ℓ} {A B C : Set ℓ} (f : B → C) (g : A → B) {a b : A} (p : a ≣ b) →
  (≣-cong (f ∘ g) p) ≣ (≣-cong f (≣-cong g p))
≣-cong-dist-∘ f g ≣-refl = ≣-refl

private 

  -- (trustMe a b) has type (a ≣ b) for any a and b, handle with care!

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

  trustMe : ∀ {ℓ} {A : Set ℓ} (a b : A) → (a ≣ b)
  trustMe a b = primTrustMe

  -- (trustMe a a) beta reduces to ≣-refl
  -- we can use this to postulate a function POSTULATE[ a ↦ b ]
  -- such that (POSTULATE[ a ↦ b ] a) beta reduces to b
  -- Note that there is no way AFAIK to allow more than one beta-reduction
  -- so we can't introduce nondeterminism this way
  
  POSTULATE[_↦_] : ∀ {ℓ m} {A : Set ℓ} {B : A → Set m} (a : A) (b : B a) → (∀ a → B a)
  POSTULATE[ a ↦ b ] a′ with trustMe a a′
  POSTULATE[ a ↦ b ] .a | ≣-refl = b

-- For example, we can introduce dependent function extensionality,
-- in such a way that (≣-dext (λ x → ≣-refl)) beta reduces to ≣-refl

≣-dext : ∀ {ℓ m} {A : Set ℓ} {B : A → Set m} {f g : ∀ a → B a} → (∀ a → f a ≣ g a) → (f ≣ g)
≣-dext {f = f} {g = g} = P g where

  P : ∀ g → (∀ a → f a ≣ g a) → (f ≣ g)
  P = POSTULATE[ f ↦ POSTULATE[ (λ a → ≣-refl) ↦ ≣-refl ] ]

-- (≣-dext (λ x → ≣-refl)) is definitionally equal to ≣-refl

≣-dext-refl : ∀ {ℓ m} {A : Set ℓ} {B : A → Set m} {f : ∀ a → B a} → (≣-dext {f = f} (λ x → ≣-refl)) ≣ ≣-refl
≣-dext-refl = ≣-refl

-- Equality on Set₀ is skeletal

record _≡₀_ {A : Set₀} (a b : A) : Set where
  constructor ⟨_⟩
  field p : (a ≣ b)

≡₀-cong : ∀ {A B} (f : A → B) {a b} → (a ≡₀ b) → (f a ≡₀ f b)
≡₀-cong f ⟨ p ⟩ = ⟨ ≣-cong f p ⟩

≡₀-refl : ∀ {A} {a : A} → (a ≡₀ a)
≡₀-refl = ⟨ ≣-refl ⟩

≡₀-sym : ∀ {A} {a b : A} → (a ≡₀ b) → (b ≡₀ a)
≡₀-sym ⟨ p ⟩ = ⟨ ≣-sym p ⟩

≡₀-trans : ∀ {A} {a b c : A} → (a ≡₀ b) → (b ≡₀ c) → (a ≡₀ c)
≡₀-trans ⟨ p ⟩ ⟨ q ⟩ = ⟨ ≣-trans p q ⟩

≡₀-uniq : ∀ {A} {a b : A} (p q : a ≡₀ b) → (p ≡₀ q)
≡₀-uniq ⟨ p ⟩ ⟨ q ⟩ = ⟨ (≣-cong ⟨_⟩ (≣-uniq p q)) ⟩

-- Equivalence

record _≃₁_ (A B : Set₀) : Set₁ where
  constructor ⟨_,_,_,_,_⟩
  field f : A → B
  field f⁻¹ : B → A
  field η : ∀ a → f⁻¹(f a) ≡₀ a
  field ε : ∀ b → f(f⁻¹ b) ≡₀ b
  field τ : ∀ a → ≡₀-cong f(η a) ≡₀ ε(f a)
open _≃₁_ using () renaming (f to apply₁ ; f⁻¹ to apply₁⁻¹ ; η to apply₁-η ; ε to apply₁-ε ; τ to apply₁-τ )

-- The identity function is an equivalence

≃₁-refl : ∀ {A} → (A ≃₁ A)
≃₁-refl = ⟨ id , id , (λ a → ≡₀-refl) , (λ a → ≡₀-refl) , (λ a → ≡₀-refl) ⟩

-- Swapping preserves equvalence

≃₁-sym : ∀ {A B} → (A ≃₁ B) → (B ≃₁ A)
≃₁-sym ⟨ f , f⁻¹ , η , ε , τ ⟩ = ⟨ f⁻¹ , f , ε , η , σ ⟩ where

  σ : ∀ b → ≡₀-cong f⁻¹ (ε b) ≡₀ η (f⁻¹ b)
  σ b = ≡₀-uniq _ _ -- This is actually provable directly, using the fact that ≣ is skeletal is just lazy

-- Function composition respects equivalence

≃₁-trans : ∀ {A B C} → (A ≃₁ B) → (B ≃₁ C) → (A ≃₁ C)
≃₁-trans ⟨ f , f⁻¹ , η , ε , τ ⟩ ⟨ g , g⁻¹ ,  η′ , ε′ , τ′ ⟩ =
  ⟨ (g ∘ f)
  , (f⁻¹ ∘ g⁻¹)
  , (λ a → ≡₀-trans (≡₀-cong f⁻¹ (η′ (f a))) (η a))
  , (λ b → ≡₀-trans (≡₀-cong g (ε (g⁻¹ b))) (ε′ b))
  , (λ a → ≡₀-uniq _ _) ⟩

-- If (A ≣ B) then (A ≃₁ B)

≣-to-≃₁ : ∀ {A B : Set₀} → (A ≣ B) → (A ≃₁ B)
≣-to-≃₁ ≣-refl = ⟨ id , id , (λ a → ≡₀-refl) , (λ a → ≡₀-refl) , (λ a → ≡₀-refl) ⟩

-- Univalence implies that (A ≃₁ B) implies (A ≣ B)

≃₁-to-≣ : ∀ {A B} → (A ≃₁ B) → (A ≣ B)
≃₁-to-≣ {A} {B} = f B where

  f : ∀ B → (A ≃₁ B) → (A ≣ B)
  f = POSTULATE[ A ↦ POSTULATE[ ≃₁-refl ↦ ≣-refl ] ]

-- ≃₁-to-≣ ≃₁-refl is definitionally equal to ≣-refl

≃₁-to-≣-refl : ∀ A → (≃₁-to-≣ (≃₁-refl {A})) ≣ ≣-refl
≃₁-to-≣-refl A = ≣-refl

-- Univalence implies that ≃₁ is a congruence

≃₁-cong-via-≣ : ∀ {A B} C → (A ≃₁ B) → (C A ≃₁ C B)
≃₁-cong-via-≣ C e = ≣-to-≃₁ (≣-cong C (≃₁-to-≣ e))

-- We postulate a congruence which respects identity

≃₁-cong : ∀ {A B} C → (A ≃₁ B) → (C A ≃₁ C B)
≃₁-cong = POSTULATE[ id ↦ id ]

-- (≃₁-cong id e) is definitionally equal to e

≃₁-cong-id : ∀ {A B} (e : A ≃₁ B) → (≃₁-cong id e) ≣ e
≃₁-cong-id e = ≣-refl

-- We also postulate that ≃₁-cong respects composition, refl, sym and trans
-- but we don't require any β-reductions for these.

postulate ≃₁-cong-∘ : ∀ C D {A B} (e : A ≃₁ B) → (≃₁-cong (C ∘ D) e) ≣ (≃₁-cong C (≃₁-cong D e))
postulate ≃₁-cong-refl : ∀ {A} C → (≃₁-cong C (≃₁-refl {A})) ≣ ≃₁-refl
postulate ≃₁-cong-sym : ∀ F {A B} (e : A ≃₁ B) → (≃₁-cong F (≃₁-sym e)) ≣ (≃₁-sym (≃₁-cong F e))
postulate ≃₁-cong-trans : ∀ F {A B C} (d : A ≃₁ B) (e : B ≃₁ C) → (≃₁-cong F (≃₁-trans d e)) ≣ (≃₁-trans (≃₁-cong F d) (≃₁-cong F e))

-- Unfortunately, this isn't a good computational model of univalence,
-- as it doesn't have "enough" beta-reductions.
-- In particular, (ap₀ (≃₁-to-≣ e) a) does not beta reduce to (apply₁ e a)
-- since (≃₁-to-≣ e) beta reduces to (primTrustMe) and so e
-- has been lost.

-- We fix this by introducing a new type (a ≡₁ b) which keeps track of
-- an equivalence as well as a proof of (a ≣ b). However we do not
-- necessarily have that a and b are sets, they can be of any type. We
-- fix that by using a contextual equivalence: (a ≡₁ b) implies that
-- (C a ≃₁ C b) for any context C.

-- This introduces too many inhabitants of (a ≡₁ b) since 
-- there is nothing relating the witness of (C a ≃₁ C b)
-- with the witness of (D a ≃₁ D b). We fix this by requiring
-- q to be a functor.

-- The idea is that (a ≣ b) is the "skeleton" of (a ≡₁ b), it just
-- records that a and b are equal, not why they are equal.

-- Rather annoyingly, for cardinality reasons we need to keep the proof
-- of (a ≣ b) explicitly. If q could be given the type
-- q : ∀ (C : A → Set (ℓ + 1)) → (C a ≃₁ C b)
-- then we would have apply₁ (q (λ x → (a ≣ x))) ≣-refl
-- as our witness of (a ≣ b).

-- Note that this is just the 2-categorical version, not the n-categorical
-- or ω-categorical version. We could iterate these definitions,
-- so (a ≡₂ b) : Set (ℓ + 2), (a ≡₃ b) : Set (ℓ + 3), ...
-- but there would be some care in doing so, as there are places
-- I've been lazy and used ≣-uniq, and there are probably extra coherence
-- conditions required. In particular there should be a proof
-- that the map from _≡₂_ to _≡₁_ gives the same path as the map from 
-- _≡₂_ to _≃₂_. 

record _≡₁_ {A : Set₁} (a b : A) : Set₁ where
  constructor ⟨_,_,_⟩
  field p : a ≣ b
  field q : ∀ C → (C a ≃₁ C b)
  field r : ∀ C D → (q (C ∘ D)) ≣ (≃₁-cong C (q D))
open _≡₁_ public using () renaming (p to ≡₁-to-≣ ; q to ≡₁-to-≃₁-cong ; r to ≡₁-to-≃₁-cong-∘ )

-- ≣ implies ≡₁ 

≣-to-≡₁ : ∀ {A} {a b : A} → (a ≣ b) → (a ≡₁ b)
≣-to-≡₁ ≣-refl = ⟨ ≣-refl , (λ C → ≃₁-refl) , (λ C D → ≣-sym (≃₁-cong-refl C)) ⟩

-- ≡₁ implies ≃₁
≡₁-to-≃₁ : ∀ {A B} → (A ≡₁ B) → (A ≃₁ B)
≡₁-to-≃₁ p = ≡₁-to-≃₁-cong p id

-- ≃₁ implies ≡₁

≃₁-to-≡₁ : ∀ {A B} → (A ≃₁ B) → (A ≡₁ B)
≃₁-to-≡₁ e = ⟨ (≃₁-to-≣ e) , (λ C → ≃₁-cong C e) , (λ C D → ≃₁-cong-∘ C D e) ⟩

-- ≡₁ is reflexive

≡₁-refl : ∀ {A} {a : A} → (a ≡₁ a)
≡₁-refl = 
  ⟨ ≣-refl
  , (λ C → ≃₁-refl) 
  , (λ C D → ≣-sym (≃₁-cong-refl C)) ⟩

-- ≡₁ is symmetric

≡₁-sym : ∀ {A} {a b : A} → (a ≡₁ b) → (b ≡₁ a)
≡₁-sym ⟨ p , q , r ⟩ = 
  ⟨ ≣-sym p
  , (λ C → ≃₁-sym (q C))
  , (λ C D → ≣-trans (≣-cong ≃₁-sym (r C D)) (≣-sym (≃₁-cong-sym C (q D)))) ⟩

-- ≡₁ is transitive

≡₁-trans : ∀ {A} {a b c : A} → (a ≡₁ b) → (b ≡₁ c) → (a ≡₁ c)
≡₁-trans ⟨ p₁ , q₁ , r₁ ⟩ ⟨ p₂ , q₂ , r₂ ⟩ = 
  ⟨ ≣-trans p₁ p₂
  , (λ C → ≃₁-trans (q₁ C) (q₂ C))
  , (λ C D → ≣-trans (≣-cong₂ ≃₁-trans (r₁ C D) (r₂ C D)) (≣-sym (≃₁-cong-trans C (q₁ D) (q₂ D)))) ⟩

-- ≡₁ is a congruence

≡₁-cong : ∀ {A B} (f : A → B) {a b : A} → (a ≡₁ b) → (f a ≡₁ f b)
≡₁-cong f p = ⟨ ≣-cong f (≡₁-to-≣ p) , (λ C → ≡₁-to-≃₁-cong p (C ∘ f)) , (λ C D → ≡₁-to-≃₁-cong-∘ p C (D ∘ f)) ⟩

-- ap₁ p just extracts the function from p

ap₁ : ∀ {A B} → (A ≡₁ B) → (A → B)
ap₁ p = apply₁ (≡₁-to-≃₁ p)

ap₁⁻¹ : ∀ {A B} → (A ≡₁ B) → (B → A)
ap₁⁻¹ p = apply₁⁻¹ (≡₁-to-≃₁ p)

-- (ap₁ (≃₁-to-≡₁ e)) is definitionally equal to (apply₁ e)

ap₁-β : ∀ {A B} (e : A ≃₁ B) → (ap₁ (≃₁-to-≡₁ e)) ≣ (apply₁ e)
ap₁-β e = ≣-refl

-- ≡₁-to-≃₁ (≃₁-to-≡₁ e) is definitionally equal to p

≡₁-to-≃-ε : ∀ {A B} (e : A ≃₁ B) → (≡₁-to-≃₁ (≃₁-to-≡₁ e)) ≡₁ e
≡₁-to-≃-ε e = ≡₁-refl

-- ≃₁-to-≡₁ (≡₁-to-≃₁ p) is propositionally equal to p

≡₁-to-≃₁-η-lemma : ∀ {A B} (p q : A ≡₁ B) → (q ≣ ≃₁-to-≡₁ (≡₁-to-≃₁ p)) → (q ≡₁ p)
≡₁-to-≃₁-η-lemma p ⟨ a  , b  , c  ⟩ H with ≣-trans (≣-cong ≡₁-to-≣ H) (≣-uniq (≡₁-to-≣ (≃₁-to-≡₁ (≡₁-to-≃₁ p))) (≡₁-to-≣ p))
≡₁-to-≃₁-η-lemma p ⟨ ._ , b  , c  ⟩ H | ≣-refl with ≣-trans (≣-cong ≡₁-to-≃₁-cong H) (≣-dext (λ C → ≣-sym (≡₁-to-≃₁-cong-∘ p C id)))
≡₁-to-≃₁-η-lemma p ⟨ ._ , ._ , c  ⟩ H | ≣-refl | ≣-refl with (≣-dext (λ C → ≣-dext (λ D → ≣-uniq (c C D) (≡₁-to-≃₁-cong-∘ p C D))))
≡₁-to-≃₁-η-lemma p ⟨ ._ , ._ , ._ ⟩ H | ≣-refl | ≣-refl | ≣-refl = ≡₁-refl

≡₁-to-≃₁-η : ∀ {A B} (p : A ≡₁ B) → (≃₁-to-≡₁ (≡₁-to-≃₁ p)) ≡₁ p
≡₁-to-≃₁-η p = ≡₁-to-≃₁-η-lemma p _ ≣-refl

-- These equalities are inverses

≡₁-to-≃₁-τ-lemma :  ∀ {A B} (p q : A ≡₁ B) → (H : q ≣ ≃₁-to-≡₁ (≡₁-to-≃₁ p)) → (≡₁-cong ≡₁-to-≃₁ (≡₁-to-≃₁-η-lemma p q H)) ≡₁ (≡₁-cong ≡₁-to-≃₁ (≣-to-≡₁ H))
≡₁-to-≃₁-τ-lemma {A} {B} p ⟨ a  , b  , c  ⟩ H with ≣-trans (≣-cong ≡₁-to-≣ H) (≣-uniq (≡₁-to-≣ (≃₁-to-≡₁ (≡₁-to-≃₁ p))) (≡₁-to-≣ p))
≡₁-to-≃₁-τ-lemma {A} {B} p ⟨ ._ , b  , c  ⟩ H | ≣-refl with ≣-trans (≣-cong ≡₁-to-≃₁-cong H) (≣-dext (λ C → ≣-sym (≡₁-to-≃₁-cong-∘ p C id)))
≡₁-to-≃₁-τ-lemma {A} {B} p ⟨ ._ , ._ , c  ⟩ H | ≣-refl | ≣-refl with (≣-dext (λ C → ≣-dext (λ D → ≣-uniq (c C D) (≡₁-to-≃₁-cong-∘ p C D))))
≡₁-to-≃₁-τ-lemma {A} {B} p ⟨ ._ , ._ , ._ ⟩ H | ≣-refl | ≣-refl | ≣-refl = lemma H ≣-refl where

  lemma : ∀ {r} (H : p ≣ r) (I : (≡₁-to-≃₁ p) ≣ (≡₁-to-≃₁ r)) → (≣-to-≡₁ I) ≡₁ (≡₁-cong ≡₁-to-≃₁ (≣-to-≡₁ H))
  lemma ≣-refl ≣-refl = ≡₁-refl

≡₁-to-≃₁-τ : ∀ {A B} (p : A ≡₁ B) → (≡₁-cong ≡₁-to-≃₁ (≡₁-to-≃₁-η p)) ≡₁ (≡₁-to-≃-ε (≡₁-to-≃₁ p))
≡₁-to-≃₁-τ p = ≡₁-to-≃₁-τ-lemma p _ ≣-refl

-- Lift ≃ up a level

record _≃₂_ (A B : Set₁) : Set₂ where
  constructor ⟨_,_,_,_,_⟩
  field f : A → B
  field f⁻¹ : B → A
  field η : ∀ a → f⁻¹(f a) ≡₁ a
  field ε : ∀ b → f(f⁻¹ b) ≡₁ b
  field τ : ∀ a → ≡₁-cong f(η a) ≡₁ ε(f a)
open _≃₂_ using () renaming (f to apply₂ ; f⁻¹ to apply₂⁻¹ ; η to apply₂-η ; ε to apply₂-ε ; τ to apply₂-τ )

-- Univalence

univalence₁ : ∀ {A B} → (A ≡₁ B) ≃₂ (A ≃₁ B)
univalence₁ = ⟨ ≡₁-to-≃₁ , ≃₁-to-≡₁ , ≡₁-to-≃₁-η , ≡₁-to-≃-ε , ≡₁-to-≃₁-τ ⟩