[Agda] Re: eta expansion
Francesco Mazzoli
f at mazzo.li
Tue Mar 19 21:26:33 CET 2013
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
More information about the Agda
mailing list