[Agda] Re: eta expansion

[Altenkirch Thorsten]

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

The universes in Agda are open hence they don't admit an induction principle unlike the closed universes defined by induction-recursion. As a consequence all you can do a with type in a universe is extensional you cannot investigate how are the built. This is reflected by the univalence principle.

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.

Since isomorphism isn't decidable this is not possible.

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".

I think Peter Lumsdaine answered that question.

The univalence axiom is usually taken to refer to a specific universe; i.e. for a universe (U, El : U -> Type), it states that for each A,B:U, the canonical map (A =_U B) -> (Equiv (El A) (El B)) is itself an equivalence.

Indeed the universe of finite sets (U=Nat,T=Fin) is univalent and this is easily provable in vanilla type theory (without univalence). I think that carries over to (CoNat,Fin') where Fin' is defined in the same way as Fin but for CoNats. I think we need ext for that.

Cheers,
Thorsten

P.S. The conat universe isn't closed under Sigma-types. Is there an extension (I.e. a universe such that the conat universe can be embedded) which is closed under Sigma?




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<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130320/ca70f6c5/attachment.html