--- a/partfunc.agda	Sat Aug 01 11:06:29 2020 +0900
+++ b/partfunc.agda	Sat Aug 01 18:05:23 2020 +0900
@@ -19,6 +19,10 @@
 open _∨_
 open Bool
 
+----
+--
+-- Partial Function without ZF
+--
 
 record PFunc  (Dom : Set n) (Cod : Set n) : Set (suc n) where
    field
@@ -26,6 +30,10 @@
       pmap : (x : Dom ) → dom x → Cod
       meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q
 
+----
+--
+-- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod)
+--
 
 data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where
    v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v  ∷ f ) Zero
@@ -48,6 +56,10 @@
                        ; pmap = λ x y → find fp (lower x) (lower y)
                        ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} 
                        }
+----
+--
+-- to List (Maybe Two) is a Latice
+--
 
 _3⊆b_ : (f g : List (Maybe Two)) → Bool
 [] 3⊆b [] = true