text:
open import Functional hiding (Domain)
import      Structure.Logic.Classical.NaturalDeduction
import      Structure.Logic.Classical.SetTheory.ZFC

module Structure.Logic.Classical.SetTheory.ZFC.Proofs {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ (_∈_ : Domain → Domain → Formula) ⦃ signature : _ ⦄ ⦃ axioms : _ ⦄ where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)
open Structure.Logic.Classical.SetTheory.ZFC.Signature {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic ⦄ {_∈_} (signature)
open Structure.Logic.Classical.SetTheory.ZFC.ZF        {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic ⦄ {_∈_} ⦃ signature ⦄ (axioms)

open import Lang.Instance
import      Lvl
open import Structure.Logic.Classical.NaturalDeduction.Proofs            ⦃ classicLogic ⦄
open import Structure.Logic.Classical.SetTheory.SetBoundedQuantification ⦃ classicLogic ⦄ (_∈_)
open import Structure.Logic.Classical.SetTheory.Relation                 ⦃ classicLogic ⦄ (_∈_)
open import Structure.Logic.Classical.SetTheory                          ⦃ classicLogic ⦄ (_∈_)
open        Structure.Logic.Classical.SetTheory.ZFC                      ⦃ classicLogic ⦄ (_∈_)
open import Structure.Logic.Constructive.Functions(Domain)
open import Structure.Logic.Constructive.Functions.Properties ⦃ constructiveLogicSignature ⦄

open SetEquality ⦃ ... ⦄        hiding (extensional)
open SingletonSet ⦃ ... ⦄       hiding (singleton)
open FilterSet ⦃ ... ⦄          hiding (filter)
open PowerSet ⦃ ... ⦄           hiding (℘)
open SetUnionSet ⦃ ... ⦄        hiding (⋃)
open UnionSet ⦃ ... ⦄           hiding (_∪_)
open IntersectionSet ⦃ ... ⦄    hiding (_∩_)
open WithoutSet ⦃ ... ⦄         hiding (_∖_)
open SetIntersectionSet ⦃ ... ⦄ hiding (⋂)

-- All sets are either empty or non-empty.
postulate Empty-excluded-middle : ∀{s} → Proof(Empty(s) ∨ NonEmpty(s))

pair-membership : Proof(∀ₗ(a₁ ↦ ∀ₗ(a₂ ↦ (∀ₗ(x ↦ (x ∈ pair(a₁)(a₂)) ⟷ (x ≡ a₁)∨(x ≡ a₂))))))
pair-membership = pairing

postulate pair-membership-[≡ₛ] : Proof(∀ₗ(a₁ ↦ ∀ₗ(a₂ ↦ (∀ₗ(x ↦ (x ∈ pair(a₁)(a₂)) ⟷ (x ≡ₛ a₁)∨(x ≡ₛ a₂))))))
-- pair-membership-[≡ₛ] = pairing

instance
  setEqualityInstance : SetEquality
  setEqualityInstance = SetEquality.intro extensional

instance
  emptySetInstance : EmptySet
  emptySetInstance = EmptySet.intro ∅ empty

instance
  singletonSetInstance : SingletonSet
  singletonSetInstance = SingletonSet.intro singleton
    ([∀].intro (\{a} →
      ([∀].intro (\{x} →
        [↔].transitivity
          ([∀].elim([∀].elim([∀].elim(pair-membership-[≡ₛ]){a}){a}){x})
          ([↔].intro ([∨].redundancyₗ) ([∨].redundancyᵣ))
      ))
    ))

instance
  filterSetInstance : FilterSet
  filterSetInstance = FilterSet.intro filter comprehension

instance
  powerSetInstance : PowerSet
  powerSetInstance = PowerSet.intro ℘ power

instance
  setUnionSetInstance : SetUnionSet
  setUnionSetInstance = SetUnionSet.intro ⋃ union

instance
  unionSetInstance : UnionSet
  unionSetInstance = UnionSet.intro _∪_
    ([∀].intro (\{a} →
      ([∀].intro (\{b} →
        ([∀].intro (\{x} →
          ([∀].elim([∀].elim [⋃]-membership{pair(a)(b)}){x})
          ⦗ₗ [↔].transitivity ⦘
          ([↔]-with-[∃] (\{s} →
            ([↔]-with-[∧]ₗ ([∀].elim([∀].elim([∀].elim pair-membership{a}){b}){s}))
            ⦗ₗ [↔].transitivity ⦘
            ([∧][∨]-distributivityᵣ)
            ⦗ₗ [↔].transitivity ⦘
            [↔]-with-[∨] ([≡]-substitute-this-is-almost-trivial) ([≡]-substitute-this-is-almost-trivial)
          ))
          ⦗ₗ [↔].transitivity ⦘
          ([↔].intro ([∃]-redundancyₗ) ([∃]-redundancyᵣ))
        ))
      ))
    ))

instance
  intersectionSetInstance : IntersectionSet
  intersectionSetInstance = IntersectionSet.intro _∩_
    ([∀].intro (\{a} →
      ([∀].intro (\{b} →
        ([∀].elim(filter-membership){a})
      ))
    ))

instance
  withoutSetInstance : WithoutSet
  withoutSetInstance = WithoutSet.intro _∖_
    ([∀].intro (\{a} →
      ([∀].intro (\{b} →
        ([∀].elim(filter-membership){a})
      ))
    ))

instance
  setIntersectionSetInstance : SetIntersectionSet
  setIntersectionSetInstance = SetIntersectionSet.intro ⋂
    ([∀].intro (\{ss} →
      ([∀].intro (\{x} →
        ([↔].intro
          -- (⟵)-case
          (allssinssxins ↦
            ([↔].elimₗ
              ([∀].elim([∀].elim filter-membership{⋃(ss)}){x})
              ([∧].intro
                -- x ∈ ⋃(ss)
                ([∨].elim
                  -- Empty(ss) ⇒ _
                  (allyyninss ↦
                    proof -- TODO: But: Empty(ss) ⇒ (ss ≡ ∅) ⇒ ⋃(ss) ≡ ∅ ⇒ (x ∉ ⋃(ss)) ? Maybe use this argument further up instead to prove something like: (⋂(ss) ≡ ∅) ⇒ (x ∉ ∅)
                  )

                  -- NonEmpty(ss) ⇒ _
                  (existsyinss ↦
                    ([∃].elim
                      (\{y} → yinss ↦ (
                        ([↔].elimₗ([∀].elim([∀].elim([⋃]-membership){ss}){x}))
                        ([∃].intro{_}
                          {y}
                          ([∧].intro
                            -- y ∈ ss
                            (yinss)

                            -- x ∈ y
                            ([→].elim
                              ([∀].elim(allssinssxins){y})
                              (yinss)
                            )
                          )
                        )
                      ))
                      (existsyinss)
                    )
                  )
                  (Empty-excluded-middle{ss})
                )

                -- ∀(s∊ss). x∈s
                (allssinssxins)
              )
            )
          )

          -- (⟶)-case
          (xinintersectss ↦
            ([∀].intro (\{s} →
              ([→].intro (sinss ↦
                ([→].elim
                  ([∀].elim
                    ([∧].elimᵣ
                      ([↔].elimᵣ
                        ([∀].elim
                          ([∀].elim
                            filter-membership
                            {⋃(ss)}
                          )
                          {x}
                        )
                        (xinintersectss)
                      )
                    )
                    {s}
                  )
                  (sinss)
                )
              ))
            ))
          )
        )
      ))
    ))
    where postulate proof : ∀{a} → a

-- postulate any : ∀{l}{a : Set(l)} → a

-- TODO: Just used for reference. Remove these lines later
-- ⋂(a) = filter(⋃(ss)) (x ↦ ∀ₗ(a₂ ↦ (a₂ ∈ ss) ⟶ (x ∈ a₂)))
-- filter-membership : ∀{φ : Domain → Formula} → Proof(∀ₗ(s ↦ ∀ₗ(x ↦ ((x ∈ filter(s)(φ)) ⟷ ((x ∈ s) ∧ φ(x))))))
-- [⋃]-membership : Proof(∀ₗ(ss ↦ ∀ₗ(x ↦ (x ∈ ⋃(ss)) ⟷ ∃ₗ(s ↦ (s ∈ ss)∧(x ∈ s)))))

-- [⨯]-membership : Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(x ↦ (x ∈ (a ⨯ b)) ⟷ ∃ₛ(a)(x₁ ↦ ∃ₛ(b)(x₂ ↦ x ≡ (x₁ , x₂)))))))
-- [⨯]-membership =

-- [⋃][℘]-inverse : Proof(∀ₗ(s ↦ ⋃(℘(s)) ≡ s))

-- TODO: https://planetmath.org/SurjectionAndAxiomOfChoice

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
open import FRP.JS.Bool using ( Bool ; not )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing ; _≟[_]_ )
open import FRP.JS.Float using ( ℝ ; _≟_ ; -_ ; _+_ ; _*_ ; _-_ ; _/_ ; _/?_ ; _≤_ ; _<_ ; show )
open import FRP.JS.String using () renaming ( _≟_ to _≟s_ )
open import FRP.JS.QUnit using ( TestSuite ; ok ; ok! ; test ; _,_ )

module FRP.JS.Test.Float where

infixr 2 _≟?_

_≟?_ : Maybe ℝ → Maybe ℝ → Bool
x ≟? y = x ≟[ _≟_ ] y

tests : TestSuite
tests =
  ( test "≟"
    ( ok "0 ≟ 0" (0.0 ≟ 0.0)
    , ok "1 ≟ 1" (1.0 ≟ 1.0)
    , ok "2 ≟ 2" (2.0 ≟ 2.0)
    , ok "0 != 1" (not (0.0 ≟ 1.0))
    , ok "0 != 2" (not (0.0 ≟ 2.0))
    , ok "1 != 2" (not (1.0 ≟ 2.0))
    , ok "1 != 0" (not (1.0 ≟ 0.0)) )
  , test "+"
    ( ok "0 + 0" (0.0 + 0.0 ≟ 0.0)
    , ok "1 + 1" (1.0 + 1.0 ≟ 2.0)
    , ok "37 + 0" (37.0 + 0.0 ≟ 37.0)
    , ok "37 + 1" (37.0 + 1.0 ≟ 38.0)
    , ok "37 + 5" (37.0 + 5.0 ≟ 42.0) )
  , test "*"
    ( ok "0 * 0" (0.0 * 0.0 ≟ 0.0)
    , ok "1 * 1" (1.0 * 1.0 ≟ 1.0)
    , ok "37 * 0" (37.0 * 0.0 ≟ 0.0)
    , ok "37 * 1" (37.0 * 1.0 ≟ 37.0)
    , ok "37 * 5" (37.0 * 5.0 ≟ 185.0) )
  , test "-"
    ( ok "0 - 0" (0.0 - 0.0 ≟ 0.0)
    , ok "1 - 1" (1.0 - 1.0 ≟ 0.0)
    , ok "37 - 0" (37.0 - 0.0 ≟ 37.0)
    , ok "37 - 1" (37.0 - 1.0 ≟ 36.0)
    , ok "37 - 5" (37.0 - 5.0 ≟ 32.0)
    , ok "5 - 37" (5.0 - 37.0 ≟ - 32.0) )
  , test "/"
    ( ok "1 / 1" (1.0 / 1.0 ≟ 1.0)
    , ok "37 / 1" (37.0 / 1.0 ≟ 37.0)
    , ok "37 / 5" (37.0 / 5.0 ≟ 7.4)
    , ok "0 /? 0" (0.0 /? 0.0 ≟? nothing)
    , ok "1 /? 1" (1.0 /? 1.0 ≟? just 1.0)
    , ok "37 /? 0" (37.0 /? 0.0 ≟? nothing)
    , ok "37 /? 1" (37.0 /? 1.0 ≟? just 37.0)
    , ok "37 /? 5" (37.0 /? 5.0 ≟? just 7.4) )
  , test "≤"
    ( ok "0 ≤ 0" (0.0 ≤ 0.0)
    , ok "0 ≤ 1" (0.0 ≤ 1.0)
    , ok "1 ≤ 0" (not (1.0 ≤ 0.0))
    , ok "1 ≤ 1" (1.0 ≤ 1.0)
    , ok "37 ≤ 0" (not (37.0 ≤ 0.0))
    , ok "37 ≤ 1" (not (37.0 ≤ 1.0))
    , ok "37 ≤ 5" (not (37.0 ≤ 5.0))
    , ok "5 ≤ 37" (5.0 ≤ 37.0) )
  , test "<"
    ( ok "0 < 0" (not (0.0 < 0.0))
    , ok "0 < 1" (0.0 < 1.0)
    , ok "1 < 0" (not (1.0 < 0.0))
    , ok "1 < 1" (not (1.0 < 1.0))
    , ok "37 < 0" (not (37.0 < 0.0))
    , ok "37 < 1" (not (37.0 < 1.0))
    , ok "37 < 5" (not (37.0 < 5.0))
    , ok "5 < 37" (5.0 < 37.0) )
  , test "show"
    ( ok "show 0" (show 0.0 ≟s "0")
    , ok "show 1" (show 1.0 ≟s "1")
    , ok "show 5" (show 5.0 ≟s "5")
    , ok "show 37" (show 37.0 ≟s "37")
    , ok "show -0" (show (- 0.0) ≟s "0")
    , ok "show -37" (show (- 37.0) ≟s "-37")
    , ok "show 3.1415" (show 3.1415 ≟s "3.1415")
    , ok "show -3.1415" (show (- 3.1415) ≟s "-3.1415") ) )

ext: agda

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT
open import cohomology.Theory
open import homotopy.PushoutSplit
open import homotopy.DisjointlyPointedSet
open import cw.CW

module cw.cohomology.WedgeOfCells {i} (OT : OrdinaryTheory i)
  {n} (⊙skel : ⊙Skeleton {i} (S n)) where

open OrdinaryTheory OT
open import cohomology.Sphere OT

Xₙ/Xₙ₋₁ : Ptd i
Xₙ/Xₙ₋₁ = ⊙Cofiber (⊙cw-incl-last ⊙skel)

module _ (m : ℤ) where
  CXₙ/Xₙ₋₁ : Group i
  CXₙ/Xₙ₋₁ = C m Xₙ/Xₙ₋₁

  CEl-Xₙ/Xₙ₋₁ : Type i
  CEl-Xₙ/Xₙ₋₁ = Group.El CXₙ/Xₙ₋₁

  abstract
    CXₙ/Xₙ₋₁-is-abelian : is-abelian CXₙ/Xₙ₋₁
    CXₙ/Xₙ₋₁-is-abelian = C-is-abelian m Xₙ/Xₙ₋₁

  CXₙ/Xₙ₋₁-abgroup : AbGroup i
  CXₙ/Xₙ₋₁-abgroup = CXₙ/Xₙ₋₁ , CXₙ/Xₙ₋₁-is-abelian

{- the equivalence is in the opposite direction because
   cohomology functors are contravariant. -}
