text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Truncation.FromNegTwo.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Nat
open import Cubical.Data.NatMinusOne
open import Cubical.HITs.Nullification
open import Cubical.HITs.Sn.Base

-- For the hub-and-spoke construction discussed in the HoTT book, which doesn't work in the base case
--  of contractibility, see `HITs.Truncation.Base`. The definition of truncation here contains
--  two more constructors which are redundant when n ≥ 1 but give contractibility when n = 0.

-- data hLevelTrunc {ℓ} (n : HLevel) (A : Type ℓ) : Type (ℓ-max ℓ ℓ') where
--   -- the hub-and-spoke definition in `Truncation.Base`
--   ∣_∣ : A → hLevelTrunc n A
--   hub   : (f : S (-1+ n) → hLevelTrunc n A) → hLevelTrunc n A
--   spoke : (f : S (-1+ n) → hLevelTrunc n A) (s : S) → hub f ≡ f s
--   -- two additional constructors needed to ensure that hLevelTrunc 0 A is contractible
--   ≡hub   : ∀ {x y} (p : S (-1+ n) → x ≡ y) → x ≡ y
--   ≡spoke : ∀ {x y} (p : S (-1+ n) → x ≡ y) (s : S (-1+ n)) → ≡hub p ≡ p s

hLevelTrunc : ∀ {ℓ} → HLevel → Type ℓ → Type ℓ
hLevelTrunc n A = Null (S (-1+ n)) A

-- Note that relative to the HoTT book, this notation is off by +2
∥_∥_ : ∀ {ℓ} → Type ℓ → HLevel → Type ℓ
∥ A ∥ n = hLevelTrunc n A

ext: agda

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:
{-# OPTIONS --safe --warning=error --without-K #-}

open import Groups.Definition
open import Setoids.Setoids
open import Setoids.Subset
open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Groups.Subgroups.Definition
open import Groups.Lemmas

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Groups.Homomorphisms.Image {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+A_ : A → A → A} {_+B_ : B → B → B} {G : Group S _+A_} {H : Group T _+B_} {f : A → B} (fHom : GroupHom G H f) where

imageGroupPred : B → Set (a ⊔ d)
imageGroupPred b = Sg A (λ a → Setoid._∼_ T (f a) b)

imageGroupSubset : subset T imageGroupPred
imageGroupSubset {x} {y} x=y (a , fa=x) = a , transitive fa=x x=y
  where
    open Setoid T
    open Equivalence eq

imageGroupSubgroup : Subgroup H imageGroupPred
Subgroup.isSubset imageGroupSubgroup = imageGroupSubset
Subgroup.closedUnderPlus imageGroupSubgroup {x} {y} (a , fa=x) (b , fb=y) = (a +A b) , transitive (GroupHom.groupHom fHom) (Group.+WellDefined H fa=x fb=y)
  where
    open Setoid T
    open Equivalence eq
Subgroup.containsIdentity imageGroupSubgroup = Group.0G G , imageOfIdentityIsIdentity fHom
Subgroup.closedUnderInverse imageGroupSubgroup {x} (a , fa=x) = Group.inverse G a , transitive (homRespectsInverse fHom) (inverseWellDefined H fa=x)
  where
    open Setoid T
    open Equivalence eq


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

module Data.Binary.Literals where

open import Data.Binary.Base

open import Literals.Number
open import Data.Unit
open import Data.Nat.Literals

instance
  number𝔹 : Number 𝔹
  Number.Constraint number𝔹 = λ _ → ⊤
  Number.fromNat number𝔹 = λ n → ⟦ n ⇑⟧

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module sn-calculus-compatconf where

open import sn-calculus
open import utility renaming (_U̬_ to _∪_)
open import context-properties
  using (get-view ; ->E-view ; ->pot-view)

open import sn-calculus-compatconf.eview
  using (1-steplρ-E-view)
open import sn-calculus-compatconf.pot
  using (1-steplρ-pot)
open import sn-calculus-confluence
  using (R-confluent)

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)

open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; cong ; trans ; subst ; module ≡-Reasoning)
open import Data.Bool
  using (Bool ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; _∷_ ; [] ; _++_)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using ()
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_) renaming (_⊔_ to _⊔ℕ_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; _,′_ ; proj₁ ; proj₂ ; _×_ ; ∃)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function using (_∘_ ; id ; _∋_)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

open ->E-view
open ->pot-view

open EvaluationContext1
open _≐_⟦_⟧e
open Context1
open _≐_⟦_⟧c

open ListSet Data.Nat._≟_

1-step-sn⟶₁ : ∀{p q r BV FV} →
  CorrectBinding p BV FV →
  p sn⟶₁ q →
  p sn⟶₁ r →
  Σ[ p' ∈ Term ] (q sn⟶* p'  ×  r sn⟶* p')
1-step-sn⟶₁ cb psn⟶₁q psn⟶₁r with R-confluent cb psn⟶₁q psn⟶₁r
... | inj₁ refl = _ , rrefl ,′ rrefl
... | inj₂ (inj₁ (_ , qsn⟶₁s , rsn⟶₁s)) =
  _ , sn⟶*-inclusion (sn⟶-inclusion qsn⟶₁s) ,′ sn⟶*-inclusion (sn⟶-inclusion rsn⟶₁s)
... | inj₂ (inj₂ (inj₁ qsn⟶₁r)) =
  _ , sn⟶*-inclusion (sn⟶-inclusion qsn⟶₁r) ,′ rrefl
... | inj₂ (inj₂ (inj₂ rsn⟶₁q)) =
  _ , rrefl ,′ sn⟶*-inclusion (sn⟶-inclusion rsn⟶₁q)

1-steplρ : ∀{p q r θ θq BV FV A Aq} →
  CorrectBinding (ρ⟨ θ , A ⟩· p) BV FV →
  ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θq , Aq ⟩· q →
  p sn⟶ r →
  Σ[ p' ∈ Term ] ((ρ⟨ θq , Aq ⟩· q) sn⟶* p'   ×    (ρ⟨ θ , A ⟩· r) sn⟶* p')
1-steplρ {p} {q} {r} cb
  ρθ·psn⟶₁ρθq·q psn⟶r@(rcontext {.p} {rin} {ro} C p≐C⟦rin⟧ rinsn⟶₁ro)
  with get-view ρθ·psn⟶₁ρθq·q
... | inj₂ (refl , refl , pot) =
  _ ,   1-steplρ-pot cb pot psn⟶r
... | inj₁ (E , qin , qo , p≐E⟦qin⟧ , q≐E⟦qo⟧ , e-view) =
  _ ,  proj₂ (1-steplρ-E-view cb p≐E⟦qin⟧ q≐E⟦qo⟧ e-view p≐C⟦rin⟧ rinsn⟶₁ro)

1-stepl : ∀{p q r BV FV} →
  CorrectBinding p BV FV →
  p sn⟶₁ q →
  p sn⟶ r →
  Σ[ p' ∈ Term ] (q sn⟶* p'  ×  r sn⟶* p')
1-stepl cb psn⟶₁q
        (rcontext [] dchole psn⟶₁r) =
  1-step-sn⟶₁ cb psn⟶₁q psn⟶₁r
1-stepl cb (rpar-done-right p' q')
        (rcontext (ceval (epar₁ _) ∷ crs) (dcpar₁ dcr) psn⟶₁r) =
  ⊥-elim (halted-¬sn⟶ p' (rcontext _ dcr psn⟶₁r))
1-stepl cb (rpar-done-left (dhalted p') q')
        (rcontext (ceval (epar₁ _) ∷ crs) (dcpar₁ dcr) psn⟶₁r) =
  ⊥-elim (halted-¬sn⟶ p' (rcontext _ dcr psn⟶₁r))
1-stepl cb (rpar-done-left (dpaused p') hnothin)
        (rcontext (ceval (epar₁ _) ∷ crs) (dcpar₁ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ dcr psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ dchole
                   (rpar-done-left
                    (dpaused (paused-sn⟶ p' (rcontext _ dcr psn⟶₁r)))
                    hnothin))
1-stepl cb (rpar-done-left (dpaused p') (hexit n))
        (rcontext (ceval (epar₁ _) ∷ crs) (dcpar₁ dcr) psn⟶₁r) =
  _ ,
  rrefl  ,′
  sn⟶*-inclusion (rcontext _ dchole
                   (rpar-done-left
                    (dpaused (paused-sn⟶ p' (rcontext _ dcr psn⟶₁r)))
                    (hexit n)))
1-stepl cb (rpar-done-right p' (dhalted q'))
        (rcontext (ceval (epar₂ p₁) ∷ crs) (dcpar₂ dcr) psn⟶₁r) =
  ⊥-elim (halted-¬sn⟶ q' (rcontext _ dcr psn⟶₁r))
1-stepl cb (rpar-done-right hnothin (dpaused q'))
        (rcontext (ceval (epar₂ .nothin) ∷ crs) (dcpar₂ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ dcr psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ dchole
                   (rpar-done-right
                    hnothin
                    (dpaused (paused-sn⟶ q' (rcontext _ dcr psn⟶₁r)))))
1-stepl cb (rpar-done-right (hexit n) (dpaused q'))
        (rcontext (ceval (epar₂ .(exit n)) ∷ crs) (dcpar₂ dcr) psn⟶₁r) =
  _ ,
  rrefl  ,′
  sn⟶*-inclusion (rcontext _ dchole
                   (rpar-done-right
                    (hexit n)
                    (dpaused (paused-sn⟶ q' (rcontext _ dcr psn⟶₁r)))))
1-stepl cb (rpar-done-left p' q')
        (rcontext (ceval (epar₂ p₁) ∷ crs) (dcpar₂ dcr) psn⟶₁r) =
  ⊥-elim (halted-¬sn⟶ q' (rcontext _ dcr psn⟶₁r))
1-stepl cb rseq-done
        (rcontext _ (dcseq₁ dchole) psn⟶₁r) =
  ⊥-elim (halted-¬sn⟶₁ hnothin psn⟶₁r)
1-stepl cb rseq-exit
        (rcontext _ (dcseq₁ dchole) psn⟶₁r) =
  ⊥-elim (halted-¬sn⟶₁ (hexit _) psn⟶₁r)
1-stepl cb rloopˢ-exit
        (rcontext _ (dcloopˢ₁ dchole) psn⟶₁r) =
  ⊥-elim (halted-¬sn⟶₁ (hexit _) psn⟶₁r)
1-stepl cb (rsuspend-done p')
        (rcontext (ceval (esuspend S) ∷ crs) (dcsuspend dcr) psn⟶₁r) =
  ⊥-elim (halted-¬sn⟶₁ (halted-⟦⟧c p' dcr) psn⟶₁r)
1-stepl cb (rtrap-done p')
        (rcontext (ceval etrap ∷ crs) (dctrap dcr) psn⟶₁r) =
  ⊥-elim (halted-¬sn⟶₁ (halted-⟦⟧c p' dcr) psn⟶₁r)
1-stepl cb rraise-signal (rcontext (csignl S ∷ crs) (dcsignl dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcenv dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ dchole rraise-signal)
1-stepl cb rloop-unroll
        (rcontext (cloop ∷ crs) (dcloop dcr) psn⟶₁r) =

  _ ,
  rstep (rcontext _ (dcloopˢ₁ dcr) psn⟶₁r)
        (rstep (rcontext _ (dcloopˢ₂ dcr) psn⟶₁r) rrefl) ,′
  sn⟶*-inclusion (rcontext [] dchole rloop-unroll)

1-stepl cb rseq-done
        (rcontext (cseq₂ .nothin ∷ crs) (dcseq₂ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ dcr psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ dchole rseq-done)
1-stepl cb rseq-exit
        (rcontext (cseq₂ .(exit _) ∷ crs) (dcseq₂ dcr) psn⟶₁r) =
  _ ,
  rrefl  ,′
  sn⟶*-inclusion (rcontext _ dchole rseq-exit)
1-stepl cb rloopˢ-exit
        (rcontext (cloopˢ₂ .(exit _) ∷ crs) (dcloopˢ₂ dcr) psn⟶₁r) =
  _ ,
  rrefl  ,′
  sn⟶*-inclusion (rcontext _ dchole rloopˢ-exit)
1-stepl {ρ⟨ .θ , .A ⟩· p} cb
        ρθpsn⟶₁q
        ρθpsn⟶r@(rcontext {p = p₂} {p' = r} (cenv θ A ∷ crs) (dcenv p≐crs⟦p₂⟧) p₂sn⟶₁r)
  with ρ-stays-ρ-sn⟶₁ ρθpsn⟶₁q
... | θ' , A' , qin , refl =
  1-steplρ cb ρθpsn⟶₁q (rcontext crs p≐crs⟦p₂⟧ p₂sn⟶₁r)

1-step : ∀{p q r BV FV} →
  CorrectBinding p BV FV →
  p sn⟶ q →
  p sn⟶ r →
  Σ[ p' ∈ Term ] (q  sn⟶* p'  ×  r sn⟶* p')
1-step cb   (rcontext [] dchole psn⟶₁q) psn⟶r =  1-stepl cb psn⟶₁q psn⟶r
1-step cb
       psn⟶q@(rcontext (_ ∷ _) _ _) (rcontext [] dchole psn⟶₁r) with 1-stepl cb psn⟶₁r psn⟶q
... | _ , rsn⟶*p' , qsn⟶*p' =  _ , qsn⟶*p' ,′ rsn⟶*p'
1-step cb@(CBpar cbp cbq _ _ _ _)
       (rcontext (cq ∷ cqs) (dcpar₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcpar₁ dcr) psn⟶₁r)
  with 1-step cbp (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBpar cbp cbq _ _ _ _)
       (rcontext (cq ∷ cqs) (dcpar₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcpar₂ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcpar₂ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcpar₁ dcq) psn⟶₁q)
1-step cb@(CBpar cbp cbq _ _ _ _)
       (rcontext (cq ∷ cqs) (dcpar₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcpar₁ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcpar₁ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcpar₂ dcq) psn⟶₁q)
1-step cb@(CBpar cbp cbq _ _ _ _)
       (rcontext (cq ∷ cqs) (dcpar₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcpar₂ dcr) psn⟶₁r)
  with 1-step cbq (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBseq cbp cbq _)
       (rcontext (cq ∷ cqs) (dcseq₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcseq₁ dcr) psn⟶₁r)
  with 1-step cbp (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb
       (rcontext (cq ∷ cqs) (dcseq₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcseq₂ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcseq₂ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcseq₁ dcq) psn⟶₁q)
1-step cb
       (rcontext (cq ∷ cqs) (dcseq₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcseq₁ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcseq₁ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcseq₂ dcq) psn⟶₁q)
1-step cb@(CBseq cbp cbq _)
       (rcontext (cq ∷ cqs) (dcseq₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcseq₂ dcr) psn⟶₁r)
  with 1-step cbq (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBloopˢ cbp cbq _ _)
       (rcontext (cq ∷ cqs) (dcloopˢ₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcloopˢ₁ dcr) psn⟶₁r)
  with 1-step cbp (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''

1-step cb
       (rcontext (cq ∷ cqs) (dcloopˢ₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcloopˢ₂ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcloopˢ₂ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcloopˢ₁ dcq) psn⟶₁q)
1-step cb
       (rcontext (cq ∷ cqs) (dcloopˢ₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcloopˢ₁ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcloopˢ₁ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcloopˢ₂ dcq) psn⟶₁q)
1-step cb@(CBloopˢ cbp cbq _ _)
       (rcontext (cq ∷ cqs) (dcloopˢ₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcloopˢ₂ dcr) psn⟶₁r)
  with 1-step cbq (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''

1-step cb@(CBsusp cb' _)
       (rcontext (cq ∷ cqs) (dcsuspend dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcsuspend dcr) psn⟶₁r)
  with 1-step cb' (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBtrap cb')
       (rcontext (cq ∷ cqs) (dctrap dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dctrap dcr) psn⟶₁r)
  with 1-step cb' (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBsig cb')
       (rcontext (cq ∷ cqs) (dcsignl dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcsignl dcr) psn⟶₁r)
  with 1-step cb' (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBpresent cbp cbq)
       (rcontext (cq ∷ cqs) (dcpresent₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcpresent₁ dcr) psn⟶₁r)
  with 1-step cbp (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb
       (rcontext (cq ∷ cqs) (dcpresent₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcpresent₂ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcpresent₂ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcpresent₁ dcq) psn⟶₁q)
1-step cb
       (rcontext (cq ∷ cqs) (dcpresent₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcpresent₁ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcpresent₁ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcpresent₂ dcq) psn⟶₁q)
1-step cb@(CBpresent cbp cbq)
       (rcontext (cq ∷ cqs) (dcpresent₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcpresent₂ dcr) psn⟶₁r)
  with 1-step cbq (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBloop cb' _)
       (rcontext (cq ∷ cqs) (dcloop dcq) psn⟶₁q) (rcontext (cr ∷ crs) (dcloop dcr) psn⟶₁r)
  with 1-step cb' (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBshared cb')
       (rcontext (cq ∷ cqs) (dcshared dcq) psn⟶₁q) (rcontext (cr ∷ crs) (dcshared dcr) psn⟶₁r)
  with 1-step cb' (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBvar cb')
       (rcontext (cq ∷ cqs) (dcvar dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcvar dcr) psn⟶₁r)
  with 1-step cb' (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBif cbp cbq)
       (rcontext (cq ∷ cqs) (dcif₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcif₁ dcr) psn⟶₁r)
  with 1-step cbp (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb
       (rcontext (cq ∷ cqs) (dcif₁ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcif₂ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcif₂ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcif₁ dcq) psn⟶₁q)
1-step cb
       (rcontext (cq ∷ cqs) (dcif₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcif₁ dcr) psn⟶₁r) =
  _ ,
  sn⟶*-inclusion (rcontext _ (dcif₁ dcr) psn⟶₁r) ,′
  sn⟶*-inclusion (rcontext _ (dcif₂ dcq) psn⟶₁q)
1-step cb@(CBif cbp cbq)
       (rcontext (cq ∷ cqs) (dcif₂ dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcif₂ dcr) psn⟶₁r)
  with 1-step cbq (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''
1-step cb@(CBρ cb')
       (rcontext (cq ∷ cqs) (dcenv dcq) psn⟶₁q)
       (rcontext (cr ∷ crs) (dcenv dcr) psn⟶₁r)
  with 1-step cb' (rcontext cqs dcq psn⟶₁q) (rcontext crs dcr psn⟶₁r)
... | p'' , q'sn⟶*p'' , r'sn⟶*p'' = _ , Context1-sn⟶* cq q'sn⟶*p'' ,′ Context1-sn⟶* cr r'sn⟶*p''

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An example of how Data.Fin.Substitution can be used: a definition
-- of substitution for the untyped λ-calculus, along with some lemmas
------------------------------------------------------------------------

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

module Data.Fin.Substitution.Example where

open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Nat
open import Data.Fin using (Fin)
open import Data.Vec
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; sym; cong; cong₂)
open PropEq.≡-Reasoning
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star; ε; _◅_)

-- A representation of the untyped λ-calculus. Uses de Bruijn indices.

infixl 9 _·_

data Tm (n : ℕ) : Set where
  var : (x : Fin n) → Tm n
  ƛ   : (t : Tm (suc n)) → Tm n
  _·_ : (t₁ t₂ : Tm n) → Tm n

-- Code for applying substitutions.

module TmApp {ℓ} {T : ℕ → Set ℓ} (l : Lift T Tm) where
  open Lift l hiding (var)

  -- Applies a substitution to a term.

  infix 8 _/_

  _/_ : ∀ {m n} → Tm m → Sub T m n → Tm n
  var x   / ρ = lift (lookup ρ x)
  ƛ t     / ρ = ƛ (t / ρ ↑)
  t₁ · t₂ / ρ = (t₁ / ρ) · (t₂ / ρ)

  open Application (record { _/_ = _/_ }) using (_/✶_)

  -- Some lemmas about _/_.

  ƛ-/✶-↑✶ : ∀ k {m n t} (ρs : Subs T m n) →
            ƛ t /✶ ρs ↑✶ k ≡ ƛ (t /✶ ρs ↑✶ suc k)
  ƛ-/✶-↑✶ k ε        = refl
  ƛ-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (ƛ-/✶-↑✶ k ρs) refl

  ·-/✶-↑✶ : ∀ k {m n t₁ t₂} (ρs : Subs T m n) →
            t₁ · t₂ /✶ ρs ↑✶ k ≡ (t₁ /✶ ρs ↑✶ k) · (t₂ /✶ ρs ↑✶ k)
  ·-/✶-↑✶ k ε        = refl
  ·-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (·-/✶-↑✶ k ρs) refl

tmSubst : TermSubst Tm
tmSubst = record { var = var; app = TmApp._/_ }

open TermSubst tmSubst hiding (var)

-- Substitution lemmas.

tmLemmas : TermLemmas Tm
tmLemmas = record
  { termSubst = tmSubst
  ; app-var   = refl
  ; /✶-↑✶     = Lemma./✶-↑✶
  }
  where
  module Lemma {T₁ T₂} {lift₁ : Lift T₁ Tm} {lift₂ : Lift T₂ Tm} where

    open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
    open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

    /✶-↑✶ : ∀ {m n} (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n) →
            (∀ k x → var x /✶₁ ρs₁ ↑✶₁ k ≡ var x /✶₂ ρs₂ ↑✶₂ k) →
             ∀ k t → t     /✶₁ ρs₁ ↑✶₁ k ≡ t     /✶₂ ρs₂ ↑✶₂ k
    /✶-↑✶ ρs₁ ρs₂ hyp k (var x) = hyp k x
    /✶-↑✶ ρs₁ ρs₂ hyp k (ƛ t)   = begin
      ƛ t /✶₁ ρs₁ ↑✶₁ k        ≡⟨ TmApp.ƛ-/✶-↑✶ _ k ρs₁ ⟩
      ƛ (t /✶₁ ρs₁ ↑✶₁ suc k)  ≡⟨ cong ƛ (/✶-↑✶ ρs₁ ρs₂ hyp (suc k) t) ⟩
      ƛ (t /✶₂ ρs₂ ↑✶₂ suc k)  ≡⟨ sym (TmApp.ƛ-/✶-↑✶ _ k ρs₂) ⟩
      ƛ t /✶₂ ρs₂ ↑✶₂ k        ∎
    /✶-↑✶ ρs₁ ρs₂ hyp k (t₁ · t₂) = begin
      t₁ · t₂ /✶₁ ρs₁ ↑✶₁ k                    ≡⟨ TmApp.·-/✶-↑✶ _ k ρs₁ ⟩
      (t₁ /✶₁ ρs₁ ↑✶₁ k) · (t₂ /✶₁ ρs₁ ↑✶₁ k)  ≡⟨ cong₂ _·_ (/✶-↑✶ ρs₁ ρs₂ hyp k t₁)
                                                            (/✶-↑✶ ρs₁ ρs₂ hyp k t₂) ⟩
      (t₁ /✶₂ ρs₂ ↑✶₂ k) · (t₂ /✶₂ ρs₂ ↑✶₂ k)  ≡⟨ sym (TmApp.·-/✶-↑✶ _ k ρs₂) ⟩
      t₁ · t₂ /✶₂ ρs₂ ↑✶₂ k                    ∎

open TermLemmas tmLemmas public hiding (var)


text:
open import Agda.Builtin.Nat

interleaved mutual

  plus : Nat → Nat → Nat
  mult : Nat → Nat → Nat

  -- base case
  mult 0 n = 0
  plus 0 n = n

  -- inductive case. The fun clauses with an ellipsis belong to mult
  mult (suc m) n with mult m n
  ... | p with plus p n
  ... | q = q
  plus (suc m) n = suc (plus m n)

open import Agda.Builtin.Equality

proof : ∀ m n → mult (suc m) n ≡ plus (mult m n) n
proof m n with mult m n
... | p with plus p n
... | q = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Testing some inductive predicates for inequalities
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.Inequalities.InductivePredicates where

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

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

module m₁ where
  data _≤_ : D → D → Set where
    z≤n : ∀ n → zero ≤ n
    s≤s : ∀ {m n} → m ≤ n → succ₁ m ≤ succ₁ n

  _<_ : D → D → Set
  m < n = succ₁ m ≤ n

  _≥_ : D → D → Set
  m ≥ n = n ≤ m

  _>_ : D → D → Set
  m > n = n < m

  x≤y→x≤Sy : ∀ {m n} → m ≤ n → m ≤ succ₁ n
  x≤y→x≤Sy {.zero} {n} (z≤n .n)  = z≤n (succ₁ n)
  x≤y→x≤Sy             (s≤s m≤n) = s≤s (x≤y→x≤Sy m≤n)

module m₂ where
  data _≤_ : D → D → Set where
    z≤n : ∀ {n} → N n → zero ≤ n
    s≤s : ∀ {m n} → N m → N n → m ≤ n → succ₁ m ≤ succ₁ n

  _<_ : D → D → Set
  m < n = succ₁ m ≤ n

  _≥_ : D → D → Set
  m ≥ n = n ≤ m

  _>_ : D → D → Set
  m > n = n < m

  x≤y→x≤Sy : ∀ {m n} → m ≤ n → m ≤ succ₁ n
  x≤y→x≤Sy (z≤n Nn)        = z≤n (nsucc Nn)
  x≤y→x≤Sy (s≤s Nm Nn m≤n) = s≤s Nm (nsucc Nn) (x≤y→x≤Sy m≤n)

  postulate
    lt    : D → D → D
    lt-00 : lt zero zero                   ≡ false
    lt-0S : ∀ n → lt zero (succ₁ n)        ≡ true
    lt-S0 : ∀ n → lt (succ₁ n) zero        ≡ false
    lt-SS : ∀ m n → lt (succ₁ m) (succ₁ n) ≡ lt m n

  le : D → D → D
  le m n = lt m (succ₁ n)

  ≤→le : ∀ {m n} → m ≤ n → le m n ≡ true
  ≤→le {n = n} (z≤n Nn) = lt-0S n
  ≤→le (s≤s nzero nzero h) = trans (lt-SS zero 1') (≤→le h)
  ≤→le (s≤s nzero (nsucc {n} Nn) h) = trans (lt-SS zero (succ₁ (succ₁ n))) (≤→le h)
  ≤→le (s≤s (nsucc {m} Nm) nzero h) = trans (lt-SS (succ₁ m) 1') (≤→le h)
  ≤→le (s≤s (nsucc {m} Nm) (nsucc {n} Nn) h) =
    trans (lt-SS (succ₁ m) (succ₁ (succ₁ n))) (≤→le h)

  le→≤ : ∀ {m n} → N m → N n → le m n ≡ true → m ≤ n
  le→≤ nzero Nn h = z≤n Nn
  le→≤ (nsucc nzero) nzero h =
    ⊥-elim (t≢f (trans (sym h) (trans (lt-SS zero zero) lt-00)))
  le→≤ (nsucc (nsucc {m} Nm)) nzero h =
    ⊥-elim (t≢f (trans (sym h) (trans (lt-SS (succ₁ m) zero) (lt-S0 m))))
  {-# CATCHALL #-}
  le→≤ (nsucc {m} Nm) (nsucc {n} Nn) h =
    s≤s Nm Nn (le→≤ Nm Nn (trans (sym (lt-SS m (succ₁ n))) h))

module m₃ where
  data _≤_ : ∀ {m n} → N m → N n → Set where
    z≤n : ∀ {n} → (Nn : N n)                          → nzero ≤ Nn
    s≤s : ∀ {m n} → (Nm : N m) → (Nn : N n) → Nm ≤ Nn → nsucc Nm ≤ nsucc Nn

  _<_ : ∀ {m n} → N m → N n → Set
  Nm < Nn = nsucc Nm ≤ Nn

  _≥_ : ∀ {m n} → N m → N n → Set
  Nm ≥ Nn = Nn ≤ Nm

  _>_ : ∀ {m n} → N m → N n → Set
  Nm > Nn = Nn < Nm

  x≤y→x≤Sy : ∀ {m n} → (Nm : N m) → (Nn : N n) → Nm ≤ Nn → Nm ≤ nsucc Nn
  x≤y→x≤Sy .nzero       Nn         (z≤n .Nn)         = z≤n (nsucc Nn)
  x≤y→x≤Sy .(nsucc Nm) .(nsucc Nn) (s≤s Nm Nn Nm≤Nn) =
    s≤s Nm (nsucc Nn) (x≤y→x≤Sy Nm Nn Nm≤Nn)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level
    A : Type ℓ

infixr 1 _≡⟨⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_
infix 2 _∎

-- Step with a non-trivial propositional equality

_≡⟨_⟩_ : ∀ x {y z : A} → x ≡ y → y ≡ z → x ≡ z
_≡⟨_⟩_ x = _∙_

-- Step with a flipped non-trivial propositional equality

_≡˘⟨_⟩_ : ∀ x {y z : A} → y ≡ x → y ≡ z → x ≡ z
x ≡˘⟨ y≡x ⟩ y≡z = x ≡⟨ sym y≡x ⟩ y≡z

-- Step with a trivial propositional equality

_≡⟨⟩_ : ∀ x {y : A} → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y

-- Syntax for path definition

≡⟨⟩-syntax : ∀ x {y z : A} → x ≡ y → y ≡ z → x ≡ z
≡⟨⟩-syntax = _≡⟨_⟩_
infixr 1 ≡⟨⟩-syntax
syntax ≡⟨⟩-syntax x (λ i → B) y = x ≡[ i ]⟨ B ⟩ y

≡˘⟨⟩-syntax : ∀ x {y z : A} → y ≡ x → y ≡ z → x ≡ z
≡˘⟨⟩-syntax = _≡˘⟨_⟩_
infixr 1 ≡˘⟨⟩-syntax
syntax ≡˘⟨⟩-syntax x (λ i → B) y = x ≡˘[ i ]⟨ B ⟩ y

-- Termination step

_∎ : ∀ (x : A) → x ≡ x
x ∎ = refl


text:
module Numeral.Natural.Relation where

open import Data.Boolean.Stmt
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Logic.Propositional
open import Logic
import      Lvl
open import Relator.Equals
open import Type

Positive : ℕ → Stmt
Positive(n) = IsTrue(positive? n)

zero-not-positive : ¬ Positive(𝟎)
zero-not-positive ()

positive-not-zero : ∀{n} → ⦃ _ : Positive(n) ⦄ → (n ≢ 𝟎)
positive-not-zero {𝟎} ⦃ pos ⦄ _ = pos

non-zero-positive : ∀{n} → (n ≢ 𝟎) → Positive(n)
non-zero-positive {𝟎}   p = p [≡]-intro
non-zero-positive {𝐒 n} p = [⊤]-intro

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Algebra.Linear.Structures.Bundles where

open import Algebra
open import Level using (Level; suc; _⊔_)
open import Relation.Binary using (Rel; IsEquivalence)

open import Algebra.FunctionProperties
open import Algebra.Structures.Field
open import Algebra.Structures.Bundles.Field
open import Algebra.Linear.Structures.VectorSpace

record RawVectorSpace {k ℓᵏ} (K : Field k ℓᵏ) (c ℓ : Level) : Set (suc (c ⊔ k ⊔ ℓ)) where
  infix  20 _≈_
  infixl 25 _+_
  infixr 30 _∙_

  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ
    _+_           : Carrier -> Carrier -> Carrier
    _∙_           : Field.Carrier K -> Carrier -> Carrier
    -_            : Carrier -> Carrier
    0#            : Carrier

  rawGroup : RawGroup c ℓ
  rawGroup = record { _≈_ = _≈_; _∙_ = _+_; ε = 0#; _⁻¹ = -_ }

  open RawGroup rawGroup public
    using (rawMagma; rawMonoid)

record VectorSpace {k ℓᵏ} (K : Field k ℓᵏ) (c ℓ : Level) : Set (suc (c ⊔ k ⊔ ℓ ⊔ ℓᵏ)) where
  infix  20 _≈_
  infixl 25 _+_
  infixr 30 _∙_

  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ
    _+_           : Carrier -> Carrier -> Carrier
    _∙_           : Field.Carrier K -> Carrier -> Carrier
    -_            : Carrier -> Carrier
    0#            : Carrier
    isVectorSpace : IsVectorSpace K _≈_ _+_ _∙_ -_ 0#

  open IsVectorSpace isVectorSpace public

  rawVectorSpace : RawVectorSpace K c ℓ
  rawVectorSpace = record
    { _≈_ = _≈_; _+_ = _+_; _∙_ = _∙_; -_ = -_; 0# = 0# }

  abelianGroup : AbelianGroup c ℓ
  abelianGroup = record { isAbelianGroup = isAbelianGroup }

  open AbelianGroup abelianGroup public
    using (rawMagma; magma; rawMonoid; monoid; rawGroup; group)

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


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

open import Numbers.ClassicalReals.RealField
open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Setoids.Orders.Partial.Definition
open import Sets.EquivalenceRelations
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Fields
open import Groups.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Functions.Definition

module Numbers.Intervals.Definition {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {_<_ : Rel {_} {c} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} (pRing : PartiallyOrderedRing R pOrder) where

record OpenInterval : Set a where
  field
    minBound : A
    maxBound : A

isInInterval : A → OpenInterval → Set c
isInInterval a record { minBound = min ; maxBound = max } = (min < a) && (a < max)


text:
open import Prelude

module Implicits.Resolution.Finite.Algorithm where

open import Induction.WellFounded
open import Induction.Nat
open import Data.Fin.Substitution
open import Data.Nat.Base using (_<′_)
open import Data.List.Any
open Membership-≡
open import Implicits.Syntax
open import Implicits.Syntax.Type.Unification
open import Implicits.Syntax.Type.Unification.Lemmas
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Implicits.Resolution.Finite.Resolution
open import Implicits.Resolution.Termination
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.Equality hiding (cong; flip; const)
open import Data.List.Any.Properties using (Any↔)
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties
open import Relation.Binary using (module DecTotalOrder)
open DecTotalOrder decTotalOrder using () renaming
  (refl to ≤-refl; trans to ≤-trans)
open Lexicographic using (left; right)

module M = MetaTypeMetaSubst

module Lemmas where
  postulate lem₄ : ∀ {m ν} (a : MetaType m (suc ν)) u us → from-meta ((M.open-meta a) M./ (us M.↑) M./ (M.sub u)) ≡ (from-meta (a M./ (us M.↑tp))) tp[/tp from-meta u ]

  m<-Acc : ∀ {m ν} → MetaType m ν → Set
  m<-Acc {m} {ν} r = Acc _m<_ (m , ν , r)

  ρ<-Acc : ∀ {ν} → Type ν → Set
  ρ<-Acc {ν} r = Acc _ρ<_ (ν , r)

  module Arg<-well-founded  where
    open Lexicographic (_N<_) (const _ρ<_)

    open import Induction.Nat
    open import Data.Nat.Properties
    module image = Subrelation {A = ℕ} {_N<_} {_<′_} ≤⇒≤′

    arg<-well-founded : Well-founded _<_
    arg<-well-founded = well-founded (image.well-founded <-well-founded) ρ<-well-founded

    _arg<_ = _<_

    -- Accessibility of the 'goal' type during resolution.
    -- Either the *head* of the goal shrinks (Oliveira's termination condition)
    -- Or the head size remains equal and the goal shrinks in an absolute sense.
    Arg<-Acc : ∀ {ν} → Type ν → Set
    Arg<-Acc a = Acc _arg<_ (h|| a || , (, a))

  open Arg<-well-founded using (Arg<-Acc; arg<-well-founded) public

  lem₆ : ∀ {ν μ} (a : Type ν) (b : Type (suc μ)) c → (, a) hρ< (, b) → (, a) hρ< (, b tp[/tp c ])
  lem₆ a b c p = ≤-trans p (h||a/s|| b (TypeSubst.sub c))
    where open SubstSizeLemmas

  lem₅ : ∀ {ν μ} {Δ : ICtx ν} {b τ} (a : Type μ) → Δ ⊢ b ↓ τ → (, a) hρ< (, b) → (, a) hρ< (, simpl τ)
  lem₅ {τ = τ} a (i-simp .τ) q = q
  lem₅ a (i-iabs _ _ p) q = lem₅ a p q
  lem₅ a (i-tabs {ρ = b} c p) q = lem₅ a p (lem₆ a b c q)

open Lemmas

mutual

  match' : ∀ {m ν ρ} (Δ : ICtx ν) (r∈Δ : ρ List.∈ Δ) τ → (r : MetaType m ν) →
           Arg<-Acc (simpl τ) →
           m<-Acc r →
           Maybe (∃ λ u → Δ ⊢ from-meta (r M./ u) ↓ τ)
  match' Δ r∈Δ τ (simpl x) f g with mgu (simpl x) τ | sound (simpl x) τ
  match' Δ r∈Δ τ (simpl x) f g | just u | just u-unifies =
    just (u , subst (λ a → Δ ⊢ a ↓ τ) (sym u-unifies) (i-simp τ))
  match' Δ r∈Δ τ (simpl x) f g | nothing | _ = nothing

  match' Δ r∈Δ τ (a ⇒ b) (acc f) (acc g) with match' Δ r∈Δ τ b (acc f) (g _ (b-m<-a⇒b a b))
  match' Δ r∈Δ τ (a ⇒ b) (acc f) (acc g) | nothing = nothing
  match' Δ r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ)
    with (from-meta (a M./ u)) hρ<? (from-meta (b M./ u))
  match' Δ r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ) | yes ρ₁<
    with resolve' Δ (from-meta (a M./ u)) (f _ (left (lem₅ (from-meta (a M./ u)) b/u↓τ ρ₁<)))
  match' Δ r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ) | yes ρ₁< | just ⊢ᵣa =
    just (u , i-iabs ρ₁< ⊢ᵣa b/u↓τ)
  match' Δ r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ) | yes _ | nothing = nothing
  match' Δ r∈Δ τ (a ⇒ b) (acc f) (acc g) | just (u , b/u↓τ) | no p = nothing

  match' Δ r∈Δ τ (∀' a) f (acc g) with match' Δ r∈Δ τ (open-meta a) f (g _ (open-meta-a-m<-∀'a a))
  match' Δ r∈Δ τ (∀' a) f (acc g) | just p = just $ lem p
    where
      lem : (∃ λ u → Δ ⊢ (from-meta ((open-meta a) M./ u)) ↓ τ) →
          ∃ λ u' → Δ ⊢ (from-meta (∀' a M./ u')) ↓ τ
      lem (u ∷ us , p) = us , (i-tabs (from-meta u) (subst (λ v → Δ ⊢ v ↓ τ) (begin
            from-meta (M._/_ (open-meta a) (u ∷ us))
              ≡⟨ cong (λ v → from-meta (M._/_ (open-meta a) v)) (sym $ us↑-⊙-sub-u≡u∷us u us) ⟩
            from-meta ((open-meta a) M./ (us M.↑ M.⊙ (M.sub u)))
              ≡⟨ cong from-meta (/-⊙ (open-meta a)) ⟩
            from-meta ((open-meta a) M./ us M.↑ M./ (M.sub u))
              ≡⟨ lem₄ a u us ⟩
            from-meta (M._/_ a (us M.↑tp)) tp[/tp from-meta u ] ∎) p))
          where open MetaTypeMetaLemmas hiding (subst)
  match' Δ r∈Δ τ (∀' r) f (acc g) | nothing = nothing

  -- match defers to match', which concerns itself with MetaTypes.
  -- If match' finds a match, we can use the fact that we have zero unification variables open here
  -- to show that we found the right thing.
  match : ∀ {ν ρ} (Δ : ICtx ν) (r∈Δ : ρ List.∈ Δ) r τ → Arg<-Acc (simpl τ) → Maybe (Δ ⊢ r ↓ τ)
  match Δ r∈Δ a τ f with match' Δ r∈Δ τ (to-meta {zero} a) f (m<-well-founded _)
  match Δ r∈Δ a τ f | just x = just (lem x)
    where
      eq : ∀ {ν} {a : Type ν} {s} → from-meta (to-meta {zero} a M./ s) ≡ a
      eq {a = a} {s = []} = begin
          from-meta (M._/_ (to-meta {zero} a) [])
          ≡⟨ cong (λ q → from-meta q) (MetaTypeMetaLemmas.id-vanishes (to-meta {zero} a)) ⟩
          from-meta (to-meta {zero} a)
          ≡⟨ to-meta-zero-vanishes ⟩
          a ∎
      lem : ∃ (λ u → Δ ⊢ from-meta (to-meta {zero} a M./ u) ↓ τ) →
                Δ ⊢ a ↓ τ
      lem ([] , proj₂) = subst (λ u → Δ ⊢ u ↓ τ) eq proj₂
  match Δ r∈Δ a τ f | nothing = nothing

  match1st : ∀ {ν} (Δ : ICtx ν) τ → Arg<-Acc (simpl τ) →
             Maybe (∃₂ λ r (r∈Δ : r List.∈ Δ) → Δ ⊢ r ↓ τ)
  match1st {ν = ν} Δ τ f = match1st' Δ Prelude.id
    where
      match1st' : ∀ (ρs : ICtx ν) → ρs ⊆ Δ → Maybe (∃₂ λ r (r∈Δ : r List.∈ Δ) → Δ ⊢ r ↓ τ)
      match1st' List.[] sub = nothing
      match1st' (x List.∷ xs) sub with match Δ (sub (here refl)) x τ f
      match1st' (x List.∷ xs) sub | just px = just (x , ((sub (here refl)) , px))
      match1st' (x List.∷ xs) sub | nothing with match1st' xs (λ r∈xs → sub (there r∈xs))
      match1st' (x List.∷ xs) sub | nothing | just p = just p
      match1st' (x List.∷ xs) sub | nothing | nothing = nothing

  resolve' : ∀ {ν} (Δ : ICtx ν) r → Arg<-Acc r → (Maybe (Δ ⊢ᵣ r))
  resolve' Δ (simpl x) f with match1st Δ x f
  resolve' Δ (simpl x) f | just (_ , r∈Δ , r↓x) = just (r-simp r∈Δ r↓x)
  resolve' Δ (simpl x) f | nothing = nothing
  resolve' Δ (a ⇒ b) (acc f) with resolve' (a List.∷ Δ) b (f _ (right (b-ρ<-a⇒b a b)))
  resolve' Δ (a ⇒ b) (acc f) | just p = just (r-iabs p)
  resolve' Δ (a ⇒ b) (acc f) | nothing = nothing
  resolve' Δ (∀' r) (acc f) with resolve' (ictx-weaken Δ) r (f _ (right (a-ρ<-∀a r)))
  resolve' Δ (∀' r) (acc f) | just p = just (r-tabs p)
  resolve' Δ (∀' r) (acc f) | nothing = nothing

  resolve : ∀ {ν} (Δ : ICtx ν) r → (Maybe (Δ ⊢ᵣ r))
  resolve Δ r = resolve' Δ r (arg<-well-founded _)


text:
-- Check that unquoted functions are termination checked.
module _ where

open import Common.Prelude hiding (_>>=_)
open import Common.Reflection

`⊥ : Type
`⊥ = def (quote ⊥) []

data Box : Set where
  box : ⊥ → Box

unbox : Box → ⊥
unbox (box x) = x

`Box : Type
`Box = def (quote Box) []

{-
Generate
  aux : Box
  aux = box (unbox aux)
-}
makeLoop : TC ⊤
makeLoop =
  freshName "aux" >>= λ aux →
  declareDef (iArg aux) `Box >>= λ _ →
  defineFun aux (clause [] (con (quote box) (vArg (def (quote unbox) (vArg (def aux []) ∷ [])) ∷ [])) ∷ [])

unquoteDecl = makeLoop

it : ∀ {a} {A : Set a} {{_ : A}} → A
it {{x}} = x

loop : ⊥
loop = unbox it


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

module Issue3577 where

open import Agda.Primitive.Cubical renaming (primTransp to transp; primHComp to hcomp)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Sigma
open import Agda.Builtin.Cubical.Sub renaming (primSubOut to ouc; Sub to _[_↦_])

refl : ∀ {l} {A : Set l} {x : A} → x ≡ x
refl {x = x} = \ _ → x

ptType : Set₁
ptType = Σ Set (λ A → A)

data Susp' (A : ptType) : Set where
  susp*  : Susp' A

-- Non-computation of transp on non-HIT's hcomp
testTr : {A' : ptType} (ψ : I) (A : I → ptType [ ψ ↦ (\ _ → A') ])
         {φ : I}
         (u : ∀ i → Partial φ (Susp' (ouc (A i0))))
         (u0 : Susp' (ouc (A i0)) [ φ ↦ u i0 ])
         → transp (\ i -> Susp' (ouc (A i))) ψ (hcomp u (ouc u0))
         ≡ hcomp (λ j .o → transp (λ i → Susp' (ouc (A i))) ψ (u j o)) (transp (λ i → Susp' (ouc (A i))) ψ (ouc u0))
testTr ψ A u u0 = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
postulate
  D  : Set
  ∃  : (A : D → Set) → Set
  vx : D
  Q₂ : D → D → Set

postulate
  foo : (∃ λ x → Q₂ vx x) → (∃ λ x → Q₂ vx x)
{-# ATP prove foo #-}

-- $ apia Bug.agda
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/Apia/Utils/AgdaAPI/DeBruijn.hs:68

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
-- Internal hom in families
module SOAS.Abstract.Hom {T : Set} where

open import SOAS.Common
open import SOAS.Construction.Structure
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core {T}
open import SOAS.Families.Isomorphism
open import SOAS.Families.BCCC

open import SOAS.Construction.Skew.SkewClosed

open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation.Dinatural using (dtHelper)

-- Heterogeneous action of a sorted family on a family
⟨_,_⟩ : Familyₛ → Family → Family
⟨ 𝒳 , Y ⟩ Γ = (Γ ~[ 𝒳 ]↝_) ⇾ Y

⟨-,-⟩F : Bifunctor 𝔽amₛ.op 𝔽amilies 𝔽amilies
⟨-,-⟩F = record
  { F₀ = λ{ (𝒳 , Y) → ⟨ 𝒳 , Y ⟩ }
  ; F₁ = λ{ (f , g) o {Δ} σ → g (o (f ∘ σ))  }
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≈ = λ{ {f = f , g} (p , p′) {Γ} {o} → dext′ (trans (cong (g ∘ o) (dext′ p)) p′) }
  }

-- Arrow mapping
⟨_,_⟩₁ : {𝒳 𝒳′ : Familyₛ} {Y Y′ : Family} → 𝒳′ ⇾̣ 𝒳 → Y ⇾ Y′ → (⟨ 𝒳 , Y ⟩ ⇾ ⟨ 𝒳′ , Y′ ⟩)
⟨ f , g ⟩₁ = Functor.₁ ⟨-,-⟩F (f , g)

-- Internal hom of sorted families
〖_,_〗 : Familyₛ → Familyₛ → Familyₛ
〖 X , Y 〗 τ = ⟨ X , Y τ ⟩

〖-,-〗F  : Bifunctor 𝔽amₛ.op 𝔽amiliesₛ 𝔽amiliesₛ
〖-,-〗F = record
  { F₀ = λ{ (X , Y) → 〖 X , Y 〗 }
  ; F₁ = λ{ (f , g) o {Δ} σ → g (o (f ∘ σ))  }
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≈ = λ{ {f = f , g} (p , p′) {x = h} → dext′ (trans (cong (g ∘ h) (dext′ p)) p′) }
  }

-- Arrow mapping
〖_,_〗₁ : {𝒳 𝒳′ 𝒴 𝒴′ : Familyₛ} → 𝒳′ ⇾̣ 𝒳 → 𝒴 ⇾̣ 𝒴′ → (〖 𝒳 , 𝒴 〗 ⇾̣ 〖 𝒳′ , 𝒴′ 〗)
〖 f , g 〗₁ h σ = g (h (f ∘ σ))

〖_,_〗ₗ : {𝒳 𝒳′ : Familyₛ} → 𝒳′ ⇾̣ 𝒳 → (𝒴 : Familyₛ) → (〖 𝒳 , 𝒴 〗 ⇾̣ 〖 𝒳′ , 𝒴 〗)
〖 f , Z 〗ₗ h σ = h (f ∘ σ)

〖_,_〗ᵣ : {𝒴 𝒴′ : Familyₛ} → (𝒳 : Familyₛ) → 𝒴 ⇾̣ 𝒴′ → (〖 𝒳 , 𝒴 〗 ⇾̣ 〖 𝒳 , 𝒴′ 〗)
〖 X , g 〗ᵣ h σ = g (h σ)

-- | Structure morphisms

i : (𝒳 : Familyₛ) → 〖 ℐ , 𝒳 〗 ⇾̣ 𝒳
i 𝒳 o = o id

i′ : (X : Family) → ⟨ ℐ , X ⟩ ⇾ X
i′ X o = o id

j : (𝒳 : Familyₛ) → ℐ ⇾̣ 〖 𝒳 , 𝒳 〗
j 𝒳 v σ = σ v

L : (𝒳 𝒴 𝒵 : Familyₛ) → 〖 𝒴 , 𝒵 〗 ⇾̣ 〖 〖 𝒳 , 𝒴 〗 , 〖 𝒳 , 𝒵 〗 〗
L 𝒳 Y Z o ς σ = o (λ v → ς v σ)

L′ : (𝒳 𝒴 : Familyₛ)(Z : Family) → ⟨ 𝒴 , Z ⟩ ⇾ ⟨ 〖 𝒳 , 𝒴 〗 , ⟨ 𝒳 , Z ⟩ ⟩
L′ 𝒳 𝒴 Z o ς σ = o (λ v → ς v σ)

-- Category of sorted families is skew-closed under the internal hom
𝔽amₛ:SkewClosed : SkewClosed 𝔽amiliesₛ
𝔽amₛ:SkewClosed = record
  { [-,-] = 〖-,-〗F
  ; unit = ℐ
  ; identity = ntHelper record { η = i  ; commute = λ f → refl }
  ; diagonal = dtHelper record { α = j ; commute = λ f → refl }
  ; L = L
  ; L-commute = refl
  ; Lj≈j = refl
  ; ijL≈id = refl
  ; iL≈i = refl
  ; ij≈id = refl
  ; pentagon = refl
  }

private
  variable
    𝒳 𝒴 𝒵 : Familyₛ
    Y Z : Family

-- ⟨X,-⟩ distributes over and factors out of products
⟨𝒳,Y×Z⟩≅⟨𝒳,Y⟩×⟨𝒳,Z⟩ : ⟨ 𝒳 , (Y ×ₘ Z) ⟩ ≅ₘ ⟨ 𝒳 , Y ⟩ ×ₘ ⟨ 𝒳 , Z ⟩
⟨𝒳,Y×Z⟩≅⟨𝒳,Y⟩×⟨𝒳,Z⟩  = record
  { from = λ h → (λ ρ → proj₁ (h ρ)) , λ ϱ → proj₂ (h ϱ)
  ; to = λ{ (bx , by) ρ → bx ρ , by ρ}
  ; iso = record { isoˡ = refl ; isoʳ = refl }
  }

-- ⟨X,-⟩ factors out of coproducts
⟨𝒳,Y⟩+⟨𝒳,Z⟩⇾⟨𝒳,Y+Z⟩ : ⟨ 𝒳 , Y ⟩ +ₘ ⟨ 𝒳 , Z ⟩ ⇾ ⟨ 𝒳 , (Y +ₘ Z) ⟩
⟨𝒳,Y⟩+⟨𝒳,Z⟩⇾⟨𝒳,Y+Z⟩ (inj₁ ox) σ = inj₁ (ox σ)
⟨𝒳,Y⟩+⟨𝒳,Z⟩⇾⟨𝒳,Y+Z⟩ (inj₂ oy) ς = inj₂ (oy ς)

-- Same properties for the hom
〖𝒳,𝒴×̣𝒵〗≅̣〖𝒳,𝒴〗×̣〖𝒳,𝒵〗 : 〖 𝒳 , 𝒴 ×̣ₘ 𝒵 〗 ≅̣ₘ 〖 𝒳 , 𝒴 〗 ×̣ₘ 〖 𝒳 , 𝒵 〗
〖𝒳,𝒴×̣𝒵〗≅̣〖𝒳,𝒴〗×̣〖𝒳,𝒵〗 = ≅ₘ→≅̣ₘ ⟨𝒳,Y×Z⟩≅⟨𝒳,Y⟩×⟨𝒳,Z⟩

〖𝒳,𝒴〗+̣〖𝒳,𝒵〗⇾̣〖𝒳,𝒴+̣𝒵〗 : 〖 𝒳 , 𝒴 〗 +̣ₘ 〖 𝒳 , 𝒵 〗 ⇾̣ 〖 𝒳 , (𝒴 +̣ₘ 𝒵) 〗
〖𝒳,𝒴〗+̣〖𝒳,𝒵〗⇾̣〖𝒳,𝒴+̣𝒵〗 = ⟨𝒳,Y⟩+⟨𝒳,Z⟩⇾⟨𝒳,Y+Z⟩

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module Data.Num where

open import Data.Num.Core renaming
    (   carry to carry'
    ;   carry-lower-bound to carry-lower-bound'
    ;   carry-upper-bound to carry-upper-bound'
    )
open import Data.Num.Maximum
open import Data.Num.Bounded
open import Data.Num.Next
open import Data.Num.Increment
open import Data.Num.Continuous

open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Properties.Simple
open import Data.Nat.Properties.Extra
open import Data.Nat.DM

open import Data.Fin as Fin
    using (Fin; fromℕ≤; inject≤)
    renaming (zero to z; suc to s)

open import Data.Fin.Properties using (toℕ-fromℕ≤; bounded)
open import Data.Product
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)

open import Function
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning
open ≤-Reasoning renaming (begin_ to start_; _∎ to _□; _≡⟨_⟩_ to _≈⟨_⟩_)
open DecTotalOrder decTotalOrder using (reflexive) renaming (refl to ≤-refl)

infix 4 _≋_

_≋_ : ∀ {b d o}
    → (xs ys : Numeral b d o)
    → Set
xs ≋ ys = ⟦ xs ⟧ ≡ ⟦ ys ⟧

fromℕ : ∀ {b d o}
    → {cont : True (Continuous? b (suc d) o)}
    → (n : ℕ)
    → n ≥ o
    → Numeral b (suc d) o
fromℕ {o = o}       n       p   with o ≟ n
fromℕ               n       n≥o | yes eq = z ∙
fromℕ {o = o}       zero    n≥o | no ¬eq = contradiction (≤0⇒≡0 o n≥o) ¬eq
fromℕ {cont = cont} (suc n) n≥o | no ¬eq = 1+ {cont = cont} (fromℕ {cont = cont} n (≤-pred $ ≤∧≢⇒< n≥o ¬eq))

fromℕ-toℕ : ∀ {b d o}
    → (cont : True (Continuous? b (suc d) o))
    → (n : ℕ)
    → (n≥o : n ≥ o)
    → ⟦ fromℕ {cont = cont} n n≥o ⟧ ≡ n
fromℕ-toℕ {o = o} cont n n≥o with o ≟ n
fromℕ-toℕ cont n n≥o | yes eq = eq
fromℕ-toℕ {o = o} cont zero n≥o | no ¬eq = contradiction (≤0⇒≡0 o n≥o) ¬eq
fromℕ-toℕ cont (suc n) n≥o | no ¬eq =
    let
        n≥o' = ≤-pred (≤∧≢⇒< n≥o ¬eq)
    in
    begin
        ⟦ 1+ {cont = cont} (fromℕ {cont = cont} n n≥o') ⟧
    ≡⟨ 1+-toℕ {cont = cont} (fromℕ {cont = cont} n n≥o') ⟩
        suc ⟦ fromℕ {cont = cont} n n≥o' ⟧
    ≡⟨ cong suc (fromℕ-toℕ cont n n≥o') ⟩
        suc n
    ∎

-- toℕ-fromℕ : ∀ {b d o}
--     → (cont : True (Continuous? b (suc d) o))
--     → (xs : Numeral b (suc d) o)
--     → fromℕ {cont = cont} ⟦ xs ⟧ (Num-lower-bound xs) ≋ xs
-- toℕ-fromℕ cont xs = fromℕ-toℕ cont ⟦ xs ⟧ (Num-lower-bound xs)

sum : ∀ {d}
    → (o : ℕ)
    → (x y : Digit (suc d))
    → ℕ
sum o x y = Digit-toℕ x o + Digit-toℕ y o

sum≥o : ∀ {d} o
    → (x y : Digit (suc d))
    → sum o x y ≥ o
sum≥o o x y = start
        o
    ≤⟨ n≤m+n (Fin.toℕ x) o ⟩
        Digit-toℕ x o
    ≤⟨ m≤m+n (Digit-toℕ x o) (Digit-toℕ y o) ⟩
        sum o x y
    □

sum-upper-bound : ∀ {d} o
    → (x y : Digit (suc d))
    → sum o x y ≤ (d + o) + (d + o)
sum-upper-bound {d} o x y =
    start
        Digit-toℕ x o + Digit-toℕ y o
    ≤⟨ ≤-pred (Digit-upper-bound o x) +-mono ≤-pred (Digit-upper-bound o y) ⟩
        d + o + (d + o)
    □

--  0   o                d+o          d+o+(1⊔o)×b
----|---|-----------------|----------------|
--    o          d              (1⊔o)×b
--                        [----------------] "buffer capacity"

data Sum : (b d o : ℕ) (x y : Digit (suc d)) → Set where
    NoCarry : ∀ {b d o x y}
        → (leftover : Digit (suc d))
        → (property : Digit-toℕ leftover o ≡ sum o x y)
        → Sum b d o x y
    Fixed : ∀ {b d o x y}
        → (leftover carry : Digit (suc d))
        → (property : Digit-toℕ leftover o + (Digit-toℕ carry o) * suc b ≡ sum o x y)
        → Sum b d o x y
    Floating : ∀ {b d o x y}
        → (leftover carry : Digit (suc d))
        → (property : Digit-toℕ leftover o + (Digit-toℕ carry o) * suc b ≡ sum o x y)
        → Sum b d o x y

sumView : ∀ b d o
    → (¬gapped : ¬ (Gapped#0 b d o))
    → (proper : 2 ≤ suc d + o)
    → (x y : Digit (suc d))
    → Sum b d o x y
sumView b d o ¬gapped proper x y with (sum o x y) ≤? d + o
sumView b d o ¬gapped proper x y | yes below
    = NoCarry
        (Digit-fromℕ leftover o leftover-upper-bound)
        property
    where
        leftover : ℕ
        leftover = sum o x y

        leftover-upper-bound : leftover ≤ d + o
        leftover-upper-bound = below

        property :
              Digit-toℕ (Digit-fromℕ leftover o leftover-upper-bound) o
            ≡ sum o x y
        property =
            begin
                Digit-toℕ (Digit-fromℕ (sum o x y) o below) o
            ≡⟨ Digit-fromℕ-toℕ (sum o x y) (sum≥o o x y) below ⟩
                sum o x y
            ∎
sumView b d o ¬gapped proper x y | no ¬below with (sum o x y) ≤? d + o + (1 ⊔ o) * (suc b)
sumView b d o ¬gapped proper x y | no ¬below | yes within
    = Fixed
        (Digit-fromℕ leftover o leftover-upper-bound)
        (Digit-fromℕ carry    o carry-upper-bound)
        property

    where
        base : ℕ
        base = suc b

        carry : ℕ
        carry = carry' o

        sum≥carry*base : sum o x y ≥ carry * base
        sum≥carry*base =
            start
                carry * base
            ≤⟨ m≤m+n (carry * base) o ⟩
                carry * base + o
            ≤⟨ +n-mono o (≤-pred (≰⇒> ¬gapped)) ⟩
                suc (d + o)
            ≤⟨ ≰⇒> ¬below ⟩
                sum o x y
            □

        leftover : ℕ
        leftover = sum o x y ∸ carry * base

        leftover-lower-bound : leftover ≥ o
        leftover-lower-bound =
            start
                o
            ≈⟨ sym (m+n∸n≡m o (carry * base)) ⟩
                o + carry * base ∸ carry * base
            ≈⟨ cong (λ w → w ∸ carry * base) (+-comm o (carry * base)) ⟩
                carry * base + o ∸ carry * base
            ≤⟨ ∸n-mono (carry * base) (+n-mono o (≤-pred (≰⇒> ¬gapped))) ⟩
                suc d + o ∸ carry * base
            ≤⟨ ∸n-mono (carry * base) (≰⇒> ¬below) ⟩
                leftover
            □

        leftover-upper-bound : leftover ≤ d + o
        leftover-upper-bound = +n-mono-inverse (carry * base) $
            start
                leftover + carry * base
            ≈⟨ refl ⟩
                sum o x y ∸ carry * base + carry * base
            ≈⟨ m∸n+n≡m sum≥carry*base ⟩
                sum o x y
            ≤⟨ within ⟩
                d + o + carry * base
            □

        carry-lower-bound : carry ≥ o
        carry-lower-bound = carry-lower-bound'

        carry-upper-bound : carry ≤ d + o
        carry-upper-bound = carry-upper-bound' {d} {o} proper

        property :
              Digit-toℕ (Digit-fromℕ leftover o leftover-upper-bound) o
            + Digit-toℕ (Digit-fromℕ    carry o    carry-upper-bound) o * base
            ≡ sum o x y
        property =
            begin
                Digit-toℕ (Digit-fromℕ leftover o leftover-upper-bound) o
              + Digit-toℕ (Digit-fromℕ    carry o    carry-upper-bound) o * base
            ≡⟨ cong₂
                (λ l c → l + c * base)
                (Digit-fromℕ-toℕ leftover leftover-lower-bound leftover-upper-bound)
                (Digit-fromℕ-toℕ    carry    carry-lower-bound    carry-upper-bound)
            ⟩
                leftover + carry * base
            ≡⟨ refl ⟩
                sum o x y ∸ carry * base + carry * base
            ≡⟨ m∸n+n≡m sum≥carry*base ⟩
                sum o x y
            ∎

sumView b d o ¬gapped proper x y | no ¬below | no ¬within with (sum o x y ∸ ((d + o) + (1 ⊔ o) * (suc b))) divMod (suc b)
sumView b d o ¬gapped proper x y | no ¬below | no ¬within | result quotient remainder divModProp _ _
    = Floating
        (Digit-fromℕ leftover o leftover-upper-bound)
        (Digit-fromℕ carry    o carry-upper-bound)
        property
    where

        base : ℕ
        base = suc b

        carry : ℕ
        carry = (1 ⊓ Fin.toℕ remainder) + quotient + (1 ⊔ o)

        divModProp' : sum o x y ≡ Fin.toℕ remainder + quotient * base + (d + o + (1 ⊔ o) * base)
        divModProp' =
            begin
                sum o x y
            ≡⟨ sym (m∸n+n≡m (<⇒≤ (≰⇒> ¬within))) ⟩
                sum o x y ∸ (d + o + (1 ⊔ o) * base) + (d + o + (1 ⊔ o) * base)
            ≡⟨ cong (λ w → w + ((d + o) + (1 ⊔ o) * base)) divModProp ⟩
                Fin.toℕ remainder + quotient * base + ((d + o) + (1 ⊔ o) * base)
            ∎

        leftover : ℕ
        leftover = sum o x y ∸ carry * base

        leftover-lower-bound-lemma :
              (remainder : Fin base)
            → (prop : sum o x y ∸ (d + o + (1 ⊔ o) * base) ≡ Fin.toℕ remainder + quotient * base)
            → sum o x y ≥ o + ((1 ⊓ Fin.toℕ remainder) + quotient + (1 ⊔ o)) * base
        leftover-lower-bound-lemma z prop =
            start
                o + (quotient + (1 ⊔ o)) * base
            ≤⟨ +n-mono ((quotient + (1 ⊔ o)) * base) (n≤m+n d o) ⟩
                d + o + (quotient + (1 ⊔ o)) * base
            ≈⟨ cong (λ w → d + o + w) (distribʳ-*-+ base quotient (1 ⊔ o)) ⟩
                d + o + (quotient * base + (1 ⊔ o) * base)
            ≈⟨ a+[b+c]≡b+[a+c] (d + o) (quotient * base) ((1 ⊔ o) * base) ⟩
                quotient * base + ((d + o) + (1 ⊔ o) * base)
            ≈⟨ cong (λ w → w + ((d + o) + (1 ⊔ o) * base)) (sym prop) ⟩
                (sum o x y ∸ ((d + o) + (1 ⊔ o) * base)) + ((d + o) + (1 ⊔ o) * base)
            ≈⟨ m∸n+n≡m (<⇒≤ (≰⇒> ¬within)) ⟩
                sum o x y
            □
        leftover-lower-bound-lemma (s r) prop =
            start
                o + ((1 ⊓ (Fin.toℕ (s r))) + quotient + (1 ⊔ o)) * base
            ≈⟨ refl ⟩
                o + (1 + (quotient + (1 ⊔ o))) * base
            ≈⟨ cong (λ w → o + w) (distribʳ-*-+ base 1 (quotient + (1 ⊔ o))) ⟩
                o + (1 * base + (quotient + (1 ⊔ o)) * base)
            ≈⟨ cong (λ w → o + (1 * base + w)) (distribʳ-*-+ base quotient (1 ⊔ o)) ⟩
                o + (1 * base + (quotient * base + (1 ⊔ o) * base))
            ≤⟨ n+-mono o
                (n+-mono (1 * base)
                    (+n-mono ((1 ⊔ o) * base)
                        (n≤m+n (Fin.toℕ r) (quotient * base)))) ⟩
                o + (1 * base + (Fin.toℕ r + quotient * base + (1 ⊔ o) * base))
            ≈⟨ a+[b+c]≡b+[a+c] o (1 * base) (Fin.toℕ r + quotient * base + (1 ⊔ o) * base) ⟩
                1 * base + (o + (Fin.toℕ r + quotient * base + (1 ⊔ o) * base))
            ≤⟨ +n-mono (o + (Fin.toℕ r + quotient * base + (1 ⊔ o) * base)) (*n-mono base (m≤m⊔n 1 o)) ⟩
                (1 ⊔ o) * base + (o + (Fin.toℕ r + quotient * base + (1 ⊔ o) * base))
            ≤⟨ +n-mono (o + ((Fin.toℕ r) + quotient * base + (1 ⊔ o) * base)) (≤-pred (≰⇒> ¬gapped)) ⟩
                suc d + (o + ((Fin.toℕ r) + quotient * base + (1 ⊔ o) * base))
            ≈⟨ cong suc (sym (+-assoc d o ((Fin.toℕ r) + quotient * base + (1 ⊔ o) * base))) ⟩
                suc (d + o + ((Fin.toℕ r) + quotient * base + (1 ⊔ o) * base))
            ≈⟨ sym (+-suc (d + o) ((Fin.toℕ r) + quotient * base + (1 ⊔ o) * base)) ⟩
                d + o + suc ((Fin.toℕ r) + quotient * base + (1 ⊔ o) * base)
            ≈⟨ a+[b+c]≡b+[a+c] (d + o) (suc (Fin.toℕ r) + quotient * base) ((1 ⊔ o) * base) ⟩
                suc (Fin.toℕ r) + quotient * base + ((d + o) + (1 ⊔ o) * base)
            ≈⟨ cong (λ w → w + ((d + o) + (1 ⊔ o) * base)) (sym prop) ⟩
                (sum o x y ∸ ((d + o) + (1 ⊔ o) * base)) + ((d + o) + (1 ⊔ o) * base)
            ≈⟨ m∸n+n≡m (<⇒≤ (≰⇒> ¬within)) ⟩
                sum o x y
            □

        leftover-lower-bound : leftover ≥ o
        leftover-lower-bound =
            start
                o
            ≈⟨ sym (m+n∸n≡m o (carry * base)) ⟩
                o + carry * base ∸ carry * base
            ≤⟨ ∸n-mono (carry * base) (leftover-lower-bound-lemma remainder divModProp) ⟩
                sum o x y ∸ carry * base
            ≈⟨ refl ⟩
                leftover
            □

        leftover-upper-bound-lemma :
              (remainder : Fin base)
            → (prop : sum o x y ∸ (d + o + (1 ⊔ o) * base) ≡ Fin.toℕ remainder + quotient * base)
            → sum o x y ≤ d + o + ((1 ⊓ Fin.toℕ remainder) + quotient + (1 ⊔ o)) * base
        leftover-upper-bound-lemma z prop =
            start
                sum o x y
            ≈⟨ sym (m∸n+n≡m (<⇒≤ (≰⇒> ¬within))) ⟩
                (sum o x y ∸ ((d + o) + (1 ⊔ o) * base)) + ((d + o) + (1 ⊔ o) * base)
            ≈⟨ cong (λ w → w + ((d + o) + (1 ⊔ o) * base)) prop ⟩
                quotient * base + ((d + o) + (1 ⊔ o) * base)
            ≈⟨ a+[b+c]≡b+[a+c] (quotient * base) (d + o) ((1 ⊔ o) * base) ⟩
                d + o + (quotient * base + (1 ⊔ o) * base)
            ≈⟨ cong (λ w → d + o + w) (sym (distribʳ-*-+ base quotient (1 ⊔ o))) ⟩
                d + o + (quotient + (1 ⊔ o)) * base
            □
        leftover-upper-bound-lemma (s r) prop =
            start
                sum o x y
            ≈⟨ sym (m∸n+n≡m (<⇒≤ (≰⇒> ¬within))) ⟩
                (sum o x y ∸ ((d + o) + (1 ⊔ o) * base)) + ((d + o) + (1 ⊔ o) * base)
            ≈⟨ cong (λ w → w + ((d + o) + (1 ⊔ o) * base)) prop ⟩
                suc (Fin.toℕ r) + quotient * base + ((d + o) + (1 ⊔ o) * base)
            ≈⟨ a+[b+c]≡b+[a+c] (suc (Fin.toℕ r) + quotient * base) (d + o) ((1 ⊔ o) * base) ⟩
                d + o + (suc (Fin.toℕ r) + quotient * base + (1 ⊔ o) * base)
            ≤⟨ n+-mono (d + o)
                (+n-mono ((1 ⊔ o) * base)
                    (+n-mono (quotient * base)
                        (≤-step (bounded r)))) ⟩
                d + o + (suc quotient * base + (1 ⊔ o) * base)
            ≈⟨ cong (λ w → d + o + w) (sym (distribʳ-*-+ base (suc quotient) (1 ⊔ o))) ⟩
                d + o + (1 + (quotient + (1 ⊔ o))) * base
            ≈⟨ refl ⟩
                d + o + ((1 ⊓ (Fin.toℕ (s r))) + quotient + (1 ⊔ o)) * base
            □

        leftover-upper-bound : leftover ≤ d + o
        leftover-upper-bound =
            start
                leftover
            ≈⟨ refl ⟩
                sum o x y ∸ carry * base
            ≤⟨ ∸n-mono (carry * base) (leftover-upper-bound-lemma remainder divModProp) ⟩
                d + o + carry * base ∸ carry * base
            ≈⟨ m+n∸n≡m (d + o) (carry * base) ⟩
                d + o
            □

        carry-lower-bound : carry ≥ o
        carry-lower-bound =
            start
                o
            ≤⟨ m≤n⊔m o 1 ⟩
                1 ⊔ o
            ≤⟨ n≤m+n (1 ⊓ Fin.toℕ remainder + quotient) (1 ⊔ o) ⟩
                1 ⊓ Fin.toℕ remainder + quotient + (1 ⊔ o)
            □

        carry-upper-bound : carry ≤ d + o
        carry-upper-bound = +n-mono-inverse (d + o) $
            start
                1 ⊓ Fin.toℕ remainder + quotient + (1 ⊔ o) + (d + o)
            ≤⟨ +n-mono (d + o)
                (+n-mono (1 ⊔ o)
                    (+n-mono quotient
                        (m⊓n≤n 1 (Fin.toℕ remainder))))
            ⟩
                Fin.toℕ remainder + quotient + (1 ⊔ o) + (d + o)
            ≈⟨ +-assoc (Fin.toℕ remainder + quotient) (1 ⊔ o) (d + o) ⟩
                Fin.toℕ remainder + quotient + (1 ⊔ o + (d + o))
            ≈⟨ cong (λ w → Fin.toℕ remainder + quotient + w) (+-comm (1 ⊔ o) (d + o)) ⟩
                Fin.toℕ remainder + quotient + (d + o + (1 ⊔ o))
            ≤⟨ +n-mono (d + o + (1 ⊔ o))
                (n+-mono (Fin.toℕ remainder) (m≤m*1+n quotient b))
            ⟩
                Fin.toℕ remainder + quotient * base + (d + o + (1 ⊔ o))
            ≤⟨ n+-mono (Fin.toℕ remainder + quotient * base)
                (n+-mono (d + o)
                    (m≤m*1+n (1 ⊔ o) b))
            ⟩
                Fin.toℕ remainder + quotient * base + (d + o + (1 ⊔ o) * base)
            ≈⟨ cong (λ w → w + (d + o + (1 ⊔ o) * base)) (sym divModProp) ⟩
                sum o x y ∸ (d + o + (1 ⊔ o) * base) + (d + o + (1 ⊔ o) * base)
            ≈⟨ m∸n+n≡m (<⇒≤ (≰⇒> ¬within)) ⟩
                sum o x y
            ≤⟨ sum-upper-bound o x y ⟩
                d + o + (d + o)
            □

        property :
              Digit-toℕ (Digit-fromℕ leftover o leftover-upper-bound) o
            + Digit-toℕ (Digit-fromℕ    carry o    carry-upper-bound) o * base
            ≡ sum o x y
        property =
            begin
                Digit-toℕ (Digit-fromℕ leftover o leftover-upper-bound) o
              + Digit-toℕ (Digit-fromℕ    carry o    carry-upper-bound) o * base
            ≡⟨ cong₂
                (λ l c → l + c * base)
                (Digit-fromℕ-toℕ leftover leftover-lower-bound leftover-upper-bound)
                (Digit-fromℕ-toℕ    carry    carry-lower-bound    carry-upper-bound)
            ⟩
                leftover + carry * base
            ≡⟨ refl ⟩
                sum o x y ∸ carry * base + carry * base
            ≡⟨ m∸n+n≡m $
                start
                    carry * base
                ≤⟨ n≤m+n o (carry * base) ⟩
                    o + carry * base
                ≤⟨ leftover-lower-bound-lemma remainder divModProp ⟩
                    sum o x y
                □
            ⟩
                sum o x y
            ∎

n+-Proper : ∀ {b d o}
    → (¬gapped : ¬ (Gapped#0 b d o))
    → (proper : suc d + o ≥ 2)
    → (x : Digit (suc d))
    → (xs : Numeral (suc b) (suc d) o)
    → Numeral (suc b) (suc d) o
n+-Proper {b} {d} {o} ¬gapped proper x xs with sumView b d o ¬gapped proper x (lsd xs)
n+-Proper ¬gapped proper x (_ ∙)    | NoCarry leftover property = leftover ∙
n+-Proper ¬gapped proper x (_ ∷ xs) | NoCarry leftover property = leftover ∷ xs
n+-Proper ¬gapped proper x (_ ∙)    | Fixed leftover carry property = leftover ∷ carry ∙
n+-Proper ¬gapped proper x (_ ∷ xs) | Fixed leftover carry property = leftover ∷ n+-Proper ¬gapped proper carry xs
n+-Proper ¬gapped proper x (_ ∙)    | Floating leftover carry property = leftover ∷ carry ∙
n+-Proper ¬gapped proper x (_ ∷ xs) | Floating leftover carry property = leftover ∷ n+-Proper ¬gapped proper carry xs

n+-Proper-toℕ : ∀ {b d o}
    → (¬gapped : ¬ (Gapped#0 b d o))
    → (proper : suc d + o ≥ 2)
    → (x : Digit (suc d))
    → (xs : Numeral (suc b) (suc d) o)
    → ⟦ n+-Proper ¬gapped proper x xs ⟧ ≡ Digit-toℕ x o + ⟦ xs ⟧
n+-Proper-toℕ {b} {d} {o} ¬gapped proper x xs with sumView b d o ¬gapped proper x (lsd xs)
n+-Proper-toℕ {b} {d} {o} ¬gapped proper x (_ ∙)    | NoCarry leftover property = property
n+-Proper-toℕ {b} {d} {o} ¬gapped proper x (x' ∷ xs) | NoCarry leftover property =
    begin
        ⟦ leftover ∷ xs ⟧
    ≡⟨ refl ⟩
        Digit-toℕ leftover o + ⟦ xs ⟧ * suc b
    ≡⟨ cong (λ w → w + ⟦ xs ⟧ * suc b) property ⟩
        Digit-toℕ x o + Digit-toℕ x' o + ⟦ xs ⟧ * suc b
    ≡⟨ +-assoc (Digit-toℕ x o) (Digit-toℕ x' o) (⟦ xs ⟧ * suc b) ⟩
        Digit-toℕ x o + ⟦ x' ∷ xs ⟧
    ∎
n+-Proper-toℕ {b} {d} {o} ¬gapped proper x (_ ∙)    | Fixed leftover carry property = property
n+-Proper-toℕ {b} {d} {o} ¬gapped proper x (x' ∷ xs) | Fixed leftover carry property =
    begin
        ⟦ leftover ∷ n+-Proper ¬gapped proper carry xs ⟧
    ≡⟨ refl ⟩
        Digit-toℕ leftover o + ⟦ n+-Proper ¬gapped proper carry xs ⟧ * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + w * suc b) (n+-Proper-toℕ ¬gapped proper carry xs) ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o + ⟦ xs ⟧) * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + w) (distribʳ-*-+ (suc b) (Digit-toℕ carry o) ⟦ xs ⟧) ⟩
        Digit-toℕ leftover o + ((Digit-toℕ carry o) * suc b + ⟦ xs ⟧ * suc b)
    ≡⟨ sym (+-assoc (Digit-toℕ leftover o) ((Digit-toℕ carry o) * suc b) (⟦ xs ⟧ * suc b)) ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o) * suc b + ⟦ xs ⟧ * suc b
    ≡⟨ cong (λ w → w + ⟦ xs ⟧ * suc b) property ⟩
        Digit-toℕ x o + Digit-toℕ x' o + ⟦ xs ⟧ * suc b
    ≡⟨ +-assoc (Digit-toℕ x o) (Digit-toℕ x' o) (⟦ xs ⟧ * suc b) ⟩
        Digit-toℕ x o + (Digit-toℕ x' o + ⟦ xs ⟧ * suc b)
    ∎
n+-Proper-toℕ {b} {d} {o} ¬gapped proper x (_ ∙)    | Floating leftover carry property = property
n+-Proper-toℕ {b} {d} {o} ¬gapped proper x (x' ∷ xs) | Floating leftover carry property =
    begin
        ⟦ leftover ∷ n+-Proper ¬gapped proper carry xs ⟧
    ≡⟨ refl ⟩
        Digit-toℕ leftover o + ⟦ n+-Proper ¬gapped proper carry xs ⟧ * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + w * suc b) (n+-Proper-toℕ ¬gapped proper carry xs) ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o + ⟦ xs ⟧) * suc b
    ≡⟨ cong (λ w → Digit-toℕ leftover o + w) (distribʳ-*-+ (suc b) (Digit-toℕ carry o) ⟦ xs ⟧) ⟩
        Digit-toℕ leftover o + ((Digit-toℕ carry o) * suc b + ⟦ xs ⟧ * suc b)
    ≡⟨ sym (+-assoc (Digit-toℕ leftover o) ((Digit-toℕ carry o) * suc b) (⟦ xs ⟧ * suc b)) ⟩
        Digit-toℕ leftover o + (Digit-toℕ carry o) * suc b + ⟦ xs ⟧ * suc b
    ≡⟨ cong (λ w → w + ⟦ xs ⟧ * suc b) property ⟩
        Digit-toℕ x o + Digit-toℕ x' o + ⟦ xs ⟧ * suc b
    ≡⟨ +-assoc (Digit-toℕ x o) (Digit-toℕ x' o) (⟦ xs ⟧ * suc b) ⟩
        Digit-toℕ x o + (Digit-toℕ x' o + ⟦ xs ⟧ * suc b)
    ∎

-- -- data N+Closed : (b d o : ℕ) → Set where
-- --     IsContinuous : ∀ {b d o} → (cont : True (Continuous? b d o)) → N+Closed b d o
-- --     ℤₙ : ∀ {o} → N+Closed 1 1 o
-- --
-- -- n+-ℤₙ : ∀ {o}
-- --     → (n : Digit 1)
-- --     → (xs : Numeral 1 1 (o))
-- --     → Numeral 1 1 o
-- -- n+-ℤₙ n xs = n ∷ xs
-- --
-- -- n+-ℤₙ-toℕ : ∀ {o}
-- --     → (n : Digit 1)
-- --     → (xs : Numeral 1 1 o)
-- --     → ⟦ n+-ℤₙ n xs ⟧ ≡ Digit-toℕ n o + ⟦ xs ⟧
-- -- n+-ℤₙ-toℕ {o} n xs =
-- --     begin
-- --         Fin.toℕ n + o + ⟦ xs ⟧ * suc zero
-- --     ≡⟨ cong (λ w → Fin.toℕ n + o + w) (*-right-identity ⟦ xs ⟧) ⟩
-- --         Fin.toℕ n + o + ⟦ xs ⟧
-- --     ∎
--
n+ : ∀ {b d o}
    → {cont : True (Continuous? b d o)}
    → (n : Digit d)
    → (xs : Numeral b d o)
    → Numeral b d o
n+ {b} {d} {o}      n xs with numView b d o
n+ {_} {_} {_} {()} n xs | NullBase d o
n+ {_} {_} {_}      n xs | NoDigits b o = NoDigits-explode xs
n+ {_} {_} {_} {()} n xs | AllZeros b
n+ {_} {_} {_}      n xs | Proper b d o proper with Gapped#0? b d o
n+ {_} {_} {_} {()} n xs | Proper b d o proper | yes gapped#0
n+ {_} {_} {_}      n xs | Proper b d o proper | no ¬gapped#0 = n+-Proper ¬gapped#0 proper n xs

n+-toℕ : ∀ {b d o}
    → {cont : True (Continuous? b d o)}
    → (n : Digit d)
    → (xs : Numeral b d o)
    → ⟦ n+ {cont = cont} n xs ⟧ ≡ Digit-toℕ n o + ⟦ xs ⟧
n+-toℕ {b} {d} {o}      n xs with numView b d o
n+-toℕ {_} {_} {_} {()} n xs | NullBase d o
n+-toℕ {_} {_} {_}      n xs | NoDigits b o = NoDigits-explode xs
n+-toℕ {_} {_} {_} {()} n xs | AllZeros b
n+-toℕ {_} {_} {_}      n xs | Proper b d o proper with Gapped#0? b d o
n+-toℕ {_} {_} {_} {()} n xs | Proper b d o proper | yes gapped#0
n+-toℕ {_} {_} {_}      n xs | Proper b d o proper | no ¬gapped#0 = n+-Proper-toℕ ¬gapped#0 proper n xs

⊹-Proper : ∀ {b d o}
    → (¬gapped : ¬ (Gapped#0 b d o))
    → (proper : suc d + o ≥ 2)
    → (xs ys : Numeral (suc b) (suc d) o)
    → Numeral (suc b) (suc d) o
⊹-Proper ¬gapped proper (x ∙)    ys       = n+-Proper ¬gapped proper x ys
⊹-Proper ¬gapped proper (x ∷ xs) (y ∙)    = n+-Proper ¬gapped proper y (x ∷ xs)
⊹-Proper {b} {d} {o} ¬gapped proper (x ∷ xs) (y ∷ ys) with sumView b d o ¬gapped proper x y
⊹-Proper ¬gapped proper (x ∷ xs) (y ∷ ys) | NoCarry leftover property = leftover ∷ ⊹-Proper ¬gapped proper xs ys
⊹-Proper ¬gapped proper (x ∷ xs) (y ∷ ys) | Fixed leftover carry property = leftover ∷ n+-Proper ¬gapped proper carry (⊹-Proper ¬gapped proper xs ys)
⊹-Proper ¬gapped proper (x ∷ xs) (y ∷ ys) | Floating leftover carry property = leftover ∷ n+-Proper ¬gapped proper carry (⊹-Proper ¬gapped proper xs ys)

_⊹_ : ∀ {b d o}
    → {cont : True (Continuous? b d o)}
    → (xs ys : Numeral b d o)
    → Numeral b d o
_⊹_ {b} {d} {o}  xs ys with numView b d o
_⊹_ {cont = ()}   xs ys | NullBase d o
_⊹_ {cont = cont} xs ys | NoDigits b o = NoDigits-explode xs
_⊹_ {cont = ()}   xs ys | AllZeros b
_⊹_ {cont = cont} xs ys | Proper b d o proper with Gapped#0? b d o
_⊹_ {cont = ()}   xs ys | Proper b d o proper | yes ¬gapped#0
_⊹_ {cont = cont} xs ys | Proper b d o proper | no ¬gapped#0 = ⊹-Proper ¬gapped#0 proper xs ys

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module Prelude.List where

open import Prelude.Nat
open import Prelude.Bool
open import Prelude.Maybe
open import Prelude.Product
open import Prelude.Empty
open import Prelude.Function
open import Prelude.Functor
open import Prelude.Applicative
open import Prelude.Monad
open import Prelude.Decidable
open import Prelude.Equality
open import Prelude.Ord
open import Prelude.Semiring
open import Prelude.Strict

open import Agda.Builtin.List public

infixr 5 _++_

pattern [_] x = x ∷ []

singleton : ∀ {a} {A : Set a} → A → List A
singleton x = x ∷ []

map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
map f []       = []
map f (x ∷ xs) = f x ∷ map f xs

_++_ : ∀ {a} {A : Set a} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ xs ++ ys

length : ∀ {a} {A : Set a} → List A → Nat
length []       = 0
length (x ∷ xs) = 1 + length xs

foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → List A → B
foldr f z []       = z
foldr f z (x ∷ xs) = f x (foldr f z xs)

foldl : ∀ {a b} {A : Set a} {B : Set b} → (B → A → B) → B → List A → B
foldl f z []       = z
foldl f z (x ∷ xs) = foldl f (f z x) xs

foldl! : ∀ {a b} {A : Set a} {B : Set b} → (B → A → B) → B → List A → B
foldl! f z []       = z
foldl! f z (x ∷ xs) = force (f z x) λ z′ → foldl! f z′ xs

reverse : ∀ {a} {A : Set a} → List A → List A
reverse xs = foldl (flip _∷_) [] xs

concat : ∀ {a} {A : Set a} → List (List A) → List A
concat = foldr _++_ []

concatMap : ∀ {a b} {A : Set a} {B : Set b} → (A → List B) → List A → List B
concatMap f = concat ∘ map f

filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
filter p [] = []
filter p (x ∷ xs) = if p x then x ∷ filter p xs
                           else filter p xs

catMaybes : ∀ {a} {A : Set a} → List (Maybe A) → List A
catMaybes [] = []
catMaybes (x ∷ xs) = maybe (catMaybes xs) (_∷ catMaybes xs) x

all? : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
all? p []       = true
all? p (x ∷ xs) = p x && all? p xs

any? : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
any? p []       = false
any? p (x ∷ xs) = p x || any? p xs

take : ∀ {a} {A : Set a} → Nat → List A → List A
take zero    _        = []
take (suc n) []       = []
take (suc n) (x ∷ xs) = x ∷ take n xs

drop : ∀ {a} {A : Set a} → Nat → List A → List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x ∷ xs) = drop n xs

splitAt : ∀ {a} {A : Set a} → Nat → List A → List A × List A
splitAt zero    xs       = [] , xs
splitAt (suc n) []       = [] , []
splitAt (suc n) (x ∷ xs) = first (x ∷_) (splitAt n xs)

null : ∀ {a} {A : Set a} → List A → Bool
null []      = true
null (_ ∷ _) = false

elem : ∀ {a} {A : Set a} {{EqA : Eq A}} → A → List A → Bool
elem x xs = not (null (filter (isYes ∘ _==_ x) xs))

lookup : ∀ {a b} {A : Set a} {B : Set b} {{EqA : Eq A}} → List (A × B) → A → Maybe B
lookup [] _ = nothing
lookup ((x₁ , v) ∷ xs) x = ifYes (x == x₁) then just v else lookup xs x

index : ∀ {a} {A : Set a} → List A → Nat → Maybe A
index [] _             = nothing
index (x ∷ xs) 0       = just x
index (x ∷ xs) (suc i) = index xs i

replicate : ∀ {a} {A : Set a} → Nat → A → List A
replicate zero x = []
replicate (suc n) x = x ∷ replicate n x

zipWith : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
            (A → B → C) → List A → List B → List C
zipWith f [] _ = []
zipWith f _ [] = []
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys

zip : ∀ {a b} {A : Set a} {B : Set b} → List A → List B → List (A × B)
zip = zipWith _,_

punctuate : ∀ {a} {A : Set a} → A → List A → List A
punctuate z []       = []
punctuate z [ x ]    = [ x ]
punctuate z (x ∷ xs) = x ∷ z ∷ punctuate z xs

module _ {a b} {F : Set a → Set b} {{_ : Applicative F}} {A : Set a} where

  replicateA : Nat → F A → F (List A)
  replicateA zero    _ = pure []
  replicateA (suc n) x = pure _∷_ <*> x <*> replicateA n x

module _ {a} {A : Set a} {{_ : Semiring A}} where

  sum : List A → A
  sum = foldl! _+_ zro

  product : List A → A
  product = foldl! _*_ one

  sumR : List A → A
  sumR = foldr _+_ zro

  productR : List A → A
  productR = foldr _*_ one

module _ {a} {A : Set a} {{_ : Ord A}} where
  insert : A → List A → List A
  insert x [] = x ∷ []
  insert x (y ∷ xs) = if x <? y then x ∷ y ∷ xs else y ∷ insert x xs

  sort : List A → List A
  sort [] = []
  sort (x ∷ xs) = insert x (sort xs)

infix 10 from_for_ from_to_ from_for_step_ from-to-step
from_for_ : Nat → Nat → List Nat
from 0 for 0     = []  -- make strict
from a for 0     = []
from a for suc d = a ∷ from suc a for d

from_for_step_ : Nat → Nat → Nat → List Nat
from 0 for 0     step _  = []  -- make strict
from a for 0     step _  = []
from a for suc c step d = a ∷ from a + d for c step d

from_to_ : Nat → Nat → List Nat
from a to b = from a for (suc b - a)

syntax from-to-step d a b = from a to b step d
from-to-step : (d : Nat) {{_ : NonZero d}} → Nat → Nat → List Nat
from-to-step d a b = from a for 1 + (b - a) div d step d

--- Equality ---

cons-inj-tail : ∀ {a} {A : Set a} {x : A} {xs : List A} {y : A}
               {ys : List A} →
             x ∷ xs ≡ y ∷ ys → xs ≡ ys
cons-inj-tail refl = refl

cons-inj-head : ∀ {a} {A : Set a} {x : A} {xs : List A} {y : A}
               {ys : List A} →
             x ∷ xs ≡ y ∷ ys → x ≡ y
cons-inj-head refl = refl

private
  dec-∷ : ∀ {a} {A : Set a} {x : A} {xs : List A} {y : A}
            {ys : List A} → Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x ∷ xs ≡ y ∷ ys)
  dec-∷ (yes refl) (yes refl) = yes refl
  dec-∷ _ (no neq) = no λ eq → neq (cons-inj-tail eq)
  dec-∷ (no neq) _ = no λ eq → neq (cons-inj-head eq)

  eqList : ∀ {a} {A : Set a} {{EqA : Eq A}} (xs ys : List A) → Dec (xs ≡ ys)
  eqList [] [] = yes refl
  eqList [] (_ ∷ _) = no (λ ())
  eqList (_ ∷ _) [] = no (λ ())
  eqList (x ∷ xs) (y ∷ ys) = dec-∷ (x == y) (eqList xs ys)

instance
  EqList : ∀ {a} {A : Set a} {{EqA : Eq A}} → Eq (List A)
  _==_ {{EqList}} = eqList

--- Ord ---

data LessList {a} {A : Set a} (_<_ : A → A → Set a) : List A → List A → Set a where
  nil<cons : ∀ {x xs} → LessList _<_ [] (x ∷ xs)
  head<    : ∀ {x y xs ys} → x < y → LessList _<_ (x ∷ xs) (y ∷ ys)
  tail<    : ∀ {x xs ys} → LessList _<_ xs ys → LessList _<_ (x ∷ xs) (x ∷ ys)

compareCons : ∀ {a} {A : Set a} {_<_ : A → A → Set a}
                {x : A} {xs : List A} {y : A} {ys : List A} →
                Comparison _<_ x y →
                Comparison (LessList _<_) xs ys →
                Comparison (LessList _<_) (x ∷ xs) (y ∷ ys)
compareCons (less lt)    _            = less (head< lt)
compareCons (greater gt) _            = greater (head< gt)
compareCons (equal refl) (less lt)    = less (tail< lt)
compareCons (equal refl) (greater gt) = greater (tail< gt)
compareCons (equal refl) (equal refl) = equal refl

compareList : ∀ {a} {A : Set a} {_<_ : A → A → Set a} (cmp : ∀ x y → Comparison _<_ x y) (xs ys : List A) →
              Comparison (LessList _<_) xs ys
compareList cmp [] [] = equal refl
compareList cmp [] (x ∷ ys) = less nil<cons
compareList cmp (x ∷ xs) [] = greater nil<cons
compareList cmp (x ∷ xs) (y ∷ ys) = compareCons (cmp x y) (compareList cmp xs ys)

instance
  OrdList : ∀ {a} {A : Set a} {{OrdA : Ord A}} → Ord (List A)
  OrdList = defaultOrd (compareList compare)

  OrdListLaws : ∀ {a} {A : Set a} {{OrdA : Ord/Laws A}} → Ord/Laws (List A)
  Ord/Laws.super OrdListLaws = it
  less-antirefl {{OrdListLaws {A = A}}} (head< hd) = less-antirefl {A = A} hd
  less-antirefl {{OrdListLaws {A = A}}} (tail< tl) = less-antirefl {A = List A} tl
  less-trans {{OrdListLaws}} nil<cons   (head< hd)  = nil<cons
  less-trans {{OrdListLaws}} nil<cons   (tail< tl)  = nil<cons
  less-trans {{OrdListLaws {A = A}}} (head< hd) (head< hd₁) = head< (less-trans {A = A} hd hd₁)
  less-trans {{OrdListLaws {A = A}}} (head< hd) (tail< tl)  = head< hd
  less-trans {{OrdListLaws {A = A}}} (tail< tl) (head< hd)  = head< hd
  less-trans {{OrdListLaws {A = A}}} (tail< tl) (tail< tl₁) = tail< (less-trans {A = List A} tl tl₁)

--- Functor ---

instance
  FunctorList : ∀ {a} → Functor (List {a})
  fmap {{FunctorList}} = map

  FunctorList′ : ∀ {a b} → Functor′ {a} {b} List
  fmap′ {{FunctorList′}} = map

  ApplicativeList : ∀ {a} → Applicative (List {a})
  pure  {{ApplicativeList}} x = x ∷ []
  _<*>_ {{ApplicativeList}} = monadAp (flip concatMap)

  ApplicativeList′ : ∀ {a b} → Applicative′ {a} {b} List
  _<*>′_ {{ApplicativeList′}} = monadAp′ (flip concatMap)

  MonadList : ∀ {a} → Monad (List {a})
  _>>=_  {{MonadList}} xs f = concatMap f xs

  MonadList′ : ∀ {a b} → Monad′ {a} {b} List
  _>>=′_ {{MonadList′}} xs f = concatMap f xs

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Dave.Embedding where
    open import Dave.Functions
    open import Dave.Equality
    open import Dave.Isomorphism

    infix 0 _≲_
    record _≲_ (A B : Set) : Set where
        field
            to : A → B
            from : B → A
            from∘to : ∀ (x : A) → from (to x) ≡ x

    open _≲_

    ≲-refl : ∀ {A : Set} → A ≲ A
    ≲-refl = record
        {
            to = λ a → a ;
            from = λ b → b ;
            from∘to = λ a → refl
        }

    ≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
    ≲-trans A≲B B≲C = record
        {
            to = λ a → to B≲C (to A≲B a) ;
            from = λ c → from A≲B (from B≲C c) ;
            from∘to = λ a → begin
                (from A≲B ∘ from B≲C) ((to B≲C ∘ to A≲B) a) ≡⟨⟩
                from A≲B (from B≲C (to B≲C (to A≲B a))) ≡⟨ cong (from A≲B) (from∘to B≲C (to A≲B a)) ⟩
                from A≲B (to A≲B a) ≡⟨ from∘to A≲B a ⟩
                a ∎
        }

    ≲-antisym : ∀ {A B : Set}
        → (A≲B : A ≲ B)
        → (B≲A : B ≲ A)
        → (to A≲B ≡ from B≲A)
        → (from A≲B ≡ to B≲A)
        → A ≃ B
    ≲-antisym A≲B B≲A to≡from from≡to = record
        {
            to = λ a → to A≲B a ;
            from = λ b → from A≲B b ;
            from∘to = from∘to A≲B;
            to∘from = λ b → begin
                to A≲B (from A≲B b) ≡⟨ cong (λ x → (to A≲B (x b))) from≡to ⟩
                to A≲B (to B≲A b) ≡⟨ cong-app to≡from (to B≲A b) ⟩
                from B≲A (to B≲A b) ≡⟨ from∘to B≲A b ⟩
                b ∎
        }

    module ≲-Reasoning where

        infix  1 ≲-begin_
        infixr 2 _≲⟨_⟩_
        infix  3 _≲-∎

        ≲-begin_ : ∀ {A B : Set}
            → A ≲ B
            -----
            → A ≲ B
        ≲-begin A≲B = A≲B

        _≲⟨_⟩_ : ∀ (A : Set) {B C : Set}
            → A ≲ B
            → B ≲ C
            -----
            → A ≲ C
        A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C

        _≲-∎ : ∀ (A : Set)
            -----
            → A ≲ A
        A ≲-∎ = ≲-refl

    open ≲-Reasoning

    ≃-implies-≲ : ∀ {A B : Set} → A ≃ B → A ≲ B
    ≃-implies-≲ A≃B = record
        {
            to = _≃_.to A≃B;
            from = _≃_.from A≃B;
            from∘to = _≃_.from∘to A≃B
        }


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

-- The phase distinction for extension.

module Calf.PhaseDistinction where

open import Calf.Prelude
open import Calf.Metalanguage

open import Relation.Binary.PropositionalEquality as P

-- Extensional phase.

postulate
  ext : Ω

-- Open/extensional modality.

◯ : □ → □
◯ A = ext → A

infix 10 ◯⁺_
infix 10 ◯⁻_
postulate
  ext/val : (ext → tp pos) → tp pos
  ext/val/decode : ∀ {A} → val (ext/val A) ≡ ∀ (u : ext) → (val (A u))
  {-# REWRITE ext/val/decode #-}

  ext/cmp : (ext → tp neg) → tp neg
  ext/cmp/decode : ∀ {A} → val (U (ext/cmp A)) ≡ ∀ (u : ext) → (cmp (A u))
  {-# REWRITE ext/cmp/decode #-}

◯⁺_ : tp pos → tp pos
◯⁺ A = ext/val (λ _ → A)
◯⁻_ : tp neg → tp neg
◯⁻ A = ext/cmp (λ _ → A)

-- Closed/intensional modality.

postulate
  ● : tp pos → tp pos
  η : ∀ {A} → val A → val (● A)
  ∗ : ∀ {A} → ext → val (● A)
  η≡∗ : ∀ {A} (a : val A) u → η {A} a ≡ ∗ u
  ●/ind : ∀ {A} (a : val (● A)) (X : val (● A) → tp neg)
    (x0 : (a : val A) → cmp (X (η a))) →
    (x1 : (u : ext) → cmp (X (∗ u))) →
    ((a : val A) → (u : ext) → P.subst (λ a → cmp (X a)) (η≡∗ a u) (x0 a) ≡ x1 u ) →
    cmp (X a)
  ●/ind/β₁ : ∀ {A} (a : val A) (X : val (● A) → tp neg)
    (x0 : (a : val A) → cmp (X (η a))) →
    (x1 : (u : ext) → cmp (X (∗ u))) →
    (h : (a : val A) → (u : ext) → P.subst (λ a → cmp (X a)) (η≡∗ a u) (x0 a) ≡ x1 u ) →
    ●/ind (η a) X x0 x1 h ≡ x0 a
  {-# REWRITE ●/ind/β₁ #-}
  ●/ind/β₂ : ∀ {A} (u : ext) (X : val (● A) → tp neg)
    (x0 : (a : val A) → cmp (X (η a))) →
    (x1 : (u : ext) → cmp (X (∗ u))) →
    (h : (a : val A) → (u : ext) → P.subst (λ a → cmp (X a)) (η≡∗ a u) (x0 a) ≡ x1 u ) →
    ●/ind (∗ u) X x0 x1 h ≡ x1 u
  {-# REWRITE ●/ind/β₂ #-}

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
module Data.List.At where

open import Data.Nat
open import Data.List
open import Data.List.Relation.Unary.All hiding (map; lookup; _[_]=_)
open import Data.List.Relation.Unary.Any hiding (map; lookup)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Binary.Pointwise hiding (refl; map)
open import Data.Fin hiding (_<_)
open import Data.Maybe hiding (map)
open import Data.Product hiding (map)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

maybe-lookup : ∀ {a}{A : Set a} → ℕ → List A → Maybe A
maybe-lookup n [] = nothing
maybe-lookup zero (x ∷ μ) = just x
maybe-lookup (suc n) (x ∷ μ) = maybe-lookup n μ

maybe-write : ∀ {a}{A : Set a} → ℕ → A →  List A → Maybe (List A)
maybe-write n _ [] = nothing
maybe-write zero v (x ∷ z) = just (v ∷ z)
maybe-write (suc n) v (x ∷ z) = maybe-write n v z

_[_]=_ : ∀ {a}{A : Set a} → List A → ℕ → A → Set _
l [ i ]= x = maybe-lookup i l ≡ just x

[]=-map : ∀ {a b}{A : Set a}{B : Set b}{x} i → (l : List A) →
                   l [ i ]= x → ∀ (f : A → B) → (map f l) [ i ]= (f x)
[]=-map _ [] ()
[]=-map zero (x ∷ l) refl = λ f → refl
[]=-map (suc i) (x ∷ l) p = []=-map i l p

at-lookup : ∀ {a}{A : Set a} → (l : List A) → (i : Fin (length l)) → l [ toℕ i ]= (lookup l i)
at-lookup [] ()
at-lookup (x ∷ l) zero = refl
at-lookup (x ∷ l) (suc i) = at-lookup l i

lookup-in : ∀ {a}{A : Set a} → (l : List A) → (i : Fin (length l)) → (lookup l i) ∈ l
lookup-in [] ()
lookup-in (x ∷ l) zero = here refl
lookup-in (x ∷ l) (suc i) = there (lookup-in l i)

dec-lookup : ∀ {a} {A : Set a} → (i : ℕ) → (l : List A) → Dec (∃ λ x → l [ i ]= x)
dec-lookup _ [] = no (λ{ (_ , ())})
dec-lookup zero (x ∷ l) = yes (x , refl)
dec-lookup (suc i) (_ ∷ l) = dec-lookup i l

all-lookup : ∀ {a} {A : Set a} {l : List A} {i x p P} → l [ i ]= x → All {p = p} P l → P x
all-lookup {l = []} () q
all-lookup {l = x ∷ l} {zero} refl (px ∷ q) = px
all-lookup {l = x ∷ l} {suc i} p (px ∷ q) = all-lookup p q

[]=-length : ∀ {a} {A : Set a} (L : List A) {i x} → L [ i ]= x → i < length L
[]=-length [] ()
[]=-length (x ∷ L) {zero} refl = s≤s z≤n
[]=-length (x ∷ L) {suc i} p = s≤s ([]=-length L p)

∷ʳ[length] : ∀ {a} {A : Set a} (l : List A) x → (l ∷ʳ x) [ length l ]= x
∷ʳ[length] [] y = refl
∷ʳ[length] (x ∷ Σ) y = ∷ʳ[length] Σ y

pointwise-lookup : ∀ {a b ℓ A B P l m i x} → Pointwise {a} {b} {ℓ} {A} {B} P l m →
                    l [ i ]= x → ∃ λ y → m [ i ]= y × P x y
pointwise-lookup [] ()
pointwise-lookup {i = zero} (x∼y ∷ q) refl = _ , refl , x∼y
pointwise-lookup {i = suc i} (x∼y ∷ q) p = pointwise-lookup q p

pointwise-lookup′ : ∀ {a b ℓ A B P l m i x y} → Pointwise {a} {b} {ℓ} {A} {B} P l m →
                    l [ i ]= x → m [ i ]= y → P x y
pointwise-lookup′ [] () q
pointwise-lookup′ {i = zero} (x∼y ∷ z) refl refl = x∼y
pointwise-lookup′ {i = suc i} (x∼y ∷ z) p q = pointwise-lookup′ z p q


text:
{-# OPTIONS --safe #-}
module Cubical.Relation.Binary.Poset where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport
open import Cubical.Foundations.SIP

open import Cubical.Data.Sigma

open import Cubical.Reflection.RecordEquiv
open import Cubical.Reflection.StrictEquiv

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Relation.Binary.Base

open Iso
open BinaryRelation

private
  variable
    ℓ ℓ' ℓ'' ℓ₀ ℓ₀' ℓ₁ ℓ₁' : Level

record IsPoset {A : Type ℓ} (_≤_ : A → A → Type ℓ') : Type (ℓ-max ℓ ℓ') where
  no-eta-equality
  constructor isposet

  field
    is-set : isSet A
    is-prop-valued : isPropValued _≤_
    is-refl : isRefl _≤_
    is-trans : isTrans _≤_
    is-antisym : isAntisym _≤_

unquoteDecl IsPosetIsoΣ = declareRecordIsoΣ IsPosetIsoΣ (quote IsPoset)

record PosetStr (ℓ' : Level) (A : Type ℓ) : Type (ℓ-max ℓ (ℓ-suc ℓ')) where

  constructor posetstr

  field
    _≤_     : A → A → Type ℓ'
    isPoset : IsPoset _≤_

  infixl 7 _≤_

  open IsPoset isPoset public

Poset : ∀ ℓ ℓ' → Type (ℓ-max (ℓ-suc ℓ) (ℓ-suc ℓ'))
Poset ℓ ℓ' = TypeWithStr ℓ (PosetStr ℓ')

poset : (A : Type ℓ) (_≤_ : A → A → Type ℓ') (h : IsPoset _≤_) → Poset ℓ ℓ'
poset A _≤_ h = A , posetstr _≤_ h

record IsPosetEquiv {A : Type ℓ₀} {B : Type ℓ₁}
  (M : PosetStr ℓ₀' A) (e : A ≃ B) (N : PosetStr ℓ₁' B)
  : Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') ℓ₁')
  where
  constructor
   isposetequiv
  -- Shorter qualified names
  private
    module M = PosetStr M
    module N = PosetStr N

  field
    pres≤ : (x y : A) → x M.≤ y ≃ equivFun e x N.≤ equivFun e y

PosetEquiv : (M : Poset ℓ₀ ℓ₀') (M : Poset ℓ₁ ℓ₁') → Type (ℓ-max (ℓ-max ℓ₀ ℓ₀') (ℓ-max ℓ₁ ℓ₁'))
PosetEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsPosetEquiv (M .snd) e (N .snd)

isPropIsPoset : {A : Type ℓ} (_≤_ : A → A → Type ℓ') → isProp (IsPoset _≤_)
isPropIsPoset _≤_ = isOfHLevelRetractFromIso 1 IsPosetIsoΣ
  (isPropΣ isPropIsSet
    λ isSetA → isPropΣ (isPropΠ2 (λ _ _ → isPropIsProp))
      λ isPropValued≤ → isProp×2
                         (isPropΠ (λ _ → isPropValued≤ _ _))
                           (isPropΠ5 λ _ _ _ _ _ → isPropValued≤ _ _)
                             (isPropΠ4 λ _ _ _ _ → isSetA _ _))

𝒮ᴰ-Poset : DUARel (𝒮-Univ ℓ) (PosetStr ℓ') (ℓ-max ℓ ℓ')
𝒮ᴰ-Poset =
  𝒮ᴰ-Record (𝒮-Univ _) IsPosetEquiv
    (fields:
      data[ _≤_ ∣ autoDUARel _ _ ∣ pres≤ ]
      prop[ isPoset ∣ (λ _ _ → isPropIsPoset _) ])
    where
    open PosetStr
    open IsPoset
    open IsPosetEquiv

PosetPath : (M N : Poset ℓ ℓ') → PosetEquiv M N ≃ (M ≡ N)
PosetPath = ∫ 𝒮ᴰ-Poset .UARel.ua

-- an easier way of establishing an equivalence of posets
module _ {P : Poset ℓ₀ ℓ₀'} {S : Poset ℓ₁ ℓ₁'} (e : ⟨ P ⟩ ≃ ⟨ S ⟩) where
  private
    module P = PosetStr (P .snd)
    module S = PosetStr (S .snd)

  module _ (isMon : ∀ x y → x P.≤ y → equivFun e x S.≤ equivFun e y)
           (isMonInv : ∀ x y → x S.≤ y → invEq e x P.≤ invEq e y) where
    open IsPosetEquiv
    open IsPoset

    makeIsPosetEquiv : IsPosetEquiv (P .snd) e (S .snd)
    pres≤ makeIsPosetEquiv x y = propBiimpl→Equiv (P.isPoset .is-prop-valued _ _)
                                                  (S.isPoset .is-prop-valued _ _)
                                                  (isMon _ _) (isMonInv' _ _)
      where
      isMonInv' : ∀ x y → equivFun e x S.≤ equivFun e y → x P.≤ y
      isMonInv' x y ex≤ey = transport (λ i → retEq e x i P.≤ retEq e y i) (isMonInv _ _ ex≤ey)

module PosetReasoning (P' : Poset ℓ ℓ') where
 private P = fst P'
 open PosetStr (snd P')
 open IsPoset

 _≤⟨_⟩_ : (x : P) {y z : P} → x ≤ y → y ≤ z → x ≤ z
 x ≤⟨ p ⟩ q = isPoset .is-trans x _ _ p q

 _◾ : (x : P) → x ≤ x
 x ◾ = isPoset .is-refl x

 infixr 0 _≤⟨_⟩_
 infix  1 _◾

max_stars_repo_name: FernandoLarrain/cubical


text:
module Common where

data PSet (A : Set) : Set where
  ⦃⦄ :  PSet A
  _::_ : A -> PSet A -> PSet A

data Pair (A : Set) : Set where
  <_,_> : A -> A -> Pair A

data Bool : Set where
  true : Bool
  false : Bool

neg : Bool -> Bool
neg true = false
neg false = true

_&&_ : Bool -> Bool -> Bool
true && true = true
_ && _ = false

_||_ : Bool -> Bool -> Bool
false || false = false
_ || _ = true

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

-- data _≡_ {a} {A : Set a} : A → A → Set where
--   refl : (a : A) → a ≡ a
-- sym : ∀ x y → x ≡ y → y ≡ x
-- sym .a .a (refl a) = refl a
-- isEq : ∀ x y -> x ≡ y -> Bool
-- isEq .a .a (refl a) = true

record Eq {a} (A : Set a) : Set a where
  field
    _==_ : A → A → Bool

open Eq {{...}} public

instance
  eqPair : {A : Set} {{_ : Eq A}} → Eq (Pair A)
  _==_ {{eqPair}} < x₁ , x₂ > < y₁ , y₂ > = (x₁ == y₁) && (x₂ == y₂)

max_stars_repo_name: daherb/Agda-Montague

max_issues_repo_name: daherb/Agda-Montague

max_forks_repo_name: daherb/Agda-Montague


text:
module Issue373 where

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

{-# BUILTIN NATURAL Nat #-}

{-# FOREIGN GHC data Nat = Zero | Suc Nat #-}
{-# COMPILE GHC Nat = data Nat (Zero | Suc) #-} -- should fail when compiling


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

module Cubical.Data.Fin.Recursive where

open import Cubical.Data.Fin.Recursive.Base public
open import Cubical.Data.Fin.Recursive.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module Issue591 where

import Issue591.M


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of List
------------------------------------------------------------------------

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

module Data.List.Categorical where

open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Data.Bool.Base using (false; true)
open import Data.List
open import Data.List.Properties
open import Function
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; _≗_; refl)
open P.≡-Reasoning

------------------------------------------------------------------------
-- List applicative functor

functor : ∀ {ℓ} → RawFunctor {ℓ} List
functor = record { _<$>_ = map }

applicative : ∀ {ℓ} → RawApplicative {ℓ} List
applicative = record
  { pure = [_]
  ; _⊛_  = λ fs as → concatMap (λ f → map f as) fs
  }

applicativeZero : ∀ {ℓ} → RawApplicativeZero {ℓ} List
applicativeZero = record
  { applicative = applicative
  ; ∅           = []
  }

alternative : ∀ {ℓ} → RawAlternative {ℓ} List
alternative = record
  { applicativeZero = applicativeZero
  ; _∣_             = _++_
  }

------------------------------------------------------------------------
-- List monad

monad : ∀ {ℓ} → RawMonad {ℓ} List
monad = record
  { return = [_]
  ; _>>=_  = flip concatMap
  }

monadZero : ∀ {ℓ} → RawMonadZero {ℓ} List
monadZero = record
  { monad           = monad
  ; applicativeZero = applicativeZero
  }

monadPlus : ∀ {ℓ} → RawMonadPlus {ℓ} List
monadPlus = record
  { monad = monad
  ; alternative = alternative
  }

------------------------------------------------------------------------
-- Get access to other monadic functions

module _ {f F} (App : RawApplicative {f} F) where

  open RawApplicative App

  sequenceA : ∀ {A} → List (F A) → F (List A)
  sequenceA []       = pure []
  sequenceA (x ∷ xs) = _∷_ <$> x ⊛ sequenceA xs

  mapA : ∀ {a} {A : Set a} {B} → (A → F B) → List A → F (List B)
  mapA f = sequenceA ∘ map f

  forA : ∀ {a} {A : Set a} {B} → List A → (A → F B) → F (List B)
  forA = flip mapA

module _ {m M} (Mon : RawMonad {m} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM = sequenceA App
  mapM = mapA App
  forM = forA App

------------------------------------------------------------------------
-- List monad transformer

monadT : ∀ {ℓ} → RawMonadT {ℓ} (_∘′ List)
monadT M = record
  { return = pure ∘′ [_]
  ; _>>=_  = λ mas f → mas >>= λ as → concat <$> mapM M f as
  } where open RawMonad M

------------------------------------------------------------------------
-- The list monad.

private
  open module LMP {ℓ} = RawMonadPlus (monadPlus {ℓ = ℓ})

module MonadProperties where

  left-identity : ∀ {ℓ} {A B : Set ℓ} (x : A) (f : A → List B) →
                  (return x >>= f) ≡ f x
  left-identity x f = ++-identityʳ (f x)

  right-identity : ∀ {ℓ} {A : Set ℓ} (xs : List A) →
                   (xs >>= return) ≡ xs
  right-identity []       = refl
  right-identity (x ∷ xs) = P.cong (x ∷_) (right-identity xs)

  left-zero : ∀ {ℓ} {A B : Set ℓ} (f : A → List B) → (∅ >>= f) ≡ ∅
  left-zero f = refl

  right-zero : ∀ {ℓ} {A B : Set ℓ} (xs : List A) →
               (xs >>= const ∅) ≡ ∅ {A = B}
  right-zero []       = refl
  right-zero (x ∷ xs) = right-zero xs

  private

    not-left-distributive :
      let xs = true ∷ false ∷ []; f = return; g = return in
      (xs >>= λ x → f x ∣ g x) ≢ ((xs >>= f) ∣ (xs >>= g))
    not-left-distributive ()

  right-distributive : ∀ {ℓ} {A B : Set ℓ}
                       (xs ys : List A) (f : A → List B) →
                       (xs ∣ ys >>= f) ≡ ((xs >>= f) ∣ (ys >>= f))
  right-distributive []       ys f = refl
  right-distributive (x ∷ xs) ys f = begin
    f x ∣ (xs ∣ ys >>= f)              ≡⟨ P.cong (f x ∣_) $ right-distributive xs ys f ⟩
    f x ∣ ((xs >>= f) ∣ (ys >>= f))    ≡⟨ P.sym $ ++-assoc (f x) _ _ ⟩
    ((f x ∣ (xs >>= f)) ∣ (ys >>= f))  ∎

  associative : ∀ {ℓ} {A B C : Set ℓ}
                (xs : List A) (f : A → List B) (g : B → List C) →
                (xs >>= λ x → f x >>= g) ≡ (xs >>= f >>= g)
  associative []       f g = refl
  associative (x ∷ xs) f g = begin
    (f x >>= g) ∣ (xs >>= λ x → f x >>= g)  ≡⟨ P.cong ((f x >>= g) ∣_) $ associative xs f g ⟩
    (f x >>= g) ∣ (xs >>= f >>= g)          ≡⟨ P.sym $ right-distributive (f x) (xs >>= f) g ⟩
    (f x ∣ (xs >>= f) >>= g)                ∎

  cong : ∀ {ℓ} {A B : Set ℓ} {xs₁ xs₂} {f₁ f₂ : A → List B} →
         xs₁ ≡ xs₂ → f₁ ≗ f₂ → (xs₁ >>= f₁) ≡ (xs₂ >>= f₂)
  cong {xs₁ = xs} refl f₁≗f₂ = P.cong concat (map-cong f₁≗f₂ xs)

------------------------------------------------------------------------
-- The applicative functor derived from the list monad.

-- Note that these proofs (almost) show that RawIMonad.rawIApplicative
-- is correctly defined. The proofs can be reused if proof components
-- are ever added to RawIMonad and RawIApplicative.

module Applicative where

  private

    module MP = MonadProperties

    -- A variant of flip map.

    pam : ∀ {ℓ} {A B : Set ℓ} → List A → (A → B) → List B
    pam xs f = xs >>= return ∘ f

  -- ∅ is a left zero for _⊛_.

  left-zero : ∀ {ℓ} {A B : Set ℓ} (xs : List A) → (∅ ⊛ xs) ≡ ∅ {A = B}
  left-zero xs = begin
    ∅ ⊛ xs          ≡⟨⟩
    (∅ >>= pam xs)  ≡⟨ MonadProperties.left-zero (pam xs) ⟩
    ∅               ∎

  -- ∅ is a right zero for _⊛_.

  right-zero : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) → (fs ⊛ ∅) ≡ ∅
  right-zero {ℓ} fs = begin
    fs ⊛ ∅            ≡⟨⟩
    (fs >>= pam ∅)    ≡⟨ (MP.cong (refl {x = fs}) λ f →
                          MP.left-zero (return ∘ f)) ⟩
    (fs >>= λ _ → ∅)  ≡⟨ MP.right-zero fs ⟩
    ∅                 ∎

  -- _⊛_ distributes over _∣_ from the right.

  right-distributive : ∀ {ℓ} {A B : Set ℓ} (fs₁ fs₂ : List (A → B)) xs →
                       ((fs₁ ∣ fs₂) ⊛ xs) ≡ (fs₁ ⊛ xs ∣ fs₂ ⊛ xs)
  right-distributive fs₁ fs₂ xs = begin
    (fs₁ ∣ fs₂) ⊛ xs                     ≡⟨⟩
    (fs₁ ∣ fs₂ >>= pam xs)               ≡⟨ MonadProperties.right-distributive fs₁ fs₂ (pam xs) ⟩
    (fs₁ >>= pam xs) ∣ (fs₂ >>= pam xs)  ≡⟨⟩
    (fs₁ ⊛ xs ∣ fs₂ ⊛ xs)                ∎

  -- _⊛_ does not distribute over _∣_ from the left.

  private

    not-left-distributive :
      let fs = id ∷ id ∷ []; xs₁ = true ∷ []; xs₂ = true ∷ false ∷ [] in
      (fs ⊛ (xs₁ ∣ xs₂)) ≢ (fs ⊛ xs₁ ∣ fs ⊛ xs₂)
    not-left-distributive ()

  -- Applicative functor laws.

  identity : ∀ {a} {A : Set a} (xs : List A) → (return id ⊛ xs) ≡ xs
  identity xs = begin
    return id ⊛ xs          ≡⟨⟩
    (return id >>= pam xs)  ≡⟨ MonadProperties.left-identity id (pam xs) ⟩
    (xs >>= return)         ≡⟨ MonadProperties.right-identity xs ⟩
    xs                      ∎

  private

    pam-lemma : ∀ {ℓ} {A B C : Set ℓ}
                (xs : List A) (f : A → B) (fs : B → List C) →
                (pam xs f >>= fs) ≡ (xs >>= λ x → fs (f x))
    pam-lemma xs f fs = begin
      (pam xs f >>= fs)                   ≡⟨ P.sym $ MP.associative xs (return ∘ f) fs ⟩
      (xs >>= λ x → return (f x) >>= fs)  ≡⟨ MP.cong (refl {x = xs}) (λ x → MP.left-identity (f x) fs) ⟩
      (xs >>= λ x → fs (f x))             ∎

  composition : ∀ {ℓ} {A B C : Set ℓ}
                (fs : List (B → C)) (gs : List (A → B)) xs →
                (return _∘′_ ⊛ fs ⊛ gs ⊛ xs) ≡ (fs ⊛ (gs ⊛ xs))
  composition {ℓ} fs gs xs = begin
    return _∘′_ ⊛ fs ⊛ gs ⊛ xs                      ≡⟨⟩
    (return _∘′_ >>= pam fs >>= pam gs >>= pam xs)  ≡⟨ MP.cong (MP.cong (MP.left-identity _∘′_ (pam fs))
                                                                              (λ f → refl {x = pam gs f}))
                                                                  (λ fg → refl {x = pam xs fg}) ⟩
    (pam fs _∘′_ >>= pam gs >>= pam xs)             ≡⟨ MP.cong (pam-lemma fs _∘′_ (pam gs)) (λ _ → refl) ⟩
    ((fs >>= λ f → pam gs (f ∘′_)) >>= pam xs)      ≡⟨ P.sym $ MP.associative fs (λ f → pam gs (_∘′_ f)) (pam xs) ⟩
    (fs >>= λ f → pam gs (f ∘′_) >>= pam xs)        ≡⟨ (MP.cong (refl {x = fs}) λ f →
                                                        pam-lemma gs (f ∘′_) (pam xs)) ⟩
    (fs >>= λ f → gs >>= λ g → pam xs (f ∘′ g))     ≡⟨ (MP.cong (refl {x = fs}) λ f →
                                                        MP.cong (refl {x = gs}) λ g →
                                                        P.sym $ pam-lemma xs g (return ∘ f)) ⟩
    (fs >>= λ f → gs >>= λ g → pam (pam xs g) f)    ≡⟨ (MP.cong (refl {x = fs}) λ f →
                                                        MP.associative gs (pam xs) (return ∘ f)) ⟩
    (fs >>= pam (gs >>= pam xs))                    ≡⟨⟩
    fs ⊛ (gs ⊛ xs)                                  ∎

  homomorphism : ∀ {ℓ} {A B : Set ℓ} (f : A → B) x →
                 (return f ⊛ return x) ≡ return (f x)
  homomorphism f x = begin
    return f ⊛ return x            ≡⟨⟩
    (return f >>= pam (return x))  ≡⟨ MP.left-identity f (pam (return x)) ⟩
    pam (return x) f               ≡⟨ MP.left-identity x (return ∘ f) ⟩
    return (f x)                   ∎

  interchange : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) {x} →
                (fs ⊛ return x) ≡ (return (λ f → f x) ⊛ fs)
  interchange fs {x} = begin
    fs ⊛ return x                    ≡⟨⟩
    (fs >>= pam (return x))          ≡⟨ (MP.cong (refl {x = fs}) λ f →
                                         MP.left-identity x (return ∘ f)) ⟩
    (fs >>= λ f → return (f x))      ≡⟨⟩
    (pam fs (λ f → f x))             ≡⟨ P.sym $ MP.left-identity (λ f → f x) (pam fs) ⟩
    (return (λ f → f x) >>= pam fs)  ≡⟨⟩
    return (λ f → f x) ⊛ fs          ∎