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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Functions.Definition
open import Setoids.Setoids
open import Setoids.Subset
open import Graphs.Definition
open import Sets.FinSet.Definition
open import Numbers.Naturals.Semiring

module Graphs.Colouring where

Colouring : (n : ℕ) {a b c : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) → Set (a ⊔ c)
Colouring n {V' = V'} G = {x y : V'} → (Graph._<->_ G x y) → FinSet n

inheritColouring : {n : ℕ} {a b c : _} {V' : Set a} {V : Setoid {a} {b} V'} {G : Graph c V} → (k : Colouring n G) → {e : _} {pred : V' → Set e} {sub : subset V pred} {d : _} {_<->'_ : Rel {_} {d} (Sg V' pred)} (H : Subgraph G sub _<->'_) → Colouring n (subgraphIsGraph H)
inheritColouring k H {v1 , _} {v2 , _} x-y = k (Subgraph.inherits H x-y)

Monochromatic : {a b c : Level} {V' : Set a} {V : Setoid {a} {b} V'} {G : Graph c V} {n : ℕ} → (k : Colouring n G) → {d e : _} {pred : V' → Set d} {sub : subset V pred} {_<->'_ : Rel {_} {e} (Sg V' pred)} (H : Subgraph G sub _<->'_) → Set (a ⊔ d ⊔ e)
Monochromatic {V' = V'} {n = n} k {pred = pred} {sub = sub} {_<->'_} H = Sg (FinSet n) (λ c → {x : Sg V' pred} {y : Sg V' pred} (edge : x <->' y) → (inheritColouring k H) edge ≡ c)


text:
module Sets.IterativeSet.Relator where

import      Lvl
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural
open import Sets.IterativeSet
open import Syntax.Function
open import Type

module _ where
  private variable {ℓ ℓ₁ ℓ₂} : Lvl.Level
  private variable {A B} : Iset{ℓ}
  open Iset

  _≡_ : (A : Iset{ℓ₁}) → (B : Iset{ℓ₂}) → Type{ℓ₁ Lvl.⊔ ℓ₂}
  record _⊆_ (A : Iset{ℓ₁}) (B : Iset{ℓ₂}) : Type{ℓ₁ Lvl.⊔ ℓ₂}
  _⊇_ : Iset{ℓ₁} → Iset{ℓ₂} → Type{ℓ₁ Lvl.⊔ ℓ₂}

  -- Set equality is by definition the antisymmetric property of the subset relation.
  _≡_ A B = (A ⊇ B) ∧ (A ⊆ B)

  -- Set membership is the existence of an index in the set that points to a set equal element to the element.
  _∈_ : Iset{ℓ₁} → Iset{ℓ₂} → Type{ℓ₁ Lvl.⊔ ℓ₂}
  a ∈ B = ∃{Obj = Index(B)} (ib ↦ a ≡ elem(B)(ib))

  -- Set subset is a mapping between the indices such that they point to the same element in both sets.
  record _⊆_ A B where
    constructor intro
    inductive
    eta-equality
    field
      map : Index(A) → Index(B)
      proof : ∀{ia} → (elem(A)(ia) ≡ elem(B)(map(ia)))

  A ⊇ B = B ⊆ A
  module _⊇_ where
    open _⊆_ public

  _∉_ : Iset{ℓ₁} → Iset{ℓ₂} → Type{ℓ₁ Lvl.⊔ ℓ₂}
  a ∉ B = ¬(a ∈ B)

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module SizedIO.Object where

open import Data.Product

record Interface : Set₁ where
  field
    Method  : Set
    Result  : (m : Method) → Set
open Interface public

-- A simple object just returns for a method the response
-- and the object itself
record Object (i : Interface) : Set where
  coinductive
  field
    objectMethod : (m : Method i) → Result i m × Object i

open Object public

_▹_ : {A : Set} → {B : Set} → A → (A → B) → B
a ▹ f = f a

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


text:
A : Set

B : Set₁
B = Set

C : Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, AIM XXIII, 2016-04-26 flight EDI-GOT home

-- {-# OPTIONS -v impossible:10 #-}

-- Parameter arguments of overloaded projection applications
-- should not be skipped!

record R A : Set where
  field f : A
open R

record S A : Set where
  field f : A
open S

module _ (A B : Set) (a : A) where

  r : R A
  f r = a

  test1 = f {A = A} r
  test2 = f {A} r

  test = f {A = B} r

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
-- Andreas, 2011-10-03
{-# OPTIONS --experimental-irrelevance #-}
module MatchOnIrrelevantData1 where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- the index does not determine the constructor

data Fin : Nat -> Set where
  zero : (n : Nat) -> Fin (suc n)
  suc  : (n : Nat) -> Fin n -> Fin (suc n)

-- should fail:
toNat : (n : Nat) → .(Fin n) -> Nat
toNat (suc n) (zero .n) = zero
toNat (suc n) (suc .n i) = suc (toNat n i)

-- Cannot split on argument of irrelevant datatype Fin (suc @0)
-- when checking the definition of toNat

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Ints.Add.Comm where

open import Ints
open import Nats.Add.Comm

open import Equality

------------------------------------------------------------------------
-- internal stuffs

private

  a+b=b+a : ∀ a b → a + b ≡ b + a
  a+b=b+a (+ a) (+ b) = + (a :+: b)
    ≡⟨ cong +_ (nat-add-comm a b) ⟩ + (b :+: a) QED
  a+b=b+a (+    a  ) (-[1+ b ])
    rewrite nat-add-comm a b = refl
  a+b=b+a (-[1+ a ]) (+    b  )
    rewrite nat-add-comm a b = refl
  a+b=b+a (-[1+ a ]) (-[1+ b ])
    rewrite nat-add-comm a b = refl

------------------------------------------------------------------------
-- public aliases

int-add-comm : ∀ a b → a + b ≡ b + a
int-add-comm = a+b=b+a


text:
-- 2010-09-07 Andreas
-- 2011-10-04 may not work even in the presence of experimental irr.
{-# OPTIONS --experimental-irrelevance #-}
module SplitOnIrrelevant where

data Bool : Set where
  true false : Bool

not : .Bool -> Bool
not true = false  -- needs to fail
not false = true

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Algebra.BasicProp where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

open import Cubical.Structures.Group

private
  variable
    ℓ ℓ' : Level

---------------------------------------------------------------------
-- Groups basic properties
---------------------------------------------------------------------

-- We will use the multiplicative notation for groups

module _ (G : Group {ℓ}) where

  open group-·syntax G

  private
    ₁· = group-lid G

    ·₁ = group-rid G

    ·-assoc = group-assoc G

    ⁻¹· = group-linv G

    ·⁻¹ = group-rinv G

  id-is-unique : isContr (Σ[ x ∈ ⟨ G ⟩ ] ∀ (y : ⟨ G ⟩) → (x · y ≡ y) × (y · x ≡ y))
  id-is-unique = (₁ , λ y → ₁· y , ·₁ y) ,
                 λ { (e , is-unit) → ΣProp≡ (λ x → isPropΠ λ y → isPropΣ (group-is-set G _ _)
                                                                    λ _ →    group-is-set G _ _)
                                              (₁     ≡⟨ sym (snd (is-unit ₁)) ⟩
                                               ₁ · e ≡⟨ ₁· e ⟩
                                               e ∎
                                              )}

  are-inverses : ∀ (x y : ⟨ G ⟩)
               → x · y ≡ ₁
               → (y ≡ x ⁻¹) × (x ≡ y ⁻¹)
  are-inverses x y eq = (y                ≡⟨ sym (₁· y) ⟩
                         ₁ · y            ≡⟨ sym (·-assoc _ _ _ ∙ cong (_· y) (⁻¹· _)) ⟩
                         (x ⁻¹) · (x · y) ≡⟨ cong ((x ⁻¹) ·_) eq ⟩
                         (x ⁻¹) · ₁       ≡⟨ ·₁ _ ⟩
                         x ⁻¹ ∎)
                     , (x                 ≡⟨ sym (·₁ x) ⟩
                        x · ₁             ≡⟨ cong (x ·_) (sym (·⁻¹ y)) ∙ ·-assoc _ _ _ ⟩
                        (x · y) · (y ⁻¹)  ≡⟨ cong (_· (y ⁻¹)) eq ⟩
                        ₁ · (y ⁻¹)        ≡⟨ ₁· _ ⟩
                        y ⁻¹ ∎)

  inv-involutive : ∀ (x : ⟨ G ⟩)
                 → (x ⁻¹) ⁻¹ ≡ x
  inv-involutive x = sym (snd (are-inverses x (x ⁻¹) (·⁻¹ x)))

  inv-distr : ∀ (x y : ⟨ G ⟩) → (x · y) ⁻¹ ≡ (y ⁻¹) · (x ⁻¹)
  inv-distr x y = sym (fst (are-inverses _ _ γ))
    where γ : (x · y) · ((y ⁻¹) · (x ⁻¹)) ≡ ₁
          γ = (x · y) · ((y ⁻¹) · (x ⁻¹)) ≡⟨ sym (cong (x ·_) (sym (·-assoc _ _ _)) ∙ ·-assoc _ _ _) ⟩
              x · ((y · (y ⁻¹)) · (x ⁻¹)) ≡⟨ cong (λ - → x · (- · (x ⁻¹))) (·⁻¹ y) ⟩
              x · (₁ · (x ⁻¹))            ≡⟨ cong (x ·_) (₁· (x ⁻¹)) ⟩
              x · (x ⁻¹)                  ≡⟨ ·⁻¹ x ⟩
              ₁ ∎

  left-cancel : ∀ (x y z : ⟨ G ⟩) → x · y ≡ x · z → y ≡ z
  left-cancel x y z eq = y                ≡⟨ sym (cong (_· y) (⁻¹· x) ∙ ₁· y) ⟩
                         ((x ⁻¹) · x) · y ≡⟨ sym (·-assoc _ _ _) ⟩
                         (x ⁻¹) · (x · y) ≡⟨ cong ((x ⁻¹) ·_) eq ⟩
                         (x ⁻¹) · (x · z) ≡⟨ ·-assoc _ _ _ ⟩
                         ((x ⁻¹) · x) · z ≡⟨ cong (_· z) (⁻¹· x) ∙ ₁· z ⟩
                         z ∎

  right-cancel : ∀ (x y z : ⟨ G ⟩) → x · z ≡ y · z → x ≡ y
  right-cancel x y z eq = x                ≡⟨ sym (cong (x ·_) (·⁻¹ z) ∙ ·₁ x) ⟩
                          x · (z · (z ⁻¹)) ≡⟨ ·-assoc _ _ _ ⟩
                          (x · z) · (z ⁻¹) ≡⟨ cong (_· (z ⁻¹)) eq ⟩
                          (y · z) · (z ⁻¹) ≡⟨ sym (·-assoc _ _ _) ⟩
                          y · (z · (z ⁻¹)) ≡⟨ cong (y ·_) (·⁻¹ z) ∙ ·₁ y ⟩
                          y ∎


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

module overloading where

-- An overloading system based on instance arguments. See `overloading.core` for
-- more details and documentation.

open import overloading.bundle public
open import overloading.core public
open import overloading.level public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

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

module Definition.Untyped where

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

infixl 30 _∙_
infix 30 Π_▹_
infixr 22 _▹▹_
infix 30 Σ_▹_
infixr 22 _××_
infix 30 ⟦_⟧_▹_
infixl 30 _ₛ•ₛ_ _•ₛ_ _ₛ•_
infix 25 _[_]
infix 25 _[_]↑

-- Typing contexts (length indexed snoc-lists, isomorphic to lists).
-- Terms added to the context are well scoped in the sense that it cannot
-- contain more unbound variables than can be looked up in the context.

data Con (A : Nat → Set) : Nat → Set where
  ε   :                             Con A 0        -- Empty context.
  _∙_ : {n : Nat} → Con A n → A n → Con A (1+ n)   -- Context extension.

private
  variable
    n m ℓ : Nat

-- Representation of sub terms using a list of binding levels

data GenTs (A : Nat → Set) : Nat → List Nat → Set where
  []  : {n : Nat} → GenTs A n []
  _∷_ : {n b : Nat} {bs : List Nat} (t : A (b + n)) (ts : GenTs A n bs) → GenTs A n (b ∷ bs)

-- Kinds are indexed on the number of expected sub terms
-- and the number of new variables bound by each sub term

data Kind : (ns : List Nat) → Set where
  Ukind : Kind []

  Pikind  : Kind (0 ∷ 1 ∷ [])
  Lamkind : Kind (1 ∷ [])
  Appkind : Kind (0 ∷ 0 ∷ [])

  Sigmakind : Kind (0 ∷ 1 ∷ [])
  Prodkind  : Kind (0 ∷ 0 ∷ [])
  Fstkind   : Kind (0 ∷ [])
  Sndkind   : Kind (0 ∷ [])

  Natkind    : Kind []
  Zerokind   : Kind []
  Suckind    : Kind (0 ∷ [])
  Natreckind : Kind (1 ∷ 0 ∷ 0 ∷ 0 ∷ [])

  Unitkind : Kind []
  Starkind : Kind []

  Emptykind    : Kind []
  Emptyreckind : Kind (0 ∷ 0 ∷ [])

-- Terms are indexed by its number of unbound variables and are either:
-- de Bruijn style variables or
-- generic terms, formed by their kind and sub terms

data Term (n : Nat) : Set where
  var : (x : Fin n) → Term n
  gen : {bs : List Nat} (k : Kind bs) (c : GenTs Term n bs) → Term n

private
  variable
    A F H t u v : Term n
    B E G       : Term (1+ n)

-- The Grammar of our language.

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

-- Type constructors.
U      : Term n                      -- Universe.
U = gen Ukind []

Π_▹_ : (A : Term n) (B : Term (1+ n)) → Term n  -- Dependent function type (B is a binder).
Π A ▹ B = gen Pikind (A ∷ B ∷ [])

Σ_▹_ : (A : Term n) (B : Term (1+ n)) → Term n  -- Dependent sum type (B is a binder).
Σ A ▹ B = gen Sigmakind (A ∷ B ∷ [])

ℕ      : Term n                      -- Type of natural numbers.
ℕ = gen Natkind []

Empty : Term n                       -- Empty type
Empty = gen Emptykind []

Unit  : Term n                       -- Unit type
Unit = gen Unitkind []

lam    : (t : Term (1+ n)) → Term n  -- Function abstraction (binder).
lam t = gen Lamkind (t ∷ [])

_∘_    : (t u : Term n) → Term n     -- Application.
t ∘ u = gen Appkind (t ∷ u ∷ [])

prod : (t u : Term n) → Term n       -- Dependent products
prod t u = gen Prodkind (t ∷ u ∷ [])

fst : (t : Term n) → Term n          -- First projection
fst t = gen Fstkind (t ∷ [])

snd : (t : Term n) → Term n          -- Second projection
snd t = gen Sndkind (t ∷ [])

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

suc    : (t : Term n)       → Term n -- Successor.
suc t = gen Suckind (t ∷ [])

natrec : (A : Term (1+ n)) (t u v : Term n) → Term n  -- Natural number recursor (A is a binder).
natrec A t u v = gen Natreckind (A ∷ t ∷ u ∷ v ∷ [])

star : Term n                        -- Unit element
star = gen Starkind []

Emptyrec : (A e : Term n) → Term n   -- Empty type recursor
Emptyrec A e = gen Emptyreckind (A ∷ e ∷ [])

-- Binding types

data BindingType : Set where
  BΠ : BindingType
  BΣ : BindingType

⟦_⟧_▹_ : BindingType → Term n → Term (1+ n) → Term n
⟦ BΠ ⟧ F ▹ G = Π F ▹ G
⟦ BΣ ⟧ F ▹ G = Σ F ▹ G

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

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

B-PE-injectivity : ∀ W → ⟦ W ⟧ F ▹ G PE.≡ ⟦ W ⟧ H ▹ E → F PE.≡ H × G PE.≡ E
B-PE-injectivity BΠ PE.refl = PE.refl , PE.refl
B-PE-injectivity BΣ PE.refl = PE.refl , PE.refl

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

suc-PE-injectivity : suc t PE.≡ suc u → t PE.≡ u
suc-PE-injectivity PE.refl = PE.refl

-- Neutral terms.

-- A term is neutral if it has a variable in head position.
-- The variable blocks reduction of such terms.

data Neutral : Term n → Set where
  var       : (x : Fin n) → Neutral (var x)
  ∘ₙ        : Neutral t   → Neutral (t ∘ u)
  fstₙ      : Neutral t   → Neutral (fst t)
  sndₙ      : Neutral t   → Neutral (snd t)
  natrecₙ   : Neutral v   → Neutral (natrec G t u v)
  Emptyrecₙ : Neutral t   → Neutral (Emptyrec A t)

-- Weak head normal forms (whnfs).

-- These are the (lazy) values of our language.

data Whnf {n : Nat} : Term n → Set where

  -- Type constructors are whnfs.
  Uₙ     : Whnf U
  Πₙ     : Whnf (Π A ▹ B)
  Σₙ     : Whnf (Σ A ▹ B)
  ℕₙ     : Whnf ℕ
  Unitₙ  : Whnf Unit
  Emptyₙ : Whnf Empty

  -- Introductions are whnfs.
  lamₙ  : Whnf (lam t)
  zeroₙ : Whnf zero
  sucₙ  : Whnf (suc t)
  starₙ : Whnf star
  prodₙ : Whnf (prod t u)

  -- Neutrals are whnfs.
  ne    : Neutral t → Whnf t

-- Whnf inequalities.

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

U≢ne : Neutral A → U PE.≢ A
U≢ne () PE.refl

ℕ≢ne : Neutral A → ℕ PE.≢ A
ℕ≢ne () PE.refl

Empty≢ne : Neutral A → Empty PE.≢ A
Empty≢ne () PE.refl

Unit≢ne : Neutral A → Unit PE.≢ A
Unit≢ne () PE.refl

B≢ne : ∀ W → Neutral A → ⟦ W ⟧ F ▹ G PE.≢ A
B≢ne BΠ () PE.refl
B≢ne BΣ () PE.refl

U≢B : ∀ W → U PE.≢ ⟦ W ⟧ F ▹ G
U≢B BΠ ()
U≢B BΣ ()

ℕ≢B : ∀ W → ℕ PE.≢ ⟦ W ⟧ F ▹ G
ℕ≢B BΠ ()
ℕ≢B BΣ ()

Empty≢B : ∀ W → Empty PE.≢ ⟦ W ⟧ F ▹ G
Empty≢B BΠ ()
Empty≢B BΣ ()

Unit≢B : ∀ W → Unit PE.≢ ⟦ W ⟧ F ▹ G
Unit≢B BΠ ()
Unit≢B BΣ ()

zero≢ne : Neutral t → zero PE.≢ t
zero≢ne () PE.refl

suc≢ne : Neutral t → suc u PE.≢ t
suc≢ne () PE.refl

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

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

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

-- A (small) type in whnf is either Π A B, Σ A B, ℕ, Empty, Unit or neutral.
-- Large types could also be U.

data Type {n : Nat} : Term n → Set where
  Πₙ     :             Type (Π A ▹ B)
  Σₙ     :             Type (Σ A ▹ B)
  ℕₙ     :             Type ℕ
  Emptyₙ :             Type Empty
  Unitₙ  :             Type Unit
  ne     : Neutral t → Type t

⟦_⟧-type : ∀ (W : BindingType) → Type (⟦ W ⟧ F ▹ G)
⟦ BΠ ⟧-type = Πₙ
⟦ BΣ ⟧-type = Σₙ

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

data Function {n : Nat} : Term n → Set where
  lamₙ : Function (lam t)
  ne   : Neutral t → Function t

-- A whnf of type Σ A ▹ B is either prod t u or neutral.

data Product {n : Nat} : Term n → Set where
  prodₙ : Product (prod t u)
  ne    : Neutral t → Product t

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

naturalWhnf : Natural t → Whnf t
naturalWhnf sucₙ   = sucₙ
naturalWhnf zeroₙ  = zeroₙ
naturalWhnf (ne x) = ne x

typeWhnf : Type A → Whnf A
typeWhnf Πₙ     = Πₙ
typeWhnf Σₙ     = Σₙ
typeWhnf ℕₙ     = ℕₙ
typeWhnf Emptyₙ = Emptyₙ
typeWhnf Unitₙ  = Unitₙ
typeWhnf (ne x) = ne x

functionWhnf : Function t → Whnf t
functionWhnf lamₙ   = lamₙ
functionWhnf (ne x) = ne x

productWhnf : Product t → Whnf t
productWhnf prodₙ  = prodₙ
productWhnf (ne x) = ne x

⟦_⟧ₙ : (W : BindingType) → Whnf (⟦ W ⟧ F ▹ G)
⟦_⟧ₙ BΠ = Πₙ
⟦_⟧ₙ BΣ = Σₙ

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

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

data Wk : Nat → Nat → Set where
  id    : {n : Nat} → Wk n n                      -- η : Γ ≤ Γ.
  step  : {n m : Nat} → Wk m n → Wk (1+ m) n      -- If η : Γ ≤ Δ then step η : Γ∙A ≤ Δ.
  lift  : {n m : Nat} → Wk m n → Wk (1+ m) (1+ n) -- If η : Γ ≤ Δ then lift η : Γ∙A ≤ Δ∙A.

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

infixl 30 _•_

_•_                :  {l m n : Nat} → Wk l m → Wk m n → Wk l n
id      • η′       =  η′
step η  • η′       =  step  (η • η′)
lift η  • id       =  lift  η
lift η  • step η′  =  step  (η • η′)
lift η  • lift η′  =  lift  (η • η′)

liftn : {k m : Nat} → Wk k m → (n : Nat) → Wk (n + k) (n + m)
liftn ρ Nat.zero = ρ
liftn ρ (1+ n)   = lift (liftn ρ n)

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

wkVar : {m n : Nat} (ρ : Wk m n) (x : Fin n) → Fin m
wkVar id x            = x
wkVar (step ρ) x      = (wkVar ρ x) +1
wkVar (lift ρ) x0     = x0
wkVar (lift ρ) (x +1) = (wkVar ρ x) +1

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

mutual
  wkGen : {m n : Nat} {bs : List Nat} (ρ : Wk m n) (c : GenTs Term n bs) → GenTs Term m bs
  wkGen ρ []                = []
  wkGen ρ (_∷_ {b = b} t c) = (wk (liftn ρ b) t) ∷ (wkGen ρ c)

  wk : {m n : Nat} (ρ : Wk m n) (t : Term n) → Term m
  wk ρ (var x)   = var (wkVar ρ x)
  wk ρ (gen k c) = gen k (wkGen ρ c)

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

wk1 : Term n → Term (1+ n)
wk1 = wk (step id)

-- Weakening of a neutral term.

wkNeutral : ∀ ρ → Neutral t → Neutral {n} (wk ρ t)
wkNeutral ρ (var n)       = var (wkVar ρ n)
wkNeutral ρ (∘ₙ n)        = ∘ₙ (wkNeutral ρ n)
wkNeutral ρ (fstₙ n)      = fstₙ (wkNeutral ρ n)
wkNeutral ρ (sndₙ n)      = sndₙ (wkNeutral ρ n)
wkNeutral ρ (natrecₙ n)   = natrecₙ (wkNeutral ρ n)
wkNeutral ρ (Emptyrecₙ e) = Emptyrecₙ (wkNeutral ρ e)

-- Weakening can be applied to our whnf views.

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

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

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

wkProduct : ∀ ρ → Product t → Product {n} (wk ρ t)
wkProduct ρ prodₙ  = prodₙ
wkProduct ρ (ne x) = ne (wkNeutral ρ x)

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

-- Non-dependent version of Π.

_▹▹_ : Term n → Term n → Term n
A ▹▹ B = Π A ▹ wk1 B

-- Non-dependent products.

_××_ : Term n → Term n → Term n
A ×× B = Σ A ▹ wk1 B

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

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

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

Subst : Nat → Nat → Set
Subst m n = Fin n → Term m

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

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

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

head : Subst m (1+ n) → Term m
head σ = σ x0

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

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

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

substVar : (σ : Subst m n) (x : Fin n) → Term m
substVar σ x = σ x

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

idSubst : Subst n n
idSubst = var

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

wk1Subst : Subst m n → Subst (1+ m) n
wk1Subst σ x = wk1 (σ x)

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

liftSubst : (σ : Subst m n) → Subst (1+ m) (1+ n)
liftSubst σ x0     = var x0
liftSubst σ (x +1) = wk1Subst σ x

liftSubstn : {k m : Nat} → Subst k m → (n : Nat) → Subst (n + k) (n + m)
liftSubstn σ Nat.zero = σ
liftSubstn σ (1+ n)   = liftSubst (liftSubstn σ n)

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

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

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

mutual
  substGen : {bs : List Nat} (σ : Subst m n) (g : GenTs Term n bs) → GenTs Term m bs
  substGen σ  []      = []
  substGen σ (_∷_ {b = b} t ts) = subst (liftSubstn σ b) t ∷ (substGen σ ts)

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

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

consSubst : Subst m n → Term m → Subst m (1+ n)
consSubst σ t  x0    = t
consSubst σ t (x +1) = σ x

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

sgSubst : Term n → Subst n (1+ n)
sgSubst = consSubst idSubst

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

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

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

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

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

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

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

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

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

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

B-subst : (σ : Subst m n) (W : BindingType) (F : Term n) (G : Term (1+ n))
        → subst σ (⟦ W ⟧ F ▹ G) PE.≡ ⟦ W ⟧ (subst σ F) ▹ (subst (liftSubst σ) G)
B-subst σ BΠ F G = PE.refl
B-subst σ BΣ F G = PE.refl

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
module A.Issue1635 (A : Set₁) where

data Foo : Set where
  foo : Foo


text:
module _ where

import Agda.Builtin.Equality
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Primitive
open import Common.IO

data ⊥ : Set where

record R₁ a : Set (lsuc a) where
  field
    R : {A : Set a} → A → A → Set a
    r : {A : Set a} (x : A) → R x x

  P : Set a → Set a
  P A = (x y : A) → R x y

record R₂ (r : ∀ ℓ → R₁ ℓ) : Set₁ where
  field
    f :
      {X Y : Σ Set (R₁.P (r lzero))} →
      R₁.R (r (lsuc lzero)) X Y → fst X → fst Y

module M (r₁ : ∀ ℓ → R₁ ℓ) (r₂ : R₂ r₁) where

  open module R₁′ {ℓ} = R₁ (r₁ ℓ) public using (P)
  open module R₂′     = R₂ r₂     public

  ⊥-elim : {A : Set} → ⊥ → A
  ⊥-elim ()

  p : P ⊥
  p x = ⊥-elim x

open Agda.Builtin.Equality

r₁ : ∀ ℓ → R₁ ℓ
R₁.R (r₁ _) = _≡_
R₁.r (r₁ _) = λ _ → refl

r₂ : R₂ r₁
R₂.f r₂ refl x = x

open M r₁ r₂

data Unit : Set where
  unit : Unit

g : Σ Unit λ _ → P (Σ Set P) → ⊥
g = unit , λ h → f (h (⊤ , λ _ _ → refl) (⊥ , p)) tt

main : IO ⊤
main = return _


text:
module kripke-semantics where

open import level
open import bool
open import closures
open import empty
open import eq
open import level
open import list
open import list-thms
open import nat
open import product
open import relations
open import string
open import sum
open import unit

data formula : Set where
  $ : string → formula
  True : formula
  Implies : formula → formula → formula
  And : formula → formula → formula

ctxt : Set
ctxt = 𝕃 formula

data _⊢_ : ctxt → formula → Set where
  Assume : ∀{Γ f} → (f :: Γ) ⊢ f
  Weaken : ∀{Γ f f'} → Γ ⊢ f → (f' :: Γ) ⊢ f
  ImpliesI : ∀{f1 f2 Γ} → (f1 :: Γ) ⊢ f2 → Γ ⊢ (Implies f1 f2)
  ImpliesE : ∀{f1 f2 Γ} → Γ ⊢ (Implies f1 f2) → Γ ⊢ f1 → Γ ⊢ f2
  TrueI : ∀ {Γ} → Γ ⊢ True
  AndI : ∀{f1 f2 Γ} → Γ ⊢ f1 → Γ ⊢ f2 → Γ ⊢ (And f1 f2)
  AndE : ∀(b : 𝔹){f1 f2 Γ} → Γ ⊢ (And f1 f2) → Γ ⊢ (if b then f1 else f2)

sample-pf : [] ⊢ Implies ($ "p") (And ($ "p") ($ "p"))
sample-pf = ImpliesI{$ "p"} (AndI (Assume{[]}) (Assume))

record struct : Set1 where
  field W         : Set -- a set of worlds
        R         : W → W → Set
        preorderR : preorder R -- a proof that R is a preorder (reflexive and transitive)
        V         : W → string → Set -- a valuation telling whether atomic formula i is true or false in a given world
        monoV     : ∀ { w w' } → R w w' → ∀ { i } → V w i → V w' i
  reflR : reflexive R
  reflR = fst preorderR
  transR : transitive R
  transR = snd preorderR

open struct

_,_⊨_ : ∀(k : struct) → W k → formula → Set
k , w ⊨ ($ x) = V k w x
k , w ⊨ True = ⊤
k , w ⊨ Implies f1 f2 = ∀ {w' : W k} → R k w w' → k , w' ⊨ f1 → k , w' ⊨ f2
k , w ⊨ And f1 f2 = k , w ⊨ f1 ∧ k , w ⊨ f2

module ⊨-example where
  data world : Set where
    w0 : world
    w1 : world
    w2 : world

  data rel : world → world → Set where
    r00 : rel w0 w0
    r11 : rel w1 w1
    r22 : rel w2 w2
    r01 : rel w0 w1
    r02 : rel w0 w2

  rel-refl : reflexive rel
  rel-refl {w0} = r00
  rel-refl {w1} = r11
  rel-refl {w2} = r22

  rel-trans : transitive rel
  rel-trans r00 r00 = r00
  rel-trans r00 r01 = r01
  rel-trans r00 r02 = r02
  rel-trans r11 r11 = r11
  rel-trans r22 r22 = r22
  rel-trans r01 r11 = r01
  rel-trans r02 r22 = r02

  data val : world → string → Set where
    v1p : val w1 "p"
    v1q : val w1 "q"
    v2p : val w2 "p"
    v2q : val w2 "q"

  mono-val : ∀{w w'} → rel w w' → ∀ { i } → val w i → val w' i
  mono-val r00 p = p
  mono-val r11 p = p
  mono-val r22 p = p
  mono-val r01 ()
  mono-val r02 ()

  k : struct
  k = record { W = world ; R = rel ; preorderR = (rel-refl , rel-trans) ; V = val ; monoV = mono-val }

  test-sem : Set
  test-sem = k , w0 ⊨ Implies ($ "p") ($ "q")

  pf-test-sem : k , w0 ⊨ Implies ($ "p") ($ "q")
  pf-test-sem r00 ()
  pf-test-sem r01 p = v1q
  pf-test-sem r02 p = v2q

mono⊨ : ∀{k : struct}{w1 w2 : W k}{f : formula} →
         R k w1 w2 →
         k , w1 ⊨ f →
         k , w2 ⊨ f
mono⊨{k} {f = $ x} r p = monoV k r p
mono⊨{k} {f = True} r p = triv
mono⊨{k} {f = Implies f1 f2} r p r' p' = p (transR k r r') p'
mono⊨{k} {f = And f1 f2} r (p1 , p2) = mono⊨{f = f1} r p1 , mono⊨{f = f2} r p2

_,_⊨ctxt_ : ∀(k : struct) → W k → ctxt → Set
k , w ⊨ctxt [] = ⊤
k , w ⊨ctxt (f :: Γ) = (k , w ⊨ f) ∧ (k , w ⊨ctxt Γ)

mono⊨ctxt : ∀{k : struct}{Γ : ctxt}{w1 w2 : W k} →
            R k w1 w2 →
            k , w1 ⊨ctxt Γ →
            k , w2 ⊨ctxt Γ
mono⊨ctxt{k}{[]} _ _ = triv
mono⊨ctxt{k}{f :: Γ} r (u , v) = mono⊨{k}{f = f} r u , mono⊨ctxt{k}{Γ} r v

_⊩_ : ctxt → formula → Set1
Γ ⊩ f = ∀{k : struct}{w : W k} → k , w ⊨ctxt Γ → k , w ⊨ f

Soundness : ∀{Γ : ctxt}{f : formula} → Γ ⊢ f → Γ ⊩ f
Soundness Assume g = fst g
Soundness (Weaken p) g = Soundness p (snd g)
Soundness (ImpliesI p) g r u' = Soundness p (u' , mono⊨ctxt r g)
Soundness (ImpliesE p p') {k} g = (Soundness p g) (reflR k) (Soundness p' g)
Soundness TrueI g = triv
Soundness (AndI p p') g = (Soundness p g , Soundness p' g)
Soundness (AndE tt p) g = fst (Soundness p g)
Soundness (AndE ff p) g = snd (Soundness p g)

data _≼_ : 𝕃 formula → 𝕃 formula → Set where
  ≼-refl : ∀ {Γ} → Γ ≼ Γ
  ≼-cons : ∀ {Γ Γ' f} → Γ ≼ Γ' → Γ ≼ (f :: Γ')

≼-trans : ∀ {Γ Γ' Γ''} → Γ ≼ Γ' → Γ' ≼ Γ'' → Γ ≼ Γ''
≼-trans u ≼-refl = u
≼-trans u (≼-cons u') = ≼-cons (≼-trans u u')

Weaken≼ : ∀ {Γ Γ'}{f : formula} → Γ ≼ Γ' → Γ ⊢ f → Γ' ⊢ f
Weaken≼ ≼-refl p = p
Weaken≼ (≼-cons d) p = Weaken (Weaken≼ d p)

U : struct
U = record { W = ctxt ;
             R = _≼_ ;
             preorderR = ≼-refl , ≼-trans ;
             V = λ Γ n → Γ ⊢ $ n ;
             monoV = λ d p → Weaken≼ d p }

CompletenessU : ∀{f : formula}{Γ : W U} → U , Γ ⊨ f → Γ ⊢ f
SoundnessU : ∀{f : formula}{Γ : W U} → Γ ⊢ f → U , Γ ⊨ f
CompletenessU {$ x} u = u
CompletenessU {True} u = TrueI
CompletenessU {And f f'} u = AndI (CompletenessU{f} (fst u)) (CompletenessU{f'} (snd u))
CompletenessU {Implies f f'}{Γ} u =
  ImpliesI
    (CompletenessU {f'}
      (u (≼-cons ≼-refl) (SoundnessU {f} (Assume {Γ}))))
SoundnessU {$ x} p = p
SoundnessU {True} p = triv
SoundnessU {And f f'} p = SoundnessU{f} (AndE tt p) , SoundnessU{f'} (AndE ff p)
SoundnessU {Implies f f'} p r u = SoundnessU (ImpliesE (Weaken≼ r p) (CompletenessU {f} u))

ctxt-id : ∀{Γ : ctxt} → U , Γ ⊨ctxt Γ
ctxt-id{[]} = triv
ctxt-id{f :: Γ} = SoundnessU{f} Assume , mono⊨ctxt (≼-cons ≼-refl) (ctxt-id {Γ})

Completeness : ∀{Γ : ctxt}{f : formula} → Γ ⊩ f → Γ ⊢ f
Completeness{Γ} p = CompletenessU (p{U}{Γ} (ctxt-id{Γ}))

Universality1 : ∀{Γ : ctxt}{f : formula} → Γ ⊩ f → U , Γ ⊨ f
Universality1{Γ}{f} p = SoundnessU (Completeness{Γ}{f} p)

Universality2 : ∀{Γ : ctxt}{f : formula} → U , Γ ⊨ f → Γ ⊩ f
Universality2{Γ}{f} p = Soundness (CompletenessU{f}{Γ} p)

nbe : ∀ {Γ f} → Γ ⊢ f → Γ ⊢ f
nbe {Γ} p = Completeness (Soundness p)

module tests where

  -- here we see several proofs which normalize to just TrueI using the nbe function

  a : [] ⊢ True
  a = AndE tt (AndI TrueI TrueI)
  a' = nbe a

  b : [] ⊢ True
  b = ImpliesE (ImpliesE (ImpliesI (ImpliesI (Assume))) TrueI) TrueI
  b' = nbe b

  c : [] ⊢ (Implies ($ "p") ($ "p"))
  c = ImpliesI (ImpliesE (ImpliesI Assume) Assume)
  c' = nbe c

  d : [ $ "q" ] ⊢ (Implies ($ "p") ($ "q"))
  d = ImpliesI (ImpliesE (ImpliesI (Weaken (Weaken Assume))) Assume)
  d' = nbe d

  e : [] ⊢ (Implies (And ($ "p") ($ "q")) (And ($ "p") ($ "q")))
  e = ImpliesI Assume
  e' = nbe e

  f : [] ⊢ (Implies (Implies ($ "p") ($ "q")) (Implies ($ "p") ($ "q")))
  f = ImpliesI Assume
  f' = nbe f

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


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

open import HoTT hiding (_::_)

module algebra.DecidableFreeGroupIsReducedWord {i} (A : Type i) (dec : has-dec-eq A) where

  open import algebra.Word A
  open import algebra.ReducedWord A dec

  -- Some helper functions.

  tail-is-reduced : (x : A) (w : Word) → is-reduced (x :: w) → is-reduced w
  tail-is-reduced x nil         red = lift unit
  tail-is-reduced x (y    :: w) red = red
  tail-is-reduced x (y inv:: w) red = snd red

  tail'-is-reduced : (x : A) (w : Word) → is-reduced (x inv:: w) → is-reduced w
  tail'-is-reduced x nil         red = lift unit
  tail'-is-reduced x (y    :: w) red = snd red
  tail'-is-reduced x (y inv:: w) red = red

  -- Conversion function.

  ReducedWord→FreeGroup : ReducedWord → FreeGroup A
  ReducedWord→FreeGroup (w , red) = f w red
    where
      f : (w : Word) → is-reduced w → FreeGroup A
      f nil         _ = fg-nil
      f (x    :: w) r = x     fg:: f w (tail-is-reduced  x w r)
      f (x inv:: w) r = x fg-inv:: f w (tail'-is-reduced x w r)

  infixr 60 _rw::_ _rw-inv::_

  _rw::_ : A → ReducedWord → ReducedWord
  x rw:: (nil , red) = ((x :: nil) , lift unit)
  x rw:: ((y    :: w) , red) = ((x :: y :: w) , red)
  x rw:: ((y inv:: w) , red) with dec x y
  x rw:: ((y inv:: w) , red) | inl x=y = (w , tail'-is-reduced y w red)
  x rw:: ((y inv:: w) , red) | inr x≠y = ((x :: y inv:: w) , (x≠y , red))

  _rw-inv::_ : A → ReducedWord → ReducedWord
  x rw-inv:: (nil , red) = ((x inv:: nil) , lift unit)
  x rw-inv:: ((y inv:: w) , red) = ((x inv:: y inv:: w) , red)
  x rw-inv:: ((y    :: w) , red) with dec x y
  x rw-inv:: ((y    :: w) , red) | inl eq  = (w , tail-is-reduced y w red)
  x rw-inv:: ((y    :: w) , red) | inr neq = ((x inv:: y :: w) , (neq , red))

  abstract
    rw-inv-r : ∀ x w → x rw:: x rw-inv:: w == w
    rw-inv-r x (nil , red) with dec x x
    rw-inv-r x (nil , red) | inl x=x = idp
    rw-inv-r x (nil , red) | inr x≠x = ⊥-rec (x≠x idp)
    rw-inv-r x ((y :: w)         , red) with dec x y
    rw-inv-r x ((y :: nil)       , red) | inl x=y = x=y |in-ctx _
    rw-inv-r x ((y :: z    :: w) , red) | inl x=y = x=y |in-ctx _
    rw-inv-r x ((y :: z inv:: w) , red) | inl x=y with dec x z
    rw-inv-r x ((y :: z inv:: w) , red) | inl x=y | inl x=z = ⊥-rec (fst red (! x=y ∙ x=z))
    rw-inv-r x ((y :: z inv:: w) , red) | inl x=y | inr x≠z = ReducedWord=-in (x=y |in-ctx _)
    rw-inv-r x ((y :: w)         , red) | inr x≠y with dec x x
    rw-inv-r x ((y :: w)         , red) | inr x≠y | inl x=x = idp
    rw-inv-r x ((y :: w)         , red) | inr x≠y | inr x≠x = ⊥-rec (x≠x idp)
    rw-inv-r x ((y inv:: w)      , red) with dec x x
    rw-inv-r x ((y inv:: w)      , red) | inl x=x = idp
    rw-inv-r x ((y inv:: w)      , red) | inr x≠x = ⊥-rec (x≠x idp)

  abstract
    rw-inv-l : ∀ x w → x rw-inv:: x rw:: w == w
    rw-inv-l x (nil , red) with dec x x
    rw-inv-l x (nil , red) | inl x=x = idp
    rw-inv-l x (nil , red) | inr x≠x = ⊥-rec (x≠x idp)
    rw-inv-l x ((y inv:: w)         , red) with dec x y
    rw-inv-l x ((y inv:: nil)       , red) | inl x=y = x=y |in-ctx _
    rw-inv-l x ((y inv:: z inv:: w) , red) | inl x=y = x=y |in-ctx _
    rw-inv-l x ((y inv:: z    :: w) , red) | inl x=y with dec x z
    rw-inv-l x ((y inv:: z    :: w) , red) | inl x=y | inl x=z = ⊥-rec (fst red (! x=y ∙ x=z))
    rw-inv-l x ((y inv:: z    :: w) , red) | inl x=y | inr x≠z = ReducedWord=-in (x=y |in-ctx _)
    rw-inv-l x ((y inv:: w)         , red) | inr x≠y with dec x x
    rw-inv-l x ((y inv:: w)         , red) | inr x≠y | inl x=x = idp
    rw-inv-l x ((y inv:: w)         , red) | inr x≠y | inr x≠x = ⊥-rec (x≠x idp)
    rw-inv-l x ((y    :: w)         , red) with dec x x
    rw-inv-l x ((y    :: w)         , red) | inl x=x = idp
    rw-inv-l x ((y    :: w)         , red) | inr x≠x = ⊥-rec (x≠x idp)

  FreeGroup→ReducedWord : FreeGroup A → ReducedWord
  FreeGroup→ReducedWord = FreeGroup-rec ReducedWord-is-set
    (nil , lift unit)
    (λ x  _  rw → x     rw:: rw)
    (λ x  _  rw → x rw-inv:: rw)
    (λ x {_} rw → rw-inv-l x rw)
    (λ x {_} rw → rw-inv-r x rw)

  abstract
    rw::-reduced : ∀ x w (red : is-reduced (x :: w))
      → x rw:: (w , tail-is-reduced x w red) == ((x :: w) , red)
    rw::-reduced x nil         red = idp
    rw::-reduced x (y    :: w) red = idp
    rw::-reduced x (y inv:: w) red with dec x y
    rw::-reduced x (y inv:: w) red | inl x=y = ⊥-rec (fst red x=y)
    rw::-reduced x (y inv:: w) red | inr x≠y = ReducedWord=-in idp

  abstract
    rw-inv::-reduced : ∀ x w (red : is-reduced (x inv:: w))
      → x rw-inv:: (w , tail'-is-reduced x w red) == ((x inv:: w) , red)
    rw-inv::-reduced x nil         red = idp
    rw-inv::-reduced x (y inv:: w) red = idp
    rw-inv::-reduced x (y    :: w) red with dec x y
    rw-inv::-reduced x (y    :: w) red | inl x=y = ⊥-rec (fst red x=y)
    rw-inv::-reduced x (y    :: w) red | inr x≠y = ReducedWord=-in idp

  ReducedWord→FreeGroup→ReducedWord :
    ∀ w → FreeGroup→ReducedWord (ReducedWord→FreeGroup w) == w
  ReducedWord→FreeGroup→ReducedWord (w , red) = f w red
    where
      f : ∀ w red → FreeGroup→ReducedWord (ReducedWord→FreeGroup (w , red)) == w , red
      f nil _ = idp
      f (x :: w) red =
        x rw:: FreeGroup→ReducedWord (ReducedWord→FreeGroup (w , tail-is-reduced x w red))
          =⟨ f w (tail-is-reduced x w red) |in-ctx (λ w → x rw:: w) ⟩
        x rw:: (w , tail-is-reduced x w red)
          =⟨ rw::-reduced x w red ⟩
        (x :: w) , red
          ∎
      f (x inv:: w) red =
        x rw-inv:: FreeGroup→ReducedWord (ReducedWord→FreeGroup (w , tail'-is-reduced x w red))
          =⟨ f w (tail'-is-reduced x w red) |in-ctx (λ w → x rw-inv:: w) ⟩
        x rw-inv:: (w , tail'-is-reduced x w red)
          =⟨ rw-inv::-reduced x w red ⟩
        (x inv:: w) , red
          ∎

  ReducedWord→FreeGroup-rw:: : ∀ x w
    → ReducedWord→FreeGroup (x rw:: w) == x fg:: ReducedWord→FreeGroup w
  ReducedWord→FreeGroup-rw:: x (nil , red) = idp
  ReducedWord→FreeGroup-rw:: x ((y     :: w) , red) = idp
  ReducedWord→FreeGroup-rw:: x ((y  inv:: w) , red) with dec x y
  ReducedWord→FreeGroup-rw:: x ((.x inv:: w) , red) | inl idp =
    ! (fg-inv-r x (ReducedWord→FreeGroup (w , tail'-is-reduced x w red)))
  ReducedWord→FreeGroup-rw:: x ((y  inv:: w) , red) | inr x≠y = idp

  ReducedWord→FreeGroup-rw-inv:: : ∀ x w
    → ReducedWord→FreeGroup (x rw-inv:: w) == x fg-inv:: ReducedWord→FreeGroup w
  ReducedWord→FreeGroup-rw-inv:: x (nil , red) = idp
  ReducedWord→FreeGroup-rw-inv:: x ((y  inv:: w) , red) = idp
  ReducedWord→FreeGroup-rw-inv:: x ((y     :: w) , red) with dec x y
  ReducedWord→FreeGroup-rw-inv:: x ((.x    :: w) , red) | inl idp =
    ! (fg-inv-l x (ReducedWord→FreeGroup (w , tail-is-reduced x w red)))
  ReducedWord→FreeGroup-rw-inv:: x ((y     :: w) , red) | inr x≠y = idp

  FreeGroup→ReducedWord→FreeGroup : ∀ fg
    → ReducedWord→FreeGroup (FreeGroup→ReducedWord fg) == fg
  FreeGroup→ReducedWord→FreeGroup = FreeGroup-elim
    (λ _ → =-preserves-set FreeGroup-is-set)
    idp
    (λ x {fg} fg* →
      ReducedWord→FreeGroup (x rw:: FreeGroup→ReducedWord fg)
        =⟨ ReducedWord→FreeGroup-rw:: x (FreeGroup→ReducedWord fg) ⟩
      x fg:: ReducedWord→FreeGroup (FreeGroup→ReducedWord fg)
        =⟨ fg* |in-ctx (_fg::_ x) ⟩
      x fg:: fg
        ∎)
    (λ x {fg} fg* →
      ReducedWord→FreeGroup (x rw-inv:: FreeGroup→ReducedWord fg)
        =⟨ ReducedWord→FreeGroup-rw-inv:: x (FreeGroup→ReducedWord fg) ⟩
      x fg-inv:: ReducedWord→FreeGroup (FreeGroup→ReducedWord fg)
        =⟨ fg* |in-ctx (_fg-inv::_ x) ⟩
      x fg-inv:: fg
        ∎)
    (λ x {fg} fg* → prop-has-all-paths-↓ (FreeGroup-is-set _ _))
    (λ x {fg} fg* → prop-has-all-paths-↓ (FreeGroup-is-set _ _))

FreeGroup≃ReducedWord : FreeGroup A ≃ ReducedWord
FreeGroup≃ReducedWord = FreeGroup→ReducedWord ,
  is-eq
    _
    ReducedWord→FreeGroup
    ReducedWord→FreeGroup→ReducedWord
    FreeGroup→ReducedWord→FreeGroup

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module GotoDefinition where
data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
x + y = {!   !}

max_stars_repo_name: EdNutting/agda-mode-vscode


text:
{-# OPTIONS --no-unicode #-}

module Issue2937.NoUnicode where

foo : _ -> _ -> Set
foo bar x = \x -> foo (bar x {!!}) x

max_forks_repo_name: shlevy/agda


text:
-- Possible improvements:
-- * Parts of the code are not reachable from main.
-- * The following primitives are not used at all: primPOr, primComp,
--   primHComp, prim^glueU and prim^unglueU.

{-# OPTIONS --erased-cubical --save-metas #-}

-- The code from Agda.Builtin.Cubical.Glue should not be compiled.

open import Agda.Builtin.Cubical.Glue

open import Agda.Builtin.Cubical.HCompU
open import Agda.Builtin.Cubical.Id
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub
open import Agda.Builtin.IO
open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma
open import Agda.Builtin.String
open import Agda.Builtin.Unit
open import Agda.Primitive.Cubical

open import Erased-cubical-Cubical

postulate
  putStr : String → IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStr = Data.Text.IO.putStr #-}
{-# COMPILE JS putStr =
    function (x) {
      return function(cb) {
        process.stdout.write(x); cb(0); }; } #-}

i₁ : I
i₁ = primIMax (primIMax (primINeg i0) i1) (primIMin i1 i0)

i₁-1 : IsOne i₁
i₁-1 = IsOne1 (primIMax (primINeg i0) i1) (primIMin i1 i0)
         (IsOne2 (primINeg i0) i1 itIsOne)

p₁ : Partial i1 Nat
p₁ = λ _ → 12

p₂ : PartialP i1 (λ _ → Nat)
p₂ = λ _ → 12

p₃ : PartialP i0 (λ _ → Nat)
p₃ = isOneEmpty

p₄ : 12 ≡ 12
p₄ = λ _ → 12

n₁ : Nat
n₁ = p₄ i0

s : Sub Nat i1 (λ _ → 13)
s = inc 13

n₂ : Nat
n₂ = primSubOut s

i₂ : I
i₂ = primFaceForall (λ _ → i1)

i₃ : Id 12 12
i₃ = conid i0 p₄

i₄ : I
i₄ = primDepIMin i1 (λ _ → i0)

i₅ : I
i₅ = primIdFace i₃

p₅ : 12 ≡ 12
p₅ = primIdPath i₃

n₃ : Nat
n₃ = primIdJ (λ _ _ → Nat) 14 i₃

n₄ : Nat
n₄ = primIdElim (λ _ _ → Nat) (λ _ _ _ → 14) i₃

infix 2 _⊎_

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

-- Some "standard" path functions.

refl : {A : Set} (x : A) → x ≡ x
refl x = λ _ → x

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym p i = p (primINeg i)

cong : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
cong f p i = f (p i)

J :
  {A : Set} {x y : A}
  (P : (x y : A) → x ≡ y → Set) →
  (∀ x → P x x (refl x)) →
  (x≡y : x ≡ y) → P x y x≡y
J {x = x} P p x≡y =
  primTransp (λ i → P _ _ (λ j → x≡y (primIMin i j))) i0 (p x)

subst :
  {A : Set} {x y : A}
  (P : A → Set) → x ≡ y → P x → P y
subst P eq p = primTransp (λ i → P (eq i)) i0 p

subst-refl :
  {A : Set} {x : A}
  (P : A → Set) {p : P x} →
  subst P (refl x) p ≡ p
subst-refl {x = x} P {p = p} i =
  primTransp (λ _ → P x) i p

-- The following definitions are perhaps less standard when paths are
-- used.

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans x≡y y≡z = subst (_ ≡_) y≡z x≡y

trans-refl-refl :
  {A : Set}
  (x : A) → trans (refl x) (refl x) ≡ refl x
trans-refl-refl x = subst-refl (x ≡_)

trans-sym :
  {A : Set} {x y : A} (x≡y : x ≡ y) →
  trans x≡y (sym x≡y) ≡ refl x
trans-sym =
  J (λ x y x≡y → trans x≡y (sym x≡y) ≡ refl x)
    trans-refl-refl

-- Propositions and sets.

Is-proposition : Set → Set
Is-proposition A = (x y : A) → x ≡ y

Is-set : Set → Set
Is-set A = (x y : A) → Is-proposition (x ≡ y)

-- Following Hedberg's "A coherence theorem for Martin-Löf's type
-- theory".

decidable-equality→is-set :
  {A : Set} →
  ((x y : A) → x ≡ y ⊎ (x ≡ y → ⊥)) →
  Is-set A
decidable-equality→is-set dec =
  constant⇒set (λ x y → decidable⇒constant (dec x y))
  where
  Constant : {A B : Set} → (A → B) → Set
  Constant f = ∀ x y → f x ≡ f y

  _Left-inverse-of_ : {A B : Set} → (B → A) → (A → B) → Set
  g Left-inverse-of f = ∀ x → g (f x) ≡ x

  proposition : {A : Set} →
                (f : Σ (A → A) Constant) →
                Σ _ (_Left-inverse-of (fst f)) →
                Is-proposition A
  proposition (f , constant) (g , left-inverse) x y =
    trans (sym (left-inverse x))
      (trans (cong g (constant x y)) (left-inverse y))

  left-inverse :
    {A : Set}
    (f : (x y : A) → x ≡ y → x ≡ y) →
    ∀ {x y} → Σ _ (_Left-inverse-of (f x y))
  left-inverse {A = A} f {x = x} {y = y} =
      (λ x≡y → trans x≡y (sym (f y y (refl y))))
    , J (λ x y x≡y → trans (f x y x≡y) (sym (f y y (refl y))) ≡ x≡y)
        (λ _ → trans-sym _)

  constant⇒set :
    {A : Set} →
    ((x y : A) → Σ (x ≡ y → x ≡ y) Constant) →
    Is-set A
  constant⇒set constant x y =
    proposition (constant x y)
                (left-inverse λ x y → fst (constant x y))

  decidable⇒constant :
    {A : Set} →
    A ⊎ (A → ⊥) →
    Σ (A → A) Constant
  decidable⇒constant (inj₁ x) =
    (λ _ → x) , (λ _ _ → refl x)
  decidable⇒constant (inj₂ ¬A) =
    (λ x → x) , (λ x → ⊥-elim (¬A x))

if_then_else_ : {A : Set₁} → Bool → A → A → A
if true  then x else y = x
if false then x else y = y

Bool-set : Is-set Bool
Bool-set = decidable-equality→is-set λ where
  false false → inj₁ λ _ → false
  true  true  → inj₁ λ _ → true
  false true  → inj₂ λ eq →
                  primTransp (λ i → if eq i then ⊥ else ⊤) i0 _
  true  false → inj₂ λ eq →
                  primTransp (λ i → if eq i then ⊤ else ⊥) i0 _

data ∥_∥ᴱ (A : Set) : Set where
  ∣_∣        : A → ∥ A ∥ᴱ
  @0 trivial : Is-proposition ∥ A ∥ᴱ

recᴱ : {A B : Set} → @0 Is-proposition B → (A → B) → ∥ A ∥ᴱ → B
recᴱ p f ∣ x ∣           = f x
recᴱ p f (trivial x y i) = p (recᴱ p f x) (recᴱ p f y) i

-- Following Vezzosi, Mörtberg and Abel's "Cubical Agda: A Dependently
-- Typed Programming Language with Univalence and Higher Inductive
-- Types".

data _/_ (A : Set) (R : A → A → Set) : Set where
  [_]                  : A → A / R
  []-respects-relation : (x y : A) → R x y → [ x ] ≡ [ y ]
  is-set               : Is-set (A / R)

rec :
  {A B : Set} {R : A → A → Set} →
  Is-set B →
  (f : A → B) →
  ((x y : A) → R x y → f x ≡ f y) →
  A / R → B
rec s f g [ x ]                          = f x
rec s f g ([]-respects-relation x y r i) = g x y r i
rec s f g (is-set x y p q i j)           =
  s (rec s f g x) (rec s f g y)
    (λ k → rec s f g (p k)) (λ k → rec s f g (q k)) i j

const-true : I → Bool
const-true i =
  rec
    {R = _≡_}
    Bool-set
    (λ x → x)
    (λ _ _ x≡y → x≡y)
    (is-set
       _ _
       ([]-respects-relation true true (refl true))
       (refl _)
       i i)

main : IO ⊤
main =
  putStr
    (recᴱ
       easy
       (λ where
          true  → "Success\n"
          false → "Failure\n")
       ∣ const-true i0 ∣)

-- It should be possible to mention things that are not compiled in
-- type signatures.

u₁ : Not-compiled → ⊤
u₁ _ = tt

@0 A : Set₁
A = Set

u₂ : A → ⊤
u₂ _ = tt


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

module Examples.Gcd.Euclid where

open import Calf.CostMonoid
import Calf.CostMonoids as CM

{- This file defines the parameters of the analysis of Euclid's algorithm for gcd
   and its cost recurrence relation. -}
open import Calf CM.ℕ-CostMonoid
open import Calf.Types.Nat
open import Data.Nat
open import Relation.Binary.PropositionalEquality as P
open import Induction.WellFounded
open import Induction
open import Data.Nat.Properties
open import Data.Nat.DivMod
open import Relation.Nullary.Decidable using (False)
open import Data.Nat.Induction using (<-wellFounded)
open import Data.Product
open import Agda.Builtin.Nat using (div-helper; mod-helper)
open import Relation.Binary using (Rel)
open import Relation.Unary using (Pred; _⊆′_)

mod-tp : (x y : val nat) → cmp (meta (False (y ≟ 0))) → tp pos
mod-tp x y h = Σ++ nat λ z → (U (meta (z ≡ _%_ x y {h})))

mod : cmp (
        Π nat λ x →
        Π nat λ y →
        Π (U (meta (False (y ≟ 0)))) λ h →
        F (mod-tp x y h))
mod x y h = step (F (mod-tp x y h)) 1 (ret {mod-tp x y h} (_%_  x y {h} , refl))

gcd/depth/helper : ∀ n → ((m : ℕ) → m < n → (k : ℕ) → (k > m) → ℕ) → (m : ℕ) → (m > n) → ℕ
gcd/depth/helper zero h m h' = 0
gcd/depth/helper n@(suc n') h m h' = suc (h (m % n) (m%n<n m n') n (m%n<n m n'))

gcd/i = Σ++ nat λ x → Σ++ nat λ y → U (meta (x > y))
m>n = val gcd/i

gcd/depth : m>n → ℕ
gcd/depth (x , (y , g)) = All.wfRec <-wellFounded _ (λ y → (x : ℕ) → x > y → ℕ)
  gcd/depth/helper y x g

gcd/depth/helper-ext : (x₁ : ℕ)
    {IH IH′ : WfRec _<_ (λ y₁ → (x₂ : ℕ) → x₂ > y₁ → ℕ) x₁} →
    ({y = y₁ : ℕ} (y<x : y₁ < x₁) → IH y₁ y<x ≡ IH′ y₁ y<x) →
    gcd/depth/helper x₁ IH ≡ gcd/depth/helper x₁ IH′
gcd/depth/helper-ext zero h = refl
gcd/depth/helper-ext (suc x) h =
  funext λ m → funext λ h1 → P.cong suc (
    let g = h {m % suc x} (m%n<n m x) in
    P.cong-app (P.cong-app g _) _
  )

module irr
  {a r ℓ}
  {A : Set a}
  {_<_ : Rel A r} (wf : WellFounded _<_)
  (P : Pred A ℓ) (f : WfRec _<_ P ⊆′ P)
  (f-ext : (x : A) {IH IH′ : WfRec _<_ P x} → (∀ {y} y<x → IH y y<x ≡ IH′ y y<x) → f x IH ≡ f x IH′)
  where

  some-wfRecBuilder-irrelevant : ∀ x → (q q′ : Acc _<_ x) → Some.wfRecBuilder P f x q ≡ Some.wfRecBuilder P f x q′
  some-wfRecBuilder-irrelevant = All.wfRec wf _
                                  ((λ x → (q q′ : Acc _<_ x) → Some.wfRecBuilder P f x q ≡ Some.wfRecBuilder P f x q′))
                                  ((λ { x IH (acc rs) (acc rs') → funext λ y → funext λ h → f-ext y λ {y'} h' →
                                    let g = IH y h (rs y h) (rs' y h) in
                                    P.cong-app (P.cong-app g y') h'
                                  }))

gcd/depth-unfold-zero : ∀ {x h} → gcd/depth (x , 0 , h) ≡ 0
gcd/depth-unfold-zero = refl

gcd/depth-unfold-suc : ∀ {x y h} → gcd/depth (x , suc y , h) ≡
                              suc (gcd/depth (suc y , x % suc y , m%n<n x y))
gcd/depth-unfold-suc {x} {y} {h} = P.cong suc
  ( P.subst (λ  ih →
      gcd/depth/helper (mod-helper 0 y x y) (ih) (suc y) (m%n<n x y) ≡
        gcd/depth/helper (mod-helper 0 y x y)
        (All.wfRecBuilder <-wellFounded _
        (λ y₁ → (x₁ : ℕ) → x₁ > y₁ → ℕ) gcd/depth/helper
        (mod-helper 0 y x y))
        (suc y) (m%n<n x y))
    (irr.some-wfRecBuilder-irrelevant <-wellFounded (λ y → (x : ℕ) → x > y → ℕ)
      gcd/depth/helper (gcd/depth/helper-ext) (x % suc y)
      (<-wellFounded (mod-helper 0 y x y))
      (Subrelation.accessible ≤⇒≤′
     (Data.Nat.Induction.<′-wellFounded′ (suc y)
      (mod-helper 0 y x y) (≤⇒≤′ (m%n<n x y)))))
    refl
  )

m%n<n' : ∀ m n h → _%_ m n {h} < n
m%n<n' m (suc n) h = m%n<n m n

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc n = ?


text:
module Generic where

import Category.Functor
import Category.Monad
open import Data.List using (List ; length ; replicate) renaming ([] to []L ; _∷_ to _∷L_)
open import Data.Maybe using (Maybe ; just ; nothing) renaming (setoid to MaybeEq)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Product using (_×_ ; _,_)
open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_)
open import Data.Vec.Equality using () renaming (module Equality to VecEq)
open import Data.Vec.Properties using (map-cong)
open import Function using (_∘_ ; id ; flip)
open import Function.Equality using (_⟶_)
open import Level using () renaming (zero to ℓ₀)
open import Relation.Binary using (Setoid ; module Setoid)
open import Relation.Binary.Core using (_≡_ ; refl)
open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid)
open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans ; cong₂) renaming (setoid to EqSetoid)

open Setoid using () renaming (_≈_ to _∋_≈_)
open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)

≡-to-Π : {A B : Set} → (A → B) → EqSetoid A ⟶ EqSetoid B
≡-to-Π f = record { _⟨$⟩_ = f; cong = cong f }

just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y
just-injective refl = refl

length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) ≡ n
length-replicate zero    = refl
length-replicate (suc n) = cong suc (length-replicate n)

sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n)
sequenceV []V       = just []V
sequenceV (x ∷V xs) = x >>= (λ y → (_∷V_ y) <$> sequenceV xs)

mapMV : {A B : Set} {n : ℕ} → (A → Maybe B) → Vec A n → Maybe (Vec B n)
mapMV f = sequenceV ∘ map f

mapMV-cong : {A B : Set} {f g : A → Maybe B} → f ≗ g → {n : ℕ} → mapMV {n = n} f ≗ mapMV g
mapMV-cong f≗g v = cong sequenceV (map-cong f≗g v)

mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (Maybe.just ∘ f) v ≡ just (map f v)
mapMV-purity f []V       = refl
mapMV-purity f (x ∷V xs) = cong (_<$>_ (_∷V_ (f x))) (mapMV-purity f xs)

maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (EqSetoid A) ∋ a ≈ b
maybeEq-from-≡ {a = just x}  {b = .(just x)} refl = just refl
maybeEq-from-≡ {a = nothing} {b = .nothing}  refl = nothing

maybeEq-to-≡ : {A : Set} {a b : Maybe A} → MaybeEq (EqSetoid A) ∋ a ≈ b → a ≡ b
maybeEq-to-≡ (just refl) = refl
maybeEq-to-≡ nothing     = refl

subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) →
             f ∘ subst T p ≗ subst T (cong g p) ∘ f
subst-cong T f refl _ = refl

subst-fromList : {A : Set} {x y : List A} → (p : y ≡ x) →
                 subst (Vec A) (cong length p) (fromList y) ≡ fromList x
subst-fromList refl = refl

subst-subst : {A : Set} (T : A → Set) {a b c : A} → (p : a ≡ b) → (p′ : b ≡ c) → (x : T a) →
              subst T p′ (subst T p x) ≡ subst T (trans p p′) x
subst-subst T refl p′ x = refl

toList-fromList : {A : Set} → (l : List A) → toList (fromList l) ≡ l
toList-fromList []L       = refl
toList-fromList (x ∷L xs) = cong (_∷L_ x) (toList-fromList xs)

toList-subst : {A : Set} → {n m : ℕ} (v : Vec A n) → (p : n ≡ m) →
               toList (subst (Vec A) p v) ≡ toList v
toList-subst v refl = refl

VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀
VecISetoid S = record
  { Carrier = Vec (Setoid.Carrier S)
  ; _≈_ = λ x → VecEq._≈_ S x
  ; isEquivalence = record
    { refl = VecEq.refl S _
    ; sym = VecEq.sym S
    ; trans = VecEq.trans S }
  }

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Product
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℚ using (ℚ)
open import Data.List
open import Relation.Binary.PropositionalEquality

module reachability-temp-output where

postulate f : Tensor ℚ (2 ∷ []) → Tensor ℚ (1 ∷ [])

abstract
  reachable : ∃ λ (x : Tensor ℚ (2 ∷ [])) → f x ≡ ℤ.+ 0 ℚ./ 1 ∷ []
  reachable = checkSpecification record
    { proofCache   = "/home/matthew/Code/AISEC/vehicle/proofcache.vclp"
    }

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


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

module Cubical.Algebra.Group.Higher where

open import Cubical.Core.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Unit
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude hiding (comp)
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Base
open import Cubical.Homotopy.PointedFibration
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.EilenbergMacLane1
open import Cubical.HITs.EilenbergMacLane1

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphism
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.HITs.PropositionalTruncation renaming (rec to propRec)
open import Cubical.HITs.Truncation.FromNegOne as Trunc renaming (rec to trRec)
open import Cubical.HITs.SetTruncation
open import Cubical.Functions.Surjection
open import Cubical.Functions.Embedding

import Cubical.Foundations.GroupoidLaws as GL

private
  variable
    ℓ ℓ' : Level

record HigherGroup ℓ : Type (ℓ-suc ℓ) where
  constructor highergroup
  field
    base : Pointed ℓ
    isConn : isConnected 2 (typ base)

record BGroup ℓ (n k : ℕ) : Type (ℓ-suc ℓ) where
  no-eta-equality
  constructor bgroup
  field
    base : Pointed ℓ
    isConn : isConnected (k + 1) (typ base)
    isTrun : isOfHLevel (n + k + 2) (typ base)

BGroupΣ : {ℓ : Level} (n k : ℕ) → Type (ℓ-suc ℓ)
BGroupΣ {ℓ} n k = Σ[ A ∈ Type ℓ ] A × (isConnected (k + 1) A) × (isOfHLevel (n + k + 2) A)

module _ where
  open BGroup
  η-BGroup : {n k : ℕ} {BG BH : BGroup ℓ n k}
             → (p : typ (base BG) ≡ typ (base BH))
             → (q : PathP (λ i → p i) (pt (base BG)) (pt (base BH)))
             → BG ≡ BH
  base (η-BGroup p q i) .fst = p i
  base (η-BGroup p q i) .snd = q i
  isConn (η-BGroup {k = k} {BG = BG} {BH = BH} p q i) = r i
    where
      r : PathP (λ i → isConnected (k + 1) (p i)) (isConn BG) (isConn BH)
      r = isProp→PathP (λ _ → isPropIsOfHLevel 0) (isConn BG) (isConn BH)
  isTrun (η-BGroup {n = n} {k = k} {BG = BG} {BH = BH} p q i) = s i
    where
      s : PathP (λ i → isOfHLevel (n + k + 2) (p i)) (isTrun BG) (isTrun BH)
      s = isProp→PathP (λ i → isPropIsOfHLevel (n + k + 2)) (isTrun BG) (isTrun BH)

-- morphisms

BGroupHom : {n k : ℕ} (G : BGroup ℓ n k) (H : BGroup ℓ' n k) → Type (ℓ-max ℓ ℓ')
BGroupHom G H = (BGroup.base G) →∙ (BGroup.base H)

BGroupHomΣ : {n k : ℕ} (BG : BGroupΣ {ℓ} n k) (BH : BGroupΣ {ℓ'} n k) → Type (ℓ-max ℓ ℓ')
BGroupHomΣ (base , pt , _) (base' , pt' , _) = (base , pt) →∙ (base' , pt')

isOfHLevel-BGroupHomΣ : {n k : ℕ} (BG : BGroupΣ {ℓ} n k) (BH : BGroupΣ {ℓ'} n k)
                        → isOfHLevel (n + 2) (BGroupHomΣ BG BH)
isOfHLevel-BGroupHomΣ {n = n} {k = k} BG BH = x'
  where
    z : isOfHLevel (n + k + 2) (fst BH)
    z = snd (snd (snd BH))
    z' : isOfHLevel (n + 1 + 1 + k) (fst BH)
    z' = subst (λ m → isOfHLevel m (fst BH))
               (n + k + 2 ≡⟨ sym (+-assoc n k 2) ⟩
               n + (k + 2) ≡⟨ cong (n +_) (+-comm k 2) ⟩
               n + (2 + k) ≡⟨ +-assoc n 2 k ⟩
               (n + 2) + k ≡⟨ cong (_+ k) (+-assoc n 1 1) ⟩
               n + 1 + 1 + k ∎)
               z
    x : isOfHLevel (n + 1 + 1) (BGroupHomΣ BG BH)
    x = sec∙Trunc (fst BG , fst (snd BG)) (fst (snd (snd BG))) λ _ → (fst BH , fst (snd BH)) , z'
    x' : isOfHLevel (n + 2) (BGroupHomΣ BG BH)
    x' = subst (λ m → isOfHLevel m (BGroupHomΣ BG BH)) (sym (+-assoc n 1 1)) x

BGroupIso : {n k : ℕ} (G : BGroup ℓ n k) (H : BGroup ℓ' n k) → Type (ℓ-max ℓ ℓ')
BGroupIso G H = (BGroup.base G) ≃∙ (BGroup.base H)

BGroupIdIso : {n k : ℕ} (BG : BGroup ℓ n k) → BGroupIso BG BG
BGroupIdIso BG = idEquiv∙ (BGroup.base BG)

BGroupIso→≡ : {n k : ℕ} {BG BH : BGroup ℓ n k}
                (f : BGroupIso BG BH)
                → BG ≡ BH
BGroupIso→≡ {BG = BG} {BH = BH} f = η-BGroup (ua (≃∙→≃ f)) (toPathP ((uaβ ((≃∙→≃ f)) (pt (BGroup.base BG))) ∙ f .fst .snd))

-- getters
carrier : {ℓ : Level} {n k : ℕ} (G : BGroup ℓ n k) → Pointed ℓ
carrier {k = k} BG = (Ω^ k) base
  where
    open BGroup BG

basetype : {ℓ : Level} {n k : ℕ} (BG : BGroup ℓ n k) → Type ℓ
basetype BG = typ (BGroup.base BG)

basepoint : {ℓ : Level} {n k : ℕ} (BG : BGroup ℓ n k) → basetype BG
basepoint BG = pt (BGroup.base BG)

baseΣ : {ℓ : Level} {n k : ℕ} (BG : BGroupΣ {ℓ} n k) → Σ[ A ∈ Type ℓ ] A
baseΣ (base , * , _ , _) = (base , *)

-- special cases
1BGroup : (ℓ : Level) → Type (ℓ-suc ℓ)
1BGroup ℓ = BGroup ℓ 0 1

1BGroupΣ : {ℓ : Level} → Type (ℓ-suc ℓ)
1BGroupΣ {ℓ} = BGroupΣ {ℓ} 0 1

-- first fundamental group of 1BGroups
π₁-1BGroup : {ℓ : Level} (BG : 1BGroup ℓ) → Group {ℓ}
π₁-1BGroup BG =
  makeGroup {G = (pt base) ≡ (pt base)}
            refl
            _∙_
            sym
            (isTrun (pt base) (pt base))
            GL.assoc
            (λ a → sym (GL.rUnit a))
            (λ g → sym (GL.lUnit g))
            GL.rCancel
            GL.lCancel
    where
      open BGroup BG

π₁-1BGroupΣ : {ℓ : Level} (BG : BGroupΣ {ℓ} 0 1) → Group {ℓ}
π₁-1BGroupΣ (BG , pt , conn , trunc) = π₁-1BGroup (bgroup (BG , pt) conn trunc)

-- coercions
Group→1BGroup : (G : Group {ℓ}) → 1BGroup ℓ
BGroup.base (Group→1BGroup G) .fst = EM₁ G
BGroup.base (Group→1BGroup G) .snd = embase
BGroup.isConn (Group→1BGroup G) = EM₁Connected G
BGroup.isTrun (Group→1BGroup G) = EM₁Groupoid G

-- functoriality of π₁ on 1BGroups
module _ (BG : 1BGroup ℓ) (BH : 1BGroup ℓ') where
  private
    π₁BG = π₁-1BGroup BG
    π₁BH = π₁-1BGroup BH

  π₁-1BGroup-functor : BGroupHom BG BH → GroupHom π₁BG π₁BH
  GroupHom.fun (π₁-1BGroup-functor f) g = sym (snd f) ∙∙ cong (fst f) g ∙∙ snd f
  GroupHom.isHom (π₁-1BGroup-functor f) g g' = q
    where
      f₁ = fst f
      f₂ = snd f
      f₂- = sym (snd f)
      abstract
        q = (f₂- ∙∙ cong f₁ (g ∙ g') ∙∙ f₂)
                 ≡⟨ doubleCompPath-elim' f₂- (cong f₁ (g ∙ g')) f₂ ⟩
            f₂- ∙ cong f₁ (g ∙ g') ∙ f₂
              ≡⟨ cong (λ z → (f₂- ∙ z ∙ f₂))
                      (congFunct f₁ g g') ⟩
            f₂- ∙ (cong f₁ g ∙ cong f₁ g') ∙ f₂
              ≡⟨ cong (λ z → (f₂- ∙ (cong f₁ g ∙ z) ∙ f₂))
                      (lUnit (cong f₁ g')) ⟩
            f₂- ∙ (cong f₁ g ∙ refl ∙ cong f₁ g') ∙ f₂
              ≡⟨ cong (λ z → (f₂- ∙ (cong f₁ g ∙ z ∙ cong f₁ g') ∙ f₂))
                      (sym (rCancel f₂)) ⟩
            f₂- ∙ (cong f₁ g ∙ (f₂ ∙ f₂-) ∙ cong f₁ g') ∙ f₂
              ≡⟨ cong (λ z → (f₂- ∙ (cong f₁ g ∙ z) ∙ f₂))
                      (sym (assoc _ _ _)) ⟩
            f₂- ∙ (cong f₁ g ∙ (f₂ ∙ (f₂- ∙ cong f₁ g'))) ∙ f₂
              ≡⟨ cong (λ z → (f₂- ∙ z ∙ f₂))
                      (assoc _ _ _) ⟩
            (f₂- ∙ ((cong f₁ g ∙ f₂) ∙ (f₂- ∙ cong f₁ g')) ∙ f₂)
              ≡⟨ cong (f₂- ∙_)
                      (sym (assoc _ _ _)) ⟩
            (f₂- ∙ ((cong f₁ g ∙ f₂) ∙ ((f₂- ∙ cong f₁ g') ∙ f₂)))
              ≡⟨ cong (λ z → (f₂- ∙ ((cong f₁ g ∙ f₂) ∙ z)))
                      (sym (assoc _ _ _)) ⟩
            (f₂- ∙ ((cong f₁ g ∙ f₂) ∙ (f₂- ∙ cong f₁ g' ∙ f₂)))
              ≡⟨ assoc _ _ _ ⟩
            (f₂- ∙ cong f₁ g ∙ f₂) ∙ (f₂- ∙ cong f₁ g' ∙ f₂)
              ≡⟨ cong (_∙ (f₂- ∙ cong f₁ g' ∙ f₂))
                      (sym (doubleCompPath-elim' f₂- (cong f₁ g) f₂)) ⟩
            (f₂- ∙∙ cong f₁ g ∙∙ f₂) ∙ (f₂- ∙ cong f₁ g' ∙ f₂)
              ≡⟨ cong ((f₂- ∙∙ cong f₁ g ∙∙ f₂) ∙_)
                      (sym (doubleCompPath-elim' f₂- (cong f₁ g') f₂)) ⟩
            (f₂- ∙∙ cong f₁ g ∙∙ f₂) ∙ (f₂- ∙∙ cong f₁ g' ∙∙ f₂) ∎

-- π₁ is a left inverse to EM₁
π₁EM₁≃inv : (G : Group {ℓ}) → GroupEquiv G (π₁-1BGroup (Group→1BGroup G))
GroupEquiv.eq (π₁EM₁≃inv G) = isoToEquiv (invIso (ΩEM₁Iso G))
GroupEquiv.isHom (π₁EM₁≃inv G) g g' = emloop-comp G g g'

π₁EM₁≃ : (G : Group {ℓ}) → GroupEquiv (π₁-1BGroup (Group→1BGroup G)) G
π₁EM₁≃ G = invGroupEquiv (π₁EM₁≃inv G)

-- the functorial action of EM₁ on groups
-- is a left inverse to the functorial action of π₁
-- on 1BGroups.
module _ (H : Group {ℓ}) (BG : 1BGroup ℓ') where
  private
    EM₁H = Group→1BGroup H
    π₁EM₁H = π₁-1BGroup EM₁H
    π₁BG = π₁-1BGroup BG

  -- from the EM construction it follows
  -- that there is a homomorphism H → π₁ (EM₁ H)
  H→π₁EM₁H : GroupHom H π₁EM₁H
  H→π₁EM₁H = GroupEquiv.hom (π₁EM₁≃inv H)

  -- the promised functorial left inverse
  -- split up into the three components:
  -- function, is equivalence and pointedness.
  -- pointedness component is trivial

  -- on the object level
  EM₁-functor-lInv-function : GroupHom π₁EM₁H π₁BG → basetype EM₁H → basetype BG
  EM₁-functor-lInv-function f =
    rec' H
        (BGroup.isTrun BG)
        (basepoint BG)
        (GroupHom.fun (compGroupHom H→π₁EM₁H f))
        λ g h → sym (GroupHom.isHom (compGroupHom H→π₁EM₁H f) g h)

  EM₁-functor-lInv-pointed : (f : GroupHom π₁EM₁H π₁BG)
                             → EM₁-functor-lInv-function f (basepoint EM₁H) ≡ basepoint BG
  EM₁-functor-lInv-pointed f = refl

  -- produces an equivalence proof when given a group iso
  EM₁-functor-lInv-onIso-isEquiv : (f : GroupEquiv π₁EM₁H π₁BG)
                                 → isEquiv (EM₁-functor-lInv-function (GroupEquiv.hom f))
  EM₁-functor-lInv-onIso-isEquiv f =
    isEmbedding×isSurjection→isEquiv (isEmbedding-φ , isSurjection-φ)
    where
      φ₁ : basetype EM₁H → basetype BG
      φ₁ = EM₁-functor-lInv-function (GroupEquiv.hom f)
      abstract
        isEmbedding-φ : isEmbedding φ₁
        isEmbedding-φ = reduceToBp isEmbPt
          where
            isEmb : (x y : basetype EM₁H) → Type (ℓ-max ℓ ℓ')
            isEmb x y = isEquiv (cong {x = x} {y = y} φ₁)

            isPropIsEmb : (x y : basetype EM₁H) → isProp (isEmb x y)
            isPropIsEmb x y = isPropIsEquiv (cong {x = x} {y = y} φ₁)

            f-equiv : (basepoint EM₁H ≡ basepoint EM₁H) ≃ (basepoint BG ≡ basepoint BG)
            f-equiv =  GroupEquiv.eq f
            f₁ = fst f-equiv

            γ : ⟨ H ⟩ ≃ ⟨ π₁EM₁H ⟩
            γ = GroupEquiv.eq (π₁EM₁≃inv H)
            β : ⟨ π₁EM₁H ⟩ ≃ typ (carrier BG)
            β = f-equiv
            δ : ⟨ H ⟩ ≃ typ (carrier BG)
            δ = compEquiv γ β
            p : equivFun δ ≡ (λ h → cong φ₁ (equivFun γ h))
            p = refl
            η = (λ (h : ⟨ H ⟩) → cong φ₁ (equivFun γ h))
            isEquiv-η : isEquiv η
            isEquiv-η = equivFun≡→isEquiv δ η λ _ → refl
            congφ∼f : (h : ⟨ H ⟩) → f₁ (GroupHom.fun H→π₁EM₁H h) ≡ cong φ₁ (GroupHom.fun H→π₁EM₁H h)
            congφ∼f p = refl

            isEmbPt : isEmb (basepoint EM₁H) (basepoint EM₁H)
            isEmbPt = equivCompLCancel γ (cong φ₁) isEquiv-η

            g : Unit → basetype EM₁H
            g _ = basepoint EM₁H

            isConn-g : isConnectedFun 1 g
            isConn-g = isConnectedPoint 1 (BGroup.isConn EM₁H) (basepoint EM₁H)

            reduceToBp1 : ((a : Unit) → isEmb (basepoint EM₁H) (g a))
                         → (h' : basetype EM₁H) → isEmb (basepoint EM₁H) h'
            reduceToBp1 =
              Iso.inv (elim.isIsoPrecompose g
                                            1
                                            (λ h' → (isEmb (basepoint EM₁H) h') , isPropIsEmb (basepoint EM₁H) h')
                                            isConn-g)
            reduceToBp1' : isEmb (basepoint EM₁H) (basepoint EM₁H)
                         → (h' : basetype EM₁H) → isEmb (basepoint EM₁H) h'
            reduceToBp1' p = reduceToBp1 λ _ → p

            reduceToBp2 : (h' : basetype EM₁H) → isEmb (basepoint EM₁H) h'
                          → ((a : Unit) → isEmb (g a) h') → (h : basetype EM₁H) → isEmb h h'
            reduceToBp2 h' p =
              Iso.inv (elim.isIsoPrecompose g
                                            1
                                            (λ h → (isEmb h h') , (isPropIsEmb h h'))
                                            isConn-g)
            reduceToBp2' : ((h' : basetype EM₁H) → isEmb (basepoint EM₁H) h')
                           → (h h' : basetype EM₁H) → isEmb h h'
            reduceToBp2' Q h h' = reduceToBp2 h' (Q h') (λ _ → Q h') h

            reduceToBp : isEmb (basepoint EM₁H) (basepoint EM₁H) → (h h' : basetype EM₁H) → isEmb h h'
            reduceToBp p = reduceToBp2' (reduceToBp1' p)

        isSurjection-φ : isSurjection φ₁
        isSurjection-φ g = propTruncΣ← (λ x → φ₁ x ≡ g) ∣ basepoint EM₁H , fst r ∣
          where
            r : isContr ∥ φ₁ (basepoint EM₁H) ≡ g ∥
            r = isContrRespectEquiv (invEquiv propTrunc≃Trunc1)
                                    (isConnectedPath 1
                                                     (BGroup.isConn BG)
                                                     (φ₁ (basepoint EM₁H))
                                                     g)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
module Type.Properties.MereProposition {ℓ ℓₑ} where

import      Lvl
open import Lang.Instance
open import Structure.Setoid
open import Type

-- A type is a mere proposition type when there is at most one inhabitant (there is at most one object with this type).
-- In other words: If there is an inhabitant of type T, it is unique (essentially only allowing empty or singleton types, but this is not provable (excluded middöe)).
-- Also called:
-- • "Irrelevance" / "Irrelevancy" / "Proof irrelevance" (in the context of proofs).
--   A proof of the proposition T is unique (using equality to determine uniqueness).
-- • "isProp" / "h-proposition" / "is of h-level 1" / "a mere proposition" (in homotopy type theory).
--   Classically, when MereProposition(T), T is either empty or a singleton (which in the context of proofs corresponds to types isomorphic to ⊥ or ⊤).
-- • "subsingleton" (in set theory)
--   When a type and its inhabitants is interpreted as a set and its elements.
-- • "subterminal object" (in category theory).
module _ (T : Type{ℓ}) ⦃ _ : Equiv{ℓₑ}(T) ⦄ where
  record MereProposition : Type{ℓ Lvl.⊔ ℓₑ} where
    constructor intro
    field uniqueness : ∀{x y : T} → (x ≡ y)
  uniqueness = inst-fn MereProposition.uniqueness

-- TODO: Consider using unicode ◐○●⧭⦵⦳


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module SelectSort.Correctness.Permutation {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_ ) where

open import Data.List
open import Data.Product
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A
open import Size
open import SList
open import SList.Properties
open import SelectSort _≤_ tot≤

lemma-select∼ : {ι : Size}(x : A) → (xs : SList A {ι}) → unsize A (x ∙ xs) ∼ unsize A (proj₁ (select x xs) ∙ proj₂ (select x xs))
lemma-select∼ x snil = ∼x /head /head ∼[]
lemma-select∼ x (y ∙ ys)
    with tot≤ x y
... | inj₁ x≤y = ∼x (/tail /head) (/tail /head) (lemma-select∼ x ys)
... | inj₂ y≤x = ∼x /head (/tail /head) (lemma-select∼ y ys)

lemma-selectSort∼ : {ι : Size}(xs : SList A {ι}) → unsize A xs ∼ unsize A (selectSort xs)
lemma-selectSort∼ snil = ∼[]
lemma-selectSort∼ (x ∙ xs) = trans∼ (lemma-select∼ x xs) (∼x /head /head (lemma-selectSort∼ (proj₂ (select x xs))))

theorem-selectSort∼ : (xs : List A) → xs ∼ unsize A (selectSort (size A xs))
theorem-selectSort∼ xs = trans∼ (lemma-unsize-size A xs) (lemma-selectSort∼ (size A xs))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
import      Structure.Logic.Classical.NaturalDeduction
-- TODO: Seems like Constructive does not work, but why?

module Structure.Logic.Constructive.Syntax.Algebra {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicalLogic : _ ⦄ where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicalLogic)

import      Lvl
open import Syntax.Function
open import Type

-- Transitivitity through an operation on proofs
record Transitivable{ℓ}{T : Type{ℓ}}(_▫_ : T → T → Formula) : Type{ℓₘₗ Lvl.⊔ ℓₒ Lvl.⊔ ℓ} where
  field
    _🝖_ : ∀{a b c} → Proof(a ▫ b) → Proof(b ▫ c) → Proof(a ▫ c)
open Transitivable ⦃ ... ⦄ public

Transitivity-to-Transitivable : ∀{_▫_ : Domain → Domain → Formula} → Proof(∀ₗ(a ↦ ∀ₗ(b ↦ ∀ₗ(c ↦ (a ▫ b)∧(b ▫ c) ⟶ (a ▫ c))))) → Transitivable(_▫_)
_🝖_ ⦃ Transitivity-to-Transitivable proof ⦄ {a}{b}{c} ab bc =
  ([→].elim
    ([∀].elim ([∀].elim ([∀].elim proof {a}){b}){c})
    ([∧].intro ab bc)
  )

instance
  [⟶]-transitivable : Transitivable(_⟶_)
  _🝖_ ⦃ [⟶]-transitivable ⦄ = [→].transitivity

instance
  [⟷]-transitivable : Transitivable(_⟷_)
  _🝖_ ⦃ [⟷]-transitivable ⦄ = [↔].transitivity


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Hom where

-- The Hom Functor from C.op × C to Setoids,
-- the two 1-argument version fixing one object
-- and some notation for the version where the category must be made explicit

open import Data.Product
open import Function using () renaming (_∘_ to _∙_)

open import Categories.Category
open import Categories.Functor hiding (id)
open import Categories.Functor.Bifunctor
open import Categories.Category.Instance.Setoids
import Categories.Morphism.Reasoning as MR

open import Relation.Binary using (Setoid)

module Hom {o ℓ e} (C : Category o ℓ e) where
  open Category C
  open MR C

  Hom[-,-] : Bifunctor (Category.op C) C (Setoids ℓ e)
  Hom[-,-] = record
    { F₀           = F₀′
    ; F₁           = λ where
      (f , g) → record
        { _⟨$⟩_ = λ h → g ∘ h ∘ f
        ; cong  = ∘-resp-≈ʳ ∙ ∘-resp-≈ˡ
        }
    ; identity     = identity′
    ; homomorphism = homomorphism′
    ; F-resp-≈     = F-resp-≈′
    }
    where F₀′ : Obj × Obj → Setoid ℓ e
          F₀′ (A , B) = hom-setoid {A} {B}
          open HomReasoning

          identity′ : {A : Obj × Obj} {x y : uncurry _⇒_ A} → x ≈ y → id ∘ x ∘ id ≈ y
          identity′ {A} {x} {y} x≈y = begin
            id ∘ x ∘ id ≈⟨ identityˡ ⟩
            x ∘ id      ≈⟨ identityʳ ⟩
            x           ≈⟨ x≈y ⟩
            y           ∎

          homomorphism′ : ∀ {X Y Z : Σ Obj (λ x → Obj)}
                            {f : proj₁ Y ⇒ proj₁ X × proj₂ X ⇒ proj₂ Y}
                            {g : proj₁ Z ⇒ proj₁ Y × proj₂ Y ⇒ proj₂ Z}
                            {x y : proj₁ X ⇒ proj₂ X} →
                            x ≈ y →
                            (proj₂ g ∘ proj₂ f) ∘ x ∘ proj₁ f ∘ proj₁ g ≈
                            proj₂ g ∘ (proj₂ f ∘ y ∘ proj₁ f) ∘ proj₁ g
          homomorphism′ {f = f₁ , f₂} {g₁ , g₂} {x} {y} x≈y = begin
            (g₂ ∘ f₂) ∘ x ∘ f₁ ∘ g₁   ≈˘⟨ refl⟩∘⟨ assoc ⟩
            (g₂ ∘ f₂) ∘ (x ∘ f₁) ∘ g₁ ≈⟨ pullʳ (pullˡ (∘-resp-≈ʳ (∘-resp-≈ˡ x≈y))) ⟩
            g₂ ∘ (f₂ ∘ y ∘ f₁) ∘ g₁   ∎

          F-resp-≈′ : ∀ {A B : Σ Obj (λ x → Obj)}
                        {f g : Σ (proj₁ B ⇒ proj₁ A) (λ x → proj₂ A ⇒ proj₂ B)} →
                        Σ (proj₁ f ≈ proj₁ g) (λ x → proj₂ f ≈ proj₂ g) →
                        {x y : proj₁ A ⇒ proj₂ A} →
                        x ≈ y → proj₂ f ∘ x ∘ proj₁ f ≈ proj₂ g ∘ y ∘ proj₁ g
          F-resp-≈′ {f = f₁ , f₂} {g₁ , g₂} (f₁≈g₁ , f₂≈g₂) {x} {y} x≈y = begin
            f₂ ∘ x ∘ f₁ ≈⟨ f₂≈g₂ ⟩∘⟨ x≈y ⟩∘⟨ f₁≈g₁ ⟩
            g₂ ∘ y ∘ g₁ ∎

  open Functor Hom[-,-]
  open Equiv
  open HomReasoning

  Hom[_,-] : Obj → Functor C (Setoids ℓ e)
  Hom[_,-] = appˡ Hom[-,-]

  Hom[-,_] : Obj → Contravariant C (Setoids ℓ e)
  Hom[-,_] = appʳ Hom[-,-]

-- Notation for when the ambient Category must be specified explicitly.
module _ {o ℓ e} (C : Category o ℓ e) where
  open Category C
  open Hom C

  Hom[_][-,-] : Bifunctor (Category.op C) C (Setoids ℓ e)
  Hom[_][-,-] = Hom[-,-]

  Hom[_][_,-] : Obj → Functor C (Setoids ℓ e)
  Hom[_][_,-] B = Hom[ B ,-]

  Hom[_][-,_] : Obj → Contravariant C (Setoids ℓ e)
  Hom[_][-,_] B = Hom[-, B ]

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


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

module Quasigroup where

open import Quasigroup.Bundles public
open import Quasigroup.Definitions public
open import Quasigroup.Structures public


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.VoteData as VoteData
open import LibraBFT.Impl.OBM.Logging.Logging
import      LibraBFT.Impl.Types.LedgerInfoWithSignatures    as LedgerInfoWithSignatures
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Hash
import      Util.KVMap                                      as Map
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                     using (String)

module LibraBFT.Impl.Consensus.ConsensusTypes.QuorumCert where

certificateForGenesisFromLedgerInfo : LedgerInfo → HashValue → QuorumCert
certificateForGenesisFromLedgerInfo ledgerInfo genesisId =
  let ancestor = BlockInfo∙new
                 (ledgerInfo ^∙ liEpoch + 1)
                 0
                 genesisId
                 (ledgerInfo ^∙ liTransactionAccumulatorHash)
                 (ledgerInfo ^∙ liVersion)
               --(ledgerInfo ^∙ liTimestamp)
                 nothing
      voteData = VoteData.new ancestor ancestor
      li       = LedgerInfo∙new ancestor (hashVD voteData)
   in QuorumCert∙new
      voteData
      (LedgerInfoWithSignatures∙new li Map.empty)

verify : QuorumCert → ValidatorVerifier → Either ErrLog Unit
verify self validator = do
  let voteHash = hashVD (self ^∙ qcVoteData)
  lcheck (self ^∙ qcSignedLedgerInfo ∙ liwsLedgerInfo ∙ liConsensusDataHash == voteHash)
         (here' ("Quorum Cert's hash mismatch LedgerInfo" ∷ []))
  if (self ^∙ qcCertifiedBlock ∙ biRound == 0)
    -- TODO-?: It would be nice not to require the parens around the do block
    then (do
      lcheck (self ^∙ qcParentBlock == self ^∙ qcCertifiedBlock)
             (here' ("Genesis QC has inconsistent parent block with certified block" ∷ []))
      lcheck (self ^∙ qcCertifiedBlock == self ^∙ qcLedgerInfo ∙ liwsLedgerInfo ∙ liCommitInfo)
             (here' ("Genesis QC has inconsistent commit block with certified block" ∷ []))
      lcheck (Map.kvm-size (self ^∙ qcLedgerInfo ∙ liwsSignatures) == 0)
             (here' ("Genesis QC should not carry signatures" ∷ []))
      )
    else do
      withErrCtx'
        ("fail to verify QuorumCert" ∷ [])
        (LedgerInfoWithSignatures.verifySignatures (self ^∙ qcLedgerInfo) validator)
      VoteData.verify (self ^∙ qcVoteData)
 where
  here' : List String → List String
  here' t = "QuorumCert" ∷ "verify" {- ∷ lsQC self-} ∷ t


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

{-

This file defines

deltaIntSec : ∀ b → toInt (fromInt b) ≡ b
succPred : ∀ n → succ (pred n) ≡ n
predSucc : ∀ n → pred (succ n) ≡ n

and proved DeltaInt ≡ DeltaInt by the above functions

succPredEq : DeltaInt ≡ DeltaInt

along with some interval-relevant lemmas

cancelDiamond  : ∀ a b i → cancel a b i ≡ cancel (suc a) (suc b) i
cancelTriangle : ∀ a b i → a ⊖ b ≡ cancel a b i

we also have DeltaInt ≡ Int proof

DeltaInt≡Int : DeltaInt ≡ Int

and we transported some proofs from Int to DeltaInt

discreteDeltaInt : Discrete DeltaInt
isSetDeltaInt : isSet DeltaInt

-}

module Cubical.HITs.Ints.DeltaInt.Properties where

open import Cubical.Foundations.Everything
open import Cubical.Data.Nat hiding (zero)
open import Cubical.Data.Int hiding (abs; sgn; _+_)
open import Cubical.HITs.Ints.DeltaInt.Base
open import Cubical.Relation.Nullary using (Discrete)

deltaIntSec : ∀ b → toInt (fromInt b) ≡ b
deltaIntSec (pos n) = refl
deltaIntSec (negsuc n) = refl

cancelDiamond : ∀ a b i → cancel a b i ≡ cancel (suc a) (suc b) i
cancelDiamond a b i j = hcomp (λ k → λ
  { (i = i0) → cancel a b j
  ; (i = i1) → cancel (suc a) (suc b) (j ∧ k)
  ; (j = i0) → cancel a b i
  ; (j = i1) → cancel (suc a) (suc b) (i ∧ k)
  }) (cancel a b (i ∨ j))

cancelTriangle : ∀ a b i → a ⊖ b ≡ cancel a b i
cancelTriangle a b i j = hcomp (λ k → λ
  { (i = i0) → a ⊖ b
  ; (j = i0) → a ⊖ b
  ; (j = i1) → cancel a b (i ∧ k)
  }) (a ⊖ b)

deltaIntRet : ∀ a → fromInt (toInt a) ≡ a
deltaIntRet (x ⊖ 0) = refl
deltaIntRet (0 ⊖ suc y) = refl
deltaIntRet (suc x ⊖ suc y) = deltaIntRet (x ⊖ y) ∙ cancel x y
deltaIntRet (cancel a 0 i) = cancelTriangle a 0 i
deltaIntRet (cancel 0 (suc b) i) = cancelTriangle 0 (suc b) i
deltaIntRet (cancel (suc a) (suc b) i) = deltaIntRet (cancel a b i) ∙ cancelDiamond a b i

DeltaInt≡Int : DeltaInt ≡ Int
DeltaInt≡Int = isoToPath (iso toInt fromInt deltaIntSec deltaIntRet)

discreteDeltaInt : Discrete DeltaInt
discreteDeltaInt = subst Discrete (sym DeltaInt≡Int) discreteInt

isSetDeltaInt : isSet DeltaInt
isSetDeltaInt = subst isSet (sym DeltaInt≡Int) isSetInt

succPred : ∀ n → succ (pred n) ≡ n
succPred (x ⊖ y) i = cancel x y (~ i)
-- cancel (suc a) (suc b) i ≡ cancel a b i
succPred (cancel a b i) = sym (cancelDiamond a b i)

predSucc : ∀ n → pred (succ n) ≡ n
predSucc (x ⊖ y) = succPred (x ⊖ y)
predSucc (cancel a b i) = succPred (cancel a b i)

succPredEq : DeltaInt ≡ DeltaInt
succPredEq = isoToPath (iso succ pred succPred predSucc)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Andreas, 2017-03-08
-- Impredicative data types are incompatible with structural recursion
-- (Coquand, Pattern Matching with Dependent Types, 1992)

{-# OPTIONS --type-in-type #-}

data ⊥ : Set where

-- An impredicative data type

data D : Set where
  c : (f : (A : Set) → A → A) → D

-- Structural recursion with  f args < c f  is no longer valid.
-- We should not be able to demonstrated that D is empty.

empty : D → ⊥
empty (c f) = empty (f D (c f))

-- This gets us to absurdity quickly:

inhabited : D
inhabited = c λ A x → x

absurd : ⊥
absurd = empty inhabited


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
{-# OPTIONS --allow-unsolved-metas #-}
open import Optics.All
open import LibraBFT.Lemmas
open import LibraBFT.Prelude
open import LibraBFT.Base.PKCS

open import LibraBFT.Impl.Consensus.Types
open import LibraBFT.Impl.NetworkMsg
open import LibraBFT.Impl.Util.Crypto
open import LibraBFT.Impl.Properties.Aux

open import LibraBFT.Concrete.System impl-sps-avp
open import LibraBFT.Concrete.System.Parameters
import      LibraBFT.Concrete.Properties.VotesOnce as VO

open import LibraBFT.Yasm.AvailableEpochs
open import LibraBFT.Yasm.Base
open import LibraBFT.Yasm.System     ConcSysParms
open import LibraBFT.Yasm.Properties ConcSysParms
open        Structural impl-sps-avp

open import LibraBFT.Concrete.Obligations

-- In this module, we (will) prove the two implementation obligations for the VotesOnce rule.  Note
-- that it is not yet 100% clear that the obligations are the best definitions to use.  See comments
-- in Concrete.VotesOnce.  We will want to prove these obligations for the fake/simple
-- implementation (or some variant on it) and streamline the proof before we proceed to tacke more
-- ambitious properties.

module LibraBFT.Impl.Properties.VotesOnce where

  postulate  -- TODO-3 : prove
    vo₁ : VO.ImplObligation₁
    vo₂ : VO.ImplObligation₂