text:
-- Raw terms, weakening (renaming) and substitution.

{-# OPTIONS --safe #-}

module Definition.Untyped where

open import Tools.Nat
open import Tools.Product
open import Tools.List
import Tools.PropositionalEquality as PE

import Data.Fin as Fin
import Data.Nat as Nat

infixl 30 _∙_^_
infix 30 Π_^_°_▹_°_°_
infixr 22 _^_°_▹▹_°_°_
infixl 30 _ₛ•ₛ_ _•ₛ_ _ₛ•_
infix 25 _[_]
infix 25 _[_]↑

data Relevance : Set where
  ! : Relevance -- proof-relevant
  % : Relevance -- proof-irrelevant

!≢% : ! PE.≢ %
!≢% ()

-- two levels of small types
data Level : Set where
  ⁰ : Level
  ¹ : Level

⁰≢¹ : ⁰ PE.≢ ¹
⁰≢¹ ()

data _<_ : (i j : Level) → Set where
  0<1 : ⁰ < ¹

data _≤_ (i j : Level) : Set where
  <is≤  : i < j → i ≤ j
  ≡is≤ : i PE.≡ j → i ≤ j

-- Large type levels : ι ⁰, ι ¹, ∞
data TypeLevel : Set where
  ι : Level → TypeLevel
  ∞ : TypeLevel

data _<∞_ : (i j : TypeLevel) → Set where
  emb< : ι ⁰ <∞ ι ¹
  ∞< : ι ¹ <∞ ∞
  -- ∞<⁰ : ι ⁰ <∞ ∞

data _≤∞_ (i j : TypeLevel) : Set where
  <∞is≤∞  : i <∞ j → i ≤∞ j
  ≡is≤∞ : i PE.≡ j → i ≤∞ j

next : Level → TypeLevel
next ⁰ = ι ¹
next ¹ = ∞

toLevel : TypeLevel → Level
toLevel (ι ⁰) = ⁰
toLevel (ι ¹) = ¹
toLevel ∞ = ¹

predLevel : TypeLevel → Level
predLevel (ι ⁰) = ⁰
predLevel (ι ¹) = ⁰
predLevel ∞ = ¹

maxLevel : (i : Level) → (j : Level) → Σ Level λ k → i ≤ k × j ≤ k
maxLevel ⁰ ⁰ = ⁰ , ((≡is≤ PE.refl) , (≡is≤ PE.refl))
maxLevel ⁰ ¹ = ¹ , ((<is≤ 0<1) , (≡is≤ PE.refl))
maxLevel ¹ ⁰ = ¹ , ((≡is≤ PE.refl) , (<is≤ 0<1))
maxLevel ¹ ¹ = ¹ , ((≡is≤ PE.refl) , (≡is≤ PE.refl))

⁰min : (i : Level) → ⁰ ≤ i
⁰min ⁰ = ≡is≤ PE.refl
⁰min ¹ = <is≤ 0<1

<next : ∀ {l} → ι l <∞ next l
<next {⁰} = emb<
<next {¹} = ∞<

levelBounded : (i : Level) → Σ TypeLevel λ k → ι i <∞ k
levelBounded i = next i , <next

ιinj : ∀ {l l'} → ι l PE.≡ ι l' → l PE.≡ l'
ιinj {⁰} {⁰} e = PE.refl
ιinj {¹} {¹} e = PE.refl

next-inj : ∀ {l l'} → next l PE.≡ next l' → l PE.≡ l'
next-inj {⁰} {⁰} e = PE.refl
next-inj {¹} {¹} e = PE.refl

-- In a typing judgment, a type is generally annotated with a pair of a relevance and a level
record TypeInfo : Set where
  constructor [_,_]
  field
    r : Relevance
    l : TypeLevel

toTypeInfo : Relevance × Level → TypeInfo
toTypeInfo ( r , l ) = [ r , ι l ]

-- Typing contexts (snoc-lists, isomorphic to lists).
data Con (A : Set) : Set where
  ε   : Con A               -- Empty context.
  _∙_^_ : Con A → A → TypeInfo → Con A  -- Context extension.

record GenT (A : Set) : Set where
  inductive
  constructor ⟦_,_⟧
  field
    l : Nat
    t : A

data Kind : Set where
  Ukind : Relevance → Level → Kind
  Pikind : Relevance → Level → Level → Level → Kind
  Natkind : Kind
  Lamkind : Level → Kind
  Appkind : Level → Kind
  Zerokind : Kind
  Suckind : Kind
  Natreckind : Level → Kind
  Emptykind : Level → Kind
  Emptyreckind : Level → Level → Kind
  Idkind : Kind
  Idreflkind : Kind
  Transpkind : Kind
  Castkind : Level → Kind
  Castreflkind : Kind
  Sigmakind : Kind
  Pairkind : Kind
  Fstkind : Kind
  Sndkind : Kind

data Term : Set where
  var : (x : Nat) → Term
  gen : (k : Kind) (c : List (GenT Term)) → Term

-- The Grammar of our language.

-- We represent the expressions of our language as de Bruijn terms.
-- Variables are natural numbers interpreted as de Bruijn indices.
-- Π, lam, ∃ , transp and natrec are binders.

-- Type constructors.
-- Universes of proof-relevant types
U      : Level → Term
U l = gen (Ukind ! l) []

-- Universes of proof-irrelevant types
SProp : Level → Term
SProp l = gen (Ukind % l) []

pattern Univ r l = gen (Ukind r l) []

-- Dependent product, with level annotations for the domain, codomain, and resulting type
Π_^_°_▹_°_°_   : Term → Relevance → Level → Term → Level → Level → Term  -- Dependent function type (B is a binder).
Π A ^ r ° lA ▹ B ° lB ° lΠ = gen (Pikind r lA lB lΠ) (⟦ 0 , A ⟧ ∷ ⟦ 1 , B ⟧ ∷ [])

-- Existential type : dependent pairs of proof-irrelevant terms
∃_▹_ : Term → Term → Term
∃ A ▹ B = gen Sigmakind (⟦ 0 , A ⟧ ∷ ⟦ 1 , B ⟧ ∷ [])

-- Natural numbers
ℕ      : Term
ℕ = gen Natkind []

-- Lambda-calculus.
-- var    : (x : Nat)        → Term  -- Variable (de Bruijn index).
-- var = var

lam_▹_^_    : Term → Term → Level → Term  -- Function abstraction (binder).
lam A ▹ t ^ l = gen (Lamkind l) (⟦ 0 , A ⟧ ∷ ⟦ 1 , t ⟧ ∷ [])

_∘_^_    : (t u : Term) (l : Level)    → Term  -- Application.
t ∘ u ^ l = gen (Appkind l) (⟦ 0 , t ⟧ ∷ ⟦ 0 , u ⟧ ∷ [])

⦅_,_,_⦆ : Term → Term → Term → Term -- Dependent pair formation
⦅ G , t , u ⦆ = gen Pairkind (⟦ 1 , G ⟧ ∷ ⟦ 0 , t ⟧ ∷ ⟦ 0 , u ⟧ ∷ [])

fst : (t : Term) → Term -- Dependent pair elimination
fst t = gen Fstkind (⟦ 0 , t ⟧ ∷ [])

snd : (t : Term) → Term -- Dependent pair elimination
snd t = gen Sndkind (⟦ 0 , t ⟧ ∷ [])

-- Introduction and elimination of natural numbers.
zero   : Term                     -- Natural number zero.
zero = gen Zerokind []

suc    : (t : Term)       → Term  -- Successor.
suc t = gen Suckind (⟦ 0 , t ⟧ ∷ [])

natrec : (l : Level) (A t u v : Term) → Term  -- Recursor (A is a binder).
natrec l A t u v = gen (Natreckind l) (⟦ 1 , A ⟧ ∷ ⟦ 0 , t ⟧ ∷ ⟦ 0 , u ⟧ ∷ ⟦ 0 , v ⟧ ∷ [])

-- Empty type
Empty : Level → Term
Empty l = gen (Emptykind l) []

-- Eliminator for the empty type
Emptyrec : (l lEmpty : Level) (A e : Term) -> Term
Emptyrec l lEmpty A e = gen (Emptyreckind l lEmpty) (⟦ 0 , A ⟧ ∷ ⟦ 0 , e ⟧ ∷ [])

-- Identity type
Id : (A t u : Term) → Term
Id A t u = gen Idkind (⟦ 0 , A ⟧ ∷ ⟦ 0 , t ⟧ ∷ ⟦ 0 , u ⟧ ∷ [])

-- witness of reflexivity of equality
Idrefl : (A t : Term) → Term
Idrefl A t = gen Idreflkind (⟦ 0 , A ⟧ ∷ ⟦ 0 , t ⟧ ∷ [])

-- transport on propositions
transp : (A P t s u e : Term) → Term
transp A P t s u e = gen Transpkind (⟦ 0 , A ⟧ ∷ ⟦ 1 , P ⟧ ∷ ⟦ 0 , t ⟧ ∷ ⟦ 0 , s ⟧ ∷ ⟦ 0 , u ⟧ ∷ ⟦ 0 , e ⟧ ∷ [])

-- cast between types, used to implement transport
cast : Level → (A B e t : Term) → Term
cast l A B e t = gen (Castkind l) (⟦ 0 , A ⟧ ∷ ⟦ 0 , B ⟧ ∷ ⟦ 0 , e ⟧ ∷ ⟦ 0 , t ⟧ ∷ [])

-- propositional proof that casting with reflexivity is the identity
castrefl : (A t : Term) → Term
castrefl A t = gen Castreflkind (⟦ 0 , A ⟧ ∷ ⟦ 0 , t ⟧ ∷ [])

-- Injectivity of term constructors w.r.t. propositional equality.

-- If  Π F G = Π H E  then  F = H  and  G = E.

Π-PE-injectivity : ∀ {F rF lF G lG lΠ H rH lH E lE lΠ'} → Π F ^ rF ° lF ▹ G ° lG ° lΠ PE.≡ Π H ^ rH ° lH ▹ E ° lE ° lΠ'
  → F PE.≡ H × rF PE.≡ rH × lF PE.≡ lH × G PE.≡ E × lG PE.≡ lE × lΠ PE.≡ lΠ'
Π-PE-injectivity PE.refl = PE.refl , PE.refl , PE.refl , PE.refl , PE.refl , PE.refl

∃-PE-injectivity : ∀ {F G H E} → ∃ F ▹ G PE.≡ ∃ H ▹ E
  → F PE.≡ H × G PE.≡ E
∃-PE-injectivity PE.refl = PE.refl , PE.refl

-- If  suc n = suc m  then  n = m.

suc-PE-injectivity : ∀ {n m} → suc n PE.≡ suc m → n PE.≡ m
suc-PE-injectivity PE.refl = PE.refl

Univ-PE-injectivity : ∀ {r r' l l'} → Univ r l PE.≡ Univ r' l' → r PE.≡ r' × l PE.≡ l'
Univ-PE-injectivity PE.refl = PE.refl , PE.refl

-- Neutral terms.

-- A term is neutral if
-- either it has a variable in head position that blocks reduction.
-- either it is of the form Emptyrec (or terms that should reduce to emptyrec, such as incompatible casts)

data Neutral : Term → Set where
  var     : ∀ n                     → Neutral (var n)
  ∘ₙ      : ∀ {k u l}     → Neutral k → Neutral (k ∘ u ^ l)
  natrecₙ : ∀ {l C c g k} → Neutral k → Neutral (natrec l C c g k)
  Idₙ : ∀ {A t u} → Neutral A → Neutral (Id A t u)
  Idℕₙ : ∀ {t u} → Neutral t → Neutral (Id ℕ t u)
  Idℕ0ₙ : ∀ {u} → Neutral u → Neutral (Id ℕ zero u)
  IdℕSₙ : ∀ {t u} → Neutral u → Neutral (Id ℕ (suc t) u)
  IdUₙ : ∀ {t u l} → Neutral t → Neutral (Id (U l) t u)
  IdUℕₙ : ∀ {u l} → Neutral u → Neutral (Id (U l) ℕ u)
  IdUΠₙ : ∀ {A rA lA B lB l u} → Neutral u → Neutral (Id (U l) (Π A ^ rA ° lA ▹ B ° lB ° l) u)
  castₙ : ∀ {l A B e t} → Neutral A → Neutral (cast l A B e t)
  castℕₙ : ∀ {l B e t} → Neutral B → Neutral (cast l ℕ B e t)
  castΠₙ : ∀ {l A rA lA P lP B e t} → Neutral B → Neutral (cast l (Π A ^ rA ° lA ▹ P ° lP ° l) B e t)
  castℕℕₙ : ∀ {l e t} → Neutral t → Neutral (cast l ℕ ℕ e t)
  castℕΠₙ : ∀ {l A rA B e t} → Neutral (cast l ℕ (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) e t)
  castΠℕₙ : ∀ {l A rA B e t} → Neutral (cast l (Π A ^ rA ° ⁰ ▹ B ° ⁰ ° l) ℕ e t)
  castΠΠ%!ₙ : ∀ {l A B A' B' e t} → Neutral (cast l (Π A ^ % ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ ! ° ⁰ ▹ B' ° ⁰ ° l) e t)
  castΠΠ!%ₙ : ∀ {l A B A' B' e t} → Neutral (cast l (Π A ^ ! ° ⁰ ▹ B ° ⁰ ° l) (Π A' ^ % ° ⁰ ▹ B' ° ⁰ ° l) e t)
  Emptyrecₙ : ∀ {l lEmpty A e} -> Neutral (Emptyrec l lEmpty A e)

-- Weak head normal forms (whnfs).
-- These are the (lazy) values of our language.

data Whnf : Term → Set where

  -- Type constructors are whnfs.
  Uₙ    : ∀ {r l} → Whnf (Univ r l)
  Πₙ    : ∀ {A r lA B lB l} → Whnf (Π A ^ r ° lA ▹ B ° lB ° l)
  ∃ₙ    : ∀ {A B} → Whnf (∃ A ▹ B)
  ℕₙ    : Whnf ℕ
  Emptyₙ : ∀ {l} → Whnf (Empty l)

  -- Introductions are whnfs.
  lamₙ  : ∀ {A t l} → Whnf (lam A ▹ t ^ l)
  zeroₙ : Whnf zero
  sucₙ  : ∀ {t} → Whnf (suc t)

  -- Neutrals are whnfs.
  ne   : ∀ {n} → Neutral n → Whnf n

-- Whnf inequalities.

-- Different whnfs are trivially distinguished by propositional equality.
-- (The following statements are sometimes called "no-confusion theorems".)

U≢ℕ : ∀ {r l} → Univ r l PE.≢ ℕ
U≢ℕ ()

U≢Empty : ∀ {r l l'} → Univ r l PE.≢ Empty l'
U≢Empty ()

U≢Π : ∀ {r r' l F lF G lG l'} → Univ r l PE.≢ Π F ^ r' ° lF ▹ G ° lG ° l'
U≢Π ()

U≢∃ : ∀ {r l F G} → Univ r l PE.≢ ∃ F ▹ G
U≢∃ ()

U≢ne : ∀ {r l K} → Neutral K → Univ r l PE.≢ K
U≢ne () PE.refl

ℕ≢Π : ∀ {F r lF G lG l} → ℕ PE.≢ Π F ^ r ° lF ▹ G ° lG ° l
ℕ≢Π ()

ℕ≢∃ : ∀ {F G} → ℕ PE.≢ ∃ F ▹ G
ℕ≢∃ ()

ℕ≢Empty : ∀ {l} → ℕ PE.≢ Empty l
ℕ≢Empty ()

Empty≢ℕ : ∀ {l} → Empty l PE.≢ ℕ
Empty≢ℕ ()

ℕ≢ne : ∀ {K} → Neutral K → ℕ PE.≢ K
ℕ≢ne () PE.refl

Empty≢ne : ∀ {l K} → Neutral K → Empty l PE.≢ K
Empty≢ne () PE.refl

Empty≢Π : ∀ {F r lF G lG l l'} → Empty l' PE.≢ Π F ^ r ° lF ▹ G ° lG ° l
Empty≢Π ()

Empty≢∃ : ∀ {l F G} → Empty l PE.≢ ∃ F ▹ G
Empty≢∃ ()

Π≢ne : ∀ {F r lF G lG K l} → Neutral K → Π F ^ r ° lF ▹ G ° lG ° l PE.≢ K
Π≢ne () PE.refl

Π≢∃ : ∀ {F r lF G lG F' G' l} → Π F ^ r ° lF ▹ G ° lG ° l PE.≢ ∃ F' ▹ G'
Π≢∃ ()

∃≢ne : ∀ {F G K} → Neutral K → ∃ F ▹ G PE.≢ K
∃≢ne () PE.refl

zero≢suc : ∀ {n} → zero PE.≢ suc n
zero≢suc ()

zero≢ne : ∀ {k} → Neutral k → zero PE.≢ k
zero≢ne () PE.refl

suc≢ne : ∀ {n k} → Neutral k → suc n PE.≢ k
suc≢ne () PE.refl

-- Several views on whnfs (note: not recursive).

-- A whnf of type ℕ is either zero, suc t, or neutral.

data Natural : Term → Set where
  zeroₙ :                     Natural zero
  sucₙ  : ∀ {t}             → Natural (suc t)
  ne    : ∀ {n} → Neutral n → Natural n

-- A type in whnf is either Π A B, ℕ, or neutral.
-- Large types could also be U.

data Type : Term → Set where
  Πₙ : ∀ {A r lA B lB l} → Type (Π A ^ r ° lA ▹ B ° lB ° l)
  ℕₙ : Type ℕ
  Uₙ : ∀ {r l} → Type (Univ r l)
  Emptyₙ : ∀ {l} → Type (Empty l)
  ∃ₙ : ∀ {A B} → Type (∃ A ▹ B)
  ne : ∀{n} → Neutral n → Type n

-- A whnf of type Π A B is either lam t or neutral.

data Function : Term → Set where
  lamₙ : ∀{A t l} → Function (lam A ▹ t ^ l)
  ne : ∀{n} → Neutral n → Function n

-- These views classify only whnfs.
-- Natural, Type, and Function are a subsets of Whnf.

naturalWhnf : ∀ {n} → Natural n → Whnf n
naturalWhnf sucₙ = sucₙ
naturalWhnf zeroₙ = zeroₙ
naturalWhnf (ne x) = ne x

typeWhnf : ∀ {A} → Type A → Whnf A
typeWhnf Πₙ = Πₙ
typeWhnf ℕₙ = ℕₙ
typeWhnf Uₙ  = Uₙ
typeWhnf ∃ₙ = ∃ₙ
typeWhnf Emptyₙ = Emptyₙ
typeWhnf (ne x) = ne x

functionWhnf : ∀ {f} → Function f → Whnf f
functionWhnf lamₙ = lamₙ
functionWhnf (ne x) = ne x

------------------------------------------------------------------------
-- Weakening

-- In the following we define untyped weakenings η : Wk.
-- The typed form could be written η : Γ ≤ Δ with the intention
-- that η transport a term t living in context Δ to a context Γ
-- that can bind additional variables (which cannot appear in t).
-- Thus, if Δ ⊢ t : A and η : Γ ≤ Δ then Γ ⊢ wk η t : wk η A.
--
-- Even though Γ is "larger" than Δ we write Γ ≤ Δ to be conformant
-- with subtyping A ≤ B.  With subtyping, relation Γ ≤ Δ could be defined as
-- ``for all x ∈ dom(Δ) have Γ(x) ≤ Δ(x)'' (in the sense of subtyping)
-- and this would be the natural extension of weakenings.

data Wk : Set where
  id    : Wk        -- η : Γ ≤ Γ.
  step  : Wk  → Wk  -- If η : Γ ≤ Δ then step η : Γ∙A ≤ Δ.
  lift  : Wk  → Wk  -- If η : Γ ≤ Δ then lift η : Γ∙A ≤ Δ∙A.

-- Composition of weakening.
-- If η : Γ ≤ Δ and η′ : Δ ≤ Φ then η • η′ : Γ ≤ Φ.

infixl 30 _•_

_•_                :  Wk → Wk → Wk
id      • η′       =  η′
step η  • η′       =  step  (η • η′)
lift η  • id       =  lift  η
lift η  • step η′  =  step  (η • η′)
lift η  • lift η′  =  lift  (η • η′)

repeat : {A : Set} → (A → A) → A → Nat → A
repeat f a 0 = a
repeat f a (1+ n) = f (repeat f a n)

-- Weakening of variables.
-- If η : Γ ≤ Δ and x ∈ dom(Δ) then wkVar ρ x ∈ dom(Γ).

wkVar : (ρ : Wk) (n : Nat) → Nat
wkVar id       n        = n
wkVar (step ρ) n        = 1+ (wkVar ρ n)
wkVar (lift ρ) 0    = 0
wkVar (lift ρ) (1+ n) = 1+ (wkVar ρ n)

  -- Weakening of terms.
  -- If η : Γ ≤ Δ and Δ ⊢ t : A then Γ ⊢ wk η t : wk η A.

mutual
  wkGen : (ρ : Wk) (g : List (GenT Term)) → List (GenT Term)
  wkGen ρ [] = []
  wkGen ρ (⟦ l , t ⟧ ∷ g) = ⟦ l , (wk (repeat lift ρ l) t) ⟧ ∷ wkGen ρ g

  wk : (ρ : Wk) (t : Term) → Term
  wk ρ (var x) = var (wkVar ρ x)
  wk ρ (gen x c) = gen x (wkGen ρ c)

-- Adding one variable to the context requires wk1.
-- If Γ ⊢ t : B then Γ∙A ⊢ wk1 t : wk1 B.

wk1 : Term → Term
wk1 = wk (step id)

wk1d : Term → Term
wk1d = wk (lift (step id))

-- Weakening of a neutral term.

wkNeutral : ∀ {t} ρ → Neutral t → Neutral (wk ρ t)
wkNeutral ρ (var n)    = var (wkVar ρ n)
wkNeutral ρ (∘ₙ n)    = ∘ₙ (wkNeutral ρ n)
wkNeutral ρ (natrecₙ n) = natrecₙ (wkNeutral ρ n)
wkNeutral ρ Emptyrecₙ = Emptyrecₙ
wkNeutral ρ (Idₙ A) = Idₙ (wkNeutral ρ A)
wkNeutral ρ (Idℕₙ t) = Idℕₙ (wkNeutral ρ t)
wkNeutral ρ (Idℕ0ₙ t) = Idℕ0ₙ (wkNeutral ρ t)
wkNeutral ρ (IdℕSₙ t) = IdℕSₙ (wkNeutral ρ t)
wkNeutral ρ (IdUₙ t) = IdUₙ (wkNeutral ρ t)
wkNeutral ρ (IdUℕₙ t) = IdUℕₙ (wkNeutral ρ t)
wkNeutral ρ (IdUΠₙ t) = IdUΠₙ (wkNeutral ρ t)
wkNeutral ρ (castₙ A) = castₙ (wkNeutral ρ A)
wkNeutral ρ (castℕₙ A) = castℕₙ (wkNeutral ρ A)
wkNeutral ρ (castΠₙ A) = castΠₙ (wkNeutral ρ A)
wkNeutral ρ (castℕℕₙ t) = castℕℕₙ (wkNeutral ρ t)
wkNeutral ρ castℕΠₙ = castℕΠₙ
wkNeutral ρ castΠℕₙ = castΠℕₙ
wkNeutral ρ castΠΠ%!ₙ = castΠΠ%!ₙ
wkNeutral ρ castΠΠ!%ₙ = castΠΠ!%ₙ

-- Weakening can be applied to our whnf views.

wkNatural : ∀ {t} ρ → Natural t → Natural (wk ρ t)
wkNatural ρ sucₙ    = sucₙ
wkNatural ρ zeroₙ   = zeroₙ
wkNatural ρ (ne x) = ne (wkNeutral ρ x)

wkType : ∀ {t} ρ → Type t → Type (wk ρ t)
wkType ρ Πₙ      = Πₙ
wkType ρ ℕₙ      = ℕₙ
wkType ρ Uₙ      = Uₙ
wkType ρ ∃ₙ      = ∃ₙ
wkType ρ Emptyₙ  = Emptyₙ
wkType ρ (ne x) = ne (wkNeutral ρ x)

wkFunction : ∀ {t} ρ → Function t → Function (wk ρ t)
wkFunction ρ lamₙ    = lamₙ
wkFunction ρ (ne x) = ne (wkNeutral ρ x)

wkWhnf : ∀ {t} ρ → Whnf t → Whnf (wk ρ t)
wkWhnf ρ Uₙ      = Uₙ
wkWhnf ρ Πₙ      = Πₙ
wkWhnf ρ ∃ₙ      = ∃ₙ
wkWhnf ρ ℕₙ      = ℕₙ
wkWhnf ρ Emptyₙ  = Emptyₙ
wkWhnf ρ lamₙ    = lamₙ
wkWhnf ρ zeroₙ   = zeroₙ
wkWhnf ρ sucₙ    = sucₙ
wkWhnf ρ (ne x) = ne (wkNeutral ρ x)

-- Non-dependent version of Π.

_^_°_▹▹_°_°_ : Term → Relevance → Level → Term → Level → Level → Term
A ^ r ° lA ▹▹ B ° lB ° l = Π A ^ r ° lA ▹ wk1 B ° lB ° l

-- Non-dependent version of ∃.

_××_ : Term → Term → Term
A ×× B = ∃ A ▹ wk1 B

------------------------------------------------------------------------
-- Substitution

-- The substitution operation  subst σ t  replaces the free de Bruijn indices
-- of term t by chosen terms as specified by σ.

-- The substitution σ itself is a map from natural numbers to terms.

Subst : Set
Subst = Nat → Term

-- Given closed contexts ⊢ Γ and ⊢ Δ,
-- substitutions may be typed via Γ ⊢ σ : Δ meaning that
-- Γ ⊢ σ(x) : (subst σ Δ)(x) for all x ∈ dom(Δ).
--
-- The substitution operation is then typed as follows:
-- If Γ ⊢ σ : Δ and Δ ⊢ t : A, then Γ ⊢ subst σ t : subst σ A.
--
-- Although substitutions are untyped, typing helps us
-- to understand the operation on substitutions.

-- We may view σ as the infinite stream σ 0, σ 1, ...

-- Extract the substitution of the first variable.
--
-- If Γ ⊢ σ : Δ∙A  then Γ ⊢ head σ : subst σ A.

head : Subst → Term
head σ = σ 0

-- Remove the first variable instance of a substitution
-- and shift the rest to accommodate.
--
-- If Γ ⊢ σ : Δ∙A then Γ ⊢ tail σ : Δ.

tail : Subst → Subst
tail σ n = σ (1+ n)

-- Substitution of a variable.
--
-- If Γ ⊢ σ : Δ then Γ ⊢ substVar σ x : (subst σ Δ)(x).

substVar : (σ : Subst) (x : Nat) → Term
substVar σ x = σ x

-- Identity substitution.
-- Replaces each variable by itself.
--
-- Γ ⊢ idSubst : Γ.

idSubst : Subst
idSubst = var

-- Weaken a substitution by one.
--
-- If Γ ⊢ σ : Δ then Γ∙A ⊢ wk1Subst σ : Δ.

wk1Subst : Subst → Subst
wk1Subst σ x = wk1 (σ x)

-- Lift a substitution.
--
-- If Γ ⊢ σ : Δ then Γ∙A ⊢ liftSubst σ : Δ∙A.

liftSubst : (σ : Subst) → Subst
liftSubst σ 0    = var 0
liftSubst σ (1+ x) = wk1Subst σ x

-- Transform a weakening into a substitution.
--
-- If ρ : Γ ≤ Δ then Γ ⊢ toSubst ρ : Δ.

toSubst : Wk → Subst
toSubst pr x = var (wkVar pr x)

-- Apply a substitution to a term.
--
-- If Γ ⊢ σ : Δ and Δ ⊢ t : A then Γ ⊢ subst σ t : subst σ A.

mutual
  substGen : (σ : Subst) (g : List (GenT Term)) → List (GenT Term)
  substGen σ [] = []
  substGen σ (⟦ l , t ⟧ ∷ g) = ⟦ l , (subst (repeat liftSubst σ l) t) ⟧ ∷ substGen σ g

  subst : (σ : Subst) (t : Term) → Term
  subst σ (var x) = substVar σ x
  subst σ (gen x c) = gen x (substGen σ c)

-- Extend a substitution by adding a term as
-- the first variable substitution and shift the rest.
--
-- If Γ ⊢ σ : Δ and Γ ⊢ t : subst σ A then Γ ⊢ consSubst σ t : Δ∙A.

consSubst : Subst → Term → Subst
consSubst σ t 0    = t
consSubst σ t (1+ n) = σ n

-- Singleton substitution.
--
-- If Γ ⊢ t : A then Γ ⊢ sgSubst t : Γ∙A.

sgSubst : Term → Subst
sgSubst = consSubst idSubst

-- Compose two substitutions.
--
-- If Γ ⊢ σ : Δ and Δ ⊢ σ′ : Φ then Γ ⊢ σ ₛ•ₛ σ′ : Φ.

_ₛ•ₛ_ : Subst → Subst → Subst
_ₛ•ₛ_ σ σ′ x = subst σ (σ′ x)

-- Composition of weakening and substitution.
--
--  If ρ : Γ ≤ Δ and Δ ⊢ σ : Φ then Γ ⊢ ρ •ₛ σ : Φ.

_•ₛ_ : Wk → Subst → Subst
_•ₛ_ ρ σ x = wk ρ (σ x)

--  If Γ ⊢ σ : Δ and ρ : Δ ≤ Φ then Γ ⊢ σ ₛ• ρ : Φ.

_ₛ•_ : Subst → Wk → Subst
_ₛ•_ σ ρ x = σ (wkVar ρ x)

-- Substitute the first variable of a term with an other term.
--
-- If Γ∙A ⊢ t : B and Γ ⊢ s : A then Γ ⊢ t[s] : B[s].

_[_] : (t : Term) (s : Term) → Term
t [ s ] = subst (sgSubst s) t

-- Substitute the first variable of a term with an other term,
-- but let the two terms share the same context.
--
-- If Γ∙A ⊢ t : B and Γ∙A ⊢ s : A then Γ∙A ⊢ t[s]↑ : B[s]↑.

_[_]↑ : (t : Term) (s : Term) → Term
t [ s ]↑ = subst (consSubst (wk1Subst idSubst) s) t

_[_]↑↑ : (t : Term) (s : Term) → Term
t [ s ]↑↑ = subst (consSubst (wk1Subst (wk1Subst idSubst)) s) t

-- Definition of syntaxic sugar

Unit : ∀ {l} → Term
Unit {l} =  Π Empty l ^ % ° l ▹ Empty l ° l ° l

Idsym : (A x y e : Term) → Term
Idsym A x y e = transp A (Id (wk1 A) (var 0) (wk1 x)) x (Idrefl A x) y e

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

module Data.List.Membership where

open import Data.List
open import Data.Fin
open import Data.Fin.Properties
open import Prelude
open import Relation.Nullary
open import Path.Reasoning
open import Data.List.Relation.Unary as Relation using (module Exists; module Congruence; ◇; ◇!)
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ
open import Data.Maybe.Properties using (just-inj)

module _ {a} {A : Type a} {x : A} where
  open Exists (_≡ x)
    using (push; pull; push!; pull!; here!; _◇++_; _++◇_)
    renaming (◇? to _∈?_)
    public

infixr 5 _∈_ _∈!_ _∉_
_∈_ : A → List A → Type _
x ∈ xs = ◇ (_≡ x) xs

_∉_ : {A : Type a} → A → List A → Type a
x ∉ xs = ¬ (x ∈ xs)

_∈!_ : A → List A → Type _
x ∈! xs = ◇! (_≡ x) xs

cong-∈ : ∀ (f : A → B) {x : A} xs → x ∈ xs → f x ∈ map f xs
cong-∈ f {x} = Congruence.cong-◇ (_≡ x) (_≡ (f x)) (cong f)

fin∈tabulate :  ∀ {n}
                (f : Fin n → A)
                (i : Fin n) →
                f i ∈ tabulate n f
fin∈tabulate {n = suc _} f f0     = f0 , refl
fin∈tabulate {n = suc _} f (fs i)  =
  push (fin∈tabulate (f ∘ fs) i)

open import Function.Injective

at : ∀ {xs : List A} (n : Fin (length xs)) → (xs ! n) ∈ xs
at n = n , refl

module _ {a} {A : Set a} (_≟_ : Discrete A) where
  isSet⟨A⟩ : isSet A
  isSet⟨A⟩ = Discrete→isSet _≟_

  infixl 6 _\\_
  _\\_ : List A → A → List A
  xs \\ x = foldr f [] xs
    where
    f : A → List A → List A
    f y xs with x ≟ y
    ... | yes p = xs
    ... | no  p = y ∷ xs

  uniques : List A → List A
  uniques = foldr f []
    where
    f : A → List A → List A
    f x xs = x ∷ (xs \\ x)

  x∉xs\\x : ∀ x xs → x ∉ xs \\ x
  x∉xs\\x x (y ∷ xs) (n , x∈xs) with x ≟ y
  x∉xs\\x x (y ∷ xs) (n      , x∈xs)  | yes p = x∉xs\\x x xs (n , x∈xs)
  x∉xs\\x x (y ∷ xs) (f0   , y≡x)   | no ¬p = ¬p (sym y≡x)
  x∉xs\\x x (y ∷ xs) (fs n  , x∈xs)  | no ¬p = x∉xs\\x x xs (n , x∈xs)

  x∈!x∷xs\\x : ∀ x xs → x ∈! x ∷ xs \\ x
  x∈!x∷xs\\x x xs = here! (refl , isSet⟨A⟩ _ _ refl) (x∉xs\\x x xs)

  x∉xs⇒x∉xs\\y : ∀ (x : A) y xs → x ∉ xs → x ∉ xs \\ y
  x∉xs⇒x∉xs\\y x y (z ∷ xs) x∉xs x∈xs\\y with y ≟ z
  x∉xs⇒x∉xs\\y x y (z ∷ xs) x∉xs x∈xs\\y | yes p =
    x∉xs⇒x∉xs\\y x y xs (x∉xs ∘ push) x∈xs\\y
  x∉xs⇒x∉xs\\y x y (z ∷ xs) x∉xs (f0  , x∈xs\\y) | no ¬p =
    x∉xs (f0 , x∈xs\\y)
  x∉xs⇒x∉xs\\y x y (z ∷ xs) x∉xs (fs n , x∈xs\\y) | no ¬p =
    x∉xs⇒x∉xs\\y x y xs (x∉xs ∘ push) (n , x∈xs\\y)

  x∈!xs⇒x∈!xs\\y : ∀ (x : A) y xs → y ≢ x → x ∈! xs → x ∈! xs \\ y
  x∈!xs⇒x∈!xs\\y x y (z ∷ xs) y≢x x∈!xs with y ≟ z
  x∈!xs⇒x∈!xs\\y x y (z ∷ xs) y≢x x∈!xs | yes p =
    x∈!xs⇒x∈!xs\\y x y xs y≢x (pull! (y≢x ∘ p ;_) x∈!xs)
  x∈!xs⇒x∈!xs\\y x y (z ∷ xs) y≢x ((f0  , x∈xs) , uniq) | no ¬p =
    here! (x∈xs , isSet⟨A⟩ _ _ _) (x∉xs⇒x∉xs\\y x y xs (ℕ.znots ∘ cong FinToℕ ∘ cong fst ∘ uniq ∘ push))
  x∈!xs⇒x∈!xs\\y x y (z ∷ xs) y≢x ((fs n , x∈xs) , uniq) | no ¬p =
    push! z≢x (x∈!xs⇒x∈!xs\\y x y xs y≢x (pull! z≢x ((fs n , x∈xs) , uniq)))
    where z≢x = ℕ.snotz ∘ cong FinToℕ ∘ cong fst ∘ uniq ∘ (f0 ,_)

  ∈⇒∈! : (x : A) (xs : List A) → x ∈ xs → x ∈! uniques xs
  ∈⇒∈! x (y ∷ xs) (f0  , x∈xs) =
    subst (_∈! (y ∷ uniques xs \\ y)) x∈xs (x∈!x∷xs\\x y (uniques xs))
  ∈⇒∈! x (y ∷ xs) (fs n , x∈xs) with y ≟ x
  ... | yes p = subst (_∈! (y ∷ uniques xs \\ y)) p (x∈!x∷xs\\x y (uniques xs))
  ... | no ¬p = push! ¬p (x∈!xs⇒x∈!xs\\y x y (uniques xs) ¬p (∈⇒∈! x xs (n , x∈xs)))

infixr 5 _∈²_
_∈²_ : A → List (List A) → Type _
x ∈² xs = ◇ (x ∈_) xs

∈²→∈ : ∀ {x : A} xs → x ∈² xs → x ∈ concat xs
∈²→∈ = Relation.◇-concat (_≡ _)

ext: agda

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

open import Categories.Category
open import Categories.Category.Monoidal

module Experiment.Categories.Category.Monoidal.Coherence
  {o ℓ e} {𝒞 : Category o ℓ e} (M : Monoidal 𝒞) where

open import Level
open import Data.Product using (Σ)

open import Categories.Morphism 𝒞
open import Categories.Functor

open Category 𝒞
open Monoidal M

𝒞′ : Category (o ⊔ ℓ ⊔ e) (ℓ ⊔ o) e
𝒞′ = categoryHelper record
  { Obj       = Σ (Endofunctor 𝒞) λ E →
     ∀ {A B} → Functor.F₀ E A ⊗₀ B ≅ Functor.F₀ E (A ⊗₀ B)
     -- TODO and more coherence
  ; _⇒_       = {!   !}
  ; _≈_       = {!   !}
  ; id        = {!   !}
  ; _∘_       = {!   !}
  ; assoc     = {!   !}
  ; identityˡ = {!   !}
  ; identityʳ = {!   !}
  ; equiv     = {!   !}
  ; ∘-resp-≈  = {!   !}
  }


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

{-

This file defines

sucPred : ∀ (i : Int) → sucInt (predInt i) ≡ i
predSuc : ∀ (i : Int) → predInt (sucInt i) ≡ i

discreteInt : discrete Int
isSetInt : isSet Int

addition of Int is defined _+_ : Int → Int → Int

as well as its commutativity and associativity
+-comm : ∀ (m n : Int) → m + n ≡ n + m
+-assoc : ∀ (m n o : Int) → m + (n + o) ≡ (m + n) + o

An alternate definition of _+_ is defined via ua,
namely _+'_, which helps us to easily prove

isEquivAddInt : (m : Int) → isEquiv (λ n → n + m)

-}

module Cubical.Data.Int.Properties where

open import Cubical.Core.Everything

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

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit renaming (Unit to ⊤)
open import Cubical.Data.Nat as ℕ using (ℕ; zero; suc; discreteℕ) renaming
  ( _·_ to _·ⁿ_
  ; _+_ to _+ⁿ_
  ; _⊓_ to _⊓ⁿ_
  ; _⊔_ to _⊔ⁿ_
  )
open import Cubical.Data.Nat.Order as ℕᵒ using () renaming ( _<_ to _<ⁿ_ )
open import Cubical.Data.Bool hiding (_≟_)
open import Cubical.Data.Sum
open import Cubical.Data.Int.Base
open import Cubical.Functions.Logic using (pathTo⇒; ⊔-comm)
open import Cubical.HITs.PropositionalTruncation as PropTrunc using (propTruncIsProp)
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Reflection.Base using (_$_) -- TODO: add this to Foundation.Function

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

abs : Int → ℕ
abs (pos n) = n
abs (negsuc n) = suc n

Sign : Type₀
Sign = Bool

pattern spos = Bool.false
pattern sneg = Bool.true

_·ˢ_ : Sign → Sign → Sign
_·ˢ_ = _⊕_

sgn : Int → Bool
sgn (pos    n) = spos
sgn (negsuc n) = sneg

signed : Sign → ℕ → Int
signed spos      x  = pos x
signed sneg  zero   = pos 0
signed sneg (suc x) = neg (suc x)

sgn-signed : ∀ s n → sgn (signed s (suc n)) ≡ s
sgn-signed spos n = refl
sgn-signed sneg n = refl

abs-signed : ∀ s n → abs (signed s n) ≡ n
abs-signed spos      n  = refl
abs-signed sneg  zero   = refl
abs-signed sneg (suc n) = refl

signed-inv : ∀ a → signed (sgn a) (abs a) ≡ a
signed-inv (pos    n) = refl
signed-inv (negsuc n) = refl

signed-zero : ∀ s → signed s 0 ≡ 0
signed-zero spos = refl
signed-zero sneg = refl

signed-reflects-sgn : ∀ s₁ s₂ n m → signed s₁ (suc n) ≡ signed s₂ (suc m) → s₁ ≡ s₂
signed-reflects-sgn s₁ s₂ n m p = sym (sgn-signed s₁ n) ∙ (λ i → sgn (p i)) ∙ sgn-signed s₂ m

signed-reflects-abs : ∀ s₁ s₂ n m → signed s₁ n ≡ signed s₂ m → n ≡ m
signed-reflects-abs s₁ s₂ n m p = sym (abs-signed s₁ n) ∙ (λ i → abs (p i)) ∙ abs-signed s₂ m

sign-abs-≡ : ∀ a b → sgn a ≡ sgn b → abs a ≡ abs b → a ≡ b
sign-abs-≡ a b p q = transport (λ i → signed-inv a i ≡ signed-inv b i) λ i → signed (p i) (q i)

sucPred : ∀ i → sucInt (predInt i) ≡ i
sucPred (pos zero)    = refl
sucPred (pos (suc n)) = refl
sucPred (negsuc n)    = refl

predSuc : ∀ i → predInt (sucInt i) ≡ i
predSuc (pos n)          = refl
predSuc (negsuc zero)    = refl
predSuc (negsuc (suc n)) = refl

predInt-inj : ∀ a b → predInt a ≡ predInt b → a ≡ b
predInt-inj a b p = sym (sucPred a) ∙ cong sucInt p ∙ sucPred b

injPos : ∀ {a b : ℕ} → pos a ≡ pos b → a ≡ b
injPos {a} h = subst T h refl
  where
  T : Int → Type₀
  T (pos x)    = a ≡ x
  T (negsuc _) = ⊥

injNegsuc : ∀ {a b : ℕ} → negsuc a ≡ negsuc b → a ≡ b
injNegsuc {a} h = subst T h refl
  where
  T : Int → Type₀
  T (pos _) = ⊥
  T (negsuc x) = a ≡ x

posNotnegsuc : ∀ (a b : ℕ) → ¬ (pos a ≡ negsuc b)
posNotnegsuc a b h = subst T h 0
  where
  T : Int → Type₀
  T (pos _)    = ℕ
  T (negsuc _) = ⊥

negsucNotpos : ∀ (a b : ℕ) → ¬ (negsuc a ≡ pos b)
negsucNotpos a b h = subst T h 0
  where
  T : Int → Type₀
  T (pos _)    = ⊥
  T (negsuc _) = ℕ

discreteInt : Discrete Int
discreteInt (pos n) (pos m) with discreteℕ n m
... | yes p = yes (cong pos p)
... | no p  = no (λ x → p (injPos x))
discreteInt (pos n) (negsuc m) = no (posNotnegsuc n m)
discreteInt (negsuc n) (pos m) = no (negsucNotpos n m)
discreteInt (negsuc n) (negsuc m) with discreteℕ n m
... | yes p = yes (cong negsuc p)
... | no p  = no (λ x → p (injNegsuc x))

isSetInt : isSet Int
isSetInt = Discrete→isSet discreteInt

_ℕ-_ : ℕ → ℕ → Int
a ℕ- 0 = pos a
0 ℕ- suc b = negsuc b
suc a ℕ- suc b = a ℕ- b

_+pos_ : Int → ℕ  → Int
z +pos 0 = z
z +pos (suc n) = sucInt (z +pos n)

_+negsuc_ : Int → ℕ → Int
z +negsuc 0 = predInt z
z +negsuc (suc n) = predInt (z +negsuc n)

infix  8 -_
infixl 7 _·_ _⊓_
infixl 6 _+_ _-_ _⊔_
infix  4 _<_ -- _≤_

_+_ : Int → Int → Int
m + pos n = m +pos n
m + negsuc n = m +negsuc n

-- TODO: in `Cubical.Papers.RepresentationIndependence` we have
--   -_ : ℤ → ℤ
--   - x = 0 - x
-- there might be an advantage of defining -_ by _-_ and not the other way around
-- e.g. in Cubical.HITs.QuoInt we have
--   -_ : ℤ → ℤ
--   - signed s n = signed (not s) n
--   - posneg i   = posneg (~ i)

-_ : Int → Int
- pos  zero   = pos zero
- pos (suc n) = negsuc n
- negsuc   n  = pos (suc n)

_-_ : Int → Int → Int
m - n = m + (- n)

_·_ : Int → Int → Int
x · y  = signed (sgn x ⊕ sgn y) (abs x ·ⁿ abs y)

_<_ : ∀(x y : Int) → Type₀
pos    x < pos    y = x <ⁿ y
pos    x < negsuc y = ⊥
negsuc x < pos    y = ⊤
negsuc x < negsuc y = y <ⁿ x

_⊓_ : Int → Int → Int
(pos    x) ⊓ (pos    y) = pos (x ⊓ⁿ y)
(pos    x) ⊓ (negsuc y) = negsuc y
(negsuc x) ⊓ (pos    y) = negsuc x
(negsuc x) ⊓ (negsuc y) = negsuc (x ⊔ⁿ y)

_⊔_ : Int → Int → Int
(pos    x) ⊔ (pos    y) = pos (x ⊔ⁿ y)
(pos    x) ⊔ (negsuc y) = pos x
(negsuc x) ⊔ (pos    y) = pos y
(negsuc x) ⊔ (negsuc y) = negsuc (x ⊓ⁿ y)

neg-involutive : ∀ n → - - n ≡ n
neg-involutive (pos  zero  ) = refl
neg-involutive (pos (suc n)) = refl
neg-involutive (negsuc   n ) = refl

neg-signed-not : ∀ s n → - signed s n ≡ signed (not s) n
neg-signed-not spos  zero   = refl
neg-signed-not sneg  zero   = refl
neg-signed-not spos (suc n) = refl
neg-signed-not sneg (suc n) = refl

neg-abs : ∀ a → abs (- a) ≡ abs a
neg-abs (pos zero) = refl
neg-abs (pos (suc n)) = refl
neg-abs (negsuc n) = refl

neg-reflects-≡ : ∀ a b → - a ≡ - b → a ≡ b
neg-reflects-≡ a b p = sym (neg-involutive a) ∙ (λ i → - p i) ∙ neg-involutive b

abs-preserves-· : ∀ a b → abs (a · b) ≡ abs a ℕ.· abs b
abs-preserves-· a b = abs-signed (sgn a ⊕ sgn b) _

sucInt+pos : ∀ n m → sucInt (m +pos n) ≡ (sucInt m) +pos n
sucInt+pos zero m = refl
sucInt+pos (suc n) m = cong sucInt (sucInt+pos n m)

predInt+negsuc : ∀ n m → predInt (m +negsuc n) ≡ (predInt m) +negsuc n
predInt+negsuc zero m = refl
predInt+negsuc (suc n) m = cong predInt (predInt+negsuc n m)

sucInt+negsuc : ∀ n m → sucInt (m +negsuc n) ≡ (sucInt m) +negsuc n
sucInt+negsuc zero m = (sucPred _) ∙ (sym (predSuc _))
sucInt+negsuc (suc n) m =      _ ≡⟨ sucPred _ ⟩
  m +negsuc n                    ≡[ i ]⟨ predSuc m (~ i) +negsuc n ⟩
  (predInt (sucInt m)) +negsuc n ≡⟨ sym (predInt+negsuc n (sucInt m)) ⟩
  predInt (sucInt m +negsuc n) ∎

predInt+pos : ∀ n m → predInt (m +pos n) ≡ (predInt m) +pos n
predInt+pos zero m = refl
predInt+pos (suc n) m =     _ ≡⟨ predSuc _ ⟩
  m +pos n                    ≡[ i ]⟨ sucPred m (~ i) + pos n ⟩
  (sucInt (predInt m)) +pos n ≡⟨ sym (sucInt+pos n (predInt m))⟩
  (predInt m) +pos (suc n)    ∎

predInt+ : ∀ m n → predInt (m + n) ≡ (predInt m) + n
predInt+ m (pos n) = predInt+pos n m
predInt+ m (negsuc n) = predInt+negsuc n m

+predInt : ∀ m n → predInt (m + n) ≡ m + (predInt n)
+predInt m (pos zero) = refl
+predInt m (pos (suc n)) = (predSuc (m + pos n)) ∙ (cong (_+_ m) (sym (predSuc (pos n))))
+predInt m (negsuc n) = refl

sucInt+ : ∀ m n → sucInt (m + n) ≡ (sucInt m) + n
sucInt+ m (pos n) = sucInt+pos n m
sucInt+ m (negsuc n) = sucInt+negsuc n m

+sucInt : ∀ m n → sucInt (m + n) ≡  m + (sucInt n)
+sucInt m (pos n) = refl
+sucInt m (negsuc zero) = sucPred _
+sucInt m (negsuc (suc n)) = (sucPred (m +negsuc n)) ∙ (cong (_+_ m) (sym (sucPred (negsuc n))))

pos0+ : ∀ z → z ≡ pos 0 + z
pos0+ (pos zero) = refl
pos0+ (pos (suc n)) = cong sucInt (pos0+ (pos n))
pos0+ (negsuc zero) = refl
pos0+ (negsuc (suc n)) = cong predInt (pos0+ (negsuc n))

negsuc0+ : ∀ z → predInt z ≡ negsuc 0 + z
negsuc0+ (pos zero) = refl
negsuc0+ (pos (suc n)) = (sym (sucPred (pos n))) ∙ (cong sucInt (negsuc0+ _))
negsuc0+ (negsuc zero) = refl
negsuc0+ (negsuc (suc n)) = cong predInt (negsuc0+ (negsuc n))

ind-comm : {A : Type₀} (_∙_ : A → A → A) (f : ℕ → A) (g : A → A)
           (p : ∀ {n} → f (suc n) ≡ g (f n))
           (g∙ : ∀ a b → g (a ∙ b) ≡ g a ∙ b)
           (∙g : ∀ a b → g (a ∙ b) ≡ a ∙ g b)
           (base : ∀ z → z ∙ f 0 ≡ f 0 ∙ z)
         → ∀ z n → z ∙ f n ≡ f n ∙ z
ind-comm _∙_ f g p g∙ ∙g base z 0 = base z
ind-comm _∙_ f g p g∙ ∙g base z (suc n) =
  z ∙ f (suc n) ≡[ i ]⟨ z ∙ p {n} i ⟩
  z ∙ g (f n)   ≡⟨ sym ( ∙g z (f n)) ⟩
  g (z ∙ f n)   ≡⟨ cong g IH ⟩
  g (f n ∙ z)   ≡⟨ g∙ (f n) z ⟩
  g (f n) ∙ z   ≡[ i ]⟨ p {n} (~ i) ∙ z ⟩
  f (suc n) ∙ z ∎
  where
  IH = ind-comm _∙_ f g p g∙ ∙g base z n

ind-assoc : {A : Type₀} (_·_ : A → A → A) (f : ℕ → A)
        (g : A → A) (p : ∀ a b → g (a · b) ≡ a · (g b))
        (q : ∀ {c} → f (suc c) ≡ g (f c))
        (base : ∀ m n → (m · n) · (f 0) ≡ m · (n · (f 0)))
        (m n : A) (o : ℕ)
      → m · (n · (f o)) ≡ (m · n) · (f o)
ind-assoc _·_ f g p q base m n 0 = sym (base m n)
ind-assoc _·_ f g p q base m n (suc o) =
    m · (n · (f (suc o))) ≡[ i ]⟨ m · (n · q {o} i) ⟩
    m · (n · (g (f o)))   ≡[ i ]⟨ m · (p n (f o) (~ i)) ⟩
    m · (g (n · (f o)))   ≡⟨ sym (p m (n · (f o)))⟩
    g (m · (n · (f o)))   ≡⟨ cong g IH ⟩
    g ((m · n) · (f o))   ≡⟨ p (m · n) (f o) ⟩
    (m · n) · (g (f o))   ≡[ i ]⟨ (m · n) · q {o} (~ i) ⟩
    (m · n) · (f (suc o)) ∎
    where
    IH = ind-assoc _·_ f g p q base m n o

+-comm : ∀ m n → m + n ≡ n + m
+-comm m (pos n) = ind-comm _+_ pos sucInt refl sucInt+ +sucInt pos0+ m n
+-comm m (negsuc n) = ind-comm _+_ negsuc predInt refl predInt+ +predInt negsuc0+ m n

+-assoc : ∀ m n o → m + (n + o) ≡ (m + n) + o
+-assoc m n (pos o) = ind-assoc _+_ pos sucInt +sucInt refl (λ _ _ → refl) m n o
+-assoc m n (negsuc o) = ind-assoc _+_ negsuc predInt +predInt refl +predInt m n o

·-nullifiesʳ : ∀ x → x · 0 ≡ 0
·-nullifiesʳ (pos    n) i = signed spos (ℕ.·-nullifiesʳ n i)
·-nullifiesʳ (negsuc n) i = signed sneg (ℕ.·-nullifiesʳ n i)

·-nullifiesˡ : ∀ x → 0 · x ≡ 0
·-nullifiesˡ (pos    n) i = pos (ℕ.·-nullifiesˡ n i)
·-nullifiesˡ (negsuc n)   = refl

+-identityʳ : ∀ x → x + 0 ≡ x
+-identityʳ x = refl

+-identityˡ : ∀ x → 0 + x ≡ x
+-identityˡ x = +-comm 0 x

·-identityʳ : ∀ x → x · 1 ≡ x
·-identityʳ x = cong₂ signed (⊕-comm (sgn x) spos) (ℕ.·-identityʳ (abs x)) ∙ signed-inv x

·-identityˡ : ∀ x → 1 · x ≡ x
·-identityˡ x = (λ i → signed (sgn x) (ℕ.+-comm (abs x) 0 i)) ∙ signed-inv x

·-comm : ∀ m n → m · n ≡ n · m
·-comm (pos m) n = cong₂ signed (⊕-comm spos (sgn n)) (ℕ.·-comm m (abs n))
·-comm (negsuc m) n = cong₂ signed (⊕-comm sneg (sgn n)) (ℕ.·-comm (suc m) (abs n))

predInt-neg : ∀ a → predInt (- a) ≡ - (sucInt a)
predInt-neg (pos     zero  ) = refl
predInt-neg (pos    (suc n)) = refl
predInt-neg (negsuc  zero  ) = refl
predInt-neg (negsuc (suc n)) = refl

sucInt-neg : ∀ a → sucInt (- a) ≡ - (predInt a)
sucInt-neg (pos     zero        ) = refl
sucInt-neg (pos    (suc zero)   ) = refl
sucInt-neg (pos    (suc (suc n))) = refl
sucInt-neg (negsuc  zero        ) = refl
sucInt-neg (negsuc (suc n)      ) = refl

private
  lem : ∀ n → -(0 + n) ≡ 0 - n
  lem n i = +-identityˡ (- +-identityˡ n i) (~ i)

negate-+ : ∀ m n → - (m + n) ≡  (- m) + (- n)
negate-+ (pos zero) = lem
negate-+ (pos (suc m)) n = (λ i → - sucInt+ (pos m) n (~ i)) ∙ sym (predInt-neg (pos m + n)) ∙ (λ i → predInt (negate-+ (pos m) n i)) ∙ predInt+ (- pos m) (- n) ∙ λ i → predInt-neg (pos m) i + - n
negate-+ (negsuc zero) n = predInt-inj (- (negsuc zero + n)) (pos 1 + - n) $ predInt-neg (negsuc 0 + n) ∙ (λ i → - sucInt+ (negsuc 0) n i) ∙ lem n ∙ sym (predInt+ (pos 1) (- n))
negate-+ (negsuc (suc m)) n = (λ i → - predInt+ (negsuc m) n (~ i)) ∙ sym (sucInt-neg (negsuc m + n)) ∙ (λ i → sucInt (negate-+ (negsuc m) n i)) ∙ sucInt+ (pos (suc m)) (- n)

negate-·ˡ : ∀ a b → -(a · b) ≡ (- a) · b
negate-·ˡ (pos zero) b = neg-signed-not (sgn b) 0 ∙ signed-zero (not (sgn b)) ∙ sym (signed-zero (sgn b))
negate-·ˡ (pos (suc n)) b = neg-signed-not (sgn b) _
negate-·ˡ (negsuc n) b = neg-signed-not (not (sgn b)) _ ∙ cong₂ signed (notnot (sgn b)) refl

negate-·ʳ : ∀ a b → -(a · b) ≡ a · (- b)
negate-·ʳ a b = (λ i → - ·-comm a b i) ∙ negate-·ˡ b a ∙ ·-comm (- b) a

negsuc+negsuc : ∀ a x → (negsuc a +negsuc x) ≡ negsuc (suc (a +ⁿ x))
negsuc+negsuc a zero = λ i → negsuc $ suc $ ℕ.+-comm 0 a i
negsuc+negsuc a (suc x) = let r = negsuc+negsuc a x in
  predInt (negsuc a +negsuc x)    ≡⟨ (λ i → predInt (r i)) ⟩
  predInt (negsuc (suc (a +ⁿ x))) ≡⟨ refl ⟩
  negsuc (suc (suc (a +ⁿ x)))     ≡⟨ (λ i → negsuc $ suc $ ℕ.+-suc a x (~ i)) ⟩
  negsuc (suc (a +ⁿ suc x))       ∎

signed-distrib : ∀ s m n → signed s (m +ⁿ n) ≡ signed s m + signed s n
signed-distrib s zero n = (sym $ +-identityˡ (signed s n)) ∙ λ i → signed-zero s (~ i) + signed s n
signed-distrib spos (suc m) n = cong sucInt (signed-distrib spos m n) ∙ sucInt+pos n (pos m)
signed-distrib sneg (suc m) zero i = negsuc (ℕ.+-comm m 0 i)
signed-distrib sneg (suc m) (suc n) = (λ i → negsuc (ℕ.+-suc m n i)) ∙  sym (negsuc+negsuc m n)

·-pos-suc : ∀ m n → pos (suc m) · n ≡ n + pos m · n
·-pos-suc m n = signed-distrib (sgn n) (abs n) (m ℕ.· abs n) ∙ λ i → signed-inv n i + signed (sgn n) (m ·ⁿ abs n)

·-negsuc-suc : ∀ m n → negsuc (suc m) · n ≡ - n + negsuc m · n
·-negsuc-suc m n = signed-distrib (not (sgn n)) (abs n) (suc m ℕ.· abs n) ∙ λ i → γ i + negsuc m · n
  where γ = sym (neg-signed-not (sgn n) (abs n)) ∙ cong -_ (signed-inv n)

-- this is a similar proof to the one in Cubical.HITs.QuoInt.Properties
--   but we have less definitional equalities
-- ·-assoc : ∀ m n o → m · (n · o) ≡ m · n · o
-- ·-assoc m n o     with abs m | signed-inv m
-- ... | zero   | pm = {!   !}
-- ... | suc mⁿ | pm with abs n | signed-inv n
-- ... | zero   | pn = (λ i → signed s₁ (γ₁ i)) ∙ signed-zero s₁ ∙ sym (signed-zero s₂) ∙ (λ i → signed s₂ (γ₂ i)) where
--   s₁ = sgn m ⊕ sgn (signed (sgn n ⊕ sgn o) 0)
--   s₂ = sgn (signed (sgn m ⊕ sgn n) (mⁿ ·ⁿ 0)) ⊕ sgn o
--   γ₁ = suc mⁿ ·ⁿ abs (signed (sgn n ⊕ sgn o) 0)        ≡⟨ {!   !} ⟩
--        suc mⁿ ·ⁿ 0                                     ≡⟨ {!   !} ⟩
--        0                                               ∎
--   γ₂ = 0                                               ≡⟨ {!   !} ⟩
--        0 ·ⁿ abs o                                      ≡⟨ {!   !} ⟩
--        (mⁿ ·ⁿ 0) ·ⁿ abs o                              ≡⟨ {!   !} ⟩
--        abs (signed (sgn m ⊕ sgn n) (mⁿ ·ⁿ 0)) ·ⁿ abs o ∎
-- ... | suc nⁿ | pn with abs o | signed-inv o
-- ... | zero   | po = (λ i → signed s₁ (γ₁ i)) ∙ signed-zero s₁ ∙ sym (signed-zero s₂) ∙ (λ i → signed s₂ (γ₂ i)) where
--   s₁ = sgn m ⊕ sgn (signed (sgn n ⊕ sgn o) (nⁿ ·ⁿ zero))
--   s₂ = sgn (signed (sgn m ⊕ sgn n) (suc mⁿ ·ⁿ suc nⁿ)) ⊕ sgn o
--   γ₁ = suc mⁿ ·ⁿ abs (signed (sgn n ⊕ sgn o) (nⁿ ·ⁿ 0)) ≡[ i ]⟨ suc mⁿ ·ⁿ abs-signed (sgn n ⊕ sgn o) (nⁿ ·ⁿ 0) i ⟩
--        suc mⁿ ·ⁿ                             (nⁿ ·ⁿ 0)  ≡[ i ]⟨ suc mⁿ ·ⁿ (ℕ.·-nullifiesʳ nⁿ i) ⟩
--        suc mⁿ ·ⁿ                                    0   ≡⟨ ℕ.·-nullifiesʳ (suc mⁿ) ⟩
--                                                     0 ∎
--   γ₂ = 0 ≡⟨ sym $ ℕ.·-nullifiesʳ (abs (signed (sgn m ⊕ sgn n) (suc mⁿ ·ⁿ suc nⁿ))) ⟩
--        abs (signed (sgn m ⊕ sgn n) (suc mⁿ ·ⁿ suc nⁿ)) ·ⁿ 0 ∎
-- ... | suc oⁿ | po = cong₂ signed γ₁ γ₂ where
--   γ₁ = sgn m ⊕ sgn (signed (sgn n ⊕ sgn o) (suc nⁿ ·ⁿ suc oⁿ)) ≡[ i ]⟨ sgn m ⊕ sgn-signed (sgn n ⊕ sgn o) (oⁿ +ⁿ nⁿ ·ⁿ suc oⁿ) i ⟩
--        sgn m ⊕ (sgn n ⊕ sgn o)                                 ≡⟨ ⊕-assoc (sgn m) (sgn n) (sgn o) ⟩
--        (sgn m ⊕ sgn n) ⊕ sgn o                                 ≡[ i ]⟨ sgn-signed (sgn m ⊕ sgn n) (nⁿ +ⁿ mⁿ ·ⁿ suc nⁿ) (~ i) ⊕ sgn o ⟩
--        sgn (signed (sgn m ⊕ sgn n) (suc mⁿ ·ⁿ suc nⁿ)) ⊕ sgn o ∎
--   γ₂ = suc mⁿ ·ⁿ abs (signed (sgn n ⊕ sgn o) (suc nⁿ ·ⁿ suc oⁿ)) ≡[ i ]⟨ suc mⁿ ·ⁿ abs-signed (sgn n ⊕ sgn o) (suc nⁿ ·ⁿ suc oⁿ) i ⟩
--        suc mⁿ ·ⁿ (suc nⁿ ·ⁿ suc oⁿ)                              ≡⟨ ℕ.·-assoc (suc mⁿ) (suc nⁿ) (suc oⁿ) ⟩
--        (suc mⁿ ·ⁿ suc nⁿ) ·ⁿ suc oⁿ                              ≡[ i ]⟨ abs-signed (sgn m ⊕ sgn n) (suc mⁿ ·ⁿ suc nⁿ) (~ i) ·ⁿ suc oⁿ ⟩
--        abs (signed (sgn m ⊕ sgn n) (suc mⁿ ·ⁿ suc nⁿ)) ·ⁿ suc oⁿ ∎

private
  lemma2 : ∀ a b c →  c +ⁿ (b +ⁿ a ·ⁿ suc b) ·ⁿ suc c
                   ≡ (c +ⁿ b ·ⁿ suc c) +ⁿ a ·ⁿ suc (c +ⁿ b ·ⁿ suc c)
  lemma2 a b c =
    c +ⁿ (b +ⁿ a ·ⁿ suc b) ·ⁿ suc c                 ≡⟨ (λ i → c +ⁿ ℕ.·-distribʳ b (a ·ⁿ suc b) (suc c) (~ i)) ⟩
    c +ⁿ (b ·ⁿ suc c +ⁿ (a ·ⁿ suc b) ·ⁿ suc c)      ≡⟨ ℕ.+-assoc c _ _ ⟩
    (c +ⁿ b ·ⁿ suc c) +ⁿ (a ·ⁿ suc b) ·ⁿ suc c      ≡⟨ (λ i → (c +ⁿ b ·ⁿ suc c) +ⁿ ℕ.·-assoc a (suc b) (suc c) (~ i)) ⟩
    (c +ⁿ b ·ⁿ suc c) +ⁿ a ·ⁿ (suc b ·ⁿ suc c)      ≡⟨ refl ⟩
    (c +ⁿ b ·ⁿ suc c) +ⁿ a ·ⁿ suc (c +ⁿ b ·ⁿ suc c) ∎

-- this is a proof ported from the non-cubical standard library
·-assoc : ∀ x y z → (x · y) · z ≡ x · (y · z)
·-assoc (pos 0) y z = (λ i → ·-nullifiesˡ y i · z) ∙ ·-nullifiesˡ z ∙ sym (·-nullifiesˡ (y · z))
·-assoc x (pos 0) z = (λ i → ·-nullifiesʳ x i · z) ∙ ·-nullifiesˡ z ∙ sym (·-nullifiesʳ x)  ∙ (λ i → x · ·-nullifiesˡ z (~ i))
·-assoc x y (pos 0) = ·-nullifiesʳ (x · y) ∙ sym (·-nullifiesʳ x) ∙ (λ i → x · ·-nullifiesʳ y (~ i))
·-assoc (negsuc   a ) (negsuc   b ) (pos (suc c)) i = (pos (suc (lemma2 a b c i)))
·-assoc (negsuc   a ) (pos (suc b)) (negsuc   c ) i = (pos (suc (lemma2 a b c i)))
·-assoc (pos (suc a)) (pos (suc b)) (pos (suc c)) i = (pos (suc (lemma2 a b c i)))
·-assoc (pos (suc a)) (negsuc   b ) (negsuc   c ) i = (pos (suc (lemma2 a b c i)))
·-assoc (negsuc   a ) (negsuc   b ) (negsuc   c ) i = (negsuc   (lemma2 a b c i) )
·-assoc (negsuc   a ) (pos (suc b)) (pos (suc c)) i = (negsuc   (lemma2 a b c i) )
·-assoc (pos (suc a)) (negsuc   b ) (pos (suc c)) i = (negsuc   (lemma2 a b c i) )
·-assoc (pos (suc a)) (pos (suc b)) (negsuc   c ) i = (negsuc   (lemma2 a b c i) )

-- this is a similar proof to the one in Cubical.HITs.QuoInt.Properties
·-distribˡ-pos : ∀ o m n → (pos o · m) + (pos o · n) ≡ pos o · (m + n)
·-distribˡ-pos zero m n = (λ i → ·-nullifiesˡ m i + ·-nullifiesˡ n i) ∙ sym (·-nullifiesˡ (m + n))
·-distribˡ-pos (suc o) m n =
  pos (suc o) · m + pos (suc o) · n ≡[ i ]⟨ ·-pos-suc o m i + ·-pos-suc o n i ⟩
  m + pos o · m + (n + pos o · n)   ≡⟨ +-assoc (m + pos o · m) n (pos o · n) ⟩
  m + pos o · m + n + pos o · n     ≡[ i ]⟨ +-assoc m (pos o · m) n (~ i) + pos o · n ⟩
  m + (pos o · m + n) + pos o · n   ≡[ i ]⟨ m + +-comm (pos o · m) n i + pos o · n ⟩
  m + (n + pos o · m) + pos o · n   ≡[ i ]⟨ +-assoc m n (pos o · m) i + pos o · n ⟩
  m + n + pos o · m + pos o · n     ≡⟨ sym (+-assoc (m + n) (pos o · m) (pos o · n)) ⟩
  m + n + (pos o · m + pos o · n)   ≡⟨ cong ((m + n) +_) (·-distribˡ-pos o m n) ⟩
  m + n + pos o · (m + n)           ≡⟨ sym (·-pos-suc o (m + n)) ⟩
  pos (suc o) · (m + n) ∎

neg-pos-neg : ∀ x → - pos x ≡ neg x
neg-pos-neg zero = refl
neg-pos-neg (suc x) = refl

·-distribˡ-neg : ∀ o m n → (neg o · m) + (neg o · n) ≡ neg o · (m + n)
·-distribˡ-neg o m n =
     neg o · m  +    neg o · n  ≡[ i ]⟨ neg-pos-neg o (~ i) · m + neg-pos-neg o (~ i) · n ⟩
  -  pos o · m  + -  pos o · n  ≡[ i ]⟨ negate-·ˡ (pos o) m (~ i) + negate-·ˡ (pos o) n (~ i) ⟩
  - (pos o · m) + - (pos o · n) ≡⟨ sym (negate-+ (pos o · m) (pos o · n)) ⟩
  - (pos o · m + pos o · n)     ≡⟨ cong -_ (·-distribˡ-pos o m n) ⟩
  - (pos o · (m + n))           ≡⟨ negate-·ˡ (pos o) (m + n) ⟩
  -  pos o · (m + n)            ≡[ i ]⟨ neg-pos-neg o i · (m + n) ⟩
     neg o · (m + n)            ∎

·-distribˡ : ∀ o m n → (o · m) + (o · n) ≡ o · (m + n)
·-distribˡ (pos    o) m n = ·-distribˡ-pos o m n
·-distribˡ (negsuc o) m n = ·-distribˡ-neg (suc o) m n

·-distribʳ : ∀ m n o → (m · o) + (n · o) ≡ (m + n) · o
·-distribʳ m n o = (λ i → ·-comm m o i + ·-comm n o i) ∙ ·-distribˡ o m n ∙ ·-comm o (m + n)

·-neg1 : ∀ x → -1 · x ≡ - x
·-neg1 x = sym (neg-signed-not (sgn x) (abs x +ⁿ 0)) ∙ (λ i → - signed (sgn x) (ℕ.+-comm (abs x) 0 i)) ∙ cong -_ (signed-inv x)

private
  possuc+negsuc≡0 : ∀ n → (pos (suc n) +negsuc n) ≡ pos 0
  possuc+negsuc≡0 zero = refl
  possuc+negsuc≡0 (suc n) = sym ind ∙ possuc+negsuc≡0 n where
    ind =           pos      (suc n)   +negsuc n  ≡⟨ refl ⟩
           predInt (pos (suc (suc n))) +negsuc n  ≡⟨ sym $ predInt+negsuc n (pos (suc (suc n))) ⟩
           predInt (pos (suc (suc n))  +negsuc n) ∎

  sucInt[negsuc+pos]≡0 : ∀ n → sucInt (negsuc n +pos n) ≡ pos 0
  sucInt[negsuc+pos]≡0 zero = refl
  sucInt[negsuc+pos]≡0 (suc n) = let r = sucInt[negsuc+pos]≡0 n in sym ind ∙ r where
    ind = sucInt (        negsuc n        +pos n ) ≡⟨ refl ⟩
          sucInt (sucInt (negsuc (suc n)) +pos n ) ≡⟨ (λ i → sucInt $ sucInt+pos n (negsuc (suc n)) (~ i)) ⟩
          sucInt (sucInt (negsuc (suc n)  +pos n)) ∎

+-inverseʳ : ∀ a → a + (- a) ≡ 0
+-inverseʳ (pos  zero  ) = refl
+-inverseʳ (pos (suc n)) = possuc+negsuc≡0 n
+-inverseʳ (negsuc   n ) = sucInt[negsuc+pos]≡0 n

+-inverseˡ : ∀ a → (- a) + a ≡ 0
+-inverseˡ a = +-comm (- a) a ∙ +-inverseʳ a

-- Compose sucPathInt with itself n times. Transporting along this
-- will be addition, transporting with it backwards will be subtraction.
-- Use this to define _+'_ for which is easier to prove
-- isEquiv (λ n → n +' m) since _+'_ is defined by transport

sucPathInt : Int ≡ Int
sucPathInt = ua (sucInt , isoToIsEquiv (iso sucInt predInt sucPred predSuc))

addEq : ℕ → Int ≡ Int
addEq zero = refl
addEq (suc n) = (addEq n) ∙ sucPathInt

predPathInt : Int ≡ Int
predPathInt = ua (predInt , isoToIsEquiv (iso predInt sucInt predSuc sucPred))

subEq : ℕ → Int ≡ Int
subEq zero = refl
subEq (suc n) = (subEq n) ∙ predPathInt

_+'_ : Int → Int → Int
m +' pos n    = transport (addEq n) m
m +' negsuc n = transport (subEq (suc n)) m

+'≡+ : _+'_ ≡ _+_
+'≡+ i m (pos zero) = m
+'≡+ i m (pos (suc n)) = sucInt (+'≡+ i m (pos n))
+'≡+ i m (negsuc zero) = predInt m
+'≡+ i m (negsuc (suc n)) = predInt (+'≡+ i m (negsuc n)) --
  -- compPath (λ i → (+'≡+ i (predInt m) (negsuc n))) (sym (predInt+negsuc n m)) i

isEquivAddInt' : (m : Int) → isEquiv (λ n → n +' m)
isEquivAddInt' (pos n)    = isEquivTransport (addEq n)
isEquivAddInt' (negsuc n) = isEquivTransport (subEq (suc n))

isEquivAddInt : (m : Int) → isEquiv (λ n → n + m)
isEquivAddInt = subst (λ add → (m : Int) → isEquiv (λ n → add n m)) +'≡+ isEquivAddInt'

-- below is an alternate proof of isEquivAddInt for comparison
-- We also have two useful lemma here.

minusPlus : ∀ m n → (n - m) + m ≡ n
minusPlus (pos zero) n = refl
minusPlus (pos 1) = sucPred
minusPlus (pos (suc (suc m))) n =
  sucInt ((n +negsuc (suc m)) +pos (suc m)) ≡⟨ sucInt+pos (suc m) _ ⟩
  sucInt (n +negsuc (suc m)) +pos (suc m)   ≡[ i ]⟨ sucPred (n +negsuc m) i +pos (suc m) ⟩
  (n - pos (suc m)) +pos (suc m)            ≡⟨ minusPlus (pos (suc m)) n ⟩
  n ∎
minusPlus (negsuc zero) = predSuc
minusPlus (negsuc (suc m)) n =
  predInt (sucInt (sucInt (n +pos m)) +negsuc m) ≡⟨ predInt+negsuc m _ ⟩
  predInt (sucInt (sucInt (n +pos m))) +negsuc m ≡[ i ]⟨ predSuc (sucInt (n +pos m)) i +negsuc m ⟩
  sucInt (n +pos m) +negsuc m                    ≡⟨ minusPlus (negsuc m) n ⟩
  n ∎

plusMinus : ∀ m n → (n + m) - m ≡ n
plusMinus (pos zero) n = refl
plusMinus (pos (suc m)) = minusPlus (negsuc m)
plusMinus (negsuc m) = minusPlus (pos (suc m))

private
  alternateProof : (m : Int) → isEquiv (λ n → n + m)
  alternateProof m = isoToIsEquiv (iso (λ n → n + m)
                                       (λ n → n - m)
                                       (minusPlus m)
                                       (plusMinus m))

<-irrefl : ∀ a → ¬ (a < a)
<-irrefl (pos  zero  ) = ℕᵒ.<-irrefl 0
<-irrefl (pos (suc n)) = ℕᵒ.<-irrefl (suc n)
<-irrefl (negsuc   n ) = ℕᵒ.<-irrefl n

<-trans : ∀ a b c → a < b → b < c → a < c
<-trans (pos    a) (pos    b) (pos    c) a<b b<c = ℕᵒ.<-trans a<b b<c
<-trans (negsuc a) (pos    b) (pos    c) a<b b<c = tt
<-trans (negsuc a) (negsuc b) (pos    c) a<b b<c = tt
<-trans (negsuc a) (negsuc b) (negsuc c) a<b b<c = ℕᵒ.<-trans b<c a<b

<-asym : ∀ a b → a < b → ¬(b < a)
<-asym a b p q = <-irrefl _ (<-trans _ _ _ p q)

private
  swap-∥⊎∥ : ∀{ℓ ℓ'} (a : Type ℓ) (b : Type ℓ') → ∥ a ⊎ b ∥ → ∥ b ⊎ a ∥
  swap-∥⊎∥ a b = PropTrunc.elim (λ _ → propTruncIsProp) λ{ (inl p) → ∣ inr p ∣ ; (inr p) → ∣ inl p ∣ }

<-cotrans : ∀ a b x → a < b → ∥ (a < x) ⊎ (x < b) ∥
<-cotrans (pos    a) (pos    b) (pos    x) a<b = ℕᵒ.<-cotrans _ _ x a<b
<-cotrans (pos    a) (pos    b) (negsuc x) a<b = ∣ inr tt ∣
<-cotrans (negsuc a) (pos    b) (pos    x) a<b = ∣ inl tt ∣
<-cotrans (negsuc a) (pos    b) (negsuc x) a<b = ∣ inr tt ∣
<-cotrans (negsuc a) (negsuc b) (pos    x) a<b = ∣ inl tt ∣
<-cotrans (negsuc a) (negsuc b) (negsuc x) a<b = swap-∥⊎∥ _ _ (ℕᵒ.<-cotrans _ _ x a<b)

data Trichotomy (m n : Int) : Type₀ where
  lt : m < n → Trichotomy m n
  eq : m ≡ n → Trichotomy m n
  gt : n < m → Trichotomy m n

_≟_ : ∀ m n → Trichotomy m n
pos    a ≟ pos    b with a ℕᵒ.≟ b
... | ℕᵒ.lt p = lt p
... | ℕᵒ.eq p = eq λ i → pos (p i)
... | ℕᵒ.gt p = gt p
pos    a ≟ negsuc b = gt tt
negsuc a ≟ pos    b = lt tt
negsuc a ≟ negsuc b with a ℕᵒ.≟ b
... | ℕᵒ.lt p = gt p
... | ℕᵒ.eq p = eq λ i → negsuc (p i)
... | ℕᵒ.gt p = lt p

sucInt-reflects-< : ∀ x y → sucInt x < sucInt y → x < y
sucInt-reflects-< (pos         x ) (pos         y ) p = ℕᵒ.suc-reflects-< x y p
sucInt-reflects-< (pos         x ) (negsuc  zero  ) p = ℕᵒ.¬-<-zero p
sucInt-reflects-< (negsuc      x ) (pos         y ) p = tt
sucInt-reflects-< (negsuc  zero  ) (negsuc  zero  ) p = p
sucInt-reflects-< (negsuc (suc x)) (negsuc  zero  ) p = ℕᵒ.zero-<-suc x
sucInt-reflects-< (negsuc (suc x)) (negsuc (suc y)) p = ℕᵒ.suc-preserves-< y x p

predInt-reflects-< : ∀ x y → predInt x < predInt y → x < y
predInt-reflects-< (pos  zero  ) (pos  zero  ) p = p
predInt-reflects-< (pos  zero  ) (pos (suc y)) p = ℕᵒ.zero-<-suc y
predInt-reflects-< (pos (suc x)) (pos (suc y)) p = ℕᵒ.suc-preserves-< x y p
predInt-reflects-< (pos  zero  ) (negsuc   y ) p = ℕᵒ.¬-<-zero p
predInt-reflects-< (negsuc   x ) (pos      y ) p = tt
predInt-reflects-< (negsuc   x ) (negsuc   y ) p = ℕᵒ.suc-reflects-< y x p

sucInt-preserves-< : ∀ x y → x < y → sucInt x < sucInt y
sucInt-preserves-< (pos         x ) (pos         y ) p = ℕᵒ.suc-preserves-< x y p
sucInt-preserves-< (negsuc  zero  ) (pos         y ) p = ℕᵒ.zero-<-suc y
sucInt-preserves-< (negsuc (suc x)) (pos         y ) p = tt
sucInt-preserves-< (negsuc  zero  ) (negsuc  zero  ) p = p
sucInt-preserves-< (negsuc  zero  ) (negsuc (suc y)) p = ℕᵒ.¬-<-zero p
sucInt-preserves-< (negsuc (suc x)) (negsuc  zero  ) p = tt
sucInt-preserves-< (negsuc (suc x)) (negsuc (suc y)) p = ℕᵒ.suc-reflects-< y x p

predInt-preserves-< : ∀ x y → x < y → predInt x < predInt y
predInt-preserves-< (pos  zero  ) (pos  zero  ) p = p
predInt-preserves-< (pos  zero  ) (pos (suc y)) p = tt
predInt-preserves-< (pos (suc x)) (pos  zero  ) p = ℕᵒ.¬-<-zero p
predInt-preserves-< (pos (suc x)) (pos (suc y)) p = ℕᵒ.suc-reflects-< x y p
predInt-preserves-< (negsuc   x ) (pos  zero  ) p = ℕᵒ.zero-<-suc x
predInt-preserves-< (negsuc   x ) (pos (suc y)) p = tt
predInt-preserves-< (negsuc   x ) (negsuc   y ) p = ℕᵒ.suc-preserves-< y x p

+-preserves-<ʳ : ∀ a b x → a < b → (a + x) < (b + x)
+-preserves-<ʳ a b (pos     zero  ) a<b = a<b
+-preserves-<ʳ a b (pos    (suc n)) a<b =  sucInt-preserves-< (a +pos n) (b +pos n) (+-preserves-<ʳ a b (pos n) a<b)
+-preserves-<ʳ a b (negsuc  zero  ) a<b = predInt-preserves-< a b a<b
+-preserves-<ʳ a b (negsuc (suc n)) a<b = predInt-preserves-< (a +negsuc n) (b +negsuc n) (+-preserves-<ʳ a b (negsuc n) a<b)

+-reflects-<ʳ : ∀ a b x → (a + x) < (b + x) → a < b
+-reflects-<ʳ a b x =
  a +  x      < b +  x      →⟨ +-preserves-<ʳ (a + x) (b + x) (- x) ⟩
  a +  x - x  < b +  x - x  →⟨ transp (λ i → +-assoc a x (- x) (~ i) < +-assoc b x (- x) (~ i)) i0 ⟩
  a + (x - x) < b + (x - x) →⟨ transp (λ i → (a + +-inverseʳ x i) < (b + +-inverseʳ x i)) i0 ⟩
  a +  0      < b +  0      →⟨⟩
  a           < b           ◼

+-reflects-<ˡ : ∀ a b x → (x + a) < (x + b) → a < b
+-reflects-<ˡ a b x p = +-reflects-<ʳ a b x (transport (λ i → +-comm x a i < +-comm x b i) p)

+-<-extensional : ∀ w x y z → (w + x) < (y + z) → ∥ (w < y) ⊎ (x < z) ∥
+-<-extensional w x y z r with w ≟ y | x ≟ z
... | lt w<y | q = ∣ inl w<y ∣
... | eq w≡y | q = ∣ inr $ +-reflects-<ˡ x z y (transport (λ i → (w≡y i + x) < (y + z)) r) ∣
... | gt y<w | q = PropTrunc.elim (λ _ → propTruncIsProp) γ (<-cotrans (w + x) (y + z) (y + x) r)
  where γ : _ ⊎ _ → _
        γ (inl p) = ∣ inr (⊥.elim {A = λ _ → x < z} (<-asym y w y<w (+-reflects-<ʳ w y x p))) ∣
        γ (inr p) = ∣ inr (+-reflects-<ˡ x z y p) ∣

max_stars_repo_name: mchristianl/cubical

max_issues_repo_name: mchristianl/cubical

max_forks_repo_name: mchristianl/cubical


text:
module UniDB.Examples.Lc where

open import UniDB

data Tm (γ : Dom) : Set where
  var : (i : Ix γ) → Tm γ
  abs : (t : Tm (suc γ)) → Tm γ
  app : (t₁ t₂ : Tm γ) → Tm γ

instance
  iVrTm : Vr Tm
  vr     {{iVrTm}}      = var
  vr-inj {{iVrTm}} refl = refl

  iApTm : Ap Tm Tm
  ap {{iApTm}} ξ (var i)    = lk ξ i
  ap {{iApTm}} ξ (abs t)    = abs (ap {Tm} (ξ ↑₁) t )
  ap {{iApTm}} ξ (app t t₁) = app (ap {Tm} ξ t) (ap {Tm} ξ t₁)

  iApVrTm : ApVr Tm
  ap-vr {{iApVrTm}} ξ i = refl

  iApIdmTm : ApIdm Tm Tm
  ap-idm {{iApIdmTm}} {Ξ} (var i)    = lk-idm {Tm} {Ξ} i
  ap-idm {{iApIdmTm}} {Ξ} (abs t)    = cong abs (begin
    ap {Tm} (idm {Ξ} _ ↑₁) t  ≡⟨ cong₂ (ap {Tm}) (idm-↑₁ {Ξ}) (refl {x = t}) ⟩
    ap {Tm} (idm {Ξ} _) t     ≡⟨ ap-idm {Tm} t ⟩
    t                         ∎)
  ap-idm {{iApIdmTm}} {Ξ} (app t t₁) =
    cong₂ app (ap-idm {Tm} t) (ap-idm {Tm} t₁)

  iApPairTm : ApPair Tm Tm
  ap-pair {{iApPairTm}} ξ ζ (var i)     = refl
  ap-pair {{iApPairTm}} ξ ζ (abs x)     = cong abs (ap-pair {Tm} (ξ ↑₁) (ζ ↑₁) x)
  ap-pair {{iApPairTm}} ξ ζ (app x₁ x₂) = cong₂ app (ap-pair {Tm} ξ ζ x₁) (ap-pair {Tm} ξ ζ x₂)

  iApRelTm : ApRel Tm Tm
  ap-rel≅ {{iApRelTm}} hyp (var i)     = lk≃ (≅-to-≃ hyp) i
  ap-rel≅ {{iApRelTm}} hyp (abs t)     = cong abs (ap-rel≅ {Tm} {Tm} (≅-↑₁ hyp) t)
  ap-rel≅ {{iApRelTm}} hyp (app t₁ t₂) = cong₂ app (ap-rel≅ {Tm} {Tm} hyp t₁) (ap-rel≅ {Tm} {Tm} hyp t₂)

postulate
  Ρ : MOR
  instance
    iIdmΡ : Idm Ρ
    iWkmΡ : Wkm Ρ
    iUpΡ : Up Ρ
    iUpIdmΡ : UpIdm Ρ
    iCompΡ : Comp Ρ
    iWkmHomΡ : WkmHom Ρ
    iLkΡ : {T : STX} {{vrT : Vr T}} → Lk T Ρ
    iLkIdmΡ : {T : STX} {{vrT : Vr T}} → LkIdm T Ρ
    iLkWkmΡ : {T : STX} {{vrT : Vr T}} → LkWkm T Ρ
    iLkCompAp : {T : STX} {{vrT : Vr T}} {{apTT : Ap T T}} {{apVrT : ApVr T}} → LkCompAp T Ρ
    iLkUpΡ : {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} → LkUp T Ρ
    iLkRenΡ : {T : STX} {{vrT : Vr T}} → LkRen T Ρ

instance
  iWkTm : Wk Tm
  wk₁ {{iWkTm}} = ap {Tm} (wkm {Ρ} 1)
  wk {{iWkTm}} δ t = ap {Tm} (wkm {Ρ} δ) t
  wk-zero {{iWkTm}} t = begin
    ap {Tm} (wkm {Ρ} 0) t ≡⟨ ap-rel≅ {Tm} (Ix≅-to-≅ {Tm} (≃-to-≅` (≃-↑ {Ix} (record { lk≃ = λ i → begin
        lk (wkm {Ρ} 0) i ≡⟨ lk-wkm {Ix} {Ρ} 0 i ⟩
        i                ≡⟨ sym (lk-idm {Ix} {Ρ} i) ⟩
        lk (idm {Ρ} _) i ∎
      })))) t ⟩
    ap {Tm} (idm {Ρ} _) t ≡⟨ ap-idm {Tm} {Tm} {Ρ} t ⟩
    t                     ∎
  wk-suc {{iWkTm}} δ t = begin
    ap {Tm} (wkm {Ρ} (suc δ)) t                 ≡⟨ cong (λ ζ → ap {Tm} {Tm} {Ρ} ζ t) (wkm-suc {Ρ} δ) ⟩
    ap {Tm} (wkm {Ρ} δ ⊙ wkm {Ρ} 1) t          ≡⟨ ap-rel≅ {Tm} (Ix≅-to-≅ {Tm} {Ρ} {Pair Ρ Ρ} (≃-to-≅`
      (≃-↑ {Ix} {Ρ} {Pair Ρ Ρ} {ξ = wkm {Ρ} δ ⊙ wkm {Ρ} 1} {wkm {Ρ} δ ⊗ wkm {Ρ} 1} (record { lk≃ =
        lk-⊙-ap {Ix} {Ρ} (wkm {Ρ} δ) (wkm {Ρ} 1)  })))) t ⟩
    ap {Tm} (wkm {Ρ} δ ⊗ wkm {Ρ} 1) t          ≡⟨ ap-pair {Tm} (wkm {Ρ} δ) (wkm {Ρ} 1) t ⟩
    ap {Tm} (wkm {Ρ} 1) (ap {Tm} (wkm {Ρ} δ) t) ∎

instance
  iWkVrTm : WkVr Tm
  wk₁-vr {{iWkVrTm}} i = lk-wkm {Tm} {Ρ} 1 i
  wk-vr {{iWkVrTm}} δ i = lk-wkm {Tm} {Ρ} δ i

  iApWkmWkTm : ApWkmWk Tm Tm
  ap-wkm-wk₁ {{iApWkmWkTm}} {Ξ} = ap-wkm-rel Tm Tm Ξ Ρ 1
  ap-wkm-wk {{iApWkmWkTm}} {Ξ} = ap-wkm-rel Tm Tm Ξ Ρ

  -- iApCompTm : ApComp Tm Tm
  -- ap-⊙ {{iApCompTm}} {Ξ} ξ₁ ξ₂ (var i) = lk-⊙-ap {Tm} {Ξ} ξ₁ ξ₂ i
  -- ap-⊙ {{iApCompTm}} {Ξ} ξ₁ ξ₂ (abs t) rewrite ⊙-↑₁ {Ξ} ξ₁ ξ₂ =
  --   cong abs (ap-⊙ {Tm} (ξ₁ ↑₁) (ξ₂ ↑₁) t)
  -- ap-⊙ {{iApCompTm}} {Ξ} ξ₁ ξ₂ (app t₁ t₂) =
  --   cong₂ app (ap-⊙ {Tm} {Tm} {Ξ} ξ₁ ξ₂ t₁) (ap-⊙ {Tm} {Tm} {Ξ} ξ₁ ξ₂ t₂)

  iApCompTm : ApComp Tm Tm
  iApCompTm = iApComp Tm Tm

  iApWkTm : ApWk Tm Tm
  iApWkTm = iApWk Tm Tm

{-}

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

subTm : {X : STX} {{apTmX : Ap Tm X}} {γ : Dom} (s : Tm γ) (x : X (suc γ)) → X γ
subTm {X} s x = ap Tm X (Sub Tm) (beta Tm (Sub Tm) s) x

data Eval {γ : Dom} : Tm γ → Tm γ → Set where
  e-app₁ : {t₁ t₁' t₂ : Tm γ} → Eval t₁ t₁' → Eval (app t₁ t₂) (app t₁' t₂)
  e-app₂ : {t₁ t₂ t₂' : Tm γ} → Eval t₂ t₂' → Eval (app t₁ t₂) (app t₁ t₂')
  e-abs  : {t t' : Tm (suc γ)} → Eval t t' → Eval (abs t) (abs t')
  e-beta : {s : Tm γ} {t : Tm (suc γ)} → Eval (app (abs t) s) (subTm s t)

--------------------------------------------------------------------------------
-}

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
-- Andreas, 2018-10-18, re #2757
-- Runtime-irrelevance analogue to issue #2640

-- {-# OPTIONS -v tc.lhs.unify:65 #-}
-- {-# OPTIONS -v tc.irr:20 #-}
-- {-# OPTIONS -v tc:30 #-}
-- {-# OPTIONS -v treeless:20 #-}

open import Common.Prelude

data D : (n : Nat) → Set where
  c : (m : Nat) → D m

test : (@0 n : Nat) → D n → Nat
test n (c m) = m

-- Should be rejected (projecting a forced argument).

main = printNat (test 142 (c _))

-- The generated Haskell program segfaults.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Fast exponentiation

module Numeric.Nat.Pow where

open import Prelude
open import Numeric.Nat.DivMod
open import Control.WellFounded
open import Tactic.Nat
open import Tactic.Cong

module _ {a} {A : Set a} {{_ : Semiring A}} where
  private
    expAcc : A → (n : Nat) → Acc _<_ n → A
    expAcc a  zero    wf = one
    expAcc a (suc n) (acc wf) with n divmod 2
    ... | qr q 0 _ eq = force (a * a) λ a² → expAcc a² q (wf q (by eq)) * a
    ... | qr q 1 _ eq = force (a * a) λ a² → expAcc a² (suc q) (wf (suc q) (by eq))
    ... | qr q (suc (suc _)) lt _ = refute lt

  infixr 8 _^′_
  _^′_ : A → Nat → A
  a ^′ n = expAcc a n (wfNat n)

  module _ (assoc : (a b c : A) → a * (b * c) ≡ (a * b) * c)
           (idr   : (a : A) → a * one ≡ a)
           (idl   : (a : A) → one * a ≡ a) where

    private
      force-eq : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) {f : ∀ x → B x} {y : B x} →
                   f x ≡ y → force x f ≡ y
      force-eq x eq = forceLemma x _ ⟨≡⟩ eq

      on-assoc-l : {a b c a₁ b₁ c₁ : A} → (a * b) * c ≡ (a₁ * b₁) * c₁ → a * (b * c) ≡ a₁ * (b₁ * c₁)
      on-assoc-l eq = assoc _ _ _ ⟨≡⟩ eq ⟨≡⟩ʳ assoc _ _ _

      on-assoc-r : {a b c a₁ b₁ c₁ : A} → a * (b * c) ≡ a₁ * (b₁ * c₁) → (a * b) * c ≡ (a₁ * b₁) * c₁
      on-assoc-r eq = assoc _ _ _ ʳ⟨≡⟩ eq ⟨≡⟩ assoc _ _ _

      lem-pow-mul-l : (a : A) (n : Nat) → a * a ^ n ≡ a ^ n * a
      lem-pow-mul-l a zero    = idr _ ⟨≡⟩ʳ idl _
      lem-pow-mul-l a (suc n) = assoc _ _ _ ⟨≡⟩ (_* a) $≡ lem-pow-mul-l a n

      lem-pow-mul-distr : (a : A) (n : Nat) → (a * a) ^ n ≡ a ^ n * a ^ n
      lem-pow-mul-distr a  zero   = sym (idl _)
      lem-pow-mul-distr a (suc n) =
        (_* (a * a)) $≡ lem-pow-mul-distr a n ⟨≡⟩ʳ
        on-assoc-r (((a ^ n) *_) $≡ (on-assoc-l ((_* a) $≡ lem-pow-mul-l a n)))

      lem-pow-add-distr : (a : A) (n m : Nat) → a ^ (n + m) ≡ a ^ n * a ^ m
      lem-pow-add-distr a  zero   m = sym (idl _)
      lem-pow-add-distr a (suc n) m =
        (_* a) $≡ lem-pow-add-distr a n m ⟨≡⟩ʳ
        on-assoc-r (((a ^ n) *_) $≡ lem-pow-mul-l a m)

      lem : ∀ a n (wf : Acc _<_ n) → expAcc a n wf ≡ a ^ n
      lem a  zero   wf = refl
      lem a (suc n) (acc wf) with n divmod 2
      lem a (suc ._) (acc wf) | qr q 0 _ refl =
        force-eq (a * a) (cong (_* a) (
          lem (a * a) q (wf q (diff _ auto)) ⟨≡⟩
          lem-pow-mul-distr a q ⟨≡⟩
          lem-pow-add-distr a q q ʳ⟨≡⟩
          cong (_^_ a) {x = q + q} {y = q * 2 + 0} auto))
      lem a (suc ._) (acc wf) | qr q 1 _ refl =
        force-eq (a * a) $
          lem (a * a) (suc q) (wf (suc q) (diff _ auto)) ⟨≡⟩
          (a * a) ^ q * (a * a)
            ≡⟨ by-cong (lem-pow-mul-distr a q ⟨≡⟩ʳ lem-pow-add-distr a q q) ⟩
          a ^ (q + q) * (a * a)
            ≡⟨ by-cong {x = q + q} {y = q * 2} auto ⟩
          a ^ (q * 2) * (a * a)
            ≡⟨ by-cong (idl a) ⟩
          a ^ (q * 2) * (a ^ 1 * a)
            ≡⟨ assoc _ _ _ ⟩
          a ^ (q * 2) * a ^ 1 * a
            ≡⟨ by-cong (lem-pow-add-distr a (q * 2) 1) ⟩
          a ^ (q * 2 + 1) * a ∎
      ... | qr _ (suc (suc _)) lt _ = refute lt

    lem-^′-sound : ∀ a n → a ^′ n ≡ a ^ n
    lem-^′-sound a n = lem a n (wfNat n)

  {-# DISPLAY expAcc a n _ = a ^′ n #-}

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
module BTree.Complete.Alternative.Correctness {A : Set} where

open import BTree {A}
open import BTree.Equality {A}
open import BTree.Equality.Properties {A}
open import BTree.Complete.Base {A}
open import BTree.Complete.Base.Properties {A}
open import BTree.Complete.Alternative {A} renaming (Complete to Complete' ; _⋘_ to _⋘'_ ; _⋙_ to _⋙'_ ; _⋗_ to _⋗'_)
open import Data.Sum renaming (_⊎_ to _∨_)

lemma-⋗'-⋗ : {l r : BTree} → l ⋗' r → l ⋗ r
lemma-⋗'-⋗ (⋗lf x) = ⋗lf x
lemma-⋗'-⋗ (⋗nd {r = r} {l' = l'} x x' _ l'≃r' l⋗'l') = ⋗nd x x' r l' (lemma-⋗-≃ (lemma-⋗'-⋗ l⋗'l') l'≃r')

lemma-⋙'-⋗ : {l r : BTree} → l ⋙' r → l ⋗ r
lemma-⋙'-⋗ (⋙lf x) = ⋗lf x
lemma-⋙'-⋗ (⋙rl {r = r} {l' = l'} x x' l≃r l'⋘'r' l⋗'r') = ⋗nd x x' r l' (lemma-⋗'-⋗ l⋗'r')
lemma-⋙'-⋗ (⋙rr {r = r} {l' = l'} x x' l≃r l'⋙'r' l≃l') = ⋗nd x x' r l' (lemma-≃-⋗ l≃l' (lemma-⋙'-⋗ l'⋙'r'))

lemma-⋘'-⋗ : {l r : BTree} → l ⋘' r → l ≃ r ∨ l ⋗ r
lemma-⋘'-⋗ lf⋘ = inj₁ ≃lf
lemma-⋘'-⋗ (ll⋘ {r = r} {l' = l'} x x' l⋘'r l'≃r' r≃l')
    with lemma-⋘'-⋗ l⋘'r
... | inj₁ l≃r = inj₁ (≃nd x x' l≃r (trans≃ l≃r r≃l') l'≃r')
... | inj₂ l⋗r = inj₂ (⋗nd x x' r l' (lemma-⋗-≃ l⋗r (trans≃ r≃l' l'≃r')))
lemma-⋘'-⋗ (lr⋘ {r = r} {l' = l'} x x' _ l'≃r' l⋗'l') = inj₂ (⋗nd x x' r l' (lemma-⋗-≃ (lemma-⋗'-⋗ l⋗'l') l'≃r'))

lemma-⋘'-⋘ : {l r : BTree} → l ⋘' r → l ⋘ r
lemma-⋘'-⋘ lf⋘ = eq⋘ ≃lf
lemma-⋘'-⋘ (ll⋘ {r = r} {l' = l'} x x' l⋘'r l'≃r' r≃l')
    with lemma-⋘'-⋗ l⋘'r
... | inj₁ l≃r = eq⋘ (≃nd x x' l≃r (trans≃ l≃r r≃l') l'≃r')
... | inj₂ l⋗r = gt⋘ (np⋗ x l⋗r) (p≃ x' l'≃r') (⋗nd x x' r l' (lemma-⋗-≃ l⋗r (trans≃ r≃l' l'≃r')))
lemma-⋘'-⋘ (lr⋘ {r = r} {l' = l'} x x' l⋙'r l'≃r' l⋗'l') = gt⋘ (np⋗ x (lemma-⋙'-⋗ l⋙'r)) (p≃ x' l'≃r') (⋗nd x x' r l' (lemma-⋗-≃ (lemma-⋗'-⋗ l⋗'l') l'≃r'))

lemma-⋙'-⋙ : {l r : BTree} → l ⋙' r → l ⋙ r
lemma-⋙'-⋙ l⋙'r = ⋙gt (lemma-⋙'-⋗ l⋙'r)

lemma-complete'-complete : {t : BTree} → Complete' t → Complete t
lemma-complete'-complete leaf = leaf
lemma-complete'-complete (left x c'l c'r l⋘'r) = left x (lemma-complete'-complete c'l) (lemma-complete'-complete c'r) (lemma-⋘'-⋘ l⋘'r)
lemma-complete'-complete (right x c'l c'r l⋙'r) = right x (lemma-complete'-complete c'l) (lemma-complete'-complete c'r) (lemma-⋙'-⋙ l⋙'r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
import Bundles
import Construct.DirectProduct
import Definitions
import Definitions.Semiring
import Morphism.Structures
import Properties.RingWithoutOne
import Structures


text:
{-# OPTIONS --show-irrelevant #-}

-- {-# OPTIONS -v tc:20 #-}

open import Agda.Primitive
open import Issue2408.LevelDependentOnIrrelevant

-- Provoke error message mentioning (ℓ a)

provokeError : Set₁
provokeError = X
  where
  X = _
  F' : (a : A) → X
  F' = F

-- If #2408 is solved by replacing irrelevant vars in levels by Prop,
-- we get a horrible error like:
--
--   Set (.Agda.Primitive.lsuc (l .(Prop))) != Set₁
--   when checking that the expression X has type Set₁

-- Expected error:
-- Set (lsuc (l a)) != Set₁
-- when checking that the expression F has type A → X

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module HasSalvation where

open import OscarPrelude

record HasSalvation (A : Set) : Set₁
 where
  field
    ▷_ : A → Set

open HasSalvation ⦃ … ⦄ public

{-# DISPLAY HasSalvation.▷_ _ = ▷_ #-}

record HasDecidableSalvation (A : Set) : Set₁
 where
  field
    ⦃ hasSalvation ⦄ : HasSalvation A
    ▷?_ : (x : A) → Dec $ ▷ x

open HasDecidableSalvation ⦃ … ⦄ public

{-# DISPLAY HasDecidableSalvation.▷?_ _ = ▷?_ #-}


text:
-- Andreas, 2014-04-23 test case by Andrea Vezzosi
{-# OPTIONS --sized-types --copatterns #-}
-- {-# OPTIONS --show-implicit -v term:60 #-}
module _ where

open import Common.Size

-- Invalid coinductive record, since not recursive.
record ▸ (A : Size → Set) (i : Size) : Set where
  coinductive         -- This should be an error, since non-recursive.
  constructor delay_
  field
    force : ∀ {j : Size< i} → A j

open ▸

-- This fixed-point combinator should not pass the termination checker.
∞fix : ∀ {A : Size → Set} → (∀ {i} → ▸ A i → A i) → ∀ {i} → ▸ A i
force (∞fix {A} f {i}) {j} = f {j} (∞fix {A} f {j})

-- The following fixed-point combinator is not strongly normalizing!
fix : ∀ {A : Size → Set} → (∀ {i} → (∀ {j : Size< i} → A j) → A i) → ∀ {i} {j : Size< i} → A j
fix f = force (∞fix (λ {i} x → f {i} (force x)))

-- test = fix {!!}
-- C-c C-n test gives me a stack overflow


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

open import Agda.Builtin.Equality

module Case₀ where

  postulate
    I : Set
    P : I → Set

  variable
    p : P _

  postulate
    D : P _ → Set
    d : D p

module Case₁ where

  postulate
    I : Set
    P : I → Set
    Q : ∀ n → P n → Set

  variable
    q : Q _ _

  postulate
    D : ∀ {p} → Q _ p → Set
    d : D q

module Case₂ where

  postulate
    I : Set
    P : I → Set
    Q : ∀ n → P n → Set

  record R n (p : P n) : Set where
    constructor c
    field
      f : Q _ p

  variable
    q : Q _ _

  data D {p} : R _ p → Set where
    d : D (c q)

module Case₃ where

  variable
    A : Set
    a : A

  record B : Set where
    id = λ x → x ≡ x
    field
      b : id a


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

open import Algebra using (Monoid)

module Data.FingerTree.MonoidSolver {ℓ₁ ℓ₂} (mon : Monoid ℓ₁ ℓ₂) where

open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.List as List using (List; _∷_; []; foldr; _++_)
open import Data.Vec as Vec using (Vec; _∷_; [])
open import Data.Fin as Fin using (Fin)
open import Data.String as String using (String)
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Relation.Nullary using (Dec; yes; no)
open import Data.Unit using (⊤; tt)

open import Relation.Binary using (Setoid)

open import Function
open import Reflection
open import Agda.Builtin.Reflection

open Monoid mon

data Expr : Set ℓ₁ where
  K   : Carrier → Expr
  _⊕_ : Expr → Expr → Expr
  E   : Expr

⟦_⟧ : Expr → Carrier
⟦ K x ⟧ = x
⟦ x ⊕ y ⟧ = ⟦ x ⟧ ∙ ⟦ y ⟧
⟦ E ⟧ = ε

Normal : Set ℓ₁
Normal = List Carrier

norm : Expr → Normal
norm (K x) = x ∷ []
norm (x ⊕ y) = norm x ++ norm y
norm E = []

⟦_,_⟧⁺⇓ : Carrier → Normal → Carrier
⟦ x , [] ⟧⁺⇓ = x
⟦ x₁ , x₂ ∷ xs ⟧⁺⇓ = x₁ ∙ ⟦ x₂ , xs ⟧⁺⇓

⟦_⟧⇓ : Normal → Carrier
⟦ [] ⟧⇓ = ε
⟦ x ∷ xs ⟧⇓ = ⟦ x , xs ⟧⁺⇓

++-homo : (xs ys : Normal) → ⟦ xs ++ ys ⟧⇓ ≈ ⟦ xs ⟧⇓ ∙ ⟦ ys ⟧⇓
++-homo [] ys = sym (identityˡ ⟦ ys ⟧⇓)
++-homo (x ∷ xs) ys = go x xs ys
  where
  go : ∀ x xs ys → ⟦ x , xs ++ ys ⟧⁺⇓ ≈ ⟦ x , xs ⟧⁺⇓ ∙ ⟦ ys ⟧⇓
  go x [] [] = sym (identityʳ x)
  go x [] (y ∷ ys) = refl
  go x₁ (x₂ ∷ xs) ys = ∙-cong refl (go x₂ xs ys) ⟨ trans ⟩ sym (assoc _ _ _)

open import Data.FingerTree.Relation.Binary.Reasoning.FasterInference.Setoid setoid

correct : (e : Expr) → ⟦ norm e ⟧⇓ ≈ ⟦ e ⟧
correct (K x) = refl
correct (x ⊕ y) = ++-homo (norm x) (norm y) ⟨ trans ⟩ (correct x ⟨ ∙-cong ⟩ correct y )
correct E = refl

infixr 5 _⟨∷⟩_ _⟅∷⟆_
pattern _⟨∷⟩_ x xs = arg (arg-info visible relevant) x ∷ xs
pattern _⟅∷⟆_ x xs = arg (arg-info hidden relevant) x ∷ xs

mutual
  E₂ : List (Arg Term) → Term
  E₂ (x ⟨∷⟩ y ⟨∷⟩ []) = quote _⊕_ ⟨ con ⟩ E′ x ⟨∷⟩ E′ y ⟨∷⟩ []
  E₂ (x ∷ xs) = E₂ xs
  E₂ _ = unknown

  E′ : Term → Term
  E′ (def (quote Monoid._∙_) xs) = E₂ xs
  E′ (def (quote Monoid.ε) _) = quote E ⟨ con ⟩ []
  E′ t = quote K ⟨ con ⟩ (t ⟨∷⟩ [])

getVisible : Arg Term → Maybe Term
getVisible (arg (arg-info visible relevant) x) = just x
getVisible (arg (arg-info visible irrelevant) x) = nothing
getVisible (arg (arg-info hidden r) x) = nothing
getVisible (arg (arg-info instance′ r) x) = nothing

getArgs : ∀ n → Term → Maybe (Vec Term n)
getArgs n (def _ xs) = Maybe.map Vec.reverse (List.foldl f b (List.mapMaybe getVisible xs) n)
  where
  f : (∀ n → Maybe (Vec Term n)) → Term → ∀ n → Maybe (Vec Term n)
  f xs x zero = just Vec.[]
  f xs x (suc n) = Maybe.map (x Vec.∷_) (xs n)

  b : ∀ n → Maybe (Vec Term n)
  b zero = just Vec.[]
  b (suc _ ) = nothing
getArgs _ _ = nothing

infixr 5 _⋯⟅∷⟆_
_⋯⟅∷⟆_ : ℕ → List (Arg Term) → List (Arg Term)
zero  ⋯⟅∷⟆ xs = xs
suc i ⋯⟅∷⟆ xs = unknown ⟅∷⟆ i ⋯⟅∷⟆ xs

constructSoln : Term → Term → Term → Term
constructSoln mon lhs rhs =
  quote Monoid.trans ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩
    (quote Monoid.sym ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩ (quote correct ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩ E′ lhs ⟨∷⟩ []) ⟨∷⟩ [])
    ⟨∷⟩
    (quote correct ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩ E′ rhs ⟨∷⟩ []) ⟨∷⟩
    []

_>>=_ : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
_>>=_ = bindTC

_>>_ : ∀ {a b} {A : Set a} {B : Set b} → TC A → TC B → TC B
xs >> ys = xs >>= λ _ → ys

solve-macro : Term → Term → TC ⊤
solve-macro mon hole = do
  hole′ ← inferType hole >>= normalise
  just (lhs ∷ rhs ∷ []) ← returnTC (getArgs 2 hole′)
    where nothing → typeError (termErr hole′ ∷ [])
  let soln = constructSoln mon lhs rhs
  unify hole soln

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


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

module Data.Pi where

open import Data.Pi.Base public


text:
------------------------------------------------------------------------------
-- The Agda standard library
--
-- Additional properties for setoids
------------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where

open Setoid S

open import Data.Product using (_,_)
open import Function using (_∘_; _$_)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------------
-- Every setoid is a preorder with respect to propositional equality

isPreorder : IsPreorder _≡_ _≈_
isPreorder = record
  { isEquivalence = P.isEquivalence
  ; reflexive     = reflexive
  ; trans         = trans
  }

preorder : Preorder a a ℓ
preorder = record
  { isPreorder = isPreorder
  }

------------------------------------------------------------------------------
-- Properties of _≉_

≉-sym :  Symmetric _≉_
≉-sym x≉y =  x≉y ∘ sym

≉-respˡ : _≉_ Respectsˡ _≈_
≉-respˡ x≈x' x≉y = x≉y ∘ trans x≈x'

≉-respʳ : _≉_ Respectsʳ _≈_
≉-respʳ y≈y' x≉y x≈y' = x≉y $ trans x≈y' (sym y≈y')

≉-resp₂ : _≉_ Respects₂ _≈_
≉-resp₂ = ≉-respʳ , ≉-respˡ


text:
module cedille-options where
open import general-util
open import options-types public
open import cedille-types

record options : Set where
  constructor mk-options
  field include-path : 𝕃 string × stringset
        use-cede-files : 𝔹
        make-rkt-files : 𝔹
        generate-logs : 𝔹
        show-qualified-vars : 𝔹
        erase-types : 𝔹
        datatype-encoding : maybe (filepath × maybe file)
        pretty-print-columns : ℕ

        -- Internal use only
        during-elaboration : 𝔹
        pretty-print : 𝔹
        show-progress-updates : 𝔹

default-options : options
default-options = record {
  include-path = [] , empty-stringset;
  use-cede-files = tt;
  make-rkt-files = ff;
  generate-logs = ff;
  show-qualified-vars = ff;
  erase-types = tt;
  datatype-encoding = nothing;
  pretty-print-columns = 80;
  during-elaboration = ff;
  pretty-print = ff ;
  show-progress-updates = ff}

include-path-insert : string → 𝕃 string × stringset → 𝕃 string × stringset
include-path-insert s (l , ss) =
  if stringset-contains ss s
    then l , ss
    else s :: l , stringset-insert ss s

options-to-rope : options → rope
options-to-rope ops =
  comment "Cedille Options File" ⊹⊹ [[ "\n" ]] ⊹⊹
  comment "List of directories to search for imported files in" ⊹⊹
  comment "Each directory should be space-delimited and inside double quotes" ⊹⊹
  comment "The current file's directory is automatically searched first, before import-directories" ⊹⊹
  comment "If a filepath is relative, it is considered relative to this options file" ⊹⊹
  option "import-directories"
    (𝕃-to-string (λ fp → "\"" ^ fp ^ "\"") " " (fst (options.include-path ops))) ⊹⊹
  comment "Cache navigation spans for performance" ⊹⊹
  option "use-cede-files" (𝔹-s options.use-cede-files) ⊹⊹
--  comment "Compile Cedille files to Racket after they are checked"⊹⊹
--  option "make-rkt-files" (𝔹-s options.make-rkt-files) ⊹⊹
  comment "Write logs to ~/.cedille/log" ⊹⊹
  option "generate-logs" (𝔹-s options.generate-logs) ⊹⊹
  comment "Print variables fully qualified" ⊹⊹
  option "show-qualified-vars" (𝔹-s options.show-qualified-vars) ⊹⊹
  comment "Print types erased" ⊹⊹
  option "erase-types" (𝔹-s options.erase-types) ⊹⊹
  comment "Preferred number of columns to pretty print elaborated files with" ⊹⊹
  option "pretty-print-columns" (ℕ-to-string (options.pretty-print-columns ops)) ⊹⊹
  comment "Encoding to use when elaborating datatypes to Cedille Core" ⊹⊹
  option "datatype-encoding" (maybe-else' (options.datatype-encoding ops) "" λ fp → "\"" ^ fst fp  ^ "\"")

  where
  𝔹-s : (options → 𝔹) → string
  𝔹-s f = if f ops then "true" else "false"

  comment : string → rope
  comment s = [[ "-- " ]] ⊹⊹ [[ s ]] ⊹⊹ [[ "\n" ]]

  option : (name : string) → (value : string) → rope
  option name value = [[ name ]] ⊹⊹ [[ " = " ]] ⊹⊹ [[ value ]] ⊹⊹ [[ ".\n\n" ]]


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

module Categories.Functor.Duality where

open import Level
open import Data.Product using (Σ; _,_)

open import Categories.Category
open import Categories.Category.Construction.Cones as Con
open import Categories.Category.Construction.Cocones as Coc
open import Categories.Functor
open import Categories.Functor.Continuous
open import Categories.Functor.Cocontinuous
open import Categories.Diagram.Limit as Lim
open import Categories.Diagram.Colimit as Col
open import Categories.Diagram.Duality
open import Categories.Morphism.Duality as MorD

private
  variable
    o ℓ e : Level
    C D E J : Category o ℓ e

module _ (G : Functor C D) {J : Category o ℓ e} where
  private
    module C = Category C
    module D = Category D
    module G = Functor G
    module J = Category J

  coLimitPreserving⇒ColimitPreserving : ∀ {F : Functor J C} (L : Limit (Functor.op F)) →
                                          LimitPreserving G.op L →
                                          ColimitPreserving G (coLimit⇒Colimit C L)
  coLimitPreserving⇒ColimitPreserving L (L′ , iso) = coLimit⇒Colimit D L′ , op-≅⇒≅ D iso

  ColimitPreserving⇒coLimitPreserving : ∀ {F : Functor J C} (L : Colimit F) →
                                          ColimitPreserving G L →
                                          LimitPreserving G.op (Colimit⇒coLimit C L)
  ColimitPreserving⇒coLimitPreserving L (L′ , iso) = Colimit⇒coLimit D L′ , op-≅⇒≅ D.op iso

module _ {o ℓ e} (G : Functor C D) where
  private
    module G = Functor G

  coContinuous⇒Cocontinuous : Continuous o ℓ e G.op → Cocontinuous o ℓ e G
  coContinuous⇒Cocontinuous Con L =
    coLimitPreserving⇒ColimitPreserving G (Colimit⇒coLimit C L) (Con (Colimit⇒coLimit C L))

  Cocontinuous⇒coContinuous : Cocontinuous o ℓ e G → Continuous o ℓ e G.op
  Cocontinuous⇒coContinuous Coc L =
    ColimitPreserving⇒coLimitPreserving G (coLimit⇒Colimit C L) (Coc (coLimit⇒Colimit C L))

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


text:
open import Data.Product using ( _,_ ; proj₁ ; proj₂ )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Relation.Unary using ( _⊆_ )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; cong )
open import Web.Semantic.DL.ABox using ( ε ; _,_ ; _∼_ ; _∈₁_ ; _∈₂_ ; ⟨ABox⟩ ; Assertions )
open import Web.Semantic.DL.ABox.Interp using ( ⌊_⌋ ; ind )
open import Web.Semantic.DL.ABox.Model using ( ⊨a-impl-⊨b ; ⟨ABox⟩-Assertions )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Object using ( Object ; _,_ ; IN ; fin ; iface )
open import Web.Semantic.DL.Category.Morphism using ( _⇒_ ; _⊑_ ; _≣_ ; _,_ )
open import Web.Semantic.DL.Category.Properties.Composition.RespectsEquiv using ( compose-resp-≣ )
open import Web.Semantic.DL.Category.Properties.Composition.RespectsWiring using ( compose-resp-wiring )
open import Web.Semantic.DL.Category.Properties.Equivalence using ( ≣-refl ; ≣-sym ; ≣-trans )
open import Web.Semantic.DL.Category.Properties.Tensor.RespectsEquiv using ( tensor-resp-≣ )
open import Web.Semantic.DL.Category.Properties.Tensor.RespectsWiring using ( tensor-resp-wiring )
open import Web.Semantic.DL.Category.Tensor using ( _⊗_ ; _⟨⊗⟩_ )
open import Web.Semantic.DL.Category.Unit using ( I )
open import Web.Semantic.DL.Category.Wiring using
  ( wiring ; wires ; wires-≈ ; wires-≈⁻¹
  ; identity ; symm ; assoc ; assoc⁻¹ ; unit₁ ; unit₁⁻¹ ; unit₂ ; unit₂⁻¹
  ; id✓ ; ⊎-swap✓ ; ⊎-assoc✓ ; ⊎-assoc⁻¹✓ ; inj₁✓ ; inj₂✓ ; ⊎-unit₁✓ ; ⊎-unit₂✓ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.DL.TBox.Interp using ( ≈-refl′ ; ≈-trans )
open import Web.Semantic.Util using
  ( id ; _∘_ ; inode ; _⟨⊎⟩_ ; ⊎-swap ; ⊎-assoc ; ⊎-assoc⁻¹ ; ⊎-unit₁ ; ⊎-unit₂ )

module Web.Semantic.DL.Category.Properties.Wiring
  {Σ : Signature} {S T : TBox Σ} where

wiring-⊑-refl : ∀ (A B : Object S T) (f g : IN B → IN A)
  (f✓ : Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A))
    (g✓ : Assertions (⟨ABox⟩ g (iface B)) ⊆ Assertions (iface A)) →
      (∀ x → f x ≡ g x) → (wiring A B f f✓ ⊑ wiring A B g g✓)
wiring-⊑-refl A B f g f✓ g✓ f≡g I I⊨STA I⊨F =
  ⊨a-impl-⊨b I (wires g (proj₁ (fin B)))
    (wires-≈⁻¹ g
      (λ x → ≈-trans ⌊ I ⌋
        (≈-refl′ ⌊ I ⌋ (cong (ind I ∘ inode) (sym (f≡g x))))
        (wires-≈ f (proj₂ (fin B) x) I⊨F))
      (proj₁ (fin B)))

wiring-≣-refl : ∀ (A B : Object S T) (f g : IN B → IN A)
  (f✓ : Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A))
    (g✓ : Assertions (⟨ABox⟩ g (iface B)) ⊆ Assertions (iface A)) →
      (∀ x → f x ≡ g x) → (wiring A B f f✓ ≣ wiring A B g g✓)
wiring-≣-refl A B f g f✓ g✓ f≡g =
  ( wiring-⊑-refl A B f g f✓ g✓ f≡g
  , wiring-⊑-refl A B g f g✓ f✓ (λ x → sym (f≡g x)) )

∘✓ :  (A B C : Object S T) →
  (f : IN B → IN A) → (g : IN C → IN B) →
  (Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A)) →
  (Assertions (⟨ABox⟩ g (iface C)) ⊆ Assertions (iface B)) →
  (Assertions (⟨ABox⟩ (f ∘ g) (iface C)) ⊆ Assertions (iface A))
∘✓ A B (X , X∈Fin , ε) f g f✓ g✓ ()
∘✓ A B (X , X∈Fin , C₁ , C₂) f g f✓ g✓ (inj₁ a∈C₁) = ∘✓ A B (X , X∈Fin , C₁) f g f✓ (g✓ ∘ inj₁) a∈C₁
∘✓ A B (X , X∈Fin , C₁ , C₂) f g f✓ g✓ (inj₂ a∈C₂) = ∘✓ A B (X , X∈Fin , C₂) f g f✓ (g✓ ∘ inj₂) a∈C₂
∘✓ A B (X , X∈Fin , x ∼ y) f g f✓ g✓ refl = f✓ (⟨ABox⟩-Assertions f (iface B) (g✓ refl))
∘✓ A B (X , X∈Fin , x ∈₁ c) f g f✓ g✓ refl = f✓ (⟨ABox⟩-Assertions f (iface B) (g✓ refl))
∘✓ A B (X , X∈Fin , (x , y) ∈₂ r) f g f✓ g✓ refl = f✓ (⟨ABox⟩-Assertions f (iface B) (g✓ refl))

⟨⊎⟩✓ : (A₁ A₂ B₁ B₂ : Object S T) →
  (f₁ : IN B₁ → IN A₁) → (f₂ : IN B₂ → IN A₂) →
  (Assertions (⟨ABox⟩ f₁ (iface B₁)) ⊆ Assertions (iface A₁)) →
  (Assertions (⟨ABox⟩ f₂ (iface B₂)) ⊆ Assertions (iface A₂)) →
  (Assertions (⟨ABox⟩ (f₁ ⟨⊎⟩ f₂) (iface (B₁ ⊗ B₂))) ⊆ Assertions (iface (A₁ ⊗ A₂)))
⟨⊎⟩✓ A₁ A₂ (X₁ , X₁∈Fin , ε) B₂ f₁ f₂ f₁✓ f₂✓ (inj₁ ())
⟨⊎⟩✓ A₁ A₂ (X₁ , X₁∈Fin , B₁₁ , B₁₂) B₂ f₁ f₂ f₁✓ f₂✓ (inj₁ (inj₁ b∈B₁₁)) =
  ⟨⊎⟩✓ A₁ A₂ (X₁ , X₁∈Fin , B₁₁) B₂ f₁ f₂ (f₁✓ ∘ inj₁) f₂✓ (inj₁ b∈B₁₁)
⟨⊎⟩✓ A₁ A₂ (X₁ , X₁∈Fin , B₁₁ , B₁₂) B₂ f₁ f₂ f₁✓ f₂✓ (inj₁ (inj₂ b∈B₁₂)) =
  ⟨⊎⟩✓ A₁ A₂ (X₁ , X₁∈Fin , B₁₂) B₂ f₁ f₂ (f₁✓ ∘ inj₂) f₂✓ (inj₁ b∈B₁₂)
⟨⊎⟩✓ A₁ A₂ (X₁ , X₁∈Fin , x ∼ y) B₂ f₁ f₂ f₁✓ f₂✓ (inj₁ refl) =
  inj₁ (⟨ABox⟩-Assertions inj₁ (iface A₁) (f₁✓ refl))
⟨⊎⟩✓ A₁ A₂ (X₁ , X₁∈Fin , x ∈₁ c) B₂ f₁ f₂ f₁✓ f₂✓ (inj₁ refl) =
  inj₁ (⟨ABox⟩-Assertions inj₁ (iface A₁) (f₁✓ refl))
⟨⊎⟩✓ A₁ A₂ (X₁ , X₁∈Fin , (x , y) ∈₂ r) B₂ f₁ f₂ f₁✓ f₂✓ (inj₁ refl) =
  inj₁ (⟨ABox⟩-Assertions inj₁ (iface A₁) (f₁✓ refl))
⟨⊎⟩✓ A₁ A₂ B₁ (X₂ , X₂∈Fin , ε) f₁ f₂ f₁✓ f₂✓ (inj₂ ())
⟨⊎⟩✓ A₁ A₂ B₁ (X₂ , X₂∈Fin , B₂₁ , B₂₂) f₁ f₂ f₁✓ f₂✓ (inj₂ (inj₁ b∈B₂₁)) =
  ⟨⊎⟩✓ A₁ A₂ B₁ (X₂ , X₂∈Fin , B₂₁) f₁ f₂ f₁✓ (f₂✓ ∘ inj₁) (inj₂ b∈B₂₁)
⟨⊎⟩✓ A₁ A₂ B₁ (X₂ , X₂∈Fin , B₂₁ , B₂₂) f₁ f₂ f₁✓ f₂✓ (inj₂ (inj₂ b∈B₂₂)) =
  ⟨⊎⟩✓ A₁ A₂ B₁ (X₂ , X₂∈Fin , B₂₂) f₁ f₂ f₁✓ (f₂✓ ∘ inj₂) (inj₂ b∈B₂₂)
⟨⊎⟩✓ A₁ A₂ B₁ (X₂ , X₂∈Fin , x ∼ y) f₁ f₂ f₁✓ f₂✓ (inj₂ refl) =
  inj₂ (⟨ABox⟩-Assertions inj₂ (iface A₂) (f₂✓ refl))
⟨⊎⟩✓ A₁ A₂ B₁ (X₂ , X₂∈Fin , x ∈₁ c) f₁ f₂ f₁✓ f₂✓ (inj₂ refl) =
  inj₂ (⟨ABox⟩-Assertions inj₂ (iface A₂) (f₂✓ refl))
⟨⊎⟩✓ A₁ A₂ B₁ (X₂ , X₂∈Fin , (x , y) ∈₂ r) f₁ f₂ f₁✓ f₂✓ (inj₂ refl) =
  inj₂ (⟨ABox⟩-Assertions inj₂ (iface A₂) (f₂✓ refl))

data Rewrite : (A B : Object S T) (F : A ⇒ B) (f : IN B → IN A) →
  (Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A)) → Set₁ where
    rewrite-wiring : ∀ A B f (f✓ : Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A)) →
      Rewrite A B (wiring A B f f✓) f f✓
    rewrite-compose : ∀ {A B C F G f g}
      {f✓ : Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A)}
        {g✓ : Assertions (⟨ABox⟩ g (iface C)) ⊆ Assertions (iface B)} →
      Rewrite A B F f f✓ → Rewrite B C G g g✓ → Rewrite A C (F ∙ G) (f ∘ g) (∘✓ A B C f g f✓ g✓)
    rewrite-tensor : ∀ {A₁ A₂ B₁ B₂ F₁ F₂ f₁ f₂}
      {f₁✓ : Assertions (⟨ABox⟩ f₁ (iface B₁)) ⊆ Assertions (iface A₁)}
        {f₂✓ : Assertions (⟨ABox⟩ f₂ (iface B₂)) ⊆ Assertions (iface A₂)} →
          Rewrite A₁ B₁ F₁ f₁ f₁✓ → Rewrite A₂ B₂ F₂ f₂ f₂✓ →
            Rewrite (A₁ ⊗ A₂) (B₁ ⊗ B₂) (F₁ ⟨⊗⟩ F₂) (f₁ ⟨⊎⟩ f₂) (⟨⊎⟩✓ A₁ A₂ B₁ B₂ f₁ f₂ f₁✓ f₂✓)

rewrite-identity : ∀ A → Rewrite A A (identity A) id (id✓ A)
rewrite-identity A = rewrite-wiring A A id (id✓ A)

rewrite-symm : ∀ A B → Rewrite (A ⊗ B) (B ⊗ A) (symm A B) ⊎-swap (⊎-swap✓ A B)
rewrite-symm A B = rewrite-wiring (A ⊗ B) (B ⊗ A) ⊎-swap (⊎-swap✓ A B)

rewrite-assoc : ∀ A B C → Rewrite ((A ⊗ B) ⊗ C) (A ⊗ (B ⊗ C)) (assoc A B C) ⊎-assoc⁻¹ (⊎-assoc⁻¹✓ A B C)
rewrite-assoc A B C = rewrite-wiring ((A ⊗ B) ⊗ C) (A ⊗ (B ⊗ C)) ⊎-assoc⁻¹ (⊎-assoc⁻¹✓ A B C)

rewrite-assoc⁻¹ : ∀ A B C → Rewrite (A ⊗ (B ⊗ C)) ((A ⊗ B) ⊗ C) (assoc⁻¹ A B C) ⊎-assoc (⊎-assoc✓ A B C)
rewrite-assoc⁻¹ A B C = rewrite-wiring (A ⊗ (B ⊗ C)) ((A ⊗ B) ⊗ C) ⊎-assoc (⊎-assoc✓ A B C)

rewrite-unit₁ : ∀ A → Rewrite (I ⊗ A) A (unit₁ A) inj₂ (inj₂✓ A)
rewrite-unit₁ A = rewrite-wiring (I ⊗ A) A inj₂ (inj₂✓ A)

rewrite-unit₁⁻¹ : ∀ A → Rewrite A (I ⊗ A) (unit₁⁻¹ A) ⊎-unit₁ (⊎-unit₁✓ A)
rewrite-unit₁⁻¹ A = rewrite-wiring A (I ⊗ A) ⊎-unit₁ (⊎-unit₁✓ A)

rewrite-unit₂ : ∀ A → Rewrite (A ⊗ I) A (unit₂ A) inj₁ (inj₁✓ A)
rewrite-unit₂ A = rewrite-wiring (A ⊗ I) A inj₁ (inj₁✓ A)

rewrite-unit₂⁻¹ : ∀ A → Rewrite A (A ⊗ I) (unit₂⁻¹ A) ⊎-unit₂ (⊎-unit₂✓ A)
rewrite-unit₂⁻¹ A = rewrite-wiring A (A ⊗ I) ⊎-unit₂ (⊎-unit₂✓ A)

rewriting : ∀ {A B F G f g}
  {f✓ : Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A)}
    {g✓ : Assertions (⟨ABox⟩ g (iface B)) ⊆ Assertions (iface A)} →
      (Rewrite A B F f f✓) → (∀ x → f x ≡ g x) → (Rewrite A B G g g✓) →
        (F ≣ G)
rewriting {A} {B} {F} {G} {f} {g} {f✓} {g✓} F⇓f f≡g G⇓g =
  ≣-trans (lemma F⇓f)
    (≣-trans (wiring-≣-refl A B f g f✓ g✓ f≡g)
      (≣-sym (lemma G⇓g))) where

  lemma :  ∀ {A B F f}
    {f✓ : Assertions (⟨ABox⟩ f (iface B)) ⊆ Assertions (iface A)} →
      (Rewrite A B F f f✓) →
        (F ≣ wiring A B f f✓)
  lemma (rewrite-wiring A B f f✓) = ≣-refl (wiring A B f f✓)
  lemma (rewrite-compose {A} {B} {C} {F} {G} {f} {g} {f✓} {g✓} F⇓f G⇓g) =
    ≣-trans (compose-resp-≣ (lemma F⇓f) (lemma G⇓g))
      (compose-resp-wiring A B C f f✓ g g✓ (f ∘ g)
        (∘✓ A B C f g f✓ g✓) (λ x → refl))
  lemma (rewrite-tensor {A₁} {A₂} {B₁} {B₂} {F₁} {F₂} {f₁} {f₂} {f₁✓} {f₂✓} F₁⇓f₁ F₂⇓f₂) =
    ≣-trans (tensor-resp-≣ (lemma F₁⇓f₁) (lemma F₂⇓f₂))
      (tensor-resp-wiring A₁ A₂ B₁ B₂ f₁ f₁✓ f₂ f₂✓ (f₁ ⟨⊎⟩ f₂)
        (⟨⊎⟩✓ A₁ A₂ B₁ B₂ f₁ f₂ f₁✓ f₂✓) (λ x → refl) (λ x → refl))

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


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

-- Modules that use --cubical can be imported when --erased-cubical is
-- used.

import Erased-cubical-Module-application.Cubical
module EC = Erased-cubical-Module-application.Cubical Set

-- However, definitions from such modules can only be used in erased
-- contexts.

_ : {A : Set} → A → EC.∥ A ∥
_ = EC.∣_∣

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
------------------------------------------------------------------------
-- Definition of the size of an expression, along with some properties
------------------------------------------------------------------------

module Expression-size where

open import Equality.Propositional
open import Prelude hiding (const)

open import List equality-with-J
open import Nat equality-with-J

-- To simplify the development, let's work with actual natural numbers
-- as variables and constants (see
-- Atom.one-can-restrict-attention-to-χ-ℕ-atoms).

open import Atom

open import Chi            χ-ℕ-atoms
open import Combinators
open import Free-variables χ-ℕ-atoms
open import Termination    χ-ℕ-atoms

open χ-atoms χ-ℕ-atoms

------------------------------------------------------------------------
-- A definition

mutual

  -- The size of an expression.

  size : Exp → ℕ
  size (apply e₁ e₂) = 1 + size e₁ + size e₂
  size (lambda x e)  = 1 + size e
  size (case e bs)   = 1 + size e + size-B⋆ bs
  size (rec x e)     = 1 + size e
  size (var x)       = 1
  size (const c es)  = 1 + size-⋆ es

  size-B : Br → ℕ
  size-B (branch c xs e) = 1 + length xs + size e

  size-⋆ : List Exp → ℕ
  size-⋆ []       = 1
  size-⋆ (e ∷ es) = 1 + size e + size-⋆ es

  size-B⋆ : List Br → ℕ
  size-B⋆ []       = 1
  size-B⋆ (b ∷ bs) = 1 + size-B b + size-B⋆ bs

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

-- Every expression has size at least one.

1≤size : ∀ e → 1 ≤ size e
1≤size (apply e₁ e₂) = suc≤suc (zero≤ _)
1≤size (lambda x e)  = suc≤suc (zero≤ _)
1≤size (case e bs)   = suc≤suc (zero≤ _)
1≤size (rec x e)     = suc≤suc (zero≤ _)
1≤size (var x)       = suc≤suc (zero≤ _)
1≤size (const c es)  = suc≤suc (zero≤ _)

1≤size-⋆ : ∀ es → 1 ≤ size-⋆ es
1≤size-⋆ []      = suc≤suc (zero≤ _)
1≤size-⋆ (_ ∷ _) = suc≤suc (zero≤ _)

1≤size-B⋆ : ∀ bs → 1 ≤ size-B⋆ bs
1≤size-B⋆ []      = suc≤suc (zero≤ _)
1≤size-B⋆ (_ ∷ _) = suc≤suc (zero≤ _)

-- Closed expressions have size at least two.

closed→2≤size : ∀ e → Closed e → 2 ≤ size e
closed→2≤size (apply e₁ e₂) cl =
  2                      ≤⟨ m≤m+n _ _ ⟩
  2 + size e₂            ≤⟨ (1 ∎≤) +-mono 1≤size e₁ +-mono (size e₂ ∎≤) ⟩∎
  1 + size e₁ + size e₂  ∎≤

closed→2≤size (lambda x e) cl =
  2           ≤⟨ (1 ∎≤) +-mono 1≤size e ⟩∎
  1 + size e  ∎≤

closed→2≤size (case e bs) cl =
  2                        ≤⟨ m≤m+n _ _ ⟩
  2 + size-B⋆ bs           ≤⟨ (1 ∎≤) +-mono 1≤size e +-mono (size-B⋆ bs ∎≤) ⟩∎
  1 + size e + size-B⋆ bs  ∎≤

closed→2≤size (rec x e) cl =
  2           ≤⟨ (1 ∎≤) +-mono 1≤size e ⟩∎
  1 + size e  ∎≤

closed→2≤size (var x) cl = ⊥-elim (cl x (λ ()) (var refl))

closed→2≤size (const c es) cl =
  2              ≤⟨ (1 ∎≤) +-mono 1≤size-⋆ es ⟩∎
  1 + size-⋆ es  ∎≤

-- Closed, non-terminating expressions of size two must have the form
-- "rec x = x" (for some x).

data Is-loop : Exp → Type where
  rec : ∀ {x y} → x ≡ y → Is-loop (rec x (var y))

closed-non-terminating-size≡2→loop :
  ∀ e → Closed e → ¬ Terminates e → size e ≡ 2 → Is-loop e
closed-non-terminating-size≡2→loop (rec x e) cl _ size≡2 with e
... | apply e₁ e₂ = ⊥-elim $ +≮ 1 (4                      ≤⟨ (2 ∎≤) +-mono 1≤size e₁ +-mono 1≤size e₂ ⟩
                                   2 + size e₁ + size e₂  ≡⟨ size≡2 ⟩≤
                                   2                      ∎≤)
... | lambda _ e′ = ⊥-elim $ +≮ 0 (3            ≤⟨ (2 ∎≤) +-mono 1≤size e′ ⟩
                                   2 + size e′  ≡⟨ size≡2 ⟩≤
                                   2            ∎≤)
... | case e′ bs  = ⊥-elim $ +≮ 0 (3                         ≤⟨ (2 ∎≤) +-mono 1≤size e′ +-mono zero≤ _ ⟩
                                   2 + size e′ + size-B⋆ bs  ≡⟨ size≡2 ⟩≤
                                   2                         ∎≤)
... | rec _ e′    = ⊥-elim $ +≮ 0 (3            ≤⟨ (2 ∎≤) +-mono 1≤size e′ ⟩
                                   2 + size e′  ≡⟨ size≡2 ⟩≤
                                   2            ∎≤)
... | const _ es  = ⊥-elim $ +≮ 0 (3              ≤⟨ (2 ∎≤) +-mono 1≤size-⋆ es ⟩
                                   2 + size-⋆ es  ≡⟨ size≡2 ⟩≤
                                   2              ∎≤)
... | var y with x V.≟ y
...   | yes x≡y = rec x≡y
...   | no  x≢y = ⊥-elim (cl y (λ ()) (rec (x≢y ∘ sym) (var refl)))

closed-non-terminating-size≡2→loop (apply e₁ e₂) _ _ size≡2 =
  ⊥-elim $ +≮ 0 (3                      ≤⟨ (1 ∎≤) +-mono 1≤size e₁ +-mono 1≤size e₂ ⟩
                 1 + size e₁ + size e₂  ≡⟨ size≡2 ⟩≤
                 2                      ∎≤)

closed-non-terminating-size≡2→loop (lambda x e) _ ¬⇓ _ =
  ⊥-elim (¬⇓ (_ , lambda))

closed-non-terminating-size≡2→loop (case e bs) _ _ size≡2 =
  ⊥-elim $ +≮ 0 (3                        ≤⟨ (1 ∎≤) +-mono 1≤size e +-mono 1≤size-B⋆ bs ⟩
                 1 + size e + size-B⋆ bs  ≡⟨ size≡2 ⟩≤
                 2                        ∎≤)

closed-non-terminating-size≡2→loop (var x) cl _ _ =
  ⊥-elim (cl x (λ ()) (var refl))

closed-non-terminating-size≡2→loop (const c []) _ ¬⇓ _ =
  ⊥-elim (¬⇓ (_ , const []))

closed-non-terminating-size≡2→loop (const c (e ∷ es)) _ _ size≡2 =
  ⊥-elim $ +≮ 1 (4                       ≤⟨ (2 ∎≤) +-mono 1≤size e +-mono 1≤size-⋆ es ⟩
                 2 + size e + size-⋆ es  ≡⟨ size≡2 ⟩≤
                 2                       ∎≤)

-- Closed, non-terminating expressions of minimal size must have the
-- form "rec x = x" (for some x).

minimal-closed-non-terminating→loop :
  let P : Exp → Type
      P e = Closed e × ¬ Terminates e
  in
  ∀ e → P e → (∀ e′ → P e′ → size e ≤ size e′) → Is-loop e
minimal-closed-non-terminating→loop e (cl , ¬⇓) minimal =
  closed-non-terminating-size≡2→loop e cl ¬⇓ (
    ≤-antisymmetric
      (minimal loop (loop-closed , ¬loop⇓))
      (closed→2≤size e cl))

max_stars_repo_name: nad/chi

max_issues_repo_name: nad/chi

max_forks_repo_name: nad/chi


text:
-- Andreas, 2020-04-12, issue #4580
-- Highlighting for builtins FROMNAT, FROMNEG, FROMSTRING

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

record Number (A : Set) : Set where
  field fromNat : Nat → A

record Negative (A : Set) : Set where
  field fromNeg : Nat → A

open Number {{...}} public
open Negative {{...}} public

{-# BUILTIN FROMNAT fromNat #-}  -- Should be highlighted.
{-# BUILTIN FROMNEG fromNeg #-}  -- Jump to definition should work.

instance
  NumberNat : Number Nat
  NumberNat = record { fromNat = λ n → n }

data Int : Set where
  pos : Nat → Int
  neg : Nat → Int

instance
  NumberInt : Number Int
  NumberInt = record { fromNat = pos }

  NegativeInt : Negative Int
  NegativeInt = record { fromNeg = λ { zero → pos 0 ; (suc n) → neg n } }

minusFive : Int
minusFive = -5

thm : -5 ≡ neg 4
thm = refl


text:
-- Andreas, 2016-11-19 issue #2308

-- Since fix of #2197, in mutual blocks, records are no-eta-equality
-- until the positivity checker has run.
-- Thus, the record pattern translation might not kick in.

-- Now, there is another pass of record pattern translation
-- after the mutual block has finished.

data Unit : Set where
  unit : Unit

mutual -- needed to trigger issue

  record R : Set where  -- needs to be in mutual block
    constructor wrap
    field f : Unit

  G : R → Set
  G (wrap _) = Unit -- match on wrap needed

test : (x : R) → G x → Set₁
test _ unit = Set

-- ERROR WAS:
-- Type mismatch
-- when checking that the pattern unit has type G x

-- Should succeed.

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Oscar.Prelude
open import Oscar.Class.HasEquivalence
import Oscar.Data.Constraint

module Oscar.Class.Properthing where

record Properthing {𝔬} ℓ (𝔒 : Ø 𝔬) : Ø 𝔬 ∙̂ ↑̂ ℓ where
  infixr 15 _∧_
  field
    ➊ : 𝔒
    _∧_ : 𝔒 → 𝔒 → 𝔒
    ⦃ ⌶HasEquivalence ⦄ : HasEquivalence 𝔒 ℓ
    Nothing : 𝔒 → Ø ℓ
    fact2 : ∀ {P Q} → P ≈ Q → Nothing P → Nothing Q
    ∧-leftIdentity : ∀ P → ➊ ∧ P ≈ P

open Properthing ⦃ … ⦄ public


text:
-- Andreas, 2016-07-21
-- Test case to ensure postfix printing of projections.

{-# OPTIONS --postfix-projections #-}

open import Common.Product
open import Common.Equality

testProj : {A : Set}{B : A → Set}(y z : Σ A B) →
  let X : Σ A B
      X = _
  in X .proj₁ ≡ y .proj₁ → X .proj₂ ≡ z .proj₂
testProj y z = _ , _


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Unsafe String operations and proofs
------------------------------------------------------------------------

{-# OPTIONS --with-K #-}

module Data.String.Unsafe where

import Data.List.Base as List
import Data.List.Properties as Listₚ
open import Data.Nat.Base using (_+_)
open import Data.String.Base

open import Relation.Binary.PropositionalEquality; open ≡-Reasoning
open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)

------------------------------------------------------------------------
-- Properties of conversion functions

toList∘fromList : ∀ s → toList (fromList s) ≡ s
toList∘fromList s = trustMe

fromList∘toList : ∀ s → fromList (toList s) ≡ s
fromList∘toList s = trustMe

toList-++ : ∀ s t → toList (s ++ t) ≡ toList s List.++ toList t
toList-++ s t = trustMe

length-++ : ∀ s t → length (s ++ t) ≡ length s + length t
length-++ s t = begin
  length (s ++ t)                         ≡⟨⟩
  List.length (toList (s ++ t))           ≡⟨ cong List.length (toList-++ s t) ⟩
  List.length (toList s List.++ toList t) ≡⟨ Listₚ.length-++ (toList s) ⟩
  length s + length t                     ∎

length-replicate : ∀ n {c} → length (replicate n c) ≡ n
length-replicate n {c} = let cs = List.replicate n c in begin
  length (replicate n c) ≡⟨ cong List.length (toList∘fromList cs) ⟩
  List.length cs         ≡⟨ Listₚ.length-replicate n ⟩
  n                      ∎


text:
module Formalization.ClassicalPropositionalLogic.Semantics where

import      Lvl
open import Data.Boolean
open import Data.Boolean.Stmt
open import Formalization.ClassicalPropositionalLogic.Syntax
open import Functional
open import Logic
import      Logic.Propositional as Logic
import      Logic.Predicate     as Logic
import      Sets.PredicateSet
open        Sets.PredicateSet.BoundedQuantifiers
open import Type

private variable ℓₚ ℓ ℓ₁ ℓ₂ : Lvl.Level

module _ where
  private variable P : Type{ℓₚ}

  -- Model.
  -- A model decides which propositional constants that are true or false.
  Model : Type{ℓₚ} → Type{ℓₚ}
  Model(P) = (P → Bool)

  -- Satisfication relation.
  -- (𝔐 ⊧ φ) means that the formula φ is satisfied in the model 𝔐.
  -- Or in other words: A formula is true in the model 𝔐.
  _⊧_ : Model(P) → Formula(P) → Stmt
  𝔐 ⊧ (• p)   = IsTrue(𝔐(p))   -- A model decides whether a propositional constant is satisifed.
  𝔐 ⊧ ⊤       = Logic.⊤        -- Any model satisfies top.
  𝔐 ⊧ ⊥       = Logic.⊥        -- No model satisfies bottom.
  𝔐 ⊧ (¬ φ)   = Logic.¬(𝔐 ⊧ φ) -- A model satisfies a negated proposition when it does not satisfy the proposition.
  𝔐 ⊧ (φ ∧ ψ) = (𝔐 ⊧ φ) Logic.∧ (𝔐 ⊧ ψ) -- A model satisfies a conjunction when it satisfies both of the propositions.
  𝔐 ⊧ (φ ∨ ψ) = (𝔐 ⊧ φ) Logic.∨ (𝔐 ⊧ ψ) -- A model satisfies a disjunction when it satisfies any one of the propositions.
  𝔐 ⊧ (φ ⟶ ψ) = Logic.¬(𝔐 ⊧ φ) Logic.∨ (𝔐 ⊧ ψ)
  𝔐 ⊧ (φ ⟷ ψ) = ((𝔐 ⊧ φ) Logic.∧ (𝔐 ⊧ ψ)) Logic.∨ (Logic.¬(𝔐 ⊧ φ) Logic.∧ Logic.¬(𝔐 ⊧ ψ))

  -- Satisfication of a set of formulas.
  -- This means that a model satisfies all formulas at the same time.
  _⊧₊_ : Model(P) → Formulas(P){ℓ} → Stmt
  𝔐 ⊧₊ Γ = ∀ₛ(Γ) (𝔐 ⊧_)

  -- Validity of a formula.
  -- A formula is valid when it is true independent of any model.
  Valid : Formula(P) → Stmt
  Valid(φ) = Logic.∀ₗ(_⊧ φ)

  -- Satisfiability of sets of formulas.
  -- A set of formulas is valid when there is a model that satisfies all of them at the same time.
  Satisfiable : Formulas(P){ℓ} → Stmt
  Satisfiable(Γ) = Logic.∃(_⊧₊ Γ)

  -- Unsatisfiability of sets of formulas.
  Unsatisfiable : Formulas(P){ℓ} → Stmt
  Unsatisfiable{ℓ} = Logic.¬_ ∘ Satisfiable{ℓ}

  -- Semantic entailment of a formula.
  -- A hypothetical statement. If a model would satisfy all formulas in Γ, then this same model satisifes the formula φ.
  _⊨_ : Formulas(P){ℓ} → Formula(P) → Stmt
  Γ ⊨ φ = ∀{𝔐} → (𝔐 ⊧₊ Γ) → (𝔐 ⊧ φ)

  _⊭_ : Formulas(P){ℓ} → Formula(P) → Stmt
  _⊭_ = Logic.¬_ ∘₂ _⊨_

  -- Axiomatization of a theory by a set of axioms.
  -- A set of axioms is a set of formulas.
  -- A theory is the closure of a set of axioms.
  -- An axiomatization is a subset of formulas of the theory which entails all formulas in the axiomatized theory.
  _axiomatizes_ : Formulas(P){ℓ₁} → Formulas(P){ℓ₂} → Stmt
  Γ₁ axiomatizes Γ₂ = ∀{φ} → (Γ₁ ⊨ φ) → Γ₂(φ)

  -- A set of formulas is closed when it includes all formulas that it entails.
  Closed : Formulas(P){ℓ} → Stmt
  Closed(Γ) = Γ axiomatizes Γ

  _⊨₊_ : Formulas(P){ℓ} → Formulas(P){ℓ} → Stmt
  Γ₁ ⊨₊ Γ₂ = ∀{𝔐} → (𝔐 ⊧₊ Γ₁) → (𝔐 ⊧₊ Γ₂)

  _⊭₊_ : Formulas(P){ℓ} → Formulas(P){ℓ} → Stmt
  _⊭₊_ = Logic.¬_ ∘₂ _⊨₊_

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda