[Agda] Re: eta expansion

[Peter Hancock]

On 19/03/2013 20:26, Francesco Mazzoli wrote:
> 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’.

What interests me is that you are using a universe, albeit a sacred universe
of Agda privileged with a silent decoding function.   I use the word Set in a completely
different way, according to which all these universes are Sets.  Maybe I should
say Type.If one assumes that
universes arise by induction-recursion, there is nothing to prevent
univalence failing for trivial reasons.  Presumably this should be
regarded as a "bad" universe.  In a good universe of sets, syntactical equality on codes
should coincide with some notion of isomorphism between the sets the names denote.
This seems to me to be a normal form property: there should be at most "one" code
(up to syntactical equality) for a given set.

One can have universes (U,T) of other things than sets: for example, universes of
functors, of things of any type D, ie T : U -> D.
D may involve Set and be large, or it may be a set.
It isn't crystal clear to me how in general equality
should be defined between elements of U so as to be "good".


Peter


>
> Then you can have your univalence axiom:
>
>      univalence : ∀ {ℓ} (A B : Set ℓ) → Iso A B → A ≡ B
>
> Where ‘Iso’ is some notion of isomorphism.
>
> Francesco
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>