text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Unsafe Float operations
------------------------------------------------------------------------

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

module Data.Float.Unsafe where

open import Data.Float
open import Data.Bool.Base using (false; true)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe

------------------------------------------------------------------------
-- Equality testing

infix 4 _≟_

_≟_ : (x y : Float) → Dec (x ≡ y)
x ≟ y with primFloatEquality x y
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _


text:
------------------------------------------------------------------------
-- Subsets of finite sets
------------------------------------------------------------------------

module Data.Fin.Subset where

open import Data.Nat
open import Data.Vec hiding (_∈_)
open import Data.Fin
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

infixr 2 _∈_ _∉_ _⊆_ _⊈_

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

data Side : Set where
  inside  : Side
  outside : Side

-- Partitions a finite set into two parts, the inside and the outside.

Subset : ℕ → Set
Subset = Vec Side

------------------------------------------------------------------------
-- Membership and subset predicates

_∈_ : ∀ {n} → Fin n → Subset n → Set
x ∈ p = p [ x ]= inside

_∉_ : ∀ {n} → Fin n → Subset n → Set
x ∉ p = ¬ (x ∈ p)

_⊆_ : ∀ {n} → Subset n → Subset n → Set
p₁ ⊆ p₂ = ∀ {x} → x ∈ p₁ → x ∈ p₂

_⊈_ : ∀ {n} → Subset n → Subset n → Set
p₁ ⊈ p₂ = ¬ (p₁ ⊆ p₂)

------------------------------------------------------------------------
-- Some specific subsets

all : ∀ {n} → Side → Subset n
all {zero}  _ = []
all {suc n} s = s ∷ all s

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

Nonempty : ∀ {n} (p : Subset n) → Set
Nonempty p = ∃ λ f → f ∈ p

Empty : ∀ {n} (p : Subset n) → Set
Empty p = ¬ Nonempty p

-- Point-wise lifting of properties.

Lift : ∀ {n} → (Fin n → Set) → (Subset n → Set)
Lift P p = ∀ {x} → x ∈ p → P x

ext: agda

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- Operations on nullary relations (like negation and decidability)
------------------------------------------------------------------------

-- Some operations on/properties of nullary relations, i.e. sets.

module Relation.Nullary where

open import Data.Product
import Relation.Nullary.Core as Core
open import Relation.Binary
open import Relation.Binary.FunctionSetoid
import Relation.Binary.EqReasoning as EqReasoning

------------------------------------------------------------------------
-- Negation

open Core public using (¬_)

------------------------------------------------------------------------
-- Equivalence

infix 3 _⇔_

_⇔_ : Set → Set → Set
P ⇔ Q = (P → Q) × (Q → P)

------------------------------------------------------------------------
-- Decidable relations

open Core public using (Dec; yes; no)

------------------------------------------------------------------------
-- Injections

Injective : ∀ {A B} → A ⟶ B → Set
Injective {A} {B} f = ∀ {x y} → f ⟨$⟩ x ≈₂ f ⟨$⟩ y → x ≈₁ y
  where
  open Setoid A renaming (_≈_ to _≈₁_)
  open Setoid B renaming (_≈_ to _≈₂_)

_LeftInverseOf_ : ∀ {A B} → B ⟶ A → A ⟶ B → Set
_LeftInverseOf_ {A} f g = ∀ x → f ⟨$⟩ (g ⟨$⟩ x) ≈₁ x
  where open Setoid A renaming (_≈_ to _≈₁_)

record Injection (From To : Setoid) : Set where
  field
    to        : From ⟶ To
    injective : Injective to

record LeftInverse (From To : Setoid) : Set where
  field
    to           : From ⟶ To
    from         : To ⟶ From
    left-inverse : from LeftInverseOf to

  open Setoid      From
  open EqReasoning From

  injective : Injective to
  injective {x} {y} eq = begin
    x                    ≈⟨ sym (left-inverse x) ⟩
    from ⟨$⟩ (to ⟨$⟩ x)  ≈⟨ pres from eq ⟩
    from ⟨$⟩ (to ⟨$⟩ y)  ≈⟨ left-inverse y ⟩
    y                    ∎

  injection : Injection From To
  injection = record { to = to; injective = injective }


text:
-- Andreas, 2019-09-13, AIM XXX, test for #4050 by gallais

-- Jesper, 2019-12-19, moved to test/Fail after unfix of #3823

record Wrap : Set₂ where
  field wrapped : Set₁

f : Wrap
f = record { M }
  module M where
    wrapped : Set₁
    wrapped = Set

-- Should be accepted.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module SimpleHoTT where

open import Data.Empty
open import Data.Sum renaming (map to _⊎→_)
open import Function renaming (_∘_ to _○_)

infixr 8  _∘_   -- path composition
infix  4  _≡_   -- propositional equality
infix  2  _∎       -- equational reasoning for paths
infixr 2  _≡⟨_⟩_   -- equational reasoning for paths

------------------------------------------------------------------------------
-- Equivalences a la HoTT (using HoTT paths and path induction)

-- Our own version of refl that makes 'a' explicit
data _≡_ {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where
  refl : (a : A) → (a ≡ a)

-- not sure where else to put this [Z]
hetType : {A B : Set} → (a : A) → A ≡ B → B
hetType a (refl _) = a

-- J
pathInd : ∀ {u ℓ} → {A : Set u} →
          (C : {x y : A} → x ≡ y → Set ℓ) →
          (c : (x : A) → C (refl x)) →
          ({x y : A} (p : x ≡ y) → C p)
pathInd C c (refl x) = c x

basedPathInd : {A : Set} → (a : A) → (C : (x : A) → (a ≡ x) → Set) →
  C a (refl a) → ((x : A) (p : a ≡ x) → C x p)
basedPathInd a C c .a (refl .a) = c

! : ∀ {u} → {A : Set u} {x y : A} → (x ≡ y) → (y ≡ x)
! = pathInd (λ {x} {y} _ → y ≡ x) refl

_∘_ : ∀ {u} → {A : Set u} → {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_∘_ {u} {A} {x} {y} {z} p q =
  pathInd {u}
    (λ {x} {y} p → ((z : A) → (q : y ≡ z) → (x ≡ z)))
    (λ x z q → pathInd (λ {x} {z} _ → x ≡ z) refl {x} {z} q)
    {x} {y} p z q

-- p = p . refl

unitTransR : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ p ∘ refl y)
unitTransR {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ p ∘ (refl y))
    (λ x → refl (refl x))
    {x} {y} p

-- p = refl . p

unitTransL : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ refl x ∘ p)
unitTransL {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ (refl x) ∘ p)
    (λ x → refl (refl x))
    {x} {y} p

ap : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {x y : A} →
     (f : A → B) → (x ≡ y) → (f x ≡ f y)
ap {ℓ} {ℓ'} {A} {B} {x} {y} f p =
  pathInd -- on p
    (λ {x} {y} p → f x ≡ f y)
    (λ x → refl (f x))
    {x} {y} p

ap2 : ∀ {ℓ ℓ' ℓ''} → {A : Set ℓ} {B : Set ℓ'} {C : Set ℓ''}
     {x₁ y₁ : A} {x₂ y₂ : B} →
     (f : A → B → C) → (x₁ ≡ y₁) → (x₂ ≡ y₂) → (f x₁ x₂  ≡ f y₁ y₂)
ap2 {ℓ} {ℓ'} {ℓ''} {A} {B} {C} {x₁} {y₁} {x₂} {y₂} f p₁ p₂ =
  pathInd -- on p₁
    (λ {x₁} {y₁} p₁ → f x₁ x₂ ≡ f y₁ y₂)
    (λ x →
      pathInd -- on p₂
        (λ {x₂} {y₂} p₂ → f x x₂ ≡ f x y₂)
        (λ y → refl (f x y))
        {x₂} {y₂} p₂)
    {x₁} {y₁} p₁

-- Abbreviations for path compositions

_≡⟨_⟩_ : ∀ {u} → {A : Set u} (x : A) {y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_ ≡⟨ p ⟩ q = p ∘ q

bydef : ∀ {u} → {A : Set u} {x : A} → (x ≡ x)
bydef {u} {A} {x} = refl x

_∎ : ∀ {u} → {A : Set u} (x : A) → x ≡ x
_∎ x = refl x

-- Transport; Lifting

transport : ∀ {ℓ ℓ'} → {A : Set ℓ} {x y : A} →
  (P : A → Set ℓ') → (p : x ≡ y) → P x → P y
transport {ℓ} {ℓ'} {A} {x} {y} P p =
  pathInd -- on p
    (λ {x} {y} p → (P x → P y))
    (λ _ → id)
    {x} {y} p

-- Lemma 2.3.10

transport-f : ∀ {ℓ ℓ' ℓ''} → {A : Set ℓ} {B : Set ℓ'} {x y : A} →
  (f : A → B) → (P : B → Set ℓ'') →
  (p : x ≡ y) → (u : P (f x)) →
  transport (P ○ f) p u ≡ transport P (ap f p) u
transport-f {ℓ} {ℓ'} {ℓ''} {A} {B} {x} {y} f P p u =
  pathInd -- on p
    (λ {x} {y} p → (u : P (f x)) →
      transport (P ○ f) p u ≡ transport P (ap f p) u)
    (λ x u → refl u)
    {x} {y} p u

-- Lemma 2.11.2

transportIdR : {A : Set} {a y z : A} → (p : y ≡ z) → (q : a ≡ y) →
  transport (λ x → a ≡ x) p q ≡ q ∘ p
transportIdR {A} {a} {y} {z} p q =
  pathInd
    (λ {y} {z} p → (q : a ≡ y) → transport (λ x → a ≡ x) p q ≡ q ∘ p)
    (λ y q → transport (λ x → a ≡ x) (refl y) q
               ≡⟨ bydef ⟩
             q
               ≡⟨ unitTransR q ⟩
             q ∘ refl y ∎)
    {y} {z} p q

transportIdL : {A : Set} {a y z : A} → (p : y ≡ z) → (q : y ≡ a) →
  transport (λ x → x ≡ a) p q ≡ ! p ∘ q
transportIdL {A} {a} {y} {z} p q =
  pathInd
    (λ {y} {z} p → (q : y ≡ a) → transport (λ x → x ≡ a) p q ≡ ! p ∘ q)
    (λ y q → transport (λ x → x ≡ a) (refl y) q
               ≡⟨ bydef ⟩
             q
               ≡⟨ unitTransL q ⟩
             ! (refl y) ∘ q ∎)
    {y} {z} p q

transportIdRefl : {A : Set} {y z : A} → (p : y ≡ z) → (q : y ≡ y) →
  transport (λ x → x ≡ x) p q ≡ ! p ∘ q ∘ p
transportIdRefl {A} {y} {z} p q =
  pathInd
    (λ {y} {z} p → (q : y ≡ y) → transport (λ x → x ≡ x) p q ≡ ! p ∘ q ∘ p)
    (λ y q → transport (λ x → x ≡ x) (refl y) q
               ≡⟨ bydef ⟩
             q
               ≡⟨ unitTransR q ⟩
             q ∘ refl y
               ≡⟨ unitTransL (q ∘ refl y) ⟩
             ! (refl y) ∘ q ∘ refl y ∎)
    {y} {z} p q

-- tools for coproducts (Sec. 2.12)

indCP : {A B : Set} → (C : A ⊎ B → Set) →
        ((a : A) → C (inj₁ a)) → ((b : B) → C (inj₂ b)) → ((x : A ⊎ B) → C x)
indCP C f g (inj₁ a) = f a
indCP C f g (inj₂ b) = g b

code : {A B : Set} → (a₀ : A) → A ⊎ B → Set
code a₀ (inj₁ a) = a₀ ≡ a
code a₀ (inj₂ b) = ⊥

encode : {A B : Set} → (a₀ : A) → (x : A ⊎ B) → (p : inj₁ a₀ ≡ x) → code a₀ x
encode {A} {B} a₀ x p = transport (code a₀) p (refl a₀)

decode : {A B : Set} → (a₀ : A) → (x : A ⊎ B) → (c : code a₀ x) → inj₁ a₀ ≡ x
decode a₀ (inj₁ a) c = ap inj₁ c
decode a₀ (inj₂ b) ()

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Oscar.Class.ThickAndThin where

open import Oscar.Data.Fin
open import Oscar.Data.Equality
open import Oscar.Data.Nat
open import Oscar.Data.Maybe

record ThickAndThin {a} (A : Nat → Set a) : Set a where
  field
    thin : ∀ {m} → Fin (suc m) → A m → A (suc m)
    thin-injective : ∀ {m} (x : Fin (suc m)) {y₁ y₂ : A m} → thin x y₁ ≡ thin x y₂ → y₁ ≡ y₂
    thick : ∀ {m} → A (suc m) → Fin m → A m
    thick∘thin=id : ∀ {m} (x : Fin m) (y : A m) → thick (thin (suc x) y) x ≡ y
    check : ∀ {m} → Fin (suc m) → A (suc m) → Maybe (A m)
    thin-check-id : ∀ {m} (x : Fin (suc m)) y → ∀ y' → thin x y' ≡ y → check x y ≡ just y'

open ThickAndThin ⦃ … ⦄ public

-- open import Oscar.Level

-- record ThickAndThin' {a} {A : Set a} (f : A → A) {b} (B : A → Set b) (g : ∀ {x} → B x → B (f x)) {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
--   field
--     thin : ∀ {n} → B (f n) → C n → C (f n)
--     thick : ∀ {n} → C (f n) → B n → C n
--     thin-injective : ∀ {n} (z : B (f n)) {x y : C n} → thin z x ≡ thin z y → x ≡ y
--     thick∘thin=id : ∀ {n} (x : B n) (y : C n) → thick (thin (g x) y) x ≡ y
--     check : ∀ {n} → B (f n) → C (f n) → Maybe (C n)
--     thin-check-id : ∀ {n} (x : B (f n)) y → ∀ y' → thin x y' ≡ y → check x y ≡ just y'

-- --open ThickAndThin' ⦃ … ⦄ public


text:
open import Mockingbird.Forest using (Forest)

module Mockingbird.Forest.Combination.Base {b ℓ} (forest : Forest {b} {ℓ}) where

open import Level using (Level; _⊔_)
open import Relation.Unary using (Pred; _∈_)

open Forest forest

private
  variable
    p : Level
    x y z : Bird
    P : Pred Bird p

-- If P is a set of birds, we can think of ⟨ P ⟩ as the set of birds ‘generated
-- by’ P.
data ⟨_⟩ (P : Pred Bird p) : Pred Bird (p ⊔ b ⊔ ℓ) where
  [_] : (x∈P : x ∈ P) → x ∈ ⟨ P ⟩

  _⟨∙⟩_∣_ :
       (x∈⟨P⟩ : x ∈ ⟨ P ⟩)
    → (y∈⟨P⟩ : y ∈ ⟨ P ⟩)
    → (xy≈z : x ∙ y ≈ z)
    → z ∈ ⟨ P ⟩

infixl 6 _⟨∙⟩_
_⟨∙⟩_ : x ∈ ⟨ P ⟩ → y ∈ ⟨ P ⟩ → x ∙ y ∈ ⟨ P ⟩
_⟨∙⟩_ = _⟨∙⟩_∣ refl

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


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

-- In this module, we define the syntax of D<:
module DsubDef where

open import Data.List as List
open import Data.List.All
open import Data.Nat as ℕ
open import Data.Maybe as Maybe
open import Data.Product
open import Data.Sum
open import Data.Empty renaming (⊥ to False)
open import Function

open import Data.Nat.Properties as ℕₚ
open import Data.Maybe.Properties as Maybeₚ
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Utils

infix 8 _∙A
infix 6 Π_∙_ ⟨A:_⋯_⟩

-- Types
--
-- Notations in Agda should be more readable than in Coq.
-- * ⊤ is a supertype of all types.
-- * ⊥ is a subtype of all types.
-- * (x ∙A) represents a path dependent type (x.A).
-- * (Π S ∙ U) represents a dependent function type (∀(x : S)U).
-- * (⟨A: S ⋯ U ⟩) represents a type declaration ({A : S .. U}).
data Typ : Set where
  ⊤       : Typ
  ⊥       : Typ
  _∙A     : (n : ℕ) → Typ
  Π_∙_    : (S U : Typ) → Typ
  ⟨A:_⋯_⟩ : (S U : Typ) → Typ

-- typing context
Env : Set
Env = List Typ

-- shifting operation of de Bruijn indices
infixl 7 _↑_
_↑_ : Typ → ℕ → Typ
⊤ ↑ n           = ⊤
⊥ ↑ n           = ⊥
(x ∙A) ↑ n with n ≤? x
... | yes n≤x   = suc x ∙A
... | no n>x    = x ∙A
(Π S ∙ U) ↑ n   = Π S ↑ n ∙ U ↑ suc n
⟨A: S ⋯ U ⟩ ↑ n = ⟨A: S ↑ n ⋯ U ↑ n ⟩

-- The remaining are technical setup.
infix 4 _↦_∈_
data _↦_∈_ : ℕ → Typ → Env → Set where
  hd : ∀ {T Γ} → 0 ↦ T ↑ 0 ∈ T ∷ Γ
  tl : ∀ {n T T′ Γ} → n ↦ T ∈ Γ → suc n ↦ T ↑ 0 ∈ T′ ∷ Γ

env-lookup : Env → ℕ → Maybe Typ
env-lookup Γ n = Maybe.map (repeat (suc n) (_↑ 0)) (lookupOpt Γ n)

↦∈⇒lookup : ∀ {x T Γ} → x ↦ T ∈ Γ → env-lookup Γ x ≡ just T
↦∈⇒lookup hd = refl
↦∈⇒lookup {x} {_} {Γ} (tl T∈Γ) with lookupOpt Γ x | ↦∈⇒lookup T∈Γ
... | just T′ | eq = cong (just ∘ (_↑ zero)) (just-injective eq)
... | nothing | ()

lookup⇒↦∈ : ∀ {x T Γ} → env-lookup Γ x ≡ just T → x ↦ T ∈ Γ
lookup⇒↦∈ {x} {_} {[]} ()
lookup⇒↦∈ {zero} {_} {T ∷ Γ} refl = hd
lookup⇒↦∈ {suc x} {_} {T ∷ Γ} eq with lookupOpt Γ x | λ {T} → lookup⇒↦∈ {x} {T} {Γ}
lookup⇒↦∈ refl | just T′ | rec = tl $ rec refl
lookup⇒↦∈ ()   | nothing | _

⟨A:⟩-injective : ∀ {S U S′ U′} → ⟨A: S ⋯ U ⟩ ≡ ⟨A: S′ ⋯ U′ ⟩ → S ≡ S′ × U ≡ U′
⟨A:⟩-injective refl = refl , refl

↑-idx : ℕ → ℕ → ℕ
↑-idx x n with n ≤? x
... | yes p = suc x
... | no ¬p = x

↑-var : ∀ x n → x ∙A ↑ n ≡ ↑-idx x n ∙A
↑-var x n with n ≤? x
... | yes p = refl
... | no ¬p = refl

↑-↑-comm : ∀ T m n → m ≤ n → T ↑ m ↑ suc n ≡ T ↑ n ↑ m
↑-↑-comm ⊤ m n m≤n                                  = refl
↑-↑-comm ⊥ m n m≤n                                  = refl
↑-↑-comm (x ∙A) m n m≤n with n ≤? x
... | yes n≤x
    rewrite ≤?-yes (≤-trans m≤n n≤x)
          | ≤?-yes n≤x
          | ≤?-yes (≤-step (≤-trans m≤n n≤x))       = refl
... | no n>x with m ≤? x
...             | yes m≤x rewrite proj₂ $ ≤?-no n>x = refl
...             | no m>x with suc n ≤? x
...                         | yes 1+n≤x             = ⊥-elim (m>x (≤-trans (≤-step m≤n) 1+n≤x))
...                         | no 1+n>x              = refl
↑-↑-comm (Π S ∙ U) m n m≤n
  rewrite ↑-↑-comm S m n m≤n
        | ↑-↑-comm U (suc m) (suc n) (s≤s m≤n)      = refl
↑-↑-comm ⟨A: S ⋯ U ⟩ m n m≤n
  rewrite ↑-↑-comm S m n m≤n | ↑-↑-comm U m n m≤n   = refl

-- These two judgments are about to capture the characteristics of the image of
-- interpretation functions from F<:⁻ to D<:.
--
-- Covar quantifies the types in D<: which appears in the covariant positions in the
-- image of the interpretation function.
data Covar : Typ → Set where
  cv⊤  : Covar ⊤
  cv∙A : ∀ n → Covar (n ∙A)
  cvΠ  : ∀ {S U} → Covar S → Covar U → Covar (Π ⟨A: ⊥ ⋯ S ⟩ ∙ U)

-- Contra quantifies the types in D<: which appears in the contravariant positions in
-- the image of the interpretation function.
data Contra : Typ → Set where
  ctt : ∀ {T} → Covar T → Contra ⟨A: ⊥ ⋯ T ⟩

ContraEnv : Env → Set
ContraEnv = All Contra

↑-Covar : ∀ {T} n → Covar T → Covar (T ↑ n)
↑-Covar n cv⊤       = cv⊤
↑-Covar n (cv∙A x)
  rewrite ↑-var x n = cv∙A _
↑-Covar n (cvΠ S U) = cvΠ (↑-Covar n S) (↑-Covar (suc n) U)

↑-Contra : ∀ {T} n → Contra T → Contra (T ↑ n)
↑-Contra n (ctt T) = ctt (↑-Covar n T)

↑-injective : ∀ {S U n} → S ↑ n ≡ U ↑ n → S ≡ U
↑-injective {⊤} {⊤} {n} eq = refl
↑-injective {⊤} {⊥} {n} ()
↑-injective {⊤} {x ∙A} {n} eq
  rewrite ↑-var x n        = case eq of λ ()
↑-injective {⊤} {Π S ∙ U} {n} ()
↑-injective {⊤} {⟨A: S ⋯ U ⟩} {n} ()
↑-injective {⊥} {⊤} {n} ()
↑-injective {⊥} {⊥} {n} eq = refl
↑-injective {⊥} {x ∙A} {n} eq
  rewrite ↑-var x n        = case eq of λ ()
↑-injective {⊥} {Π S ∙ U} {n} ()
↑-injective {⊥} {⟨A: S ⋯ U ⟩} {n} ()
↑-injective {x ∙A} {⊤} {n} eq
  rewrite ↑-var x n        = case eq of λ ()
↑-injective {x ∙A} {⊥} {n} eq
  rewrite ↑-var x n        = case eq of λ ()
↑-injective {x ∙A} {y ∙A} {n} eq
  with n ≤? x | n ≤? y
↑-injective {x ∙A} {y ∙A} {n} refl
    | yes n≤x | yes n≤y    = refl
↑-injective {x ∙A} {y ∙A} {n} refl
    | yes n≤x | no n>y     = ⊥-elim (n>y (≤-step n≤x))
↑-injective {x ∙A} {y ∙A} {n} refl
    | no n>x  | yes n≤y    = ⊥-elim (n>x (≤-step n≤y))
↑-injective {x ∙A} {y ∙A} {n} refl
    | no n>x  | no n>y     = refl
↑-injective {x ∙A} {Π S ∙ U} {n} eq
  rewrite ↑-var x n        = case eq of λ ()
↑-injective {x ∙A} {⟨A: S ⋯ U ⟩} {n} eq
  rewrite ↑-var x n        = case eq of λ ()
↑-injective {Π S ∙ U} {⊤} {n} ()
↑-injective {Π S ∙ U} {⊥} {n} ()
↑-injective {Π S ∙ U} {x ∙A} {n} eq
  rewrite ↑-var x n        = case eq of λ ()
↑-injective {Π S ∙ U} {Π S′ ∙ U′} {n} eq
  with S ↑ n | U ↑ suc n | S′ ↑ n | U′ ↑ suc n
     | ↑-injective {S} {S′} {n} | ↑-injective {U} {U′} {suc n}
...  | _ | _ | _ | _ | rec₁ | rec₂
     with eq
...     | refl             = cong₂ Π_∙_ (rec₁ refl) (rec₂ refl)
↑-injective {Π S ∙ U} {⟨A: _ ⋯ _ ⟩} {n} ()
↑-injective {⟨A: S ⋯ U ⟩} {⊤} {n} ()
↑-injective {⟨A: S ⋯ U ⟩} {⊥} {n} ()
↑-injective {⟨A: S ⋯ U ⟩} {x ∙A} {n} eq
  rewrite ↑-var x n        = case eq of λ ()
↑-injective {⟨A: S ⋯ U ⟩} {Π _ ∙ _} {n} ()
↑-injective {⟨A: S ⋯ U ⟩} {⟨A: S′ ⋯ U′ ⟩} {n} eq
  with S ↑ n | U ↑ n | S′ ↑ n | U′ ↑ n
     | ↑-injective {S} {S′} {n} | ↑-injective {U} {U′} {n}
...  | _ | _ | _ | _ | rec₁ | rec₂
     with eq
...     | refl             = cong₂ ⟨A:_⋯_⟩ (rec₁ refl) (rec₂ refl)

↑-⊥-inv : ∀ {S n} → S ↑ n ≡ ⊥ → S ≡ ⊥
↑-⊥-inv {⊤} {n} ()
↑-⊥-inv {⊥} {n} refl = refl
↑-⊥-inv {x ∙A} {n} eq
  rewrite ↑-var x n  = case eq of λ ()
↑-⊥-inv {Π _ ∙ _} {n} ()
↑-⊥-inv {⟨A: _ ⋯ _ ⟩} {n} ()

⟨A:⟩-↑-inv : ∀ {T n S U} → ⟨A: S ⋯ U ⟩ ≡ T ↑ n → ∃₂ λ S′ U′ → T ≡ ⟨A: S′ ⋯ U′ ⟩ × S ≡ S′ ↑ n × U ≡ U′ ↑ n
⟨A:⟩-↑-inv {⊤} ()
⟨A:⟩-↑-inv {⊥} ()
⟨A:⟩-↑-inv {x ∙A} {n} eq
  rewrite ↑-var x n             = case eq of λ ()
⟨A:⟩-↑-inv {Π _ ∙ _} ()
⟨A:⟩-↑-inv {⟨A: S′ ⋯ U′ ⟩} refl = S′ , U′ , refl , refl , refl

↦∈ContraEnv : ∀ {Γ n T} → n ↦ T ∈ Γ → ContraEnv Γ → Contra T
↦∈ContraEnv hd (T ∷ cT)       = ↑-Contra 0 T
↦∈ContraEnv (tl T∈Γ) (_ ∷ cT) = ↑-Contra 0 (↦∈ContraEnv T∈Γ cT)

lookupContraEnv : ∀ {Γ n T} → env-lookup Γ n ≡ just T → ContraEnv Γ → Contra T
lookupContraEnv lk cT = ↦∈ContraEnv (lookup⇒↦∈ lk) cT

lookupContraBot : ∀ {Γ n} → ContraEnv Γ → ¬ env-lookup Γ n ≡ just ⊥
lookupContraBot all eq with lookupContraEnv eq all
... | ()

lookupContraBndBot : ∀ {Γ n S} → ContraEnv Γ → ¬ env-lookup Γ n ≡ just ⟨A: S ⋯ ⊥ ⟩
lookupContraBndBot all eq with lookupContraEnv eq all
... | ctt ()

lookupContraBndBnd : ∀ {Γ n T S U} → ContraEnv Γ →
                       ¬ env-lookup Γ n ≡ just ⟨A: T ⋯ ⟨A: S ⋯ U ⟩ ⟩
lookupContraBndBnd all eq with lookupContraEnv eq all
... | ctt ()

lookupContra⊥Lb : ∀ {Γ n S U} → ContraEnv Γ →
                    env-lookup Γ n ≡ just ⟨A: S ⋯ U ⟩ → S ≡ ⊥
lookupContra⊥Lb all eq with lookupContraEnv eq all
... | ctt _ = refl

Typ-measure : Typ → ℕ
Typ-measure ⊤           = 1
Typ-measure ⊥           = 1
Typ-measure (_ ∙A)      = 2
Typ-measure (Π S ∙ U)   = 1 + Typ-measure S + Typ-measure U
Typ-measure ⟨A: S ⋯ U ⟩ = 1 + Typ-measure S + Typ-measure U

Typ-measure-↑ : ∀ T n → Typ-measure (T ↑ n) ≡ Typ-measure T
Typ-measure-↑ ⊤ n                 = refl
Typ-measure-↑ ⊥ n                 = refl
Typ-measure-↑ (x ∙A) n
  rewrite ↑-var x n               = refl
Typ-measure-↑ (Π S ∙ U) n
  rewrite Typ-measure-↑ S n
        | Typ-measure-↑ U (suc n) = refl
Typ-measure-↑ ⟨A: S ⋯ U ⟩ n
  rewrite Typ-measure-↑ S n
        | Typ-measure-↑ U n       = refl

-- Definition of Invertible Contexts
--
-- As per Definition 9, we define a predicate for invertible contexts.
record InvertibleEnv (P : Env → Set) : Set where
  field
    no-⊥       : ∀ {Γ n} → P Γ → ¬ env-lookup Γ n ≡ just ⊥
    no-bnd-⊥   : ∀ {Γ n S} → P Γ → ¬ env-lookup Γ n ≡ just ⟨A: S ⋯ ⊥ ⟩
    no-bnd-bnd : ∀ {Γ n T S U} → P Γ → ¬ env-lookup Γ n ≡ just ⟨A: T ⋯ ⟨A: S ⋯ U ⟩ ⟩
    ⊥-lb       : ∀ {Γ n S U} → P Γ → env-lookup Γ n ≡ just ⟨A: S ⋯ U ⟩ → S ≡ ⊥

contraInvertible : InvertibleEnv ContraEnv
contraInvertible = record
  { no-⊥       = lookupContraBot
  ; no-bnd-⊥   = lookupContraBndBot
  ; no-bnd-bnd = lookupContraBndBnd
  ; ⊥-lb       = lookupContra⊥Lb
  }

-- Properties of Invertible Contexts
--
-- Just by knowing the contexts being invertible, we can already derive many
-- properties of D<:. In the following module, we show that in invertible contexts,
-- inversion properties are recovered. For technical reasons, we leave the subtyping
-- judgment open in order to accomodate multiple definition of subtyping in D<:.
--
-- These properties are discussed in Section 4.4.
module InvertibleProperties {P : Env → Set}
                            (invertible : InvertibleEnv P)
                            (_⊢_<:_ : Env → Typ → Typ → Set) where
  open InvertibleEnv invertible public

  -- We define <:ᵢ to describe a fragment of <: under the restriction of invertible contexts.
  infix 4 _⊢ᵢ_<:_
  data _⊢ᵢ_<:_ : Env → Typ → Typ → Set where
    ditop   : ∀ {Γ T} → Γ ⊢ᵢ T <: ⊤
    dibot   : ∀ {Γ T} → Γ ⊢ᵢ ⊥ <: T
    direfl  : ∀ {Γ T} → Γ ⊢ᵢ T <: T
    ditrans : ∀ {Γ S U} T →
                (S<:T : Γ ⊢ᵢ S <: T) →
                (T<:U : Γ ⊢ᵢ T <: U) →
                Γ ⊢ᵢ S <: U
    dibnd   : ∀ {Γ S U S′ U′} →
                (S′<:S : Γ ⊢ᵢ S′ <: S) →
                (U<:U′ : Γ ⊢ᵢ U <: U′) →
                Γ ⊢ᵢ ⟨A: S ⋯ U ⟩ <: ⟨A: S′ ⋯ U′ ⟩
    diall   : ∀ {Γ S U S′ U′} →
                (S′<:S : Γ ⊢ᵢ S′ <: S) →
                (U<:U′ : (Γ ‣ S′ !) ⊢ U <: U′) →
                Γ ⊢ᵢ Π S ∙ U <: Π S′ ∙ U′
    disel   : ∀ {Γ n U} →
                (T∈Γ : env-lookup Γ n ≡ just ⟨A: ⊥ ⋯ U ⟩) →
                Γ ⊢ᵢ n ∙A <: U

  module _ where

    ⊤<: : ∀ {Γ T} → Γ ⊢ᵢ ⊤ <: T → T ≡ ⊤
    ⊤<: ditop  = refl
    ⊤<: direfl = refl
    ⊤<: (ditrans T S<:T T<:U) with ⊤<: S<:T
    ... | refl = ⊤<: T<:U

    <:⊥ : ∀ {Γ T} → Γ ⊢ᵢ T <: ⊥ → P Γ → T ≡ ⊥
    <:⊥ dibot pΓ       = refl
    <:⊥ direfl pΓ      = refl
    <:⊥ (ditrans T S<:T T<:U) pΓ with <:⊥ T<:U pΓ
    ... | refl         = <:⊥ S<:T pΓ
    <:⊥ (disel T∈Γ) pΓ = ⊥-elim (no-bnd-⊥ pΓ T∈Γ)

    ⟨A:⟩<: : ∀ {Γ T S U} → Γ ⊢ᵢ ⟨A: S ⋯ U ⟩ <: T → T ≡ ⊤ ⊎ ∃₂ (λ S′ U′ → T ≡ ⟨A: S′ ⋯ U′ ⟩)
    ⟨A:⟩<: ditop            = inj₁ refl
    ⟨A:⟩<: direfl           = inj₂ (-, -, refl)
    ⟨A:⟩<: (ditrans T S<:T T<:U) with ⟨A:⟩<: S<:T
    ... | inj₁ refl         = inj₁ (⊤<: T<:U)
    ... | inj₂ (_ , _ , refl) with ⟨A:⟩<: T<:U
    ... | inj₁ eq           = inj₁ eq
    ... | inj₂ (_ , _ , eq) = inj₂ (-, -, eq)
    ⟨A:⟩<: (dibnd D₁ D₂)    = inj₂ (-, -, refl)

    <:⟨A:⟩ : ∀ {Γ T S U} → Γ ⊢ᵢ T <: ⟨A: S ⋯ U ⟩ → P Γ →
               T ≡ ⊥ ⊎ ∃₂ (λ S′ U′ → T ≡ ⟨A: S′ ⋯ U′ ⟩)
    <:⟨A:⟩ dibot pΓ           = inj₁ refl
    <:⟨A:⟩ direfl pΓ          = inj₂ (-, -, refl)
    <:⟨A:⟩ (ditrans T S<:T T<:U) pΓ with <:⟨A:⟩ T<:U pΓ
    ... | inj₁ refl           = inj₁ (<:⊥ S<:T pΓ)
    ... | inj₂ (S′ , U′ , refl) with <:⟨A:⟩ S<:T pΓ
    ... | inj₁ eq             = inj₁ eq
    ... | inj₂ (S″ , U″ , eq) = inj₂ (S″ , U″ , eq)
    <:⟨A:⟩ (dibnd D₁ D₂) pΓ   = inj₂ (-, -, refl)
    <:⟨A:⟩ (disel T∈Γ) pΓ     = ⊥-elim (no-bnd-bnd pΓ T∈Γ)

    ⟨A:⟩<:⟨A:⟩ : ∀ {Γ S S′ U U′} → Γ ⊢ᵢ ⟨A: S ⋯ U ⟩ <: ⟨A: S′ ⋯ U′ ⟩ → P Γ →
                   Γ ⊢ᵢ S′ <: S × Γ ⊢ᵢ U <: U′
    ⟨A:⟩<:⟨A:⟩ direfl pΓ                  = direfl , direfl
    ⟨A:⟩<:⟨A:⟩ (ditrans T S<:T T<:U) pΓ with ⟨A:⟩<: S<:T
    ... | inj₁ refl with ⊤<: T<:U
    ... | ()
    ⟨A:⟩<:⟨A:⟩ (ditrans T S<:T T<:U) pΓ | inj₂ (_ , _ , refl)
      with ⟨A:⟩<:⟨A:⟩ S<:T pΓ | ⟨A:⟩<:⟨A:⟩ T<:U pΓ
    ... | S″<:S , U<:U″ | S′<:S″ , U″<:U′ = ditrans _ S′<:S″ S″<:S , ditrans _ U<:U″ U″<:U′
    ⟨A:⟩<:⟨A:⟩ (dibnd D₁ D₂) pΓ           = D₁ , D₂

    infix 4 _reach_from_
    data _reach_from_ : Env → Typ → ℕ → Set where
      /_/ : ∀ {Γ n T} →
              env-lookup Γ n ≡ just ⟨A: ⊥ ⋯ T ⟩ →
              Γ reach T from n
      _∷_ : ∀ {Γ n m T} →
              env-lookup Γ n ≡ just ⟨A: ⊥ ⋯ m ∙A ⟩ →
              Γ reach T from m →
              Γ reach T from n

    rf-concat : ∀ {Γ T m n} → Γ reach T from m → Γ reach m ∙A from n → Γ reach T from n
    rf-concat m↝T / B∈Γ /       = B∈Γ ∷ m↝T
    rf-concat m↝T (B∈Γ ∷ n↝m∙A) = B∈Γ ∷ rf-concat m↝T n↝m∙A

    ∙A<: : ∀ {Γ n T} → Γ ⊢ᵢ n ∙A <: T →
             T ≡ ⊤ ⊎ T ≡ n ∙A ⊎ ∃ λ T′ → Γ reach T′ from n × Γ ⊢ᵢ T′ <: T
    ∙A<: ditop                            = inj₁ refl
    ∙A<: direfl                           = inj₂ (inj₁ refl)
    ∙A<: (ditrans T S<:T T<:U) with ∙A<: S<:T
    ... | inj₁ refl                       = inj₁ (⊤<: T<:U)
    ... | inj₂ (inj₁ refl)                = ∙A<: T<:U
    ... | inj₂ (inj₂ (T′ , n↝T′ , T′<:T)) = inj₂ (inj₂ (T′ , n↝T′ , ditrans _ T′<:T T<:U))
    ∙A<: (disel T∈Γ)                      = inj₂ (inj₂ (-, / T∈Γ / , direfl))

    <:∙A : ∀ {Γ n T} → Γ ⊢ᵢ T <: n ∙A → P Γ →
             T ≡ ⊥ ⊎
             T ≡ n ∙A ⊎
             ∃ (λ m → T ≡ m ∙A × Γ reach n ∙A from m)
    <:∙A dibot pΓ                             = inj₁ refl
    <:∙A direfl pΓ                            = inj₂ (inj₁ refl)
    <:∙A (ditrans T S<:T T<:U) pΓ with <:∙A T<:U pΓ
    ... | inj₁ refl                           = inj₁ (<:⊥ S<:T pΓ)
    ... | inj₂ (inj₁ refl)                    = <:∙A S<:T pΓ
    ... | inj₂ (inj₂ (m , refl , m↝n∙A))
        with <:∙A S<:T pΓ
    ...    | inj₁ refl                        = inj₁ refl
    ...    | inj₂ (inj₁ refl)                 = inj₂ (inj₂ (-, refl , m↝n∙A))
    ...    | inj₂ (inj₂ (m′ , refl , m′↝m∙A)) = inj₂ (inj₂ (-, refl , rf-concat m↝n∙A m′↝m∙A))
    <:∙A (disel T∈Γ) pΓ                       = inj₂ (inj₂ (-, refl , / T∈Γ /))

    Π<: : ∀ {Γ S U T} → Γ ⊢ᵢ Π S ∙ U <: T →
            T ≡ ⊤ ⊎ ∃₂ (λ S′ U′ → T ≡ Π S′ ∙ U′)
    Π<: ditop                 = inj₁ refl
    Π<: direfl                = inj₂ (-, -, refl)
    Π<: (ditrans T S<:T T<:U) with Π<: S<:T
    ... | inj₁ refl           = inj₁ (⊤<: T<:U)
    ... | inj₂ (_ , _ , refl) = Π<: T<:U
    Π<: (diall D₁ D₂)         = inj₂ (-, -, refl)

    <:Π : ∀ {Γ S U T} → Γ ⊢ᵢ T <: Π S ∙ U → P Γ →
            T ≡ ⊥ ⊎
            ∃ (λ n → T ≡ n ∙A) ⊎
            ∃₂ (λ S′ U′ → T ≡ Π S′ ∙ U′)
    <:Π dibot pΓ                       = inj₁ refl
    <:Π direfl pΓ                      = inj₂ (inj₂ (-, -, refl))
    <:Π (ditrans T S<:T T<:U) pΓ with <:Π T<:U pΓ
    ... | inj₁ refl                    = inj₁ (<:⊥ S<:T pΓ)
    ... | inj₂ (inj₁ (_ , refl)) with <:∙A S<:T pΓ
    ... | inj₁ eq                      = inj₁ eq
    ... | inj₂ (inj₁ eq)               = inj₂ (inj₁ (-, eq))
    ... | inj₂ (inj₂ (_ , eq , _))     = inj₂ (inj₁ (-, eq))
    <:Π (ditrans T S<:T T<:U) pΓ | inj₂ (inj₂ (_ , _ , refl))
                                       = <:Π S<:T pΓ
    <:Π (diall D₁ D₂) pΓ               = inj₂ (inj₂ (-, -, refl))
    <:Π (disel T∈Γ) pΓ                 = inj₂ (inj₁ (-, refl))

-- Terms and Values
infix 6 var_ val_
infix 6 ⟨A=_⟩ _$$_
infixr 7 lt_inn_
infixr 6 Λ_∙_

mutual
  -- Values
  --
  -- * (⟨A= T ⟩) represents a type tag ({A = T}).
  -- * (Λ T ∙ t) represents a lambda expression (λ(x : T)t)
  data Val : Set where
    ⟨A=_⟩  : (T : Typ) → Val
    Λ_∙_   : (T : Typ) → (t : Trm) → Val

  -- Terms
  --
  -- * (var x) represents a variable.
  -- * (val v) represents a value as a term.
  -- * (x $$ y) is an application of two variables.
  -- * (lt t inn u) represents let binding (let x = t in u).
  data Trm  : Set where
    var_    : ℕ → Trm
    val_    : (v : Val) → Trm
    _$$_    : (x y : ℕ) → Trm
    lt_inn_ : Trm → Trm → Trm

-- substitution operation
record Subst (T : Set) : Set where
  infixl 5 _[_/_]
  field
    _[_/_] : T → ℕ → ℕ → T

open Subst {{...}} public

infixl 5 _[_/_]ᵥ _[_/_]ₜ _[_/_]T

ℕsubst : ℕ → ℕ → ℕ → ℕ
ℕsubst x n m with x ≟ m
... | yes x≡m = n
... | no x≢m  = x

instance
  substℕ : Subst ℕ
  substℕ = record { _[_/_] = ℕsubst }

_[_/_]T : Typ → ℕ → ℕ → Typ
⊤ [ n / m ]T           = ⊤
⊥ [ n / m ]T           = ⊥
x ∙A [ n / m ]T        = (x [ n / m ]) ∙A
Π S ∙ U [ n / m ]T     = Π S [ n / m ]T ∙ (U [ suc n / suc m ]T)
⟨A: S ⋯ U ⟩ [ n / m ]T = ⟨A: S [ n / m ]T ⋯ U [ n / m ]T ⟩

instance
  substTyp : Subst Typ
  substTyp = record { _[_/_] = _[_/_]T }

mutual
  _[_/_]ᵥ : Val → ℕ → ℕ → Val
  ⟨A= T ⟩ [ n / m ]ᵥ = ⟨A= T [ n / m ] ⟩
  Λ T ∙ t [ n / m ]ᵥ = Λ T [ n / m ] ∙ (t [ suc n / suc m ]ₜ)

  _[_/_]ₜ : Trm → ℕ → ℕ → Trm
  var x [ n / m ]ₜ      = var (x [ n / m ])
  val v [ n / m ]ₜ      = val (v [ n / m ]ᵥ)
  x $$ y [ n / m ]ₜ     = (x [ n / m ]) $$ (y [ n / m ])
  lt t inn u [ n / m ]ₜ = lt (t [ n / m ]ₜ) inn (u [ suc n / suc m ]ₜ)

instance
  substVal : Subst Val
  substVal = record { _[_/_] = _[_/_]ᵥ }

  substTrm : Subst Trm
  substTrm = record { _[_/_] = _[_/_]ₜ }

data Closed : ℕ → Typ → Set where
  cl-⊤   : ∀ {n} → Closed n ⊤
  cl-⊥   : ∀ {n} → Closed n ⊥
  cl-∙A  : ∀ {n m} (m≥n : m ≥ n) → Closed n (m ∙A)
  cl-Π   : ∀ {n S U} → Closed n S → Closed (suc n) U → Closed n (Π S ∙ U)
  cl-⟨A⟩ : ∀ {n S U} → Closed n S → Closed n U → Closed n ⟨A: S ⋯ U ⟩

infix 7 _↓
_↓ : ∀ {n T} → Closed (suc n) T → Typ
cl-⊤ ↓              = ⊤
cl-⊥ ↓              = ⊥
cl-∙A {_} {m} m≥n ↓ = pred m ∙A
cl-Π S U ↓          = Π S ↓ ∙ (U ↓)
cl-⟨A⟩ S U ↓        = ⟨A: S ↓ ⋯ U ↓ ⟩


text:
{-# OPTIONS --safe --cubical-compatible --no-universe-polymorphism --no-sized-types --no-guardedness #-}
module Issue2487-1 where

import Issue2487.Coinfective


text:
-- Andreas, 2012-01-11
module Issue551b where

data Box (A : Set) : Set where
  [_] : .A → Box A

implicit : {A : Set}{{a : A}} -> A
implicit {{a}} = a

postulate
  A B : Set
  instance a : A

a' : Box A
a' = [ implicit ]
-- this should succeed

f : Box B → Box (Box B)
f [ x ] = [ [ x ] ]
-- this as well

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- Yet another implementation of the Fibonacci sequence using tail
------------------------------------------------------------------------

module LargeCombinators where

open import Codata.Musical.Notation
open import Codata.Musical.Stream as S using (Stream; _∷_; _≈_)
open import Data.Nat
import Relation.Binary.PropositionalEquality as P

-- Stream programs. Note that the destructor tail is encapsulated in a
-- larger combinator, which also incorporates a constructor. This
-- ensures that the combinator can be used freely, with no risk of
-- destroying productivity.
--
-- Note that, in the general case, the implementation of whnf for the
-- "large combinator" may be quite tricky. In this case the
-- implementation turns out to be very simple, though.
--
-- The idea to use a "large combinator" is due to Thorsten Altenkirch.

infixr 5 _∷_

data StreamP (A : Set) : Set where
  _∷_     : (x : A) (xs : ∞ (StreamP A)) → StreamP A
  zipWith : (f : A → A → A) (xs ys : StreamP A) → StreamP A

  -- The intention is that ⟦ x ∷zipWith f · xs [tail ys ] ⟧P should be
  -- equal to x ∷ ♯ S.zipWith f ⟦ xs ⟧P (S.tail ⟦ ys ⟧P).

  _∷zipWith_·_[tail_] :
    (x : A) (f : A → A → A) (xs ys : StreamP A) → StreamP A

-- WHNFs.

data StreamW (A : Set) : Set where
  _∷_ : (x : A) (xs : StreamP A) → StreamW A

-- Stream programs can be turned into streams.

whnf : ∀ {A} → StreamP A → StreamW A
whnf (x ∷ xs) = x ∷ ♭ xs
whnf (x ∷zipWith f · xs′ [tail ys ]) with whnf ys
... | _ ∷ ys′ = x ∷ zipWith f xs′ ys′
whnf (zipWith f xs ys) with whnf xs | whnf ys
... | x ∷ xs′ | y ∷ ys′ = f x y ∷ zipWith f xs′ ys′

mutual

  ⟦_⟧W : ∀ {A} → StreamW A → Stream A
  ⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧P

  ⟦_⟧P : ∀ {A} → StreamP A → Stream A
  ⟦ xs ⟧P = ⟦ whnf xs ⟧W

-- The Fibonacci sequence.

fib : StreamP ℕ
fib = 0 ∷ ♯ (1 ∷zipWith _+_ · fib [tail fib ])

-- ⟦_⟧P is homomorphic with respect to zipWith/S.zipWith.

zipWith-hom :
  ∀ {A} (f : A → A → A) (xs ys : StreamP A) →
  ⟦ zipWith f xs ys ⟧P ≈ S.zipWith f ⟦ xs ⟧P ⟦ ys ⟧P
zipWith-hom f xs ys with whnf xs | whnf ys
... | x ∷ xs′ | y ∷ ys′ = P.refl ∷ ♯ zipWith-hom f xs′ ys′

-- The stream ⟦ fib ⟧P satisfies its intended defining equation.

fib-correct :
  ⟦ fib ⟧P ≈ 0 ∷ ♯ (1 ∷ ♯ (S.zipWith _+_ ⟦ fib ⟧P (S.tail ⟦ fib ⟧P)))
fib-correct =
  P.refl ∷ ♯ (P.refl ∷ ♯
    zipWith-hom _+_ fib (1 ∷zipWith _+_ · fib [tail fib ]))

-- For completeness, let us show that _∷zipWith_·_[tail_] is correctly
-- implemented.

open import Relation.Binary.PropositionalEquality as P using (_≡_; [_])

_∷zipWith_·_[tail_]-hom :
  ∀ {A} (x : A) (f : A → A → A) (xs ys : StreamP A) →
  ⟦ x ∷zipWith f · xs [tail ys ] ⟧P ≈
  x ∷ ♯ S.zipWith f ⟦ xs ⟧P (S.tail ⟦ ys ⟧P)
x ∷zipWith f · xs [tail ys ]-hom with whnf ys | P.inspect whnf ys
... | y ∷ ys′ | [ eq ] = P.refl ∷ ♯ helper eq
  where
  helper : whnf ys ≡ y ∷ ys′ →
           ⟦ zipWith f xs ys′ ⟧P ≈
           S.zipWith f ⟦ xs ⟧P (S.tail ⟦ ys ⟧P)
  helper eq rewrite eq = zipWith-hom f xs ys′

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
------------------------------------------------------------------------------
-- Inductive PA properties
------------------------------------------------------------------------------

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

module PA.Inductive.PropertiesI where

open import PA.Inductive.Base
open import PA.Inductive.Relation.Binary.EqReasoning

------------------------------------------------------------------------------
-- Congruence properties

succCong : ∀ {m n} → m ≡ n → succ m ≡ succ n
succCong refl = refl

+-leftCong : ∀ {m n o} → m ≡ n → m + o ≡ n + o
+-leftCong refl = refl

+-rightCong : ∀ {m n o} → n ≡ o → m + n ≡ m + o
+-rightCong refl = refl

------------------------------------------------------------------------------
-- Peano's third axiom.
P₃ : ∀ {m n} → succ m ≡ succ n → m ≡ n
P₃ refl = refl

-- Peano's fourth axiom.
P₄ : ∀ {n} → zero ≢ succ n
P₄ ()

x≢Sx : ∀ {n} → n ≢ succ n
x≢Sx {zero} ()
x≢Sx {succ n} h = x≢Sx (P₃ h)

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity n = refl

-- Adapted from the Agda standard library 0.8.1 (see
-- Data.Nat.Properties.Simple.+-rightIdentity).
+-rightIdentity : ∀ n → n + zero ≡ n
+-rightIdentity zero     = refl
+-rightIdentity (succ n) = succCong (+-rightIdentity n)

-- Adapted from the Agda standard library_0.8.1 (see
-- Data.Nat.Properties.Simple.+-assoc).
+-assoc : ∀ m n o → m + n + o ≡ m + (n + o)
+-assoc zero     _ _ = refl
+-assoc (succ m) n o = succCong (+-assoc m n o)

-- Adapted from the Agda standard library 0.8.1 (see
-- Data.Nat.Properties.Simple.+-suc).
x+Sy≡S[x+y] : ∀ m n → m + succ n ≡ succ (m + n)
x+Sy≡S[x+y] zero     _ = refl
x+Sy≡S[x+y] (succ m) n = succCong (x+Sy≡S[x+y] m n)

-- Adapted from the Agda standard library 0.8.1 (see
-- Data.Nat.Properties.Simple.+-comm).
+-comm : ∀ m n → m + n ≡ n + m
+-comm zero     n = sym (+-rightIdentity n)
+-comm (succ m) n = succ (m + n) ≡⟨ succCong (+-comm m n) ⟩
                    succ (n + m) ≡⟨ sym (x+Sy≡S[x+y] n m) ⟩
                    n + succ m   ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Relation.Binary.Core
open import Level using (Level; _⊔_; suc)
open import Data.Product using (Σ; _×_; _,_; Σ-syntax;  ∃-syntax; proj₁; proj₂)
open import Function

open import DeBruijn
open import Beta
open import Takahashi
open import Z
open import ConfluenceTakahashi using (lemma3-3; lemma3-5)

star-left :  ∀ {n} {M L N : Term n}
  → M —→ L
  → Star _—→_ L N
    -------------
  → Star _—→_ M N
star-left ML ε = ε ▻ ML
star-left ML (L*N′ ▻ N′N) =
  star-left ML L*N′ ▻ N′N

betas-star : ∀ {n} {M N : Term n}
  → M —↠ N
    -------------
  → Star _—→_ M N
betas-star (M ∎) = ε
betas-star (M —→⟨ M—→M′ ⟩ M′—↠N) =
  star-left M—→M′ (betas-star M′—↠N)

z-confluence-beta : ∀ {n} → Confluence (_—→_ {n})
z-confluence-beta = z-confluence ( _*
                                 , betas-star ∘ lemma3-3
                                 , betas-star ∘ lemma3-5)

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Values for standard evaluation with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Denotation.Value where

open import Nehemiah.Syntax.Type public
open import Nehemiah.Change.Type public
open import Base.Denotation.Notation public

open import Structure.Bag.Nehemiah
open import Data.Integer

import Parametric.Denotation.Value Base as Value

⟦_⟧Base : Value.Structure
⟦ base-int ⟧Base = ℤ
⟦ base-bag ⟧Base = Bag

open Value.Structure ⟦_⟧Base public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
import Everything

open import Prelude
open import Container.Traversable
open import Container.Foldable
open import Container.List
open import Text.Parse
open import Text.Lex
open import Text.Printf
open import Control.Monad.State
open import Control.Monad.Transformer
open import Control.WellFounded
open import Builtin.Size
open import Builtin.Coinduction
open import Builtin.Float
open import Builtin.Reflection

open import Tactic.Reflection.DeBruijn
open import Tactic.Reflection.Equality
open import Tactic.Reflection.Free
open import Tactic.Reflection.Quote
open import Tactic.Reflection.Telescope
open import Tactic.Deriving.Eq
open import Tactic.Nat

open import Numeric.Nat.DivMod
open import Numeric.Nat.Divide
open import Numeric.Nat.GCD
open import Numeric.Nat.Prime
open import Numeric.Rational
open import Numeric.Nat.Modulo
open import Numeric.Nat.Pow

open import MonoidTactic

-- open import DeriveEqTest

Hello = printf "%c%s" 'H' "ello"
World = printf "%-7s(%.6f)" "World" π

M = StateT Nat IO

putStrI : String → StateT Nat IO Unit
putStrI s = do
  n ← get
  put (suc n)
  lift (putStr (printf "[%d] %s\n" n s))

main : IO ⊤
main = do
  runStateT (mapM putStrI (Hello ∷ World ∷ " " ∷ [])) 0
  putStr (show (432429 divmod 41))
  putStr ("\n" & show (gcd! (19 * 17 * 31) (31 * 5)))
  putStrLn ""

downFrom : Nat → List Nat
downFrom zero    = []
downFrom (suc n) = suc n ∷ downFrom n

thm : ∀ n → 6 * sumR (map (_^ 2) (downFrom n)) ≡ n * (n + 1) * (2 * n + 1)
thm = induction

thm₂ : (a b : Nat) → (a - b) * (a + b) ≡ a ^ 2 - b ^ 2
thm₂ a b = auto

data N : Set where
  z : N
  s : N → N

unquoteDecl eqN = deriveEq eqN (quote N)

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
module Syntax.Number where

import      Lvl
open import Logic.Propositional
open import Numeral.Natural
open import Type

record Numeral {ℓ} (T : Type{ℓ}) : Typeω where
  field
    {restriction-ℓ} : Lvl.Level
    restriction : ℕ → Type{restriction-ℓ}
    num : (n : ℕ) → ⦃ _ : restriction(n) ⦄ → T
open Numeral ⦃ ... ⦄ public using (num)
{-# BUILTIN FROMNAT num #-}

InfiniteNumeral = Numeral
module InfiniteNumeral {ℓ} {T : Type{ℓ}} where
  intro : (ℕ → T) → InfiniteNumeral(T)
  Numeral.restriction-ℓ (intro(_))         = Lvl.𝟎
  Numeral.restriction   (intro(_)) _       = ⊤
  Numeral.num           (intro(f)) n ⦃ _ ⦄ = f(n)

-- record InfiniteNumeral {ℓ} (T : Type{ℓ}) : Type{ℓ} where
-- record InfiniteNumeral {ℓ} (T : Type{ℓ}) : Type{ℓ} where
--   field
--     num : ℕ → T

-- instance
--   Numeral-from-InfiniteNumeral : ∀{ℓ}{T} → ⦃ _ : InfiniteNumeral{ℓ}(T) ⦄ → Numeral{ℓ}(T)
--   Numeral.restriction-ℓ ( Numeral-from-InfiniteNumeral ) = Lvl.𝟎
--   Numeral.restriction ( Numeral-from-InfiniteNumeral ) (_) = ⊤
--   num ⦃ Numeral-from-InfiniteNumeral ⦃ infNum ⦄ ⦄ (n) ⦃ _ ⦄ = InfiniteNumeral.num(infNum) (n)

instance
  ℕ-InfiniteNumeral : InfiniteNumeral (ℕ)
  ℕ-InfiniteNumeral = InfiniteNumeral.intro(id) where
    id : ℕ → ℕ
    id x = x

instance
  Level-InfiniteNumeral : InfiniteNumeral (Lvl.Level)
  Level-InfiniteNumeral = InfiniteNumeral.intro(f) where
    f : ℕ → Lvl.Level
    f(ℕ.𝟎)    = Lvl.𝟎
    f(ℕ.𝐒(n)) = Lvl.𝐒(f(n))

record NegativeNumeral {ℓ} (T : Type{ℓ}) : Typeω where
  field
    {restriction-ℓ} : Lvl.Level
    restriction : ℕ → Type{restriction-ℓ}
    num : (n : ℕ) → ⦃ _ : restriction(n) ⦄ → T
open NegativeNumeral ⦃ ... ⦄ public using () renaming (num to -num)
{-# BUILTIN FROMNEG -num #-}

InfiniteNegativeNumeral = NegativeNumeral
module InfiniteNegativeNumeral {ℓ} {T : Type{ℓ}} where
  intro : (ℕ → T) → InfiniteNegativeNumeral(T)
  NegativeNumeral.restriction-ℓ (intro(_))         = Lvl.𝟎
  NegativeNumeral.restriction   (intro(_)) _       = ⊤
  NegativeNumeral.num           (intro(f)) n ⦃ _ ⦄ = f(n)

-- record InfiniteNegativeNumeral {ℓ} (T : Type{ℓ}) : Type{ℓ} where
--   field
--     num : ℕ → T
-- open InfiniteNegativeNumeral ⦃ ... ⦄ public

-- instance
--   NegativeNumeral-from-InfiniteNegativeNumeral : ∀{ℓ}{T} → ⦃ _ : InfiniteNegativeNumeral{ℓ}(T) ⦄ → NegativeNumeral{ℓ}(T)
--   NegativeNumeral.restriction-ℓ ( NegativeNumeral-from-InfiniteNegativeNumeral ) = Lvl.𝟎
--   NegativeNumeral.restriction ( NegativeNumeral-from-InfiniteNegativeNumeral ) (_) = ⊤
--   -num ⦃ NegativeNumeral-from-InfiniteNegativeNumeral ⦃ infNegNum ⦄ ⦄ (n) ⦃ _ ⦄ = InfiniteNegativeNumeral.num(infNegNum) (n)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Number.Operations.Specification where

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Data.Unit.Base -- Unit

open import Number.Postulates
open import Number.Base

open ℕⁿ
open ℤᶻ
open ℚᶠ
open ℝʳ
open ℂᶜ

open PatternsType

-- workflow:
-- 1. split on the both positivities at once
-- 2. add a general clause on top
-- 3. check file
-- 4. remove all unreachable clauses and goto 2.
-- feel free to remove too many clauses and let agda display the missing ones
+-Positivityᵒʳ : PositivityKindOrderedRing → PositivityKindOrderedRing → PositivityKindOrderedRing
+-Positivityᵒʳ _   X   = X
+-Positivityᵒʳ X   _   = X
+-Positivityᵒʳ _   X⁺⁻ = X
+-Positivityᵒʳ X⁺⁻ _   = X
-- clauses with same sign
+-Positivityᵒʳ X₀⁺ X₀⁺ = X₀⁺
+-Positivityᵒʳ X₀⁻ X₀⁻ = X₀⁻
+-Positivityᵒʳ X₀⁺ X⁺  = X⁺
+-Positivityᵒʳ X⁺  X₀⁺ = X⁺
+-Positivityᵒʳ X⁺  X⁺  = X⁺
+-Positivityᵒʳ X₀⁻ X⁻  = X⁻
+-Positivityᵒʳ X⁻  X⁻  = X⁻
+-Positivityᵒʳ X⁻  X₀⁻ = X⁻
-- remaining clauses with alternating sign
+-Positivityᵒʳ X₀⁻ X₀⁺ = X
+-Positivityᵒʳ X₀⁺ X₀⁻ = X
+-Positivityᵒʳ X⁻  X₀⁺ = X
+-Positivityᵒʳ X₀⁺ X⁻  = X
+-Positivityᵒʳ X⁻  X⁺  = X
+-Positivityᵒʳ X⁺  X⁻  = X
+-Positivityᵒʳ X₀⁻ X⁺  = X
+-Positivityᵒʳ X⁺  X₀⁻ = X

+-Positivityᶠ : PositivityKindField → PositivityKindField → PositivityKindField
-- positivity information is lost after _+_ on a field
+-Positivityᶠ x   y   = X

+-Positivityʰ : (l : NumberKind) → PositivityKindType l → PositivityKindType l → PositivityKindType l
+-Positivityʰ isNat     = +-Positivityᵒʳ
+-Positivityʰ isInt     = +-Positivityᵒʳ
+-Positivityʰ isRat     = +-Positivityᵒʳ
+-Positivityʰ isReal    = +-Positivityᵒʳ
+-Positivityʰ isComplex = +-Positivityᶠ

·-Positivityᵒʳ : PositivityKindOrderedRing → PositivityKindOrderedRing → PositivityKindOrderedRing
·-Positivityᵒʳ _   X   = X
·-Positivityᵒʳ X   _   = X
·-Positivityᵒʳ X₀⁺ X⁺⁻ = X
·-Positivityᵒʳ X⁺⁻ X₀⁺ = X
·-Positivityᵒʳ X₀⁻ X⁺⁻ = X
·-Positivityᵒʳ X⁺⁻ X₀⁻ = X
-- multiplying nonzero numbers gives a nonzero number
·-Positivityᵒʳ X⁺⁻ X⁺⁻ = X⁺⁻
·-Positivityᵒʳ X⁺  X⁺⁻ = X⁺⁻
·-Positivityᵒʳ X⁺⁻ X⁺  = X⁺⁻
·-Positivityᵒʳ X⁻  X⁺⁻ = X⁺⁻
·-Positivityᵒʳ X⁺⁻ X⁻  = X⁺⁻
-- multiplying positive numbers gives a positive number
·-Positivityᵒʳ X₀⁺ X₀⁺ = X₀⁺
·-Positivityᵒʳ X₀⁺ X⁺  = X₀⁺
·-Positivityᵒʳ X⁺  X₀⁺ = X₀⁺
·-Positivityᵒʳ X⁺  X⁺  = X⁺
-- multiplying negative numbers gives a positive number
·-Positivityᵒʳ X₀⁻ X⁻  = X₀⁺
·-Positivityᵒʳ X⁻  X₀⁻ = X₀⁺
·-Positivityᵒʳ X₀⁻ X₀⁻ = X₀⁺
·-Positivityᵒʳ X⁻  X⁻  = X⁺
-- multiplying a positive and a negative number gives a negative number
·-Positivityᵒʳ X⁻  X₀⁺ = X₀⁻
·-Positivityᵒʳ X₀⁺ X⁻  = X₀⁻
·-Positivityᵒʳ X₀⁻ X⁺  = X₀⁻
·-Positivityᵒʳ X⁺  X₀⁻ = X₀⁻
·-Positivityᵒʳ X₀⁻ X₀⁺ = X₀⁻
·-Positivityᵒʳ X₀⁺ X₀⁻ = X₀⁻
·-Positivityᵒʳ X⁻  X⁺  = X⁻
·-Positivityᵒʳ X⁺  X⁻  = X⁻

·-Positivityᶠ : PositivityKindField → PositivityKindField → PositivityKindField
·-Positivityᶠ X   X   = X
·-Positivityᶠ X   X⁺⁻ = X
·-Positivityᶠ X⁺⁻ X   = X
-- multiplying nonzero numbers gives a nonzero number
·-Positivityᶠ X⁺⁻ X⁺⁻ = X⁺⁻

·-Positivityʰ : (l : NumberKind) → PositivityKindType l → PositivityKindType l → PositivityKindType l
·-Positivityʰ isNat     = ·-Positivityᵒʳ
·-Positivityʰ isInt     = ·-Positivityᵒʳ
·-Positivityʰ isRat     = ·-Positivityᵒʳ
·-Positivityʰ isReal    = ·-Positivityᵒʳ
·-Positivityʰ isComplex = ·-Positivityᶠ

min-Positivityᵒʳ : PositivityKindOrderedRing → PositivityKindOrderedRing → PositivityKindOrderedRing
min-Positivityᵒʳ X   X   = X
min-Positivityᵒʳ X   X⁺⁻ = X
min-Positivityᵒʳ X   X₀⁺ = X
min-Positivityᵒʳ X   X⁺  = X
min-Positivityᵒʳ X   X⁻  = X⁻
min-Positivityᵒʳ X   X₀⁻ = X₀⁻
min-Positivityᵒʳ X⁺⁻ X   = X
min-Positivityᵒʳ X⁺⁻ X⁺⁻ = X⁺⁻
min-Positivityᵒʳ X⁺⁻ X₀⁺ = X
min-Positivityᵒʳ X⁺⁻ X⁺  = X⁺⁻
min-Positivityᵒʳ X⁺⁻ X⁻  = X⁻
min-Positivityᵒʳ X⁺⁻ X₀⁻ = X₀⁻
min-Positivityᵒʳ X₀⁺ X   = X
min-Positivityᵒʳ X₀⁺ X⁺⁻ = X
min-Positivityᵒʳ X₀⁺ X₀⁺ = X₀⁺
min-Positivityᵒʳ X₀⁺ X⁺  = X₀⁺
min-Positivityᵒʳ X₀⁺ X⁻  = X⁻
min-Positivityᵒʳ X₀⁺ X₀⁻ = X₀⁻
min-Positivityᵒʳ X⁺  X   = X
min-Positivityᵒʳ X⁺  X⁺⁻ = X⁺⁻
min-Positivityᵒʳ X⁺  X₀⁺ = X₀⁺
min-Positivityᵒʳ X⁺  X⁺  = X⁺
min-Positivityᵒʳ X⁺  X⁻  = X⁻
min-Positivityᵒʳ X⁺  X₀⁻ = X₀⁻
min-Positivityᵒʳ X⁻  X   = X⁻
min-Positivityᵒʳ X⁻  X⁺⁻ = X⁻
min-Positivityᵒʳ X⁻  X₀⁺ = X⁻
min-Positivityᵒʳ X⁻  X⁺  = X⁻
min-Positivityᵒʳ X⁻  X⁻  = X⁻
min-Positivityᵒʳ X⁻  X₀⁻ = X⁻
min-Positivityᵒʳ X₀⁻ X   = X₀⁻
min-Positivityᵒʳ X₀⁻ X⁺⁻ = X₀⁻
min-Positivityᵒʳ X₀⁻ X₀⁺ = X₀⁻
min-Positivityᵒʳ X₀⁻ X⁺  = X₀⁻
min-Positivityᵒʳ X₀⁻ X⁻  = X⁻
min-Positivityᵒʳ X₀⁻ X₀⁻ = X₀⁻

max-Positivityᵒʳ : PositivityKindOrderedRing → PositivityKindOrderedRing → PositivityKindOrderedRing
max-Positivityᵒʳ X   X   = X
max-Positivityᵒʳ X   X⁺⁻ = X
max-Positivityᵒʳ X   X₀⁺ = X₀⁺
max-Positivityᵒʳ X   X⁺  = X⁺
max-Positivityᵒʳ X   X⁻  = X
max-Positivityᵒʳ X   X₀⁻ = X
max-Positivityᵒʳ X⁺⁻ X   = X
max-Positivityᵒʳ X⁺⁻ X⁺⁻ = X⁺⁻
max-Positivityᵒʳ X⁺⁻ X₀⁺ = X₀⁺
max-Positivityᵒʳ X⁺⁻ X⁺  = X⁺
max-Positivityᵒʳ X⁺⁻ X⁻  = X⁺⁻
max-Positivityᵒʳ X⁺⁻ X₀⁻ = X
max-Positivityᵒʳ X₀⁺ X   = X₀⁺
max-Positivityᵒʳ X₀⁺ X⁺⁻ = X₀⁺
max-Positivityᵒʳ X₀⁺ X₀⁺ = X₀⁺
max-Positivityᵒʳ X₀⁺ X⁺  = X⁺
max-Positivityᵒʳ X₀⁺ X⁻  = X₀⁺
max-Positivityᵒʳ X₀⁺ X₀⁻ = X₀⁺
max-Positivityᵒʳ X⁺  X   = X⁺
max-Positivityᵒʳ X⁺  X⁺⁻ = X⁺
max-Positivityᵒʳ X⁺  X₀⁺ = X⁺
max-Positivityᵒʳ X⁺  X⁺  = X⁺
max-Positivityᵒʳ X⁺  X⁻  = X⁺
max-Positivityᵒʳ X⁺  X₀⁻ = X⁺
max-Positivityᵒʳ X⁻  X   = X
max-Positivityᵒʳ X⁻  X⁺⁻ = X⁺⁻
max-Positivityᵒʳ X⁻  X₀⁺ = X₀⁺
max-Positivityᵒʳ X⁻  X⁺  = X⁺
max-Positivityᵒʳ X⁻  X⁻  = X⁻
max-Positivityᵒʳ X⁻  X₀⁻ = X₀⁻
max-Positivityᵒʳ X₀⁻ X   = X
max-Positivityᵒʳ X₀⁻ X⁺⁻ = X
max-Positivityᵒʳ X₀⁻ X₀⁺ = X₀⁺
max-Positivityᵒʳ X₀⁻ X⁺  = X⁺
max-Positivityᵒʳ X₀⁻ X⁻  = X₀⁻
max-Positivityᵒʳ X₀⁻ X₀⁻ = X₀⁻

min-Positivityʰ : (l : NumberKind) → PositivityKindType l → PositivityKindType l → PositivityKindType l
min-Positivityʰ isNat     = min-Positivityᵒʳ
min-Positivityʰ isInt     = min-Positivityᵒʳ
min-Positivityʰ isRat     = min-Positivityᵒʳ
min-Positivityʰ isReal    = min-Positivityᵒʳ
min-Positivityʰ isComplex = λ _ _ → X -- doesn't matter since `min` is undefined for ℂ

max-Positivityʰ : (l : NumberKind) → PositivityKindType l → PositivityKindType l → PositivityKindType l
max-Positivityʰ isNat     = max-Positivityᵒʳ
max-Positivityʰ isInt     = max-Positivityᵒʳ
max-Positivityʰ isRat     = max-Positivityᵒʳ
max-Positivityʰ isReal    = max-Positivityᵒʳ
max-Positivityʰ isComplex = λ _ _ → X -- doesn't matter since `max` is undefined for ℂ

+-Types : NumberProp → NumberProp → NumberProp
+-Types (level₀ , pos₀) (level₁ , pos₁) =
  let level  = maxₙₗ level₀ level₁
  in level , +-Positivityʰ level (coerce-PositivityKind level₀ level pos₀) (coerce-PositivityKind level₁ level pos₁)

·-Types : NumberProp → NumberProp → NumberProp
·-Types (level₀ , pos₀) (level₁ , pos₁) =
  let level  = maxₙₗ level₀ level₁
  in level , ·-Positivityʰ level (coerce-PositivityKind level₀ level pos₀) (coerce-PositivityKind level₁ level pos₁)

⁻¹-Types : ∀{l p} → Number (l , p) → Type (ℓ-max (NumberLevel (maxₙₗ l isRat)) (NumberKindProplevel l))
-- numbers that can be zero need an additional apartness proof
⁻¹-Types {isNat    } {X  } (x ,, p) = ∀{{ q : x #ⁿ 0ⁿ }} → Number (isRat     , X⁺⁻)
⁻¹-Types {isInt    } {X  } (x ,, p) = ∀{{ q : x #ᶻ 0ᶻ }} → Number (isRat     , X⁺⁻)
⁻¹-Types {isRat    } {X  } (x ,, p) = ∀{{ q : x #ᶠ 0ᶠ }} → Number (isRat     , X⁺⁻)
⁻¹-Types {isReal   } {X  } (x ,, p) = ∀{{ q : x #ʳ 0ʳ }} → Number (isReal    , X⁺⁻)
⁻¹-Types {isComplex} {X  } (x ,, p) = ∀{{ q : x #ᶜ 0ᶜ }} → Number (isComplex , X⁺⁻)
⁻¹-Types {isNat    } {X₀⁺} (x ,, p) = ∀{{ q : x #ⁿ 0ⁿ }} → Number (isRat     , X⁺ )
⁻¹-Types {isInt    } {X₀⁺} (x ,, p) = ∀{{ q : x #ᶻ 0ᶻ }} → Number (isRat     , X⁺ )
⁻¹-Types {isRat    } {X₀⁺} (x ,, p) = ∀{{ q : x #ᶠ 0ᶠ }} → Number (isRat     , X⁺ )
⁻¹-Types {isReal   } {X₀⁺} (x ,, p) = ∀{{ q : x #ʳ 0ʳ }} → Number (isReal    , X⁺ )
⁻¹-Types {isNat    } {X₀⁻} (x ,, p) = ∀{{ q : x #ⁿ 0ⁿ }} → Number (isRat     , X⁻ )
⁻¹-Types {isInt    } {X₀⁻} (x ,, p) = ∀{{ q : x #ᶻ 0ᶻ }} → Number (isRat     , X⁻ )
⁻¹-Types {isRat    } {X₀⁻} (x ,, p) = ∀{{ q : x #ᶠ 0ᶠ }} → Number (isRat     , X⁻ )
⁻¹-Types {isReal   } {X₀⁻} (x ,, p) = ∀{{ q : x #ʳ 0ʳ }} → Number (isReal    , X⁻ )
-- positive, negative and nonzero numbers are already apart from zero
⁻¹-Types {isNat    } {X⁺⁻} (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isNat    } Unit }} → Number (isRat     , X⁺⁻)
⁻¹-Types {isNat    } {X⁺ } (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isNat    } Unit }} → Number (isRat     , X⁺ )
⁻¹-Types {isInt    } {X⁺⁻} (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isInt    } Unit }} → Number (isRat     , X⁺⁻)
⁻¹-Types {isInt    } {X⁺ } (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isInt    } Unit }} → Number (isRat     , X⁺ )
⁻¹-Types {isInt    } {X⁻ } (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isInt    } Unit }} → Number (isRat     , X⁻ )
⁻¹-Types {isRat    } {X⁺⁻} (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isRat    } Unit }} → Number (isRat     , X⁺⁻)
⁻¹-Types {isRat    } {X⁺ } (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isRat    } Unit }} → Number (isRat     , X⁺ )
⁻¹-Types {isRat    } {X⁻ } (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isRat    } Unit }} → Number (isRat     , X⁻ )
⁻¹-Types {isReal   } {X⁺⁻} (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isReal   } Unit }} → Number (isReal    , X⁺⁻)
⁻¹-Types {isReal   } {X⁺ } (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isReal   } Unit }} → Number (isReal    , X⁺ )
⁻¹-Types {isReal   } {X⁻ } (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isReal   } Unit }} → Number (isReal    , X⁻ )
⁻¹-Types {isComplex} {X⁺⁻} (x ,, p) = ∀{{ q : Lift {j = NumberKindProplevel isComplex} Unit }} → Number (isComplex , X⁺⁻)

-Types : ∀{l p} → Number (l , p) → Type (NumberLevel (maxₙₗ l isInt))
-Types {isInt    } {X  } (x ,, p) = Number (isInt     , X)
-Types {isRat    } {X  } (x ,, p) = Number (isRat     , X)
-Types {isReal   } {X  } (x ,, p) = Number (isReal    , X)
-Types {isComplex} {X  } (x ,, p) = Number (isComplex , X)
-- the negative of a natural number is a Nonpositive integer
-Types {isNat    } {X  } (x ,, p) = Number (isInt     , X₀⁻)
-- the negative of a nonzero number is a nonzero number
-Types {isNat    } {X⁺⁻} (x ,, p) = Number (isInt     , X⁺⁻)
-Types {isInt    } {X⁺⁻} (x ,, p) = Number (isInt     , X⁺⁻)
-Types {isRat    } {X⁺⁻} (x ,, p) = Number (isRat     , X⁺⁻)
-Types {isReal   } {X⁺⁻} (x ,, p) = Number (isReal    , X⁺⁻)
-Types {isComplex} {X⁺⁻} (x ,, p) = Number (isComplex , X⁺⁻)
-- the negative of a positive number is a negative number
-Types {isNat    } {X₀⁺} (x ,, p) = Number (isInt     , X₀⁻)
-Types {isInt    } {X₀⁺} (x ,, p) = Number (isInt     , X₀⁻)
-Types {isRat    } {X₀⁺} (x ,, p) = Number (isRat     , X₀⁻)
-Types {isReal   } {X₀⁺} (x ,, p) = Number (isReal    , X₀⁻)
-Types {isNat    } {X⁺ } (x ,, p) = Number (isInt     , X⁻ )
-Types {isInt    } {X⁺ } (x ,, p) = Number (isInt     , X⁻ )
-Types {isRat    } {X⁺ } (x ,, p) = Number (isRat     , X⁻ )
-Types {isReal   } {X⁺ } (x ,, p) = Number (isReal    , X⁻ )
-- the negative of a negative number is a positive number
-Types {isNat    } {X₀⁻} (x ,, p) = Number (isInt     , X₀⁺)
-Types {isInt    } {X₀⁻} (x ,, p) = Number (isInt     , X₀⁺)
-Types {isRat    } {X₀⁻} (x ,, p) = Number (isRat     , X₀⁺)
-Types {isReal   } {X₀⁻} (x ,, p) = Number (isReal    , X₀⁺)
-Types {isInt    } {X⁻ } (x ,, p) = Number (isInt     , X⁺ )
-Types {isRat    } {X⁻ } (x ,, p) = Number (isRat     , X⁺ )
-Types {isReal   } {X⁻ } (x ,, p) = Number (isReal    , X⁺ )

abs-Types : ∀{l p} → Number (l , p) → Type (NumberLevel (minₙₗ l isReal))
abs-Types {isNat    } {X  } (x ,, p) = Number (isNat  , X₀⁺)
abs-Types {isNat    } {X⁺⁻} (x ,, p) = Number (isNat  , X⁺ )
abs-Types {isNat    } {X₀⁺} (x ,, p) = Number (isNat  , X₀⁺)
abs-Types {isNat    } {X⁺ } (x ,, p) = Number (isNat  , X⁺ )
abs-Types {isNat    } {X₀⁻} (x ,, p) = Number (isNat  , X₀⁺)
abs-Types {isInt    } {X  } (x ,, p) = Number (isInt  , X₀⁺)
abs-Types {isInt    } {X⁺⁻} (x ,, p) = Number (isInt  , X⁺ )
abs-Types {isInt    } {X₀⁺} (x ,, p) = Number (isInt  , X₀⁺)
abs-Types {isInt    } {X⁺ } (x ,, p) = Number (isInt  , X⁺ )
abs-Types {isInt    } {X⁻ } (x ,, p) = Number (isInt  , X⁺ )
abs-Types {isInt    } {X₀⁻} (x ,, p) = Number (isInt  , X₀⁺)
abs-Types {isRat    } {X  } (x ,, p) = Number (isRat  , X₀⁺)
abs-Types {isRat    } {X⁺⁻} (x ,, p) = Number (isRat  , X⁺ )
abs-Types {isRat    } {X₀⁺} (x ,, p) = Number (isRat  , X₀⁺)
abs-Types {isRat    } {X⁺ } (x ,, p) = Number (isRat  , X⁺ )
abs-Types {isRat    } {X⁻ } (x ,, p) = Number (isRat  , X⁺ )
abs-Types {isRat    } {X₀⁻} (x ,, p) = Number (isRat  , X₀⁺)
abs-Types {isReal   } {X  } (x ,, p) = Number (isReal , X₀⁺)
abs-Types {isReal   } {X⁺⁻} (x ,, p) = Number (isReal , X⁺ )
abs-Types {isReal   } {X₀⁺} (x ,, p) = Number (isReal , X₀⁺)
abs-Types {isReal   } {X⁺ } (x ,, p) = Number (isReal , X⁺ )
abs-Types {isReal   } {X⁻ } (x ,, p) = Number (isReal , X⁺ )
abs-Types {isReal   } {X₀⁻} (x ,, p) = Number (isReal , X₀⁺)
abs-Types {isComplex} {X  } (x ,, p) = Number (isReal , X₀⁺)
abs-Types {isComplex} {X⁺⁻} (x ,, p) = Number (isReal , X⁺ )

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


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

module Categories.Category.Equivalence where

-- Strong equivalence of categories.  Same as ordinary equivalence in Cat.
-- May not include everything we'd like to think of as equivalences, namely
-- the full, faithful functors that are essentially surjective on objects.

open import Level
open import Relation.Binary using (IsEquivalence; Setoid)

open import Categories.Adjoint.Equivalence
open import Categories.Category
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Properties
open import Categories.NaturalTransformation using (ntHelper; _∘ᵥ_; _∘ˡ_; _∘ʳ_)
open import Categories.NaturalTransformation.NaturalIsomorphism as NI
  using (NaturalIsomorphism ; unitorˡ; unitorʳ; associator; _ⓘᵥ_; _ⓘˡ_; _ⓘʳ_)
  renaming (sym to ≃-sym)
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties

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

record WeakInverse (F : Functor C D) (G : Functor D C) : Set (levelOfTerm F ⊔ levelOfTerm G) where
  field
    F∘G≈id : NaturalIsomorphism (F ∘F G) idF
    G∘F≈id : NaturalIsomorphism (G ∘F F) idF

  module F∘G≈id = NaturalIsomorphism F∘G≈id
  module G∘F≈id = NaturalIsomorphism G∘F≈id

  private
    module C = Category C
    module D = Category D
    module F = Functor F
    module G = Functor G

  -- adjoint equivalence
  F⊣G : ⊣Equivalence F G
  F⊣G = record
    { unit   = ≃-sym G∘F≈id
    ; counit =
      let open D
          open HomReasoning
          open MR D
          open MP D
      in record
        { F⇒G = ntHelper record
          { η       = λ X → F∘G≈id.⇒.η X ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
          ; commute = λ {X Y} f → begin
            (F∘G≈id.⇒.η Y ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ Y)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ Y))) ∘ F.F₁ (G.F₁ f)
              ≈⟨ pull-last (F∘G≈id.⇐.commute (F.F₁ (G.F₁ f))) ⟩
            F∘G≈id.⇒.η Y ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ Y)) ∘ (F.F₁ (G.F₁ (F.F₁ (G.F₁ f))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X)))
              ≈˘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
            F∘G≈id.⇒.η Y ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ Y) C.∘ G.F₁ (F.F₁ (G.F₁ f))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ refl ⟩∘⟨ F.F-resp-≈ (G∘F≈id.⇒.commute (G.F₁ f)) ⟩∘⟨ refl ⟩
            F∘G≈id.⇒.η Y ∘ F.F₁ (G.F₁ f C.∘ G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ refl ⟩∘⟨ F.homomorphism ⟩∘⟨ refl ⟩
            F∘G≈id.⇒.η Y ∘ (F.F₁ (G.F₁ f) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ center⁻¹ (F∘G≈id.⇒.commute f) refl ⟩
            (f ∘ F∘G≈id.⇒.η X) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ≈⟨ assoc ⟩
            f ∘ F∘G≈id.⇒.η X ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ X)) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ X))
              ∎
          }
        ; F⇐G = ntHelper record
          { η       = λ X → (F∘G≈id.⇒.η (F.F₀ (G.F₀ X)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X))) ∘ F∘G≈id.⇐.η X
          ; commute = λ {X Y} f → begin
            ((F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ Y))) ∘ F∘G≈id.⇐.η Y) ∘ f
              ≈⟨ pullʳ (F∘G≈id.⇐.commute f) ⟩
            (F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ Y))) ∘ F.F₁ (G.F₁ f) ∘ F∘G≈id.⇐.η X
              ≈⟨ center (⟺ F.homomorphism) ⟩
            F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ Y) C.∘ G.F₁ f) ∘ F∘G≈id.⇐.η X
              ≈⟨ refl ⟩∘⟨ F.F-resp-≈ (G∘F≈id.⇐.commute (G.F₁ f)) ⟩∘⟨ refl ⟩
            F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ F.F₁ (G.F₁ (F.F₁ (G.F₁ f)) C.∘ G∘F≈id.⇐.η (G.F₀ X)) ∘ F∘G≈id.⇐.η X
              ≈⟨ refl ⟩∘⟨ F.homomorphism ⟩∘⟨ refl ⟩
            F∘G≈id.⇒.η (F.F₀ (G.F₀ Y)) ∘ (F.F₁ (G.F₁ (F.F₁ (G.F₁ f))) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X))) ∘ F∘G≈id.⇐.η X
              ≈⟨ center⁻¹ (F∘G≈id.⇒.commute _) refl ⟩
            (F.F₁ (G.F₁ f) ∘ F∘G≈id.⇒.η (F.F₀ (G.F₀ X))) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X)) ∘ F∘G≈id.⇐.η X
              ≈⟨ center refl ⟩
            F.F₁ (G.F₁ f) ∘ (F∘G≈id.⇒.η (F.F₀ (G.F₀ X)) ∘ F.F₁ (G∘F≈id.⇐.η (G.F₀ X))) ∘ F∘G≈id.⇐.η X
              ∎
          }
        ; iso = λ X → Iso-∘ (Iso-∘ (Iso-swap (F∘G≈id.iso _)) ([ F ]-resp-Iso (G∘F≈id.iso _)))
                            (F∘G≈id.iso X)
        }
    ; zig    = λ {A} →
      let open D
          open HomReasoning
          open MR D
      in begin
      (F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ (F.F₀ A))) ∘ F∘G≈id.⇐.η (F.F₀ (G.F₀ (F.F₀ A))))
        ∘ F.F₁ (G∘F≈id.⇐.η A)
        ≈⟨ pull-last (F∘G≈id.⇐.commute (F.F₁ (G∘F≈id.⇐.η A))) ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ (F.F₀ A))) ∘
        F.F₁ (G.F₁ (F.F₁ (G∘F≈id.⇐.η A))) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈˘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇒.η (G.F₀ (F.F₀ A)) C.∘ G.F₁ (F.F₁ (G∘F≈id.⇐.η A))) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈⟨ refl ⟩∘⟨ F.F-resp-≈ (G∘F≈id.⇒.commute (G∘F≈id.⇐.η A)) ⟩∘⟨ refl ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F.F₁ (G∘F≈id.⇐.η A C.∘ G∘F≈id.⇒.η A) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈⟨ refl ⟩∘⟨ elimˡ ((F.F-resp-≈ (G∘F≈id.iso.isoˡ _)) ○ F.identity) ⟩
      F∘G≈id.⇒.η (F.F₀ A) ∘ F∘G≈id.⇐.η (F.F₀ A)
        ≈⟨ F∘G≈id.iso.isoʳ _ ⟩
      id
        ∎
    }

  module F⊣G = ⊣Equivalence F⊣G

record StrongEquivalence {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  field
    F            : Functor C D
    G            : Functor D C
    weak-inverse : WeakInverse F G

  open WeakInverse weak-inverse public

refl : StrongEquivalence C C
refl = record
  { F            = idF
  ; G            = idF
  ; weak-inverse = record
    { F∘G≈id = unitorˡ
    ; G∘F≈id = unitorˡ
    }
  }

sym : StrongEquivalence C D → StrongEquivalence D C
sym e = record
  { F            = G
  ; G            = F
  ; weak-inverse = record
    { F∘G≈id     = G∘F≈id
    ; G∘F≈id     = F∘G≈id
    }
  }
  where open StrongEquivalence e

trans : StrongEquivalence C D → StrongEquivalence D E → StrongEquivalence C E
trans {C = C} {D = D} {E = E} e e′ = record
  { F            = e′.F ∘F e.F
  ; G            = e.G ∘F e′.G
  ; weak-inverse = record
    { F∘G≈id = let module S = Setoid (NI.Functor-NI-setoid E E)
               in S.trans (S.trans (associator (e.G ∘F e′.G) e.F e′.F)
                                   (e′.F ⓘˡ (unitorˡ ⓘᵥ (e.F∘G≈id ⓘʳ e′.G) ⓘᵥ NI.sym (associator e′.G e.G e.F))))
                          e′.F∘G≈id
    ; G∘F≈id = let module S = Setoid (NI.Functor-NI-setoid C C)
               in S.trans (S.trans (associator (e′.F ∘F e.F) e′.G e.G)
                                   (e.G ⓘˡ (unitorˡ ⓘᵥ (e′.G∘F≈id ⓘʳ e.F) ⓘᵥ NI.sym (associator e.F e′.F e′.G))))
                          e.G∘F≈id
    }
  }
  where module e  = StrongEquivalence e
        module e′ = StrongEquivalence e′

isEquivalence : ∀ {o ℓ e} → IsEquivalence (StrongEquivalence {o} {ℓ} {e})
isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = trans
  }

setoid : ∀ o ℓ e → Setoid _ _
setoid o ℓ e = record
  { Carrier       = Category o ℓ e
  ; _≈_           = StrongEquivalence
  ; isEquivalence = isEquivalence
  }

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module nodcap.LocalChoice where

open import Algebra
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺
open import Data.List as L using (List; []; _∷_; _++_)
open import Data.List.Any as LA using (Any; here; there)
open import Data.List.Any.BagAndSetEquality as B
open import Data.Product as PR using (∃; _×_; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_$_; flip)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as I using ()
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)

open import Data.Environment
open import nodcap.Base
open import nodcap.Typing

open I.Inverse using (to; from)
private module ++ {a} {A : Set a} = Monoid (L.monoid A)

-- We define local choice as follows:
_or_ : {A : Type} → ⊢ A ∷ [] → ⊢ A ∷ [] → ⊢ A ∷ []
x or y = cut (pool (in? x) (in? y)) out
  where
    in? : ∀ {A} → ⊢ A ∷ [] → ⊢ ![ suc 0 ] (𝟏 & A) ∷ []
    in? x = mk!₁ $ case halt x
    out : ∀ {A} → ⊢ ?[ suc 1 ] (⊥ ⊕ (A ^)) ∷ A ∷ []
    out = cont $ mk?₁ $ sel₁ $ wait $ mk?₁ $ sel₂ $ exch (bbl []) $ ax

-- However, Luís Caires defines local choice with contexts. For this to work we
-- need an additional trick: conversion between contexts and types.

-- We can represent a context as a sequence of pars.
⅋[_] : Environment → Type
⅋[ [] ]    = ⊥
⅋[ A ∷ Γ ] = A ⅋ ⅋[ Γ ]

-- See:
recv⋆ : {Γ Δ : Environment} →

  ⊢ Γ ++ Δ →
  ------------
  ⊢ ⅋[ Γ ] ∷ Δ

recv⋆ {[]}    x = wait x
recv⋆ {A ∷ Γ} x = recv $ exch (bbl []) $ recv⋆ $ exch (bwd [] Γ) $ x

-- In order to reverse this, we need to show that the `recv` rule is invertible.
-- Fortunately, it is:
recv⁻¹ : {Γ : Environment} {A B : Type} →

  ⊢ A ⅋ B ∷ Γ →
  -------------
  ⊢ A ∷ B ∷ Γ

recv⁻¹ {Γ} {A} {B} x
  = exch (swp₂ (A ∷ B ∷ []))
  $ cut {Γ} {A ∷ B ∷ []} x
  $ send
  ( exch (bbl []) ax )
  ( exch (bbl []) ax )

-- It should come as no surprise that the repeated application of `recv` is also
-- invertible.
recv⋆⁻¹ : {Γ Δ : Environment} →

  ⊢ ⅋[ Γ ] ∷ Δ →
  --------------
  ⊢ Γ ++ Δ

recv⋆⁻¹ {[]}    x = cut halt x
recv⋆⁻¹ {A ∷ Γ} x = exch (fwd [] Γ) $ recv⋆⁻¹ {Γ} $ exch (bbl []) $ recv⁻¹ x

-- Using these additional derivable operators, we can represent the version of
-- local choice as used by Luís Caires:
_or⋆_ : {Γ : Environment} → ⊢ Γ → ⊢ Γ → ⊢ Γ
_or⋆_ {Γ} x y
  = P.subst ⊢_ (proj₂ ++.identity Γ)
  $ recv⋆⁻¹ {Γ}
  $  ( recv⋆ $ P.subst ⊢_ (P.sym $ proj₂ ++.identity Γ) x )
  or ( recv⋆ $ P.subst ⊢_ (P.sym $ proj₂ ++.identity Γ) y )

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

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
-- In this file we consider the special of localising at a single
-- element f : R (or rather the set of powers of f). This is also
-- known as inverting f.

{-# OPTIONS --cubical --no-import-sorts --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Localisation.InvertingElements where

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

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)
open import Cubical.Data.Vec
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Localisation.Base
open import Cubical.Algebra.CommRing.Localisation.UniversalProperty
open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

open Iso

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

module _(R' : CommRing {ℓ}) where
 open isMultClosedSubset
 private R = R' .fst
 -- open CommRingStr ⦃...⦄
 open CommRingStr (R' .snd)
 open Exponentiation R'

 [_ⁿ|n≥0] : R → ℙ R
 [ f ⁿ|n≥0] g = (∃[ n ∈ ℕ ] g ≡ f ^ n) , propTruncIsProp
 -- Σ[ n ∈ ℕ ] (s ≡ f ^ n) × (∀ m → s ≡ f ^ m → n ≤ m) maybe better, this isProp:
 -- (n,s≡fⁿ,p) (m,s≡fᵐ,q) then n≤m by p and  m≤n by q => n≡m

 powersFormMultClosedSubset : (f : R) → isMultClosedSubset R' [ f ⁿ|n≥0]
 powersFormMultClosedSubset f .containsOne = ∣ zero , refl ∣
 powersFormMultClosedSubset f .multClosed =
             PT.map2 λ (m , p) (n , q) → (m +ℕ n) , (λ i → (p i) · (q i)) ∙ ·-of-^-is-^-of-+ f m n

 R[1/_] : R → Type ℓ
 R[1/ f ] = Loc.S⁻¹R R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)

 R[1/_]AsCommRing : R → CommRing {ℓ}
 R[1/ f ]AsCommRing = Loc.S⁻¹RAsCommRing R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)

 -- A useful lemma: (gⁿ/1)≡(g/1)ⁿ in R[1/f]
 ^-respects-/1 : {f g : R} (n : ℕ) → [ (g ^ n) , 1r , ∣ 0 , (λ _ → 1r) ∣ ] ≡
     Exponentiation._^_ R[1/ f ]AsCommRing [ g , 1r , powersFormMultClosedSubset _ .containsOne ] n
 ^-respects-/1 zero = refl
 ^-respects-/1 {f} {g} (suc n) = eq/ _ _ ( (1r , powersFormMultClosedSubset f .containsOne)
                                         , cong (1r · (g · (g ^ n)) ·_) (·-lid 1r))
                           ∙ cong (CommRingStr._·_ (R[1/ f ]AsCommRing .snd)
                           [ g , 1r , powersFormMultClosedSubset f .containsOne ]) (^-respects-/1 n)

 -- A slight improvement for eliminating into propositions
 InvElPropElim : {f : R} {P : R[1/ f ] → Type ℓ'}
               → (∀ x →  isProp (P x))
               → (∀ (r : R) (n : ℕ) → P [ r , (f ^ n) , ∣ n , refl ∣ ])
              ----------------------------------------------------------
               → (∀ x → P x)
 InvElPropElim {f = f} {P = P} PisProp base = elimProp (λ _ → PisProp _) []-case
  where
  S[f] = Loc.S R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
  []-case : (a : R × S[f]) → P [ a ]
  []-case (r , s , s∈S[f]) = PT.rec (PisProp _) Σhelper s∈S[f]
   where
   Σhelper : Σ[ n ∈ ℕ ] s ≡ f ^ n → P [ r , s , s∈S[f] ]
   Σhelper (n , p) = subst P (cong [_] (≡-× refl (Σ≡Prop (λ _ → propTruncIsProp) (sym p)))) (base r n)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module IIDg where

open import LF

-- Codes for indexed inductive types
data OPg (I : Set) : Set1 where
  ι : I -> OPg I
  σ : (A : Set)(γ : A -> OPg I) -> OPg I
  δ : (H : Set)(i : H -> I)(γ : OPg I) -> OPg I

-- The top-level structure of values in an IIDg
Args : {I : Set}(γ : OPg I)(U : I -> Set) -> Set
Args (ι _)     U = One
Args (σ A γ)   U = A × \a -> Args (γ a) U
Args (δ H i γ) U = ((x : H) -> U (i x)) × \_ -> Args γ U

-- The index of a value in an IIDg
Index : {I : Set}(γ : OPg I)(U : I -> Set) -> Args γ U -> I
Index (ι i)	U _	    = i
Index (σ A γ)	U < a | b > = Index (γ a) U b
Index (δ _ _ γ) U < _ | b > = Index γ U b

-- The assumptions of a particular inductive occurrence.
IndArg : {I : Set}(γ : OPg I)(U : I -> Set) -> Args γ U -> Set
IndArg (ι _)     U _	     = Zero
IndArg (σ A γ)	 U < a | b > = IndArg (γ a) U b
IndArg (δ H i γ) U < _ | b > = H + IndArg γ U b

-- The index of an inductive occurrence.
IndIndex : {I : Set}(γ : OPg I)(U : I -> Set)(a : Args γ U) -> IndArg γ U a -> I
IndIndex (ι _)	   U _	     ()
IndIndex (σ A γ)   U < a | b > h       = IndIndex (γ a) U b h
IndIndex (δ A i γ) U < g | b > (inl h) = i h
IndIndex (δ A i γ) U < g | b > (inr h) = IndIndex γ U b h

-- An inductive occurrence.
Ind : {I : Set}(γ : OPg I)(U : I -> Set)(a : Args γ U)(h : IndArg γ U a) -> U (IndIndex γ U a h)
Ind (ι _)     U _	  ()
Ind (σ A γ)   U < a | b > h	  = Ind (γ a) U b h
Ind (δ H i γ) U < g | b > (inl h) = g h
Ind (δ H i γ) U < _ | b > (inr h) = Ind γ U b h

-- The type of induction hypotheses.
IndHyp : {I : Set}(γ : OPg I)(U : I -> Set)(C : (i : I) -> U i -> Set)(a : Args γ U) -> Set
IndHyp γ U C a = (hyp : IndArg γ U a) -> C (IndIndex γ U a hyp) (Ind γ U a hyp)

-- Large induction hypostheses.
IndHyp₁ : {I : Set}(γ : OPg I)(U : I -> Set)(C : (i : I) -> U i -> Set1)(a : Args γ U) -> Set1
IndHyp₁ γ U C a = (hyp : IndArg γ U a) -> C (IndIndex γ U a hyp) (Ind γ U a hyp)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Fresh lists, a proof relevant variant of Catarina Coquand's contexts in
-- "A Formalised Proof of the Soundness and Completeness of a Simply Typed
-- Lambda-Calculus with Explicit Substitutions"
------------------------------------------------------------------------

-- See README.Data.List.Fresh and README.Data.Trie.NonDependent for
-- examples of how to use fresh lists.

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

module Data.List.Fresh where

open import Level using (Level; _⊔_; Lift)
open import Data.Bool.Base using (true; false)
open import Data.Unit.Base
open import Data.Product using (∃; _×_; _,_; -,_; proj₁; proj₂)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Function using (_∘′_; flip; id; _on_)
open import Relation.Nullary      using (does)
open import Relation.Unary   as U using (Pred)
open import Relation.Binary  as B using (Rel)
open import Relation.Nary

private
  variable
    a b p r s : Level
    A : Set a
    B : Set b

------------------------------------------------------------------------
-- Basic type

-- If we pick an R such that (R a b) means that a is different from b
-- then we have a list of distinct values.

module _ {a} (A : Set a) (R : Rel A r) where

  data List# : Set (a ⊔ r)
  fresh : (a : A) (as : List#) → Set r

  data List# where
    []   : List#
    cons : (a : A) (as : List#) → fresh a as → List#

  -- Whenever R can be reconstructed by η-expansion (e.g. because it is
  -- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we
  -- do not care about the proof, it is convenient to get back list syntax.

  -- We use a different symbol to avoid conflict when importing both Data.List
  -- and Data.List.Fresh.
  infixr 5 _∷#_
  pattern _∷#_ x xs = cons x xs _

  fresh a []        = Lift _ ⊤
  fresh a (x ∷# xs) = R a x × fresh a xs

-- Convenient notation for freshness making A and R implicit parameters
infix 5 _#_
_#_ : {R : Rel A r} (a : A) (as : List# A R) → Set r
_#_ = fresh _ _

------------------------------------------------------------------------
-- Operations for modifying fresh lists

module _ {R : Rel A r} {S : Rel B s} (f : A → B) (R⇒S : ∀[ R ⇒ (S on f) ]) where

  map   : List# A R → List# B S
  map-# : ∀ {a} as → a # as → f a # map as

  map []             = []
  map (cons a as ps) = cons (f a) (map as) (map-# as ps)

  map-# []        _        = _
  map-# (a ∷# as) (p , ps) = R⇒S p , map-# as ps

module _ {R : Rel B r} (f : A → B) where

  map₁ : List# A (R on f) → List# B R
  map₁ = map f id

module _ {R : Rel A r} {S : Rel A s} (R⇒S : ∀[ R ⇒ S ]) where

  map₂ : List# A R → List# A S
  map₂ = map id R⇒S

------------------------------------------------------------------------
-- Views

data Empty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
  [] : Empty []

data NonEmpty {A : Set a} {R : Rel A r} : List# A R → Set (a ⊔ r) where
  cons : ∀ x xs pr → NonEmpty (cons x xs pr)

------------------------------------------------------------------------
-- Operations for reducing fresh lists

length : {R : Rel A r} → List# A R → ℕ
length []        = 0
length (_ ∷# xs) = suc (length xs)

------------------------------------------------------------------------
-- Operations for constructing fresh lists

pattern [_] a = a ∷# []

fromMaybe : {R : Rel A r} → Maybe A → List# A R
fromMaybe nothing  = []
fromMaybe (just a) = [ a ]

module _ {R : Rel A r} (R-refl : B.Reflexive R) where

  replicate   : ℕ → A → List# A R
  replicate-# : (n : ℕ) (a : A) → a # replicate n a

  replicate zero    a = []
  replicate (suc n) a = cons a (replicate n a) (replicate-# n a)

  replicate-# zero    a = _
  replicate-# (suc n) a = R-refl , replicate-# n a

------------------------------------------------------------------------
-- Operations for deconstructing fresh lists

uncons : {R : Rel A r} → List# A R → Maybe (A × List# A R)
uncons []        = nothing
uncons (a ∷# as) = just (a , as)

head : {R : Rel A r} → List# A R → Maybe A
head = Maybe.map proj₁ ∘′ uncons

tail : {R : Rel A r} → List# A R → Maybe (List# A R)
tail = Maybe.map proj₂ ∘′ uncons

take   : {R : Rel A r} → ℕ → List# A R → List# A R
take-# : {R : Rel A r} → ∀ n a (as : List# A R) → a # as → a # take n as

take zero    xs             = []
take (suc n) []             = []
take (suc n) (cons a as ps) = cons a (take n as) (take-# n a as ps)

take-# zero    a xs        _        = _
take-# (suc n) a []        ps       = _
take-# (suc n) a (x ∷# xs) (p , ps) = p , take-# n a xs ps

drop : {R : Rel A r} → ℕ → List# A R → List# A R
drop zero    as        = as
drop (suc n) []        = []
drop (suc n) (a ∷# as) = drop n as

module _ {P : Pred A p} (P? : U.Decidable P) where

  takeWhile   : {R : Rel A r} → List# A R → List# A R
  takeWhile-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # takeWhile as

  takeWhile []             = []
  takeWhile (cons a as ps) with does (P? a)
  ... | true  = cons a (takeWhile as) (takeWhile-# a as ps)
  ... | false = []

  takeWhile-# a []        _        = _
  takeWhile-# a (x ∷# xs) (p , ps) with does (P? x)
  ... | true  = p , takeWhile-# a xs ps
  ... | false = _

  dropWhile : {R : Rel A r} → List# A R → List# A R
  dropWhile []            = []
  dropWhile aas@(a ∷# as) with does (P? a)
  ... | true  = dropWhile as
  ... | false = aas

  filter   : {R : Rel A r} → List# A R → List# A R
  filter-# : ∀ {R : Rel A r} a (as : List# A R) → a # as → a # filter as

  filter []             = []
  filter (cons a as ps) with does (P? a)
  ... | true  = cons a (filter as) (filter-# a as ps)
  ... | false = filter as

  filter-# a []        _        = _
  filter-# a (x ∷# xs) (p , ps) with does (P? x)
  ... | true  = p , filter-# a xs ps
  ... | false = filter-# a xs ps

------------------------------------------------------------------------
-- Relationship to List and AllPairs

toList : {R : Rel A r} → List# A R → ∃ (AllPairs R)
toAll  : ∀ {R : Rel A r} {a} as → fresh A R a as → All (R a) (proj₁ (toList as))

toList []             = -, []
toList (cons x xs ps) = -, toAll xs ps ∷ proj₂ (toList xs)

toAll []        ps       = []
toAll (a ∷# as) (p , ps) = p ∷ toAll as ps

fromList   : ∀ {R : Rel A r} {xs} → AllPairs R xs → List# A R
fromList-# : ∀ {R : Rel A r} {x xs} (ps : AllPairs R xs) →
             All (R x) xs → x # fromList ps

fromList []       = []
fromList (r ∷ rs) = cons _ (fromList rs) (fromList-# rs r)

fromList-# []       _        = _
fromList-# (p ∷ ps) (r ∷ rs) = r , fromList-# ps rs


text:
{-

This file contains:

- Definition of propositional truncation

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

open import Cubical.Core.Primitives

-- Propositional truncation as a higher inductive type:

data ∥_∥ {ℓ} (A : Type ℓ) : Type ℓ where
  ∣_∣ : A → ∥ A ∥
  squash : ∀ (x y : ∥ A ∥) → x ≡ y

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
-- Reported by stevan.andjelkovic, 2014-10-23

-- Case splitting on n in the goal g produces the wrong output, it
-- seems like {n} in f is the problem...

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

f : {_ : ℕ}  → Set₁
f {n} = Set
  where
  g : ℕ → Set
  g n = {!n!}


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Equiv.Base where

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

open import Cubical.Core.Glue public
  using ( isEquiv ; equiv-proof ; _≃_ ; equivFun ; equivProof )

fiber : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) (y : B) → Type (ℓ-max ℓ ℓ')
fiber {A = A} f y = Σ[ x ∈ A ] f x ≡ y

-- Helper function for constructing equivalences from pairs (f,g) that cancel each other up to definitional
-- equality. For such (f,g), the result type simplifies to isContr (fiber f b).
strictContrFibers : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} (g : B → A) (b : B)
  → Σ[ t ∈ fiber f (f (g b)) ]
    ((t' : fiber f b) → Path (fiber f (f (g b))) t (g (f (t' .fst)) , cong (f ∘ g) (t' .snd)))
strictContrFibers {f = f} g b .fst = (g b , refl)
strictContrFibers {f = f} g b .snd (a , p) i = (g (p (~ i)) , λ j → f (g (p (~ i ∨ j))))

-- The identity equivalence
idIsEquiv : ∀ {ℓ} (A : Type ℓ) → isEquiv (idfun A)
idIsEquiv A .equiv-proof = strictContrFibers (idfun A)

idEquiv : ∀ {ℓ} (A : Type ℓ) → A ≃ A
idEquiv A .fst = idfun A
idEquiv A .snd = idIsEquiv A

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module par-swap.properties where

open import par-swap
open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Context
open import Data.List using ([] ; [_] ; _∷_ ; List ; _++_)
open import Data.Product

Context1-∥R : ∀{p p'} → (C1 : Context1) → p ∥R p' → ((C1 ∷ []) ⟦ p ⟧c) ∥R ((C1 ∷ []) ⟦ p' ⟧c)
Context1-∥R (ceval (epar₁ q₁)) (∥Rstep dc) = ∥Rstep (dcpar₁ dc)
Context1-∥R (ceval (epar₂ p₂)) (∥Rstep dc) = ∥Rstep (dcpar₂ dc)
Context1-∥R (ceval (eseq q₁)) (∥Rstep dc) = ∥Rstep (dcseq₁ dc)
Context1-∥R (ceval (eloopˢ q₁)) (∥Rstep dc) = ∥Rstep (dcloopˢ₁ dc)
Context1-∥R (ceval (esuspend S)) (∥Rstep dc) = ∥Rstep (dcsuspend dc)
Context1-∥R (ceval etrap) (∥Rstep dc) = ∥Rstep (dctrap dc)
Context1-∥R (csignl S) (∥Rstep dc) = ∥Rstep (dcsignl dc)
Context1-∥R (cpresent₁ S q₁) (∥Rstep dc) = ∥Rstep (dcpresent₁ dc)
Context1-∥R (cpresent₂ S p₂) (∥Rstep dc) = ∥Rstep (dcpresent₂ dc)
Context1-∥R cloop (∥Rstep dc) = ∥Rstep (dcloop dc)
Context1-∥R (cloopˢ₂ p₂) (∥Rstep dc) = ∥Rstep (dcloopˢ₂ dc)
Context1-∥R (cseq₂ p₂) (∥Rstep dc) = ∥Rstep (dcseq₂ dc)
Context1-∥R (cshared s e) (∥Rstep dc) = ∥Rstep (dcshared dc)
Context1-∥R (cvar x e) (∥Rstep dc) = ∥Rstep (dcvar dc)
Context1-∥R (cif₁ x q₁) (∥Rstep dc) = ∥Rstep (dcif₁ dc)
Context1-∥R (cif₂ x p₂) (∥Rstep dc) = ∥Rstep (dcif₂ dc)
Context1-∥R (cenv θ A) (∥Rstep dc) = ∥Rstep (dcenv dc)

Context1-∥R* : ∀ {p q} -> (C1 : Context1) -> p ∥R* q -> ((C1 ∷ []) ⟦ p ⟧c) ∥R* ((C1 ∷ []) ⟦ q ⟧c)
Context1-∥R* C1 ∥R0 = ∥R0
Context1-∥R* C1 (∥Rn p∥Rq q∥R*r) = ∥Rn (Context1-∥R C1 p∥Rq) (Context1-∥R* C1 q∥R*r)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Quotients for Heterogeneous equality
------------------------------------------------------------------------

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

module Relation.Binary.HeterogeneousEquality.Quotients where

open import Function
open import Level hiding (lift)
open import Relation.Binary
open import Relation.Binary.HeterogeneousEquality
open ≅-Reasoning

record Quotient {c ℓ} (S : Setoid c ℓ) : Set (suc (c ⊔ ℓ)) where
  open Setoid S renaming (Carrier to A)
  field
    Q   : Set c
    abs : A → Q

  compat : (B : Q → Set c) (f : ∀ a → B (abs a)) → Set (c ⊔ ℓ)
  compat _ f = {a a′ : A} → a ≈ a′ → f a ≅ f a′

  field
    compat-abs : compat _ abs
    lift       : (B : Q → Set c) (f : ∀ a → B (abs a)) → compat B f → ∀ q → B q
    lift-conv  : {B : Q → Set c} (f : ∀ a → B (abs a)) (p : compat B f) →
                 ∀ a → lift B f p (abs a) ≅ f a

Quotients : ∀ c ℓ → Set (suc (c ⊔ ℓ))
Quotients c ℓ = (S : Setoid c ℓ) → Quotient S

module Properties {c ℓ} {S : Setoid c ℓ} (Qu : Quotient S) where

  open Setoid S renaming (Carrier to A) hiding (refl; sym; trans)
  open Quotient Qu

  module _ {B B′ : Q → Set c} {f : ∀ a → B (abs a)} {p : compat B f} where

   lift-unique : {g : ∀ q → B′ q} → (∀ a → g (abs a) ≅ f a) →
                 ∀ x → lift B f p x ≅ g x
   lift-unique {g} ext = lift _ liftf≅g liftf≅g-ext where

     liftf≅g : ∀ a → lift B f p (abs a) ≅ g (abs a)
     liftf≅g x = begin
       lift _ f p (abs x) ≅⟨ lift-conv f p x ⟩
       f x                ≅⟨ sym (ext x) ⟩
       g (abs x)          ∎

     liftf≅g-ext : ∀ {a a′} → a ≈ a′ → liftf≅g a ≅ liftf≅g a′
     liftf≅g-ext eq = ≅-heterogeneous-irrelevantˡ _ _
                    $ cong (lift B f p) (compat-abs eq)

   lift-ext : {g : ∀ a → B′ (abs a)} {p′ : compat B′ g} → (∀ x → f x ≅ g x) →
              ∀ x → lift B f p x ≅ lift B′ g p′ x
   lift-ext {g} {p′} h = lift-unique $ λ a → begin
       lift B′ g p′ (abs a) ≅⟨ lift-conv g p′ a ⟩
       g a                  ≅⟨ sym (h a) ⟩
       f a                  ∎

  lift-conv-abs : ∀ a → lift (const Q) abs compat-abs a ≅ a
  lift-conv-abs = lift-unique (λ _ → refl)

  lift-fold : {B : Q → Set c} (f : ∀ q → B q) →
              ∀ a → lift B (f ∘ abs) (cong f ∘ compat-abs) a ≅ f a
  lift-fold f = lift-unique (λ _ → refl)

  abs-epimorphism : {B : Q → Set c} {f g : ∀ q → B q} →
                    (∀ x → f (abs x) ≅ g (abs x)) → ∀ q → f q ≅ g q
  abs-epimorphism {B} {f} {g} p q = begin
    f q                                      ≅⟨ sym (lift-fold f q) ⟩
    lift B (f ∘ abs) (cong f ∘ compat-abs) q ≅⟨ lift-ext p q ⟩
    lift B (g ∘ abs) (cong g ∘ compat-abs) q ≅⟨ lift-fold g q ⟩
    g q                                      ∎

------------------------------------------------------------------------
-- Properties provable with extensionality

module _ (ext : ∀ {a b} {A : Set a} {B₁ B₂ : A → Set b} {f₁ : ∀ a → B₁ a}
                {f₂ : ∀ a → B₂ a} → (∀ a → f₁ a ≅ f₂ a) → f₁ ≅ f₂) where

  module Properties₂
         {c ℓ} {S₁ S₂ : Setoid c ℓ} (Qu₁ : Quotient S₁) (Qu₂ : Quotient S₂)
         where

    module S₁  = Setoid S₁
    module S₂  = Setoid S₂
    module Qu₁ = Quotient Qu₁
    module Qu₂ = Quotient Qu₂

    module _  {B : _ → _ → Set c} (f : ∀ s₁ s₂ → B (Qu₁.abs s₁) (Qu₂.abs s₂)) where

     compat₂ : Set _
     compat₂ = ∀ {a b a′ b′} → a S₁.≈ a′ → b S₂.≈ b′ → f a b ≅ f a′ b′

     lift₂ : compat₂ → ∀ q q′ → B q q′
     lift₂ p = Qu₁.lift _ g (ext ∘ g-ext) module Lift₂ where

       g : ∀ a q → B (Qu₁.abs a) q
       g a = Qu₂.lift (B (Qu₁.abs a)) (f a) (p S₁.refl)

       g-ext : ∀ {a a′} → a S₁.≈ a′ → ∀ q → g a q ≅ g a′ q
       g-ext a≈a′ = Properties.lift-ext Qu₂ (λ _ → p a≈a′ S₂.refl)

     lift₂-conv : (p : compat₂) → ∀ a a′ → lift₂ p (Qu₁.abs a) (Qu₂.abs a′) ≅ f a a′
     lift₂-conv p a a′ = begin
       lift₂ p (Qu₁.abs a) (Qu₂.abs a′)
          ≅⟨ cong (_$ (Qu₂.abs a′)) (Qu₁.lift-conv (Lift₂.g p) (ext ∘ Lift₂.g-ext p) a) ⟩
       Lift₂.g p a (Qu₂.abs a′)
          ≡⟨⟩
       Qu₂.lift (B (Qu₁.abs a)) (f a) (p S₁.refl) (Qu₂.abs a′)
          ≅⟨ Qu₂.lift-conv (f a) (p S₁.refl) a′ ⟩
       f a a′
          ∎

  module Properties₃ {c ℓ} {S₁ S₂ S₃ : Setoid c ℓ}
         (Qu₁ : Quotient S₁) (Qu₂ : Quotient S₂) (Qu₃ : Quotient S₃)
         where

    module S₁  = Setoid S₁
    module S₂  = Setoid S₂
    module S₃  = Setoid S₃
    module Qu₁ = Quotient Qu₁
    module Qu₂ = Quotient Qu₂
    module Qu₃ = Quotient Qu₃

    module _ {B : _ → _ → _ → Set c}
             (f : ∀ s₁ s₂ s₃ → B (Qu₁.abs s₁) (Qu₂.abs s₂) (Qu₃.abs s₃)) where

     compat₃ : Set _
     compat₃ = ∀ {a b c a′ b′ c′} → a S₁.≈ a′ → b S₂.≈ b′ → c S₃.≈ c′ →
               f a b c ≅ f a′ b′ c′

     lift₃ : compat₃ → ∀ q₁ q₂ q₃ → B q₁ q₂ q₃
     lift₃ p = Qu₁.lift _ h (ext ∘ h-ext) module Lift₃ where

       g : ∀ a b q → B (Qu₁.abs a) (Qu₂.abs b) q
       g a b = Qu₃.lift (B (Qu₁.abs a) (Qu₂.abs b)) (f a b) (p S₁.refl S₂.refl)

       g-ext : ∀ {a a′ b b′} → a S₁.≈ a′ → b S₂.≈ b′ → ∀ c → g a b c ≅ g a′ b′ c
       g-ext a≈a′ b≈b′ = Properties.lift-ext Qu₃ (λ _ → p a≈a′ b≈b′ S₃.refl)

       h : ∀ a q₂ q₃ → B (Qu₁.abs a) q₂ q₃
       h a = Qu₂.lift (λ b → ∀ q → B (Qu₁.abs a) b q) (g a) (ext ∘ g-ext S₁.refl)

       h-ext : ∀ {a a′} → a S₁.≈ a′ → ∀ b → h a b ≅ h a′ b
       h-ext a≈a′ = Properties.lift-ext Qu₂ $ λ _ → ext (g-ext a≈a′ S₂.refl)


text:
-- Reasoning with both a strict and non-strict relation.
{-# OPTIONS --cubical --no-import-sorts --safe #-}

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

module Cubical.Relation.Binary.Reasoning.Base.Double {a ℓ₁ ℓ₂} {A : Type a}
  {_≤_ : RawRel A ℓ₁} {_<_ : RawRel A ℓ₂}
  (≤-isPreorder : IsPreorder _≤_)
  (<-transitive : Transitive _<_) (<⇒≤ : _<_ ⇒ _≤_)
  (<-≤-transitive : Trans _<_ _≤_ _<_) (≤-<-transitive : Trans _≤_ _<_ _<_)
  where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Prod using (proj₁; proj₂)
open import Cubical.Foundations.Function using (case_of_; id)
open import Cubical.Relation.Nullary using (Dec; yes; no; IsYes; toWitness)

open IsPreorder ≤-isPreorder
  renaming
  ( reflexive  to ≤-reflexive
  ; transitive to ≤-transitive
  )

------------------------------------------------------------------------
-- A datatype to abstract over the current relation

infix 4 _IsRelatedTo_

data _IsRelatedTo_ (x y : A) : Type (ℓ-max a (ℓ-max ℓ₁ ℓ₂)) where
  strict    : (x<y : x < y) → x IsRelatedTo y
  nonstrict : (x≤y : x ≤ y) → x IsRelatedTo y

------------------------------------------------------------------------
-- Types that are used to ensure that the final relation proved by the
-- chain of reasoning can be converted into the required relation.

data IsStrict {x y} : x IsRelatedTo y → Type (ℓ-max a (ℓ-max ℓ₁ ℓ₂)) where
  isStrict : ∀ x<y → IsStrict (strict x<y)

IsStrict? : ∀ {x y} (x≲y : x IsRelatedTo y) → Dec (IsStrict x≲y)
IsStrict? (strict    x<y) = yes (isStrict x<y)
IsStrict? (nonstrict _)   = no λ()

extractStrict : ∀ {x y} {x≲y : x IsRelatedTo y} → IsStrict x≲y → x < y
extractStrict (isStrict x<y) = x<y

------------------------------------------------------------------------
-- Reasoning combinators

infix  0 begin_ begin-strict_
infixr 1 _<⟨_⟩_ _≤⟨_⟩_ _≡⟨_⟩_ _≡˘⟨_⟩_ _≡⟨⟩_
infix  2 _∎

-- Beginnings of various types of proofs

begin_ : ∀ {x y} → x IsRelatedTo y → x ≤ y
begin strict    x<y = <⇒≤ x<y
begin nonstrict x≤y = x≤y

begin-strict_ : ∀ {x y} (r : x IsRelatedTo y) → {s : IsYes (IsStrict? r)} → x < y
begin-strict_ r {s} = extractStrict (toWitness s)

-- Step with the strict relation

_<⟨_⟩_ : ∀ (x : A) {y z} → x < y → y IsRelatedTo z → x IsRelatedTo z
x <⟨ x<y ⟩ strict    y<z = strict (<-transitive x<y y<z)
x <⟨ x<y ⟩ nonstrict y≤z = strict (<-≤-transitive x<y y≤z)

-- Step with the non-strict relation

_≤⟨_⟩_ : ∀ (x : A) {y z} → x ≤ y → y IsRelatedTo z → x IsRelatedTo z
x ≤⟨ x≤y ⟩ strict    y<z = strict    (≤-<-transitive x≤y y<z)
x ≤⟨ x≤y ⟩ nonstrict y≤z = nonstrict (≤-transitive x≤y y≤z)

-- Step with non-trivial propositional equality

_≡⟨_⟩_ : ∀ (x : A) {y z} → x ≡ y → y IsRelatedTo z → x IsRelatedTo z
_≡⟨_⟩_ x {_} {z} x≡y y≲z = J (λ w _ → w IsRelatedTo z) y≲z (sym x≡y)

-- Flipped step with non-trivial propositional equality

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

-- Step with trivial propositional equality

_≡⟨⟩_ : ∀ (x : A) {y} → x IsRelatedTo y → x IsRelatedTo y
x ≡⟨⟩ x≲y = x≲y

-- Syntax for path definition

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

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

-- Termination step

_∎ : ∀ x → x IsRelatedTo x
x ∎ = nonstrict ≤-reflexive