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

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Function.Base using (_∋_; _$_)
open import Cubical.Data.Sigma renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.HITs.PropositionalTruncation.Base -- ∣_∣
import Cubical.HITs.PropositionalTruncation.Properties as PTrunc
open import Cubical.Foundations.Logic renaming
  ( inl to inlᵖ
  ; inr to inrᵖ
  ; _⇒_ to infixr 0 _⇒_                  -- shifting by -6
  ; _⇔_ to infixr -2 _⇔_                 --
  ; ∃[]-syntax  to infix -4 ∃[]-syntax   --
  ; ∃[∶]-syntax to infix -4 ∃[∶]-syntax  --
  ; ∀[∶]-syntax to infix -4 ∀[∶]-syntax  --
  ; ∀[]-syntax  to infix -4 ∀[]-syntax   --
  )

open import Utils
open import MoreLogic.Reasoning
open import MoreLogic.Definitions renaming
  ( _ᵗ⇒_ to infixr 0 _ᵗ⇒_
  ; ∀ᵖ[∶]-syntax  to infix -4 ∀ᵖ[∶]-syntax
  ; ∀ᵖ〚∶〛-syntax  to infix -4 ∀ᵖ〚∶〛-syntax
  ; ∀ᵖ!〚∶〛-syntax to infix -4 ∀ᵖ!〚∶〛-syntax
  ; ∀〚∶〛-syntax   to infix -4 ∀〚∶〛-syntax
  ; Σᵖ[]-syntax   to infix -4 Σᵖ[]-syntax
  ; Σᵖ[∶]-syntax  to infix -4 Σᵖ[∶]-syntax
  ) hiding (≡ˢ-syntax)
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Consequences
open import MorePropAlgebra.Bundles

module MorePropAlgebra.Properties.AlmostPartiallyOrderedField {ℓ} {ℓ'} (assumptions : AlmostPartiallyOrderedField {ℓ} {ℓ'})
  (let F = AlmostPartiallyOrderedField.Carrier assumptions
       _≡ˢ_ = λ(x y : F) → MoreLogic.Definitions.≡ˢ-syntax x y {AlmostPartiallyOrderedField.is-set assumptions}
       infixl 4 _≡ˢ_
  ) where

import MorePropAlgebra.Properties.Group
module Group'Properties  = MorePropAlgebra.Properties.Group   record { AlmostPartiallyOrderedField assumptions ; is-Group = AlmostPartiallyOrderedField.+-Group assumptions }
module Group'            =                            Group   record { AlmostPartiallyOrderedField assumptions ; is-Group = AlmostPartiallyOrderedField.+-Group assumptions }
(      Group')           =                            Group ∋ record { AlmostPartiallyOrderedField assumptions ; is-Group = AlmostPartiallyOrderedField.+-Group assumptions }
module GroupLemmas'      = Group'Properties.GroupLemmas'

import MorePropAlgebra.Properties.Ring
module Ring'Properties  = MorePropAlgebra.Properties.Ring   record { AlmostPartiallyOrderedField assumptions }
module Ring'            =                            Ring   record { AlmostPartiallyOrderedField assumptions }
(      Ring')           =                            Ring ∋ record { AlmostPartiallyOrderedField assumptions }
module RingTheory'      = Ring'Properties.RingTheory'

open AlmostPartiallyOrderedField assumptions -- renaming (Carrier to F; _-_ to _-_)

-- Bridges' definition of _≤__
_≤''_ : hPropRel F F (ℓ-max ℓ ℓ')
x ≤'' y = ∀[ ε ] (y < ε) ⇒ (x < ε)
infixl 4 _≤''_

private
  -- infixl 4 _≡ˢ_
  -- _≡ˢ_ = λ(x y : F) → MoreLogic.Definitions.≡ˢ-syntax x y {is-set} -- [ is-set ] x ≡ˢ y

  ≡ˢ-sym : ∀ a b → [ (a ≡ˢ b) ⇔ (b ≡ˢ a) ]
  ≡ˢ-sym a b .fst a≡b = sym a≡b
  ≡ˢ-sym a b .snd b≡a = sym b≡a

  ≡ˢ-symᵗ : ∀ a b → (a ≡ˢ b) ≡ (b ≡ˢ a)
  ≡ˢ-symᵗ a b = let (p , q) = ≡ˢ-sym a b in ⇔toPath p q

abstract
  -dist' : ∀ a b → -(a + b) ≡ (- b) + (- a)
  -dist  : ∀ a b → -(a + b) ≡ (- a) + (- b)

  ·-inv#0 : ∀ x y → x · y ≡ 1f → [ (x # 0f) ⊓ (y # 0f) ]

  ·-reflects-≡ : (a b c : F) → [ c # 0f ⇒ (a · c ≡ˢ b · c) ⇒ (a ≡ˢ b) ]; _ : [ operation _·_ reflects _≡ˢ_ when (λ c → c # 0f) ]; _ = ·-reflects-≡

  ·-rinv-unique'' : (x y z : F) → [ x · y ≡ˢ 1f ] → [ x · z ≡ˢ 1f ] → [ y ≡ˢ z ]

  _⁻¹'' : ∀ x → {{[ x # 0f ]}} → Σ[ y ∈ F ] x · y ≡ 1f
  _⁻¹   : ∀ x → {{[ x # 0f ]}} → F
  infix  9 _⁻¹

  ·-rinv        : ∀ x                    → (p : [ x # 0f ]) → [ x · (x ⁻¹) {{p}} ≡ˢ 1f ]
  ·-linv        : ∀ x                    → (p : [ x # 0f ]) → [ (x ⁻¹) {{p}} · x ≡ˢ 1f ]
  ·-linv-unique : (x y : F) → x · y ≡ 1f → (p : [ y # 0f ]) → x ≡ (y ⁻¹) {{p}}

  <-≤-trans    : ∀ x y z → [ x < y ⇒ y ≤ z ⇒ x < z ]
  ≤-<-trans    : ∀ x y z → [ x ≤ y ⇒ y < z ⇒ x < z ]
  ≤-⇔-≤''      : ∀ x y   → [  (x ≤ y) ⇔ (x ≤'' y)  ]
  ≤-reflects-≡ : ∀ x y   → [ (∀[ z ] z ≤ x ⇔ z ≤ y) ⇔ x ≡ˢ y ]

  -dist' a b = GroupLemmas'.invDistr a b
  -dist  a b = -dist' a b ∙ +-comm _ _

  ·-inv#0 x y x·y≡1 .fst = ·-inv'' x .fst ∣ (y ,              x·y≡1) ∣
  ·-inv#0 x y x·y≡1 .snd = ·-inv'' y .fst ∣ (x , ·-comm y x ∙ x·y≡1) ∣

  ·-reflects-≡ a b c p = PTrunc.rec (isProp[] ((a · c ≡ˢ b · c) ⇒ (a ≡ˢ b) )) γ (·-inv'' c .snd p) where
    γ : Σ[ c⁻¹ ∈ F ] [ c · c⁻¹ ≡ˢ 1f ] → [ (a · c ≡ˢ b · c) ⇒ a ≡ˢ b ]
    γ (c⁻¹ , c·c⁻¹≡1) a·c≡b·c =
       a              ≡⟨ sym (fst (·-identity a)) ∙ cong (a ·_) (sym c·c⁻¹≡1) ∙ ·-assoc _ _ _ ⟩
      (a · c) · (c⁻¹) ≡⟨ cong (_· c⁻¹) a·c≡b·c ⟩
      (b · c) · (c⁻¹) ≡⟨ sym (·-assoc _ _ _) ∙ cong (b ·_) c·c⁻¹≡1 ∙ fst (·-identity b)  ⟩
       b ∎

  -- uniqueness of inverses from `·-assoc` + `·-comm` + `·-lid` + `·-rid`
  ·-rinv-unique'' x y z x·y≡1 x·z≡1 =
    (      x  · y  ≡ˢ     1f ⇒ᵖ⟨ (λ x·y≡1 i → z · x·y≡1 i) ⟩
      z · (x  · y) ≡ˢ z · 1f ⇒ᵖ⟨ pathTo⇒ (λ i → ·-assoc z x y i ≡ˢ ·-rid z i) ⟩
     (z ·  x) · y  ≡ˢ z      ⇒ᵖ⟨ pathTo⇒ (λ i → (·-comm z x i) · y  ≡ˢ z) ⟩
     (x ·  z) · y  ≡ˢ z      ⇒ᵖ⟨ pathTo⇒ (λ i → x·z≡1 i · y  ≡ˢ z) ⟩
        1f    · y  ≡ˢ z      ⇒ᵖ⟨ pathTo⇒ (λ i → ·-lid y i ≡ˢ z) ⟩
                y  ≡ˢ z      ◼ᵖ) .snd x·y≡1

  -- inverse function from `·-rinv-unique''` and `∀[ x ] (∃[ y ] x · y ≡ˢ 1f) ⇔ x # 0f`
  (x ⁻¹'') {{x#0f}} = PTrunc.rec γ (λ p → p) (·-inv'' x .snd x#0f) where
     γ : isProp (Σ[ y ∈ F ] x · y ≡ 1f)
     γ (a , x·a≡1) (b , x·b≡1) = let a≡b = ·-rinv-unique'' x a b x·a≡1 x·b≡1
                                 in Σ≡Prop (λ c → isProp[] (x · c ≡ˢ 1f)) a≡b

  (x ⁻¹) {{p}} = (x ⁻¹'') .fst

  ·-rinv x p = (x ⁻¹'') {{p}} .snd

  ·-linv x p = ·-comm _ _ ∙ ·-rinv x p

  ·-linv-unique x y x·y≡1 p = sym $ ·-rinv-unique'' y ((y ⁻¹) {{p}}) x (·-rinv y p) (·-comm _ _ ∙ x·y≡1)

  <-≤-trans x y z x<y y≤z = ⊔-elim (x < z) (z < y) (λ _ → x < z) (λ x<z → x<z) (λ z<y → ⊥-elim (y≤z z<y)) (<-cotrans _ _ x<y z)
  ≤-<-trans x y z x≤y y<z = ⊔-elim (y < x) (x < z) (λ _ → x < z) (λ y<x → ⊥-elim (x≤y y<x)) (λ x<z → x<z) (<-cotrans y z y<z x)

  -- Booij's _≤_ ⇔ Brigdes' _≤''_
  ≤-⇔-≤'' x y .fst x≤y ε y<ε = ≤-<-trans x y ε x≤y y<ε
  ≤-⇔-≤'' x y .snd x≤''y y<x = <-irrefl x (x≤''y x y<x)

  ≤-reflects-≡ x y .fst z≤x⇔z≤y = ≤-antisym x y (z≤x⇔z≤y x .fst (≤-refl x)) (z≤x⇔z≤y y .snd (≤-refl y))
  ≤-reflects-≡ x y .snd x≡y z .fst = subst (λ p → [ z ≤ p ]) x≡y
  ≤-reflects-≡ x y .snd x≡y z .snd = subst (λ p → [ z ≤ p ]) (sym x≡y)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
data ⊤ : Set where tt : ⊤

postulate
  A : Set
  B : A → Set
  a : A
  b : B a
  G : ∀ x → B x → Set

postulate tt' : ⊤

poo : G a b
poo with tt | a
... | _ | _ = {!!}

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --universe-polymorphism #-}
-- {-# OPTIONS --verbose tc.rec:15 #-}
-- {-# OPTIONS --verbose tc.records.ifs:15 #-}
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}
-- {-# OPTIONS --verbose tc.term.args.ifs:15 #-}

module 05-equality-std2 where

open import Relation.Binary
open import Data.Bool hiding (_≟_)

open DecSetoid {{...}}

test = isDecEquivalence
test2 = false ≟ false

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-

This file contains:

- Natural functions from FreeGroupoid into FreeGroupoid
- Proofs that they induce equivalences
- Natural paths in Universe from FreeGroupoid to FreeGroupoid
- Proofs that these functions and paths respect the groupoid structure of FreeGroupoid

-}
{-# OPTIONS --safe #-}

module Cubical.HITs.FreeGroupoid.GroupoidActions where

open import Cubical.HITs.FreeGroupoid.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.BiInvertible
open import Cubical.Foundations.Function

private
  variable
    ℓ : Level
    A : Type ℓ

-- A function for every element of FreeGroupoid A

action : ∀ (a : FreeGroupoid A) → FreeGroupoid A → FreeGroupoid A
action a g = g · a

invAction :  FreeGroupoid A → FreeGroupoid A → FreeGroupoid A
invAction a = action (inv a)

-- Naturality properties of the FreeGroupoid operations

multNaturality : (g1 g2 : FreeGroupoid A) → action (g1 · g2) ≡ (action g2 ∘ action g1)
multNaturality g1 g2 = funExt (pointwise g1 g2) where
  pointwise : (g1 g2 g3 : FreeGroupoid A) → action (g1 · g2) g3 ≡ (action g2 ∘ action g1) g3
  pointwise g1 g2 g3 =
    action (g1 · g2) g3
    ≡⟨ assoc g3 g1 g2 ⟩
    (action g2 ∘ action g1) g3 ∎

idNaturality : action ε ≡ idfun (FreeGroupoid A)
idNaturality = funExt pointwise where
  pointwise : (g : FreeGroupoid A) → action ε g ≡ idfun (FreeGroupoid A) g
  pointwise g =
    action ε g
    ≡⟨ sym (idr g) ⟩
    idfun _ g ∎

rCancelAction : ∀ (a : FreeGroupoid A) → action a ∘ invAction a ≡ idfun (FreeGroupoid A)
rCancelAction a =
  action a ∘ invAction a
  ≡⟨ sym (multNaturality (inv a) a) ⟩
  action ((inv a) · a)
  ≡⟨ cong action (invl a) ⟩
  action ε
  ≡⟨ idNaturality ⟩
  idfun _ ∎

lCancelAction : ∀ (a : FreeGroupoid A) → invAction a ∘ action a ≡ idfun (FreeGroupoid A)
lCancelAction a =
  invAction a ∘ action a
  ≡⟨ sym (multNaturality a (inv a)) ⟩
  action (a · (inv a))
  ≡⟨ cong action (invr a) ⟩
  action ε
  ≡⟨ idNaturality ⟩
  idfun _ ∎

-- Characterization of the action functions

actionCharacterization : ∀ (f : FreeGroupoid A → FreeGroupoid A)
      → (∀ g1 g2 → f (g1 · g2) ≡ g1 · (f g2))
      → Σ[ a ∈ FreeGroupoid A ] (f ≡ action a)
actionCharacterization f property = f ε , (funExt pointwise) where
  pointwise : ∀ g → f g ≡ action (f ε) g
  pointwise g =
    f g
    ≡⟨ cong f (idr g) ⟩
    f (g · ε)
    ≡⟨ property g ε ⟩
    action (f ε) g ∎

-- Actions induce equivalences

biInvAction : FreeGroupoid A → BiInvEquiv (FreeGroupoid A) (FreeGroupoid A)
biInvAction a = biInvEquiv (action a) (invAction a) (rhomotopy a) (invAction a) (lhomotopy a) where
  rhomotopy : ∀ a g → (action a ∘ invAction a) g ≡ g
  rhomotopy a g = cong (λ f → f g) (rCancelAction a)
  lhomotopy : ∀ a g → (invAction a ∘ action a) g ≡ g
  lhomotopy a g = cong (λ f → f g) (lCancelAction a)

equivs : FreeGroupoid A → (FreeGroupoid A) ≃ (FreeGroupoid A)
equivs a = biInvEquiv→Equiv-right (biInvAction a)

-- Naturality properties of the equivs group

multEquivsNaturality : ∀ (k1 k2 : FreeGroupoid A) → equivs (k1 · k2) ≡ compEquiv (equivs k1) (equivs k2)
multEquivsNaturality k1 k2 = equivEq h where
  h : (equivs (k1 · k2)) .fst ≡ (compEquiv (equivs k1) (equivs k2)) .fst
  h =
    equivs (k1 · k2) .fst
    ≡⟨ multNaturality k1 k2 ⟩
    compEquiv (equivs k1) (equivs k2) .fst ∎

idEquivsNaturality : equivs ε ≡ idEquiv (FreeGroupoid A)
idEquivsNaturality = equivEq h where
  h : (equivs ε) .fst ≡ idEquiv (FreeGroupoid A) .fst
  h =
    (equivs ε) .fst
    ≡⟨ idNaturality ⟩
    idEquiv _ .fst ∎

invEquivsNaturality : ∀ (g : FreeGroupoid A) → equivs (inv g) ≡ invEquiv (equivs g)
invEquivsNaturality g = equivEq refl

-- Actions induce paths in Universe

pathsInU : {A : Type ℓ} → FreeGroupoid A → (FreeGroupoid A) ≡ (FreeGroupoid A)
pathsInU a = ua (equivs a)

-- Naturality properties of the paths group

multPathsInUNaturality : ∀ (g1 g2 : FreeGroupoid A) → pathsInU (g1 · g2) ≡ (pathsInU g1) ∙ (pathsInU g2)
multPathsInUNaturality g1 g2 =
  pathsInU (g1 · g2)
  ≡⟨ cong ua (multEquivsNaturality g1 g2) ⟩
  ua (compEquiv (equivs g1) (equivs g2))
  ≡⟨ uaCompEquiv (equivs g1) (equivs g2) ⟩
  (pathsInU g1) ∙ (pathsInU g2) ∎

idPathsInUNaturality : pathsInU {A = A} ε ≡ refl
idPathsInUNaturality =
  pathsInU ε
  ≡⟨ cong ua idEquivsNaturality ⟩
  ua (idEquiv _)
  ≡⟨ uaIdEquiv ⟩
  refl ∎

invPathsInUNaturality : ∀ (g : FreeGroupoid A) → pathsInU (inv g) ≡ sym (pathsInU g)
invPathsInUNaturality g =
  pathsInU (inv g)
  ≡⟨ cong ua (invEquivsNaturality g) ⟩
  ua (invEquiv (equivs g))
  ≡⟨ uaInvEquiv (equivs g) ⟩
  sym (pathsInU g) ∎

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------------
-- ABP terms
------------------------------------------------------------------------------

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

module FOTC.Program.ABP.Terms where

open import FOTC.Base
open import FOTC.Base.Loop
open import FOTC.Data.Bool

------------------------------------------------------------------------------
-- N.B. We did not define @Bit = Bool@ due to the issue #11.
Bit : D → Set
Bit b = Bool b
{-# ATP definition Bit #-}

F T : D
F = false
T = true
{-# ATP definition F T #-}

postulate
  <_,_> : D → D → D
  ok    : D → D

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- An implementation of Olivier Danvy's Type-Directed Partial Evaluation (POPL 1996)
-- for STLC with sum types using continuations in form of shift and reset.
--
-- The algorithm was originally for a two-level lambda-calculus.

-- Our use of Kripke semantics makes the effect of fresh variable generation explicit and formal.

open import Library

module DanvyShiftReset where

data Base : Set where
  α β : Base

-- import Formulas   ; open module Form = Formulas    Base
-- import Derivations; open module Der  = Derivations Base
open import Formulas    Base
open import Derivations Base

-- -- Shift-reset continutation monad

-- record M (A B C : Set) : Set where
--   field run : (C → B) → A
-- open M

-- return : ∀{X A} → A → M X X A
-- return x .run k = k x

-- _>>=_ : ∀{X Y Z A B} (m : M X Y A) (f : A → M Y Z B) → M X Z B
-- (m >>= f) .run k = m .run λ a → f a .run k

-- _<$>_ : ∀{X Y A B} (f : A → B) (m : M X Y A) → M X Y B
-- (f <$> m) .run k = m .run (k ∘ f)

-- shift : ∀{X Y A} (f : (A → Y) → M X Y Y) → M X Y A
-- shift f .run k = f k .run id

-- shift' : ∀{X Y A} (f : (A → Y) → X) → M X Y A
-- shift' f .run k = f k

-- reset : ∀{X Y A} (m : M A Y Y) → M X X A
-- reset m .run k = k (m .run id)

-- Shift-reset continutation monad

record M (A B C : Cxt → Set) (Γ : Cxt) : Set where
  field run : KFun (KFun C B) A Γ
open M

return : ∀{X A} → □ A →̇ M X X A
return x .run τ k = k id≤ (x τ)

return' : ∀{X A} → □ A →̇ M X X (□ A)
return' x .run τ k = k id≤ λ τ₁ → x (τ₁ • τ)

_>>=_ : ∀{X Y Z A B Γ} (m : M X Y A Γ) (f : KFun A (M Y Z B) Γ) → M X Z B Γ
(m >>= f) .run σ k = m .run σ λ τ a → f (τ • σ) a .run id≤ λ τ′ → k (τ′ • τ)

_<$>_ : ∀{X Y A B} (f : A →̇ B) → M X Y A →̇ M X Y B
(f <$> m) .run σ k = m .run σ λ τ → k τ ∘ f

-- liftA2 : ∀{X Y A B C} (f : ∀{Γ} → A Γ → B Γ → C Γ) → ∀{Γ} → M X Y A Γ → M X Y B Γ → M X Y C Γ
-- liftA2 f ma mb .run σ k = ma .run σ λ τ a → {!mb .run!}

K$ : ∀{X Y A B} → KFun A B →̇ KFun (M X Y A) (M X Y B)
K$ f τ m .run σ k = m .run σ λ τ′ a →  k τ′ (f (τ′ • (σ • τ)) a)

shift' : ∀{X Y A Γ} (f : KFun (KFun A Y) X Γ) → M X Y A Γ
shift' f .run σ k = f σ k

shift : ∀{X Y A Γ} (f : KFun (KFun A Y) (M X Y Y) Γ) → M X Y A Γ
shift f .run σ k = f σ k .run id≤ λ τ → id

reset' : ∀{Y A} → M A Y Y →̇ A
reset' m = m .run id≤ λ τ → id

reset : ∀{X Y A} → M A Y Y →̇ M X X A
reset m .run σ k = k id≤ (m .run σ λ τ → id)

-- We use a continuation monad with answer type Nf.

M' : (X : Cxt → Set) (Γ : Cxt) → Set
M' X Γ = ∀ {C} → M (Nf' C) (Nf' C) X Γ

T⟦_⟧ : (A : Form) (Γ : Cxt) → Set
T⟦ Atom P ⟧ = Nf' (Atom P)
T⟦ True   ⟧ Γ = ⊤
T⟦ False  ⟧ Γ = ⊥
T⟦ A ∨ B  ⟧ Γ = T⟦ A ⟧ Γ ⊎ T⟦ B ⟧ Γ
T⟦ A ∧ B  ⟧ Γ = T⟦ A ⟧ Γ × T⟦ B ⟧ Γ
T⟦ A ⇒ B  ⟧ Γ = ∀{Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Δ → M' T⟦ B ⟧ Δ

-- Monotonicity of the model is proven by induction on the proposition.

-- monT : ∀ A {Γ Δ} (τ : Δ ≤ Γ) → T⟦ A ⟧ Γ → T⟦ A ⟧ Δ

monT : ∀ A → Mon T⟦ A ⟧
monT (Atom P) = monNf
monT True     = _
monT False  τ ()
monT (A ∨ B) τ = map-⊎ (monT A τ) (monT B τ)
monT (A ∧ B) τ (a , b) = monT A τ a , monT B τ b
monT (A ⇒ B) τ f σ = f (σ • τ)

-- Reflection / reification, proven simultaneously by induction on the proposition.

-- Reflection is η-expansion (and recursively reflection);

mutual

  reflect : ∀{Γ} A (t : Ne Γ A) → M' T⟦ A ⟧ Γ
  reflect (Atom P) t = return λ τ → ne (monNe τ t)
  reflect True     t = return _
  reflect False    t = shift' λ τ k → falseE (monNe τ t)
  reflect (A ∨ B)  t = shift' λ τ k → orE (monNe τ t)
    (reset' (K$ k (weak id≤) (inj₁ <$> reflect A (hyp top))))
    (reset' (K$ k (weak id≤) (inj₂ <$> reflect B (hyp top))))

    -- ((inj₂ <$> reflect B (hyp top)) .run λ τ → k (τ • weak id≤))
    -- Wrong:
    --     (reset' (k (weak id≤) <$> (inj₁ <$> reflect A (hyp top))))

  -- reflect (A ∧ B) t = do
  --   a ← reflect A (andE₁ t)
  --   b ← reflect B (andE₂ t)
  --   return (a , b)

  reflect (A ∧ B) t =
    reflect A (andE₁ t          ) >>= λ τ a →
    reflect B (andE₂ (monNe τ t)) >>= λ τ′ b →
    return λ τ₁ → monT A (τ₁ • τ′) a , monT B τ₁ b

  reflect (A ⇒ B)  t = return' λ τ a → reflect B (impE (monNe τ t) (reify A a))

  reify : ∀{Γ} A (⟦f⟧ : T⟦ A ⟧ Γ) → Nf Γ A

  reify (Atom P) t      = t
  reify True _          = trueI
  reify False   ()
  reify (A ∨ B) (inj₁ a) = orI₁ (reify A a)
  reify (A ∨ B) (inj₂ b) = orI₂ (reify B b)
  reify (A ∧ B) (a , b) = andI (reify A a) (reify B b)

  reify (A ⇒ B) f     = impI $ reset' $
    reflect A (hyp top) >>= λ τ a →
    reify B <$> f (τ • weak id≤) a

-- Fundamental theorem

-- Extension of T⟦_⟧ to contexts

G⟦_⟧ : ∀ (Γ Δ : Cxt) → Set
G⟦ ε     ⟧ Δ = ⊤
G⟦ Γ ∙ A ⟧ Δ = G⟦ Γ ⟧ Δ × T⟦ A ⟧ Δ

-- monG : ∀{Γ Δ Φ} (τ : Φ ≤ Δ) → G⟦ Γ ⟧ Δ → G⟦ Γ ⟧ Φ

monG : ∀{Γ} → Mon G⟦ Γ ⟧
monG {ε} τ _ = _
monG {Γ ∙ A} τ (γ , a) = monG τ γ , monT A τ a

-- Variable case.

fundH : ∀{Γ Δ A} (x : Hyp A Γ) (γ : G⟦ Γ ⟧ Δ) → T⟦ A ⟧ Δ
fundH top     = proj₂
fundH (pop x) = fundH x ∘ proj₁

-- The fundamental theorem:
-- A call-by-value interpreter.

fund :  ∀{Γ A} (t : Γ ⊢ A) {Δ} (γ : G⟦ Γ ⟧ Δ) → M' T⟦ A ⟧ Δ

fund (hyp {A} x) γ = return λ τ → monT A τ (fundH x γ)
fund (impI t)    γ = return' λ τ a → fund t (monG τ γ , a)

fund (impE t u)  γ =
  fund t γ          >>= λ τ f →
  fund u (monG τ γ) >>= λ τ′ a →
  f τ′ a

fund (andI {A} {B} t u) γ =
  fund t γ >>= λ τ a →
  fund u (monG τ γ) >>= λ τ′ b →
  return λ τ₁ → monT A (τ₁ • τ′) a , monT B τ₁ b

fund (andE₁ t)    γ = proj₁ <$> fund t γ
fund (andE₂ t)    γ = proj₂ <$> fund t γ
fund (orI₁ t)     γ = inj₁  <$> fund t γ
fund (orI₂ t)     γ = inj₂  <$> fund t γ

fund (orE t u v) γ = fund t γ >>= λ τ →
  [ (λ a → fund u (monG τ γ , a))
  , (λ b → fund v (monG τ γ , b))
  ]

fund (falseE t)  γ = fund t γ >>= λ τ ()
fund trueI       γ = return _

-- Identity environment

ide : ∀ Γ → □ (M' G⟦ Γ ⟧) Γ
ide ε       τ = return _
ide (Γ ∙ A) τ =
  ide Γ (τ • weak id≤)                >>= λ τ₁ γ →
  reflect A (monNe (τ₁ • τ) (hyp top)) >>= λ τ₂ a →
  return λ τ₃ → monG (τ₃ • τ₂) γ , monT A τ₃ a

-- Normalization

norm : ∀{A Γ} (t : Γ ⊢ A) → Nf Γ A
norm {A} {Γ} t = reset' $
  ide Γ id≤ >>= λ _ γ →
  reify A <$> fund t γ

idD : (A : Form) → ε ⊢ (A ⇒ A)
idD A = impI (hyp top)

test : let A = Atom α; B = Atom β in Nf ε (A ∨ B ⇒ A ∨ B)
test = norm (idD (Atom α ∨ Atom β))

test2 = norm (idD (Atom α ∨ Atom β ∨ Atom α))

-- Q.E.D. -}
-- -}
-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
data C : Set₁ where
  c : Set → C

data D : Set where
  d : D

F : C → {y : D} → C → Set₁
F z (c _) = G d
  module M where
  G : D → Set₁
  G _ = Set

fail : Set
fail = M.G

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT renaming (pt to ⊙pt)
open import homotopy.Bouquet
open import homotopy.FinWedge
open import homotopy.LoopSpaceCircle
open import homotopy.SphereEndomorphism
open import groups.SphereEndomorphism
open import cw.CW
open import cw.FinCW
open import cw.WedgeOfCells
open import cw.DegreeByProjection {lzero}
open import homotopy.DisjointlyPointedSet
open import cohomology.Theory

module cw.cohomology.cochainequiv.FirstCoboundaryAbstractDefs (OT : OrdinaryTheory lzero)
  (⊙fin-skel : ⊙FinSkeleton 1) where

open OrdinaryTheory OT
open import cohomology.Bouquet OT

private
  ⊙skel = ⊙FinSkeleton-realize ⊙fin-skel
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel
  skel = ⊙Skeleton.skel ⊙skel
  dec = FinSkeleton-has-cells-with-dec-eq fin-skel

  endpoint = attaching-last skel
  I₋₁ = AttachedFinSkeleton.skel fin-skel
  ⊙head = ⊙cw-head ⊙skel
  pt = ⊙pt ⊙head

open import cw.cohomology.reconstructed.TipCoboundary OT ⊙skel

⊙head-is-separable : is-separable ⊙head
⊙head-is-separable = Fin-has-dec-eq pt

⊙head-separate = separate-pt ⊙head-is-separable

⊙head-separate-equiv = (unite-pt ⊙head , separable-has-disjoint-pt ⊙head-is-separable)⁻¹

MinusPoint-⊙head-has-choice : has-choice 0 (MinusPoint ⊙head) lzero
MinusPoint-⊙head-has-choice = MinusPoint-has-choice ⊙head-is-separable (Fin-has-choice 0 lzero)

MinusPoint-⊙head-has-dec-eq : has-dec-eq (MinusPoint ⊙head)
MinusPoint-⊙head-has-dec-eq = MinusPoint-has-dec-eq Fin-has-dec-eq

⊙function₀ : ⊙FinBouquet I 1 ⊙→ ⊙Susp (⊙Bouquet (MinusPoint ⊙head) 0)
⊙function₀ = ⊙Susp-fmap (⊙<– (Bouquet-⊙equiv-X ⊙head-is-separable))
          ⊙∘ ⊙cw-∂-head'-before-Susp
          ⊙∘ ⊙–> (Bouquet-⊙equiv-Xₙ/Xₙ₋₁ skel)

function₁ : Fin I → MinusPoint ⊙head → Sphere-endo 0
function₁ <I b x with Fin-has-dec-eq (fst b) (endpoint <I x)
function₁ <I b x | inl _ = false
function₁ <I b x | inr _ = true

abstract
  ⊙function₀' : ⊙FinBouquet I 1 ⊙→ ⊙Susp (⊙Bouquet (MinusPoint ⊙head) 0)
  ⊙function₀' = ⊙function₀

  ⊙function₀'-β : ⊙function₀' == ⊙function₀
  ⊙function₀'-β = idp

  function₁' : Fin I → MinusPoint ⊙head → Sphere-endo 0
  function₁' = function₁

  function₁'-β : ∀ <I b → function₁' <I b == function₁ <I b
  function₁'-β _ _ = idp

  private
    mega-reduction-cases : ∀ <I b x
      →  bwproj MinusPoint-⊙head-has-dec-eq b (<– (Bouquet-equiv-X ⊙head-is-separable) (endpoint <I x))
      == function₁ <I b x
    mega-reduction-cases <I b x with Fin-has-dec-eq pt (endpoint <I x)
    mega-reduction-cases <I b x | inl _ with Fin-has-dec-eq (fst b) (endpoint <I x)
    mega-reduction-cases <I b x | inl pt=end | inl b=end = ⊥-rec (snd b (pt=end ∙ ! b=end))
    mega-reduction-cases <I b x | inl _ | inr _ = idp
    mega-reduction-cases <I b x | inr _ with Fin-has-dec-eq (fst b) (endpoint <I x)
    mega-reduction-cases <I b x | inr _ | inl b=end =
      bwproj MinusPoint-⊙head-has-dec-eq b (bwin (endpoint <I x , _) false)
        =⟨ ap (λ b' → bwproj MinusPoint-⊙head-has-dec-eq b (bwin b' false)) $ ! $
            Subtype=-out (MinusPoint-prop ⊙head) b=end ⟩
      bwproj MinusPoint-⊙head-has-dec-eq b (bwin b false)
        =⟨ bwproj-bwin-diag MinusPoint-⊙head-has-dec-eq b false ⟩
      false
        =∎
    mega-reduction-cases <I b x | inr _ | inr b≠end =
      bwproj-bwin-≠ MinusPoint-⊙head-has-dec-eq (b≠end ∘ ap fst) false

  mega-reduction : ∀ <I b →
      Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b) ∘ fst ⊙function₀' ∘ fwin <I
    ∼ Susp-fmap (function₁' <I b)
  mega-reduction <I b = Susp-elim idp idp λ x → ↓-='-in' $ ! $
    ap (Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b) ∘ fst ⊙function₀ ∘ fwin <I) (merid x)
      =⟨ ap-∘
          ( Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b)
          ∘ Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable))
          ∘ cw-∂-head'-before-Susp)
          (Bouquet-to-Xₙ/Xₙ₋₁ skel ∘ fwin <I)
          (merid x) ⟩
    ap ( Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b)
       ∘ Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable))
       ∘ cw-∂-head'-before-Susp)
       (ap (Bouquet-to-Xₙ/Xₙ₋₁ skel ∘ fwin <I) (merid x))
      =⟨ ap (ap ( Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b)
                ∘ Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable))
                ∘ cw-∂-head'-before-Susp))
            (Bouquet-to-Xₙ/Xₙ₋₁-in-merid-β skel <I x) ⟩
    ap ( Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b)
       ∘ Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable))
       ∘ cw-∂-head'-before-Susp)
       (cfglue (endpoint <I x) ∙' ap cfcod (spoke <I x))
      =⟨ ap-∘
          ( Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b)
          ∘ Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable)))
          cw-∂-head'-before-Susp
          (cfglue (endpoint <I x) ∙' ap cfcod (spoke <I x)) ⟩
    ap ( Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b)
       ∘ Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable)))
       (ap cw-∂-head'-before-Susp
         (cfglue (endpoint <I x) ∙' ap cfcod (spoke <I x)))
      =⟨ ap (ap ( Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b)
                ∘ Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable))))
            ( ap-∙' cw-∂-head'-before-Susp (cfglue (endpoint <I x)) (ap cfcod (spoke <I x))
            ∙ ap2 _∙'_
                (cw-∂-head'-before-Susp-glue-β (endpoint <I x))
                ( ∘-ap cw-∂-head'-before-Susp cfcod (spoke <I x)
                ∙ ap-cst south (spoke <I x))) ⟩
    ap ( Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b)
       ∘ Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable)))
       (merid (endpoint <I x))
      =⟨ ap-∘
          (Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b))
          (Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable)))
          (merid (endpoint <I x)) ⟩
    ap (Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b))
       (ap (Susp-fmap (<– (Bouquet-equiv-X ⊙head-is-separable)))
           (merid (endpoint <I x)))
      =⟨ ap
          (ap (Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b)))
          (SuspFmap.merid-β
            (<– (Bouquet-equiv-X ⊙head-is-separable))
            (endpoint <I x)) ⟩
    ap (Susp-fmap (bwproj MinusPoint-⊙head-has-dec-eq b))
       (merid (<– (Bouquet-equiv-X ⊙head-is-separable) (endpoint <I x)))
      =⟨ SuspFmap.merid-β (bwproj MinusPoint-⊙head-has-dec-eq b)
          (<– (Bouquet-equiv-X ⊙head-is-separable) (endpoint <I x)) ⟩
    merid (bwproj MinusPoint-⊙head-has-dec-eq b (<– (Bouquet-equiv-X ⊙head-is-separable) (endpoint <I x)))
      =⟨ ap merid (mega-reduction-cases <I b x) ⟩
    merid (function₁ <I b x)
      =⟨ ! $ SuspFmap.merid-β (function₁ <I b) x ⟩
    ap (Susp-fmap (function₁ <I b)) (merid x)
      =∎

  open DegreeAtOne skel dec

  degree-matches' : ∀ <I b
    →  merid (function₁' <I b false) ∙ ! (merid (function₁' <I b true))
    == loop^ (degree <I (fst b))
  degree-matches' <I b with Fin-has-dec-eq (fst b) (endpoint <I false)
  degree-matches' <I b | inl _ with Fin-has-dec-eq (fst b) (endpoint <I true)
  degree-matches' <I b | inl _ | inl _ = !-inv-r (merid false)
  degree-matches' <I b | inl _ | inr _ = idp
  degree-matches' <I b | inr _ with Fin-has-dec-eq (fst b) (endpoint <I true)
  degree-matches' <I b | inr _ | inl _ = ap (_∙ ! (merid false)) (! (!-! (merid true))) ∙ ∙-! (! (merid true)) (merid false)
  degree-matches' <I b | inr _ | inr _ = !-inv-r (merid true)

  degree-matches : ∀ <I b
    →  ⊙SphereS-endo-degree 0 (Susp-fmap (function₁' <I b) , idp)
    == degree <I (fst b)
  degree-matches <I b = equiv-adj' ΩS¹-equiv-ℤ $
    ap (Susp-fmap (function₁ <I b)) loop
      =⟨ ap-∙ (Susp-fmap (function₁ <I b)) (merid false) (! (merid true))  ⟩
    ap (Susp-fmap (function₁ <I b)) (merid false)
    ∙ ap (Susp-fmap (function₁ <I b)) (! (merid true))
      =⟨ ap2 _∙_
          (SuspFmap.merid-β (function₁ <I b) false)
            ( ap-! (Susp-fmap (function₁ <I b)) (merid true)
            ∙ ap ! (SuspFmap.merid-β (function₁ <I b) true)) ⟩
    merid (function₁ <I b false) ∙ ! (merid (function₁ <I b true))
      =⟨ degree-matches' <I b ⟩
    loop^ (degree <I (fst b))
      =∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- The ATP pragma with the role <axiom> can be used with data constructors.

module ATPAxiomDataConstructors where

postulate
  D    : Set
  zero : D
  succ : D → D

data N : D → Set where
  zN :               N zero
  sN : ∀ {n} → N n → N (succ n)
{-# ATP axiom zN #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Construct.Never where

open import Cubical.Core.Everything

open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Construct.Constant
open import Cubical.Data.Empty.Polymorphic

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

Never : ∀ {a b ℓ} {A : Type a} {B : Type b} → REL A B ℓ
Never = Const (⊥ , isProp⊥)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Matrix where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Functions.FunExtEquiv

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat hiding (_+_ ; +-comm ; +-assoc)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma.Base
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary

open import Cubical.Algebra.Group hiding (⟨_⟩)
open import Cubical.Algebra.AbGroup hiding (⟨_⟩)
open import Cubical.Algebra.Monoid hiding (⟨_⟩)
open import Cubical.Algebra.Ring

open Iso

private
  variable
    ℓ : Level
    A : Type ℓ

-- Equivalence between Vec matrix and Fin function matrix

FinMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
FinMatrix A m n = FinVec (FinVec A n) m

VecMatrix : (A : Type ℓ) (m n : ℕ) → Type ℓ
VecMatrix A m n = Vec (Vec A n) m

FinMatrix→VecMatrix : {m n : ℕ} → FinMatrix A m n → VecMatrix A m n
FinMatrix→VecMatrix M = FinVec→Vec (λ fm → FinVec→Vec (M fm))

VecMatrix→FinMatrix : {m n : ℕ} → VecMatrix A m n → FinMatrix A m n
VecMatrix→FinMatrix M fn fm = lookup fm (lookup fn M)

FinMatrix→VecMatrix→FinMatrix : {m n : ℕ} (M : FinMatrix A m n)
                              → VecMatrix→FinMatrix (FinMatrix→VecMatrix M) ≡ M
FinMatrix→VecMatrix→FinMatrix {m = zero} M = funExt (⊥.rec ∘ ¬Fin0)
FinMatrix→VecMatrix→FinMatrix {n = zero} M = funExt₂ (λ _ → ⊥.rec ∘ ¬Fin0)
FinMatrix→VecMatrix→FinMatrix {m = suc m} {n = suc n} M = funExt₂ goal
  where
  goal : (fm : Fin (suc m)) (fn : Fin (suc n))
       → VecMatrix→FinMatrix (_ ∷ FinMatrix→VecMatrix (M ∘ suc)) fm fn ≡ M fm fn
  goal zero zero       = refl
  goal zero (suc fn) i = FinVec→Vec→FinVec (M zero ∘ suc) i fn
  goal (suc fm) fn i   = FinMatrix→VecMatrix→FinMatrix (M ∘ suc) i fm fn

VecMatrix→FinMatrix→VecMatrix : {m n : ℕ} (M : VecMatrix A m n)
                              → FinMatrix→VecMatrix (VecMatrix→FinMatrix M) ≡ M
VecMatrix→FinMatrix→VecMatrix {m = zero} [] = refl
VecMatrix→FinMatrix→VecMatrix {m = suc m} (M ∷ MS) i =
  Vec→FinVec→Vec M i ∷ VecMatrix→FinMatrix→VecMatrix MS i

FinMatrixIsoVecMatrix : (A : Type ℓ) (m n : ℕ) → Iso (FinMatrix A m n) (VecMatrix A m n)
fun (FinMatrixIsoVecMatrix A m n)      = FinMatrix→VecMatrix
inv (FinMatrixIsoVecMatrix A m n)      = VecMatrix→FinMatrix
rightInv (FinMatrixIsoVecMatrix A m n) = VecMatrix→FinMatrix→VecMatrix
leftInv (FinMatrixIsoVecMatrix A m n)  = FinMatrix→VecMatrix→FinMatrix

FinMatrix≃VecMatrix : {m n : ℕ} → FinMatrix A m n ≃ VecMatrix A m n
FinMatrix≃VecMatrix {_} {A} {m} {n} = isoToEquiv (FinMatrixIsoVecMatrix A m n)

FinMatrix≡VecMatrix : (A : Type ℓ) (m n : ℕ) → FinMatrix A m n ≡ VecMatrix A m n
FinMatrix≡VecMatrix _ _ _ = ua FinMatrix≃VecMatrix

-- Define abelian group structure on matrices
module FinMatrixAbGroup (G' : AbGroup {ℓ}) where

  open AbGroup G' renaming ( Carrier to G ; is-set to isSetG )

  zeroFinMatrix : ∀ {m n} → FinMatrix G m n
  zeroFinMatrix _ _ = 0g

  negFinMatrix : ∀ {m n} → FinMatrix G m n → FinMatrix G m n
  negFinMatrix M i j = - M i j

  addFinMatrix : ∀ {m n} → FinMatrix G m n → FinMatrix G m n → FinMatrix G m n
  addFinMatrix M N i j = M i j + N i j

  isSetFinMatrix : ∀ {m n} → isSet (FinMatrix G m n)
  isSetFinMatrix = isSetΠ2 λ _ _ → isSetG

  addFinMatrixAssoc : ∀ {m n} → (M N K : FinMatrix G m n)
                    → addFinMatrix M (addFinMatrix N K) ≡ addFinMatrix (addFinMatrix M N) K
  addFinMatrixAssoc M N K i j k = assoc (M j k) (N j k) (K j k) i

  addFinMatrix0r : ∀ {m n} → (M : FinMatrix G m n)
                 → addFinMatrix M zeroFinMatrix ≡ M
  addFinMatrix0r M i j k = rid (M j k) i

  addFinMatrix0l : ∀ {m n} → (M : FinMatrix G m n)
                 → addFinMatrix zeroFinMatrix M ≡ M
  addFinMatrix0l M i j k = lid (M j k) i

  addFinMatrixNegMatrixr : ∀ {m n} → (M : FinMatrix G m n)
                         → addFinMatrix M (negFinMatrix M) ≡ zeroFinMatrix
  addFinMatrixNegMatrixr M i j k = invr (M j k) i

  addFinMatrixNegMatrixl : ∀ {m n} → (M : FinMatrix G m n)
                         → addFinMatrix (negFinMatrix M) M ≡ zeroFinMatrix
  addFinMatrixNegMatrixl M i j k = invl (M j k) i

  addFinMatrixComm : ∀ {m n} → (M N : FinMatrix G m n)
                   → addFinMatrix M N ≡ addFinMatrix N M
  addFinMatrixComm M N i k l = comm (M k l) (N k l) i

  FinMatrixAbGroup : (m n : ℕ) → AbGroup {ℓ}
  FinMatrixAbGroup m n =
    makeAbGroup {G = FinMatrix G m n} zeroFinMatrix addFinMatrix negFinMatrix
                isSetFinMatrix addFinMatrixAssoc addFinMatrix0r
                addFinMatrixNegMatrixr addFinMatrixComm

-- Define a abelian group structure on vector matrices and prove that
-- it is equal to FinMatrixAbGroup using the SIP
module _ (G' : AbGroup {ℓ}) where

  open AbGroup G' renaming ( Carrier to G )

  zeroVecMatrix : ∀ {m n} → VecMatrix G m n
  zeroVecMatrix = replicate (replicate 0g)

  negVecMatrix : ∀ {m n} → VecMatrix G m n → VecMatrix G m n
  negVecMatrix = map (map (λ x → - x))

  addVec : ∀ {m} → Vec G m → Vec G m → Vec G m
  addVec [] [] = []
  addVec (x ∷ xs) (y ∷ ys) = x + y ∷ addVec xs ys

  addVecMatrix : ∀ {m n} → VecMatrix G m n → VecMatrix G m n → VecMatrix G m n
  addVecMatrix [] [] = []
  addVecMatrix (M ∷ MS) (N ∷ NS) = addVec M N ∷ addVecMatrix MS NS

  open FinMatrixAbGroup

  -- Proof that FinMatrix→VecMatrix is a group homorphism
  FinMatrix→VecMatrixHomAdd : (m n : ℕ) (M N : FinMatrix G m n)
    → FinMatrix→VecMatrix (addFinMatrix G' M N) ≡
      addVecMatrix (FinMatrix→VecMatrix M) (FinMatrix→VecMatrix N)
  FinMatrix→VecMatrixHomAdd zero n M N = refl
  FinMatrix→VecMatrixHomAdd (suc m) n M N =
    λ i → lem n (M zero) (N zero) i
        ∷ FinMatrix→VecMatrixHomAdd m n (λ i j → M (suc i) j) (λ i j → N (suc i) j) i
     where
     lem : (n : ℕ) (V W : FinVec G n)
       → FinVec→Vec (λ j → V j + W j) ≡ addVec (FinVec→Vec V) (FinVec→Vec W)
     lem zero V W = refl
     lem (suc n) V W = λ i → V zero + W zero ∷ lem n (V ∘ suc) (W ∘ suc) i

  -- Combine everything to get an induced abelian group structure of
  -- VecMatrix that is equal to the one on FinMatrix
  VecMatrixAbGroup : (m n : ℕ) → AbGroup
  VecMatrixAbGroup m n =
    InducedAbGroup (FinMatrixAbGroup G' m n) (_ , addVecMatrix)
                    FinMatrix≃VecMatrix (FinMatrix→VecMatrixHomAdd m n)

  FinMatrixAbGroup≡VecMatrixAbGroup : (m n : ℕ) → FinMatrixAbGroup G' m n ≡ VecMatrixAbGroup m n
  FinMatrixAbGroup≡VecMatrixAbGroup m n =
    InducedAbGroupPath (FinMatrixAbGroup G' m n) (_ , addVecMatrix)
                        FinMatrix≃VecMatrix (FinMatrix→VecMatrixHomAdd m n)

-- Define identity matrix and matrix multiplication for FinMatrix and
-- prove that square matrices form a ring
module _ (R' : Ring {ℓ}) where

  open Ring R' renaming ( Carrier to R ; is-set to isSetR )
  open Theory R'
  open FinMatrixAbGroup (abgroup R _ _ _ (R' .Ring.+-isAbGroup))

  oneFinMatrix : ∀ {n} → FinMatrix R n n
  oneFinMatrix i j = if i == j then 1r else 0r

  -- TODO: upstream and state for monoids
  ∑ : ∀ {n} → FinVec R n → R
  ∑ = foldrFin _+_ 0r

  mulFinMatrix : ∀ {m1 m2 m3} → FinMatrix R m1 m2 → FinMatrix R m2 m3 → FinMatrix R m1 m3
  mulFinMatrix M N i k = ∑ λ j → M i j · N j k

  -- Properties
  sumVecExt : ∀ {n} → {V W : FinVec R n} → ((i : Fin n) → V i ≡ W i) → ∑ V ≡ ∑ W
  sumVecExt {n = zero} _    = refl
  sumVecExt {n = suc n} h i = h zero i + sumVecExt (h ∘ suc) i

  sumVecSplit : ∀ {n} → (V W : FinVec R n) → ∑ (λ i → V i + W i) ≡ ∑ V + ∑ W
  sumVecSplit {n = zero}  V W = sym (+-rid 0r)
  sumVecSplit {n = suc n} V W =
    V zero + W zero + ∑ (λ i → V (suc i) + W (suc i)) ≡⟨ (λ i → V zero + W zero + sumVecSplit (V ∘ suc) (W ∘ suc) i) ⟩
    V zero + W zero + (∑ (V ∘ suc) + ∑ (W ∘ suc))     ≡⟨ sym (+-assoc _ _ _) ⟩
    V zero + (W zero + (∑ (V ∘ suc) + ∑ (W ∘ suc)))   ≡⟨ cong (λ x → V zero + x) (+-assoc-comm1 _ _ _) ⟩
    V zero + (∑ (V ∘ suc) + (W zero + (∑ (W ∘ suc)))) ≡⟨ +-assoc _ _ _ ⟩
    V zero + ∑ (V ∘ suc) + (W zero + ∑ (W ∘ suc))     ∎

  sumVec0r : (n : ℕ) → ∑ (λ (i : Fin n) → 0r) ≡ 0r
  sumVec0r zero    = refl
  sumVec0r (suc n) = cong (λ x → 0r + x) (sumVec0r n) ∙ +-rid 0r

  sumVecExchange : ∀ {m n} → (M : FinMatrix R m n) → ∑ (λ i → ∑ (λ j → M i j)) ≡ ∑ (λ j → ∑ (λ i → M i j))
  sumVecExchange {m = zero}  {n = n}     M = sym (sumVec0r n)
  sumVecExchange {m = suc m} {n = zero}  M = cong (λ x → 0r + x) (sumVec0r m) ∙ +-rid 0r
  sumVecExchange {m = suc m} {n = suc n} M =
     let a  = M zero zero
         L  = ∑ λ j → M zero (suc j)
         C  = ∑ λ i → M (suc i) zero
         N  = ∑ λ i → ∑ λ j → M (suc i) (suc j)
         -- N reindexed
         N' = ∑ λ j → ∑ λ i → M (suc i) (suc j)
     in a + L + ∑ (λ i → ∑ (λ j → M (suc i) j)) ≡⟨ (λ k → a + L + sumVecSplit (λ i → M (suc i) zero) (λ i → ∑ (λ j → M (suc i) (suc j))) k) ⟩
        a + L + (C + N)                         ≡⟨ (λ k → a + L + (C + sumVecExchange (λ i j → M (suc i) (suc j)) k)) ⟩
        a + L + (C + N')                        ≡⟨ sym (+-assoc _ _ _) ⟩
        a + (L + (C + N'))                      ≡⟨ (λ k → a + +-assoc-comm1 L C N' k) ⟩
        a + (C + (L + N'))                      ≡⟨ +-assoc _ _ _ ⟩
        a + C + (L + N')                        ≡⟨ (λ k → a + C + sumVecSplit (λ j → M zero (suc j)) (λ j → ∑ (λ i → M (suc i) (suc j))) (~ k)) ⟩
        a + C + ∑ (λ j → ∑ (λ i → M i (suc j))) ∎

  sumVecMulrdist : ∀ {n} → (x : R) → (V : FinVec R n)
                 → x · ∑ V ≡ ∑ λ i → x · V i
  sumVecMulrdist {n = zero}  x _ = 0-rightNullifies x
  sumVecMulrdist {n = suc n} x V =
    x · (V zero + ∑ (V ∘ suc))           ≡⟨ ·-rdist-+ _ _ _ ⟩
    x · V zero + x · ∑ (V ∘ suc)         ≡⟨ (λ i → x · V zero + sumVecMulrdist x (V ∘ suc) i) ⟩
    x · V zero + ∑ (λ i → x · V (suc i)) ∎

  sumVecMulldist : ∀ {n} → (x : R) → (V : FinVec R n)
                 → (∑ V) · x ≡ ∑ λ i → V i · x
  sumVecMulldist {n = zero}  x _ = 0-leftNullifies x
  sumVecMulldist {n = suc n} x V =
    (V zero + ∑ (V ∘ suc)) · x           ≡⟨ ·-ldist-+ _ _ _ ⟩
    V zero · x + (∑ (V ∘ suc)) · x       ≡⟨ (λ i → V zero · x + sumVecMulldist x (V ∘ suc) i) ⟩
    V zero · x + ∑ (λ i → V (suc i) · x) ∎

  sumVecMulr0 : ∀ {n} → (V : FinVec R n) → ∑ (λ i → V i · 0r) ≡ 0r
  sumVecMulr0 V = sym (sumVecMulldist 0r V) ∙ 0-rightNullifies _

  sumVecMul0r : ∀ {n} → (V : FinVec R n) → ∑ (λ i → 0r · V i) ≡ 0r
  sumVecMul0r V = sym (sumVecMulrdist 0r V) ∙ 0-leftNullifies _

  sumVecMulr1 : (n : ℕ) (V : FinVec R n) → (j : Fin n) → ∑ (λ i → V i · (if i == j then 1r else 0r)) ≡ V j
  sumVecMulr1 (suc n) V zero = (λ k → ·-rid (V zero) k + sumVecMulr0 (V ∘ suc) k) ∙ +-rid (V zero)
  sumVecMulr1 (suc n) V (suc j) =
     (λ i → 0-rightNullifies (V zero) i + ∑ (λ x → V (suc x) · (if x == j then 1r else 0r)))
     ∙∙ +-lid _ ∙∙ sumVecMulr1 n (V ∘ suc) j

  sumVecMul1r : (n : ℕ) (V : FinVec R n) → (j : Fin n) → ∑ (λ i → (if j == i then 1r else 0r) · V i) ≡ V j
  sumVecMul1r (suc n) V zero = (λ k → ·-lid (V zero) k + sumVecMul0r (V ∘ suc) k) ∙ +-rid (V zero)
  sumVecMul1r (suc n) V (suc j) =
    (λ i → 0-leftNullifies (V zero) i + ∑ (λ i → (if j == i then 1r else 0r) · V (suc i)))
    ∙∙ +-lid _ ∙∙ sumVecMul1r n (V ∘ suc) j

  mulFinMatrixAssoc : ∀ {m n k l} → (M : FinMatrix R m n) → (N : FinMatrix R n k) → (K : FinMatrix R k l)
                   → mulFinMatrix M (mulFinMatrix N K) ≡ mulFinMatrix (mulFinMatrix M N) K
  mulFinMatrixAssoc M N K = funExt₂ λ i j →
    ∑ (λ k → M i k · ∑ (λ l → N k l · K l j))   ≡⟨ sumVecExt (λ k → sumVecMulrdist (M i k) (λ l → N k l · K l j)) ⟩
    ∑ (λ k → ∑ (λ l → M i k · (N k l · K l j))) ≡⟨ sumVecExt (λ k → sumVecExt (λ l → ·-assoc (M i k) (N k l) (K l j))) ⟩
    ∑ (λ k → ∑ (λ l → M i k · N k l · K l j))   ≡⟨ sumVecExchange (λ k l → M i k · N k l · K l j) ⟩
    ∑ (λ l → ∑ (λ k → M i k · N k l · K l j))   ≡⟨ sumVecExt (λ l → sym (sumVecMulldist (K l j) (λ k → M i k · N k l))) ⟩
    ∑ (λ l → ∑ (λ k → M i k · N k l) · K l j)   ∎

  mulFinMatrixr1 : ∀ {m n} → (M : FinMatrix R m n) → mulFinMatrix M oneFinMatrix ≡ M
  mulFinMatrixr1 M = funExt₂ λ i j → sumVecMulr1 _ (M i) j

  mulFinMatrix1r : ∀ {m n} → (M : FinMatrix R m n) → mulFinMatrix oneFinMatrix M ≡ M
  mulFinMatrix1r M = funExt₂ λ i j → sumVecMul1r _ (λ x → M x j) i

  mulFinMatrixrDistrAddFinMatrix : ∀ {n} (M N K : FinMatrix R n n)
                                 → mulFinMatrix M (addFinMatrix N K) ≡ addFinMatrix (mulFinMatrix M N) (mulFinMatrix M K)
  mulFinMatrixrDistrAddFinMatrix M N K = funExt₂ λ i j →
    ∑ (λ k → M i k · (N k j + K k j))                 ≡⟨ sumVecExt (λ k → ·-rdist-+ (M i k) (N k j) (K k j)) ⟩
    ∑ (λ k → M i k · N k j + M i k · K k j)           ≡⟨ sumVecSplit (λ k → M i k · N k j) (λ k → M i k · K k j) ⟩
    ∑ (λ k → M i k · N k j) + ∑ (λ k → M i k · K k j) ∎

  mulFinMatrixlDistrAddFinMatrix : ∀ {n} (M N K : FinMatrix R n n)
                                 → mulFinMatrix (addFinMatrix M N) K ≡ addFinMatrix (mulFinMatrix M K) (mulFinMatrix N K)
  mulFinMatrixlDistrAddFinMatrix M N K = funExt₂ λ i j →
    ∑ (λ k → (M i k + N i k) · K k j)                 ≡⟨ sumVecExt (λ k → ·-ldist-+ (M i k) (N i k) (K k j)) ⟩
    ∑ (λ k → M i k · K k j + N i k · K k j)           ≡⟨ sumVecSplit (λ k → M i k · K k j) (λ k → N i k · K k j) ⟩
    ∑ (λ k → M i k · K k j) + ∑ (λ k → N i k · K k j) ∎

  FinMatrixRing : (n : ℕ) → Ring {ℓ}
  FinMatrixRing n =
    makeRing {R = FinMatrix R n n} zeroFinMatrix oneFinMatrix addFinMatrix
             mulFinMatrix negFinMatrix isSetFinMatrix addFinMatrixAssoc
             addFinMatrix0r addFinMatrixNegMatrixr addFinMatrixComm
             mulFinMatrixAssoc mulFinMatrixr1 mulFinMatrix1r
             mulFinMatrixrDistrAddFinMatrix mulFinMatrixlDistrAddFinMatrix

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module _ {A : Set} (P : A → Set) where

  instance
   postulate
    forbidden : {x : A} → P x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Binary.Equality.Propositional directly.
------------------------------------------------------------------------

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

module Data.Vec.Relation.Equality.Propositional where

open import Data.Vec.Relation.Binary.Equality.Propositional public

{-# WARNING_ON_IMPORT
"Data.Vec.Relation.Equality.Propositional was deprecated in v1.0.
Use Data.Vec.Relation.Binary.Equality.Propositional instead."
#-}


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

-- Singleton type and its 'inverse'

module Singleton where

open import Data.Unit using (⊤; tt)
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; subst; cong ; cong₂ ; inspect ; [_])
-- open import Level
--   using (zero)
-- open import Axiom.Extensionality.Propositional
--   using (Extensionality)

is-contr : Set → Set
is-contr A = Σ A (λ a → (x : A) → a ≡ x)

is-prop : Set → Set
is-prop A = (x y : A) → x ≡ y

is-set : Set → Set
is-set A = (x y : A) → is-prop (x ≡ y)

contr-prop : {A : Set} → is-contr A → is-prop A
contr-prop (a , ϕ) x y = trans (sym (ϕ x)) (ϕ y)

apd : ∀ {a b} {A : Set a} {B : A → Set b} (f : (x : A) → B x) {x y} → (p : x ≡ y) → subst B p (f x) ≡ f y
apd f refl = refl

prop-set : {A : Set} → is-prop A → is-set A
prop-set {A} ϕ x y p q = trans (l p) (sym (l q))
  where g : (z : A) → x ≡ z
        g z = ϕ x z
        unitr : {y z : A} (p : y ≡ z) → refl ≡ trans (sym p) p
        unitr refl = refl
        l : {y z : A} (p : y ≡ z) → p ≡ trans (sym (g y)) (g z)
        l refl = unitr (g _)

prop-contr : {A : Set} → is-prop A → A → is-contr A
prop-contr ϕ a = a , ϕ a

------------------------------------------------------------------------------
-- Singleton type: A type with a distinguished point
--  The 'interesting' part is that the point is both a parameter
--  and a field.

{--
record Singleton (A : Set) (v : A) : Set where
  constructor ⇑
  field
    ● : A
    v≡● : v ≡ ●

open Singleton public
--}

Singleton : (A : Set) → (v : A) → Set
Singleton A v = ∃ (λ ● → v ≡ ●)

-- Singleton types are contractible:
pointed-contr : {A : Set} {v : A} → is-contr (Singleton A v)
--pointed-contr {A} {v} = ⇑ v refl , λ { (⇑ ● refl) → refl }
pointed-contr {A} {v} = (v , refl) , λ { ( ● , refl) → refl }

-- and thus have all paths between them:
pointed-all-paths : {A : Set} {v : A} {p q : Singleton A v} → p ≡ q
pointed-all-paths = contr-prop pointed-contr _ _

-- What does Singleton of Singleton do?
-- Values of type Singleton A v are of the form (w , p) where p : v ≡ w
-- Values of type Singleton (Singleton A v) x

ssv : (A : Set) (v : A) (x : Singleton A v) → Singleton (Singleton A v) x
ssv A v (.v , refl) = (v , refl) , refl

{--
ss=s : (A : Set) (v : A) (x : Singleton A v) → Singleton (Singleton A v) x ≡ Singleton A v
ss=s A v (.v , refl) with pointed-contr {A} {v}
... | (.v , refl) , f = let p = f (v , refl) in {!!} -- ??
--}
------------------------------------------------------------------------------
-- The 'reciprocal' of a Singleton type is a function that accepts exactly
-- that point, and returns no information. It acts as a 'witness' that
-- the right point has been fed to it.
{--
Recip : (A : Set) → (v : A) → Set
Recip A v = (w : A) → (v ≡ w) → ⊤
--}

Recip : (A : Set) → (v : A) → Set
Recip A v = Singleton A v → ⊤

-- Recip A v = Singleton A v → ⊤

-- Recip is also contractible, if we're thinking of homotopy types.
-- We need funext to prove it which is not --safe

-- posulate
--   funext : Extensionality zero zero

-- recip-contr : {A : Set} {v : A} → is-contr (Recip A v)
-- recip-contr = (λ _ _ → tt) , λ r → funext λ _ → funext λ _ → refl

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

-- Recip' : {A : Set} {v : A} → Singleton A v → Set
-- Recip' {A} {v} (⇑ w v≡w) = v ≡ w

-- Recip'-ptd : {A : Set} {v : A} → (p : Singleton A v) → Singleton (Recip' p) (v≡● p)
-- Recip'-ptd (⇑ w v≡w) = ⇑ v≡w refl

-- family of path types from arbitrary w to a fixed v

Recip' : (A : Set) → (v : A) → Set
Recip' A v = (w : A) → v ≡ w

-- If A is a n-type, Recip' is a (n-1)-type

-- recip'-contr : {A : Set} {v : A} → is-prop A → is-contr (Recip' A v)
-- recip'-contr {A} {v} ϕ = (λ w → ϕ v w) , λ r → funext λ x → prop-set ϕ v x (ϕ v x) (r x)

-- recip'-prop : {A : Set} {v : A} → is-set A → is-prop (Recip' A v)
-- recip'-prop ϕ r s = funext (λ x → ϕ _ x (r x) (s x))

------------------------------------------------------------------------------
-- Singleton is an idempotent bimonad on pointed sets
-- (need to check some coherences)

∙Set = Σ Set (λ X → X)

∙Set[_,_] : ∙Set → ∙Set → Set
∙Set[ (A , a) , (B , b) ] = Σ (A → B) λ f → f a ≡ b

_∙×_ : ∙Set → ∙Set → ∙Set
(A , a) ∙× (B , b) = (A × B) , (a , b)

-- left version, there's also a right version
-- note that this isn't a coproduct
-- wedge sum is the coproduct
_∙+_ : ∙Set → ∙Set → ∙Set
(A , a) ∙+ (B , b) = (A ⊎ B) , inj₁ a

∙id : ∀{∙A} → ∙Set[ ∙A , ∙A ]
∙id = (λ a → a) , refl

_∘_ : ∀ {∙A ∙B ∙C} → ∙Set[ ∙A , ∙B ] → ∙Set[ ∙B , ∙C ] → ∙Set[ ∙A , ∙C ]
(f , p) ∘ (g , q) = (λ x → g (f x)) , trans (cong g p) q

-- terminal and initial
∙1 : ∙Set
∙1 = ⊤ , tt

∙![_] : ∀ ∙A → ∙Set[ ∙A , ∙1 ]
∙![ (A , a) ] = (λ _ → tt) , refl

∙!-uniq : ∀ {∙A} {x : ∙A .proj₁} → (∙f : ∙Set[ ∙A , ∙1 ]) → (∙f .proj₁) x ≡ (∙![ ∙A ] .proj₁) x
∙!-uniq {A , a} {x} (f , p) = refl

∙¡[_] : ∀ ∙A → ∙Set[ ∙1 , ∙A ]
∙¡[ A , a ] = (λ _ → a) , refl

∙¡-uniq : ∀ {∙A} → (∙f : ∙Set[ ∙1 , ∙A ]) → (∙f .proj₁) tt ≡ (∙¡[ ∙A ] .proj₁) tt
∙¡-uniq (f , p) = p

record ∙Iso[_,_] (∙A ∙B : ∙Set) : Set where
  constructor iso
  field
    ∙f : ∙Set[ ∙A , ∙B ]
    ∙g : ∙Set[ ∙B , ∙A ]
  f = ∙f .proj₁
  g = ∙g .proj₁
  field
    f-g : ∀ b → f (g b) ≡ b
    g-f : ∀ a → g (f a) ≡ a

open ∙Iso[_,_]

∙Iso⁻¹ : ∀ {∙A ∙B} → ∙Iso[ ∙A , ∙B ] → ∙Iso[ ∙B , ∙A ]
∙Iso⁻¹ (iso ∙f ∙g f-g g-f) = iso ∙g ∙f g-f f-g

Sing : ∙Set → ∙Set
Sing (A , a) = Singleton A a , a , refl

Sing[_,_] : ∀ ∙A ∙B → ∙Set[ ∙A , ∙B ] → ∙Set[ Sing ∙A , Sing ∙B  ]
Sing[ (A , a) , (B , .(f a)) ] (f , refl) = (λ { (x , refl) → f x , refl }) , refl

-- monad
η[_] : ∀ ∙A → ∙Set[ ∙A , Sing ∙A ]
η[ (A , a) ] = (λ x → a , refl) , refl

-- Sing(A) is terminal
η-uniq : ∀ {∙A} {x : ∙A .proj₁} → (∙f : ∙Set[ ∙A , Sing ∙A ]) → (∙f .proj₁) x ≡ (η[ ∙A ] .proj₁) x
η-uniq {A , a} (f , p) = pointed-all-paths

Sing≃1 : ∀ {∙A} → ∙Iso[ Sing ∙A , ∙1 ]
Sing≃1 {∙A@(A , a)} = iso ∙![ Sing ∙A ] ( ((λ _ → a) , refl) ∘ η[ ∙A ]) (λ _ → refl) (λ _ → pointed-all-paths)

μ[_] : ∀ ∙A → ∙Iso[ Sing (Sing ∙A) , Sing ∙A ]
μ[ (A , a) ] = iso ((λ { (.(a , refl) , refl) → a , refl }) , refl)
                   ((λ { (a , refl) → (a , refl) , refl }) , refl)
                   (λ { (a , refl) → refl})
                   (λ { ((a , refl) , refl) → refl })

-- check
Sη-μ : ∀ {∙A} → ((Sing[ ∙A , Sing ∙A ] η[ ∙A ] ∘ (μ[ ∙A ] .∙f)) .proj₁) (∙A .proj₂ , refl) ≡ (∙A .proj₂ , refl)
Sη-μ = refl

ηS-μ : ∀ {∙A} → ((Sing[ Sing ∙A , Sing (Sing ∙A) ] η[ Sing ∙A ] ∘ (μ[ Sing ∙A ] .∙f)) .proj₁) ((∙A .proj₂ , refl) , refl) ≡ ((∙A .proj₂ , refl) , refl)
ηS-μ = refl

-- strength
σ×[_,_] : ∀ ∙A ∙B → ∙Set[ Sing ∙A ∙× ∙B , Sing (∙A ∙× ∙B) ]
σ×[ (A , a) , (B , b) ] = (λ { ((a , refl) , _) → (a , b) , refl }) , refl

τ×[_,_] : ∀ ∙A ∙B → ∙Set[ ∙A ∙× Sing ∙B , Sing (∙A ∙× ∙B) ]
τ×[ (A , a) , (B , b) ] = (λ { (_ , (b , refl)) → (a , b) , refl }) , refl

σ+[_,_] : ∀ ∙A ∙B → ∙Set[ Sing ∙A ∙+ ∙B , Sing (∙A ∙+ ∙B) ]
σ+[ (A , a) , (B , b) ] = (λ _ → inj₁ a , refl) , refl

τ+[_,_] : ∀ ∙A ∙B → ∙Set[ ∙A ∙+ Sing ∙B , Sing (∙A ∙+ ∙B) ]
τ+[ (A , a) , (B , b) ] = (λ _ → inj₁ a , refl) , refl

-- comonad
ε[_] : ∀ ∙A → ∙Set[ Sing ∙A , ∙A ]
ε[ (A , a) ] = (λ { (x , refl) → x }) , refl

δ[_] : ∀ ∙A → ∙Iso[ Sing ∙A , Sing (Sing ∙A) ]
δ[ ∙A ] = ∙Iso⁻¹ μ[ ∙A ]

-- check
δ-Sε : ∀ {∙A} → ((δ[ ∙A ] .∙f ∘ Sing[ Sing ∙A , ∙A ] ε[ ∙A ]) .proj₁) (∙A .proj₂ , refl) ≡ (∙A .proj₂ , refl)
δ-Sε = refl

δ-εS : ∀ {∙A} → ((δ[ Sing ∙A ] .∙f ∘ Sing[ Sing (Sing ∙A) , Sing ∙A ] ε[ Sing ∙A ]) .proj₁) ((∙A .proj₂ , refl) , refl) ≡ ((∙A .proj₂ , refl) , refl)
δ-εS = refl

-- costrength
σ'×[_,_] : ∀ ∙A ∙B → ∙Set[ Sing (∙A ∙× ∙B) , Sing ∙A ∙× ∙B ]
σ'×[ (A , a) , (B , b) ] = (λ { (.(a , b) , refl) → (a , refl) , b }) , refl

τ'×[_,_] : ∀ ∙A ∙B → ∙Set[ Sing (∙A ∙× ∙B) , ∙A ∙× Sing ∙B ]
τ'×[ (A , a) , (B , b) ] = (λ { (.(a , b) , refl) → a , (b , refl) }) , refl

σ'+[_,_] : ∀ ∙A ∙B → ∙Set[ Sing (∙A ∙+ ∙B) , Sing ∙A ∙+ ∙B ]
σ'+[ (A , a) , (B , b) ] = (λ _ → inj₁ (a , refl)) , refl

τ'+[_,_] : ∀ ∙A ∙B → ∙Set[ Sing (∙A ∙+ ∙B) , ∙A ∙+ Sing ∙B ]
τ'+[ (A , a) , (B , b) ] = (λ _ → inj₁ a) , refl

-- even better, strong monoidal functor
ν×[_,_] : ∀ ∙A ∙B → ∙Iso[ Sing ∙A ∙× Sing ∙B , Sing (∙A ∙× ∙B) ]
ν×[ (A , a) , (B , b) ] = iso ((λ _ → (a , b) , refl) , refl)
                              ((λ _ → (a , refl) , b , refl) , refl)
                              (λ { (.(a , b) , refl) → refl })
                              (λ { ((a , refl) , (b , refl)) → refl })

-- this one is only lax
ν+[_,_] : ∀ ∙A ∙B → ∙Set[ Sing ∙A ∙+ Sing ∙B , Sing (∙A ∙+ ∙B) ]
ν+[ (A , a) , (B , b) ] = (λ _ → inj₁ a , refl) , refl

-- free pointed set
U : ∙Set → Set
U = proj₁

U[_,_] : ∀ ∙A ∙B → ∙Set[ ∙A , ∙B ] → (U ∙A → U ∙B)
U[ _ , _ ] = proj₁

F : Set → ∙Set
F A = (A ⊎ ⊤) , inj₂ tt

F[_,_] : ∀ A B → (A → B) → ∙Set[ F A , F B ]
F[ A , B ] f = (λ { (inj₁ a) → inj₁ (f a) ; (inj₂ tt) → inj₂ tt }) , refl

->adj : ∀ {A ∙B} → (A → U ∙B) → ∙Set[ F A , ∙B ]
->adj f = (λ { (inj₁ a) → f a ; (inj₂ tt) → _ }) , refl

<-adj : ∀ {A ∙B} → ∙Set[ F A , ∙B ] → (A → U ∙B)
<-adj (f , refl) a = f (inj₁ a)

η-adj : ∀ {A} → (A → U (F A))
η-adj = <-adj ∙id

ε-adj : ∀ {∙A} → ∙Set[ F (U ∙A), ∙A ]
ε-adj = ->adj λ x → x

-- maybe monad
T : Set → Set
T A = U (F A)

T-η[_] : ∀ A → (A → T A)
T-η[ A ] = η-adj

T-μ[_] : ∀ A → (T (T A) → T A)
T-μ[ A ] = U[ F (T A) , F A ] ε-adj

-- comaybe comonad
D : ∙Set → ∙Set
D ∙A = F (U ∙A)

D-ε[_] : ∀ ∙A → ∙Set[ D ∙A , ∙A ]
D-ε[ ∙A ] = ε-adj

D-δ[_] : ∀ ∙A → ∙Set[ D ∙A , D (D ∙A) ]
D-δ[ ∙A ] = F[ U ∙A , U (D ∙A) ] η-adj

-- but also
D-η[_] : ∀ ∙A → ∙Set[ ∙A , D ∙A ]
D-η[ ∙A ] = (λ _ → inj₂ tt) , refl
-- D ∙A is not contractible

-- distributive laws?
-- same as ∙Set[ ∙1 , D ∙1 ] so follows D-η
Λ : ∀ {∙A} → ∙Set[ Sing (D ∙A) , D (Sing ∙A) ]
Λ = (λ { (.(inj₂ tt) , refl) → inj₂ tt }) , refl

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Cubical.Categories.Equivalence.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Morphism
open import Cubical.Categories.Equivalence.Base
open import Cubical.HITs.PropositionalTruncation.Base

open Precategory
open Functor
open NatIso
open CatIso
open NatTrans
open isEquivalence

private
  variable
    ℓC ℓC' ℓD ℓD' : Level

-- Equivalence implies Full, Faithul, and Essentially Surjective

module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} where
  symEquiv : ∀ {F : Functor C D} → (e : isEquivalence F) → isEquivalence (e .invFunc)
  symEquiv {F} record { invFunc = G ; η = η ; ε = ε } = record { invFunc = F ; η = symNatIso ε ; ε = symNatIso η }

  isEquiv→Faithful : ∀ {F : Functor C D} → isEquivalence F → isFaithful F
  isEquiv→Faithful {F} record { invFunc = G
                              ; η = η
                              ; ε = _ }
                   c c' f g p = f
                              ≡⟨ sqRL η ⟩
                                cIso .mor ⋆⟨ C ⟩ G ⟪ F ⟪ f ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .inv
                              ≡⟨ cong (λ v → cIso .mor ⋆⟨ C ⟩ (G ⟪ v ⟫) ⋆⟨ C ⟩ c'Iso .inv) p ⟩
                                cIso .mor ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ c'Iso .inv
                              ≡⟨ sym (sqRL η) ⟩
                                g
                              ∎
    where

      -- isomorphism between c and GFc
      cIso = isIso→CatIso (η .nIso c)
      -- isomorphism between c' and GFc'
      c'Iso = isIso→CatIso (η .nIso c')

module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} where
  isEquiv→Full : ∀ {F : Functor C D} → isEquivalence F → isFull F
  isEquiv→Full {F} eq@record { invFunc = G
                             ; η = η
                             ; ε = _ }
               c c' g = ∣ h , isEquiv→Faithful (symEquiv eq) _ _ _ _ GFh≡Gg ∣ -- apply faithfulness of G
    where
      -- isomorphism between c and GFc
      cIso = isIso→CatIso (η .nIso c)
      -- isomorphism between c' and GFc'
      c'Iso = isIso→CatIso (η .nIso c')

      -- reverses
      cIso⁻ = symCatIso cIso
      c'Iso⁻ = symCatIso c'Iso

      h = cIso .mor ⋆⟨ C ⟩ G ⟪ g ⟫ ⋆⟨ C ⟩ c'Iso .inv

      -- we show that both `G ⟪ g ⟫` and `G ⟪ F ⟪ h ⟫ ⟫`
      -- are equal to the same thing
      -- namely : cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor
      Gg≡ηhη : G ⟪ g ⟫ ≡ cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor
      Gg≡ηhη = invMoveL cAreInv move-c' ∙ sym (C .⋆Assoc _ _ _)
        where
          cAreInv : areInv (cIso .mor) (cIso .inv)
          cAreInv = CatIso→areInv cIso

          c'AreInv : areInv (c'Iso .mor) (c'Iso .inv)
          c'AreInv = CatIso→areInv c'Iso

          move-c' : cIso .mor ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ h ⋆⟨ C ⟩ c'Iso .mor
          move-c' = invMoveR (symAreInv c'AreInv) refl

      GFh≡Gg : G ⟪ F ⟪ h ⟫ ⟫ ≡ G ⟪ g ⟫
      GFh≡Gg = G ⟪ F ⟪ h ⟫ ⟫
             ≡⟨ sqLR η ⟩
               cIso .inv ⋆⟨ C ⟩ h ⋆⟨ C ⟩ c'Iso .mor
             ≡⟨ sym Gg≡ηhη ⟩
               G ⟪ g ⟫
             ∎

  isEquiv→Surj : ∀ {F : Functor C D} → isEquivalence F → isEssentiallySurj F
  isEquiv→Surj isE d = (isE .invFunc ⟅ d ⟆) , isIso→CatIso ((isE .ε .nIso) d)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------------
-- Properties of the Collatz function
------------------------------------------------------------------------------

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

module FOTC.Program.Collatz.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.PropertiesATP using ( ∸-N )
open import FOTC.Data.Nat.UnaryNumbers
open import FOTC.Data.Nat.UnaryNumbers.TotalityATP using ( 2-N )
open import FOTC.Program.Collatz.Collatz
open import FOTC.Program.Collatz.Data.Nat
open import FOTC.Program.Collatz.Data.Nat.PropertiesATP

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

helper : ∀ {n} → N n → collatz (2' ^ succ₁ n) ≡ collatz (2' ^ n)
helper nzero = prf
  where postulate prf : collatz (2' ^ succ₁ zero) ≡ collatz (2' ^ zero)
        {-# ATP prove prf #-}
helper (nsucc {n} Nn) = prf
  where postulate prf : collatz (2' ^ succ₁ (succ₁ n)) ≡ collatz (2' ^ succ₁ n)
        {-# ATP prove prf +∸2 ^-N 2-N 2^x≢0 2^[x+1]≢1 div-2^[x+1]-2≡2^x
                      x-Even→SSx-Even ∸-N ∸-Even 2^[x+1]-Even 2-Even
        #-}

collatz-2^x : ∀ {n} → N n → collatz (2' ^ n) ≡ 1'
collatz-2^x nzero = prf
  where postulate prf : collatz (2' ^ 0') ≡ 1'
        {-# ATP prove prf #-}

collatz-2^x (nsucc {n} Nn) = prf (collatz-2^x Nn)
  where postulate prf : collatz (2' ^ n) ≡ 1' → collatz (2' ^ succ₁ n) ≡ 1'
        {-# ATP prove prf helper #-}


text:
{-# OPTIONS --sized-types #-}
module SNat where

open import Data.Nat hiding (_+_)
open import Size

data SNat : {ι : Size} → Set where
  zero : {ι : Size}
                   → SNat {↑ ι}
  succ : {ι : Size}
                   → SNat {ι}
                   → SNat {↑ ι}

subtyping : {ι : Size} → SNat {ι} → SNat {↑ ι}
subtyping zero = zero
subtyping (succ n) = succ (subtyping n)

_/2 : {ι : Size} → SNat { ι} → SNat {ι}
zero /2 = zero
(succ zero) /2 = zero
(succ (succ n)) /2 = subtyping (succ (n /2))

log₂ : {ι : Size} → SNat {ι} → SNat {ι}
log₂ zero = zero
log₂ (succ zero) = zero
log₂ (succ (succ n)) = succ (log₂ (succ (n /2)))

_+_ : SNat → SNat → SNat
zero + n = n
(succ m) + n = succ (m + n)

toNat : SNat → ℕ
toNat zero = zero
toNat (succ n) = suc (toNat n)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module nat-log-test where

open import eq
open import nat
open import nat-log

test : log-result 11 3
test = log 11 3 refl refl

exp-from-test : ℕ
exp-from-test with test
exp-from-test | pos-power e s p = e
exp-from-test | no-power p = 0

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Thunk wrappers for sized codata, copredicates and corelations
------------------------------------------------------------------------

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

module Codata.Thunk where

open import Size
open import Relation.Unary

------------------------------------------------------------------------
-- Basic types.

record Thunk {ℓ} (F : Size → Set ℓ) (i : Size) : Set ℓ where
  coinductive
  field force : {j : Size< i} → F j
open Thunk public

Thunk^P : ∀ {f p} {F : Size → Set f} (P : Size → F ∞ → Set p)
          (i : Size) (tf : Thunk F ∞) → Set p
Thunk^P P i tf = Thunk (λ i → P i (tf .force)) i

Thunk^R : ∀ {f g r} {F : Size → Set f} {G : Size → Set g}
          (R : Size → F ∞ → G ∞ → Set r)
          (i : Size) (tf : Thunk F ∞) (tg : Thunk G ∞) → Set r
Thunk^R R i tf tg = Thunk (λ i → R i (tf .force) (tg .force)) i

------------------------------------------------------------------------
-- Syntax

Thunk-syntax : ∀ {ℓ} → (Size → Set ℓ) → Size → Set ℓ
Thunk-syntax = Thunk

syntax Thunk-syntax (λ j → e) i = Thunk[ j < i ] e

------------------------------------------------------------------------
-- Basic functions.

-- Thunk is a functor
module _ {p q} {P : Size → Set p} {Q : Size → Set q} where

  map : ∀[ P ⇒ Q ] → ∀[ Thunk P ⇒ Thunk Q ]
  map f p .force = f (p .force)

-- Thunk is a comonad
module _ {p} {P : Size → Set p} where

  extract : ∀[ Thunk P ] → P ∞
  extract p = p .force

  duplicate : ∀[ Thunk P ⇒ Thunk (Thunk P) ]
  duplicate p .force .force = p .force

module _ {p q} {P : Size → Set p} {Q : Size → Set q} where

  infixl 1 _<*>_
  _<*>_ : ∀[ Thunk (P ⇒ Q) ⇒ Thunk P ⇒ Thunk Q ]
  (f <*> p) .force = f .force (p .force)

-- We can take cofixpoints of functions only making Thunk'd recursive calls
module _ {p} (P : Size → Set p) where

  cofix : ∀[ Thunk P ⇒ P ] → ∀[ P ]
  cofix f = f λ where .force → cofix f


text:
{-# OPTIONS --cubical #-}
module TranspComputing where

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical
open import Agda.Builtin.List

transpList : ∀ (φ : I) (A : Set) x xs → primTransp (λ _ → List A) φ (x ∷ xs) ≡ (primTransp (λ i → A) φ x ∷ primTransp (λ i → List A) φ xs)
transpList φ A x xs = \ _ → primTransp (λ _ → List A) φ (x ∷ xs)

data S¹ : Set where
  base : S¹
  loop : base ≡ base

-- This should be refl.
transpS¹ : ∀ (φ : I) (u0 : S¹) → primTransp (λ _ → S¹) φ u0 ≡ u0
transpS¹ φ u0 = \ _ →  u0


text:
-- {-# OPTIONS -v interaction:50 #-}
module Issue841 where

postulate
  D : Set
  c : (A : Set) (B : Set1) → D
  e : (A : Set) (B : Set1) (C : Set2) (X : Set3) → D

-- When the following is refined the goals end up being the wrong way
-- around.
bad : D
bad = {!c ?!}

-- I.e. bad ?3 ?2 instead of bad ?2 ?3.

-- Andreas, 2013-05-01 should now be correct.

bad' : D
bad' = {!e ? ?!}

-- This works:
good : D
good = {!c!}

also-good : D
also-good = {!c ? ?!}


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Maybe where

data Maybe {a} (A : Set a) : Set a where
  nothing : Maybe A
  just    : A → Maybe A


text:
module Reduction where

open import Data.Sum
open import Library
open import Terms
open import Substitution
open import TermShape
open import SN

data βECxt (Γ : Cxt) : (Δ : Cxt) (a b : Ty) → Set where
  appl  : ∀ {a b} (u : Tm Γ a)          → βECxt Γ Γ (a →̂ b) b
  appr  : ∀ {a b} (t : Tm Γ (a →̂  b))   → βECxt Γ Γ a b
  abs   : ∀ {a b}                       → βECxt Γ (a ∷ Γ) b (a →̂  b)

data βEhole {Γ : Cxt} : {Δ : Cxt} {b a : Ty} → Tm Γ b → βECxt Γ Δ a b → Tm Δ a → Set where
  appl  : ∀ {a b} {t : Tm Γ (a →̂ b)} (u : Tm Γ a)  → βEhole (app t u) (appl u) t
  appr  : ∀ {a b u} (t : Tm Γ (a →̂  b))            → βEhole (app t u) (appr t) u
  abs   : ∀ {a b} {t : Tm (a ∷ Γ) b}               → βEhole (abs t) abs t

-- Plugging a hole
mkHole : ∀ {Γ Δ} {a b} (E : βECxt Γ Δ a b) {t} → ∃ λ E[t] → βEhole E[t] E t
mkHole (appl u)  = _ , appl u
mkHole (appr t)  = _ , appr t
mkHole abs       = _ , abs

data _⇒β_ {Γ} : ∀ {a} → Tm Γ a → Tm Γ a → Set where

  β     : ∀ {a b}{t : Tm (a ∷ Γ) b}{u}
          → (app (abs t) u) ⇒β subst0 u t

  cong  : ∀ {Δ a b t t' Et Et'}{E : βECxt Γ Δ a b}
          → (𝑬𝒕 : βEhole Et E t)
          → (𝑬𝒕' : βEhole Et' E t')
          → (t⇒β : t ⇒β t')
          → Et ⇒β Et'

subst⇒β : ∀ {m vt a Γ} {t t' : Tm Γ a} {Δ}
           (σ : RenSub {m} vt Γ Δ) → t ⇒β t' → subst σ t ⇒β subst σ t'
subst⇒β σ (β {t = t} {u = u})          = ≡.subst (λ t' → app (abs (subst (lifts σ) t)) (subst σ u) ⇒β t')
                                                   (sgs-lifts-term {σ = σ} {u} {t})
                                           β
subst⇒β σ (cong (appl u) (appl .u) t⇒) = cong (appl _) (appl _) (subst⇒β σ t⇒)
subst⇒β σ (cong (appr t) (appr .t) t⇒) = cong (appr _) (appr _) (subst⇒β σ t⇒)
subst⇒β σ (cong abs abs t⇒)            = cong abs abs (subst⇒β (lifts σ) t⇒)

-- Multi-step β-reduction (β-reduction sequences).
-- Reflexive-transitive closure of single-step β-reduction.

infix 7 _⇒β_ _⇒β*_

data _⇒β*_ {Γ} {a} : Tm Γ a → Tm Γ a → Set where
  []  : ∀ {t} → t ⇒β* t
  _∷_ : ∀ {ti tm to} → ti ⇒β tm → tm ⇒β* to → ti ⇒β* to

-- Concatenating β-reduction sequences

_++β_ : ∀ {Γ} {a} {t₀ t₁ t₂ : Tm Γ a} → t₀ ⇒β* t₁ → t₁ ⇒β* t₂ → t₀ ⇒β* t₂
[]       ++β ys = ys
(x ∷ xs) ++β ys = x ∷ (xs ++β ys)

-- Multi-step β-reduction is compatible with term constructors.

cong* : ∀ {a Γ Δ} {b} {t tβ* : Tm Γ a} {E : βECxt Δ Γ a b} {E[t] E[tβ*]}
  → βEhole E[t] E t
  → βEhole E[tβ*] E tβ*
  → t    ⇒β* tβ*
  → E[t] ⇒β* E[tβ*]
cong* E1         E2          (x ∷ t⇒) = cong E1 (proj₂ (mkHole _)) x ∷ cong* (proj₂ (mkHole _)) E2 t⇒
cong* (appl u)   (appl .u)   []       = []
cong* (appr t₁)  (appr .t₁)  []       = []
cong* abs        abs         []       = []

EC→βEC : ∀ {Γ} {a b} (E : ECxt Γ a b) → βECxt Γ Γ a b
EC→βEC (appl u) = appl u

mkHole4 : ∀ {Γ} {a b} (E : ECxt Γ a b) {t : Tm Γ a} → βEhole (E [ t ]) (EC→βEC E) t
mkHole4 (appl u) = appl u

cong*3 : ∀ {Γ a b t t'}(E : ECxt* Γ a b)
          → (t⇒ : t ⇒β t')
          → E [ t ]* ⇒β E [ t' ]*
cong*3 [] t⇒ = t⇒
cong*3 (x ∷ E) t⇒ = cong*3 E (cong (mkHole4 x) (mkHole4 x) t⇒)

cong*4 : ∀ {Γ a b t t'}(E : ECxt* Γ a b)
          → (t⇒ : t ⇒β* t')
          → E [ t ]* ⇒β* E [ t' ]*
cong*4 E [] = []
cong*4 E (x ∷ xs) = cong*3 E x ∷ cong*4 E xs

subst⇒β*₀ : ∀ {m vt a Γ} {t t' : Tm Γ a} {Δ} (σ : RenSub {m} vt Γ Δ) → t ⇒β* t' → subst σ t ⇒β* subst σ t'
subst⇒β*₀ σ [] = []
subst⇒β*₀ σ (x ∷ xs) = (subst⇒β σ x) ∷ (subst⇒β*₀ σ xs)

mutual
  subst⇒β* : ∀ {m vt a Γ} {Δ} {σ ρ : RenSub {m} vt Γ Δ}
    → (∀ {b} (x : Var Γ b) → vt2tm _ (σ x) ⇒β* vt2tm _ (ρ x))
    → (t : Tm Γ a)
    → subst σ t ⇒β* subst ρ t
  subst⇒β* σ₁ (var x) = σ₁ x
  subst⇒β* {vt = vt} σ₁ (abs t) = cong* abs abs (subst⇒β* (lifts⇒β* {vt = vt} σ₁) t)
  subst⇒β* σ₁ (app t t₁) = cong* (appl _) (appl _) (subst⇒β* σ₁ t) ++β cong* (appr _) (appr _) (subst⇒β* σ₁ t₁)

  lifts⇒β* : ∀ {m vt a Γ} {Δ} {σ ρ : RenSub {m} vt Γ Δ}
    → (∀ {b} (x : Var Γ b) → vt2tm _ (σ x) ⇒β* vt2tm _ (ρ x))
    →  ∀ {b} (x : Var (a ∷ Γ) b)
    → vt2tm _ (lifts {a = a} σ x) ⇒β* vt2tm _ (lifts {a = a} ρ x)
  lifts⇒β* {vt = `Var} σ (zero) = []
  lifts⇒β* {vt = `Tm}  σ (zero) = []
  lifts⇒β* {vt = `Var} σ (suc x)   = subst⇒β*₀ {vt = `Var} suc (σ x)
  lifts⇒β* {vt = `Tm}  σ (suc x)   = subst⇒β*₀ {vt = `Var} suc (σ x)

-- Altenkirch's weak standardization lemma.

mutual
  beta-shr : ∀ {i a Γ} {t tβ th : Tm Γ a}
    → t ⇒β tβ
    → t ⟨ i ⟩⇒ th
    → (tβ ≡ th) ⊎ ∃ λ t' → tβ ⟨ i ⟩⇒ t' × th ⇒β* t'
  beta-shr β (β 𝒖)                                                   = inj₁ ≡.refl
  beta-shr (cong (appl u) (appl .u) (cong abs abs tβ⇒)) (β 𝒖)        = inj₂ (_ , β 𝒖 , (subst⇒β (sgs u) tβ⇒ ∷ []))
  beta-shr (cong (appr ._) (appr ._) tβ⇒) (β {t = t} 𝒖)
    = inj₂ (_ , β (mapβSN tβ⇒ 𝒖) , subst⇒β* {vt = `Tm} (λ { {._} (zero) → tβ⇒ ∷ [] ; (suc x) → [] }) t)
  beta-shr β (cong (appl u) (appl .u) (cong () 𝑬𝒕' th⇒))
  beta-shr (cong E1 E2 t⇒) (cong E0 E3 th⇒)                          = helper E1 E2 t⇒ E0 E3 th⇒

    where
      helper : ∀ {i}{a Γ} {t tβ th : Tm Γ a} {Δ a₁} {t₁ ta : Tm Δ a₁}
           {E : βECxt Γ Δ a₁ a} {a₂} {t₂ tb : Tm Γ a₂} {E₁ : ECxt Γ a₂ a}
        → βEhole t E t₁
        → βEhole tβ E ta
        → t₁ ⇒β ta
        → Ehole t E₁ t₂
        → Ehole th E₁ tb
        → t₂ ⟨ i ⟩⇒ tb
        → tβ ≡ th ⊎ ∃ λ t' → tβ ⟨ i ⟩⇒ t' × th ⇒β* t'
      helper (appl u) (appl .u) t⇒₁ (appl .u) (appl .u) th⇒₁ with beta-shr t⇒₁ th⇒₁
      helper (appl u) (appl .u) t⇒₁ (appl .u) (appl .u) th⇒₁ | inj₁ ≡.refl = inj₁ ≡.refl
      helper (appl u) (appl .u) t⇒₁ (appl .u) (appl .u) th⇒₁ | inj₂ (tm , h⇒tm , tm⇒β)
             = inj₂ (_ , cong (appl _) (appl _) h⇒tm , cong* (appl _) (appl _) tm⇒β)
      helper (appr t₂) (appr .t₂) t⇒₁ (appl t₁) (appl .t₁) th⇒₁ = inj₂ (_ , cong (appl _) (appl _) th⇒₁ , (cong (appr _) (appr _) t⇒₁ ∷ []))

  -- SNe is preserved under reduction.

  mapβSNe : ∀ {i a Γ} {t t' : Tm Γ a}
   → t ⇒β t'
   → SNe {i} t
   → SNe {i} t'
  mapβSNe (cong (appl u) (appl .u) t⇒)  (elim 𝒏 (appl 𝒖))  = elim (mapβSNe t⇒ 𝒏) (appl 𝒖)
  mapβSNe (cong (appr u) (appr .u) t⇒)  (elim 𝒏 (appl 𝒖))  = elim 𝒏 (appl (mapβSN t⇒ 𝒖))
  -- The other cases are impossible
  mapβSNe (cong abs abs t⇒)             (elim 𝒏 ())
  mapβSNe β                             (elim (elim 𝒏 ()) (appl 𝒖))

  -- SN is preserved under reduction.

  mapβSN : ∀ {i a Γ} {t t' : Tm Γ a}
    → t ⇒β t'
    → SN {i} t
    → SN {i} t'
  mapβSN t⇒                (ne 𝒏)                = ne (mapβSNe t⇒ 𝒏)
  mapβSN (cong abs abs t⇒) (abs 𝒕)               = abs (mapβSN t⇒ 𝒕)
  mapβSN t⇒                (exp t⇒₁ 𝒕)           with beta-shr t⇒ t⇒₁
  mapβSN t⇒ (exp t⇒₁ 𝒕) | inj₁ ≡.refl = 𝒕
  mapβSN t⇒ (exp t⇒₁ 𝒕) | inj₂ (_ , t⇒h , t⇒β*)  = exp t⇒h (mapβ*SN t⇒β* 𝒕)

  -- SN is preserved under multi-step reduction.

  mapβ*SN : ∀ {i a Γ} {t t' : Tm Γ a}
   → t ⇒β* t'
   → SN {i} t
   → SN {i} t'
  mapβ*SN []          𝒕 = 𝒕
  mapβ*SN (t⇒ ∷ t⇒β*) 𝒕 = mapβ*SN t⇒β* (mapβSN t⇒ 𝒕)

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


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

open import Cubical.Relation.Binary.Base
open import Cubical.Core.Everything

module Cubical.Relation.Binary.Raw.Structures
  {a ℓ} {A : Type a} -- The underlying type
  (_<>_ : RawRel A ℓ)   -- The relation
  where

open import Cubical.Foundations.Prelude using (refl; sym)
open import Cubical.Foundations.Function using (_∘_)

open import Cubical.Data.Prod.Base using (proj₁; proj₂; _,_)
open import Cubical.Relation.Nullary.Decidable
open import Cubical.Relation.Binary.Raw.Definitions
open import Cubical.Relation.Binary.Raw.Properties

private
  variable
    ℓ₂ : Level

------------------------------------------------------------------------
-- Preorders
------------------------------------------------------------------------

record IsPreorder : Type (ℓ-max a ℓ) where
  constructor ispreorder
  field
    reflexive  : Reflexive _<>_
    transitive : Transitive _<>_

  fromEq : FromEq _<>_
  fromEq = reflx→fromeq _<>_ reflexive

------------------------------------------------------------------------
-- Equivalences
------------------------------------------------------------------------

record IsPartialEquivalence : Type (ℓ-max a ℓ) where
  constructor ispartialeq
  field
    symmetric  : Symmetric _<>_
    transitive : Transitive _<>_

record IsEquivalence : Type (ℓ-max a ℓ) where
  constructor isequivalence
  field
    reflexive            : Reflexive _<>_
    isPartialEquivalence : IsPartialEquivalence

  open IsPartialEquivalence isPartialEquivalence public

  from-≡ : FromEq _<>_
  from-≡ = reflx→fromeq _<>_ reflexive

  isPreorder : IsPreorder
  isPreorder = record
    { reflexive  = reflexive
    ; transitive = transitive
    }

record IsDecEquivalence : Type (ℓ-max a ℓ) where
  constructor isdeceq
  infix 4 _≟_
  field
    isEquivalence : IsEquivalence
    _≟_           : Decidable _<>_

  open IsEquivalence isEquivalence public

------------------------------------------------------------------------
-- Partial orders
------------------------------------------------------------------------

record IsPartialOrder : Type (ℓ-max a ℓ) where
  constructor ispartialorder
  field
    isPreorder : IsPreorder
    antisym    : Antisymmetric _<>_

  open IsPreorder isPreorder public

record IsDecPartialOrder : Type (ℓ-max a ℓ) where
  constructor isdecpartialorder
  infix 4 _≤?_
  field
    isPartialOrder : IsPartialOrder
    _≤?_           : Decidable _<>_

  open IsPartialOrder isPartialOrder public

  private
    lemma : ∀ {x y} → ¬ x <> y → ¬ x ≡ y
    lemma x≰y x≡y = x≰y (fromEq x≡y)

  _≟_ : Discrete A
  _≟_ x y with x ≤? y
  ... | no ¬p = no (lemma ¬p)
  ... | yes p with y ≤? x
  ...   | no ¬q = no (lemma ¬q ∘ sym)
  ...   | yes q = yes (antisym p q)

record IsStrictPartialOrder : Type (ℓ-max a ℓ) where
  constructor isstrictpartialorder
  field
    irrefl     : Irreflexive _<>_
    transitive : Transitive _<>_

  asym : Asymmetric _<>_
  asym {x} {y} = trans∧irr→asym _<>_ transitive irrefl

record IsDecStrictPartialOrder : Type (ℓ-max a ℓ) where
  constructor isdecstrictpartialorder
  infix 4 _<?_
  field
    isStrictPartialOrder : IsStrictPartialOrder
    _<?_                 : Decidable _<>_

  open IsStrictPartialOrder isStrictPartialOrder public

------------------------------------------------------------------------
-- Total orders
------------------------------------------------------------------------

record IsTotalOrder : Type (ℓ-max a ℓ) where
  constructor istotalorder
  field
    isPartialOrder : IsPartialOrder
    total          : PropTotal _<>_

  open IsPartialOrder isPartialOrder public

record IsDecTotalOrder : Type (ℓ-max a ℓ) where
  constructor isdectotalorder
  infix 4 _≤?_
  field
    isTotalOrder : IsTotalOrder
    _≤?_         : Decidable _<>_

  open IsTotalOrder isTotalOrder public

  isDecPartialOrder : IsDecPartialOrder
  isDecPartialOrder = record
    { isPartialOrder = isPartialOrder
    ; _≤?_           = _≤?_
    }

  open IsDecPartialOrder isDecPartialOrder public using (_≟_)

-- Note that these orders are decidable. The current implementation
-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
-- definition capturing these three properties implies decidability
-- as `Trichotomous` necessarily separates out the equality case.

record IsStrictTotalOrder : Type (ℓ-max a ℓ) where
  constructor isstricttotalorder
  field
    transitive : Transitive _<>_
    compare    : Trichotomous _<>_

  infix 4 _<?_

  _<?_ : Decidable _<>_
  _<?_ = tri→dec< _<>_ compare

  _≟_ : Discrete A
  _≟_ = tri→dec≡ _<>_ compare

  isStrictPartialOrder : IsStrictPartialOrder
  isStrictPartialOrder = record
    { irrefl     = tri→irr _<>_ compare
    ; transitive = transitive
    }

  isDecStrictPartialOrder : IsDecStrictPartialOrder
  isDecStrictPartialOrder = record
    { isStrictPartialOrder = isStrictPartialOrder
    ; _<?_                 = _<?_
    }

  open IsStrictPartialOrder isStrictPartialOrder public hiding (transitive)


text:
module Algebra where

-- Core graph construction primitives
data Graph (A : Set) : Set where
    ε   : Graph A                       -- Empty graph
    v   : A -> Graph A                  -- Graph comprising a single vertex
    _+_ : Graph A -> Graph A -> Graph A -- Overlay two graphs
    _*_ : Graph A -> Graph A -> Graph A -- Connect two graphs

infixl 4  _≡_
infixl 8  _+_
infixl 9  _*_
infix  10 _⊆_

-- Equational theory of graphs
data _≡_ {A} : (x y : Graph A) -> Set where
    -- Equivalence relation
    reflexivity  : ∀ {x     : Graph A} ->                   x ≡ x
    symmetry     : ∀ {x y   : Graph A} -> x ≡ y ->          y ≡ x
    transitivity : ∀ {x y z : Graph A} -> x ≡ y -> y ≡ z -> x ≡ z

    -- Congruence
    +left-congruence  : ∀ {x y z : Graph A} -> x ≡ y -> x + z ≡ y + z
    +right-congruence : ∀ {x y z : Graph A} -> x ≡ y -> z + x ≡ z + y
    *left-congruence  : ∀ {x y z : Graph A} -> x ≡ y -> x * z ≡ y * z
    *right-congruence : ∀ {x y z : Graph A} -> x ≡ y -> z * x ≡ z * y

    -- Axioms of +
    +commutativity : ∀ {x y : Graph A}   -> x + y       ≡ y + x
    +associativity : ∀ {x y z : Graph A} -> x + (y + z) ≡ (x + y) + z

    -- Axioms of *
    *left-identity  : ∀ {x     : Graph A} -> ε * x       ≡ x
    *right-identity : ∀ {x     : Graph A} -> x * ε       ≡ x
    *associativity  : ∀ {x y z : Graph A} -> x * (y * z) ≡ (x * y) * z

    -- Other axioms
    left-distributivity  : ∀ {x y z : Graph A} -> x * (y + z) ≡ x * y + x * z
    right-distributivity : ∀ {x y z : Graph A} -> (x + y) * z ≡ x * z + y * z
    decomposition        : ∀ {x y z : Graph A} -> x * y * z   ≡ x * y + x * z + y * z

-- Subgraph relation
_⊆_ : ∀ {A} -> Graph A -> Graph A -> Set
x ⊆ y = x + y ≡ y

max_stars_repo_name: asr/alga

max_issues_repo_name: asr/alga

max_forks_repo_name: asr/alga


text:
-- Andreas, 2014-01-10, reported by fredrik.forsberg

record ⊤ : Set where

record Σ (A : Set) (B : A → Set) : Set  where

syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

test : Set
test = {! Σ[ x ∈ ⊤ ] ?!}

-- Fredrik's report:

-- Using the darcs version of Agda from today 10 January,
-- if I load the file and give (or refine) in the hole, I end up with
--
--   test = Σ ⊤ (λ x → {!!})
--
-- i.e. Agda has translated away the syntax Σ[ x ∈ ⊤ ] {!!} for me.
-- I would of course expect
--
--   test = Σ[ x ∈ ⊤ ] {!!}
--
-- instead, and I think this used to be the behaviour? (Using the Σ from
-- the standard library, this is more annoying, as one gets
--
--   test = Σ-syntax ⊤ (λ x → {!!})
--
-- as a result.)
--
-- This might be related to issue 994?

-- Expected test case behavior:
--
-- Bad (at the time of report:
--
--   (agda2-give-action 0 "Σ ⊤ (λ x → ?)")
--
-- Good:
--
--   (agda2-give-action 0 'no-paren)


text:
module heap.libraryNat where

open import Data.Nat renaming (_⊔_ to _⊔n_; _≟_ to _≟ℕ_) hiding ( _<_ )
open import Data.Bool
open import Data.Fin hiding (pred)
open import Data.Unit
open import Data.Empty
open import Function
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

{-
--- WARNING USES TODO
postulate TODO : {A : Set} → A
-}

_==b_ : ℕ → ℕ → Bool
zero ==b zero = true
zero ==b suc a' = false
suc a ==b zero = false
suc a ==b suc a' = a ==b a'

transferℕ  : (P : ℕ → Set)
            → (a a' : ℕ) → T (a ==b a')
            → P a → P a'
transferℕ P zero zero aa' q = q
transferℕ P zero (suc a') () q
transferℕ P (suc a) zero () q
transferℕ P (suc a) (suc a') aa' q = transferℕ (P ∘ suc) a a' aa' q

_<ℕb_ : ℕ → ℕ → Bool
_ <ℕb zero = false
zero <ℕb suc a' = true
suc a <ℕb suc a' = a <ℕb a'

_<ℕ_ : ℕ → ℕ → Set
n <ℕ m = T (n <ℕb m)

_≦ℕb_ : ℕ → ℕ → Bool
zero ≦ℕb _ = true
suc a ≦ℕb zero = false
suc a ≦ℕb suc a' = a ≦ℕb a'

_≧ℕb_ : ℕ → ℕ → Bool
n ≧ℕb m = m ≦ℕb n

<ℕb-suc : {a b : ℕ} → T (a <ℕb b) → T (a <ℕb suc b)
<ℕb-suc{zero} = λ _ → tt
<ℕb-suc{_}{zero} ()
<ℕb-suc{suc a}{suc b} = <ℕb-suc{a}{b}

<ℕb-suc' : {a b : ℕ} → T (a ≦ℕb b) → T (a <ℕb suc b)
<ℕb-suc' {zero} {zero} ab = ab
<ℕb-suc' {zero} {suc b} ab = ab
<ℕb-suc' {suc a} {zero} ab = ab
<ℕb-suc' {suc a} {suc b} ab = <ℕb-suc'{a}{b} ab

n<sucnLem : {n m : ℕ} → T  (n ==b m) → T (n <ℕb suc m)
n<sucnLem {zero} {zero} nm = tt
n<sucnLem {zero} {suc m} ()
n<sucnLem {suc n} {zero} ()
n<sucnLem {suc n} {suc m} nm = n<sucnLem {n} {m} nm

n<mImpliesn/=m : (n m : ℕ) → T (m <ℕb n) → ¬ T (n ==b m)
n<mImpliesn/=m zero m ()
n<mImpliesn/=m (suc n) zero p ()
n<mImpliesn/=m (suc n) (suc m) p q = n<mImpliesn/=m n m p q

le : {n m : ℕ} → ¬ (n ==b m) ≡ false → T (n ==b m)
le{zero}{zero} p = tt
le {zero} {suc n} p = p refl
le {suc n} {zero} p = p refl
le {suc n} {suc m} p = le{n}{m} p

refl==b : {n : ℕ} → T (n ==b n)
refl==b {zero} = tt
refl==b {suc n} = refl==b {n}

symb : (n m : ℕ) → T (n ==b m) → T (m ==b n)
symb zero zero p = tt
symb zero (suc m) ()
symb (suc n) zero ()
symb (suc n) (suc m) p = symb n m p

neqsymb : (n m : ℕ) → ¬ T (n ==b m) → ¬ T (m ==b n)
neqsymb n m p q = p (symb m n q)

n<ℕbsucn : {n : ℕ} → T (n <ℕb suc n)
n<ℕbsucn {zero} = tt
n<ℕbsucn {suc n} = n<ℕbsucn{n}

n≦ℕbsucn : {n : ℕ} → T (n ≦ℕb suc n)
n≦ℕbsucn {zero} = tt
n≦ℕbsucn {suc n} = n≦ℕbsucn {n}

¬n<ℕbn : {n : ℕ} → ¬ (T (n <ℕb n))
¬n<ℕbn {zero} ()
¬n<ℕbn {suc n} p = ¬n<ℕbn {n} p

refl≦ℕb : (n : ℕ) → T (n ≦ℕb n)
refl≦ℕb zero = tt
refl≦ℕb (suc n) = refl≦ℕb n

trans≦ℕb : (n m k : ℕ) → T (n ≦ℕb m) → T (m ≦ℕb k) → T (n ≦ℕb k)
trans≦ℕb zero m k nm mk = tt
trans≦ℕb (suc n) zero k () mk
trans≦ℕb (suc n) (suc m) zero nm ()
trans≦ℕb (suc n) (suc m) (suc k) nm mk = trans≦ℕb n m k nm mk

⊔isMaxl : {n m : ℕ} →   T (n ≦ℕb (n ⊔n m ))
⊔isMaxl {zero} {m} = tt
⊔isMaxl {suc n} {zero} = refl≦ℕb (suc n)
⊔isMaxl {suc n} {suc m} = ⊔isMaxl {n} {m}

⊔isMaxr : {n m : ℕ} →   T (m ≦ℕb (n ⊔n m ))
⊔isMaxr {n} {zero}  = tt
⊔isMaxr {zero} {suc m}  = refl≦ℕb (suc m)
⊔isMaxr {suc n} {suc m} = ⊔isMaxr {n} {m}

⊔zero : {n : ℕ} → (n ⊔n zero) ≡ n
⊔zero {zero} = refl
⊔zero {suc n} = refl

⊔isMaxl' : {n m k : ℕ} →   T (n ≦ℕb m ) → T (n ≦ℕb (m ⊔n k ))
⊔isMaxl' {zero} {m} {k} = λ _ → tt
⊔isMaxl' {suc n} {zero} {k} = λ ()
⊔isMaxl' {suc n} {suc m} {zero} = λ z → z
⊔isMaxl' {suc n} {suc m} {suc k} = ⊔isMaxl'{n}{m}

⊔isMax<l : {n m k : ℕ} →   T ((n ⊔n m) <ℕb k) → T (n <ℕb k)
⊔isMax<l {n} {m} {zero} p = p
⊔isMax<l {zero} {m} {suc k} p = tt
⊔isMax<l {suc n} {zero} {suc k} p = p
⊔isMax<l {suc n} {suc m} {suc k} p = ⊔isMax<l {n} {m} {k} p

⊔isMax<r : {n m k : ℕ} →   T ((n ⊔n m) <ℕb k) → T (m <ℕb k)
⊔isMax<r {n} {zero} {zero} p = p
⊔isMax<r {n} {zero} {suc k} p = tt
⊔isMax<r {zero} {suc m} {k} p = p
⊔isMax<r {suc n} {suc m} {zero} p = p
⊔isMax<r {suc n} {suc m} {suc k} p = ⊔isMax<r{n}{m}{k} p

sucinvertible : {n m : ℕ} → suc n ≡ suc m → n ≡ m
sucinvertible {n} {m} = cong pred

¬n≡m→¬sucn≡sucm : {n m : ℕ} → ¬ (n ≡ m) → ¬ (suc n ≡ suc m)
¬n≡m→¬sucn≡sucm {n} {m} p q = p (sucinvertible q)

<impliesnoteq : {n m : ℕ} → T (n  <ℕb m) → ¬ (n ≡ m)
<impliesnoteq {n} {zero} p = λ _ → p
<impliesnoteq {zero} {suc m} p = λ ()
<impliesnoteq {suc n} {suc m} p = ¬n≡m→¬sucn≡sucm {n}{m} (<impliesnoteq{n}{m} p)

<impliesNot= = <impliesnoteq

-- {- Fin n related lemmata -}

-- fromℕ< : ∀ {n m} → n <ℕ m → Fin m
-- fromℕ< {_} {zero} ()
-- fromℕ< {zero} {suc m} p = zero
-- fromℕ< {suc n} {suc m} p = suc (fromℕ< {n} {m} p)

update : {A : Set} (f : ℕ → A) (n : ℕ) (a : A) → ℕ → A
update {A} f n a m = aux  (n ≟ℕ m)
    module updateaux where
           aux : Dec (n ≡ m)
                 →  A
           aux (yes _) = a
           aux (no _) = f m

updateLem : {A : Set}(Q : A → Set)(f : ℕ → A)(n : ℕ)(a : A)
            → (m :  ℕ)
            → ¬ (n ≡ m)
            → Q (f m)
            → Q (update f n a m)
updateLem {A} Q f n a m nm Qfm = aux (n ≟ℕ m)
     module  updateLemaux where
        aux : (x : Dec (n ≡ m)) → Q(updateaux.aux f n a m x)
        aux (yes p) = ⊥-elim (nm p)
        aux (no ¬p) = Qfm

updateLem2 : {A : Set}(f : ℕ → A)(n : ℕ)(a : A)(m : ℕ)
            → (n ≡ m)
            → update f n a m ≡ a
updateLem2 {A} f n a m nm = aux (n ≟ℕ m)
     module  updateLem2aux where
        aux : (x : Dec (n ≡ m)) → updateaux.aux f n a m x ≡ a
        aux (yes p) = refl
        aux (no ¬p) = ⊥-elim (¬p nm)

updateLem3 : {A : Set}(f : ℕ → A)(n : ℕ)(a : A)(m : ℕ)
            → ¬ (n ≡ m)
            → update f n a m ≡ f m
updateLem3 f n a m nm = updateLem (λ a' → a' ≡ f m) f n a m nm refl

leqEmbedLem : (P : ℕ → Set) → (l : (n : ℕ) → P n → P (suc n))
              → (n m : ℕ) → T (n ≦ℕb m) → P n → P m
leqEmbedLem P l zero zero nm p = p
leqEmbedLem P l zero (suc m) nm p = l m (leqEmbedLem P l zero m tt p)
leqEmbedLem P l (suc n) zero () p
leqEmbedLem P l (suc n) (suc m) nm p = leqEmbedLem (P ∘ suc) (l ∘ suc) n m nm p

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


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

module Number.Instances.QuoIntFromInt where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything hiding (⋆) renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)

open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool as Bool using (Bool; not; true; false)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)
open import Function.Base using (it; _∋_; _$_)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.HITs.PropositionalTruncation --.Properties

open import Utils using (!_; !!_)
open import MoreLogic.Reasoning
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Structures
open import MorePropAlgebra.Bundles
open import MorePropAlgebra.Consequences
open import Number.Structures2
open import Number.Bundles2

import Agda.Builtin.Int as Builtin
import Data.Integer.Base as BuiltinBase
import Data.Integer.Properties as BuiltinProps

open import Cubical.Data.Nat.Literals
open import Number.Prelude.Nat
open import Number.Prelude.Int
import Cubical.Data.Int as Int
import Number.Instances.Int

open import Cubical.HITs.Ints.QuoInt as QuoInt using
  ( ℤ
  ; _+_
  ; -_
  ; Int≡ℤ
  ; signed
  ; posneg
  ; ℤ→Int
  ; sucℤ
  ; predℤ
  ; sign
  ; abs
  ; pos
  ; neg
  ; +-comm
  ; +-assoc
  ; sucℤ-+ʳ
  ) renaming
  ( _*_ to _·_ )

ℤ≡Int = sym Int≡ℤ

private
  _·ᵗʳ_ : Int → Int → Int
  _·ᵗʳ_ = transport (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) _·_

  ·≡·ᵗʳ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) _·_ _·ᵗʳ_
  ·≡·ᵗʳ i = transp (λ j → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j)) (~ i) _·_

  lemma1 : ∀ a b → b +ⁿ a ·ⁿ suc b ≡ a ·ⁿ b +ⁿ (a +ⁿ b)
  lemma1 a b =
    b +ⁿ a ·ⁿ suc b    ≡⟨ (λ i → b +ⁿ ·ⁿ-suc a b i) ⟩
    b +ⁿ (a +ⁿ a ·ⁿ b) ≡⟨ +ⁿ-assoc b a (a ·ⁿ b) ⟩
    (b +ⁿ a) +ⁿ a ·ⁿ b ≡⟨ (λ i → +ⁿ-comm b a i +ⁿ a ·ⁿ b) ⟩
    (a +ⁿ b) +ⁿ a ·ⁿ b ≡⟨ +ⁿ-comm (a +ⁿ b) (a ·ⁿ b) ⟩
    a ·ⁿ b +ⁿ (a +ⁿ b) ∎

  ·ᵗʳ≡'·ᶻ : ∀ a b → a ·ᵗʳ b ≡ a ·ᶻ b
  ·ᵗʳ≡'·ᶻ (posᶻ      0 ) (posᶻ      0 )   = refl
  ·ᵗʳ≡'·ᶻ (posᶻ      0 ) (posᶻ (suc b))   = refl
  ·ᵗʳ≡'·ᶻ (posᶻ (suc a)) (posᶻ      0 )   = refl
  ·ᵗʳ≡'·ᶻ (posᶻ (suc a)) (posᶻ (suc b))   = refl
  ·ᵗʳ≡'·ᶻ (posᶻ      0 ) (negsucᶻ   b )   = refl
  ·ᵗʳ≡'·ᶻ (posᶻ (suc a)) (negsucᶻ   b ) i = negsucᶻ (lemma1 a b i)
  ·ᵗʳ≡'·ᶻ (negsucᶻ   a ) (posᶻ      0 ) i = ℤ→Int (signed sneg (·ⁿ-nullifiesʳ a i))
  ·ᵗʳ≡'·ᶻ (negsucᶻ   a ) (posᶻ (suc b)) i = negsucᶻ (lemma1 a b i)
  ·ᵗʳ≡'·ᶻ (negsucᶻ   a ) (negsucᶻ   b )   = refl

  ·ᵗʳ≡·ᶻ : _·ᵗʳ_ ≡ _·ᶻ_
  ·ᵗʳ≡·ᶻ i a b = ·ᵗʳ≡'·ᶻ a b i

·≡·ᶻ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) _·_ _·ᶻ_
·≡·ᶻ = J (λ _⋆_ _ → PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) _·_ _⋆_) ·≡·ᵗʳ ·ᵗʳ≡·ᶻ

-- ·-assoc''''' : ∀ a b c → a · (b · c) ≡ (a · b) · c
-- ·-assoc''''' = transport γ ·-assoc where
--   γ : ((m n o : Z) → m · (n · o) ≡ (m · n) · o)
--     ≡ ((a b c : ℤ) → a · (b · c) ≡ (a · b) · c)
--   γ i = let _⋆_ = QuoInt·≡· i in (x y z : ℤ≡Int i) → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z

sucInt-preserves-ℤ→Int : ∀ a → sucInt (ℤ→Int a) ≡ ℤ→Int (sucℤ a)
sucInt-preserves-ℤ→Int (signed spos n) = refl
sucInt-preserves-ℤ→Int (signed sneg zero) = refl
sucInt-preserves-ℤ→Int (signed sneg (suc zero)) = refl
sucInt-preserves-ℤ→Int (signed sneg (suc (suc n))) = refl
sucInt-preserves-ℤ→Int (posneg i) = refl

predInt-preserves-ℤ→Int : ∀ a → predInt (ℤ→Int a) ≡ ℤ→Int (predℤ a)
predInt-preserves-ℤ→Int (signed spos zero) = refl
predInt-preserves-ℤ→Int (signed spos (suc n)) = refl
predInt-preserves-ℤ→Int (signed sneg zero) = refl
predInt-preserves-ℤ→Int (signed sneg (suc n)) = refl
predInt-preserves-ℤ→Int (posneg i) = refl

-sucℤ-sucℤ≡id : ∀ a → - sucℤ (- sucℤ a) ≡ a
-sucℤ-sucℤ≡id (signed spos n) = refl
-sucℤ-sucℤ≡id (signed sneg zero) = posneg
-sucℤ-sucℤ≡id (signed sneg (suc n)) = refl
-sucℤ-sucℤ≡id (posneg i) j = posneg (i ∧ j)

sucℤ-sucℤ-≡id : ∀ a → sucℤ (- sucℤ (- a)) ≡ a
sucℤ-sucℤ-≡id (signed spos zero) i = posneg (~ i)
sucℤ-sucℤ-≡id (signed spos (suc n)) = refl
sucℤ-sucℤ-≡id (signed sneg n) = refl
sucℤ-sucℤ-≡id (posneg i) j = posneg (i ∨ (~ j))

-sucℤ-sucℤ≡sucℤ-sucℤ- : ∀ a → - sucℤ (- sucℤ a) ≡ sucℤ (- sucℤ (- a))
-sucℤ-sucℤ≡sucℤ-sucℤ- a = -sucℤ-sucℤ≡id a ∙ sym (sucℤ-sucℤ-≡id a)

private
  _+ᵗʳ_ : Int → Int → Int
  _+ᵗʳ_ = transport (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) _+_

  +≡+ᵗʳ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) _+_ _+ᵗʳ_
  +≡+ᵗʳ i = transp (λ j → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j)) (~ i) _+_

  +ᵗʳ≡'+ᶻ : ∀ a b → a +ᵗʳ b ≡ a +ᶻ b
  +ᵗʳ≡'+ᶻ (posᶻ      0 ) (posᶻ      0 )   = refl
  +ᵗʳ≡'+ᶻ (posᶻ      0 ) (posᶻ (suc b))  i = sucInt (Int.+-comm (posᶻ b) 0 i)
  +ᵗʳ≡'+ᶻ (posᶻ (suc a)) (posᶻ      0 )  i = ℤ→Int (sucℤ (+-comm (pos a) 0 i))
  +ᵗʳ≡'+ᶻ (posᶻ (suc a)) (posᶻ (suc b))   =
    (posᶻ (suc a) +ᵗʳ posᶻ (suc b))  ≡⟨ sym (sucInt-preserves-ℤ→Int (signed spos a + signed spos (suc b))) ⟩
    sucInt (posᶻ a +ᵗʳ posᶻ (suc b)) ≡⟨ (λ i → sucInt $ (+ᵗʳ≡'+ᶻ (posᶻ a) (posᶻ (suc b)) ∙ sucInt+ (posᶻ a) (posᶻ b)) i) ⟩
    sucInt (posᶻ (suc a) +pos b)   ∎
  +ᵗʳ≡'+ᶻ (posᶻ      0 ) (negsucᶻ   b )   = sym (+negsuc-identityˡ b)
  +ᵗʳ≡'+ᶻ (posᶻ (suc a)) (negsucᶻ   b )   =
    (posᶻ (suc a) +ᵗʳ negsucᶻ b)  ≡⟨ sym $ sucInt-preserves-ℤ→Int (signed spos a + signed sneg (suc b)) ⟩
    sucInt (posᶻ a +ᵗʳ negsucᶻ b) ≡⟨ (λ i → sucInt $ +ᵗʳ≡'+ᶻ (posᶻ a) (negsucᶻ b) i) ⟩
    sucInt (posᶻ a +ᶻ  negsucᶻ b) ≡⟨ sucInt+ (posᶻ a) (negsucᶻ b) ⟩
    (posᶻ (suc a) +negsuc b)    ∎
  +ᵗʳ≡'+ᶻ (negsucᶻ   a ) (posᶻ      0 )   i = ℤ→Int $ -_ $  sucℤ $ -_ $ +-comm (signed sneg a) (pos 0) i
  +ᵗʳ≡'+ᶻ (negsucᶻ   a ) (posᶻ (suc b))   =
    (negsucᶻ a +ᵗʳ posᶻ (suc b))  ≡⟨ (λ i → ℤ→Int $ - sucℤ (- sucℤ-+ʳ (signed sneg a) (signed spos b) (~ i))) ⟩
    ℤ→Int (- sucℤ (- sucℤ (signed sneg a + signed spos b))) ≡⟨ (λ i → ℤ→Int $ -sucℤ-sucℤ≡sucℤ-sucℤ- (signed sneg a + signed spos b) i) ⟩
    ℤ→Int (sucℤ (- sucℤ (- (signed sneg a + signed spos b)))) ≡⟨ sym $ sucInt-preserves-ℤ→Int (- sucℤ (- (signed sneg a + signed spos b))) ⟩
    sucInt (negsucᶻ a +ᵗʳ posᶻ b) ≡⟨ (λ i → sucInt $ +ᵗʳ≡'+ᶻ (negsucᶻ a) (posᶻ b) i) ⟩
    sucInt (negsucᶻ a +pos b)   ∎
  +ᵗʳ≡'+ᶻ (negsucᶻ zero) (negsucᶻ b) = sym $ negsuc+negsuc≡+ⁿ 0 b
  +ᵗʳ≡'+ᶻ (negsucᶻ (suc a)) (negsucᶻ b) =
   (negsucᶻ (suc a) +ᵗʳ negsucᶻ b)   ≡⟨ sym $ predInt-preserves-ℤ→Int (- sucℤ (- (signed sneg a + signed sneg (suc b)))) ⟩
   predInt (negsucᶻ a +ᵗʳ negsucᶻ b) ≡⟨ (λ i → predInt $ +ᵗʳ≡'+ᶻ (negsucᶻ a) (negsucᶻ b) i) ⟩
   predInt (negsucᶻ a +ᶻ  negsucᶻ b) ≡⟨ predInt+ (negsucᶻ a) (negsucᶻ b) ⟩
   (negsucᶻ (suc a) +negsuc b)     ∎

  +ᵗʳ≡+ᶻ : _+ᵗʳ_ ≡ _+ᶻ_
  +ᵗʳ≡+ᶻ i a b = +ᵗʳ≡'+ᶻ a b i

+≡+ᶻ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) _+_ _+ᶻ_
+≡+ᶻ = J (λ _+ᵗʳ_ _ → PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) _+_ _+ᵗʳ_) +≡+ᵗʳ +ᵗʳ≡+ᶻ

private
  -ᵗʳ_ : Int → Int
  -ᵗʳ_ = transport (λ i → (ℤ≡Int i → ℤ≡Int i)) -_

  -≡-ᵗʳ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i)) -_ -ᵗʳ_
  -≡-ᵗʳ i = transp (λ j → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j)) (~ i) -_

  -ᵗʳ≡'-ᶻ : ∀ a → -ᵗʳ a ≡ -ᶻ a
  -ᵗʳ≡'-ᶻ (posᶻ zero) = refl
  -ᵗʳ≡'-ᶻ (posᶻ (suc n)) = refl
  -ᵗʳ≡'-ᶻ (negsucᶻ n) = refl

  -ᵗʳ≡-ᶻ : (-ᵗʳ_) ≡ (-ᶻ_)
  -ᵗʳ≡-ᶻ i a = -ᵗʳ≡'-ᶻ a i

-≡-ᶻ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i)) (-_) (-ᶻ_)
-≡-ᶻ = J (λ -ᵗʳ_ _ → PathP (λ i → (ℤ≡Int i → ℤ≡Int i)) -_ -ᵗʳ_) -≡-ᵗʳ -ᵗʳ≡-ᶻ

min : ℤ → ℤ → ℤ
min x y with sign x | sign y
... | spos | spos = pos (minⁿ (abs x) (abs y))
... | spos | sneg = y
... | sneg | spos = x
... | sneg | sneg = neg (maxⁿ (abs x) (abs y))

max : ℤ → ℤ → ℤ
max x y with sign x | sign y
... | spos | spos = pos (maxⁿ (abs x) (abs y))
... | spos | sneg = x
... | sneg | spos = y
... | sneg | sneg = neg (minⁿ (abs x) (abs y))

private
  minᵗʳ : Int → Int → Int
  minᵗʳ = transport (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) min

  maxᵗʳ : Int → Int → Int
  maxᵗʳ = transport (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) max

  min≡minᵗʳ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) min minᵗʳ
  min≡minᵗʳ i = transp (λ j → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j)) (~ i) min

  max≡maxᵗʳ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) max maxᵗʳ
  max≡maxᵗʳ i = transp (λ j → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j)) (~ i) max

  minᵗʳ≡'minᶻ : ∀ a b → minᵗʳ a b ≡ minᶻ a b
  minᵗʳ≡'minᶻ (posᶻ      0 ) (posᶻ      0 ) = refl
  minᵗʳ≡'minᶻ (posᶻ      0 ) (posᶻ (suc b)) = refl
  minᵗʳ≡'minᶻ (posᶻ (suc a)) (posᶻ      0 ) = refl
  minᵗʳ≡'minᶻ (posᶻ (suc a)) (posᶻ (suc b)) = refl
  minᵗʳ≡'minᶻ (posᶻ      0 ) (negsucᶻ   b ) = refl
  minᵗʳ≡'minᶻ (posᶻ (suc a)) (negsucᶻ   b ) = refl
  minᵗʳ≡'minᶻ (negsucᶻ   a ) (posᶻ      0 ) = refl
  minᵗʳ≡'minᶻ (negsucᶻ   a ) (posᶻ (suc b)) = refl
  minᵗʳ≡'minᶻ (negsucᶻ   a ) (negsucᶻ   b ) = refl

  maxᵗʳ≡'maxᶻ : ∀ a b → maxᵗʳ a b ≡ maxᶻ a b
  maxᵗʳ≡'maxᶻ (posᶻ      0 ) (posᶻ      0 ) = refl
  maxᵗʳ≡'maxᶻ (posᶻ      0 ) (posᶻ (suc b)) = refl
  maxᵗʳ≡'maxᶻ (posᶻ (suc a)) (posᶻ      0 ) = refl
  maxᵗʳ≡'maxᶻ (posᶻ (suc a)) (posᶻ (suc b)) = refl
  maxᵗʳ≡'maxᶻ (posᶻ      0 ) (negsucᶻ   b ) = refl
  maxᵗʳ≡'maxᶻ (posᶻ (suc a)) (negsucᶻ   b ) = refl
  maxᵗʳ≡'maxᶻ (negsucᶻ   a ) (posᶻ      0 ) = refl
  maxᵗʳ≡'maxᶻ (negsucᶻ   a ) (posᶻ (suc b)) = refl
  maxᵗʳ≡'maxᶻ (negsucᶻ   a ) (negsucᶻ   b ) = refl

  minᵗʳ≡minᶻ : minᵗʳ ≡ minᶻ
  minᵗʳ≡minᶻ i a b = minᵗʳ≡'minᶻ a b i

  maxᵗʳ≡maxᶻ : maxᵗʳ ≡ maxᶻ
  maxᵗʳ≡maxᶻ i a b = maxᵗʳ≡'maxᶻ a b i

min≡min : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) min minᶻ
min≡min = J (λ minᵗʳ _ → PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) min minᵗʳ) min≡minᵗʳ minᵗʳ≡minᶻ

max≡max : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) max maxᶻ
max≡max = J (λ maxᵗʳ _ → PathP (λ i → (ℤ≡Int i → ℤ≡Int i → ℤ≡Int i)) max maxᵗʳ) max≡maxᵗʳ maxᵗʳ≡maxᶻ

infixl 4 _<_
_<_ : ∀(x y : ℤ) → hProp ℓ-zero
x < y with sign x | sign y
... | spos | spos = abs x <ⁿ abs y
... | spos | sneg = ⊥
... | sneg | spos = ⊤
... | sneg | sneg = abs y <ⁿ abs x

private

  _<ᵗʳ_ : Int → Int → hProp ℓ-zero
  _<ᵗʳ_ = transport (λ i → (ℤ≡Int i → ℤ≡Int i → hProp ℓ-zero)) _<_

  <≡<ᵗʳ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → hProp ℓ-zero)) _<_ _<ᵗʳ_
  <≡<ᵗʳ i = transp (λ j → ℤ≡Int (i ∧ j) → ℤ≡Int (i ∧ j) → hProp ℓ-zero) (~ i) _<_

  <ᵗʳ⇔<ᶻ : ∀ a b → [ (a <ᵗʳ b) ⇔ (a <ᶻ b) ]
  <ᵗʳ⇔<ᶻ (posᶻ      0 ) (posᶻ      0 ) .fst pᵗʳ = pᵗʳ
  <ᵗʳ⇔<ᶻ (posᶻ      0 ) (posᶻ (suc b)) .fst pᵗʳ = pᵗʳ
  <ᵗʳ⇔<ᶻ (posᶻ (suc a)) (posᶻ      0 ) .fst pᵗʳ = pᵗʳ
  <ᵗʳ⇔<ᶻ (posᶻ (suc a)) (posᶻ (suc b)) .fst pᵗʳ = pᵗʳ
  <ᵗʳ⇔<ᶻ (posᶻ      0 ) (negsucᶻ   b ) .fst pᵗʳ = pᵗʳ
  <ᵗʳ⇔<ᶻ (posᶻ (suc a)) (negsucᶻ   b ) .fst pᵗʳ = pᵗʳ
  <ᵗʳ⇔<ᶻ (negsucᶻ   a ) (posᶻ      0 ) .fst pᵗʳ = pᵗʳ
  <ᵗʳ⇔<ᶻ (negsucᶻ   a ) (posᶻ (suc b)) .fst pᵗʳ = pᵗʳ
  <ᵗʳ⇔<ᶻ (negsucᶻ   a ) (negsucᶻ   b ) .fst pᵗʳ = sucⁿ-creates-<ⁿ b a .snd pᵗʳ
  <ᵗʳ⇔<ᶻ (posᶻ      0 ) (posᶻ      0 ) .snd p  = p
  <ᵗʳ⇔<ᶻ (posᶻ      0 ) (posᶻ (suc b)) .snd p  = p
  <ᵗʳ⇔<ᶻ (posᶻ (suc a)) (posᶻ      0 ) .snd p  = p
  <ᵗʳ⇔<ᶻ (posᶻ (suc a)) (posᶻ (suc b)) .snd p  = p
  <ᵗʳ⇔<ᶻ (negsucᶻ   a ) (posᶻ      0 ) .snd p  = p
  <ᵗʳ⇔<ᶻ (negsucᶻ   a ) (posᶻ (suc b)) .snd p  = p
  <ᵗʳ⇔<ᶻ (negsucᶻ   a ) (negsucᶻ   b ) .snd p  = sucⁿ-creates-<ⁿ b a .fst p

  <ᵗʳ≡<ᶻ : _<ᵗʳ_ ≡ _<ᶻ_
  <ᵗʳ≡<ᶻ i a b = ⇔toPath {P = a <ᵗʳ b} {Q = a <ᶻ b} (<ᵗʳ⇔<ᶻ a b .fst) (<ᵗʳ⇔<ᶻ a b .snd) i

<≡<ᶻ : PathP (λ i → (ℤ≡Int i → ℤ≡Int i → hProp ℓ-zero)) _<_ _<ᶻ_
<≡<ᶻ = J (λ _<ᵗʳ_ _ → PathP (λ i → (ℤ≡Int i → ℤ≡Int i → hProp ℓ-zero)) _<_ _<ᵗʳ_) <≡<ᵗʳ <ᵗʳ≡<ᶻ

is-LinearlyOrderedCommRing : [ isLinearlyOrderedCommRing 0 1 _+_ _·_ -_ _<_ min max ]
is-LinearlyOrderedCommRing = transport γ is-LinearlyOrderedCommRingᶻ where
  γ : ([ isLinearlyOrderedCommRing 0 1 _+ᶻ_ _·ᶻ_ (-ᶻ_) _<ᶻ_ minᶻ maxᶻ ])
    ≡ [ isLinearlyOrderedCommRing 0 1 _+_ _·_ -_ _<_ min max ]
  γ i = [ isLinearlyOrderedCommRing 0ⁱ 1ⁱ _+ⁱ_ _·ⁱ_ -ⁱ_ _<ⁱ_ minⁱ maxⁱ ] where
    0ⁱ = transport (λ j → ℤ≡Int (~ i ∧ j)) 0
    1ⁱ = transport (λ j → ℤ≡Int (~ i ∧ j)) 1
    _+ⁱ_ = +≡+ᶻ (~ i)
    _·ⁱ_ = ·≡·ᶻ (~ i)
    -ⁱ_  = -≡-ᶻ (~ i)
    _<ⁱ_ = <≡<ᶻ (~ i)
    minⁱ = min≡min (~ i)
    maxⁱ = max≡max (~ i)

bundle : LinearlyOrderedCommRing {ℓ-zero} {ℓ-zero}
bundle .LinearlyOrderedCommRing.Carrier                    = ℤ
bundle .LinearlyOrderedCommRing.0f                         = 0
bundle .LinearlyOrderedCommRing.1f                         = 1
bundle .LinearlyOrderedCommRing._+_                        = _+_
bundle .LinearlyOrderedCommRing._·_                        = _·_
bundle .LinearlyOrderedCommRing.-_                         = -_
bundle .LinearlyOrderedCommRing.min                        = min
bundle .LinearlyOrderedCommRing.max                        = max
bundle .LinearlyOrderedCommRing._<_                        = _<_
bundle .LinearlyOrderedCommRing.is-LinearlyOrderedCommRing = is-LinearlyOrderedCommRing

·-reflects-< : (x y z : ℤ) → [ 0 < z ] → [ (x · z) < (y · z) ] → [ x < y ]
·-reflects-< = transport γ ·ᶻ-reflects-<ᶻ where
  γ : ((x y z : Int) → [ 0 <ᶻ z ] → [  x ·ᶻ z  <ᶻ  y ·ᶻ z  ] → [ x <ᶻ y ])
    ≡ ((x y z :   ℤ) → [ 0 < z ] → [ (x · z) < (y · z) ] → [ x < y ])
  γ i = let _·'_ = ·≡·ᶻ (~ i); _<'_ = <≡<ᶻ (~ i); 0ⁱ = transport (λ j → ℤ≡Int (~ i ∧ j)) 0 in
      ((x y z :    ℤ≡Int (~ i)) → [ 0ⁱ <' z ] → [ (x ·' z) <' (y ·' z) ] → [ x <' y ])

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals