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

module Luau.StrictMode where

open import Agda.Builtin.Equality using (_≡_)
open import FFI.Data.Maybe using (just; nothing)
open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; _∪_; _∩_; src; tgt)
open import Luau.Subtyping using (_≮:_)
open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function; srcBinOp)
open import Properties.Contradiction using (¬)
open import Properties.TypeCheck using (typeCheckᴮ)
open import Properties.Product using (_,_)

data Warningᴱ (H : Heap yes) {Γ} : ∀ {M T} → (Γ ⊢ᴱ M ∈ T) → Set
data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set

data Warningᴱ H {Γ} where

  UnallocatedAddress : ∀ {a T} →

    (H [ a ]ᴴ ≡ nothing) →
    ---------------------
    Warningᴱ H (addr {a} T)

  UnboundVariable : ∀ {x T p} →

    (Γ [ x ]ⱽ ≡ nothing) →
    ------------------------
    Warningᴱ H (var {x} {T} p)

  FunctionCallMismatch : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →

    (U ≮: src T) →
    -----------------
    Warningᴱ H (app D₁ D₂)

  app₁ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →

    Warningᴱ H D₁ →
    -----------------
    Warningᴱ H (app D₁ D₂)

  app₂ : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →

    Warningᴱ H D₂ →
    -----------------
    Warningᴱ H (app D₁ D₂)

  BinOpMismatch₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →

    (T ≮: srcBinOp op) →
    ------------------------------
    Warningᴱ H (binexp {op} D₁ D₂)

  BinOpMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →

    (U ≮: srcBinOp op) →
    ------------------------------
    Warningᴱ H (binexp {op} D₁ D₂)

  bin₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →

    Warningᴱ H D₁ →
    ------------------------------
    Warningᴱ H (binexp {op} D₁ D₂)

  bin₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →

    Warningᴱ H D₂ →
    ------------------------------
    Warningᴱ H (binexp {op} D₁ D₂)

  FunctionDefnMismatch : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →

    (V ≮: U) →
    -------------------------
    Warningᴱ H (function {f} {U = U} D)

  function₁ : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →

    Warningᴮ H D →
    -------------------------
    Warningᴱ H (function {f} {U = U} D)

  BlockMismatch : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →

    (U ≮: T) →
    ------------------------------
    Warningᴱ H (block {b} {T = T} D)

  block₁ : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →

    Warningᴮ H D →
    ------------------------------
    Warningᴱ H (block {b} {T = T} D)

data Warningᴮ H {Γ} where

  return : ∀ {M B T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴮ B ∈ U} →

    Warningᴱ H D₁ →
    ------------------
    Warningᴮ H (return D₁ D₂)

  LocalVarMismatch : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →

    (U ≮: T) →
    --------------------
    Warningᴮ H (local D₁ D₂)

  local₁ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →

    Warningᴱ H D₁ →
    --------------------
    Warningᴮ H (local D₁ D₂)

  local₂ : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →

    Warningᴮ H D₂ →
    --------------------
    Warningᴮ H (local D₁ D₂)

  FunctionDefnMismatch : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →

    (V ≮: U) →
    -------------------------------------
    Warningᴮ H (function D₁ D₂)

  function₁ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →

    Warningᴮ H D₁ →
    --------------------
    Warningᴮ H (function D₁ D₂)

  function₂ : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →

    Warningᴮ H D₂ →
    --------------------
    Warningᴮ H (function D₁ D₂)

data Warningᴼ (H : Heap yes) : ∀ {V} → (⊢ᴼ V) → Set where

  FunctionDefnMismatch : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} →

    (V ≮: U) →
    ---------------------------------
    Warningᴼ H (function {f} {U = U} D)

  function₁ : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} →

    Warningᴮ H D →
    ---------------------------------
    Warningᴼ H (function {f} {U = U} D)

data Warningᴴ H (D : ⊢ᴴ H) : Set where

  addr : ∀ a {O} →

    (p : H [ a ]ᴴ ≡ O) →
    Warningᴼ H (D a p) →
    ---------------
    Warningᴴ H D

data Warningᴴᴱ H {Γ M T} : (Γ ⊢ᴴᴱ H ▷ M ∈ T) → Set where

  heap : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M ∈ T} →

    Warningᴴ H D₁ →
    -----------------
    Warningᴴᴱ H (D₁ , D₂)

  expr : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴱ M ∈ T} →

    Warningᴱ H D₂ →
    ---------------------
    Warningᴴᴱ H (D₁ , D₂)

data Warningᴴᴮ H {Γ B T} : (Γ ⊢ᴴᴮ H ▷ B ∈ T) → Set where

  heap : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B ∈ T} →

    Warningᴴ H D₁ →
    -----------------
    Warningᴴᴮ H (D₁ , D₂)

  block : ∀ {D₁ : ⊢ᴴ H} {D₂ : Γ ⊢ᴮ B ∈ T} →

    Warningᴮ H D₂ →
    ---------------------
    Warningᴴᴮ H (D₁ , D₂)

max_stars_repo_name: MeltzDev/luau

max_issues_repo_name: MeltzDev/luau

max_forks_repo_name: MeltzDev/luau


text:
open import FRP.JS.RSet using ( RSet ; _⇒_ ; ⟦_⟧ ; ⟨_⟩ )

module FRP.JS.Event where

infixr 4 _∪_

postulate
  Evt : RSet → RSet
  map : ∀ {A B} → ⟦ A ⇒ B ⟧ → ⟦ Evt A ⇒ Evt B ⟧
  ∅ : ∀ {A} → ⟦ Evt A ⟧
  _∪_ : ∀ {A} → ⟦ Evt A ⇒ Evt A ⇒ Evt A ⟧
  accumBy : ∀ {A B} → ⟦ ⟨ B ⟩ ⇒ A ⇒ ⟨ B ⟩ ⟧ → B → ⟦ Evt A ⇒ Evt ⟨ B ⟩ ⟧

{-# COMPILED_JS map function(A) { return function(B) {
  return function(f) { return function(s) { return function(e) {
    return e.map(function (t,v) { return f(t)(v); });
  }; }; };
}; } #-}

{-# COMPILED_JS ∅ function(A) { return require("agda.frp.signal").zero; } #-}

{-# COMPILED_JS _∪_ function(A) { return function(s) {
  return function(x) { return function(y) { return x.merge(y); }; };
}; } #-}

{-# COMPILED_JS accumBy function(A) { return function(B) { return function(f) {
  return function(b) { return function(s) { return function(e) {
    return e.accumBy(function(t,b,a) { return f(t)(b)(a); },b);
  }; }; };
}; }; } #-}

tag : ∀ {A B} → ⟦ B ⟧ → ⟦ Evt A ⇒ Evt B ⟧
tag b = map (λ _ → b)

ext: agda

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


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

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

module Cubical.Relation.Binary.Raw.Construct.NonStrictToStrict
  {a ℓ} {A : Type a} (_≤_ : RawRel A ℓ) where

open import Cubical.Relation.Binary.Raw.Properties
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.Sum.Base using (inl; inr)
open import Cubical.Data.Empty hiding (rec)
open import Cubical.Foundations.Function using (_∘_; flip)
open import Cubical.Relation.Nullary
open import Cubical.HITs.PropositionalTruncation hiding (elim)

private
  _≢_ : RawRel A a
  x ≢ y = ¬ (x ≡ y)

------------------------------------------------------------------------
-- _≤_ can be turned into _<_ as follows:

_<_ : RawRel A _
x < y = x ≤ y × x ≢ y

------------------------------------------------------------------------
-- Relationship between relations

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = fst

<⇒≢ : _<_ ⇒ _≢_
<⇒≢ = snd

≤∧≢⇒< : ∀ {x y} → x ≤ y → x ≢ y → x < y
≤∧≢⇒< = _,_

<⇒≱ : Antisymmetric _≤_ → ∀ {x y} → x < y → ¬ (y ≤ x)
<⇒≱ antisym (x≤y , x≢y) y≤x = x≢y (antisym x≤y y≤x)

≤⇒≯ : Antisymmetric _≤_ → ∀ {x y} → x ≤ y → ¬ (y < x)
≤⇒≯ antisym x≤y y<x = <⇒≱ antisym y<x x≤y

≰⇒> : Reflexive _≤_ → Total _≤_ →
      ∀ {x y} → ¬ (x ≤ y) → y < x
≰⇒> rfl total {x} {y} x≰y with total x y
... | inl x≤y = elim (x≰y x≤y)
... | inr y≤x = y≤x , x≰y ∘ reflx→fromeq _≤_ rfl ∘ sym

≮⇒≥ : Discrete A → Reflexive _≤_ → Total _≤_ →
      ∀ {x y} → ¬ (x < y) → y ≤ x
≮⇒≥ _≟_ ≤-refl _≤?_ {x} {y} x≮y with x ≟ y
... | yes x≈y            = reflx→fromeq _≤_ ≤-refl (sym x≈y)
... | no x≢y with y ≤? x
...   | inl y≤x = y≤x
...   | inr x≤y = elim (x≮y (x≤y , x≢y))

------------------------------------------------------------------------
-- Relational properties

<-isPropValued : isPropValued _≤_ → isPropValued _<_
<-isPropValued propv x y = isProp× (propv x y) (isPropΠ λ _ → isProp⊥)

<-toNotEq : ToNotEq _<_
<-toNotEq (_ , x≢y) x≡y = x≢y x≡y

<-irrefl : Irreflexive _<_
<-irrefl = tonoteq→irrefl _<_ <-toNotEq

<-transitive : IsPartialOrder _≤_ → Transitive _<_
<-transitive po (x≤y , x≢y) (y≤z , y≉z) =
  (transitive x≤y y≤z , x≢y ∘ antisym x≤y ∘ transitive y≤z ∘ fromEq ∘ sym)
  where open IsPartialOrder po

<-≤-trans : Transitive _≤_ → Antisymmetric _≤_ →
           Trans _<_ _≤_ _<_
<-≤-trans transitive antisym (x≤y , x≢y) y≤z =
  transitive x≤y y≤z , (λ x≡z → x≢y (antisym x≤y (Respectsʳ≡ _≤_ (sym x≡z) y≤z)))

≤-<-trans : Transitive _≤_ → Antisymmetric _≤_ →
           Trans _≤_ _<_ _<_
≤-<-trans trans antisym x≤y (y≤z , y≢z) =
  trans x≤y y≤z , (λ x≡z → y≢z (antisym y≤z (Respectsˡ≡ _≤_ x≡z x≤y)))

<-asym : Antisymmetric _≤_ → Asymmetric _<_
<-asym antisym (x≤y , x≢y) (y≤x , _) = x≢y (antisym x≤y y≤x)

<-decidable : Discrete A → Decidable _≤_ → Decidable _<_
<-decidable _≟_ _≤?_ x y with x ≤? y
... | no ¬p = no (¬p ∘ fst)
... | yes p with x ≟ y
...   | yes q = no (λ x<y → snd x<y q)
...   | no ¬q = yes (p , ¬q)

------------------------------------------------------------------------
-- Structures

isStrictPartialOrder : IsPartialOrder _≤_ → IsStrictPartialOrder _<_
isStrictPartialOrder po = record
  { irrefl     = <-irrefl
  ; transitive = <-transitive po
  } where open IsPartialOrder po


text:
{-# OPTIONS --erased-cubical #-}
module Common.Path where

open import Agda.Builtin.Cubical.Path public
open import Agda.Builtin.Cubical.HCompU
open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_;
                                             primHComp to hcomp; primTransp to transp; primComp to comp;
                                             itIsOne to 1=1)
                                   public
open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to outS; inc to inS) public

open Helpers public

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)

import SecondOrder.Arity
import SecondOrder.VContext

module SecondOrder.Signature
  ℓ
  (𝔸 : SecondOrder.Arity.Arity)
  where

  open SecondOrder.Arity.Arity 𝔸

  -- a second-order algebraic signature
  record Signature : Set (lsuc ℓ) where

    -- a signature consists of a set of sorts and a set of operations
    -- e.g. sorts A, B, C, ... and operations f, g, h
    field
      sort : Set ℓ -- sorts
      oper : Set ℓ -- operations

    open SecondOrder.VContext sort public

    -- each operation has arity and a sort (the sort of its codomain)
    field
      oper-arity : oper → arity -- the arity of an operation
      oper-sort : oper → sort -- the operation sort
      arg-sort : ∀ (f : oper) → arg (oper-arity f) → sort -- the sorts of arguments
      -- a second order operation can bind some free variables that occur as its arguments
      -- e.g. the lambda operation binds one type and one term
      arg-bind : ∀ (f : oper) → arg (oper-arity f) → VContext -- the argument bindings

    -- the arguments of an operation
    oper-arg : oper → Set
    oper-arg f = arg (oper-arity f)

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

open import Agda.Builtin.Equality
open import Data.Product
open import Level
open import Relation.Unary using (_⊆_)

module is-lib.InfSys.Induction {𝓁} where

  private
    variable
      U : Set 𝓁

  open import is-lib.InfSys.Base {𝓁}
  open MetaRule
  open IS

  {- Inductive Interpretation -}

  data Ind⟦_⟧ {𝓁c 𝓁p 𝓁n : Level} (is : IS {𝓁c} {𝓁p} {𝓁n} U) : U →  Set (𝓁 ⊔ 𝓁c ⊔ 𝓁p ⊔ 𝓁n) where
    fold : ∀{u} → ISF[ is ] Ind⟦ is ⟧ u → Ind⟦ is ⟧ u

  {- Induction Principle -}

  ind[_] : ∀{𝓁c 𝓁p 𝓁n 𝓁'}
      → (is : IS {𝓁c} {𝓁p} {𝓁n} U)  -- IS
      → (S : U → Set 𝓁')            -- specification
      → ISClosed is S               -- S is closed
      → Ind⟦ is ⟧ ⊆ S
  ind[ is ] S cl (fold (rn , c , refl , pr)) = cl rn c λ i → ind[ is ] S cl (pr i)

  {- Apply Rule -}

  apply-ind : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → (rn : is .Names) → RClosed (is .rules rn) Ind⟦ is ⟧
  apply-ind {is = is} rn = prefix⇒closed (is .rules rn) {P = Ind⟦ _ ⟧} λ{(c , refl , pr) → fold (rn , c , refl , pr)}

  {- Postfix - Prefix -}

  ind-postfix : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → Ind⟦ is ⟧ ⊆ ISF[ is ] Ind⟦ is ⟧
  ind-postfix (fold x) = x

  ind-prefix : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → ISF[ is ] Ind⟦ is ⟧ ⊆ Ind⟦ is ⟧
  ind-prefix x = fold x

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module SizedPolyIO.ConsoleObject where

open import Size
open import Level using (_⊔_) renaming (suc to lsuc)

open import SizedPolyIO.Console
open import SizedPolyIO.Object
open import SizedPolyIO.IOObject

-- A console object is an IO object for the IO interface  of console
ConsoleObject : ∀{μ ρ}(i : Size)  → (iface : Interface μ ρ) → Set (μ ⊔ ρ)
ConsoleObject i iface = IOObject consoleI iface i

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module _ where

open import Common.Equality

postulate
  _def_ _more_ _less_ : Set → Set → Set
  X : Set

infix 21 _more_
-- default fixity should be 20
infix 19 _less_

test : (X more X def X less X) ≡ _less_ (_def_ (_more_ X X) X) X
test = refl

module NoFix where
  data NoFix : Set₁ where
    _+_ : Set → Set → NoFix

module YesFix where
  data YesFix : Set₁ where
    _+_ : Set → Set → YesFix
  infix 10 _+_

open NoFix
open YesFix

-- overloaded _+_ should get fixity 10
test₂ : X less X + X ≡ NoFix._+_ (_less_ X X) X
test₂ = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.Units.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open Setoid S
open Ring R

Unit : A → Set (a ⊔ b)
Unit r = Sg A (λ s → (r * s) ∼ 1R)


text:
------------------------------------------------------------------------------
-- Properties of the iter₀ function
------------------------------------------------------------------------------

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

module FOT.FOTC.Program.Iter0.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.PropertiesI
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.Nat.Type
open import FOTC.Data.Nat.List.Type
open import FOTC.Program.Iter0.Iter0
open import FOTC.Program.Iter0.PropertiesI

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

{-# TERMINATING #-}
iter₀-ListN : ∀ f {n} → N n → (∀ {n} → N n → N (f · n)) → ListN (iter₀ f n)
iter₀-ListN f nzero h = subst ListN (sym (iter₀-0 f)) lnnil
iter₀-ListN f (nsucc {n} Nn) h =
  subst ListN
        (sym prf)
        (lncons (nsucc Nn) (iter₀-ListN f (h (nsucc Nn)) h))
  where
  prf : iter₀ f (succ₁ n) ≡ succ₁ n ∷ iter₀ f (f · (succ₁ n))
  prf = iter₀ f (succ₁ n)
          ≡⟨ iter₀-eq f (succ₁ n) ⟩
        (if (iszero₁ (succ₁ n)) then [] else (succ₁ n ∷ iter₀ f (f · (succ₁ n))))
          ≡⟨ ifCong₁ (iszero-S n) ⟩
        (if false then [] else (succ₁ n ∷ iter₀ f (f · (succ₁ n))))
          ≡⟨ if-false (succ₁ n ∷ iter₀ f (f · (succ₁ n))) ⟩
        succ₁ n ∷ iter₀ f (f · (succ₁ n)) ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Common where

open import Data.Bool
open import Data.Maybe
open import Data.Sum
open import Data.Product

BoolQ : Set₁
BoolQ = (A : Set) -> A -> A -> A

unBoolQ : {A : Set} -> A -> A -> BoolQ -> A
unBoolQ a a' q = q _ a a'

trueQ : BoolQ
trueQ = \_ a a' -> a

falseQ : BoolQ
falseQ = \_ a a' -> a'

fromBoolQ : BoolQ -> Bool
fromBoolQ q = unBoolQ true false q

toBoolQ : Bool -> BoolQ
toBoolQ true  = trueQ
toBoolQ false = falseQ

MaybeQ : Set -> Set₁
MaybeQ A = (B : Set) -> (A -> B) -> B -> B

unMaybeQ : {A B : Set} -> (A -> B) -> B -> MaybeQ A -> B
unMaybeQ f b q = q _ f b

justQ : {A : Set} -> A -> MaybeQ A
justQ a = \_ f b -> f a

nothingQ : {A : Set} -> MaybeQ A
nothingQ = \_ f b -> b

fromMaybeQ : {A : Set} -> MaybeQ A -> Maybe A
fromMaybeQ q = unMaybeQ just nothing q

toMaybeQ : {A : Set} -> Maybe A -> MaybeQ A
toMaybeQ (just a) = justQ a
toMaybeQ nothing  = nothingQ

EitherQ : Set -> Set -> Set₁
EitherQ A B = (C : Set) -> (A -> C) -> (B -> C) -> C

unEitherQ : {A B C : Set} -> (A -> C) -> (B -> C) -> EitherQ A B -> C
unEitherQ f g q = q _ f g

leftQ : {A B : Set} -> A -> EitherQ A B
leftQ a = \_ f g -> f a

rightQ : {A B : Set} -> B -> EitherQ A B
rightQ b = \_ f g -> g b

fromEitherQ : {A B : Set} -> EitherQ A B -> A ⊎ B
fromEitherQ q = unEitherQ inj₁ inj₂ q

toEitherQ : {A B : Set} -> A ⊎ B -> EitherQ A B
toEitherQ (inj₁ a) = leftQ a
toEitherQ (inj₂ b) = rightQ b

PairQ : Set -> Set -> Set₁
PairQ A B = (C : Set) -> (A -> B -> C) -> C

unPairQ : {A B C : Set} -> (A -> B -> C) -> PairQ A B -> C
unPairQ f q = q _ f

pairQ : {A B : Set} -> A -> B -> PairQ A B
pairQ a b = \_ f -> f a b

fromPairQ : {A B : Set} -> PairQ A B -> A × B
fromPairQ q = unPairQ (\a b -> (a , b)) q

toPairQ : {A B : Set} -> A × B -> PairQ A B
toPairQ (a , b) = pairQ a b

fstQ : {A B : Set} -> PairQ A B -> A
fstQ q = unPairQ (\a b -> a) q

sndQ : {A B : Set} -> PairQ A B -> B
sndQ q = unPairQ (\a b -> b) q

max_stars_repo_name: mietek/scott-encoding

max_issues_repo_name: mietek/scott-encoding

max_forks_repo_name: mietek/scott-encoding


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

module Music where

open import Data.Nat     using (ℕ; zero; suc; _+_; _*_)
open import Data.Integer using (ℤ; +_)
open import Data.List    using (List; foldr; []; _∷_; reverse)
open import Data.Product using (_×_; _,_)
open import Data.Vec     using (Vec; []; _∷_; replicate; concat; map; zipWith; toList; _++_; sum; foldr₁)
open import Function     using (_∘_)

open import Note
open import Pitch
open import Interval

-- A point in the music grid, which can either be a tone,
-- a continuation of a previous tone, or a rest.
data Point : Set where
  tone : Pitch → Point
  hold : Pitch → Point
  rest : Point

data Melody (n : ℕ) : Set where
  melody : Vec Point n → Melody n

unmelody : {n : ℕ} → Melody n → Vec Point n
unmelody (melody ps) = ps

note→melody : (n : Note) → Melody (noteDuration n)
note→melody (tone (duration zero)    p) = melody []
note→melody (tone (duration (suc d)) p) = melody (tone p ∷ replicate (hold p))
note→melody (rest _)                    = melody (replicate rest)

-- Assumes melody is well-formed in that a held note has the
-- same pitch as the note before it.
-- Does not consolidate rests.
melody→notes : {n : ℕ} → Melody n → List Note
melody→notes (melody m) = (reverse ∘ mn 0 ∘ reverse ∘ toList) m
  where mn : ℕ → List Point → List Note -- c is the number of held points
        mn c []            = []
        mn c (tone p ∷ ps) = tone (duration (suc c)) p ∷ mn 0 ps
        mn c (hold _ ∷ ps) = mn (suc c) ps
        mn c (rest ∷ ps)   = rest (duration 1) ∷ mn 0 ps

pitches→melody : {n : ℕ} → (d : Duration) → (ps : Vec Pitch n) → Melody (n * unduration d)
pitches→melody d ps = melody (concat (map (unmelody ∘ note→melody ∘ tone d) ps))

transposePoint : ℤ → Point → Point
transposePoint k (tone p) = tone (transposePitch k p)
transposePoint k (hold p) = hold (transposePitch k p)
transposePoint k rest     = rest

transposeMelody : {n : ℕ} → ℤ → Melody n → Melody n
transposeMelody k = melody ∘ map (transposePoint k) ∘ unmelody

data Chord (n : ℕ) : Set where
  chord : Vec Point n → Chord n

unchord : {n : ℕ} → Chord n → Vec Point n
unchord (chord ps) = ps

-- We represent music as a v × d grid where v is the number of voices and d is the duration.
-- The primary representation is as parallel melodies (counterpoint).
data Counterpoint (v : ℕ) (d : ℕ): Set where
  cp : Vec (Melody d) v → Counterpoint v d

uncp : {v d : ℕ} → Counterpoint v d → Vec (Melody d) v
uncp (cp m) = m

-- An alternative representation of music is as a series of chords (harmonic progression).
data Harmony (v : ℕ) (d : ℕ): Set where
  harmony : Vec (Chord v) d → Harmony v d

unharmony : {v d : ℕ} → Harmony v d → Vec (Chord v) d
unharmony (harmony h) = h

pitches→harmony : {n : ℕ} (d : Duration) → (ps : Vec Pitch n) → Harmony n (unduration d)
pitches→harmony (duration zero)    ps = harmony []
pitches→harmony (duration (suc d)) ps = harmony (chord (map tone ps) ∷ replicate (chord (map hold ps)))

pitchPair→Harmony : (d : Duration) → PitchPair → Harmony 2 (unduration d)
pitchPair→Harmony d (p , q) = pitches→harmony d (p ∷ q ∷ [])

pitchInterval→Harmony : (d : Duration) → PitchInterval → Harmony 2 (unduration d)
pitchInterval→Harmony d = pitchPair→Harmony d ∘ pitchIntervalToPitchPair

{-
pitchIntervalsToCounterpoint : PitchInterval → Counterpoint
pitchIntervalsToCounterpoint = pitchPairToCounterpoint ∘ pitchIntervalToPitchPair
-}

addEmptyVoice : {v d : ℕ} → Harmony v d → Harmony (suc v) d
addEmptyVoice (harmony h) = harmony (map (chord ∘ (rest ∷_) ∘ unchord) h)

infixl 5 _+H+_
_+H+_ : {v d d' : ℕ} → Harmony v d → Harmony v d' → Harmony v (d + d')
h +H+ h' = harmony (unharmony h ++ unharmony h')

foldIntoHarmony : {k n : ℕ} (ds : Vec Duration (suc k)) → (pss : Vec (Vec Pitch n) (suc k)) → Harmony n (foldr₁ _+_ (map unduration ds))
foldIntoHarmony (d ∷ [])      (ps ∷ [])        = pitches→harmony d ps
foldIntoHarmony (d ∷ d' ∷ ds) (ps ∷ ps' ∷ pss) = (pitches→harmony d ps) +H+ (foldIntoHarmony (d' ∷ ds) (ps' ∷ pss))

-- matrix transposition
mtranspose : {A : Set}{m n : ℕ} → Vec (Vec A n) m → Vec (Vec A m) n
mtranspose []         = replicate []
mtranspose (xs ∷ xss) = zipWith _∷_ xs (mtranspose xss)

counterpoint→harmony : {v d : ℕ} → Counterpoint v d → Harmony v d
counterpoint→harmony = harmony ∘ map chord ∘ mtranspose ∘ map unmelody ∘ uncp

harmony→counterpoint : {v d : ℕ} → Harmony v d → Counterpoint v d
harmony→counterpoint = cp ∘ map melody ∘ mtranspose ∘ map unchord ∘ unharmony

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Inverse where

open import Level using (Level; suc; _⊔_)

open import Categories.Category
open import Data.Product
import Categories.Morphism

record pseudo-iso {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  open Category C
  open Definitions C
  open Categories.Morphism C

  infix 10 _⁻¹
  field
    _⁻¹ : ∀ {A B} → (f : A ⇒ B) → B ⇒ A
    pseudo-iso₁ : ∀ {A B} {f : A ⇒ B} → f ∘ f ⁻¹ ∘ f ≈ f
    pseudo-iso₂ : ∀ {A B} {f : A ⇒ B} → f ⁻¹ ∘ f ∘ f ⁻¹ ≈ f ⁻¹

record Inverse {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  open Category C
  open Definitions C
  open Categories.Morphism C
  open pseudo-iso

  field
    piso : pseudo-iso C
    unique : ∀ {p : pseudo-iso C} {A B} → (f : A ⇒ B) → _⁻¹ piso f ≈ _⁻¹ p f

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Human.Char where

open import Human.Nat
open import Human.Bool

postulate Char : Set
{-# BUILTIN CHAR Char #-}

primitive
  primIsLower             : Char → Bool
  primIsDigit             : Char → Bool
  primIsAlpha             : Char → Bool
  primIsSpace             : Char → Bool
  primIsAscii             : Char → Bool
  primIsLatin1            : Char → Bool
  primIsPrint             : Char → Bool
  primIsHexDigit          : Char → Bool
  primToUpper primToLower : Char → Char
  primCharToNat           : Char → Nat
  primNatToChar           : Nat → Char
  primCharEquality        : Char → Char → Bool

-- {-# COMPILE JS primCharToNat = function(c) { return c.charCodeAt(0); } #-}
-- {-# COMPILE JS primNatToChar = function(c) { return JSON.stringify(c); } #-}
-- {-# COMPILE JS primCharEquality = function(c) { return function(d) { return c === d; }; } #-}

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
-- Andreas, 2019-12-03, issue #4200 reported and testcase by nad

open import Agda.Builtin.Bool

data D : Set where
  c₁ : D
  @0 c₂ : D

f : D → Bool
f c₁ = true
f c₂ = false

@0 _ : D
_ = c₂  -- OK.

_ : D
_ = c₂  -- Not allowed.

-- Expected error:

-- Identifier c₂ is declared erased, so it cannot be used here
-- when checking that the expression c₂ has type D


text:
-- Andreas, 2017-01-14, issue #2405 reported by m0davis
-- Instance not found due to regression introduced by
-- parameter-refinement.

-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.instance:70 #-}
-- {-# OPTIONS -v tc.meta.assign:40 #-}
-- {-# OPTIONS -v tc.conv:40 #-}
-- {-# OPTIONS -v tc.sig.param:100 #-}

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

module M1 (X : Set) where
  postulate
    F : Set → Set
    instance Ri : {A : Set} → R (F A)
    Si-works : S F ⦃ Ri ⦄
    Si-test  : S F

-- WAS:
-- No instance of type R (F A) was found in scope. -}
--
-- candidate:
--   Ri X    : (A : Set) → R (F X A)
--   Ri 0    : Π Set λ A → R (F 1 0)
--   Ri 0 _A : R (F 0 (_A 1 0))
-- goal:
--   getMetaType
--   ? : (X A : Set) → R (F X A)
--   ? : Π Set λ X → Pi Set λ A → R (F 1 0)
--   ? : R (F A)
--   ? : R (F 1 0)

-- Should succeed.


text:
------------------------------------------------------------------------------
-- Co-lists
------------------------------------------------------------------------------

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

module GFPs.Colist where

open import FOTC.Base
open import FOTC.Base.List

------------------------------------------------------------------------------
-- Colist is a greatest fixed-point of a functor

-- The functor.
ListF : (D → Set) → D → Set
ListF A xs = xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs')

-- Colist is the greatest fixed-point of ListF.
postulate
  Colist : D → Set

  -- Colist is a post-fixed point of ListF, i.e.
  --
  -- Colist ≤ ListF Colist.
  Colist-out-ho : ∀ {n} → Colist n → ListF Colist n

  -- Colist is the greatest post-fixed point of ListF, i.e.
  --
  -- ∀ A. A ≤ ListF A ⇒ A ≤ Colist.
  Colist-coind-ho :
    (A : D → Set) →
    -- A is post-fixed point of ListF.
    (∀ {xs} → A xs → ListF A xs) →
    -- Colist is greater than A.
    ∀ {xs} → A xs → Colist xs

------------------------------------------------------------------------------
-- First-order versions

Colist-out : ∀ {xs} →
             Colist xs →
             xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Colist xs')
Colist-out = Colist-out-ho

Colist-coind :
  (A : D → Set) →
  (∀ {xs} → A xs → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs')) →
  ∀ {xs} → A xs → Colist xs
Colist-coind = Colist-coind-ho

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the
-- Colist predicate is also a pre-fixed point of the functional ListF,
-- i.e.
--
-- ListF Colist ≤ Colist.
Colist-in-ho : ∀ {xs} → ListF Colist xs → Colist xs
Colist-in-ho h = Colist-coind-ho A h' h
  where
  A : D → Set
  A xs = ListF Colist xs

  h' : ∀ {xs} → A xs → ListF A xs
  h' (inj₁ xs≡0) = inj₁ xs≡0
  h' (inj₂ (x' , xs' , prf , CLxs' )) =
    inj₂ (x' , xs' , prf , Colist-out CLxs')

-- The first-order version.
Colist-in : ∀ {xs} →
            xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Colist xs') →
            Colist xs
Colist-in = Colist-in-ho

------------------------------------------------------------------------------
-- A stronger co-induction principle
--
-- From (Paulson, 1997. p. 16).

postulate
  Colist-coind-stronger-ho :
    (A : D → Set) →
    (∀ {xs} → A xs → ListF A xs ∨ Colist xs) →
    ∀ {xs} → A xs → Colist xs

Colist-coind-ho' :
  (A : D → Set) →
  (∀ {xs} → A xs → ListF A xs) →
  ∀ {xs} → A xs → Colist xs
Colist-coind-ho' A h Axs =
  Colist-coind-stronger-ho A (λ Ays → inj₁ (h Ays)) Axs

-- The first-order version.
Colist-coind-stronger :
  (A : D → Set) →
  (∀ {xs} → A xs →
    (xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs'))
    ∨ Colist xs) →
  ∀ {xs} → A xs → Colist xs
Colist-coind-stronger = Colist-coind-stronger-ho

-- 13 January 2014. As expected, we cannot prove
-- Colist-coind-stronger-ho from Colist-coind-ho.
Colist-coind-stronger-ho' :
  (A : D → Set) →
  (∀ {xs} → A xs → ListF A xs ∨ Colist xs) →
  ∀ {xs} → A xs → Colist xs
Colist-coind-stronger-ho' A h {xs} Axs = case prf (λ h' → h') (h Axs)
  where
  prf : ListF A xs → Colist xs
  prf h' = Colist-coind-ho A {!!} Axs

------------------------------------------------------------------------------
-- References
--
-- Paulson, L. C. (1997). Mechanizing Coinduction and Corecursion in
-- Higher-order Logic. Journal of Logic and Computation 7.2,
-- pp. 175–204.


text:
module Issue561 where

open import Common.Prelude hiding (primIsDigit)

primitive
  primIsDigit : Char → Bool

main : IO Bool
main = return true

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
------------------------------------------------------------------------
-- The Step function, used to define strong and weak bisimilarity as
-- well as expansion
------------------------------------------------------------------------

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

open import Prelude

open import Labelled-transition-system

module Bisimilarity.Step
         {ℓ}
         (lts : LTS ℓ)
         (open LTS lts)
         (_[_]↝₁_ _[_]↝₂_ : Proc → Label → Proc → Type ℓ)
         where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)

open import Bijection equality-with-J using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J as F hiding (_∘_)
open import H-level.Closure equality-with-J

import Similarity.Step lts as One-sided
open import Indexed-container hiding (⟨_⟩)
open import Indexed-container.Combinators hiding (_∘_)
open import Relation

private
 module Temporarily-private where

  -- If _[_]↝₁_ and _[_]↝₂_ are instantiated with _[_]⟶_, then this is
  -- basically the function from Definition 6.3.1 in Pous and
  -- Sangiorgi's "Enhancements of the bisimulation proof method",
  -- except that clause (3) is omitted.
  --
  -- Similarly, if the relations are instantiated with _[_]⇒̂_, then
  -- this is basically the function wb₁, again with the exception that
  -- clause (3) is omitted.
  --
  -- Finally, if _[_]↝₁_ is instantiated with _[_]⟶̂_ and _[_]↝₂_ is
  -- instantiated with _[_]⇒_, then we get the expansion relation's
  -- "step" function.

  record Step {r} (R : Rel₂ r Proc) (pq : Proc × Proc) :
              Type (ℓ ⊔ r) where
    constructor ⟨_,_⟩

    private
      p = proj₁ pq
      q = proj₂ pq

    field
      left-to-right : ∀ {p′ μ} →
                      p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝₁ q′ × R (p′ , q′)
      right-to-left : ∀ {q′ μ} →
                      q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]↝₂ p′ × R (p′ , q′)

open Temporarily-private using (Step)

-- The Step function, expressed as an indexed container.

StepC : Container (Proc × Proc) (Proc × Proc)
StepC = One-sided.StepC _[_]↝₁_ ⟷ One-sided.StepC _[_]↝₂_

-- The strong bisimilarity container presented in the paper,
-- generalised to use _[_]↝₁_ and _[_]↝₂_.

StepC′ : Container (Proc × Proc) (Proc × Proc)
StepC′ =
  (λ { (p , q) → (∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝₁ q′) ×
                 (∀ {q′ μ} → q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]↝₂ p′)
     })
    ◁
  (λ { {(p , q)} (lr , rl) (p′ , q′) →
       (∃ λ μ → ∃ λ (p⟶p′ : p [ μ ]⟶ p′) → proj₁ (lr p⟶p′) ≡ q′) ⊎
       (∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ q′) → proj₁ (rl q⟶q′) ≡ p′)
     })

-- The interpretations of the two containers above are pointwise
-- logically equivalent, and in the presence of extensionality they
-- are pointwise isomorphic.

StepC↔StepC′ :
  ∀ {k r} {R : Rel₂ r Proc} {pq} →
  Extensionality? k ℓ (ℓ ⊔ r) →
  ⟦ StepC ⟧ R pq ↝[ k ] ⟦ StepC′ ⟧ R pq
StepC↔StepC′ {pq = p , q} =
  inverse-ext? λ {k} ext →
  Σ-cong (inverse $
          drop-⊤-left-Σ (One-sided.Magic↔⊤ _)
            ×-cong
          drop-⊤-left-Σ (One-sided.Magic↔⊤ _)) λ { (lr , rl) →
  implicit-∀-cong ext λ { {p′ , q′} →
  Π-cong (lower-extensionality? k lzero ℓ ext)
    (F.id ⊎-cong (

       (∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ q′) →
            proj₁ (rl q⟶q′) ≡ p′)                            ↝⟨ inverse $ drop-⊤-left-Σ (_⇔_.to contractible⇔↔⊤ (singleton-contractible _)) ⟩

       (∃ λ (q′p′≡ : ∃ λ q′p′ → q′p′ ≡ (q′ , p′)) →
        ∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ proj₁ (proj₁ q′p′≡)) →
          proj₁ (rl q⟶q′) ≡ proj₂ (proj₁ q′p′≡))             ↝⟨ inverse Σ-assoc ⟩

       (∃ λ q′p′ → q′p′ ≡ (q′ , p′) ×
        ∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ proj₁ q′p′) →
          proj₁ (rl q⟶q′) ≡ proj₂ q′p′)                      ↔⟨ (∃-cong λ _ → (inverse $ Eq.≃-≡ (Eq.↔⇒≃ ×-comm)) ×-cong F.id) ⟩□

       (∃ λ q′p′ → swap q′p′ ≡ (p′ , q′) ×
        ∃ λ μ → ∃ λ (q⟶q′ : q [ μ ]⟶ proj₁ q′p′) →
          proj₁ (rl q⟶q′) ≡ proj₂ q′p′)                      □))

    (λ _ → F.id) }}

-- The definition of Step in terms of a container is pointwise
-- logically equivalent to the direct definition, and in the presence
-- of extensionality it is pointwise isomorphic to the direct
-- definition.

Step↔StepC :
  ∀ {k r} {R : Rel₂ r Proc} {pq} →
  Extensionality? k ℓ (ℓ ⊔ r) →
  Step R pq ↝[ k ] ⟦ StepC ⟧ R pq
Step↔StepC {R = R} {pq} ext =
  Step R pq                                     ↔⟨ lemma ⟩

  One-sided.Step _[_]↝₁_ R pq
    ×
  One-sided.Step _[_]↝₂_ (R ⁻¹) (swap pq)       ↝⟨ One-sided.Step↔StepC _ ext ×-cong One-sided.Step↔StepC _ ext ⟩

  ⟦ One-sided.StepC _[_]↝₁_ ⟧ R pq
    ×
  ⟦ One-sided.StepC _[_]↝₂_ ⟧ (R ⁻¹) (swap pq)  ↝⟨ inverse-ext? (λ ext → ⟦⟷⟧↔ ext (One-sided.StepC _[_]↝₁_) (One-sided.StepC _[_]↝₂_)) ext ⟩□

  ⟦ StepC ⟧ R pq                                □
  where
  lemma : _ ↔ _
  lemma = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ s → One-sided.⟨ Step.left-to-right s ⟩
                     , One-sided.⟨ Step.right-to-left s ⟩
        ; from = λ { (lr , rl) →
                     Temporarily-private.⟨ One-sided.Step.challenge lr
                                         , One-sided.Step.challenge rl
                                         ⟩
                   }
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    }

-- A variant of the previous lemma, stated for StepC′ instead of
-- StepC.

Step↔StepC′ :
  ∀ {k r} {R : Rel₂ r Proc} {pq} →
  Extensionality? k ℓ (ℓ ⊔ r) →
  Step R pq ↝[ k ] ⟦ StepC′ ⟧ R pq
Step↔StepC′ {R = R} {pq} ext =
  Step R pq        ↝⟨ Step↔StepC   ext ⟩
  ⟦ StepC  ⟧ R pq  ↝⟨ StepC↔StepC′ ext ⟩□
  ⟦ StepC′ ⟧ R pq  □

module StepC {r} {R : Rel₂ r Proc} {p q} where

  -- A "constructor".

  ⟨_,_⟩ :
    (∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝₁ q′ × R (p′ , q′)) →
    (∀ {q′ μ} → q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]↝₂ p′ × R (p′ , q′)) →
    ⟦ StepC ⟧ R (p , q)
  ⟨ lr , rl ⟩ = _⇔_.to (Step↔StepC _) Temporarily-private.⟨ lr , rl ⟩

  -- Some "projections".

  left-to-right :
    ⟦ StepC ⟧ R (p , q) →
    ∀ {p′ μ} → p [ μ ]⟶ p′ → ∃ λ q′ → q [ μ ]↝₁ q′ × R (p′ , q′)
  left-to-right = Step.left-to-right ∘ _⇔_.from (Step↔StepC _)

  right-to-left :
    ⟦ StepC ⟧ R (p , q) →
    ∀ {q′ μ} → q [ μ ]⟶ q′ → ∃ λ p′ → p [ μ ]↝₂ p′ × R (p′ , q′)
  right-to-left = Step.right-to-left ∘ _⇔_.from (Step↔StepC _)

open Temporarily-private public

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

-- Adjoints

open import Level

open import Data.Product using (_,_; _×_)
open import Function using (_$_) renaming (_∘_ to _∙_)
open import Function.Equality using (Π; _⟶_)
import Function.Inverse as FI
open import Relation.Binary using (Rel; IsEquivalence; Setoid)

-- be explicit in imports to 'see' where the information comes from
open import Categories.Category.Core using (Category)
open import Categories.Category.Product using (Product; _⁂_)
open import Categories.Category.Instance.Setoids
open import Categories.Morphism
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Hom using (Hom[_][-,-])
open import Categories.Functor.Construction.LiftSetoids
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper; _∘ₕ_; _∘ᵥ_; _∘ˡ_; _∘ʳ_)
  renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; unitorˡ; unitorʳ; associator; _≃_)
import Categories.Morphism.Reasoning as MR

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

record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
  private
    module C = Category C
    module D = Category D
    module L = Functor L
    module R = Functor R

  field
    unit   : NaturalTransformation idF (R ∘F L)
    counit : NaturalTransformation (L ∘F R) idF

  module unit = NaturalTransformation unit
  module counit = NaturalTransformation counit

  field
    zig : ∀ {A : C.Obj} → counit.η (L.F₀ A) D.∘ L.F₁ (unit.η A) D.≈ D.id
    zag : ∀ {B : D.Obj} → R.F₁ (counit.η B) C.∘ unit.η (R.F₀ B) C.≈ C.id

  private
    variable
      A : C.Obj
      B : D.Obj

  Ladjunct : L.F₀ A D.⇒ B → A C.⇒ R.F₀ B
  Ladjunct f = R.F₁ f C.∘ unit.η _

  Radjunct : A C.⇒ R.F₀ B → L.F₀ A D.⇒ B
  Radjunct f = counit.η _ D.∘ L.F₁ f

  RLadjunct≈id : ∀ {f : L.F₀ A D.⇒ B} → Radjunct (Ladjunct f) D.≈ f
  RLadjunct≈id {f = f} = begin
    Radjunct (Ladjunct f)                            ≈⟨ refl⟩∘⟨ L.homomorphism ⟩
    counit.η _ D.∘ L.F₁ (R.F₁ f) D.∘ L.F₁ (unit.η _) ≈⟨ pullˡ (counit.commute f) ⟩
    (f D.∘ counit.η _) D.∘ L.F₁ (unit.η _)           ≈⟨ pullʳ zig ⟩
    f D.∘ D.id                                       ≈⟨ D.identityʳ ⟩
    f                                                ∎
    where open D.HomReasoning
          open MR D

  LRadjunct≈id : ∀ {f : A C.⇒ R.F₀ B} → Ladjunct (Radjunct f) C.≈ f
  LRadjunct≈id {f = f} = begin
    Ladjunct (Radjunct f)                              ≈⟨ R.homomorphism ⟩∘⟨refl ⟩
    (R.F₁ (counit.η _) C.∘ R.F₁ (L.F₁ f)) C.∘ unit.η _ ≈˘⟨ pushʳ (unit.commute f) ⟩
    R.F₁ (counit.η _) C.∘ unit.η _ C.∘ f               ≈⟨ pullˡ zag ⟩
    C.id C.∘ f                                         ≈⟨ C.identityˡ ⟩
    f                                                  ∎
    where open C.HomReasoning
          open MR C

  Hom[L-,-] : Bifunctor C.op D (Setoids _ _)
  Hom[L-,-] = Hom[ D ][-,-] ∘F (L.op ⁂ idF)

  Hom[-,R-] : Bifunctor C.op D (Setoids _ _)
  Hom[-,R-] = Hom[ C ][-,-] ∘F (idF ⁂ R)

  module Hom[L-,-] = Functor Hom[L-,-]
  module Hom[-,R-] = Functor Hom[-,R-]

  -- Inverse is more 'categorical' than bijection defined via injection/surjection
  Hom-inverse : ∀ A B → FI.Inverse (Hom[L-,-].F₀ (A , B)) (Hom[-,R-].F₀ (A , B))
  Hom-inverse A B = record
    { to = record
      { _⟨$⟩_ = Ladjunct {A} {B}
      ; cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈
      }
    ; from = record
      { _⟨$⟩_ = Radjunct {A} {B}
      ; cong = D.∘-resp-≈ʳ ∙ L.F-resp-≈
      }
    ; inverse-of = record
      { left-inverse-of = λ _ → RLadjunct≈id
      ; right-inverse-of = λ _ → LRadjunct≈id
      }
    }

  module Hom-inverse {A} {B} = FI.Inverse (Hom-inverse A B)

  op : Adjoint R.op L.op
  op = record
    { unit   = counit.op
    ; counit = unit.op
    ; zig    = zag
    ; zag    = zig
    }

  -- naturality condition on the two hom functors.
  -- these conditions are separated out because a complication due to the
  -- universe level in Agda.
  module _ where
    open C
    open HomReasoning
    open MR C

    Ladjunct-comm : ∀ {X Y A B} {h i : L.F₀ X D.⇒ Y} {f : A ⇒ X} {g : Y D.⇒ B} →
                      h D.≈ i →
                      R.F₁ (g D.∘ h D.∘ L.F₁ f) ∘ unit.η A ≈ R.F₁ g ∘ (R.F₁ i ∘ unit.η X) ∘ f
    Ladjunct-comm {X} {Y} {A} {B} {h} {i} {f} {g} eq = begin
      R.F₁ (g D.∘ h D.∘ L.F₁ f) ∘ unit.η A         ≈⟨ R.homomorphism ⟩∘⟨refl ⟩
      (R.F₁ g ∘ R.F₁ (h D.∘ L.F₁ f)) ∘ unit.η A    ≈⟨ (refl⟩∘⟨ R.homomorphism) ⟩∘⟨refl ⟩
      (R.F₁ g ∘ R.F₁ h ∘ R.F₁ (L.F₁ f)) ∘ unit.η A ≈⟨ pullʳ assoc ⟩
      R.F₁ g ∘ R.F₁ h ∘ R.F₁ (L.F₁ f) ∘ unit.η A   ≈˘⟨ refl⟩∘⟨ ⟺ (R.F-resp-≈ eq) ⟩∘⟨ unit.commute f ⟩
      R.F₁ g ∘ R.F₁ i ∘ unit.η X ∘ f               ≈⟨ refl⟩∘⟨ sym-assoc ⟩
      R.F₁ g ∘ (R.F₁ i ∘ unit.η X) ∘ f             ∎

    Ladjunct-comm′ : ∀ {X A B} {f : A ⇒ X} {g : L.F₀ X D.⇒ B} →
                      Ladjunct (g D.∘ L.F₁ f) ≈ Ladjunct g ∘ f
    Ladjunct-comm′ = ∘-resp-≈ˡ R.homomorphism ○ (pullʳ (⟺ (unit.commute _))) ○ sym-assoc

    Ladjunct-resp-≈ : ∀ {A B} {f g : L.F₀ A D.⇒ B} → f D.≈ g → Ladjunct f ≈ Ladjunct g
    Ladjunct-resp-≈ eq = ∘-resp-≈ˡ (R.F-resp-≈ eq)

  module _ where
    open D
    open HomReasoning
    open MR D

    Radjunct-comm : ∀ {X Y A B} {h i : X C.⇒ R.F₀ Y} {f : A C.⇒ X} {g : Y ⇒ B} →
                      h C.≈ i →
                      counit.η B ∘ L.F₁ (R.F₁ g C.∘ h C.∘ f) ≈ g ∘ (counit.η Y ∘ L.F₁ i) ∘ L.F₁ f
    Radjunct-comm {X} {Y} {A} {B} {h} {i} {f} {g} eq = begin
      counit.η B ∘ L.F₁ (R.F₁ g C.∘ h C.∘ f)       ≈⟨ refl⟩∘⟨ L.homomorphism ⟩
      counit.η B ∘ L.F₁ (R.F₁ g) ∘ L.F₁ (h C.∘ f)  ≈⟨ pullˡ (counit.commute g) ⟩
      (g ∘ counit.η Y) ∘ L.F₁ (h C.∘ f)            ≈⟨ refl⟩∘⟨ L.homomorphism ⟩
      (g ∘ counit.η Y) ∘ L.F₁ h ∘ L.F₁ f           ≈⟨ refl⟩∘⟨ L.F-resp-≈ eq ⟩∘⟨refl ⟩
      (g ∘ counit.η Y) ∘ L.F₁ i ∘ L.F₁ f           ≈⟨ pullʳ sym-assoc ⟩
      g ∘ (counit.η Y ∘ L.F₁ i) ∘ L.F₁ f           ∎

    Radjunct-comm′ : ∀ {Y A B} {f : A C.⇒ R.F₀ Y} {g : Y ⇒ B} →
                      Radjunct (R.F₁ g C.∘ f) ≈ g ∘ Radjunct f
    Radjunct-comm′ = ∘-resp-≈ʳ L.homomorphism ○ pullˡ (counit.commute _) ○ assoc

    Radjunct-resp-≈ : ∀ {A B} {f g : A C.⇒ R.F₀ B} → f C.≈ g → Radjunct f ≈ Radjunct g
    Radjunct-resp-≈ eq = ∘-resp-≈ʳ (L.F-resp-≈ eq)

  -- a complication: the two hom functors do not live in the same Setoids,
  -- so they need to be mapped to the same Setoids first before establishing
  -- natural isomorphism!
  module _ where
    private
      levelℓ : Category o ℓ e → Level
      levelℓ {ℓ = ℓ} _ = ℓ

      levele : Category o ℓ e → Level
      levele {e = e} _ = e

    Hom[L-,-]′ : Bifunctor C.op D (Setoids _ _)
    Hom[L-,-]′ = LiftSetoids (levelℓ C) (levele C) ∘F Hom[ D ][-,-] ∘F (L.op ⁂ idF)

    Hom[-,R-]′ : Bifunctor C.op D (Setoids _ _)
    Hom[-,R-]′ = LiftSetoids (levelℓ D) (levele D) ∘F Hom[ C ][-,-] ∘F (idF ⁂ R)

    Hom-NI : NaturalIsomorphism Hom[L-,-]′ Hom[-,R-]′
    Hom-NI = record
      { F⇒G = ntHelper record
        { η       = λ _ → record
          { _⟨$⟩_ = λ f → lift (Ladjunct (lower f))
          ; cong  = λ eq → lift (Ladjunct-resp-≈ (lower eq))
          }
        ; commute = λ _ eq → lift $ Ladjunct-comm (lower eq)
        }
      ; F⇐G = ntHelper record
        { η       = λ _ → record
          { _⟨$⟩_ = λ f → lift (Radjunct (lower f))
          ; cong  = λ eq → lift (Radjunct-resp-≈ (lower eq))
          }
        ; commute = λ _ eq → lift $ Radjunct-comm (lower eq)
        }
      ; iso = λ X → record
        { isoˡ = λ eq → let open D.HomReasoning in lift (RLadjunct≈id ○ lower eq)
        ; isoʳ = λ eq → let open C.HomReasoning in lift (LRadjunct≈id ○ lower eq)
        }
      }

  module Hom-NI = NaturalIsomorphism Hom-NI

infix 5 _⊣_
_⊣_ = Adjoint

⊣-id : idF {C = C} ⊣ idF {C = C}
⊣-id {C = C} = record
  { unit   = F⇐G unitorˡ
  ; counit = F⇒G unitorʳ
  ; zig    = identityˡ
  ; zag    = identityʳ
  }
  where open Category C
        open NaturalIsomorphism

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


text:
module main where

open import IO

main : Main
main = run (putStrLn "Hello World!")

max_stars_repo_name: jappeace/agda-nix

max_issues_repo_name: jappeace/agda-nix

max_forks_repo_name: jappeace/agda-nix


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

module Light.Implementation.Relation.Binary.Equality.Propositional where

open import Agda.Builtin.Equality using (_≡_ ; refl)
open import Light.Library.Relation.Binary
      using (SelfSymmetric ; SelfTransitive ; Reflexive ; Binary ; SelfBinary ; Symmetric ; Transitive ; CongruentFor ; Preserved)
open import Light.Implementation.Relation.Sets using (base) public
open import Light.Library.Relation.Binary.Equality using (SelfEquality ; wrap)
open import Light.Variable.Sets
open import Light.Variable.Levels

open Reflexive
open Symmetric
open Transitive
open Preserved

module _ {𝕒 : Set aℓ} where
      instance relation : SelfBinary 𝕒
      relation = record { are = λ a b → a ≡ b }

      instance reflexive : Reflexive relation
      reflexive .reflexivity = refl

      instance symmetric : SelfSymmetric relation
      symmetric .symmetry refl = refl

      instance transitive : SelfTransitive relation
      transitive .transitivity refl refl = refl

      instance equals : SelfEquality 𝕒
      equals = wrap relation

instance congruent : ∀ {f : 𝕒 → 𝕓} → CongruentFor f relation relation
congruent .preservation refl = refl

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Groups.Torus where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn
open import Cubical.ZCohomology.Groups.Prelims
open import Cubical.ZCohomology.KcompPrelims

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Sigma
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +-comm to +ℤ-comm ; +-assoc to +ℤ-assoc)
open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Algebra.Group

open import Cubical.HITs.Pushout
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim2 to pElim2 ; ∣_∣ to ∣_∣₁)
open import Cubical.HITs.Nullification
open import Cubical.HITs.Truncation renaming (elim to trElim ; elim2 to trElim2 ; map to trMap ; rec to trRec)

--------- H⁰(T²) ------------
H⁰-T²≅ℤ : GroupEquiv (coHomGr 0 (S₊ 1 × S₊ 1)) intGroup
H⁰-T²≅ℤ =
  H⁰-connected (north , north)
    λ (a , b) → pRec propTruncIsProp
                     (λ id1 → pRec propTruncIsProp
                                   (λ id2 → ∣ ΣPathP (id1 , id2) ∣₁)
                                   (Sn-connected 0 b) )
                     (Sn-connected 0 a)

------------------ H¹(T²) -------------------------------

H¹-T²≅ℤ×ℤ : GroupEquiv (coHomGr 1 ((S₊ 1) × (S₊ 1))) (dirProd intGroup intGroup)
H¹-T²≅ℤ×ℤ =
    groupequiv (isoToEquiv (setTruncIso (curryIso ⋄ codomainIso S1→K₁≡S1×Int ⋄ toProdIso)
                          ⋄ setTruncOfProdIso))
               (sElim2 (λ _ _ → isOfHLevelPath 2 (isOfHLevelΣ 2 setTruncIsSet (λ _ → setTruncIsSet)) _ _)
                    λ f g → ΣPathP ((cong ∣_∣₂
                                     (funExt (λ x → helper (f (x , S¹→S1 base) +ₖ g (x , S¹→S1 base))
                                                   ∙ sym (cong₂ (λ x y → x +ₖ y)
                                                                (helper (f (x , S¹→S1 base)))
                                                                (helper (g (x , S¹→S1 base))))))) ,
                                   (cong ∣_∣₂
                                      (funExt
                                        (suspToPropRec
                                           north
                                           (λ _ → isSetInt _ _)
                                           (cong winding
                                                 (basechange-lemma2
                                                   (λ x → f (north , S¹→S1 x))
                                                   (λ x → g (north , S¹→S1 x))
                                                   λ x → S¹map (trMap S1→S¹ x))
                                          ∙∙ winding-hom
                                              (basechange2⁻
                                                  (S¹map (trMap S1→S¹ (f (north , S¹→S1 base))))
                                                  (λ i → S¹map (trMap S1→S¹ (f (north , S¹→S1 (loop i))))))
                                              (basechange2⁻
                                                  (S¹map (trMap S1→S¹ (g (north , S¹→S1 base))))
                                                  (λ i → S¹map (trMap S1→S¹ (g (north , S¹→S1 (loop i))))))
                                          ∙∙ sym (addLemma
                                                  (winding
                                                    (basechange2⁻
                                                      (S¹map (trMap S1→S¹ (f (north , S¹→S1 base))))
                                                      (λ i → S¹map (trMap S1→S¹ (f (north , S¹→S1 (loop i)))))))
                                                  (winding
                                                    (basechange2⁻
                                                      (S¹map (trMap S1→S¹ (g (north , S¹→S1 base))))
                                                      (λ i → S¹map (trMap S1→S¹ (g (north , S¹→S1 (loop i))))))))))))))
  □ dirProdEquiv (invGroupEquiv (Hⁿ-Sⁿ≅ℤ 0)) (H⁰-Sⁿ≅ℤ 0)

  where
  helper : (x : hLevelTrunc 3 (S₊ 1)) → ∣ S¹→S1 (S¹map (trMap S1→S¹ x)) ∣ ≡ x
  helper = trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _)
                  λ a → cong ∣_∣ (S1→S¹-retr a)

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

----------------------- H²(T²) ------------------------------
open import Cubical.Foundations.Equiv
H²-T²≅ℤ : GroupEquiv (coHomGr 2 (S₊ 1 × S₊ 1)) intGroup
H²-T²≅ℤ = invGroupEquiv ℤ≅H²-T²
  where
  ℤ≅H²-T² : GroupEquiv intGroup (coHomGr 2 (S₊ 1 × S₊ 1))
  GroupEquiv.eq ℤ≅H²-T² =
    compEquiv (isoToEquiv helper')
      (compEquiv (invEquiv (≃-× (GroupEquiv.eq H²-S¹≅0)
                                (invEquiv (GroupEquiv.eq (Hⁿ-Sⁿ≅ℤ 0)))))
                 (isoToEquiv
                    (invIso setTruncOfProdIso
                   ⋄ invIso (setTruncIso (curryIso
                                        ⋄ codomainIso S1→K2≡K2×K1
                                        ⋄ toProdIso)))))
    where
    helper' : Iso Int (Unit × Int)
    Iso.inv helper' = snd
    Iso.fun helper' x = tt , x
    Iso.leftInv helper' _ = refl
    Iso.rightInv helper' _ = refl

  GroupEquiv.isHom ℤ≅H²-T² a b =
      (λ i → f (GroupEquiv.isHom (invGroupEquiv (dirProdEquiv H²-S¹≅0 (invGroupEquiv (Hⁿ-Sⁿ≅ℤ 0)))) (_ , a) (_ , b) i))
    ∙ ((λ i → f (guyId i , (g a +ₕ g b)))
    ∙∙ helper (g a) (g b)
    ∙∙ (λ i → f (guyId2 (~ i) , g a) +ₕ f (guyId2 (~ i) , g b)))
    where
    f = Iso.fun (((invIso setTruncOfProdIso ⋄ invIso (setTruncIso (curryIso ⋄ codomainIso S1→K2≡K2×K1 ⋄ toProdIso)))))
    g = invEq (GroupEquiv.eq (invGroupEquiv (Hⁿ-Sⁿ≅ℤ 0)))

    isPropH²-S¹ : isProp (coHom 2 (S₊ 1))
    isPropH²-S¹ = transport (λ i → isProp (ua (GroupEquiv.eq H²-S¹≅0) (~ i))) isPropUnit

    guyId : ∣ _ ∣₂ ≡ 0ₕ
    guyId = isPropH²-S¹ _ _

    guyId2 : ∣ _ ∣₂ ≡ 0ₕ
    guyId2 = isPropH²-S¹ _ _

    helper : (x y : ∥ ((S₊ 1) → (hLevelTrunc 3 (S₊ 1) )) ∥₂) →
              f (0ₕ , x +ₕ y) ≡ f (0ₕ , x) +ₕ f (0ₕ , y)
    helper =
      sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
             λ f g i → ∣ (λ x → helper2 (f (fst x)) (g (fst x)) (snd x) i) ∣₂
      where
      helper2 : (x y : coHomK 1) (s : S₊ 1)
             → Iso.inv S1→K2≡K2×K1 (0ₖ , x +ₖ y) s ≡ (Iso.inv S1→K2≡K2×K1 (0ₖ , x)) s +ₖ (Iso.inv S1→K2≡K2×K1 (0ₖ , y)) s
      helper2 =
        trElim2 (λ _ _ → isOfHLevelΠ 3 λ _ → isOfHLevelTrunc 4 _ _)
               λ a b →
                λ {north → cong₂ (_+ₖ_) (sym (lUnitₖ 0ₖ)) (sym (lUnitₖ 0ₖ))
                ; south → cong₂ (_+ₖ_) (sym (lUnitₖ 0ₖ)) (sym (lUnitₖ 0ₖ))
                ; (merid south i) j →
                  hcomp (λ k → λ {(i = i0) → cong₂ (_+ₖ_) (sym (lUnitₖ 0ₖ)) (sym (lUnitₖ 0ₖ)) (j ∧ k)
                                 ; (i = i1) → cong₂ (_+ₖ_) (sym (lUnitₖ 0ₖ)) (sym (lUnitₖ 0ₖ)) (j ∧ k)
                                 ; (j = i0) → 0ₖ +ₖ Kn→ΩKn+1 1 (∣ a ∣ +ₖ ∣ b ∣) i
                                 ; (j = i1) →  cong₂ (_+ₖ_) (sym (lUnitₖ (Kn→ΩKn+1 1 ∣ a ∣ i))) (sym (lUnitₖ (Kn→ΩKn+1 1 ∣ b ∣ i))) k})
                        (helper3 ∣ a ∣ ∣ b ∣ j i)
                ; (merid north i) → cong₂ (_+ₖ_) (sym (lUnitₖ 0ₖ)) (sym (lUnitₖ 0ₖ)) }
        where
        helper3 : (a b : coHomK 1) → cong (0ₖ +ₖ_) (Kn→ΩKn+1 1 (a +ₖ b)) ≡ cong₂ _+ₖ_ (Kn→ΩKn+1 1 a) (Kn→ΩKn+1 1 b)
        helper3 a b = (cong (cong (0ₖ +ₖ_)) helper4
                    ∙ congFunct (0ₖ +ₖ_) (Kn→ΩKn+1 1 a) (Kn→ΩKn+1 1 b))
                   ∙∙ cong (_∙ cong (0ₖ +ₖ_) (Kn→ΩKn+1 1 b)) (helper5 (Kn→ΩKn+1 1 a))
                   ∙∙ sym (cong₂Funct (_+ₖ_) (Kn→ΩKn+1 1 a) (Kn→ΩKn+1 1 b))
          where
          helper4 : Kn→ΩKn+1 1 (a +ₖ b) ≡ Kn→ΩKn+1 1 a ∙ Kn→ΩKn+1 1 b -- Termination issues unless this is put as a separate lemma...
          helper4 = +ₖ→∙ 1 a b

          helper6 : ∀{ℓ} {A : Type ℓ} {a b : A} (p : a ≡ b) → p ≡ (refl ∙ refl) ∙ p ∙ refl ∙ refl
          helper6 p = (λ i → rUnit p i) ∙∙ (λ i → lUnit (p ∙ rUnit refl i) i) ∙∙ λ i → rUnit refl i ∙ p ∙ refl ∙ refl
          helper5 : (a : Path (coHomK 2) 0ₖ 0ₖ) → cong (0ₖ +ₖ_) a ≡ cong (_+ₖ 0ₖ) a
          helper5 a = (((helper6 (cong (0ₖ +ₖ_) a))
                   ∙∙ (λ i → ((λ j → lUnitₖ 0ₖ (i ∧ j)) ∙ refl) ∙ cong (λ x → lUnitₖ x i) a ∙ refl ∙ λ j → lUnitₖ 0ₖ (i ∧ (~ j)))
                   ∙∙ λ i → (lUnitₖ 0ₖ ∙ λ j → rUnitₖ 0ₖ ((~ i) ∨ (~ j))) ∙ cong (λ x → rUnitₖ x (~ i)) a ∙ (λ j → rUnitₖ 0ₖ (~ i ∨ j)) ∙ sym (lUnitₖ 0ₖ))
                   ∙∙ (λ i → (lUnitₖ 0ₖ ∙ sym (rUnitₖ 0ₖ)) ∙ isCommΩK-based 2 (0ₖ +ₖ 0ₖ) (cong (_+ₖ 0ₖ) a) (rUnitₖ 0ₖ ∙ sym (lUnitₖ 0ₖ)) i)
                   ∙∙ λ i → assoc (lUnitₖ 0ₖ ∙ sym (rUnitₖ 0ₖ)) (symDistr ((lUnitₖ 0ₖ)) (sym (rUnitₖ 0ₖ)) (~ i)) (cong (_+ₖ 0ₖ) a) i)
                   ∙∙ cong (_∙ (cong (_+ₖ 0ₖ) a)) (rCancel (lUnitₖ 0ₖ ∙ sym (rUnitₖ 0ₖ)))
                   ∙∙ sym (lUnit (cong (_+ₖ 0ₖ) a))
private
  to₂ : coHom 2 (S₊ 1 × S₊ 1) → Int
  to₂ = fst (GroupEquiv.eq H²-T²≅ℤ)

  from₂ : Int → coHom 2 (S₊ 1 × S₊ 1)
  from₂ = invEq (GroupEquiv.eq H²-T²≅ℤ)

  to₁ : coHom 1 (S₊ 1 × S₊ 1) → Int × Int
  to₁ = fst (GroupEquiv.eq H¹-T²≅ℤ×ℤ)

  from₁ : Int × Int → coHom 1 (S₊ 1 × S₊ 1)
  from₁ = invEq (GroupEquiv.eq H¹-T²≅ℤ×ℤ)

  to₀ : coHom 0 (S₊ 1 × S₊ 1) → Int
  to₀ = fst (GroupEquiv.eq H⁰-T²≅ℤ)

  from₀ : Int → coHom 0 (S₊ 1 × S₊ 1)
  from₀ = invEq (GroupEquiv.eq H⁰-T²≅ℤ)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Data.List.FunctionsProven where

import      Lvl
open import Data.Boolean
open import Data.List as List using (List ; ∅ ; _⊰_)
import      Data.List.Functions as List
open import Data.List.Relation.Membership
open import Data.List.Relation.Quantification
open import Functional
open import Lang.Instance
open import Syntax.Function
open import Type

private variable ℓ : Lvl.Level
private variable A B T Result : Type{ℓ}
private variable P : T → Type{ℓ}

foldₗ : (Result → (x : T) → P(x) → Result) → Result → (l : List(T)) → AllElements(P)(l) → Result
foldₗ f result ∅       ∅         = result
foldₗ f result (x ⊰ l) (px ⊰ pl) = foldₗ f (f result x px) l pl

foldᵣ : ((x : T) → P(x) → Result → Result) → Result → (l : List(T)) → AllElements(P)(l) → Result
foldᵣ f init ∅       ∅         = init
foldᵣ f init (x ⊰ l) (px ⊰ pl) = f x px (foldᵣ f init l pl)

map : ((x : A) → P(x) → B) → ((l : List(A)) → AllElements(P)(l) → List(B))
map f ∅       ∅         = ∅
map f (x ⊰ l) (px ⊰ pl) = (f x px) ⊰ (map f l pl)

filter : ((x : T) → P(x) → Bool) → ((l : List(T)) → AllElements(P)(l) → List(T))
filter f ∅       ∅         = ∅
filter f (x ⊰ l) (px ⊰ pl) = (if(f(x) px) then (x List.⊰_) else id) (filter f l pl)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Type
open import Data.Nat.NP
open import Data.Product
open import Data.Sum.NP
open import Data.Zero
open import Data.Maybe
open import Data.One using (𝟙)
open import Data.Fin.NP using (Fin; Fin′; zero; suc;
                               inject₁; inject!;
                               Fin▹ℕ; ℕ▹Fin; [zero:_,suc:_])
open import Function.NP
open import Function.Extensionality
open import HoTT
open Equivalences
open import Type.Identities
open import Algebra.FunctionProperties.Eq
{-
open import Function.Related as FR
open import Function.Related.TypeIsomorphisms.NP
import Function.Inverse.NP as I
open I using (_↔_; inverses; module Inverse) renaming (_$₁_ to to; _$₂_ to from)
open import Relation.Binary.Product.Pointwise
open import Relation.Binary.Sum
-}
open import Relation.Binary.PropositionalEquality.NP
  renaming (!_ to ¡_)
open ≡-Reasoning

-- n ! ≡ product [1..n]

module v1 where
  _! : ℕ → ℕ
  zero  ! = 1
  suc n ! = (1 + n) * n !

  _!★ : ℕ → ★
  zero  !★ = 𝟙
  suc n !★ = Fin (1 + n) × n !★

  module _ {{_ : UA}} where
    !★≡Fin! : ∀ {n} → n !★ ≡ Fin (n !)
    !★≡Fin! {zero}  = ¡ Fin1≡𝟙
    !★≡Fin! {suc n} = ×= idp !★≡Fin! ∙ Fin-×-*

module v2 where
  _! : ℕ → ℕ
  _+1! : ℕ → ℕ

  zero  ! = 1
  suc n ! = n +1!

  n +1! = n ! + n * n !

  _!★ : ℕ → ★
  zero  !★ = 𝟙
  suc n !★ = n !★ ⊎ Fin n × n !★

  1+_!★ : ℕ → ★
  1+ n !★ = n !★ ⊎ Fin n × n !★

  module _ {{_ : UA}} where
    !★≡Fin! : ∀ {n} → n !★ ≡ Fin (n !)
    !★≡Fin! {zero}  = ¡ Fin1≡𝟙
    !★≡Fin! {suc n} = ⊎= !★≡Fin! (×= idp !★≡Fin! ∙ Fin-×-*)
                    ∙ Fin-⊎-+

productFin : ∀ n → (Fin n → ℕ) → ℕ
productFin zero    f = 1
productFin (suc n) f = f zero * productFin n (f ∘ suc)

product[0…_] : ℕ → (ℕ → ℕ) → ℕ
product[0… n ] f = productFin n (f ∘ Fin▹ℕ)
{-
product[0… zero  ] f = 1
product[0… suc n ] f = f zero * product[0… n ] (f ∘ suc)
-}

product[1…_] : ℕ → (ℕ → ℕ) → ℕ
product[1… zero  ] f = 1
product[1… suc n ] f = f 1 * product[1… n ] (f ∘ suc)

product[_to_] : ℕ → ℕ → (ℕ → ℕ) → ℕ
product[ start to stop ] f = product[0… stop ∸ start ] (f ∘ _+_ start)

{-
data Bnd (l : ℕ) : (h : ℕ) → Set where
  low : Bnd l (suc l)
  suc : ∀ {h} → Bnd l h → Bnd l (suc h)

Bnd▹ℕ : {l h : ℕ} → Bnd l h → ℕ
Bnd▹ℕ {l} low = l
Bnd▹ℕ (suc x) = suc (Bnd▹ℕ x)

productBnd : ∀ {l h} → l ≤ h → (Bnd l h → ℕ) → ℕ
productBnd z≤n f = {!!}
productBnd (s≤s p) f = {!!}

productBnd p f = {!f low * productBnd l h (f ∘ suc)!}
-}

test-product[1…3] : product[1… 3 ] ≡ (λ f → f 1 * (f 2 * (f 3 * 1)))
test-product[1…3] = idp

open v1
{-
adequate1 : ∀ n → n ! ≡ product[1… n ] id
adequate1 zero = ≡.refl
adequate1 (suc n) rewrite adequate1 n = {!!}
  Π{x∈1…n}x + n * Π{x∈1…n}x

  (1 + n) * Π{x∈1…n}x

  Π{x∈1…n}1+x
  -}

Π[0…_-1] : ℕ → (ℕ → ℕ) → ★
Π[0… n -1] f = Π (Fin n) (Fin ∘ f ∘ Fin▹ℕ)

Π[0…_] : ℕ → (ℕ → ℕ) → ★
Π[0… n ] = Π[0… suc n -1]

{-
Π[1…_] : ℕ → (ℕ → ℕ) → ★
Π[1… 0     ] f = 𝟙
Π[1… suc n ] f = {!!}
-}

Π[0…_-1]′ : ℕ → (ℕ → ℕ) → ★
Π[0… zero  -1]′ f = 𝟙
Π[0… suc n -1]′ f = Fin (f 0) × Π[0… n -1]′ (f ∘ suc)

Π[0…_]′ : ℕ → (ℕ → ℕ) → ★
Π[0… n ]′ = Π[0… suc n -1]′

{-
Π[1…_]′ : ℕ → (ℕ → ℕ) → ★
Π[1… zero  ]′ f = 𝟙
Π[1… suc n ]′ f = Fin (f 1) × Π[1… n ]′ (f ∘ suc)
-}

[zero:,suc:] = [zero:_,suc:_]
syntax [zero:,suc:] z (λ y → s) = [zero: z ,suc y :→ s ]

Π! : ℕ → ★
Π! n = Π[0… n ] suc

↺ : ℕ → ★
↺ n = Fin n → Fin n

Π!↺ : ∀ {n} → Π! n → ↺ (suc n)
Π!↺ {n} f = inject! ∘ f

Π!↺-inj : ∀ {n}(f : Π! n) → Injective (Π!↺ f)
Π!↺-inj f {x} {y} e = {!!}

-- Move to Type.Identities
module _ {{_ : UA}}{{_ : FunExt}} where
  ΠMaybe : ∀ {A : ★} {F : Maybe A → ★} →
           Π (Maybe A) F ≡ (F nothing × Π A (F ∘ just))
  ΠMaybe {A} {F}
    = (Π (Maybe A) F)
    ≡⟨ Π≃ Maybe≃𝟙⊎ (maybe (λ _ → idp) idp) ⟩
      (Π (𝟙 ⊎ A) [inl: (λ _ → F nothing) ,inr: F ∘ just ])
    ≡⟨ dist-×-Π ⟩
      ((𝟙 → F nothing) × Π A (F ∘ just))
    ≡⟨ ×= 𝟙→A≡A idp ⟩
      (F nothing × Π A (F ∘ just))
    ∎

  ΠFin0≡𝟙 : ∀ {F : Fin 0 → ★} → Π (Fin 0) F ≡ 𝟙
  ΠFin0≡𝟙 = Π= Fin0≡𝟘 (λ()) ∙ Π𝟘-uniq₀ (λ ())

  ΠFin1+ : ∀ n {F : Fin (1 + n) → ★} →
           Π (Fin (1 + n)) F ≡ (F zero × Π (Fin n) (F ∘ suc))
  ΠFin1+ n {F}
    = Π (Fin (1 + n)) F
    ≡⟨ Π≃ Fin∘suc≃𝟙⊎Fin [zero: idp ,suc _ :→ idp ] ⟩
       Π (𝟙 ⊎ Fin n) [inl: (λ _ → F zero) ,inr: F ∘ suc ]
    ≡⟨ dist-×-Π[] ⟩
       ((𝟙 → F zero) × Π (Fin n) (F ∘ suc))
    ≡⟨ ×= 𝟙→A≡A idp ⟩
       (F zero × Π (Fin n) (F ∘ suc))
    ∎

  rot : ∀ {n} → Fin (suc n) → Fin (suc n)
  rot {n} = [zero: ℕ▹Fin n ,suc: inject₁ ]

  ΠFin1+' : ∀ n {F : Fin (1 + n) → ★} →
           Π (Fin (1 + n)) F ≡ (F (ℕ▹Fin n) × Π (Fin n) (F ∘ inject₁))
  ΠFin1+' n {F} =
     Π (Fin (1 + n)) F
    ≡⟨ Π≃ Fin∘suc≃𝟙⊎Fin (λ x → {!WRONG!}) ⟩
     Π (𝟙 ⊎ Fin n) [inl: (λ _ → F {!!}) ,inr: F ∘ {!!} ]
    ≡⟨ {!!} ⟩
     Π (𝟙 ⊎ Fin n) [inl: (λ _ → F (ℕ▹Fin n)) ,inr: F ∘ inject₁ ]
    ≡⟨ dist-×-Π[] ⟩
     ((𝟙 → F (ℕ▹Fin n)) × Π (Fin n) (F ∘ inject₁))
    ≡⟨ ×= 𝟙→A≡A idp ⟩
     (F (ℕ▹Fin n) × Π (Fin n) (F ∘ inject₁))
    ∎

{-
  ΠFin1≡F0 : {F : Fin 1 → ★} → Π (Fin 1) F ≡ F zero
  ΠFin1≡F0 = ΠFin1+ 0 ∙ ×= idp ΠFin0≡𝟙 ∙ A×𝟙≡A

  ΠFin2≡F0×F1 : {F : Fin 2 → ★} → Π (Fin 2) F ≡ (F zero × F (suc zero))
  ΠFin2≡F0×F1 = ΠFin1+ 1 ∙ ×= idp ΠFin1≡F0

  test-Π[0…-1] : ∀ {f} → Π[0… 0 -1] f ≡ 𝟙
  test-Π[0…-1] = ΠFin0≡𝟙

  test-Π[0…0] : ∀ {f} → Π[0… 0 ] f ≡ Fin (f zero)
  test-Π[0…0] = ΠFin1≡F0

  test-Π[0…1] : ∀ {f} → Π[0… 1 ] f ≡ (Fin (f zero) × Fin (f (suc zero)))
  test-Π[0…1] = ΠFin2≡F0×F1

  ΠFin1+ʳ′ : ∀ n (F : ℕ → ★) →
               Π (Fin (1 + n)) (F ∘ Fin▹ℕ) ≡ (F n × Π (Fin n) (F ∘ Fin▹ℕ))
  ΠFin1+ʳ′ n F
      = Π (Fin (1 + n)) (F ∘ Fin▹ℕ)
      ≡⟨ Π=′ (Fin (1 + n)) F∘Fin▹ℕ≗F' ⟩
        Π (Fin (1 + n)) F'
      ≡⟨ ΠFin1+ n ⟩
        (F' zero × Π (Fin n) (F' ∘ suc))
      ≡⟨by-definition⟩
        (F n × Π (Fin n) (F ∘ Fin▹ℕ))
      ∎
    where F' : (x : Fin (suc n)) → ★₀
          F' zero = F n
          F' (suc x) = F (Fin▹ℕ x)
          F∘Fin▹ℕ≗F' : F ∘ Fin▹ℕ ≗ F'
          F∘Fin▹ℕ≗F' zero = {!!}
          F∘Fin▹ℕ≗F' (suc x₂) = {!!}

{-Π (Fin (1 + n)) (F ∘ Fin▹ℕ)
            ≡⟨ {!!} ⟩
               Π (𝟙 ⊎ Fin n) {!!}
            ≡⟨ {!dist-×-Π!} ⟩
               (F n × Π (Fin n) (F ∘ Fin▹ℕ))
            ∎
-}

module _ {{_ : UA}}{{_ : FunExt}} where
  Π≡Π′[0…_-1] : ∀ n f → Π[0… n -1]′ f ≡ Π[0… n -1] f
  Π≡Π′[0… zero  -1] f = ¡ ΠFin0≡𝟙
  Π≡Π′[0… suc n -1] f = Π[0… 1 + n -1]′ f
                     ≡⟨by-definition⟩
                       (Fin (f 0) × Π[0… n -1]′ (f ∘ suc))
                     ≡⟨ ×= idp (Π≡Π′[0… n -1] (f ∘ suc)) ⟩
                       (Fin (f 0) × Π[0… n -1] (f ∘ suc))
                     ≡⟨ ¡ ΠFin1+ n ⟩
                       Π[0… 1 + n -1] f
                     ∎

  Π≡Π′[0…_] : ∀ n f → Π[0… n ]′ f ≡ Π[0… n ] f
  Π≡Π′[0… n ] = Π≡Π′[0… suc n -1]
-- (A → B ⊎ C)

-- TODO
-- adequate! : ∀ n → Fin (suc n) × Fin (n !) ≡ Π (Fin n) (Fin′ ∘ suc)

example : ∀ {n} → (2 + n)! ≡ (2 + n) * (1 + n)!
example = idp

module _ {{_ : UA}}{{_ : FunExt}} where

{-
  -- WRONG
  adequate! : ∀ {n} → Fin (n !) ≡ Π[0… n -1] suc
  adequate! {zero}  = {!¡ ΠFin1≡F0!}
  adequate! {suc n} = (Fin ((1 + n)!))
                    ≡⟨by-definition⟩
                      Fin ((1 + n) * n !)
                    ≡⟨ ¡ Fin-×-* ⟩
                      (Fin (1 + n) × Fin (n !))
                    ≡⟨ ×= idp adequate! ⟩
                      (Fin (1 + n) × Π[0… n -1] suc)
                    ≡⟨ {!ΠFin1+!} ⟩
                      (Fin 1 × Π[0… n -1] (_+_ 2))
                    ≡⟨ ¡ ΠFin1+ n ⟩
                      Π[0… n ] suc
                    ∎
                    -}

  adequate! : ∀ {n} → Fin (n !) ≡ Π[0… n ] suc
  adequate! {zero}  = ¡ ΠFin1≡F0
  adequate! {suc n} = (Fin ((1 + n)!))
                    ≡⟨by-definition⟩
                      Fin ((1 + n) * n !)
                    ≡⟨ ¡ Fin-×-* ⟩
                      (Fin (1 + n) × Fin (n !))
                    ≡⟨ ×= idp adequate! ⟩
                      (Fin (1 + n) × Π[0… n ] suc)
                    ≡⟨ ¡ ΠFin1+ʳ′ (suc n) _ ⟩
                      ((x : Fin (2 + n)) → Fin (suc (Fin▹ℕ x)))
                    ≡⟨ idp ⟩
                      Π[0… 1 + n ] suc
                    ∎

{-
  adequate! : ∀ {n} → Fin ((1 + n)!) ≡ Π[0… n -1] suc
  adequate! {zero}  = {!idp!}
  adequate! {suc n} = (Fin ((2 + n)!))
                    ≡⟨ {!!} ⟩
                      Fin ((1 + n) * (1 + n)!)
                    ≡⟨ ¡ Fin-×-* ⟩
                      (Fin (1 + n) × Fin ((1 + n)!))
                    ≡⟨ ×= idp adequate! ⟩
                      (Fin (1 + n) × Π[0… n -1] suc)
                    ≡⟨ ¡ (ΠFin1+ʳ′ n (Fin ∘ suc)) ⟩
                      Π[0… suc n -1] suc
                    ∎
-}
{-

HI: (n+1)! ≡ Π n suc

(n+2)!
(n+2) * (n+1)!
(n+2) * Π n suc
(n+1) * Π n suc + Π n suc

(2+n)*(n! * 1+n)
(n! * 1+n) + (1+n)*(n! * 1+n)

≡ Π n (2+)
≡ 1 × Π n (2+)

(2+n) * Π n suc
Π (1+n) suc

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

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Ag03 where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties using (+-comm; *-comm; +-suc)

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

infix 4 _≤_

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
  → m ≤ n

inv-s≤s (s≤s m≤n) = m≤n

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
  → m ≡ zero

inv-z≤n z≤n = refl

≤-refl : ∀ {n : ℕ} → n ≤ n
≤-refl {0} = z≤n
≤-refl {suc n} = s≤s ≤-refl

≤-trans : ∀ {m n p : ℕ } → m ≤ n → n ≤ p → m ≤ p
≤-trans z≤n _ = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

≤-antisym : ∀ {m n : ℕ} → m ≤ n → n ≤ m → m ≡ n
≤-antisym z≤n z≤n = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)

data Total (m n : ℕ) : Set where
  forward :
    m ≤ n → Total m n
  flipped :
    n ≤ m → Total m n

+-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
    -------------
  → n + p ≤ n + q
+-monoʳ-≤ zero    p q p≤q  =  p≤q
+-monoʳ-≤ (suc n) p q p≤q  =  s≤s (+-monoʳ-≤ n p q p≤q)

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    -------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n  rewrite +-comm m p | +-comm n p  = +-monoʳ-≤ p m n m≤n

+-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q  =  ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)

*-mono-ʳ : ∀ (n p q : ℕ) → p ≤ q → n * p ≤ n * q
*-mono-ʳ 0 _ _ p≤q = z≤n
*-mono-ʳ (suc n) p q p≤q = +-mono-≤ p q (n * p) (n * q) p≤q (*-mono-ʳ n p q p≤q)

*-mono-ˡ : ∀ (m n p : ℕ) → m ≤ n → m * p ≤ n * p
*-mono-ˡ m n p m≤n rewrite *-comm m p | *-comm n p = *-mono-ʳ p m n m≤n

*-mono : ∀ (m n p q : ℕ) → m ≤ n → p ≤ q → m * p ≤ n * q
*-mono m n p q m≤n p≤q = ≤-trans (*-mono-ˡ m n p m≤n) (*-mono-ʳ n p q p≤q)

infix 4 _⟨_

data _⟨_ : ℕ → ℕ → Set where
  z⟨s : ∀ {n : ℕ} → 0 ⟨ suc n
  s⟨s : ∀ {m n : ℕ} → m ⟨ n → suc m ⟨ suc n

⟨-trans : ∀ {m n p : ℕ} → m ⟨ n → n ⟨ p → m ⟨ p
⟨-trans z⟨s (s⟨s n⟨p) = z⟨s
⟨-trans (s⟨s m⟨n) (s⟨s n⟨p) = s⟨s (⟨-trans m⟨n n⟨p)

data Total-trichotomy (m n : ℕ) : Set where
  lt : m ⟨ n → Total-trichotomy m n
  eq : m ≡ n → Total-trichotomy m n
  gt : n ⟨ m → Total-trichotomy m n

trichotomy : ∀ (m n : ℕ) → Total-trichotomy m n
trichotomy zero zero = eq refl
trichotomy zero (suc n) = lt z⟨s
trichotomy (suc m) zero = gt z⟨s
trichotomy (suc m) (suc n) with trichotomy m n
...                          | lt m⟨n = lt (s⟨s m⟨n)
...                          | eq m≡n = eq (cong suc m≡n)
...                          | gt n⟨m = gt (s⟨s n⟨m)

+-monoʳ-⟨ : ∀ (n p q : ℕ) → p ⟨ q → n + p ⟨ n + q
+-monoʳ-⟨ 0 _ _ p⟨q = p⟨q
+-monoʳ-⟨ (suc n) p q p⟨q = s⟨s (+-monoʳ-⟨ n p q p⟨q)

+-monoˡ-⟨ : ∀ (m n p : ℕ) → m ⟨ n → m + p ⟨ n + p
+-monoˡ-⟨ m n p m⟨n rewrite +-comm m p | +-comm n p = +-monoʳ-⟨ p m n m⟨n

+-mono-⟨ : ∀ (m n p q : ℕ) → m ⟨ n → p ⟨ q → m + p ⟨ n + q
+-mono-⟨ m n p q m⟨n p⟨q = ⟨-trans (+-monoˡ-⟨ m n p m⟨n) (+-monoʳ-⟨ n p q p⟨q)

≤-iffˡ-⟨ : ∀ (m n : ℕ) → suc m ≤ n → m ⟨ n
≤-iffˡ-⟨ 0 _ (s≤s z≤n) = z⟨s
≤-iffˡ-⟨ (suc m) (suc n) (s≤s sm≤n) = s⟨s (≤-iffˡ-⟨ m n sm≤n)

≤-iffʳ-⟨ : ∀ (m n : ℕ) → m ⟨ n → suc m ≤ n
≤-iffʳ-⟨ .0 .(suc _) z⟨s = s≤s z≤n
≤-iffʳ-⟨ .(suc _) .(suc _) (s⟨s m⟨n) = s≤s (≤-iffʳ-⟨ _ _ m⟨n)

data Even : ℕ → Set
data Odd  : ℕ → Set

data Even where

  zero :
      ---------
      Even zero

  suc  : ∀ {n : ℕ}
    → Odd n
      ------------
    → Even (suc n)

data Odd where

  suc   : ∀ {n : ℕ}
    → Even n
      -----------
    → Odd (suc n)

e+e≡e : ∀ {m n : ℕ}
  → Even m
  → Even n
    ------------
  → Even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → Odd m
  → Even n
    -----------
  → Odd (m + n)

e+e≡e zero     en  =  en
e+e≡e (suc om) en  =  suc (o+e≡o om en)

o+e≡o (suc em) en  =  suc (e+e≡e em en)

o+o≡e : ∀ {m n : ℕ} → Odd m → Odd n → Even (m + n)
o+o≡e {m} {suc n} om (suc en) rewrite +-suc m n = suc (o+e≡o om en)

e+o≡o : ∀ (m n : ℕ) → Even m → Odd n → Odd(m + n)
e+o≡o .0 .(suc _) zero (suc x) = suc x
e+o≡o (suc m) (suc n) (suc x) (suc x₁) rewrite +-suc m n = suc (suc (o+e≡o x x₁))

infixl 7 _e*e_ _o*e_ _o*o_ _e*o_
_e*e_ : ∀ {m n : ℕ} → Even m → Even n → Even (m * n)
_o*e_ : ∀ {m n : ℕ} → Odd  m → Even n → Even (m * n)
_o*o_ : ∀ {m n : ℕ} → Odd  m → Odd  n → Odd  (m * n)
_e*o_ : ∀ {m n : ℕ} → Even m → Odd  n → Even (m * n)

zero e*e en  = zero
suc x e*e en = e+e≡e en (x o*e en)

suc x o*e en = e+e≡e en (x e*e en)

suc x o*o on = o+e≡o on (x e*o on)

zero e*o on  = zero
suc x e*o on = o+o≡e on (x o*o on)

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


text:
------------------------------------------------------------------------------
-- Simple example of a nested recursive function
------------------------------------------------------------------------------

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

-- From: Ana Bove and Venanzio Capretta. Nested general recursion and
-- partiality in type theory. Vol. 2152 of LNCS. 2001.

module FOT.FOTC.Program.Nest.NestConditional where

open import FOTC.Base

------------------------------------------------------------------------------
-- The nest function.
postulate
  nest    : D → D
  nest-eq : ∀ n → nest n ≡ (if (iszero₁ n)
                              then zero
                              else (nest (nest (pred₁ n))))
{-# ATP axiom nest-eq #-}


text:
{-# OPTIONS --guardedness-preserving-type-constructors #-}
module Issue602 where

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

data CoNat : Set0 where
  z : CoNat
  s : ∞ CoNat → CoNat

record A : Set2 where
  field
    f : Set1

record B (a : ∞ A) : Set1 where
  field
    f : A.f (♭ a)

postulate
  a : A

e : CoNat → A
e z = a
e (s n) = record
  { f = B (♯ e (♭ n))
  }

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Data.Fin.Subset.Dec where
open import Data.Nat as ℕ
open import Data.Fin as Fin
open import Data.Fin.Subset
open import Relation.Nullary
open import Relation.Unary renaming (Decidable to Decidable₁) using ()
open import Function using (_∘_)
open import Data.Vec using ([]; _∷_)

subset : ∀ {n}{p} {P : Fin n → Set p} → Decidable₁ P → Subset n
subset {zero} dec = []
subset {suc n} dec with dec (# 0)
subset {suc n} dec | yes p0 = inside ∷ subset (dec ∘ Fin.suc)
subset {suc n} dec | no ¬p0 = outside ∷ subset (dec ∘ Fin.suc)

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


text:
------------------------------------------------------------------------------
-- Well-founded induction on natural numbers
------------------------------------------------------------------------------

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

-- Adapted from
-- http://www.iis.sinica.edu.tw/~scm/2008/well-founded-recursion-and-accessibility/
-- and the Agda standard library 0.8.1.

module FOT.FOTC.Data.Nat.Induction.Acc.WF-I where

open import FOTC.Base

open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- The accessibility predicate: x is accessible if everything which is
-- smaller than x is also accessible (inductively).
data AccLT : D → Set where
 accLT : ∀ {x} → N x → (∀ {y} → N y → y < x → AccLT y) → AccLT x

accFoldLT : {P : D → Set} →
            (∀ {x} → N x → (∀ {y} → N y → y < x → P y) → P x) →
            ∀ {x} → N x → AccLT x → P x
accFoldLT f Nx (accLT _ h) = f Nx (λ Ny y<x → accFoldLT f Ny (h Ny y<x))

-- The accessibility predicate encodes what it means to be
-- well-founded; if all elements are accessible, then LT is
-- well-founded.
WellFoundedLT : Set
WellFoundedLT = ∀ {x} → N x → AccLT x

WellFoundedInductionLT : {P : D → Set} →
                         WellFoundedLT →
                         (∀ {x} → N x → (∀ {y} → N y → y < x → P y) → P x) →
                         ∀ {x} → N x → P x
WellFoundedInductionLT wf f Nx = accFoldLT f Nx (wf Nx)


text:
module vector-test-ctors where

open import bool
open import list
open import vector

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

test-vector : 𝕃 (𝕍 𝔹 2)
test-vector = (ff :: tt :: []) :: (tt :: ff :: []) :: (tt :: ff :: []) :: []

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
open import Relation.Binary.PropositionalEquality using ( refl )
open import Web.Semantic.DL.Category.Object using ( Object )
open import Web.Semantic.DL.Category.Morphism using ( _≣_ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Tensor using ( _⊗_ ; _⟨⊗⟩_ )
open import Web.Semantic.DL.Category.Unit using ( I )
open import Web.Semantic.DL.Category.Wiring using
  ( identity ; symm ; assoc ; assoc⁻¹ ; unit₁ ; unit₁⁻¹ ; unit₂ ; unit₂⁻¹ )
open import Web.Semantic.DL.Category.Properties.Wiring using
  ( rewriting ; rewrite-compose ; rewrite-tensor
  ; rewrite-identity ; rewrite-symm ; rewrite-assoc ; rewrite-assoc⁻¹
  ; rewrite-unit₁ ; rewrite-unit₁⁻¹ ; rewrite-unit₂ ; rewrite-unit₂⁻¹ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.Util using ( _≡⊎≡_ )

module Web.Semantic.DL.Category.Properties.Tensor.Isomorphisms
  {Σ : Signature} {S T : TBox Σ} where

symm-iso : ∀ (A₁ A₂ : Object S T) →
  (symm A₁ A₂ ∙ symm A₂ A₁ ≣ identity (A₁ ⊗ A₂))
symm-iso A₁ A₂ =
  rewriting
    (rewrite-compose (rewrite-symm A₁ A₂) (rewrite-symm A₂ A₁))
    ((λ x → refl) ≡⊎≡ (λ x → refl))
    (rewrite-identity (A₁ ⊗ A₂))

assoc-iso : ∀ (A₁ A₂ A₃ : Object S T) →
  (assoc A₁ A₂ A₃ ∙ assoc⁻¹ A₁ A₂ A₃ ≣ identity ((A₁ ⊗ A₂) ⊗ A₃))
assoc-iso A₁ A₂ A₃ = rewriting
  (rewrite-compose (rewrite-assoc A₁ A₂ A₃) (rewrite-assoc⁻¹ A₁ A₂ A₃))
  (((λ x → refl) ≡⊎≡ (λ x → refl)) ≡⊎≡ (λ x → refl))
  (rewrite-identity ((A₁ ⊗ A₂) ⊗ A₃))

assoc⁻¹-iso : ∀ (A₁ A₂ A₃ : Object S T) →
  (assoc⁻¹ A₁ A₂ A₃ ∙ assoc A₁ A₂ A₃ ≣ identity (A₁ ⊗ (A₂ ⊗ A₃)))
assoc⁻¹-iso A₁ A₂ A₃ = rewriting
  (rewrite-compose (rewrite-assoc⁻¹ A₁ A₂ A₃) (rewrite-assoc A₁ A₂ A₃))
  ((λ x → refl) ≡⊎≡ ((λ x → refl) ≡⊎≡ (λ x → refl)))
  (rewrite-identity (A₁ ⊗ (A₂ ⊗ A₃)))

unit₁-iso : ∀ (A : Object S T) →
  (unit₁ A ∙ unit₁⁻¹ A ≣ identity (I ⊗ A))
unit₁-iso A = rewriting
  (rewrite-compose (rewrite-unit₁ A) (rewrite-unit₁⁻¹ A))
  ((λ ()) ≡⊎≡ (λ x → refl))
  (rewrite-identity (I ⊗ A))

unit₁⁻¹-iso : ∀ (A : Object S T) →
  (unit₁⁻¹ A ∙ unit₁ A ≣ identity A)
unit₁⁻¹-iso A = rewriting
  (rewrite-compose (rewrite-unit₁⁻¹ A) (rewrite-unit₁ A))
  (λ x → refl)
  (rewrite-identity A)

unit₂-iso : ∀ (A : Object S T) →
  (unit₂ A ∙ unit₂⁻¹ A ≣ identity (A ⊗ I))
unit₂-iso A = rewriting
  (rewrite-compose (rewrite-unit₂ A) (rewrite-unit₂⁻¹ A))
  ((λ x → refl) ≡⊎≡ (λ ()))
  (rewrite-identity (A ⊗ I))

unit₂⁻¹-iso : ∀ (A : Object S T) →
  (unit₂⁻¹ A ∙ unit₂ A ≣ identity A)
unit₂⁻¹-iso A = rewriting
  (rewrite-compose (rewrite-unit₂⁻¹ A) (rewrite-unit₂ A))
  (λ x → refl)
  (rewrite-identity A)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

-- Equalizers in a Category C
module Categories.Diagram.Equalizer {o ℓ e} (C : Category o ℓ e) where

open Category C
open HomReasoning

open import Level
open import Data.Product as Σ
open import Function using (_$_)
open import Categories.Morphism C
open import Categories.Morphism.Reasoning C

private
  variable
    A B X : Obj
    h i j k : A ⇒ B

record Equalizer (f g : A ⇒ B) : Set (o ⊔ ℓ ⊔ e) where
  field
    {obj} : Obj
    arr   : obj ⇒ A

    equality  : f ∘ arr ≈ g ∘ arr
    equalize  : ∀ {h : X ⇒ A} → f ∘ h ≈ g ∘ h → X ⇒ obj
    universal : ∀ {eq : f ∘ h ≈ g ∘ h} → h ≈ arr ∘ equalize eq
    unique    : ∀ {eq : f ∘ h ≈ g ∘ h} → h ≈ arr ∘ i → i ≈ equalize eq

  unique′ : (eq eq′ : f ∘ h ≈ g ∘ h) → equalize eq ≈ equalize eq′
  unique′ eq eq′ = unique universal

  id-equalize : id ≈ equalize equality
  id-equalize = unique (sym identityʳ)

  equalize-resp-≈ : ∀ {eq : f ∘ h ≈ g ∘ h} {eq′ : f ∘ i ≈ g ∘ i} →
    h ≈ i → equalize eq ≈ equalize eq′
  equalize-resp-≈ {h = h} {i = i} {eq = eq} {eq′ = eq′} h≈i = unique $ begin
    i                 ≈˘⟨ h≈i ⟩
    h                 ≈⟨ universal ⟩
    arr ∘ equalize eq ∎

  equalize-resp-≈′ : (eq : f ∘ h ≈ g ∘ h) → (eq′ : f ∘ i ≈ g ∘ i) →
    h ≈ i → j ≈ equalize eq → k ≈ equalize eq′ → j ≈ k
  equalize-resp-≈′ {j = j} {k = k} eq eq′ h≈i eqj eqk = begin
    j            ≈⟨ eqj ⟩
    equalize eq  ≈⟨ equalize-resp-≈ h≈i ⟩
    equalize eq′ ≈˘⟨ eqk ⟩
    k            ∎

  equality-∘ : f ∘ arr ∘ h ≈ g ∘ arr ∘ h
  equality-∘ {h = h} = begin
    f ∘ arr ∘ h   ≈⟨ pullˡ equality ⟩
    (g ∘ arr) ∘ h ≈⟨ assoc ⟩
    g ∘ arr ∘ h   ∎

  unique-diagram : arr ∘ h ≈ arr ∘ i → h ≈ i
  unique-diagram {h = h} {i = i} eq = begin
    h                           ≈⟨ unique (sym eq) ⟩
    equalize (extendʳ equality) ≈˘⟨ unique refl ⟩
    i                           ∎

Equalizer⇒Mono : (e : Equalizer h i) → Mono (Equalizer.arr e)
Equalizer⇒Mono e f g eq =
  equalize-resp-≈′ equality-∘ equality-∘ eq (unique refl) (unique refl)
  where open Equalizer e

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
open import Everything

module Test.SubstitunctionPropId {𝔭} (𝔓 : Ø 𝔭) where

open Substitunction 𝔓

relpropid-Substitunction : ∀ {m n ℓ} {f : Substitunction m n} (P : LeftExtensionṖroperty ℓ Substitunction Proposextensequality m) (let P₀ = π₀ (π₀ P)) → P₀ f → P₀ (ε ∙ f)
relpropid-Substitunction P pf = hmap _ P pf


text:
module UniDB.Morph.Depth where

open import UniDB.Spec
open import Data.Sum

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

data Depth (Ξ : MOR) : MOR where
  depth : {γ₁ γ₂ : Dom} (ξ : Ξ γ₁ γ₂) (δ : Dom) →
    Depth Ξ (γ₁ ∪ δ) (γ₂ ∪ δ)

Fin-∪ : {γ₁ : Dom} (γ₂ δ : Dom) (i : Ix (γ₁ ∪ δ)) → Ix γ₁ ⊎ Ix (γ₂ ∪ δ)
Fin-∪ γ₂ zero    i       = inj₁ i
Fin-∪ γ₂ (suc δ) zero    = inj₂ zero
Fin-∪ γ₂ (suc δ) (suc i) = map id suc (Fin-∪ γ₂ δ i)

instance
  iLkDepth :
    {T : STX} {{vrT : Vr T}} {{wkT : Wk T}}
    {Ξ : MOR} {{lkTΞ : Lk T Ξ}} →
    Lk T (Depth Ξ)
  lk {{iLkDepth {T} {Ξ}}} (depth {γ₁} {γ₂} ξ δ) i with Fin-∪ γ₂ δ i
  ... | inj₁ j = wk δ (lk {T} {Ξ} ξ j)
  ... | inj₂ j = vr {T = T} j

  iUpDepth : {Ξ : MOR} → Up (Depth Ξ)
  _↑₁ {{iUpDepth}} (depth ξ δ) = depth ξ (suc δ)
  _↑_ {{iUpDepth {Ξ}}} ξ 0 = ξ
  _↑_ {{iUpDepth {Ξ}}} ξ (suc δ⁺) = ξ ↑ δ⁺ ↑₁
  ↑-zero {{iUpDepth}} ξ = refl
  ↑-suc {{iUpDepth {Ξ}}} ξ δ⁺ = refl

  iWkmDepth : {Ξ : MOR} {{wkmΞ : Wkm Ξ}} → Wkm (Depth Ξ)
  wkm {{iWkmDepth {Ξ}}} δ = depth (wkm {Ξ} δ) 0

  iLkWkmDepth :
    {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{wkVrT : WkVr T}}
    {Ξ : MOR} {{lkTΞ : Lk T Ξ}} {{wkmΞ : Wkm Ξ}} {{lkWkmΞ : LkWkm T Ξ}} →
    LkWkm T (Depth Ξ)
  lk-wkm {{iLkWkmDepth {T} {Ξ}}} δ i = begin
    wk 0 (lk {T} {Ξ} (wkm δ) i) ≡⟨ wk-zero (lk {T} {Ξ} (wkm δ) i) ⟩
    lk {T} {Ξ} (wkm δ) i        ≡⟨ lk-wkm {T} {Ξ} δ i ⟩
    vr (wk δ i)         ∎

  iBetaDepth : {T : STX} {Ξ : MOR} {{betaTΞ : Beta T Ξ}} → Beta T (Depth Ξ)
  beta {{iBetaDepth {T} {Ξ}}} t = depth (beta {T} {Ξ} t) 0

  iLkUpDepth :
    {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{wkVrT : WkVr T}}
    {Ξ : MOR} {{lkTΞ : Lk T Ξ}} →
    LkUp T (Depth Ξ)
  lk-↑₁-zero {{iLkUpDepth {T} {Ξ}}} (depth ξ δ) = refl
  lk-↑₁-suc {{iLkUpDepth {T} {Ξ}}} (depth {γ₁} {γ₂} ξ δ) i with Fin-∪ γ₂ δ i
  ... | inj₁ j = wk-suc {T} δ (lk {T} {Ξ} ξ j)
  ... | inj₂ j = sym (wk₁-vr {T} j)

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

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
{- NEW TRANSLATION STUFF: same thing but interpret source nat as ♭nat-}

open import Preliminaries
open import Source
open import Pilot

module Translation-New where

  mutual
    ⟨⟨_⟩⟩ : Tp → CTp
    ⟨⟨ unit ⟩⟩ = unit
    ⟨⟨ nat ⟩⟩ = nat
    ⟨⟨ susp A ⟩⟩ = || A ||
    ⟨⟨ A ->s B ⟩⟩ = ⟨⟨ A ⟩⟩ ->c || B ||
    ⟨⟨ A ×s B ⟩⟩ = ⟨⟨ A ⟩⟩ ×c ⟨⟨ B ⟩⟩
    ⟨⟨ list A ⟩⟩ = list ⟨⟨ A ⟩⟩
    ⟨⟨ bool ⟩⟩ = bool

    ||_|| : Tp → CTp
    || τ || = C ×c ⟨⟨ τ ⟩⟩

  ⟨⟨_⟩⟩c : Source.Ctx → Pilot.Ctx
  ⟨⟨ [] ⟩⟩c = []
  ⟨⟨ x :: Γ ⟩⟩c = ⟨⟨ x ⟩⟩ :: ⟨⟨ Γ ⟩⟩c

  interp-Cost : ∀{Γ} → Cost → Γ Pilot.|- C
  interp-Cost 0c = 0C
  interp-Cost 1c = 1C
  interp-Cost (m +c n) = plusC (interp-Cost m) (interp-Cost n)

  lookup : ∀{Γ τ} → τ Source.∈ Γ → ⟨⟨ τ ⟩⟩ Pilot.∈ ⟨⟨ Γ ⟩⟩c
  lookup i0 = i0
  lookup (iS x) = iS (lookup x)

  -- translation from source expressions to complexity expressions
  ||_||e : ∀{Γ τ} → Γ Source.|- τ → ⟨⟨ Γ ⟩⟩c Pilot.|- || τ ||
  || unit ||e = prod 0C unit
  || var x ||e = prod 0C (var (lookup x))
  || z ||e = prod 0C z
  || suc e ||e = prod (l-proj (|| e ||e)) (s (r-proj (|| e ||e)))
  || rec e e0 e1 ||e = (l-proj (|| e ||e)) +C (rec (r-proj || e ||e) (1C +C || e0 ||e) (1C +C || e1 ||e))
  || lam e ||e = prod 0C (lam || e ||e)
  || app e1 e2 ||e = prod (plusC (plusC (l-proj (|| e1 ||e)) (l-proj (|| e2 ||e))) (l-proj (app (r-proj (|| e1 ||e)) (r-proj (|| e2 ||e)))))
                          (r-proj (app (r-proj (|| e1 ||e)) (r-proj (|| e2 ||e))))
  || prod e1 e2 ||e = prod (plusC (l-proj (|| e1 ||e)) (l-proj (|| e2 ||e))) (prod (r-proj (|| e1 ||e)) (r-proj (|| e2 ||e)))
  || delay e ||e = prod 0C (|| e ||e)
  || force e ||e = prod (plusC (l-proj (|| e ||e)) (l-proj (r-proj || e ||e))) (r-proj (r-proj (|| e ||e)))
  || split e0 e1 ||e = prod (plusC (l-proj (|| e0 ||e)) (l-proj E1)) (r-proj E1)
    where E1 = (Pilot.subst || e1 ||e (Pilot.lem4 (l-proj (r-proj || e0 ||e)) (r-proj (r-proj || e0 ||e))))
  || nil ||e = prod 0C nil
  || e ::s e₁ ||e = prod (plusC (l-proj || e ||e) (l-proj || e₁ ||e)) ((r-proj || e ||e) ::c (r-proj || e₁ ||e))
  || listrec e e₁ e₂ ||e = l-proj || e ||e +C listrec (r-proj || e ||e) (1C +C || e₁ ||e) (1C +C || e₂ ||e)
  || true ||e = prod 0C true
  || false ||e = prod 0C false

max_stars_repo_name: benhuds/Agda

max_issues_repo_name: benhuds/Agda

max_forks_repo_name: benhuds/Agda


text:
-- Andreas, 2020-03-27, re #3684

record R : Set₁ where

_ : R
_ = record { f = Set; f = Set }

-- Should complain about alien fields rather than duplicate fields

-- The record type R does not have the fields f, f
-- when checking that the expression record { f = Set ; f = Set } has type R

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------------
-- Agda internal syntax
------------------------------------------------------------------------------

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

-- Tested with Agda development version on 25 February 2013.

module InternalSyntax where

------------------------------------------------------------------------------
-- Sets

postulate A B C : Set

-- El {getSort = Type (Max [ClosedLevel 1]), unEl = Sort (Type (Max []))}

postulate A₁ : Set₁

-- El {getSort = Type (Max [ClosedLevel 2]), unEl = Sort (Type (Max [ClosedLevel 1]))}

------------------------------------------------------------------------------
-- The term is Def

postulate def : A

-- El {getSort = Type (Max []), unEl = Def InternalSyntax.A []}

------------------------------------------------------------------------------
-- The term is Pi

postulate fun₁ : A → B

-- El {getSort = Type (Max []),
--    unEl = Pi []r(El {getSort = Type (Max []), unEl = Def InternalSyntax.A []})
--              (NoAbs "_" El {getSort = Type (Max []), unEl = Def InternalSyntax.B []})}

postulate fun₂ : A → B → C

-- El {getSort = Type (Max []),
--    unEl = Pi []r(El {getSort = Type (Max []), unEl = Def InternalSyntax.A []})
--           (NoAbs "_" El {getSort = Type (Max []),
--                      unEl = Pi []r(El {getSort = Type (Max []), unEl = Def InternalSyntax.B []})
--                            (NoAbs "_" El {getSort = Type (Max []), unEl = Def InternalSyntax.C []})})}

postulate fun₃ : (a : A) → B

-- El (Type (Max []))
--    (Pi r(El (Type (Max []))
--             (Def InternalSyntax.A []))
--        (Abs "a" El (Type (Max []))
--                 (Def InternalSyntax.B [])))

-- El {getSort = Type (Max []),
--    unEl = Pi []r(El {getSort = Type (Max []), unEl = Def InternalSyntax.A []})
--              (NoAbs "a" El {getSort = Type (Max []), unEl = Def InternalSyntax.B []})}

postulate P : A → Set

-- El {getSort = Type (Max [ClosedLevel 1]),
--    unEl = Pi []r(El {getSort = Type (Max []), unEl = Def InternalSyntax.A []})
--              (NoAbs "_" El {getSort = Type (Max [ClosedLevel 1]), unEl = Sort (Type (Max []))})}

postulate fun₅ : (a : A) → P a

-- El {getSort = Type (Max []),
--    unEl = Pi []r(El {getSort = Type (Max []), unEl = Def InternalSyntax.A []})
--             (Abs "a" El {getSort = Type (Max []), unEl = Def InternalSyntax.P [[]r(Var 0 [])]})}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
module Graph where

import      Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Data.List
open import Logic.Propositional{Lvl.𝟎}
open import Logic.Predicate{Lvl.𝟎}{Lvl.𝟎}
open import Relator.Equals{Lvl.𝟎}
open import Data.List.Relation.Membership{Lvl.𝟎} using (_∈_)

-- EdgeClass(V)(E) means that E is a type which can represent an edge between vertices of type V.
record EdgeClass (V : Set) (Self : Set) : Set where
  constructor edgeInstance
  field
    from           : Self → V
    to             : Self → V
    _withVertices_ : Self → (V ⨯ V) → Self

module Edge where
  open EdgeClass ⦃ ... ⦄ public

instance
  EdgeInstance-Tuple : ∀{V} → EdgeClass(V)(V ⨯ V)
  Edge.from          ⦃ EdgeInstance-Tuple ⦄ (v₁ , v₂) = v₁
  Edge.to            ⦃ EdgeInstance-Tuple ⦄ (v₁ , v₂) = v₂
  Edge._withVertices_ ⦃ EdgeInstance-Tuple ⦄ (v₁ , v₂) (w₁ , w₂) = (w₁ , w₂)

record Graph (V : Set) (E : Set) ⦃ _ : EdgeClass(V)(E) ⦄ : Set where
  constructor graph

  field
    edges : List(E)

  -- Propositions
  HasEdge[_⟶_] : V → V → Set
  HasEdge[_⟶_](v₁)(v₂) = ∃(edge ↦ (edge ∈ edges)∧(Edge.from(edge) ≡ v₁)∧(Edge.to(edge) ≡ v₂))

  HasEdge[_⟵_] : V → V → Set
  HasEdge[_⟵_](v₁)(v₂) = HasEdge[_⟶_](v₂)(v₁)

  HasEdge[_⟷_] : V → V → Set
  HasEdge[_⟷_](v₁)(v₂) = HasEdge[_⟵_](v₁)(v₂) ∧ HasEdge[_⟶_](v₁)(v₂)

  data Path : V → V → Set where
    PathIntro        : ∀{v₁ v₂ : V} → HasEdge[ v₁ ⟶ v₂ ] → Path(v₁)(v₂)
    PathTransitivity : ∀{v₁ v₂ v₃ : V} → Path(v₁)(v₂) → Path(v₂)(v₃) → Path(v₁)(v₃)

  Connected : V → V → Set
  Connected(v₁)(v₂) = Path(v₁)(v₂)

  Disconnected : V → V → Set
  Disconnected(v₁)(v₂) = ¬(Connected(v₁)(v₂))

  -- Constructions
  mapVertices : ∀{V₂} → ⦃ _ : EdgeClass(V₂)(E) ⦄ → (V → V₂) → Graph(V₂)(E)
  mapVertices(f) = record{edges = map(edge ↦ (edge Edge.withVertices(f(Edge.from(edge)) , f(Edge.to(edge))))) (edges)}

  -- Boolean testing
  -- with-edge
  -- without-edge
  -- has-edge
  -- is-connected
  -- is-disconnected


text:
-- Andreas, 2017-03-27 fixing regression #2472

-- Auto should be applicable also outside function clauses

-- {-# OPTIONS -v auto:100 #-}

open import Agda.Primitive

test : Set {!!}
test = Set

-- Auto should succeed on this goal

max_forks_repo_name: Agda-zh/agda


text:
module TermUnification where

open import OscarPrelude
open import Delay
open import VariableName
open import FunctionName
open import Arity
open import Vector
open import Term

mutual
  substituteTerm⇑ : VariableName → Term → ∀ {i} → Term → Delay i Term
  substituteTerm⇑ 𝑥ₛ τₛ τ@(variable 𝑥)  = now $ ifYes 𝑥ₛ ≟ 𝑥 then τₛ else τ
  substituteTerm⇑ 𝑥ₛ τₛ (function 𝑓 τs) =
    substituteTerms⇑ 𝑥ₛ τₛ τs >>= λ τsₛ →
    now $ function 𝑓 τsₛ

  substituteTerms⇑ : VariableName → Term → ∀ {i} → Terms → Delay i Terms
  substituteTerms⇑ 𝑥ₛ τₛ ⟨ ⟨ [] ⟩ ⟩ = now ⟨ ⟨ [] ⟩ ⟩
  substituteTerms⇑ 𝑥ₛ τₛ ⟨ ⟨ τ ∷ τs ⟩ ⟩ =
    let τs = substituteTerms⇑ 𝑥ₛ τₛ ⟨ ⟨ τs ⟩ ⟩
        τ = substituteTerm⇑ 𝑥ₛ τₛ τ in
    τs >>= λ { ⟨ ⟨ τs ⟩ ⟩ →
    τ >>= λ { τ →
    now $ ⟨ ⟨ τ ∷ τs ⟩ ⟩ } }

substituteTerms⇓ : (𝑥ₛ : VariableName) → (τₛ : Term) → (τs : Terms) → substituteTerms⇑ 𝑥ₛ τₛ τs ⇓
substituteTerms⇓ 𝑥ₛ τₛ ⟨ ⟨ [] ⟩ ⟩ = _ , now⇓
substituteTerms⇓ 𝑥ₛ τₛ ⟨ ⟨ (variable 𝑥) ∷ τs ⟩ ⟩ = _ , substituteTerms⇓ 𝑥ₛ τₛ ⟨ ⟨ τs ⟩ ⟩ ⇓>>=⇓ now⇓
substituteTerms⇓ 𝑥ₛ τₛ ⟨ ⟨ (function 𝑓 τs₁) ∷ τs ⟩ ⟩ = _ , substituteTerms⇓ 𝑥ₛ τₛ ⟨ ⟨ τs ⟩ ⟩ ⇓>>=⇓ ((substituteTerms⇓ 𝑥ₛ τₛ τs₁ ⇓>>=⇓ now⇓) >>=⇓ now⇓)

substituteTerm⇓ : (𝑥ₛ : VariableName) → (τₛ : Term) → (τ : Term) → substituteTerm⇑ 𝑥ₛ τₛ τ ⇓
substituteTerm⇓ 𝑥ₛ τₛ (variable 𝑥) = _ , now⇓
substituteTerm⇓ 𝑥ₛ τₛ (function 𝑓 τs) = _ , substituteTerms⇓ 𝑥ₛ τₛ τs ⇓>>=⇓ now⇓

substitute : VariableName → Term → Term → Term
substitute 𝑥ₛ τₛ τ = fst $ substituteTerm⇓ 𝑥ₛ τₛ τ

data AListOfSubstitutions : Set
 where
  [] : AListOfSubstitutions
  _∷_ : VariableName × Term → AListOfSubstitutions → AListOfSubstitutions

substituteA : AListOfSubstitutions → Term → Term
substituteA [] τ = τ
substituteA ((𝑥ₛ , τₛ) ∷ as) τ = substituteA as (substitute 𝑥ₛ τₛ τ)

record Unifier (τ₁ τ₂ : Term) : Set
 where
  field
    u₁ u₂ : AListOfSubstitutions
    unifier-law : substituteA u₁ τ₁ ≡ substituteA u₂ τ₂

unify? : (τ₁ τ₂ : Term) → Dec $ Unifier τ₁ τ₂
unify? (variable x) (variable x₁) = {!!}
unify? (variable x) (function x₁ x₂) = {!!}
unify? (function x x₁) (variable x₂) = {!!}
unify? (function 𝑓₁ x₁) (function 𝑓₂ x₃) with 𝑓₁ ≟ 𝑓₂
unify? (function 𝑓₁ x₁) (function .𝑓₁ x₃) | yes refl = {!!}
unify? (function 𝑓₁ x₁) (function 𝑓₂ x₃) | no 𝑓₁≢𝑓₂ = no (λ { record { u₁ = u₁ ; u₂ = u₂ ; unifier-law = unifier-law } → {!!}})


text:
{-

        Agda Implementors' Meeting VI

                  Göteborg
             May 24 - 30, 2007

                Hello Agda!

                Ulf Norell

-}

-- Let's have a closer look at the module system

module Modules where

{-

  Importing and opening modules

-}

-- You can import a module defined in a different file.
import Naturals

-- This will bring the module into scope and allows you to
-- access its contents using qualified names.
plusTwo : Naturals.Nat -> Naturals.Nat
plusTwo n = Naturals._+_ n 2

-- To bring everything from a module into scope you can open
-- the module.
open Naturals

z : Nat
z = zero

-- There's also a short-hand to import and open at the same time
open import Bool

_&&_ : Bool -> Bool -> Bool
x && y = if x then y else false

-- Sometimes it's nice to be able to control what is brought
-- into scope when you open a module. There are three modifiers
-- that affect this: using, hiding and renaming.

module DifferentWaysOfOpeningNat where

  -- nothing but Nat
  open Naturals using (Nat)

  -- everything but zero
  open Naturals hiding (zero)

  -- everything, but zero and suc under different names
  open Naturals renaming (zero to ZZ; suc to S_S)

  two : Nat
  two = S S ZZ S S

  -- you can combine using or hiding with renaming, but not using
  -- with hiding (for obvious reasons).

-- To re-export something opened use the public modifier.
module A where
  open Naturals public using (Nat)

N = A.Nat -- now Nat is a visible name in module A

{-

  Parameterised modules

-}

-- A very useful feature is parameterised modules.

data Vec (A : Set) : Nat -> Set where
  []   : Vec A 0
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

infixr 40 _::_

module Sort {A : Set}(_≤_ : A -> A -> Bool) where

  insert : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
  insert x [] = x :: []
  insert x (y :: ys) = if x ≤ y
                       then x :: y :: ys
                       else y :: insert x ys

  sort : {n : Nat} -> Vec A n -> Vec A n
  sort []        = []
  sort (x :: xs) = insert x (sort xs)

_≤_ : Nat -> Nat -> Bool
zero  ≤ m     = true
suc n ≤ zero  = false
suc n ≤ suc m = n ≤ m

-- When used directly, functions from parameterised modules
-- take the parameters as extra arguments.
test = Sort.sort _≤_ (6 :: 2 :: 0 :: 4 :: [])

-- But, you can also apply the entire module to its arguments.
-- Let's open the new module while we're at it.
open module SortNat = Sort _≤_

test' = sort (3 :: 2 :: 4 :: 0 :: [])

{-

  Local definitions

-}

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

subst : {A : Set}(C : A -> Set){x y : A} -> x == y -> C x -> C y
subst C refl cx = cx

cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

lem₁ : (n : Nat) -> n + 0 == n
lem₁ zero    = refl
lem₁ (suc n) = cong suc (lem₁ n)

lem₂ : (n m : Nat) -> n + suc m == suc n + m
lem₂  zero   m = refl
lem₂ (suc n) m = cong suc (lem₂ n m)

-- You can define things locally to a function clause
reverse : {A : Set}{n : Nat} -> Vec A n -> Vec A n
reverse {A} = \xs -> subst (Vec A) (lem₁ _) (rev xs [])
  where
    rev : {n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
    rev []              ys = ys
    rev (_::_ {n} x xs) ys = subst (Vec A) (lem₂ n _)
                                   (rev xs (x :: ys))

-- More precisely, each clause can have one local module. In the
-- example above we didn't bother naming the module. We could've
-- said
reverse' : {A : Set}{n : Nat} -> Vec A n -> Vec A n
reverse' {A}{n} = \xs -> subst (Vec A) (lem₁ n) (rev xs [])
  module Rev where
    rev : {m p : Nat} -> Vec A m -> Vec A p -> Vec A (m + p)
    rev []              ys = ys
    rev (_::_ {n} x xs) ys = subst (Vec A) (lem₂ n _)
                                   (rev xs (x :: ys))

-- Now we can access the local function from inside the module Rev.
-- Variables bound in the left hand side of the clause become
-- parameters to the module, so since the implicit n argument to
-- reverse' is bound implicitly there's an extra argument of type
-- Nat which isn't used.

test'' = Rev.rev {_}{0} (4 :: 3 :: 2 :: []) (5 :: 6 :: [])

{-

  What's next?

-}

-- The final thing on the agenda is records.

-- Move on to: Records.agda

max_stars_repo_name: asr/agda-kanso