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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition
open import Setoids.Setoids
open import Setoids.Subset

module Graphs.Definition where

record Graph {a b : _} (c : _) {V' : Set a} (V : Setoid {a} {b} V') : Set (a ⊔ b ⊔ lsuc c) where
  field
    _<->_ : Rel {a} {c} V'
    noSelfRelation : (x : V') → x <-> x → False
    symmetric : {x y : V'} → x <-> y → y <-> x
    wellDefined : {x y r s : V'} → Setoid._∼_ V x y → Setoid._∼_ V r s → x <-> r → y <-> s

record GraphIso {a b c d e m : _} {V1' : Set a} {V2' : Set b} {V1 : Setoid {a} {c} V1'} {V2 : Setoid {b} {d} V2'} (G : Graph e V1) (H : Graph m V2) (f : V1' → V2') : Set (a ⊔ b ⊔ c ⊔ d ⊔ e ⊔ m) where
  field
    bij : SetoidBijection V1 V2 f
    respects : (x y : V1') → Graph._<->_ G x y → Graph._<->_ H (f x) (f y)
    respects' : (x y : V1') → Graph._<->_ H (f x) (f y) → Graph._<->_ G x y

record Subgraph {a b c d e : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) {pred : V' → Set d} (sub : subset V pred) (_<->'_ : Rel {_} {e} (Sg V' pred)) : Set (a ⊔ b ⊔ c ⊔ d ⊔ e) where
  field
    inherits : {x y : Sg V' pred} → (x <->' y) → (Graph._<->_ G (underlying x) (underlying y))
    symmetric : {x y : Sg V' pred} → (x <->' y) → (y <->' x)
    wellDefined : {x y r s : Sg V' pred} → Setoid._∼_ (subsetSetoid V sub) x y → Setoid._∼_ (subsetSetoid V sub) r s → x <->' r → y <->' s

subgraphIsGraph : {a b c d e : _} {V' : Set a} {V : Setoid {a} {b} V'} {G : Graph c V} {pred : V' → Set d} {sub : subset V pred} {rel : Rel {_} {e} (Sg V' pred)} (H : Subgraph G sub rel) → Graph e (subsetSetoid V sub)
Graph._<->_ (subgraphIsGraph {rel = rel} H) = rel
Graph.noSelfRelation (subgraphIsGraph {G = G} H) (v , isSub) v=v = Graph.noSelfRelation G v (Subgraph.inherits H v=v)
Graph.symmetric (subgraphIsGraph H) v1=v2 = Subgraph.symmetric H v1=v2
Graph.wellDefined (subgraphIsGraph H) = Subgraph.wellDefined H


text:
{-

   A defintion of the real projective spaces following:

   [BR17] U. Buchholtz, E. Rijke, The real projective spaces in homotopy type theory.
           (2017) https://arxiv.org/abs/1704.05770

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.RPn.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Bundle

open import Cubical.Foundations.SIP
open import Cubical.Structures.Pointed
open import Cubical.Structures.TypeEqvTo

open import Cubical.Data.Bool
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.NatMinusOne
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Data.Empty as ⊥ hiding (elim)
open import Cubical.Data.Sum as ⊎ hiding (elim)

open import Cubical.Data.Prod renaming (_×_ to _×'_; _×Σ_ to _×_; swapΣEquiv to swapEquiv)
                              hiding (swapEquiv)

open import Cubical.HITs.PropositionalTruncation as PropTrunc hiding (elim)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.Join
open import Cubical.HITs.Pushout
open import Cubical.HITs.Pushout.Flattening

private
  variable
    ℓ ℓ' ℓ'' : Level

-- Definition II.1 in [BR17], see also Cubical.Foundations.Bundle

2-EltType₀    = TypeEqvTo    ℓ-zero Bool -- Σ[ X ∈ Type₀ ] ∥ X ≃ Bool ∥
2-EltPointed₀ = PointedEqvTo ℓ-zero Bool -- Σ[ X ∈ Type₀ ] X × ∥ X ≃ Bool ∥

Bool* : 2-EltType₀
Bool* = Bool , ∣ idEquiv _ ∣

-- Our first goal is to 'lift' `_⊕_ : Bool → Bool ≃ Bool` to a function `_⊕_ : A → A ≃ Bool`
--  for any 2-element type (A, ∣e∣).

-- `isContr-BoolPointedIso` and `isContr-2-EltPointed-iso` are contained in the proof
--  of Lemma II.2 in [BR17], though we prove `isContr-BoolPointedIso` more directly
--  with ⊕ -- [BR17] proves it for just the x = false case and uses notEquiv to get
--  the x = true case.

-- (λ y → x ⊕ y) is the unqiue pointed isomorphism (Bool , false) ≃ (Bool , x)
isContr-BoolPointedIso : ∀ x → isContr ((Bool , false) ≃[ pointed-iso ] (Bool , x))
fst (isContr-BoolPointedIso x) = ((λ y → x ⊕ y) , isEquiv-⊕ x) , ⊕-comm x false
snd (isContr-BoolPointedIso x) (e , p)
  = ΣProp≡ (λ e → isSetBool (equivFun e false) x)
           (ΣProp≡ isPropIsEquiv (funExt λ { false → ⊕-comm x false ∙ sym p
                                           ; true  → ⊕-comm x true  ∙ sym q }))
  where q : e .fst true ≡ not x
        q with dichotomyBool (invEq e (not x))
        ... | inl q = invEq≡→equivFun≡ e q
        ... | inr q = ⊥.rec (not≢const x (sym (invEq≡→equivFun≡ e q) ∙ p))

-- Since isContr is a mere proposition, we can eliminate a witness ∣e∣ : ∥ X ≃ Bool ∥ to get
--  that there is therefore a unique pointed isomorphism (Bool , false) ≃ (X , x) for any
--  2-element pointed type (X , x, ∣e∣).
isContr-2-EltPointed-iso : (X∙ : 2-EltPointed₀)
                         → isContr ((Bool , false , ∣ idEquiv Bool ∣) ≃[ PointedEqvTo-iso Bool ] X∙)
isContr-2-EltPointed-iso (X , x , ∣e∣)
  = PropTrunc.rec isPropIsContr
                  (λ e → J (λ X∙ _ → isContr ((Bool , false) ≃[ pointed-iso ] X∙))
                           (isContr-BoolPointedIso (e .fst x))
                           (sym (pointed-sip _ _ (e , refl))))
                  ∣e∣

-- This unique isomorphism must be _⊕_ 'lifted' to X. This idea is alluded to at the end of the
--  proof of Theorem III.4 in [BR17], where the authors reference needing ⊕-comm.
module ⊕* (X : 2-EltType₀) where

  _⊕*_ : typ X → typ X → Bool
  y ⊕* z = invEquiv (fst (fst (isContr-2-EltPointed-iso (fst X , y , snd X)))) .fst z

  -- we've already shown that this map is an equivalence on the right

  isEquivʳ : (y : typ X) → isEquiv (y ⊕*_)
  isEquivʳ y = invEquiv (fst (fst (isContr-2-EltPointed-iso (fst X , y , snd X)))) .snd

  Equivʳ : typ X → typ X ≃ Bool
  Equivʳ y = (y ⊕*_) , isEquivʳ y

  -- any mere proposition that holds for (Bool, _⊕_) holds for (typ X, _⊕*_)
  -- this amounts to just carefully unfolding the PropTrunc.elim and J in isContr-2-EltPointed-iso
  elim : ∀ {ℓ'} (P : (A : Type₀) (_⊕'_ : A → A → Bool) → Type ℓ') (propP : ∀ A _⊕'_ → isProp (P A _⊕'_))
         → P Bool _⊕_ → P (typ X) _⊕*_
  elim {ℓ'} P propP r = PropTrunc.elim {P = λ ∣e∣ → P (typ X) (R₁ ∣e∣)} (λ _ → propP _ _)
                                       (λ e → EquivJ (λ A e → P A (R₂ A e)) r e)
                                       (snd X)
    where R₁ : ∥ fst X ≃ Bool ∥ → typ X → typ X → Bool
          R₁ ∣e∣ y = invEq (fst (fst (isContr-2-EltPointed-iso (fst X , y , ∣e∣))))
          R₂ : (B : Type₀) → B ≃ Bool → B → B → Bool
          R₂ A e y = invEq (fst (fst (J (λ A∙ _ → isContr ((Bool , false) ≃[ pointed-iso ] A∙))
                                        (isContr-BoolPointedIso (e .fst y))
                                        (sym (pointed-sip (A , y) (Bool , e .fst y) (e , refl))))))

  -- as a consequence, we get that ⊕* is commutative, and is therefore also an equivalence on the left

  comm : (y z : typ X) → y ⊕* z ≡ z ⊕* y
  comm = elim (λ A _⊕'_ → (x y : A) → x ⊕' y ≡ y ⊕' x)
              (λ _ _ → isPropPi (λ _ → isPropPi (λ _ → isSetBool _ _)))
              ⊕-comm

  isEquivˡ : (y : typ X) → isEquiv (_⊕* y)
  isEquivˡ y = subst isEquiv (funExt (λ z → comm y z)) (isEquivʳ y)

  Equivˡ : typ X → typ X ≃ Bool
  Equivˡ y = (_⊕* y) , isEquivˡ y

-- Lemma II.2 in [BR17], though we do not use it here
-- Note: Lemma II.3 is `pointed-sip`, used in `PointedEqvTo-sip`
isContr-2-EltPointed : isContr (2-EltPointed₀)
fst isContr-2-EltPointed = (Bool , false , ∣ idEquiv Bool ∣)
snd isContr-2-EltPointed A∙ = PointedEqvTo-sip Bool _ A∙ (fst (isContr-2-EltPointed-iso A∙))

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

-- Now we mutually define RP n and its double cover (Definition III.1 in [BR17]),
--  and show that the total space of this double cover is S n (Theorem III.4).

RP  : ℕ₋₁ → Type₀
cov⁻¹ : (n : ℕ₋₁) → RP n → 2-EltType₀ -- (see Cubical.Foundations.Bundle)

RP neg1 = ⊥
RP (ℕ→ℕ₋₁ n) = Pushout (pr (cov⁻¹ (-1+ n))) (λ _ → tt)
{-
                         tt
   Total (cov⁻¹ (n-1)) — — — > Unit
            |                    ∙
        pr  |                    ∙  inr
            |                    ∙
            V                    V
        RP (n-1) ∙ ∙ ∙ ∙ ∙ ∙ > RP n := Pushout pr (const tt)
                      inl
-}

cov⁻¹ neg1 x = Bool*
cov⁻¹ (ℕ→ℕ₋₁ n) (inl x)          = cov⁻¹ (-1+ n) x
cov⁻¹ (ℕ→ℕ₋₁ n) (inr _)          = Bool*
cov⁻¹ (ℕ→ℕ₋₁ n) (push (x , y) i) = ua ((λ z → y ⊕* z) , ⊕*.isEquivʳ (cov⁻¹ (-1+ n) x) y) i , ∣p∣ i
  where open ⊕* (cov⁻¹ (-1+ n) x)
        ∣p∣ = isProp→PathP (λ i → squash {A = ua (⊕*.Equivʳ (cov⁻¹ (-1+ n) x) y) i ≃ Bool})
                           (str (cov⁻¹ (-1+ n) x)) (∣ idEquiv _ ∣)
{-
                         tt
   Total (cov⁻¹ (n-1)) — — — > Unit
            |                    |
        pr  |     // ua α //     | Bool
            |                    |
            V                    V
        RP (n-1) - - - - - - > Type
                  cov⁻¹ (n-1)

   where α : ∀ (x : Total (cov⁻¹ (n-1))) → cov⁻¹ (n-1) (pr x) ≃ Bool
         α (x , y) = (λ z → y ⊕* z) , ⊕*.isEquivʳ y
-}

TotalCov≃Sn : ∀ n → Total (cov⁻¹ n) ≃ S n
TotalCov≃Sn neg1 = isoToEquiv (iso (λ { () }) (λ { () }) (λ { () }) (λ { () }))
TotalCov≃Sn (ℕ→ℕ₋₁ n) =
  Total (cov⁻¹ (ℕ→ℕ₋₁ n))           ≃⟨ i ⟩
  Pushout Σf Σg                      ≃⟨ ii ⟩
  join (Total (cov⁻¹ (-1+ n))) Bool  ≃⟨ iii ⟩
  S (ℕ→ℕ₋₁ n)                       ■
  where
{-
    (i) First we want to show that `Total (cov⁻¹ (ℕ→ℕ₋₁ n))` is equivalent to a pushout.
    We do this using the flattening lemma, which states:

    Given f,g,F,G,e such that the following square commutes:

             g
       A — — — — > C                 Define:   E : Pushout f g → Type
       |           |                           E (inl b) = F b
    f  |   ua e    |  G                        E (inr c) = G c
       V           V                           E (push a i) = ua (e a) i
       B — — — — > Type
             F

    Then, the total space `Σ (Pushout f g) E` is the following pushout:

                                Σg := (g , e a)
            Σ[ a ∈ A ] F (f a) — — — — — — — — > Σ[ c ∈ C ] G c
                   |                                ∙
    Σf := (f , id) |                                ∙
                   V                                V
            Σ[ b ∈ B ] F b ∙ ∙ ∙ ∙ ∙ ∙ ∙ ∙ ∙ ∙ > Σ (Pushout f g) E

    In our case, setting `f = pr (cov⁻¹ (n-1))`, `g = λ _ → tt`, `F = cov⁻¹ (n-1)`, `G = λ _ → Bool`,
     and `e = λ (x , y) → ⊕*.Equivʳ (cov⁻¹ (n-1) x) y` makes E equal (up to funExt) to `cov⁻¹ n`.

    Thus the flattening lemma gives us that `Total (cov⁻¹ n) ≃ Pushout Σf Σg`.
-}
    open FlatteningLemma {- f = -} (λ x → pr (cov⁻¹ (-1+ n)) x)  {- g = -} (λ _ → tt)
                         {- F = -} (λ x → typ (cov⁻¹ (-1+ n) x)) {- G = -} (λ _ → Bool)
                         {- e = -} (λ { (x , y) → ⊕*.Equivʳ (cov⁻¹ (-1+ n) x) y })
                         hiding (Σf ; Σg)

    cov⁻¹≃E : ∀ x → typ (cov⁻¹ (ℕ→ℕ₋₁ n) x) ≃ E x
    cov⁻¹≃E (inl x) = idEquiv _
    cov⁻¹≃E (inr x) = idEquiv _
    cov⁻¹≃E (push a i) = idEquiv _

    -- for easier reference, we copy these definitons here
    Σf : Σ[ x ∈ Total (cov⁻¹ (-1+ n)) ] typ (cov⁻¹ (-1+ n) (fst x)) → Total (cov⁻¹ (-1+ n))
    Σg : Σ[ x ∈ Total (cov⁻¹ (-1+ n)) ] typ (cov⁻¹ (-1+ n) (fst x)) → Unit × Bool
    Σf ((x , y) , z) = (x , z)       -- ≡ (f a , x)
    Σg ((x , y) , z) = (tt , y ⊕* z) -- ≡ (g a , (e a) .fst x)
      where open ⊕* (cov⁻¹ (-1+ n) x)

    i : Total (cov⁻¹ (ℕ→ℕ₋₁ n)) ≃ Pushout Σf Σg
    i = (Σ[ x ∈ RP (ℕ→ℕ₋₁ n) ] typ (cov⁻¹ (ℕ→ℕ₋₁ n) x)) ≃⟨ congΣEquiv cov⁻¹≃E ⟩
        (Σ[ x ∈ RP (ℕ→ℕ₋₁ n) ] E x)                     ≃⟨ flatten ⟩
        Pushout Σf Σg                                   ■
{-
    (ii) Next we want to show that `Pushout Σf Σg` is equivalent to `join (Total (cov⁻¹ (n-1))) Bool`.
    Since both are pushouts, this can be done by defining a diagram equivalence:

                          Σf                                                  Σg
    Total (cov⁻¹ (n-1)) < — — Σ[ x ∈ Total (cov⁻¹ (n-1)) ] cov⁻¹ (n-1) (pr x) — — > Unit × Bool
            |                                        ∙                                   |
        id  |≃                                    u  ∙≃                             snd  |≃
            V                                        V                                   V
    Total (cov⁻¹ (n-1)) < — — — — — — — Total (cov⁻¹ (n-1)) × Bool — — — — — — — — — > Bool
                              proj₁                                      proj₂

    where the equivalence u above must therefore satisfy: `u .fst x ≡ (Σf x , snd (Σg x))`
    Unfolding this, we get: `u .fst ((x , y) , z) ≡ ((x , z) , (y ⊕* z))`

    It suffices to show that the map y ↦ y ⊕* z is an equivalence, since we can then express u as
     the following composition of equivalences:
    ((x , y) , z) ↦ (x , (y , z)) ↦ (x , (z , y)) ↦ (x , (z , y ⊕* z)) ↦ ((x , z) , y ⊕* z)

    This was proved above by ⊕*.isEquivˡ.
-}
    u : ∀ {n} → (Σ[ x ∈ Total (cov⁻¹ n) ] typ (cov⁻¹ n (fst x))) ≃ (Total (cov⁻¹ n) ×' Bool)
    u {n} = Σ[ x ∈ Total (cov⁻¹ n) ] typ (cov⁻¹ n (fst x))      ≃⟨ assocΣ ⟩
            Σ[ x ∈ RP n ] (typ (cov⁻¹ n x)) × (typ (cov⁻¹ n x)) ≃⟨ congΣEquiv (λ x → swapEquiv _ _) ⟩
            Σ[ x ∈ RP n ] (typ (cov⁻¹ n x)) × (typ (cov⁻¹ n x)) ≃⟨ congΣEquiv (λ x → congΣEquiv (λ y →
                                                                             ⊕*.Equivˡ (cov⁻¹ n x) y)) ⟩
            Σ[ x ∈ RP n ] (typ (cov⁻¹ n x)) × Bool              ≃⟨ invEquiv assocΣ ⟩
            Total (cov⁻¹ n) × Bool                              ≃⟨ invEquiv A×B≃A×ΣB ⟩
            Total (cov⁻¹ n) ×' Bool                             ■

    H : ∀ x → u .fst x ≡ (Σf x , snd (Σg x))
    H x = refl

    nat : 3-span-equiv (3span Σf Σg) (3span {A2 = Total (cov⁻¹ (-1+ n)) ×' Bool} proj₁ proj₂)
    nat = record { e0 = idEquiv _ ; e2 = u ; e4 = ΣUnit _
                 ; H1 = λ x → cong proj₁ (H x)
                 ; H3 = λ x → cong proj₂ (H x) }

    ii : Pushout Σf Σg ≃ join (Total (cov⁻¹ (-1+ n))) Bool
    ii = compEquiv (pathToEquiv (spanEquivToPushoutPath nat)) (joinPushout≃join _ _)

{-
    (iii) Finally, it's trivial to show that `join (Total (cov⁻¹ (n-1))) Bool` is equivalent to
     `Susp (Total (cov⁻¹ (n-1)))`. Induction then gives us that `Susp (Total (cov⁻¹ (n-1)))`
     is equivalent to `S n`, which completes the proof.
-}

    iii : join (Total (cov⁻¹ (-1+ n))) Bool ≃ S (ℕ→ℕ₋₁ n)
    iii = join (Total (cov⁻¹ (-1+ n))) Bool ≃⟨ invEquiv Susp≃joinBool ⟩
          Susp (Total (cov⁻¹ (-1+ n)))      ≃⟨ congSuspEquiv (TotalCov≃Sn (-1+ n)) ⟩
          S (ℕ→ℕ₋₁ n)                      ■

-- the usual covering map S n → RP n, with fibers exactly cov⁻¹

cov : (n : ℕ₋₁) → S n → RP n
cov n = pr (cov⁻¹ n) ∘ invEq (TotalCov≃Sn n)

fibcov≡cov⁻¹ : ∀ n (x : RP n) → fiber (cov n) x ≡ cov⁻¹ n x .fst
fibcov≡cov⁻¹ n x =
  fiber (cov n)        x ≡[ i ]⟨ fiber {A = ua e i} (pr (cov⁻¹ n) ∘ ua-unglue e i) x ⟩
  fiber (pr (cov⁻¹ n)) x ≡⟨ ua (fibPrEquiv (cov⁻¹ n) x) ⟩
  cov⁻¹ n x .fst         ∎
  where e = invEquiv (TotalCov≃Sn n)

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

-- Finally, we state the trivial equivalences for RP 0 and RP 1 (Example III.3 in [BR17])

RP0≃Unit : RP 0 ≃ Unit
RP0≃Unit = isoToEquiv (iso (λ _ → tt) (λ _ → inr tt) (λ _ → refl) (λ { (inr tt) → refl }))

RP1≡S1 : RP 1 ≡ S 1
RP1≡S1 = Pushout {A = Total (cov⁻¹ 0)} {B = RP 0} (pr (cov⁻¹ 0)) (λ _ → tt) ≡⟨ i ⟩
         Pushout {A = Total (cov⁻¹ 0)} {B = Unit} (λ _ → tt)     (λ _ → tt) ≡⟨ ii ⟩
         Pushout {A = S 0}             {B = Unit} (λ _ → tt)     (λ _ → tt) ≡⟨ PushoutSusp≡Susp ⟩
         S 1                                                                ∎
  where i = λ i → Pushout {A = Total (cov⁻¹ 0)}
                          {B = ua RP0≃Unit i}
                          (λ x → ua-gluePt RP0≃Unit i (pr (cov⁻¹ 0) x))
                          (λ _ → tt)
        ii = λ j → Pushout {A = ua (TotalCov≃Sn 0) j} (λ _ → tt) (λ _ → tt)

ext: agda

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Builtin.Bool

postulate
  A : Set

F : Bool → Set
F true  = A
F false = A

data D {b : Bool} (x : F b) : Set where

variable
  b : Bool
  x : F b

postulate
  f : D x → (P : F b → Set) → P x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- {-# OPTIONS -v scope.clash:20 #-}
-- Andreas, 2012-10-19 test case for Issue 719
module ShadowModule2 where

open import Common.Size as YesDuplicate
import Common.Size as NotDuplicate

private open module YesDuplicate = NotDuplicate
-- should report:
-- Duplicate definition of module YesDuplicate.
-- NOT: Duplicate definition of module NotDuplicate.


text:
------------------------------------------------------------------------
-- Various forms of induction for natural numbers
------------------------------------------------------------------------

module Induction.Nat where

open import Data.Function
open import Data.Nat
open import Data.Fin
open import Data.Fin.Props
open import Data.Product
open import Data.Unit
open import Induction
import Induction.WellFounded as WF
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Ordinary induction

Rec : RecStruct ℕ
Rec P zero    = ⊤
Rec P (suc n) = P n

rec-builder : RecursorBuilder Rec
rec-builder P f zero    = tt
rec-builder P f (suc n) = f n (rec-builder P f n)

rec : Recursor Rec
rec = build rec-builder

------------------------------------------------------------------------
-- Complete induction

CRec : RecStruct ℕ
CRec P zero    = ⊤
CRec P (suc n) = P n × CRec P n

cRec-builder : RecursorBuilder CRec
cRec-builder P f zero    = tt
cRec-builder P f (suc n) = f n ih , ih
  where ih = cRec-builder P f n

cRec : Recursor CRec
cRec = build cRec-builder

------------------------------------------------------------------------
-- Complete induction based on _<′_

open WF _<′_ using (acc) renaming (Acc to <-Acc)

<-allAcc : ∀ n → <-Acc n
<-allAcc n = acc (helper n)
  where
  helper : ∀ n m → m <′ n → <-Acc m
  helper zero     _ ()
  helper (suc n) .n ≤′-refl       = acc (helper n)
  helper (suc n)  m (≤′-step m<n) = helper n m m<n

open WF _<′_ public using () renaming (WfRec to <-Rec)
open WF.All _<′_ <-allAcc public
  renaming ( wfRec-builder to <-rec-builder
           ; wfRec to <-rec
           )

------------------------------------------------------------------------
-- Complete induction based on _≺_

open WF _≺_ renaming (Acc to ≺-Acc)

<-Acc⇒≺-Acc : ∀ {n} → <-Acc n → ≺-Acc n
<-Acc⇒≺-Acc (acc rs) =
  acc (λ m m≺n → <-Acc⇒≺-Acc (rs m (≺⇒<′ m≺n)))

≺-allAcc : ∀ n → ≺-Acc n
≺-allAcc n = <-Acc⇒≺-Acc (<-allAcc n)

open WF _≺_ public using () renaming (WfRec to ≺-Rec)
open WF.All _≺_ ≺-allAcc public
  renaming ( wfRec-builder to ≺-rec-builder
           ; wfRec to ≺-rec
           )

------------------------------------------------------------------------
-- Examples

private

 module Examples where

  -- The half function.

  HalfPred : ℕ → Set
  HalfPred _ = ℕ

  half₁ : ℕ → ℕ
  half₁ = cRec HalfPred half₁'
    where
    half₁' : ∀ n → CRec HalfPred n → HalfPred n
    half₁' zero          _                = zero
    half₁' (suc zero)    _                = zero
    half₁' (suc (suc n)) (_ , half₁n , _) = suc half₁n

  half₂ : ℕ → ℕ
  half₂ = <-rec HalfPred half₂'
    where
    half₂' : ∀ n → <-Rec HalfPred n → HalfPred n
    half₂' zero          _   = zero
    half₂' (suc zero)    _   = zero
    half₂' (suc (suc n)) rec = suc (rec n (≤′-step ≤′-refl))

max_issues_repo_name: larrytheliquid/Lemmachine


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

module Issue3526-2 where

open import Agda.Builtin.Equality

record Truth (P : Prop) : Set where
  constructor [_]
  field
    truth : P
open Truth public

data ⊥' : Prop where

⊥ = Truth ⊥'

¬ : Set → Set
¬ A = A → ⊥

unique : {A : Set} (x y : ¬ A) → x ≡ y
unique x y = refl

⊥-elim : (A : Set) → ⊥ → A
⊥-elim A b = {!!}

open import Agda.Builtin.Bool
open import Agda.Builtin.Unit

set : Bool → Set
set false = ⊥
set true  = ⊤

set-elim : ∀ b → set b → Set
set-elim b x = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Notation for freely adding extrema to any set
------------------------------------------------------------------------

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

module Relation.Nullary.Construct.Add.Extrema where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary.Construct.Add.Infimum  as Infimum  using (_₋)
open import Relation.Nullary.Construct.Add.Supremum as Supremum using (_⁺)

------------------------------------------------------------------------
-- Definition

_± : ∀ {a} → Set a → Set a
A ± = A ₋ ⁺

pattern ⊥±    = Supremum.[ Infimum.⊥₋ ]
pattern [_] k = Supremum.[ Infimum.[ k ] ]
pattern ⊤±    = Supremum.⊤⁺

------------------------------------------------------------------------
-- Properties

[_]-injective : ∀ {a} {A : Set a} {k l : A} → [ k ] ≡ [ l ] → k ≡ l
[_]-injective refl = refl


text:
{-# OPTIONS --universe-polymorphism #-}

module Categories.Groupoid.Product where

open import Data.Product

open import Categories.Category
open import Categories.Groupoid
open import Categories.Morphisms
import Categories.Product as ProductC

Product : ∀ {o₁ ℓ₁ e₁ o₂ ℓ₂ e₂} {C : Category o₁ ℓ₁ e₁} {D : Category o₂ ℓ₂ e₂}
        → Groupoid C → Groupoid D → Groupoid (ProductC.Product C D)
Product c₁ c₂ = record
         { _⁻¹ = λ {(x₁ , x₂) → Groupoid._⁻¹ c₁ x₁
                              , Groupoid._⁻¹ c₂ x₂}
         ; iso = record { isoˡ = Iso.isoˡ (Groupoid.iso c₁)
                               , Iso.isoˡ (Groupoid.iso c₂)
                        ; isoʳ = Iso.isoʳ (Groupoid.iso c₁)
                               , Iso.isoʳ (Groupoid.iso c₂) } }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
------------------------------------------------------------------------------
-- Some properties of the function iter₀
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.Iter0.PropertiesATP where

open import FOTC.Program.Iter0.Iter0

open import FOTC.Base
open import FOTC.Base.List

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

postulate iter₀-0 : ∀ f → iter₀ f zero ≡ []
{-# ATP prove iter₀-0 #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.Pushout.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.HITs.Susp.Base

data Pushout {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
             (f : A → B) (g : A → C) : Type (ℓ-max ℓ (ℓ-max ℓ' ℓ'')) where
  inl : B → Pushout f g
  inr : C → Pushout f g
  push : (a : A) → inl (f a) ≡ inr (g a)

-- cofiber (equivalent to Cone in Cubical.HITs.MappingCones.Base)
cofib : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type _
cofib f = Pushout (λ _ → tt) f

cfcod : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) → B → cofib f
cfcod f = inr

-- Symmetry of pushout

symPushout : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
  → (f : A → B) (g : A → C) → Pushout f g ≃ Pushout g f
symPushout f g = isoToEquiv
  (iso (λ { (inl x) → inr x ; (inr x) → inl x ; (push x i) → push x (~ i)})
       (λ { (inl x) → inr x ; (inr x) → inl x ; (push x i) → push x (~ i)})
       (λ { (inl x) → refl  ; (inr x) → refl  ; (push x i) → refl})
       (λ { (inl x) → refl  ; (inr x) → refl  ; (push x i) → refl}))

-- Suspension defined as a pushout

PushoutSusp : ∀ {ℓ} (A : Type ℓ) → Type ℓ
PushoutSusp A = Pushout {A = A} {B = Unit} {C = Unit} (λ _ → tt) (λ _ → tt)

PushoutSusp→Susp : ∀ {ℓ} {A : Type ℓ} → PushoutSusp A → Susp A
PushoutSusp→Susp (inl _) = north
PushoutSusp→Susp (inr _) = south
PushoutSusp→Susp (push a i) = merid a i

Susp→PushoutSusp : ∀ {ℓ} {A : Type ℓ} → Susp A → PushoutSusp A
Susp→PushoutSusp north = inl tt
Susp→PushoutSusp south = inr tt
Susp→PushoutSusp (merid a i) = push a i

Susp→PushoutSusp→Susp : ∀ {ℓ} {A : Type ℓ} (x : Susp A) →
                        PushoutSusp→Susp (Susp→PushoutSusp x) ≡ x
Susp→PushoutSusp→Susp north = refl
Susp→PushoutSusp→Susp south = refl
Susp→PushoutSusp→Susp (merid _ _) = refl

PushoutSusp→Susp→PushoutSusp : ∀ {ℓ} {A : Type ℓ} (x : PushoutSusp A) →
                               Susp→PushoutSusp (PushoutSusp→Susp x) ≡ x
PushoutSusp→Susp→PushoutSusp (inl _) = refl
PushoutSusp→Susp→PushoutSusp (inr _) = refl
PushoutSusp→Susp→PushoutSusp (push _ _) = refl

PushoutSuspIsoSusp : ∀ {ℓ} {A : Type ℓ} → Iso (PushoutSusp A) (Susp A)
Iso.fun PushoutSuspIsoSusp = PushoutSusp→Susp
Iso.inv PushoutSuspIsoSusp = Susp→PushoutSusp
Iso.rightInv PushoutSuspIsoSusp = Susp→PushoutSusp→Susp
Iso.leftInv PushoutSuspIsoSusp = PushoutSusp→Susp→PushoutSusp

PushoutSusp≃Susp : ∀ {ℓ} {A : Type ℓ} → PushoutSusp A ≃ Susp A
PushoutSusp≃Susp = isoToEquiv PushoutSuspIsoSusp

PushoutSusp≡Susp : ∀ {ℓ} {A : Type ℓ} → PushoutSusp A ≡ Susp A
PushoutSusp≡Susp = isoToPath PushoutSuspIsoSusp

-- Generalised pushout, used in e.g. BlakersMassey
data PushoutGen {ℓ₁ ℓ₂ ℓ₃ : Level} {X : Type ℓ₁} {Y : Type ℓ₂}
                (Q : X → Y → Type ℓ₃) : Type (ℓ-max (ℓ-max ℓ₁ ℓ₂) ℓ₃)
     where
     inl : X → PushoutGen Q
     inr : Y → PushoutGen Q
     push : {x : X} {y : Y} → Q x y → inl x ≡ inr y

-- The usual pushout is a special case of the above
module _ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃}
         (f : A → B) (g : A → C) where
  open Iso

  doubleFib : B → C → Type _
  doubleFib b c = Σ[ a ∈ A ] (f a ≡ b) × (g a ≡ c)

  PushoutGenFib = PushoutGen doubleFib

  Pushout→PushoutGen : Pushout f g → PushoutGenFib
  Pushout→PushoutGen (inl x) = inl x
  Pushout→PushoutGen (inr x) = inr x
  Pushout→PushoutGen (push a i) = push (a , refl , refl) i

  PushoutGen→Pushout : PushoutGenFib → Pushout f g
  PushoutGen→Pushout (inl x) = inl x
  PushoutGen→Pushout (inr x) = inr x
  PushoutGen→Pushout (push (x , p , q) i) =
    ((λ i → inl (p (~ i))) ∙∙ push x ∙∙ (λ i → inr (q i))) i

  IsoPushoutPushoutGen : Iso (Pushout f g) (PushoutGenFib)
  fun IsoPushoutPushoutGen = Pushout→PushoutGen
  inv IsoPushoutPushoutGen = PushoutGen→Pushout
  rightInv IsoPushoutPushoutGen (inl x) = refl
  rightInv IsoPushoutPushoutGen (inr x) = refl
  rightInv IsoPushoutPushoutGen (push (x , p , q) i) j = lem x p q j i
    where
    lem : {b : B} {c : C} (x : A) (p : f x ≡ b) (q : g x ≡ c)
      → cong Pushout→PushoutGen (cong PushoutGen→Pushout (push (x , p , q)))
      ≡ push (x , p , q)
    lem {c = c} x =
      J (λ b p → (q : g x ≡ c)
        → cong Pushout→PushoutGen
           (cong PushoutGen→Pushout (push (x , p , q)))
         ≡ push (x , p , q))
        (J (λ c q → cong Pushout→PushoutGen
                      (cong PushoutGen→Pushout (push (x , refl , q)))
         ≡ push (x , refl , q))
         (cong (cong Pushout→PushoutGen) (sym (rUnit (push x)))))
  leftInv IsoPushoutPushoutGen (inl x) = refl
  leftInv IsoPushoutPushoutGen (inr x) = refl
  leftInv IsoPushoutPushoutGen (push a i) j = rUnit (push a) (~ j) i

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --without-K --safe --erased-cubical --no-import-sorts #-}

module SUtil where

open import Prelude

_∈_ : Name → List Name → Bool
n ∈ []       = false
n ∈ (x ∷ ns) = if n == x then true else n ∈ ns

-- treat list as set
insert : Name → List Name → List Name
insert n ns = if n ∈ ns then ns else n ∷ ns

lookup : {A : Type} → List (Name × List A) → Name → List A
lookup []             n = []
lookup ((m , x) ∷ xs) n = if n == m then x else lookup xs n

nameSet : List Name → List Name
nameSet = foldr insert []

iterate : {A : Type} → ℕ → (A → A) → A → A
iterate zero    f x = x
iterate (suc k) f x = iterate k f (f x)

2ⁿSpeed : ℕ → List Note → List Note
2ⁿSpeed n = map (iterate n doubleSpeed)

zipFull : {A : Type} → List (List A) → List (List A) → List (List A)
zipFull []          yss        = yss
zipFull xss@(_ ∷ _) []         = xss
zipFull (xs ∷ xss)  (ys ∷ yss) = (xs ++ ys) ∷ zipFull xss yss

_+1 : {n : ℕ} → Fin n → Fin n
_+1 {suc n} k = (suc (toℕ k)) mod (suc n)

emptyVec : {n : ℕ}{A : Type} → Vec (List A) n
emptyVec {zero}  = []
emptyVec {suc n} = [] ∷ emptyVec {n}

foldIntoVector : {n : ℕ} {A : Type} → List (List A) → Vec (List A) (suc n)
foldIntoVector {n} {A} xss = fiv fz emptyVec xss
  where fiv : Fin (suc n) → Vec (List A) (suc n) → List (List A) → Vec (List A) (suc n)
        fiv k xss []         = xss
        fiv k xss (ys ∷ yss) = fiv (k +1) (updateAt k (_++ ys) xss) yss

max_stars_repo_name: halfaya/Music

max_issues_repo_name: halfaya/Music

max_forks_repo_name: halfaya/Music


text:
------------------------------------------------------------------------
-- Various parser combinator laws
------------------------------------------------------------------------

-- Note that terms like "monad" and "Kleene algebra" are interpreted
-- liberally in the modules listed below.

module TotalParserCombinators.Laws where

open import Algebra
open import Category.Monad
open import Codata.Musical.Notation
open import Data.List as List
import Data.List.Categorical
open import Data.List.Properties
open import Data.List.Relation.Binary.BagAndSetEquality as Eq
  using (bag) renaming (_∼[_]_ to _List-∼[_]_)
open import Data.Maybe hiding (_>>=_)
open import Function
import Level
open import Relation.Binary.PropositionalEquality as P using (_≡_)

private
  module BagMonoid {k} {A : Set} =
    CommutativeMonoid (Eq.commutativeMonoid k A)
  open module ListMonad =
    RawMonad {f = Level.zero} Data.List.Categorical.monad
    using () renaming (_⊛_ to _⊛′_)

open import TotalParserCombinators.Derivative using (D)
open import TotalParserCombinators.Congruence
  hiding (return; fail; token)
open import TotalParserCombinators.Lib hiding (module Return⋆)
open import TotalParserCombinators.Parser

------------------------------------------------------------------------
-- Reexported modules

-- Laws related to _∣_.

import TotalParserCombinators.Laws.AdditiveMonoid
module AdditiveMonoid = TotalParserCombinators.Laws.AdditiveMonoid

-- Laws related to D.

import TotalParserCombinators.Laws.Derivative
module D = TotalParserCombinators.Laws.Derivative
  hiding (left-zero-⊛; right-zero-⊛;
          left-zero->>=; right-zero->>=)

-- Laws related to return⋆.

import TotalParserCombinators.Laws.ReturnStar
module Return⋆ = TotalParserCombinators.Laws.ReturnStar

-- Laws related to _⊛_.

import TotalParserCombinators.Laws.ApplicativeFunctor
module ApplicativeFunctor =
  TotalParserCombinators.Laws.ApplicativeFunctor

-- Laws related to _>>=_.

import TotalParserCombinators.Laws.Monad
module Monad = TotalParserCombinators.Laws.Monad

-- Do the parser combinators form a Kleene algebra?

import TotalParserCombinators.Laws.KleeneAlgebra
module KleeneAlgebra = TotalParserCombinators.Laws.KleeneAlgebra

------------------------------------------------------------------------
-- Some laws for _<$>_

module <$> where

  open D

  -- _<$>_ could have been defined using return and _⊛_.

  return-⊛ : ∀ {Tok R₁ R₂ xs} {f : R₁ → R₂} (p : Parser Tok R₁ xs) →
             f <$> p ≅P return f ⊛ p
  return-⊛ {xs = xs} {f} p =
    BagMonoid.reflexive (lemma xs) ∷ λ t → ♯ (
      f <$> D t p         ≅⟨ return-⊛ (D t p) ⟩
      return f ⊛ D t p    ≅⟨ sym $ D-return-⊛ f p ⟩
      D t (return f ⊛ p)  ∎)
    where
    lemma : ∀ xs → List.map f xs ≡ ([ f ] ⊛′ xs)
    lemma []       = P.refl
    lemma (x ∷ xs) = P.cong (_∷_ (f x)) $ lemma xs

  -- fail is a zero for _<$>_.

  zero : ∀ {Tok R₁ R₂} {f : R₁ → R₂} →
         f <$> fail {Tok = Tok} ≅P fail
  zero {f = f} =
    f <$> fail       ≅⟨ return-⊛ fail ⟩
    return f ⊛ fail  ≅⟨ ApplicativeFunctor.right-zero (return f) ⟩
    fail             ∎

  -- A variant of ApplicativeFunctor.homomorphism.

  homomorphism : ∀ {Tok R₁ R₂} (f : R₁ → R₂) {x} →
                 f <$> return {Tok = Tok} x ≅P return (f x)
  homomorphism f {x} =
    f <$> return x       ≅⟨ return-⊛ {f = f} (return x) ⟩
    return f ⊛ return x  ≅⟨ ApplicativeFunctor.homomorphism f x ⟩
    return (f x)         ∎

  -- Adjacent uses of _<$>_ can be fused.

  <$>-<$> : ∀ {Tok R₁ R₂ R₃ xs}
              {f : R₂ → R₃} {g : R₁ → R₂} {p : Parser Tok R₁ xs} →
            f <$> (g <$> p) ≅P (f ∘ g) <$> p
  <$>-<$> = BagMonoid.reflexive (P.sym (map-compose _)) ∷ λ _ → ♯ <$>-<$>

------------------------------------------------------------------------
-- A law for nonempty

module Nonempty where

  -- fail is a zero for nonempty.

  zero : ∀ {Tok R} → nonempty {Tok = Tok} {R = R} fail ≅P fail
  zero = BagMonoid.refl ∷ λ t → ♯ (fail ∎)

  -- nonempty (return x) is parser equivalent to fail.

  nonempty-return :
    ∀ {Tok R} {x : R} → nonempty {Tok = Tok} (return x) ≅P fail
  nonempty-return = BagMonoid.refl ∷ λ t → ♯ (fail ∎)

  -- nonempty can be defined in terms of token, _>>=_ and D.

  private

    nonempty′ : ∀ {Tok R xs} (p : Parser Tok R xs) → Parser Tok R []
    nonempty′ p = token >>= λ t → D t p

  nonempty-definable : ∀ {Tok R xs} (p : Parser Tok R xs) →
                       nonempty p ≅P nonempty′ p
  nonempty-definable p = BagMonoid.refl ∷ λ t → ♯ (
    D t p              ≅⟨ sym $ Monad.left-identity t (λ t′ → D t′ p) ⟩
    ret-D t            ≅⟨ sym $ AdditiveMonoid.right-identity (ret-D t) ⟩
    ret-D t ∣ fail     ≅⟨ (ret-D t ∎) ∣ sym (Monad.left-zero _) ⟩
    D t (nonempty′ p)  ∎)
    where ret-D = λ (t : _) → return t >>= (λ t′ → D t′ p)

------------------------------------------------------------------------
-- A law for cast

module Cast where

  -- Casts can be erased.

  correct : ∀ {Tok R xs₁ xs₂}
              {xs₁≈xs₂ : xs₁ List-∼[ bag ] xs₂}
              {p : Parser Tok R xs₁} →
            cast xs₁≈xs₂ p ≅P p
  correct {xs₁≈xs₂ = xs₁≈xs₂} {p} =
    BagMonoid.sym xs₁≈xs₂ ∷ λ t → ♯ (D t p ∎)

------------------------------------------------------------------------
-- A law for subst

module Subst where

  -- Uses of subst can be erased.

  correct : ∀ {Tok R xs₁ xs₂}
              (xs₁≡xs₂ : xs₁ ≡ xs₂)
              {p : Parser Tok R xs₁} →
            P.subst (Parser Tok R) xs₁≡xs₂ p ≅P p
  correct P.refl {p} = p ∎

  correct∞ : ∀ {Tok R xs₁ xs₂ A} {m : Maybe A}
              (xs₁≡xs₂ : xs₁ ≡ xs₂)
              (p : ∞⟨ m ⟩Parser Tok R xs₁) →
             ♭? (P.subst (∞⟨ m ⟩Parser Tok R) xs₁≡xs₂ p) ≅P ♭? p
  correct∞ P.refl p = ♭? p ∎

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --without-K #-}
module Util.HoTT.Univalence.Beta where

open import Util.HoTT.Equiv
open import Util.HoTT.Equiv.Induction
open import Util.HoTT.Univalence.Axiom
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁻ ; cast )

private
  variable
    α β γ : Level
    A B C : Set α

≃→≡-β : ≃→≡ (≃-refl {A = A}) ≡ refl
≃→≡-β = ≃→≡∘≡→≃ refl

cast-≃→≡ : ∀ (A≃B : A ≃ B) {x}
  → cast (≃→≡ A≃B) x ≡ A≃B .forth x
cast-≃→≡ A≃B {x}
  = J-≃ (λ A B A≃B → ∀ x → cast (≃→≡ A≃B) x ≡ A≃B .forth x)
      (λ A x → subst (λ p → cast p x ≡ x) (sym ≃→≡-β) refl) A≃B x

cast-≅→≡ : ∀ (A≅B : A ≅ B) {x}
  → cast (≅→≡ A≅B) x ≡ A≅B .forth x
cast-≅→≡ = cast-≃→≡ ∘ ≅→≃

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
------------------------------------------------------------------------------
-- Testing records
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module Record where

postulate
  D  : Set
  P₁ : D → Set
  P₂ : D → D → Set

record P (a b : D) : Set where
  constructor is
  field
    property₁ : P₁ a
    property₂ : P₂ a b
{-# ATP axiom is #-}

postulate
  p₁ : ∀ a → P₁ a
  p₂ : ∀ a b → P₂ a b
{-# ATP axiom p₁ #-}
{-# ATP axiom p₂ #-}

thm₁ : ∀ a b → P a b
thm₁ a b = is (p₁ a) (p₂ a b)

postulate thm₂ : ∀ a b → P a b
{-# ATP prove thm₂ #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Structure.Container.SetLike.Proofs where

{-
open import Data.Boolean
open import Data.Boolean.Stmt
open import Functional
open import Lang.Instance
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Container.SetLike
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Relator hiding (module Names)
open import Structure.Setoid renaming (_≡_ to _≡ₛ_ ; _≢_ to _≢ₛ_)
open import Type.Properties.Inhabited
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆ ℓ₇ ℓ₈ ℓ₉ ℓ₁₀ ℓₗ ℓₗ₁ ℓₗ₂ ℓₗ₃ : Lvl.Level
private variable A B C C₁ C₂ Cₒ Cᵢ E E₁ E₂ : Type{ℓ}
private variable _∈_ _∈ₒ_ _∈ᵢ_ : E → C

import      Data
import      Data.Either as Either
import      Data.Tuple as Tuple
open import Logic.Predicate.Theorems
open import Logic.Propositional.Theorems
open import Structure.Relator.Ordering
open import Structure.Relator.Proofs
open import Syntax.Transitivity

module _ ⦃ setLike : SetLike{ℓ₁}{ℓ₁}{ℓ₂}{C}{C} (_∈_) {ℓ₄}{ℓ₅} ⦄ where
  open SetLike(setLike)

  module _ ⦃ _ : Equiv{ℓₗ}(C) ⦄ where
    private
      instance
        big-intersection-filter-unary-relator : ⦃ _ : Equiv{ℓₗ}(E) ⦄ ⦃ _ : BinaryRelator{B = C}(_∈_) ⦄ → ∀{As} → UnaryRelator(\a → ∀{A} → (A ∈ As) → (a ∈ A))
        big-intersection-filter-unary-relator ⦃ [∈]-binaryRelator ⦄ = [∀]-unaryRelator ⦃ rel-P = \{A} → [→]-unaryRelator ⦃ rel-P = const-unaryRelator ⦄ ⦃ rel-Q = BinaryRelator.left (binaryRelator(_∈_)) {A} ⦄ ⦄

    filter-big-union-to-big-intersection : ⦃ _ : BinaryRelator(_∈_) ⦄ ⦃ _ : FilterFunction(_∈_){ℓ = ℓ₁ Lvl.⊔ ℓ₂} ⦄ ⦃ _ : BigUnionOperator(_∈_)(_∈_) ⦄ → BigIntersectionOperator(_∈_)(_∈_)
    BigIntersectionOperator.⋂ filter-big-union-to-big-intersection As = filter(\a → ∀{A} → (A ∈ As) → (a ∈ A))(⋃ As)
    Tuple.left (BigIntersectionOperator.membership filter-big-union-to-big-intersection {As} eAs {a}) p = [↔]-to-[←] Filter.membership ([∧]-intro ([↔]-to-[←] BigUnion.membership ([∃]-map-proof (aAs ↦ [∧]-intro aAs (p aAs)) eAs)) (\{x} → p{x}))
    Tuple.right (BigIntersectionOperator.membership filter-big-union-to-big-intersection {As} eAs {a}) xfilter {A} AAs = [∧]-elimᵣ([↔]-to-[→] Filter.membership xfilter) AAs

  module _
    ⦃ _ : Equiv{ℓₗ}(C) ⦄
    ⦃ _ : BinaryRelator(_∈_) ⦄
    where

    -- Also called: Russell's paradox.
    filter-universal-contradiction : ⦃ _ : FilterFunction(_∈_){ℓ = ℓ₂} ⦄ ⦃ _ : UniversalSet(_∈_) ⦄ → ⊥
    filter-universal-contradiction = proof-not-in proof-in where
      instance
        filter-unary-relator : UnaryRelator(x ↦ (x ∉ x))
        filter-unary-relator = [¬]-unaryRelator ⦃ rel-P = binary-unaryRelator ⦄

      notInSelf : C
      notInSelf = filter (x ↦ (x ∉ x))(𝐔)

      proof-not-in : (notInSelf ∉ notInSelf)
      proof-not-in pin = [∧]-elimᵣ([↔]-to-[→] Filter.membership pin) pin

      proof-in : (notInSelf ∈ notInSelf)
      proof-in = [↔]-to-[←] Filter.membership ([∧]-intro Universal.membership proof-not-in)

module _ ⦃ setLike : SetLike{ℓ₁}{ℓ₂}{ℓ₃}{C}{E} (_∈_) {ℓ₄}{ℓ₅} ⦄ where
  open SetLike(setLike)

  private variable a b c : C
  private variable x y z : E

  [⊇]-membership : ∀{a b} → (a ⊇ b) ↔ (∀{x} → (x ∈ a) ← (x ∈ b))
  [⊇]-membership = [⊆]-membership

  module _ ⦃ _ : Equiv{ℓₗ}(E) ⦄ where
    pair-to-singleton : ⦃ _ : PairSet(_∈_) ⦄ → SingletonSet(_∈_)
    SingletonSet.singleton  pair-to-singleton e = pair e e
    SingletonSet.membership pair-to-singleton = [↔]-transitivity Pair.membership ([↔]-intro [∨]-introₗ ([∨]-elim id id))

    filter-to-empty : let _ = c in ⦃ _ : FilterFunction(_∈_){ℓ = Lvl.𝟎} ⦄ → EmptySet(_∈_)
    EmptySet.∅ (filter-to-empty {c = c}) = filter (const ⊥) c
    EmptySet.membership filter-to-empty p = [∧]-elimᵣ ([↔]-to-[→] Filter.membership p)

    module _
      ⦃ _ : Equiv{ℓₗ}(C) ⦄
      ⦃ _ : BinaryRelator(_∈_) ⦄
      where

      filter-to-intersection : ⦃ _ : FilterFunction(_∈_){ℓ = ℓ₃} ⦄ → IntersectionOperator(_∈_)
      IntersectionOperator._∩_ filter-to-intersection a b = filter (_∈ b) ⦃ unaryRelator = BinaryRelator.left infer ⦄ a
      IntersectionOperator.membership filter-to-intersection = Filter.membership ⦃ unaryRelator = BinaryRelator.left infer ⦄

  module _ ⦃ equivalence : Equivalence(_≡_) ⦄ where
    private
      instance
        [≡]-equiv : Equiv{ℓ₅}(C)
        Equiv._≡_ [≡]-equiv = _≡_
        Equiv.equivalence [≡]-equiv = equivalence

    [∈]-unaryOperatorᵣ : UnaryRelator(x ∈_)
    UnaryRelator.substitution [∈]-unaryOperatorᵣ xy = [↔]-to-[→] ([↔]-to-[→] [≡]-membership xy)

    module _
      ⦃ _ : Equiv{ℓₗ₂}(E) ⦄
      ⦃ _ : Weak.PartialOrder(_⊆_)(_≡_) ⦄
      ⦃ _ : BinaryRelator(_∈_) ⦄
      ⦃ _ : (_≡_) ⊆₂ (_⊆_) ⦄
      ⦃ _ : (_≡_) ⊆₂ (_⊇_) ⦄
      where

      [⊆]-binaryRelator : BinaryRelator(_⊆_)
      BinaryRelator.substitution [⊆]-binaryRelator p1 p2 ps = sub₂(_≡_)(_⊇_) p1 🝖 ps 🝖 sub₂(_≡_)(_⊆_) p2

      [⊇]-binaryRelator : BinaryRelator(_⊇_)
      BinaryRelator.substitution [⊇]-binaryRelator = swap(substitute₂(_⊆_) ⦃ [⊆]-binaryRelator ⦄)

  [≡]-to-[⊆] : (_≡_) ⊆₂ (_⊆_)
  _⊆₂_.proof [≡]-to-[⊆] =
    [↔]-to-[←] [⊆]-membership
    ∘ [∀][→]-distributivity [↔]-to-[→]
    ∘ [↔]-to-[→] [≡]-membership

  [≡]-to-[⊇] : (_≡_) ⊆₂ (_⊇_)
  _⊆₂_.proof [≡]-to-[⊇] =
    [↔]-to-[←] [⊆]-membership
    ∘ [∀][→]-distributivity [↔]-to-[←]
    ∘ [↔]-to-[→] [≡]-membership

  [⊆]-reflexivity : Reflexivity(_⊆_)
  Reflexivity.proof [⊆]-reflexivity = [↔]-to-[←] [⊆]-membership [→]-reflexivity

  [⊆]-antisymmetry : Antisymmetry(_⊆_)(_≡_)
  Antisymmetry.proof [⊆]-antisymmetry ab ba =
    [↔]-to-[←] [≡]-membership ([↔]-intro ([↔]-to-[→] [⊇]-membership ba) ([↔]-to-[→] [⊆]-membership ab))

  [⊆]-transitivity : Transitivity(_⊆_)
  Transitivity.proof [⊆]-transitivity xy yz =
    [↔]-to-[←] [⊆]-membership ([→]-transitivity ([↔]-to-[→] [⊆]-membership xy) ([↔]-to-[→] [⊆]-membership yz))

  [⊆]-partialOrder : Weak.PartialOrder(_⊆_)(_≡_)
  [⊆]-partialOrder = Weak.intro ⦃ [⊆]-antisymmetry ⦄ ⦃ [⊆]-transitivity ⦄ ⦃ [⊆]-reflexivity ⦄

  [≡]-reflexivity : Reflexivity(_≡_)
  Reflexivity.proof [≡]-reflexivity = [↔]-to-[←] [≡]-membership [↔]-reflexivity

  [≡]-symmetry : Symmetry(_≡_)
  Symmetry.proof [≡]-symmetry =
    [↔]-to-[←] [≡]-membership
    ∘ [∀][→]-distributivity [↔]-symmetry
    ∘ [↔]-to-[→] [≡]-membership

  [≡]-transitivity : Transitivity(_≡_)
  Transitivity.proof [≡]-transitivity xy yz = [↔]-to-[←] [≡]-membership ([↔]-transitivity ([↔]-to-[→] [≡]-membership xy) ([↔]-to-[→] [≡]-membership yz))

  [≡]-equivalence : Equivalence(_≡_)
  [≡]-equivalence = intro ⦃ [≡]-reflexivity ⦄ ⦃ [≡]-symmetry ⦄ ⦃ [≡]-transitivity ⦄

  -- TODO: These are unneccessary if one uses Structure.Operator.SetAlgebra or lattices
  module _ ⦃ _ : EmptySet(_∈_) ⦄ ⦃ _ : UniversalSet(_∈_) ⦄ ⦃ _ : ComplementOperator(_∈_) ⦄ where
    ∁-of-∅ : (∁(∅) ≡ 𝐔)
    ∁-of-∅ = [↔]-to-[←] [≡]-membership ([↔]-intro ([↔]-to-[←] Complement.membership ∘ const Empty.membership) (const Universal.membership))

    ∁-of-𝐔 : (∁(𝐔) ≡ ∅)
    ∁-of-𝐔 = [↔]-to-[←] [≡]-membership ([↔]-intro ([⊥]-elim ∘ Empty.membership) ([⊥]-elim ∘ apply Universal.membership ∘ [↔]-to-[→] Complement.membership))

module _ ⦃ setLike : SetLike{ℓ₁}{ℓ₂}{ℓ₃}{C}{E} (_∈_) {ℓ₄}{ℓ₅} ⦄ where
  open SetLike(setLike)

  open import Logic.Classical
  open import Structure.Operator.Lattice
  open import Structure.Operator.Properties

  module _ where
    private
      instance
        equiv-C : Equiv{ℓ₅}(C)
        equiv-C = intro(_≡_) ⦃ [≡]-equivalence ⦄

    module _ ⦃ _ : ComplementOperator(_∈_) ⦄ where
      instance
        [∁]-function : Function(∁)
        Function.congruence [∁]-function xy =
          [↔]-to-[←] [≡]-membership (
            Complement.membership                            ⦗ [↔]-transitivity ⦘ᵣ
            [¬]-unaryOperator ([↔]-to-[→] [≡]-membership xy) ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry Complement.membership
          )

      instance
        [∁]-involution : ⦃ _ : ∀{x y} → Classical(x ∈ y) ⦄ → Involution(∁)
        Involution.proof [∁]-involution =
          [↔]-to-[←] [≡]-membership (
            Complement.membership                   ⦗ [↔]-transitivity ⦘ᵣ
            [¬]-unaryOperator Complement.membership ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro [¬¬]-intro [¬¬]-elim
          )

    module _ ⦃ _ : UnionOperator(_∈_) ⦄ where
      instance
        [∪]-binaryOperator : BinaryOperator(_∪_)
        BinaryOperator.congruence [∪]-binaryOperator xy₁ xy₂ =
          [↔]-to-[←] [≡]-membership (
            Union.membership ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro (Either.map ([↔]-to-[←] ([↔]-to-[→] [≡]-membership xy₁)) ([↔]-to-[←] ([↔]-to-[→] [≡]-membership xy₂))) (Either.map ([↔]-to-[→] ([↔]-to-[→] [≡]-membership xy₁)) ([↔]-to-[→] ([↔]-to-[→] [≡]-membership xy₂))) ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry Union.membership
          )

      instance
        [∪]-commutativity : Commutativity(_∪_)
        Commutativity.proof [∪]-commutativity {x} {y} =
          [↔]-to-[←] [≡]-membership (
            Union.membership                    ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro [∨]-symmetry [∨]-symmetry ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry Union.membership
          )

      instance
        [∪]-associativity : Associativity(_∪_)
        Associativity.proof [∪]-associativity {x} {y} =
          [↔]-to-[←] [≡]-membership (
            Union.membership ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro (Either.mapLeft ([↔]-to-[←] Union.membership)) (Either.mapLeft ([↔]-to-[→] Union.membership)) ⦗ [↔]-transitivity ⦘ᵣ
            [∨]-associativity ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry([↔]-intro (Either.mapRight ([↔]-to-[←] Union.membership)) (Either.mapRight ([↔]-to-[→] Union.membership))) ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry Union.membership
          )

      module _ ⦃ _ : EmptySet(_∈_) ⦄ where
        instance
          [∪]-identityₗ : Identityₗ(_∪_)(∅)
          Identityₗ.proof [∪]-identityₗ {x} =
            [↔]-to-[←] [≡]-membership (
              Union.membership ⦗ [↔]-transitivity ⦘ᵣ
              [↔]-intro (Either.mapLeft [⊥]-elim) (Either.mapLeft Empty.membership) ⦗ [↔]-transitivity ⦘ᵣ
              [↔]-intro [∨]-introᵣ [∨]-identityₗ
            )

    module _ ⦃ _ : IntersectionOperator(_∈_) ⦄ where
      instance
        [∩]-binaryOperator : BinaryOperator(_∩_)
        BinaryOperator.congruence [∩]-binaryOperator xy₁ xy₂ =
          [↔]-to-[←] [≡]-membership (
            Intersection.membership ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro (Tuple.map ([↔]-to-[←] ([↔]-to-[→] [≡]-membership xy₁)) ([↔]-to-[←] ([↔]-to-[→] [≡]-membership xy₂))) (Tuple.map ([↔]-to-[→] ([↔]-to-[→] [≡]-membership xy₁)) ([↔]-to-[→] ([↔]-to-[→] [≡]-membership xy₂))) ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry Intersection.membership
          )

      instance
        [∩]-commutativity : Commutativity(_∩_)
        Commutativity.proof [∩]-commutativity {x} {y} =
          [↔]-to-[←] [≡]-membership (
            Intersection.membership             ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro [∧]-symmetry [∧]-symmetry ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry Intersection.membership
          )

      instance
        [∩]-associativity : Associativity(_∩_)
        Associativity.proof [∩]-associativity {x} {y} =
          [↔]-to-[←] [≡]-membership (
            Intersection.membership ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro (Tuple.mapLeft ([↔]-to-[←] Intersection.membership)) (Tuple.mapLeft ([↔]-to-[→] Intersection.membership)) ⦗ [↔]-transitivity ⦘ᵣ
            [∧]-associativity ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry([↔]-intro (Tuple.mapRight ([↔]-to-[←] Intersection.membership)) (Tuple.mapRight ([↔]-to-[→] Intersection.membership))) ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry Intersection.membership
          )

      module _ ⦃ _ : UniversalSet(_∈_) ⦄ where
        instance
          [∩]-identityₗ : Identityₗ(_∩_)(𝐔)
          Identityₗ.proof [∩]-identityₗ {x} =
            [↔]-to-[←] [≡]-membership (
              Intersection.membership ⦗ [↔]-transitivity ⦘ᵣ
              [↔]-intro (Tuple.mapLeft {ℓ₁} (const Universal.membership)) (Tuple.mapLeft (const [⊤]-intro)) ⦗ [↔]-transitivity ⦘ᵣ
              [↔]-intro ([∧]-intro [⊤]-intro) [∧]-elimᵣ
            )

    module _ ⦃ _ : UnionOperator(_∈_) ⦄ ⦃ _ : IntersectionOperator(_∈_) ⦄ where
      instance
        [∩][∪]-distributivityₗ : Distributivityₗ(_∩_)(_∪_)
        Distributivityₗ.proof [∩][∪]-distributivityₗ {x} {y} {z} =
          [↔]-to-[←] [≡]-membership (
            Intersection.membership ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro (Tuple.mapRight ([↔]-to-[←] Union.membership)) (Tuple.mapRight ([↔]-to-[→] Union.membership)) ⦗ [↔]-transitivity ⦘ᵣ
            [∧][∨]-distributivityₗ ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro (Either.map ([↔]-to-[→] Intersection.membership) ([↔]-to-[→] Intersection.membership)) (Either.map ([↔]-to-[←] Intersection.membership) ([↔]-to-[←] Intersection.membership)) ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry Union.membership
          )

      instance
        [∪][∩]-distributivityₗ : Distributivityₗ(_∪_)(_∩_)
        Distributivityₗ.proof [∪][∩]-distributivityₗ {x} {y} {z} =
          [↔]-to-[←] [≡]-membership (
            Union.membership ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro (Either.mapRight ([↔]-to-[←] Intersection.membership)) (Either.mapRight ([↔]-to-[→] Intersection.membership)) ⦗ [↔]-transitivity ⦘ᵣ
            [∨][∧]-distributivityₗ ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-intro (Tuple.map ([↔]-to-[→] Union.membership) ([↔]-to-[→] Union.membership)) (Tuple.map ([↔]-to-[←] Union.membership) ([↔]-to-[←] Union.membership)) ⦗ [↔]-transitivity ⦘ᵣ
            [↔]-symmetry Intersection.membership
          )

      instance
        [∩][∪]-absorptionₗ : Absorptionₗ(_∩_)(_∪_)
        Absorptionₗ.proof [∩][∪]-absorptionₗ {x} {y} =
          [↔]-to-[←] [≡]-membership (
            Intersection.membership ⦗ [↔]-transitivity ⦘
            [↔]-intro (ax ↦ [∧]-intro ax ([↔]-to-[←] Union.membership ([∨]-introₗ ax))) [∧]-elimₗ
          )

      instance
        [∪][∩]-absorptionₗ : Absorptionₗ(_∪_)(_∩_)
        Absorptionₗ.proof [∪][∩]-absorptionₗ {x} {y} =
          [↔]-to-[←] [≡]-membership (
            Union.membership ⦗ [↔]-transitivity ⦘
            [↔]-intro [∨]-introₗ ([∨]-elim id ([∧]-elimₗ ∘ [↔]-to-[→] Intersection.membership))
          )

      instance
        [∪][∩]-lattice : Lattice(C) (_∪_)(_∩_)
        Lattice.[∨]-operator       [∪][∩]-lattice = [∪]-binaryOperator
        Lattice.[∧]-operator       [∪][∩]-lattice = [∩]-binaryOperator
        Lattice.[∨]-commutativity  [∪][∩]-lattice = [∪]-commutativity
        Lattice.[∧]-commutativity  [∪][∩]-lattice = [∩]-commutativity
        Lattice.[∨]-associativity  [∪][∩]-lattice = [∪]-associativity
        Lattice.[∧]-associativity  [∪][∩]-lattice = [∩]-associativity
        Lattice.[∨][∧]-absorptionₗ [∪][∩]-lattice = [∪][∩]-absorptionₗ
        Lattice.[∧][∨]-absorptionₗ [∪][∩]-lattice = [∩][∪]-absorptionₗ

      instance
        [∪][∩]-distributiveLattice : Lattice.Distributive([∪][∩]-lattice)
        [∪][∩]-distributiveLattice = intro

      module _ ⦃ _ : EmptySet(_∈_) ⦄ ⦃ _ : UniversalSet(_∈_) ⦄ where
        instance
          [∪][∩]-boundedLattice : Lattice.Bounded([∪][∩]-lattice)(∅)(𝐔)
          Lattice.Bounded.[∨]-identityₗ [∪][∩]-boundedLattice = [∪]-identityₗ
          Lattice.Bounded.[∧]-identityₗ [∪][∩]-boundedLattice = [∩]-identityₗ

      module _ ⦃ _ : ComplementOperator(_∈_) ⦄ where
-}

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:
module Issue835 where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

postulate
  A : Set
  x y : A

F : x ≡ y → Set
F ()


text:
-- 2014-05-02
-- This looped in the epic backend after Andreas' big projection refactoring (Oct 2013)

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}   -- Essential

f : ℕ → ℕ
f zero    = zero
f (suc m) = m

postulate
  IO : Set → Set

{-# COMPILED_TYPE IO IO #-}

postulate
  return  : ∀ {A} → A → IO A

{-# COMPILED_EPIC return (u1 : Unit, a : Any) -> Any = ioreturn(a) #-}

main : IO ℕ
main = return zero


text:
module Issue4924 where

record R (T : Set) : Set where
  field
    f : T → T

module _ {A B : Set} (ra : R A) (rb : R B) (pri : {T : Set} → {{r : R T}} → T) where
  open R ra
  open R rb

  instance
    _ = ra

  _ : A
  _ = f pri

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --without-K --safe #-}
-- https://www.cs.bham.ac.uk/~mhe/papers/omniscient-journal-revised.pdf

module Constructive.Omniscience where

open import Level renaming (zero to lzero; suc to lsuc)
import Data.Bool as 𝔹 using (_≤_)
open import Data.Bool as 𝔹 using (Bool; true; false; T; f≤t; b≤b; _∧_; not; _∨_)
import Data.Bool.Properties as 𝔹ₚ
open import Data.Empty
open import Data.Unit using (tt)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product as Prod
open import Data.Sum as Sum
open import Function.Base
open import Relation.Binary as B
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Relation.Nullary.Decidable
import Relation.Unary as U

-- agda-misc
open import Constructive.Axiom
open import Constructive.Axiom.Properties
open import Constructive.Axiom.Properties.Base.Lemma
open import Constructive.Common
open import Constructive.Combinators

ℕ∞ : Set
ℕ∞ = Σ (ℕ → Bool) λ x → ∀ i → T (x (suc i)) → T (x i)

⟦_⟧C : ℕ → ℕ → Bool
⟦ n ⟧C = λ m → isYes (m <? n)

⟦_⟧C-con : ∀ n i → T (⟦ n ⟧C (suc i)) → T (⟦ n ⟧C i)
⟦ n ⟧C-con i True[si<n] = fromWitness (m+n≤o⇒n≤o 1 $ toWitness True[si<n])

⟦_⟧ : ℕ → ℕ∞
⟦ n ⟧ = ⟦ n ⟧C , ⟦ n ⟧C-con

∞ : ℕ∞
∞ = (λ _ → true) , (λ i _ → tt)

_≈_ : Rel (ℕ → Bool) lzero
α ≈ β = ∀ i → α i ≡ β i

_≉_ : Rel (ℕ → Bool) lzero
α ≉ β = ¬ (α ≈ β)

_#_ : Rel (ℕ → Bool) lzero
α # β = ∃ λ i → α i ≢ β i

#⇒≉  : {α β : ℕ → Bool} → α # β → α ≉ β
#⇒≉ {α} {β} (i , αi≢βi) α≈β = αi≢βi (α≈β i)

≈-refl : {α : ℕ → Bool} → α ≈ α
≈-refl _ = refl

≈-sym : {α β : ℕ → Bool} → α ≈ β → β ≈ α
≈-sym α≈β i = sym (α≈β i)

≈-trans : {α β γ : ℕ → Bool} → α ≈ β → β ≈ γ → α ≈ γ
≈-trans α≈β β≈γ i = trans (α≈β i) (β≈γ i)

_≈∞_ : Rel ℕ∞ lzero
x ≈∞ y = proj₁ x ≈ proj₁ y

_≉∞_ : Rel ℕ∞ lzero
x ≉∞ y = proj₁ x ≉ proj₁ y

_#∞_ : Rel ℕ∞ lzero
x #∞ y = proj₁ x # proj₁ y

⟦⟧-cong : ∀ {m n} → m ≡ n → ⟦ m ⟧ ≈∞ ⟦ n ⟧
⟦⟧-cong {m} {n} m≡n i = cong (λ x → ⟦ x ⟧C i) m≡n

-- Proposition 3.1
-- r = ≤-all
≤-all : (ℕ → Bool) → (ℕ → Bool)
≤-all α zero    = α 0
≤-all α (suc n) = α (suc n) ∧ ≤-all α n

≤-all-idem : ∀ α → ≤-all (≤-all α) ≈ ≤-all α
≤-all-idem α zero    = refl
≤-all-idem α (suc n) = begin
  (α (suc n) ∧ ≤-all α n) ∧ ≤-all (≤-all α) n
    ≡⟨ cong ((α (suc n) ∧ ≤-all α n) ∧_) $ ≤-all-idem α n ⟩
  (α (suc n) ∧ ≤-all α n) ∧ ≤-all α n
    ≡⟨ 𝔹ₚ.∧-assoc (α (suc n)) (≤-all α n) (≤-all α n) ⟩
  α (suc n) ∧ (≤-all α n ∧ ≤-all α n)
    ≡⟨ cong (α (suc n) ∧_) $ 𝔹ₚ.∧-idem (≤-all α n) ⟩
  α (suc n) ∧ ≤-all α n
    ∎
  where open ≡-Reasoning

private
  T-∧-× : ∀ {x y} → T (x ∧ y) → (T x × T y)
  T-∧-× {true} {true} t = tt , tt

  T-×-∧ : ∀ {x y} → (T x × T y) → T (x ∧ y)
  T-×-∧ {true} {true} (tt , tt) = tt

  ≤⇒≡∨< : ∀ {m n} → m ≤ n → (m ≡ n) ⊎ (m < n)
  ≤⇒≡∨< {m} {n} m≤n with m ≟ n
  ... | yes m≡n = inj₁ m≡n
  ... | no  m≢n = inj₂ (≤∧≢⇒< m≤n m≢n)

≤-all-convergent : ∀ α i → T (≤-all α (suc i)) → T (≤-all α i)
≤-all-convergent α n t = proj₂ (T-∧-× t)

≤-all-ℕ∞ : (ℕ → Bool) → ℕ∞
≤-all-ℕ∞ α = ≤-all α , ≤-all-convergent α

≤-all-extract-by-≤ : ∀ α {n k} → k ≤ n → T (≤-all α n) → T (α k)
≤-all-extract-by-≤ α {zero}  {.0}    z≤n       t = t
≤-all-extract-by-≤ α {suc n} {zero}  z≤n       t =
  ≤-all-extract-by-≤ α {n} {0} z≤n (proj₂ (T-∧-× t))
≤-all-extract-by-≤ α {suc n} {suc k} (s≤s k≤n) t with ≤⇒≡∨< k≤n
... | inj₁ k≡n    = subst (T ∘′ α ∘′ suc) (sym k≡n) (proj₁ (T-∧-× t))
... | inj₂ suck≤n = ≤-all-extract-by-≤ α suck≤n (proj₂ (T-∧-× t))

≤-all-extract : ∀ α n → T (≤-all α n) → T (α n)
≤-all-extract α n = ≤-all-extract-by-≤ α ≤-refl

≤-all-construct : ∀ α n → (∀ k → k ≤ n → T (α k)) → T (≤-all α n)
≤-all-construct α zero    f = f zero ≤-refl
≤-all-construct α (suc n) f =
  T-×-∧ ((f (suc n) ≤-refl) , ≤-all-construct α n λ k k≤n → f k (≤-step k≤n))

private
  not-injective : ∀ {x y} → not x ≡ not y → x ≡ y
  not-injective {false} {false} refl = refl
  not-injective {true}  {true}  refl = refl

  x≢y⇒not[x]≡y : ∀ {x y} → x ≢ y → not x ≡ y
  x≢y⇒not[x]≡y {false} {false} x≢y = contradiction refl x≢y
  x≢y⇒not[x]≡y {false} {true}  x≢y = refl
  x≢y⇒not[x]≡y {true}  {false} x≢y = refl
  x≢y⇒not[x]≡y {true}  {true}  x≢y = contradiction refl x≢y

  x≡y⇒not[x]≢y : ∀ {x y} → x ≡ y → not x ≢ y
  x≡y⇒not[x]≢y {false} {false} p ()
  x≡y⇒not[x]≢y {false} {true}  () q
  x≡y⇒not[x]≢y {true}  {false} () q
  x≡y⇒not[x]≢y {true}  {true}  p ()

  not[x]≢y⇒x≡y : ∀ {x y} → not x ≢ y → x ≡ y
  not[x]≢y⇒x≡y {x} {y} not[x]≢y =
    subst (_≡ y) (𝔹ₚ.not-involutive x) $ x≢y⇒not[x]≡y not[x]≢y

  not[x]≡y⇒x≢y : ∀ {x y} → not x ≡ y → x ≢ y
  not[x]≡y⇒x≢y not[x]≡y x≡y = x≡y⇒not[x]≢y x≡y not[x]≡y

-- LPO-Bool <=> ∀ x → (x #∞ ∞) ⊎ (x ≈∞ ∞)
lpo-Bool⇒∀x→x#∞⊎x≈∞ : LPO-Bool ℕ → ∀ x → (x #∞ ∞) ⊎ (x ≈∞ ∞)
lpo-Bool⇒∀x→x#∞⊎x≈∞ lpo-Bool (α , con) with lpo-Bool λ n → not (α n)
... | inj₁ (x , not[αx]≡true) = inj₁ (x , not[x]≡y⇒x≢y not[αx]≡true)
... | inj₂ ¬∃x→not[αx]≡true   =
  inj₂ λ i → not[x]≢y⇒x≡y $′ ¬∃P→∀¬P ¬∃x→not[αx]≡true i

private
  T-to-≡ : ∀ {x} → T x → x ≡ true
  T-to-≡ {true} tx = refl

  ≡-to-T : ∀ {x} → x ≡ true → T x
  ≡-to-T {true} x≡true = tt

  T-¬-not : ∀ {x} → ¬ (T x) → T (not x)
  T-¬-not {false} n = tt
  T-¬-not {true}  n = n tt

  T-not-¬ : ∀ {x} → T (not x) → ¬ (T x)
  T-not-¬ {false} tt ()
  T-not-¬ {true}  () y

  ¬-T-not-to-T : ∀ {x} → ¬ T (not x) → T x
  ¬-T-not-to-T {x} ¬Tnotx = subst T (𝔹ₚ.not-involutive x) $ T-¬-not ¬Tnotx

  ≤-to-→ : ∀ {x y} → x 𝔹.≤ y → T x → T y
  ≤-to-→ {true} {true} x≤y _ = tt

  →-to-≤ : ∀ {x y} → (T x → T y) → x 𝔹.≤ y
  →-to-≤ {false} {false} Tx→Ty = b≤b
  →-to-≤ {false} {true}  Tx→Ty = f≤t
  →-to-≤ {true}  {false} Tx→Ty = ⊥-elim (Tx→Ty tt)
  →-to-≤ {true}  {true}  Tx→Ty = b≤b

  T-≡ : ∀ {x y} → (T x → T y) → (T y → T x) → x ≡ y
  T-≡ Tx→Ty Ty→Tx = 𝔹ₚ.≤-antisym (→-to-≤ Tx→Ty) (→-to-≤ Ty→Tx)

¬T-≤-all-to-≤ : ∀ α n → ¬ T (≤-all α n) → ∃ λ k → k ≤ n × ¬ T (α k)
¬T-≤-all-to-≤ α zero    ¬T with 𝔹ₚ.T? (α 0)
... | yes Tα0 = contradiction Tα0 ¬T
... | no ¬Tα0 = 0 , (z≤n , ¬Tα0)
¬T-≤-all-to-≤ α (suc n) ¬T with 𝔹ₚ.T? (α (suc n))
... | yes Tαsn =
 Prod.map₂ (Prod.map₁ ≤-step) $
   ¬T-≤-all-to-≤ α n (contraposition (λ T≤-allαn → T-×-∧ (Tαsn , T≤-allαn)) ¬T)
... | no ¬Tαsn = suc n , ≤-refl , ¬Tαsn

¬T-≤-all-to-≤′ : ∀ α n → ¬ T (≤-all (not ∘′ α) n) → ∃ λ k → k ≤ n × T (α k)
¬T-≤-all-to-≤′ α n ¬T with ¬T-≤-all-to-≤ (not ∘ α) n ¬T
... | (k , k≤n , ¬Tnotαn) = k , (k≤n , ¬-T-not-to-T ¬Tnotαn)

¬T-≤-all-to-∃ : ∀ α n → ¬ T (≤-all α n) → ∃ λ k → ¬ T (α k)
¬T-≤-all-to-∃ α n ¬T = Prod.map₂ proj₂ (¬T-≤-all-to-≤ α n ¬T)

¬T-≤-all-to-∃′ : ∀ α n → ¬ T (≤-all (not ∘′ α) n) → ∃ λ k → T (α k)
¬T-≤-all-to-∃′ α n ¬T = Prod.map₂ proj₂ (¬T-≤-all-to-≤′ α n ¬T)

≤-to-¬T-≤-all : ∀ α n → ∃ (λ k → k ≤ n × ¬ T (α k)) → ¬ T (≤-all α n)
≤-to-¬T-≤-all α n (k , k≤n  , ¬Tαk) ttt = ¬Tαk (≤-all-extract-by-≤ α k≤n ttt)

∀x→x#∞⊎x≈∞⇒lpo-Bool : (∀ x → (x #∞ ∞) ⊎ (x ≈∞ ∞)) → LPO-Bool ℕ
∀x→x#∞⊎x≈∞⇒lpo-Bool ≈∞? P with ≈∞? (≤-all-ℕ∞ (λ n → not (P n)))
... | inj₁ (x , ≤-all[not∘P,x]≢true) =
  inj₁ (Prod.map₂ T-to-≡ (¬T-≤-all-to-∃′ P x
    (contraposition T-to-≡ ≤-all[not∘P,x]≢true)))
... | inj₂ ∀i→≤-all[not∘P,i]≡true =
  inj₂ (∀¬P→¬∃P λ i → not[x]≡y⇒x≢y (T-to-≡ $ ≤-all-extract (not ∘ P) i $
    ≡-to-T (∀i→≤-all[not∘P,i]≡true i)))

-- Theorem 3.5
ε : (ℕ∞ → Bool) → ℕ∞
ε p = ≤-all-ℕ∞ λ n → p ⟦ n ⟧

T-⟦⟧C-to-< : ∀ {n i} → T (⟦ n ⟧C i) → i < n
T-⟦⟧C-to-< t = toWitness t

<-to-T-⟦⟧C : ∀ {n i} → i < n → T (⟦ n ⟧C i)
<-to-T-⟦⟧C i<n = fromWitness i<n

lemma-1-forward : ∀ (p : ℕ∞ → Bool) n →
                  ε p ≈∞ ⟦ n ⟧ → ¬ T (p ⟦ n ⟧) × (∀ k → k < n → T (p ⟦ k ⟧))
lemma-1-forward p n εp≈∞⟦n⟧ = ¬T[p⟦n⟧] , i<n⇒Tp⟦i⟧
  where
  ∀i→≤-all[p∘⟦⟧,i]≡⟦n⟧Ci : ∀ i → ≤-all (λ m → p ⟦ m ⟧) i ≡ ⟦ n ⟧C i
  ∀i→≤-all[p∘⟦⟧,i]≡⟦n⟧Ci = εp≈∞⟦n⟧

  i<n⇒Tp⟦i⟧ : ∀ i → i < n → T (p ⟦ i ⟧)
  i<n⇒Tp⟦i⟧ i i<n = ≤-all-extract (p ∘′ ⟦_⟧) i T[≤-all[p∘⟦⟧,i]]
    where
    ⟦n⟧Ci≡true : ⟦ n ⟧C i ≡ true
    ⟦n⟧Ci≡true = T-to-≡ (<-to-T-⟦⟧C i<n)

    ≤-all[p∘⟦⟧,i]≡true : ≤-all (λ m → p ⟦ m ⟧) i ≡ true
    ≤-all[p∘⟦⟧,i]≡true = trans (∀i→≤-all[p∘⟦⟧,i]≡⟦n⟧Ci i) ⟦n⟧Ci≡true

    T[≤-all[p∘⟦⟧,i]] : T (≤-all (λ m → p ⟦ m ⟧) i)
    T[≤-all[p∘⟦⟧,i]] = ≡-to-T ≤-all[p∘⟦⟧,i]≡true

  ¬T[p⟦n⟧] : ¬ T (p ⟦ n ⟧)
  ¬T[p⟦n⟧] = contraposition (subst (T ∘′ p ∘′ ⟦_⟧) (sym m≡n)) ¬T[p⟦m⟧]
    where
    ⟦n⟧Cn≡false : ⟦ n ⟧C n ≡ false
    ⟦n⟧Cn≡false = not-injective (T-to-≡ (T-¬-not (contraposition T-⟦⟧C-to-< (n≮n n))))

    ≤-all[p∘⟦⟧,n]≡false : ≤-all (λ m → p ⟦ m ⟧) n ≡ false
    ≤-all[p∘⟦⟧,n]≡false = trans (∀i→≤-all[p∘⟦⟧,i]≡⟦n⟧Ci n) ⟦n⟧Cn≡false

    ¬T-≤-all[p∘⟦⟧,n] : ¬ T (≤-all (λ m → p ⟦ m ⟧) n)
    ¬T-≤-all[p∘⟦⟧,n] = T-not-¬ (≡-to-T (cong not ≤-all[p∘⟦⟧,n]≡false))

    ∃m→m≤n×¬T[p⟦m⟧] : ∃ λ m → m ≤ n × ¬ T (p ⟦ m ⟧)
    ∃m→m≤n×¬T[p⟦m⟧] = ¬T-≤-all-to-≤ (p ∘′ ⟦_⟧) n ¬T-≤-all[p∘⟦⟧,n]

    m : ℕ
    m = proj₁ ∃m→m≤n×¬T[p⟦m⟧]

    m≤n : m ≤ n
    m≤n = proj₁ (proj₂ ∃m→m≤n×¬T[p⟦m⟧])

    ¬T[p⟦m⟧] : ¬ T (p ⟦ m ⟧)
    ¬T[p⟦m⟧] = proj₂ (proj₂ ∃m→m≤n×¬T[p⟦m⟧])

    m≮n : m ≮ n
    m≮n m<n = ¬T[p⟦m⟧] (i<n⇒Tp⟦i⟧ m m<n)

    m≡n : m ≡ n
    m≡n = ≤-antisym m≤n (≮⇒≥ m≮n)

lemma-1-backwards : ∀ (p : ℕ∞ → Bool) n →
                    ¬ T (p ⟦ n ⟧) × (∀ k → k < n → T (p ⟦ k ⟧)) →
                    ε p ≈∞ ⟦ n ⟧
lemma-1-backwards p n (¬Tp⟦n⟧ , ∀k→k<n→Tp⟦k⟧) = ∀i→≤-all[p∘⟦⟧,i]≡⟦n⟧Ci
  where
  open ≡-Reasoning

  ∀i→≤-all[p∘⟦⟧,i]≡⟦n⟧Ci : ∀ i → ≤-all (λ m → p ⟦ m ⟧) i ≡ ⟦ n ⟧C i
  ∀i→≤-all[p∘⟦⟧,i]≡⟦n⟧Ci i with n ≤? i
  ... | yes n≤i = trans (not-injective (T-to-≡ (T-¬-not ¬T≤-all[p∘⟦⟧,i])))
                        (sym ⟦n⟧Ci≡false)
    where
    ⟦n⟧Ci≡false : ⟦ n ⟧C i ≡ false
    ⟦n⟧Ci≡false = not-injective (T-to-≡ (T-¬-not (contraposition T-⟦⟧C-to-< (≤⇒≯ n≤i))))

    ¬T≤-all[p∘⟦⟧,i] : ¬ T (≤-all (λ m → p ⟦ m ⟧) i)
    ¬T≤-all[p∘⟦⟧,i] t = ¬Tp⟦n⟧ (≤-all-extract-by-≤ (p ∘′ ⟦_⟧) n≤i t)
  ... | no  n≰i = begin
    ≤-all (λ m → p ⟦ m ⟧) i
      ≡⟨ T-to-≡ (≤-all-construct (p ∘ ⟦_⟧) i
                λ k k≤i → ∀k→k<n→Tp⟦k⟧ k (<-transʳ k≤i i<n)) ⟩
    true
     ≡⟨ sym $ T-to-≡ (<-to-T-⟦⟧C i<n) ⟩
    ⟦ n ⟧C i
     ∎
    where i<n = ≰⇒> n≰i

{-
pp : ℕ∞ → Bool
pp (x , _) = not (x 0) ∨ (x 0 ∧ not (x 1))
-}

ε-correct : (P : ℕ∞ → Bool) → P (ε P) ≡ true → ∀ x → P x ≡ true
ε-correct P P[εP]≡true x = {!   !}

searchable-Bool : Searchable-Bool ℕ∞
searchable-Bool = ε , ε-correct


text:
-- Some very simple problems just to test that things work properly.
-- If everything has been installed properly following
--
-- https://github.com/HoTT/EPIT-2020/tree/main/04-cubical-type-theory#installation-of-cubical-agda-and-agdacubical
--
-- then this file should load fine and one should get 4 holes which
-- one can fill with appropriate terms. Everything should work with
-- both Agda 2.6.1.3 and agda/cubical v0.2 as well as with the
-- development version of both Agda and agda/cubical.
--
-- Solution how to fill the holes is written at the bottom of the file.
--
{-# OPTIONS --cubical #-}
module Warmup where

open import Part1

variable
  A B C : Type ℓ

-- Cong/ap satisfies a lot of nice equations:

congRefl : (f : A → B) {x : A} → cong f (refl {x = x}) ≡ refl
congRefl f = {!!}

congId : {x y : A} (p : x ≡ y) → cong id p ≡ p
congId p = {!!}

_∘_ : (g : B → C) (f : A → B) → A → C
(g ∘ f) x = g (f x)

congComp : (f : A → B) (g : B → C) {x y : A} (p : x ≡ y) →
           cong (g ∘ f) p ≡ cong g (cong f p)
congComp f g x = {!!}

-- Sym is an involution:

symInv : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p
symInv p = {!!}

-- Solution: replace all holes by refl


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Values for standard evaluation (Def. 3.1 and 3.2, Fig. 4c and 4f).
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type

module Parametric.Denotation.Value
    (Base : Type.Structure)
  where

open import Base.Denotation.Notation

open Type.Structure Base

-- Extension point: Values for base types.
Structure : Set₁
Structure = Base → Set

module Structure (⟦_⟧Base : Structure) where
  -- We provide: Values for arbitrary types.
  ⟦_⟧Type : Type → Set
  ⟦ base ι ⟧Type = ⟦ ι ⟧Base
  ⟦ σ ⇒ τ ⟧Type = ⟦ σ ⟧Type → ⟦ τ ⟧Type

  instance
    -- This means: Overload ⟦_⟧ to mean ⟦_⟧Type.
    meaningOfType : Meaning Type
    meaningOfType = meaning ⟦_⟧Type

  -- We also provide: Environments of such values.
  open import Base.Denotation.Environment Type ⟦_⟧Type public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --safe #-}

module Cubical.Data.FinSet.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)

open import Cubical.HITs.PropositionalTruncation as Prop

open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Data.Bool
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sigma

open import Cubical.Data.Fin.Base renaming (Fin to Finℕ)
open import Cubical.Data.SumFin
open import Cubical.Data.FinSet.Base

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidableEq
open import Cubical.Relation.Nullary.HLevels

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Type ℓ
    B : Type ℓ'

-- operators to more conveniently compose equivalences

module _
  {A : Type ℓ}{B : Type ℓ'}{C : Type ℓ''} where

  infixr 30 _⋆̂_

  _⋆̂_ : ∥ A ≃ B ∥ → ∥ B ≃ C ∥ → ∥ A ≃ C ∥
  _⋆̂_ = Prop.map2 (_⋆_)

module _
  {A : Type ℓ}{B : Type ℓ'} where

  ∣invEquiv∣ : ∥ A ≃ B ∥ → ∥ B ≃ A ∥
  ∣invEquiv∣ = Prop.map invEquiv

-- useful implications

EquivPresIsFinSet : A ≃ B → isFinSet A → isFinSet B
EquivPresIsFinSet e (_ , p) = _ , ∣ invEquiv e ∣ ⋆̂ p

isFinSetFin : {n : ℕ} → isFinSet (Fin n)
isFinSetFin = _ , ∣ idEquiv _ ∣

isFinSetUnit : isFinSet Unit
isFinSetUnit = 1 , ∣ invEquiv Fin1≃Unit ∣

isFinSetBool : isFinSet Bool
isFinSetBool = 2 , ∣ invEquiv SumFin2≃Bool ∣

isFinSet→Discrete : isFinSet A → Discrete A
isFinSet→Discrete h = Prop.rec isPropDiscrete (λ p → EquivPresDiscrete (invEquiv p) discreteFin) (h .snd)

isContr→isFinSet : isContr A → isFinSet A
isContr→isFinSet h = 1 , ∣ isContr→≃Unit* h ⋆ invEquiv Unit≃Unit* ⋆ invEquiv Fin1≃Unit ∣

isDecProp→isFinSet : isProp A → Dec A → isFinSet A
isDecProp→isFinSet h (yes p) = isContr→isFinSet (inhProp→isContr p h)
isDecProp→isFinSet h (no ¬p) = 0 , ∣ uninhabEquiv ¬p (idfun _) ∣

isDec→isFinSet∥∥ : Dec A → isFinSet ∥ A ∥
isDec→isFinSet∥∥ dec = isDecProp→isFinSet isPropPropTrunc (Dec∥∥ dec)

isFinSet→Dec∥∥ : isFinSet A → Dec ∥ A ∥
isFinSet→Dec∥∥ h =
  Prop.rec (isPropDec isPropPropTrunc)
      (λ p → EquivPresDec (propTrunc≃ (invEquiv p)) (Dec∥Fin∥ _)) (h .snd)

isFinProp→Dec : isFinSet A → isProp A → Dec A
isFinProp→Dec p h = subst Dec (propTruncIdempotent h) (isFinSet→Dec∥∥ p)

PeirceLaw∥∥ : isFinSet A → NonEmpty ∥ A ∥ → ∥ A ∥
PeirceLaw∥∥ p = Dec→Stable (isFinSet→Dec∥∥ p)

PeirceLaw : isFinSet A → NonEmpty A → ∥ A ∥
PeirceLaw p q = PeirceLaw∥∥ p (λ f → q (λ x → f ∣ x ∣))

-- transprot family towards Fin

transpFamily :
    {A : Type ℓ}{B : A → Type ℓ'}
  → ((n , e) : isFinOrd A) → (x : A) → B x ≃ B (invEq e (e .fst x))
transpFamily {B = B} (n , e) x = pathToEquiv (λ i → B (retEq e x (~ i)))

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Groups.Lemmas
open import Groups.Definition
open import Setoids.Orders.Partial.Definition
open import Setoids.Orders.Total.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Modulo.Definition
open import Semirings.Definition
open import Orders.Total.Definition
open import Sequences

-- Note: totality is necessary here. The construction of a base-n expansion fundamentally relies on being able to take floors.

module Rings.Orders.Total.BaseExpansion {a m p : _} {A : Set a} {S : Setoid {a} {m} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S _<_} {pOrderRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pOrderRing) {n : ℕ} (1<n : 1 <N n) where

open Ring R
open Group additiveGroup
open Setoid S
open Equivalence eq
open SetoidPartialOrder pOrder
open TotallyOrderedRing order
open SetoidTotalOrder total
open PartiallyOrderedRing pOrderRing
open import Rings.Lemmas R
open import Rings.Orders.Partial.Lemmas pOrderRing
open import Rings.Orders.Total.Lemmas order
open import Rings.InitialRing R
open import Rings.IntegralDomains.Lemmas

record FloorIs (a : A) (n : ℕ) : Set (m ⊔ p) where
  field
    prBelow : fromN n <= a
    prAbove : a < fromN (succ n)

addOneToFloor : {a : A} {n : ℕ} → FloorIs a n → FloorIs (a + 1R) (succ n)
FloorIs.prBelow (addOneToFloor record { prBelow = (inl x) ; prAbove = prAbove }) = inl (<WellDefined groupIsAbelian reflexive (orderRespectsAddition x 1R))
FloorIs.prBelow (addOneToFloor record { prBelow = (inr x) ; prAbove = prAbove }) = inr (transitive groupIsAbelian (+WellDefined x reflexive))
FloorIs.prAbove (addOneToFloor record { prBelow = x ; prAbove = prAbove }) = <WellDefined reflexive groupIsAbelian (orderRespectsAddition prAbove 1R)

private
  0<n : {x y : A} → (x < y) → 0R < fromN n
  0<n x<y = fromNPreservesOrder (0<1 (anyComparisonImpliesNontrivial x<y)) (lessTransitive (succIsPositive 0) 1<n)

  0<aFromN : {a : A} → (0<a : 0R < a) → 0R < (a * fromN n)
  0<aFromN 0<a = orderRespectsMultiplication 0<a (0<n 0<a)

  floorWellDefinedLemma : {a : A} {n1 n2 : ℕ} → FloorIs a n1 → FloorIs a n2 → n1 <N n2 → False
  floorWellDefinedLemma {a} {n1} {n2} record { prAbove = prAbove1 } record { prBelow = inl prBelow } n1<n2 with TotalOrder.totality ℕTotalOrder (succ n1) n2
  ... | inl (inl n1+1<n2) = irreflexive (<Transitive prAbove1 (<Transitive (fromNPreservesOrder (0<1 (anyComparisonImpliesNontrivial prBelow)) n1+1<n2) prBelow))
  ... | inl (inr n2<n1+1) = noIntegersBetweenXAndSuccX n1 n1<n2 n2<n1+1
  ... | inr refl = irreflexive (<Transitive prAbove1 prBelow)
  floorWellDefinedLemma {a} {n1} {n2} record { prBelow = (inl x) ; prAbove = prAbove1 } record { prBelow = (inr eq) ; prAbove = _ } n1<n2 with TotalOrder.totality ℕTotalOrder (succ n1) n2
  ... | inl (inl n1+1<n2) = irreflexive (<Transitive prAbove1 (<WellDefined reflexive eq (fromNPreservesOrder (0<1 (anyComparisonImpliesNontrivial prAbove1)) n1+1<n2)))
  ... | inl (inr n2<n1+1) = noIntegersBetweenXAndSuccX n1 n1<n2 n2<n1+1
  ... | inr refl = irreflexive (<WellDefined reflexive eq prAbove1)
  floorWellDefinedLemma {a} {n1} {n2} record { prBelow = (inr x) ; prAbove = prAbove1 } record { prBelow = (inr eq) ; prAbove = _ } n1<n2 = lessIrreflexive {n1} (fromNPreservesOrder' (anyComparisonImpliesNontrivial prAbove1) (<WellDefined reflexive (transitive eq (symmetric x)) (fromNPreservesOrder (0<1 (anyComparisonImpliesNontrivial prAbove1)) n1<n2)))

  floorWellDefined : {a : A} {n1 n2 : ℕ} → FloorIs a n1 → FloorIs a n2 → n1 ≡ n2
  floorWellDefined {a} {n1} {n2} record { prBelow = prBelow1 ; prAbove = prAbove1 } record { prBelow = prBelow ; prAbove = prAbove } with TotalOrder.totality ℕTotalOrder n1 n2
  ... | inr x = x
  floorWellDefined {a} {n1} {n2} f1 f2 | inl (inl x) = exFalso (floorWellDefinedLemma f1 f2 x)
  floorWellDefined {a} {n1} {n2} f1 f2 | inl (inr x) = exFalso (floorWellDefinedLemma f2 f1 x)

  floorWellDefined' : {a b : A} {n : ℕ} → (a ∼ b) → FloorIs a n → FloorIs b n
  FloorIs.prBelow (floorWellDefined' {a} {b} {n} a=b record { prBelow = (inl x) ; prAbove = s }) = inl (<WellDefined reflexive a=b x)
  FloorIs.prBelow (floorWellDefined' {a} {b} {n} a=b record { prBelow = (inr x) ; prAbove = s }) = inr (transitive x a=b)
  FloorIs.prAbove (floorWellDefined' {a} {b} {n} a=b record { prBelow = t ; prAbove = s }) = <WellDefined a=b reflexive s

  computeFloor' : {k : ℕ} → (fuel : ℕ) → .(k +N fuel ≡ n) → (a : A) → (0R < a) → .(a < fromN k) → Sg ℕ (FloorIs a)
  computeFloor' {zero} zero pr a 0<a a<f = exFalso (lessIrreflexive (lessTransitive 1<n (le 0 (applyEquality succ (equalityCommutative pr)))))
  computeFloor' {zero} (succ k) pr a 0<a a<f = exFalso (irreflexive (<Transitive 0<a a<f))
  computeFloor' {succ k} n pr a 0<a a<f with totality 1R a
  ... | inl (inr a<1) = 0 , (record { prAbove = <WellDefined reflexive (symmetric identRight) a<1 ; prBelow = inl 0<a })
  ... | inr 1=a = 1 , (record { prAbove = <WellDefined (transitive identRight 1=a) reflexive (fromNPreservesOrder (0<1 (anyComparisonImpliesNontrivial 0<a)) {1} (le 0 refl)) ; prBelow = inr (transitive identRight 1=a) })
  ... | inl (inl 1<a) with computeFloor' {k} (succ n) (transitivity (transitivity (Semiring.commutative ℕSemiring k (succ n)) (applyEquality succ (Semiring.commutative ℕSemiring n k))) pr) (a + inverse 1R) (moveInequality 1<a) (<WellDefined reflexive (transitive groupIsAbelian (transitive +Associative (transitive (+WellDefined invLeft reflexive) identLeft))) (orderRespectsAddition a<f (inverse 1R)))
  ... | N , snd = succ N , floorWellDefined' (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) (addOneToFloor snd)

computeFloor : (a : A) → (0R < a) → .(a < fromN n) → Sg (ℤn n (lessTransitive (succIsPositive 0) 1<n)) (λ z → FloorIs a (ℤn.x z))
computeFloor a 0<a a<n with computeFloor' {n} 0 (Semiring.sumZeroRight ℕSemiring n) a 0<a a<n
... | floor , record { prBelow = inl p ; prAbove = prAbove } = record { x = floor ; xLess = fromNPreservesOrder' (anyComparisonImpliesNontrivial 0<a) (<Transitive p a<n) } , record { prBelow = inl p ; prAbove = prAbove }
... | floor , record { prBelow = inr p ; prAbove = prAbove } = record { x = floor ; xLess = fromNPreservesOrder' (anyComparisonImpliesNontrivial 0<a) (<WellDefined (symmetric p) reflexive a<n) } , record { prBelow = inr p ; prAbove = prAbove }

firstDigit : (a : A) → 0R < a → .(a < 1R) → ℤn n (lessTransitive (succIsPositive 0) 1<n)
firstDigit a 0<a a<1 = underlying (computeFloor (a * fromN n) (orderRespectsMultiplication 0<a (0<n 0<a)) (<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1)))

baseNExpansion : (a : A) → 0R < a → .(a < 1R) → Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n))
Sequence.head (baseNExpansion a 0<a a<1) = firstDigit a 0<a a<1
Sequence.tail (baseNExpansion a 0<a a<1) with computeFloor (a * fromN n) (0<aFromN 0<a) (<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1))
... | record { x = x ; xLess = xLess } , record { prBelow = inl prB ; prAbove = prA } = baseNExpansion ((a * fromN n) + inverse (fromN x)) (moveInequality prB) (<WellDefined reflexive (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition prA (inverse (fromN x))))
... | record { x = x ; xLess = xLess } , record { prBelow = inr prB ; prAbove = prA } = constSequence (record { x = 0 ; xLess = lessTransitive (succIsPositive 0) 1<n })

private
  powerSeq : (i : A) → (start : A) → Sequence A
  Sequence.head (powerSeq i start) = start
  Sequence.tail (powerSeq i start) = powerSeq i (start * i)

  powerSeqInduction : (i : A) (start : A) → (m : ℕ) → (index (powerSeq i start) (succ m)) ∼ i * (index (powerSeq i start) m)
  powerSeqInduction i start zero = *Commutative
  powerSeqInduction i start (succ m) = powerSeqInduction i (start * i) m

  powerSeq' : (i : A) → Sequence A
  powerSeq' i = powerSeq i i

  dot : A → ℤn n (lessTransitive (succIsPositive 0) 1<n) → A
  dot 1/n^i x = fromN (ℤn.x {n} {lessTransitive (succIsPositive 0) 1<n} x) * 1/n^i

  dotWellDefined : {x y : A} {b : ℤn n (lessTransitive (succIsPositive 0) 1<n)} → (x ∼ y) → dot x b ∼ dot y b
  dotWellDefined eq = *WellDefined reflexive eq

  sequenceEntries : (b : A) → (b * fromN n ∼ 1R) → Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n)) → Sequence A
  sequenceEntries 1/n pr1/n s = apply dot (powerSeq' 1/n) s

private
  partialSums' : A → Sequence A → Sequence A
  Sequence.head (partialSums' a seq) = a + Sequence.head seq
  Sequence.tail (partialSums' a seq) = partialSums' (a + Sequence.head seq) (Sequence.tail seq)

  partialSums'WellDefined : (a b : A) → (a ∼ b) → (s : Sequence A) → (m : ℕ) → (index (partialSums' a s) m) ∼ (index (partialSums' b s) m)
  partialSums'WellDefined a b a=b s zero = +WellDefined a=b reflexive
  partialSums'WellDefined a b a=b s (succ m) = partialSums'WellDefined (a + Sequence.head s) (b + Sequence.head s) (+WellDefined a=b reflexive) (Sequence.tail s) m

  partialSums'WellDefined' : (a : A) → (s1 s2 : Sequence A) → (equal : (m : ℕ) → index s1 m ∼ index s2 m) → (m : ℕ) → (index (partialSums' a s1) m) ∼ (index (partialSums' a s2) m)
  partialSums'WellDefined' a s1 s2 equal zero = +WellDefined reflexive (equal 0)
  partialSums'WellDefined' a s1 s2 equal (succ m) = transitive (partialSums'WellDefined (a + Sequence.head s1) (a + Sequence.head s2) (+WellDefined reflexive (equal 0)) _ m) (partialSums'WellDefined' (a + Sequence.head s2) (Sequence.tail s1) (Sequence.tail s2) (λ m → equal (succ m)) m)

  partialSums'Translate : (a b : A) → (s : Sequence A) → (m : ℕ) → (index (partialSums' (a + b) s) m) ∼ (b + index (partialSums' a s) m)
  partialSums'Translate a b s zero = transitive (+WellDefined groupIsAbelian reflexive) (symmetric +Associative)
  partialSums'Translate a b s (succ m) = transitive (partialSums'WellDefined _ _ (transitive (symmetric +Associative) (transitive (+WellDefined reflexive groupIsAbelian) +Associative)) (Sequence.tail s) m) (partialSums'Translate (a + Sequence.head s) b (Sequence.tail s) m)

  powerSeqWellDefined : {a b start1 start2 : A} → (a ∼ b) → (start1 ∼ start2) → (m : ℕ) → (index (powerSeq a start1) m) ∼ (index (powerSeq b start2) m)
  powerSeqWellDefined {a} {b} {s1} {s2} a=b s1=s2 zero = s1=s2
  powerSeqWellDefined {a} {b} {s1} {s2} a=b s1=s2 (succ m) = powerSeqWellDefined a=b (*WellDefined s1=s2 a=b) m

  powerSeqMove : (a start : A) (m : ℕ) → index (powerSeq a (a * start)) m ∼ a * index (powerSeq a start) m
  powerSeqMove a start zero = reflexive
  powerSeqMove a start (succ m) = transitive (powerSeqWellDefined reflexive (transitive *Commutative (*WellDefined reflexive *Commutative)) m) (powerSeqMove _ _ m)

  partialSumsConst : (r s : A) → (m : ℕ) → index (partialSums' r (constSequence s)) m ∼ (r + (s * fromN (succ m)))
  partialSumsConst r s zero = +WellDefined reflexive (transitive (symmetric identIsIdent) (transitive *Commutative (*WellDefined reflexive (symmetric identRight))))
  partialSumsConst r s (succ m) = transitive (partialSumsConst (r + s) s m) (transitive (symmetric +Associative) (+WellDefined reflexive (transitive (+WellDefined (symmetric (transitive *Commutative identIsIdent)) reflexive) (symmetric *DistributesOver+))))

  applyWellDefined : {b : _} {B : Set b} (r1 r2 : Sequence A) (s : Sequence B) → (f : A → B → A) → ({x y : A} {b : B} → (x ∼ y) → f x b ∼ f y b) → ((m : ℕ) → index r1 m ∼ index r2 m) → (m : ℕ) → index (apply f r1 s) m ∼ index (apply f r2 s) m
  applyWellDefined r1 r2 s f wd eq zero = wd (eq 0)
  applyWellDefined r1 r2 s f wd eq (succ m) = applyWellDefined _ _ (Sequence.tail s) f wd (λ n → eq (succ n)) m

partialSums : Sequence A → Sequence A
partialSums = partialSums' 0R

approximations : (b : A) → (b * (fromN n) ∼ 1R) → Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n)) → Sequence A
approximations 1/n pr1/n s = partialSums (sequenceEntries 1/n pr1/n s)

private
  multiplyZeroSequence : (s : Sequence A) (m : ℕ) → index (apply dot s (constSequence (record { x = 0 ; xLess = lessTransitive (succIsPositive 0) 1<n }))) m ∼ 0R
  multiplyZeroSequence s zero = timesZero'
  multiplyZeroSequence s (succ m) = multiplyZeroSequence _ m

  lemma1 : (x y : A) (s : Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n))) → (m : ℕ) → index (apply dot (powerSeq x (y * x)) s) m ∼ x * (index (apply dot (powerSeq x y) s) m)
  lemma1 x y s zero = transitive *Associative *Commutative
  lemma1 x y s (succ m) = lemma1 x (y * x) (Sequence.tail s) m

  lemma2 : (w x y z : A) (s : Sequence (ℤn n (lessTransitive (succIsPositive 0) 1<n))) → (m : ℕ) → (w * index (partialSums' x (apply dot (powerSeq y z) s)) m) ∼ index (partialSums' (w * x) (apply dot (powerSeq y (z * w)) s)) m
  lemma2 x y z w s zero = transitive *DistributesOver+ (+WellDefined reflexive (transitive (transitive (*WellDefined reflexive *Commutative) (transitive *Associative (*WellDefined *Commutative reflexive))) *Commutative))
  lemma2 x y z w s (succ m) = transitive (lemma2 x (y + dot w (Sequence.head s)) z (w * z) (Sequence.tail s) m) (transitive (partialSums'WellDefined _ (_ + dot (w * x) (Sequence.head s)) (transitive *DistributesOver+ (+WellDefined reflexive (transitive *Commutative (symmetric *Associative)))) _ m) (partialSums'WellDefined' _ _ _ (λ n → applyWellDefined (powerSeq z ((w * z) * x)) (powerSeq z ((w * x) * z)) (Sequence.tail s) dot (λ {m} {n} {s} m=n → dotWellDefined {m} {n} {s} m=n) (λ n → powerSeqWellDefined reflexive (transitive (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative)) *Associative) n) n) m))

approximationComesFromBelow : (1/n : A) → (1/nPr : 1/n * (fromN n) ∼ 1R) → (a : A) → (0<a : 0R < a) → (a<1 : a < 1R) → (m : ℕ) → index (approximations 1/n 1/nPr (baseNExpansion a 0<a a<1)) m <= a
approximationComesFromBelow 1/n 1/nPr a 0<a a<1 zero with computeFloor' 0 (Semiring.sumZeroRight ℕSemiring n) (a * fromN n) (0<aFromN 0<a) ((<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1)))
... | x , record { prBelow = inl prBelow ; prAbove = prAbove } = inl (<WellDefined (symmetric identLeft) reflexive (ringCanCancelPositive (0<n prBelow) (<WellDefined (transitive (symmetric identIsIdent) (transitive *Commutative (transitive (*WellDefined reflexive (symmetric 1/nPr)) *Associative))) reflexive prBelow)))
... | x , record { prBelow = inr prBelow ; prAbove = prAbove } = inr (transitive identLeft (transitive (transitive (transitive (transitive (*WellDefined prBelow reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))) (*WellDefined reflexive 1/nPr)) (*Commutative)) identIsIdent))
approximationComesFromBelow 1/n 1/nPr a 0<a a<1 (succ m) with computeFloor' 0 (Semiring.sumZeroRight ℕSemiring n) (a * fromN n) (0<aFromN 0<a) ((<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1)))
... | x , record { prBelow = inr x=an ; prAbove = an<x+1 } = inr (transitive (partialSums'Translate 0G _ _ m) (transitive (+WellDefined (transitive (*WellDefined x=an reflexive) (transitive (symmetric *Associative) (*WellDefined reflexive (transitive *Commutative 1/nPr)))) reflexive) (transitive (+WellDefined (transitive *Commutative identIsIdent) (transitive (partialSums'WellDefined' 0G _ (constSequence 0G) (λ m → transitive (multiplyZeroSequence (powerSeq 1/n (1/n * 1/n)) m) (identityOfIndiscernablesRight _∼_ reflexive (equalityCommutative (indexAndConst 0G m)))) m) (transitive (partialSumsConst _ _ m) (transitive identLeft timesZero')))) identRight)))
... | x , record { prBelow = inl x<an ; prAbove = an<x+1 } with approximationComesFromBelow 1/n 1/nPr ((a * fromN n) + inverse (fromN x)) (moveInequality x<an) (<WellDefined reflexive (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition an<x+1 (inverse (fromN x)))) m
... | inl inter<an = inl (<WellDefined (symmetric (partialSums'Translate 0G (fromN x * 1/n) _ m)) reflexive (<WellDefined (+WellDefined reflexive (symmetric (partialSums'WellDefined 0G (fromN n * 0G) (symmetric timesZero) _ m))) reflexive (ringCanCancelPositive (0<n an<x+1) (<WellDefined (symmetric (transitive *DistributesOver+' (+WellDefined (transitive (symmetric *Associative) (transitive (*WellDefined reflexive 1/nPr) (transitive *Commutative identIsIdent))) (transitive *Commutative (transitive (lemma2 (fromN n) (fromN n * 0G) 1/n (1/n * 1/n) _ m) (transitive (partialSums'WellDefined _ 0G (transitive (*WellDefined reflexive timesZero) timesZero) _ m) (partialSums'WellDefined' 0G _ _ (λ m → applyWellDefined _ _ _ dot (λ {x} {y} {s} → dotWellDefined {x} {y} {s}) (λ m → powerSeqWellDefined {_} {1/n} {_} {1/n} reflexive (transitive (symmetric *Associative) (transitive (transitive *Commutative (*WellDefined 1/nPr reflexive)) identIsIdent)) m) m) m))))))) reflexive (<WellDefined groupIsAbelian (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) (orderRespectsAddition inter<an (fromN x)))))))
... | inr inter=an = inr (transitive (partialSums'Translate 0G (fromN x * 1/n) _ m) (cancelIntDom' (isIntDom λ t → anyComparisonImpliesNontrivial a<1 (symmetric t)) ans λ t → irreflexive (<WellDefined reflexive t (fromNPreservesOrder (0<1 (anyComparisonImpliesNontrivial a<1)) (lessTransitive (succIsPositive 0) 1<n)))))
  where
    ans : (((fromN x * 1/n) + index (partialSums' 0G (apply dot (powerSeq 1/n (1/n * 1/n)) (baseNExpansion ((a * fromN n) + inverse (fromN x)) (moveInequality x<an) (<WellDefined reflexive (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition an<x+1 (inverse (fromN x))))))) m) * fromN n) ∼ a * fromN n
    ans = transitive (transitive *DistributesOver+' (+WellDefined (transitive (symmetric *Associative) (transitive (*WellDefined reflexive 1/nPr) (transitive *Commutative identIsIdent))) *Commutative)) (transitive (+WellDefined reflexive (transitive (lemma2 (fromN n) 0G 1/n (1/n * 1/n) _ m) (transitive (partialSums'WellDefined _ _ timesZero _ m) (partialSums'WellDefined' _ _ _ (λ m → applyWellDefined _ _ _ dot (λ {x} {y} {s} → dotWellDefined {x} {y} {s}) (λ m → powerSeqWellDefined reflexive (transitive (symmetric *Associative) (transitive (*WellDefined reflexive 1/nPr) (transitive *Commutative identIsIdent))) m) m) m)))) (transitive (+WellDefined reflexive inter=an) (transitive groupIsAbelian (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)))))

pow : ℕ → A → A
pow zero x = 1R
pow (succ n) x = x * pow n x

powPos : (m : ℕ) {a : A} → (0R < a) → 0R < pow m a
powPos zero 0<a = 0<1 (anyComparisonImpliesNontrivial 0<a)
powPos (succ m) 0<a = orderRespectsMultiplication 0<a (powPos m 0<a)

approximationIsNear : (1/n : A) → (1/nPr : 1/n * (fromN n) ∼ 1R) → (a : A) → (0<a : 0R < a) → (a<1 : a < 1R) → (m : ℕ) → a < ((index (approximations 1/n 1/nPr (baseNExpansion a 0<a a<1)) m) + pow m 1/n)
approximationIsNear 1/n 1/npr a 0<a a<1 zero with computeFloor' 0 (Semiring.sumZeroRight ℕSemiring n) (a * fromN n) (0<aFromN 0<a) (<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1))
... | x , record { prBelow = inl prBelow ; prAbove = prAbove } = <WellDefined reflexive (transitive (symmetric identLeft) +Associative) (ringCanCancelPositive (0<n prAbove) (<Transitive prAbove (<WellDefined reflexive (transitive (+WellDefined (transitive (*WellDefined reflexive (symmetric 1/npr)) *Associative) (symmetric identIsIdent)) (symmetric *DistributesOver+')) (<WellDefined reflexive (transitive groupIsAbelian (+WellDefined (transitive (symmetric identIsIdent) *Commutative) reflexive)) (orderRespectsAddition (<WellDefined identRight reflexive (fromNPreservesOrder (0<1 (anyComparisonImpliesNontrivial prAbove)) 1<n)) (fromN x))))))
... | x , record { prBelow = inr prBelow ; prAbove = prAbove } = <WellDefined reflexive (symmetric (transitive (symmetric +Associative) identLeft)) (ringCanCancelPositive (0<n prAbove) (<WellDefined prBelow (symmetric (transitive *DistributesOver+' (+WellDefined (transitive (symmetric *Associative) (transitive *Commutative (transitive (*WellDefined 1/npr reflexive) identIsIdent))) identIsIdent))) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (0<n prAbove) (fromN x)))))
approximationIsNear 1/n 1/npr a 0<a a<1 (succ m) with computeFloor' 0 (Semiring.sumZeroRight ℕSemiring n) (a * fromN n) (0<aFromN 0<a) (<WellDefined reflexive identIsIdent (ringCanMultiplyByPositive (0<n 0<a) a<1))
... | x , record { prBelow = inl prBelow ; prAbove = prAbove } = <WellDefined reflexive (+WellDefined (symmetric (partialSums'Translate 0G (fromN x * 1/n) _ m)) reflexive) (ringCanCancelPositive (0<n prAbove) (<WellDefined reflexive (transitive (+WellDefined (transitive (+WellDefined (transitive (transitive (symmetric identIsIdent) (transitive *Commutative (*WellDefined reflexive (symmetric 1/npr))) ) *Associative) *Commutative) (symmetric *DistributesOver+')) (transitive (transitive (transitive (symmetric identIsIdent) (*WellDefined (transitive (symmetric 1/npr) *Commutative) reflexive)) (symmetric *Associative)) *Commutative)) (symmetric *DistributesOver+')) (<WellDefined reflexive (+WellDefined (+WellDefined reflexive (transitive (partialSums'WellDefined' _ _ _ (λ m → applyWellDefined _ _ _ dot (λ {_} {_} {s} → dotWellDefined {_} {_} {s}) (λ m → powerSeqWellDefined reflexive (transitive (transitive (transitive (symmetric identIsIdent) *Commutative) (*WellDefined reflexive (symmetric 1/npr))) *Associative) m) m) m) (symmetric (lemma2 (fromN n) 0G 1/n (1/n * 1/n) _ m)))) reflexive) (<WellDefined reflexive (+WellDefined (+WellDefined reflexive (partialSums'WellDefined _ _ (symmetric timesZero) _ m)) reflexive) (<WellDefined reflexive +Associative u)))))
  where
    t : ((a * fromN n) + inverse (fromN x)) < ((index (partialSums' 0R (apply dot (powerSeq 1/n 1/n) (baseNExpansion ((a * fromN n) + inverse (fromN x)) (moveInequality prBelow) _))) m) + pow m 1/n)
    t = approximationIsNear 1/n 1/npr ((a * fromN n) + inverse (fromN x)) (moveInequality prBelow) (<WellDefined reflexive (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invRight)) identRight) (orderRespectsAddition prAbove (inverse (fromN x)))) m
    u : (a * fromN n) < (fromN x + ((index (partialSums' 0R (apply dot (powerSeq 1/n 1/n) (baseNExpansion ((a * fromN n) + inverse (fromN x)) (moveInequality prBelow) _))) m) + pow m 1/n))
    u = <WellDefined (transitive (transitive (symmetric +Associative) (+WellDefined reflexive invLeft)) identRight) groupIsAbelian (orderRespectsAddition t (fromN x))
... | x , record { prBelow = inr prBelow ; prAbove = prAbove } = <WellDefined reflexive (+WellDefined (symmetric (partialSums'Translate 0G (fromN x * 1/n) _ m)) reflexive) (ringCanCancelPositive (0<n prAbove) (<WellDefined reflexive (transitive (+WellDefined (transitive (+WellDefined (transitive (transitive (symmetric identIsIdent) (transitive *Commutative (*WellDefined reflexive (symmetric 1/npr))) ) *Associative) *Commutative) (symmetric *DistributesOver+')) (transitive (transitive (transitive (symmetric identIsIdent) (*WellDefined (transitive (symmetric 1/npr) *Commutative) reflexive)) (symmetric *Associative)) *Commutative)) (symmetric *DistributesOver+')) (<WellDefined reflexive (+WellDefined (+WellDefined reflexive (transitive (partialSums'WellDefined' _ _ _ (λ m → applyWellDefined _ _ _ dot (λ {_} {_} {s} → dotWellDefined {_} {_} {s}) (λ m → powerSeqWellDefined reflexive (transitive (transitive (transitive (symmetric identIsIdent) *Commutative) (*WellDefined reflexive (symmetric 1/npr))) *Associative) m) m) m) (symmetric (lemma2 (fromN n) 0G 1/n (1/n * 1/n) _ m)))) reflexive) (<WellDefined reflexive (+WellDefined (+WellDefined reflexive (partialSums'WellDefined _ _ (symmetric timesZero) _ m)) reflexive) (<WellDefined reflexive +Associative (<WellDefined (transitive identLeft prBelow) groupIsAbelian (orderRespectsAddition (<WellDefined reflexive (transitive (symmetric identLeft) (+WellDefined (symmetric (transitive (partialSums'WellDefined' 0R _ (constSequence 0R) (λ m → transitive (multiplyZeroSequence _ m) (identityOfIndiscernablesLeft _∼_ reflexive (indexAndConst 0G m))) m ) (transitive (partialSumsConst _ _ m) (transitive identLeft timesZero')))) reflexive)) (powPos m {1/n} (reciprocalPositive _ _ (0<n 0<a) (transitive *Commutative 1/npr)))) (fromN x))))))))