refactor: various refactoring (#26)

src/Mugen/Algebra/Displacement/Constant.agda

@@ -30,22 +30,17 @@ module Constant
     open Strict-order-coproduct A B.strict-order
 
   _⊗α_ : ⌞ A ⌟ ⊎ ⌞ B ⌟ → ⌞ A ⌟ ⊎ ⌞ B ⌟ → ⌞ A ⌟ ⊎ ⌞ B ⌟
-  inr x ⊗α inr y = inr (x B.⊗ y)
+  _ ⊗α inl a = inl a
   inl a ⊗α inr x = inl (⟦ α ⟧ʳ a x)
-  inr _ ⊗α inl a = inl a
-  inl _ ⊗α inl a = inl a
+  inr x ⊗α inr y = inr (x B.⊗ y)
 
   εα : ⌞ A ⌟ ⊎ ⌞ B ⌟
   εα = inr B.ε
 
   ⊗α-associative : ∀ (x y z : ⌞ A ⌟ ⊎ ⌞ B ⌟) → (x ⊗α (y ⊗α z)) ≡ ((x ⊗α y) ⊗α z)
-  ⊗α-associative (inl a) (inl b) (inl c) = refl
-  ⊗α-associative (inl a) (inl b) (inr z) = refl
-  ⊗α-associative (inl a) (inr y) (inl c) = refl
+  ⊗α-associative _ _ (inl _) = refl
+  ⊗α-associative _ (inl _) (inr _) = refl
   ⊗α-associative (inl a) (inr y) (inr z) = ap inl (sym (α.compat a y z))
-  ⊗α-associative (inr x) (inl b) (inl c) = refl
-  ⊗α-associative (inr x) (inl b) (inr z) = refl
-  ⊗α-associative (inr x) (inr y) (inl c) = refl
   ⊗α-associative (inr x) (inr y) (inr z) = ap inr B.associative
 
   ⊗α-idl : ∀ (x : ⌞ A ⌟ ⊎ ⌞ B ⌟) → (εα ⊗α x) ≡ x
@@ -71,9 +66,8 @@ module Constant
   -- Left Invariance
 
   ⊗α-left-invariant : ∀ (x y z : ⌞ A ⌟ ⊎ ⌞ B ⌟) → y <α z → (x ⊗α y) <α (x ⊗α z)
-  ⊗α-left-invariant (inl x) (inl y) (inl z) y<z = y<z
+  ⊗α-left-invariant _ (inl y) (inl z) y<z = y<z
   ⊗α-left-invariant (inl x) (inr y) (inr z) y<z = α.invariant x y z y<z
-  ⊗α-left-invariant (inr x) (inl y) (inl z) y<z = y<z
   ⊗α-left-invariant (inr x) (inr y) (inr z) y<z = B.left-invariant y<z
 
 Const
@@ -119,7 +113,6 @@ module ConstantProperties
       module B-ordered-monoid = is-ordered-monoid (B-ordered-monoid)
 
       ⊗α-right-invariant : ∀ x y z → x ≤α y → (x ⊗α z) ≤α (y ⊗α z)
-      ⊗α-right-invariant (inl x) (inl y) (inl z) x≤y = inl refl
+      ⊗α-right-invariant _ _ (inl z) x≤y = inl refl
       ⊗α-right-invariant (inl x) (inl y) (inr z) x≤y = α-right-invariant x≤y
-      ⊗α-right-invariant (inr x) (inr y) (inl z) x≤y = inl refl
       ⊗α-right-invariant (inr x) (inr y) (inr z) x≤y = B-ordered-monoid.right-invariant x≤y

src/Mugen/Algebra/Displacement/NearlyConstant.agda

@@ -76,60 +76,29 @@ module NearlyConst
 
   --------------------------------------------------------------------------------
   -- Compactness Predicate
-  --
-  -- This is defined as a recursive family to avoid
-  -- frustrating situations with indexed types + cubical.
-  -- Furthermore, we avoid with-abstraction for things
-  -- that we actually want to compute: Agda can get
-  -- very confused if we do that!
 
   -- A list is compact relative to a base 'b' if it has
   -- no trailing b's.
-  is-compact : ⌞ 𝒟 ⌟ → Bwd ⌞ 𝒟 ⌟ → Type
-  is-compact base [] = ⊤
-  is-compact base (xs #r x) =
-    Dec-elim _
-      (λ _ → ⊥)
-      (λ _ → ⊤)
-      (x ≡? base)
-
-  -- Helper type for motives.
-  is-compact-case : ∀ {x base : ⌞ 𝒟 ⌟} → Dec (x ≡ base) → Type
-  is-compact-case p =
-    Dec-elim _
-      (λ _ → ⊥)
-      (λ _ → ⊤)
-      p
-
-  -- Propositional computation helpers for 'is-compact'
-  ¬base-is-compact : ∀ xs {x base} → (x ≡ base → ⊥) → is-compact base (xs #r x)
-  ¬base-is-compact xs {x = x} {base = base} ¬base with x ≡? base
-  ... | yes base! = ¬base base!
-  ... | no _ = tt
-
-  base-isnt-compact : ∀ xs {x base} → x ≡ base → is-compact base (xs #r x) → ⊥
-  base-isnt-compact xs {x = x} {base = base} base! is-compact with x ≡? base
-  ... | no ¬base = ¬base base!
+  is-compact : ⌞ 𝒟 ⌟ → Bwd ⌞ 𝒟 ⌟ → Type o
+  is-compact base [] = Lift o ⊤
+  is-compact base (xs #r x) = ¬ (x ≡ base)
 
   -- A singleton list consisting of only 'b' is not compact.
   base-isnt-compact-∷ : ∀ {xs x base} → xs ≡ [] → x ≡ base → is-compact base (bwd (x ∷ xs)) → ⊥
-  base-isnt-compact-∷ {xs = []} p base! is-compact = base-isnt-compact [] base! is-compact
+  base-isnt-compact-∷ {xs = []} p base! is-compact = is-compact base!
   base-isnt-compact-∷ {xs = x ∷ xs} p base! is-compact = ∷≠[] p
 
   is-compact-++r : ∀ xs ys base → is-compact base (xs ++r ys) → is-compact base ys
-  is-compact-++r xs [] base compact = tt
-  is-compact-++r xs (ys #r x) base compact with x ≡? base
-  ... | no ¬base = tt
+  is-compact-++r xs [] base compact = lift tt
+  is-compact-++r xs (ys #r x) base compact = compact
 
   is-compact-tail : ∀ x xs base → is-compact base (bwd (x ∷ xs)) → is-compact base (bwd xs)
   is-compact-tail x xs base compact =
-     is-compact-++r ([] #r x) (bwd xs) base (subst (is-compact base) (bwd-++ (x ∷ []) xs) compact)
+    is-compact-++r ([] #r x) (bwd xs) base (subst (is-compact base) (bwd-++ (x ∷ []) xs) compact)
 
   is-compact-is-prop : ∀ base xs → is-prop (is-compact base xs)
   is-compact-is-prop base [] = hlevel 1
-  is-compact-is-prop base (xs #r x) with x ≡? base
-  ... | yes _ = hlevel 1
-  ... | no _ = hlevel 1
+  is-compact-is-prop base (xs #r x) = hlevel 1
 
   --------------------------------------------------------------------------------
   -- Compacting Lists
@@ -140,14 +109,11 @@ module NearlyConst
 
   -- Remove all trailing 'base' elements
   compact : ⌞ 𝒟 ⌟ → Bwd ⌞ 𝒟 ⌟ → Bwd ⌞ 𝒟 ⌟
+  compact-case : ∀ xs {x base} → Dec (x ≡ base) → Bwd ⌞ 𝒟 ⌟
+
   compact base [] = []
-  compact base (xs #r x) =
-    Dec-elim _
-      (λ _ → compact base xs)
-      (λ _ → xs #r x)
-      (x ≡? base)
+  compact base (xs #r x) = compact-case xs (x ≡? base)
 
-  compact-case : ∀ xs {x base} → Dec (x ≡ base) → Bwd ⌞ 𝒟 ⌟
   compact-case xs {x = x} {base = base} p =
     Dec-elim _
       (λ _ → compact base xs)
@@ -167,14 +133,13 @@ module NearlyConst
 
   compact-compacted : ∀ base xs → is-compact base xs → compact base xs ≡ xs
   compact-compacted base [] is-compact = refl
-  compact-compacted base (xs #r x) is-compact with x ≡? base
-  ... | no _ = refl
+  compact-compacted base (xs #r x) is-compact = compact-done xs is-compact
 
   compact-is-compact : ∀ base xs → is-compact base (compact base xs)
-  compact-is-compact base [] = tt
+  compact-is-compact base [] = lift tt
   compact-is-compact base (xs #r x) with x ≡? base
   ... | yes _ = compact-is-compact base xs
-  ... | no ¬base = ¬base-is-compact xs ¬base
+  ... | no ¬base = ¬base
 
   compact-last : ∀ base xs ys y → compact base xs ≡ ys #r y → y ≡ base → ⊥
   compact-last base [] ys y p y≡base = #r≠[] (sym p)
@@ -516,7 +481,7 @@ module NearlyConst
   empty : SupportList
   empty .base = ε
   empty .elts = []
-  empty .compacted = tt
+  empty .compacted = lift tt
 
   -- Compacting a support lists elements does nothing
   elts-compact : ∀ xs → compact (xs .base) (xs .elts) ≡ xs .elts
@@ -1394,6 +1359,7 @@ module NearlyConst
   -- If a non-empty list denotes the function 'λ _ → b', then the list is not compact.
   all-base→¬compact : ∀ b x xs → (∀ n → index b (x ∷ xs) n ≡ b) → is-compact b (bwd (x ∷ xs)) → ⊥
   all-base→¬compact b x [] p xs-compact with x ≡? b
+  ... | yes x=base = absurd (xs-compact x=base)
   ... | no x≠base = x≠base (p 0)
   all-base→¬compact b x (y ∷ xs) p xs-compact =
     all-base→¬compact b y xs (λ n → p (suc n)) (is-compact-tail x (y ∷ xs) b xs-compact)
@@ -1734,7 +1700,7 @@ module _
   open has-bottom 𝒟-bottom
 
   bot-list : SupportList
-  bot-list = support-list bot [] tt
+  bot-list = support-list bot [] (lift tt)
 
   bot-list-is-bottom : ∀ b xs → merge-list≤ bot [] b xs
   bot-list-is-bottom b [] = is-bottom b

src/Mugen/Axioms/LPO.agda

@@ -42,16 +42,15 @@ module _ {o r} (A : Strict-order o r) (_≡?_ : Discrete ⌞ A ⌟) where
   LPO : Type (o ⊔ r)
   LPO = ∀ {f g : Nat → ⌞ A ⌟} → (∀ n → f n ≤ g n) → f ≡ g ⊎ ∃[ n ∈ Nat ] (f n < g n)
 
-  Markov+LEM→LPO : (∀ (f g : Nat → ⌞ A ⌟) → Markov (λ n → f n ≡ g n))
-                 → (∀ (f g : Nat → ⌞ A ⌟) → LEM (∀ n → f n ≡ g n))
-                 → LPO
-  Markov+LEM→LPO markov lem {f = f} {g = g} p = ∥-∥-rec (disjoint-⊎-is-prop f≡g-is-prop squash disjoint) (λ x → x) $ do
-    all-eq? ← lem f g
-    pure $ Dec-elim _
-      (λ all-eq → inl (funext all-eq))
-      (λ ¬all-eq → inr (∥-∥-map (Σ-map₂ (λ {n} fx≠gx → [ (λ fx≡gx → absurd $ fx≠gx fx≡gx) , (λ fx<gx → fx<gx) ] (p n))) $
-        markov f g (λ n → f n ≡? g n) ¬all-eq))
-      all-eq?
+  Markov+LEM→LPO
+    : (∀ (f g : Nat → ⌞ A ⌟) → Markov (λ n → f n ≡ g n))
+    → (∀ (f g : Nat → ⌞ A ⌟) → LEM (∀ n → f n ≡ g n))
+    → LPO
+  Markov+LEM→LPO markov lem {f = f} {g = g} p = ∥-∥-proj (disjoint-⊎-is-prop f≡g-is-prop squash disjoint) $ do
+    no ¬all-eq ← lem f g
+      where yes all-eq → pure $ inl $ funext all-eq
+    n , fn≠gn ← markov f g (λ n → f n ≡? g n) ¬all-eq
+    pure $ inr $ inc (n , [ (λ fn≡gn → absurd $ fn≠gn fn≡gn) , (λ fn<gn → fn<gn) ] (p n))
     where
       disjoint : (f ≡ g) × ∃[ n ∈ Nat ] (f n < g n) → ⊥
       disjoint (f≡g , ∃fn<gn) = ∥-∥-rec (hlevel 1) (λ { (n , fn<gn) → <-not-equal fn<gn (happly f≡g n) }) ∃fn<gn