text:
------------------------------------------------------------------------
-- CCS
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude

module Labelled-transition-system.CCS {ℓ} (Name : Type ℓ) where

open import Equality.Propositional
open import Prelude.Size

open import Bool equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)

open import Labelled-transition-system

------------------------------------------------------------------------
-- Fixity declarations

infix  12 _∙
infixr 12 _·_ _∙_
infix  10 !_
infix   8 _⊕_
infix   6 _∣_
infix   5 _[_] _[_]′
infix   4 _[_]⟶_ _∉_

------------------------------------------------------------------------
-- CCS, roughly as defined in "Enhancements of the bisimulation proof
-- method" by Pous and Sangiorgi, with support for corecursive
-- processes (instead of the named process constants presented in
-- "Coinduction All the Way Up" by Pous)

-- Names with kinds: (a , true) stands for "a", and (a , false) stands
-- for "a̅".

Name-with-kind : Type ℓ
Name-with-kind = Name × Bool

-- Turns names of one kind into names of the other kind.

co : Name-with-kind → Name-with-kind
co (a , kind) = a , not kind

-- Actions.

data Action : Type ℓ where
  name : Name-with-kind → Action
  τ    : Action

-- The only silent action is τ.

is-silent : Action → Bool
is-silent (name _) = false
is-silent τ        = true

-- Processes.

mutual

  data Proc (i : Size) : Type ℓ where
    ∅       : Proc i
    _∣_ _⊕_ : Proc i → Proc i → Proc i
    _·_     : Action → Proc′ i → Proc i
    ⟨ν_⟩    : Name → Proc i → Proc i
    !_      : Proc i → Proc i

  record Proc′ (i : Size) : Type ℓ where
    coinductive
    field
      force : {j : Size< i} → Proc j

open Proc′ public

-- An inductive variant of _·_.

_∙_ : ∀ {i} → Action → Proc i → Proc i
μ ∙ P = μ · λ { .force → P }

-- An abbreviation.

_∙ : Name-with-kind → Proc ∞
a ∙ = name a ∙ ∅

-- The predicate a ∉ μ holds if a is not the underlying name of μ (if
-- any).

_∉_ : Name → Action → Type ℓ
a ∉ name (b , _) = ¬ a ≡ b
a ∉ τ            = ↑ ℓ ⊤

-- Transition relation.

data _[_]⟶_ : Proc ∞ → Action → Proc ∞ → Type ℓ where
  par-left    : ∀ {P Q P′ μ} → P [ μ ]⟶ P′ → P ∣ Q [ μ ]⟶ P′ ∣ Q
  par-right   : ∀ {P Q Q′ μ} → Q [ μ ]⟶ Q′ → P ∣ Q [ μ ]⟶ P  ∣ Q′
  par-τ       : ∀ {P P′ Q Q′ a} →
                P [ name a ]⟶ P′ → Q [ name (co a) ]⟶ Q′ →
                P ∣ Q [ τ ]⟶ P′ ∣ Q′
  sum-left    : ∀ {P Q P′ μ} → P [ μ ]⟶ P′ → P ⊕ Q [ μ ]⟶ P′
  sum-right   : ∀ {P Q Q′ μ} → Q [ μ ]⟶ Q′ → P ⊕ Q [ μ ]⟶ Q′
  action      : ∀ {P μ} → μ · P [ μ ]⟶ force P
  restriction : ∀ {P P′ a μ} →
                a ∉ μ → P [ μ ]⟶ P′ → ⟨ν a ⟩ P [ μ ]⟶ ⟨ν a ⟩ P′
  replication : ∀ {P P′ μ} → ! P ∣ P [ μ ]⟶ P′ → ! P [ μ ]⟶ P′

-- The CCS LTS.

CCS : LTS ℓ
CCS = record
  { Proc      = Proc ∞
  ; Label     = Action
  ; _[_]⟶_    = _[_]⟶_
  ; is-silent = is-silent
  }

open LTS CCS public hiding (Proc; _[_]⟶_; is-silent)

------------------------------------------------------------------------
-- Contexts and some related definitions, roughly following
-- "Enhancements of the bisimulation proof method" by Pous and
-- Sangiorgi

mutual

  -- Polyadic contexts.

  data Context (i : Size) (n : ℕ) : Type ℓ where
    hole    : (x : Fin n) → Context i n
    ∅       : Context i n
    _∣_ _⊕_ : Context i n → Context i n → Context i n
    _·_     : (μ : Action) → Context′ i n → Context i n
    ⟨ν_⟩    : (a : Name) → Context i n → Context i n
    !_      : Context i n → Context i n

  record Context′ (i : Size) (n : ℕ) : Type ℓ where
    coinductive
    field
      force : {j : Size< i} → Context j n

open Context′ public

mutual

  -- Hole filling.

  _[_] : ∀ {i n} → Context i n → (Fin n → Proc ∞) → Proc i
  hole x   [ Ps ] = Ps x
  ∅        [ Ps ] = ∅
  C₁ ∣ C₂  [ Ps ] = (C₁ [ Ps ]) ∣ (C₂ [ Ps ])
  C₁ ⊕ C₂  [ Ps ] = (C₁ [ Ps ]) ⊕ (C₂ [ Ps ])
  μ · C    [ Ps ] = μ · (C [ Ps ]′)
  ⟨ν a ⟩ C [ Ps ] = ⟨ν a ⟩ (C [ Ps ])
  ! C      [ Ps ] = ! (C [ Ps ])

  _[_]′ : ∀ {i n} → Context′ i n → (Fin n → Proc ∞) → Proc′ i
  force (C [ Ps ]′) = force C [ Ps ]

-- A context is weakly guarded if every hole is under a prefix (μ ·_).

data Weakly-guarded {n : ℕ} : Context ∞ n → Type ℓ where
  ∅      : Weakly-guarded ∅
  _∣_    : ∀ {C₁ C₂} →
           Weakly-guarded C₁ → Weakly-guarded C₂ →
           Weakly-guarded (C₁ ∣ C₂)
  _⊕_    : ∀ {C₁ C₂} →
           Weakly-guarded C₁ → Weakly-guarded C₂ →
           Weakly-guarded (C₁ ⊕ C₂)
  action : ∀ {μ C} → Weakly-guarded (μ · C)
  ⟨ν⟩    : ∀ {a C} → Weakly-guarded C → Weakly-guarded (⟨ν a ⟩ C)
  !_     : ∀ {C} → Weakly-guarded C → Weakly-guarded (! C)

-- Turns processes into contexts without holes.

context : ∀ {i n} → Proc i → Context i n
context ∅          = ∅
context (P₁ ∣ P₂)  = context P₁ ∣ context P₂
context (P₁ ⊕ P₂)  = context P₁ ⊕ context P₂
context (μ · P)    = μ · λ { .force → context (force P) }
context (⟨ν a ⟩ P) = ⟨ν a ⟩ (context P)
context (! P)      = ! context P

-- Non-degenerate contexts.

mutual

  data Non-degenerate (i : Size) {n : ℕ} : Context ∞ n → Type ℓ where
    hole   : ∀ {x} → Non-degenerate i (hole x)
    ∅      : Non-degenerate i ∅
    _∣_    : ∀ {C₁ C₂} →
             Non-degenerate i C₁ → Non-degenerate i C₂ →
             Non-degenerate i (C₁ ∣ C₂)
    _⊕_    : ∀ {C₁ C₂} →
             Non-degenerate-summand i C₁ →
             Non-degenerate-summand i C₂ →
             Non-degenerate i (C₁ ⊕ C₂)
    action : ∀ {μ C} →
             Non-degenerate′ i (force C) → Non-degenerate i (μ · C)
    ⟨ν⟩    : ∀ {a C} → Non-degenerate i C → Non-degenerate i (⟨ν a ⟩ C)
    !_     : ∀ {C} → Non-degenerate i C → Non-degenerate i (! C)

  data Non-degenerate-summand (i : Size) {n : ℕ} :
                              Context ∞ n → Type ℓ where
    process : ∀ P → Non-degenerate-summand i (context P)
    action  : ∀ {μ C} →
              Non-degenerate′ i (force C) →
              Non-degenerate-summand i (μ · C)

  record Non-degenerate′ (i : Size) {n} (C : Context ∞ n) : Type ℓ where
    coinductive
    field
      force : {j : Size< i} → Non-degenerate j C

open Non-degenerate′ public

------------------------------------------------------------------------
-- Very strong bisimilarity

-- "Very strong" bisimilarity for processes: Equal ∞ P Q means that P
-- and Q have the same structure.

mutual

  data Equal (i : Size) : Proc ∞ → Proc ∞ → Type ℓ where
    ∅    : Equal i ∅ ∅
    _∣_  : ∀ {P₁ P₂ Q₁ Q₂} →
           Equal i P₁ P₂ → Equal i Q₁ Q₂ → Equal i (P₁ ∣ Q₁) (P₂ ∣ Q₂)
    _⊕_  : ∀ {P₁ P₂ Q₁ Q₂} →
           Equal i P₁ P₂ → Equal i Q₁ Q₂ → Equal i (P₁ ⊕ Q₁) (P₂ ⊕ Q₂)
    _·_  : ∀ {μ₁ μ₂ P₁ P₂} →
           μ₁ ≡ μ₂ → Equal′ i (force P₁) (force P₂) →
           Equal i (μ₁ · P₁) (μ₂ · P₂)
    ⟨ν_⟩ : ∀ {a₁ a₂ P₁ P₂} →
           a₁ ≡ a₂ → Equal i P₁ P₂ → Equal i (⟨ν a₁ ⟩ P₁) (⟨ν a₂ ⟩ P₂)
    !_   : ∀ {P₁ P₂} → Equal i P₁ P₂ → Equal i (! P₁) (! P₂)

  record Equal′ (i : Size) (P₁ P₂ : Proc ∞) : Type ℓ where
    coinductive
    field
      force : {j : Size< i} → Equal j P₁ P₂

open Equal′ public

-- Extensionality for very strong bisimilarity.

Proc-extensionality : Type ℓ
Proc-extensionality = ∀ {P Q} → Equal ∞ P Q → P ≡ Q

------------------------------------------------------------------------
-- Some lemmas

-- The co function is involutive.

co-involutive : ∀ a → co (co a) ≡ a
co-involutive (a , kind) =
  (a , not (not kind))  ≡⟨ cong (_ ,_) $ not-involutive kind ⟩∎
  (a , kind)            ∎

-- A name is not equal to the corresponding coname.

id≢co : ∀ {a} → a ≢ co a
id≢co {a} =
  a ≡ co a                 ↝⟨ cong proj₂ ⟩
  proj₂ a ≡ not (proj₂ a)  ↝⟨ not≡⇒≢ _ _ ∘ sym ⟩
  proj₂ a ≢ proj₂ a        ↝⟨ _$ refl ⟩□
  ⊥                        □

-- A cancellation law.

cancel-name : ∀ {a b} → name a ≡ name b → a ≡ b
cancel-name refl = refl

-- A disjointness law.

name≢τ : ∀ {a} → name a ≢ τ
name≢τ ()

-- The only silent label is τ.

silent≡τ : ∀ {μ} → Silent μ → μ ≡ τ
silent≡τ {τ}      _  = refl
silent≡τ {name _} ()

-- Names do not match (the only silent label) τ.

∉τ : ∀ {μ a} → Silent μ → a ∉ μ
∉τ s rewrite silent≡τ s = _

-- A variant of par-τ.

par-τ′ : ∀ {P P′ Q Q′ a b} →
         b ≡ co a → P [ name a ]⟶ P′ → Q [ name b ]⟶ Q′ →
         P ∣ Q [ τ ]⟶ P′ ∣ Q′
par-τ′ refl = par-τ

-- The process μ · P can only make μ-transitions.

·-only : ∀ {μ₁ μ₂ P Q} → μ₁ · P [ μ₂ ]⟶ Q → μ₁ ≡ μ₂
·-only action = refl

-- The process μ · P can only transition to force P.

·-only⟶ : ∀ {μ₁ μ₂ P Q} → μ₁ · P [ μ₂ ]⟶ Q → Q ≡ force P
·-only⟶ action = refl

-- A simple corollary.

names-are-not-inverted :
  ∀ {a P Q} → ¬ (name a · P [ name (co a) ]⟶ Q)
names-are-not-inverted {a} {P} {Q} =
  name a · P [ name (co a) ]⟶ Q  ↝⟨ ·-only ⟩
  name a ≡ name (co a)           ↝⟨ id≢co ∘ cancel-name ⟩□
  ⊥                              □

-- If P₁ and P₂ can only make μ-transitions, then P₁ ∣ P₂ can only
-- make μ-transitions.

∣-only : ∀ {μ₀ P₁ P₂} →
         (∀ {P′ μ} → P₁ [ μ ]⟶ P′ → μ₀ ≡ μ) →
         (∀ {P′ μ} → P₂ [ μ ]⟶ P′ → μ₀ ≡ μ) →
         ∀ {P′ μ} → P₁ ∣ P₂ [ μ ]⟶ P′ → μ₀ ≡ μ
∣-only      only₁ only₂ (par-left tr)           = only₁ tr
∣-only      only₁ only₂ (par-right tr)          = only₂ tr
∣-only {μ₀} only₁ only₂ (par-τ {a = a} tr₁ tr₂) = ⊥-elim (
                                  $⟨ only₁ tr₁ , only₂ tr₂ ⟩
  μ₀ ≡ name a × μ₀ ≡ name (co a)  ↝⟨ uncurry trans ∘ Σ-map sym id ⟩
  name a ≡ name (co a)            ↝⟨ id≢co ∘ cancel-name ⟩□
  ⊥                               □)

-- If P can only make μ-transitions, then ! P can only make
-- μ-transitions.

!-only : ∀ {μ₀ P} →
         (∀ {P′ μ} → P [ μ ]⟶ P′ → μ₀ ≡ μ) →
         ∀ {P′ μ} → ! P [ μ ]⟶ P′ → μ₀ ≡ μ
!-only      only (replication (par-left  tr)) = !-only only tr
!-only      only (replication (par-right tr)) = only tr
!-only {μ₀} only (replication (par-τ {a = a} tr₁ tr₂)) = ⊥-elim (
                                  $⟨ !-only only tr₁ , only tr₂ ⟩
  μ₀ ≡ name a × μ₀ ≡ name (co a)  ↝⟨ uncurry trans ∘ Σ-map sym id ⟩
  name a ≡ name (co a)            ↝⟨ id≢co ∘ cancel-name ⟩□
  ⊥                               □)

-- If P₁ and P₂ can only make μ-transitions, then P₁ ⊕ P₂ can only
-- make μ-transitions.

⊕-only : ∀ {μ₀ P₁ P₂} →
         (∀ {P′ μ} → P₁ [ μ ]⟶ P′ → μ₀ ≡ μ) →
         (∀ {P′ μ} → P₂ [ μ ]⟶ P′ → μ₀ ≡ μ) →
         ∀ {P′ μ} → P₁ ⊕ P₂ [ μ ]⟶ P′ → μ₀ ≡ μ
⊕-only only₁ only₂ (sum-left tr)  = only₁ tr
⊕-only only₁ only₂ (sum-right tr) = only₂ tr

-- If P can only make μ-transitions, then ⟨ν a ⟩ P can only make
-- μ-transitions.

⟨ν⟩-only : ∀ {μ₀ a P} →
           (∀ {P′ μ} → P [ μ ]⟶ P′ → μ₀ ≡ μ) →
           ∀ {P′ μ} → ⟨ν a ⟩ P [ μ ]⟶ P′ → μ₀ ≡ μ
⟨ν⟩-only only (restriction _ tr) = only tr

-- A simple lemma.

·⊕·-co :
  ∀ {a b c P Q R S} →
  name a · P ⊕ name b · Q [ name c ]⟶      R →
  name a · P ⊕ name b · Q [ name (co c) ]⟶ S →
  b ≡ co a × (R ≡ force P × S ≡ force Q ⊎ R ≡ force Q × S ≡ force P)
·⊕·-co (sum-left  action)
       (sum-left  tr)     = ⊥-elim (names-are-not-inverted tr)
·⊕·-co (sum-left  action)
       (sum-right action) = refl , inj₁ (refl , refl)
·⊕·-co (sum-right action)
       (sum-left  action) =   sym (co-involutive _)
                            , inj₂ (refl , refl)
·⊕·-co (sum-right action)
       (sum-right tr)     = ⊥-elim (names-are-not-inverted tr)

-- Very strong bisimilarity is reflexive.

Proc-refl : ∀ {i} P → Equal i P P
Proc-refl ∅          = ∅
Proc-refl (P₁ ∣ P₂)  = Proc-refl P₁ ∣ Proc-refl P₂
Proc-refl (P₁ ⊕ P₂)  = Proc-refl P₁ ⊕ Proc-refl P₂
Proc-refl (μ · P)    = refl · λ { .force → Proc-refl (force P) }
Proc-refl (⟨ν a ⟩ P) = ⟨ν refl ⟩ (Proc-refl P)
Proc-refl (! P)      = ! Proc-refl P

-- Very strong bisimilarity is symmetric.

Proc-sym : ∀ {i P Q} → Equal i P Q → Equal i Q P
Proc-sym ∅          = ∅
Proc-sym (P₁ ∣ P₂)  = Proc-sym P₁ ∣ Proc-sym P₂
Proc-sym (P₁ ⊕ P₂)  = Proc-sym P₁ ⊕ Proc-sym P₂
Proc-sym (p · P)    = sym p · λ { .force → Proc-sym (force P) }
Proc-sym (⟨ν p ⟩ P) = ⟨ν sym p ⟩ (Proc-sym P)
Proc-sym (! P)      = ! Proc-sym P

-- Very strong bisimilarity is transitive.

Proc-trans : ∀ {i P Q R} → Equal i P Q → Equal i Q R → Equal i P R
Proc-trans ∅          ∅          = ∅
Proc-trans (P₁ ∣ P₂)  (Q₁ ∣ Q₂)  = Proc-trans P₁ Q₁ ∣ Proc-trans P₂ Q₂
Proc-trans (P₁ ⊕ P₂)  (Q₁ ⊕ Q₂)  = Proc-trans P₁ Q₁ ⊕ Proc-trans P₂ Q₂
Proc-trans (p · P)    (q · Q)    = trans p q · λ { .force →
                                     Proc-trans (force P) (force Q) }
Proc-trans (⟨ν p ⟩ P) (⟨ν q ⟩ Q) = ⟨ν trans p q ⟩ (Proc-trans P Q)
Proc-trans (! P)      (! Q)      = ! Proc-trans P Q

-- Weakening of contexts.

weaken : ∀ {i n} → Context i n → Context i (suc n)
weaken (hole x)   = hole (fsuc x)
weaken ∅          = ∅
weaken (C₁ ∣ C₂)  = weaken C₁ ∣ weaken C₂
weaken (C₁ ⊕ C₂)  = weaken C₁ ⊕ weaken C₂
weaken (μ · C)    = μ · λ { .force → weaken (force C) }
weaken (⟨ν a ⟩ C) = ⟨ν a ⟩ (weaken C)
weaken (! C)      = ! weaken C

-- A lemma relating weakening and hole filling.

weaken-[] :
  ∀ {i n ps} (C : Context ∞ n) →
  Equal i (weaken C [ ps ]) (C [ ps ∘ fsuc ])
weaken-[] (hole x)   = Proc-refl _
weaken-[] ∅          = ∅
weaken-[] (C₁ ∣ C₂)  = weaken-[] C₁ ∣ weaken-[] C₂
weaken-[] (C₁ ⊕ C₂)  = weaken-[] C₁ ⊕ weaken-[] C₂
weaken-[] (μ · C)    = refl · λ { .force → weaken-[] (force C) }
weaken-[] (⟨ν a ⟩ C) = ⟨ν refl ⟩ (weaken-[] C)
weaken-[] (! C)      = ! weaken-[] C

-- The result of filling the holes in the context "context P" is P.

context-[] : ∀ {i n} {Ps : Fin n → Proc ∞} P →
             Equal i P (context P [ Ps ])
context-[] ∅          = ∅
context-[] (P₁ ∣ P₂)  = context-[] P₁ ∣ context-[] P₂
context-[] (P₁ ⊕ P₂)  = context-[] P₁ ⊕ context-[] P₂
context-[] (μ · P)    = refl · λ { .force → context-[] (force P) }
context-[] (⟨ν a ⟩ P) = ⟨ν refl ⟩ (context-[] P)
context-[] (! P)      = ! (context-[] P)

-- The contexts constructed by the context function are always
-- non-degenerate.

context-non-degenerate :
  ∀ {i n} (P : Proc ∞) → Non-degenerate i (context {n = n} P)
context-non-degenerate ∅          = ∅
context-non-degenerate (P₁ ∣ P₂)  = context-non-degenerate P₁ ∣
                                    context-non-degenerate P₂
context-non-degenerate (P₁ ⊕ P₂)  = process P₁ ⊕ process P₂
context-non-degenerate (μ · P)    = action λ { .force →
                                      context-non-degenerate (force P) }
context-non-degenerate (⟨ν a ⟩ P) = ⟨ν⟩ (context-non-degenerate P)
context-non-degenerate (! P)      = ! context-non-degenerate P

mutual

  -- A relation expressing that a certain process matches a certain
  -- context.

  data Matches (i : Size) {n} : Proc ∞ → Context ∞ n → Type ℓ where
    hole   : ∀ {P} (x : Fin n) → Matches i P (hole x)
    ∅      : Matches i ∅ ∅
    _∣_    : ∀ {P₁ P₂ C₁ C₂} →
             Matches i P₁ C₁ → Matches i P₂ C₂ →
             Matches i (P₁ ∣ P₂) (C₁ ∣ C₂)
    _⊕_    : ∀ {P₁ P₂ C₁ C₂} →
             Matches i P₁ C₁ → Matches i P₂ C₂ →
             Matches i (P₁ ⊕ P₂) (C₁ ⊕ C₂)
    action : ∀ {μ P C} →
             Matches′ i (force P) (force C) →
             Matches i (μ · P) (μ · C)
    ⟨ν⟩    : ∀ {a P C} → Matches i P C → Matches i (⟨ν a ⟩ P) (⟨ν a ⟩ C)
    !_     : ∀ {P C} → Matches i P C → Matches i (! P) (! C)

  record Matches′
           (i : Size) {n} (P : Proc ∞) (C : Context ∞ n) : Type ℓ where
    coinductive
    field
      force : {j : Size< i} → Matches j P C

open Matches′ public

-- The process obtained by filling a context's holes matches the
-- context.

Matches-[] : ∀ {i n Ps} (C : Context ∞ n) → Matches i (C [ Ps ]) C
Matches-[] (hole x)   = hole x
Matches-[] ∅          = ∅
Matches-[] (C₁ ∣ C₂)  = Matches-[] C₁ ∣ Matches-[] C₂
Matches-[] (C₁ ⊕ C₂)  = Matches-[] C₁ ⊕ Matches-[] C₂
Matches-[] (μ · C)    = action λ { .force → Matches-[] (force C) }
Matches-[] (⟨ν a ⟩ C) = ⟨ν⟩ (Matches-[] C)
Matches-[] (! C)      = ! Matches-[] C

-- Matches respects very strong bisimilarity.

Matches-cong : ∀ {i P Q n} {C : Context ∞ n} →
               Equal i P Q → Matches i P C → Matches i Q C
Matches-cong _             (hole x)   = hole x
Matches-cong ∅             ∅          = ∅
Matches-cong (p₁ ∣ p₂)     (q₁ ∣ q₂)  = Matches-cong p₁ q₁ ∣
                                        Matches-cong p₂ q₂
Matches-cong (p₁ ⊕ p₂)     (q₁ ⊕ q₂)  = Matches-cong p₁ q₁ ⊕
                                        Matches-cong p₂ q₂
Matches-cong (refl · p)    (action q) = action λ { .force →
                                          Matches-cong (force p)
                                                       (force q) }
Matches-cong (⟨ν refl ⟩ p) (⟨ν⟩ q)    = ⟨ν⟩ (Matches-cong p q)
Matches-cong (! p)         (! q)      = ! Matches-cong p q

-- A predicate that identifies a process as being finite. Note that
-- this is an inductive definition.

data Finite : Proc ∞ → Type ℓ where
  ∅      : Finite ∅
  _∣_    : ∀ {P Q} → Finite P → Finite Q → Finite (P ∣ Q)
  _⊕_    : ∀ {P Q} → Finite P → Finite Q → Finite (P ⊕ Q)
  action : ∀ {μ P} → Finite (force P) → Finite (μ · P)
  ⟨ν_⟩   : ∀ {a P} → Finite P → Finite (⟨ν a ⟩ P)
  !_     : ∀ {P} → Finite P → Finite (! P)

-- The transition relation takes finite processes to finite processes.

finite→finite : ∀ {P μ Q} → P [ μ ]⟶ Q → Finite P → Finite Q
finite→finite (par-left tr)       (f₁ ∣ f₂)  = finite→finite tr f₁ ∣ f₂
finite→finite (par-right tr)      (f₁ ∣ f₂)  = f₁ ∣ finite→finite tr f₂
finite→finite (par-τ tr₁ tr₂)     (f₁ ∣ f₂)  = finite→finite tr₁ f₁ ∣
                                               finite→finite tr₂ f₂
finite→finite (sum-left tr)       (f₁ ⊕ f₂)  = finite→finite tr f₁
finite→finite (sum-right tr)      (f₁ ⊕ f₂)  = finite→finite tr f₂
finite→finite action              (action f) = f
finite→finite (restriction a∉ tr) ⟨ν f ⟩     = ⟨ν finite→finite tr f ⟩
finite→finite (replication tr)    (! f)      = finite→finite tr (! f ∣ f)

-- Subprocess P Q means that P is a syntactic subprocess of Q.

data Subprocess (P : Proc ∞) : Proc ∞ → Type ℓ where
  refl        : ∀ {Q} → Equal ∞ P Q → Subprocess P Q
  par-left    : ∀ {Q₁ Q₂} → Subprocess P Q₁ → Subprocess P (Q₁ ∣ Q₂)
  par-right   : ∀ {Q₁ Q₂} → Subprocess P Q₂ → Subprocess P (Q₁ ∣ Q₂)
  sum-left    : ∀ {Q₁ Q₂} → Subprocess P Q₁ → Subprocess P (Q₁ ⊕ Q₂)
  sum-right   : ∀ {Q₁ Q₂} → Subprocess P Q₂ → Subprocess P (Q₁ ⊕ Q₂)
  action      : ∀ {μ Q} → Subprocess P (force Q) → Subprocess P (μ · Q)
  restriction : ∀ {a Q} → Subprocess P Q → Subprocess P (⟨ν a ⟩ Q)
  replication : ∀ {Q} → Subprocess P Q → Subprocess P (! Q)

-- A process is regular if it has a finite number of distinct
-- subprocesses.

Regular : Proc ∞ → Type ℓ
Regular P =
  ∃ λ n → ∃ λ (Qs : Fin n → Proc ∞) →
    ∀ {Q} → Subprocess Q P →
      ∃ λ (i : Fin n) → Equal ∞ Q (Qs i)

-- Lemma 6.2.15 from "Enhancements of the bisimulation proof method".
-- That text claims that the lemma is proved by induction on the
-- structure of the context. Perhaps that is possible, but the proof
-- below uses induction on the structure of the transition relation,
-- and in the replication case's recursive call the context is not
-- structurally smaller.

6-2-15 :
  ∀ {n Ps μ P}
  (C : Context ∞ n) → Weakly-guarded C →
  C [ Ps ] [ μ ]⟶ P →
  ∃ λ (C′ : Context ∞ n) →
    P ≡ C′ [ Ps ] × ∀ Qs → C [ Qs ] [ μ ]⟶ C′ [ Qs ]
6-2-15 ∅          ∅         ()
6-2-15 (C₁ ∣ C₂)  (w₁ ∣ w₂) (par-left  tr)       = Σ-map (_∣ C₂) (Σ-map (cong (_∣ _)) (par-left  ∘_)) (6-2-15 C₁ w₁ tr)
6-2-15 (C₁ ∣ C₂)  (w₁ ∣ w₂) (par-right tr)       = Σ-map (C₁ ∣_) (Σ-map (cong (_ ∣_)) (par-right ∘_)) (6-2-15 C₂ w₂ tr)
6-2-15 (C₁ ∣ C₂)  (w₁ ∣ w₂) (par-τ tr₁ tr₂)      = Σ-zip _∣_ (Σ-zip (cong₂ _)
                                                                    (λ trs₁ trs₂ Qs → par-τ (trs₁ Qs) (trs₂ Qs)))
                                                     (6-2-15 C₁ w₁ tr₁) (6-2-15 C₂ w₂ tr₂)
6-2-15 (C₁ ⊕ C₂)  (w₁ ⊕ w₂) (sum-left  tr)       = Σ-map id (Σ-map id (sum-left  ∘_)) (6-2-15 C₁ w₁ tr)
6-2-15 (C₁ ⊕ C₂)  (w₁ ⊕ w₂) (sum-right tr)       = Σ-map id (Σ-map id (sum-right ∘_)) (6-2-15 C₂ w₂ tr)
6-2-15 (μ · C)    action    action               = force C , refl , λ _ → action
6-2-15 (⟨ν a ⟩ C) (⟨ν⟩ w)   (restriction a∉μ tr) = Σ-map ⟨ν a ⟩ (Σ-map (cong _) (restriction a∉μ ∘_)) (6-2-15 C w tr)
6-2-15 (! C)      (! w)     (replication tr)     = Σ-map id (Σ-map id (replication ∘_)) (6-2-15 (! C ∣ C) (! w ∣ w) tr)

-- A variant of the previous lemma.

6-2-15-nd :
  Proc-extensionality →
  ∀ {n Ps μ P}
  (C : Context ∞ n) → Weakly-guarded C → Non-degenerate ∞ C →
  C [ Ps ] [ μ ]⟶ P →
  ∃ λ (C′ : Context ∞ n) →
    Non-degenerate ∞ C′ ×
    P ≡ C′ [ Ps ] × ∀ Qs → C [ Qs ] [ μ ]⟶ C′ [ Qs ]
6-2-15-nd ext ∅          ∅         ∅ ()
6-2-15-nd ext (C₁ ∣ C₂)  (w₁ ∣ w₂) (n₁ ∣ n₂)         (par-left  tr)       = Σ-map (_∣ C₂) (Σ-map (_∣ n₂) (Σ-map (cong (_∣ _)) (par-left  ∘_)))
                                                                              (6-2-15-nd ext C₁ w₁ n₁ tr)
6-2-15-nd ext (C₁ ∣ C₂)  (w₁ ∣ w₂) (n₁ ∣ n₂)         (par-right tr)       = Σ-map (C₁ ∣_) (Σ-map (n₁ ∣_) (Σ-map (cong (_ ∣_)) (par-right ∘_)))
                                                                              (6-2-15-nd ext C₂ w₂ n₂ tr)
6-2-15-nd ext (C₁ ∣ C₂)  (w₁ ∣ w₂) (n₁ ∣ n₂)         (par-τ tr₁ tr₂)      = Σ-zip _∣_ (Σ-zip _∣_ (Σ-zip (cong₂ _) (λ trs₁ trs₂ Qs →
                                                                                par-τ (trs₁ Qs) (trs₂ Qs))))
                                                                              (6-2-15-nd ext C₁ w₁ n₁ tr₁) (6-2-15-nd ext C₂ w₂ n₂ tr₂)
6-2-15-nd ext (μ · C)    action    (action n)        action               = force C , force n , refl , λ _ → action
6-2-15-nd ext (⟨ν a ⟩ C) (⟨ν⟩ w)   (⟨ν⟩ n)           (restriction a∉μ tr) = Σ-map ⟨ν a ⟩ (Σ-map ⟨ν⟩ (Σ-map (cong _) (restriction a∉μ ∘_)))
                                                                              (6-2-15-nd ext C w n tr)
6-2-15-nd ext (! C)      (! w)     (! n)             (replication tr)     = Σ-map id (Σ-map id (Σ-map id (replication ∘_)))
                                                                              (6-2-15-nd ext (! C ∣ C) (! w ∣ w) (! n ∣ n) tr)
6-2-15-nd ext (C₁ ⊕ C₂)  (w₁ ⊕ w₂) (action n₁  ⊕ n₂) (sum-left  tr)       = Σ-map id (Σ-map id (Σ-map id (sum-left ∘_)))
                                                                              (6-2-15-nd ext (_ · _) action (action n₁) tr)
6-2-15-nd ext {Ps = Ps} {P = P}
              (C₁ ⊕ C₂)  (w₁ ⊕ w₂) (process P₁ ⊕ n₂) (sum-left  tr)       = context P , context-non-degenerate P , ext (context-[] P) , λ Qs →
                                                                              subst (_ [ _ ]⟶_) (ext $ context-[] P) $
                                                                              subst (λ P → P ⊕ _ [ _ ]⟶ _)
                                                                                (context P₁ [ Ps ]  ≡⟨ sym $ ext $ context-[] P₁ ⟩
                                                                                P₁                 ≡⟨ ext $ context-[] P₁ ⟩∎
                                                                                context P₁ [ Qs ]  ∎) $
                                                                              sum-left tr
6-2-15-nd ext (C₁ ⊕ C₂)  (w₁ ⊕ w₂) (n₁ ⊕ action n₂)  (sum-right tr)       = Σ-map id (Σ-map id (Σ-map id (sum-right ∘_)))
                                                                              (6-2-15-nd ext (_ · _) action (action n₂) tr)
6-2-15-nd ext {Ps = Ps} {P = P}
              (C₁ ⊕ C₂)  (w₁ ⊕ w₂) (n₁ ⊕ process P₂) (sum-right tr)       = context P , context-non-degenerate P , ext (context-[] P) , λ Qs →
                                                                              subst (_ [ _ ]⟶_) (ext $ context-[] P) $
                                                                              subst (λ P → _ ⊕ P [ _ ]⟶ _)
                                                                                (context P₂ [ Ps ]  ≡⟨ sym $ ext $ context-[] P₂ ⟩
                                                                                P₂                 ≡⟨ ext $ context-[] P₂ ⟩∎
                                                                                context P₂ [ Qs ]  ∎) $
                                                                              sum-right tr

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
True : Prop
True = {P : Prop} → P → P

ext: agda

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --keep-pattern-variables #-}

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

test₁ : (m : Nat) → m ≡ 0 → Set
test₁ m eq = {!eq!}

test₂ : (A B : Set) → A ≡ B → Set
test₂ A B eq = {!eq!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Logic where

data Bool : Set where
  true : Bool
  false : Bool

_∧_ : Bool → Bool → Bool
false ∧ _ = false
true ∧ b = b

_∨_ : Bool → Bool → Bool
true ∨ _ = true
false ∨ b = b

max_stars_repo_name: neosimsim/merkdas

max_issues_repo_name: neosimsim/merkdas

max_forks_repo_name: neosimsim/merkdas


text:
{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --rewriting #-}

module CBVNTranslations where

open import Library
open import Polarized

-- Intuitionistic propositional logic

data IPL : Set where
  Atom        : (P : Atoms) → IPL
  True False  : IPL
  _∨_ _∧_ _⇒_ : (A B : IPL) → IPL

module CallByName where

  _⁻ : IPL → Form -
  Atom P ⁻  = Atom- P
  True ⁻    = True
  False ⁻   = Comp False
  (A ∨ B) ⁻ = Comp (Thunk (A ⁻) ∨ Thunk (B ⁻))
  (A ∧ B) ⁻ = A ⁻ ∧ B ⁻
  (A ⇒ B) ⁻ = Thunk (A ⁻) ⇒ B ⁻

module CallByValue where

  _⁺ : IPL → Form +
  Atom P ⁺  = Atom P
  True ⁺    = True
  False ⁺   = False
  (A ∨ B) ⁺ = A ⁺ ∨ B ⁺
  (A ∧ B) ⁺ = A ⁺ ∧ B ⁺
  (A ⇒ B) ⁺ = Thunk (A ⁺ ⇒ Comp (B ⁺))

mutual

  _⁺ : IPL → Form +
  Atom P ⁺  = Atom P
  True ⁺    = True
  False ⁺   = False
  (A ∨ B) ⁺ = A ⁺ ∨ B ⁺
  (A ∧ B) ⁺ = A ⁺ ∧ B ⁺
  (A ⇒ B) ⁺ = Thunk (A ⁺ ⇒ B ⁻)

  _⁻ : IPL → Form -
  Atom P ⁻  = Atom- P
  True ⁻    = True
  False ⁻   = Comp False
  (A ∨ B) ⁻ = Comp (A ⁺ ∨ B ⁺)
  (A ∧ B) ⁻ = A ⁻ ∧ B ⁻
  (A ⇒ B) ⁻ = A ⁺ ⇒ B ⁻

-- Derivations

infix 2 _⊢_

data _⊢_ (Γ : Cxt' IPL) : (A : IPL) → Set where
  hyp    : ∀{A} (x : Hyp' IPL A Γ) → Γ ⊢ A
  impI   : ∀{A B} (t : Γ ∙ A ⊢ B) → Γ ⊢ A ⇒ B
  impE   : ∀{A B} (t : Γ ⊢ A ⇒ B) (u : Γ ⊢ A) → Γ ⊢ B
  andI   : ∀{A B} (t : Γ ⊢ A) (u : Γ ⊢ B) → Γ ⊢ A ∧ B
  andE₁  : ∀{A B} (t : Γ ⊢ A ∧ B) → Γ ⊢ A
  andE₂  : ∀{A B} (t : Γ ⊢ A ∧ B) → Γ ⊢ B
  orI₁   : ∀{A B} (t : Γ ⊢ A) → Γ ⊢ A ∨ B
  orI₂   : ∀{A B} (t : Γ ⊢ B) → Γ ⊢ A ∨ B
  orE    : ∀{A B C} (t : Γ ⊢ A ∨ B) (u : Γ ∙ A ⊢ C) (v : Γ ∙ B ⊢ C) → Γ ⊢ C
  falseE : ∀{C} (t : Γ ⊢ False) → Γ ⊢ C
  trueI  : Γ ⊢ True

Tm = λ A Γ → Γ ⊢ A

-- Call-by value evaluation

module CBV where

  V⟦_⟧ = λ A → ⟦ A ⁺ ⟧
  C⟦_⟧ = λ A → ⟦ A ⁻ ⟧

  return : ∀ A → V⟦ A ⟧ →̇ C⟦ A ⟧
  return (Atom P) v = returnC v
  return True v = v
  return False v = returnC v
  return (A ∨ B) v = returnC v
  return (A ∧ B) (a , b) = return A a , return B b
  return (A ⇒ B) v = v

  run : ∀ A → C⟦ A ⟧ →̇ Cover ∞ ∞ V⟦ A ⟧
  run (Atom P) c = c
  run True c = returnC c
  run False c = c
  run (A ∨ B) c = c
  run (A ∧ B) c = joinCover (mapCover' (λ τ a → mapCover' (λ τ' b → (mon⟦ A ⁺ ⟧ τ' a , b)) (run B (mon⟦ B ⁻ ⟧ τ (proj₂ c)))) (run A (proj₁ c)))
  run (A ⇒ B) c = returnC c

  -- Fundamental theorem
  -- Extension of ⟦_⟧ to contexts

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

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

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

  -- Variable case.

  lookup : ∀{Γ A} (x : Hyp' IPL A Γ) → G⟦ Γ ⟧ →̇ V⟦ A ⟧
  lookup top     = proj₂
  lookup (pop x) = lookup x ∘ proj₁

  impIntro : ∀ {A B Γ} (f : KFun (Cover ∞ ∞ ⟦ A ⟧) ⟦ B ⟧ Γ) → ⟦ A ⇒ B ⟧ Γ
  impIntro f τ a = f τ (returnC a)

  -- impElim : ∀ A B {Γ} → (f : C⟦ A ⇒ B ⟧ Γ) (a : C⟦ A ⟧ Γ) → C⟦ B ⟧ Γ
  -- impElim (Atom P) B f = paste (B ⁻) ∘ mapCover' f
  -- impElim False B f = paste (B ⁻) ∘ mapCover' f
  -- impElim True B f = f id≤
  -- impElim (A ∨ A₁) B f = paste (B ⁻) ∘ mapCover' f
  -- impElim (A ∧ A₁) B f = {!paste (B ⁻) ∘ mapCover' f!}
  -- impElim (A ⇒ A₁) B f = f id≤

  impElim : ∀ A B {Γ} → (f : C⟦ A ⇒ B ⟧ Γ) (a : C⟦ A ⟧ Γ) → C⟦ B ⟧ Γ
  impElim A B f a = paste (B ⁻) (mapCover' f (run A a))

  -- A lemma for the orE case.

  orElim : ∀ A B C {Γ} → C⟦ A ∨ B ⟧ Γ → C⟦ A ⇒ C ⟧ Γ → C⟦ B ⇒ C ⟧ Γ → C⟦ C ⟧ Γ
  orElim A B C c g h = paste (C ⁻) (mapCover' (λ τ → [ g τ , h τ ]) c)

  -- A lemma for the falseE case.

  -- Casts an empty cover into any semantic value (by contradiction).

  falseElim : ∀ C → C⟦ False ⟧ →̇ C⟦ C ⟧
  falseElim C = paste (C ⁻) ∘ mapCover ⊥-elim

  -- The fundamental theorem
  eval :  ∀{A Γ} (t : Γ ⊢ A) → G⟦ Γ ⟧ →̇ C⟦ A ⟧
  eval {A} (hyp x)           = return A ∘ lookup x
  eval (impI t)    γ τ a     = eval t (monG τ γ , a)
  eval (impE {A} {B} t u)  γ = impElim A B (eval t γ) (eval u γ)
  eval (andI t u)  γ         = eval t γ , eval u γ
  eval (andE₁ t)             = proj₁ ∘ eval t
  eval (andE₂ t)             = proj₂ ∘ eval t
  eval (orI₁ {A} {B} t) γ    = mapCover inj₁ (run A (eval t γ))
  eval (orI₂ {A} {B} t) γ    = mapCover inj₂ (run B (eval t γ))
  eval (orE {A} {B} {C} t u v) γ = orElim A B C (eval t γ)
    (λ τ a → eval u (monG τ γ , a))
    (λ τ b → eval v (monG τ γ , b))
  eval {C} (falseE t) γ      = falseElim C (eval t γ)
  eval trueI       γ         = _

  _⁺⁺ : (Γ : Cxt' IPL) → Cxt
  ε ⁺⁺ = ε
  (Γ ∙ A) ⁺⁺ = Γ ⁺⁺ ∙ A ⁻

  -- Identity environment

  ide : ∀ Γ → Cover ∞ ∞ G⟦ Γ ⟧ (Γ ⁺⁺)
  ide ε = returnC _
  ide (Γ ∙ A) = {!!}
    -- monG (weak id≤) (ide Γ) , {! reflectHyp (A ⁺) (λ τ a → a) !}
{-
  -- Normalization

  norm : ∀{A : IPL} {Γ : Cxt' IPL} → Tm A Γ → RInv (Γ ⁺⁺) (A ⁻)
  norm t = reify- _ (eval t (ide _))

-- -}
-- -}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
module UniDB.Morph.SubsPrime where

open import UniDB.Spec
open import Function
open import Data.Product

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

mutual
  data Subs* (T : STX) : MOR where
    refl : {γ : Dom} → Subs* T γ γ
    incl : {γ₁ γ₂ : Dom} (ξ : Subs+ T γ₁ γ₂) → Subs* T γ₁ γ₂

  data Subs+ (T : STX) : MOR where
    step : {γ₁ γ₂ : Dom} (ξ : Subs* T γ₁ γ₂) (t : T γ₂) → Subs+ T (suc γ₁) γ₂
    skip : {γ₁ γ₂ : Dom} (ξ : Subs+ T γ₁ γ₂) → Subs+ T (suc γ₁) (suc γ₂)

{-
data Subs (T : STX) : MOR where
  refl : {γ : Dom} → Subs T γ γ
  step : {γ₁ γ₂ : Dom} (ξ : Subs T γ₁ γ₂) (t : T γ₂) → Subs T (suc γ₁) γ₂
  skip : {γ₁ γ₂ : Dom} (ξ : Subs T γ₁ γ₂) → Subs T (suc γ₁) (suc γ₂)

instance
  iUpSubs : {T : STX} → Up (Subs T)
  _↑₁    {{iUpSubs}}            = skip
  _↑_    {{iUpSubs}} ξ 0        = ξ
  _↑_    {{iUpSubs}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
  ↑-zero {{iUpSubs}} ξ          = refl
  ↑-suc  {{iUpSubs}} ξ δ        = refl

module _ {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} where

  instance
    iLkSubs : Lk T (Subs T)
    lk {{iLkSubs}} refl       i       = vr {T} i
    lk {{iLkSubs}} (step ξ t) zero    = t
    lk {{iLkSubs}} (step ξ t) (suc i) = lk {T} {Subs T} ξ i
    lk {{iLkSubs}} (skip ξ)   zero    = vr {T} zero
    lk {{iLkSubs}} (skip ξ)   (suc i) = wk₁ (lk {T} {Subs T} ξ i)
-}

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
------------------------------------------------------------------------
-- Brzozowski-style derivatives of parsers
------------------------------------------------------------------------

module TotalParserCombinators.Derivative.Definition where

open import Category.Monad
open import Codata.Musical.Notation
open import Data.List using (List; map)
import Data.List.Categorical
import Data.Maybe; open Data.Maybe.Maybe
open import Level

open RawMonadPlus {f = zero} Data.List.Categorical.monadPlus
  using ()
  renaming ( return to return′
           ; ∅      to fail′
           ; _∣_    to _∣′_
           ; _⊛_    to _⊛′_
           ; _>>=_  to _>>=′_
           )

open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser

-- A function which calculates the index of the derivative.

D-bag : ∀ {Tok R xs} → Tok → Parser Tok R xs → List R
D-bag t (return x)   = fail′
D-bag t fail         = fail′
D-bag t token        = return′ t
D-bag t (p₁ ∣ p₂)    = D-bag t p₁ ∣′ D-bag t p₂
D-bag t (nonempty p) = D-bag t p
D-bag t (cast eq p)  = D-bag t p
D-bag t (f <$> p)    = map f (D-bag t p)
D-bag t (p₁ ⊛ p₂)    with forced? p₁ | forced? p₂
... | just xs | nothing = D-bag t p₁ ⊛′ xs
... | just xs | just fs = D-bag t p₁ ⊛′ xs ∣′ fs ⊛′ D-bag t p₂
... | nothing | nothing = fail′
... | nothing | just fs =                     fs ⊛′ D-bag t p₂
D-bag t (p₁ >>= p₂)  with forced? p₁ | forced?′ p₂
... | just f  | nothing =  D-bag t p₁ >>=′ f
... | just f  | just xs = (D-bag t p₁ >>=′ f) ∣′ (xs >>=′ λ x → D-bag t (p₂ x))
... | nothing | nothing = fail′
... | nothing | just xs =                         xs >>=′ λ x → D-bag t (p₂ x)

-- "Derivative": x ∈ D t p · s  iff  x ∈ p · t ∷ s.

D : ∀ {Tok R xs}
    (t : Tok) (p : Parser Tok R xs) → Parser Tok R (D-bag t p)
D t (return x)   = fail
D t fail         = fail
D t token        = return t
D t (p₁ ∣ p₂)    = D t p₁ ∣ D t p₂
D t (nonempty p) = D t p
D t (cast eq p)  = D t p
D t (f <$> p)    = f <$> D t p
D t (p₁ ⊛ p₂)    with forced? p₁ | forced? p₂
... | just xs | nothing =   D t    p₁  ⊛ ♭ p₂
... | just xs | just fs =   D t    p₁  ⊛   p₂ ∣ return⋆ fs ⊛ D t p₂
... | nothing | nothing = ♯ D t (♭ p₁) ⊛ ♭ p₂
... | nothing | just fs = ♯ D t (♭ p₁) ⊛   p₂ ∣ return⋆ fs ⊛ D t p₂
D t (p₁ >>= p₂)  with forced? p₁ | forced?′ p₂
... | just f  | nothing = D t p₁ >>= (λ x → ♭ (p₂ x))
... | just f  | just xs = D t p₁ >>= (λ x →    p₂ x)
                        ∣ return⋆ xs >>= λ x → D t (p₂ x)
... | nothing | nothing = ♯ D t (♭ p₁) >>= (λ x → ♭ (p₂ x))
... | nothing | just xs = ♯ D t (♭ p₁) >>= (λ x →    p₂ x)
                        ∣ return⋆ xs >>= λ x → D t (p₂ x)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Cone where

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

open import Categories.Support.PropositionalEquality

open import Categories.Category
open import Categories.Functor hiding (_≡_; _∘_)

module ConeOver {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) where
  module J = Category J
  open Category C
  open Functor F
  record Cone : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) where
    field
      N : Obj
      ψ : ∀ X → (N ⇒ F₀ X)
      .commute : ∀ {X Y} (f : J [ X , Y ]) → F₁ f ∘ ψ X ≡ ψ Y

  Cone′ = Cone

  record _≜_ (X Y : Cone) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) where
    module X = Cone X
    module Y = Cone Y
    field
      N-≣ : X.N ≣ Y.N
      ψ-≡ : ∀ j → C [ X.ψ j ∼ Y.ψ j ]

  ≜-is-equivalence : IsEquivalence _≜_
  ≜-is-equivalence = record
    { refl = record { N-≣ = ≣-refl; ψ-≡ = λ j → refl }
    ; sym = λ X≜Y → let module X≜Y = _≜_ X≜Y in record
      { N-≣ = ≣-sym X≜Y.N-≣
      ; ψ-≡ = λ j → sym (X≜Y.ψ-≡ j)
      }
    ; trans = λ X≜Y Y≜Z →
      let module X≜Y = _≜_ X≜Y in
      let module Y≜Z = _≜_ Y≜Z in
      record
        { N-≣ = ≣-trans X≜Y.N-≣ Y≜Z.N-≣
        ; ψ-≡ = λ j → trans (X≜Y.ψ-≡ j) (Y≜Z.ψ-≡ j)
        }
    }
    where open Heterogeneous C

  cone-setoid : Setoid _ _
  cone-setoid = record
    { Carrier = Cone
    ; _≈_ = _≜_
    ; isEquivalence = ≜-is-equivalence
    }

  record ConeUnder (N : Obj) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) where
    field
      ψ′ : ∀ X → (N ⇒ F₀ X)
      .commute : ∀ {X Y} (f : J [ X , Y ]) → F₁ f ∘ ψ′ X ≡ ψ′ Y

  ConeUnder′ = ConeUnder

  untether : ∀ {N} → ConeUnder N → Cone
  untether {N} K = record { N = N; ψ = ψ′; commute = commute }
    where open ConeUnder K

  -- this Henry Ford bit is a little weird but it turns out to be handy
  tether : ∀ {N} → (K : Cone) → (N ≣ Cone.N K) → ConeUnder N
  tether K ≣-refl = record { ψ′ = Cone.ψ K; commute = Cone.commute K }

  record _≜′_ {N} (X Y : ConeUnder N) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) where
    module X = ConeUnder X
    module Y = ConeUnder Y
    field
      .ψ′-≡ : ∀ j → C [ X.ψ′ j ≡ Y.ψ′ j ]

  ≜′-is-equivalence : (N : Obj) → IsEquivalence (_≜′_ {N})
  ≜′-is-equivalence N = record
    { refl = record { ψ′-≡ = λ j → Equiv.refl }
    ; sym = λ X≜′Y → let module X≜′Y = _≜′_ X≜′Y in record
      { ψ′-≡ = λ j → Equiv.sym (X≜′Y.ψ′-≡ j)
      }
    ; trans = λ X≜′Y Y≜′Z →
      let module X≜′Y = _≜′_ X≜′Y in
      let module Y≜′Z = _≜′_ Y≜′Z in
      record { ψ′-≡ = λ j → Equiv.trans (X≜′Y.ψ′-≡ j) (Y≜′Z.ψ′-≡ j) }
    }
    where open Heterogeneous C

  cone-under-setoid : (N : Obj) → Setoid _ _
  cone-under-setoid N = record
    { Carrier = ConeUnder N
    ; _≈_ = _≜′_
    ; isEquivalence = ≜′-is-equivalence N
    }

  private
    .lemma₁ : ∀ {N j} {f : N ⇒ F₀ j} K → C [ f ∼ Cone.ψ K j ] → (pf : N ≣ Cone.N K) → f ≡ ConeUnder.ψ′ (tether K pf) j
    lemma₁ K eq ≣-refl = ∼⇒≡ eq
      where open Heterogeneous C

  -- allow replacing the N-≣ because sometimes refl is available at the place
  --   of use.  in fact that's the main reason to even have ConeUnders.
  --   coincidentally, it makes this easier to write!
  homogenize : ∀ {K₁ K₂} → K₁ ≜ K₂ → (pf : Cone.N K₁ ≣ Cone.N K₂) → tether K₁ ≣-refl ≜′ tether K₂ pf
  homogenize {K₂ = K₂} K₁≜K₂ pf = record { ψ′-≡ = λ j → lemma₁ K₂ (ψ-≡ j) pf }
    where
    open _≜_ K₁≜K₂
    open Heterogeneous C

  heterogenize : ∀ {N} {K₁ K₂ : ConeUnder N} → K₁ ≜′ K₂ → untether K₁ ≜ untether K₂
  heterogenize {N} {K₁} {K₂} pf = record
    { N-≣ = ≣-refl
    ; ψ-≡ = λ j → Heterogeneous.≡⇒∼ (ψ′-≡ j)
    }
    where open _≜′_ pf

  open Setoid cone-setoid public renaming (refl to ≜-refl; sym to ≜-sym; trans to ≜-trans; reflexive to ≜-reflexive)
  module ≜′ {N : Obj} = Setoid (cone-under-setoid N)

open ConeOver public using (cone-setoid) renaming (_≜_ to _[_≜_]; Cone′ to Cone; _≜′_ to _[_≜′_]; ConeUnder′ to ConeUnder)

module Cone {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} {F : Functor J C} (K : ConeOver.Cone F) = ConeOver.Cone K

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import lib.Basics
open import lib.types.Empty
open import lib.types.Group
open import lib.types.Word
open import lib.groups.GeneratedGroup
open import lib.groups.Homomorphism

module lib.groups.FreeGroup where

module FreeGroup {i} (A : Type i) where

  private
    module Gen = GeneratedGroup A empty-rel
  open Gen hiding (GenGroup) public

  FreeGroup : Group i
  FreeGroup = Gen.GenGroup

  module Freeness {j} (G : Group j) where

    private
      module G = Group G
      module HE = HomomorphismEquiv G

    extend-equiv : (A → G.El) ≃ (FreeGroup →ᴳ G)
    extend-equiv =
      HE.extend-equiv ∘e every-function-respects-empty-rel-equiv A G

    extend : (A → G.El) → (FreeGroup →ᴳ G)
    extend = –> extend-equiv

    extend-is-equiv : is-equiv extend
    extend-is-equiv = snd extend-equiv

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

open import lib.Basics
open import lib.NConnected
open import lib.NType2
open import lib.types.Span
open import lib.types.Pointed
open import lib.types.Pushout
open import lib.types.PushoutFlip
open import lib.types.PushoutFmap
open import lib.types.PushoutFlattening
open import lib.types.Unit
open import lib.types.Paths
open import lib.types.Truncation
open import lib.types.Lift
open import lib.cubical.Square

-- Suspension is defined as a particular case of pushout

module lib.types.Suspension where

module _ {i} (A : Type i) where

  susp-span : Span
  susp-span = span Unit Unit A (λ _ → tt) (λ _ → tt)

  Susp : Type i
  Susp = Pushout susp-span

  -- [north'] and [south'] explictly ask for [A]

  north' : Susp
  north' = left tt

  south' : Susp
  south' = right tt

module _ {i} {A : Type i} where

  north : Susp A
  north = north' A

  south : Susp A
  south = south' A

  merid : A → north == south
  merid x = glue x

  module SuspElim {j} {P : Susp A → Type j} (n : P north)
    (s : P south) (p : (x : A) → n == s [ P ↓ merid x ]) where
    open module P = PushoutElim (λ _ → n) (λ _ → s) p
      public using (f) renaming (glue-β to merid-β)

  open SuspElim public using () renaming (f to Susp-elim)

  module SuspRec {j} {C : Type j} (n s : C) (p : A → n == s) where
    open module P = PushoutRec {d = susp-span A} (λ _ → n) (λ _ → s) p
      public using (f) renaming (glue-β to merid-β)

  open SuspRec public using () renaming (f to Susp-rec)

  module SuspRecType {j} (n s : Type j) (p : A → n ≃ s)
    = PushoutRecType {d = susp-span A} (λ _ → n) (λ _ → s) p

susp-⊙span : ∀ {i} → Ptd i → ⊙Span
susp-⊙span X =
  ⊙span ⊙Unit ⊙Unit X (⊙cst {X = X}) (⊙cst {X = X})

⊙Susp : ∀ {i} → Ptd i → Ptd i
⊙Susp ⊙[ A , _ ] = ⊙[ Susp A , north ]

σloop : ∀ {i} (X : Ptd i) → de⊙ X → north' (de⊙ X) == north' (de⊙ X)
σloop ⊙[ _ , x₀ ] x = merid x ∙ ! (merid x₀)

σloop-pt : ∀ {i} {X : Ptd i} → σloop X (pt X) == idp
σloop-pt {X = ⊙[ _ , x₀ ]} = !-inv-r (merid x₀)

⊙σloop : ∀ {i} (X : Ptd i) → X ⊙→ ⊙[ north' (de⊙ X) == north' (de⊙ X) , idp ]
⊙σloop X = σloop X , σloop-pt

module SuspFlip {i} {A : Type i} = SuspRec
  (south' A) north (! ∘ merid)

Susp-flip : ∀ {i} {A : Type i} → Susp A → Susp A
Susp-flip = SuspFlip.f

⊙Susp-flip : ∀ {i} (X : Ptd i) → ⊙Susp X ⊙→ ⊙Susp X
⊙Susp-flip X = (Susp-flip , ! (merid (pt X)))

Susp-flip-equiv : ∀ {i} {A : Type i} → Susp A ≃ Susp A
Susp-flip-equiv {A = A} = Pushout-flip-equiv (susp-span A)

module _ {i j} where

  module SuspFmap {A : Type i} {B : Type j} (f : A → B) =
    SuspRec north south (merid ∘ f)

  Susp-fmap : {A : Type i} {B : Type j} (f : A → B)
    → (Susp A → Susp B)
  Susp-fmap = SuspFmap.f

  ⊙Susp-fmap : {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
    → ⊙Susp X ⊙→ ⊙Susp Y
  ⊙Susp-fmap (f , fpt) = (Susp-fmap f , idp)

module _ {i} where

  Susp-fmap-idf : (A : Type i) → ∀ a → Susp-fmap (idf A) a == a
  Susp-fmap-idf A = Susp-elim idp idp $ λ a →
    ↓-='-in' (ap-idf (merid a) ∙ ! (SuspFmap.merid-β (idf A) a))

  ⊙Susp-fmap-idf : (X : Ptd i)
    → ⊙Susp-fmap (⊙idf X) == ⊙idf (⊙Susp X)
  ⊙Susp-fmap-idf X = ⊙λ=' (Susp-fmap-idf (de⊙ X)) idp

module _ {i j} where

  Susp-fmap-cst : {A : Type i} {B : Type j} (b : B)
    (a : Susp A) → Susp-fmap (cst b) a == north
  Susp-fmap-cst b = Susp-elim idp (! (merid b)) $ (λ a →
    ↓-app=cst-from-square $ SuspFmap.merid-β (cst b) a ∙v⊡ tr-square _)

  ⊙Susp-fmap-cst : {X : Ptd i} {Y : Ptd j}
    → ⊙Susp-fmap (⊙cst {X = X} {Y = Y}) == ⊙cst
  ⊙Susp-fmap-cst = ⊙λ=' (Susp-fmap-cst _) idp

  Susp-flip-fmap : {A : Type i} {B : Type j} (f : A → B)
    → ∀ σ → Susp-flip (Susp-fmap f σ) == Susp-fmap f (Susp-flip σ)
  Susp-flip-fmap f = Susp-elim idp idp $ λ y → ↓-='-in' $
    ap-∘ (Susp-fmap f) Susp-flip (merid y)
    ∙ ap (ap (Susp-fmap f)) (SuspFlip.merid-β y)
    ∙ ap-! (Susp-fmap f) (merid y)
    ∙ ap ! (SuspFmap.merid-β f y)
    ∙ ! (SuspFlip.merid-β (f y))
    ∙ ! (ap (ap Susp-flip) (SuspFmap.merid-β f y))
    ∙ ∘-ap Susp-flip (Susp-fmap f) (merid y)

module _ {i j k} where

  Susp-fmap-∘ : {A : Type i} {B : Type j} {C : Type k} (g : B → C) (f : A → B)
    (σ : Susp A) → Susp-fmap (g ∘ f) σ == Susp-fmap g (Susp-fmap f σ)
  Susp-fmap-∘ g f = Susp-elim
    idp
    idp
    (λ a → ↓-='-in' $
      ap-∘ (Susp-fmap g) (Susp-fmap f) (merid a)
      ∙ ap (ap (Susp-fmap g)) (SuspFmap.merid-β f a)
      ∙ SuspFmap.merid-β g (f a)
      ∙ ! (SuspFmap.merid-β (g ∘ f) a))

  ⊙Susp-fmap-∘ : {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
    (g : Y ⊙→ Z) (f : X ⊙→ Y)
    → ⊙Susp-fmap (g ⊙∘ f) == ⊙Susp-fmap g ⊙∘ ⊙Susp-fmap f
  ⊙Susp-fmap-∘ g f = ⊙λ=' (Susp-fmap-∘ (fst g) (fst f)) idp

{- Extract the 'glue component' of a pushout -}
module _ {i j k} {s : Span {i} {j} {k}} where

  module ExtractGlue = PushoutRec {d = s} {D = Susp (Span.C s)}
    (λ _ → north) (λ _ → south) merid

  extract-glue = ExtractGlue.f

  module _ {x₀ : Span.A s} where

    ⊙extract-glue : ⊙[ Pushout s , left x₀ ] ⊙→ ⊙[ Susp (Span.C s) , north ]
    ⊙extract-glue = extract-glue , idp

module _ {i j} {A : Type i} {B : Type j} (eq : A ≃ B) where

  susp-span-emap : SpanEquiv (susp-span A) (susp-span B)
  susp-span-emap = ( span-map (idf _) (idf _) (fst eq) (comm-sqr λ _ → idp) (comm-sqr λ _ → idp)
                  , idf-is-equiv _ , idf-is-equiv _ , snd eq)

  Susp-emap : Susp A ≃ Susp B
  Susp-emap = Pushout-emap susp-span-emap

  private
    -- This is to make sure that we did not screw up [Susp-emap].
    test₀ : fst Susp-emap == Susp-fmap (fst eq)
    test₀ = idp

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  ⊙Susp-emap : X ⊙≃ Y → ⊙Susp X ⊙≃ ⊙Susp Y
  ⊙Susp-emap ⊙eq = ≃-to-⊙≃ (Susp-emap (⊙≃-to-≃ ⊙eq)) idp

{- Interaction with [Lift] -}
module _ {i j} (X : Type i) where

  Susp-Lift-econv : Susp (Lift {j = j} X) ≃ Lift {j = j} (Susp X)
  Susp-Lift-econv = lift-equiv ∘e Susp-emap lower-equiv

  Susp-Lift-conv : Susp (Lift {j = j} X) == Lift {j = j} (Susp X)
  Susp-Lift-conv = ua Susp-Lift-econv

module _ {i j} (X : Ptd i) where

  ⊙Susp-Lift-econv : ⊙Susp (⊙Lift {j = j} X) ⊙≃ ⊙Lift {j = j} (⊙Susp X)
  ⊙Susp-Lift-econv = ⊙lift-equiv {j = j} ⊙∘e ⊙Susp-emap {X = ⊙Lift {j = j} X} {Y = X} ⊙lower-equiv

  ⊙Susp-Lift-conv : ⊙Susp (⊙Lift {j = j} X) == ⊙Lift {j = j} (⊙Susp X)
  ⊙Susp-Lift-conv = ⊙ua ⊙Susp-Lift-econv

{- Suspension of an n-connected space is n+1-connected -}
abstract
  Susp-conn : ∀ {i} {A : Type i} {n : ℕ₋₂}
    → is-connected n A → is-connected (S n) (Susp A)
  Susp-conn {A = A} {n = n} cA = has-level-in
    ([ north ] ,
     Trunc-elim
       (Susp-elim
         idp
         (Trunc-rec (λ a → ap [_] (merid a))
                    (contr-center cA))
         (λ x → Trunc-elim
            {P = λ y → idp ==
              Trunc-rec (λ a → ap [_] (merid a)) y
              [ (λ z → [ north ] == [ z ]) ↓ (merid x) ]}
            {{λ _ → ↓-preserves-level ⟨⟩}}
            (λ x' → ↓-cst=app-in (∙'-unit-l _ ∙ mers-eq n x x'))
            (contr-center cA))))
    where
    instance _ = cA

    mers-eq : ∀ {i} {A : Type i} (n : ℕ₋₂)
      {{_ : is-connected n A}} → (x x' : A)
      → ap ([_] {n = S n}) (merid x)
        == Trunc-rec {{has-level-apply (Trunc-level {n = S n}) _ _}} (λ a → ap [_] (merid a)) [ x' ]
    mers-eq ⟨-2⟩ x x' = contr-has-all-paths _ _
    mers-eq {A = A} (S n) x x' =
      conn-extend (pointed-conn-out A x)
        (λ y → ((ap [_] (merid x) == ap [_] (merid y)) ,
                has-level-apply (has-level-apply (Trunc-level {n = S (S n)}) _ _) _ _))
        (λ _ → idp) x'

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- {-# OPTIONS -v tc.meta:25 #-}
module Issue418 where

data _≡_ (A : Set₁) : Set₁ → Set₂ where
  refl : A ≡ A

abstract

  A : Set₁
  A = Set

  unfold-A : A ≡ _
  unfold-A = refl

-- I don't think we should solve the meta-variable corresponding to
-- the underscore above. We have two obvious choices, A and Set, and
-- these choices are not equivalent.

-- Andreas, 2011-05-30
-- Meta-Variable should remain unsolved


text:
module _ where

id : (A B : Set₁) → (A → B) → A → B
id _ _ f = f

postulate
  P    : (A : Set₁) → A → Set₁
  cong : (A B : Set₁) (f : A → B) (x : A) → P A x → P B (f x)
  A    : Set

record R₀ (B : Set) : Set₁ where
  constructor mkR₀
  no-eta-equality
  field
    proj₁ : Set
    proj₂ : B

record R₁ (_ : Set) : Set₁ where
  constructor mkR₁
  eta-equality
  field
    p : R₀ A

  X : Set
  X = R₀.proj₁ p

record R₂ (r : R₁ A) : Set₁ where
  constructor mkR₂
  eta-equality
  field
    g : R₀ (R₁.X r)

should-succeed :
  (r₁ : R₁ A) (r₂ : R₂ r₁) →
  P (R₂ r₁) r₂ → P (R₀ (R₁.X r₁)) (R₂.g r₂)
should-succeed r₁ r₂ =
  id (P _ _)
     (P (R₀ (R₁.X r₁)) (R₂.g r₂))
     (cong _ _ R₂.g _)

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Jesper, 2018-12-04, Issue #3431 reported by François Thiré on the
-- Agda mailing list
-- (https://lists.chalmers.se/pipermail/agda/2018/010686.html)

-- The instance of the Reduce typeclass for pairs did not have an
-- implementation for reduceB' (only reduce'), which made it default
-- to the standard implementation and forget the blocking tags.

{-# OPTIONS --rewriting #-}

open import Agda.Primitive
open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

0ℓ : Level
0ℓ = lzero

1ℓ : Level
1ℓ = lsuc lzero

record Lift {a} ℓ (A : Set a) : Set (a ⊔ ℓ) where
  constructor lift
  field lower : A

postulate
  prod  : {ℓ ℓ′ : Level} → (A : Set ℓ) → (B : Set ℓ′) → Set (ℓ ⊔ ℓ′)

  p : Set 1ℓ → Set 1ℓ
  q : Set 1ℓ → Set 1ℓ
  f : ∀ (c : Set 0ℓ) → p (Lift 1ℓ c) → q (Lift 1ℓ c)
  g : ∀ (a : Set 1ℓ) → ∀ (b : Set 1ℓ) → p (prod a b)
  a : Set 0ℓ
  b : Set 0ℓ

  canL : {ℓ ℓ′ ℓ″ : Level} → (A : Set ℓ) → (B : Set ℓ′)  → (prod (Lift ℓ″ A) B) ≡ Lift (ℓ″ ⊔ ℓ′) (prod A B)
  canR : {ℓ ℓ′ ℓ″ : Level} → (A : Set ℓ) → (B : Set ℓ′)  → (prod A (Lift ℓ″ B)) ≡ Lift (ℓ ⊔ ℓ″) (prod A B)
  canT : {ℓ ℓ′ ℓ″ : Level} → (A : Set ℓ) → Lift ℓ″ (Lift ℓ′ A) ≡ Lift (ℓ″ ⊔ ℓ′) A

{-# REWRITE canL #-}
{-# REWRITE canR #-}
{-# REWRITE canT #-}

ali : q (Lift 1ℓ (prod a b))
ali = f (prod a b) (g (Lift 1ℓ {!!}) (Lift 1ℓ b))

-- WAS: Set₁ != Set
-- SHOULD: succeed (with unsolved metas and constraints)

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Unit

macro
  pickWhatever : Term → TC ⊤
  pickWhatever hole@(meta m _) = do
    (cand ∷ _) ← getInstances m
      where [] -> typeError (strErr "No candidates!" ∷ [])
    unify hole cand
  pickWhatever _ = typeError (strErr "Already solved!" ∷ [])

-- Testing basic functionality
data YesNo : Set where instance yes no : YesNo

test₁ : YesNo
test₁ = pickWhatever

test₁-ok : test₁ ≡ yes
test₁-ok = refl

-- Testing if candidates are correctly filtered
data IsYesNo : YesNo → Set where instance
  isYes : IsYesNo yes
  isNo : IsYesNo no

test₂ : IsYesNo no
test₂ = pickWhatever

-- Testing local candidates
test₃ : {{YesNo}} → YesNo
test₃ = pickWhatever

test₃-ok : ∀ {x} → test₃ {{x}} ≡ x
test₃-ok = refl

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Definitions where

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

data _≡_ (x : ℕ) : ℕ → Set where
  refl : x ≡ x

data _≢_ : ℕ → ℕ → Set where
  z≢s : ∀ {n} → zero ≢ suc n
  s≢z : ∀ {n} → suc n ≢ zero
  s≢s : ∀ {m n} → m ≢ n → suc m ≢ suc n

data Equal? (m n : ℕ) : Set where
  yes : m ≡ n → Equal? m n
  no  : m ≢ n → Equal? m n

data ⊥ : Set where

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


text:
module STLC where

open import Data.Nat
open import Data.Empty
open import Relation.Binary.PropositionalEquality

-- infix  4 _⊢_
-- infix  4 _∋_∶_
-- infixl 5 _,_

infixr 7 _⟶_

infix  5 ƛ_
infixl 7 _∙_
-- infix  9 `_
infixl 10 _∶_

-- infix  5 μ_
-- infix  8 `suc_
-- infix  9 S_
-- infix  9 #_

data Type : Set where
  _⟶_ : Type → Type → Type
  ⊤    : Type

data Context : Set
data Term : Set

infix 4 _∋_∶_
data _∋_∶_ : Context → Term → Type → Set

infixl 10 _,_∶_
data Context where
  ∅   : Context
  _,_∶_ : Context → Term → Type → Context

data Term where
  ‵_ : ∀ {Γ x A} → Γ ∋ x ∶ A → Term

  ƛ_ : Term → Term

  _∙_ : Term → Term → Term

  _∶_ : Term → Type → Term

  tt : Term

data _∋_∶_ where
  Z : ∀ {Γ x A}
      ---------
    → Γ , x ∶ A ∋ x ∶ A

  S_ : ∀ {Γ x A y B}
    → Γ ∋ x ∶ A
      ---------
    → Γ , y ∶ B ∋ x ∶ A

-- lookup : Context → ℕ → Type
-- lookup (Γ , A) zero     =  A
-- lookup (Γ , _) (suc n)  =  lookup Γ n
-- lookup ∅       _        =  ⊥-elim impossible
--   where postulate impossible : ⊥

-- count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
-- count {Γ , _} zero     =  Z
-- count {Γ , _} (suc n)  =  S (count n)
-- count {∅}     _        =  ⊥-elim impossible
--   where postulate impossible : ⊥

-- -- #_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
-- -- # n  =  ` count n

-- a = {!   !}

infix 4 _⊢_⇐_
infix 4 _⊢_⇒_

data _⊢_⇐_ : Context → Term → Type → Set
data _⊢_⇒_ : Context → Term → Type → Set

variable
  Γ : Context
  x e f : Term
  A B : Type

data _⊢_⇒_ where

  Var :
      Γ ∋ x ∶ A
    ----------------------------
    → Γ ⊢ x ⇒ A

  Anno :
      Γ ⊢ e ⇐ A
    ----------------------------
    → Γ ⊢ (e ∶ A) ⇒ A

  ⟶E :
      Γ ⊢ f ⇒ (A ⟶ B)
    → Γ ⊢ e ⇐ A
    ----------------------------
    → Γ ⊢ f ∙ e ⇒ B

data _⊢_⇐_ where

  Sub :
      Γ ∋ e ∶ A
    → A ≡ B
    ----------------------------
    → Γ ⊢ e ⇐ B

  ⊤I : ∀ {Γ}
    ----------------------------
    → Γ ⊢ tt ⇐ ⊤

  ⟶I :
      (Γ , x ∶ A) ⊢ e ⇐ B
    ----------------------------
    → Γ ⊢ ƛ e ⇐ A ⟶ B

4-4-Synth : ∅ , x ∶ A ⊢ x ⇒ A
4-4-Synth = Var Z

4-4-Check : ∅ , x ∶ A ⊢ x ⇐ A
4-4-Check = Sub Z refl

4-4-Sym→Elim : ∅ , f ∶ (A ⟶ B) , x ∶ A ⊢ (f ∙ x) ⇒ B
4-4-Sym→Elim = ⟶E (Var (S Z)) (Sub Z refl)

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Categories.Instances.CommAlgebras where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.HLevels

open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Algebra
open import Cubical.Algebra.CommAlgebra
open import Cubical.Algebra.CommAlgebra.Instances.Unit

open import Cubical.Categories.Category
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.Limits.Terminal
open import Cubical.Categories.Limits.Pullback
open import Cubical.Categories.Instances.CommRings

open import Cubical.HITs.PropositionalTruncation

open Category hiding (_∘_) renaming (_⋆_ to _⋆c_)
open CommAlgebraHoms
open Cospan
open Pullback

private
 variable
  ℓ ℓ' ℓ'' : Level

module _ (R : CommRing ℓ) where
  CommAlgebrasCategory : Category (ℓ-suc (ℓ-max ℓ ℓ')) (ℓ-max ℓ ℓ')
  ob CommAlgebrasCategory       = CommAlgebra R _
  Hom[_,_] CommAlgebrasCategory = CommAlgebraHom
  id CommAlgebrasCategory {A}   = idCommAlgebraHom A
  _⋆c_ CommAlgebrasCategory {A} {B} {C}     = compCommAlgebraHom A B C
  ⋆IdL CommAlgebrasCategory {A} {B}           = compIdCommAlgebraHom {A = A} {B}
  ⋆IdR CommAlgebrasCategory {A} {B}           = idCompCommAlgebraHom {A = A} {B}
  ⋆Assoc CommAlgebrasCategory {A} {B} {C} {D} = compAssocCommAlgebraHom {A = A} {B} {C} {D}
  isSetHom CommAlgebrasCategory               = isSetAlgebraHom _ _

  TerminalCommAlgebra : Terminal (CommAlgebrasCategory {ℓ' = ℓ'})
  fst TerminalCommAlgebra = UnitCommAlgebra R
  fst (fst (snd TerminalCommAlgebra A)) = λ _ → tt*
  snd (fst (snd TerminalCommAlgebra A)) = makeIsAlgebraHom
                                            refl (λ _ _ → refl) (λ _ _ → refl) (λ _ _ → refl)
  snd (snd TerminalCommAlgebra A) f = AlgebraHom≡ (funExt (λ _ → refl))

module PullbackFromCommRing (R : CommRing ℓ)
                            (commRingCospan : Cospan (CommRingsCategory {ℓ = ℓ}))
                            (commRingPB : Pullback _ commRingCospan)
                            (f₁ : CommRingHom R (commRingPB .pbOb))
                            (f₂ : CommRingHom R (commRingCospan .r))
                            (f₃ : CommRingHom R (commRingCospan .l))
                            (f₄ : CommRingHom R (commRingCospan .m))
                            where

 open AlgebraHoms
 open CommAlgChar R
 open CommAlgebraStr ⦃...⦄

 private
  CommAlgCat = CommAlgebrasCategory {ℓ = ℓ} R {ℓ' = ℓ}

  A = commRingPB .pbOb
  B = commRingCospan .r
  C = commRingCospan .l
  D = commRingCospan .m

  g₁ = commRingPB .pbPr₂
  g₂ = commRingPB .pbPr₁
  g₃ = commRingCospan .s₂
  g₄ = commRingCospan .s₁

  {-
              g₁
           A  →  B
             ⌟
        g₂ ↓     ↓ g₃

           C  →  D
              g₄
  -}

 open RingHoms
 univPropCommRingWithHomHom : (isRHom₁ : isCommRingWithHomHom (A , f₁) (B , f₂) g₁)
                              (isRHom₂ : isCommRingWithHomHom (A , f₁) (C , f₃) g₂)
                              (isRHom₃ : isCommRingWithHomHom (B , f₂) (D , f₄) g₃)
                              (isRHom₄ : isCommRingWithHomHom (C , f₃) (D , f₄) g₄)
                              (E,f₅ : CommRingWithHom)
                              (h₂ : CommRingWithHomHom E,f₅ (C , f₃))
                              (h₁ : CommRingWithHomHom E,f₅ (B , f₂))
                            → g₄ ∘r fst h₂ ≡ g₃ ∘r fst h₁
                            → ∃![ h₃ ∈ CommRingWithHomHom E,f₅ (A , f₁) ]
                                 (fst h₂ ≡ g₂ ∘r fst h₃) × (fst h₁ ≡ g₁ ∘r fst h₃)
 univPropCommRingWithHomHom isRHom₁ isRHom₂ isRHom₃ isRHom₄
                             (E , f₅) (h₂ , comm₂) (h₁ , comm₁) squareComm =
    ((h₃ , h₃∘f₅≡f₁) , h₂≡g₂∘h₃ , h₁≡g₁∘h₃)
  , λ h₃' → Σ≡Prop (λ _ → isProp× (isSetRingHom _ _ _ _) (isSetRingHom _ _ _ _))
                     (Σ≡Prop (λ _ → isSetRingHom _ _ _ _)
                       (cong fst (commRingPB .univProp h₂ h₁ squareComm .snd
                         (h₃' .fst .fst , h₃' .snd .fst , h₃' .snd .snd))))
  where
  h₃ : CommRingHom E A
  h₃ = commRingPB .univProp h₂ h₁ squareComm .fst .fst
  h₂≡g₂∘h₃ : h₂ ≡ g₂ ∘r h₃
  h₂≡g₂∘h₃ = commRingPB .univProp h₂ h₁ squareComm .fst .snd .fst
  h₁≡g₁∘h₃ : h₁ ≡ g₁ ∘r h₃
  h₁≡g₁∘h₃ = commRingPB .univProp h₂ h₁ squareComm .fst .snd .snd

  -- the crucial obervation:
  -- we can apply the universal property to maps R → A
  fgSquare : g₄ ∘r f₃ ≡ g₃ ∘r f₂
  fgSquare = isRHom₄ ∙ sym isRHom₃

  h₃∘f₅≡f₁ : h₃ ∘r f₅ ≡ f₁
  h₃∘f₅≡f₁ = cong fst (isContr→isProp (commRingPB .univProp f₃ f₂ fgSquare)
                        (h₃ ∘r f₅ , triangle1 , triangle2) (f₁ , (sym isRHom₂) , sym isRHom₁))
    where
    triangle1 : f₃ ≡ g₂ ∘r (h₃ ∘r f₅)
    triangle1 = sym comm₂ ∙∙ cong (compRingHom f₅) h₂≡g₂∘h₃ ∙∙ sym (compAssocRingHom f₅ h₃ g₂)

    triangle2 : f₂ ≡ g₁ ∘r (h₃ ∘r f₅)
    triangle2 = sym comm₁ ∙∙ cong (compRingHom f₅) h₁≡g₁∘h₃ ∙∙ sym (compAssocRingHom f₅ h₃ g₁)

 algCospan : (isRHom₁ : isCommRingWithHomHom (A , f₁) (B , f₂) g₁)
             (isRHom₂ : isCommRingWithHomHom (A , f₁) (C , f₃) g₂)
             (isRHom₃ : isCommRingWithHomHom (B , f₂) (D , f₄) g₃)
             (isRHom₄ : isCommRingWithHomHom (C , f₃) (D , f₄) g₄)
           → Cospan CommAlgCat
 l (algCospan isRHom₁ isRHom₂ isRHom₃ isRHom₄) = toCommAlg (C , f₃)
 m (algCospan isRHom₁ isRHom₂ isRHom₃ isRHom₄) = toCommAlg (D , f₄)
 r (algCospan isRHom₁ isRHom₂ isRHom₃ isRHom₄) = toCommAlg (B , f₂)
 s₁ (algCospan isRHom₁ isRHom₂ isRHom₃ isRHom₄) = toCommAlgebraHom _ _ g₄ isRHom₄
 s₂ (algCospan isRHom₁ isRHom₂ isRHom₃ isRHom₄) = toCommAlgebraHom _ _ g₃ isRHom₃

 algPullback : (isRHom₁ : isCommRingWithHomHom (A , f₁) (B , f₂) g₁)
               (isRHom₂ : isCommRingWithHomHom (A , f₁) (C , f₃) g₂)
               (isRHom₃ : isCommRingWithHomHom (B , f₂) (D , f₄) g₃)
               (isRHom₄ : isCommRingWithHomHom (C , f₃) (D , f₄) g₄)
             → Pullback CommAlgCat (algCospan isRHom₁ isRHom₂ isRHom₃ isRHom₄)
 pbOb (algPullback isRHom₁ isRHom₂ isRHom₃ isRHom₄) = toCommAlg (A , f₁)
 pbPr₁ (algPullback isRHom₁ isRHom₂ isRHom₃ isRHom₄) = toCommAlgebraHom _ _ g₂ isRHom₂
 pbPr₂ (algPullback isRHom₁ isRHom₂ isRHom₃ isRHom₄) = toCommAlgebraHom _ _ g₁ isRHom₁
 pbCommutes (algPullback isRHom₁ isRHom₂ isRHom₃ isRHom₄) =
               AlgebraHom≡ (cong fst (pbCommutes commRingPB))
 univProp (algPullback isRHom₁ isRHom₂ isRHom₃ isRHom₄) {d = F} h₂' h₁' g₄∘h₂'≡g₃∘h₁' =
  (k , kComm₂ , kComm₁) , uniqueness
  where
  E = fromCommAlg F .fst
  f₅ = fromCommAlg F .snd

  h₁ : CommRingHom E B
  fst h₁ = fst h₁'
  IsRingHom.pres0 (snd h₁) = IsAlgebraHom.pres0 (snd h₁')
  IsRingHom.pres1 (snd h₁) = IsAlgebraHom.pres1 (snd h₁')
  IsRingHom.pres+ (snd h₁) = IsAlgebraHom.pres+ (snd h₁')
  IsRingHom.pres· (snd h₁) = IsAlgebraHom.pres· (snd h₁')
  IsRingHom.pres- (snd h₁) = IsAlgebraHom.pres- (snd h₁')

  h₁comm : h₁ ∘r f₅ ≡ f₂
  h₁comm = RingHom≡ (funExt (λ x → IsAlgebraHom.pres⋆ (snd h₁') x 1a
                                      ∙∙ cong (fst f₂ x ·_) (IsAlgebraHom.pres1 (snd h₁'))
                                      ∙∙ ·Rid _))
   where
   instance
    _ = snd F
    _ = snd (toCommAlg (B , f₂))

  h₂ : CommRingHom E C
  fst h₂ = fst h₂'
  IsRingHom.pres0 (snd h₂) = IsAlgebraHom.pres0 (snd h₂')
  IsRingHom.pres1 (snd h₂) = IsAlgebraHom.pres1 (snd h₂')
  IsRingHom.pres+ (snd h₂) = IsAlgebraHom.pres+ (snd h₂')
  IsRingHom.pres· (snd h₂) = IsAlgebraHom.pres· (snd h₂')
  IsRingHom.pres- (snd h₂) = IsAlgebraHom.pres- (snd h₂')

  h₂comm : h₂ ∘r f₅ ≡ f₃
  h₂comm = RingHom≡ (funExt (λ x → IsAlgebraHom.pres⋆ (snd h₂') x 1a
                                      ∙∙ cong (fst f₃ x ·_) (IsAlgebraHom.pres1 (snd h₂'))
                                      ∙∙ ·Rid _))
   where
   instance
    _ = snd F
    _ = snd (toCommAlg (C , f₃))

  commRingSquare : g₄ ∘r h₂ ≡ g₃ ∘r h₁
  commRingSquare = RingHom≡ (funExt (λ x → funExt⁻ (cong fst g₄∘h₂'≡g₃∘h₁') x))

  uniqueH₃ : ∃![ h₃ ∈ CommRingWithHomHom (E , f₅) (A , f₁) ] (h₂ ≡ g₂ ∘r fst h₃) × (h₁ ≡ g₁ ∘r fst h₃)
  uniqueH₃ = univPropCommRingWithHomHom isRHom₁ isRHom₂ isRHom₃ isRHom₄
                                          (E , f₅) (h₂ , h₂comm) (h₁ , h₁comm) commRingSquare

  h₃ : CommRingHom E A
  h₃ = uniqueH₃ .fst .fst .fst

  h₃comm = uniqueH₃ .fst .fst .snd

  k : CommAlgebraHom F (toCommAlg (A , f₁))
  fst k = fst h₃
  IsAlgebraHom.pres0 (snd k) = IsRingHom.pres0 (snd h₃)
  IsAlgebraHom.pres1 (snd k) = IsRingHom.pres1 (snd h₃)
  IsAlgebraHom.pres+ (snd k) = IsRingHom.pres+ (snd h₃)
  IsAlgebraHom.pres· (snd k) = IsRingHom.pres· (snd h₃)
  IsAlgebraHom.pres- (snd k) = IsRingHom.pres- (snd h₃)
  IsAlgebraHom.pres⋆ (snd k) =
    λ r y → sym (fst f₁ r · fst h₃ y ≡⟨ cong (_· fst h₃ y) (sym (funExt⁻ (cong fst h₃comm) r)) ⟩
                 fst h₃ (fst f₅ r) · fst h₃ y ≡⟨ sym (IsRingHom.pres· (snd h₃) _ _) ⟩
                 fst h₃ (fst f₅ r · y) ≡⟨ refl ⟩
                 fst h₃ ((r ⋆ 1a) · y) ≡⟨ cong (fst h₃) (⋆-lassoc _ _ _) ⟩
                 fst h₃ (r ⋆ (1a · y)) ≡⟨ cong (λ x → fst h₃ (r ⋆ x)) (·Lid y) ⟩
                 fst h₃ (r ⋆ y) ∎)
   where
   instance
    _ = snd F
    _ = (toCommAlg (A , f₁) .snd)

  kComm₂ : h₂' ≡ toCommAlgebraHom _ _ g₂ isRHom₂ ∘a k
  kComm₂ = AlgebraHom≡ (cong fst (uniqueH₃ .fst .snd .fst))

  kComm₁ : h₁' ≡ toCommAlgebraHom _ _ g₁ isRHom₁ ∘a k
  kComm₁ = AlgebraHom≡ (cong fst (uniqueH₃ .fst .snd .snd))

  uniqueness : (y : Σ[ k' ∈ CommAlgebraHom F (toCommAlg (A , f₁)) ]
                       (h₂' ≡ toCommAlgebraHom _ _ g₂ isRHom₂ ∘a k')
                     × (h₁' ≡ toCommAlgebraHom _ _ g₁ isRHom₁ ∘a k'))
             → (k , kComm₂ , kComm₁) ≡ y
  uniqueness (k' , k'Comm₂ , k'Comm₁) = Σ≡Prop (λ _ → isProp× (isSetAlgebraHom _ _ _ _)
                                                              (isSetAlgebraHom _ _ _ _))
                                               (AlgebraHom≡ (cong (fst ∘ fst ∘ fst) uniqHelper))
   where
   h₃' : CommRingHom E A
   fst h₃' = fst k'
   IsRingHom.pres0 (snd h₃') = IsAlgebraHom.pres0 (snd k')
   IsRingHom.pres1 (snd h₃') = IsAlgebraHom.pres1 (snd k')
   IsRingHom.pres+ (snd h₃') = IsAlgebraHom.pres+ (snd k')
   IsRingHom.pres· (snd h₃') = IsAlgebraHom.pres· (snd k')
   IsRingHom.pres- (snd h₃') = IsAlgebraHom.pres- (snd k')

   h₃'IsRHom : h₃' ∘r f₅ ≡ f₁
   h₃'IsRHom = RingHom≡ (funExt (λ x → IsAlgebraHom.pres⋆ (snd k') x 1a
                                     ∙ cong (fst f₁ x ·_) (IsAlgebraHom.pres1 (snd k'))
                                     ∙ ·Rid (fst f₁ x)))
    where
    instance
     _ = snd F
     _ = (toCommAlg (A , f₁) .snd)

   h₃'Comm₂ : h₂ ≡ g₂ ∘r h₃'
   h₃'Comm₂ = RingHom≡ (cong fst k'Comm₂)

   h₃'Comm₁ : h₁ ≡ g₁ ∘r h₃'
   h₃'Comm₁ = RingHom≡ (cong fst k'Comm₁)

   -- basically saying that h₃≡h₃' but we have to give all the commuting triangles
   uniqHelper : uniqueH₃ .fst ≡ ((h₃' , h₃'IsRHom) , h₃'Comm₂ , h₃'Comm₁)
   uniqHelper = uniqueH₃ .snd ((h₃' , h₃'IsRHom) , h₃'Comm₂ , h₃'Comm₁)

module PreSheafFromUniversalProp (C : Category ℓ ℓ') (P : ob C → Type ℓ)
         {R : CommRing ℓ''} (𝓕 : Σ (ob C) P → CommAlgebra R ℓ'')
         (uniqueHom : ∀ x y → C [ fst x , fst y ] → isContr (CommAlgebraHom (𝓕 y) (𝓕 x)))
         where

 private
  ∥P∥ : ℙ (ob C)
  ∥P∥ x  = ∥ P x ∥ , isPropPropTrunc
  ΣC∥P∥Cat = ΣPropCat C ∥P∥
  CommAlgCat = CommAlgebrasCategory {ℓ = ℓ''} R {ℓ' = ℓ''}

 𝓕UniqueEquiv : (x : ob C) (p q : P x) → isContr (CommAlgebraEquiv (𝓕 (x , p)) (𝓕 (x , q)))
 𝓕UniqueEquiv x = contrCommAlgebraHom→contrCommAlgebraEquiv (curry 𝓕 x) λ p q → uniqueHom _ _ (id C)

 theMap : (x : ob C) → ∥ P x ∥ → CommAlgebra R ℓ''
 theMap x = recPT→CommAlgebra (curry 𝓕 x) (λ p q → 𝓕UniqueEquiv x p q .fst)
                                         λ p q r → 𝓕UniqueEquiv x p r .snd _

 theAction : (x y : ob C) → C [ x , y ]
           → (p : ∥ P x ∥) (q : ∥ P y ∥) → isContr (CommAlgebraHom (theMap y q) (theMap x p))
 theAction _ _ f = elim2 (λ _ _ → isPropIsContr) λ _ _ → uniqueHom _ _ f

 open Functor
 universalPShf : Functor (ΣC∥P∥Cat ^op) CommAlgCat
 F-ob universalPShf = uncurry theMap
 F-hom universalPShf {x = x} {y = y} f = theAction _ _ f (y .snd) (x. snd) .fst
 F-id universalPShf {x = x} = theAction (x .fst) (x .fst) (id C) (x .snd) (x .snd) .snd _
 F-seq universalPShf {x = x} {z = z} f g = theAction _ _ (g ⋆⟨ C ⟩ f) (z .snd) (x .snd) .snd _

 -- a big transport to help verifying the sheaf property
 module toSheaf (x y u v : ob ΣC∥P∥Cat)
                {f : C [ v .fst , y . fst ]} {g : C [ v .fst , u .fst ]}
                {h : C [ u .fst , x . fst ]} {k : C [ y .fst , x .fst ]}
                (Csquare : g ⋆⟨ C ⟩ h ≡ f ⋆⟨ C ⟩ k)
                {-
                    v → y
                    ↓   ↓
                    u → x
                -}
                (AlgCospan : Cospan CommAlgCat)
                (AlgPB : Pullback _ AlgCospan)
                (p₁ : AlgPB .pbOb ≡ F-ob universalPShf x) (p₂ : AlgCospan .l ≡ F-ob universalPShf u)
                (p₃ : AlgCospan .r ≡ F-ob universalPShf y) (p₄ : AlgCospan .m ≡ F-ob universalPShf v)
                where

  private
   -- just: 𝓕 k ⋆ 𝓕 f ≡ 𝓕 h ⋆ 𝓕 g
   inducedSquare : seq' CommAlgCat {x = F-ob universalPShf x}
                                   {y = F-ob universalPShf u}
                                   {z = F-ob universalPShf v}
                                   (F-hom universalPShf h) (F-hom universalPShf g)
                 ≡ seq' CommAlgCat {x = F-ob universalPShf x}
                                   {y = F-ob universalPShf y}
                                   {z = F-ob universalPShf v}
                                   (F-hom universalPShf k) (F-hom universalPShf f)
   inducedSquare = F-square universalPShf Csquare

   f' = F-hom universalPShf {x = y} {y = v} f
   g' = F-hom universalPShf {x = u} {y = v} g
   h' = F-hom universalPShf {x = x} {y = u} h
   k' = F-hom universalPShf {x = x} {y = y} k

   gPathP : PathP (λ i → CommAlgCat [ p₂ i , p₄ i ]) (AlgCospan .s₁) g'
   gPathP = toPathP (sym (theAction _ _ g (v .snd) (u .snd) .snd _))

   fPathP : PathP (λ i → CommAlgCat [ p₃ i , p₄ i ]) (AlgCospan .s₂) f'
   fPathP = toPathP (sym (theAction _ _ f (v .snd) (y .snd) .snd _))

   kPathP : PathP (λ i → CommAlgCat [ p₁ i , p₃ i ]) (AlgPB .pbPr₂) k'
   kPathP = toPathP (sym (theAction _ _ k (y .snd) (x .snd) .snd _))

   hPathP : PathP (λ i → CommAlgCat [ p₁ i , p₂ i ]) (AlgPB .pbPr₁) h'
   hPathP = toPathP (sym (theAction _ _ h (u .snd) (x .snd) .snd _))

   fgCospan : Cospan CommAlgCat
   l fgCospan = F-ob universalPShf u
   m fgCospan = F-ob universalPShf v
   r fgCospan = F-ob universalPShf y
   s₁ fgCospan = g'
   s₂ fgCospan = f'

   cospanPath : AlgCospan ≡ fgCospan
   l (cospanPath i) = p₂ i
   m (cospanPath i) = p₄ i
   r (cospanPath i) = p₃ i
   s₁ (cospanPath i) = gPathP i
   s₂ (cospanPath i) = fPathP i

   squarePathP : PathP (λ i → hPathP i ⋆⟨ CommAlgCat ⟩ gPathP i ≡ kPathP i ⋆⟨ CommAlgCat ⟩ fPathP i)
                      (AlgPB .pbCommutes) inducedSquare
   squarePathP = toPathP (CommAlgCat .isSetHom _ _ _ _)

  abstract
   lemma : isPullback CommAlgCat fgCospan {c = F-ob universalPShf x} h' k' inducedSquare
   lemma = transport (λ i → isPullback CommAlgCat (cospanPath i) {c = p₁ i}
                                                  (hPathP i) (kPathP i) (squarePathP i))
                     (AlgPB .univProp)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module HT where

open import Prelude
open import T
open import SubstTheory
open import DynTheory

module HT where

  ---- Halting and Hereditary Termination
  -- An old comment about lhs-halt

  -- Mostly for fun, I didn't want to include "and it halts" as part
  -- of the definition of HT for arrows, and I didn't want to define
  -- it in terms of evaluating to a lambda and then substituting.
  -- This seems to require being able to generate an inhabitant of an
  -- arbitrary type as well as a proof that it is HT. The former is
  -- easy in T and we accomplish the latter by appealing to all-HT,
  -- although we could have also generated the proof along with the
  -- inhabitant.  This all seems to be handwaved away when doing it on
  -- paper. Things get more unclear when in a system where not all
  -- types are inhabited; if we know that either a type is inhabited or
  -- it is not, then we are fine. But since we are constructive, we would
  -- get tripped up by a language like System F in which type inhabitability
  -- is undecidable. (Of course, the proof is easy to repair in a number of
  -- ways by modifying the definition of HT.)
  --
  -- When I went to make the system deterministic, I found that I now depended
  -- on HT-halts in all-HT, which broke the previous proof technique.
  -- I decided that proving the inhabitant we construct is HT would be
  -- annoying, so I decided to not bother and went back to hanging onto the
  -- proof that arrows halt.

  -- Extract that the lhs must halt if its application to something halts.
  -- I think this isn't actually useful, though, since to use it we would
  -- need to be able to produce an argument to the function.
  {-
  lhs-halt : {A B : TTp} {e : TCExp (A ⇒ B)} {e' : TCExp A} →
              THalts (e $ e') → THalts e
  lhs-halt (halts eval-refl ())
  lhs-halt (halts (eval-cons (step-app-l S1) E) val) with lhs-halt (halts E val)
  ... | halts E' val' = halts (eval-cons S1 E') val'
  lhs-halt (halts (eval-cons step-beta E) val) = halts eval-refl val-lam
  -}

  -- I think the induction principle for this datatype is the definition of
  -- HTω from http://www.cs.cmu.edu/~rwh/courses/typesys/hw3/hw3-handout.pdf
  data HTω : TNat → Set where
    HT-z : {e : TNat} → (E : e ~>* zero) → HTω e
    HT-s : {e e' : TNat} → (E : e ~>* suc e') → (HT : HTω e') → HTω e

  -- definition of hereditary termination
  HT : (A : TTp) → TCExp A → Set
  HT nat e = THalts e
  -- It is kind of ugly to have to hang on to the halting proof.
  HT (A ⇒ B) e = THalts e × ((e' : TCExp A) → HT A e' → HT B (e $ e'))

  -- proof that hereditary termination implies termination
  HT-halts : ∀{A} → (e : TCExp A) → HT A e → THalts e
  HT-halts {nat} e h = h
  HT-halts {A ⇒ B} _ (h , _) = h

  -- extend HT to substitutions
  HTΓ : (Γ : Ctx) → TSubst Γ [] → Set
  HTΓ Γ γ = ∀{A} (x : A ∈ Γ) -> HT A (γ x)

  emptyHTΓ : ∀{γ : TSubst [] []} -> HTΓ [] γ
  emptyHTΓ ()

  extendHTΓ : ∀{Γ A} {e : TCExp A} {γ : TSubst Γ []} ->
              HTΓ Γ γ -> HT A e -> HTΓ (A :: Γ) (extendγ γ e)
  extendHTΓ η ht Z = ht
  extendHTΓ {_} {_} {e} {γ} η ht {B} (S n) =
             ID.coe1 (HT B) (extend-nofail-s γ e n) (η n)

  -- head expansion lemma
  head-expansion : ∀{A} {e e' : TCExp A} → (e ~>* e') → HT A e' → HT A e
  head-expansion {nat} eval (halts eval₁ val) = halts (eval-trans eval eval₁) val
  head-expansion {A ⇒ B} eval (halts eval' val , ht-logic) =
     halts (eval-trans eval eval') val ,
     (λ e' ht → head-expansion (eval-compat step-app-l eval) (ht-logic e' ht))

  -- the main theorem
  all-HT : ∀{Γ A} {γ : TSubst Γ []} → (e : TExp Γ A) → HTΓ Γ γ
            → HT A (ssubst γ e)
  all-HT (var x) η = η x
  all-HT (e₁ $ e₂) η with all-HT e₁ η
  ... | _ , HT₁ = HT₁ (ssubst _ e₂) (all-HT e₂ η)
  all-HT zero η = halts eval-refl val-zero
  all-HT (suc e) η with all-HT e η
  ... | halts eval val = halts (eval-compat step-suc eval) (val-suc val)

  all-HT {Γ} {A ⇒ B} {γ} (Λ e) η =
    (halts eval-refl val-lam) ,
     lam-case
    where lam-case : (e' : TCExp A) → HT A e' → HT B (Λ (ssubst (liftγ γ) e) $ e')
          lam-case e' ht' with all-HT {γ = extendγ γ e'} e (extendHTΓ η ht')
          ... | ht with eval-step (step-beta {e = (ssubst (liftγ γ) e)})
          ... | steps-full with combine-subst-noob γ e e'
          ... | eq = head-expansion steps-full (ID.coe1 (HT B) eq ht)

  all-HT {Γ} {A} {γ} (rec e e₀ es) η with all-HT e η
  ... | halts E val = head-expansion (eval-compat step-rec E) (inner val)
    where inner : {n : TNat} → TVal n → HT A (rec n (ssubst γ e₀) (ssubst (liftγ γ) es))
          inner val-zero = head-expansion (eval-step step-rec-z) (all-HT e₀ η)
          inner (val-suc v) with all-HT es (extendHTΓ η (inner v))
          ... | ht with eval-step (step-rec-s v)
          ... | steps with combine-subst-noob γ es _
          ... | eq = head-expansion steps (ID.coe1 (HT A) eq ht)

  -- Prove that all programs in Gödel's System T halt.
  all-halt : ∀{A} → (e : TCExp A) → THalts e
  all-halt {A} e = HT-halts e (ID.coe1 (HT A) (subid e) (all-HT e (emptyHTΓ {emptyγ})))

open HT public

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
{-# OPTIONS --copatterns --sized-types #-}

module Copatterns where

open import Size

record Stream {i : Size} (A : Set) : Set where
  coinductive
  constructor _::_
  field
    head : A
    tail : {j : Size< i} ->  Stream {j} A
open Stream

map : ∀ {i A B} (f : A -> B) -> (s : Stream {i} A) -> Stream {i} B
head (map {i} f s)  = f (head s)
tail (map {i} f s) {j} = map {j} f (tail s {j})

iter : {A : Set} -> (A -> A) -> A -> Stream A
head (iter f a) = a
tail (iter f a) = iter f (f a)

repeat : {A : Set} -> A -> Stream A
head (repeat a) = a
tail (repeat a) = repeat a

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

zipWith : ∀ {i : Size} {A B C : Set} -> (A -> B -> C) -> Stream {i} A -> Stream {i} B -> Stream {i} C
head (zipWith {i} f as bs) = f (head as) (head bs)
tail (zipWith {i} f as bs) {j} = zipWith {j} f (tail as {j}) (tail bs {j})

_+_ : Nat -> Nat -> Nat
_+_ Z     m = m
_+_ (S n) m = S (n + m)

_*_ : Nat -> Nat -> Nat
_*_ Z m = Z
_*_ (S n) m = m + (n * m)

nats : Stream Nat
nats = iter S Z

nats' : ∀ {i : Size} -> Stream {i} Nat
head (nats' {i})     = Z
tail (nats' {i}) {j} = map {j} S (nats' {j})

fib : ∀ {i : Size} -> Stream {i} Nat
head (fib {i})                = Z
head (tail (fib {i}) {j})     = S Z
tail (tail (fib {i}) {j}) {k} = zipWith {k} _+_ (fib {k}) (tail (fib {j}) {k})

{-
pow2 : ∀ {i : Size} ->  Stream {i} Nat
head pow2 = S Z
head (tail pow2) = S (S Z)
tail (tail pow2) = zipWith _+_ (tail pow2) (tail pow2)

-}

max_stars_repo_name: tdidriksen/copatterns

max_issues_repo_name: tdidriksen/copatterns

max_forks_repo_name: tdidriksen/copatterns


text:
-- Kit instances and generic term traversals
module Syntax.Substitution.Instances where

open import Syntax.Types
open import Syntax.Context
open import Syntax.Terms
open import Syntax.Substitution.Kits

open import Data.Sum
open import Relation.Binary.PropositionalEquality as ≡
    using (_≡_ ; refl ; sym ; cong ; subst)
open import Function using (id ; flip ; _∘_)
open ≡.≡-Reasoning

-- | Variable and term schemas
Var : Schema
Var = flip _∈_

Term : Schema
Term = _⊢_

-- | Variable kit

-- Variable kit
𝒱ar : Kit Var
𝒱ar = record
    { 𝓋 = id
    ; 𝓉 = var
    ; 𝓌 = pop
    ; 𝒶 = 𝒶-var
    }
    where
    𝒶-var : ∀{A Γ} → Var Γ (A always) → Var (Γ ˢ) (A always)
    𝒶-var top = top
    𝒶-var (pop {B = B now} v) = 𝒶-var v
    𝒶-var (pop {B = B always} v) = pop (𝒶-var v)

-- Generic substitution in a variable to any schema
subst-var : ∀ {𝒮 Γ Δ A} -> Subst 𝒮 Γ Δ → Var Γ A → 𝒮 Δ A
subst-var ● ()
subst-var (σ ▸ T) top = T
subst-var (σ ▸ T) (pop v) = subst-var σ v

-- Substitutable variable kit
𝒱arₛ : SubstKit Var
𝒱arₛ = record { 𝓀 = 𝒱ar ; 𝓈 = subst-var }

-- | Term traversal

module K {𝒮 : Schema} (k : Kit 𝒮) where
    open Kit k

    -- | Type-preserving term traversal
    -- | Traverses the syntax tree of the term, applying
    -- | the given substitution to the variables.
    mutual
        traverse : ∀{Γ Δ A} -> Subst 𝒮 Γ Δ -> Γ ⊢ A -> Δ ⊢ A
        traverse σ (var x)     = 𝓉 (subst-var σ x)
        traverse σ (lam M)     = lam (traverse (σ ↑ k) M)
        traverse σ (M $ N)     = traverse σ M $ traverse σ N
        traverse σ unit        = unit
        traverse σ [ M ,, N ]  = [ traverse σ M ,, traverse σ N ]
        traverse σ (fst M)     = fst (traverse σ M)
        traverse σ (snd M)     = snd (traverse σ M)
        traverse σ (inl M)     = inl (traverse σ M)
        traverse σ (inr M)     = inr (traverse σ M)
        traverse σ (case M inl↦ N₁ ||inr↦ N₂)
                               = case traverse σ M
                                   inl↦ traverse (σ ↑ k) N₁
                                 ||inr↦ traverse (σ ↑ k) N₂
        traverse σ (sample M) = sample (traverse σ M)
        traverse σ (stable M)  = stable (traverse (σ ↓ˢ k) M)
        traverse σ (sig M)     = sig (traverse σ M)
        traverse σ (letSig S In M) = letSig traverse σ S
                                         In traverse (σ ↑ k) M
        traverse σ (event E)   = event (traverse′ σ E)

        traverse′ : ∀{Γ Δ A} -> Subst 𝒮 Γ Δ -> Γ ⊨ A -> Δ ⊨ A
        traverse′ σ (pure M) = pure (traverse σ M)
        traverse′ σ (letSig S InC C) = letSig traverse σ S
                                         InC traverse′ (σ ↑ k) C
        traverse′ σ (letEvt E In C)  = letEvt traverse σ E
                                         In traverse′ (σ ↓ˢ k ↑ k) C
        traverse′ σ (select E₁ ↦ C₁ || E₂ ↦ C₂ ||both↦ C₃) =
            select traverse σ E₁ ↦ traverse′ (σ ↓ˢ k ↑ k ↑ k) C₁
                || traverse σ E₂ ↦ traverse′ (σ ↓ˢ k ↑ k ↑ k) C₂
                ||both↦            traverse′ (σ ↓ˢ k ↑ k ↑ k) C₃
open K

-- Renaming is a term traversal with variable substitutions
rename : ∀{A Γ Δ} -> Subst Var Γ Δ -> Γ ⊢ A -> Δ ⊢ A
rename = traverse 𝒱ar

-- Weakening is a renaming with a weakening substitution
weaken-top : ∀{B Γ A} -> Γ ⊢ A → Γ , B ⊢ A
weaken-top = rename (weak-topₛ 𝒱arₛ)

-- Weakening is a renaming with a weakening substitution
weaken′-top : ∀{B Γ A} -> Γ ⊨ A → Γ , B ⊨ A
weaken′-top = traverse′ 𝒱ar (weak-topₛ 𝒱arₛ)

-- | Term kit

-- Term kit
𝒯erm : Kit Term
𝒯erm = record
    { 𝓋 = var
    ; 𝓉 = id
    ; 𝓌 = weaken-top
    ; 𝒶 = 𝒶-term
    }
    where
    𝒶-term : {Γ : Context} {A : Type} → Γ ⊢ A always → Γ ˢ ⊢ A always
    𝒶-term {∙} M = M
    𝒶-term {Γ , B now} (var (pop x)) = 𝒶-term (var x)
    𝒶-term {Γ , B always} (var top) = var top
    𝒶-term {Γ , B always} (var {A = A} (pop x)) = weaken-top (𝒶-term (var x))
    𝒶-term {Γ , B now} (stable M) = 𝒶-term {Γ} (stable M)
    𝒶-term {Γ , B always} (stable {A = A} M) =
        stable (subst (λ x → x , B always ⊢ A now) (sym (ˢ-idemp Γ)) M)

-- Substitution is a traversal with term substitutions
substitute : ∀{Γ Δ A} -> Subst Term Γ Δ -> Γ ⊢ A -> Δ ⊢ A
substitute = traverse 𝒯erm

-- Computational substitution is a traversal with term substitutions
substitute′ : ∀{Γ Δ A} -> Subst Term Γ Δ -> Γ ⊨ A -> Δ ⊨ A
substitute′ = traverse′ 𝒯erm

-- Substitutable term kit
𝒯ermₛ : SubstKit Term
𝒯ermₛ = record { 𝓀 = 𝒯erm ; 𝓈 = substitute }

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
module Terminal where

open import Base
open import Category
open import Unique
open import Dual
import Iso

module Term (ℂ : Cat) where

  private ℂ' = η-Cat ℂ
  private open module C	= Cat ℂ'
  private open module U = Uniq ℂ'
  private open module I = Iso ℂ'

  Terminal : (A : Obj) -> Set1
  Terminal A = (B : Obj) -> ∃! \(f : B ─→ A) -> True

  toTerminal : {A B : Obj} -> Terminal A -> B ─→ A
  toTerminal term = getWitness (term _)

  terminalIso : {A B : Obj} -> Terminal A -> Terminal B -> A ≅ B
  terminalIso tA tB = iso (toTerminal tB)
			   (toTerminal tA)
			   p q
    where
      p : toTerminal tB ∘ toTerminal tA == id
      p = witnessEqual (tB _) tt tt

      q : toTerminal tA ∘ toTerminal tB == id
      q = witnessEqual (tA _) tt tt

module Init (ℂ : Cat) = Term (η-Cat ℂ op)
    renaming
      ( Terminal    to Initial
      ; toTerminal  to fromInitial
      ; terminalIso to initialIso
      )

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Ual.Eq where

open import Agda.Primitive
open import Ual.Void

record Eq {a} (A : Set a) : Set (lsuc a) where
  infix 30 _==_
  infix 30 _≠_
  field
    _==_  : A → A → Set
    self  : {x : A} → x == x
    sym   : {x y : A} → x == y → y == x
    trans : {x y z : A} → x == y → y == z → x == z
  _≠_  : A → A → Set
  x ≠ y = ¬ (x == y)

open Eq ⦃ ... ⦄ public

data Equality {a} {A : Set a} ⦃ eqA : Eq A ⦄ : A → A → Set where
  equal    : {x y : A} → x == y → Equality x y
  notEqual : {x y : A} → x ≠ y → Equality x y

record Test {a} (A : Set a) : Set (lsuc a) where
  field
    ⦃ eqA ⦄ : Eq A
    test  : (x : A) → (y : A) → Equality x y

max_stars_repo_name: brunoczim/ual

max_issues_repo_name: brunoczim/ual

max_forks_repo_name: brunoczim/ual


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

open import LogicalFormulae
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Definition
open import Numbers.Integers.Integers
open import Numbers.Integers.Addition
open import Sets.FinSet.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Groups
open import Groups.Subgroups.Definition
open import Groups.Lemmas
open import Groups.Subgroups.Definition
open import Groups.Abelian.Definition
open import Groups.Definition
open import Groups.Cyclic.Definition
open import Groups.Cyclic.DefinitionLemmas
open import Semirings.Definition
open import Rings.Definition

module Groups.Cyclic.Lemmas {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) where

elementPowerHom : (x : A) → GroupHom ℤGroup G (λ i → elementPower G x i)
GroupHom.groupHom (elementPowerHom x) {a} {b} = symmetric (elementPowerCollapse G x a b)
  where
    open Equivalence (Setoid.eq S)
GroupHom.wellDefined (elementPowerHom x) {.y} {y} refl = reflexive
  where
    open Equivalence (Setoid.eq S)

subgroupOfCyclicIsCyclic : {c : _} {pred : A → Set c} → (sub : Subgroup G pred) → CyclicGroup G → CyclicGroup (subgroupIsGroup G sub)
CyclicGroup.generator (subgroupOfCyclicIsCyclic {pred = pred} sub record { generator = g ; cyclic = cyclic }) = {!!}
  where
    leastPowerInGroup : (bound : ℕ) → ℕ
    leastPowerInGroup bound = {!!}
CyclicGroup.cyclic (subgroupOfCyclicIsCyclic sub cyc) = {!!}

-- Prefer to prove that subgroup of cyclic is cyclic, then deduce this like with abelian groups
{-
cyclicIsGroupProperty : {m n o p : _} {A : Set m} {B : Set o} {S : Setoid {m} {n} A} {T : Setoid {o} {p} B} {_+_ : A → A → A} {_*_ : B → B → B} {G : Group S _+_} {H : Group T _*_} → GroupsIsomorphic G H → CyclicGroup G → CyclicGroup H
CyclicGroup.generator (cyclicIsGroupProperty {H = H} iso G) = GroupsIsomorphic.isomorphism iso (CyclicGroup.generator G)
CyclicGroup.cyclic (cyclicIsGroupProperty {H = H} iso G) {a} with GroupIso.surj (GroupsIsomorphic.proof iso) {a}
CyclicGroup.cyclic (cyclicIsGroupProperty {H = H} iso G) {a} | a' , b with CyclicGroup.cyclic G {a'}
... | pow , prPow = pow , {!!}
-}

cyclicGroupIsAbelian : (cyclic : CyclicGroup G) → AbelianGroup G
AbelianGroup.commutative (cyclicGroupIsAbelian record { generator = generator ; cyclic = cyclic }) {a} {b} with cyclic {a}
... | bl with cyclic {b}
AbelianGroup.commutative (cyclicGroupIsAbelian record { generator = generator ; cyclic = cyclic }) {a} {b} | nA , prA | nB , prB = transitive (+WellDefined (symmetric prA) (symmetric prB)) (transitive (symmetric (GroupHom.groupHom (elementPowerHom generator) {nA} {nB})) (transitive (transitive (elementPowerWellDefinedZ' G (nA +Z nB) (nB +Z nA) (Ring.groupIsAbelian ℤRing {nA} {nB}) {generator}) (GroupHom.groupHom (elementPowerHom generator) {nB} {nA})) (+WellDefined prB prA)))
  where
    open Setoid S
    open Equivalence eq
    open Group G


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

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

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Macro
open import Cubical.Structures.Semigroup hiding (⟨_⟩)
open import Cubical.Structures.Monoid    hiding (⟨_⟩)
open import Cubical.Structures.AbGroup   hiding (⟨_⟩)

open Iso

private
  variable
    ℓ : Level

record IsRing {R : Type ℓ}
              (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R) : Type ℓ where

  constructor isring

  field
    +-isAbGroup : IsAbGroup 0r _+_ -_
    ·-isMonoid  : IsMonoid 1r _·_
    dist        : (x y z : R) → (x · (y + z) ≡ (x · y) + (x · z))
                              × ((x + y) · z ≡ (x · z) + (y · z))
    -- This is in the Agda stdlib, but it's redundant
    -- zero             : (x : R) → (x · 0r ≡ 0r) × (0r · x ≡ 0r)

  open IsAbGroup +-isAbGroup public
    renaming
    ( assoc       to +-assoc
    ; identity    to +-identity
    ; lid         to +-lid
    ; rid         to +-rid
    ; inverse     to +-inv
    ; invl        to +-linv
    ; invr        to +-rinv
    ; comm        to +-comm
    ; isSemigroup to +-isSemigroup
    ; isMonoid    to +-isMonoid
    ; isGroup     to +-isGroup
    )

  open IsMonoid ·-isMonoid public
    renaming
    ( assoc       to ·-assoc
    ; identity    to ·-identity
    ; lid         to ·-lid
    ; rid         to ·-rid
    ; isSemigroup to ·-isSemigroup
    )

  ·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
  ·-rdist-+ x y z = dist x y z .fst

  ·-ldist-+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z)
  ·-ldist-+ x y z = dist x y z .snd

  -- TODO: prove these somewhere

  -- zero-lid : (x : R) → 0r · x ≡ 0r
  -- zero-lid x = zero x .snd

  -- zero-rid : (x : R) → x · 0r ≡ 0r
  -- zero-rid x = zero x .fst

record Ring : Type (ℓ-suc ℓ) where

  constructor ring

  field
    Carrier : Type ℓ
    0r      : Carrier
    1r      : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    isRing  : IsRing 0r 1r _+_ _·_ -_

  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_

  open IsRing isRing public

-- Extractor for the carrier type
⟨_⟩ : Ring → Type ℓ
⟨_⟩ = Ring.Carrier

isSetRing : (R : Ring {ℓ}) → isSet ⟨ R ⟩
isSetRing R = R .Ring.isRing .IsRing.·-isMonoid .IsMonoid.isSemigroup .IsSemigroup.is-set

makeIsRing : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R} { -_ : R → R}
             (is-setR : isSet R)
             (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
             (+-rid : (x : R) → x + 0r ≡ x)
             (+-rinv : (x : R) → x + (- x) ≡ 0r)
             (+-comm : (x y : R) → x + y ≡ y + x)
             (+-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
             (·-rid : (x : R) → x · 1r ≡ x)
             (·-lid : (x : R) → 1r · x ≡ x)
             (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
             (·-ldist-+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z))
           → IsRing 0r 1r _+_ _·_ -_
makeIsRing is-setR assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+ =
  isring (makeIsAbGroup is-setR assoc +-rid +-rinv +-comm)
         (makeIsMonoid is-setR ·-assoc ·-rid ·-lid)
         λ x y z → ·-rdist-+ x y z , ·-ldist-+ x y z

makeRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
           (is-setR : isSet R)
           (+-assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
           (+-rid : (x : R) → x + 0r ≡ x)
           (+-rinv : (x : R) → x + (- x) ≡ 0r)
           (+-comm : (x y : R) → x + y ≡ y + x)
           (+-assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
           (·-rid : (x : R) → x · 1r ≡ x)
           (·-lid : (x : R) → 1r · x ≡ x)
           (·-rdist-+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
           (·-ldist-+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z))
         → Ring
makeRing 0r 1r _+_ _·_ -_ is-setR assoc +-rid +-rinv +-comm ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+ =
  ring _ 0r 1r _+_ _·_ -_
       (makeIsRing is-setR assoc +-rid +-rinv +-comm
                   ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+ )

record RingEquiv (R S : Ring {ℓ}) : Type ℓ where

  constructor ringequiv

  private
    module R = Ring R
    module S = Ring S

  field
    e : ⟨ R ⟩ ≃ ⟨ S ⟩
    pres1 : equivFun e R.1r ≡ S.1r
    isHom+ : (x y : ⟨ R ⟩) → equivFun e (x R.+ y) ≡ equivFun e x S.+ equivFun e y
    isHom· : (x y : ⟨ R ⟩) → equivFun e (x R.· y) ≡ equivFun e x S.· equivFun e y

module RingΣTheory {ℓ} where

  open Macro ℓ (recvar (recvar var) , var , recvar (recvar var)) public renaming
    ( structure to RawRingStructure
    ; equiv     to RawRingEquivStr
    ; univalent to rawRingUnivalentStr )

  RingAxioms : (R : Type ℓ) (s : RawRingStructure R) → Type ℓ
  RingAxioms R (_+_ , 1r , _·_) =
    AbGroupΣTheory.AbGroupAxioms R _+_
    × IsMonoid 1r _·_
    × ((x y z : R) → (x · (y + z) ≡ (x · y) + (x · z)) × ((x + y) · z ≡ (x · z) + (y · z)))

  RingStructure : Type ℓ → Type ℓ
  RingStructure = AxiomsStructure RawRingStructure RingAxioms

  RingΣ : Type (ℓ-suc ℓ)
  RingΣ = TypeWithStr ℓ RingStructure

  RingEquivStr : StrEquiv RingStructure ℓ
  RingEquivStr = AxiomsEquivStr RawRingEquivStr RingAxioms

  isPropRingAxioms : (R : Type ℓ) (s : RawRingStructure R) → isProp (RingAxioms R s)
  isPropRingAxioms R (_+_ , 1r , _·_) =
    isProp× (AbGroupΣTheory.isPropAbGroupAxioms R _+_)
            (isPropΣ (isPropIsMonoid 1r _·_)
                     λ R → isPropΠ3 λ _ _ _ →
                           isProp× (IsSemigroup.is-set (R .IsMonoid.isSemigroup) _ _)
                                   (IsSemigroup.is-set (R .IsMonoid.isSemigroup) _ _))

  Ring→RingΣ : Ring → RingΣ
  Ring→RingΣ (ring R 0r 1r _+_ _·_ -_ (isring +-isAbelianGroup ·-isMonoid dist)) =
    ( R
    , (_+_ , 1r , _·_)
    , AbGroupΣTheory.AbGroup→AbGroupΣ (abgroup _ _ _ _ +-isAbelianGroup) .snd .snd
    , ·-isMonoid , dist
    )

  RingΣ→Ring : RingΣ → Ring
  RingΣ→Ring (_ , (y1 , y2 , y3) , z , w1 , w2) =
    ring _ _ y2 y1 y3 _
      (isring (AbGroupΣTheory.AbGroupΣ→AbGroup (_ , _ , z ) .AbGroup.isAbGroup)
              w1 w2)

  RingIsoRingΣ : Iso Ring RingΣ
  RingIsoRingΣ = iso Ring→RingΣ RingΣ→Ring (λ _ → refl) (λ _ → refl)

  ringUnivalentStr : UnivalentStr RingStructure RingEquivStr
  ringUnivalentStr = axiomsUnivalentStr _ isPropRingAxioms rawRingUnivalentStr

  RingΣPath : (R S : RingΣ) → (R ≃[ RingEquivStr ] S) ≃ (R ≡ S)
  RingΣPath = SIP ringUnivalentStr

  RingEquivΣ : (R S : Ring) → Type ℓ
  RingEquivΣ R S = Ring→RingΣ R ≃[ RingEquivStr ] Ring→RingΣ S

  RingIsoΣPath : {R S : Ring} → Iso (RingEquiv R S) (RingEquivΣ R S)
  fun RingIsoΣPath (ringequiv e h1 h2 h3) = e , h2 , h1 , h3
  inv RingIsoΣPath (e , h1 , h2 , h3)    = ringequiv e h2 h1 h3
  rightInv RingIsoΣPath _                = refl
  leftInv RingIsoΣPath _                 = refl

  RingPath : (R S : Ring) → (RingEquiv R S) ≃ (R ≡ S)
  RingPath R S =
    RingEquiv R S               ≃⟨ isoToEquiv RingIsoΣPath ⟩
    RingEquivΣ R S              ≃⟨ RingΣPath _ _ ⟩
    Ring→RingΣ R ≡ Ring→RingΣ S ≃⟨ isoToEquiv (invIso (congIso RingIsoRingΣ)) ⟩
    R ≡ S ■

RingPath : (R S : Ring {ℓ}) → (RingEquiv R S) ≃ (R ≡ S)
RingPath = RingΣTheory.RingPath

isPropIsRing : {R : Type ℓ} (0r 1r : R) (_+_ _·_ : R → R → R) (-_ : R → R)
             → isProp (IsRing 0r 1r _+_ _·_ -_)
isPropIsRing 0r 1r _+_ _·_ -_ (isring RG RM RD) (isring SG SM SD) =
  λ i → isring (isPropIsAbGroup _ _ _ RG SG i)
               (isPropIsMonoid _ _ RM SM i)
               (isPropDistr RD SD i)
  where
  isSetR : isSet _
  isSetR = RM .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropDistr : isProp ((x y z : _) → ((x · (y + z)) ≡ ((x · y) + (x · z)))
                                    × (((x + y) · z) ≡ ((x · z) + (y · z))))
  isPropDistr = isPropΠ3 λ _ _ _ → isProp× (isSetR _ _) (isSetR _ _)

-- Rings have an abelian group and a monoid

Ring→AbGroup : Ring {ℓ} → AbGroup {ℓ}
Ring→AbGroup (ring _ _ _ _ _ _ R) = abgroup _ _ _ _ (IsRing.+-isAbGroup R)

Ring→Monoid : Ring {ℓ} → Monoid {ℓ}
Ring→Monoid (ring _ _ _ _ _ _ R) = monoid _ _ _ (IsRing.·-isMonoid R)

{-
  some basic calculations (used for example in QuotientRing.agda),
  that might should become obsolete or subject to change once we
  have a ring solver (see https://github.com/agda/cubical/issues/297)
-}
module Theory (R : Ring {ℓ}) where

  open Ring R

  implicitInverse : (x y : ⟨ R ⟩)
                 → x + y ≡ 0r
                 → y ≡ - x
  implicitInverse x y p =
    y               ≡⟨ sym (+-lid y) ⟩
    0r + y          ≡⟨ cong (λ u → u + y) (sym (+-linv x)) ⟩
    (- x + x) + y   ≡⟨ sym (+-assoc _ _ _) ⟩
    (- x) + (x + y) ≡⟨ cong (λ u → (- x) + u) p ⟩
    (- x) + 0r      ≡⟨ +-rid _ ⟩
    - x             ∎

  0-selfinverse : - 0r ≡ 0r
  0-selfinverse = sym (implicitInverse _ _ (+-rid 0r))

  0-idempotent : 0r + 0r ≡ 0r
  0-idempotent = +-lid 0r

  +-idempotency→0 : (x : ⟨ R ⟩) → x ≡ x + x → 0r ≡ x
  +-idempotency→0 x p =
    0r              ≡⟨ sym (+-rinv _) ⟩
    x + (- x)       ≡⟨ cong (λ u → u + (- x)) p ⟩
    (x + x) + (- x) ≡⟨ sym (+-assoc _ _ _) ⟩
    x + (x + (- x)) ≡⟨ cong (λ u → x + u) (+-rinv _) ⟩
    x + 0r          ≡⟨ +-rid x ⟩
    x               ∎

  0-rightNullifies : (x : ⟨ R ⟩) → x · 0r ≡ 0r
  0-rightNullifies x =
              let x·0-is-idempotent : x · 0r ≡ x · 0r + x · 0r
                  x·0-is-idempotent =
                    x · 0r               ≡⟨ cong (λ u → x · u) (sym 0-idempotent) ⟩
                    x · (0r + 0r)        ≡⟨ ·-rdist-+ _ _ _ ⟩
                    (x · 0r) + (x · 0r)  ∎
              in sym (+-idempotency→0 _ x·0-is-idempotent)

  0-leftNullifies : (x : ⟨ R ⟩) → 0r · x ≡ 0r
  0-leftNullifies x =
              let 0·x-is-idempotent : 0r · x ≡ 0r · x + 0r · x
                  0·x-is-idempotent =
                    0r · x               ≡⟨ cong (λ u → u · x) (sym 0-idempotent) ⟩
                    (0r + 0r) · x        ≡⟨ ·-ldist-+ _ _ _ ⟩
                    (0r · x) + (0r · x)  ∎
              in sym (+-idempotency→0 _ 0·x-is-idempotent)

  -commutesWithRight-· : (x y : ⟨ R ⟩) →  x · (- y) ≡ - (x · y)
  -commutesWithRight-· x y = implicitInverse (x · y) (x · (- y))

                               (x · y + x · (- y)     ≡⟨ sym (·-rdist-+ _ _ _) ⟩
                               x · (y + (- y))        ≡⟨ cong (λ u → x · u) (+-rinv y) ⟩
                               x · 0r                 ≡⟨ 0-rightNullifies x ⟩
                               0r ∎)

  -commutesWithLeft-· : (x y : ⟨ R ⟩) →  (- x) · y ≡ - (x · y)
  -commutesWithLeft-· x y = implicitInverse (x · y) ((- x) · y)

                              (x · y + (- x) · y     ≡⟨ sym (·-ldist-+ _ _ _) ⟩
                              (x - x) · y            ≡⟨ cong (λ u → u · y) (+-rinv x) ⟩
                              0r · y                 ≡⟨ 0-leftNullifies y ⟩
                              0r ∎)

  -isDistributive : (x y : ⟨ R ⟩) → (- x) + (- y) ≡ - (x + y)
  -isDistributive x y =
    implicitInverse _ _
         ((x + y) + ((- x) + (- y)) ≡⟨ sym (+-assoc _ _ _) ⟩
          x + (y + ((- x) + (- y))) ≡⟨ cong
                                         (λ u → x + (y + u))
                                         (+-comm _ _) ⟩
          x + (y + ((- y) + (- x))) ≡⟨ cong (λ u → x + u) (+-assoc _ _ _) ⟩
          x + ((y + (- y)) + (- x)) ≡⟨ cong (λ u → x + (u + (- x)))
                                            (+-rinv _) ⟩
          x + (0r + (- x))           ≡⟨ cong (λ u → x + u) (+-lid _) ⟩
          x + (- x)                 ≡⟨ +-rinv _ ⟩
          0r ∎)

  translatedDifference : (x a b : ⟨ R ⟩) → a - b ≡ (x + a) - (x + b)
  translatedDifference x a b =
              a - b                       ≡⟨ cong (λ u → a + u)
                                                  (sym (+-lid _)) ⟩
              (a + (0r + (- b)))          ≡⟨ cong (λ u → a + (u + (- b)))
                                                  (sym (+-rinv _)) ⟩
              (a + ((x + (- x)) + (- b))) ≡⟨ cong (λ u → a + u)
                                                  (sym (+-assoc _ _ _)) ⟩
              (a + (x + ((- x) + (- b)))) ≡⟨ (+-assoc _ _ _) ⟩
              ((a + x) + ((- x) + (- b))) ≡⟨ cong (λ u → u + ((- x) + (- b)))
                                                  (+-comm _ _) ⟩
              ((x + a) + ((- x) + (- b))) ≡⟨ cong (λ u → (x + a) + u)
                                                  (-isDistributive _ _) ⟩
              ((x + a) - (x + b)) ∎

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
{-# OPTIONS --no-positivity-check #-}

{- This file gives a standard example showing that if arguments to
   constructors can use the datatype in a negative position (to the
   left of one or an odd number of arrows), then termination and
   logical consistency is lost. -}

module neg-datatype-nonterm where

open import empty

data Bad : Set where
  bad : (Bad → ⊥) → Bad

badFunc : Bad → ⊥
badFunc (bad f) = f (bad f)

-- if you try to normalize the following, it will diverge
inconsistency : ⊥
inconsistency = badFunc (bad badFunc)

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL