[Agda] Re: eta expansion

[Francesco Mazzoli]

Peter Hancock <hancock at ...> writes:
> May I ask a naive question that puzzles me?  In type theory, there is no
> constructor making types A = B from types A and B.  There is only
> the type a =_A b between objects of type A.  So how to express the univalence
axiom
> in type theory?  If I understand it, this says that
> a certain map f : A = B -> .. has contractible fibres.  But we don't have
> equality between types, only between objects in types.  Even to write down
> the univalence axiom, we need a binary type-constructor, or to define a
> type as an object u : U in a universe (U,T) having some kind of normal form
theorem.

Maybe I’m misunderstanding, but nothing prevents you from forming types of type
`A =_Set B':

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

    ℕ≡ℕ : ℕ ≡ ℕ
    ℕ≡ℕ = refl ℕ

‘refl’ will relate definitionally equal types as it relates definitionally equal
values.  Note that ‘ℕ ≡ ℕ : Set₁’, while ‘0 ≡ 0 : Set’.

Then you can have your univalence axiom:

    univalence : ∀ {ℓ} (A B : Set ℓ) → Iso A B → A ≡ B

Where ‘Iso’ is some notion of isomorphism.

Francesco