<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; font-family: Calibri, sans-serif; font-size: 14px; color: rgb(0, 0, 0); "><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><div><br><br></div><div>What interests me is that you are using a universe, albeit a sacred universe</div><div>of Agda privileged with a silent decoding function. I use the word Set in a completely</div></blockquote><div><br></div><div>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.</div><div><br></div><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><div>different way, according to which all these universes are Sets. Maybe I should</div><div>say Type.If one assumes that</div><div>universes arise by induction-recursion, there is nothing to prevent</div><div>univalence failing for trivial reasons. Presumably this should be</div><div>regarded as a "bad" universe. In a good universe of sets, syntactical equality on codes</div><div>should coincide with some notion of isomorphism between the sets the names denote.</div><div>This seems to me to be a normal form property: there should be at most "one" code</div><div>(up to syntactical equality) for a given set.</div></blockquote><div><br></div><div>Since isomorphism isn't decidable this is not possible. </div><div><br></div><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><div>One can have universes (U,T) of other things than sets: for example, universes of</div><div>functors, of things of any type D, ie T : U -> D.</div><div>D may involve Set and be large, or it may be a set.</div><div>It isn't crystal clear to me how in general equality</div><div>should be defined between elements of U so as to be "good".</div></blockquote><div><br></div><div>I think Peter Lumsdaine answered that question.</div><div><br></div><div><blockquote style="margin:0 0 0 40px; border:none; padding:0px;"><div>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.</div><div><br></div></blockquote></div><div>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. </div><div><br></div><div>Cheers,</div><div>Thorsten</div><div><br></div><div>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?</div><div><br></div><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><div><br></div><div><br></div><blockquote id="MAC_OUTLOOK_ATTRIBUTION_BLOCKQUOTE" style="BORDER-LEFT: #b5c4df 5 solid; PADDING:0 0 0 5; MARGIN:0 0 0 5;"><div><br></div><div> Then you can have your univalence axiom:</div><div><br></div><div> univalence : ∀ {ℓ} (A B : Set ℓ) → Iso A B → A ≡ B</div><div><br></div><div> Where ‘Iso’ is some notion of isomorphism.</div><div><br></div><div> Francesco</div><div><br></div><div><br></div><div> _______________________________________________</div><div> Agda mailing list</div><div> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a></div><div> <a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></div><div><br></div></blockquote><div>_______________________________________________</div><div>Agda mailing list</div><div><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a></div><div><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></div><div><br></div></blockquote></body></html>