# HG changeset patch
# User Shinji KONO
# Date 1593443825 -32400
# Node ID d4802179a66f50519e20e933973b4ea128db052c
# Parent b172ab9f12bc195e06e28b309d83f6fcaaf9282a
...
diff -r b172ab9f12bc -r d4802179a66f OD.agda
--- a/OD.agda Tue Jun 30 00:05:16 2020 +0900
+++ b/OD.agda Tue Jun 30 00:17:05 2020 +0900
@@ -57,15 +57,15 @@
-- HOD = { x | TC x ⊆ OD }
-- where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x.
-- This is not possible because we don't have V yet.
--- We simply assume V=OD here.
--
--- We also assumes ODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
--- ODs have an ovbious maximum, but Ordinals are not. This means, od→ord is not an on-to mapping.
---
--- ==→o≡ is necessary to prove axiom of extensionality.
+-- We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
+-- ODs have an ovbious maximum, but Ordinals are not. So HOD cannot be a maximum OD.
--
-- In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic,
-- we need explict assumption on sup.
+-- In order to allow sup on od→ord HOD, solutions of a HOD have to have a maximu.
+--
+-- ==→o≡ is necessary to prove axiom of extensionality.
data One : Set n where
OneObj : One
@@ -80,14 +80,6 @@
odmax : Ordinal