[Agda] Re: eta expansion
Altenkirch Thorsten
psztxa at exmail.nottingham.ac.uk
Wed Mar 20 14:27:12 CET 2013
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
More information about the Agda
mailing list