BigWedge-⊙equiv-Xₙ/Xₙ₋₁ : ⊙BigWedge {A = ⊙cells-last ⊙skel} (λ _ → ⊙Sphere (S n)) ⊙≃ Xₙ/Xₙ₋₁
BigWedge-⊙equiv-Xₙ/Xₙ₋₁ = ≃-to-⊙≃
  (PS.split-equiv ∘e equiv to from to-from from-to) idp
  where
    open AttachedSkeleton (⊙Skeleton.skel ⊙skel)

    module PS = PushoutLSplit (uncurry attaching) (λ _ → tt) fst

    module SphereToCofiber (a : fst cells) = SuspRec {A = Sphere n}
      (cfbase' (fst :> (fst cells × Sphere n → fst cells)))
      (cfcod a) (λ s → cfglue (a , s))

    module To = BigWedgeRec {A = fst cells} {X = λ _ → ⊙Sphere (S n)}
      cfbase SphereToCofiber.f (λ _ → idp)
    to = To.f

    module From = CofiberRec {f = fst :> (fst cells × Sphere n → fst cells)}
      (bwbase {A = fst cells} {X = λ _ → ⊙Sphere (S n)})
      (λ a → bwin a south) (λ{(a , s) → bwglue a ∙ ap (bwin a) (merid s)})
    from = From.f

    abstract
      from-to : ∀ b → from (to b) == b
      from-to = BigWedge-elim
        idp
        (λ a → Susp-elim (bwglue a) idp
          (λ s → ↓-='-from-square $
            ( ap-∘ from (SphereToCofiber.f a) (merid s)
            ∙ ap (ap from) (SphereToCofiber.merid-β a s)
            ∙ From.glue-β (a , s))
            ∙v⊡ (tl-square (bwglue a) ⊡h vid-square)))
        (λ a → ↓-∘=idf-from-square from to $
          ap (ap from) (To.glue-β a) ∙v⊡ br-square (bwglue a))

      to-from : ∀ c → to (from c) == c
      to-from = Cofiber-elim
        idp (λ a → idp)
        (λ{(a , s) → ↓-∘=idf-in' to from $
            ap (ap to) (From.glue-β (a , s))
          ∙ ap-∙ to (bwglue a) (ap (bwin a) (merid s))
          ∙ ap2 _∙_ (To.glue-β a)
                    ( ∘-ap to (bwin a) (merid s)
                    ∙ SphereToCofiber.merid-β a s)})

CXₙ/Xₙ₋₁-β : ∀ m → ⊙has-cells-with-choice 0 ⊙skel i
  → C m Xₙ/Xₙ₋₁ ≃ᴳ Πᴳ (⊙cells-last ⊙skel) (λ _ → C m (⊙Lift (⊙Sphere (S n))))
CXₙ/Xₙ₋₁-β m ac = C-additive-iso m (λ _ → ⊙Lift (⊙Sphere (S n))) (⊙cells-last-has-choice ⊙skel ac)
              ∘eᴳ C-emap m ( BigWedge-⊙equiv-Xₙ/Xₙ₋₁
                         ⊙∘e ⊙BigWedge-emap-r (λ _ → ⊙lower-equiv))

CXₙ/Xₙ₋₁-β-diag : ⊙has-cells-with-choice 0 ⊙skel i
  → CXₙ/Xₙ₋₁ (ℕ-to-ℤ (S n)) ≃ᴳ Πᴳ (⊙cells-last ⊙skel) (λ _ → C2 0)
CXₙ/Xₙ₋₁-β-diag ac = Πᴳ-emap-r (⊙cells-last ⊙skel) (λ _ → C-Sphere-diag (S n))
                 ∘eᴳ CXₙ/Xₙ₋₁-β (ℕ-to-ℤ (S n)) ac

abstract
  CXₙ/Xₙ₋₁-≠-is-trivial : ∀ {m} (m≠Sn : m ≠ ℕ-to-ℤ (S n))
    → ⊙has-cells-with-choice 0 ⊙skel i
    → is-trivialᴳ (CXₙ/Xₙ₋₁ m)
  CXₙ/Xₙ₋₁-≠-is-trivial {m} m≠Sn ac =
    iso-preserves'-trivial (CXₙ/Xₙ₋₁-β m ac) $
      Πᴳ-is-trivial (⊙cells-last ⊙skel)
        (λ _ → C m (⊙Lift (⊙Sphere (S n))))
        (λ _ → C-Sphere-≠-is-trivial m (S n) m≠Sn)

  CXₙ/Xₙ₋₁-<-is-trivial : ∀ {m} (m<Sn : m < S n)
    → ⊙has-cells-with-choice 0 ⊙skel i
    → is-trivialᴳ (CXₙ/Xₙ₋₁ (ℕ-to-ℤ m))
  CXₙ/Xₙ₋₁-<-is-trivial m<Sn = CXₙ/Xₙ₋₁-≠-is-trivial (ℕ-to-ℤ-≠ (<-to-≠ m<Sn))

  CXₙ/Xₙ₋₁->-is-trivial : ∀ {m} (m>Sn : S n < m)
    → ⊙has-cells-with-choice 0 ⊙skel i
    → is-trivialᴳ (CXₙ/Xₙ₋₁ (ℕ-to-ℤ m))
  CXₙ/Xₙ₋₁->-is-trivial m>Sn = CXₙ/Xₙ₋₁-≠-is-trivial (≠-inv (ℕ-to-ℤ-≠ (<-to-≠ m>Sn)))

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --warning=error --safe --without-K #-}

open import LogicalFormulae

module Maybe where

data Maybe {a : _} (A : Set a) : Set a where
  no : Maybe A
  yes : A → Maybe A

joinMaybe : {a : _} → {A : Set a} → Maybe (Maybe A) → Maybe A
joinMaybe no = no
joinMaybe (yes s) = s

bindMaybe : {a b : _} → {A : Set a} → {B : Set b} → Maybe A → (A → Maybe B) → Maybe B
bindMaybe no f = no
bindMaybe (yes x) f = f x

applyMaybe : {a b : _} → {A : Set a} → {B : Set b} → Maybe (A → B) → Maybe A → Maybe B
applyMaybe f no = no
applyMaybe no (yes x) = no
applyMaybe (yes f) (yes x) = yes (f x)

yesInjective : {a : _} → {A : Set a} → {x y : A} → (yes x ≡ yes y) → x ≡ y
yesInjective {a} {A} {x} {.x} refl = refl

mapMaybe : {a b : _} → {A : Set a} → {B : Set b} → (f : A → B) → Maybe A → Maybe B
mapMaybe f no = no
mapMaybe f (yes x) = yes (f x)

defaultValue : {a : _} → {A : Set a} → (default : A) → Maybe A → A
defaultValue default no = default
defaultValue default (yes x) = x

noNotYes : {a : _} {A : Set a} {b : A} → (no ≡ yes b) → False
noNotYes ()

mapMaybePreservesNo : {a b : _} {A : Set a} {B : Set b} {f : A → B} {x : Maybe A} → mapMaybe f x ≡ no → x ≡ no
mapMaybePreservesNo {f = f} {no} pr = refl

mapMaybePreservesYes : {a b : _} {A : Set a} {B : Set b} {f : A → B} {x : Maybe A} {y : B} → mapMaybe f x ≡ yes y → Sg A (λ z → (x ≡ yes z) && (f z ≡ y))
mapMaybePreservesYes {f = f} {x} {y} map with x
mapMaybePreservesYes {f = f} {x} {y} map | yes z = z , (refl ,, yesInjective map)


text:
{-# OPTIONS --cubical --safe --no-import-sorts #-}
{-
Implements the monadic interface of propositional truncation, for reasoning in do-syntax.
-}

module Cubical.HITs.PropositionalTruncation.Monad where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Functions.Logic
open import Cubical.HITs.PropositionalTruncation

private
  variable
    ℓ : Level
    P Q : Type ℓ

infix 1 proof_by_
proof_by_ : (P : hProp ℓ) → ∥ ⟨ P ⟩ ∥ → ⟨ P ⟩
proof P by p = rec (isProp⟨⟩ P) (λ p → p) p

return : P → ∥ P ∥
return p = ∣ p ∣

exact_ : ∥ P ∥ → ∥ P ∥
exact p = p

_>>=_ : ∥ P ∥ → (P → ∥ Q ∥) → ∥ Q ∥
p >>= f = rec propTruncIsProp f p

_>>_ : ∥ P ∥ → ∥ Q ∥ → ∥ Q ∥
_ >> q = q

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Applicative functors on indexed sets (predicates)
------------------------------------------------------------------------

-- Note that currently the applicative functor laws are not included
-- here.

{-# OPTIONS --without-K --safe #-}

module Category.Applicative.Predicate where

open import Category.Functor.Predicate
open import Data.Product
open import Function
open import Level
open import Relation.Unary
open import Relation.Unary.PredicateTransformer using (Pt)

------------------------------------------------------------------------

record RawPApplicative {i ℓ} {I : Set i} (F : Pt I ℓ) :
                       Set (i ⊔ suc ℓ) where
  infixl 4 _⊛_ _<⊛_ _⊛>_
  infix  4 _⊗_

  field
    pure : ∀ {P} → P ⊆ F P
    _⊛_  : ∀ {P Q} → F (P ⇒ Q) ⊆ F P ⇒ F Q

  rawPFunctor : RawPFunctor F
  rawPFunctor = record
    { _<$>_ = λ g x → pure g ⊛ x
    }

  private
    open module RF = RawPFunctor rawPFunctor public

  _<⊛_ : ∀ {P Q} → F P ⊆ const (∀ {j} → F Q j) ⇒ F P
  x <⊛ y = const <$> x ⊛ y

  _⊛>_ : ∀ {P Q} → const (∀ {i} → F P i) ⊆ F Q ⇒ F Q
  x ⊛> y = flip const <$> x ⊛ y

  _⊗_ : ∀ {P Q} → F P ⊆ F Q ⇒ F (P ∩ Q)
  x ⊗ y = (_,_) <$> x ⊛ y

  zipWith : ∀ {P Q R} → (P ⊆ Q ⇒ R) → F P ⊆ F Q ⇒ F R
  zipWith f x y = f <$> x ⊛ y


text:
-- Parameter arguments of overloaded projection applications
-- should not be skipped!

record R A : Set where
  field f : A → A
open R

record S A : Set where
  field f : A → A
open S

r : ∀{A} → R A
f r x = x

test : ∀{A : Set} → A → A
test a = f r a

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
module Issue4022.Import where

open import Agda.Builtin.Nat

Binary : Set
Binary = Nat → Nat → Nat

-- Search should be able to find `plus` if:
-- * either we do not normalise the type and look for `Binary`
-- * or we do normalise the type and look for `Nat`

plus : Binary
plus = _+_

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

  Functions building UARels and DUARels on function types

-}
{-# OPTIONS --no-exact-split --safe #-}
module Cubical.Displayed.Function where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path

open import Cubical.Functions.FunExtEquiv
open import Cubical.Functions.Implicit

open import Cubical.Displayed.Base
open import Cubical.Displayed.Constant
open import Cubical.Displayed.Morphism
open import Cubical.Displayed.Subst
open import Cubical.Displayed.Sigma

private
  variable
    ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C : Level

-- UARel on dependent function type
-- from UARel on domain and DUARel on codomain

module _ {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) {B : A → Type ℓB} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B) where

  open UARel 𝒮-A
  open DUARel 𝒮ᴰ-B

  𝒮-Π : UARel ((a : A) → B a) (ℓ-max ℓA ℓ≅B)
  UARel._≅_ 𝒮-Π f f' = ∀ a → f a ≅ᴰ⟨ ρ a ⟩ f' a
  UARel.ua 𝒮-Π f f' =
    compEquiv
      (equivΠCod λ a → uaᴰρ (f a) (f' a))
      funExtEquiv

-- Parameterize UARel by type

_→𝒮_ : (A : Type ℓA) {B : Type ℓB} (𝒮-B : UARel B ℓ≅B) → UARel (A → B) (ℓ-max ℓA ℓ≅B)
(A →𝒮 𝒮-B) .UARel._≅_ f f' = ∀ a → 𝒮-B .UARel._≅_ (f a) (f' a)
(A →𝒮 𝒮-B) .UARel.ua f f' =
  compEquiv
    (equivΠCod λ a → 𝒮-B .UARel.ua (f a) (f' a))
    funExtEquiv

𝒮-app : {A : Type ℓA} {B : Type ℓB} {𝒮-B : UARel B ℓ≅B}
  → A → UARelHom (A →𝒮 𝒮-B) 𝒮-B
𝒮-app a .UARelHom.fun f = f a
𝒮-app a .UARelHom.rel h = h a
𝒮-app a .UARelHom.ua h = refl

-- DUARel on dependent function type
-- from DUARels on domain and codomain

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {C : (a : A) → B a → Type ℓC} (𝒮ᴰ-C : DUARel (∫ 𝒮ᴰ-B) (uncurry C) ℓ≅C)
  where

  open UARel 𝒮-A
  private
    module B = DUARel 𝒮ᴰ-B
    module C = DUARel 𝒮ᴰ-C

  𝒮ᴰ-Π : DUARel 𝒮-A (λ a → (b : B a) → C a b) (ℓ-max (ℓ-max ℓB ℓ≅B) ℓ≅C)
  DUARel._≅ᴰ⟨_⟩_ 𝒮ᴰ-Π f p f' =
    ∀ {b b'} (q : b B.≅ᴰ⟨ p ⟩ b') → f b C.≅ᴰ⟨ p , q ⟩ f' b'
  DUARel.uaᴰ 𝒮ᴰ-Π f p f' =
    compEquiv
      (equivImplicitΠCod λ {b} →
        (equivImplicitΠCod λ {b'} →
          (equivΠ (B.uaᴰ b p b') (λ q → C.uaᴰ (f b) (p , q) (f' b')))))
      funExtDepEquiv

_→𝒮ᴰ_ : {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} (𝒮ᴰ-B : DUARel 𝒮-A B ℓ≅B)
  {C : A → Type ℓC} (𝒮ᴰ-C : DUARel 𝒮-A C ℓ≅C)
  → DUARel 𝒮-A (λ a → B a → C a) (ℓ-max (ℓ-max ℓB ℓ≅B) ℓ≅C)
𝒮ᴰ-B →𝒮ᴰ 𝒮ᴰ-C =
  𝒮ᴰ-Π 𝒮ᴰ-B (𝒮ᴰ-Lift _ 𝒮ᴰ-C 𝒮ᴰ-B)

-- DUARel on dependent function type
-- from a SubstRel on the domain and DUARel on the codomain

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} (𝒮ˢ-B : SubstRel 𝒮-A B)
  {C : (a : A) → B a → Type ℓC} (𝒮ᴰ-C : DUARel (∫ˢ 𝒮ˢ-B) (uncurry C) ℓ≅C)
  where

  open UARel 𝒮-A
  open SubstRel 𝒮ˢ-B
  open DUARel 𝒮ᴰ-C

  𝒮ᴰ-Πˢ : DUARel 𝒮-A (λ a → (b : B a) → C a b) (ℓ-max ℓB ℓ≅C)
  DUARel._≅ᴰ⟨_⟩_ 𝒮ᴰ-Πˢ f p f' =
    (b : B _) → f b ≅ᴰ⟨ p , refl ⟩ f' (act p .fst b)
  DUARel.uaᴰ 𝒮ᴰ-Πˢ f p f' =
    compEquiv
      (compEquiv
        (equivΠCod λ b → Jequiv (λ b' q → f b ≅ᴰ⟨ p , q ⟩ f' b'))
        (invEquiv implicit≃Explicit))
      (DUARel.uaᴰ (𝒮ᴰ-Π (Subst→DUA 𝒮ˢ-B) 𝒮ᴰ-C) f p f')

-- SubstRel on a dependent function type
-- from a SubstRel on the domain and SubstRel on the codomain

equivΠ' : ∀ {ℓA ℓA' ℓB ℓB'} {A : Type ℓA} {A' : Type ℓA'}
  {B : A → Type ℓB} {B' : A' → Type ℓB'}
  (eA : A ≃ A')
  (eB : {a : A} {a' : A'} → eA .fst a ≡ a' → B a ≃ B' a')
  → ((a : A) → B a) ≃ ((a' : A') → B' a')
equivΠ' {B' = B'} eA eB = isoToEquiv isom
  where
  open Iso

  isom : Iso _ _
  isom .fun f a' =
    eB (retEq eA a') .fst (f (invEq eA a'))
  isom .inv f' a =
    invEq (eB refl) (f' (eA .fst a))
  isom .rightInv f' =
    funExt λ a' →
    J (λ a'' p → eB p .fst (invEq (eB refl) (f' (p i0))) ≡ f' a'')
      (retEq (eB refl) (f' (eA .fst (invEq eA a'))))
      (retEq eA a')
  isom .leftInv f =
    funExt λ a →
    subst
      (λ p → invEq (eB refl) (eB p .fst (f (invEq eA (eA .fst a)))) ≡ f a)
      (sym (commPathIsEq (eA .snd) a))
      (J (λ a'' p → invEq (eB refl) (eB (cong (eA .fst) p) .fst (f (invEq eA (eA .fst a)))) ≡ f a'')
        (secEq (eB refl) (f (invEq eA (eA .fst a))))
        (secEq eA a))

module _ {A : Type ℓA} {𝒮-A : UARel A ℓ≅A}
  {B : A → Type ℓB} (𝒮ˢ-B : SubstRel 𝒮-A B)
  {C : Σ A B → Type ℓC} (𝒮ˢ-C : SubstRel (∫ˢ 𝒮ˢ-B) C)
  where

  open UARel 𝒮-A
  open SubstRel
  private
    module B = SubstRel 𝒮ˢ-B
    module C = SubstRel 𝒮ˢ-C

  𝒮ˢ-Π : SubstRel 𝒮-A (λ a → (b : B a) → C (a , b))
  𝒮ˢ-Π .act p = equivΠ' (B.act p) (λ q → C.act (p , q))
  𝒮ˢ-Π .uaˢ p f =
    fromPathP
      (DUARel.uaᴰ (𝒮ᴰ-Π (Subst→DUA 𝒮ˢ-B) (Subst→DUA 𝒮ˢ-C)) f p (equivFun (𝒮ˢ-Π .act p) f) .fst
        (λ {b} →
          J (λ b' q →
                equivFun (C.act (p , q)) (f b)
                ≡ equivFun (equivΠ' (𝒮ˢ-B .act p) (λ q → C.act (p , q))) f b')
            (λ i →
              C.act (p , λ j → commSqIsEq (𝒮ˢ-B .act p .snd) b (~ i) j) .fst
                (f (secEq (𝒮ˢ-B .act p) b (~ i))))))

max_stars_repo_name: jespercockx/cubical

max_issues_repo_name: jespercockx/cubical

max_forks_repo_name: jespercockx/cubical


text:
-- AIM XXXV, 2022-05-06, issue #5891.
-- When checking that the sort of a data type admits data definitions
-- (checkDataSort), we need to handle the case of PiSort.

mutual
  Univ1 = _
  Univ2 = _
  Univ3 = _

  postulate
    A1 : Univ1
    A2 : Univ2

  A : Univ3
  A = A1 → A2

  -- This demonstrates that the sort of a data types can be a PiSort
  -- (temporarily, until further information becomes available later):
  data Empty : Univ3 where

  _ : Univ1
  _ = Set

  _ : Univ2
  _ = Set

-- Should succeed.


text:
module Human.Equality where

data _==_ {A : Set} (x : A) : A -> Set where
  refl : x == x

{-# BUILTIN EQUALITY _==_ #-}

sym : {A : Set} (x : A) (y : A) -> x == y -> y == x
sym x .x refl = refl

cong : {A : Set} {B : Set} (x : A) (y : A) (f : A -> B) -> x == y -> f x == f y
cong x y f refl = refl

max_stars_repo_name: MaisaMilena/AgdaCalculator

max_issues_repo_name: MaisaMilena/AgdaCalculator

max_forks_repo_name: MaisaMilena/AgdaCalculator


text:
module Issue271 where

data D (A : Set) : Set where
  d : D A → D A

f : {A : Set} → D A → D A
f x = d {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --prop --rewriting #-}

open import Examples.Sorting.Parallel.Comparable

module Examples.Sorting.Parallel.MergeSortPar.Merge (M : Comparable) where

open Comparable M
open import Examples.Sorting.Parallel.Core M

open import Calf costMonoid
open import Calf.ParMetalanguage parCostMonoid
open import Calf.Types.Bool
open import Calf.Types.Nat
open import Calf.Types.List
open import Calf.Types.Eq
open import Calf.Types.Bounded costMonoid

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; module ≡-Reasoning)
open import Data.Product using (_×_; _,_; ∃; proj₁; proj₂)
open import Data.Sum using (inj₁; inj₂)
open import Data.Nat as Nat using (ℕ; zero; suc; z≤n; s≤s; _+_; _*_; ⌊_/2⌋; ⌈_/2⌉; pred; _⊔_)
open import Data.Nat.Properties as N using (module ≤-Reasoning)
open import Data.Nat.Log2
open import Data.Nat.PredExp2

open import Examples.Sorting.Parallel.MergeSort.Split M

triple = Σ++ (list A) λ _ → Σ++ A λ _ → (list A)

splitMid/clocked : cmp (Π nat λ k → Π (list A) λ l → Π (U (meta (k Nat.< length l))) λ _ → F triple)
splitMid/clocked zero    (x ∷ xs) (s≤s h) = ret ([] , x , xs)
splitMid/clocked (suc k) (x ∷ xs) (s≤s h) =
  bind (F triple) (splitMid/clocked k xs h) λ (l₁ , mid , l₂) → ret ((x ∷ l₁) , mid , l₂)

splitMid/clocked/correct : ∀ k k' l h → k + suc k' ≡ length l →
  ◯ (∃ λ l₁ → ∃ λ mid → ∃ λ l₂ → splitMid/clocked k l h ≡ ret (l₁ , mid , l₂) × length l₁ ≡ k × length l₂ ≡ k' × l ≡ (l₁ ++ [ mid ] ++ l₂))
splitMid/clocked/correct zero    k' (x ∷ xs) (s≤s h) refl     u = [] , x , xs , refl , refl , refl , refl
splitMid/clocked/correct (suc k) k' (x ∷ xs) (s≤s h) h-length u =
  let (l₁ , mid , l₂ , ≡ , h₁ , h₂ , ≡-↭) = splitMid/clocked/correct k k' xs h (N.suc-injective h-length) u in
  x ∷ l₁ , mid , l₂ , Eq.cong (λ e → bind (F triple) e _) ≡ , Eq.cong suc h₁ , h₂ , Eq.cong (x ∷_) ≡-↭

splitMid/clocked/cost : cmp (Π nat λ k → Π (list A) λ l → Π (U (meta (k Nat.< length l))) λ _ → cost)
splitMid/clocked/cost _ _ _ = 𝟘

splitMid/clocked≤splitMid/clocked/cost : ∀ k l h → IsBounded triple (splitMid/clocked k l h) (splitMid/clocked/cost k l h)
splitMid/clocked≤splitMid/clocked/cost zero    (x ∷ xs) (s≤s h) = bound/ret
splitMid/clocked≤splitMid/clocked/cost (suc k) (x ∷ xs) (s≤s h) =
  bound/bind/const 𝟘 𝟘 (splitMid/clocked≤splitMid/clocked/cost k xs h) λ _ → bound/ret

splitMid : cmp (Π (list A) λ l → Π (U (meta (0 Nat.< length l))) λ _ → F triple)
splitMid (x ∷ xs) (s≤s h) = splitMid/clocked ⌊ length (x ∷ xs) /2⌋ (x ∷ xs) (N.⌊n/2⌋<n _)

splitMid/correct : ∀ l h →
  ◯ (∃ λ l₁ → ∃ λ mid → ∃ λ l₂ → splitMid l h ≡ ret (l₁ , mid , l₂) × length l₁ Nat.≤ ⌊ length l /2⌋ × length l₂ Nat.≤ ⌊ length l /2⌋ × l ≡ (l₁ ++ [ mid ] ++ l₂))
splitMid/correct (x ∷ xs) (s≤s h) u =
  let (l₁ , mid , l₂ , ≡ , h₁ , h₂ , ≡-↭) = splitMid/clocked/correct ⌊ length (x ∷ xs) /2⌋ ⌊ pred (length (x ∷ xs)) /2⌋ (x ∷ xs) (N.⌊n/2⌋<n _)
                                              (let open ≡-Reasoning in
                                              begin
                                                ⌊ length (x ∷ xs) /2⌋ + suc ⌊ pred (length (x ∷ xs)) /2⌋
                                              ≡⟨⟩
                                                ⌊ length (x ∷ xs) /2⌋ + suc ⌊ length xs /2⌋
                                              ≡⟨⟩
                                                ⌈ length xs /2⌉ + suc ⌊ length xs /2⌋
                                              ≡⟨ N.+-suc ⌈ length xs /2⌉ ⌊ length xs /2⌋ ⟩
                                                suc (⌈ length xs /2⌉ + ⌊ length xs /2⌋)
                                              ≡⟨ Eq.cong suc (N.+-comm ⌈ length xs /2⌉ ⌊ length xs /2⌋) ⟩
                                                suc (⌊ length xs /2⌋ + ⌈ length xs /2⌉)
                                              ≡⟨ Eq.cong suc (N.⌊n/2⌋+⌈n/2⌉≡n (length xs)) ⟩
                                                suc (length xs)
                                              ≡⟨⟩
                                                length (x ∷ xs)
                                              ∎) u in
  l₁ , mid , l₂ , ≡ , N.≤-reflexive h₁ , (
    let open ≤-Reasoning in
    begin
      length l₂
    ≡⟨ h₂ ⟩
      ⌊ pred (length (x ∷ xs)) /2⌋
    ≤⟨ N.⌊n/2⌋-mono N.pred[n]≤n ⟩
      ⌊ length (x ∷ xs) /2⌋
    ∎
  ), ≡-↭

splitMid/cost : cmp (Π (list A) λ l → Π (U (meta (0 Nat.< length l))) λ _ → cost)
splitMid/cost (x ∷ xs) (s≤s h) = splitMid/clocked/cost ⌊ length (x ∷ xs) /2⌋ (x ∷ xs) (N.⌊n/2⌋<n _)

splitMid≤splitMid/cost : ∀ l h → IsBounded triple (splitMid l h) (splitMid/cost l h)
splitMid≤splitMid/cost (x ∷ xs) (s≤s h) = splitMid/clocked≤splitMid/clocked/cost ⌊ length (x ∷ xs) /2⌋ (x ∷ xs) (N.⌊n/2⌋<n _)

splitBy/clocked : cmp (Π nat λ _ → Π (list A) λ _ → Π A λ _ → F pair)
splitBy/clocked/aux : cmp (Π nat λ _ → Π A λ _ → Π (list A) λ _ → Π A λ _ → Π (list A) λ _ → Π bool λ _ → F pair)

splitBy/clocked zero    l        pivot = ret ([] , l)
splitBy/clocked (suc k) []       pivot = ret ([] , [])
splitBy/clocked (suc k) (x ∷ xs) pivot =
  bind (F pair) (splitMid (x ∷ xs) (s≤s z≤n)) λ (l₁ , mid , l₂) →
    bind (F pair) (mid ≤ᵇ pivot) (splitBy/clocked/aux k pivot l₁ mid l₂)

splitBy/clocked/aux k pivot l₁ mid l₂ false =
  bind (F pair) (splitBy/clocked k l₁ pivot) λ (l₁₁ , l₁₂) → ret (l₁₁ , l₁₂ ++ mid ∷ l₂)
splitBy/clocked/aux k pivot l₁ mid l₂ true  =
  bind (F pair) (splitBy/clocked k l₂ pivot) λ (l₂₁ , l₂₂) → ret (l₁ ++ mid ∷ l₂₁ , l₂₂)

splitBy/clocked/correct : ∀ k l pivot → ⌈log₂ suc (length l) ⌉ Nat.≤ k →
  ◯ (∃ λ l₁ → ∃ λ l₂ → splitBy/clocked k l pivot ≡ ret (l₁ , l₂) × (Sorted l → All (_≤ pivot) l₁ × All (pivot ≤_) l₂) × l ≡ (l₁ ++ l₂))
splitBy/clocked/correct zero    l        pivot h u with ⌈log₂n⌉≡0⇒n≤1 {suc (length l)} (N.n≤0⇒n≡0 h)
splitBy/clocked/correct zero    []       pivot h u | s≤s z≤n = [] , [] , refl , (λ _ → [] , []) , refl
splitBy/clocked/correct (suc k) []       pivot h u = [] , [] , refl , (λ _ → [] , []) , refl
splitBy/clocked/correct (suc k) (x ∷ xs) pivot (s≤s h) u with splitMid/correct (x ∷ xs) (s≤s z≤n) u
splitBy/clocked/correct (suc k) (x ∷ xs) pivot (s≤s h) u | (l₁ , mid , l₂ , ≡ , h₁ , h₂ , ≡-↭) with h-cost mid pivot
splitBy/clocked/correct (suc k) (x ∷ xs) pivot (s≤s h) u | (l₁ , mid , l₂ , ≡ , h₁ , h₂ , ≡-↭) | ⇓ b withCost q [ _ , h-eq ]
  with ≤ᵇ-reflects-≤ u (Eq.trans (eq/ref h-eq) (step/ext (F bool) (ret b) q u)) | ≤-total mid pivot
splitBy/clocked/correct (suc k) (x ∷ xs) pivot (s≤s h) u | (l₁ , mid , l₂ , ≡ , h₁ , h₂ , ≡-↭) | ⇓ b     withCost q [ _ , h-eq ] | ofⁿ ¬p | inj₁ mid≤pivot = contradiction mid≤pivot ¬p
splitBy/clocked/correct (suc k) (x ∷ xs) pivot (s≤s h) u | (l₁ , mid , l₂ , ≡ , h₁ , h₂ , ≡-↭) | ⇓ false withCost q [ _ , h-eq ] | ofⁿ ¬p | inj₂ pivot≤mid =
  let (l₁₁ , l₁₂ , ≡' , h-sorted , ≡-↭') = splitBy/clocked/correct k l₁ pivot (
                                              let open ≤-Reasoning in
                                              begin
                                                ⌈log₂ suc (length l₁) ⌉
                                              ≤⟨ log₂-mono (s≤s h₁) ⟩
                                                ⌈log₂ suc ⌊ length (x ∷ xs) /2⌋ ⌉
                                              ≤⟨ h ⟩
                                                k
                                              ∎
                                            ) u in
  l₁₁ , l₁₂ ++ mid ∷ l₂ , (
    let open ≡-Reasoning in
    begin
      splitBy/clocked (suc k) (x ∷ xs) pivot
    ≡⟨⟩
      (bind (F pair) (splitMid (x ∷ xs) (s≤s z≤n)) λ (l₁ , mid , l₂) →
        bind (F pair) (mid ≤ᵇ pivot) (splitBy/clocked/aux k pivot l₁ mid l₂))
    ≡⟨ Eq.cong (λ e → bind (F pair) e _) (≡) ⟩
      bind (F pair) (mid ≤ᵇ pivot) (splitBy/clocked/aux k pivot l₁ mid l₂)
    ≡⟨ Eq.cong (λ e → bind (F pair) e (splitBy/clocked/aux k pivot l₁ mid l₂)) (eq/ref h-eq) ⟩
      step (F pair) q (splitBy/clocked/aux k pivot l₁ mid l₂ false)
    ≡⟨ step/ext (F pair) (splitBy/clocked/aux k pivot l₁ mid l₂ false) q u ⟩
      splitBy/clocked/aux k pivot l₁ mid l₂ false
    ≡⟨⟩
      (bind (F pair) (splitBy/clocked k l₁ pivot) λ (l₁₁ , l₁₂) → ret (l₁₁ , l₁₂ ++ mid ∷ l₂))
    ≡⟨ Eq.cong (λ e → bind (F pair) e _) ≡' ⟩
      ret (l₁₁ , l₁₂ ++ mid ∷ l₂)
    ∎
  ) , (
    λ sorted →
      let sorted' = Eq.subst Sorted ≡-↭ sorted in
      let (h₁₁ , h₁₂) = h-sorted (++⁻ˡ l₁ sorted') in
      h₁₁ , ++⁺-All h₁₂ (pivot≤mid ∷ ≤-≤* pivot≤mid (uncons₁ (++⁻ʳ l₁ sorted')))
  ) , (
    let open ≡-Reasoning in
    begin
      (x ∷ xs)
    ≡⟨ ≡-↭ ⟩
      l₁ ++ mid ∷ l₂
    ≡⟨ Eq.cong (_++ (mid ∷ l₂)) ≡-↭' ⟩
      (l₁₁ ++ l₁₂) ++ mid ∷ l₂
    ≡⟨ ++-assoc l₁₁ l₁₂ (mid ∷ l₂) ⟩
      l₁₁ ++ (l₁₂ ++ mid ∷ l₂)
    ∎
  )
splitBy/clocked/correct (suc k) (x ∷ xs) pivot (s≤s h) u | (l₁ , mid , l₂ , ≡ , h₁ , h₂ , ≡-↭) | ⇓ true withCost q [ _ , h-eq ] | ofʸ p  | _              =
  let (l₂₁ , l₂₂ , ≡' , h-sorted , ≡-↭') = splitBy/clocked/correct k l₂ pivot (
                                              let open ≤-Reasoning in
                                              begin
                                                ⌈log₂ suc (length l₂) ⌉
                                              ≤⟨ log₂-mono (s≤s h₂) ⟩
                                                ⌈log₂ suc ⌊ length (x ∷ xs) /2⌋ ⌉
                                              ≤⟨ h ⟩
                                                k
                                              ∎
                                            ) u in
  l₁ ++ mid ∷ l₂₁ , l₂₂ , (
    let open ≡-Reasoning in
    begin
      splitBy/clocked (suc k) (x ∷ xs) pivot
    ≡⟨⟩
      (bind (F pair) (splitMid (x ∷ xs) (s≤s z≤n)) λ (l₁ , mid , l₂) →
        bind (F pair) (mid ≤ᵇ pivot) (splitBy/clocked/aux k pivot l₁ mid l₂))
    ≡⟨ Eq.cong (λ e → bind (F pair) e _) (≡) ⟩
      bind (F pair) (mid ≤ᵇ pivot) (splitBy/clocked/aux k pivot l₁ mid l₂)
    ≡⟨ Eq.cong (λ e → bind (F pair) e (splitBy/clocked/aux k pivot l₁ mid l₂)) (eq/ref h-eq) ⟩
      step (F pair) q (splitBy/clocked/aux k pivot l₁ mid l₂ true)
    ≡⟨ step/ext (F pair) (splitBy/clocked/aux k pivot l₁ mid l₂ true) q u ⟩
      splitBy/clocked/aux k pivot l₁ mid l₂ true
    ≡⟨⟩
      (bind (F pair) (splitBy/clocked k l₂ pivot) λ (l₂₁ , l₂₂) → ret (l₁ ++ mid ∷ l₂₁ , l₂₂))
    ≡⟨ Eq.cong (λ e → bind (F pair) e _) ≡' ⟩
      ret (l₁ ++ mid ∷ l₂₁ , l₂₂)
    ∎
  ) , (
    λ sorted →
      let sorted' = Eq.subst Sorted ≡-↭ sorted in
      let (h₂₁ , h₂₂) = h-sorted (uncons₂ (++⁻ʳ l₁ sorted')) in
      ++⁺-All
        (map (λ h → ≤-trans h p) (split-sorted₁ l₁ (++⁻ˡ (l₁ ∷ʳ mid) (Eq.subst Sorted (Eq.sym (++-assoc l₁ [ mid ] l₂)) sorted'))))
        (p ∷ h₂₁) ,
      h₂₂
  ) , (
    let open ≡-Reasoning in
    begin
      (x ∷ xs)
    ≡⟨ ≡-↭ ⟩
      l₁ ++ mid ∷ l₂
    ≡⟨ Eq.cong (λ l₂ → l₁ ++ mid ∷ l₂) ≡-↭' ⟩
      l₁ ++ mid ∷ (l₂₁ ++ l₂₂)
    ≡˘⟨ ++-assoc l₁ (mid ∷ l₂₁) l₂₂ ⟩
      (l₁ ++ mid ∷ l₂₁) ++ l₂₂
    ∎
  )

splitBy/clocked/cost : cmp (Π nat λ _ → Π (list A) λ _ → Π A λ _ → cost)
splitBy/clocked/cost/aux : cmp (Π nat λ _ → Π A λ _ → Π (list A) λ _ → Π A λ _ → Π (list A) λ _ → Π bool λ _ → cost)

splitBy/clocked/cost zero    l        pivot = 𝟘
splitBy/clocked/cost (suc k) []       pivot = 𝟘
splitBy/clocked/cost (suc k) (x ∷ xs) pivot =
  bind cost (splitMid (x ∷ xs) (s≤s z≤n)) λ (l₁ , mid , l₂) → splitMid/cost (x ∷ xs) (s≤s z≤n) ⊕
    bind cost (mid ≤ᵇ pivot) λ b → (1 , 1) ⊕ splitBy/clocked/cost/aux k pivot l₁ mid l₂ b

splitBy/clocked/cost/aux k pivot l₁ mid l₂ false =
  bind cost (splitBy/clocked k l₁ pivot) λ (l₁₁ , l₁₂) → splitBy/clocked/cost k l₁ pivot ⊕ 𝟘
splitBy/clocked/cost/aux k pivot l₁ mid l₂ true  =
  bind cost (splitBy/clocked k l₂ pivot) λ (l₂₁ , l₂₂) → splitBy/clocked/cost k l₂ pivot ⊕ 𝟘

splitBy/clocked/cost/closed : cmp (Π nat λ _ → Π (list A) λ _ → Π A λ _ → cost)
splitBy/clocked/cost/closed k _ _ = k , k

splitBy/clocked/cost≤splitBy/clocked/cost/closed : ∀ k l pivot → ⌈log₂ suc (length l) ⌉ Nat.≤ k →
  ◯ (splitBy/clocked/cost k l pivot ≤ₚ splitBy/clocked/cost/closed k l pivot)
splitBy/clocked/cost/aux≤k : ∀ k pivot l₁ mid l₂ b → ⌈log₂ suc (length l₁) ⌉ Nat.≤ k → ⌈log₂ suc (length l₂) ⌉ Nat.≤ k →
  ◯ (splitBy/clocked/cost/aux k pivot l₁ mid l₂ b ≤ₚ (k , k))

splitBy/clocked/cost≤splitBy/clocked/cost/closed zero    l        pivot h u = z≤n , z≤n
splitBy/clocked/cost≤splitBy/clocked/cost/closed (suc k) []       pivot h u = z≤n , z≤n
splitBy/clocked/cost≤splitBy/clocked/cost/closed (suc k) (x ∷ xs) pivot (s≤s h) u with splitMid/correct (x ∷ xs) (s≤s z≤n) u
... | (l₁ , mid , l₂ , ≡ , h₁ , h₂ , ≡-↭) with h-cost mid pivot
... | ⇓ b withCost q [ _ , h-eq ] =
  begin
    splitBy/clocked/cost (suc k) (x ∷ xs) pivot
  ≡⟨⟩
    (bind cost (splitMid (x ∷ xs) (s≤s z≤n)) λ (l₁ , mid , l₂) → splitMid/cost (x ∷ xs) (s≤s z≤n) ⊕
      bind cost (mid ≤ᵇ pivot) λ b → (1 , 1) ⊕ splitBy/clocked/cost/aux k pivot l₁ mid l₂ b)
  ≡⟨ Eq.cong (λ e → bind cost e _) (≡) ⟩
    (splitMid/cost (x ∷ xs) (s≤s z≤n) ⊕
      bind cost (mid ≤ᵇ pivot) λ b → (1 , 1) ⊕ splitBy/clocked/cost/aux k pivot l₁ mid l₂ b)
  ≡⟨⟩
    (𝟘 ⊕
      bind cost (mid ≤ᵇ pivot) λ b → (1 , 1) ⊕ splitBy/clocked/cost/aux k pivot l₁ mid l₂ b)
  ≡⟨ ⊕-identityˡ _ ⟩
    (bind cost (mid ≤ᵇ pivot) λ b → (1 , 1) ⊕ splitBy/clocked/cost/aux k pivot l₁ mid l₂ b)
  ≡⟨ Eq.cong (λ e → bind cost e λ b → (1 , 1) ⊕ splitBy/clocked/cost/aux k pivot l₁ mid l₂ b) (eq/ref h-eq) ⟩
    step cost q ((1 , 1) ⊕ splitBy/clocked/cost/aux k pivot l₁ mid l₂ b)
  ≡⟨ step/ext cost _ q u ⟩
    (1 , 1) ⊕ splitBy/clocked/cost/aux k pivot l₁ mid l₂ b
  ≤⟨
    ⊕-monoʳ-≤ (1 , 1) (
      splitBy/clocked/cost/aux≤k k pivot l₁ mid l₂ b
        (N.≤-trans (log₂-mono (s≤s h₁)) h)
        (N.≤-trans (log₂-mono (s≤s h₂)) h)
        u
    )
  ⟩
    (1 , 1) ⊕ (k , k)
  ≡⟨⟩
    (suc k , suc k)
  ≡⟨⟩
    splitBy/clocked/cost/closed (suc k) (x ∷ xs) pivot
  ∎
    where open ≤ₚ-Reasoning

splitBy/clocked/cost/aux≤k k pivot l₁ mid l₂ false h₁ h₂ u =
  let (l₁₁ , l₁₂ , ≡' , _ , ≡-↭') = splitBy/clocked/correct k l₁ pivot h₁ u in
  begin
    splitBy/clocked/cost/aux k pivot l₁ mid l₂ false
  ≡⟨⟩
    (bind cost (splitBy/clocked k l₁ pivot) λ (l₁₁ , l₁₂) → splitBy/clocked/cost k l₁ pivot ⊕ 𝟘)
  ≡⟨ Eq.cong (λ e → bind cost e λ (l₁₁ , l₁₂) → splitBy/clocked/cost k l₁ pivot ⊕ 𝟘) ≡' ⟩
    splitBy/clocked/cost k l₁ pivot ⊕ 𝟘
  ≡⟨ ⊕-identityʳ _ ⟩
    splitBy/clocked/cost k l₁ pivot
  ≤⟨ splitBy/clocked/cost≤splitBy/clocked/cost/closed k l₁ pivot h₁ u ⟩
    (k , k)
  ∎
    where open ≤ₚ-Reasoning
splitBy/clocked/cost/aux≤k k pivot l₁ mid l₂ true  h₁ h₂ u =
  let (l₂₁ , l₂₂ , ≡' , _ , ≡-↭') = splitBy/clocked/correct k l₂ pivot h₂ u in
  begin
    splitBy/clocked/cost/aux k pivot l₁ mid l₂ true
  ≡⟨⟩
    (bind cost (splitBy/clocked k l₂ pivot) λ (l₂₁ , l₂₂) → splitBy/clocked/cost k l₂ pivot ⊕ 𝟘)
  ≡⟨ Eq.cong (λ e → bind cost e λ (l₂₁ , l₂₂) → splitBy/clocked/cost k l₂ pivot ⊕ 𝟘) ≡' ⟩
    splitBy/clocked/cost k l₂ pivot ⊕ 𝟘
  ≡⟨ ⊕-identityʳ _ ⟩
    splitBy/clocked/cost k l₂ pivot
  ≤⟨ splitBy/clocked/cost≤splitBy/clocked/cost/closed k l₂ pivot h₂ u ⟩
    (k , k)
  ∎
    where open ≤ₚ-Reasoning

splitBy/clocked≤splitBy/clocked/cost : ∀ k l pivot → IsBounded pair (splitBy/clocked k l pivot) (splitBy/clocked/cost k l pivot)
splitBy/clocked≤splitBy/clocked/cost zero    l        pivot = bound/ret
splitBy/clocked≤splitBy/clocked/cost (suc k) []       pivot = bound/ret
splitBy/clocked≤splitBy/clocked/cost (suc k) (x ∷ xs) pivot =
  bound/bind {e = splitMid (x ∷ xs) (s≤s z≤n)} (splitMid/cost (x ∷ xs) (s≤s z≤n)) _ (splitMid≤splitMid/cost (x ∷ xs) (s≤s z≤n)) λ (l₁ , mid , l₂) →
    bound/bind (1 , 1) _ (h-cost mid pivot)
      λ { false → bound/bind (splitBy/clocked/cost k l₁ pivot) (λ _ → 𝟘) (splitBy/clocked≤splitBy/clocked/cost k l₁ pivot) λ _ → bound/ret
        ; true  → bound/bind (splitBy/clocked/cost k l₂ pivot) (λ _ → 𝟘) (splitBy/clocked≤splitBy/clocked/cost k l₂ pivot) λ _ → bound/ret }

splitBy/clocked≤splitBy/clocked/cost/closed : ∀ k l pivot → ⌈log₂ suc (length l) ⌉ Nat.≤ k → IsBounded pair (splitBy/clocked k l pivot) (splitBy/clocked/cost/closed k l pivot)
splitBy/clocked≤splitBy/clocked/cost/closed k l pivot h = bound/relax (splitBy/clocked/cost≤splitBy/clocked/cost/closed k l pivot h) (splitBy/clocked≤splitBy/clocked/cost k l pivot)

splitBy : cmp (Π (list A) λ _ → Π A λ _ → F pair)
splitBy l pivot = splitBy/clocked ⌈log₂ suc (length l) ⌉ l pivot

splitBy/correct : ∀ l pivot →
  ◯ (∃ λ l₁ → ∃ λ l₂ → splitBy l pivot ≡ ret (l₁ , l₂) × (Sorted l → All (_≤ pivot) l₁ × All (pivot ≤_) l₂) × l ≡ (l₁ ++ l₂))
splitBy/correct l pivot = splitBy/clocked/correct ⌈log₂ suc (length l) ⌉ l pivot N.≤-refl

splitBy/cost : cmp (Π (list A) λ _ → Π A λ _ → cost)
splitBy/cost l pivot = splitBy/clocked/cost ⌈log₂ suc (length l) ⌉ l pivot

splitBy/cost/closed : cmp (Π (list A) λ _ → Π A λ _ → cost)
splitBy/cost/closed l pivot = splitBy/clocked/cost/closed ⌈log₂ suc (length l) ⌉ l pivot

splitBy≤splitBy/cost : ∀ l pivot → IsBounded pair (splitBy l pivot) (splitBy/cost l pivot)
splitBy≤splitBy/cost l pivot = splitBy/clocked≤splitBy/clocked/cost ⌈log₂ suc (length l) ⌉ l pivot

splitBy≤splitBy/cost/closed : ∀ l pivot → IsBounded pair (splitBy l pivot) (splitBy/cost/closed l pivot)
splitBy≤splitBy/cost/closed l pivot = splitBy/clocked≤splitBy/clocked/cost/closed ⌈log₂ suc (length l) ⌉ l pivot N.≤-refl

merge/clocked : cmp (Π nat λ _ → Π pair λ _ → F (list A))
merge/clocked zero    (l₁     , l₂) = ret (l₁ ++ l₂)
merge/clocked (suc k) ([]     , l₂) = ret l₂
merge/clocked (suc k) (x ∷ l₁ , l₂) =
  bind (F (list A)) (splitMid (x ∷ l₁) (s≤s z≤n)) λ (l₁₁ , pivot , l₁₂) →
    bind (F (list A)) (splitBy l₂ pivot) λ (l₂₁ , l₂₂) →
      bind (F (list A)) (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') →
        ret (l₁' ++ pivot ∷ l₂')

merge/clocked/correct : ∀ k l₁ l₂ → ⌈log₂ suc (length l₁) ⌉ Nat.≤ k →
  ◯ (∃ λ l → merge/clocked k (l₁ , l₂) ≡ ret l × (Sorted l₁ → Sorted l₂ → SortedOf (l₁ ++ l₂) l))
merge/clocked/correct zero    l₁       l₂ h-clock u with ⌈log₂n⌉≡0⇒n≤1 {suc (length l₁)} (N.n≤0⇒n≡0 h-clock)
merge/clocked/correct zero    []       l₂ h-clock u | s≤s z≤n = l₂ , refl , (λ sorted₁ sorted₂ → refl , sorted₂)
merge/clocked/correct (suc k) []       l₂ h-clock u = l₂ , refl , (λ sorted₁ sorted₂ → refl , sorted₂)
merge/clocked/correct (suc k) (x ∷ l₁) l₂ h-clock u =
  let (l₁₁ , pivot , l₁₂ , ≡ , h₁₁ , h₁₂ , ≡-↭) = splitMid/correct (x ∷ l₁) (s≤s z≤n) u in
  let (l₂₁ , l₂₂ , ≡' , h-sorted₂ , ≡-↭') = splitBy/correct l₂ pivot u in
  let (l₁' , ≡₁' , h-sorted₁') = merge/clocked/correct k l₁₁ l₂₁
                                  (let open ≤-Reasoning in
                                  begin
                                    ⌈log₂ suc (length l₁₁) ⌉
                                  ≤⟨ log₂-mono (s≤s h₁₁) ⟩
                                    ⌈log₂ ⌈ suc (length (x ∷ l₁)) /2⌉ ⌉
                                  ≤⟨ log₂-suc (suc (length (x ∷ l₁))) h-clock ⟩
                                    k
                                  ∎)
                                  u in
  let (l₂' , ≡₂' , h-sorted₂') = merge/clocked/correct k l₁₂ l₂₂
                                  (let open ≤-Reasoning in
                                  begin
                                    ⌈log₂ suc (length l₁₂) ⌉
                                  ≤⟨ log₂-mono (s≤s h₁₂) ⟩
                                    ⌈log₂ ⌈ suc (length (x ∷ l₁)) /2⌉ ⌉
                                  ≤⟨ log₂-suc (suc (length (x ∷ l₁))) h-clock ⟩
                                    k
                                  ∎)
                                  u in
  l₁' ++ pivot ∷ l₂' , (
    let open ≡-Reasoning in
    begin
      merge/clocked (suc k) (x ∷ l₁ , l₂)
    ≡⟨⟩
      (bind (F (list A)) (splitMid (x ∷ l₁) (s≤s z≤n)) λ (l₁₁ , pivot , l₁₂) →
        bind (F (list A)) (splitBy l₂ pivot) λ (l₂₁ , l₂₂) →
          bind (F (list A)) (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') →
            ret (l₁' ++ pivot ∷ l₂'))
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e _) (≡) ⟩
      (bind (F (list A)) (splitBy l₂ pivot) λ (l₂₁ , l₂₂) →
        bind (F (list A)) (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') →
          ret (l₁' ++ pivot ∷ l₂'))
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e _) (≡') ⟩
      (bind (F (list A)) (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') →
        ret (l₁' ++ pivot ∷ l₂'))
    ≡⟨ Eq.cong (λ e → bind (F (list A)) e _) (Eq.cong₂ _&_ ≡₁' ≡₂') ⟩
      ret (l₁' ++ pivot ∷ l₂')
    ∎
  ) ,
  λ sorted₁ sorted₂ →
    let (h₂₁ , h₂₂) = h-sorted₂ sorted₂ in
    let sorted₁ = Eq.subst Sorted ≡-↭  sorted₁
        sorted₂ = Eq.subst Sorted ≡-↭' sorted₂ in
    let (↭₁' , sorted₁') = h-sorted₁'          (++⁻ˡ l₁₁ sorted₁)  (++⁻ˡ l₂₁ sorted₂)
        (↭₂' , sorted₂') = h-sorted₂' (uncons₂ (++⁻ʳ l₁₁ sorted₁)) (++⁻ʳ l₂₁ sorted₂) in
    (
      let open PermutationReasoning in
      begin
        (x ∷ l₁) ++ l₂
      ≡⟨ Eq.cong₂ (_++_) ≡-↭ ≡-↭' ⟩
        (l₁₁ ++ pivot ∷ l₁₂) ++ (l₂₁ ++ l₂₂)
      ≡⟨ ++-assoc l₁₁ (pivot ∷ l₁₂) (l₂₁ ++ l₂₂) ⟩
        l₁₁ ++ (pivot ∷ l₁₂ ++ (l₂₁ ++ l₂₂))
      ↭⟨ ++⁺ˡ-↭ l₁₁ (++⁺ˡ-↭ (pivot ∷ l₁₂) (++-comm-↭ l₂₁ l₂₂)) ⟩
        l₁₁ ++ (pivot ∷ l₁₂ ++ (l₂₂ ++ l₂₁))
      ≡˘⟨ Eq.cong (l₁₁ ++_) (++-assoc (pivot ∷ l₁₂) l₂₂ l₂₁) ⟩
        l₁₁ ++ ((pivot ∷ l₁₂ ++ l₂₂) ++ l₂₁)
      ↭⟨ ++⁺ˡ-↭ l₁₁ (++-comm-↭ (pivot ∷ l₁₂ ++ l₂₂) l₂₁) ⟩
        l₁₁ ++ (l₂₁ ++ (pivot ∷ l₁₂ ++ l₂₂))
      ≡˘⟨ ++-assoc l₁₁ l₂₁ (pivot ∷ l₁₂ ++ l₂₂) ⟩
        (l₁₁ ++ l₂₁) ++ (pivot ∷ l₁₂ ++ l₂₂)
      ≡⟨⟩
        (l₁₁ ++ l₂₁) ++ pivot ∷ (l₁₂ ++ l₂₂)
      ↭⟨ ++⁺-↭ ↭₁' (prep pivot ↭₂') ⟩
        l₁' ++ pivot ∷ l₂'
      ∎
    ) ,
    join-sorted
      sorted₁'
      sorted₂'
      (All-resp-↭ ↭₁' (++⁺-All (split-sorted₁ l₁₁ (++⁻ˡ (l₁₁ ∷ʳ pivot) (Eq.subst Sorted (Eq.sym (++-assoc l₁₁ [ pivot ] l₁₂)) sorted₁))) h₂₁))
      (All-resp-↭ ↭₂' (++⁺-All (uncons₁ (++⁻ʳ l₁₁ sorted₁)) h₂₂))

merge/clocked/cost : cmp (Π nat λ _ → Π pair λ _ → cost)
merge/clocked/cost zero    (l₁     , l₂) = 𝟘
merge/clocked/cost (suc k) ([]     , l₂) = 𝟘
merge/clocked/cost (suc k) (x ∷ l₁ , l₂) =
  bind cost (splitMid (x ∷ l₁) (s≤s z≤n)) λ (l₁₁ , pivot , l₁₂) → splitMid/cost (x ∷ l₁) (s≤s z≤n) ⊕
    bind cost (splitBy l₂ pivot) λ (l₂₁ , l₂₂) → splitBy/cost/closed l₂ pivot ⊕
      bind cost (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') → (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) ⊕
        𝟘

merge/clocked/cost/closed : cmp (Π nat λ _ → Π pair λ _ → cost)
merge/clocked/cost/closed k (l₁ , l₂) = pred[2^ k ] * ⌈log₂ suc (length l₂) ⌉ , k * ⌈log₂ suc (length l₂) ⌉

merge/clocked/cost≤merge/clocked/cost/closed : ∀ k l₁ l₂ → ⌈log₂ suc (length l₁) ⌉ Nat.≤ k →
  ◯ (merge/clocked/cost k (l₁ , l₂) ≤ₚ merge/clocked/cost/closed k (l₁ , l₂))
merge/clocked/cost≤merge/clocked/cost/closed zero    l₁       l₂ h-clock u = z≤n , z≤n
merge/clocked/cost≤merge/clocked/cost/closed (suc k) []       l₂ h-clock u = z≤n , z≤n
merge/clocked/cost≤merge/clocked/cost/closed (suc k) (x ∷ l₁) l₂ h-clock u =
  let (l₁₁ , pivot , l₁₂ , ≡-splitMid , h₁₁ , h₁₂ , ≡-↭) = splitMid/correct (x ∷ l₁) (s≤s z≤n) u in
  let (l₂₁ , l₂₂ , ≡' , _ , ≡-↭') = splitBy/correct l₂ pivot u in
  let h₁ : ⌈log₂ suc (length l₁₁) ⌉ Nat.≤ k
      h₁ =
        let open ≤-Reasoning in
        begin
          ⌈log₂ suc (length l₁₁) ⌉
        ≤⟨ log₂-mono (s≤s h₁₁) ⟩
          ⌈log₂ ⌈ suc (length (x ∷ l₁)) /2⌉ ⌉
        ≤⟨ log₂-suc (suc (length (x ∷ l₁))) h-clock ⟩
          k
        ∎

      h₂ : ⌈log₂ suc (length l₁₂) ⌉ Nat.≤ k
      h₂ =
        let open ≤-Reasoning in
        begin
          ⌈log₂ suc (length l₁₂) ⌉
        ≤⟨ log₂-mono (s≤s h₁₂) ⟩
          ⌈log₂ ⌈ suc (length (x ∷ l₁)) /2⌉ ⌉
        ≤⟨ log₂-suc (suc (length (x ∷ l₁))) h-clock ⟩
          k
        ∎
  in
  let (l₁' , ≡₁' , _) = merge/clocked/correct k l₁₁ l₂₁ h₁ u in
  let (l₂' , ≡₂' , _) = merge/clocked/correct k l₁₂ l₂₂ h₂ u in
  let open ≤ₚ-Reasoning in
  begin
    (bind cost (splitMid (x ∷ l₁) (s≤s z≤n)) λ (l₁₁ , pivot , l₁₂) → splitMid/cost (x ∷ l₁) (s≤s z≤n) ⊕
      bind cost (splitBy l₂ pivot) λ (l₂₁ , l₂₂) → splitBy/cost/closed l₂ pivot ⊕
        bind cost (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') → (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) ⊕
          𝟘)
  ≡⟨ Eq.cong (λ e → bind cost e λ (l₁₁ , pivot , l₁₂) → splitMid/cost (x ∷ l₁) (s≤s z≤n) ⊕ _) ≡-splitMid ⟩
    (splitMid/cost (x ∷ l₁) (s≤s z≤n) ⊕
      bind cost (splitBy l₂ pivot) λ (l₂₁ , l₂₂) → splitBy/cost/closed l₂ pivot ⊕
        bind cost (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') → (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) ⊕
          𝟘)
  ≡⟨⟩
    (𝟘 ⊕
      bind cost (splitBy l₂ pivot) λ (l₂₁ , l₂₂) → splitBy/cost/closed l₂ pivot ⊕
        bind cost (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') → (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) ⊕
          𝟘)
  ≡⟨ ⊕-identityˡ _ ⟩
    (bind cost (splitBy l₂ pivot) λ (l₂₁ , l₂₂) → splitBy/cost/closed l₂ pivot ⊕
      bind cost (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') → (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) ⊕
        𝟘)
  ≡⟨
    Eq.cong
      (λ e →
        bind cost e λ (l₂₁ , l₂₂) → splitBy/cost/closed l₂ pivot ⊕
          bind cost (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') → (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) ⊕
            𝟘)
      ≡'
  ⟩
    (splitBy/cost/closed l₂ pivot ⊕
      bind cost (merge/clocked k (l₁₁ , l₂₁) & merge/clocked k (l₁₂ , l₂₂)) λ (l₁' , l₂') → (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) ⊕
        𝟘)
  ≡⟨
    Eq.cong₂
      (λ e₁ e₂ →
        splitBy/cost/closed l₂ pivot ⊕
          bind cost (e₁ & e₂) λ (l₁' , l₂') → (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) ⊕
            𝟘)
      ≡₁'
      ≡₂' ⟩
    splitBy/cost/closed l₂ pivot ⊕ ((merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) ⊕ 𝟘)
  ≡⟨ Eq.cong (splitBy/cost/closed l₂ pivot ⊕_) (⊕-identityʳ _) ⟩
    splitBy/cost/closed l₂ pivot ⊕ (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂))
  ≤⟨
    ⊕-monoʳ-≤ (splitBy/cost/closed l₂ pivot) (
      ⊗-mono-≤
        (merge/clocked/cost≤merge/clocked/cost/closed k l₁₁ l₂₁ h₁ u)
        (merge/clocked/cost≤merge/clocked/cost/closed k l₁₂ l₂₂ h₂ u)
    )
  ⟩
    splitBy/cost/closed l₂ pivot ⊕ (merge/clocked/cost/closed k (l₁₁ , l₂₁) ⊗ merge/clocked/cost/closed k (l₁₂ , l₂₂))
  ≡⟨⟩
    (⌈log₂ suc (length l₂) ⌉ , ⌈log₂ suc (length l₂) ⌉) ⊕
      ((pred[2^ k ] * ⌈log₂ suc (length l₂₁) ⌉ , k * ⌈log₂ suc (length l₂₁) ⌉) ⊗
        (pred[2^ k ] * ⌈log₂ suc (length l₂₂) ⌉ , k * ⌈log₂ suc (length l₂₂) ⌉))
  ≤⟨
    ⊕-monoʳ-≤ (⌈log₂ suc (length l₂) ⌉ , ⌈log₂ suc (length l₂) ⌉) (
      let h-length : length l₂₁ + length l₂₂ ≡ length l₂
          h-length = Eq.sym (Eq.trans (Eq.cong length ≡-↭') (length-++ l₂₁))

          h₁ : ⌈log₂ suc (length l₂₁) ⌉ Nat.≤ ⌈log₂ suc (length l₂) ⌉
          h₁ = log₂-mono (s≤s (N.m+n≤o⇒m≤o (length l₂₁) (N.≤-reflexive h-length)))

          h₂ : ⌈log₂ suc (length l₂₂) ⌉ Nat.≤ ⌈log₂ suc (length l₂) ⌉
          h₂ = log₂-mono (s≤s (N.m+n≤o⇒n≤o (length l₂₁) (N.≤-reflexive h-length)))
      in
      ⊗-mono-≤
        (N.*-monoʳ-≤ pred[2^ k ] h₁ , N.*-monoʳ-≤ k h₁)
        (N.*-monoʳ-≤ pred[2^ k ] h₂ , N.*-monoʳ-≤ k h₂)
    )
  ⟩
    (⌈log₂ suc (length l₂) ⌉ , ⌈log₂ suc (length l₂) ⌉) ⊕
      ((pred[2^ k ] * ⌈log₂ suc (length l₂) ⌉ , k * ⌈log₂ suc (length l₂) ⌉) ⊗
        (pred[2^ k ] * ⌈log₂ suc (length l₂) ⌉ , k * ⌈log₂ suc (length l₂) ⌉))
  ≡⟨ Eq.cong₂ _,_ (arithmetic/work ⌈log₂ suc (length l₂) ⌉) (arithmetic/span ⌈log₂ suc (length l₂) ⌉) ⟩
    pred[2^ suc k ] * ⌈log₂ suc (length l₂) ⌉ , suc k * ⌈log₂ suc (length l₂) ⌉
  ≡⟨⟩
    merge/clocked/cost/closed (suc k) (x ∷ l₁ , l₂)
  ∎
    where
      arithmetic/work : ∀ n → n + (pred[2^ k ] * n + pred[2^ k ] * n) ≡ pred[2^ suc k ] * n
      arithmetic/work n =
        begin
          n + (pred[2^ k ] * n + pred[2^ k ] * n)
        ≡˘⟨ Eq.cong (n +_) (N.*-distribʳ-+ n (pred[2^ k ]) (pred[2^ k ])) ⟩
          n + (pred[2^ k ] + pred[2^ k ]) * n
        ≡⟨⟩
          suc (pred[2^ k ] + pred[2^ k ]) * n
        ≡⟨ Eq.cong (_* n) (pred[2^suc[n]] k) ⟩
          pred[2^ suc k ] * n
        ∎
          where open ≡-Reasoning

      arithmetic/span : ∀ n → n + (k * n ⊔ k * n) ≡ suc k * n
      arithmetic/span n =
        begin
          n + (k * n ⊔ k * n)
        ≡⟨ Eq.cong (n +_) (N.⊔-idem (k * n)) ⟩
          n + k * n
        ≡⟨⟩
          suc k * n
        ∎
          where open ≡-Reasoning

merge/clocked≤merge/clocked/cost : ∀ k l₁ l₂ → IsBounded (list A) (merge/clocked k (l₁ , l₂)) (merge/clocked/cost k (l₁ , l₂))
merge/clocked≤merge/clocked/cost zero    l₁       l₂ = bound/ret
merge/clocked≤merge/clocked/cost (suc k) []       l₂ = bound/ret
merge/clocked≤merge/clocked/cost (suc k) (x ∷ l₁) l₂ =
  bound/bind (splitMid/cost (x ∷ l₁) (s≤s z≤n)) _ (splitMid≤splitMid/cost (x ∷ l₁) (s≤s z≤n)) λ (l₁₁ , pivot , l₁₂) →
    bound/bind (splitBy/cost/closed l₂ pivot) _ (splitBy≤splitBy/cost/closed l₂ pivot) λ (l₂₁ , l₂₂) →
      bound/bind (merge/clocked/cost k (l₁₁ , l₂₁) ⊗ merge/clocked/cost k (l₁₂ , l₂₂)) _ (bound/par (merge/clocked≤merge/clocked/cost k l₁₁ l₂₁) (merge/clocked≤merge/clocked/cost k l₁₂ l₂₂)) λ (l₁' , l₂') →
        bound/ret

merge/clocked≤merge/clocked/cost/closed : ∀ k l₁ l₂ → ⌈log₂ suc (length l₁) ⌉ Nat.≤ k →
  IsBounded (list A) (merge/clocked k (l₁ , l₂)) (merge/clocked/cost/closed k (l₁ , l₂))
merge/clocked≤merge/clocked/cost/closed k l₁ l₂ h =
  bound/relax (merge/clocked/cost≤merge/clocked/cost/closed k l₁ l₂ h) (merge/clocked≤merge/clocked/cost k l₁ l₂)

merge : cmp (Π pair λ _ → F (list A))
merge (l₁ , l₂) = merge/clocked ⌈log₂ suc (length l₁) ⌉ (l₁ , l₂)

merge/correct : ∀ l₁ l₂ →
  ◯ (∃ λ l → merge (l₁ , l₂) ≡ ret l × (Sorted l₁ → Sorted l₂ → SortedOf (l₁ ++ l₂) l))
merge/correct l₁ l₂ = merge/clocked/correct ⌈log₂ suc (length l₁) ⌉ l₁ l₂ N.≤-refl

merge/cost : cmp (Π pair λ _ → cost)
merge/cost (l₁ , l₂) = merge/clocked/cost ⌈log₂ suc (length l₁) ⌉ (l₁ , l₂)

merge/cost/closed : cmp (Π pair λ _ → cost)
merge/cost/closed (l₁ , l₂) = merge/clocked/cost/closed ⌈log₂ suc (length l₁) ⌉ (l₁ , l₂)

merge≤merge/cost : ∀ l₁ l₂ → IsBounded (list A) (merge (l₁ , l₂)) (merge/cost (l₁ , l₂))
merge≤merge/cost l₁ l₂ = merge/clocked≤merge/clocked/cost ⌈log₂ suc (length l₁) ⌉ l₁ l₂

merge≤merge/cost/closed : ∀ l₁ l₂ → IsBounded (list A) (merge (l₁ , l₂)) (merge/cost/closed (l₁ , l₂))
merge≤merge/cost/closed l₁ l₂ = merge/clocked≤merge/clocked/cost/closed ⌈log₂ suc (length l₁) ⌉ l₁ l₂ N.≤-refl

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Data.List.Instance where

open import Category.FAM
open import Data.List
open import Data.List.Properties
open import Function using (_$_)
open import Relation.Binary.PropositionalEquality hiding ([_])

instance
    ListFunctor : ∀ {ℓ} → Functor {ℓ} List
    ListFunctor = record
        { _<$>_ = map
        ; isFunctor = record
            { identity = map-id
            ; homo = λ f g a → map-compose a
            }
        }
    ListApplicative : ∀ {ℓ} → Applicative {ℓ} List
    ListApplicative {ℓ} = record
        { pure = [_]
        ; _⊛_ = λ fs xs → concat (map (flip map xs) fs)
        ; isApplicative = record
            { identity = λ xs → begin
                    map id xs ++ []
                ≡⟨ ++-identityʳ (map id xs) ⟩
                    map id xs
                ≡⟨ map-id xs ⟩
                    xs
                ∎
            ; compose = compose
            ; homo = λ _ _ → refl
            ; interchange = interchange
            }
        }
        where
            open ≡-Reasoning
            open import Function

            concat-∷ : {A : Set ℓ} (xs : List A) (xss : List (List A))
                → concat (xs ∷ xss) ≡ xs ++ concat xss
            concat-∷ []       xss = refl
            concat-∷ (x ∷ xs) xss = refl

            concat-++ : {A : Set ℓ} (xs ys : List (List A))
                → concat (xs ++ ys) ≡ concat xs ++ concat ys
            concat-++ []         ys = refl
            concat-++ (xs ∷ xss) ys = begin
                    concat ((xs ∷ xss) ++ ys)
                ≡⟨ refl ⟩
                    concat (xs ∷ xss ++ ys)
                ≡⟨ concat-∷ xs (xss ++ ys) ⟩
                    xs ++ concat (xss ++ ys)
                ≡⟨ cong (λ x → xs ++ x) (concat-++ xss ys) ⟩
                    xs ++ concat xss ++ concat ys
                ≡⟨ sym (++-assoc xs (concat xss) (concat ys)) ⟩
                    (xs ++ concat xss) ++ concat ys
                ≡⟨ cong (λ x → x ++ concat ys) (sym (concat-∷ xs xss)) ⟩
                    concat (xs ∷ xss) ++ concat ys
                ∎

            lemma : {A B C : Set ℓ} (f : B → C) (gs : List (A → B)) (xs : List A)
                → map (flip map xs) (flip map gs (_∘′_ f)) ≡ map (map f) (map (flip map xs) gs)
            lemma f []       xs       = refl
            lemma f (g ∷ gs) xs       =
                let shit = map (flip map xs) (map (_∘′_ f) gs) in
                begin
                    flip map xs (f ∘′ g) ∷ shit
                ≡⟨ refl ⟩
                    map (f ∘′ g) xs ∷ shit
                ≡⟨ cong (λ x → x ∷ shit) (map-compose xs) ⟩
                    map f (map g xs) ∷ shit
                ≡⟨ refl ⟩
                    map f (flip map xs g) ∷ shit
                ≡⟨ cong (λ x → map f (flip map xs g) ∷ x) (lemma f gs xs) ⟩
                    map f (flip map xs g) ∷ map (map f) (map (flip map xs) gs)
                ∎

            compose : {A B C : Set ℓ} (fs : List (B → C)) (gs : List (A → B)) (xs : List A)
                → concat (map (flip map xs) (concat (map (flip map gs) (map _∘′_ fs ++ []))))
                    ≡ concat (map (flip map (concat (map (flip map xs) gs))) fs)
            compose []       gs xs = refl
            compose (f ∷ fs) gs xs =
                begin
                    concat (map (flip map xs) (concat (flip map gs (_∘′_ f) ∷ map (flip map gs) (map _∘′_ fs ++ []))))
                ≡⟨ cong (λ x → concat (map (flip map xs) x)) (concat-∷ (flip map gs (_∘′_ f)) (map (flip map gs) (map _∘′_ fs ++ []))) ⟩
                    concat (map (flip map xs) (flip map gs (_∘′_ f) ++ concat (map (flip map gs) (map _∘′_ fs ++ []))))
                ≡⟨ cong concat (map-++-commute (flip map xs) (flip map gs (_∘′_ f)) (concat (map (flip map gs) (map _∘′_ fs ++ [])))) ⟩
                    concat (map (flip map xs) (flip map gs (_∘′_ f)) ++ map (flip map xs) (concat (map (flip map gs) (map _∘′_ fs ++ []))))
                ≡⟨ concat-++ (map (flip map xs) (flip map gs (_∘′_ f))) (map (flip map xs) (concat (map (flip map gs) (map _∘′_ fs ++ [])))) ⟩
                    concat (map (flip map xs) (flip map gs (_∘′_ f))) ++ concat (map (flip map xs) (concat (map (flip map gs) (map _∘′_ fs ++ []))))
                ≡⟨ cong (λ x → concat x ++ concat (map (flip map xs) (concat (map (flip map gs) (map _∘′_ fs ++ []))))) (lemma f gs xs) ⟩
                    concat (map (map f) (map (flip map xs) gs)) ++ concat (map (flip map xs) (concat (map (flip map gs) (map _∘′_ fs ++ []))))
                ≡⟨ cong (λ x → x ++ concat (map (flip map xs) (concat (map (flip map gs) (map _∘′_ fs ++ []))))) (concat-map ((map (flip map xs) gs)))⟩
                    map f (concat (map (flip map xs) gs)) ++ concat (map (flip map xs) (concat (map (flip map gs) (map _∘′_ fs ++ []))))
                ≡⟨ refl ⟩
                    flip map (concat (map (flip map xs) gs)) f ++ concat (map (flip map xs) (concat (map (flip map gs) (map _∘′_ fs ++ []))))
                ≡⟨ cong (λ x → flip map (concat (map (flip map xs) gs)) f ++ x) (compose fs gs xs) ⟩
                    flip map (concat (map (flip map xs) gs)) f ++ concat (map (flip map (concat (map (flip map xs) gs))) fs)
                ≡⟨ sym (concat-∷ (flip map (concat (map (flip map xs) gs)) f) (map (flip map (concat (map (flip map xs) gs))) fs)) ⟩
                    concat (flip map (concat (map (flip map xs) gs)) f ∷ map (flip map (concat (map (flip map xs) gs))) fs)
                ≡⟨ refl ⟩
                    concat (map (flip map (concat (map (flip map xs) gs))) (f ∷ fs))
                ∎

            interchange : {A B : Set ℓ} (fs : List (A → B)) (x : A)
                → concat (map (flip map [ x ]) fs) ≡ concat (map (flip map fs) [ (λ g → g x) ])
            interchange [] x       = refl
            interchange (f ∷ fs) x =
                begin
                    concat (flip map [ x ] f ∷ map (flip map [ x ]) fs)
                ≡⟨ refl ⟩
                    concat (map f [ x ] ∷ map (flip map [ x ]) fs)
                ≡⟨ concat-∷ (map f [ x ]) (map (flip map [ x ]) fs) ⟩
                    map f [ x ] ++ concat (map (flip map [ x ]) fs)
                ≡⟨ cong (λ w → map f [ x ] ++ w) (interchange fs x) ⟩
                    map f [ x ] ++ map (λ z → z x) fs ++ []
                ≡⟨ refl ⟩
                    concat (flip map (f ∷ fs) (λ g → g x) ∷ [])
                ∎

max_stars_repo_name: banacorn/FAM

max_issues_repo_name: banacorn/FAM

max_forks_repo_name: banacorn/FAM


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module NumberFirstAttempt where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Binary.Base -- Rel
open import Cubical.Data.Unit.Base -- Unit

record PoorField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    Carrier : Type ℓ
    -- comm ring
    0f   : Carrier
    1f   : Carrier
    _+_  : Carrier → Carrier → Carrier
    _·_  : Carrier → Carrier → Carrier
    -_   : Carrier → Carrier
    -- lattice
    _<_  : Rel Carrier Carrier ℓ' -- stronger than _#_ and _≤_
    min  : Carrier → Carrier → Carrier
    max  : Carrier → Carrier → Carrier
    -- other
    _#_  : Rel Carrier Carrier ℓ'
    _≤_  : Rel Carrier Carrier ℓ'
    ∣_∣ᶠ' : Carrier → Σ[ x ∈ Carrier ] 0f ≤ x -- absolute value NOTE: better have `0 ≤ x` as a separate property
    _⁻¹ᶠ : (x : Carrier) → {{x # 0f}} → Carrier
    conj : Carrier → Carrier -- complex conjugation (only for ℂ; this is the identity function on ℝ)
    -- sqrt⁺ -- positive sqrt
    --       -- need that on ℝ₀⁺ to define a norm from an inner product
    --       -- on ℝ₀⁺ we have `∀ x → sqrt (x · x) ≡ x`
    -- NOTE: squares are nonnegative in an ordered field

  ∣_∣ᶠ : Carrier → Carrier -- NOTE: well, this should be "into" ℝ₀⁺
  ∣ x ∣ᶠ = fst (∣ x ∣ᶠ')

  _-_ : Carrier → Carrier → Carrier
  x - y = x + (- y)

  infix  9 _⁻¹ᶠ
  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_
  infixl 6 _-_
  infixl 4 _#_
  infixl 4 _<_
  infixl 4 _≤_

record IsℝField (PF : PoorField {ℓ} {ℓ'}) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  open PoorField PF

record Isℝ₀⁺Field (PF : PoorField {ℓ} {ℓ'}) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  open PoorField PF
  field
    isℝField : IsℝField PF
    isNonnegative : ∀ x → 0f ≤ x
  open IsℝField isℝField public

record Isℝ⁺Field (PF : PoorField {ℓ} {ℓ'}) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  open PoorField PF
  field
    isℝField : IsℝField PF
    -- NOTE: 0f is not an element of ℝ⁺, so we do not have a neutral element for addition
    --       so the following holds in a different way
    -- isPositive : ∀ x → 0f < x
  open IsℝField isℝField public

record Is𝕂Field (PF : PoorField {ℓ} {ℓ'}) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  open PoorField PF

record ℝField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    poorField : PoorField {ℓ} {ℓ'}
    isℝField : IsℝField poorField
  open PoorField poorField public
  open IsℝField isℝField public

record ℝ₀⁺Field : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    poorField : PoorField {ℓ} {ℓ'}
    isℝ₀⁺Field : Isℝ₀⁺Field poorField
  open PoorField poorField public
  open Isℝ₀⁺Field isℝ₀⁺Field public

record ℝ⁺Field : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    poorField : PoorField {ℓ} {ℓ'}
    isℝ⁺Field : Isℝ⁺Field poorField
  open PoorField poorField public
  open Isℝ⁺Field isℝ⁺Field public

record 𝕂Field : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    poorField : PoorField {ℓ} {ℓ'}
    is𝕂Field : Is𝕂Field poorField
  open PoorField poorField public
  open Is𝕂Field is𝕂Field public

postulate
  ℝℓ ℝℓ' : Level
  ℝF    : ℝField   {ℝℓ} {ℝℓ'} -- reals
  ℝ⁺F   : ℝ⁺Field  {ℝℓ} {ℝℓ'} -- positive reals without 0
  ℝ₀⁺F  : ℝ₀⁺Field {ℝℓ} {ℝℓ'} -- positive reals with 0

open ℝField ℝF using () renaming
  ( Carrier to ℝ
  )

record PoorSubField-ℝ (φ : ℝ → Type ℓ) : Type (ℓ-max ℝℓ ℓ) where
  -- module R = ℝField ℝF
  open ℝField ℝF
  field
    ι : Σ ℝ φ

  _<⁺_ : Σ ℝ φ → Σ ℝ φ → Type ℝℓ'
  _<⁺_ (x , xp) (y , yp) = x < y

module Test where
  module R =  ℝField ℝF
  φᵢ = λ(x : ℝ) → Unit

  -- the following "absorbs" different `Σ ℝ φ` ℝ-numbers and falls back to the "raw" operation from ℝ
  _+_ : {φ₁ φ₂ : ℝ → Type ℓ'} → Σ ℝ φ₁ → Σ ℝ φ₂ → Σ ℝ φᵢ
  _+_ (x , _) (y , _) = x R.+ y , tt

  -- we might add an enumeration for different φs and pattern-match on those
  data ℝ-props (x : ℝ) : Type ℝℓ where
    φ-id : Unit → ℝ-props x
    -- more ...

  -- this works for subsets of ℝ but not for inter-sort-mixing (e.g. ℕ + ℝ) .. which we do want to coerce explicitly?
  -- we could start with a number, e.g. z₀ ∈ ℕ
  -- then include it into ℝ and have a Σ ℝ φ-from-nat
  -- we could track the from-nat'ness and back-coerce this number when needed (as long as from-nat is preserved)

  {-
  data ℝ-sub (x : ℝ) : Type ℝℓ where
    φ-from-ℝ   : Unit -- default "fallback" case
    φ-from-ℕ   : Σ[ z ∈ ℕ ] ℕ↪ℝ z ≡ x -- with this we can use the `reflects`-properties of `ℕ↪ℝ` to get corresponding properties on ℕ
    φ-from-ℤ   : Σ[ z ∈ ℤ ] ℤ↪ℝ z ≡ x
    φ-from-ℚ   : Σ[ z ∈ ℚ ] ℚ↪ℝ z ≡ x
    φ-from-ℝ₀⁺ :  0f ≤ x
                ¬( x < 0f)
    φ-from-ℝ⁺  :  0f < x
    -- ... more

  -- first projection
  num : ∀{x} → ℝ-sub x → ℝ
  num p = ... cases

  -- target type "table"
  +-Coerce : (x y : ℝ-sub) → Type ℝℓ
  +-Coerce x y = ... cases

  -- implementation
  _+_ : (x y : ℝ-sub) → +-Coerce x y
  x + y = ... cases
  -}

record IsPoorFieldInclusion
  {ℓ ℓ' ℓₚ ℓₚ'}
  (F : PoorField {ℓ} {ℓₚ}) (G : PoorField {ℓ'} {ℓₚ'})
  (f : (PoorField.Carrier F) → (PoorField.Carrier G)) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ'))
  where
  private
    module F = PoorField F
    module G = PoorField G
  field
    -- injectivity? might follow from preserves-#?
    reflects-≡    : ∀ x y → f x   ≡ f y →   x ≡     y
    -- lattice
    preserves-<   : ∀ x y →   x F.<   y → f x G.< f y
    preserves-≤   : ∀ x y →   x F.≤   y → f x G.≤ f y
    preserves-#   : ∀ x y →   x F.#   y → f x G.# f y
    reflects-<    : ∀ x y → f x G.< f y →   x F.<   y
    reflects-≤    : ∀ x y → f x G.≤ f y →   x F.≤   y
    reflects-#    : ∀ x y → f x G.# f y →   x F.#   y
    preserves-min : ∀ x y → f (F.min x y) ≡ G.min (f x) (f y)
    preserves-max : ∀ x y → f (F.max x y) ≡ G.max (f x) (f y)
    preserves-0   :         f  F.0f       ≡ G.0f
    -- Fin 1 does not preserve
    preserves-1   :         f  F.1f       ≡ G.1f
    -- Fin k might not preserve
    preserves-+   : ∀ x y → f (x F.+ y)   ≡ f x G.+  f y
    preserves-·   : ∀ x y → f (x F.· y)   ≡ f x G.·  f y
    -- ℕ might not preserve
    preserves-    : ∀ x   → f (  F.- x)   ≡     G.- (f x)
    -- ℤ does not preserve
    -- preserves-⁻¹' : ∀ x → (p : x F.# F.0f) → f (F._⁻¹ᶠ x {{p}}) ≡ G._⁻¹ᶠ (f x) {{ transport (λ i → f x G.# preserves-0 i) (preserves-# x F.0f p) }}
    -- NOTE: we better let the "user" decide how the proof of `f x # 0` is obtained
    preserves-⁻¹  : ∀ x → (p : x F.# F.0f) → (q : f x G.# G.0f) → f (F._⁻¹ᶠ x {{p}}) ≡ G._⁻¹ᶠ (f x) {{q}}

record PoorFieldInclusion {ℓ ℓ' ℓₚ ℓₚ'} (F : PoorField {ℓ} {ℓₚ}) (G : PoorField {ℓ'} {ℓₚ'}) : Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-max ℓₚ ℓₚ')) where
  constructor poorfieldmor
  module F = PoorField F
  module G = PoorField G
  field
    fun : F.Carrier → G.Carrier
    isPoorFieldInclusion : IsPoorFieldInclusion F G fun
  open IsPoorFieldInclusion isPoorFieldInclusion public

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
module Nat where

  data Nat : Set where
    zero : Nat
    suc  : Nat -> Nat

  one : Nat
  one = suc zero

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics