text:
data Unit : Set where
  unit : Unit

P : Unit → Set
P unit = Unit

postulate
  Q : (u : Unit) → P u → Set

variable
  u : Unit
  p : P u

postulate
  q : P u → Q u p

q' : (u : Unit) (p : P u) → P u → Q u p
q' u p = q {u} {p}

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

{-# BUILTIN NATURAL ℕ #-}

infixl 6 _+_
infix  6 _∸_

_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero  = m
zero  ∸ suc n = zero
suc m ∸ suc n = m ∸ n

should-be-rejected : ℕ
should-be-rejected = 1 + 0 ∸ 1


text:
-- {-# OPTIONS -v term:20 #-}
-- Andreas, 2011-04-19 (Agda list post by Leonard Rodriguez)
module TerminationSubExpression where

infixr 3 _⇨_
data Type : Set where
 int   : Type
 _⇨_   : Type → Type → Type

test : Type → Type
test int = int
test (φ ⇨ int) = test φ
test (φ ⇨ (φ′ ⇨ φ″))  = test (φ′ ⇨ φ″)
-- this should terminate since rec. call on subterm

test' : Type → Type
test' int = int
test' (φ ⇨ int) = test' φ
test' (φ ⇨ φ′)  = test' φ′

ok : Type → Type
ok int = int
ok (φ ⇨ φ′) with φ′
... | int = ok φ
... | (φ″ ⇨ φ‴) = ok (φ″ ⇨ φ‴)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

open import Sets.EquivalenceRelations
open import Setoids.Setoids
open import Functions.Definition
open import Groups.Definition
open import Groups.Homomorphisms.Definition
open import Groups.Subgroups.Definition
open import Groups.Subgroups.Normal.Definition

module Groups.Cosets {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) {c : _} {pred : A → Set c} (subgrp : Subgroup G pred) where

open Equivalence (Setoid.eq S)
open import Groups.Lemmas G
open Group G
open Subgroup subgrp

cosetSetoid : Setoid A
Setoid._∼_ cosetSetoid g h = pred ((Group.inverse G h) + g)
Equivalence.reflexive (Setoid.eq cosetSetoid) = isSubset (symmetric (Group.invLeft G)) containsIdentity
Equivalence.symmetric (Setoid.eq cosetSetoid) yx = isSubset (transitive invContravariant (+WellDefined reflexive invInv)) (closedUnderInverse yx)
Equivalence.transitive (Setoid.eq cosetSetoid) yx zy = isSubset (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) reflexive)) (closedUnderPlus zy yx)

cosetGroup : normalSubgroup G subgrp → Group cosetSetoid _+_
Group.+WellDefined (cosetGroup norm) {m} {n} {x} {y} m=x n=y = ans
  where
    t : pred (inverse y + n)
    t = n=y
    u : pred (inverse x + m)
    u = m=x
    v : pred (m + inverse x)
    v = isSubset (+WellDefined reflexive (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight))) (norm u)
    ans' : pred ((inverse y) + ((inverse x + m) + inverse (inverse y)))
    ans' = norm u
    ans'' : pred ((inverse y) + ((inverse x + m) + y))
    ans'' = isSubset (+WellDefined reflexive (+WellDefined reflexive (invTwice y))) ans'
    ans : pred (inverse (x + y) + (m + n))
    ans = isSubset (transitive (transitive +Associative (transitive (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight))) +Associative)) reflexive) (symmetric +Associative))) (symmetric (+WellDefined invContravariant reflexive))) (closedUnderPlus ans'' t)
Group.0G (cosetGroup norm) = 0G
Group.inverse (cosetGroup norm) = inverse
Group.+Associative (cosetGroup norm) {a} {b} {c} = isSubset (symmetric (transitive (+WellDefined (inverseWellDefined (symmetric +Associative)) reflexive) (invLeft {a + (b + c)}))) containsIdentity
Group.identRight (cosetGroup norm) = isSubset (symmetric (transitive +Associative (transitive (+WellDefined invLeft reflexive) identRight))) containsIdentity
Group.identLeft (cosetGroup norm) = isSubset (symmetric (transitive (+WellDefined reflexive identLeft) invLeft)) containsIdentity
Group.invLeft (cosetGroup norm) = isSubset (symmetric (transitive (+WellDefined reflexive invLeft) invLeft)) containsIdentity
Group.invRight (cosetGroup norm) = isSubset (symmetric (transitive (+WellDefined reflexive invRight) invLeft)) containsIdentity

cosetGroupHom : (norm : normalSubgroup G subgrp) → GroupHom G (cosetGroup norm) id
GroupHom.groupHom (cosetGroupHom norm) = isSubset (symmetric (transitive (+WellDefined invContravariant reflexive) (transitive +Associative (transitive (+WellDefined (transitive (symmetric +Associative) (+WellDefined reflexive invLeft)) reflexive) (transitive (+WellDefined identRight reflexive) invLeft))))) (Subgroup.containsIdentity subgrp)
GroupHom.wellDefined (cosetGroupHom norm) {x} {y} x=y = isSubset (symmetric (transitive (+WellDefined reflexive x=y) invLeft)) (Subgroup.containsIdentity subgrp)


text:
{-# BUILTIN NATURAL ℕ #-}

module the-naturals where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

infixl 6  _+_  _∸_
infixl 7  _*_

-- the naturals
data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

-- addition
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

-- multiplication
_*_ : ℕ → ℕ → ℕ
zero    * n  =  zero
(suc m) * n  =  n + (m * n)

-- monus ( subtraction for the naturals )
_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n


text:
module Category.Functor.Arr where
open import Agda.Primitive using (_⊔_)
open import Category.Functor     using (RawFunctor    ; module RawFunctor    )
open import Category.Applicative using (RawApplicative; module RawApplicative)
open import Function using (_∘_)
open import Category.Functor.Lawful
open import Relation.Binary.PropositionalEquality using (refl)

Arr : ∀ {l₁ l₂} → Set l₁ → Set l₂ → Set (l₁ ⊔ l₂)
Arr A B = A → B

arrFunctor : ∀ {l₁ l₂} {B : Set l₁} → RawFunctor (Arr {l₁} {l₂} B)
arrFunctor = record { _<$>_ = λ z z₁ x → z (z₁ x) } -- auto-found

arrLawfulFunctor : ∀ {l₁ l₂} {B : Set l₁} → LawfulFunctorImp (arrFunctor {l₁} {l₂} {B})
arrLawfulFunctor = record
  { <$>-identity = refl
  ; <$>-compose  = refl
  }

arrApplicative : ∀ {l₁} {B : Set l₁} → RawApplicative (Arr {l₁} {l₁} B)
arrApplicative = record { pure = λ z x → z ; _⊛_ = λ z z₁ x → z x (z₁ x) } -- auto-found

arrLawfulApplicative : ∀ {l₁} {B : Set l₁} → LawfulApplicativeImp (arrApplicative {l₁} {B})
arrLawfulApplicative = record
  { ⊛-identity = refl
  ; ⊛-homomorphism = refl
  ; ⊛-interchange = refl
  ; ⊛-composition = refl
  }

max_stars_repo_name: crisoagf/agda-optics

max_issues_repo_name: crisoagf/agda-optics

max_forks_repo_name: crisoagf/agda-optics


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Universe levels
------------------------------------------------------------------------

module Level where

-- Levels.

open import Agda.Primitive public
  using    (Level; _⊔_)
  renaming (lzero to zero; lsuc to suc)

-- Lifting.

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

open Lift public


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

open import lib.Basics
open import lib.NConnected
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Empty
open import lib.types.Group
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Paths
open import lib.types.Sigma
open import lib.types.Truncation
open import lib.cubical.Square

module lib.types.LoopSpace where

module _ {i} where

  ⊙Ω : Ptd i → Ptd i
  ⊙Ω (A , a) = ⊙[ (a == a) , idp ]

  Ω : Ptd i → Type i
  Ω = fst ∘ ⊙Ω

  ⊙Ω^ : (n : ℕ) → Ptd i → Ptd i
  ⊙Ω^ O X = X
  ⊙Ω^ (S n) X = ⊙Ω (⊙Ω^ n X)

  Ω^ : (n : ℕ) → Ptd i → Type i
  Ω^ n X = fst (⊙Ω^ n X)

idp^ : ∀ {i} (n : ℕ) {X : Ptd i} → Ω^ n X
idp^ n {X} = snd (⊙Ω^ n X)

{- for n ≥ 1, we have a group structure on the loop space -}
module _ {i} where
  !^ : (n : ℕ) (t : n ≠ O) {X : Ptd i} → Ω^ n X → Ω^ n X
  !^ O t = ⊥-rec (t idp)
  !^ (S n) _ = !

  conc^ : (n : ℕ) (t : n ≠ O) {X : Ptd i} → Ω^ n X → Ω^ n X → Ω^ n X
  conc^ O t = ⊥-rec (t idp)
  conc^ (S n) _ = _∙_

{- ap and ap2 for pointed functions -}

private
  pt-lemma : ∀ {i} {A : Type i} {x y : A} (p : x == y)
    → ! p ∙ (idp ∙' p) == idp
  pt-lemma idp = idp

⊙ap : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → fst (X ⊙→ Y) → fst (⊙Ω X ⊙→ ⊙Ω Y)
⊙ap (f , fpt) = ((λ p → ! fpt ∙ ap f p ∙' fpt) , pt-lemma fpt)

⊙ap2 : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → fst (X ⊙× Y ⊙→ Z) → fst (⊙Ω X ⊙× ⊙Ω Y ⊙→ ⊙Ω Z)
⊙ap2 (f , fpt) = ((λ {(p , q) → ! fpt ∙ ap2 (curry f) p q ∙' fpt}) ,
                  pt-lemma fpt)

⊙ap-∘ : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
  → ⊙ap (g ⊙∘ f) == ⊙ap g ⊙∘ ⊙ap f
⊙ap-∘ (g , idp) (f , idp) = ⊙λ= (λ p → ap-∘ g f p) idp

⊙ap-idf : ∀ {i} {X : Ptd i} → ⊙ap (⊙idf X) == ⊙idf _
⊙ap-idf = ⊙λ= ap-idf idp

⊙ap2-fst : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → ⊙ap2 {X = X} {Y = Y} ⊙fst == ⊙fst
⊙ap2-fst = ⊙λ= (uncurry ap2-fst) idp

⊙ap2-snd : ∀ {i j} {X : Ptd i} {Y : Ptd j}
  → ⊙ap2 {X = X} {Y = Y} ⊙snd == ⊙snd
⊙ap2-snd = ⊙λ= (uncurry ap2-snd) idp

⊙ap-ap2 : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (G : fst (Z ⊙→ W)) (F : fst (X ⊙× Y ⊙→ Z))
  → ⊙ap G ⊙∘ ⊙ap2 F == ⊙ap2 (G ⊙∘ F)
⊙ap-ap2 (g , idp) (f , idp) =
  ⊙λ= (uncurry (ap-ap2 g (curry f))) idp

⊙ap2-ap : ∀ {i j k l m}
  {X : Ptd i} {Y : Ptd j} {U : Ptd k} {V : Ptd l} {Z : Ptd m}
  (G : fst ((U ⊙× V) ⊙→ Z)) (F₁ : fst (X ⊙→ U)) (F₂ : fst (Y ⊙→ V))
  → ⊙ap2 G ⊙∘ pair⊙→ (⊙ap F₁) (⊙ap F₂) == ⊙ap2 (G ⊙∘ pair⊙→ F₁ F₂)
⊙ap2-ap (g , idp) (f₁ , idp) (f₂ , idp) =
  ⊙λ= (λ {(p , q) → ap2-ap-l (curry g) f₁ p (ap f₂ q)
                  ∙ ap2-ap-r (λ x v → g (f₁ x , v)) f₂ p q})
      idp

⊙ap2-diag : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : fst (X ⊙× X ⊙→ Y))
  → ⊙ap2 F ⊙∘ ⊙diag == ⊙ap (F ⊙∘ ⊙diag)
⊙ap2-diag (f , idp) = ⊙λ= (ap2-diag (curry f)) idp

{- ap and ap2 for higher loop spaces -}

ap^ : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → fst (X ⊙→ Y) → fst (⊙Ω^ n X ⊙→ ⊙Ω^ n Y)
ap^ O F = F
ap^ (S n) F = ⊙ap (ap^ n F)

ap2^ : ∀ {i j k} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → fst ((X ⊙× Y) ⊙→ Z)
  → fst ((⊙Ω^ n X ⊙× ⊙Ω^ n Y) ⊙→ ⊙Ω^ n Z)
ap2^ O F = F
ap2^ (S n) F = ⊙ap2 (ap2^ n F)

ap^-idf : ∀ {i} (n : ℕ) {X : Ptd i} → ap^ n (⊙idf X) == ⊙idf _
ap^-idf O = idp
ap^-idf (S n) = ap ⊙ap (ap^-idf n) ∙ ⊙ap-idf

ap^-ap2^ : ∀ {i j k l} (n : ℕ) {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (G : fst (Z ⊙→ W)) (F : fst ((X ⊙× Y) ⊙→ Z))
  → ap^ n G ⊙∘ ap2^ n F == ap2^ n (G ⊙∘ F)
ap^-ap2^ O G F = idp
ap^-ap2^ (S n) G F = ⊙ap-ap2 (ap^ n G) (ap2^ n F) ∙ ap ⊙ap2 (ap^-ap2^ n G F)

ap2^-fst : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → ap2^ n {X} {Y} ⊙fst == ⊙fst
ap2^-fst O = idp
ap2^-fst (S n) = ap ⊙ap2 (ap2^-fst n) ∙ ⊙ap2-fst

ap2^-snd : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  → ap2^ n {X} {Y} ⊙snd == ⊙snd
ap2^-snd O = idp
ap2^-snd (S n) = ap ⊙ap2 (ap2^-snd n) ∙ ⊙ap2-snd

ap2^-ap^ : ∀ {i j k l m} (n : ℕ)
  {X : Ptd i} {Y : Ptd j} {U : Ptd k} {V : Ptd l} {Z : Ptd m}
  (G : fst ((U ⊙× V) ⊙→ Z)) (F₁ : fst (X ⊙→ U)) (F₂ : fst (Y ⊙→ V))
  → ap2^ n G ⊙∘ pair⊙→ (ap^ n F₁) (ap^ n F₂) == ap2^ n (G ⊙∘ pair⊙→ F₁ F₂)
ap2^-ap^ O G F₁ F₂ = idp
ap2^-ap^ (S n) G F₁ F₂ =
  ⊙ap2-ap (ap2^ n G) (ap^ n F₁) (ap^ n F₂) ∙ ap ⊙ap2 (ap2^-ap^ n G F₁ F₂)

ap2^-diag : ∀ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j} (F : fst (X ⊙× X ⊙→ Y))
  → ap2^ n F ⊙∘ ⊙diag == ap^ n (F ⊙∘ ⊙diag)
ap2^-diag O F = idp
ap2^-diag (S n) F = ⊙ap2-diag (ap2^ n F) ∙ ap ⊙ap (ap2^-diag n F)

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

  {- Prove these as lemmas now
   - so we don't have to deal with the n = O case later -}

  conc^-unit-l : (n : ℕ) (t : n ≠ O) (q : Ω^ n X)
    → (conc^ n t (idp^ n) q) == q
  conc^-unit-l O t _ = ⊥-rec (t idp)
  conc^-unit-l (S n) _ _ = idp

  conc^-unit-r : (n : ℕ) (t : n ≠ O) (q : Ω^ n X)
    → (conc^ n t q (idp^ n)) == q
  conc^-unit-r O t = ⊥-rec (t idp)
  conc^-unit-r (S n) _ = ∙-unit-r

  conc^-assoc : (n : ℕ) (t : n ≠ O) (p q r : Ω^ n X)
    → conc^ n t (conc^ n t p q) r == conc^ n t p (conc^ n t q r)
  conc^-assoc O t = ⊥-rec (t idp)
  conc^-assoc (S n) _ = ∙-assoc

  !^-inv-l : (n : ℕ) (t : n ≠ O) (p : Ω^ n X)
    → conc^ n t (!^ n t p) p == idp^ n
  !^-inv-l O t = ⊥-rec (t idp)
  !^-inv-l (S n) _ = !-inv-l

  !^-inv-r : (n : ℕ) (t : n ≠ O) (p : Ω^ n X)
    → conc^ n t p (!^ n t p) == idp^ n
  !^-inv-r O t = ⊥-rec (t idp)
  !^-inv-r (S n) _ = !-inv-r

abstract
  ap^-conc^ : ∀ {i j} (n : ℕ) (t : n ≠ O)
    {X : Ptd i} {Y : Ptd j} (F : fst (X ⊙→ Y)) (p q : Ω^ n X)
    → fst (ap^ n F) (conc^ n t p q)
      == conc^ n t (fst (ap^ n F) p) (fst (ap^ n F) q)
  ap^-conc^ O t _ _ _ = ⊥-rec (t idp)
  ap^-conc^ (S n) _ {X = X} {Y = Y} F p q =
    ! gpt ∙ ap g (p ∙ q) ∙' gpt
      =⟨ ap-∙ g p q |in-ctx (λ w → ! gpt ∙ w ∙' gpt) ⟩
    ! gpt ∙ (ap g p ∙ ap g q) ∙' gpt
      =⟨ lemma (ap g p) (ap g q) gpt ⟩
    (! gpt ∙ ap g p ∙' gpt) ∙ (! gpt ∙ ap g q ∙' gpt) ∎
    where
    g : Ω^ n X → Ω^ n Y
    g = fst (ap^ n F)

    gpt : g (idp^ n) == idp^ n
    gpt = snd (ap^ n F)

    lemma : ∀ {i} {A : Type i} {x y : A}
      → (p q : x == x) (r : x == y)
      → ! r ∙ (p ∙ q) ∙' r == (! r ∙ p ∙' r) ∙ (! r ∙ q ∙' r)
    lemma p q idp = idp

{- ap^ preserves (pointed) equivalences -}
module _ {i j} {X : Ptd i} {Y : Ptd j} where

  is-equiv-ap^ : (n : ℕ) (F : fst (X ⊙→ Y)) (e : is-equiv (fst F))
    → is-equiv (fst (ap^ n F))
  is-equiv-ap^ O F e = e
  is-equiv-ap^ (S n) F e =
         pre∙-is-equiv (! (snd (ap^ n F)))
    ∘ise post∙'-is-equiv (snd (ap^ n F))
    ∘ise snd (equiv-ap (_ , is-equiv-ap^ n F e) _ _)

  equiv-ap^ : (n : ℕ) (F : fst (X ⊙→ Y)) (e : is-equiv (fst F))
    → Ω^ n X ≃ Ω^ n Y
  equiv-ap^ n F e = (fst (ap^ n F) , is-equiv-ap^ n F e)

Ω^-level-in : ∀ {i} (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
  → (has-level ((n -2) +2+ m) (fst X) → has-level m (Ω^ n X))
Ω^-level-in m O X pX = pX
Ω^-level-in m (S n) X pX =
  Ω^-level-in (S m) n X
    (transport (λ k → has-level k (fst X)) (! (+2+-βr (n -2) m)) pX)
    (idp^ n) (idp^ n)

Ω^-conn-in : ∀ {i} (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
  → (is-connected ((n -2) +2+ m) (fst X)) → is-connected m (Ω^ n X)
Ω^-conn-in m O X pX = pX
Ω^-conn-in m (S n) X pX =
  path-conn $ Ω^-conn-in (S m) n X $
    transport (λ k → is-connected k (fst X)) (! (+2+-βr (n -2) m)) pX

{- Eckmann-Hilton argument -}
module _ {i} {X : Ptd i} where

  conc^2-comm : (α β : Ω^ 2 X) → conc^ 2 (ℕ-S≠O _) α β == conc^ 2 (ℕ-S≠O _) β α
  conc^2-comm α β = ! (⋆2=conc^ α β) ∙ ⋆2=⋆'2 α β ∙ ⋆'2=conc^ α β
    where
      ⋆2=conc^ : (α β : Ω^ 2 X) → α ⋆2 β == conc^ 2 (ℕ-S≠O _) α β
      ⋆2=conc^ α β = ap (λ π → π ∙ β) (∙-unit-r α)

      ⋆'2=conc^ : (α β : Ω^ 2  X) → α ⋆'2 β == conc^ 2 (ℕ-S≠O _) β α
      ⋆'2=conc^ α β = ap (λ π → β ∙ π) (∙-unit-r α)

{- Pushing truncation through loop space -}
module _ {i} where

  Trunc-Ω^ : (m : ℕ₋₂) (n : ℕ) (X : Ptd i)
    → ⊙Trunc m (⊙Ω^ n X) == ⊙Ω^ n (⊙Trunc ((n -2) +2+ m) X)
  Trunc-Ω^ m O X = idp
  Trunc-Ω^ m (S n) X =
    ⊙Trunc m (⊙Ω^ (S n) X)
      =⟨ ! (pair= (Trunc=-path [ _ ] [ _ ]) (↓-idf-ua-in _ idp)) ⟩
    ⊙Ω (⊙Trunc (S m) (⊙Ω^ n X))
      =⟨ ap ⊙Ω (Trunc-Ω^ (S m) n X) ⟩
    ⊙Ω^ (S n) (⊙Trunc ((n -2) +2+ S m) X)
      =⟨ +2+-βr (n -2) m |in-ctx (λ k → ⊙Ω^ (S n) (⊙Trunc k X)) ⟩
    ⊙Ω^ (S n) (⊙Trunc (S (n -2) +2+ m) X) ∎

  Ω-Trunc-equiv : (m : ℕ₋₂) (X : Ptd i)
    → Ω (⊙Trunc (S m) X) ≃ Trunc m (Ω X)
  Ω-Trunc-equiv m X = Trunc=-equiv [ snd X ] [ snd X ]

{- A loop space is a pregroup, and a group if it has the right level -}
module _ {i} (n : ℕ) (t : n ≠ O) (X : Ptd i) where

  Ω^-group-structure : GroupStructure (Ω^ n X)
  Ω^-group-structure = record {
    ident = idp^ n;
    inv = !^ n t;
    comp = conc^ n t;
    unitl = conc^-unit-l n t;
    unitr = conc^-unit-r n t;
    assoc = conc^-assoc n t;
    invr = !^-inv-r n t;
    invl = !^-inv-l n t
    }

  Ω^-Group : has-level ⟨ n ⟩ (fst X) → Group i
  Ω^-Group pX = group
    (Ω^ n X)
    (Ω^-level-in ⟨0⟩ n X $
       transport (λ t → has-level t (fst X)) (+2+-comm ⟨0⟩ (n -2)) pX)
    Ω^-group-structure

{- Our definition of Ω^ builds up loops on the outside,
 - but this is equivalent to building up on the inside -}
module _ {i} where
  ⊙Ω^-inner-path : (n : ℕ) (X : Ptd i)
    → ⊙Ω^ (S n) X == ⊙Ω^ n (⊙Ω X)
  ⊙Ω^-inner-path O X = idp
  ⊙Ω^-inner-path (S n) X = ap ⊙Ω (⊙Ω^-inner-path n X)

  ⊙Ω^-inner-out : (n : ℕ) (X : Ptd i)
    → fst (⊙Ω^ (S n) X ⊙→ ⊙Ω^ n (⊙Ω X))
  ⊙Ω^-inner-out O _ = (idf _ , idp)
  ⊙Ω^-inner-out (S n) X = ap^ 1 (⊙Ω^-inner-out n X)

  Ω^-inner-out : (n : ℕ) (X : Ptd i)
    → (Ω^ (S n) X → Ω^ n (⊙Ω X))
  Ω^-inner-out n X = fst (⊙Ω^-inner-out n X)

  Ω^-inner-out-conc^ : (n : ℕ) (t : n ≠ O)
    (X : Ptd i) (p q : Ω^ (S n) X)
    → Ω^-inner-out n X (conc^ (S n) (ℕ-S≠O _) p q)
      == conc^ n t (Ω^-inner-out n X p) (Ω^-inner-out n X q)
  Ω^-inner-out-conc^ O t X _ _ = ⊥-rec (t idp)
  Ω^-inner-out-conc^ (S n) t X p q =
    ap^-conc^ 1 (ℕ-S≠O _) (⊙Ω^-inner-out n X) p q

  Ω^-inner-is-equiv : (n : ℕ) (X : Ptd i)
    → is-equiv (fst (⊙Ω^-inner-out n X))
  Ω^-inner-is-equiv O X = is-eq (idf _) (idf _) (λ _ → idp) (λ _ → idp)
  Ω^-inner-is-equiv (S n) X =
    is-equiv-ap^ 1 (⊙Ω^-inner-out n X) (Ω^-inner-is-equiv n X)

  Ω^-inner-equiv : (n : ℕ) (X : Ptd i) → Ω^ (S n) X ≃ Ω^ n (⊙Ω X)
  Ω^-inner-equiv n X = _ , Ω^-inner-is-equiv n X

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
open import Prelude

module Implicits.Syntax.Term where

open import Implicits.Syntax.Type

infixl 9 _[_] _·_
data Term (ν n : ℕ) : Set where
  var  : (x : Fin n) → Term ν n
  Λ    : Term (suc ν) n → Term ν n
  λ'   : Type ν → Term ν (suc n) → Term ν n
  _[_] : Term ν n → Type ν → Term ν n
  _·_  : Term ν n → Term ν n → Term ν n

  -- rule abstraction and application
  ρ    : Type ν → Term ν (suc n) → Term ν n
  _with'_ : Term ν n → Term ν n → Term ν n

  -- implicit rule application
  _⟨⟩  : Term ν n → Term ν n

ClosedTerm : Set
ClosedTerm = Term 0 0

-----------------------------------------------------------------------------
-- syntactic sugar

let'_∶_in'_ : ∀ {ν n} → Term ν n → Type ν → Term ν (suc n) → Term ν n
let' e₁ ∶ r in' e₂ = (λ' r e₂) · e₁

implicit_∶_in'_ : ∀ {ν n} → Term ν n → Type ν → Term ν (suc n) → Term ν n
implicit e₁ ∶ r in' e₂ = (ρ r e₂) with' e₁

¿_ : ∀ {ν n} → Type ν → Term ν n
¿ r = (ρ r (var zero)) ⟨⟩


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library where

module Literals where open import Light.Literals public

module Data where
      module Empty where open import Light.Library.Data.Empty public
      module Either where open import Light.Library.Data.Either public
      module Natural where open import Light.Library.Data.Natural public
      module Unit where open import Light.Library.Data.Unit public
      module Integer where open import Light.Library.Data.Integer public
      module Boolean where open import Light.Library.Data.Boolean public
      module Both where open import Light.Library.Data.Both public
      module Product where open import Light.Library.Data.Product public
      module These where open import Light.Library.Data.These public

module Relation where
      module Binary where
            open import Light.Library.Relation.Binary public
            module Equality where
                  open import Light.Library.Relation.Binary.Equality public
                  module Decidable where open import Light.Library.Relation.Binary.Equality.Decidable public
            module Decidable where open import Light.Library.Relation.Binary.Decidable public
      open import Light.Library.Relation public
      module Decidable where open import Light.Library.Relation.Decidable public

module Action where open import Light.Library.Action public

module Arithmetic where open import Light.Library.Arithmetic public
module Level where open import Light.Level public
module Subtyping where open import Light.Subtyping public

module Variable where
      module Levels where open import Light.Variable.Levels public
      module Sets where open import Light.Variable.Sets public
      module Other {ℓ} (𝕒 : Set ℓ) where open import Light.Variable.Other 𝕒 public

module Package where open import Light.Package public
open Package using (Package) hiding (module Package) public

-- module Indexed where open import Light.Indexed

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

module Cubical.Algebra.CommRing.Instances.Polynomials where

open import Cubical.Foundations.Prelude
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Polynomials

private
  variable
    ℓ : Level

Poly : (CommRing ℓ) → CommRing ℓ
Poly R = (PolyMod.Poly R) , str
    where
      open CommRingStr --(snd R)
      str : CommRingStr (PolyMod.Poly R)
      0r str = PolyMod.0P R
      1r str = PolyMod.1P R
      _+_ str = PolyMod._Poly+_ R
      _·_ str = PolyMod._Poly*_ R
      - str = PolyMod.Poly- R
      isCommRing str = makeIsCommRing (PolyMod.isSetPoly R)
                                      (PolyMod.Poly+Assoc R)
                                      (PolyMod.Poly+Rid R)
                                      (PolyMod.Poly+Inverses R)
                                      (PolyMod.Poly+Comm  R)
                                      (PolyMod.Poly*Associative R)
                                      (PolyMod.Poly*Rid R)
                                      (PolyMod.Poly*LDistrPoly+ R)
                                      (PolyMod.Poly*Commutative R)

max_stars_repo_name: AkermanRydbeck/cubical

max_issues_repo_name: AkermanRydbeck/cubical

max_forks_repo_name: AkermanRydbeck/cubical


text:
module empty where

open import level

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data ⊥ {ℓ : Level} : Set ℓ where

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

----------------------------------------------------------------------
-- theorems
----------------------------------------------------------------------
⊥-elim : ∀{ℓ} → ⊥ {ℓ} → ∀{ℓ'}{P : Set ℓ'} → P
⊥-elim ()

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Andreas, 2015-08-11, issue reported by G.Allais

-- The `a` record field of `Pack` is identified as a function
-- (coloured blue, put in a \AgdaFunction in the LaTeX backend)
-- when it should be coloured pink.
-- The problem does not show up when dropping the second record
-- type or removing the module declaration.

record Pack (A : Set) : Set where
  field
    a : A

record Packed {A : Set} (p : Pack A) : Set where
  module PP = Pack p

module Synchronised {A : Set} {p : Pack A} (rel : Packed p) where
  module M = Packed rel

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Nat.GCD where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

open import Cubical.Induction.WellFounded

open import Cubical.Data.Fin
open import Cubical.Data.Sigma as Σ
open import Cubical.Data.NatPlusOne

open import Cubical.HITs.PropositionalTruncation as PropTrunc

open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties
open import Cubical.Data.Nat.Order
open import Cubical.Data.Nat.Divisibility

private
  variable
    m n d : ℕ

-- common divisors

isCD : ℕ → ℕ → ℕ → Type₀
isCD m n d = (d ∣ m) × (d ∣ n)

isPropIsCD : isProp (isCD m n d)
isPropIsCD = isProp× isProp∣ isProp∣

symCD : isCD m n d → isCD n m d
symCD (d∣m , d∣n) = (d∣n , d∣m)

-- greatest common divisors

isGCD : ℕ → ℕ → ℕ → Type₀
isGCD m n d = (isCD m n d) × (∀ d' → isCD m n d' → d' ∣ d)

GCD : ℕ → ℕ → Type₀
GCD m n = Σ ℕ (isGCD m n)

isPropIsGCD : isProp (isGCD m n d)
isPropIsGCD = isProp× isPropIsCD (isPropΠ2 (λ _ _ → isProp∣))

isPropGCD : isProp (GCD m n)
isPropGCD (d , dCD , gr) (d' , d'CD , gr') =
  Σ≡Prop (λ _ → isPropIsGCD) (antisym∣ (gr' d dCD) (gr d' d'CD))

symGCD : isGCD m n d → isGCD n m d
symGCD (dCD , gr) = symCD dCD , λ { d' d'CD → gr d' (symCD d'CD) }

divsGCD : m ∣ n → isGCD m n m
divsGCD p = (∣-refl refl , p) , λ { d (d∣m , _) → d∣m }

oneGCD : ∀ m → isGCD m 1 1
oneGCD m = symGCD (divsGCD (∣-oneˡ m))

-- The base case of the Euclidean algorithm
zeroGCD : ∀ m → isGCD m 0 m
zeroGCD m = divsGCD (∣-zeroʳ m)

private
  lem₁ : prediv d (suc n) → prediv d (m % suc n) → prediv d m
  lem₁ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = (q · c₁ + c₂) , p
    where r = m % suc n; q = n%k≡n[modk] m (suc n) .fst
          p = (q · c₁ + c₂) · d     ≡⟨ sym (·-distribʳ (q · c₁) c₂ d) ⟩
              (q · c₁) · d + c₂ · d ≡⟨ cong (_+ c₂ · d) (sym (·-assoc q c₁ d))  ⟩
              q · (c₁ · d) + c₂ · d ≡[ i ]⟨ q · (p₁ i) + (p₂ i) ⟩
              q · (suc n)  + r      ≡⟨ n%k≡n[modk] m (suc n) .snd ⟩
              m                     ∎

  lem₂ : prediv d (suc n) → prediv d m → prediv d (m % suc n)
  lem₂ {d} {n} {m} (c₁ , p₁) (c₂ , p₂) = c₂ ∸ q · c₁ , p
    where r = m % suc n; q = n%k≡n[modk] m (suc n) .fst
          p = (c₂ ∸ q · c₁) · d               ≡⟨ ∸-distribʳ c₂ (q · c₁) d ⟩
              c₂ · d ∸ (q · c₁) · d           ≡⟨ cong (c₂ · d ∸_) (sym (·-assoc q c₁ d)) ⟩
              c₂ · d ∸ q · (c₁ · d)           ≡[ i ]⟨ p₂ i ∸ q · (p₁ i) ⟩
              m      ∸ q · (suc n)            ≡⟨ cong (_∸ q · (suc n)) (sym (n%k≡n[modk] m (suc n) .snd)) ⟩
              (q · (suc n) + r) ∸ q · (suc n) ≡⟨ cong (_∸ q · (suc n)) (+-comm (q · (suc n)) r) ⟩
              (r + q · (suc n)) ∸ q · (suc n) ≡⟨ ∸-cancelʳ r zero (q · (suc n)) ⟩
              r ∎

-- The inductive step of the Euclidean algorithm
stepGCD : isGCD (suc n) (m % suc n) d
        → isGCD m       (suc n)     d
fst (stepGCD ((d∣n , d∣m%n) , gr)) = PropTrunc.map2 lem₁ d∣n d∣m%n , d∣n
snd (stepGCD ((d∣n , d∣m%n) , gr)) d' (d'∣m , d'∣n) = gr d' (d'∣n , PropTrunc.map2 lem₂ d'∣n d'∣m)

-- putting it all together using well-founded induction

euclid< : ∀ m n → n < m → GCD m n
euclid< = WFI.induction <-wellfounded λ {
  m rec zero    p → m , zeroGCD m ;
  m rec (suc n) p → let d , dGCD = rec (suc n) p (m % suc n) (n%sk<sk m n)
                     in d , stepGCD dGCD }

euclid : ∀ m n → GCD m n
euclid m n with n ≟ m
... | lt p = euclid< m n p
... | gt p = Σ.map-snd symGCD (euclid< n m p)
... | eq p = m , divsGCD (∣-refl (sym p))

isContrGCD : ∀ m n → isContr (GCD m n)
isContrGCD m n = euclid m n , isPropGCD _

-- the gcd operator on ℕ

gcd : ℕ → ℕ → ℕ
gcd m n = euclid m n .fst

gcdIsGCD : ∀ m n → isGCD m n (gcd m n)
gcdIsGCD m n = euclid m n .snd

isGCD→gcd≡ : isGCD m n d → gcd m n ≡ d
isGCD→gcd≡ dGCD = cong fst (isContrGCD _ _ .snd (_ , dGCD))

gcd≡→isGCD : gcd m n ≡ d → isGCD m n d
gcd≡→isGCD p = subst (isGCD _ _) p (gcdIsGCD _ _)

-- multiplicative properties of the gcd

isCD-cancelʳ : ∀ k → isCD (m · suc k) (n · suc k) (d · suc k)
                   → isCD m n d
isCD-cancelʳ k (dk∣mk , dk∣nk) = (∣-cancelʳ k dk∣mk , ∣-cancelʳ k dk∣nk)

isCD-multʳ : ∀ k → isCD m n d
                 → isCD (m · k) (n · k) (d · k)
isCD-multʳ k (d∣m , d∣n) = (∣-multʳ k d∣m , ∣-multʳ k d∣n)

isGCD-cancelʳ : ∀ k → isGCD (m · suc k) (n · suc k) (d · suc k)
                    → isGCD m n d
isGCD-cancelʳ {m} {n} {d} k (dCD , gr) =
  isCD-cancelʳ k dCD ,  λ d' d'CD → ∣-cancelʳ k (gr (d' · suc k) (isCD-multʳ (suc k) d'CD))

gcd-factorʳ : ∀ m n k → gcd (m · k) (n · k) ≡ gcd m n · k
gcd-factorʳ m n zero = (λ i → gcd (0≡m·0 m (~ i)) (0≡m·0 n (~ i))) ∙ 0≡m·0 (gcd m n)
gcd-factorʳ m n (suc k) = sym p ∙ cong (_· suc k) (sym q)
  where k∣gcd : suc k ∣ gcd (m · suc k) (n · suc k)
        k∣gcd = gcdIsGCD (m · suc k) (n · suc k) .snd (suc k) (∣-right m , ∣-right n)
        d' = ∣-untrunc k∣gcd .fst
        p : d' · suc k ≡ gcd (m · suc k) (n · suc k)
        p = ∣-untrunc k∣gcd .snd

        d'GCD : isGCD m n d'
        d'GCD = isGCD-cancelʳ _ (subst (isGCD _ _) (sym p) (gcdIsGCD (m · suc k) (n · suc k)))
        q : gcd m n ≡ d'
        q = isGCD→gcd≡ d'GCD

-- Q: Can this be proved directly? (i.e. without a transport)
isGCD-multʳ : ∀ k → isGCD m n d
                  → isGCD (m · k) (n · k) (d · k)
isGCD-multʳ {m} {n} {d} k dGCD = gcd≡→isGCD (gcd-factorʳ m n k ∙ cong (_· k) r)
  where r : gcd m n ≡ d
        r = isGCD→gcd≡ dGCD

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Calf.Types.Bool where

open import Calf.Prelude
open import Calf.Metalanguage

open import Data.Bool public using (Bool; true; false; if_then_else_)

bool : tp pos
bool = U (meta Bool)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
{-# OPTIONS --safe #-}
module MissingDefinition where

T : Set -> Set


text:
{- Cubical Agda with K

This file demonstrates the incompatibility of the --cubical
and --with-K flags, relying on the well-known incosistency of K with
univalence.

The --safe flag can be used to prevent accidentally mixing such
incompatible flags.

-}

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

module Cubical.WithK where

open import Cubical.Data.Equality
open import Cubical.Data.Bool
open import Cubical.Data.Empty

private
 variable
  ℓ : Level
  A : Type ℓ
  x y : A

uip : (prf : x ≡ x) → Path _ prf refl
uip refl i = refl

transport-uip : (prf : A ≡ A) → Path _ (transportPath (eqToPath prf) x) x
transport-uip {x = x} prf =
  compPath (congPath (λ p → transportPath (eqToPath p) x) (uip prf)) (transportRefl x)

transport-not : Path _ (transportPath (eqToPath (pathToEq notEq)) true) false
transport-not = congPath (λ a → transportPath a true) (eqToPath-pathToEq notEq)

false-true : Path _ false true
false-true = compPath (symPath transport-not) (transport-uip (pathToEq notEq))

absurd : (X : Type) → X
absurd X = transportPath (congPath sel false-true) true
  where
    sel : Bool → Type
    sel false = Bool
    sel true = X

inconsistency : ⊥
inconsistency = absurd ⊥

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module WrongNamedArgument2 where

postulate
  f : {A : Set₁} → A

test : Set
test = f {B = Set}

-- Unsolved meta.
-- It is not an error since A could be instantiated to a function type
-- accepting hidden argument with name B.


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Argument information used in the reflection machinery
------------------------------------------------------------------------

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

module Reflection.Argument.Information where

open import Data.Product
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Reflection.Argument.Relevance as Relevance using (Relevance)
open import Reflection.Argument.Visibility as Visibility using (Visibility)

------------------------------------------------------------------------
-- Re-exporting the builtins publically

open import Agda.Builtin.Reflection public using (ArgInfo)
open ArgInfo public

------------------------------------------------------------------------
-- Operations

visibility : ArgInfo → Visibility
visibility (arg-info v _) = v

relevance : ArgInfo → Relevance
relevance (arg-info _ r) = r

------------------------------------------------------------------------
-- Decidable equality

arg-info-injective₁ : ∀ {v r v′ r′} → arg-info v r ≡ arg-info v′ r′ → v ≡ v′
arg-info-injective₁ refl = refl

arg-info-injective₂ : ∀ {v r v′ r′} → arg-info v r ≡ arg-info v′ r′ → r ≡ r′
arg-info-injective₂ refl = refl

arg-info-injective : ∀ {v r v′ r′} → arg-info v r ≡ arg-info v′ r′ → v ≡ v′ × r ≡ r′
arg-info-injective = < arg-info-injective₁ , arg-info-injective₂ >

_≟_ : DecidableEquality ArgInfo
arg-info v r ≟ arg-info v′ r′ =
  Dec.map′ (uncurry (cong₂ arg-info))
           arg-info-injective
           (v Visibility.≟ v′ ×-dec r Relevance.≟ r′)


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

module FFI.Data.Vector where

open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Equality.Rewrite using ()
open import Agda.Builtin.Int using (Int; pos; negsuc)
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.Bool using (Bool; false; true)
open import FFI.Data.HaskellInt using (HaskellInt; haskellIntToInt; intToHaskellInt)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import Properties.Equality using (_≢_)

{-# FOREIGN GHC import qualified Data.Vector #-}

postulate Vector : Set → Set
{-# POLARITY Vector ++ #-}
{-# COMPILE GHC Vector = type Data.Vector.Vector #-}

postulate
  empty : ∀ {A} → (Vector A)
  null : ∀ {A} → (Vector A) → Bool
  unsafeHead : ∀ {A} → (Vector A) → A
  unsafeTail : ∀ {A} → (Vector A) → (Vector A)
  length : ∀ {A} → (Vector A) → Nat
  lookup : ∀ {A} → (Vector A) → Nat → (Maybe A)
  snoc : ∀ {A} → (Vector A) → A → (Vector A)
{-# COMPILE GHC empty = \_ -> Data.Vector.empty #-}
{-# COMPILE GHC null = \_ -> Data.Vector.null #-}
{-# COMPILE GHC unsafeHead = \_ -> Data.Vector.unsafeHead #-}
{-# COMPILE GHC unsafeTail = \_ -> Data.Vector.unsafeTail #-}
{-# COMPILE GHC length = \_ -> (fromIntegral . Data.Vector.length) #-}
{-# COMPILE GHC lookup = \_ v -> ((v Data.Vector.!?) . fromIntegral) #-}
{-# COMPILE GHC snoc = \_ -> Data.Vector.snoc #-}

postulate length-empty : ∀ {A} → (length (empty {A}) ≡ 0)
postulate lookup-empty : ∀ {A} n → (lookup (empty {A}) n ≡ nothing)
postulate lookup-snoc : ∀ {A} (x : A) (v : Vector A) → (lookup (snoc v x) (length v) ≡ just x)
postulate lookup-length : ∀ {A} (v : Vector A) → (lookup v (length v) ≡ nothing)
postulate lookup-snoc-empty : ∀ {A} (x : A) → (lookup (snoc empty x) 0 ≡ just x)
postulate lookup-snoc-not : ∀ {A n} (x : A) (v : Vector A) → (n ≢ length v) → (lookup v n ≡ lookup (snoc v x) n)

{-# REWRITE length-empty lookup-snoc lookup-length lookup-snoc-empty lookup-empty #-}

head : ∀ {A} → (Vector A) → (Maybe A)
head vec with null vec
head vec | false = just (unsafeHead vec)
head vec | true = nothing

tail : ∀ {A} → (Vector A) → Vector A
tail vec with null vec
tail vec | false = unsafeTail vec
tail vec | true = empty

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
open import Function using (_∘_)
open import Category.Functor
open import Category.Monad
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Fin as Fin using (Fin; zero; suc)
open import Data.Fin.Props as FinProps using ()
open import Data.Maybe as Maybe using (Maybe; maybe; just; nothing)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (Σ; ∃; _,_; proj₁; proj₂) renaming (_×_ to _∧_)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Data.Vec as Vec using (Vec; []; _∷_; head; tail)
open import Data.Vec.Equality as VecEq
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; _≢_; refl; sym; trans; cong; cong₂; inspect; Reveal_is_; [_])

module Unification.Correctness (Symbol : ℕ -> Set) (decEqSym : ∀ {k} (f g : Symbol k) → Dec (f ≡ g)) where

  open import Unification Symbol decEqSym

  open RawFunctor {{...}}
  open DecSetoid {{...}} using (_≟_)

  private maybeFunctor = Maybe.functor
  private finDecSetoid : ∀ {n} → DecSetoid _ _
          finDecSetoid {n} = FinProps.decSetoid n

  -- * proving correctness of replacement function

  mutual
    -- | proof that var is the identity of replace
    replace-thm₁ : ∀ {n} (t : Term n) → replace var t ≡ t
    replace-thm₁ (var x)    = refl
    replace-thm₁ (con s ts) = cong (con s) (replaceChildren-thm₁ ts)

    -- | proof that var is the identity of replaceChildren
    replaceChildren-thm₁ : ∀ {n k} (ts : Vec (Term n) k) → replaceChildren var ts ≡ ts
    replaceChildren-thm₁ [] = refl
    replaceChildren-thm₁ (t ∷ ts) rewrite replace-thm₁ t = cong (_∷_ _) (replaceChildren-thm₁ ts)

  -- * proving correctness of substitution/replacement composition

  -- | proof that `var ∘ _` is the identity of ◇
  compose-thm₁
    : ∀ {m n l} (f : Fin m → Term n) (r : Fin l → Fin m) (t : Term l)
    → f ◇ (var ∘ r) ≡ f ∘ r
  compose-thm₁ f r t = refl

  mutual
    -- | proof that _◇_ behaves as composition of replacements
    compose-thm₂
      : ∀ {m n l} (f : Fin m → Term n) (g : Fin l → Term m) (t : Term l)
      → replace (f ◇ g) t ≡ replace f (replace g t)
    compose-thm₂ f g (var x) = refl
    compose-thm₂ f g (con s ts) = cong (con s) (composeChildren-thm₂ f g ts)

    -- | proof that _◇_ behaves as composition of replacements
    composeChildren-thm₂
      : ∀ {m n l k} (f : Fin m → Term n) (g : Fin l → Term m) (ts : Vec (Term l) k)
      → replaceChildren (f ◇ g) ts ≡ replaceChildren f (replaceChildren g ts)
    composeChildren-thm₂ f g [] = refl
    composeChildren-thm₂ f g (t ∷ ts) rewrite compose-thm₂ f g t = cong (_∷_ _) (composeChildren-thm₂ f g ts)

  -- * proving correctness of thick and thin

  -- | predecessor function over finite numbers
  pred : ∀ {n} → Fin (suc (suc n)) → Fin (suc n)
  pred  zero   = zero
  pred (suc x) = x

  -- | proof of injectivity of thin
  thin-injective
    : ∀ {n} (x : Fin (suc n)) (y z : Fin n)
    → thin x y ≡ thin x z → y ≡ z
  thin-injective {zero}   zero    ()      _       _
  thin-injective {zero}  (suc _)  ()      _       _
  thin-injective {suc _}  zero    zero    zero    refl = refl
  thin-injective {suc _}  zero    zero   (suc _)  ()
  thin-injective {suc _}  zero   (suc _)  zero    ()
  thin-injective {suc _}  zero   (suc y) (suc .y) refl = refl
  thin-injective {suc _} (suc _)  zero    zero    refl = refl
  thin-injective {suc _} (suc _)  zero   (suc _)  ()
  thin-injective {suc _} (suc _) (suc _)  zero    ()
  thin-injective {suc n} (suc x) (suc y) (suc z)  p
    = cong suc (thin-injective x y z (cong pred p))

  -- | proof that thin x will never map anything to x
  thinxy≢x
    : ∀ {n} (x : Fin (suc n)) (y : Fin n)
    → thin x y ≢ x
  thinxy≢x  zero    zero   ()
  thinxy≢x  zero   (suc _) ()
  thinxy≢x (suc _)  zero   ()
  thinxy≢x (suc x) (suc y) p
    = thinxy≢x x y (cong pred p)

  -- | proof that `thin x` reaches all y where x ≢ y
  x≢y→thinxz≡y
    : ∀ {n} (x y : Fin (suc n))
    → x ≢ y → ∃ (λ z → thin x z ≡ y)
  x≢y→thinxz≡y          zero     zero 0≢0 with 0≢0 refl
  x≢y→thinxz≡y          zero     zero 0≢0 | ()
  x≢y→thinxz≡y {zero}  (suc ())  _       _
  x≢y→thinxz≡y {zero}   zero    (suc ()) _
  x≢y→thinxz≡y {suc _}  zero    (suc y)  _ = y , refl
  x≢y→thinxz≡y {suc _} (suc x)   zero    _ = zero , refl
  x≢y→thinxz≡y {suc _} (suc x)  (suc y)  sx≢sy
    = (suc (proj₁ prf)) , (lem x y (proj₁ prf) (proj₂ prf))
    where
    x≢y = sx≢sy ∘ cong suc
    prf = x≢y→thinxz≡y x y x≢y
    lem : ∀ {n} (x y : Fin (suc n)) (z : Fin n)
        → thin x z ≡ y → thin (suc x) (suc z) ≡ suc y
    lem  zero    zero              _      ()
    lem  zero    (suc .z)          z      refl = refl
    lem (suc _)  zero              zero   refl = refl
    lem (suc _)  zero             (suc _) ()
    lem (suc _) (suc _)            zero   ()
    lem (suc x) (suc .(thin x z)) (suc z) refl = refl

  -- | proof that thick x composed with thin x is the identity
  thickx∘thinx≡yes
    : ∀ {n} (x : Fin (suc n)) (y : Fin n)
    → thick x (thin x y) ≡ just y
  thickx∘thinx≡yes  zero    zero   = refl
  thickx∘thinx≡yes  zero   (suc _) = refl
  thickx∘thinx≡yes (suc _)  zero   = refl
  thickx∘thinx≡yes (suc x) (suc y) = cong (_<$>_ suc) (thickx∘thinx≡yes x y)

  -- | proof that `thin` is a partial inverse of `thick`
  thin≡thick⁻¹
    : ∀ {n} (x : Fin (suc n)) (y : Fin n) (z : Fin (suc n))
    → thin x y ≡ z
    → thick x z ≡ just y
  thin≡thick⁻¹ x y z p with p
  thin≡thick⁻¹ x y .(thin x y) _ | refl = thickx∘thinx≡yes x y

  -- | proof that `thick x x` returns nothing
  thickxx≡no
    : ∀ {n} (x : Fin (suc n))
    → thick x x ≡ nothing
  thickxx≡no zero = refl
  thickxx≡no {zero}  (suc ())
  thickxx≡no {suc n} (suc x)
    = cong (maybe (λ x → just (suc x)) nothing) (thickxx≡no x)

  -- | proof that `thick x y` returns something when x ≢ y
  x≢y→thickxy≡yes
    : ∀ {n} (x y : Fin (suc n))
    → x ≢ y → ∃ (λ z → thick x y ≡ just z)
  x≢y→thickxy≡yes zero zero 0≢0 with 0≢0 refl
  x≢y→thickxy≡yes zero zero 0≢0 | ()
  x≢y→thickxy≡yes zero (suc y) p = y , refl
  x≢y→thickxy≡yes {zero}  (suc ())  _ _
  x≢y→thickxy≡yes {suc n} (suc x) zero _ = zero , refl
  x≢y→thickxy≡yes {suc n} (suc x) (suc y) sx≢sy
    = (suc (proj₁ prf)) , (cong (_<$>_ suc) (proj₂ prf))
    where
    x≢y = sx≢sy ∘ cong suc
    prf = x≢y→thickxy≡yes {n} x y x≢y

  -- | proof that `thick` is the partial inverse of `thin`
  thick≡thin⁻¹ : ∀ {n} (x y : Fin (suc n)) (r : Maybe (Fin n))
    → thick x y ≡ r
    → x ≡ y ∧ r ≡ nothing
    ⊎ ∃ (λ z → thin x z ≡ y ∧ r ≡ just z)
  thick≡thin⁻¹ x  y _ thickxy≡r with x ≟ y | thickxy≡r
  thick≡thin⁻¹ x .x .(thick x x) _ | yes refl | refl
    = inj₁ (refl , thickxx≡no x)
  thick≡thin⁻¹ x  y .(thick x y) _ | no  x≢y  | refl
    = inj₂ (proj₁ prf₁ , (proj₂ prf₁) , prf₂)
    where
    prf₁ = x≢y→thinxz≡y x y x≢y
    prf₂ = thin≡thick⁻¹ x (proj₁ prf₁) y (proj₂ prf₁)

  -- | proof that if check returns nothing, checkChildren will too
  check≡no→checkChildren≡no
    : ∀ {n} (x : Fin (suc n)) (s : Symbol (suc n)) (ts : Vec (Term (suc n)) (suc n))
    → check x (con s ts) ≡ nothing → checkChildren x ts ≡ nothing
  check≡no→checkChildren≡no x s ts p with checkChildren x ts
  check≡no→checkChildren≡no x s ts p  | nothing = refl
  check≡no→checkChildren≡no x s ts () | just _

  -- | proof that if check returns something, checkChildren will too
  check≡yes→checkChildren≡yes
    : ∀ {n} (x : Fin (suc n)) (s : Symbol (suc n)) (ts : Vec (Term (suc n)) (suc n)) (ts' : Vec (Term n) (suc n))
    → check x (con s ts) ≡ just (con s ts') → checkChildren x ts ≡ just ts'
  check≡yes→checkChildren≡yes x s ts ts' p with checkChildren x ts
  check≡yes→checkChildren≡yes x s ts ts' refl | just .ts' = refl
  check≡yes→checkChildren≡yes x s ts ts' ()   | nothing

  -- | occurs predicate that is only inhabited if x occurs in t
  mutual
    data Occurs {n : ℕ} (x : Fin n) : Term n → Set where
      Here    : Occurs x (var x)
      Further : ∀ {k ts} {s : Symbol k} → OccursChildren x {k} ts → Occurs x (con s ts)

    data OccursChildren {n : ℕ} (x : Fin n) : {k : ℕ} → Vec (Term n) k → Set where
      Here    : ∀ {k t ts} → Occurs x t → OccursChildren x {suc k} (t ∷ ts)
      Further : ∀ {k t ts} → OccursChildren x {k} ts → OccursChildren x {suc k} (t ∷ ts)

  -- | proof of decidability for the occurs predicate
  mutual
    occurs? : ∀ {n} (x : Fin n) (t : Term n) → Dec (Occurs x t)
    occurs?  x₁ (var x₂) with x₁ ≟ x₂
    occurs? .x₂ (var x₂) | yes refl = yes Here
    occurs?  x₁ (var x₂) | no x₁≢x₂ = no (x₁≢x₂ ∘ lem x₁ x₂)
      where
      lem : ∀ {n} (x y : Fin n) → Occurs x (var y) → x ≡ y
      lem  zero    zero    _    = refl
      lem  zero   (suc _)  ()
      lem (suc x)  zero    ()
      lem (suc x) (suc .x) Here = refl
    occurs?  x₁ (con s ts) with occursChildren? x₁ ts
    occurs?  x₁ (con s ts) | yes x₁∈ts = yes (Further x₁∈ts)
    occurs?  x₁ (con s ts) | no  x₁∉ts = no (x₁∉ts ∘ lem x₁)
      where
      lem : ∀ {n s ts} (x : Fin n) → Occurs x (con s ts) → OccursChildren x ts
      lem x (Further x₂) = x₂

    occursChildren? : ∀ {n k} (x : Fin n) (ts : Vec (Term n) k) → Dec (OccursChildren x ts)
    occursChildren? x₁ [] = no (λ ())
    occursChildren? x₁ (t ∷ ts) with occurs? x₁ t
    occursChildren? x₁ (t ∷ ts) | yes h = yes (Here h)
    occursChildren? x₁ (t ∷ ts) | no ¬h with occursChildren? x₁ ts
    occursChildren? x₁ (t ∷ ts) | no ¬h | yes f = yes (Further f)
    occursChildren? x₁ (t ∷ ts) | no ¬h | no ¬f = no lem
      where
      lem : OccursChildren x₁ (t ∷ ts) → ⊥
      lem (Here p)    = ¬h p
      lem (Further p) = ¬f p

  -- * proving correctness of check

  mutual
    -- | proving that if x occurs in t, check returns nothing
    occurs→check≡no
      : ∀ {n} (x : Fin (suc n)) (t : Term (suc n))
      → Occurs x t → check x t ≡ nothing
    occurs→check≡no x .(Unification.var x) Here
      rewrite thickxx≡no x = refl
    occurs→check≡no x .(Unification.con s ts) (Further {k} {ts} {s} p)
      rewrite occursChildren→checkChildren≡no x ts p = refl

    -- | proving that if x occurs in ts, checkChildren returns nothing
    occursChildren→checkChildren≡no
      : ∀ {n k} (x : Fin (suc n)) (ts : Vec (Term (suc n)) k)
      → OccursChildren x ts → checkChildren x ts ≡ nothing
    occursChildren→checkChildren≡no x .(t ∷ ts) (Here {k} {t} {ts} p)
      rewrite occurs→check≡no x t p = refl
    occursChildren→checkChildren≡no x .(t ∷ ts) (Further {k} {t} {ts} p)
      with check x t
    ... | just  _ rewrite occursChildren→checkChildren≡no x ts p = refl
    ... | nothing rewrite occursChildren→checkChildren≡no x ts p = refl

  mutual
    -- | proof that if check x t returns nothing, x occurs in t
    check≡no→occurs
      : ∀ {n} (x : Fin (suc n)) (t : Term (suc n))
      → check x t ≡ nothing → Occurs x t
    check≡no→occurs  x₁ (var x₂) p with x₁ ≟ x₂
    check≡no→occurs .x₂ (var x₂) p | yes refl = Here
    check≡no→occurs  x₁ (var x₂) p | no x₁≢x₂ = ⊥-elim (lem₂ p)
      where
      lem₁ : ∃ (λ z → thick x₁ x₂ ≡ just z)
      lem₁ = x≢y→thickxy≡yes x₁ x₂ x₁≢x₂
      lem₂ : var <$> thick x₁ x₂ ≡ nothing → ⊥
      lem₂ rewrite proj₂ lem₁ = λ ()
    check≡no→occurs {n} x₁ (con s ts) p
      = Further (checkChildren≡no→occursChildren x₁ ts (lem p))
      where
      lem : con s <$> checkChildren x₁ ts ≡ nothing → checkChildren x₁ ts ≡ nothing
      lem p with checkChildren x₁ ts | inspect (checkChildren x₁) ts
      lem () | just  _ | [ eq ]
      lem p  | nothing | [ eq ] = refl

    -- | proof that if checkChildren x ts returns nothing, x occurs in ts
    checkChildren≡no→occursChildren
      : ∀ {n k} (x : Fin (suc n)) (ts : Vec (Term (suc n)) k)
      → checkChildren x ts ≡ nothing → OccursChildren x ts
    checkChildren≡no→occursChildren x [] ()
    checkChildren≡no→occursChildren x (t ∷ ts) p with check x t | inspect (check x) t
    ... | nothing | [ e₁ ] = Here (check≡no→occurs x t e₁)
    ... | just  _ | [ e₁ ] with checkChildren x ts | inspect (checkChildren x) ts
    ... | nothing | [ e₂ ] = Further (checkChildren≡no→occursChildren x ts e₂)
    checkChildren≡no→occursChildren x (t ∷ ts) () | just _ | [ e₁ ] | just _ | [ e₂ ]

  -- | proof that if check returns just, x does not occur in t
  check≡yes→¬occurs
    : ∀ {n} (x : Fin (suc n)) (t : Term (suc n)) (t' : Term n)
    → check x t ≡ just t' → ¬ (Occurs x t)
  check≡yes→¬occurs x t t' p₁ x∈t with occurs→check≡no x t x∈t
  check≡yes→¬occurs x t t' p₁ _   | p₂  with check x t
  check≡yes→¬occurs x t t' p₁ _   | ()  | just _
  check≡yes→¬occurs x t t' () _   | p₂  | nothing

  -- | proof that x does not occur in t, check returns just
  ¬occurs→check≡yes
    : ∀ {n} (x : Fin (suc n)) (t : Term (suc n))
    → ¬ (Occurs x t) → ∃ (λ t' → check x t ≡ just t')
  ¬occurs→check≡yes x t x∉t with check x t | inspect (check x) t
  ¬occurs→check≡yes x t x∉t | nothing | [ eq ] with x∉t (check≡no→occurs x t eq)
  ¬occurs→check≡yes x t x∉t | nothing | [ eq ] | ()
  ¬occurs→check≡yes x t x∉t | just t' | [ eq ] = t' , refl

  -- * proving correctness of _for_

  -- | proof that if there is nothing to unify, _for_ is the identity
  for-thm₁
    : ∀ {n} (t : Term n) (x : Fin (suc n)) (y : Fin n)
    → (t for x) (thin x y) ≡ var y
  for-thm₁ t x y rewrite thickx∘thinx≡yes x y = refl

  mutual
    -- | proof that if there is something to unify, _for_ unifies
    for-thm₂
      : ∀ {n} (x : Fin (suc n)) (t : Term (suc n)) (t' : Term n)
      → check x t ≡ just t' → replace (t' for x) t ≡ (t' for x) x
    for-thm₂  x (var y) _ _ with x ≟ y
    for-thm₂ .y (var y) _ _ | yes refl = refl
    for-thm₂  x (var y) _ _ | no x≢y
      with thick x y | x≢y→thickxy≡yes x y x≢y
         | thick x x | thickxx≡no x
    for-thm₂  x (var y) .(var z) refl | no _
         | .(just z) | z , refl
         | .nothing  | refl = refl
    for-thm₂  x (con s ts) _ _ with checkChildren x ts | inspect (checkChildren x) ts
    for-thm₂  x (con s ts) _ ()              | nothing  | _
    for-thm₂  x (con s ts) .(con s ts') refl | just ts' | [ checkChildren≡yes ]
      rewrite thickxx≡no x = cong (con s) (forChildren-thm₂ x s ts ts' checkChildren≡yes)

    forChildren-thm₂ : ∀ {n k} -> (x : Fin (suc n)) (s : Symbol k)
     (ts : Vec (Term (suc n)) k) (ts' : Vec (Term n) k) ->
     checkChildren x ts ≡ just ts' ->
     replaceChildren (con s ts' for x) ts ≡ ts'
    forChildren-thm₂ x s [] [] eq rewrite thickxx≡no x = refl
    forChildren-thm₂ x s (t1 ∷ ts) (t2 ∷ ts') eq
      with check x t1 | inspect (check x) t1 | checkChildren x ts |  inspect (checkChildren x) ts
    forChildren-thm₂ x s (t1 ∷ ts) (t2 ∷ ts') refl | just .t2 | [ eq1 ] | just .ts' | [ eq2 ]
      = cong₂ _∷_ {!!} {!!}
      where
      lemma₁ = for-thm₂ x t1 t2 eq1
    forChildren-thm₂ x s (t1 ∷ ts) (t2 ∷ ts') () | just x₁ | _ | nothing | _
    forChildren-thm₂ x s (t1 ∷ ts) (t2 ∷ ts') () | nothing | _ | cs | _

  -- * proving correctness of apply, concat and compose

  ++-thm₁ : ∀ {m n} (s : Subst m n) → nil ++ s ≡ s
  ++-thm₁ nil = refl
  ++-thm₁ (snoc s t x) = cong (λ s → snoc s t x) (++-thm₁ s)

  mutual
    replace-var-id : ∀ {m} (t : Term m) -> replace var t ≡ t
    replace-var-id (Unification.var x) = refl
    replace-var-id (Unification.con s ts) = cong (con s) (replaceChildren-var-id ts)

    replaceChildren-var-id : ∀ {m n} -> (ts : Vec (Term m) n) -> replaceChildren var ts ≡ ts
    replaceChildren-var-id [] = refl
    replaceChildren-var-id (x ∷ ts) = cong₂ _∷_ (replace-var-id x) (replaceChildren-var-id ts)

  mutual

    replace-var-id' : ∀ {n m} (f : Fin n -> Term m) (t : Term n)  ->
      replace (\x -> replace var (f x)) t ≡ replace f t
    replace-var-id' f (Unification.var x) = replace-var-id (f x)
    replace-var-id' f (Unification.con s ts) = cong (con s) (replaceChildren-var-id' f ts)

    replaceChildren-var-id' : ∀ {m n k} -> (f : Fin m -> Term k) (ts : Vec (Term m) n) ->
      replaceChildren (\x -> replace var (f x)) ts ≡ replaceChildren f ts
    replaceChildren-var-id' f [] = refl
    replaceChildren-var-id' f (x ∷ ts) = cong₂ _∷_ (replace-var-id' f x) (replaceChildren-var-id' f ts)

  ++-lem₁ : ∀ {m n} (s : Subst m n) (t : Term (suc m)) (t' : Term m) (x : Fin (suc m)) ->
       replace (apply s) (replace (t' for x) t) ≡ replace (\x' -> replace (apply s) (_for_ t' x x')) t
  ++-lem₁ Unification.nil t t' x
    rewrite replace-var-id (replace (t' for x) t)
    | replace-var-id' (t' for x) t = refl
  ++-lem₁ (Unification.snoc s t x) t₁ t' x₁ = {!!}

  ++-lem₂
    : ∀ {l m n} (s₁ : Subst m n) (s₂ : Subst l m) (t : Term l)
    → replace (apply (s₁ ++ s₂)) t ≡ replace (apply s₁) (replace (apply s₂) t)
  ++-lem₂ s₁ nil t rewrite replace-thm₁ t = refl
  ++-lem₂ {.(suc k)} {m} {n} s₁ (snoc {k} s₂ t₂ x) t = {!!}
    where
    lem = ++-lem₂ s₁ s₂ (replace (t₂ for x) t)

  ++-thm₂
    : ∀ {l m n} (s₁ : Subst m n) (s₂ : Subst l m) (x : Fin l)
    → apply (s₁ ++ s₂) x ≡ (apply s₁ ◇ apply s₂) x
  ++-thm₂ s₁ nil x = refl
  ++-thm₂ s₁ (snoc s₂ t y) x with thick y x
  ++-thm₂ s₁ (snoc s₂ t y) x | just t' = ++-thm₂ s₁ s₂ t'
  ++-thm₂ s₁ (snoc s₂ t y) x | nothing = ++-lem₂ s₁ s₂ t

max_stars_repo_name: wenkokke/FirstOrderUnificationInAgda

max_issues_repo_name: wenkokke/FirstOrderUnificationInAgda

max_forks_repo_name: wenkokke/FirstOrderUnificationInAgda