text:
-- Andreas, 2022-03-09, issue #5819, reported by Zilin Chen
--
-- This test uncovered an unsound optimization (8e0fca895b9c6740d9d6c1751ed1e0ecefe63473)
-- in the termination checker which replaced a (stripAllProjections . normalize)
-- by a (iteratively reduce . stripAllProjections).
-- Those reductions on now ill-formed terms triggered the __IMPOSSIBLE__:
-- Incomplete pattern matching when applying Issue5819.dl-iso

open import Agda.Builtin.Unit using (⊤; tt)
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality
open import Agda.Builtin.Sigma renaming (fst to proj₁; snd to proj₂)

data ⊥ : Set where

∃ : {A : Set} (B : A → Set) → Set
∃ B = Σ _ B

_×_ : (A B : Set) → Set
A × B = Σ A λ _ → B

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

_≢_ : {A : Set} (x y : A) → Set
x ≢ y = x ≡ y → ⊥

record Inverse (A B : Set) : Set where
  field
    f         : A → B
    f⁻¹       : B → A
    inverse   : ∀ x → f (f⁻¹ x) ≡ x
open Inverse

data DList : Set
Fresh : (a : ℕ) → (l : DList) → Set

data DList where
  dnil  : DList
  dcons : (a : ℕ) → (l : DList) → Fresh a l → DList

Fresh a dnil = ⊤
Fresh a (dcons b l _) = (a ≢ b) × Fresh a l

data List′ : Set where
  nil′  : List′
  cons′ : ℕ → List′ → List′

Fresh′ : ℕ → List′ → Set
Fresh′ a nil′ = ⊤
Fresh′ a (cons′ b l) = (a ≢ b) × Fresh′ a l

AllFresh : List′ → Set
AllFresh nil′ = ⊤
AllFresh (cons′ a l) = Fresh′ a l × AllFresh l

data DList′ : List′ → Set → Set₁ where
  dnil′  : DList′ nil′ ⊤
  dcons′ : ∀{l}{prf} → (a : ℕ) → DList′ l prf → DList′ (cons′ a l) (Fresh′ a l × prf)

data DList″ : Set where
  dl″ : (l : List′) → AllFresh l → DList″

undl″-l : DList″ → List′
undl″-l (dl″ l _) = l

undl″-p : DList″ → ∃ AllFresh
undl″-p (dl″ l p) = l , p

-- dl-iso : DList ↔ DList″
dl-iso : Inverse DList DList″
-- f-dl-iso : DList → DList″
-- g-dl-iso : DList″ → DList
-- inverse-dl-iso : ∀ x → f-dl-iso (g-dl-iso x) ≡ x

Fresh→Fresh′ : ∀{a}{l}{l″}
             → (f dl-iso l ≡ l″)
             → Fresh a l
             → Fresh′ a (undl″-l l″)

Fresh→AllFresh : ∀{a}{l}{l″}
               → (f dl-iso l ≡ l″)
               → Fresh a l
               → AllFresh (undl″-l l″)

All/Fresh′→Fresh : ∀{a}{l}{l″}
       → (l ≡ f⁻¹ dl-iso l″)
       → Fresh′ a (undl″-l l″) × AllFresh (undl″-l l″)
       → Fresh a l

f dl-iso dnil = dl″ nil′ tt
f dl-iso (dcons a l p)
  = dl″ (cons′ a (undl″-l (f dl-iso l)))
        ((Fresh→Fresh′ {l = l}{l″ = f dl-iso l} refl p) ,
         (Fresh→AllFresh {a = a}{l = l}{l″ = f dl-iso l} refl p))

f⁻¹ dl-iso (dl″ nil′ p) = dnil
f⁻¹ dl-iso (dl″ (cons′ a l′) p)
  = dcons a (f⁻¹ dl-iso (dl″ l′ (proj₂ p)))
            (All/Fresh′→Fresh {l″ = dl″ l′ (proj₂ p)} refl p)

-- Can't do any further, otherwise an Agda bug occurs.
inverse dl-iso x = invˡ
  where
  invˡ : ∀{x} → f dl-iso (f⁻¹ dl-iso x) ≡ x
  invˡ {dl″ nil′ _} = refl
  invˡ {dl″ (cons′ a l) p} rewrite invˡ {dl″ l {!!}} = {!!}  -- add "rewrite invˡ {dl″ l ?}" (w/o quotes) to the left of the = sign and C-c C-l

Fresh→Fresh′ {a} {dnil} eq p rewrite sym eq = tt
Fresh→Fresh′ {a} {dcons a₁ l x} eq p rewrite sym eq
  = proj₁ p ,  Fresh→Fresh′ {l″ = f dl-iso l} refl (proj₂ p)

Fresh→AllFresh {l = dnil} eq p rewrite sym eq = tt
Fresh→AllFresh {l = dcons a l x} eq p rewrite sym eq
  = (Fresh→Fresh′ {l″ = f dl-iso l} refl x) , Fresh→AllFresh {a = a}{l = l}{l″ = f dl-iso l} refl x

All/Fresh′→Fresh {a} {l″ = dl″ nil′ x} eq p rewrite eq = tt
All/Fresh′→Fresh {a} {l″ = dl″ (cons′ b l) x} eq p rewrite eq
  = (proj₁ (proj₁ p)) , {!All/Fresh′→Fresh!}  -- put "All/Fresh′→Fresh" in the hole and C-c C-r

-- WAS: internal error in reduction machinery
-- SHOULD: fail with termination error


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

open import HoTT
open import homotopy.HSpace

module homotopy.EM1HSpace where

module EM₁HSpace {i} (A : Group i) (A-abelian : is-abelian A) where

  module A = Group A
  open EM₁ A

  mult-loop : (g : A.El) (x : EM₁) → x == x
  mult-loop g = EM₁-elim
    {P = λ x → x == x}
    (λ _ → =-preserves-level _ emlevel)
    (emloop g)
    loop'
    (set-↓-has-all-paths-↓ (emlevel embase embase))
    (λ _ _ → set-↓-has-all-paths-↓ (emlevel embase embase))
    where
    abstract
      loop' : (g' : A.El) → emloop g == emloop g [ (λ x → x == x) ↓ emloop g' ]
      loop' g' = ↓-idf=idf-in $
        emloop g ∙ emloop g'     =⟨ ! (emloop-comp g g') ⟩
        emloop (A.comp g g')      =⟨ ap emloop (A-abelian g g') ⟩
        emloop (A.comp g' g)      =⟨ emloop-comp g' g ⟩
        emloop g' ∙ emloop g     =⟨ ∙=∙' (emloop g') (emloop g) ⟩
        emloop g' ∙' emloop g    ∎

  mult-hom : GroupHom A
    (Ω^S-group 0 ((EM₁ → EM₁) , (λ x → x)) (Π-level (λ _ → emlevel)))
  mult-hom = record {f = f; pres-comp = pres-comp}
    where
    f = λ g → λ= (mult-loop g)

    pres-comp = λ g₁ g₂ →
      ap λ= (λ= (EM₁-elim
        {P = λ x → mult-loop (A.comp g₁ g₂) x
                == mult-loop g₁ x ∙ mult-loop g₂ x}
        (λ _ →  =-preserves-level _ (=-preserves-level _ emlevel))
        (emloop-comp g₁ g₂)
        (λ _ → prop-has-all-paths-↓ (emlevel _ _ _ _))
        (set-↓-has-all-paths-↓ (=-preserves-level _ (emlevel _ _)))
        (λ _ _ → set-↓-has-all-paths-↓ (=-preserves-level _ (emlevel _ _)))))
      ∙ ! (∙-λ= _ _)

  mult : EM₁ → EM₁ → EM₁
  mult = EM₁-rec {C = EM₁ → EM₁} (Π-level (λ _ → emlevel)) (λ x → x) mult-hom

  H-EM₁ : HSpaceStructure EM₁
  H-EM₁ = record { e = embase; μ = mult; μ-e-l = μ-e-l; μ-e-r = μ-e-r; μ-coh = μ-coh }
    where
    μ-e-l : (x : EM₁) → mult embase x == x
    μ-e-l = EM₁-elim
      {P = λ x → mult embase x == x}
      (λ _ → =-preserves-level 1 emlevel)
      idp
      (λ g → ↓-app=idf-in $ ∙'-unit-l (emloop g) ∙ (! (ap-idf (emloop g)))
                            ∙ ! (∙-unit-r (ap (mult embase) (emloop g))))
      (set-↓-has-all-paths-↓ (emlevel _ _))
      (λ _ _ → set-↓-has-all-paths-↓ (emlevel _ _))

    μ-e-r : (x : EM₁) → mult x embase == x
    μ-e-r = EM₁-elim
      {P = λ x → mult x embase == x}
      (λ _ → =-preserves-level 1 emlevel)
      idp
      (λ g → ↓-app=idf-in $
         idp ∙' emloop g
           =⟨ ∙'-unit-l (emloop g) ⟩
         emloop g
           =⟨ ! (app=-β (mult-loop g) embase) ⟩
         app= (λ= (mult-loop g)) embase
           =⟨ ! (EM₁Rec.emloop-β {C = EM₁ → EM₁}
                   (Π-level (λ _ → emlevel)) (λ x → x) mult-hom g)
              |in-ctx (λ w → app= w embase) ⟩
         app= (ap mult (emloop g)) embase
           =⟨ ∘-ap (λ f → f embase) mult (emloop g) ⟩
         ap (λ z → mult z embase) (emloop g)
           =⟨ ! (∙-unit-r (ap (λ z → mult z embase) (emloop g))) ⟩
         ap (λ z → mult z embase) (emloop g) ∙ idp ∎)
      (set-↓-has-all-paths-↓ (emlevel _ _))
      (λ _ _ → set-↓-has-all-paths-↓ (emlevel _ _))

    μ-coh : μ-e-l embase == μ-e-r embase
    μ-coh = idp

  open HSpaceStructure H-EM₁

ext: agda

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Format strings for Printf and Scanf
------------------------------------------------------------------------

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

module Text.Format where

open import Level using (0ℓ)
open import Category.Applicative
open import Data.List.Base as List
open import Data.Product
open import Data.Product.Nary.NonDependent
open import Data.Sum.Base
import Data.Sum.Categorical.Left as Sumₗ
open import Function
open import Function.Nary.NonDependent using (0ℓs; Sets)
open import Strict

-- Formatted types
open import Data.Char.Base
open import Data.Integer.Base
open import Data.Float
open import Data.Nat.Base
open import Data.String.Base

------------------------------------------------------------------------
-- Basic types

data Chunk : Set where
  `ℕ `ℤ `Float `Char `String : Chunk
  Raw : String → Chunk

Format : Set
Format = List Chunk

------------------------------------------------------------------------
-- Semantics

size : Format → ℕ
size = List.sum ∘′ List.map λ { (Raw _) → 0; _ → 1 }

-- Meaning of a format as a list of value types

⟦_⟧ : (fmt : Format) → Sets (size fmt) 0ℓs
⟦ []           ⟧ = _
⟦ `ℕ      ∷ cs ⟧ = ℕ      , ⟦ cs ⟧
⟦ `ℤ      ∷ cs ⟧ = ℤ      , ⟦ cs ⟧
⟦ `Float  ∷ cs ⟧ = Float  , ⟦ cs ⟧
⟦ `Char   ∷ cs ⟧ = Char   , ⟦ cs ⟧
⟦ `String ∷ cs ⟧ = String , ⟦ cs ⟧
⟦ Raw _   ∷ cs ⟧ =          ⟦ cs ⟧

------------------------------------------------------------------------
-- Lexer: from Strings to Formats

-- Lexing may fail. To have a useful error message, we defined the following
-- enumerated type

data Error : Set where
  UnexpectedEndOfString : String → Error
  -- ^ expected a type declaration; found an empty string
  InvalidType : String → Char → String → Error
  -- ^ invalid type declaration
  --   return a focus: prefix processed, character causing failure, rest

lexer : String → Error ⊎ List Chunk
lexer input = loop [] [] (toList input) where

  open RawApplicative (Sumₗ.applicative Error 0ℓ)

  -- Type synonyms used locally to document the code
  RevWord = List Char -- Mere characters accumulated so far
  Prefix  = RevWord   -- Prefix of the input String already read

  toRevString : RevWord → String
  toRevString = fromList ∘′ reverse

  -- Push a Raw token if we have accumulated some mere characters
  push : RevWord → List Chunk → List Chunk
  push [] ks = ks
  push cs ks = Raw (toRevString cs) ∷ ks

  -- Main loop
  loop : RevWord → Prefix → List Char → Error ⊎ List Chunk
  type :           Prefix → List Char → Error ⊎ List Chunk

  loop acc bef []               = pure (push acc [])
  -- escaped '%' character: treat like a mere character
  loop acc bef ('%' ∷ '%' ∷ cs) = loop ('%' ∷ acc) ('%' ∷ '%' ∷ bef) cs
  -- non escaped '%': type declaration following
  loop acc bef ('%' ∷ cs)       = push acc <$> type ('%' ∷ bef) cs
  -- mere character: push onto the accumulator
  loop acc bef (c ∷ cs)         = loop (c ∷ acc) (c ∷ bef) cs

  type bef []       = inj₁ (UnexpectedEndOfString input)
  type bef (c ∷ cs) = _∷_ <$> chunk c ⊛ loop [] (c ∷ bef) cs where

    chunk : Char → Error ⊎ Chunk
    chunk 'd' = pure `ℤ
    chunk 'i' = pure `ℤ
    chunk 'u' = pure `ℕ
    chunk 'f' = pure `Float
    chunk 'c' = pure `Char
    chunk 's' = pure `String
    chunk _   = force′ (toRevString bef) $′ λ prefix →
                force′ (fromList cs)     $′ λ suffix →
                inj₁ (InvalidType prefix c suffix)


text:
------------------------------------------------------------------------------
-- Testing Agsy *without* using the Agda standard library
------------------------------------------------------------------------------

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

-- Tested with the development version of Agda on 15 June 2012.

module FOT.Agsy.NoStd.AgsyNoStd where

-- The equational reasoning from the Agda standard library 0.8.1.
-- open import Relation.Binary.PropositionalEquality
-- open ≡-Reasoning

-- My equational reasoning.
open import FOT.Agsy.NoStd.MyPropositionalEquality
open ≡-Reasoning

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Data/Nat.agda).
infixl 9 _+_

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

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

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

+-assoc : ∀ m n o → m + n + o ≡ m + (n + o)
+-assoc zero    n o = refl  -- via Agsy
+-assoc (suc m) n o = {!!}  -- Agsy fails using my propositional equality

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Tactic.Nat.Subtract.Simplify where

open import Prelude hiding (abs)
open import Builtin.Reflection
open import Tactic.Reflection.Quote
open import Tactic.Reflection
open import Control.Monad.State

open import Tactic.Nat.Reflect
open import Tactic.Nat.NF
open import Tactic.Nat.Exp
open import Tactic.Nat.Auto
open import Tactic.Nat.Auto.Lemmas
open import Tactic.Nat.Simpl.Lemmas
open import Tactic.Nat.Simpl
open import Tactic.Nat.Reflect

open import Tactic.Nat.Subtract.Exp
open import Tactic.Nat.Subtract.Reflect
open import Tactic.Nat.Subtract.Lemmas
open import Tactic.Nat.Less.Lemmas

simplifySubEqn : ∀ eqn ρ → c⟦ eqn ⟧eqn ρ → ⟦ eqn ⟧eqn ρ
simplifySubEqn (a :≡ b) = simplifySubEq a b
simplifySubEqn (a :< b) = simplifySubLess a b

complicateSubEqn : ∀ eqn ρ → ⟦ eqn ⟧eqn ρ → c⟦ eqn ⟧eqn ρ
complicateSubEqn (a :≡ b) = complicateSubEq a b
complicateSubEqn (a :< b) = complicateSubLess a b

⟦_⟧sh : List Eqn → Env Var → Set
⟦ [] ⟧sh ρ = ⊥
⟦ h ∷ [] ⟧sh ρ = ⟦ h ⟧eqn ρ
⟦ h ∷ g  ⟧sh ρ = ⟦ h ⟧eqn ρ → ⟦ g ⟧sh ρ

⟦_⟧shs : List Eqn → Env Var → Set
⟦ [] ⟧shs ρ = ⊥
⟦ h ∷ [] ⟧shs ρ = c⟦ h ⟧eqn ρ
⟦ h ∷ g  ⟧shs ρ = c⟦ h ⟧eqn ρ → ⟦ g ⟧shs ρ

simplifySubH : ∀ goal ρ → ⟦ goal ⟧shs ρ → ⟦ goal ⟧sh ρ
simplifySubH []            ρ ()
simplifySubH (h ∷ [])     ρ H = simplifySubEqn h ρ H
simplifySubH (h ∷ h₂ ∷ g) ρ H = λ H₁ → simplifySubH (h₂ ∷ g) ρ $ H (complicateSubEqn h ρ H₁)

simplifysub-tactic : Term → Type → TC Term
simplifysub-tactic prf g =
  inferType prf >>= λ h →
  let t = pi (vArg h) (abs "_" (weaken 1 g)) in
  caseM termToSubHyps t of
  λ { nothing → pure $ failedProof (quote invalidGoal) t
    ; (just (goal , Γ)) → pure $
      def (quote flip)
        $ vArg (def (quote simplifySubH)
                    ( vArg (` goal)
                    ∷ vArg (quotedEnv Γ) ∷ [] ))
        ∷ vArg prf ∷ []
    }

simplifygoal-tactic : Type → TC Term
simplifygoal-tactic t =
  caseM termToSubHyps t of λ
  { nothing → pure $ failedProof (quote invalidGoal) t
  ; (just (goal , Γ)) → pure $
      def (quote simplifySubH)
        $ vArg (` goal)
        ∷ vArg (quotedEnv Γ)
        ∷ []
  }

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Groups.WedgeOfSpheres where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Sigma.Base

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.Groups.Wedge
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.Data.Int renaming (_+_ to _ℤ+_)

open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge
open import Cubical.HITs.Pushout
open import Cubical.HITs.Truncation renaming (elim to trElim) hiding (map ; elim2)
open import Cubical.Algebra.Group renaming (ℤ to ℤGroup ; Bool to BoolGroup ; Unit to UnitGroup)
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to sRec2 ; elim to sElim)

S¹⋁S¹ : Type₀
S¹⋁S¹ = S₊∙ 1 ⋁ S₊∙ 1

S²⋁S¹⋁S¹ : Type₀
S²⋁S¹⋁S¹ = S₊∙ 2 ⋁ (S¹⋁S¹ , inl base)

------------- H⁰(S¹⋁S¹) ------------
H⁰-S¹⋁S¹ : GroupIso (coHomGr 0 S¹⋁S¹) ℤGroup
H⁰-S¹⋁S¹ = H⁰-connected (inl base) (wedgeConnected _ _ (Sn-connected 0) (Sn-connected 0))

------------- H¹(S¹⋁S¹) ------------
H¹-S¹⋁S¹ : GroupIso (coHomGr 1 S¹⋁S¹) (DirProd ℤGroup ℤGroup)
H¹-S¹⋁S¹ =  (Hⁿ-⋁ _ _ 0) □ GroupIsoDirProd coHom1S1≃ℤ coHom1S1≃ℤ

------------- H⁰(S²⋁S¹⋁S¹) ---------
H⁰-S²⋁S¹⋁S¹ : GroupIso (coHomGr 0 S²⋁S¹⋁S¹) ℤGroup
H⁰-S²⋁S¹⋁S¹ = H⁰-connected (inl north)
                  (wedgeConnected _ _
                    (Sn-connected 1)
                    (wedgeConnected _ _
                      (Sn-connected 0)
                      (Sn-connected 0)))

------------- H¹(S²⋁S¹⋁S¹) ---------
H¹-S²⋁S¹⋁S¹ : GroupIso (coHomGr 1 S²⋁S¹⋁S¹) (DirProd ℤGroup ℤGroup)
H¹-S²⋁S¹⋁S¹ =
    Hⁿ-⋁ (S₊∙ 2) (S¹⋁S¹ , inl base) 0
  □ GroupIsoDirProd (H¹-Sⁿ≅0 0) H¹-S¹⋁S¹
  □ lUnitGroupIso

------------- H²(S²⋁S¹⋁S¹) ---------

H²-S²⋁S¹⋁S¹ : GroupIso (coHomGr 2 S²⋁S¹⋁S¹) ℤGroup
H²-S²⋁S¹⋁S¹ =
  compGroupIso
  (Hⁿ-⋁ _ _ 1)
  (GroupIsoDirProd {B = UnitGroup}
    (Hⁿ-Sⁿ≅ℤ 1)
    ((Hⁿ-⋁ _ _ 1)  □ GroupIsoDirProd (Hⁿ-S¹≅0 0) (Hⁿ-S¹≅0 0) □ rUnitGroupIso)
  □ rUnitGroupIso)

private
  open IsGroupHom
  open Iso

  to₂ : coHom 2 S²⋁S¹⋁S¹ → ℤ
  to₂ = fun (fst H²-S²⋁S¹⋁S¹)
  from₂ : ℤ → coHom 2 S²⋁S¹⋁S¹
  from₂ = inv (fst H²-S²⋁S¹⋁S¹)

  to₁ : coHom 1 S²⋁S¹⋁S¹ → ℤ × ℤ
  to₁ = fun (fst H¹-S²⋁S¹⋁S¹)
  from₁ : ℤ × ℤ → coHom 1 S²⋁S¹⋁S¹
  from₁ = inv (fst H¹-S²⋁S¹⋁S¹)

  to₀ : coHom 0 S²⋁S¹⋁S¹ → ℤ
  to₀ = fun (fst H⁰-S²⋁S¹⋁S¹)
  from₀ : ℤ → coHom 0 S²⋁S¹⋁S¹
  from₀ = inv (fst H⁰-S²⋁S¹⋁S¹)

{-

-- Compute pretty fast
test1 : to₁ (from₁ (1 , 0) +ₕ from₁ (0 , 1)) ≡ (1 , 1)
test1 = refl

-- Computes, but only when computing some smaller numbers first
test2 : to₁ (from₁ (50 , 3) +ₕ from₁ (2 , -2)) ≡ (52 , 1)
test2 = refl

test3 : to₂ (from₂ 0) ≡ 0
test3 = refl

test4 : to₂ (from₂ 3) ≡ 3
test4 = refl

test5 : to₂ (from₂ 1 +ₕ from₂ 1) ≡ 2
test5 = refl
-}

  g : S²⋁S¹⋁S¹ → ∥ Susp S¹ ∥ 4
  g (inl x) = ∣ x ∣
  g (inr x) = 0ₖ _
  g (push a i) = 0ₖ _

  G = ∣ g ∣₂

{- Does not compute:
test₀ : to₂ (G +ₕ G) ≡ 2
test₀ = refl

but this does:
test₀ : to₂ (G +'ₕ G) ≡ 2
test₀ = refl
-}


text:
------------------------------------------------------------------------
-- Vectors, defined as functions from finite sets
------------------------------------------------------------------------

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

open import Equality

module Vec.Function
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude

open import Bijection eq using (_↔_)
open Derived-definitions-and-properties eq
open import Function-universe eq hiding (id; _∘_)
open import List eq using (length)
open import Surjection eq using (_↠_; ↠-≡)

private
  variable
    a   : Level
    A B : Type a
    n   : ℕ
    k   : Kind

------------------------------------------------------------------------
-- The type

-- Vectors.

Vec : ∀ {a} → Type a → ℕ → Type a
Vec A n = Fin n → A

-- Nil.

nil : Vec A zero
nil = λ ()

-- Cons.

cons : A → Vec A n → Vec A (suc n)
cons x xs = [ const x , xs ]

------------------------------------------------------------------------
-- Some simple functions

-- Finds the element at the given position.

index : Vec A n → Fin n → A
index = id

-- Applies the function to every element in the vector.

map : (A → B) → Vec A n → Vec B n
map f xs = f ∘ xs

-- Constructs a vector containing a certain number of copies of the
-- given element.

replicate : A → Vec A n
replicate = const

-- The head of the vector.

head : Vec A (suc n) → A
head = _$ fzero

-- The tail of the vector.

tail : Vec A (suc n) → Vec A n
tail = _∘ fsuc

-- Updates the element at the given position.

infix 3 _[_≔_]

_[_≔_] : Vec A n → Fin n → A → Vec A n
_[_≔_] {n = zero}  _  ()       _
_[_≔_] {n = suc _} xs fzero    x = cons x (tail xs)
_[_≔_] {n = suc _} xs (fsuc i) x = cons (head xs) (tail xs [ i ≔ x ])

------------------------------------------------------------------------
-- Some properties

-- Empty lists are equal to nil (assuming extensionality).

empty≡nil :
  {A : Type a} →
  Extensionality lzero a →
  {xs : Vec A zero} →
  xs ≡ nil
empty≡nil ext = apply-ext ext λ ()

-- A non-empty list is equal to its head consed onto its tail
-- (assuming extensionality).

non-empty≡cons-head-tail :
  {A : Type a} →
  Extensionality lzero a →
  (xs : Vec A (suc n)) →
  xs ≡ cons (head xs) (tail xs)
non-empty≡cons-head-tail ext _ =
  apply-ext ext [ (λ _ → refl _) , (λ _ → refl _) ]

------------------------------------------------------------------------
-- Conversions to and from lists

-- Vectors can be converted to lists.

to-list : Vec A n → List A
to-list {n = zero}  _  = []
to-list {n = suc _} xs = head xs ∷ to-list (tail xs)

-- Lists can be converted to vectors.

from-list : (xs : List A) → Vec A (length xs)
from-list []       = nil
from-list (x ∷ xs) = cons x (from-list xs)

-- There is a split surjection from ∃ (Vec A) to List A.

∃Vec↠List : ∃ (Vec A) ↠ List A
∃Vec↠List {A = A} = record
  { logical-equivalence = record
    { to   = to-list ∘ proj₂
    ; from = λ xs → length xs , from-list xs
    }
  ; right-inverse-of = to∘from
  }
  where
  to∘from : (xs : List A) → to-list (from-list xs) ≡ xs
  to∘from []       = refl _
  to∘from (x ∷ xs) = cong (x ∷_) (to∘from xs)

-- ∃ (Vec A) is equivalent to List A (assuming extensionality).

∃Vec≃List :
  {A : Type a} →
  ∃ (Vec A) ↝[ lzero ∣ a ] List A
∃Vec≃List {a = a} {A = A} =
  generalise-ext?
    (_↠_.logical-equivalence ∃Vec↠List)
    (λ ext →
         _↠_.right-inverse-of ∃Vec↠List
       , uncurry (from∘to ext))
  where
  tail′ : A → ∃ (Vec A) ↠ ∃ (Vec A)
  tail′ y = record
    { logical-equivalence = record
      { to   = λ where
                 (suc n , xs)  → n , tail xs
                 xs@(zero , _) → xs
      ; from = Σ-map suc (cons y)
      }
    ; right-inverse-of = refl
    }

  from∘to :
    Extensionality lzero a →
    ∀ n (xs : Vec A n) →
    (length (to-list xs) , from-list (to-list xs)) ≡ (n , xs)
  from∘to ext zero xs =
    (length {A = A} [] , nil)  ≡⟨ cong (zero ,_) $ sym $ empty≡nil ext ⟩∎
    (zero , xs)                ∎

  from∘to ext (suc n) xs =                                        $⟨ from∘to ext n (tail xs) ⟩
    (length (to-list (tail xs)) , from-list (to-list (tail xs)))
      ≡
    (n , tail xs)                                                 ↝⟨ _↠_.from $ ↠-≡ (tail′ (head xs)) ⟩

    (length (to-list xs) , from-list (to-list xs))
      ≡
    (suc n , cons (head xs) (tail xs))                            ↝⟨ ≡⇒↝ _ $ cong (λ ys → (_ , from-list (to-list xs)) ≡ (_ , ys)) $ sym $
                                                                     non-empty≡cons-head-tail ext xs ⟩□
    (length (to-list xs) , from-list (to-list xs))
      ≡
    (suc n , xs)                                                  □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

open import HoTT
import homotopy.ConstantToSetExtendsToProp as ConstExt

{-
          q[_]ᴳ
     G/Q ↞------ G
      ↑          ↑
   φ₂ ╎          ╎ inject
      ↑          ↑
      H ↞------- P
           φ₁

     Then, H ≃ᴳ P/Q.
-}

module groups.PropQuotUniqueFactorization
  {i j l₁ l₂} {G : Group i} {H : Group j}
  (P : SubgroupProp G l₁)
  (Q : NormalSubgroupProp G l₂)
  (φ₁ : Subgroup P →ᴳ H) (φ₁-is-surj : is-surjᴳ φ₁)
  (φ₂ : H →ᴳ QuotGroup Q) (φ₂-is-inj : is-injᴳ φ₂)
  (φ-comm : ∀ p → GroupHom.f (φ₂ ∘ᴳ φ₁) p == q[ fst p ])
  where

  private
    module G = Group G
    module H = Group H
    module P = Subgroup P
    module φ₁ = GroupHom φ₁
    module φ₂ = GroupHom φ₂

    P/Q-prop : NormalSubgroupProp (Subgroup P) l₂
    P/Q-prop = quot-of-sub P Q

    P/Q : Group (lmax i (lmax l₁ l₂))
    P/Q = QuotGroup P/Q-prop
    module P/Q = Group P/Q

    module _ (k : Group.El H) where
      H-to-P/Q-f' : hfiber φ₁.f k → P/Q.El
      H-to-P/Q-f' (p , _) = q[ p ]

      abstract
        H-to-P/Q-f'-const : (hf₁ hf₂ : hfiber φ₁.f k)
          → H-to-P/Q-f' hf₁ == H-to-P/Q-f' hf₂
        H-to-P/Q-f'-const (h₁ , r₁) (h₂ , r₂) =
          quot-relᴳ {P = P/Q-prop} $ <– (quot-relᴳ-equiv {P = Q}) $
            ! (φ-comm h₁) ∙ ap φ₂.f (r₁ ∙ ! r₂) ∙ φ-comm h₂

      module HToP/Q = ConstExt P/Q.El-is-set
        H-to-P/Q-f' H-to-P/Q-f'-const

      H-to-P/Q-f : Trunc -1 (hfiber φ₁.f k) → P/Q.El
      H-to-P/Q-f = HToP/Q.ext

      H-to-P/Q-f-is-const : ∀ hf₁ hf₂ → H-to-P/Q-f hf₁ == H-to-P/Q-f hf₂
      H-to-P/Q-f-is-const = HToP/Q.ext-is-const

    abstract
      H-to-P/Q-f-comp : (k₁ k₂ : H.El)
        → (hf₁₂ : Trunc -1 (hfiber φ₁.f (H.comp k₁ k₂)))
        → (hf₁ : Trunc -1 (hfiber φ₁.f k₁))
        → (hf₂ : Trunc -1 (hfiber φ₁.f k₂))
        → H-to-P/Q-f (H.comp k₁ k₂) hf₁₂ == P/Q.comp (H-to-P/Q-f k₁ hf₁) (H-to-P/Q-f k₂ hf₂)
      H-to-P/Q-f-comp k₁ k₂ hf₁₂ = Trunc-elim
        (λ hf₁ → Π-is-prop λ hf₂ →
          P/Q.El-is-set _ (P/Q.comp (H-to-P/Q-f k₁ hf₁) (H-to-P/Q-f k₂ hf₂)))
        (λ{(p₁ , r₁) → Trunc-elim
          (λ hf₂ → P/Q.El-is-set _ (P/Q.comp q[ p₁ ] (H-to-P/Q-f k₂ hf₂)))
          (λ{(p₂ , r₂) → H-to-P/Q-f-is-const (H.comp k₁ k₂)
              hf₁₂ [ P.comp p₁ p₂ , φ₁.pres-comp p₁ p₂ ∙ ap2 H.comp r₁ r₂ ]})})

  H-to-P/Q : H →ᴳ P/Q
  H-to-P/Q = record {
    f = λ k → H-to-P/Q-f k (φ₁-is-surj k);
    pres-comp = λ k₁ k₂ → H-to-P/Q-f-comp k₁ k₂
      (φ₁-is-surj (H.comp k₁ k₂)) (φ₁-is-surj k₁) (φ₁-is-surj k₂)}

  H-iso-P/Q : H ≃ᴳ P/Q
  H-iso-P/Q = H-to-P/Q , is-eq to from to-from from-to where
    to : H.El → P/Q.El
    to = λ k → H-to-P/Q-f k (φ₁-is-surj k)

    from : P/Q.El → H.El
    from = SetQuot-rec H.El-is-set
      (λ p → φ₁.f p)
      (λ {p₁} {p₂} q'p₁p₂⁻¹ → φ₂-is-inj (φ₁.f p₁) (φ₁.f p₂) $
        φ-comm p₁ ∙ quot-relᴳ {P = Q} q'p₁p₂⁻¹ ∙ ! (φ-comm p₂))

    abstract
      to-from : ∀ p/q → to (from p/q) == p/q
      to-from = SetQuot-elim (λ p/q → raise-level -1 $ P/Q.El-is-set _ p/q)
        (λ p → H-to-P/Q-f-is-const (φ₁.f p) (φ₁-is-surj (φ₁.f p)) [ p , idp ])
        (λ _ → prop-has-all-paths-↓ $ P/Q.El-is-set _ _)

      from-to' : ∀ k (hf : Trunc -1 (hfiber φ₁.f k)) → from (H-to-P/Q-f k hf) == k
      from-to' k = Trunc-elim (λ hf → H.El-is-set (from (H-to-P/Q-f k hf)) k) (λ{(p , r) → r})

      from-to : ∀ k → from (to k) == k
      from-to k = from-to' k (φ₁-is-surj k)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --safe --without-K #-}
open import Generics.Prelude
open import Generics.Telescope
open import Generics.Desc
open import Agda.Builtin.Reflection

module Generics.Helpers
         P I
         {levelArgRel : Level → Level}
         (ArgRel      : ∀ {a} → Set a → Set (levelArgRel a))
         {levelArgIrr : Level → Level}
         (ArgIrr      : ∀ {a} → Set a → Set (levelArgIrr a))
         (Ind         : ∀ {V} (C : ConDesc P V I) → Setω)
         where

  data ConHelper p {V} : ConDesc P V I → Setω where
    instance var    : ∀ {f} → ConHelper p (var f)
             pi-irr : ∀ {ℓ n v q}
                      {S : ⟦ P , V ⟧xtel → Set ℓ}
                      (let ai = n , arg-info v (modality irrelevant q))
                      {C : ConDesc P (V ⊢< ai > S) I}
                    → ⦃ ∀ {v} → ArgIrr (S (p , v)) ⦄
                    → ⦃ ConHelper p C              ⦄
                    → ConHelper p (π ai S C)
             pi-rel : ∀ {ℓ n v q}
                      {S : ⟦ P , V ⟧xtel → Set ℓ}
                      (let ai = n , arg-info v (modality relevant q))
                      {C : ConDesc P (V ⊢< ai > S) I}
                    → ⦃ ∀ {v} → ArgRel (S (p , v)) ⦄
                    → ⦃ ConHelper p C              ⦄
                    → ConHelper p (π ai S C)
             prod   : {A B : ConDesc P V I}
                    → ⦃ Ind A         ⦄
                    → ⦃ ConHelper p B ⦄
                    → ConHelper p (A ⊗ B)

  data Helpers p : {n : ℕ} → DataDesc P I n → Setω where
    instance nil  : Helpers p []
             cons : ∀ {n} {C : ConDesc  P ε I}
                          {D : DataDesc P I n}
                  → ⦃ ConHelper p C ⦄
                  → ⦃ Helpers p D   ⦄
                  → Helpers p (C ∷ D)

  lookupHelper : ∀ {n} {D : DataDesc P I n} {p}
                 (HD : Helpers p D) (k : Fin n)
               → ConHelper p (lookupCon D k)
  lookupHelper (cons ⦃ HC ⦄ ⦃ HD ⦄) zero    = HC
  lookupHelper (cons ⦃ HC ⦄ ⦃ HD ⦄) (suc k) = lookupHelper HD k

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
open import Common.Prelude hiding (_>>=_)
open import Common.Reflection
open import Common.Equality

set₀ = sort (lit 0)
set! = sort unknown

-- Definitions added by tactics always use the original context, and thus are not
-- affected by inContext and extendContext. The reason for this is that they are added
-- to the module of the macro call, so they need to live in the context of that module
-- or things break.

freshFun : Type → List Clause → Tactic
freshFun t cs hole =
  freshName "fresh" >>= λ n →
  inContext [] (define (vArg n) (funDef t cs)) >>= λ _ →
  unify hole (def n [])

macro
  ack : Tactic
  ack = freshFun set! (clause [] set₀ ∷ [])

  theA : Tactic
  theA = freshFun set₀ (clause [] (var 0 []) ∷ [])

module Foo (A : Set) where
  foo : Set
  foo = theA

  bar : Set₁
  bar = ack

check : {A : Set} → Foo.foo A ≡ A
check = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --universe-polymorphism #-}

module Categories.NaturalTransformation.Core where

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

open import Categories.Support.Equivalence
open import Categories.Category
open import Categories.Functor.Core renaming (id to idF; _∘_ to _∘F_)

record NaturalTransformation {o ℓ e o′ ℓ′ e′}
                             {C : Category o ℓ e}
                             {D : Category o′ ℓ′ e′}
                             (F G : Functor C D) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  private module C = Category C
  private module D = Category D
  private module F = Functor F
  private module G = Functor G
  open F using (F₀; F₁)
  open G using () renaming (F₀ to G₀; F₁ to G₁)

  field
    η : ∀ X → D [ F₀ X , G₀ X ]
    .commute : ∀ {X Y} (f : C [ X , Y ]) → D.CommutativeSquare (F₁ f) (η X) (η Y) (G₁ f)

  op : NaturalTransformation G.op F.op
  op = record
    { η = η
    ; commute = λ f → D.Equiv.sym (commute f)
    }

id : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F : Functor C D} → NaturalTransformation F F
id {C = C} {D} {F} = record
  { η = λ _ → D.id
  ; commute = commute′
  }
  where
  module C = Category C
  module D = Category D
  module F = Functor F
  open F

  .commute′ : ∀ {X Y} (f : C [ X , Y ]) → D [ D [ D.id ∘ F₁ f ] ≡ D [ F₁ f ∘ D.id ] ]
  commute′ f = begin
                 D [ D.id ∘ F₁ f ]
               ↓⟨ D.identityˡ ⟩
                 F₁ f
               ↑⟨ D.identityʳ ⟩
                 D [ F₁ f ∘ D.id ]
               ∎
    where
    open D.HomReasoning

infixr 9 _∘₁_ _∘₀_

-- "Vertical composition"
_∘₁_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁}
        {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁}
        {F G H : Functor C D}
    → NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
_∘₁_ {C = C} {D} {F} {G} {H} X Y = record
  { η = λ q → D [ X.η q ∘ Y.η q ]
  ; commute = commute′
  }
  where
  module C = Category C
  module D = Category D
  module F = Functor F
  module G = Functor G
  module H = Functor H
  module X = NaturalTransformation X
  module Y = NaturalTransformation Y
  open F
  open G renaming (F₀ to G₀; F₁ to G₁)
  open H renaming (F₀ to H₀; F₁ to H₁)

  .commute′ : ∀ {A B} (f : C [ A , B ]) → D [ D [ D [ X.η B ∘ Y.η B ] ∘ F₁ f ] ≡ D [ H₁ f ∘ D [ X.η A ∘  Y.η A ] ] ]
  commute′ {A} {B} f =
           begin
             D [ D [ X.η B ∘ Y.η B ] ∘ F₁ f ]
           ↓⟨ D.assoc ⟩
             D [ X.η B ∘ D [ Y.η B ∘ F₁ f ] ]
           ↓⟨ D.∘-resp-≡ʳ (Y.commute f) ⟩
             D [ X.η B ∘ D [ G₁ f ∘ Y.η A ] ]
           ↑⟨ D.assoc ⟩
             D [ D [ X.η B ∘ G₁ f ] ∘ Y.η A ]
           ↓⟨ D.∘-resp-≡ˡ (X.commute f) ⟩
             D [ D [ H₁ f ∘ X.η A ] ∘ Y.η A ]
           ↓⟨ D.assoc ⟩
             D [ H₁ f ∘ D [ X.η A ∘ Y.η A ] ]
           ∎
    where
    open D.HomReasoning

-- "Horizontal composition"
_∘₀_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
        {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
        {F G : Functor C D} {H I : Functor D E}
    → NaturalTransformation H I → NaturalTransformation F G → NaturalTransformation (H ∘F F) (I ∘F G)
_∘₀_ {C = C} {D} {E} {F} {G} {H} {I} Y X = record
  { η = λ q → E [ I₁ (X.η q) ∘ Y.η (F₀ q) ]
  ; commute = commute′
  }
  where
  module C = Category C
  module D = Category D
  module E = Category E
  module F = Functor F
  module G = Functor G
  module H = Functor H
  module I = Functor I
  module X = NaturalTransformation X
  module Y = NaturalTransformation Y
  open F
  open G renaming (F₀ to G₀; F₁ to G₁; F-resp-≡ to G-resp-≡)
  open H renaming (F₀ to H₀; F₁ to H₁; F-resp-≡ to H-resp-≡)
  open I renaming (F₀ to I₀; F₁ to I₁; F-resp-≡ to I-resp-≡)

  .commute′ : ∀ {A B} (f : C [ A , B ]) → E [ E [ E [ I₁ (X.η B) ∘ Y.η (F₀ B) ] ∘ H₁ (F₁ f) ] ≡ E [ I₁ (G₁ f) ∘ E [ I₁ (X.η A) ∘ Y.η (F₀ A) ] ] ]
  commute′ {A} {B} f =
           begin
             E [ E [ I₁ (X.η B) ∘ Y.η (F₀ B) ] ∘ H₁ (F₁ f) ]
           ↓⟨ E.assoc ⟩
             E [ I₁ (X.η B) ∘ E [ Y.η (F₀ B) ∘ H₁ (F₁ f) ] ]
           ↓⟨ E.∘-resp-≡ʳ (Y.commute (F₁ f)) ⟩
             E [ I₁ (X.η B) ∘ E [ I₁ (F₁ f) ∘ Y.η (F₀ A) ] ]
           ↑⟨ E.assoc ⟩
             E [ E [ I₁ (X.η B) ∘ I₁ (F₁ f) ] ∘ Y.η (F₀ A) ]
           ↑⟨ E.∘-resp-≡ˡ I.homomorphism ⟩
             E [ I₁ (D [ X.η B ∘ F₁ f ]) ∘ Y.η (F₀ A) ]
           ↓⟨ E.∘-resp-≡ˡ (I-resp-≡ (X.commute f)) ⟩
             E [ I₁ (D [ G₁ f ∘ X.η A ]) ∘ Y.η (F₀ A) ]
           ↓⟨ E.∘-resp-≡ˡ I.homomorphism ⟩
             E [ E [ I₁ (G₁ f) ∘ I₁ (X.η A) ] ∘ Y.η (F₀ A) ]
           ↓⟨ E.assoc ⟩
             E [ I₁ (G₁ f) ∘ E [ I₁ (X.η A) ∘ Y.η (F₀ A) ] ]
           ∎
    where
    open E.HomReasoning

infix 4 _≡_

_≡_ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D} → Rel (NaturalTransformation F G) (o ⊔ e′)
_≡_ {D = D} X Y = ∀ {x} → D [ NaturalTransformation.η X x ≡ NaturalTransformation.η Y x ]

.equiv : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D} → IsEquivalence (_≡_ {F = F} {G})
equiv {C = C} {D} {F} {G} = record
  { refl = refl
  ; sym = λ f → sym f
  ; trans = λ f g → trans f g
  }
  where
  open Category.Equiv D

setoid : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D} → Setoid _ _
setoid {F = F} {G} = record
  { Carrier = NaturalTransformation F G
  ; _≈_ = _≡_
  ; isEquivalence = equiv {F = F}
  }

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Incrementalization as term-to-term transformation with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Change.Derive where

open import Nehemiah.Syntax.Type
open import Nehemiah.Syntax.Term
open import Nehemiah.Change.Type
open import Nehemiah.Change.Term

open import Data.Integer

import Parametric.Change.Derive Const ΔBase as Derive

derive-const : Derive.Structure
derive-const (intlit-const n) = intlit (+ 0)
derive-const add-const        = absV 4 (λ s ds t dt → add ds dt)
derive-const minus-const      = absV 2 (λ t dt → minus dt)
derive-const empty-const      = empty
derive-const insert-const     = absV 4 (λ s ds t dt →
  insert (s ⊕₍ int ₎ ds) (t ⊕₍ bag ₎ dt) ⊝ insert s t)
derive-const union-const      = absV 4 (λ s ds t dt → union ds dt)
derive-const negate-const     = absV 2 (λ t dt → negate dt)
derive-const flatmap-const    = absV 4 (λ s ds t dt →
  flatmap (s ⊕₍ int ⇒ bag ₎ ds) (t ⊕₍ bag ₎ dt) ⊝ flatmap s t)
derive-const sum-const        = absV 2 (λ t dt → sum dt)

open Derive.Structure derive-const public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module InferrableFields where

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

data Vec A : ℕ → Set where
  []  : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

record SomeVec A : Set where
  field n      : ℕ
        unpack : Vec A n

open SomeVec using (unpack)

pack : ∀ {A n} → Vec A n -> SomeVec A
pack xs = record { unpack = xs }

data _≡_ {A : Set}(x : A) : A → Set where
  refl : x ≡ x

lemPack : ∀ {A}(xs : SomeVec A) → pack (unpack xs) ≡ xs
lemPack xs = refl


text:
-- {-# OPTIONS -v scope.operators:100 #-}
module Issue675 where

data D : Set where
  d : D → D

Foo : {x : D} → Set₁
Foo {x = D.d x} = Set
-- qualified constructors should also work in hidden arguments

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Functor where

open import Level
import Data.Nat as N

open import Basic
open import Category
open Category.Category

record Functor {c₀ c₁ ℓ c₀′ c₁′ ℓ′} (C : Category c₀ c₁ ℓ) (D : Category c₀′ c₁′ ℓ′) : Set (suc (c₀ ⊔ c₀′ ⊔ c₁ ⊔ c₁′ ⊔ ℓ ⊔ ℓ′)) where
  field
    fobj : Obj C → Obj D
    fmapsetoid : {A B : Obj C} → Map.Map (Homsetoid C A B) (Homsetoid D (fobj A) (fobj B))

  fmap : {A B : Obj C} → Hom C A B → Hom D (fobj A) (fobj B)
  fmap {A} {B} = Map.Map.mapping (fmapsetoid {A} {B})

  field
    preserveId : {A : Obj C} → D [ fmap (id C {A}) ≈ id D {fobj A} ]
    preserveComp : {a b c : Obj C} {f : Hom C b c} {g : Hom C a b} → D [ fmap (C [ f ∘ g ]) ≈ (D [ fmap f ∘ fmap g ]) ]

open Functor

preserveEq : ∀ {c₀ c₁ ℓ c₀′ c₁′ ℓ′} {C : Category c₀ c₁ ℓ} {D : Category c₀′ c₁′ ℓ′} {A B : Obj C} {x y : Hom C A B} (F : Functor C D) → C [ x ≈ y ] → D [ fmap F x ≈ fmap F y ]
preserveEq F xy = Map.Map.preserveEq (fmapsetoid F) xy

compose : ∀ {c₀ c₁ ℓ c₀′ c₁′ ℓ′ c₀″ c₁″ ℓ″} {C : Category c₀ c₁ ℓ} {D : Category c₀′ c₁′ ℓ′} {E : Category c₀″ c₁″ ℓ″} → Functor {c₀′} {c₁′} {ℓ′} {c₀″} {c₁″} {ℓ″} D E → Functor {c₀} {c₁} {ℓ} {c₀′} {c₁′} {ℓ′} C D → Functor {c₀} {c₁} {ℓ} {c₀″} {c₁″} {ℓ″} C E
compose {C = C} {D} {E} G F = record {
  fobj = λ x → fobj G (fobj F x);
  fmapsetoid = record { mapping = λ f → fmap G (fmap F f) ; preserveEq = λ {x} {y} x≈y → begin⟨ E ⟩
    fmap G (fmap F x) ≈⟨ preserveEq G (begin⟨ D ⟩
      fmap F x ≈⟨ preserveEq F x≈y ⟩
      fmap F y ∎) ⟩
    fmap G (fmap F y) ∎
  };
  preserveId = begin⟨ E ⟩
    fmap G (fmap F (id C)) ≈⟨ preserveEq G (preserveId F) ⟩
    fmap G (id D) ≈⟨ preserveId G ⟩
    (id E) ∎;
  preserveComp = λ {_} {_} {_} {f} {g} → begin⟨ E ⟩
    fmap G (fmap F (C [ f ∘ g ])) ≈⟨ preserveEq G (preserveComp F) ⟩
    fmap G (D [ fmap F f ∘ fmap F g ]) ≈⟨ preserveComp G ⟩
    (E [ fmap G (fmap F f) ∘ fmap G (fmap F g) ]) ∎
  }

identity : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) → Functor {c₀} {c₁} {ℓ} {c₀} {c₁} {ℓ} C C
identity C = record {
  fobj = λ x → x ;
  fmapsetoid = record { mapping = λ x → x ; preserveEq = λ x₁ → x₁ } ;
  preserveId = refl-hom C ; preserveComp = refl-hom C }

exp : ∀ {c₀ c₁ ℓ} {C : Category c₀ c₁ ℓ} → Functor C C → N.ℕ → Functor C C
exp {C = C} F N.zero = identity C
exp F (N.suc N.zero) = F
exp F (N.suc n) = compose F (exp F n)

data _[_~_]
  {C₀ C₁ ℓ : Level} (C : Category C₀ C₁ ℓ) {A B : Obj C} (f : Hom C A B)
  : ∀{X Y : Obj C} → Hom C X Y → Set (suc (C₀ ⊔ C₁ ⊔ ℓ)) where
  eqArrow : {g : Hom C A B} → C [ f ≈ g ] → C [ f ~ g ]

eqArrowRefl : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {A B : Obj C} {f : Hom C A B} → C [ f ~ f ]
eqArrowRefl C = eqArrow (refl-hom C)

eqArrowSym : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {X Y Z W : Obj C} {f : Hom C X Y} {g : Hom C Z W} → C [ f ~ g ] → C [ g ~ f ]
eqArrowSym C (eqArrow f~g) = eqArrow (sym-hom C f~g)

eqArrowTrans : ∀ {c₀ c₁ ℓ} (C : Category c₀ c₁ ℓ) {X Y Z W S T : Obj C} {f : Hom C X Y} {g : Hom C Z W} {h : Hom C S T} → C [ f ~ g ] → C [ g ~ h ] → C [ f ~ h ]
eqArrowTrans C (eqArrow f~g) (eqArrow g~h) = eqArrow (trans-hom C f~g g~h)

eqArrowFmap : ∀ {c₀ c₁ ℓ c₀′ c₁′ ℓ′} {C : Category c₀ c₁ ℓ} {D : Category c₀′ c₁′ ℓ′} {X Y Z W : Obj C} {x : Category.Hom C X Y} {y : Category.Hom C Z W} (F : Functor C D) → C [ x ~ y ] → D [ fmap F x ~ fmap F y ]
eqArrowFmap F (eqArrow x~y) = eqArrow (preserveEq F x~y)

equality : ∀ {c₀ c₁ ℓ} {C D : Category c₀ c₁ ℓ} → (F G : Functor C D) → _
equality {C = C} {D} F G = ∀ {A B : Obj C} (f : Hom C A B) → D [ fmap F f ~ fmap G f ]

Cat : ∀ {c₀ c₁ ℓ} → Category (suc (c₀ ⊔ c₁ ⊔ ℓ)) _ _
Cat {c₀} {c₁} {ℓ} = record {
  Obj = Category c₀ c₁ ℓ;
  Homsetoid = λ A B → record {
    Carrier = Functor A B ; _≈_ = equality ;
    isEquivalence = record {
      refl = λ f → eqArrowRefl B ;
      sym = λ x f → eqArrowSym B (x f);
      trans = λ x x₁ f → eqArrowTrans B (x f) (x₁ f) } };
  comp = compose;
  id = λ {A} → identity A;
  leftId = λ {A} {B} {f} f₁ → eqArrow (refl-hom B);
  rightId = λ {A} {B} {f} f₁ → eqArrow (refl-hom B);
  assoc = λ {A} {B} {C} {D} {f} {g} {h} f₁ → eqArrow (begin⟨ D ⟩
    fmap (compose (compose h g) f) f₁ ≈⟨ refl-hom D ⟩
    fmap h (fmap g (fmap f f₁)) ≈⟨ refl-hom D ⟩
    fmap (compose h (compose g f)) f₁
    ∎);
  ≈-composite = λ {A} {B} {C} {f} {g} {h} {i} f~g h~i f₁ → eqArrowTrans C (f~g (fmap h f₁)) (eqArrowFmap g (h~i f₁))
  }

max_stars_repo_name: myuon/agda-cate

max_issues_repo_name: myuon/agda-cate

max_forks_repo_name: myuon/agda-cate


text:
-- Bi-Cartesian closed structure of families
module SOAS.Families.BCCC {T : Set} where

open import SOAS.Common
open import SOAS.Context {T}
open import SOAS.Sorting {T}
open import SOAS.Families.Core {T}
open import SOAS.Families.Isomorphism {T}

import Categories.Category.CartesianClosed.Canonical as Canonical
import Categories.Category.CartesianClosed as CCC
import Categories.Category.Cartesian as Cart
open import Categories.Category.Cocartesian
open import Categories.Category.BicartesianClosed
import Categories.Object.Initial as Initial
open import Categories.Category.Monoidal

import Data.Unit as Unit
import Data.Empty as Empty

-- | Unsorted

-- Category of families is Cartesian closed
𝔽am-CanCCC : Canonical.CartesianClosed 𝔽amilies
𝔽am-CanCCC = record
  { ⊤ = λ Γ → Unit.⊤
  ; _×_ = λ X Y Γ → X Γ × Y Γ
  ; ! = λ _ → Unit.tt
  ; π₁ = proj₁
  ; π₂ = proj₂
  ; ⟨_,_⟩ = λ f g x → f x , g x
  ; !-unique = λ f → refl
  ; π₁-comp = refl
  ; π₂-comp = refl
  ; ⟨,⟩-unique = λ p₁ p₂ {Γ}{x} → sym (cong₂ _,_ p₁ p₂)
  ; _^_ = λ X Y Γ → Y Γ → X Γ
  ; eval = λ{ (f , x) → f x}
  ; curry = λ f x y → f (x , y)
  ; eval-comp = refl
  ; curry-resp-≈ = λ{X}{Y}{Z}{f}{g} p → ext (λ x → p)
  ; curry-unique = λ p → ext (λ x → p)
  }

𝔽am-CCC : CCC.CartesianClosed 𝔽amilies
𝔽am-CCC = Canonical.Equivalence.fromCanonical _ 𝔽am-CanCCC
module 𝔽am-CCC = CCC.CartesianClosed 𝔽am-CCC

-- Category of families is co-Cartesian
𝔽am-Cocartesian : Cocartesian 𝔽amilies
𝔽am-Cocartesian = record
  { initial = record { ⊥ = λ Γ → Empty.⊥ ; ⊥-is-initial = record { ! = λ () ; !-unique = λ{ f  {Γ} {()}} } }
  ; coproducts = record { coproduct = λ{X}{Y} → record
    { A+B = λ Γ → X Γ ⊎ Y Γ
    ; i₁ = inj₁
    ; i₂ = inj₂
    ; [_,_] = λ{ f g (inj₁ x) → f x ; f g (inj₂ y) → g y}
    ; inject₁ = refl
    ; inject₂ = refl
    ; unique = λ{ p₁ p₂ {Γ} {inj₁ x} → sym p₁ ; p₁ p₂ {Γ} {inj₂ y} → sym p₂}
    } }
  }
module 𝔽am-Cocart = Cocartesian 𝔽am-Cocartesian

-- Category of families is bi-Cartesian closed
𝔽am-BCCC : BicartesianClosed 𝔽amilies
𝔽am-BCCC = record { cartesianClosed = 𝔽am-CCC ; cocartesian = 𝔽am-Cocartesian }

module 𝔽am-BCCC = BicartesianClosed 𝔽am-BCCC

-- Shorthand for family product and sum and exponential
_×ₘ_ : Family → Family → Family
_×ₘ_ = 𝔽am-CCC._×_

_+ₘ_ : Family → Family → Family
_+ₘ_ = 𝔽am-Cocart._+_

_⇨_ : Family → Family → Family
_⇨_ = 𝔽am-CCC._⇨_
infixr 25 _⇨_

⊤ₘ : Family
⊤ₘ Γ = Unit.⊤

private variable X Y Z W : Family

curryₘ-iso : (X ×ₘ Y ⇾ Z) ≅ₛ (X ⇾ Y ⇨ Z)
curryₘ-iso = record
  { from = λ f x y → f (x , y)
  ; to = λ{ f (x , y) → f x y }
  ; iso = record { isoˡ = refl ; isoʳ = refl }
  }

-- Congruence for indexed families of functions
⇾-cong : X ≅ₘ Y → W ≅ₘ Z → (X ⇾ W) ≅ₛ (Y ⇾ Z)
⇾-cong X≅Y W≅Z = record
  { from = λ f y → _≅ₘ_.from W≅Z (f (_≅ₘ_.to X≅Y y))
  ; to = λ g x → _≅ₘ_.to W≅Z (g (_≅ₘ_.from X≅Y x))
  ; iso = record
    { isoˡ = λ {f} → dext′ (trans (_≅ₘ_.isoˡ W≅Z) (cong f (_≅ₘ_.isoˡ X≅Y)))
    ; isoʳ = λ {g} → dext′ (trans (_≅ₘ_.isoʳ W≅Z) (cong g (_≅ₘ_.isoʳ X≅Y)))
    }
  }

⇾-≅dom : X ≅ₘ Y → (X ⇾ W) ≅ₛ (Y ⇾ W)
⇾-≅dom X≅Y = ⇾-cong X≅Y ≅ₘ.refl

⇾-≅cod : W ≅ₘ Z → (X ⇾ W) ≅ₛ (X ⇾ Z)
⇾-≅cod W≅Z = ⇾-cong ≅ₘ.refl W≅Z

-- | Sorted

-- Category of sorted families is Cartesian closed
𝔽amₛ-CanCCC : Canonical.CartesianClosed 𝔽amiliesₛ
𝔽amₛ-CanCCC = 𝕊orted-CanCCC 𝔽am-CanCCC

𝔽amₛ-CCC : CCC.CartesianClosed 𝔽amiliesₛ
𝔽amₛ-CCC = Canonical.Equivalence.fromCanonical _ 𝔽amₛ-CanCCC

-- Category of sorted families is co-Cartesian
𝔽amₛ-Cocartesian : Cocartesian 𝔽amiliesₛ
𝔽amₛ-Cocartesian = 𝕊orted-Cocartesian 𝔽am-Cocartesian

-- Category of sorted families is bi-Cartesian closed
𝔽amₛ-BCCC : BicartesianClosed 𝔽amiliesₛ
𝔽amₛ-BCCC = 𝕊orted-BCCC 𝔽am-BCCC

module 𝔽amₛ-CCC = CCC.CartesianClosed 𝔽amₛ-CCC
module 𝔽amₛ-Cocart = Cocartesian 𝔽amₛ-Cocartesian

𝔽amₛ-Mon : Monoidal 𝔽amiliesₛ
𝔽amₛ-Mon = Cart.CartesianMonoidal.monoidal 𝔽amiliesₛ 𝔽amₛ-CCC.cartesian

-- Shorthand for sorted family product and sum and exponential
_×̣ₘ_ : Familyₛ → Familyₛ → Familyₛ
_×̣ₘ_ = 𝔽amₛ-CCC._×_

_+̣ₘ_ : Familyₛ → Familyₛ → Familyₛ
_+̣ₘ_ = 𝔽amₛ-Cocart._+_

_⇨̣_ : Familyₛ → Familyₛ → Familyₛ
_⇨̣_ = 𝔽amₛ-CCC._⇨_
infixr 25 _⇨̣_

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module test where

open import Relation.Binary.PropositionalEquality

module NewCodata where
  open import Data.Nat
  open import Data.List
  open import Data.Maybe
  record Pair (A B : Set) : Set where
    field
      fst : A
      snd : B

  record Stream (A : Set) : Set where
    coinductive
    field
      hd : A
      tl : Stream A

  open Stream

  repeat : ∀ {A : Set} → A → Stream A
  hd (repeat x) = x
  tl (repeat x) = repeat x

  nth : ∀ {A : Set} → ℕ → Stream A → A
  nth zero s = hd s
  nth (suc n) s = nth n (tl s)

  mutual
    data μColist (A : Set) : Set where
      []   : μColist A
      _∷_ : (x : A) (xs : νColist A) → μColist A
    record νColist (A : Set) : Set where
      coinductive
      field out : μColist A

  open νColist

  record νTree (A : Set) : Set where
    coinductive
    field label : A
          subs  : List (νTree A)
  open νTree

  append : {A : Set} → List A → νColist A → νColist A
  out (append []        ys) = out ys
  out (append (x ∷ xs) ys) = x ∷ append xs ys

  appendS : {A : Set} → List A → Stream A → Stream A
  hd (appendS [] s) = hd s
  hd (appendS (x ∷ xs) s) = x
  tl (appendS [] s) = tl s
  tl (appendS (x ∷ xs) s) = tl (appendS xs s)

  record Pi (A : Set) (B : A → Set) : Set where
    field _$_ : (x : A) → B x
    infixl 20 _$_

  open Pi

  _→'_ : Set → Set → Set
  A →' B = Pi A (λ _ → B)

  infixr 20 _→'_

  plus2 : ℕ →' ℕ
  plus2 $ x = suc (suc x)

  plus : ℕ →' ℕ →' ℕ
  plus $ 0       $ m = m
  plus $ (suc n) $ m = suc (plus $ n $ m)

  data Vec (A : Set) : ℕ → Set where
    nil : Vec A 0
    _:::_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

  test : Vec ℕ 2
  test = 2 ::: (2 ::: nil)

  repeat2V : Pi ℕ (λ n → Vec ℕ n)
  repeat2V $ 0     = nil
  repeat2V $ suc n =  2 ::: (repeat2V $ n)

  {-
  bf : {A : Set} → List (νTree A) → νColist A
  out (bf [])        = []
  out (bf (t ∷ ts)) = label t ∷
                       append (map label ts)
                              (bf (concatMap subs (t ∷ ts)))
  -}

  record ℕ∞ : Set where
    coinductive
    field
      pred∞ : Maybe ℕ∞
  open ℕ∞

  infinity : ℕ∞
  pred∞ infinity = just infinity

  zero∞ : ℕ∞
  pred∞ zero∞ = nothing

  one∞ : ℕ∞
  pred∞ one∞ = just zero∞

  suc∞ : ℕ∞ → ℕ∞
  pred∞ (suc∞ x) = just x

  plus∞ : ℕ∞ → ℕ∞ → ℕ∞
  pred∞ (plus∞ n m) with pred∞ n
  ...               | nothing = pred∞ m
  ...               | just n' = just (plus∞ n' m)

  {-
  record PStr (A : Set) (n : ℕ∞) : Set where
    coinductive
    field
      phd : (k : ℕ∞) → PStr A (suc∞ k) → A
      ptl : (k : ℕ∞) → PStr A (suc∞ k) → PStr A k
  -}

module OldCodata where
  open import Codata.Musical.Notation
  open import Data.Nat

  data Stream (A : Set) : Set where
     cons : A → ∞ (Stream A) → Stream A

  repeat : {A : Set} → A → Stream A
  repeat x = cons x (♯ (repeat x))

  nth : {A : Set} → ℕ → Stream A → A
  nth 0       (cons x _)  = x
  nth (suc n) (cons _ xs) = nth n (♭ xs)

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

  infinity : ℕ∞
  infinity = suc∞ (♯ infinity)

module NonTerminating where
  open import Data.Nat

  {-
  _/_ :  ℕ → ℕ → ℕ
  zero / y = zero
  suc x / y = suc ( (x ∸ y) / y)
  -}

module PositiveSizedTypes where
  open import Agda.Builtin.Size

  data ℕ : Size → Set where
    zero : {i : Size} → ℕ i
    suc : {i : Size} → ℕ i → ℕ (↑ i)

  one : ℕ ∞
  one = suc zero
  two : ℕ ∞
  two = suc one
  three : ℕ ∞
  three = suc two
  four : ℕ ∞
  four = suc three
  five : ℕ ∞
  five = suc four

  _-_ : {i : Size} → ℕ i → ℕ ∞ → ℕ i
  zero    - _      = zero
  n       - zero   = n
  (suc n) - (suc m) = n - m
  infixl 20 _-_

  -test₁ : five - two ≡ three
  -test₁ = refl

  _/_ : {i : Size} → ℕ i → ℕ ∞ → ℕ i
  zero  / _ = zero
  suc x / y = suc ( (x - y) / y)
  infixl 30 _/_

  _+_ : ℕ ∞ → ℕ ∞ → ℕ ∞
  zero + y  = y
  suc x + y = suc (x + y)
  infixl 20 _+_

  _*_ : ℕ ∞ → ℕ ∞ → ℕ ∞
  zero * _ = zero
  suc x * y = x + x * y
  infixl 30 _*_

  min : {i : Size} → ℕ i → ℕ i → ℕ i
  min zero     _        = zero
  min _        zero     = zero
  min (suc  m) (suc  n) = suc (min  m n)

  test₁ : zero / zero ≡ zero
  test₁ = refl
  test₂ : zero / five ≡ zero
  test₂ = refl
  test₃ : one / one ≡ one
  test₃ = refl
  test₄ : two / two ≡ one
  test₄ = refl
  test₅ : five / five ≡ one
  test₅ = refl
  test₆ : one / zero ≡ one
  test₆ = refl
  test₇ : two / one ≡ one
  test₇ = refl
  test₈ : four / two ≡ two
  test₈ = refl

module NegativSizedTypes where
  open import Agda.Builtin.Size
  open import Data.Nat
  open import Data.Bool using (if_then_else_)
  open import Relation.Nullary.Decidable using (⌊_⌋)

  record Stream (i : Size) (A : Set) : Set where
    coinductive
    field
      hd : A
      tl : ∀ {j : Size< i} → Stream j A
  open Stream

  cons : {i : Size} {A : Set} → A -> Stream i A → Stream i A
  hd (cons x _)  = x
  tl (cons _ xs) = xs

  map : {A B : Set} {i : Size} → (A → B) → Stream i A → Stream i B
  hd (map f xs) = f (hd xs)
  tl (map f xs) = map f (tl xs)

  merge : {i : Size} → Stream i ℕ → Stream i ℕ → Stream i ℕ
  hd (merge xs ys) = hd xs ⊓ hd ys
  tl (merge xs ys) = if ⌊ hd xs ≤? hd ys ⌋
                     then cons (hd ys) (merge (tl xs) (tl ys))
                     else cons (hd xs) (merge (tl xs) (tl ys))

  ham : {i : Size} → Stream i ℕ
  hd ham = 1
  tl ham = (merge (map (_*_ 2) ham) (map (_*_ 3) ham))

max_stars_repo_name: StillerHarpo/masterarbeit

max_issues_repo_name: StillerHarpo/masterarbeit

max_forks_repo_name: StillerHarpo/masterarbeit


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

module BottomUp1 where

record R (_ : Set) : Set where
  no-eta-equality

record S (F : Set → Set)
         ⦃ _ : {A : Set} → R (F A) ⦄
       : Set where

module M0 where
  private
    postulate
      F : Set → Set
      instance Ri : {A : Set} → R (F A)
      instance Si : S F

module M1 (_ : Set) where
  private
    postulate
      F : Set → Set
      instance Ri : {A : Set} → R (F A)
      instance Si-works : S F ⦃ Ri ⦄
      instance Si-fails : S F
      {- No instance of type R (F A) was found in scope. -}


text:
open import Data.ByteString using ( lazy ; strict )
open import System.IO using ( _>>_ ; _>>=_ ; getBytes ; putStr ; commit )

module System.IO.Examples.DevNull where

main =
  getBytes {lazy} >>= λ bs →
  putStr "Done.\n" >>
  commit

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io


text:
module Data.Fin.Substitution.Lemmas.Extra where

import Function as Fun
open import Data.Nat
open import Data.Fin hiding (_+_)
open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Vec.Properties
open import Data.Vec
open import Data.Star using (_◅_ ; ε)
open import Function hiding (id)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

module AdditionalLemmas {T} (lemmas : TermLemmas T) where

  open TermLemmas lemmas
  module Var = VarSubst

  -- Weakening commutes with single-variable substitution
  weaken-sub : ∀ {n} (a : T (1 + n)) (b : T n) →
                weaken (a / sub b) ≡ a / wk ↑ / sub (weaken b)
  weaken-sub a b = begin
    weaken (a / sub b)        ≡⟨ sym (/-wk′ (a / sub b)) ⟩
    a / sub b / wk            ≡⟨ sub-commutes a ⟩
    a / wk ↑ / sub (b / wk)   ≡⟨ cong (λ c → a / wk ↑ / sub c) (/-wk′ b) ⟩
    a / wk ↑ / sub (weaken b) ∎
    where /-wk′ : ∀ {n} (a : T n) → a / wk ≡ weaken a
          /-wk′ a = /-wk {t = a}

  -- Weakening commutes with reverse composition of substitutions.
  map-weaken-⊙ : ∀ {m n k} (σ₁ : Sub T m n) (σ₂ : Sub T n k) →
                  map weaken (σ₁ ⊙ σ₂) ≡ (map weaken σ₁) ⊙ (σ₂ ↑)
  map-weaken-⊙ σ₁ σ₂ = begin
    map weaken (σ₁ ⊙ σ₂)     ≡⟨ map-weaken ⟩
    (σ₁ ⊙ σ₂) ⊙ wk           ≡⟨ sym ⊙-assoc ⟩
    σ₁ ⊙ (σ₂ ⊙ wk)           ≡⟨ cong (λ σ₂ → σ₁ ⊙ σ₂) ⊙-wk ⟩
    σ₁ ⊙ (wk ⊙ (σ₂ ↑))       ≡⟨ ⊙-assoc ⟩
    (σ₁ ⊙ wk) ⊙ (σ₂ ↑)       ≡⟨ cong (λ σ₁ → σ₁ ⊙ (σ₂ ↑)) (sym map-weaken) ⟩
    (map weaken σ₁) ⊙ (σ₂ ↑) ∎

  weaken⋆↑ : ∀ {ν μ} (x : T ν) (s : Sub T ν μ) → (weaken x) / (s ↑) ≡ weaken (x / s)
  weaken⋆↑ x s = begin
    (weaken x) / (s ↑) ≡⟨ cong (λ u → u / (s ↑)) (sym /-wk) ⟩
    x / wk / (s ↑) ≡⟨ sym (/-⊙ x) ⟩
    x / (wk ⊙ (s ↑)) ≡⟨ cong (_/_ x) (sym ⊙-wk) ⟩
    x / (s ⊙ wk) ≡⟨ /-⊙ x ⟩
    x / s / wk ≡⟨ /-wk ⟩
    weaken (x / s) ∎

  weaken-sub-vanishes : ∀ {ν} {a b : T ν} → (weaken a) / (sub b) ≡ a
  weaken-sub-vanishes {ν} {a} {b} = begin
    (weaken a) / (sub b) ≡⟨ cong (flip _/_ (sub b)) (sym $ /-wk {t = a}) ⟩
    a / wk / (sub b) ≡⟨ wk-sub-vanishes a ⟩
    a ∎

  -- make /Var usable from lemmas
  open TermSubst termSubst using (_/Var_) public

  private
    var⋆weaken : ∀ {n} → _≗_ {A = Fin n} (var ∘ suc) (weaken ∘ var)
    var⋆weaken n = begin
      var (suc n) ≡⟨ sym $ lookup-wk n ⟩
      lookup n wk ≡⟨ sym $ var-/ ⟩
      (var n) / wk ≡⟨ /-wk ⟩
      weaken (var n) ∎

    map-var⋆weaken : ∀ {n m} {v : Vec (Fin n) m} → map var (map suc v) ≡ map weaken (map var v)
    map-var⋆weaken {v = v} = begin
      map var (map suc v) ≡⟨ sym $ map-∘ var suc v ⟩
      map (var ∘ suc) v ≡⟨ map-cong var⋆weaken v ⟩
      map (weaken ∘ var) v ≡⟨ map-∘ weaken var v ⟩
      map weaken (map var v) ∎

  map-var-varid≡id : ∀ {n} → map var (Var.id {n}) ≡ id {n}
  map-var-varid≡id {zero} = refl
  map-var-varid≡id {suc n} = begin
    var zero ∷ (map var $ map suc Var.id)
      ≡⟨ cong (_∷_ (var zero)) map-var⋆weaken ⟩
    var zero ∷ (map weaken $ map var Var.id)
      ≡⟨ cong (λ u → var zero ∷ (map weaken u)) map-var-varid≡id ⟩
    id ↑ ∎

  map-var-varwk≡wk : ∀ {n} → map var (Var.wk {n}) ≡ wk {n}
  map-var-varwk≡wk {zero} = refl
  map-var-varwk≡wk {suc n} = begin
    map var (map suc Var.id) ≡⟨ map-var⋆weaken ⟩
    map weaken (map var Var.id) ≡⟨ cong (map weaken) map-var-varid≡id ⟩
    wk ∎

  map-var-↑ : ∀ {n m} {s : Vec (Fin n) m} {s'} → map var s ≡ s' → map var (s Var.↑) ≡ s' ↑
  map-var-↑ {s = s} {s' = s'} eq = begin
    var zero ∷ (map var $ map suc s)
      ≡⟨ cong (_∷_ $ var zero) map-var⋆weaken ⟩
    var zero ∷ (map weaken $ map var s)
      ≡⟨ cong (λ u → var zero ∷ (map weaken u)) eq ⟩
    s' ↑ ∎

  a/wk↑/sub0≡a : ∀ {ν} (a : T (suc ν)) → a / wk ↑ / (sub $ var zero) ≡ a
  a/wk↑/sub0≡a a = begin
    a / wk ↑ / (sub $ var zero)
      ≡⟨ sym $ /-⊙ a ⟩
    a / (var zero / (sub $ var zero) ∷ map /-var-zero (map weaken wk))
      ≡⟨ cong (λ u → a / (u ∷ map /-var-zero (map weaken wk))) var-/ ⟩
    a / (var zero ∷ map /-var-zero (map weaken wk))
      ≡⟨ cong' (sym $ map-∘ /-var-zero weaken wk) ⟩
    a / (var zero ∷ map (λ t → (weaken t) / (sub $ var zero)) wk)
      ≡⟨ cong' (map-cong (λ t → weaken-sub-vanishes) wk) ⟩
    a / (var zero ∷ map Fun.id wk)
      ≡⟨ cong' (map-id wk) ⟩
    a / ((var zero ∷ wk))
      ≡⟨ id-vanishes a ⟩
    a ∎
    where
      /-var-zero = (λ t → t / (sub $ var zero))
      cong' : ∀ {x y} → x ≡ y → a / (var zero ∷ x) ≡ a / (var zero ∷ y)
      cong' = λ rest → cong (λ u → a / (var zero ∷ u)) rest

  lookup-lift-∷ : ∀ {v w} k x {b}{ρ : Sub T v w} → lookup (lift k suc x) ((b ∷ ρ) ↑⋆ k) ≡ lookup x (ρ ↑⋆ k)
  lookup-lift-∷ zero zero = refl
  lookup-lift-∷ zero (suc x) = refl
  lookup-lift-∷ (suc k) zero = refl
  lookup-lift-∷ (suc k) (suc x) {b} {ρ} = begin
    lookup (lift k suc x) (map (λ t → t /Var Var.wk) ((b ∷ ρ) ↑⋆ k))
      ≡⟨ lookup-map (lift k suc x) (λ t → t /Var Var.wk) ((b ∷ ρ) ↑⋆ k) ⟩
    lookup (lift k suc x) ((b ∷ ρ) ↑⋆ k) /Var Var.wk
      ≡⟨ cong (λ t → t /Var Var.wk) (lookup-lift-∷ k x) ⟩
    lookup x (ρ ↑⋆ k) /Var Var.wk
      ≡⟨ sym (lookup-map x (λ t → t /Var Var.wk) (ρ ↑⋆ k)) ⟩
    lookup x (map (λ t → t /Var Var.wk) (ρ ↑⋆ k))
    ∎

  wk-∷ : ∀ {ν ν'} (a : T ν)(ρ : Sub T ν ν'){b} → a / wk / (b ∷ ρ) ≡ a / ρ
  wk-∷ a ρ {b} = begin
    a / wk / (b ∷ ρ)
    ≡⟨ /✶-↑✶ ((b ∷ ρ) ◅ wk ◅ ε) (ρ ◅ ε) (λ k x → begin
      (var x) /✶ ((b ∷ ρ) ◅ wk ◅ ε) ↑✶ k
        ≡⟨ refl ⟩
      (var x) / wk ↑⋆ k / (b ∷ ρ) ↑⋆ k
        ≡⟨ cong (flip _/_ ((b ∷ ρ) ↑⋆ k)) var-/ ⟩
      (lookup x (wk ↑⋆ k)) / (b ∷ ρ) ↑⋆ k
        ≡⟨ cong (flip _/_ ((b ∷ ρ) ↑⋆ k)) (lookup-wk-↑⋆ k x) ⟩
      (var (lift k suc x)) / (b ∷ ρ) ↑⋆ k
        ≡⟨ var-/ ⟩
      lookup (lift k suc x) ((b ∷ ρ) ↑⋆ k)
        ≡⟨ lookup-lift-∷ k x ⟩
      lookup x (ρ ↑⋆ k)
        ≡⟨ sym var-/ ⟩
      (var x) /✶ (ρ ◅ ε) ↑✶ k ∎) 0 a ⟩
    a / ρ
    ∎

  wk⋆-++ : ∀ {ν ν'} μ (a : T ν)(ρ : Sub T ν ν'){ρ'} → a / wk⋆ μ / (ρ' ++ ρ) ≡ a / ρ
  wk⋆-++ zero a ρ {[]} = cong (λ t → t / ρ) (id-vanishes a)
  wk⋆-++ (suc μ) a ρ {_ ∷ ρ'} = begin
    a / wk⋆ (suc μ) / (_ ∷ ρ' ++ ρ)
      ≡⟨ cong (λ φ → a / φ / (_ ∷ ρ' ++ ρ)) map-weaken ⟩
    a / (wk⋆ μ ⊙ wk) / (_ ∷ ρ' ++ ρ)
      ≡⟨ cong (λ t → _/_ t (_ ∷ ρ' ++ ρ)) (/-⊙ a) ⟩
    a / wk⋆ μ / wk / (_ ∷ ρ' ++ ρ)
      ≡⟨ wk-∷ (a / wk⋆ μ) (ρ' ++ ρ) ⟩
    a / wk⋆ μ / (ρ' ++ ρ)
      ≡⟨ wk⋆-++ μ a ρ ⟩
    a / ρ
    ∎


text:
module Ual.Either where

infix 10 _∨_
data _∨_ (A B : Set) : Set where
  orL : A → A ∨ B
  orR : B → A ∨ B

max_stars_repo_name: brunoczim/ual

max_issues_repo_name: brunoczim/ual

max_forks_repo_name: brunoczim/ual


text:
------------------------------------------------------------------------------
-- Group theory congruence proofs using pattern matching
------------------------------------------------------------------------------

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

module LogicalFramework.GroupCongruence where

open import GroupTheory.Base

·-cong : ∀ {a b c d} → a ≡ b → c ≡ d → a · c ≡ b · d
·-cong refl refl = refl

·-leftCong : ∀ {a b c} → a ≡ b → a · c ≡ b · c
·-leftCong refl = refl

·-rightCong : ∀ {a b c} → b ≡ c → a · b ≡ a · c
·-rightCong refl = refl

⁻¹-cong : ∀ {a b} → a ≡ b → a ⁻¹ ≡ b ⁻¹
⁻¹-cong refl = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where at least one element satisfies a given property
------------------------------------------------------------------------

module Data.List.Any where

open import Data.Empty
open import Data.Fin
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Equiv using (module Equivalence)
open import Function.Related as Related hiding (_∼[_]_)
open import Data.List as List using (List; []; _∷_)
open import Data.Product as Prod using (∃; _×_; _,_)
open import Level using (Level; _⊔_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)
open import Relation.Binary hiding (Decidable)
import Relation.Binary.InducedPreorders as Ind
open import Relation.Binary.List.Pointwise as ListEq using ([]; _∷_)
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_)

-- Any P xs means that at least one element in xs satisfies P.

data Any {a p} {A : Set a}
         (P : A → Set p) : List A → Set (a ⊔ p) where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

-- Map.

map : ∀ {a p q} {A : Set a} {P : A → Set p} → {Q : A → Set q} →
      P ⋐ Q → Any P ⋐ Any Q
map g (here px)   = here (g px)
map g (there pxs) = there (map g pxs)

-- If the head does not satisfy the predicate, then the tail will.

tail : ∀ {a p} {A : Set a} {x : A} {xs : List A} {P : A → Set p} →
       ¬ P x → Any P (x ∷ xs) → Any P xs
tail ¬px (here  px)  = ⊥-elim (¬px px)
tail ¬px (there pxs) = pxs

-- Decides Any.

any : ∀ {a p} {A : Set a} {P : A → Set p} →
      Decidable P → Decidable (Any P)
any p []       = no λ()
any p (x ∷ xs) with p x
any p (x ∷ xs) | yes px = yes (here px)
any p (x ∷ xs) | no ¬px = Dec.map′ there (tail ¬px) (any p xs)

-- index x∈xs is the list position (zero-based) which x∈xs points to.

index : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
        Any P xs → Fin (List.length xs)
index (here  px)  = zero
index (there pxs) = suc (index pxs)

------------------------------------------------------------------------
-- List membership and some related definitions

module Membership {c ℓ : Level} (S : Setoid c ℓ) where

  private
    open module  S = Setoid S using (_≈_) renaming (Carrier to A)
    open module LS = Setoid (ListEq.setoid S)
      using () renaming (_≈_ to _≋_)

  -- If a predicate P respects the underlying equality then Any P
  -- respects the list equality.

  lift-resp : ∀ {p} {P : A → Set p} →
              P Respects _≈_ → Any P Respects _≋_
  lift-resp resp []            ()
  lift-resp resp (x≈y ∷ xs≈ys) (here px)   = here (resp x≈y px)
  lift-resp resp (x≈y ∷ xs≈ys) (there pxs) =
    there (lift-resp resp xs≈ys pxs)

  -- List membership.

  infix 4 _∈_ _∉_

  _∈_ : A → List A → Set _
  x ∈ xs = Any (_≈_ x) xs

  _∉_ : A → List A → Set _
  x ∉ xs = ¬ x ∈ xs

  -- Subsets.

  infix 4 _⊆_ _⊈_

  _⊆_ : List A → List A → Set _
  xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys

  _⊈_ : List A → List A → Set _
  xs ⊈ ys = ¬ xs ⊆ ys

  -- Equality is respected by the predicate which is used to define
  -- _∈_.

  ∈-resp-≈ : ∀ {x} → (_≈_ x) Respects _≈_
  ∈-resp-≈ = flip S.trans

  -- List equality is respected by _∈_.

  ∈-resp-list-≈ : ∀ {x} → _∈_ x Respects _≋_
  ∈-resp-list-≈ = lift-resp ∈-resp-≈

  -- _⊆_ is a preorder.

  ⊆-preorder : Preorder _ _ _
  ⊆-preorder = Ind.InducedPreorder₂ (ListEq.setoid S) _∈_ ∈-resp-list-≈

  module ⊆-Reasoning where
    import Relation.Binary.PreorderReasoning as PreR
    open PreR ⊆-preorder public
      renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)

    infix 1 _∈⟨_⟩_

    _∈⟨_⟩_ : ∀ x {xs ys} → x ∈ xs → xs IsRelatedTo ys → x ∈ ys
    x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs

  -- A variant of List.map.

  map-with-∈ : ∀ {b} {B : Set b}
               (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
  map-with-∈ []       f = []
  map-with-∈ (x ∷ xs) f = f (here S.refl) ∷ map-with-∈ xs (f ∘ there)

  -- Finds an element satisfying the predicate.

  find : ∀ {p} {P : A → Set p} {xs} →
         Any P xs → ∃ λ x → x ∈ xs × P x
  find (here px)   = (_ , here S.refl , px)
  find (there pxs) = Prod.map id (Prod.map there id) (find pxs)

  lose : ∀ {p} {P : A → Set p} {x xs} →
         P Respects _≈_ → x ∈ xs → P x → Any P xs
  lose resp x∈xs px = map (flip resp px) x∈xs

-- The code above instantiated (and slightly changed) for
-- propositional equality, along with some additional definitions.

module Membership-≡ where

  private
    open module M {a} {A : Set a} = Membership (PropEq.setoid A) public
      hiding (lift-resp; lose; ⊆-preorder; module ⊆-Reasoning)

  lose : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} →
         x ∈ xs → P x → Any P xs
  lose {P = P} = M.lose (PropEq.subst P)

  -- _⊆_ is a preorder.

  ⊆-preorder : ∀ {a} → Set a → Preorder _ _ _
  ⊆-preorder A = Ind.InducedPreorder₂ (PropEq.setoid (List A)) _∈_
                                      (PropEq.subst (_∈_ _))

  -- Set and bag equality and related preorders.

  open Related public
    using (Kind; Symmetric-kind)
    renaming ( implication         to subset
             ; reverse-implication to superset
             ; equivalence         to set
             ; injection           to subbag
             ; reverse-injection   to superbag
             ; bijection           to bag
             )

  [_]-Order : Kind → ∀ {a} → Set a → Preorder _ _ _
  [ k ]-Order A = Related.InducedPreorder₂ k (_∈_ {A = A})

  [_]-Equality : Symmetric-kind → ∀ {a} → Set a → Setoid _ _
  [ k ]-Equality A = Related.InducedEquivalence₂ k (_∈_ {A = A})

  infix 4 _∼[_]_

  _∼[_]_ : ∀ {a} {A : Set a} → List A → Kind → List A → Set _
  _∼[_]_ {A = A} xs k ys = Preorder._∼_ ([ k ]-Order A) xs ys

  -- Bag equality implies the other relations.

  bag-=⇒ : ∀ {k a} {A : Set a} {xs ys : List A} →
           xs ∼[ bag ] ys → xs ∼[ k ] ys
  bag-=⇒ xs≈ys = ↔⇒ xs≈ys

  -- "Equational" reasoning for _⊆_.

  module ⊆-Reasoning where
    import Relation.Binary.PreorderReasoning as PreR
    private
      open module PR {a} {A : Set a} = PreR (⊆-preorder A) public
        renaming (_∼⟨_⟩_ to _⊆⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_)

    infixr 2 _∼⟨_⟩_
    infix  1 _∈⟨_⟩_

    _∈⟨_⟩_ : ∀ {a} {A : Set a} x {xs ys : List A} →
             x ∈ xs → xs IsRelatedTo ys → x ∈ ys
    x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs

    _∼⟨_⟩_ : ∀ {k a} {A : Set a} xs {ys zs : List A} →
             xs ∼[ ⌊ k ⌋→ ] ys → ys IsRelatedTo zs → xs IsRelatedTo zs
    xs ∼⟨ xs≈ys ⟩ ys≈zs = xs ⊆⟨ ⇒→ xs≈ys ⟩ ys≈zs

------------------------------------------------------------------------
-- Another function

-- If any element satisfies P, then P is satisfied.

satisfied : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
            Any P xs → ∃ P
satisfied = Prod.map id Prod.proj₂ ∘ Membership-≡.find


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Well-founded induction
------------------------------------------------------------------------

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

open import Relation.Binary

module Induction.WellFounded where

open import Data.Product
open import Function
open import Induction
open import Level
open import Relation.Unary

-- When using well-founded recursion you can recurse arbitrarily, as
-- long as the arguments become smaller, and "smaller" is
-- well-founded.

WfRec : ∀ {a r} {A : Set a} → Rel A r → ∀ {ℓ} → RecStruct A ℓ _
WfRec _<_ P x = ∀ y → y < x → P y

-- The accessibility predicate: x is accessible if everything which is
-- smaller than x is also accessible (inductively).

data Acc {a ℓ} {A : Set a} (_<_ : Rel A ℓ) (x : A) : Set (a ⊔ ℓ) where
  acc : (rs : WfRec _<_ (Acc _<_) x) → Acc _<_ x

-- The accessibility predicate encodes what it means to be
-- well-founded; if all elements are accessible, then _<_ is
-- well-founded.

WellFounded : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
WellFounded _<_ = ∀ x → Acc _<_ x

Well-founded = WellFounded
{-# WARNING_ON_USAGE Well-founded
"Warning: Well-founded was deprecated in v0.15.
Please use WellFounded instead."
#-}

------------------------------------------------------------------------
-- Well-founded induction for the subset of accessible elements:

module Some {a lt} {A : Set a} {_<_ : Rel A lt} {ℓ} where

  wfRecBuilder : SubsetRecursorBuilder (Acc _<_) (WfRec _<_ {ℓ = ℓ})
  wfRecBuilder P f x (acc rs) = λ y y<x →
    f y (wfRecBuilder P f y (rs y y<x))

  wfRec : SubsetRecursor (Acc _<_) (WfRec _<_)
  wfRec = subsetBuild wfRecBuilder

  wfRec-builder = wfRecBuilder
  {-# WARNING_ON_USAGE wfRec-builder
  "Warning: wfRec-builder was deprecated in v0.15.
  Please use wfRecBuilder instead."
  #-}

------------------------------------------------------------------------
-- Well-founded induction for all elements, assuming they are all
-- accessible:

module All {a lt} {A : Set a} {_<_ : Rel A lt}
           (wf : WellFounded _<_) ℓ where

  wfRecBuilder : RecursorBuilder (WfRec _<_ {ℓ = ℓ})
  wfRecBuilder P f x = Some.wfRecBuilder P f x (wf x)

  wfRec : Recursor (WfRec _<_)
  wfRec = build wfRecBuilder

  wfRec-builder = wfRecBuilder
  {-# WARNING_ON_USAGE wfRec-builder
  "Warning: wfRec-builder was deprecated in v0.15.
  Please use wfRecBuilder instead."
  #-}

------------------------------------------------------------------------
-- It might be useful to establish proofs of Acc or Well-founded using
-- combinators such as the ones below (see, for instance,
-- "Constructing Recursion Operators in Intuitionistic Type Theory" by
-- Lawrence C Paulson).

module Subrelation {a ℓ₁ ℓ₂} {A : Set a}
                   {_<₁_ : Rel A ℓ₁} {_<₂_ : Rel A ℓ₂}
                   (<₁⇒<₂ : ∀ {x y} → x <₁ y → x <₂ y) where

  accessible : Acc _<₂_ ⊆ Acc _<₁_
  accessible (acc rs) = acc (λ y y<x → accessible (rs y (<₁⇒<₂ y<x)))

  wellFounded : WellFounded _<₂_ → WellFounded _<₁_
  wellFounded wf = λ x → accessible (wf x)

  well-founded = wellFounded
  {-# WARNING_ON_USAGE well-founded
  "Warning: well-founded was deprecated in v0.15.
  Please use wellFounded instead."
  #-}

module InverseImage {a b ℓ} {A : Set a} {B : Set b} {_<_ : Rel B ℓ}
                    (f : A → B) where

  accessible : ∀ {x} → Acc _<_ (f x) → Acc (_<_ on f) x
  accessible (acc rs) = acc (λ y fy<fx → accessible (rs (f y) fy<fx))

  wellFounded : WellFounded _<_ → WellFounded (_<_ on f)
  wellFounded wf = λ x → accessible (wf (f x))

  well-founded = wellFounded
  {-# WARNING_ON_USAGE well-founded
  "Warning: well-founded was deprecated in v0.15.
  Please use wellFounded instead."
  #-}

module TransitiveClosure {a ℓ} {A : Set a} (_<_ : Rel A ℓ) where

  infix 4 _<⁺_

  data _<⁺_ : Rel A (a ⊔ ℓ) where
    [_]   : ∀ {x y} (x<y : x < y) → x <⁺ y
    trans : ∀ {x y z} (x<y : x <⁺ y) (y<z : y <⁺ z) → x <⁺ z

  downwardsClosed : ∀ {x y} → Acc _<⁺_ y → x <⁺ y → Acc _<⁺_ x
  downwardsClosed (acc rs) x<y = acc (λ z z<x → rs z (trans z<x x<y))

  mutual

    accessible : ∀ {x} → Acc _<_ x → Acc _<⁺_ x
    accessible acc-x = acc (accessible′ acc-x)

    accessible′ : ∀ {x} → Acc _<_ x → WfRec _<⁺_ (Acc _<⁺_) x
    accessible′ (acc rs) y [ y<x ]         = accessible (rs y y<x)
    accessible′ acc-x    y (trans y<z z<x) =
      downwardsClosed (accessible′ acc-x _ z<x) y<z

  wellFounded : WellFounded _<_ → WellFounded _<⁺_
  wellFounded wf = λ x → accessible (wf x)

  downwards-closed = downwardsClosed
  {-# WARNING_ON_USAGE downwards-closed
  "Warning: downwards-closed was deprecated in v0.15.
  Please use downwardsClosed instead."
  #-}
  well-founded     = wellFounded
  {-# WARNING_ON_USAGE well-founded
  "Warning: well-founded was deprecated in v0.15.
  Please use wellFounded instead."
  #-}

module Lexicographic {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b}
                     (RelA : Rel A ℓ₁)
                     (RelB : ∀ x → Rel (B x) ℓ₂) where

  data _<_ : Rel (Σ A B) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
    left  : ∀ {x₁ y₁ x₂ y₂} (x₁<x₂ : RelA   x₁ x₂) → (x₁ , y₁) < (x₂ , y₂)
    right : ∀ {x y₁ y₂}     (y₁<y₂ : RelB x y₁ y₂) → (x  , y₁) < (x  , y₂)

  mutual

    accessible : ∀ {x y} →
                 Acc RelA x → (∀ {x} → WellFounded (RelB x)) →
                 Acc _<_ (x , y)
    accessible accA wfB = acc (accessible′ accA (wfB _) wfB)

    accessible′ :
      ∀ {x y} →
      Acc RelA x → Acc (RelB x) y → (∀ {x} → WellFounded (RelB x)) →
      WfRec _<_ (Acc _<_) (x , y)
    accessible′ (acc rsA) _    wfB ._ (left  x′<x) = accessible (rsA _ x′<x) wfB
    accessible′ accA (acc rsB) wfB ._ (right y′<y) =
      acc (accessible′ accA (rsB _ y′<y) wfB)

  wellFounded : WellFounded RelA → (∀ {x} → WellFounded (RelB x)) →
                WellFounded _<_
  wellFounded wfA wfB p = accessible (wfA (proj₁ p)) wfB

  well-founded = wellFounded
  {-# WARNING_ON_USAGE well-founded
  "Warning: well-founded was deprecated in v0.15.
  Please use wellFounded instead."
  #-}

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.0

module Inverse-image      = InverseImage
module Transitive-closure = TransitiveClosure


text:
open import FRP.LTL.RSet.Core using ( RSet )

module FRP.LTL.RSet.Stateless where

infixr 1 _⇒_

_⇒_ : RSet → RSet → RSet
(A ⇒ B) t = A t → B t

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of binary trees
------------------------------------------------------------------------

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

module Data.Tree.Binary.Properties where

open import Level using (Level)
open import Data.Nat.Base using (suc; _+_)
open import Data.Tree.Binary
open import Function.Base
open import Relation.Binary.PropositionalEquality

private
  variable
    a b : Level
    A : Set a
    B : Set b

size-map : ∀ (f : A → B) t → size (map f t) ≡ size t
size-map f leaf         = refl
size-map f (node l m r) =
  cong₂ (λ l r → l + suc r) (size-map f l) (size-map f r)

map-id : ∀ (t : Tree A) → map id t ≡ t
map-id leaf         = refl
map-id (node l v r) = cong₂ (flip node v) (map-id l) (map-id r)


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

module ideals where

import abelian-subgroups
import rings
open abelian-subgroups public
open rings public

{- Subsets of rings -}

subset-Ring :
  (l : Level) {l1 : Level} (R : Ring l1) → UU ((lsuc l) ⊔ l1)
subset-Ring l R = type-Ring R → UU-Prop l

is-set-subset-Ring :
  (l : Level) {l1 : Level} (R : Ring l1) → is-set (subset-Ring l R)
is-set-subset-Ring l R =
  is-set-function-type (is-set-UU-Prop l)

{- Closure properties of subsets of rings -}

is-additive-subgroup-subset-Ring :
  {l1 l2 : Level} (R : Ring l1) (P : subset-Ring l2 R) → UU (l1 ⊔ l2)
is-additive-subgroup-subset-Ring R = is-subgroup-Ab (ab-Ring R)

is-closed-under-mul-left-subset-Ring :
  {l1 l2 : Level} (R : Ring l1) (P : subset-Ring l2 R) → UU (l1 ⊔ l2)
is-closed-under-mul-left-subset-Ring R P =
  (x : type-Ring R) (y : type-Ring R) →
  type-Prop (P y) → type-Prop (P (mul-Ring R x y))

is-closed-under-mul-right-subset-Ring :
  {l1 l2 : Level} (R : Ring l1) (P : subset-Ring l2 R) → UU (l1 ⊔ l2)
is-closed-under-mul-right-subset-Ring R P =
  (x : type-Ring R) (y : type-Ring R) →
  type-Prop (P x) → type-Prop (P (mul-Ring R x y))

{- The definition of left and right ideals -}

is-left-ideal-subset-Ring :
  {l1 l2 : Level} (R : Ring l1) (P : subset-Ring l2 R) → UU (l1 ⊔ l2)
is-left-ideal-subset-Ring R P =
  is-additive-subgroup-subset-Ring R P ×
  is-closed-under-mul-left-subset-Ring R P

Left-Ideal-Ring :
  (l : Level) {l1 : Level} (R : Ring l1) → UU ((lsuc l) ⊔ l1)
Left-Ideal-Ring l R = Σ (subset-Ring l R) (is-left-ideal-subset-Ring R)

is-right-ideal-subset-Ring :
  {l1 l2 : Level} (R : Ring l1) (P : subset-Ring l2 R) → UU (l1 ⊔ l2)
is-right-ideal-subset-Ring R P =
  is-additive-subgroup-subset-Ring R P ×
  is-closed-under-mul-right-subset-Ring R P

Right-Ideal-Ring :
  (l : Level) {l1 : Level} (R : Ring l1) → UU ((lsuc l) ⊔ l1)
Right-Ideal-Ring l R = Σ (subset-Ring l R) (is-right-ideal-subset-Ring R)

is-two-sided-ideal-subset-Ring :
  {l1 l2 : Level} (R : Ring l1) (P : subset-Ring l2 R) → UU (l1 ⊔ l2)
is-two-sided-ideal-subset-Ring R P =
  is-additive-subgroup-subset-Ring R P ×
  ( is-closed-under-mul-left-subset-Ring R P ×
    is-closed-under-mul-right-subset-Ring R P)

Two-Sided-Ideal-Ring :
  (l : Level) {l1 : Level} (R : Ring l1) → UU ((lsuc l) ⊔ l1)
Two-Sided-Ideal-Ring l R =
  Σ (subset-Ring l R) (is-two-sided-ideal-subset-Ring R)

{- Special ideals -}

max_stars_repo_name: UlrikBuchholtz/HoTT-Intro

max_issues_repo_name: UlrikBuchholtz/HoTT-Intro

max_forks_repo_name: UlrikBuchholtz/HoTT-Intro


text:
open import Auto.Prelude

-- using a type argument as a proof

h0 : (x₁ x₂ : ⊥) → x₁ ≡ x₂
h0 = {!!}
--h0 = λ x₁ → λ ()

-- using dependent pair to define non-dep pair

module DND where
 _×_ : Set → Set → Set
 A × B = Σ A (λ _ → B)

 h1-2 : ∀ {A B} → A × B → B × A
-- h1-2 = {!!}  -- no solution found
 h1-2 = λ h → Σ-i {!!} {!!}
-- h1-2 = λ h → Σ-i (Σ.prf h) (Σ.wit h)

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe --without-K #-}
open import Relation.Binary

module Data.List.Membership.Setoid.Distinct  where

open import Data.List as List using (List; [];  _∷_; _++_)
open import Data.List.Any as Any hiding (map; head; tail)
open import Data.List.Any.Properties

open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Function
open import Function.Equivalence using (_⇔_; equivalence)
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using ()
open import Function.Injection using (_↣_; Injection)
open import Data.Product hiding (map)
open import Data.Sum     hiding (map)
import Level as L
open import Data.Fin as Fin using (Fin)
open import Data.Nat as ℕ

module _ {a p} {S : Setoid a p} where
  open Setoid S renaming (Carrier to A)
  open import Data.List.Membership.Setoid (S)
  open import Data.List.Membership.Setoid.Properties
  open import Data.List.Membership.Setoid.Disjoint (S) renaming (Disjoint to _⋈_)
  open import Data.List.Membership.Setoid.Trans (S)
  open import Data.Empty
  data Distinct : List A → Set (a L.⊔ p) where
    distinct-[] : Distinct []
    _distinct-∷_by_ : ∀ x {xs} → Distinct xs → x ∉ xs → Distinct (x ∷ xs)

  head : ∀ {x}{xs : List A} → Distinct (x ∷ xs) → A
  head (x distinct-∷ _ by _) = x

  tail : ∀ {x}{xs : List A} → Distinct (x ∷ xs) → Distinct xs
  tail (_ distinct-∷ dis by _) = dis

  head∉tail : ∀ {x}{xs : List A} → Distinct (x ∷ xs) → x ∉ xs
  head∉tail (_ distinct-∷ _ by x∉xs) = x∉xs

  distinct-[_] : ∀ x → Distinct (List.[ x ])
  distinct-[ x ] = x distinct-∷ distinct-[] by (λ ())

  ⋈-++ : ∀ (xs ys : List A) →
    Distinct (xs ++ ys) ⇔ (Distinct xs × Distinct ys × xs ⋈ ys)
  ⋈-++ xs ys = equivalence to from
    where
      to : ∀ {xs ys : List A} → Distinct (xs ++ ys) → (Distinct xs × Distinct ys × xs ⋈ ys)
      to {[]} dys = distinct-[] , dys , disjoint-[]ʳ
      to {x ∷ xs} {ys} (.x distinct-∷ dis by x∉xsys) with to {xs = xs} dis
      ... | dxs , dys , xs⋈ys = x distinct-∷ dxs by (λ x∈xs → x∉xsys (++⁺ˡ x∈xs)) , dys ,
            λ { (here px) ∈ys → x∉xsys (++⁺ʳ xs (≈-trans-∈ (sym px) ∈ys)) ; (there ∈xs) ∈ys → xs⋈ys ∈xs ∈ys}

      from : ∀ {xs ys : List A} →
           (Distinct xs × Distinct ys × xs ⋈ ys) → Distinct (xs ++ ys)
      from (distinct-[] , dys , xs⋈ys) = dys
      from {xs = .x ∷ xs} ((x distinct-∷ dxs by x∉xs) , dys , xxs⋈ys) with from (dxs , dys , xxs⋈ys ∘ there)
      ... | dxsys = x distinct-∷ dxsys by λ x∈xsys → case ++⁻ xs x∈xsys of λ { (inj₁ x∈xs) → x∉xs x∈xs
                                                                               ; (inj₂ x∈ys) → xxs⋈ys (here refl) x∈ys}

  lookup-injective : {xs : List A}(dxs : Distinct xs) → ∀ {i j} → List.lookup xs i ≡ List.lookup xs j → i ≡ j
  lookup-injective distinct-[] {()} {()} _
  lookup-injective (x distinct-∷ dxs by x∉xs) {Fin.zero} {Fin.zero} _ = P.refl
  lookup-injective (x distinct-∷ dxs by x∉xs) {Fin.suc i} {Fin.suc j} eq = P.cong Fin.suc (lookup-injective dxs eq)
  lookup-injective {xs} (x distinct-∷ dxs by x∉xs) {Fin.zero} {Fin.suc j} eq rewrite eq = ⊥-elim (x∉xs (∈-lookup S _ j))
  lookup-injective (x distinct-∷ dxs by x∉xs) {Fin.suc i} {Fin.zero} eq rewrite P.sym eq = ⊥-elim (x∉xs (∈-lookup S _ i))

module _ {a₁ a₂ p₁ p₂}{S₁ : Setoid a₁ p₁} {S₂ : Setoid a₂ p₂} where
  open Setoid S₁ renaming (Carrier to A) using ()
  open Setoid S₂ renaming (Carrier to B) using ()
  open import Data.List.Membership.Setoid (S₂) renaming (_∉_ to _∉₂_) using ()
  open import Data.List.Membership.Setoid.Properties
  open import Data.List.Membership.Setoid.Trans (S₁)
  map : (f : Injection S₁ S₂) → ∀ {xs : List A} → Distinct {S = S₁} xs → Distinct {S = S₂} (List.map (Injection.to f ⟨$⟩_) xs)
  map f {[]} distinct-[] = distinct-[]
  map f {.x ∷ xs} (x distinct-∷ dis by x∉xs) = fx distinct-∷ map f dis by lemma
      where
        fx = Injection.to f ⟨$⟩ x

        lemma : fx ∉₂ List.map (Injection.to f ⟨$⟩_) xs
        lemma p with ∈-map⁻ S₁ S₂ p
        ... | _ , y∈xs , fx≈fy = x∉xs (≈-trans-∈ (Injection.injective f fx≈fy) y∈xs)

max_stars_repo_name: tizmd/agda-distinct-disjoint

max_issues_repo_name: tizmd/agda-distinct-disjoint

max_forks_repo_name: tizmd/agda-distinct-disjoint


text:
module StateSized.GUI.BitMaps where

open import StateSizedIO.GUI.WxBindingsFFI

ship : Bitmap
ship = bitmap "./StateSized/GUI/ship.ico"

rock : Bitmap
rock = bitmap "./StateSized/GUI/rock.ico"

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
-- Andreas, 2020-04-15, issue #4586
-- Better error message when `let` contains a `where` clause.

foo : Set₁
foo = let x = Set
              where y = Set
      in  Set

-- WAS:
-- Not a valid let-declaration
-- when scope checking
-- let x = Set
--       where
--         y = Set
-- in Set

-- EXPECTED:
-- No `where' clauses allowed in let binding
-- when scope checking
-- let x = Set
--       where
--         y = Set
-- in Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Least common multiple
------------------------------------------------------------------------

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

module Data.Nat.LCM where

open import Algebra
open import Data.Nat.Base
open import Data.Nat.Coprimality using (Coprime)
open import Data.Nat.Divisibility
open import Data.Nat.DivMod
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Data.Nat.GCD
open import Data.Product
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Function
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
open import Relation.Binary
open import Relation.Nullary.Decidable using (False; fromWitnessFalse)

open +-*-Solver

private
  gcd≢0′ : ∀ m n → False (gcd (suc m) n ≟ 0)
  gcd≢0′ m n = fromWitnessFalse (gcd[m,n]≢0 (suc m) n (inj₁ (λ())))

------------------------------------------------------------------------
-- Definition

lcm : ℕ → ℕ → ℕ
lcm zero        n = zero
lcm m@(suc m-1) n = m * (n / gcd m n) {gcd≢0′ m-1 n}

------------------------------------------------------------------------
-- Core properties

private
  rearrange : ∀ m-1 n → lcm (suc m-1) n ≡ ((suc m-1) * n / gcd (suc m-1) n) {gcd≢0′ m-1 n}
  rearrange m-1 n = sym (*-/-assoc m {n} {gcd m n} {gcd≢0′ m-1 n} (gcd[m,n]∣n m n))
    where m = suc m-1

m∣lcm[m,n] : ∀ m n → m ∣ lcm m n
m∣lcm[m,n] zero      n = 0 ∣0
m∣lcm[m,n] m@(suc _) n = m∣m*n (n / gcd m n)

n∣lcm[m,n] : ∀ m n → n ∣ lcm m n
n∣lcm[m,n] zero        n = n ∣0
n∣lcm[m,n] m@(suc m-1) n = begin
  n                 ∣⟨ m∣m*n (m / gcd m n) ⟩
  n * (m / gcd m n) ≡⟨ sym (*-/-assoc n {≢0 = gcd≢0′ m-1 n} (gcd[m,n]∣m m n)) ⟩
  n * m / gcd m n   ≡⟨ cong (λ v → (v / gcd m n) {gcd≢0′ m-1 n}) (*-comm n m) ⟩
  m * n / gcd m n   ≡⟨ sym (rearrange m-1 n) ⟩
  m * (n / gcd m n) ∎
  where open ∣-Reasoning

lcm-least : ∀ {m n c} → m ∣ c → n ∣ c → lcm m n ∣ c
lcm-least {zero}        {n} {c} 0∣c _   = 0∣c
lcm-least {m@(suc m-1)} {n} {c} m∣c n∣c = P.subst (_∣ c) (sym (rearrange m-1 n))
  (m∣n*o⇒m/n∣o {n≢0 = gcd≢0′ m-1 n} gcd[m,n]∣m*n mn∣c*gcd)
  where
  open ∣-Reasoning
  gcd[m,n]∣m*n : gcd m n ∣ m * n
  gcd[m,n]∣m*n = ∣-trans (gcd[m,n]∣m m n) (m∣m*n n)

  mn∣c*gcd : m * n ∣ c * gcd m n
  mn∣c*gcd = begin
    m * n               ∣⟨ gcd-greatest (P.subst (_∣ c * m) (*-comm n m) (*-monoˡ-∣ m n∣c)) (*-monoˡ-∣ n m∣c) ⟩
    gcd (c * m) (c * n) ≡⟨ sym (c*gcd[m,n]≡gcd[cm,cn] c m n) ⟩
    c * gcd m n         ∎

------------------------------------------------------------------------
-- Other properties

-- Note that all other properties of `gcd` should be inferable from the
-- 3 core properties above.

gcd*lcm : ∀ m n → gcd m n * lcm m n ≡ m * n
gcd*lcm zero        n = *-zeroʳ (gcd 0 n)
gcd*lcm m@(suc m-1) n = trans (cong (gcd m n *_) (rearrange m-1 n)) (m*[n/m]≡n {gcd m n} (begin
  gcd m n ∣⟨ gcd[m,n]∣m m n ⟩
  m       ∣⟨ m∣m*n n ⟩
  m * n   ∎))
  where open ∣-Reasoning

lcm[0,n]≡0 : ∀ n → lcm 0 n ≡ 0
lcm[0,n]≡0 n = 0∣⇒≡0 (m∣lcm[m,n] 0 n)

lcm[n,0]≡0 : ∀ n → lcm n 0 ≡ 0
lcm[n,0]≡0 n = 0∣⇒≡0 (n∣lcm[m,n] n 0)

lcm-comm : ∀ m n → lcm m n ≡ lcm n m
lcm-comm m n = ∣-antisym
  (lcm-least (n∣lcm[m,n] n m) (m∣lcm[m,n] n m))
  (lcm-least (n∣lcm[m,n] m n) (m∣lcm[m,n] m n))

------------------------------------------------------------------------
-- Least common multiple (lcm).

module LCM where

  -- Specification of the least common multiple (lcm) of two natural
  -- numbers.

  record LCM (i j lcm : ℕ) : Set where
    field
      -- The lcm is a common multiple.
      commonMultiple : i ∣ lcm × j ∣ lcm

      -- The lcm divides all common multiples, i.e. the lcm is the least
      -- common multiple according to the partial order _∣_.
      least : ∀ {m} → i ∣ m × j ∣ m → lcm ∣ m

  open LCM public

  -- The lcm is unique.

  unique : ∀ {d₁ d₂ m n} → LCM m n d₁ → LCM m n d₂ → d₁ ≡ d₂
  unique d₁ d₂ = ∣-antisym (LCM.least d₁ (LCM.commonMultiple d₂))
                           (LCM.least d₂ (LCM.commonMultiple d₁))

open LCM public using (LCM) hiding (module LCM)

------------------------------------------------------------------------
-- Calculating the LCM

lcm-LCM : ∀ m n → LCM m n (lcm m n)
lcm-LCM m n = record
  { commonMultiple = m∣lcm[m,n] m n , n∣lcm[m,n] m n
  ; least          = uncurry′ lcm-least
  }

mkLCM : ∀ m n → ∃ λ d → LCM m n d
mkLCM m n = lcm m n , lcm-LCM m n

GCD*LCM : ∀ {m n g l} → GCD m n g → LCM m n l → m * n ≡ g * l
GCD*LCM {m} {n} {g} {l} gc lc = sym (begin
  g * l             ≡⟨ cong₂ _*_ (GCD.unique gc (gcd-GCD m n)) (LCM.unique lc (lcm-LCM m n)) ⟩
  gcd m n * lcm m n ≡⟨ gcd*lcm m n ⟩
  m * n             ∎)
  where open ≡-Reasoning


text:
_ : (@0 Set → Set) → (@ω Set → Set)
_ = λ f → f


text:
-- Andreas, 2012-04-18, bug reported by pumpkingod on 2012-04-16
module Issue610 where

import Common.Level
open import Common.Equality

data ⊥ : Set where
record ⊤ : Set where

record A : Set₁ where
  constructor set
  field
    .a : Set

.get : A → Set
get x = helper x
  module R where
  helper : .A -> Set
  helper x = A.a x

ack : A → Set
ack x = R.helper x x

-- Expected error:
-- Identifier R.helper is declared irrelevant, so it cannot be used here

hah : set ⊤ ≡ set ⊥
hah = refl

.moo : ⊥
moo with cong ack hah
moo | q = subst (λ x → x) q _

baa : .⊥ → ⊥
baa ()

yoink : ⊥
yoink = baa moo


text:
module Relation.Path where

open import Relation.Path.Operation

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
open import Mockingbird.Forest using (Forest)

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

open import Mockingbird.Forest.Combination.Base public

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


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

-- nothing for the standard library needed directly!

open import FT
open import Equivalences
open import TypeEquivalences

-- We now have enough to map each Pi combinator to the corresponding type equivalence

path2equiv : {B₁ B₂ : FT} → (B₁ ⇛ B₂) → (⟦ B₁ ⟧ ≃ ⟦ B₂ ⟧)
path2equiv unite₊⇛  = unite₊equiv
path2equiv uniti₊⇛  = uniti₊equiv
path2equiv swap₊⇛   = swap₊equiv
path2equiv assocl₊⇛ = assocl₊equiv
path2equiv assocr₊⇛ = assocr₊equiv
path2equiv unite⋆⇛  = unite⋆equiv
path2equiv uniti⋆⇛  = uniti⋆equiv
path2equiv swap⋆⇛   = swap⋆equiv
path2equiv assocl⋆⇛ = assocl⋆equiv
path2equiv assocr⋆⇛ = assocr⋆equiv
path2equiv distz⇛   = distzequiv
path2equiv factorz⇛ = factorzequiv
path2equiv dist⇛    = distequiv
path2equiv factor⇛  = factorequiv
path2equiv id⇛      = idequiv
path2equiv (sym⇛ p) = sym≃ (path2equiv p)
path2equiv (p ◎ q)  = trans≃ (path2equiv p) (path2equiv q)
path2equiv (p ⊕ q)  = path⊎ (path2equiv p) (path2equiv q)
path2equiv (p ⊗ q)  = path× (path2equiv p) (path2equiv q)

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- Recursive types and potentially infinite trees
------------------------------------------------------------------------

module RecursiveTypes.Syntax where

open import Data.Nat
open import Data.Fin
open import Function.Base
open import Data.Product
open import Codata.Musical.Notation
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
import Data.Fin.Properties as FP
private
  open module DF {n} = DecSetoid (FP.≡-decSetoid n)
                         using () renaming (_≟_ to _≟F_)

------------------------------------------------------------------------
-- Types

infixr 10 _⟶_
infix  10 μ_⟶_

-- Recursive types, parameterised on the maximum number of free
-- variables.
--
-- μ σ ⟶ τ stands for μX. σ ⟶ τ, where X can be free in σ and τ. The
-- arrow is included to avoid nonsensical types like μX.X. Note that
-- no attempt is made to ensure that the variable bound in μ_⟶_ is
-- actually used.

data Ty (n : ℕ) : Set where
  ⊥    : Ty n
  ⊤    : Ty n
  var  : (x : Fin n) → Ty n
  _⟶_  : (τ₁ τ₂ : Ty n) → Ty n
  μ_⟶_ : (τ₁ τ₂ : Ty (suc n)) → Ty n

-- Potentially infinite trees.

data Tree (n : ℕ) : Set where
  ⊥    : Tree n
  ⊤    : Tree n
  var  : (x : Fin n) → Tree n
  _⟶_  : (τ₁ τ₂ : ∞ (Tree n)) → Tree n

------------------------------------------------------------------------
-- Syntactic equality of types is decidable

private

  drop-var : ∀ {n x y} → (Ty n ∋ var x) ≡ var y → x ≡ y
  drop-var refl = refl

  drop⟶ˡ : ∀ {n σ₁ σ₂ τ₁ τ₂} →
           (Ty n ∋ σ₁ ⟶ σ₂) ≡ τ₁ ⟶ τ₂ → σ₁ ≡ τ₁
  drop⟶ˡ refl = refl

  drop⟶ʳ : ∀ {n σ₁ σ₂ τ₁ τ₂} →
           (Ty n ∋ σ₁ ⟶ σ₂) ≡ τ₁ ⟶ τ₂ → σ₂ ≡ τ₂
  drop⟶ʳ refl = refl

  dropμ⟶ˡ : ∀ {n σ₁ σ₂ τ₁ τ₂} →
            (Ty n ∋ μ σ₁ ⟶ σ₂) ≡ μ τ₁ ⟶ τ₂ → σ₁ ≡ τ₁
  dropμ⟶ˡ refl = refl

  dropμ⟶ʳ : ∀ {n σ₁ σ₂ τ₁ τ₂} →
            (Ty n ∋ μ σ₁ ⟶ σ₂) ≡ μ τ₁ ⟶ τ₂ → σ₂ ≡ τ₂
  dropμ⟶ʳ refl = refl

infix 4 _≡?_

_≡?_ : ∀ {n} (σ τ : Ty n) → Dec (σ ≡ τ)
⊥         ≡? ⊥           = yes refl
⊥         ≡? ⊤           = no (λ ())
⊥         ≡? var y       = no (λ ())
⊥         ≡? τ₁ ⟶ τ₂     = no (λ ())
⊥         ≡? μ τ₁ ⟶ τ₂   = no (λ ())
⊤         ≡? ⊥           = no (λ ())
⊤         ≡? ⊤           = yes refl
⊤         ≡? var y       = no (λ ())
⊤         ≡? τ₁ ⟶ τ₂     = no (λ ())
⊤         ≡? μ τ₁ ⟶ τ₂   = no (λ ())
var x     ≡? ⊥           = no (λ ())
var x     ≡? ⊤           = no (λ ())
var x     ≡? var  y      = Dec.map′ (cong var) drop-var (x ≟F y)
var x     ≡? τ₁ ⟶ τ₂     = no (λ ())
var x     ≡? μ τ₁ ⟶ τ₂   = no (λ ())
σ₁ ⟶ σ₂   ≡? ⊥           = no (λ ())
σ₁ ⟶ σ₂   ≡? ⊤           = no (λ ())
σ₁ ⟶ σ₂   ≡? var y       = no (λ ())
σ₁ ⟶ σ₂   ≡?  τ₁ ⟶  τ₂   with σ₁ ≡? τ₁ | σ₂ ≡? τ₂
σ₁ ⟶ σ₂   ≡? .σ₁ ⟶ .σ₂   | yes refl | yes refl = yes refl
σ₁ ⟶ σ₂   ≡?  τ₁ ⟶  τ₂   | no σ₁≢τ₁ | _        = no (σ₁≢τ₁ ∘ drop⟶ˡ)
σ₁ ⟶ σ₂   ≡?  τ₁ ⟶  τ₂   | _        | no σ₂≢τ₂ = no (σ₂≢τ₂ ∘ drop⟶ʳ)
σ₁ ⟶ σ₂   ≡? μ τ₁ ⟶ τ₂   = no (λ ())
μ σ₁ ⟶ σ₂ ≡? ⊥           = no (λ ())
μ σ₁ ⟶ σ₂ ≡? ⊤           = no (λ ())
μ σ₁ ⟶ σ₂ ≡? var y       = no (λ ())
μ σ₁ ⟶ σ₂ ≡? τ₁ ⟶ τ₂     = no (λ ())
μ σ₁ ⟶ σ₂ ≡? μ  τ₁ ⟶  τ₂ with σ₁ ≡? τ₁ | σ₂ ≡? τ₂
μ σ₁ ⟶ σ₂ ≡? μ .σ₁ ⟶ .σ₂ | yes refl | yes refl = yes refl
μ σ₁ ⟶ σ₂ ≡? μ  τ₁ ⟶  τ₂ | no σ₁≢τ₁ | _        = no (σ₁≢τ₁ ∘ dropμ⟶ˡ)
μ σ₁ ⟶ σ₂ ≡? μ  τ₁ ⟶  τ₂ | _        | no σ₂≢τ₂ = no (σ₂≢τ₂ ∘ dropμ⟶ʳ)

------------------------------------------------------------------------
-- Hypotheses

-- A hypothesis is a pair of types where the first is assumed to be a
-- subtype of the other.

open Data.Product public using () renaming (_,_ to _≲_)

Hyp : ℕ → Set
Hyp n = Ty n × Ty n

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module _ where

module M₁ where

  record R : Set₂ where
    field
      _A : Set₁

  open R

  -- The following code used to be syntactically incorrect, because
  -- the left-hand side could be parsed either as the function r
  -- applied to a pattern variable, or as the copattern _A applied
  -- to r. Now the former interpretation is ruled out.

  r : R
  r A = Set

module M₂ where

  record R : Set₂ where
    field
      _A : Set₁

  open R

  data D : Set where
    d_A : D

  -- Name parts coming from constructors can be used as part of
  -- copatterns.

  r : R
  r A = Set

module M₃ where

  data D₂ : Set where
    c : D₂

  record R₂ : Set₁ where
    field
      f_c : Set

  open R₂

  -- Name parts coming from projections can be used as part of
  -- constructor patterns.

  F : D₂ → Set₁
  F c = Set

max_forks_repo_name: Agda-zh/agda


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

open import HoTT hiding (_::_)

module algebra.Word {i} (A : Type i) where

  data Word : Type i where
    nil : Word
    _::_ : A → Word → Word
    _inv::_ : A → Word → Word
  infixr 60 _::_ _inv::_

  -- The following six functions prove things like if [x ∷ v ≡ y ∷ w],
  -- then [x ≡ y].
  -- This is not as easy as it sounds, you cannot directly induct on the equality
  -- (because [x ∷ v] is not a general element of type word), so you have to
  -- extract the head, but it’s not always possible…

  Word= : (v w : Word) → Type i
  Word= nil         nil         = Lift ⊤
  Word= nil         (y    :: w) = Lift ⊥
  Word= nil         (y inv:: w) = Lift ⊥
  Word= (x    :: v) nil         = Lift ⊥
  Word= (x    :: v) (y    :: w) = (x == y) × (v == w)
  Word= (x    :: v) (y inv:: w) = Lift ⊥
  Word= (x inv:: v) nil         = Lift ⊥
  Word= (x inv:: v) (y    :: w) = Lift ⊥
  Word= (x inv:: v) (y inv:: w) = (x == y) × (v == w)

  Word=-out : {v w : Word} (p : v == w) → Word= v w
  Word=-out {v = nil}       idp = lift unit
  Word=-out {v = x    :: v} idp = (idp , idp)
  Word=-out {v = x inv:: v} idp = (idp , idp)

  Word=-in : {v w : Word} → Word= v w → v == w
  Word=-in {nil}       {nil}       _         = idp
  Word=-in {nil}       {y    :: w} (lift ())
  Word=-in {nil}       {y inv:: w} (lift ())
  Word=-in {x    :: v} {nil}       (lift ())
  Word=-in {x    :: v} {y    :: w} (p , q)   = ap2 _::_ p q
  Word=-in {x    :: v} {y inv:: w} (lift ())
  Word=-in {x inv:: v} {nil}       (lift ())
  Word=-in {x inv:: v} {y    :: w} (lift ())
  Word=-in {x inv:: v} {y inv:: w} (p , q)   = ap2 _inv::_ p q

  Word-fst= : {x y : A} {v w : Word} (p : x :: v == y :: w) → x == y
  Word-fst= p = fst (Word=-out p)

  Word-snd= : {x y : A} {v w : Word} (p : x :: v == y :: w) → v == w
  Word-snd= p = snd (Word=-out p)

  Word-fst=' : {x y : A} {v w : Word} (p : x inv:: v == y inv:: w) → x == y
  Word-fst=' p = fst (Word=-out p)

  Word-snd=' : {x y : A} {v w : Word} (p : x inv:: v == y inv:: w) → v == w
  Word-snd=' p = snd (Word=-out p)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Relation.Binary.Core

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

open import BBSTree _≤_
open import Bound.Total A
open import Bound.Total.Order _≤_
open import Data.List
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import TreeSort.Impl2 _≤_ tot≤

lemma-insert-/ : {a b : Bound}{x : A}(a≤x : LeB a (val x))(x≤b : LeB (val x) b)(t : BBSTree a b) → (flatten (insert a≤x x≤b t)) / x ⟶ (flatten t)
lemma-insert-/ a≤x x≤b (bslf _) = /head
lemma-insert-/ {x = x} b≤x x≤t (bsnd {x = y} b≤y y≤t l r)
    with tot≤ x y
... | inj₁ x≤y = lemma++/r (lemma-insert-/ b≤x (lexy x≤y) l)
... | inj₂ y≤x = lemma++/l {xs = flatten l} (/tail (lemma-insert-/ (lexy y≤x) x≤t r))

theorem-treeSort∼ : (xs : List A) → xs ∼ (flatten (treeSort xs))
theorem-treeSort∼ [] = ∼[]
theorem-treeSort∼ (x ∷ xs) = ∼x /head (lemma-insert-/ lebx lext (treeSort xs)) (theorem-treeSort∼ xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Jesper, 2017-01-24: if we allow a variable to be instantiated with a value
-- of a supertype, the resulting dot pattern won't be type-correct.

open import Common.Size

data D (i : Size) : (j : Size< ↑ i) → Set where

  c : ∀ (j : Size< ↑ i) (k : Size< ↑ j)
       → D i j
       → D j k
       → D i k

split : ∀ i (j : Size< ↑ i) → D i j → Set
split i j x = {!x!}  -- split on x

-- Expected: splitting on x succeeds with
--   split i .k (c j₁ k x x₁) = {!!}

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


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

open import HoTT
open import homotopy.EilenbergMacLane

module cohomology.CupProduct.OnEM.InLowDegrees2 {i} {j} (G : AbGroup i) (H : AbGroup j) where

private
  module G = AbGroup G
  module H = AbGroup H
  module G⊗H = TensorProduct G H

open EMExplicit G⊗H.abgroup
open import cohomology.CupProduct.OnEM.InLowDegrees G H public
open import cohomology.CupProduct.OnEM.CommutativityInLowDegrees
open CP₁₁-comm G H

cp₁₁-embase-r : (x : EM₁ G.grp) → cp₁₁ x embase == [ north ]₂
cp₁₁-embase-r x = CP₁₁Comm.f x embase

module ∧-cp₁₁-Rec =
  SmashRec {X = ⊙EM₁ G.grp} {Y = ⊙EM₁ H.grp} {C = EM 2}
            cp₁₁
            [ north ]₂ [ north ]₂
            cp₁₁-embase-r
            (λ y → idp)

∧-cp₁₁ : ⊙EM₁ G.grp ∧ ⊙EM₁ H.grp → EM 2
∧-cp₁₁ = ∧-cp₁₁-Rec.f

⊙∧-cp₁₁ : ⊙EM₁ G.grp ⊙∧ ⊙EM₁ H.grp ⊙→ ⊙EM 2
⊙∧-cp₁₁ = ∧-cp₁₁-Rec.f , idp

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
------------------------------------------------------------------------------
-- Axiomatic PA propositional equality
------------------------------------------------------------------------------

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

module PA.Axiomatic.Mendelson.Relation.Binary.PropositionalEqualityATP where

open import PA.Axiomatic.Mendelson.Base

------------------------------------------------------------------------------
-- Identity properties

postulate ≈-refl : ∀ {n} → n ≈ n
{-# ATP prove ≈-refl #-}

postulate ≈-sym : ∀ {m n} → m ≈ n → n ≈ m
{-# ATP prove ≈-sym #-}

postulate ≈-trans : ∀ {m n o} → m ≈ n → n ≈ o → m ≈ o
{-# ATP prove ≈-trans #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc