text:
module Thesis.DeriveCorrect where

open import Thesis.Lang
open import Thesis.Changes
open import Thesis.LangChanges
open import Thesis.Derive

open import Relation.Binary.PropositionalEquality

open import Theorem.Groups-Nehemiah

fromtoDeriveConst : ∀ {τ : Type} (c : Const τ) →
  ch ⟦ c ⟧ΔConst from ⟦ c ⟧Const to ⟦ c ⟧Const
fromtoDeriveConst unit = tt
fromtoDeriveConst (lit n) = right-id-int n
fromtoDeriveConst plus da a1 a2 daa db b1 b2 dbb rewrite sym daa | sym dbb = sym (mn·pq=mp·nq {a1} {da} {b1} {db})
fromtoDeriveConst minus da a1 a2 daa db b1 b2 dbb rewrite sym daa | sym dbb | sym (-m·-n=-mn {b1} {db}) = sym (mn·pq=mp·nq {a1} {da} { - b1} { - db})
fromtoDeriveConst cons da a1 a2 daa db b1 b2 dbb = daa , dbb
fromtoDeriveConst fst (da , db) (a1 , b1) (a2 , b2) (daa , dbb) = daa
fromtoDeriveConst snd (da , db) (a1 , b1) (a2 , b2) (daa , dbb) = dbb
fromtoDeriveConst linj da a1 a2 daa = sft₁ daa
fromtoDeriveConst rinj db b1 b2 dbb = sft₂ dbb
fromtoDeriveConst match .(inj₁ (inj₁ _)) .(inj₁ _) .(inj₁ _) (sft₁ daa) df f1 f2 dff dg g1 g2 dgg = dff _ _ _ daa
fromtoDeriveConst match .(inj₁ (inj₂ _)) .(inj₂ _) .(inj₂ _) (sft₂ dbb) df f1 f2 dff dg g1 g2 dgg = dgg _ _ _ dbb
fromtoDeriveConst match .(inj₂ (inj₂ b2)) .(inj₁ a1) .(inj₂ b2) (sftrp (inj₁ a1) (inj₂ b2)) df f1 f2 dff dg g1 g2 dgg
 rewrite changeMatchSem-lem1 f1 df g1 dg a1 b2
 | sym (fromto→⊕ dg g1 g2 dgg)
 = ⊝-fromto (f1 a1) ((g1 ⊕ dg) b2)
fromtoDeriveConst match .(inj₂ (inj₁ a2)) .(inj₂ b1) .(inj₁ a2) (sftrp (inj₂ b1) (inj₁ a2)) df f1 f2 dff dg g1 g2 dgg
  rewrite changeMatchSem-lem2 f1 df g1 dg b1 a2
  | sym (fromto→⊕ df f1 f2 dff)
  = ⊝-fromto (g1 b1) ((f1 ⊕ df) a2)
fromtoDeriveConst match .(inj₂ (inj₁ a2)) .(inj₁ a1) .(inj₁ a2) (sftrp (inj₁ a1) (inj₁ a2)) df f1 f2 dff dg g1 g2 dgg
  rewrite changeMatchSem-lem3 f1 df g1 dg a1 a2
  | sym (fromto→⊕ df f1 f2 dff)
  = ⊝-fromto (f1 a1) ((f1 ⊕ df) a2)
fromtoDeriveConst match .(inj₂ (inj₂ b2)) .(inj₂ b1) .(inj₂ b2) (sftrp (inj₂ b1) (inj₂ b2)) df f1 f2 dff dg g1 g2 dgg
  rewrite changeMatchSem-lem4 f1 df g1 dg b1 b2
 | sym (fromto→⊕ dg g1 g2 dgg)
  = ⊝-fromto (g1 b1) ((g1 ⊕ dg) b2)

fromtoDeriveVar : ∀ {Γ τ} → (x : Var Γ τ) →
  ∀ {dρ ρ1 ρ2} → [ Γ ]Γ dρ from ρ1 to ρ2 →
    [ τ ]τ (⟦ x ⟧ΔVar ρ1 dρ) from (⟦ x ⟧Var ρ1) to (⟦ x ⟧Var ρ2)
fromtoDeriveVar this (dvv v• dρρ) = dvv
fromtoDeriveVar (that x) (dvv v• dρρ) = fromtoDeriveVar x dρρ

fromtoDeriveBase : ∀ {Γ} τ → (t : Term Γ τ) →
  ch ⟦ t ⟧ΔTerm from ⟦ t ⟧Term to ⟦ t ⟧Term
fromtoDeriveBase τ (const c) dρ ρ1 ρ2 dρρ rewrite ⟦ c ⟧ΔConst-rewrite ρ1 dρ = fromtoDeriveConst c
fromtoDeriveBase τ (var x) dρ ρ1 ρ2 dρρ = fromtoDeriveVar x dρρ
fromtoDeriveBase τ (app {σ} s t) dρ ρ1 ρ2 dρρ rewrite sym (fit-sound t dρρ) =
  let fromToF = fromtoDeriveBase (σ ⇒ τ) s _ _ _ dρρ
  in let fromToB = fromtoDeriveBase σ t _ _ _ dρρ in fromToF _ _ _ fromToB
fromtoDeriveBase (σ ⇒ τ) (abs t) dρ ρ1 ρ2 dρρ = λ dv v1 v2 dvv →
   fromtoDeriveBase τ t _ _ _ (dvv v• dρρ)
fromtoDerive : ∀ {Γ} τ → (t : Term Γ τ) →
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
    [ τ ]τ (⟦ t ⟧ΔTerm ρ1 dρ) from (⟦ t ⟧Term ρ1) to (⟦ t ⟧Term ρ2)
fromtoDerive τ t dρρ = fromtoDeriveBase τ t _ _ _ dρρ

-- Getting to the original equation 1 from PLDI'14.

correctDeriveOplus : ∀ {Γ} τ → (t : Term Γ τ) →
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
     (⟦ t ⟧Term ρ1) ⊕ (⟦ t ⟧ΔTerm ρ1 dρ) ≡ (⟦ t ⟧Term ρ2)
correctDeriveOplus τ t dρρ = fromto→⊕ _ _ _ (fromtoDerive τ t dρρ)

open import Thesis.LangOps

correctDeriveOplusτ : ∀ {Γ} τ → (t : Term Γ τ)
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
     (⟦ app₂ (oplusτo τ) (fit t) (derive t) ⟧Term dρ) ≡ (⟦ t ⟧Term ρ2)
correctDeriveOplusτ τ t {dρ = dρ} {ρ1 = ρ1} dρρ
  rewrite oplusτ-equiv _ dρ _ (⟦ fit t ⟧Term dρ) (⟦ derive t ⟧Term dρ)
  | sym (fit-sound t dρρ)
  = correctDeriveOplus τ t dρρ

deriveGivesDerivative : ∀ {Γ} σ τ → (f : Term Γ (σ ⇒ τ)) (a : Term Γ σ)→
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
     (⟦ app f a ⟧Term ρ1) ⊕ (⟦ app f a ⟧ΔTerm ρ1 dρ) ≡ (⟦ app f a ⟧Term ρ2)
deriveGivesDerivative σ τ f a dρρ = correctDeriveOplus τ (app f a) dρρ

deriveGivesDerivative₂ : ∀ {Γ} σ τ → (f : Term Γ (σ ⇒ τ)) (a : Term Γ σ) →
  {dρ : ChΓ Γ} {ρ1 ρ2 : ⟦ Γ ⟧Context} → [ Γ ]Γ dρ from ρ1 to ρ2 →
     (⟦ app₂ (oplusτo τ) (fit (app f a)) (app₂ (derive f) (fit a) (derive a)) ⟧Term dρ) ≡ (⟦ app f a ⟧Term ρ2)
deriveGivesDerivative₂ σ τ f a dρρ = correctDeriveOplusτ τ (app f a) dρρ

-- Proof of the original equation 1 from PLDI'14. The original was restricted to
-- closed terms. This is a generalization, because it holds also for open terms,
-- *as long as* the environment change is a nil change.
eq1 : ∀ {Γ} σ τ →
  {nilρ : ChΓ Γ} {ρ : ⟦ Γ ⟧Context} → [ Γ ]Γ nilρ from ρ to ρ →
  ∀ (f : Term Γ (σ ⇒ τ)) (a : Term Γ σ) (da : Term (ΔΓ Γ) (Δt σ)) →
  (daa : [ σ ]τ (⟦ da ⟧Term nilρ) from (⟦ a ⟧Term ρ) to (⟦ a ⟧Term ρ ⊕ ⟦ da ⟧Term nilρ)) →
    ⟦ app₂ (oplusτo τ) (fit (app f a)) (app₂ (derive f) (fit a) da) ⟧Term nilρ ≡ ⟦ app (fit f) (app₂ (oplusτo σ) (fit a) da) ⟧Term nilρ
eq1 σ τ {nilρ} {ρ} dρρ f a da daa
  rewrite
    oplusτ-equiv _ nilρ _ (⟦ fit (app f a) ⟧Term nilρ) (⟦ (app₂ (derive f) (fit a) da) ⟧Term nilρ)
  | sym (fit-sound f dρρ)
  | oplusτ-equiv _ nilρ _ (⟦ fit a ⟧Term nilρ) (⟦ da ⟧Term nilρ)
  | sym (fit-sound a dρρ)
  = fromto→⊕ (⟦ f ⟧ΔTerm ρ nilρ (⟦ a ⟧Term ρ) (⟦ da ⟧Term nilρ)) _ _
    (fromtoDerive _ f dρρ (⟦ da ⟧Term nilρ) (⟦ a ⟧Term ρ)
      (⟦ a ⟧Term ρ ⊕ ⟦ da ⟧Term nilρ) daa)

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:
module Logic.Convenience {ℓ} where

import      Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Logic.Propositional{ℓ}
open import Type

record [⇒]-proof (Proof : Stmt → Stmt → Type{ℓ}) : Type{Lvl.𝐒(ℓ)} where
  infixl 10 _⇒_
  infixr 10 _⇐_

  field
    _⇒_ : ∀{X Y : Stmt} → X → Proof(X)(Y) → Y

  _⇐_ : ∀{X Y : Stmt} → Proof(X)(Y) → X → Y
  _⇐_ = swap(_⇒_)
open [⇒]-proof ⦃...⦄ public

instance
  [⇒]-proof-[→] : [⇒]-proof (X ↦ Y ↦ (X → Y))
  _⇒_ ⦃ [⇒]-proof-[→] ⦄ = apply

instance
  [⇒]-proof-[↔] : [⇒]-proof (X ↦ Y ↦ (X ↔ Y))
  _⇒_ ⦃ [⇒]-proof-[↔] ⦄ = swap(Tuple.right)

instance
  [⇒]-proof-unrelated : [⇒]-proof (X ↦ Y ↦ Y)
  _⇒_ ⦃ [⇒]-proof-unrelated ⦄ = swap(const)

-- TODO: ⇔ probably means using transitivity

ext: agda

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:
-- Andreas, 2016-05-04, discussion with Ulf
-- Projections should be treated in the same way asonstructors,
-- what parameters concerns

-- {-# OPTIONS -v tc.mod.apply:15  #-}
-- {-# OPTIONS -v tc.term.con:50 -v tc.term.def:10 #-}

module _ where

module M (A : Set) where

  data D : Set where
    c : A → D

  record R : Set where
    field f : A
    g = f
  open R public

open module N A = M A

-- After module copy, constructor parameter is still hidden

check : ∀ A → A → D A
check A x = c {A = A} x

pat : ∀ A → D A → Set
pat A (c x) = A

-- Field parameter should be hidden

infer : ∀ A → R A → A
infer A r = f r

-- and skipped on the lhs.

copat : ∀ A (a : A) → R A
f (copat A a) = a

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Control.Monad.Except where

open import Prelude
open import Control.Monad.Zero
open import Control.Monad.Identity
open import Control.Monad.Transformer

record ExceptT {a} (E : Set a) (M : Set a → Set a) (A : Set a) : Set a where
  no-eta-equality
  constructor maybeT
  field runExceptT : M (Either E A)

open ExceptT public

module _ {a} {E : Set a} {M : Set a → Set a} where

  instance
    FunctorExceptT : {{_ : Functor M}} → Functor {a = a} (ExceptT E M)
    runExceptT (fmap {{FunctorExceptT}} f m) = fmap f <$> runExceptT m

    FunctorZeroExceptT : {{_ : Monad M}} {{_ : Monoid E}} → FunctorZero {a = a} (ExceptT E M)
    runExceptT (empty {{FunctorZeroExceptT}}) = return (left mempty)

    AlternativeExceptT : {{_ : Monad M}} {{_ : Monoid E}} → Alternative {a = a} (ExceptT E M)
    runExceptT (_<|>_ {{AlternativeExceptT {{monadM}}}} mx my) = do
      right x ← runExceptT mx
        where
          left e₁ → do
            right y ← runExceptT my
              where left e₂ → return (left (e₁ <> e₂))
            return (right y)
      return (right x)

  module _ {{_ : Monad M}} where

    private
      bindExceptT : ∀ {A B} → ExceptT E M A → (A → ExceptT E M B) → ExceptT E M B
      runExceptT (bindExceptT m f) = do
        right x ← runExceptT m
          where left e → return (left e)
        runExceptT (f x)

    instance
      ApplicativeExceptT : Applicative {a = a} (ExceptT E M)
      runExceptT (pure {{ApplicativeExceptT}} x) = pure (right x)
      _<*>_ {{ApplicativeExceptT}} = monadAp bindExceptT

      MonadExceptT : Monad {a = a} (ExceptT E M)
      _>>=_  {{MonadExceptT}} = bindExceptT

    liftExceptT : {A : Set a} → M A → ExceptT E M A
    runExceptT (liftExceptT m) = right <$> m

instance
  TransformerExceptT : ∀ {a} {E : Set a} → Transformer {a} (ExceptT E)
  lift {{TransformerExceptT}} = liftExceptT

Except : ∀ {a} (E : Set a) (A : Set a) → Set a
Except R = ExceptT R Identity

runExcept : ∀ {a} {E : Set a} {A : Set a} → Except E A → Either E A
runExcept m = runIdentity (runExceptT m)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
module type-level where

open import bool
open import level
open import nat

{- multiApply{n} applies a sequence f1, f2, ..., f_n of functions
   to a starting point a:

   multiApply{n} a f1 f2 ... f_n = f_n (... (f2 (f1 a)))
-}

multiApplyTh : ℕ → Set → Set lone
multiApplyTh 0 A = Lift A
multiApplyTh (suc n) A = ∀{B : Set} → (A → B) → multiApplyTh n B

multiApplyT : ℕ → Set lone
multiApplyT n = ∀{A : Set} → A → multiApplyTh n A

multiApply-testT = multiApplyT 2

multiApplyh : {A : Set}{n : ℕ} → A → multiApplyTh n A
multiApplyh {n = zero} a = lift a
multiApplyh {n = suc n} a f = multiApplyh{n = n} (f a)

multiApply : {n : ℕ} → multiApplyT n
multiApply{n} = λ{A : Set}(a : A) → multiApplyh{A}{n} a

multiApply-test1 : Lift 𝔹
multiApply-test1 = multiApply{3} 3 (_+_ 3) is-even ~_

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
module Oscar.Category.Monoid where

open import Oscar.Level

record Monoid 𝔬 𝔪 𝔮 : Set (lsuc (𝔬 ⊔ 𝔪 ⊔ 𝔮)) where


text:
module Numeral.Integer.Oper where

open import Numeral.Natural      as ℕ using (ℕ)
import      Numeral.Natural.Oper as ℕ
open import Numeral.Integer
open import Numeral.Integer.Sign
import      Numeral.Sign       as Sign
import      Numeral.Sign.Oper0 as Sign

-- Unclosed total subtraction from natural numbers to integers
_−ₙ_ : ℕ → ℕ → ℤ
x      −ₙ ℕ.𝟎    = ℤ.+ₙ x
ℕ.𝟎    −ₙ ℕ.𝐒(x) = ℤ.−𝐒ₙ(x)
ℕ.𝐒(x) −ₙ ℕ.𝐒(y) = x −ₙ y

-- Construction of an integer with the sign and numeral components
signed : (Sign.+|−) → ℕ → ℤ
signed (Sign.➕) (n) = +ₙ n
signed (Sign.➖) (n) = −ₙ n

signed0 : (Sign.+|0|−) → ℕ → ℤ
signed0(Sign.➕) (ℕ.𝐒(n)) = +𝐒ₙ(n)
signed0(Sign.➖) (ℕ.𝐒(n)) = −𝐒ₙ(n)
{-# CATCHALL #-}
signed0(_)      (_)      = 𝟎

------------------------------------------
-- Unary operations

-- Predecessor
𝐏 : ℤ → ℤ
𝐏(+𝐒ₙ(n)) = +ₙ n
𝐏(𝟎)      = −𝐒ₙ(ℕ.𝟎)
𝐏(−𝐒ₙ(n)) = −𝐒ₙ(ℕ.𝐒(n))

-- Successor
𝐒 : ℤ → ℤ
𝐒(+ₙ n)        = +ₙ ℕ.𝐒(n)
𝐒(−𝐒ₙ(ℕ.𝟎))    = +ₙ ℕ.𝟎
𝐒(−𝐒ₙ(ℕ.𝐒(n))) = −𝐒ₙ(n)

-- Identity
+_ : ℤ → ℤ
+ n = n

-- Negation
−_ : ℤ → ℤ
− 𝟎 = 𝟎
− (+𝐒ₙ(n)) = −𝐒ₙ(n)
− (−𝐒ₙ(n)) = +𝐒ₙ(n)

-- Absolute value
abs : ℤ → ℤ
abs(+ₙ x)  = +ₙ x
abs(−𝐒ₙ x) = +𝐒ₙ x

------------------------------------------
-- Binary operations

infixl 10010 _+_
infixl 10020 _⋅_

-- Addition
_+_ : ℤ → ℤ → ℤ
(+ₙ  x) + (+ₙ  y) = +ₙ (x ℕ.+ y)
(−𝐒ₙ x) + (−𝐒ₙ y) = −𝐒ₙ(ℕ.𝐒(x ℕ.+ y))
(+ₙ  x) + (−𝐒ₙ y) = x −ₙ ℕ.𝐒(y)
(−𝐒ₙ x) + (+ₙ  y) = (+ₙ y) + (−𝐒ₙ x)

-- Subtraction
_−_ : ℤ → ℤ → ℤ
x − y = x + (− y)

-- Multiplication
_⋅_ : ℤ → ℤ → ℤ
x ⋅ y = signed0 ((sign0 x) Sign.⨯ (sign0 y)) ((absₙ x) ℕ.⋅ (absₙ y))

-- Distance
_𝄩_ : ℤ → ℤ → ℕ
(+ₙ  x)     𝄩 (+ₙ  y)     = x ℕ.𝄩 y
(−𝐒ₙ x)     𝄩 (−𝐒ₙ y)     = x ℕ.𝄩 y
(+ₙ(ℕ.𝟎))   𝄩 (−𝐒ₙ y)     = ℕ.𝐒(y)
(+ₙ(ℕ.𝐒 x)) 𝄩 (−𝐒ₙ y)     = ℕ.𝐒((+ₙ x) 𝄩 (−𝐒ₙ y))
(−𝐒ₙ x)     𝄩 (+ₙ(ℕ.𝟎))   = ℕ.𝐒(x)
(−𝐒ₙ x)     𝄩 (+ₙ(ℕ.𝐒 y)) = ℕ.𝐒((−𝐒ₙ x) 𝄩 (+ₙ y))


text:
------------------------------------------------------------------------
-- A formalisation of some definitions and laws from Section 2.4 of
-- Ralf Hinze's paper "Streams and Unique Fixed Points"
------------------------------------------------------------------------

-- Note: Using the approach of Stream.Programs and Stream.Equality the
-- proofs look just like Hinze's, but they are based on guarded
-- coinduction rather than relying (directly) on universality.

-- Also note that the formalisation can be simplified by defining the
-- streams differently. See Hinze.Simplified.

module Hinze.Section2-4 where

open import Stream.Programs
open import Stream.Equality
open import Stream.Pointwise hiding (⟦_⟧)
open import Hinze.Lemmas

open import Codata.Musical.Notation hiding (∞)
open import Data.Nat
open import Relation.Binary.PropositionalEquality
  renaming (module ≡-Reasoning to ER)
open import Algebra.Structures
import Data.Nat.Properties as Nat
private
  module CS = IsCommutativeSemiring Nat.+-*-isCommutativeSemiring
open import Data.Product

------------------------------------------------------------------------
-- Definitions

nat : Prog ℕ
nat = 0 ≺ ♯ (nat ⟨ _+_ ⟩ 1 ∞)

2*nat : Prog ℕ
2*nat = 2 ∞ ⟨ _*_ ⟩ nat

2*nat+1 : Prog ℕ
2*nat+1 = 2*nat ⟨ _+_ ⟩ 1 ∞

fac : Prog ℕ
fac = 1 ≺ ♯ ((nat ⟨ _+_ ⟩ 1 ∞) ⟨ _*_ ⟩ fac)

fib : Prog ℕ
fib = 0 ≺ ♯ (fib ⟨ _+_ ⟩ (1 ≺ ♯ fib))

bin : Prog ℕ
bin = 0 ≺ ♯ ((2 ∞ ⟨ _*_ ⟩ bin) ⟨ _+_ ⟩ 1 ∞ ⋎
             (2 ∞ ⟨ _*_ ⟩ bin) ⟨ _+_ ⟩ 2 ∞)

------------------------------------------------------------------------
-- Laws and properties

const-is-∞ : ∀ {A} {x : A} {xs} →
             xs ≊ x ≺♯ xs → xs ≊ x ∞
const-is-∞ {x = x} {xs} eq =
  xs
            ≊⟨ eq ⟩
  x ≺♯ xs
            ≊⟨ refl ≺ ♯ const-is-∞ eq ⟩
  x ≺♯ x ∞
            ≡⟨ refl ⟩
  x ∞
            ∎

nat-lemma₁ : 0 ≺♯ 2*nat+1 ⋎ 2*nat ⟨ _+_ ⟩ 2 ∞ ≊ 2*nat ⋎ 2*nat+1
nat-lemma₁ =
  0 ≺♯ 2*nat+1 ⋎ 2*nat ⟨ _+_ ⟩ 2 ∞
                                                ≊⟨ refl ≺ ♯ ⋎-cong 2*nat+1 2*nat+1 (2*nat+1 ∎)
                                                                   (2*nat ⟨ _+_ ⟩ 2 ∞)
                                                                   (2 ∞ ⟨ _*_ ⟩ (nat ⟨ _+_ ⟩ 1 ∞))
                                                                   (lemma (2 ∞) nat) ⟩
  0 ≺♯ 2*nat+1 ⋎ 2 ∞ ⟨ _*_ ⟩ (nat ⟨ _+_ ⟩ 1 ∞)
                                                ≡⟨ refl ⟩
  2*nat ⋎ 2*nat+1
                                                ∎
  where
  lemma : ∀ s t →
          (s ⟨ _*_ ⟩ t) ⟨ _+_ ⟩ s ≊ s ⟨ _*_ ⟩ (t ⟨ _+_ ⟩ 1 ∞)
  lemma = pointwise 2 (λ s t → (s ⟨ _*_ ⟩ t) ⟨ _+_ ⟩ s)
                      (λ s t → s ⟨ _*_ ⟩ (t ⟨ _+_ ⟩ 1 ∞))
                      (λ m n → sym (ER.begin
                         m * (n + 1)
                                        ER.≡⟨ proj₁ CS.distrib m n 1 ⟩
                         m * n + m * 1
                                        ER.≡⟨ cong (_+_ (m * n)) (proj₂ CS.*-identity m) ⟩
                         m * n + m
                                        ER.∎))

nat-lemma₂ : nat ≊ 2*nat ⋎ 2*nat+1
nat-lemma₂ =
  nat
                                      ≡⟨ refl ⟩
  0 ≺♯ nat ⟨ _+_ ⟩ 1 ∞
                                      ≊⟨ refl ≺ ♯ ⟨ _+_ ⟩-cong nat (2*nat ⋎ 2*nat+1) nat-lemma₂
                                                               (1 ∞) (1 ∞) (1 ∞ ∎) ⟩
  0 ≺♯ (2*nat ⋎ 2*nat+1) ⟨ _+_ ⟩ 1 ∞
                                      ≊⟨ refl ≺ ♯ zip-⋎-const _+_ 2*nat 2*nat+1 1 ⟩
  0 ≺♯ 2*nat+1 ⋎ 2*nat+1 ⟨ _+_ ⟩ 1 ∞
                                      ≊⟨ refl ≺ ♯ ⋎-cong 2*nat+1 2*nat+1 (2*nat+1 ∎)
                                                         (2*nat+1 ⟨ _+_ ⟩ 1 ∞)
                                                         (2*nat ⟨ _+_ ⟩ 2 ∞) (lemma 2*nat) ⟩
  0 ≺♯ 2*nat+1 ⋎ 2*nat ⟨ _+_ ⟩ 2 ∞
                                      ≊⟨ nat-lemma₁ ⟩
  2*nat ⋎ 2*nat+1
                                      ∎
  where
  lemma : ∀ s → (s ⟨ _+_ ⟩ 1 ∞) ⟨ _+_ ⟩ 1 ∞ ≊ s ⟨ _+_ ⟩ 2 ∞
  lemma = pointwise 1 (λ s → (s ⟨ _+_ ⟩ 1 ∞) ⟨ _+_ ⟩ 1 ∞)
                      (λ s → s ⟨ _+_ ⟩ 2 ∞)
                      (λ n → CS.+-assoc n 1 1)

nat≊bin : nat ≊ bin
nat≊bin =
  nat
                                        ≊⟨ nat-lemma₂ ⟩
  2*nat ⋎ 2*nat+1
                                        ≊⟨ ≅-sym nat-lemma₁ ⟩
  0 ≺♯ 2*nat+1 ⋎ 2*nat ⟨ _+_ ⟩ 2 ∞
                                        ≊⟨ refl ≺ coih ⟩
  0 ≺♯ (2 ∞ ⟨ _*_ ⟩ bin) ⟨ _+_ ⟩ 1 ∞ ⋎
       (2 ∞ ⟨ _*_ ⟩ bin) ⟨ _+_ ⟩ 2 ∞
                                        ≡⟨ refl ⟩
  bin
                                        ∎
  where
  coih = ♯ ⋎-cong 2*nat+1 ((2 ∞ ⟨ _*_ ⟩ bin) ⟨ _+_ ⟩ 1 ∞)
                  (⟨ _+_ ⟩-cong 2*nat (2 ∞ ⟨ _*_ ⟩ bin)
                                (⟨ _*_ ⟩-cong (2 ∞) (2 ∞) (2 ∞ ∎)
                                              nat bin nat≊bin)
                                (1 ∞) (1 ∞) (1 ∞ ∎))
                  (2*nat ⟨ _+_ ⟩ 2 ∞)
                  ((2 ∞ ⟨ _*_ ⟩ bin) ⟨ _+_ ⟩ 2 ∞)
                  (⟨ _+_ ⟩-cong 2*nat (2 ∞ ⟨ _*_ ⟩ bin)
                                (⟨ _*_ ⟩-cong (2 ∞) (2 ∞) (2 ∞ ∎)
                                              nat bin nat≊bin)
                                (2 ∞) (2 ∞) (2 ∞ ∎))

iterate-fusion
  : ∀ {A B} (h : A → B) (f₁ : A → A) (f₂ : B → B) →
    (∀ x → h (f₁ x) ≡ f₂ (h x)) →
    ∀ x → h · iterate f₁ x ≊ iterate f₂ (h x)
iterate-fusion h f₁ f₂ hyp x =
  h · iterate f₁ x
                                ≡⟨ refl ⟩
  h x ≺♯ h · iterate f₁ (f₁ x)
                                ≊⟨ refl ≺ ♯ iterate-fusion h f₁ f₂ hyp (f₁ x) ⟩
  h x ≺♯ iterate f₂ (h (f₁ x))
                                ≡⟨ cong (λ y → ⟦ h x ≺♯ iterate f₂ y ⟧) (hyp x) ⟩
  h x ≺♯ iterate f₂ (f₂ (h x))
                                ≡⟨ refl ⟩
  iterate f₂ (h x)
                                ∎

nat-iterate : nat ≊ iterate suc 0
nat-iterate =
  nat
                            ≡⟨ refl ⟩
  0 ≺♯ nat ⟨ _+_ ⟩ 1 ∞
                            ≊⟨ refl ≺ ♯ pointwise 1 (λ s → s ⟨ _+_ ⟩ 1 ∞) (_·_ suc)
                                                    (λ x → CS.+-comm x 1) nat ⟩
  0 ≺♯ suc · nat
                            ≊⟨ refl ≺ ♯ ·-cong suc nat (iterate suc 0) nat-iterate ⟩
  0 ≺♯ suc · iterate suc 0
                            ≊⟨ refl ≺ ♯ iterate-fusion suc suc suc (λ _ → refl) 0 ⟩
  0 ≺♯ iterate suc 1
                            ≡⟨ refl ⟩
  iterate suc 0
                            ∎

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax Monad | M

type
  T : 1-ary

term
  ret  : α  ->  T α
  bind : T α  α.(T β)  ->  T β | _>>=_ r10

theory
  (LU) a : α   b : α.(T β) |> bind (ret(a), x. b[x]) =  b[a]
  (RU) t : T α |> bind (t, x. ret(x)) = t
  (AS) t : T α  b : α.(T β)  c : β.(T γ) |> bind (bind (t, x.b[x]), y.c[y]) = bind (t, x. bind (b[x], y.c[y]))
-}

module Monad.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Monad.Signature
open import Monad.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution M:Syn
open import SOAS.Metatheory.SecondOrder.Equality M:Syn

private
  variable
    α β γ τ : MT
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ M) α Γ → (𝔐 ▷ M) α Γ → Set where
  LU : ⁅ α ⁆ ⁅ α ⊩ T β ⁆̣               ▹ ∅ ⊢         (ret 𝔞) >>= 𝔟⟨ x₀ ⟩ ≋ₐ 𝔟⟨ 𝔞 ⟩
  RU : ⁅ T α ⁆̣                         ▹ ∅ ⊢              𝔞 >>= (ret x₀) ≋ₐ 𝔞
  AS : ⁅ T α ⁆ ⁅ α ⊩ T β ⁆ ⁅ β ⊩ T γ ⁆̣ ▹ ∅ ⊢ (𝔞 >>= 𝔟⟨ x₀ ⟩) >>= 𝔠⟨ x₀ ⟩ ≋ₐ 𝔞 >>= (𝔟⟨ x₀ ⟩ >>= 𝔠⟨ x₀ ⟩)

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module PiQ.Opsem where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Relation.Binary.Core
open import Relation.Binary
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import Base
open import PiQ.Syntax

infix  1  _↦_

-- Base combinators
base : ∀ {A B} (c : A ↔ B) → Set
base unite₊l = ⊤
base uniti₊l = ⊤
base swap₊ = ⊤
base assocl₊ = ⊤
base assocr₊ = ⊤
base unite⋆l = ⊤
base uniti⋆l = ⊤
base swap⋆ = ⊤
base assocl⋆ = ⊤
base assocr⋆ = ⊤
base absorbr = ⊤
base factorzl = ⊤
base dist = ⊤
base factor = ⊤
base _ = ⊥

-- Dual combinators
dual : ∀ {A B} (c : A ↔ B) → Set
dual (ηₓ _) = ⊤
dual (εₓ _) = ⊤
dual η₊ = ⊤
dual ε₊ = ⊤
dual _ = ⊥

base-is-prop : ∀ {A B} (c : A ↔ B) → is-prop (base c)
base-is-prop unite₊l tt tt = refl
base-is-prop uniti₊l tt tt = refl
base-is-prop swap₊ tt tt = refl
base-is-prop assocl₊ tt tt = refl
base-is-prop assocr₊ tt tt = refl
base-is-prop unite⋆l tt tt = refl
base-is-prop uniti⋆l tt tt = refl
base-is-prop swap⋆ tt tt = refl
base-is-prop assocl⋆ tt tt = refl
base-is-prop assocr⋆ tt tt = refl
base-is-prop absorbr tt tt = refl
base-is-prop factorzl tt tt = refl
base-is-prop dist tt tt = refl
base-is-prop factor tt tt = refl

-- Evaluator for base combinators
δ : ∀ {A B} (c : A ↔ B) {_ : base c} → ⟦ A ⟧ → ⟦ B ⟧
δ unite₊l (inj₂ v) = v
δ uniti₊l v = inj₂ v
δ swap₊ (inj₁ x) = inj₂ x
δ swap₊ (inj₂ y) = inj₁ y
δ assocl₊ (inj₁ v) = inj₁ (inj₁ v)
δ assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
δ assocl₊ (inj₂ (inj₂ v)) = inj₂ v
δ assocr₊ (inj₁ (inj₁ v)) = inj₁ v
δ assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
δ assocr₊ (inj₂ v) = inj₂ (inj₂ v)
δ unite⋆l (tt , v) = v
δ uniti⋆l v = (tt , v)
δ swap⋆ (x , y) = (y , x)
δ assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
δ assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
δ absorbr ()
δ factorzl ()
δ dist (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
δ dist (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
δ factor (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
δ factor (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)

-- Decidable equality of PiQ values
_≟_ : {t : 𝕌} → Decidable (_≡_ {A = ⟦ t ⟧})
_≟_ {𝟙} tt tt = yes refl
_≟_ {t₁ +ᵤ t₂} (inj₁ x) (inj₁ y) with x ≟ y
... | yes refl = yes refl
... | no  x≠y  = no  (x≠y ∘ λ {refl → refl})
_≟_ {t₁ +ᵤ t₂} (inj₁ x) (inj₂ y) = no (λ ())
_≟_ {t₁ +ᵤ t₂} (inj₂ x) (inj₁ y) = no (λ ())
_≟_ {t₁ +ᵤ t₂} (inj₂ x) (inj₂ y) with x ≟ y
... | yes refl = yes refl
... | no  x≠y  = no  (x≠y ∘ λ {refl → refl})
_≟_ {t₁ ×ᵤ t₂} (x₁ , x₂) (y₁ , y₂) with x₁ ≟ y₁ | x₂ ≟ y₂
... | yes refl | yes refl = yes refl
... | yes refl | no x₂≠y₂ = no  (x₂≠y₂ ∘ cong proj₂)
... | no x₁≠y₁ | yes refl = no  (x₁≠y₁ ∘ cong proj₁)
... | no x₁≠y₁ | no x₂≠y₂ = no  (x₁≠y₁ ∘ cong proj₁)
_≟_ {𝟙/ t} ↻ ↻ = yes refl
_≟_ { - t} (- v₁) (- v₂) with v₁ ≟ v₂
... | yes refl = yes refl
... | no  neq  = no (λ {refl → neq refl})

-- Context
data Context : {A B : 𝕌} → Set where
  ☐ : ∀ {A B} → Context {A} {B}
  ☐⨾_•_ : ∀ {A B C} → (c₂ : B ↔ C) → Context {A} {C} → Context {A} {B}
  _⨾☐•_ : ∀ {A B C} → (c₁ : A ↔ B) → Context {A} {C} → Context {B} {C}
  ☐⊕_•_ : ∀ {A B C D} → (c₂ : C ↔ D) → Context {A +ᵤ C} {B +ᵤ D} → Context {A} {B}
  _⊕☐•_ : ∀ {A B C D} → (c₁ : A ↔ B) → Context {A +ᵤ C} {B +ᵤ D} → Context {C} {D}
  ☐⊗[_,_]•_ : ∀ {A B C D} → (c₂ : C ↔ D) → ⟦ C ⟧ → Context {A ×ᵤ C} {B ×ᵤ D} → Context {A} {B}
  [_,_]⊗☐•_ : ∀ {A B C D} → (c₁ : A ↔ B) → ⟦ B ⟧ → Context {A ×ᵤ C} {B ×ᵤ D} → Context {C} {D}

-- Machine state
data State : Set where
  ⟨_∣_∣_⟩▷ : ∀ {A B} → (c : A ↔ B) → ⟦ A ⟧ → Context {A} {B} → State
  ［_∣_∣_］▷ : ∀ {A B} → (c : A ↔ B) → ⟦ B ⟧ → Context {A} {B} → State
  ⟨_∣_∣_⟩◁ : ∀ {A B} → (c : A ↔ B) → ⟦ A ⟧ → Context {A} {B} → State
  ［_∣_∣_］◁ : ∀ {A B} → (c : A ↔ B) → ⟦ B ⟧ → Context {A} {B} → State
  ⊠ : State

-- Reduction relation
data _↦_ : State → State → Set where
  ↦⃗₁  : ∀ {A B} {c : A ↔ B} {b : base c} {v : ⟦ A ⟧} {κ : Context}
       → ⟨ c ∣ v ∣ κ ⟩▷ ↦ ［ c ∣ δ c {b} v ∣ κ ］▷
  ↦⃗₂  : ∀ {A} {v : ⟦ A ⟧} {κ : Context} → ⟨ id↔ ∣ v ∣ κ ⟩▷ ↦ ［ id↔ ∣ v ∣ κ ］▷
  ↦⃗₃  : ∀ {A B C} {c₁ : A ↔ B} {c₂ : B ↔ C} {v : ⟦ A ⟧} {κ : Context}
       → ⟨ c₁ ⨾ c₂ ∣ v ∣ κ ⟩▷ ↦ ⟨ c₁ ∣ v ∣ ☐⨾ c₂ • κ ⟩▷
  ↦⃗₄  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ A ⟧} {κ : Context}
       → ⟨ c₁ ⊕ c₂ ∣ inj₁ x ∣ κ ⟩▷ ↦ ⟨ c₁ ∣ x ∣ ☐⊕ c₂ • κ ⟩▷
  ↦⃗₅  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {y : ⟦ C ⟧} {κ : Context}
       → ⟨ c₁ ⊕ c₂ ∣ inj₂ y ∣ κ ⟩▷ ↦ ⟨ c₂ ∣ y ∣ c₁ ⊕☐• κ ⟩▷
  ↦⃗₆  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ A ⟧} {y : ⟦ C ⟧} {κ : Context}
       → ⟨ c₁ ⊗ c₂ ∣ (x , y) ∣ κ ⟩▷ ↦ ⟨ c₁ ∣ x ∣ ☐⊗[ c₂ , y ]• κ ⟩▷
  ↦⃗₇  : ∀ {A B C} {c₁ : A ↔ B} {c₂ : B ↔ C} {v : ⟦ B ⟧} {κ : Context}
       → ［ c₁ ∣ v ∣ ☐⨾ c₂ • κ ］▷ ↦ ⟨ c₂ ∣ v ∣ (c₁ ⨾☐• κ) ⟩▷
  ↦⃗₈  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ B ⟧} {y : ⟦ C ⟧} {κ : Context}
       → ［ c₁ ∣ x ∣ ☐⊗[ c₂ , y ]• κ ］▷ ↦ ⟨ c₂ ∣ y ∣ [ c₁ , x ]⊗☐• κ ⟩▷
  ↦⃗₉  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ B ⟧} {y : ⟦ D ⟧} {κ : Context}
       → ［ c₂ ∣ y ∣ [ c₁ , x ]⊗☐• κ ］▷ ↦ ［ c₁ ⊗ c₂ ∣ (x , y) ∣ κ ］▷
  ↦⃗₁₀ : ∀ {A B C} {c₁ : A ↔ B} {c₂ : B ↔ C} {v : ⟦ C ⟧} {κ : Context}
       → ［ c₂ ∣ v ∣ (c₁ ⨾☐• κ) ］▷ ↦ ［ c₁ ⨾ c₂ ∣ v ∣ κ ］▷
  ↦⃗₁₁ : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ B ⟧} {κ : Context}
       → ［ c₁ ∣ x ∣ ☐⊕ c₂ • κ ］▷ ↦ ［ c₁ ⊕ c₂ ∣ inj₁ x ∣ κ ］▷
  ↦⃗₁₂ : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {y : ⟦ D ⟧} {κ : Context}
       → ［ c₂ ∣ y ∣ c₁ ⊕☐• κ ］▷ ↦ ［ c₁ ⊕ c₂ ∣ inj₂ y ∣ κ ］▷
  ↦⃖₁  : ∀ {A B} {c : A ↔ B} {b : base c} {v : ⟦ A ⟧} {κ : Context}
      → ［ c ∣ δ c {b} v ∣ κ ］◁ ↦ ⟨ c ∣ v ∣ κ ⟩◁
  ↦⃖₂  : ∀ {A} {v : ⟦ A ⟧} {κ : Context} → ［ id↔ ∣ v ∣ κ ］◁ ↦ ⟨ id↔ ∣ v ∣ κ ⟩◁
  ↦⃖₃  : ∀ {A B C} {c₁ : A ↔ B} {c₂ : B ↔ C} {v : ⟦ A ⟧} {κ : Context}
      → ⟨ c₁ ∣ v ∣ ☐⨾ c₂ • κ ⟩◁ ↦ ⟨ c₁ ⨾ c₂ ∣ v ∣ κ ⟩◁
  ↦⃖₄  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ A ⟧} {κ : Context}
      → ⟨ c₁ ∣ x ∣ ☐⊕ c₂ • κ ⟩◁ ↦ ⟨ c₁ ⊕ c₂ ∣ inj₁ x ∣ κ ⟩◁
  ↦⃖₅  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {y : ⟦ C ⟧} {κ : Context}
      → ⟨ c₂ ∣ y ∣ c₁ ⊕☐• κ ⟩◁ ↦ ⟨ c₁ ⊕ c₂ ∣ inj₂ y ∣ κ ⟩◁
  ↦⃖₆  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ A ⟧} {y : ⟦ C ⟧} {κ : Context}
      → ⟨ c₁ ∣ x ∣ ☐⊗[ c₂ , y ]• κ ⟩◁ ↦ ⟨ c₁ ⊗ c₂ ∣ (x , y) ∣ κ ⟩◁
  ↦⃖₇  : ∀ {A B C} {c₁ : A ↔ B} {c₂ : B ↔ C} {v : ⟦ B ⟧} {κ : Context}
      → ⟨ c₂ ∣ v ∣ (c₁ ⨾☐• κ) ⟩◁ ↦ ［ c₁ ∣ v ∣ ☐⨾ c₂ • κ ］◁
  ↦⃖₈  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ B ⟧} {y : ⟦ C ⟧} {κ : Context}
      → ⟨ c₂ ∣ y ∣ [ c₁ , x ]⊗☐• κ ⟩◁ ↦ ［ c₁ ∣ x ∣ ☐⊗[ c₂ , y ]• κ ］◁
  ↦⃖₉  : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ B ⟧} {y : ⟦ D ⟧} {κ : Context}
      → ［ c₁ ⊗ c₂ ∣ (x , y) ∣ κ ］◁ ↦ ［ c₂ ∣ y ∣ [ c₁ , x ]⊗☐• κ ］◁
  ↦⃖₁₀ : ∀ {A B C} {c₁ : A ↔ B} {c₂ : B ↔ C} {v : ⟦ C ⟧} {κ : Context}
      → ［ c₁ ⨾ c₂ ∣ v ∣ κ ］◁ ↦ ［ c₂ ∣ v ∣ (c₁ ⨾☐• κ) ］◁
  ↦⃖₁₁ : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {x : ⟦ B ⟧} {κ : Context}
      → ［ c₁ ⊕ c₂ ∣ inj₁ x ∣ κ ］◁ ↦ ［ c₁ ∣ x ∣ ☐⊕ c₂ • κ ］◁
  ↦⃖₁₂ : ∀ {A B C D} {c₁ : A ↔ B} {c₂ : C ↔ D} {y : ⟦ D ⟧} {κ : Context}
      → ［ c₁ ⊕ c₂ ∣ inj₂ y ∣ κ ］◁ ↦ ［ c₂ ∣ y ∣ c₁ ⊕☐• κ ］◁
  ↦η₊₁ : ∀ {A} {v : ⟦ A ⟧} {κ : Context} → ［ η₊ ∣ inj₁ v ∣ κ ］◁ ↦ ［ η₊ ∣ inj₂ (- v) ∣ κ ］▷
  ↦η₊₂ : ∀ {A} {v : ⟦ A ⟧} {κ : Context} → ［ η₊ ∣ inj₂ (- v) ∣ κ ］◁ ↦ ［ η₊ ∣ inj₁ v ∣ κ ］▷
  ↦ε₊₁ : ∀ {A} {v : ⟦ A ⟧} {κ : Context} → ⟨ ε₊ ∣ inj₁ v ∣ κ ⟩▷ ↦ ⟨ ε₊ ∣ inj₂ (- v) ∣ κ ⟩◁
  ↦ε₊₂ : ∀ {A} {v : ⟦ A ⟧} {κ : Context} → ⟨ ε₊ ∣ inj₂ (- v) ∣ κ ⟩▷ ↦ ⟨ ε₊ ∣ inj₁ v ∣ κ ⟩◁
  ↦⃗ηₓ  : ∀ {A} {v : ⟦ A ⟧} {κ : Context} → ⟨ ηₓ v ∣ tt ∣ κ ⟩▷ ↦ ［ ηₓ v ∣ (v , ↻) ∣ κ ］▷
  ↦⃖ηₓ₁ : ∀ {A} {v v' : ⟦ A ⟧} {κ : Context} {eq  : v ≡ v'} → ［ ηₓ v ∣ (v' , ↻) ∣ κ ］◁ ↦ ⟨ ηₓ v ∣ tt ∣ κ ⟩◁
  ↦⃖ηₓ₂ : ∀ {A} {v v' : ⟦ A ⟧} {κ : Context} {neq : v ≢ v'} → ［ ηₓ v ∣ (v' , ↻) ∣ κ ］◁ ↦ ⊠
  ↦⃗εₓ₁ : ∀ {A} {v v' : ⟦ A ⟧} {κ : Context} {eq  : v ≡ v'} → ⟨ εₓ v ∣ (v' , ↻) ∣ κ ⟩▷ ↦ ［ εₓ v ∣ tt ∣ κ ］▷
  ↦⃗εₓ₂ : ∀ {A} {v v' : ⟦ A ⟧} {κ : Context} {neq : v ≢ v'} → ⟨ εₓ v ∣ (v' , ↻) ∣ κ ⟩▷ ↦ ⊠
  ↦⃖εₓ  : ∀ {A} {v : ⟦ A ⟧} {κ : Context} → ［ εₓ v ∣ tt ∣ κ ］◁ ↦ ⟨ εₓ v ∣ (v , ↻) ∣ κ ⟩◁


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.
   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Consensus.Types hiding (getEpoch)
open import Optics.All
import      Util.KVMap                          as Map
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                         using (String)

module LibraBFT.Impl.Storage.DiemDB.LedgerStore.LedgerStore where

record EpochEndingLedgerInfoIter : Set where
  constructor EpochEndingLedgerInfoIter∙new
  field
    _eeliiObmLIWS : List LedgerInfoWithSignatures
open EpochEndingLedgerInfoIter public

new : LedgerStore
new = mkLedgerStore Map.empty Map.empty nothing

-- OBM-LBFT-DIFF : the entire Haskell impl file is VERY different from the Rust code.
-- The Agda below mirrors Haskell.

getEpoch : LedgerStore → Version → Either ErrLog Epoch
getEpoch self version =
  maybeS (Map.lookup version (self ^∙ lsObmVersionToEpoch))
         -- COMMENT FROM RUST CODE:
         -- There should be a genesis LedgerInfo at version 0.
         -- This normally doesn't happen.
         -- This part of impl does not need to rely on this assumption.
         (pure 0)
         pure

getEpochEndingLedgerInfo : LedgerStore → Version → Either ErrLog LedgerInfoWithSignatures
getEpochEndingLedgerInfo self version = do
  epoch ← getEpoch self version
  case Map.lookup epoch (self ^∙ lsObmEpochToLIWS) of λ where
    nothing   → Left fakeErr -- ["DiemDbError::NotFound", "LedgerInfo for epoch", lsE epoch]
    (just li) →
      grd‖ li ^∙ liwsLedgerInfo ∙ liVersion /= version ≔
           Left fakeErr --["epoch did not end at version", lsE epoch, lsVersion version]
         ‖ is-nothing (li ^∙ liwsLedgerInfo ∙ liNextEpochState) ≔
           Left fakeErr -- ["not an epoch change at version", lsVersion version]
         ‖ otherwise≔
           pure li
--where
-- here t = "LedgerStore":"getEpochEndingLedgerInfo":t

getEpochState : LedgerStore → Epoch → Either ErrLog EpochState
getEpochState self epoch = do
  lcheck (epoch >? 0) (here' ("EpochState only queryable for epoch >= 1" {-∷ lsE epoch-} ∷ []))
  case Map.lookup (epoch ∸ 1) (self ^∙ lsObmEpochToLIWS) of λ where
    nothing → Left fakeErr --[ "DiemDbError::NotFound"
                           --, "last LedgerInfo of epoch", lsE (epoch - 1) ]))
    (just ledgerInfoWithSigs) →
      maybeS (ledgerInfoWithSigs ^∙ liwsNextEpochState)
             (Left fakeErr) --[ "last LedgerInfo in epoch must carry nextEpochState"
                            --, lsE epoch, lsLI (ledgerInfoWithSigs^.liwsLedgerInfo) ]
             pure
 where
  here' : List String → List String
  here' t = "LedgerStore" ∷ "getEPochState" ∷ t

-- iterator that yields epoch ending ledger infos
-- starting from `start_epoch`
-- ends at the one before `end_epoch`
getEpochEndingLedgerInfoIter
  : LedgerStore → Epoch → Epoch
  → Either ErrLog EpochEndingLedgerInfoIter
getEpochEndingLedgerInfoIter self startEpoch endEpoch =
  -- TODO-2: prove endEpoch > 0
  -- Use of monus in context where it is not clear that endEpoch > 0.
  -- If not, Agda and Haskell code would behave differently.
  -- TODO-2: IMPL-DIFF: Haskell uses a list comprehension; Agda uses homegrown 'fromToList'
  -- The combination of monus and fromToList risks misunderstanding/misuse of fromToList later.
  -- Ranges would differ in Haskell and Agda if, say, startEpoch were negative and endEpoch was 0.
  -- It could be correct and verified in Agda, but wrong in Haskell
  -- (e.g., if the Haskell code accidentally calculates a negative epoch).
  EpochEndingLedgerInfoIter∙new <$> (foldM) go [] (fromToList startEpoch (endEpoch ∸ 1))
 where
  go : List LedgerInfoWithSignatures → Epoch → Either ErrLog (List LedgerInfoWithSignatures)
  go acc e = maybeS (Map.lookup e (self ^∙ lsObmEpochToLIWS))
                    (Left fakeErr) --[ "LedgerStore", "getEpochEndingLedgerInfoIter"
                                   --, "no LIWS for epoch", lsE e ]
                    (λ x → Right (acc ++ (x ∷ []))) -- TODO

putLedgerInfo : LedgerStore → LedgerInfoWithSignatures → Either ErrLog LedgerStore
putLedgerInfo self ledgerInfoWithSigs =
  let ledgerInfo = ledgerInfoWithSigs ^∙ liwsLedgerInfo
   in pure
    $ mkLedgerStore
      ((if ledgerInfo ^∙ liEndsEpoch
         then Map.insert (ledgerInfo ^∙ liVersion) (ledgerInfo ^∙ liEpoch)
         else identity)
       (self ^∙ lsObmVersionToEpoch))
      (Map.insert (ledgerInfo ^∙ liEpoch) ledgerInfoWithSigs
       (self ^∙ lsObmEpochToLIWS))
      (self ^∙ lsLatestLedgerInfo)

obmEELIICollect : EpochEndingLedgerInfoIter → List LedgerInfoWithSignatures
obmEELIICollect = _eeliiObmLIWS


text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

module SyntheticReals where

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

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Structures.CommRing
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base -- Rel
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
-- open import Cubical.Structures.Poset
open import Cubical.Foundations.Function

open import Function.Base using (_∋_)
-- open import Function.Reasoning using (∋-syntax)
open import Function.Base using (it) -- instance search

open import Utils
open import MoreLogic
open MoreLogic.Reasoning
open MoreLogic.Properties
open import MoreAlgebra
open MoreAlgebra.Definitions
open MoreAlgebra.Consequences
open import Bundles
-- open MoreAlgebra.Properties.Group

-- https://www.cs.bham.ac.uk/~abb538/thesis.pdf
-- Booij 2020 - Analysis in Univalent Type Theory

-- Lemma 4.1.6.
import Properties.ConstructiveField

-- Lemma 4.1.11.
import Properties.AlmostOrderedField

-- Lemma 4.1.12. An ordered field (F, 0, 1, +, · , min, max, <) is a constructive field (F, 0, 1, +, · , #).
lemma-4-1-12 :
  -- NOTE: we do a slightly different thing here
  ∀{ℓ ℓ'} (OF : OrderedField {ℓ} {ℓ'}) →
  let open OrderedField OF
  ----------------------------------------------------
  in (IsConstructiveField 0f 1f _+_ _·_ -_ _#_ _⁻¹ᶠ)
lemma-4-1-12 {ℓ} {ℓ'} OF = let -- NOTE: for mentioning the ℓ and ℓ' and not taking them as new "variables" we bring them into scope
  open OrderedField OF
  in record -- We need to show that + is #-extensional, and that # is tight.
   { OrderedField OF
   ; isApartnessRel  = #'-isApartnessRel <-isStrictPartialOrder -- NOTE: We've proved this before

     -- First, assume w + x # y + z. We need to show w # y ∨ x # z.
   ; +-#-extensional = λ where
                       -- Consider the case w + x < y + z, so that we can use (†) to obtain w < y ∨ x < z,
                       --   which gives w # y ∨ x # z in either case.
                       w x y z (inl w+x<y+z) → case +-<-extensional _ _ _ _ w+x<y+z of (
                         (_ → (w # y) ⊎ (x # z)) ∋ λ -- NOTE: here we had to add a (return-)type annotation to the λ
                         { (inl w<y) → inl (inl w<y)
                         ; (inr x<z) → inr (inl x<z)
                         })
                       -- The case w + x > y + z is similar.
                       w x y z (inr y+z<w+x) → case  +-<-extensional _ _ _ _ y+z<w+x of (
                         (_ → (w # y) ⊎ (x # z)) ∋ λ
                         { (inl y<w) → inl (inr y<w)
                         ; (inr z<x) → inr (inr z<x)
                         })

     -- Tightness follows from the fact that ≤ is antisymmetric, combined with the fact
     --   that ¬(P ∨ Q) is equivalent to ¬P ∧ ¬Q.
   ; #-tight         = λ x y ¬[x<y]⊎¬[y<x] → let (¬[x<y] , ¬[y<x]) = deMorgan₂' ¬[x<y]⊎¬[y<x]
                                             in  ≤-antisym _ _ ¬[y<x] ¬[x<y]
   }

-- We will mainly be concerned with ordered fields, as opposed to the more general con-
-- structive fields. This is because the Archimedean property can be phrased straightforwardly
-- for ordered fields, as in Section 4.3, and because the ordering relation allows us to define loca-
-- tors, as in Chapter 6.
--
-- We have defined ordered fields, which capture the algebraic structure of the real numbers.

-- 4.2 Rationals
-- ...
-- NOTE: we have in cubical
--   import Cubical.HITs.Rationals.HITQ
--     ℚ as a higher inductive type
--   import Cubical.HITs.Rationals.QuoQ
--     ℚ as a set quotient of ℤ × ℕ₊₁ (as in the HoTT book)
--   import Cubical.HITs.Rationals.SigmaQ
--     ℚ as the set of coprime pairs in ℤ × ℕ₊₁

import Cubical.HITs.Rationals.QuoQ renaming (ℚ to ℚ-Carrier)

postulate
  ℚℓ : Level
  ℚOF : OrderedField {ℓ-zero} {ℚℓ}
{-
ℚ = λ where
  .OrderedField.Carrier        → ℚ-Carrier
  .OrderedField.0f             → 0
  .OrderedField.1f             → 1
  .OrderedField._+_            → _+_
  .OrderedField.-_             → -_
  .OrderedField._·_            → _*_
  .OrderedField.min            → {!!}
  .OrderedField.max            → {!!}
  .OrderedField._<_            → {!!}
  .OrderedField.<-isProp       → {!!}
  .OrderedField._⁻¹ᶠ           → {!!}
  .OrderedField.isOrderedField → {!!}
-}

-- 4.3 Archimedean property
--
-- We now define the notion of Archimedean ordered fields. We phrase this in terms of a certain
-- interpolation property, that can be defined from the fact that there is a unique morphism of
-- ordered fields from the rationals to every ordered field.

-- Lemma 4.3.3. For every ordered field (F, 0 F , 1 F , + F , · F , min F , max F , < F ), there is a unique morphism
-- i of ordered fields from the rationals to F . Additionally, i preserves < in the sense that for every q, r : Q
--   q < r ⇒ i (q) < F i (r ).

-- ∃! : ∀ {ℓ ℓ'} (A : Type ℓ) (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
-- ∃! A B = isContr (Σ A B)

-- isContr' A = Σ[ x ∈ A ] (∀ y → x ≡ y)

ℚ-IsInitialObject : ∀(OF : OrderedField {ℓ} {ℓ'}) → isContr (OrderedFieldMor ℚOF OF)
ℚ-IsInitialObject OF = {!!} , {!!}

-- Definition 4.3.5. Let (F, 0 F , 1 F , + F , · F , min F , max F , < F ) be an ordered field, so that we get a
-- canonical morphism i : Q → F of ordered fields, as in Lemma 4.3.3. We say the ordered field
-- (F, 0 F , 1 F , + F , · F , min F , max F , < F ) is Archimedean if
--   (∀x, y : F )(∃q : Q)x < i (q) < y.

IsArchimedian : OrderedField {ℓ} {ℓ'} → Type (ℓ-max ℓ ℓ')
IsArchimedian OF = let (orderedfieldmor i _) = fst (ℚ-IsInitialObject OF)
                       open OrderedField OF
                       ℚ = OrderedField.Carrier ℚOF
                   in ∀ x y → ∃[ q ∈ ℚ ] (x < i q) × (i q < y)

-- If the ordered field is clear from the context, we will identify rationals q : Q with their in-
-- clusion i (q) in the ordered field, so that we may also say that (F, 0 F , 1 F , + F , · F , min F , max F , < F )
-- is Archimedean if
-- (∀x, y : F )(∃q : Q)x < q < y.

-- Example 4.3.6. In an Archimedean ordered field, all numbers are bounded by rationals. That
-- is, for a given x : F , there exist q, r : Q with q < x < r .

Example-4-3-6 : (OF : OrderedField {ℓ} {ℓ'})
              → IsArchimedian OF
              → let open OrderedField OF renaming (Carrier to F)
                    (orderedfieldmor i _) = fst (ℚ-IsInitialObject OF)
                    ℚ = OrderedField.Carrier ℚOF
                in ∀(x : F) → (∃[ q ∈ ℚ ] i q < x) × (∃[ r ∈ ℚ ] x < i r)
-- This follows from applying the Archimedean property to x − 1 < x and x < x + 1.
Example-4-3-6 OF isArchimedian = {!!}

-- 4.4 Cauchy completeness of real numbers
--
-- We focus on Cauchy completeness, rather than Dedekind or Dedekind-MacNeille completeness,
-- as we will focus on the computation of digit expansions, for which Cauchy completeness suffices.

-- In order to state that an ordered field is Cauchy complete, we need to define when sequences
-- are Cauchy, and when a sequence has a limit. We also take the opportunity to define
-- the set of Cauchy reals in Definition 4.4.9. Surprisingly, this ordered field cannot be shown to
-- be Cauchy complete.

-- NOTE: in the following we make use of ℚ⁺ a few times. Maybe this should be a primitive?

-- Fix an ordered field (F, 0 F , 1 F , + F , · F , min F , max F , < F ).
module _ (OF : OrderedField {ℓ} {ℓ'}) where
  open OrderedField OF renaming (Carrier to F)
  -- module ℚ = OrderedField ℚ
  open OrderedField ℚOF using () renaming (_<_ to _<ᵣ_; 0f to 0ᵣ)
  ℚ = OrderedField.Carrier ℚOF
  iᵣ = OrderedFieldMor.fun (fst (ℚ-IsInitialObject OF))
  open import Data.Nat.Base using (ℕ) renaming (_≤_ to _≤ₙ_)

  -- We get a notion of distance, given by the absolute value as
  --   |x − y| := max F (x − y, −(x − y)).

  distance : ∀(x y : F) → F
  distance x y = max (x - y) (- (x - y))

  -- Consider a sequence x : N → F of elements of F . Classically, we may state that x is Cauchy as
  -- (∀ε : Q + )(∃N : N)(∀m, n : N)m, n ≥ N ⇒ |x m − x n | < ε,
  IsCauchy : (x : ℕ → F) → Type (ℓ-max ℓ' ℚℓ)
  IsCauchy x = ∀(ε : ℚ) → 0ᵣ <ᵣ ε → ∃[ N ∈ ℕ ] ∀(m n : ℕ) → N ≤ₙ m → N ≤ₙ n → distance (x m) (x n) < iᵣ ε

  -- We can interpret the quantifiers as in Definition 2.4.5.
  -- NOTE: this is the case, since `∃ A B = ∥ Σ A B ∥`

  -- Following a propositions-as-types interpretation, we may also state that x is Cauchy as the
  -- structure
  -- (Πε : Q + )(ΣN : N)(Πm, n : N)m, n ≥ N → |x m − x n | < ε.

  -- The dependent sum represents a choice of index N for every error ε, and so we have arrived at the following definition.

  -- Definition 4.4.1.
  -- For a sequence of reals x : N → F , a a modulus of Cauchy convergence is a map M : Q + → N such that
  -- (∀ε : Q + )(∀m, n : N)m, n ≥ M (ε) ⇒ |x m − x n | < ε.

  -- NOTE: do we already call these x "reals" ?
  -- NOTE: we are using the Modulus-type `((y : ℚ) → {{0ᵣ <ᵣ y}} → ℕ)` a few times and might abbreviate it

  IsModulusOfCauchyConvergence : (x : ℕ → F) → (M : ((y : ℚ) → {{0ᵣ <ᵣ y}} → ℕ)) → Type (ℓ-max ℓ' ℚℓ)
  IsModulusOfCauchyConvergence x M = ∀(ε : ℚ) → (p : 0ᵣ <ᵣ ε) → ∀(m n : ℕ)
                                   → let instance _ = p
                                     in M ε ≤ₙ m → M ε ≤ₙ n → distance (x m) (x n) < iᵣ ε

  -- In constructive mathematics, we typically use such sequences with modulus, for example,
  -- because they can sometimes be used to compute limits of Cauchy sequences, avoiding choice axioms.

  -- Definition 4.4.2.
  -- A number l : F is the limit of a sequence x : N → F if the sequence
  -- converges to l in the usual sense:
  --   (∀ε : Q + )(∃N : N)(∀n : N)n ≥ N ⇒ |x n − l | < ε.

  IsLimit : (x : ℕ → F) → (l : F) → Type (ℓ-max ℓ' ℚℓ)
  IsLimit x l = ∀(ε : ℚ) → (0ᵣ <ᵣ ε) → ∃[ N ∈ ℕ ] ∀(n : ℕ) → N ≤ₙ n → distance (x n) l < iᵣ ε

  -- Remark 4.4.3. We do not consider the statement of convergence in propositions-as-types
  --
  --   (Πε : Q + )(ΣN : N)(Πn : N)n ≥ N → |x n − l | < ε,
  --
  -- because if the sequence has a modulus of Cauchy convergence M, then λε.M (ε/2) is a
  -- modulus of convergence to the limit l, so that we get an element of the above type.

  -- Definition 4.4.4.
  -- The ordered field (F, 0 F , 1 F , + F , · F , min F , max F , < F ) is said to be Cauchy complete
  -- if for every sequence x with modulus of Cauchy convergence M, we have a limit of x.
  -- In other words, an ordered field is Cauchy complete iff from a sequence–modulus pair (x, M), we can compute a limit of x.

  IsCauchyComplete : Type (ℓ-max (ℓ-max ℓ ℓ') ℚℓ)
  IsCauchyComplete = (x : ℕ → F)
                   → (M : ((y : ℚ) → {{0ᵣ <ᵣ y}} → ℕ))
                   → IsModulusOfCauchyConvergence x M
                   → Σ[ l ∈ F ] IsLimit x l

  -- For the remainder of this section, additionally assume that F is Archimedean.
  module _ (isArchimedian : IsArchimedian OF) where

    -- Lemma 4.4.5.
    -- The type of limits of a fixed sequence x : N → F is a proposition.
    Lemma-4-4-5 : ∀(x : ℕ → F) → isProp (Σ[ l ∈ F ] IsLimit x l)
    -- Proof. This can be shown using the usual proof that limits are unique in Archimedean ordered fields, followed by an application of Lemma 2.6.20.
    Lemma-4-4-5 x = {!!}

    -- Corollary 4.4.6.
    -- Fix a given sequence x : N → F . Suppose that we know that there exists a
    -- limit of the sequence. Then we can compute a limit of the sequence.
    Corollary-4-4-6 : ∀(x : ℕ → F) → (∃[ l ∈ F ] IsLimit x l) → Σ[ l ∈ F ] IsLimit x l
    -- Proof. By applying the induction principle of propositional truncations of Definition 2.4.3.
    Corollary-4-4-6 x p = {!!} , {!!}

    -- Corollary 4.4.7.
    -- Fix a given sequence x : N → F . Suppose that, from a modulus of Cauchy
    -- convergence, we can compute a limit of the sequence. Then from the existence of the modulus of
    -- Cauchy convergence we can compute a limit of the sequence.
    Corollary-4-4-7 : (x : ℕ → F)
                    → ( (M : ((y : ℚ) → {{0ᵣ <ᵣ y}} → ℕ))
                      → (isMCC : IsModulusOfCauchyConvergence x M)
                      → Σ[ l ∈ F ] IsLimit x l
                      )
                    -----------------------------------------------------------------------
                    → ∃[ M ∈ ((y : ℚ) → {{0ᵣ <ᵣ y}} → ℕ) ] IsModulusOfCauchyConvergence x M
                    → Σ[ l ∈ F ] IsLimit x l
    -- Proof. By applying the induction principle of propositional truncations of Definition 2.4.3.
    Corollary-4-4-7 x f p = {!!}

    -- We can thus compute the limit of x : N → F as the number lim(x, p), where p is a proof
    -- that the limit of x exists. We will rather use the more traditional notation lim n→∞ x n for this
    -- number.

    -- Example 4.4.8 (Exponential function).
    -- In a Cauchy complete Archimedean ordered field, we can define an exponential function exp : F → F by
    --
    --    exp(x) = Σ_{k=0}^{∞} (xᵏ) / (k!)
    --
    -- For a given input x, we obtain the existence of a modulus of Cauchy convergence for the output from boundedness of
    -- x, that is, from the fact that (∃q, r : Q) q < x < r .

    exp : F → F
    exp x = {!!}

    Example-4-4-8 : ∀(x : F) → ∃[ M ∈ ((y : ℚ) → {{0ᵣ <ᵣ y}} → ℕ) ] IsModulusOfCauchyConvergence {!!} M
    Example-4-4-8 x with Example-4-3-6 OF isArchimedian x
    ... | q' , r' = let q : ∃[ q ∈ ℚ ] iᵣ q < x
                        q = q'
                        r : ∃[ r ∈ ℚ ] x < iᵣ r
                        r = r'
                    in {!!}

    -- The point of this work is that, because we have a single language for properties and struc-
    -- ture, we can see more precisely what is needed for certain computations. In the above example,
    -- we explicitly do not require that inputs come equipped with a modulus of Cauchy convergence,
    -- but rather that there exists such a modulus. On the one hand, we do need a modulus to obtain
    -- the limit, but as the limit value is independent of the chosen modulus, existence of such a
    -- modulus suffices.

    -- Definition 4.4.9. The Cauchy reals ℝC is the collection of rational sequences equipped with
    -- a modulus of Cauchy convergence, quotiented (as in Section 2.7) by an equivalence relation
    -- that relates two sequence–modulus pairs (x, M) and (y, N ) iff
    -- (∀ε : Q + ) x M (ε/4) − y M (ε/4) < ε.

    ℝC : {!!}
    ℝC = {!!}

    -- The Cauchy reals form an Archimedean ordered field in a natural way. The natural strategy
    -- to prove that the Cauchy reals are Cauchy complete, perhaps surprisingly, does not work, and
    -- in some constructive foundations the Cauchy completeness of the Cauchy reals is known to
    -- be false [68].
    --
    -- ...
    --
    -- An alternative interpretation of the non-completeness of the Cauchy reals is that the sequential
    -- definition of completeness ought to be amended [80].

    -- NOTE: now we're back to https://github.com/agda/cubical/issues/286 ?

-- Auke would send an email to Ayberk Tosun and Martin Escardo
-- I could prepare a PR for the cubical standard library
-- the cubical standard library does not supersede the standard library
--   using setoids need not to be a shortcoming but can be a concious decision
-- Postulating the rationals as an ordered field for which there exists a unique morphism to every other ordered field should be sufficient
--   (we went a little bit into the coprime and quotient construction of the rational numbers)
-- I can prepare some statements that I would like to formalize (with just guessing) to have a more concrete guidance for the necessary detail of a real number formulation
-- the impredicative `--prop` is not equivalent to hProp
--   therefore, one should make props explicit arguments or at least be aware of them at all times

{-

in a world where we "just have" real numbers in Agda, I would do the following:

Adjoint theory
  Vector space
  normed space
  Banach space
  Inner Product space
  unbounded Linear operator
  adjoint linear operator
  orthogonal decomposition of Banach spaces
  inf-sup conditions
  lax-milgram

Local Multilinear Algebra
  euclidean space
  linear representation of hodge star
  locally euclidean

Global Multilinear Algebra
  locally euclidean topological space
  chart representation

-}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


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

-- Enriched category over a Monoidal category V

open import Categories.Category
  using (categoryHelper) renaming (Category to Setoid-Category)
open import Categories.Category.Monoidal using (Monoidal)

module Categories.Enriched.Category {o ℓ e} {V : Setoid-Category o ℓ e}
                                    (M : Monoidal V) where

open import Level
open import Function using (_$_)

open import Categories.Category.Monoidal.Properties M using (module Kelly's)
open import Categories.Category.Monoidal.Reasoning M
open import Categories.Category.Monoidal.Utilities M using (module Shorthands)
open import Categories.Functor using (Functor)
open import Categories.Morphism.Reasoning V
import Categories.Morphism.IsoEquiv V as IsoEquiv

open Setoid-Category V renaming (Obj to ObjV; id to idV)
open Commutation
open Monoidal M
open Shorthands
open IsoEquiv._≃_

record Category v : Set (o ⊔ ℓ ⊔ e ⊔ suc v) where
  field
    Obj : Set v
    hom : (A B : Obj)   → ObjV
    id  : {A : Obj}     → unit ⇒ hom A A
    ⊚   : {A B C : Obj} → hom B C ⊗₀ hom A B ⇒ hom A C

    ⊚-assoc : {A B C D : Obj} →
      [ (hom C D ⊗₀ hom B C) ⊗₀ hom A B ⇒ hom A D ]⟨
        ⊚ ⊗₁ idV          ⇒⟨ hom B D ⊗₀ hom A B ⟩
        ⊚
      ≈ associator.from   ⇒⟨ hom C D ⊗₀ (hom B C ⊗₀ hom A B) ⟩
        idV ⊗₁ ⊚          ⇒⟨ hom C D ⊗₀ hom A C ⟩
        ⊚
      ⟩
    unitˡ : {A B : Obj} →
      [ unit ⊗₀ hom A B ⇒ hom A B ]⟨
        id ⊗₁ idV         ⇒⟨ hom B B ⊗₀ hom A B ⟩
        ⊚
      ≈ unitorˡ.from
      ⟩
    unitʳ : {A B : Obj} →
      [ hom A B ⊗₀ unit ⇒ hom A B ]⟨
        idV ⊗₁ id         ⇒⟨ hom A B ⊗₀ hom A A ⟩
        ⊚
      ≈ unitorʳ.from
      ⟩

  -- A version of ⊚-assoc using generalized hom-variables.
  --
  -- In this version of associativity, the generalized variables f, g
  -- and h represent V-morphisms, or rather, morphism-valued maps,
  -- such as V-natural transofrmations or V-functorial actions.  This
  -- version is therefore well-suited for proving derived equations,
  -- such as functorial laws or commuting diagrams, that involve such
  -- maps.  For examples, see Underlying.assoc below, or the modules
  -- Enriched.Functor and Enriched.NaturalTransformation.

  ⊚-assoc-var : {X Y Z : ObjV} {A B C D : Obj}
                {f : X ⇒ hom C D} {g : Y ⇒ hom B C} {h : Z ⇒ hom A B} →
      [ (X ⊗₀ Y) ⊗₀ Z ⇒ hom A D ]⟨
        (⊚ ∘ f ⊗₁ g) ⊗₁ h  ⇒⟨ hom B D ⊗₀ hom A B ⟩
        ⊚
      ≈ associator.from    ⇒⟨ X ⊗₀ (Y ⊗₀ Z) ⟩
        f ⊗₁ (⊚ ∘ g ⊗₁ h)  ⇒⟨ hom C D ⊗₀ hom A C ⟩
        ⊚
      ⟩
  ⊚-assoc-var {f = f} {g} {h} = begin
    ⊚ ∘ (⊚ ∘ f ⊗₁ g) ⊗₁ h                 ≈⟨ refl⟩∘⟨ split₁ˡ ⟩
    ⊚ ∘ ⊚ ⊗₁ idV ∘ (f ⊗₁ g) ⊗₁ h          ≈⟨ pullˡ ⊚-assoc ⟩
    (⊚ ∘ idV ⊗₁ ⊚ ∘ α⇒) ∘ (f ⊗₁ g) ⊗₁ h   ≈⟨ pullʳ (pullʳ assoc-commute-from) ⟩
    ⊚ ∘ idV ⊗₁ ⊚ ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒     ≈˘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
    ⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h) ∘ α⇒            ∎

-- The usual shorthand for hom-objects of an arbitrary category.

infix 15 _[_,_]

_[_,_] : ∀ {c} (C : Category c) (X Y : Category.Obj C) → ObjV
_[_,_] = Category.hom

-- A V-category C does not have morphisms of its own, but the
-- collection of V-morphisms from the monoidal unit into the
-- hom-objects of C forms a setoid.  This induces the *underlying*
-- category of C.

Underlying : ∀ {c} (C : Category c) → Setoid-Category c ℓ e
Underlying C = categoryHelper (record
  { Obj = Obj
  ; _⇒_ = λ A B → unit ⇒ hom A B
  ; _≈_ = λ f g → f ≈ g
  ; id  = id
  ; _∘_ = λ f g → ⊚ ∘ f ⊗₁ g ∘ λ⇐
  ; assoc = λ {_} {_} {_} {_} {f} {g} {h} →
    begin
      ⊚ ∘ (⊚ ∘ h ⊗₁ g ∘ λ⇐) ⊗₁ f ∘ λ⇐
    ≈˘⟨ refl⟩∘⟨ assoc ⟩⊗⟨refl ⟩∘⟨refl ⟩
      ⊚ ∘ ((⊚ ∘ h ⊗₁ g) ∘ λ⇐) ⊗₁ f ∘ λ⇐
    ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩
      ⊚ ∘ (⊚ ∘ h ⊗₁ g) ⊗₁ f ∘ (λ⇐ ⊗₁ idV) ∘ λ⇐
    ≈⟨ pullˡ ⊚-assoc-var ⟩
      (⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f) ∘ α⇒) ∘ (λ⇐ ⊗₁ idV) ∘ λ⇐
    ≈˘⟨ pushˡ (pushʳ (pushʳ
          (switch-tofromˡ associator (to-≈ Kelly's.coherence-iso₁)))) ⟩
      (⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f) ∘ λ⇐) ∘ λ⇐
    ≈⟨ pullʳ (pullʳ unitorˡ-commute-to) ⟩
      ⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f) ∘ idV ⊗₁ λ⇐ ∘ λ⇐
    ≈˘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩
      ⊚ ∘ h ⊗₁ ((⊚ ∘ g ⊗₁ f) ∘ λ⇐) ∘ λ⇐
    ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟩
      ⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f ∘ λ⇐) ∘ λ⇐
    ∎
  ; identityˡ = λ {_} {_} {f} → begin
      ⊚ ∘ id ⊗₁ f ∘ λ⇐                 ≈⟨ refl⟩∘⟨ serialize₁₂ ⟩∘⟨refl ⟩
      ⊚ ∘ (id ⊗₁ idV ∘ idV ⊗₁ f) ∘ λ⇐  ≈˘⟨ refl⟩∘⟨ pushʳ unitorˡ-commute-to ⟩
      ⊚ ∘ id ⊗₁ idV ∘ λ⇐ ∘ f           ≈⟨ pullˡ unitˡ ⟩
      λ⇒ ∘ λ⇐ ∘ f                      ≈⟨ cancelˡ unitorˡ.isoʳ ⟩
      f                                ∎
  ; identityʳ = λ {_} {_} {f} → begin
      ⊚ ∘ f ⊗₁ id ∘ λ⇐                 ≈⟨ refl⟩∘⟨ serialize₂₁ ⟩∘⟨refl ⟩
      ⊚ ∘ (idV ⊗₁ id ∘ f ⊗₁ idV) ∘ λ⇐  ≈⟨ pullˡ (pullˡ unitʳ) ⟩
      (unitorʳ.from ∘ f ⊗₁ idV) ∘ λ⇐   ≈⟨ unitorʳ-commute-from ⟩∘⟨refl ⟩
      (f ∘ unitorʳ.from) ∘ λ⇐          ≈˘⟨ (refl⟩∘⟨ Kelly's.coherence₃) ⟩∘⟨refl ⟩
      (f ∘ λ⇒) ∘ λ⇐                    ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
      f                                ∎
  ; equiv    = equiv
  ; ∘-resp-≈ = λ eq₁ eq₂ → ∘-resp-≈ʳ $ ∘-resp-≈ˡ $ ⊗-resp-≈ eq₁ eq₂
  })
  where open Category C

module Underlying {c} (C : Category c) = Setoid-Category (Underlying C)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
{-
This file contains:
1. An iso πₙ'(Sⁿ) ≅ ℤ, where πₙ'(Sⁿ) = ∥ Sⁿ →∙ Sⁿ ∥₀
2. A proof that idfun∙ : Sⁿ →∙ Sⁿ is the generator of πₙ'(Sⁿ)
-}
module Cubical.Homotopy.Group.PinSn where

open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.Group.SuspensionMap
open import Cubical.Homotopy.Connected

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Path
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.SetTruncation
  renaming (elim to sElim ; elim2 to sElim2
          ; map to sMap)
open import Cubical.HITs.Truncation renaming
  (elim to trElim ; elim2 to trElim2)
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp

open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Int renaming (_+_ to _+ℤ_)

open import Cubical.ZCohomology.Properties

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Instances.Int
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties

open Iso

-- The goal is to prove that πₙSⁿ ≅ ℤ. This is of course trivial, given
-- that ΩⁿK(ℤ,n) ≅ ℤ is already proved. However, we would like to do
-- this for πₙSⁿ defined via (Sⁿ →∙ Sⁿ) and prove that the generator
-- of this group is idfun∙ : Sⁿ → Sⁿ.

private
  suspMapS^ : (n : ℕ) → (S₊∙ (suc n) →∙ S₊∙ (suc n))
                        → S₊∙ (2 + n) →∙ S₊∙ (2 + n)
  suspMapS^ n = suspMap {A = S₊∙ (suc n)} n

is2ConnectedSuspMap : (n : ℕ) → isConnectedFun 2 (suspMapS^ (suc n))
is2ConnectedSuspMap n =
  isConnectedFunSubtr 2 n _
    (subst (λ x → isConnectedFun x (suspMapS^ (suc n)))
                   (subtrLem n (suc (suc n)) ∙ +-comm 2 n)
      (isConnectedSuspMap (suc n) (suc n)))
  where
  subtrLem : (n m : ℕ) → (n + m ∸ n) ≡ m
  subtrLem zero m = refl
  subtrLem (suc n) m = subtrLem n m

-- From the connectedness of the suspension map,
--  we get an iso πₙSⁿ ≅ πₙ₊₁(Sⁿ⁺¹) for n ≥ 2.
SphereSuspIso : (n : ℕ)
  → Iso (π' (2 + n) (S₊∙ (2 + n))) (π' (3 + n) (S₊∙ (3 + n)))
SphereSuspIso n =
  compIso setTruncTrunc2Iso
   (compIso
     (connectedTruncIso 2
       (suspMap {A = S₊∙ (suc (suc n))} (suc n)) (is2ConnectedSuspMap n))
     (invIso (setTruncTrunc2Iso)))

SphereSuspGrIso : (n : ℕ)
  → GroupIso (π'Gr (suc n) (S₊∙ (2 + n))) (π'Gr (2 + n) (S₊∙ (3 + n)))
fst (SphereSuspGrIso n) = SphereSuspIso n
snd (SphereSuspGrIso n) =
  makeIsGroupHom (sElim2 (λ _ _ → isSetPathImplicit)
    λ f g → IsGroupHom.pres· (suspMapπ'Hom (suc n) .snd) ∣ f ∣₂ ∣ g ∣₂)

private
  stLoop₁ : π 2 (S₊∙ 2)
  stLoop₁ = ∣ sym (rCancel (merid base))
          ∙∙ (λ i → merid (loop i) ∙ sym (merid base))
          ∙∙ rCancel (merid base) ∣₂

  stLoop₁flip : π 2 (S₊∙ 2)
  stLoop₁flip = sMap flipSquare stLoop₁

flipSquareIso : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
  → GroupIso (πGr (suc n) A) (πGr (suc n) A)
fun (fst (flipSquareIso n)) = sMap flipSquare
inv (fst (flipSquareIso n)) = sMap flipSquare
rightInv (fst (flipSquareIso n)) =
  sElim (λ _ → isSetPathImplicit) λ _ → refl
leftInv (fst (flipSquareIso n)) =
  sElim (λ _ → isSetPathImplicit) λ _ → refl
snd (flipSquareIso n) =
  makeIsGroupHom
    (sElim2 (λ _ _ → isSetPathImplicit)
      λ f g → cong ∣_∣₂
        ((sym (sym≡flipSquare (f ∙ g))
      ∙∙ symDistr f g
      ∙∙ cong₂ _∙_ (sym≡flipSquare g) (sym≡flipSquare f)
       ∙ EH n (flipSquare g) (flipSquare f))))

-- We now want to prove π₁S¹≅π₂S². This will be done by passing through
-- The loop space defintion of the groups
π'₂S²≅π₂S² : GroupIso (π'Gr 1 (S₊∙ 2)) (πGr 1 (S₊∙ 2))
π'₂S²≅π₂S² = π'Gr≅πGr 1 (S₊∙ 2)

{- We now define the iso π₂S² ≅ π₁S¹ -}
π₂S²≅π₁S¹ : GroupIso (πGr 1 (S₊∙ 2)) (πGr 0 (S₊∙ 1))
fst π₂S²≅π₁S¹ =
  compIso setTruncTrunc2Iso
   (compIso
    (compIso (invIso (PathIdTruncIso 2))
     (compIso (congIso (invIso (PathIdTruncIso 3)))
      (compIso
        (congIso (invIso (Iso-Kn-ΩKn+1 1)))
        (PathIdTruncIso 2))))
    (invIso setTruncTrunc2Iso))
snd π₂S²≅π₁S¹ =
  makeIsGroupHom
    (sElim2 (λ _ _ → isSetPathImplicit)
      λ f g →
        cong (inv setTruncTrunc2Iso)
          (cong (fun (PathIdTruncIso 2))
            (cong (cong (ΩKn+1→Kn 1))
              (cong (cong (inv (PathIdTruncIso 3)))
                (cong (inv (PathIdTruncIso 2))
                  (refl {x = ∣ f ∙ g ∣})
               ∙ cong-∙ ∣_∣ₕ f g)
             ∙ cong-∙ (inv (PathIdTruncIso 3)) (cong ∣_∣ₕ f) (cong ∣_∣ₕ g))
           ∙ cong-∙ (ΩKn+1→Kn 1)
              (cong (inv (PathIdTruncIso 3)) (cong ∣_∣ₕ f))
              (cong (inv (PathIdTruncIso 3)) (cong ∣_∣ₕ g)))
         ∙ PathIdTruncIsoFunct 1
            (cong (ΩKn+1→Kn 1) (λ i → inv (PathIdTruncIso 3) ∣ f i ∣ₕ))
            (cong (ΩKn+1→Kn 1) (λ i → inv (PathIdTruncIso 3) ∣ g i ∣ₕ)))
         ∙ setTruncTrunc2IsoFunct
            ((fun (PathIdTruncIso 2))
             (cong (ΩKn+1→Kn 1) (λ i → inv (PathIdTruncIso 3) ∣ f i ∣ₕ)))
            ((fun (PathIdTruncIso 2))
             (cong (ΩKn+1→Kn 1) (λ i → inv (PathIdTruncIso 3) ∣ g i ∣ₕ))))
  where
  setTruncTrunc2IsoFunct : ∀ {ℓ} {A : Type ℓ} {x : A}
    (p q : hLevelTrunc 2 (x ≡ x))
    → inv setTruncTrunc2Iso
         (Cubical.HITs.Truncation.map2 _∙_ p q)
       ≡ ·π 0 (inv setTruncTrunc2Iso p) (inv setTruncTrunc2Iso q)
  setTruncTrunc2IsoFunct =
    trElim2 (λ  _ _ → isSetPathImplicit) λ _ _ → refl

π₂'S²≅π₁'S¹ : GroupIso (π'Gr 1 (S₊∙ 2)) (π'Gr 0 (S₊∙ 1))
π₂'S²≅π₁'S¹ =
  compGroupIso (π'Gr≅πGr 1 (S₊∙ 2))
    (compGroupIso (flipSquareIso 0)
      (compGroupIso π₂S²≅π₁S¹
        (invGroupIso (π'Gr≅πGr 0 (S₊∙ 1)))))

-- We get our iso
πₙ'Sⁿ≅ℤ : (n : ℕ) → GroupIso (π'Gr n (S₊∙ (suc n))) ℤGroup
πₙ'Sⁿ≅ℤ zero =
  compGroupIso (π'Gr≅πGr zero (S₊∙ 1))
    ((compIso (setTruncIdempotentIso (isGroupoidS¹ _ _)) ΩS¹Isoℤ)
      , makeIsGroupHom (sElim2 (λ _ _ → isProp→isSet (isSetℤ _ _))
           winding-hom))
πₙ'Sⁿ≅ℤ (suc zero) = compGroupIso π₂'S²≅π₁'S¹ (πₙ'Sⁿ≅ℤ zero)
πₙ'Sⁿ≅ℤ (suc (suc n)) =
  compGroupIso (invGroupIso (SphereSuspGrIso n)) (πₙ'Sⁿ≅ℤ (suc n))

-- Same thing for the loop space definition
πₙSⁿ≅ℤ : (n : ℕ) → GroupIso (πGr n (S₊∙ (suc n))) ℤGroup
πₙSⁿ≅ℤ n =
  compGroupIso (invGroupIso (π'Gr≅πGr n (S₊∙ (suc n)))) (πₙ'Sⁿ≅ℤ n)

-- The goal now is to show that πₙ'Sⁿ≅ℤ takes idfun∙ : Sⁿ → Sⁿ to 1.
-- For this, we need a bunch of identities:
private
  Isoπ₁S¹ℤ = (compIso (setTruncIdempotentIso (isGroupoidS¹ _ _)) ΩS¹Isoℤ)

  π'₂S²≅π₂S²⁻-stLoop' : inv (fst (π'₂S²≅π₂S²)) stLoop₁flip ≡ ∣ idfun∙ _ ∣₂
  π'₂S²≅π₂S²⁻-stLoop' =
    cong ∣_∣₂ (ΣPathP ((funExt
      (λ { north → refl
         ; south → merid base
         ; (merid base i) j →
           hcomp (λ k
             → λ {(i = i0) → north
                 ; (i = i1) → merid base (j ∧ k)
                 ; (j = i0) → rUnit (λ _ → north) k i
                 ; (j = i1) → merid base (i ∧ k)})
                 north
         ; (merid (loop k) i) j
                  → hcomp (λ r
                    → λ {(i = i0) → north
                        ; (i = i1) → merid base (j ∧ r)
                        ; (j = i0) →
                          rUnit (funExt⁻ (cong fst (cong (Ω→SphereMap 1)
                              (flipSquare (sym (rCancel (merid base))
                            ∙∙ (λ i₁ → merid (loop i₁)
                             ∙ sym (merid base))
                            ∙∙ rCancel (merid base))))) (loop k)) r i
                        ; (j = i1) → lem₂ r i k})
                 (((sym (rCancel (merid base)) ∙∙
                    (λ i₁ → merid (loop i₁) ∙ sym (merid base)) ∙∙
                    rCancel (merid base))) k i)})) , refl))
    where
    genBot+side : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y)
                → Cube {A = A} (λ j r → x) (λ j r → p (~ j ∨ r))
                                (λ i r → p i) (λ i r → p (i ∧ r))
                                (λ i j → p (i ∧ ~ j)) (λ i j → p i)
                 × Cube {A = A} (λ j r → p (~ j ∨ r)) (λ j r → p (r ∧ j))
                                (λ k r → p (~ k)) (λ k r → p r)
                                (λ k j → p (~ k ∧ ~ j)) λ k j → p (j ∨ ~ k)
    genBot+side {A = A} {x = x} =
      J (λ y p → Cube {A = A} (λ j r → x) (λ j r → p (~ j ∨ r))
                                (λ i r → p i) (λ i r → p (i ∧ r))
                                (λ i j → p (i ∧ ~ j)) (λ i j → p i)
                 × Cube {A = A} (λ j r → p (~ j ∨ r)) (λ j r → p (r ∧ j))
                                (λ k r → p (~ k)) (λ k r → p r)
                                (λ k j → p (~ k ∧ ~ j)) λ k j → p (j ∨ ~ k))
         (refl , refl)

    lem₁ : I → I → I → S₊ 2
    lem₁ j i r =
      hcomp (λ k → λ {(i = i0) → north
                     ; (i = i1) → genBot+side (merid base) .snd k j r
                     ; (j = i0) → compPath-filler
                                    (merid base) (sym (merid base)) k i
                     ; (j = i1) → merid base (i ∧ r)
                     ; (r = i0) → rCancel-filler (merid base) k j i
                     ; (r = i1) → compPath-filler
                                   (merid base) (sym (merid base)) (~ j ∧ k) i})
            (genBot+side (merid base) .fst i j r)

    lem₂ : I → I → I → S₊ 2
    lem₂ r i k =
      hcomp (λ j → λ {(i = i0) → north
                     ; (i = i1) → merid base (r ∧ j)
                     ; (r = i0) → doubleCompPath-filler
                                    (sym (rCancel (merid base)))
                                    (λ i₁ → merid (loop i₁) ∙ sym (merid base))
                                    (rCancel (merid base)) j k i
                     ; (r = i1) → compPath-filler
                                   (merid (loop k)) (sym (merid base)) (~ j) i
                     ; (k = i0) → lem₁ j i r
                     ; (k = i1) → lem₁ j i r})
            ((merid (loop k) ∙ sym (merid base)) i)

  π₂S²≅π₁S¹-stLoop : fun (fst π₂S²≅π₁S¹) stLoop₁ ≡ ∣ loop ∣₂
  π₂S²≅π₁S¹-stLoop =
      sym (leftInv Isoπ₁S¹ℤ
          (fun (fst π₂S²≅π₁S¹) stLoop₁))
   ∙∙ cong (inv Isoπ₁S¹ℤ) compute
   ∙∙ leftInv (compIso (setTruncIdempotentIso (isGroupoidS¹ _ _)) ΩS¹Isoℤ)
              ∣ loop ∣₂
    where
    compute : fun Isoπ₁S¹ℤ (fun (fst π₂S²≅π₁S¹) stLoop₁)
            ≡ fun Isoπ₁S¹ℤ ∣ loop ∣₂
    compute = refl

  π₂'S²≅π₁'S¹≡ : fun (fst π₂'S²≅π₁'S¹) ∣ idfun∙ _ ∣₂ ≡ ∣ idfun∙ _ ∣₂
  π₂'S²≅π₁'S¹≡ =
    lem₁ ∣ idfun∙ _ ∣₂ stLoop₁
      (sym π'₂S²≅π₂S²⁻-stLoop')
      (cong (inv (fst (π'Gr≅πGr zero (S₊∙ 1)))) π₂S²≅π₁S¹-stLoop
     ∙ lem₂)
    where
    lem₁ : (x : _) (y : π 2 (S₊∙ 2))
       → (x ≡ inv (fst π'₂S²≅π₂S²) (fun (fst (flipSquareIso 0)) y))
       → inv (fst (π'Gr≅πGr zero (S₊∙ 1))) (fun (fst π₂S²≅π₁S¹) y)
          ≡ ∣ idfun∙ _ ∣₂
       → fun (fst π₂'S²≅π₁'S¹) x ≡ ∣ idfun∙ _ ∣₂
    lem₁ x y p q =
         cong (fun (fst π₂'S²≅π₁'S¹)) p
      ∙∙ (λ i → inv (fst (π'Gr≅πGr zero (S₊∙ (suc zero)))) (fun (fst π₂S²≅π₁S¹)
          (fun (fst (flipSquareIso zero))
            (rightInv
              (fst (π'Gr≅πGr (suc zero) (S₊∙ (suc (suc zero)))))
              (inv (fst (flipSquareIso zero)) y) i)
          )))
      ∙∙ cong (inv (fst (π'Gr≅πGr zero (S₊∙ (suc zero)))))
              (cong (fun (fst π₂S²≅π₁S¹))
                (rightInv (fst (flipSquareIso zero)) y))
       ∙ q

    lem₂ : inv (fst (π'Gr≅πGr zero (S₊∙ 1))) ∣ loop ∣₂ ≡ ∣ idfun∙ _ ∣₂
    lem₂ =
      cong ∣_∣₂ (ΣPathP (funExt (λ { base → refl ; (loop i) → refl}) , refl))

  suspPresIdfun : (n : ℕ) → suspMap n (idfun∙ (S₊∙ (suc n))) ≡ idfun∙ _
  suspPresIdfun n =
    ΣPathP ((funExt
      (λ { north → refl
         ; south → merid (ptSn (suc n))
         ; (merid a i) j
           → compPath-filler (merid a) (sym (merid (ptSn (suc n)))) (~ j) i}))
        , refl)

  suspPresIdfun2 : (n : ℕ)
    → fun (fst (invGroupIso (SphereSuspGrIso n)))
        ∣ idfun∙ (S₊∙ (suc (suc (suc n)))) ∣₂
    ≡ ∣ idfun∙ _ ∣₂
  suspPresIdfun2 n =
      sym (cong (fun (fst (invGroupIso (SphereSuspGrIso n))))
          (cong ∣_∣₂ (suspPresIdfun (suc n))))
    ∙ leftInv (SphereSuspIso n) ∣ idfun∙ _ ∣₂

-- We finally have our results
πₙ'Sⁿ≅ℤ-idfun∙ : (n : ℕ)
  → fun (fst (πₙ'Sⁿ≅ℤ n)) ∣ idfun∙ _ ∣₂ ≡ (pos (suc zero))
πₙ'Sⁿ≅ℤ-idfun∙ zero = refl
πₙ'Sⁿ≅ℤ-idfun∙ (suc zero) = speedUp ∣ idfun∙ _ ∣₂ π₂'S²≅π₁'S¹≡
  where
  speedUp : (x : _) -- stated like this for faster type checking
     → fun (fst π₂'S²≅π₁'S¹) x ≡ ∣ idfun∙ _ ∣₂
     → fun (fst (πₙ'Sⁿ≅ℤ (suc zero))) x ≡ pos (suc zero)
  speedUp x p = cong (fun (fst (πₙ'Sⁿ≅ℤ zero))) p
πₙ'Sⁿ≅ℤ-idfun∙ (suc (suc n)) =
  cong (fun (fst (πₙ'Sⁿ≅ℤ (suc n)))) (suspPresIdfun2 n)
  ∙ πₙ'Sⁿ≅ℤ-idfun∙ (suc n)

πₙ'Sⁿ-gen-by-idfun : (n : ℕ) → gen₁-by (π'Gr n (S₊∙ (suc n))) ∣ idfun∙ _ ∣₂
πₙ'Sⁿ-gen-by-idfun n =
  subst (gen₁-by (π'Gr n (S₊∙ (suc n))))
        (sym (cong (inv (fst (πₙ'Sⁿ≅ℤ n))) (πₙ'Sⁿ≅ℤ-idfun∙ n))
        ∙ leftInv (fst (πₙ'Sⁿ≅ℤ n)) ∣ idfun∙ _ ∣₂)
        (Iso-pres-gen₁ ℤGroup (π'Gr n (S₊∙ (suc n)))
          (pos (suc zero))
          (λ h → h , (sym (·Comm h (pos 1)) ∙ ℤ·≡· h (pos 1)))
          (invGroupIso (πₙ'Sⁿ≅ℤ n)))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module IgnoreWarnings where

-- all of the following files have warnings, which should be ignored
-- because of the command-line flag

import Issue2243
import Issue708quote
import OldCompilerPragmas
import RewritingEmptyPragma
import Unreachable

-- this should also be ignored
{-# REWRITE #-}

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
-- Andreas, 2012-01-12
module Common.Irrelevance where

open import Common.Level

record Squash {a}(A : Set a) : Set a where
  constructor squash
  field
    .unsquash : A
open Squash public


text:
------------------------------------------------------------------------------
-- FOTC natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat where

open import FOTC.Base
open import FOTC.Data.Nat.Type public

infixl 7 _*_
infixl 6 _+_ _∸_

------------------------------------------------------------------------------
-- Arithmetic operations

postulate
  _+_  : D → D → D
  +-0x : ∀ n → zero + n      ≡ n
  +-Sx : ∀ m n → succ₁ m + n ≡ succ₁ (m + n)
{-# ATP axioms +-0x +-Sx #-}

postulate
  _∸_  : D → D → D
  ∸-x0 : ∀ n → n ∸ zero      ≡ n
  ∸-xS : ∀ m n → m ∸ succ₁ n ≡ pred₁ (m ∸ n)
{-# ATP axioms ∸-x0 ∸-xS #-}

postulate
  _*_  : D → D → D
  *-0x : ∀ n → zero * n      ≡ zero
  *-Sx : ∀ m n → succ₁ m * n ≡ n + m * n
{-# ATP axioms *-0x *-Sx #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.CohomologyRings.Unit where

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

open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_)
open import Cubical.Data.Int
open import Cubical.Data.Vec
open import Cubical.Data.FinData

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Int renaming (ℤGroup to ℤG)
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.QuotientRing
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-Quotient
open import Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly-notationZ
open import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.A[X]X-A

open import Cubical.HITs.Truncation
open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _/sq_)
open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.CohomologyRing
open import Cubical.ZCohomology.Groups.Unit

open Iso

module Equiv-Unit-Properties where

  open CommRingStr (snd ℤCR) using ()
    renaming
    ( 0r        to 0ℤ
    ; 1r        to 1ℤ
    ; _+_       to _+ℤ_
    ; -_        to -ℤ_
    ; _·_       to _·ℤ_
    ; +Assoc    to +ℤAssoc
    ; +IdL      to +ℤIdL
    ; +IdR      to +ℤIdR
    ; +Comm     to +ℤComm
    ; ·Assoc    to ·ℤAssoc
    ; ·IdL      to ·ℤIdL
    ; ·IdR      to ·ℤIdR
    ; ·DistR+   to ·ℤDistR+
    ; is-set    to isSetℤ     )

  open RingStr (snd (H*R Unit)) using ()
    renaming
    ( 0r        to 0H*
    ; 1r        to 1H*
    ; _+_       to _+H*_
    ; -_        to -H*_
    ; _·_       to _cup_
    ; +Assoc    to +H*Assoc
    ; +IdL      to +H*IdL
    ; +IdR      to +H*IdR
    ; +Comm     to +H*Comm
    ; ·Assoc    to ·H*Assoc
    ; ·IdL      to ·H*IdL
    ; ·IdR      to ·H*IdR
    ; ·DistR+   to ·H*DistR+
    ; is-set    to isSetH*     )

  open CommRingStr (snd ℤ[X]) using ()
    renaming
    ( 0r        to 0Pℤ
    ; 1r        to 1Pℤ
    ; _+_       to _+Pℤ_
    ; -_        to -Pℤ_
    ; _·_       to _·Pℤ_
    ; +Assoc    to +PℤAssoc
    ; +IdL      to +PℤIdL
    ; +IdR      to +PℤIdR
    ; +Comm     to +PℤComm
    ; ·Assoc    to ·PℤAssoc
    ; ·IdL      to ·PℤIdL
    ; ·IdR      to ·PℤIdR
    ; ·DistR+   to ·PℤDistR+
    ; is-set    to isSetPℤ     )

  open CommRingStr (snd ℤ[X]/X) using ()
    renaming
    ( 0r        to 0PℤI
    ; 1r        to 1PℤI
    ; _+_       to _+PℤI_
    ; -_        to -PℤI_
    ; _·_       to _·PℤI_
    ; +Assoc    to +PℤIAssoc
    ; +IdL      to +PℤIIdL
    ; +IdR      to +PℤIIdR
    ; +Comm     to +PℤIComm
    ; ·Assoc    to ·PℤIAssoc
    ; ·IdL      to ·PℤIIdL
    ; ·IdR      to ·PℤIIdR
    ; ·DistR+   to ·PℤIDistR+
    ; is-set    to isSetPℤI     )

-----------------------------------------------------------------------------
-- Direct Sens on ℤ[x]

  ℤ[x]→H*-Unit : ℤ[x] → H* Unit
  ℤ[x]→H*-Unit = DS-Rec-Set.f _ _ _ _ isSetH*
                  0H*
                  base-trad
                  _+H*_
                  +H*Assoc
                  +H*IdR
                  +H*Comm
                  base-neutral-eq
                  base-add-eq
               where
               base-trad : _
               base-trad (zero ∷ []) a = base zero (inv (fst H⁰-Unit≅ℤ) a)
               base-trad (suc n ∷ []) a = 0H*

               base-neutral-eq :  _
               base-neutral-eq (zero ∷ []) = base-neutral _
               base-neutral-eq (suc n ∷ []) = refl

               base-add-eq : _
               base-add-eq (zero ∷ []) a b = base-add _ _ _
               base-add-eq (suc n ∷ []) a b = +H*IdR _

  ℤ[x]→H*-Unit-pres1Pℤ : ℤ[x]→H*-Unit (1Pℤ) ≡ 1H*
  ℤ[x]→H*-Unit-pres1Pℤ = refl

  ℤ[x]→H*-Unit-pres+ : (x y : ℤ[x]) → ℤ[x]→H*-Unit (x +Pℤ y) ≡ ℤ[x]→H*-Unit x +H* ℤ[x]→H*-Unit y
  ℤ[x]→H*-Unit-pres+ x y = refl

-- -- Proving the morphism on the cup product

  T0 : (z : ℤ) → coHom 0 Unit
  T0 = λ z → inv (fst H⁰-Unit≅ℤ) z

  T0g : IsGroupHom (ℤG .snd) (fst (invGroupIso H⁰-Unit≅ℤ) .fun) (coHomGr 0 Unit .snd)
  T0g = snd (invGroupIso H⁰-Unit≅ℤ)

    -- idea : control of the unfolding + simplification of T0 on the left
  pres·-base-case-00 : (a : ℤ) → (b : ℤ) →
                        T0 (a ·ℤ b) ≡ (T0 a) ⌣ (T0 b)
  pres·-base-case-00 (pos zero)       b = (IsGroupHom.pres1 T0g)
  pres·-base-case-00 (pos (suc n))    b = ((IsGroupHom.pres· T0g b (pos n ·ℤ b)))
                                          ∙ (cong (λ X → (T0 b) +ₕ X) (pres·-base-case-00 (pos n) b))
  pres·-base-case-00 (negsuc zero)    b = IsGroupHom.presinv T0g b
  pres·-base-case-00 (negsuc (suc n)) b = cong T0 (+ℤComm (-ℤ b) (negsuc n ·ℤ b)) -- ·ℤ and ·₀ are defined asymetrically !
                                          ∙ IsGroupHom.pres· T0g (negsuc n ·ℤ b) (-ℤ b)
                                          ∙ cong₂ _+ₕ_ (pres·-base-case-00 (negsuc n) b)
                                                         (IsGroupHom.presinv T0g b)

  pres·-base-case-int : (n : ℕ) → (a : ℤ) → (m : ℕ) → (b : ℤ) →
                ℤ[x]→H*-Unit (base (n ∷ []) a ·Pℤ base (m ∷ []) b)
              ≡ ℤ[x]→H*-Unit (base (n ∷ []) a) cup ℤ[x]→H*-Unit (base (m ∷ []) b)
  pres·-base-case-int zero    a zero    b = cong (base 0) (pres·-base-case-00 a b)
  pres·-base-case-int zero    a (suc m) b = refl
  pres·-base-case-int (suc n) a m       b = refl

  pres·-base-case-vec : (v : Vec ℕ 1) → (a : ℤ) → (v' : Vec ℕ 1) → (b : ℤ) →
                ℤ[x]→H*-Unit (base v a ·Pℤ base v' b)
              ≡ ℤ[x]→H*-Unit (base v a) cup ℤ[x]→H*-Unit (base v' b)
  pres·-base-case-vec (n ∷ []) a (m ∷ []) b = pres·-base-case-int n a m b

  ℤ[x]→H*-Unit-pres· : (x y : ℤ[x]) → ℤ[x]→H*-Unit (x ·Pℤ y) ≡ ℤ[x]→H*-Unit x cup ℤ[x]→H*-Unit y
  ℤ[x]→H*-Unit-pres· = DS-Ind-Prop.f _ _ _ _
                         (λ x p q i y j → isSetH* _ _ (p y) (q y) i j)
                         (λ y → refl)
                         base-case
                         λ {U V} ind-U ind-V y → cong₂ _+H*_ (ind-U y) (ind-V y)
    where
    base-case : _
    base-case (n ∷ []) a = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH* _ _)
                           (sym (RingTheory.0RightAnnihilates (H*R Unit) _))
                           (λ v' b → pres·-base-case-vec (n ∷ []) a v' b)
                           λ {U V} ind-U ind-V → (cong₂ _+H*_ ind-U ind-V) ∙ sym (·H*DistR+ _ _ _)

    -- raising to the product
  ℤ[x]→H*-Unit-cancelX : (k : Fin 1) → ℤ[x]→H*-Unit (<X> k) ≡ 0H*
  ℤ[x]→H*-Unit-cancelX zero = refl

  ℤ[X]→H*-Unit : RingHom (CommRing→Ring ℤ[X]) (H*R Unit)
  fst ℤ[X]→H*-Unit = ℤ[x]→H*-Unit
  snd ℤ[X]→H*-Unit = makeIsRingHom ℤ[x]→H*-Unit-pres1Pℤ ℤ[x]→H*-Unit-pres+ ℤ[x]→H*-Unit-pres·

  ℤ[X]/X→H*R-Unit : RingHom (CommRing→Ring ℤ[X]/X) (H*R Unit)
  ℤ[X]/X→H*R-Unit = Quotient-FGideal-CommRing-Ring.inducedHom ℤ[X] (H*R Unit) ℤ[X]→H*-Unit <X> ℤ[x]→H*-Unit-cancelX

  ℤ[x]/x→H*-Unit : ℤ[x]/x → H* Unit
  ℤ[x]/x→H*-Unit = fst ℤ[X]/X→H*R-Unit

-----------------------------------------------------------------------------
-- Converse Sens on ℤ[X]

  H*-Unit→ℤ[x] : H* Unit → ℤ[x]
  H*-Unit→ℤ[x] = DS-Rec-Set.f _ _ _ _ isSetPℤ
                  0Pℤ
                  base-trad
                  _+Pℤ_
                  +PℤAssoc
                  +PℤIdR
                  +PℤComm
                  base-neutral-eq
                  base-add-eq
               where
               base-trad : (n : ℕ) → coHom n Unit → ℤ[x]
               base-trad zero a = base (0 ∷ []) (fun (fst H⁰-Unit≅ℤ) a)
               base-trad (suc n) a = 0Pℤ

               base-neutral-eq : _
               base-neutral-eq zero = base-neutral _
               base-neutral-eq (suc n) = refl

               base-add-eq : _
               base-add-eq zero a b = base-add _ _ _
                                      ∙ cong (base (0 ∷ [])) (sym (IsGroupHom.pres· (snd H⁰-Unit≅ℤ) a b))
               base-add-eq (suc n) a b = +PℤIdR _

  H*-Unit→ℤ[x]-pres+ : (x y : H* Unit) → H*-Unit→ℤ[x] ( x +H* y) ≡ H*-Unit→ℤ[x] x +Pℤ H*-Unit→ℤ[x] y
  H*-Unit→ℤ[x]-pres+ x y = refl

  H*-Unit→ℤ[x]/x : H* Unit → ℤ[x]/x
  H*-Unit→ℤ[x]/x = [_] ∘ H*-Unit→ℤ[x]

  H*-Unit→ℤ[x]/x-pres+ : (x y : H* Unit) → H*-Unit→ℤ[x]/x (x +H* y) ≡ (H*-Unit→ℤ[x]/x x) +PℤI (H*-Unit→ℤ[x]/x y)
  H*-Unit→ℤ[x]/x-pres+ x y = cong [_] (H*-Unit→ℤ[x]-pres+ x y)

-----------------------------------------------------------------------------
-- Section

  e-sect : (x : H* Unit) → ℤ[x]/x→H*-Unit (H*-Unit→ℤ[x]/x x) ≡ x
  e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH* _ _)
           refl
           base-case
           λ {U V} ind-U ind-V → cong ℤ[x]/x→H*-Unit (H*-Unit→ℤ[x]/x-pres+ U V)
                                  ∙ IsRingHom.pres+ (snd ℤ[X]/X→H*R-Unit) (H*-Unit→ℤ[x]/x U) (H*-Unit→ℤ[x]/x V)
                                  ∙ cong₂ _+H*_ ind-U ind-V
           where
           base-case : _
           base-case zero a = cong (base 0) (leftInv (fst H⁰-Unit≅ℤ) a)
           base-case (suc n) a = (sym (base-neutral (suc n)))
                                 ∙ (cong (base (suc n)) ((isContr→isProp (isContrHⁿ-Unit n) _ a)))

-----------------------------------------------------------------------------
-- Retraction

  e-retr : (x : ℤ[x]/x) → H*-Unit→ℤ[x]/x (ℤ[x]/x→H*-Unit x) ≡ x
  e-retr = SQ.elimProp (λ _ → isSetPℤI _ _)
           (DS-Ind-Prop.f _ _ _ _ (λ _ → isSetPℤI _ _)
           refl
           base-case
           λ {U V} ind-U ind-V → cong₂ _+PℤI_ ind-U ind-V)
           where
           base-case : _
           base-case (zero ∷ []) a = refl
           base-case (suc n ∷ []) a = eq/ 0Pℤ (base (suc n ∷ []) a) ∣ ((λ x → base (n ∷ []) (-ℤ a)) , foo) ∣₁
             where
             foo : (0Pℤ +Pℤ base (suc n ∷ []) (- a)) ≡ (base (n +n 1 ∷ []) (- a · pos 1) +Pℤ 0Pℤ)
             foo = (0Pℤ +Pℤ base (suc n ∷ []) (- a)) ≡⟨ +PℤIdL _ ⟩
                   base (suc n ∷ []) (- a) ≡⟨ cong₂ base (cong (λ X → X ∷ []) (sym ((+-suc n 0)
                                              ∙ (cong suc (+-zero n))))) (sym (·ℤIdR _)) ⟩
                   base (n +n suc 0 ∷ []) (- a ·ℤ 1ℤ) ≡⟨ refl ⟩
                   base (n +n 1 ∷ []) (- a · pos 1) ≡⟨ sym (+PℤIdR _) ⟩
                   (base (n +n 1 ∷ []) (- a · pos 1) +Pℤ 0Pℤ) ∎

-----------------------------------------------------------------------------
-- Computation of the Cohomology Ring

module _ where

  open Equiv-Unit-Properties
  open RingEquivs

  Unit-CohomologyRingP : RingEquiv (CommRing→Ring ℤ[X]/X) (H*R Unit)
  fst Unit-CohomologyRingP = isoToEquiv is
    where
    is : Iso ℤ[x]/x (H* Unit)
    fun is = ℤ[x]/x→H*-Unit
    inv is = H*-Unit→ℤ[x]/x
    rightInv is = e-sect
    leftInv is = e-retr
  snd Unit-CohomologyRingP = snd ℤ[X]/X→H*R-Unit

  CohomologyRing-UnitP : RingEquiv (H*R Unit) (CommRing→Ring ℤ[X]/X)
  CohomologyRing-UnitP = invRingEquiv Unit-CohomologyRingP

  Unit-CohomologyRingℤ : RingEquiv (CommRing→Ring ℤCR) (H*R Unit)
  Unit-CohomologyRingℤ = compRingEquiv (invRingEquiv Equiv-ℤ[X]/X-ℤ) Unit-CohomologyRingP

  CohomologyRing-Unitℤ : RingEquiv (H*R Unit) (CommRing→Ring ℤCR)
  CohomologyRing-Unitℤ = compRingEquiv CohomologyRing-UnitP Equiv-ℤ[X]/X-ℤ


text:
module Implicits.Resolution.Embedding where

open import Prelude

open import Data.Vec
open import Data.List as List hiding (map)

open import Implicits.Syntax
open import SystemF.Everything as F using ()

⟦_⟧tp← : ∀ {ν} → F.Type ν → Type ν
⟦ F.tc x ⟧tp← = simpl (tc x)
⟦ F.tvar n ⟧tp← = simpl (tvar n)
⟦ a F.→' b ⟧tp← = (⟦ a ⟧tp← ⇒ ⟦ b ⟧tp←)
⟦ a F.⟶ b ⟧tp← = simpl (⟦ a ⟧tp← →' ⟦ b ⟧tp←)
⟦ F.∀' x ⟧tp← = ∀' ⟦ x ⟧tp←

⟦_⟧tps← : ∀ {ν n} → Vec (F.Type ν) n → Vec (Type ν) n
⟦ v ⟧tps← = map (⟦_⟧tp←) v

⟦_⟧ctx← : ∀ {ν n} → Vec (F.Type ν) n → List (Type ν)
⟦ v ⟧ctx← = toList $ map ⟦_⟧tp← v

⟦_⟧tp→ : ∀ {ν} → Type ν → F.Type ν
⟦ simpl (tc x) ⟧tp→ = F.tc x
⟦ simpl (tvar n) ⟧tp→ = F.tvar n
⟦ simpl (a →' b) ⟧tp→ = ⟦ a ⟧tp→ F.⟶ ⟦ b ⟧tp→
⟦ a ⇒ b ⟧tp→ = ⟦ a ⟧tp→ F.→' ⟦ b ⟧tp→
⟦ ∀' x ⟧tp→ = F.∀' ⟦ x ⟧tp→

⟦_⟧tps→ : ∀ {ν n} → Vec (Type ν) n → Vec (F.Type ν) n
⟦ v ⟧tps→ = map (⟦_⟧tp→) v

⟦_⟧ctx→ : ∀ {ν} → (Δ : ICtx ν) → Vec (F.Type ν) (List.length (List.map ⟦_⟧tp→ Δ))
⟦ Δ ⟧ctx→ = fromList (List.map ⟦_⟧tp→ Δ)


text:
------------------------------------------------------------------------
-- A parametrised specification of "natrec", along with a proof that
-- the specification is propositional (assuming extensionality)
------------------------------------------------------------------------

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

open import Equality
open import Prelude hiding (ℕ; zero; suc)

-- The module is parametrised by equality and some type that is closed
-- under "zero" and "suc".

module Nat.Eliminator
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive)
  (ℕ : Type) (zero : ℕ) (suc : ℕ → ℕ)
  where

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
import Equivalence eq as Eq
open import Function-universe eq hiding (_∘_)
open import H-level eq as H-level
open import H-level.Closure eq
open import Surjection eq using (_↠_)

-- Specification of natrec.

Natrec : (ℓ : Level) → Type (lsuc ℓ)
Natrec ℓ =
  (P : ℕ → Type ℓ) (z : P zero) (s : ∀ n → P n → P (suc n)) →
  ∃ λ (natrec : ∀ n → P n) →
    natrec zero ≡ z
      ×
    ∀ n → natrec (suc n) ≡ s n (natrec n)

-- This specification is propositional (assuming extensionality).
--
-- Note that the proof uses some lemmas that are defined by recursion
-- on natural numbers. I suspect that it would be easy (although
-- perhaps somewhat tedious) to avoid such recursion.
--
-- I got the idea for this result from Christian Sattler, who
-- mentioned the work of Awodey, Gambino and Sojakova: in "Inductive
-- types in homotopy type theory" they prove something similar for a
-- non-dependent eliminator.

Natrec-propositional :
  ∀ {ℓ} →
  Extensionality (lsuc ℓ) ℓ →
  Is-proposition (Natrec ℓ)
Natrec-propositional {ℓ} ext₊ =
  [inhabited⇒+]⇒+ 0 λ natrec₀ →
  Π-closure ext₊ 1 λ P →
  Π-closure ext₌ 1 λ z →
  Π-closure ext₌ 1 λ s →
  H-level.respects-surjection (∃-cong (lemma natrec₀ P z s)) 1
    (mono₁ 0 (singleton-contractible _))
  where
  ext₌ : Extensionality ℓ ℓ
  ext₌ = lower-extensionality _ lzero ext₊

  ext₀ : Extensionality lzero ℓ
  ext₀ = lower-extensionality _ lzero ext₊

  ext : Extensionality lzero ℓ
  ext = Eq.good-ext ext₀

  lemma :
    (natrec₀ : Natrec ℓ)
    (P : ℕ → Type ℓ) (z : P zero) (s : ∀ n → P n → P (suc n))
    (natrec : ∀ n → P n) →

    natrec ≡ proj₁ (natrec₀ P z s)

      ↠

    (natrec zero ≡ z
       ×
     ∀ n → natrec (suc n) ≡ s n (natrec n))

  lemma natrec₀ P z s natrec = record
    { logical-equivalence = record
      { to   = λ eq →
                   (natrec zero      ≡⟨ cong (_$ zero) eq ⟩
                    rec₀ P z s zero  ≡⟨ nz₀ P z s ⟩∎
                    z                ∎)
                 , λ n →
                     natrec (suc n)      ≡⟨ cong (_$ suc n) eq ⟩
                     rec₀ P z s (suc n)  ≡⟨ ns₀ P z s n ⟩
                     s n (rec₀ P z s n)  ≡⟨ sym $ cong (s n) $ cong (_$ n) eq ⟩∎
                     s n (natrec n)      ∎
      ; from = λ { (nz , ns) → apply-ext ext $
                     lower ∘
                     rec₀ (λ n → ↑ ℓ (natrec n ≡ rec₀ P z s n))
                       (lift (
                          natrec zero      ≡⟨ nz ⟩
                          z                ≡⟨ sym $ nz₀ P z s ⟩∎
                          rec₀ P z s zero  ∎))
                       (λ n ih → lift (
                          natrec (suc n)      ≡⟨ ns n ⟩
                          s n (natrec n)      ≡⟨ cong (s n) (lower ih) ⟩
                          s n (rec₀ P z s n)  ≡⟨ sym $ ns₀ P z s n ⟩∎
                          rec₀ P z s (suc n)  ∎))
                 }
      }
    ; right-inverse-of = λ { (nz , ns) →
          let f = lower ∘
                  rec₀ _
                    (lift (trans nz (sym $ nz₀ P z s)))
                    (λ n ih →
                       lift (trans (ns n)
                               (trans (cong (s n) (lower ih))
                                  (sym $ ns₀ P z s n)))) in

          _↔_.to ≡×≡↔≡
            ( (trans (cong (_$ zero) (apply-ext ext f)) (nz₀ P z s)  ≡⟨ cong (flip trans (nz₀ P z s)) $ Eq.cong-good-ext ext₀ f ⟩
               trans (f zero) (nz₀ P z s)                            ≡⟨ cong (flip trans (nz₀ P z s) ∘ lower) $ nz₀ _ _ _ ⟩
               trans (trans nz (sym $ nz₀ P z s)) (nz₀ P z s)        ≡⟨ trans-[trans-sym]- _ (nz₀ P z s) ⟩∎
               nz                                                    ∎)

            , apply-ext ext λ n →
                trans
                  (cong (_$ suc n) (apply-ext ext f))
                  (trans (ns₀ P z s n)
                     (sym $ cong (s n) $ cong (_$ n) (apply-ext ext f)))     ≡⟨ cong₂ (λ p q → trans p (trans (ns₀ P z s n) (sym $ cong (s n) q)))
                                                                                (Eq.cong-good-ext ext₀ f) (Eq.cong-good-ext ext₀ f) ⟩
                trans
                  (f (suc n))
                  (trans (ns₀ P z s n) (sym $ cong (s n) (f n)))             ≡⟨ cong (flip trans (trans _ (sym $ cong (s n) (f n))) ∘ lower) $
                                                                                ns₀ _ _ _ _ ⟩
                trans
                  (trans (ns n)
                     (trans (cong (s n) (f n))
                        (sym $ ns₀ P z s n)))
                  (trans (ns₀ P z s n) (sym $ cong (s n) (f n)))             ≡⟨ cong (flip trans (trans _ (sym $ cong (s n) (f n)))) $
                                                                                sym $ trans-assoc _ _ (sym $ ns₀ P z s n) ⟩
                trans
                  (trans (trans (ns n) (cong (s n) (f n)))
                     (sym $ ns₀ P z s n))
                  (trans (ns₀ P z s n) (sym $ cong (s n) (f n)))             ≡⟨ sym $ trans-assoc _ _ (sym $ cong (s n) (f n)) ⟩

                trans
                  (trans (trans (trans (ns n) (cong (s n) (f n)))
                            (sym $ ns₀ P z s n))
                     (ns₀ P z s n))
                  (sym $ cong (s n) (f n))                                   ≡⟨ cong (flip trans (sym $ cong (s n) (f n))) $
                                                                                trans-[trans-sym]- _ (ns₀ P z s n) ⟩
                trans
                  (trans (ns n) (cong (s n) (f n)))
                  (sym $ cong (s n) (f n))                                   ≡⟨ trans-[trans]-sym _ (cong (s n) (f n)) ⟩∎

                ns n                                                         ∎
            )
        }
    }
    where
    rec₀ : (P : ℕ → Type ℓ) (z : P zero) (s : ∀ n → P n → P (suc n)) →
           ∀ n → P n
    rec₀ P z s = proj₁ (natrec₀ P z s)

    nz₀ : (P : ℕ → Type ℓ) (z : P zero) (s : ∀ n → P n → P (suc n)) →
          rec₀ P z s zero ≡ z
    nz₀ P z s = proj₁ (proj₂ (natrec₀ P z s))

    ns₀ : (P : ℕ → Type ℓ) (z : P zero) (s : ∀ n → P n → P (suc n)) →
          ∀ n → rec₀ P z s (suc n) ≡ s n (rec₀ P z s n)
    ns₀ P z s = proj₂ (proj₂ (natrec₀ P z s))

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --allow-unsolved-metas #-}
module turing where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Nat -- hiding ( erase )
open import Data.List
open import Data.Maybe hiding ( map )
-- open import Data.Bool using ( Bool ; true ; false ) renaming ( not to negate )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Product hiding ( map )
open import logic

data Write   (  Σ : Set  ) : Set  where
   write   : Σ → Write  Σ
   wnone   : Write  Σ
   --   erase write tnone

data Move : Set  where
   left   : Move
   right  : Move
   mnone  : Move

-- at tδ both stack is poped

-- write S      push S  , push SR
-- erase        push SL , push tone
-- none         push SL , push SR
-- left         push SR , pop
-- right        pop     , push SL

{-# TERMINATING #-}
move : {Q Σ : Set } → { tnone : Σ} → {tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move } → (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
move {Q} {Σ} {tnone} {tδ} q L [] = move {Q} {Σ} {tnone} {tδ} q  L  ( tnone  ∷ [] )
move {Q} {Σ} {tnone} {tδ} q [] R = move {Q} {Σ} {tnone} {tδ} q  ( tnone  ∷ [] )  R
move {Q} {Σ} {tnone} {tδ} q ( LH  ∷ LT ) ( RH ∷ RT ) with  tδ q LH
... | nq , write x , left  = ( nq , ( RH ∷ x  ∷ LT ) , RT )
... | nq , write x , right = ( nq , LT , ( x  ∷ RH  ∷ RT ) )
... | nq , write x , mnone = ( nq , ( x  ∷ LT ) , (  RH ∷ RT ) )
... | nq , wnone , left    = ( nq , ( RH  ∷ LH  ∷ LT ) , RT  )
... | nq , wnone , right   = ( nq ,  LT , ( LH  ∷ RH  ∷ RT ) )
... | nq , wnone , mnone   = ( nq , ( LH  ∷ LT ) , (  RH ∷ RT )  )
{-# TERMINATING #-}
move-loop : {Q Σ : Set } → {tend :  Q → Bool}  → { tnone : Σ} → {tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move }
    → (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
move-loop {Q} {Σ} {tend} {tnone} {tδ}  q L R with tend q
... | true = ( q , L , R )
... | flase = move-loop {Q} {Σ} {tend} {tnone} {tδ} ( proj₁ next ) ( proj₁ ( proj₂ next ) )  ( proj₂  ( proj₂ next ) )
        where
        next = move {Q} {Σ} {tnone} {tδ} q  L  R

{-# TERMINATING #-}
move0 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move)
   (q : Q ) ( L : List  Σ ) ( L : List   Σ ) → ( Q × List  Σ × List  Σ )
move0 tend tnone tδ  q L R with tend q
... | true = ( q , L , R )
move0 tend tnone tδ  q L [] | false = move0 tend tnone tδ  q  L  ( tnone  ∷ [] )
move0 tend tnone tδ  q [] R | false = move0 tend tnone tδ  q  ( tnone  ∷ [] )  R
move0 tend tnone tδ  q ( LH  ∷ LT ) ( RH ∷ RT ) | false with  tδ q LH
... | nq , write x , left  = move0 tend tnone tδ  nq ( RH ∷ x  ∷ LT ) RT
... | nq , write x , right = move0 tend tnone tδ  nq LT ( x  ∷ RH  ∷ RT )
... | nq , write x , mnone = move0 tend tnone tδ  nq ( x  ∷ LT ) (  RH ∷ RT )
... | nq , wnone , left    = move0 tend tnone tδ  nq ( RH  ∷ LH  ∷ LT ) RT
... | nq , wnone , right   = move0 tend tnone tδ  nq  LT ( LH  ∷ RH  ∷ RT )
... | nq , wnone , mnone   = move0 tend tnone tδ  nq ( LH  ∷ LT ) (  RH ∷ RT )

record Turing ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
        tδ : Q →  Σ → Q × ( Write  Σ ) ×  Move
        tstart : Q
        tend : Q → Bool
        tnone :  Σ
    taccept : List  Σ → ( Q × List  Σ × List  Σ )
    taccept L = move0 tend tnone tδ tstart L []

open import automaton
open Automaton

{-# TERMINATING #-}
move1 : {Q Σ : Set } ( tend : Q → Bool ) (tnone : Σ ) (δ : Q →  Σ → Q ) (tδ : Q → Σ →  Write  Σ  ×  Move)
   (q : Q ) ( L : List  Σ ) ( R : List   Σ ) →  Q × List  Σ × List  Σ
move1 tend tnone δ tδ  q L R with tend q
... | true = ( q , L , R )
move1 tend tnone δ tδ  q L [] | false = move1 tend tnone δ tδ  q  L  ( tnone  ∷ [] )
move1 tend tnone δ tδ  q [] R | false = move1 tend tnone δ tδ  q  ( tnone  ∷ [] )  R
move1 tend tnone δ tδ  q ( LH  ∷ LT ) ( RH ∷ RT ) | false with tδ (δ q LH) LH
... |  write x , left  = move1 tend tnone δ tδ  (δ q LH) ( RH ∷ x  ∷ LT ) RT
... |  write x , right = move1 tend tnone δ tδ  (δ q LH) LT ( x  ∷ RH  ∷ RT )
... |  write x , mnone = move1 tend tnone δ tδ  (δ q LH) ( x  ∷ LT ) (  RH ∷ RT )
... |  wnone , left    = move1 tend tnone δ tδ  (δ q LH) ( RH  ∷ LH  ∷ LT ) RT
... |  wnone , right   = move1 tend tnone δ tδ  (δ q LH)  LT ( LH  ∷ RH  ∷ RT )
... |  wnone , mnone   = move1 tend tnone δ tδ  (δ q LH) ( LH  ∷ LT ) (  RH ∷ RT )

record TM ( Q : Set ) ( Σ : Set  )
       : Set  where
    field
        automaton : Automaton  Q Σ
        tδ : Q → Σ → Write  Σ  ×  Move
        tnone :  Σ
    taccept : Q → List  Σ → ( Q × List  Σ × List  Σ )
    taccept q L = move1 (aend automaton) tnone (δ automaton) tδ q L []

data CopyStates : Set where
   s1 : CopyStates
   s2 : CopyStates
   s3 : CopyStates
   s4 : CopyStates
   s5 : CopyStates
   H  : CopyStates

Copyδ :  CopyStates →  ℕ  → CopyStates × ( Write  ℕ ) × Move
Copyδ s1 0  = H    , wnone       , mnone
Copyδ s1 1  = s2   , write 0 , right
Copyδ s2 0  = s3   , write 0 , right
Copyδ s2 1  = s2   , write 1 , right
Copyδ s3 0  = s4   , write 1 , left
Copyδ s3 1  = s3   , write 1 , right
Copyδ s4 0  = s5   , write 0 , left
Copyδ s4 1  = s4   , write 1 , left
Copyδ s5 0  = s1   , write 1 , right
Copyδ s5 1  = s5   , write 1 , left
Copyδ H  _  = H    , wnone   , mnone
Copyδ _  (suc (suc _))      = H    , wnone       , mnone

copyMachine : Turing CopyStates ℕ
copyMachine = record {
        tδ = Copyδ
     ;  tstart = s1
     ;  tend = tend
     ;  tnone =  0
  } where
      tend : CopyStates →  Bool
      tend H = true
      tend _ = false

copyTM : TM CopyStates ℕ
copyTM = record {
        automaton = record { δ = λ q i → proj₁ (Copyδ q i) ; aend = tend }
     ;  tδ = λ q i → proj₂ (Copyδ q i )
     ;  tnone =  0
  } where
      tend : CopyStates →  Bool
      tend H = true
      tend _ = false

test1 : CopyStates × ( List  ℕ ) × ( List  ℕ )
test1 = Turing.taccept copyMachine  ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  )

test2 : ℕ  → CopyStates × ( List  ℕ ) × ( List  ℕ )
test2 n  = loop n (Turing.tstart copyMachine) ( 1  ∷ 1  ∷ 0  ∷ 0  ∷  0 ∷ []  ) []
  where
        loop :  ℕ → CopyStates → ( List  ℕ ) → ( List  ℕ ) → CopyStates × ( List  ℕ ) × ( List  ℕ )
        loop zero q L R = ( q , L , R )
        loop (suc n) q L R = loop n ( proj₁ t1 ) ( proj₁ ( proj₂ t1 ) )  ( proj₂  ( proj₂ t1 ) )
          where
              t1 = move {CopyStates} {ℕ} {0} {Copyδ} q L R

-- testn = map (\ n -> test2 n) ( 0 ∷  1 ∷  2 ∷  3 ∷  4 ∷  5 ∷  6 ∷  [] )

testn : ℕ →  List ( CopyStates × ( List  ℕ ) × ( List  ℕ ) )
testn 0 = test2 0 ∷ []
testn (suc n)  = test2 n ∷ testn n

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda