[Agda] Re: Univalence via Agda's primTrustMe again^2

[Alan Jeffrey]

Sorry for the spam...

I managed to prove what were previously postulates. The remaining 
postulates are J, and the congruence rule for ≃. Univalence follows from 
these, using the inductive definition of ≡.

I am a bit surprised by this, am I missing something?

A.

On 02/17/2015 12:02 PM, Alan Jeffrey wrote:
> Hi everyone,
>
> Here is a very tidied up version of how Agda's primTrustMe can be used
> to define a model in which univalence holds...
>
> The idea is to define equivalence and identity types by induction of
> universe level. At level n, (A ≃ B) is the usual definition of
> half-adjoint equivalence, which uses ≡ at level n. At level 0, (a ≡ b)
> is just skeletal propositional equality. At level n+1, (a ≡ b) is
> defined to be ∀ F → (F a ≃ F b).
>
> We can postulate J, with its beta reduction rule (using Agda's
> primTrustMe to define postulates with beta-reductions).
>
> Part of univalence is postulating that ≃ is a congruence, that is there
> is a term cong F : (A ≃ B) → (F A ≃ F B). Somewhat annoyingly, this has
> two obvious beta-reductions:
>
>    (cong F refl)  -->  refl
>      (cong id p)  -->  p
>
> Agda doesn't allow such nondeterminism, so in the Agda development I
> introduced two congruence rules, cong and cong′. From cong, we can
> define ua (and ditto ua′) as:
>
>    ua : (A ≃ B) -> (A ≡ B)
>    ua p F = cong F p
>
> These have inverses, with type:
>
>    ua⁻¹ : (A ≡ B) -> (A ≃ B)
>
> The inverse of ua is the usual extension of the identity function using
> J. The invrse of ua′ is:
>
>    ua′⁻¹ p = p id
>
> and we can check that ua′⁻¹ (ua′ e) beta reduces to e. To get
> univalence, we postulate that ua and ua′ are equivalent, that ua⁻¹ and
> ua′⁻¹ are equivalent, and a beta-reduction saying that everything
> collapses on reflexivity:
>
>    ua≡ua′ : ∀ e → (ua n e ≡ ua′ n e)
>    ua⁻¹≡ua′⁻¹-cong : (p ≡ q) → (ua⁻¹ n p ≡ ua′⁻¹ n q)
>    (ua⁻¹≡ua′⁻¹-cong (ua≡ua′ (ua⁻¹ refl)))  -->  refl
>
>  From these, we get univalence.
>
> All comments welcome...
>
> Alan.
-------------- next part --------------
open import Level using (Level ; zero ; suc ; _⊔_ )

module UnivalenceViaPrimTrustMe4 where

-- Identity and composition of functions

id : ∀ {ℓ} {A : Set ℓ} → A → A
id x = x

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

-- Skeletal propositional equality

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

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

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

-- Postulates which beta-reduce

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

  POSTULATE[_↦_] : ∀ {ℓ m} {A : Set ℓ} {B : A → Set m} → ∀ a → B a → (∀ a → B a)
  POSTULATE[ a ↦ b ] a′ with trustMe a a′
  POSTULATE[ a ↦ b ] .a | ≣-refl = b

-- Natural numbers

data ℕ : Set where
  O : ℕ
  _+1 : ℕ → ℕ

-- Induction over universe levels

level : ℕ → Level
level O = zero
level (n +1) = suc (level n)

Type : ∀ n → Set (level (n +1))
Type n = Set (level n)

-- Equivalence and identity types defined as contextual equivalence
-- (a ≡ b) at level 0 whenever (a ≣ b)
-- (a ≡ b) at level n+1 whenever for every F, (F a ≃ F b) at level n
-- (A ≃ B) at level n is half-adjoint equivalence, using ≡ at level n
-- Note that this definition is by inudction on universe level

Type_∋_∋_≡_ : ∀ n (A : Type n) (a b : A) → Type n
≡-cong : ∀ n {A B : Type n} (f : A → B) {x y : A} → (Type n ∋ A ∋ x ≡ y) → (Type n ∋ B ∋ f x ≡ f y)
record Type_∋_≃_ n (A B : Type n) : Type (n +1)

(Type O      ∋ A ∋ a ≡ b) = (a ≣ b)
(Type (n +1) ∋ A ∋ a ≡ b) = ∀ (F : A → Type n) → (Type n ∋ F a ≃ F b)

≡-cong O      f p = ≣-cong f p
≡-cong (n +1) f p = λ F → p (F ∘ f)

record Type_∋_≃_ n (A B : Type n) where
  constructor ⟨_,_,_,_,_⟩
  field f : A → B
  field f⁻¹ : B → A
  field η : ∀ a → Type n ∋ A ∋ f⁻¹(f a) ≡ a
  field ε : ∀ b → Type n ∋ B ∋ f(f⁻¹ b) ≡ b
  field τ : ∀ a → Type n ∋ (Type n ∋ B ∋ f (f⁻¹ (f a)) ≡ f a) ∋ (≡-cong n f (η a)) ≡ (ε (f a))
open Type_∋_≃_ public using () renaming (f to apply)

-- Reflexivity

≡-refl : ∀ n {A} {a} → (Type n ∋ A ∋ a ≡ a)
≡-refl-τ : ∀ n {A} {a} → (Type n ∋ (Type n ∋ A ∋ a ≡ a) ∋ (≡-cong n (λ x → x) (≡-refl n)) ≡ (≡-refl n))
≃-refl : ∀ n {A} → (Type n ∋ A ≃ A)

≡-refl O      = ≣-refl
≡-refl (n +1) = λ F → ≃-refl n

≡-refl-τ O = ≣-refl
≡-refl-τ (n +1) = λ F → ≃-refl n

≃-refl n = ⟨ (λ x → x) , (λ x → x) , (λ x → ≡-refl n) , (λ x → ≡-refl n) , (λ x → ≡-refl-τ n) ⟩

-- Postulate J

J : ∀ n {A} (C : ∀ a b → (Type n ∋ A ∋ a ≡ b) → Type n) → (∀ a → C a a (≡-refl n)) → ∀ a b p → C a b p
J n C c a = POSTULATE[ a ↦ POSTULATE[ ≡-refl n ↦ c a ] ]

-- Symmetry and transitivity of ≡ follow from J

≡-sym : ∀ n {A a b} → (Type n ∋ A ∋ a ≡ b) → (Type n ∋ A ∋ b ≡ a)
≡-sym n {A} {a} {b} = J n (λ a b p → Type n ∋ A ∋ b ≡ a) (λ a → ≡-refl n) a b

≡-trans : ∀ n {A a b c} → (Type n ∋ A ∋ a ≡ b) → (Type n ∋ A ∋ b ≡ c) → (Type n ∋ A ∋ a ≡ c)
≡-trans n {A} {a} {b} {c} = J n (λ a b p → Type n ∋ A ∋ b ≡ c → Type n ∋ A ∋ a ≡ c) (λ a → id) a b

-- Two possible definitions of ≃ being a conguruence...
-- both of them have the type ≃-cong n F : (Type n ∋ A ≃ B) → (Type n ∋ F A ≃ F B)
-- but they have different beta-reductions:
-- ≃-cong n F (≡-refl n) beta-reduces to (≡-refl n)
-- ≃-cong′ n id p beta-reduces to p

≃-cong : ∀ n → (F : Type n → Type n) → ∀ {A B} → (Type n ∋ A ≃ B) → (Type n ∋ F A ≃ F B)
≃-cong n F {A} {B} = f B where 

  f : ∀ B → (Type n ∋ A ≃ B) → (Type n ∋ F A ≃ F B)
  f = POSTULATE[ A ↦ POSTULATE[ ≃-refl n ↦ ≃-refl n ] ]

≃-cong′ : ∀ n {A B} → (F : Type n → Type n) → (Type n ∋ A ≃ B) → (Type n ∋ F A ≃ F B)
≃-cong′ n = POSTULATE[ id ↦ id ]

-- From these two definitions of ≃-cong, we get two definitions of ua

ua : ∀ n {A B} → (Type n ∋ A ≃ B) → (Type (n +1) ∋ Type n ∋ A ≡ B)
ua n e F = ≃-cong n F e

ua′ : ∀ n {A B} → (Type n ∋ A ≃ B) → (Type (n +1) ∋ Type n ∋ A ≡ B)
ua′ n e F = ≃-cong′ n F e

-- Each of these has an inverse.
-- Note that (ua′⁻¹ n (ua′ n p)) beta-reduces to p

ua⁻¹ : ∀ n {A B} → (Type (n +1) ∋ Type n ∋ A ≡ B) → (Type n ∋ A ≃ B)
ua⁻¹ n {A} {B} = J (n +1) (λ A B p → (Type n ∋ A ≃ B)) (λ A → ≃-refl n) A B

ua′⁻¹ : ∀ n {A B} → (Type (n +1) ∋ Type n ∋ A ≡ B) → (Type n ∋ A ≃ B)
ua′⁻¹ n p = p id

-- Univalence

ua-η : ∀ n {A B} (p : Type (n +1) ∋ Type n ∋ A ≡ B) → 
  (Type (n +1) ∋ (Type (n +1) ∋ Type n ∋ A ≡ B) ∋ (ua n (ua⁻¹ n p)) ≡ p)
ua-η n {A} {B} p = J (n +1) (λ A B p → Type n +1 ∋ _ ∋ ua n (ua⁻¹ n p) ≡ p) (λ A → ≡-refl (n +1)) A B p

ua-ε-Y : ∀ n {A B} (p : Type (n +1) ∋ Type n ∋ A ≡ B) → 
  (Type (n +1) ∋ (Type n ∋ A ≃ B) ∋ (ua⁻¹ n (ua n (ua′⁻¹ n p))) ≡ (ua′⁻¹ n p))
ua-ε-Y n {A} {B} p = J (n +1) (λ A B p → Type n +1 ∋ Type n ∋ A ≃ B ∋ ua⁻¹ n (ua n (ua′⁻¹ n p)) ≡ ua′⁻¹ n p) (λ A → ≡-refl (n +1)) A B p

ua-ε : ∀ n {A B} (e : Type n ∋ A ≃ B) → 
  (Type (n +1) ∋ (Type n ∋ A ≃ B) ∋ (ua⁻¹ n (ua n e)) ≡ e)
ua-ε n {A} {B} e = ua-ε-Y n (ua′ n e)

ua-τ : ∀ n {A B} (e : Type n ∋ A ≃ B) → 
  (Type (n +1) ∋ _ ∋ (≡-cong (n +1) (ua n) (ua-ε n e)) ≡ (ua-η n (ua n e)))
ua-τ n {A} {B} e = J 
  (n +1) 
  (λ A B p → Type (n +1) ∋ _ ∋ ≡-cong (n +1) (ua n) (ua-ε-Y n p) ≡ ua-η n (ua n (ua′⁻¹ n p))) 
  (λ A → ≡-refl (n +1)) 
  A B (ua′ n e)

univalence : ∀ n {A B} → (Type (n +1) ∋ (Type n ∋ A ≃ B) ≃ (Type (n +1) ∋ Type n ∋ A ≡ B))
univalence n = ⟨ ua n , ua⁻¹ n , ua-ε n , ua-η n , ua-τ n ⟩

-- ua and ua′ are the same

ua′⁻¹≡ua⁻¹ : ∀ n {A B} p → (Type (n +1) ∋ (Type n ∋ A ≃ B) ∋ ua′⁻¹ n p ≡ ua⁻¹ n p)
ua′⁻¹≡ua⁻¹ n {A} {B} p = J (n +1) (λ A B p → Type (n +1) ∋ _ ∋ (ua′⁻¹ n p) ≡ (ua⁻¹ n p)) (λ A → ≡-refl (n +1)) A B p

ua≡ua′ : ∀ n {A B} e → (Type (n +1) ∋ (Type (n +1) ∋ Type n ∋ A ≡ B) ∋ ua n e ≡ ua′ n e)
ua≡ua′ n {A} {B} e = ≡-trans (n +1) (≡-cong (n +1) (ua n) (ua′⁻¹≡ua⁻¹ n (ua′ n e))) (ua-η n (ua′ n e))