Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
tree: c45779a59c
Fetching contributors…

Octocat-spinner-32-eaf2f5

Cannot retrieve contributors at this time

file 129 lines (102 sloc) 5.913 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
------------------------------------------------------------------------
-- The univalence axiom
------------------------------------------------------------------------

-- Copyright (c) 2012 Favonia
-- Copyright (c) 2011-2012 Nils Anders Danielsson

{-# OPTIONS --without-K #-}

-- Partly based on Voevodsky's work on univalent foundations.

module Univalence where

open import Prelude
open import Path
open import Path.Lemmas
open import Map.WeakEquivalence as Weak hiding (_∘_; id)

------------------------------------------------------------------------
-- The univalence axiom

-- If two sets are equal, then they are weakly equivalent.

≡⇒≈ : {} {A B : Set} A ≡ B A ≈ B
≡⇒≈ = elim (λ {A B} _ A ≈ B) (λ _ Weak.id)

-- The univalence axiom states that ≡⇒≈ is a weak equivalence.

Univalence-axiom : {} Set Set Set (lsuc ℓ)
Univalence-axiom A B = Is-weak-equivalence (≡⇒≈ {A = A} {B = B})

------------------------------------------------------------------------
-- Experimental Area
--
-- Another insight given by Robert Harper:
-- The Univalence axiom is equivalence induction!
--
-- Note: Here we show that "weak-equivalent induction"
-- and the Univalence axiom are mutually derivable.

private

  -- The definition of "weak-equivalence induction"
  ≈-Elim : (ℓ₁ ℓ₂ : Level) Set (lsuc (ℓ₁ ⊔ ℓ₂))
  ≈-Elim ℓ₁ ℓ₂ = (P : {A B : Set ℓ₁} A ≈ B Set ℓ₂)
                 ((A : Set ℓ₁) P (Weak.id {A = A}))
                  {A B : Set ℓ₁} (A≈B : A ≈ B) P A≈B
  
  ≈-Elim-id : (ℓ₁ ℓ₂ : Level) ≈-Elim ℓ₁ ℓ₂ Set (lsuc (ℓ₁ ⊔ ℓ₂))
  ≈-Elim-id ℓ₁ ℓ₂ ≈-elim = (P : {A B : Set ℓ₁} A ≈ B Set ℓ₂)
                           (pid : (A : Set ℓ₁) P (Weak.id {A = A}))
                            {A} ≈-elim P pid Weak.id ≡ pid A

  -- The elimination and computation rules imply Univalence
  weq-elim⇒univ : {} (≈-elim : ≈-Elim ℓ (lsuc ℓ)) ≈-Elim-id ℓ (lsuc ℓ) ≈-elim
                   (A B : Set) Univalence-axiom A B
  weq-elim⇒univ {} ≈-elim ≈-elim-id A B =
    _≈_.is-weak-equivalence $ ↔⇒≈ $ record
      { surjection = record
        { to = ≡⇒≈
        ; from = ≈⇒≡
        ; right-inverse-of = right-inverse-of
        }
      ; left-inverse-of = left-inverse-of
      }
      where
        ≈⇒≡ : {A B : Set} A ≈ B A ≡ B
        ≈⇒≡ = ≈-elim (λ {A} {B} A≈B A ≡ B) (λ A refl A)
    
        ≈⇒≡-id : (A : Set) ≈⇒≡ Weak.id ≡ refl A
        ≈⇒≡-id A = ≈-elim-id (λ {A B} A≈B A ≡ B) (λ A refl A)
    
        left-inverse-of : (A≡B : A ≡ B) ≈⇒≡ (≡⇒≈ A≡B) ≡ A≡B
        left-inverse-of A≡B = elim
          (λ {A B} A≡B ≈⇒≡ (≡⇒≈ A≡B) ≡ A≡B)
          (λ A ≈⇒≡-id A)
          A≡B
       
        -- Here we use ↑ to handle the universe mismatch.
        right-inverse-of : (A≈B : A ≈ B) ≡⇒≈ (≈⇒≡ A≈B) ≡ A≈B
        right-inverse-of A≈B = ↑.lower $ ≈-elim
          (λ {A B : Set} A≈B (lsuc ℓ) (≡⇒≈ (≈⇒≡ A≈B) ≡ A≈B))
          (λ A lift (cong ≡⇒≈ (≈⇒≡-id A)))
          A≈B

  -- The other way around. The Univalence axiom implies both.
  --
  -- Maybe we should have one big lemma outputting a pair containing
  -- the elimination rule and the computation rule directly?
  univ⇒weq-elim : {ℓ ℓ′} ( (A B : Set) Univalence-axiom A B) ≈-Elim ℓ ℓ′
  univ⇒weq-elim {} {ℓ′} univ P pid {A} {B} A≈B =
      subst P right-inverse (elim (λ {A B : Set} A≡B P (≡⇒≈ A≡B)) pid (≈⇒≡ A≈B))
      where
        A≡B≈A≈B : (A ≡ B)(A ≈ B)
        A≡B≈A≈B = weq ≡⇒≈ (univ A B)

        ≈⇒≡ : A ≈ B A ≡ B
        ≈⇒≡ = _≈_.from A≡B≈A≈B

        right-inverse : ≡⇒≈ (≈⇒≡ A≈B) ≡ A≈B
        right-inverse = _≈_.right-inverse-of A≡B≈A≈B A≈B

  univ⇒weq-elim-id : {ℓ ℓ′} (univ : (A B : Set) Univalence-axiom A B)
                     ≈-Elim-id ℓ ℓ′ (univ⇒weq-elim univ)
  univ⇒weq-elim-id {} {ℓ′} univ P pid {A} =
      subst P right-inverse (elim (λ {_ _} A≡B P (≡⇒≈ A≡B)) pid (≈⇒≡ Weak.id))
          ≡⟨ cong (λ p subst P p (elim (λ {_ _} A≡B P (≡⇒≈ A≡B)) pid (≈⇒≡ Weak.id))) $ sym cong-left ⟩
      subst P (cong ≡⇒≈ left-inverse) (elim (λ {_ _} A≡B P (≡⇒≈ A≡B)) pid (≈⇒≡ Weak.id))
          ≡⟨ subst-cong P ≡⇒≈ left-inverse (elim (λ {_ _} A≡B P (≡⇒≈ A≡B)) pid (≈⇒≡ Weak.id))
      subst (P ∘ ≡⇒≈) left-inverse (elim (λ {_ _} A≡B P (≡⇒≈ A≡B)) pid (≈⇒≡ Weak.id))
          ≡⟨ cong[dep] (P ∘ ≡⇒≈) (elim (λ {_ _} A≡B P (≡⇒≈ A≡B)) pid) left-inverse ⟩∎
      elim (λ {_ _} A≡B P (≡⇒≈ A≡B)) pid (refl A)
          ∎
      where
        A≡A≈A≈A : (A ≡ A)(A ≈ A)
        A≡A≈A≈A = weq ≡⇒≈ (univ A A)

        ≈⇒≡ : A ≈ A A ≡ A
        ≈⇒≡ = _≈_.from A≡A≈A≈A

        left-inverse : ≈⇒≡ Weak.id ≡ refl A
        left-inverse = _≈_.left-inverse-of A≡A≈A≈A (refl A)

        right-inverse : ≡⇒≈ (≈⇒≡ Weak.id) ≡ Weak.id
        right-inverse = _≈_.right-inverse-of A≡A≈A≈A Weak.id

        cong-left : cong ≡⇒≈ left-inverse ≡ right-inverse
        cong-left = _≈_.left-right-lemma A≡A≈A≈A (refl A)
Something went wrong with that request. Please try again.