消息来源频道

前向兼容手札

@zyf_at_rochester

频道122 位成员公开可见0 人在线

后向兼容什么的，才没人在意呢！

成员规模122 位成员

在线情况0 人在线

消息总数888 条消息

浏览量总数15,140 次浏览

频道详情频道地址

2022/09/13 01:55

hedberg : {X : 𝓤 ̇ } → has-decidable-equality X → is-set X
hedberg {𝓤} {X} d = types-with-wconstant-＝-endomaps-are-sets X (hedberg-lemma d)
Does the reverse hold?