From 7579d3da25a75ee8213bf2241aef759e61751292 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <aliaksandr.hryzlou@imdea.org>
Date: Wed, 6 Nov 2024 22:21:41 +0100
Subject: [PATCH] propositionally truncated version

---
 src/Data/AF/Base.agda     | 43 ++--------------------
 src/Data/AF/Examples.agda | 70 ++++++++++++++----------------------
 src/Data/AF/Prop.agda     | 76 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 106 insertions(+), 83 deletions(-)
 create mode 100644 src/Data/AF/Prop.agda

diff --git a/src/Data/AF/Base.agda b/src/Data/AF/Base.agda
index 43332b90..4abcd805 100644
--- a/src/Data/AF/Base.agda
+++ b/src/Data/AF/Base.agda
@@ -9,10 +9,10 @@ open import Meta.Effect.Idiom
 open import Data.Empty.Base
 open import Data.Unit.Base
 open import Data.Sum.Base
+
 open import Data.List.Base
 open import Data.List.Correspondences.Unary.Any
 open import Data.List.Membership
-open import Data.Truncation.Propositional as ∥-∥₁
 
 _↑_ : ∀ {ℓ ℓ′} {A : 𝒰 ℓ} → (A → A → 𝒰 ℓ′) → A → A → A → 𝒰 ℓ′
 (R ↑ a) x y = R x y ⊎ R a x
@@ -21,17 +21,10 @@ data AF {ℓ ℓ′} {A : 𝒰 ℓ} (R : A → A → 𝒰 ℓ′) : 𝒰 (ℓ 
   AFfull : (∀ x y → R x y) → AF R
   AFlift : (∀ a → AF (R ↑ a)) → AF R
 
-{-
-data AF₁ {ℓ ℓ′} {A : 𝒰 ℓ} (R : A → A → 𝒰 ℓ′) : 𝒰 (ℓ ⊔ ℓ′) where
-  AF₁full : (∀ x y → ∥ R x y ∥₁) → AF₁ R
-  AF₁lift : (∀ a → AF₁ (R ↑ a)) → AF₁ R
--}
-
 private variable
   ℓ ℓ′ ℓ″ : Level
   A B : 𝒰 ℓ
   R T : A → A → 𝒰 ℓ′
---  T : A → A → 𝒰 ℓ″
 
 ↑-mono : (∀ {x y} → R x y → T x y) -- TODO subseteq
        → ∀ {x y a} → (R ↑ a) x y → (T ↑ a) x y
@@ -72,15 +65,6 @@ af-mono sub (AFfull f) =
 af-mono sub (AFlift l) =
   AFlift λ a → af-mono (λ {x} {y} → ↑-mono sub {x} {y} {a}) (l a)
 
-{-
-af₁-mono : (∀ {x y} → R x y → T x y) -- TODO subseteq
-        → AF₁ R → AF₁ T
-af₁-mono sub (AF₁full f) =
-  AF₁full λ x y → map sub (f x y)
-af₁-mono sub (AF₁lift l) =
-  AF₁lift λ a → af₁-mono (λ {x} {y} → ↑-mono sub {x} {y} {a}) (l a)
--}
-
 af-comap : ∀ {ℓa ℓb ℓr} {A : 𝒰 ℓa} {B : 𝒰 ℓb} {R : A → A → 𝒰 ℓr}
          → (f : B → A)
          → AF R → AF (λ x y → R (f x) (f y))
@@ -116,6 +100,8 @@ af-rel-morph f surj mor (AFlift al) =
                                (inr ra₁) → inr (mor a  x₁ x  y₁ fa f₁ ra₁))
     (al a)
 
+-- derived versions
+
 af-mono′ : (∀ {x y} → R x y → T x y)
          → AF R → AF T
 af-mono′ {T} f =
@@ -136,26 +122,3 @@ af-map′ : ∀ {ℓa ℓb ℓr ℓt} {A : 𝒰 ℓa} {B : 𝒰 ℓb}
 af-map′ {R} {f} fr =
   af-rel-morph (λ x y → x ＝ f y) (λ y → f y , refl)
     λ x₁ x₂ y₁ y₂ e₁ e₂ → fr y₁ y₂ ∘ subst (λ q → R q (f y₂)) e₁ ∘ subst (R x₁) e₂
-
---  af-rel-morph (λ x y → x ＝ fst y) (λ y → fst y , refl)
---    λ x₁ x₂ y₁ y₂ e₁ e₂ → subst (λ q → R q (fst y₂)) e₁ ∘ subst (R x₁) e₂
-{-
-af₁-rel-morph : ∀ {ℓa ℓb ℓr ℓt} {A : 𝒰 ℓa} {B : 𝒰 ℓb} {R : A → A → 𝒰 ℓr} {T : B → B → 𝒰 ℓt}
-                  → (f : A → B → 𝒰 ℓ)
-                  → ((y : B) → ∃[ x ꞉ A ] (f x y))
-                  → ((x₁ x₂ : A) → (y₁ y₂ : B) → f x₁ y₁ → f x₂ y₂ → R x₁ x₂ → T y₁ y₂)
-                  → AF₁ R → AF₁ T
-af₁-rel-morph f surj mor (AF₁full af) =
-  AF₁full λ x y →
-  (surj x) & ∥-∥₁.elim (λ _ → squash₁)
-  λ where (a , fa) →
-             (surj y) & ∥-∥₁.elim (λ _ → squash₁)
-              λ where (b , fb) →
-                         (af a b) & ∥-∥₁.elim (λ _ → squash₁)
-                          λ r → ∣ mor a b x y fa fb r ∣₁
-af₁-rel-morph f surj mor (AF₁lift al) =
-  AF₁lift λ x →
-  (surj x) & ∥-∥₁.elim (λ _ → {!squash₁!})
-  λ where (a , fa) →
-             {!!}
--}
diff --git a/src/Data/AF/Examples.agda b/src/Data/AF/Examples.agda
index 6b6f2fb8..fcd08109 100644
--- a/src/Data/AF/Examples.agda
+++ b/src/Data/AF/Examples.agda
@@ -38,27 +38,19 @@ Rfl (x₁ , x₂) (y₁ , y₂) = (x₁ ≤ y₁) × (x₂ ≤ y₂)
 
 Tfl-empty-intersect : ∀ {x₁ x₂ y₁ y₂}
                     → Plus Tfl (x₁ , x₂) (y₁ , y₂)
-                    → y₁ ≤ x₁
-                    → y₂ ≤ x₂
+                    → Rfl (y₁ , y₂) (x₁ , x₂)
                     → ⊥
-Tfl-empty-intersect [ inl x<y₁ ]⁺       y≤x₁ y≤x₂ = <→≱ x<y₁ y≤x₁
-Tfl-empty-intersect [ inr (e , x<y₂) ]⁺ y≤x₁ y≤x₂ = <→≱ x<y₂ y≤x₂
-Tfl-empty-intersect (h ◅⁺ p)            y≤x₁ y≤x₂ =
-  [ (λ x<w₁ → <→≱ x<w₁ (prf p ∙ y≤x₁))
-  , (λ where (e , x<w₂) → Tfl-empty-intersect p (y≤x₁ ∙ =→≤ e) (y≤x₂ ∙ <→≤ x<w₂))
+Tfl-empty-intersect [ inl x<y₁ ]⁺       (y≤x₁ , y≤x₂) = <→≱ x<y₁ y≤x₁
+Tfl-empty-intersect [ inr (e , x<y₂) ]⁺ (y≤x₁ , y≤x₂) = <→≱ x<y₂ y≤x₂
+Tfl-empty-intersect (h ◅⁺ p)            (y≤x₁ , y≤x₂) =
+  [ ≤→≯ (plus-fold1 Trans-≤ (plus-map [ <→≤ , =→≤ ∘ fst ]ᵤ p) ∙ y≤x₁)
+  , (λ where (e , x<w₂) → Tfl-empty-intersect p (y≤x₁ ∙ =→≤ e , y≤x₂ ∙ <→≤ x<w₂))
   ]ᵤ h
-  where
-  prf : ∀ {x₁ x₂ y₁ y₂}
-      → Plus Tfl (x₁ , x₂) (y₁ , y₂)
-      → x₁ ≤ y₁
-  prf pl = plus-fold1 Trans-≤ (plus-map [ <→≤ , =→≤ ∘ fst ]ᵤ pl)
 
 flex : ℕ × ℕ → ℕ
 flex =
   to-induction
-    (AF→WF {R = Rfl} {T = Tfl}
-           (af-× af-≤ af-≤)
-           λ where p (y≤x₁ , y≤x₂) → Tfl-empty-intersect p y≤x₁ y≤x₂)
+    (AF→WF (af-× af-≤ af-≤) Tfl-empty-intersect)
     (λ _ → ℕ)
     λ x ih → go (x .fst) (x .snd) λ a b → ih (a , b)
   where
@@ -86,10 +78,9 @@ Tgr-trans (inr (x₂<y₁ , x₁<y₁)) (inr (_     , y₁<z₁)) = inr (<-trans
 
 Tgr-empty-intersect : ∀ {x₁ x₂ y₁ y₂}
                     → Plus Tgr (x₁ , x₂) (y₁ , y₂)
-                    → y₁ ≤ x₁
-                    → y₂ ≤ x₂
+                    → Rgr (y₁ , y₂) (x₁ , x₂)
                     → ⊥
-Tgr-empty-intersect p y≤x₁ y≤x₂ =
+Tgr-empty-intersect p (y≤x₁ , y≤x₂) =
   [ (λ where (_ , x<y₂) → <→≱ x<y₂ y≤x₂)
   , (λ where (_ , x<y₁) → <→≱ x<y₁ y≤x₁)
   ]ᵤ (plus-fold1 (record { _∙_ = Tgr-trans }) p)
@@ -97,9 +88,7 @@ Tgr-empty-intersect p y≤x₁ y≤x₂ =
 grok : ℕ × ℕ → ℕ
 grok =
   to-induction
-    (AF→WF {R = Rgr} {T = Tgr}
-           (af-× af-≤ af-≤)
-           λ where p (y≤x₁ , y≤x₂) → Tgr-empty-intersect p y≤x₁ y≤x₂)
+    (AF→WF (af-× af-≤ af-≤) Tgr-empty-intersect)
     (λ _ → ℕ)
     λ x ih → go (x .fst) (x .snd) λ a b → ih (a , b)
   where
@@ -118,7 +107,7 @@ Rf1 (x₁ , x₂) (y₁ , y₂) = x₁ + x₂ ≤ y₁ + y₂
 
 Tf1-intersection-empty : ∀ {x₁ x₂ y₁ y₂}
                        → Plus Tf1 (x₁ , x₂) (y₁ , y₂)
-                       → y₁ + y₂ ≤ x₁ + x₂
+                       → Rf1 (y₁ , y₂) (x₁ , x₂)
                        → ⊥
 Tf1-intersection-empty {x₁} {x₂} {y₁} {y₂} p y₁₂≤x₁₂ =
   ≤→≯ y₁₂≤x₁₂ $
@@ -129,9 +118,7 @@ Tf1-intersection-empty {x₁} {x₂} {y₁} {y₂} p y₁₂≤x₁₂ =
 flip1 : ℕ × ℕ → ℕ
 flip1 =
   to-induction
-    (AF→WF {R = Rf1} {T = Tf1}
-           (af-comap (λ where (x , y) → x + y) af-≤)
-           Tf1-intersection-empty)
+    (AF→WF (af-comap (λ where (x , y) → x + y) af-≤) Tf1-intersection-empty)
     (λ _ → ℕ)
     λ x ih → go (x .fst) (x .snd) λ a b → ih (a , b)
   where
@@ -179,12 +166,22 @@ T2-plus-inv (_◅⁺_ {y = (w₁ , w₂)} p2 pl) with T2-inv p2 | T2-plus-inv pl
 ... | inr (inr (x<w₁ , x<w₂)) | inr (inl (w<y₂ , w<y₁)) = inr $ inl (<-trans x<w₂ w<y₂ , <-trans x<w₁ w<y₁)
 ... | inr (inr (x<w₁ , x<w₂)) | inr (inr (w<y₁ , w<y₂)) = inr $ inr (<-trans x<w₁ w<y₁ , <-trans x<w₂ w<y₂)
 
+Tgn-plus-decompose : ∀ {x₁ x₂ y₁ y₂}
+                   → Plus Tgn (x₁ , x₂) (y₁ , y₂)
+                   → Tgn (x₁ , x₂) (y₁ , y₂)
+                   ⊎ Plus (pow 2 Tgn) (x₁ , x₂) (y₁ , y₂)
+                   ⊎ (Σ[ (z₁ , z₂) ꞉ ℕ × ℕ ] (Tgn (x₁ , x₂) (z₁ , z₂)) × (Plus (pow 2 Tgn) (z₁ , z₂) (y₁ , y₂)))
+Tgn-plus-decompose                     [ txy ]⁺                       = inl txy
+Tgn-plus-decompose {x₁} {x₂} {y₁} {y₂} (_◅⁺_ {y = (w₁ , w₂)} txw pwy) with Tgn-plus-decompose pwy
+... | inl twy                           = inr $ inl [ (w₁ , w₂) , txw , (y₁ , y₂) , twy , lift refl ]⁺
+... | inr (inl p)                       = inr $ inr ((w₁ , w₂) , txw , p)
+... | inr (inr ((z₁ , z₂) , twz , pzy)) = inr $ inl (((w₁ , w₂) , txw , (z₁ , z₂) , twz , lift refl) ◅⁺ pzy)
+
 Tgn-empty-intersect : ∀ {x₁ x₂ y₁ y₂}
                     → Plus Tgn (x₁ , x₂) (y₁ , y₂)
-                    → y₁ ≤ x₁
-                    → y₂ ≤ x₂
+                    → Rgn (y₁ , y₂) (x₁ , x₂)
                     → ⊥
-Tgn-empty-intersect p y≤x₁ y≤x₂ =
+Tgn-empty-intersect p (y≤x₁ , y≤x₂) =
   [ (λ where
          (inl (e , x₂<y₂)) → <→≱ x₂<y₂ y≤x₂
          (inr (e , x₂<y₁)) → <→≱ x₂<y₁ (y≤x₁ ∙ =→≤ e ∙ y≤x₂))
@@ -206,25 +203,12 @@ Tgn-empty-intersect p y≤x₁ y≤x₂ =
                     ]ᵤ txz
                   ]ᵤ (T2-plus-inv pzy))
     ]ᵤ
-  ]ᵤ (prf p)
-  where
-  prf : ∀ {x₁ x₂ y₁ y₂}
-      → Plus Tgn (x₁ , x₂) (y₁ , y₂)
-      → Tgn (x₁ , x₂) (y₁ , y₂)
-      ⊎ Plus (pow 2 Tgn) (x₁ , x₂) (y₁ , y₂)
-      ⊎ (Σ[ (z₁ , z₂) ꞉ ℕ × ℕ ] (Tgn (x₁ , x₂) (z₁ , z₂)) × (Plus (pow 2 Tgn) (z₁ , z₂) (y₁ , y₂)))
-  prf                     [ txy ]⁺                       = inl txy
-  prf {x₁} {x₂} {y₁} {y₂} (_◅⁺_ {y = (w₁ , w₂)} txw pwy) with prf pwy
-  ... | inl twy                           = inr $ inl [ (w₁ , w₂) , txw , (y₁ , y₂) , twy , lift refl ]⁺
-  ... | inr (inl p)                       = inr $ inr ((w₁ , w₂) , txw , p)
-  ... | inr (inr ((z₁ , z₂) , twz , pzy)) = inr $ inl (((w₁ , w₂) , txw , (z₁ , z₂) , twz , lift refl) ◅⁺ pzy)
+  ]ᵤ (Tgn-plus-decompose p)
 
 gnlex : ℕ × ℕ → ℕ
 gnlex =
   to-induction
-    (AF→WF {R = Rgn} {T = Tgn}
-           (af-× af-≤ af-≤)
-           λ where p (y≤x₁ , y≤x₂) → Tgn-empty-intersect p y≤x₁ y≤x₂)
+    (AF→WF (af-× af-≤ af-≤) Tgn-empty-intersect)
     (λ _ → ℕ)
     λ x ih → go (x .fst) (x .snd) λ a b → ih (a , b)
   where
diff --git a/src/Data/AF/Prop.agda b/src/Data/AF/Prop.agda
new file mode 100644
index 00000000..7b7ba072
--- /dev/null
+++ b/src/Data/AF/Prop.agda
@@ -0,0 +1,76 @@
+{-# OPTIONS --safe #-}
+module Data.AF.Prop where
+
+open import Foundations.Base
+open Variadics _
+open import Meta.Effect.Map
+open import Meta.Effect.Idiom
+
+open import Data.Empty.Base
+open import Data.Unit.Base
+open import Data.Sum.Base
+open import Data.AF.Base
+open import Data.Truncation.Propositional as ∥-∥₁
+
+data AF₁ {ℓ ℓ′} {A : 𝒰 ℓ} (R : A → A → 𝒰 ℓ′) : 𝒰 (ℓ ⊔ ℓ′) where
+  AF₁full : (∀ x y → ∥ R x y ∥₁) → AF₁ R
+  AF₁lift : (∀ a → AF₁ (R ↑ a)) → AF₁ R
+  AF₁squash : is-prop (AF₁ R)
+
+private variable
+  ℓ ℓ′ ℓ″ : Level
+  A B : 𝒰 ℓ
+  R T : A → A → 𝒰 ℓ′
+
+af₁-inv : AF₁ R → ∀ {a} → AF₁ (R ↑ a)
+af₁-inv (AF₁full f)         = AF₁full λ x y → map inl (f x y)
+af₁-inv (AF₁lift l) {a}     = l a
+af₁-inv (AF₁squash a₁ a₂ i) = AF₁squash (af₁-inv a₁) (af₁-inv a₂) i
+
+af₁-mono : (∀ {x y} → R x y → T x y) -- TODO subseteq
+        → AF₁ R → AF₁ T
+af₁-mono sub (AF₁full f) =
+  AF₁full λ x y → map sub (f x y)
+af₁-mono sub (AF₁lift l) =
+  AF₁lift λ a → af₁-mono (λ {x} {y} → ↑-mono sub {x} {y} {a}) (l a)
+af₁-mono sub (AF₁squash a₁ a₂ i) = AF₁squash (af₁-mono sub a₁) (af₁-mono sub a₂) i
+
+af₁-comap : ∀ {ℓa ℓb ℓr} {A : 𝒰 ℓa} {B : 𝒰 ℓb} {R : A → A → 𝒰 ℓr}
+         → (f : B → A)
+         → AF₁ R → AF₁ (λ x y → R (f x) (f y))
+af₁-comap f (AF₁full af)        = AF₁full λ x y → af (f x) (f y)
+af₁-comap f (AF₁lift al)        = AF₁lift λ a → af₁-comap f (al (f a))
+af₁-comap f (AF₁squash a₁ a₂ i) = AF₁squash (af₁-comap f a₁) (af₁-comap f a₂) i
+
+af₁-map : ∀ {ℓa ℓb ℓr ℓt} {A : 𝒰 ℓa} {B : 𝒰 ℓb}
+           {R : A → A → 𝒰 ℓr} {T : B → B → 𝒰 ℓt}
+       → {f : B → A} → (∀ x y → R (f x) (f y) → T x y)
+       → AF₁ R → AF₁ T
+af₁-map {f} fr (AF₁full af)        = AF₁full λ x y → map (fr x y) (af (f x) (f y))
+af₁-map {f} fr (AF₁lift al)        = AF₁lift λ b → af₁-map (λ x y → [ inl ∘ fr x y , inr ∘ fr b x ]ᵤ) (al (f b))
+af₁-map {f} fr (AF₁squash a₁ a₂ i) = AF₁squash (af₁-map fr a₁) (af₁-map fr a₂) i
+
+af₁-rel-morph : ∀ {ℓa ℓb ℓr ℓt} {A : 𝒰 ℓa} {B : 𝒰 ℓb} {R : A → A → 𝒰 ℓr} {T : B → B → 𝒰 ℓt}
+              → (f : A → B → 𝒰 ℓ)
+              → ((y : B) → ∃[ x ꞉ A ] (f x y))
+              → ((x₁ x₂ : A) → (y₁ y₂ : B) → f x₁ y₁ → f x₂ y₂ → R x₁ x₂ → T y₁ y₂)
+              → AF₁ R → AF₁ T
+af₁-rel-morph f surj mor (AF₁full af) =
+  AF₁full λ x y →
+  (surj x) & ∥-∥₁.elim (λ _ → squash₁)
+  λ where (a , fa) →
+             (surj y) & ∥-∥₁.elim (λ _ → squash₁)
+              λ where (b , fb) →
+                         (af a b) & ∥-∥₁.elim (λ _ → squash₁)
+                          λ r → ∣ mor a b x y fa fb r ∣₁
+af₁-rel-morph f surj mor (AF₁lift al) =
+  AF₁lift λ x →
+  (surj x) & ∥-∥₁.elim (λ _ → AF₁squash)
+  λ where (a , fa) →
+            af₁-rel-morph f surj
+              (λ x₁ x₂ y₁ y₂ f₁ f₂ → λ where
+                                         (inl r₁₂) → inl (mor x₁ x₂ y₁ y₂ f₁ f₂ r₁₂)
+                                         (inr ra₁) → inr (mor a  x₁ x  y₁ fa f₁ ra₁))
+              (al a)
+af₁-rel-morph f surj mor (AF₁squash a₁ a₂ i) =
+  AF₁squash (af₁-rel-morph f surj mor a₁) (af₁-rel-morph f surj mor a₂) i