text:
module Dave.Equality where
  data _≡_ {A : Set} (x : A) : A → Set where
    refl : x ≡ x

  infix 4 _≡_

  {-# BUILTIN EQUALITY _≡_ #-}

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

  trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  trans refl b = b

  cong : ∀ {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
  cong f refl = refl

  cong₂ : ∀ {A B C : Set} (f : A → B → C) {u x : A} {v y : B}
    → u ≡ x
    → v ≡ y
    → f u v ≡ f x y
  cong₂ f refl refl = refl

  cong-app : ∀ {A B : Set} {f g : A → B}
    → f ≡ g
    → ∀ (x : A) → f x ≡ g x
  cong-app refl x = refl

  subst : ∀ {A : Set} {x y : A} (P : A → Set)
    → x ≡ y
    → P x → P y
  subst P refl px = px

  infix  1 begin_
  infixr 2 _≡⟨⟩_ _≡⟨_⟩_
  infix  3 _∎

  begin_ : ∀ {A : Set} {x y : A}
    → x ≡ y
      -----
    → x ≡ y
  begin x≡y  =  x≡y

  _≡⟨⟩_ : ∀ {A : Set} (x : A) {y : A}
    → x ≡ y
      -----
    → x ≡ y
  x ≡⟨⟩ x≡y  =  x≡y

  _≡⟨_⟩_ : ∀ {A : Set} (x : A) {y z : A}
    → x ≡ y
    → y ≡ z
      -----
    → x ≡ z
  x ≡⟨ x≡y ⟩ y≡z  =  trans x≡y y≡z

  _∎ : ∀ {A : Set} (x : A)
     -----
     → x ≡ x
  x ∎  =  refl


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

module UniversePolymorphicIO where

open import Common.Level

postulate
  IO : ∀ {ℓ} → Set ℓ → Set ℓ

{-# IMPORT UniversePolymorphicIO #-}
{-# COMPILED_TYPE IO UniversePolymorphicIO.AgdaIO #-}
{-# BUILTIN IO IO #-}

postulate
  return : ∀ {a} {A : Set a} → A → IO A
  _>>=_  : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B

postulate
  String : Set

{-# BUILTIN STRING String #-}

{-# COMPILED return (\_ _ -> return :: a -> IO a) #-}
{-# COMPILED _>>=_  (\_ _ _ _ ->
                        (>>=) :: IO a -> (a -> IO b) -> IO b) #-}

{-# IMPORT Data.Text.IO #-}

postulate
  Unit : Set
  putStrLn : String →  IO Unit

{-# COMPILED_TYPE Unit () #-}

{-# COMPILED putStrLn Data.Text.IO.putStrLn #-}

data List A : Set where
  [] : List A
  _∷_ : A → List A → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _∷_ #-}

main = putStrLn "ok" >>= λ _ → return lzero

ext: agda


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

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

open import Cubical.Data.Sigma

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open import Cubical.Algebra.Module
open import Cubical.Algebra.Ring
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Group
open import Cubical.Algebra.Monoid

open Iso

private
  variable
    ℓ ℓ' ℓ'' ℓ''' : Level

record IsAlgebra (R : Ring ℓ) {A : Type ℓ'}
                 (0a 1a : A) (_+_ _·_ : A → A → A) (-_ : A → A)
                 (_⋆_ : ⟨ R ⟩ → A → A) : Type (ℓ-max ℓ ℓ') where

  constructor isalgebra

  open RingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·r_)

  field
    isLeftModule : IsLeftModule R 0a _+_ -_ _⋆_
    ·-isMonoid  : IsMonoid 1a _·_
    dist        : (x y z : A) → (x · (y + z) ≡ (x · y) + (x · z))
                              × ((x + y) · z ≡ (x · z) + (y · z))
    ⋆-lassoc     : (r : ⟨ R ⟩) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y)
    ⋆-rassoc     : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x · y) ≡ x · (r ⋆ y)

  open IsLeftModule isLeftModule public

  isRing : IsRing _ _ _ _ _
  isRing = isring (IsLeftModule.+-isAbGroup isLeftModule) ·-isMonoid dist
  open IsRing isRing public hiding (_-_; +Assoc; +Lid; +Linv; +Rid; +Rinv; +Comm)

unquoteDecl IsAlgebraIsoΣ = declareRecordIsoΣ IsAlgebraIsoΣ (quote IsAlgebra)

record AlgebraStr (R : Ring ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where

  constructor algebrastr

  field
    0a             : A
    1a             : A
    _+_            : A → A → A
    _·_            : A → A → A
    -_             : A → A
    _⋆_            : ⟨ R ⟩ → A → A
    isAlgebra      : IsAlgebra R 0a 1a _+_ _·_ -_ _⋆_

  open IsAlgebra isAlgebra public

Algebra : (R : Ring ℓ) → ∀ ℓ' → Type (ℓ-max ℓ (ℓ-suc ℓ'))
Algebra R ℓ' = Σ[ A ∈ Type ℓ' ] AlgebraStr R A

module commonExtractors {R : Ring ℓ} where

  Algebra→Module : (A : Algebra R ℓ') → LeftModule R ℓ'
  Algebra→Module (_ , algebrastr A _ _ _ _ _ (isalgebra isLeftModule _ _ _ _)) =
    _ , leftmodulestr A _ _ _ isLeftModule

  Algebra→Ring : (A : Algebra R ℓ') → Ring ℓ'
  Algebra→Ring (_ , str) = _ , ringstr _ _ _ _ _ (IsAlgebra.isRing (AlgebraStr.isAlgebra str))

  Algebra→AbGroup : (A : Algebra R ℓ') → AbGroup ℓ'
  Algebra→AbGroup A = LeftModule→AbGroup (Algebra→Module A)

  Algebra→Group : (A : Algebra R ℓ') → Group ℓ'
  Algebra→Group A = Ring→Group (Algebra→Ring A)

  Algebra→AddMonoid : (A : Algebra R ℓ') → Monoid ℓ'
  Algebra→AddMonoid A = Group→Monoid (Algebra→Group A)

  Algebra→MultMonoid : (A : Algebra R ℓ') → Monoid ℓ'
  Algebra→MultMonoid A = Ring→MultMonoid (Algebra→Ring A)

  isSetAlgebra : (A : Algebra R ℓ') → isSet ⟨ A ⟩
  isSetAlgebra A = isSetAbGroup (Algebra→AbGroup A)

  open RingStr (snd R) using (1r; ·Ldist+) renaming (_+_ to _+r_; _·_ to _·s_)

  makeIsAlgebra : {A : Type ℓ'} {0a 1a : A}
                  {_+_ _·_ : A → A → A} { -_ : A → A} {_⋆_ : ⟨ R ⟩ → A → A}
                  (isSet-A : isSet A)
                  (+-assoc :  (x y z : A) → x + (y + z) ≡ (x + y) + z)
                  (+-rid : (x : A) → x + 0a ≡ x)
                  (+-rinv : (x : A) → x + (- x) ≡ 0a)
                  (+-comm : (x y : A) → x + y ≡ y + x)
                  (·-assoc :  (x y z : A) → x · (y · z) ≡ (x · y) · z)
                  (·-rid : (x : A) → x · 1a ≡ x)
                  (·-lid : (x : A) → 1a · x ≡ x)
                  (·-rdist-+ : (x y z : A) → x · (y + z) ≡ (x · y) + (x · z))
                  (·-ldist-+ : (x y z : A) → (x + y) · z ≡ (x · z) + (y · z))
                  (⋆-assoc : (r s : ⟨ R ⟩) (x : A) → (r ·s s) ⋆ x ≡ r ⋆ (s ⋆ x))
                  (⋆-ldist : (r s : ⟨ R ⟩) (x : A) → (r +r s) ⋆ x ≡ (r ⋆ x) + (s ⋆ x))
                  (⋆-rdist : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x + y) ≡ (r ⋆ x) + (r ⋆ y))
                  (⋆-lid   : (x : A) → 1r ⋆ x ≡ x)
                  (⋆-lassoc : (r : ⟨ R ⟩) (x y : A) → (r ⋆ x) · y ≡ r ⋆ (x · y))
                  (⋆-rassoc : (r : ⟨ R ⟩) (x y : A) → r ⋆ (x · y) ≡ x · (r ⋆ y))
                → IsAlgebra R 0a 1a _+_ _·_ -_ _⋆_
  makeIsAlgebra isSet-A
                +-assoc +-rid +-rinv +-comm
                ·-assoc ·-rid ·-lid ·-rdist-+ ·-ldist-+
                ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid ⋆-lassoc ⋆-rassoc =
                isalgebra
                  (makeIsLeftModule isSet-A
                                    +-assoc +-rid +-rinv +-comm
                                    ⋆-assoc ⋆-ldist ⋆-rdist ⋆-lid)
                  (makeIsMonoid isSet-A ·-assoc ·-rid ·-lid)
                  (λ x y z → ·-rdist-+ x y z , ·-ldist-+ x y z)
                  ⋆-lassoc ⋆-rassoc

open commonExtractors public

record IsAlgebraHom {R : Ring ℓ} {A : Type ℓ'} {B : Type ℓ''}
  (M : AlgebraStr R A) (f : A → B) (N : AlgebraStr R B)
  : Type (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
  where

  -- Shorter qualified names
  private
    module M = AlgebraStr M
    module N = AlgebraStr N

  field
    pres0 : f M.0a ≡ N.0a
    pres1 : f M.1a ≡ N.1a
    pres+ : (x y : A) → f (x M.+ y) ≡ f x N.+ f y
    pres· : (x y : A) → f (x M.· y) ≡ f x N.· f y
    pres- : (x : A) → f (M.- x) ≡ N.- (f x)
    pres⋆ : (r : ⟨ R ⟩) (y : A) → f (r M.⋆ y) ≡ r N.⋆ f y

unquoteDecl IsAlgebraHomIsoΣ = declareRecordIsoΣ IsAlgebraHomIsoΣ (quote IsAlgebraHom)
open IsAlgebraHom

AlgebraHom : {R : Ring ℓ} (M : Algebra R ℓ') (N : Algebra R ℓ'') → Type (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
AlgebraHom M N = Σ[ f ∈ (⟨ M ⟩ → ⟨ N ⟩) ] IsAlgebraHom (M .snd) f (N .snd)

IsAlgebraEquiv : {R : Ring ℓ} {A : Type ℓ'} {B : Type ℓ''}
  (M : AlgebraStr R A) (e : A ≃ B) (N : AlgebraStr R B)
  → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
IsAlgebraEquiv M e N = IsAlgebraHom M (e .fst) N

AlgebraEquiv : {R : Ring ℓ} (M : Algebra R ℓ') (N : Algebra R ℓ'') → Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
AlgebraEquiv M N = Σ[ e ∈ ⟨ M ⟩ ≃ ⟨ N ⟩ ] IsAlgebraEquiv (M .snd) e (N .snd)

_$a_ : {R : Ring ℓ} {A : Algebra R ℓ'} {B : Algebra R ℓ''} → AlgebraHom A B → ⟨ A ⟩ → ⟨ B ⟩
f $a x = fst f x

AlgebraEquiv→AlgebraHom : {R : Ring ℓ} {A : Algebra R ℓ'} {B : Algebra R ℓ''}
                        → AlgebraEquiv A B → AlgebraHom A B
AlgebraEquiv→AlgebraHom (e , eIsHom) = e .fst , eIsHom

isPropIsAlgebra : (R : Ring ℓ) {A : Type ℓ'}
  (0a 1a : A)
  (_+_ _·_ : A → A → A)
  (-_ : A → A)
  (_⋆_ : ⟨ R ⟩ → A → A)
  → isProp (IsAlgebra R 0a 1a _+_ _·_ -_ _⋆_)
isPropIsAlgebra R _ _ _ _ _ _ = let open IsLeftModule in
  isOfHLevelRetractFromIso 1 IsAlgebraIsoΣ
    (isPropΣ
      (isPropIsLeftModule _ _ _ _ _)
      (λ mo → isProp×3 (isPropIsMonoid _ _)
                       (isPropΠ3 λ _ _ _ → isProp× (mo .is-set _ _) (mo .is-set _ _))
                       (isPropΠ3 λ _ _ _ → mo .is-set _ _)
                       (isPropΠ3 λ _ _ _ → mo .is-set _ _) ))

isPropIsAlgebraHom : (R : Ring ℓ) {A : Type ℓ'} {B : Type ℓ''}
                     (AS : AlgebraStr R A) (f : A → B) (BS : AlgebraStr R B)
                   → isProp (IsAlgebraHom AS f BS)
isPropIsAlgebraHom R AS f BS = isOfHLevelRetractFromIso 1 IsAlgebraHomIsoΣ
                               (isProp×5 (isSetAlgebra (_ , BS) _ _)
                                         (isSetAlgebra (_ , BS) _ _)
                                         (isPropΠ2 λ _ _ → isSetAlgebra (_ , BS) _ _)
                                         (isPropΠ2 λ _ _ → isSetAlgebra (_ , BS) _ _)
                                         (isPropΠ λ _ → isSetAlgebra (_ , BS) _ _)
                                         (isPropΠ2 λ _ _ → isSetAlgebra (_ , BS) _ _))

isSetAlgebraHom : {R : Ring ℓ} (M : Algebra R ℓ') (N : Algebra R ℓ'')
                → isSet (AlgebraHom M N)
isSetAlgebraHom _ N = isSetΣ (isSetΠ (λ _ → isSetAlgebra N))
                        λ _ → isProp→isSet (isPropIsAlgebraHom _ _ _ _)

isSetAlgebraEquiv : {R : Ring ℓ} (M N : Algebra R ℓ')
                  → isSet (AlgebraEquiv M N)
isSetAlgebraEquiv M N = isSetΣ (isOfHLevel≃ 2 (isSetAlgebra M) (isSetAlgebra N))
                          λ _ → isProp→isSet (isPropIsAlgebraHom _ _ _ _)

AlgebraHom≡ : {R : Ring ℓ} {A B : Algebra R ℓ'} {φ ψ : AlgebraHom A B} → fst φ ≡ fst ψ → φ ≡ ψ
AlgebraHom≡ = Σ≡Prop λ f → isPropIsAlgebraHom _ _ f _

𝒮ᴰ-Algebra : (R : Ring ℓ) → DUARel (𝒮-Univ ℓ') (AlgebraStr R) (ℓ-max ℓ ℓ')
𝒮ᴰ-Algebra R =
  𝒮ᴰ-Record (𝒮-Univ _) (IsAlgebraEquiv {R = R})
    (fields:
      data[ 0a ∣ nul ∣ pres0 ]
      data[ 1a ∣ nul ∣ pres1 ]
      data[ _+_ ∣ bin ∣ pres+ ]
      data[ _·_ ∣ bin ∣ pres· ]
      data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
      data[ _⋆_ ∣ autoDUARel _ _ ∣ pres⋆ ]
      prop[ isAlgebra ∣ (λ _ _ → isPropIsAlgebra _ _ _ _ _ _ _) ])
  where
  open AlgebraStr

  -- faster with some sharing
  nul = autoDUARel (𝒮-Univ _) (λ A → A)
  bin = autoDUARel (𝒮-Univ _) (λ A → A → A → A)

AlgebraPath : {R : Ring ℓ} (A B : Algebra R ℓ') → (AlgebraEquiv A B) ≃ (A ≡ B)
AlgebraPath {R = R} = ∫ (𝒮ᴰ-Algebra R) .UARel.ua

uaAlgebra : {R : Ring ℓ} {A B : Algebra R ℓ'} → AlgebraEquiv A B → A ≡ B
uaAlgebra {A = A} {B = B} = equivFun (AlgebraPath A B)

isGroupoidAlgebra : {R : Ring ℓ} → isGroupoid (Algebra R ℓ')
isGroupoidAlgebra _ _ = isOfHLevelRespectEquiv 2 (AlgebraPath _ _) (isSetAlgebraEquiv _ _)

-- Smart constructor for ring homomorphisms
-- that infers the other equations from pres1, pres+, and pres·

module _  {R : Ring ℓ} {A : Algebra R ℓ'} {B : Algebra R ℓ''} {f : ⟨ A ⟩ → ⟨ B ⟩} where

  private
    module A = AlgebraStr (A .snd)
    module B = AlgebraStr (B .snd)

  module _
    (p1 : f A.1a ≡ B.1a)
    (p+ : (x y : ⟨ A ⟩) → f (x A.+ y) ≡ f x B.+ f y)
    (p· : (x y : ⟨ A ⟩) → f (x A.· y) ≡ f x B.· f y)
    (p⋆ : (r : ⟨ R ⟩) (x : ⟨ A ⟩) → f (r A.⋆ x) ≡ r B.⋆ f x)
    where

    open IsAlgebraHom
    private
      isGHom : IsGroupHom (Algebra→Group A .snd) f (Algebra→Group B .snd)
      isGHom = makeIsGroupHom p+

    makeIsAlgebraHom : IsAlgebraHom (A .snd) f (B .snd)
    makeIsAlgebraHom .pres0 = isGHom .IsGroupHom.pres1
    makeIsAlgebraHom .pres1 = p1
    makeIsAlgebraHom .pres+ = p+
    makeIsAlgebraHom .pres· = p·
    makeIsAlgebraHom .pres- = isGHom .IsGroupHom.presinv
    makeIsAlgebraHom .pres⋆ = p⋆

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
open import Common.Prelude
open import Common.Reflect

module TermSplicing1 where

x = unquote Set

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

-- The basic CBPV metalanguage.

open import Calf.CostMonoid

module Calf.Metalanguage where

open import Calf.Prelude
open import Relation.Binary.PropositionalEquality
open import Data.Product

postulate
  mode : □
  pos : mode
  neg : mode

  tp : mode → □
  val : tp pos → □

  F : tp pos → tp neg
  U : tp neg → tp pos

-- This is equivalent to adding "thunk / force" operations. But less bureaucratic.
cmp : tp neg → □
cmp X = val (U X)

postulate
  ret : ∀ {A} → val A → cmp (F A)
  tbind : ∀ {A} → cmp (F A) → (val A → tp neg) → tp neg
  tbind_ret : ∀ {A} {X : val A → tp neg} {v : val A} → tbind (ret v) X ≡ X v
  {-# REWRITE tbind_ret #-}

  dbind : ∀ {A} (X : val A → tp neg) (e : cmp (F A)) (f : (x : val A) → cmp (X x)) → cmp (tbind e X)

  -- note that bind is not a special case of dbind: in general, one does not expect (tbind e (λ _ → m)) ≡ m.
  -- This would hold, however, in the case of a language where there are no true effects. But we don't want
  -- to assume that.
  bind : ∀ {A} X → cmp (F A) → (val A → cmp X) → cmp X

  bind/ret : ∀ {A X} {v : val A} {f : (x : val A) → cmp X} → bind X (ret v) f ≡ f v
  dbind/ret : ∀ {A} {X : val A → tp neg} {v : val A} {f : (x : val A) → cmp (X x)} → dbind X (ret v) f ≡ f v
  {-# REWRITE bind/ret dbind/ret #-}

  tbind/assoc : ∀ {A B X} {e : cmp (F A)} {f : val A → cmp (F B)} →
    tbind {B} (bind (F B) e f) X ≡ tbind {A} e (λ v → tbind {B} (f v) X)
  bind/assoc : ∀ {A B C} {e : cmp (F A)} {f1 : val A → cmp (F B)} {f2 : val B → cmp C} →
    bind C (bind (F B) e f1) f2 ≡ bind C e (λ v → bind C (f1 v) f2)
  {-# REWRITE tbind/assoc bind/assoc #-}

  -- dependent product
  Π : (A : tp pos) (X : val A → tp neg) → tp neg
  Π/decode : ∀ {A} {X : val A → tp neg} → val (U (Π A X)) ≡ ((x : val A) → cmp (X x))
  {-# REWRITE Π/decode #-}

  -- mixed polarity dependent sum
  Σ+- : (A : tp pos) (X : val A → tp neg) → tp neg
  Σ+-/decode : ∀ {A} {X : val A → tp neg} → val (U (Σ+- A X)) ≡ Σ (val A) λ x → cmp (X x)
  {-# REWRITE Σ+-/decode #-}

  -- positive dependent sum
  Σ++ : (A : tp pos) (B : val A → tp pos) → tp pos
  Σ++/decode : ∀ {A} {B : val A → tp pos} → val (Σ++ A B) ≡ Σ (val A) λ x → val (B x)
  {-# REWRITE Σ++/decode #-}

  -- agda sets
  meta : Set → tp neg
  meta/out : ∀ {A} → val (U (meta A)) ≡ A
  {-# REWRITE meta/out #-}

  bind/meta : ∀ A 𝕊 𝕋 e f (g : 𝕊 → 𝕋) → g (bind {A} (meta 𝕊) e f) ≡ bind {A} (meta 𝕋) e (λ a → g(f a))
  tbind/meta : ∀ A 𝕊 e f (p : 𝕊 → □) → p (bind {A} (meta 𝕊) e f) ≡ cmp (tbind {A} e (λ a → meta (p (f a))))
  bind/idem : ∀ A 𝕊 e (f : val A → val A → 𝕊) → bind {A} (meta 𝕊) e (λ a → (bind {A} (meta 𝕊) e (λ a' → f a a'))) ≡ bind {A} (meta 𝕊) e (λ a → f a a)

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
open import Mockingbird.Forest using (Forest)

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

open import Data.Fin using (Fin; zero; suc; #_)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Nat.Properties using (_≤?_)
open import Data.Vec as Vec using (Vec; _∷_)
open import Data.Vec.Relation.Unary.Any using (here; there) public
open import Level using (_⊔_)
open import Relation.Nullary.Decidable.Core using (True)
open import Relation.Unary using (Pred; _∈_)

open Forest forest

import Mockingbird.Forest.Combination.Base forest as Base
import Mockingbird.Forest.Combination.Properties forest as Combinationₚ
open import Mockingbird.Forest.Combination.Base forest using ([_]; _⟨∙⟩_∣_; _⟨∙⟩_) public
open import Data.Vec.Membership.Setoid setoid using () renaming (_∈_ to _∈′_)

⟨_⟩ : ∀ {n} → Vec Bird n → Pred Bird (b ⊔ ℓ)
⟨ bs ⟩ = Base.⟨ _∈′ bs ⟩

[_]′ : ∀ {n} {bs : Vec Bird n} (i : Fin n) → Vec.lookup bs i ∈ ⟨ bs ⟩
[_]′ {suc n} {x ∷ bs} zero = [ here refl ]
[_]′ {suc n} {x ∷ bs} (suc i) = Combinationₚ.⟨ _ ⟩⊆⟨ _ ⟩ there [ i ]′

[#_] : ∀ m {n} {m<n : True (suc m ≤? n)} {bs : Vec Bird n}
  → Vec.lookup bs (#_ m {m<n = m<n}) ∈ ⟨ bs ⟩
[# m ] = [ # m ]′

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Injections
------------------------------------------------------------------------

module Function.Injection where

open import Function as Fun using () renaming (_∘_ to _⟨∘⟩_)
open import Level
open import Relation.Binary
open import Function.Equality as F
  using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
import Relation.Binary.PropositionalEquality as P

-- Injective functions.

Injective : ∀ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} →
            A ⟶ B → Set _
Injective {A = A} {B} f = ∀ {x y} → f ⟨$⟩ x ≈₂ f ⟨$⟩ y → x ≈₁ y
  where
  open Setoid A renaming (_≈_ to _≈₁_)
  open Setoid B renaming (_≈_ to _≈₂_)

-- The set of all injections between two setoids.

record Injection {f₁ f₂ t₁ t₂}
                 (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
                 Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    to        : From ⟶ To
    injective : Injective to

-- The set of all injections from one set to another.

infix 3 _↣_

_↣_ : ∀ {f t} → Set f → Set t → Set _
From ↣ To = Injection (P.setoid From) (P.setoid To)

-- Identity and composition.

infixr 9 _∘_

id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → Injection S S
id = record { to = F.id; injective = Fun.id }

_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
        {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
      Injection M T → Injection F M → Injection F T
f ∘ g = record
  { to        =          to        f  ⟪∘⟫ to        g
  ; injective = (λ {_} → injective g) ⟨∘⟩ injective f
  } where open Injection


text:
open import Oscar.Prelude
open import Oscar.Class

module Oscar.Class.Quadricity where

module Quadricity
  {𝔞} {𝔄 : Ø 𝔞}
  {𝔟} {𝔅 : Ø 𝔟}
  {ℓ} (_↦_ : 𝔅 → 𝔅 → Ø ℓ) (let infix 4 _↦_; _↦_ = _↦_)
  (_∧_ : 𝔅 → 𝔅 → 𝔅) (let infixr 15 _∧_; _∧_ = _∧_)
  (_∼_ : 𝔄 → 𝔄 → 𝔅) (let infix 18 _∼_; _∼_ = _∼_)
  (_⊛_ : 𝔄 → 𝔄 → 𝔄)
  = ℭLASS (_↦_ , _∼_ , _∧_ , _⊛_) (∀ s1 s2 t1 t2 → s1 ⊛ s2 ∼ t1 ⊛ t2 ↦ s1 ∼ t1 ∧ s2 ∼ t2)

module _
  {𝔞} {𝔄 : Ø 𝔞}
  {𝔟} {𝔅 : Ø 𝔟}
  {ℓ} {_↦_ : 𝔅 → 𝔅 → Ø ℓ}
  {_∧_ : 𝔅 → 𝔅 → 𝔅}
  {_∼_ : 𝔄 → 𝔄 → 𝔅}
  {_⊛_ : 𝔄 → 𝔄 → 𝔄}
  where
  quadricity = Quadricity.method _↦_ _∧_ _∼_ _⊛_

open import Oscar.Class.Properthing
open import Oscar.Class.HasEquivalence

module Properfact1
  {𝔞} {𝔄 : Ø 𝔞} {𝔟} {𝔅 : Ø 𝔟} (∼ : 𝔄 → 𝔄 → 𝔅) {ℓ} ⦃ _ : Properthing ℓ 𝔅 ⦄ (⊛ : 𝔄 → 𝔄 → 𝔄)
  = Quadricity _≈_ _∧_ ∼ ⊛


text:
module Data.Num.Redundant where

--  Base: 2
--  Digit: { 0, 1, 2 }
--
--  Numeral System which maxports efficient addition, substraction
--  and arithmetic shift.

open import Data.List using (List ; []; _∷_) public
open import Data.Nat renaming (_+_ to _+ℕ_; _<_ to _<ℕ_)
open import Data.Num.Bij

open import Data.Empty
open import Relation.Nullary
open import Relation.Nullary.Negation using (contradiction; contraposition)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_; _≢_)
import Level
open PropEq.≡-Reasoning

--------------------------------------------------------------------------------
--  Digits
--------------------------------------------------------------------------------

data Digit : Set where
    zero : Digit
    one : Digit
    two : Digit

-- plus
_⊕_ : Digit → Digit → Digit
zero ⊕ y    = y
x    ⊕ zero = x
one  ⊕ one  = two
one  ⊕ two  = one
two  ⊕ one  = one
two  ⊕ two  = two

-- minus
_⊝_ : Digit → Digit → Digit
zero ⊝ y    = zero
x    ⊝ zero = x
one  ⊝ one  = zero
one  ⊝ two  = one
two  ⊝ one  = one
two  ⊝ two  = zero

-- carry
_⊙_ : Digit → Digit → Digit
one ⊙ two = one
two ⊙ one = one
two ⊙ two = one
_   ⊙ _   = zero

-- borrow
_⊘_ : Digit → Digit → Digit
zero ⊘ one = one
zero ⊘ two = one
one  ⊘ two = one
_    ⊘ _   = zero

--------------------------------------------------------------------------------
--  Sequence of Digits
--------------------------------------------------------------------------------

Redundant : Set
Redundant = List Digit

-- "one-sided"
incr : Digit → Redundant → Redundant
incr x [] = x ∷ []
incr x (y ∷ ys) = x ⊕ y ∷ incr (x ⊙ y) ys

decr : Digit → Redundant → Redundant
decr x [] = []
decr x (y ∷ ys) = x ⊝ y ∷ decr (x ⊘ y) ys

-- "two-sided"
_+_ : Redundant → Redundant → Redundant
[] + ys = ys
xs + [] = xs
(x ∷ xs) + (y ∷ ys) = x ⊕ y ∷ incr (x ⊙ y) (xs + ys)

_─_ : Redundant → Redundant → Redundant
[] ─ ys = []
xs ─ [] = xs
(x ∷ xs) ─ (y ∷ ys) = x ⊝ y ∷ decr (x ⊘ y) (xs ─ ys)

-- arithmetic shift
>> : Redundant → Redundant
>> xs = zero ∷ xs

<< : Redundant → Redundant
<< [] = []
<< (x ∷ xs) = xs

_>>>_ : ℕ → Redundant → Redundant
zero >>> xs = xs
suc n >>> xs = n >>> (>> xs)

_<<<_ : ℕ → Redundant → Redundant
zero  <<< xs = xs
suc n <<< [] = []
suc n <<< (x ∷ xs) = n <<< xs

--------------------------------------------------------------------------------
-- instances of Conversion, so that we can convert Redundant to B
--------------------------------------------------------------------------------

instance convRedundant : Conversion Redundant
convRedundant = conversion [_]' !_!' [!!]-id'
    where   [_]' : Redundant → Bij
            [     [] ]' = []
            [ zero ∷ xs ]' =    *2 [ xs ]'
            [ one  ∷ xs ]' = one ∷ [ xs ]'
            [ two  ∷ xs ]' = two ∷ [ xs ]'

            !_!' : Bij → Redundant
            ! []     !' = []
            ! one ∷ xs !' = one ∷ ! xs !'
            ! two ∷ xs !' = two ∷ ! xs !'

            [!!]-id' : ∀ xs → [ ! xs !' ]' ≡ xs
            [!!]-id' [] = PropEq.refl
            [!!]-id' (one ∷ xs) = PropEq.cong (λ x → one ∷ x) ([!!]-id' xs)
            [!!]-id' (two ∷ xs) = PropEq.cong (λ x → two ∷ x) ([!!]-id' xs)

--------------------------------------------------------------------------------
--  Equivalence relation
--------------------------------------------------------------------------------

infix 4 _≈_ _≉_

data _≈_ (a b : Redundant) : Set where
    eq : ([a]≡[b] : [ a ] ≡ [ b ]) → a ≈ b

-- the inverse of `eq`
to≡ : ∀ {a b} → a ≈ b → [ a ] ≡ [ b ]
to≡ (eq x) = x

_≉_ : (a b : Redundant) → Set
a ≉ b = a ≈ b → ⊥

-- decidable
{-
_≈?_ : Decidable {A = Redundant} _≈_
a ≈? b with [ a ] ≟ [ b ]
a ≈? b | yes p = yes (eq p)
a ≈? b | no ¬p = no (contraposition to≡ ¬p)
-}

--------------------------------------------------------------------------------
--  Ordering
--------------------------------------------------------------------------------

infix 4 _≲_ _<_
data _≲_ : Rel Redundant Level.zero where
    le : ∀ {a b} ([a]≤[b] : [ a ] ≤B [ b ]) → a ≲ b

-- the inverse of `le`
to≤ : ∀ {a b} → a ≲ b → [ a ] ≤B [ b ]
to≤ (le [a]≤B[b]) = [a]≤B[b]

_<_ : Rel Redundant Level.zero
a < b = incr one a ≲ b

{-
-- decidable
_≲?_ : Decidable _≲_
a ≲? b with [ a ] ≤? [ b ]
a ≲? b | yes p = yes (le p)
a ≲? b | no ¬p = no (contraposition to≤ ¬p)
-}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
module Data.Vec.Membership.Propositional.Distinct where

open import Data.Vec as Vec using (Vec; [];  _∷_; _++_)

open import Data.Vec.Membership.Propositional
open import Data.Vec.Any hiding (map; index; head; tail)
open import Data.List as List using (List)
open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; _≗_ )
open import Relation.Binary.HeterogeneousEquality as H using (_≅_; _≇_)
import Data.List.Membership.Propositional.Distinct as ListDistinct
open import Data.Product as Prod hiding (map)
open import Data.Sum     hiding (map)
open import Data.Empty   using (⊥-elim)
open import Relation.Nullary
open import Data.Fin as Fin
open import Data.Fin.Properties using (suc-injective)
open import Data.Nat as ℕ
open import Function using (_∘_)
open import Function.Equivalence using (_⇔_; equivalence)
open import Function.Equality as F using (_⟨$⟩_)
open import Function.Injection using (_↣_; Injection)

data Distinct {a}{A : Set a} : ∀ {n} → Vec A n → Set a where
  distinct-[] : Distinct []
  _distinct-∷_by_ : ∀ {n} x {xs : Vec A n} → Distinct xs → x ∉ xs → Distinct (x ∷ xs)

head : ∀ {a}{A : Set a} {n} {x}{xs : Vec A n} → Distinct (x ∷ xs) → A
head (x distinct-∷ _ by _) = x

tail : ∀ {a}{A : Set a} {n} {x}{xs : Vec A n} → Distinct (x ∷ xs) → Distinct xs
tail (_ distinct-∷ dis by _) = dis

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

[_] : ∀{a}{A : Set a}(x : A) → Distinct Vec.[ x ]
[ x ] = x distinct-∷ distinct-[] by (λ ())

{-
_distinct-∷ʳ_by_ : ∀ {a}{A : Set a} {n} {xs : Vec A n} → Distinct xs → (x : A) → x ∉ xs → Distinct (xs Vec.∷ʳ x)
distinct-[] distinct-∷ʳ x by x∉xs = x distinct-∷ distinct-[] by x∉xs
(y distinct-∷ dxs by y∉xs) distinct-∷ʳ x by x∉yxs = y distinct-∷ dxs distinct-∷ʳ x by (x∉yxs ∘ there) by lemma y∉xs x∉yxs
  where
    lemma : ∀ {a}{A : Set a} {n} {xs : Vec A n} {x y} → y ∉ xs → x ∉ y Vec.∷ xs → y ∉ xs Vec.∷ʳ x
    lemma {xs = []} y∉xs x∉y∷xs (here P.refl) = x∉y∷xs (here P.refl)
    lemma {xs = []} y∉xs x∉y∷xs (there ())
    lemma {xs = _ ∷ xs} y∉xs x∉y∷xs (here P.refl) = y∉xs (here P.refl)
    lemma {xs = x₁ ∷ xs}{x}{y} y∉xs x∉y∷xs (there y∈xs∷ʳx) = {!!}
-}
initLast : ∀ {a n} {A : Set a}{xs : Vec A (suc n)} → Distinct xs →
  let (ys , y , xs≡ysy) = Vec.initLast xs in Distinct ys × y ∉ ys
initLast {n = zero} {xs = x ∷ []} (.x distinct-∷ distinct-[] by x∉[]) = distinct-[] , x∉[]
initLast {n = suc n} {xs = x ∷ xs} (.x distinct-∷ dxs by x∉xs) with Vec.initLast xs | initLast dxs
initLast {_} {suc n} {_} {x ∷ .(ys Vec.∷ʳ y)} (.x distinct-∷ dxs by x∉xs) | ys , y , P.refl | dys , y∉ys =
             x distinct-∷ dys by (x∉xs ∘ ∈-∷ʳ) , λ { (here P.refl) → x∉xs (∷ʳ-∈ y ys)
                                                  ; ( there p) → y∉ys p }
         where
           ∈-∷ʳ : ∀ {a n} {A : Set a}{xs : Vec A n}{x y} → x ∈ xs → x ∈ xs Vec.∷ʳ y
           ∈-∷ʳ {xs = []} ()
           ∈-∷ʳ {xs = x ∷ xs} (here eq) = here eq
           ∈-∷ʳ {xs = x ∷ xs} (there x∈xs) = there (∈-∷ʳ x∈xs)
           ∷ʳ-∈ : ∀ {a n} {A : Set a} x (xs : Vec A n) → x ∈ xs Vec.∷ʳ x
           ∷ʳ-∈ x [] = here P.refl
           ∷ʳ-∈ x (y ∷ xs) = there (∷ʳ-∈ x xs)

private
  initLast₁≡init  : ∀ {a n} {A : Set a}(xs : Vec A (suc n)) → proj₁ (Vec.initLast xs) ≡ Vec.init xs
  initLast₁≡init xs with Vec.initLast xs
  initLast₁≡init .(ys Vec.∷ʳ y) | ys , y , P.refl = P.refl

  initLast₂≡last  : ∀ {a n} {A : Set a}(xs : Vec A (suc n)) → proj₁ (proj₂ (Vec.initLast xs)) ≡ Vec.last xs
  initLast₂≡last xs with Vec.initLast xs
  initLast₂≡last .(ys Vec.∷ʳ y) | ys , y , P.refl = P.refl

init : ∀ {a n} {A : Set a}{xs : Vec A (suc n)} → Distinct xs → Distinct (Vec.init xs)
init {xs = xs} dxs with initLast dxs
... | dys , y∉ys rewrite initLast₁≡init xs = dys

last : ∀ {a n} {A : Set a}{xs : Vec A (suc n)} → Distinct xs → Vec.last xs ∉ Vec.init xs
last {xs = xs} dxs with initLast dxs
... | dys , y∉ys rewrite initLast₁≡init xs | initLast₂≡last xs = y∉ys

map : ∀ {a b}{A : Set a}{B : Set b} → (f : A ↣ B) → ∀ {n}{xs : Vec A n} → Distinct xs → Distinct (Vec.map (Injection.to f ⟨$⟩_) xs)
map f {0}{[]} distinct-[] = distinct-[]
map {A = A} f {ℕ.suc _} {x ∷ xs} (.x distinct-∷ dis by x∉xs) = fx distinct-∷ map f dis by fx∉mapfxs
    where

      fx = Injection.to f ⟨$⟩ x
      -- missing
      ∈-map⁻ : ∀{a b}{A : Set a}{B : Set b}(f : A → B){m}{xs : Vec A m}{y} →
        y ∈ Vec.map f xs → ∃ λ x → x ∈ xs × y ≡ f x
      ∈-map⁻ f {xs = []} ()
      ∈-map⁻ f {xs = x ∷ xs} (here P.refl) = x , here P.refl , P.refl
      ∈-map⁻ f {xs = x ∷ xs} (there y∈mapfxs) with ∈-map⁻ _ y∈mapfxs
      ... | v , v∈xs , eq = v , there v∈xs , eq

      fx∉mapfxs : fx ∉ Vec.map (Injection.to f ⟨$⟩_) xs
      fx∉mapfxs fx∈mapfxs with ∈-map⁻ _ fx∈mapfxs
      ... | v , v∈xs , fx≡fv with Injection.injective f fx≡fv
      fx∉mapfxs fx∈mapfxs | v , v∈xs , fx≡fv | P.refl = x∉xs v∈xs

private
  injection : ∀ {a b}{A : Set a}{B : Set b} {f : A → B} → (∀ {x y} → f x ≡ f y → x ≡ y) → A ↣ B
  Injection.to (injection {f = f} inj) = P.→-to-⟶ f
  Injection.injective (injection inj) = inj

tabulate : ∀ {a}{A : Set a}{n} → (f : Fin n ↣ A) → Distinct (Vec.tabulate (Injection.to f ⟨$⟩_))
tabulate {n = zero} f = distinct-[]
tabulate {n = suc n} f = (Injection.to f ⟨$⟩ zero) distinct-∷ tabulate (f ⟨∘⟩ injection suc-injective) by lemma
  where
    open import Function.Injection using () renaming (_∘_ to _⟨∘⟩_)
    open import Data.Vec.Membership.Propositional.Properties
    ∈-tabulateˡ : ∀ {a}{A : Set a}{n}{x}(f : Fin n → A) → x ∈ Vec.tabulate f →
      ∃ λ i → x ≡ f i
    ∈-tabulateˡ {n = zero} f ()
    ∈-tabulateˡ {n = suc n} f (here P.refl) = _ , P.refl
    ∈-tabulateˡ {n = suc n} f (there x∈tabf) with ∈-tabulateˡ _ x∈tabf
    ... | i , eq = suc i , eq

    lemma : (Injection.to f ⟨$⟩ zero) ∉ Vec.tabulate ((Injection.to f ⟨$⟩_) ∘ Fin.suc)
    lemma p with ∈-tabulateˡ _ p
    lemma p | i , fi≡f0 with Injection.injective f fi≡f0
    lemma p | i , fi≡f0 | ()

allFin : ∀ n → Distinct (Vec.allFin n)
allFin n = tabulate ⟨id⟩
  where
    open import Function.Injection using () renaming (id to ⟨id⟩)

private
  ∈-zipˡ : ∀ {a b n}{A : Set a}{B : Set b}{xs : Vec A n}{ys : Vec B n} {x y} →
    (x , y) ∈ Vec.zip xs ys → x ∈ xs
  ∈-zipˡ {xs = []} {[]} ()
  ∈-zipˡ {xs = x ∷ xs} {y ∷ ys} (here P.refl) = here P.refl
  ∈-zipˡ {xs = x ∷ xs} {y ∷ ys} (there p) = there (∈-zipˡ p)

  ∈-zipʳ : ∀ {a b n}{A : Set a}{B : Set b}{xs : Vec A n}{ys : Vec B n} {x y} →
    (x , y) ∈ Vec.zip xs ys → y ∈ ys
  ∈-zipʳ {xs = []} {[]} ()
  ∈-zipʳ {xs = x ∷ xs} {y ∷ ys} (here P.refl) = here P.refl
  ∈-zipʳ {xs = x ∷ xs} {y ∷ ys} (there p) = there (∈-zipʳ p)

zipˡ : ∀ {a b n}{A : Set a}{B : Set b}{xs : Vec A n} →
     Distinct xs → (ys : Vec B n) → Distinct (Vec.zip xs ys)
zipˡ distinct-[] [] = distinct-[]
zipˡ (x distinct-∷ dxs by x∉xs) (y ∷ ys) = (x , y) distinct-∷ zipˡ dxs ys
  by λ p → x∉xs (∈-zipˡ p)

zipʳ : ∀ {a b n}{A : Set a}{B : Set b}(xs : Vec A n){ys : Vec B n} →
  Distinct ys → Distinct (Vec.zip xs ys)
zipʳ [] distinct-[] = distinct-[]
zipʳ (x ∷ xs) (y distinct-∷ dys by y∉ys) = (x , y) distinct-∷ zipʳ xs dys
  by λ p → y∉ys (∈-zipʳ p)

toList : ∀ {a n}{A : Set a}{xs : Vec A n} → Distinct xs → ListDistinct.Distinct (Vec.toList xs)
toList distinct-[] = ListDistinct.distinct-[]
toList (x distinct-∷ dxs by x∉xs) = x ListDistinct.distinct-∷ toList dxs
  by λ x∈xs → x∉xs (lemma x∈xs)
  where
    import Data.List.Membership.Propositional as ListMem
    import Data.List.Any as ListAny
    lemma : ∀ {a n}{A : Set a}{x}{xs : Vec A n} → x ListMem.∈ Vec.toList xs → x ∈ xs
    lemma {xs = []} ()
    lemma {xs = x ∷ xs} (ListAny.here P.refl) = here P.refl
    lemma {xs = x ∷ xs} (ListAny.there p) = there (lemma p)

fromList : ∀ {a}{A : Set a}{xs : List A} → ListDistinct.Distinct xs → Distinct (Vec.fromList xs)
fromList ListDistinct.distinct-[] = distinct-[]
fromList (x ListDistinct.distinct-∷ dxs by x∉xs) =
  x distinct-∷ fromList dxs by λ x∈xs → x∉xs (lemma x∈xs)
    where
      import Data.List.Membership.Propositional as ListMem
      import Data.List.Any as ListAny
      lemma : ∀ {a}{A : Set a}{x}{xs : List A} → x ∈ Vec.fromList xs →
        x ListMem.∈ xs
      lemma {xs = List.[]} ()
      lemma {xs = x List.∷ xs} (here P.refl) = ListAny.here P.refl
      lemma {xs = x List.∷ xs} (there p) = ListAny.there (lemma p)

max_stars_repo_name: tizmd/agda-distinct-disjoint

max_issues_repo_name: tizmd/agda-distinct-disjoint

max_forks_repo_name: tizmd/agda-distinct-disjoint


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.DiffInt.Base where

open import Cubical.Foundations.Prelude

open import Cubical.HITs.SetQuotients.Base

open import Cubical.Data.Prod
open import Cubical.Data.Nat

rel : (ℕ ×Σ ℕ) → (ℕ ×Σ ℕ) → Type₀
rel (a₀ , b₀) (a₁ , b₁) = x ≡ y
  where
    x = a₀ + b₁
    y = a₁ + b₀

ℤ = (ℕ ×Σ ℕ) / rel

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
module SystemF.Substitutions where

open import Prelude hiding (subst)
open import SystemF.Syntax
open import Data.Fin.Substitution
open import Data.Star hiding (map)
open import Data.Vec hiding ([_])

open import SystemF.Substitutions.Types public

module TermTypeSubst where

  module TermTypeApp {T} (l : Lift T Type) where
    open Lift l hiding (var)
    open TypeSubst.TypeApp l renaming (_/_ to _tp/_)

    infixl 8 _/_

    -- Apply a type substitution to a term
    _/_ : ∀ {ν μ n} → Term ν n → Sub T ν μ → Term μ n
    var x      / σ = var x
    Λ t        / σ = Λ (t / σ ↑)
    λ' a t     / σ = λ' (a tp/ σ) (t / σ)
    t [ a ]    / σ = (t / σ) [ a tp/ σ ]
    s · t      / σ = (s / σ) · (t / σ)

  open TypeSubst using (varLift; termLift; sub)

  module Lifted {T} (lift : Lift T Type) {n} where
    application : Application (λ ν → Term ν n) T
    application = record { _/_ = TermTypeApp._/_ lift {n = n} }

    open Application application public

  open Lifted termLift public

  -- apply a type variable substitution (renaming) to a term
  _/Var_ : ∀ {ν μ n} → Term ν n → Sub Fin ν μ → Term μ n
  _/Var_ = TermTypeApp._/_ varLift

  -- weaken a term with an additional type variable
  weaken : ∀ {ν n} → Term ν n → Term (suc ν) n
  weaken t = t /Var VarSubst.wk

  infix 8 _[/_]

  -- shorthand for single-variable type substitutions in terms
  _[/_] : ∀ {ν n} → Term (suc ν) n → Type ν → Term ν n
  t [/ b ] = t / sub b

module CtxSubst where

  _/_ : ∀ {ν μ n} → Ctx ν n → Sub Type ν μ → Ctx μ n
  Γ / σ = Γ TypeSubst.⊙ σ

  weaken : ∀ {ν n} → Ctx ν n → Ctx (suc ν) n
  weaken Γ = Γ / TypeSubst.wk

  -- Variable substitution (renaming) lifted to typing contexts
  _/Var_ : ∀ {ν m k} → Sub Fin k m → Ctx ν m → Ctx ν k
  σ /Var Γ = map (λ x → lookup x Γ) σ

module TermTermSubst where

  -- Substitutions of terms in terms
  TermSub : (ℕ → ℕ → Set) → ℕ → ℕ → ℕ → Set
  TermSub T ν m n = Sub (T ν) m n

  record TermLift (T : ℕ → ℕ → Set) : Set where
    infix 10 _↑tm _↑tp
    field
      lift : ∀ {ν n} → T ν n → Term ν n
      _↑tm : ∀ {ν m n} → TermSub T ν m n → TermSub T ν (suc m) (suc n)
      _↑tp : ∀ {ν m n} → TermSub T ν m n → TermSub T (suc ν) m n

  module TermTermApp {T} (l : TermLift T) where
    open TermLift l

    infixl 8 _/_

    -- Apply a term substitution to a term
    _/_ : ∀ {ν m n} → Term ν m → TermSub T ν m n → Term ν n
    var x      / σ = lift (lookup x σ)
    Λ t        / σ = Λ (t / (σ ↑tp))
    λ' a t     / σ = λ' a (t / σ ↑tm)
    t [ a ]    / σ = (t / σ) [ a ]
    s · t      / σ = (s / σ) · (t / σ)

  Fin′ : ℕ → ℕ → Set
  Fin′ _ m = Fin m

  varLift : TermLift Fin′
  varLift = record { lift = var; _↑tm = VarSubst._↑; _↑tp = id }

  infixl 8 _/Var_

  _/Var_ : ∀ {ν m n} → Term ν m → Sub Fin m n → Term ν n
  _/Var_ = TermTermApp._/_ varLift

  private
    module ExpandSimple {n : ℕ} where
      simple : Simple (Term n)
      simple = record { var = var; weaken = λ t → t /Var VarSubst.wk }

      open Simple simple public

  open ExpandSimple  using (_↑; simple)
  open TermTypeSubst using () renaming (weaken to weakenTp)

  termLift : TermLift Term
  termLift = record
    { lift = id; _↑tm = _↑ ; _↑tp = λ ρ → map weakenTp ρ }

  private
    module ExpandSubst {ν : ℕ} where
      app : Application (Term ν) (Term ν)
      app = record { _/_ = TermTermApp._/_ termLift {ν = ν} }

      subst : Subst (Term ν)
      subst = record
        { simple      = simple
        ; application = app
        }

      open Subst subst public

  open ExpandSubst public hiding (var; simple)

  infix 8 _[/_]

  -- Shorthand for single-variable term substitutions in terms
  _[/_] : ∀ {ν n} → Term ν (suc n) → Term ν n → Term ν n
  s [/ t ] = s / sub t

open TermTermSubst public using ()
  renaming (_/_ to _tm/tm_; _[/_] to _tm[/tm_]; weaken to tmtm-weaken)
open TermTypeSubst public using ()
  renaming (_/_ to _tm/tp_; _[/_] to _tm[/tp_]; weaken to tm-weaken)
open CtxSubst public using ()
  renaming (_/_ to _ctx/_; weaken to ctx-weaken; _/Var_ to _ctx/Var_)


text:
{-

Theory about isomorphisms

- Definitions of [section] and [retract]
- Definition of isomorphisms ([Iso])
- Any isomorphism is an equivalence ([isoToEquiv])

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Isomorphism where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level

-- Section and retract
module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
  section : (f : A → B) → (g : B → A) → Type ℓ'
  section f g = ∀ b → f (g b) ≡ b

  -- NB: `g` is the retraction!
  retract : (f : A → B) → (g : B → A) → Type ℓ
  retract f g = ∀ a → g (f a) ≡ a

record Iso {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') : Type (ℓ-max ℓ ℓ') where
  constructor iso
  field
    fun : A → B
    inv : B → A
    rightInv : section fun inv
    leftInv : retract fun inv

-- Any iso is an equivalence
module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (i : Iso A B) where
  open Iso i renaming ( fun to f
                      ; inv to g
                      ; rightInv to s
                      ; leftInv to t)

  private
    module _ (y : B) (x0 x1 : A) (p0 : f x0 ≡ y) (p1 : f x1 ≡ y) where
      fill0 : I → I → A
      fill0 i = hfill (λ k → λ { (i = i1) → t x0 k
                               ; (i = i0) → g y })
                      (inS (g (p0 (~ i))))

      fill1 : I → I → A
      fill1 i = hfill (λ k → λ { (i = i1) → t x1 k
                               ; (i = i0) → g y })
                      (inS (g (p1 (~ i))))

      fill2 : I → I → A
      fill2 i = hfill (λ k → λ { (i = i1) → fill1 k i1
                               ; (i = i0) → fill0 k i1 })
                      (inS (g y))

      p : x0 ≡ x1
      p i = fill2 i i1

      sq : I → I → A
      sq i j = hcomp (λ k → λ { (i = i1) → fill1 j (~ k)
                              ; (i = i0) → fill0 j (~ k)
                              ; (j = i1) → t (fill2 i i1) (~ k)
                              ; (j = i0) → g y })
                     (fill2 i j)

      sq1 : I → I → B
      sq1 i j = hcomp (λ k → λ { (i = i1) → s (p1 (~ j)) k
                               ; (i = i0) → s (p0 (~ j)) k
                               ; (j = i1) → s (f (p i)) k
                               ; (j = i0) → s y k })
                      (f (sq i j))

      lemIso : (x0 , p0) ≡ (x1 , p1)
      lemIso i .fst = p i
      lemIso i .snd = λ j → sq1 i (~ j)

  isoToIsEquiv : isEquiv f
  isoToIsEquiv .equiv-proof y .fst .fst = g y
  isoToIsEquiv .equiv-proof y .fst .snd = s y
  isoToIsEquiv .equiv-proof y .snd z = lemIso y (g y) (fst z) (s y) (snd z)

isoToPath : ∀ {ℓ} {A B : Type ℓ} → (Iso A B) → A ≡ B
isoToPath {A = A} {B = B} f i =
  Glue B (λ { (i = i0) → (A , (Iso.fun f , isoToIsEquiv f))
            ; (i = i1) → (B , (λ x → x) ,
                              record { equiv-proof = λ y → (y , refl)
                                                          , λ z i → z .snd (~ i)
                                                                  , λ j → z .snd (~ i ∨ j)})})


text:
module PiNF-syntax where

infixr 30 _⟷_
infixr 20 _◎_

------------------------------------------------------------------------------
-- First we define a universe of our value types

data B : Set where
  ZERO  : B
  ONE   : B
  PLUS  : B → B → B
  NEG   : B → B
  TIMES : B → B → B
  RECIP : B → B

------------------------------------------------------------------------------
-- Now we define another universe for our equivalences. First the codes for
-- equivalences.

data _⟷_ : B → B → Set where
  unite₊  : { b : B } → PLUS ZERO b ⟷ b
  uniti₊  : { b : B } → b ⟷ PLUS ZERO b
  swap₊   : { b₁ b₂ : B } → PLUS b₁ b₂ ⟷ PLUS b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷ PLUS b₁ (PLUS b₂ b₃)
  unite⋆  : { b : B } → TIMES ONE b ⟷ b
  uniti⋆  : { b : B } → b ⟷ TIMES ONE b
  swap⋆   : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷ TIMES b₂ b₁
  assocl⋆ : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷ TIMES (TIMES b₁ b₂) b₃
  assocr⋆ : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷ TIMES b₁ (TIMES b₂ b₃)
  dist    : { b₁ b₂ b₃ : B } →
            TIMES (PLUS b₁ b₂) b₃ ⟷ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor  : { b₁ b₂ b₃ : B } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷ TIMES (PLUS b₁ b₂) b₃
  η₊      : { b : B } → ZERO ⟷ PLUS (NEG b) b
  ε₊      : { b : B } → PLUS b (NEG b) ⟷ ZERO
  refe⋆   : { b : B } → RECIP (RECIP b) ⟷ b
  refi⋆   : { b : B } → b ⟷ RECIP (RECIP b)
  rile⋆   : { b : B } → TIMES b (TIMES b (RECIP b)) ⟷ b
  rili⋆   : { b : B } → b ⟷ TIMES b (TIMES b (RECIP b))
  id⟷   : { b : B } → b ⟷ b
  sym    : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
  _◎_    : { b₁ b₂ b₃ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₃) → (b₁ ⟷ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (PLUS b₁ b₂ ⟷ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : B } →
           (b₁ ⟷ b₃) → (b₂ ⟷ b₄) → (TIMES b₁ b₂ ⟷ TIMES b₃ b₄)

--

adjoint : { b₁ b₂ : B } → (b₁ ⟷ b₂) → (b₂ ⟷ b₁)
adjoint unite₊    = uniti₊
adjoint uniti₊    = unite₊
adjoint swap₊     = swap₊
adjoint assocl₊   = assocr₊
adjoint assocr₊   = assocl₊
adjoint unite⋆    = uniti⋆
adjoint uniti⋆    = unite⋆
adjoint swap⋆     = swap⋆
adjoint assocl⋆   = assocr⋆
adjoint assocr⋆   = assocl⋆
adjoint dist      = factor
adjoint factor    = dist
adjoint η₊        = swap₊ ◎ ε₊
adjoint ε₊        = η₊ ◎ swap₊
adjoint refe⋆     = refi⋆
adjoint refi⋆     = refe⋆
adjoint rile⋆     = rili⋆
adjoint rili⋆     = rile⋆
adjoint id⟷      = id⟷
adjoint (sym c)   = c
adjoint (c₁ ◎ c₂) = adjoint c₂ ◎ adjoint c₁
adjoint (c₁ ⊕ c₂) = adjoint c₁ ⊕ adjoint c₂
adjoint (c₁ ⊗ c₂) = adjoint c₁ ⊗ adjoint c₂

--

dist' : {b₁ b₂ b₃ : B} → TIMES b₁ (PLUS b₂ b₃) ⟷ PLUS (TIMES b₁ b₂) (TIMES b₁ b₃)
dist' = swap⋆ ◎ dist ◎ (swap⋆ ⊕ swap⋆)

midtofront : {a b c : B} → TIMES a (TIMES b c) ⟷ TIMES b (TIMES a c)
midtofront = assocl⋆ ◎ (swap⋆ ⊗ id⟷) ◎ assocr⋆

neg : {b₁ b₂ : B} → (b₁ ⟷ b₂) → (NEG b₁ ⟷ NEG b₂)
neg {b₁} {b₂} c =              -- -b1
  uniti₊ ◎                     -- 0 + (-b1)
  (η₊ {b₂} ⊕ id⟷) ◎           -- (-b2 + b2) + (-b1)
  ((id⟷ ⊕ sym c) ⊕ id⟷) ◎    -- (-b2 + b1) + (-b1)
  assocr₊ ◎                    -- (-b2) + (b1 + (-b1))
  (id⟷ ⊕ ε₊) ◎                -- (-b2) + 0
  swap₊ ◎                      -- 0 + (-b2)
  unite₊                       -- -b2

--

mul0 : {b : B} → TIMES ZERO b ⟷ ZERO
mul0 =                    -- 0*b
  uniti₊ ◎                  --  0 + 0*b
  (η₊ ⊕ id⟷) ◎        -- (-(0*b) + 0*b) + 0*b
  assocr₊ ◎              -- -(0*b) + (0*b + 0*b)
  (id⟷ ⊕ factor) ◎  -- -(0*b) + (0+0)*b
  (id⟷ ⊕ (unite₊ ⊗ id⟷)) ◎  -- -(0*b) + 0*b
  swap₊ ◎  ε₊ -- 0

{-
mul0 : {b : B} → TIMES ZERO b ⟷ ZERO
mul0 {b} = ⟷-begin
         TIMES ZERO b
   ⟷⟨ uniti₊ ⟩
         0 + 0*b
   ⟷⟨ η₊ ⊕ id⟷ ⟩
         (-(0*b) + 0*b) + 0*b
   ⟷⟨ assocr₊ ⟩
         -(0*b) + (0*b + 0*b)
   ⟷⟨ id⟷ ⊕ factor ⟩
         -(0*b) + (0+0)*b
  (id⟷ ⊕ (unite₊ ⊗ id⟷)) ◎  -- -(0*b) + 0*b
  swap₊ ◎  ε₊ -- 0
  ∎
-}

--  conType T cond = Σ[ x ∶ T ] cond x

inv0 : TIMES ZERO (RECIP ZERO) ⟷ ZERO
inv0 = mul0

--

recip : {b₁ b₂ : B} → (b₁ ⟷ b₂) → (RECIP b₁ ⟷ RECIP b₂)
recip {b₁} {b₂} c =          -- 1/a
  rili⋆ {RECIP b₁} ◎         -- 1/a * (1/a * 1/1/a)
  (id⟷ ⊗ (id⟷ ⊗ refe⋆)) ◎   -- 1/a * (1/a * a)
  assocl⋆ ◎                  -- (1/a * 1/a) * a
  (id⟷ ⊗ reciplem c) ◎     -- (1/a * 1/a) * (a * ((a * 1/b) * (b * 1/b)))
  assocl⋆ ◎                  -- (((1/a * 1/a) * a) * ((a * 1/b) * (b * 1/b)))
  ((id⟷ ⊗ refi⋆ ) ⊗ id⟷) ◎   -- (((1/a *1/a) * 1/(1/a)) * ((a * 1/b) * (b * 1/b))
  ((assocr⋆ ◎ rile⋆ ) ⊗ (id⟷ ⊗ ((sym c) ⊗ id⟷))) ◎ -- 1/a * ((a * 1/b) * (a * 1/b))
  (id⟷ ⊗ (assocr⋆ ◎ (id⟷ ⊗ midtofront))) ◎ -- 1/a * (a * (a * (1/b * 1/b)))
  (assocl⋆ ◎ assocl⋆) ◎                      -- ((1/a * a) * a) * (1/b * 1/b)
  (((swap⋆ ⊗ id⟷) ◎ swap⋆) ⊗ id⟷) ◎         -- ((a * (a * 1/a)) * (1/b * 1/b))
  (rile⋆ ⊗ id⟷ ) ◎                           -- a * (1/b * 1/b)
  ((c ◎ refi⋆ ) ⊗ id⟷) ◎ swap⋆ ◎             -- (1/b * 1/b) * 1/(1/b)
  assocr⋆ ◎ rile⋆                             -- 1/b
  where
    reciplem : {b₁ b₂ : B} → (b₁ ⟷ b₂) → (b₁ ⟷ (TIMES b₁ (TIMES (TIMES b₁ (RECIP b₂)) (TIMES b₂ (RECIP b₂)))))
    reciplem {b₁} {b₂} c =  c ◎                       -- b
      rili⋆ ◎                                -- b * (b * 1/b)
      (rili⋆ ⊗ id⟷) ◎                        -- (b * (b * 1/b)) * (b * 1/b)
      (((sym c) ⊗ ((sym c) ⊗ id⟷)) ⊗ id⟷) ◎ -- ((a * (a * 1/b)) * (b * 1/b))
      assocr⋆                                -- a * ((a * 1/b) * (b * 1/b))

------------------------------------------------------------------------------
-- Examples

BOOL : B
BOOL = PLUS ONE ONE

notπ : BOOL ⟷ BOOL
notπ = swap₊

BOOL² : B
BOOL² = TIMES BOOL BOOL

BOOL³ : B
BOOL³ = TIMES BOOL BOOL²

ifc : { b : B } → (b ⟷ b) → (TIMES BOOL b ⟷ TIMES BOOL b)
ifc c = dist ◎ ((id⟷ ⊗ c) ⊕ id⟷) ◎ factor

cnot : BOOL² ⟷ BOOL²
cnot = ifc notπ

toffoli : BOOL³ ⟷ BOOL³
toffoli = ifc cnot

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Human.Maybe where

data Maybe (A : Set) : Set where
  just    : A -> Maybe A
  nothing : Maybe A

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
module Issue2575 where

import Issue2575.M

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue373 where

data ⊤ : Set where
    tt : ⊤

{-# COMPILED_DATA ⊤ () () #-}

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

{-# BUILTIN NATURAL ℕ    #-}
{-# IMPORT Imports.Nat #-}

data List (A : Set) : Set where
  []   : List A
  _∷_ : A → List A → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}
{-# COMPILED_DATA List [] [] (:) #-}

postulate
  String : Set

{-# BUILTIN STRING String #-}

postulate
  IO : Set → Set

{-# BUILTIN IO IO #-}
{-# COMPILED_TYPE IO IO #-}

infixl 1 _>>=_

postulate
  _>>=_ : ∀ {A B} → IO A → (A → IO B) → IO B

{-# COMPILED _>>=_ (\_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b) #-}

{-# IMPORT Data.Text.IO #-}

postulate
  putStrLn : String → IO ⊤

{-# COMPILED putStrLn Data.Text.IO.putStrLn #-}

f : ℕ → String
f zero = "bad"
f _    = "ok"

-- Works:

-- main = putStrLn (f (suc zero))

-- Compiles, but when the program is run we (used to) get the output
-- "bad":

main = putStrLn (f 1)


text:
module BuiltinMustBeConstructor where

data Nat : Set where
  zero : Nat
  one  : Nat

suc : Nat -> Nat
suc x = x

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN SUC suc #-}

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


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

-- The Zero functor maps everything to the initial object of a
-- category (when it exists). Note quite const.

open import Level

open import Categories.Category
open import Categories.Functor using (Functor)
open import Categories.Object.Initial

private
  variable
    o ℓ e : Level
    C D : Category o ℓ e

Zero : Initial D → Functor C D
Zero {D = D} init = record
  { F₀ = λ _ → ⊥
  ; F₁ = λ _ → id
  ; identity = Equiv.refl
  ; homomorphism = Equiv.sym identity²
  ; F-resp-≈ = λ _ → Equiv.refl
  }
  where
  open Initial init
  open Category D

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:
{-

Theory about equivalences (definitions are in Core/Glue.agda)

- isEquiv is a proposition ([isPropIsEquiv])
- Any isomorphism is an equivalence ([isoToEquiv])

There are more statements about equivalences in Equiv/Properties.agda:

- if f is an equivalence then (cong f) is an equivalence
- if f is an equivalence then precomposition with f is an equivalence
- if f is an equivalence then postcomposition with f is an equivalence

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Equiv where

open import Cubical.Core.Glue

open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Nat

private
  variable
    ℓ ℓ'  : Level
    A B C : Type ℓ

fiber : ∀ {A : Type ℓ} {B : Type ℓ'} (f : A → B) (y : B) → Type (ℓ-max ℓ ℓ')
fiber {A = A} f y = Σ[ x ∈ A ] f x ≡ y

equivIsEquiv : ∀ {A : Type ℓ} {B : Type ℓ'} (e : A ≃ B) → isEquiv (equivFun e)
equivIsEquiv e = snd e

equivCtr : ∀ {A : Type ℓ} {B : Type ℓ'} (e : A ≃ B) (y : B) → fiber (equivFun e) y
equivCtr e y = e .snd .equiv-proof y .fst

equivCtrPath : ∀ {A : Type ℓ} {B : Type ℓ'} (e : A ≃ B) (y : B) →
  (v : fiber (equivFun e) y) → Path _ (equivCtr e y) v
equivCtrPath e y = e .snd .equiv-proof y .snd

-- The identity equivalence
idIsEquiv : ∀ (A : Type ℓ) → isEquiv (idfun A)
equiv-proof (idIsEquiv A) y =
  ((y , refl) , λ z i → z .snd (~ i) , λ j → z .snd (~ i ∨ j))

idEquiv : ∀ (A : Type ℓ) → A ≃ A
idEquiv A = (idfun A , idIsEquiv A)

-- Proof using isPropIsContr. This is slow and the direct proof below is better

isPropIsEquiv' : (f : A → B) → isProp (isEquiv f)
equiv-proof (isPropIsEquiv' f u0 u1 i) y =
  isPropIsContr (u0 .equiv-proof y) (u1 .equiv-proof y) i

-- Direct proof that computes quite ok (can be optimized further if
-- necessary, see:
-- https://github.com/mortberg/cubicaltt/blob/pi4s3_dimclosures/examples/brunerie2.ctt#L562

isPropIsEquiv : (f : A → B) → isProp (isEquiv f)
equiv-proof (isPropIsEquiv f p q i) y =
  let p2 = p .equiv-proof y .snd
      q2 = q .equiv-proof y .snd
  in p2 (q .equiv-proof y .fst) i
   , λ w j → hcomp (λ k → λ { (i = i0) → p2 w j
                            ; (i = i1) → q2 w (j ∨ ~ k)
                            ; (j = i0) → p2 (q2 w (~ k)) i
                            ; (j = i1) → w })
                   (p2 w (i ∨ j))

equivEq : (e f : A ≃ B) → (h : e .fst ≡ f .fst) → e ≡ f
equivEq e f h = λ i → (h i) , isProp→PathP isPropIsEquiv h (e .snd) (f .snd) i

isoToEquiv : Iso A B →  A ≃ B
isoToEquiv i = _ , isoToIsEquiv i

module _ (w : A ≃ B) where
  invEq : B → A
  invEq y = fst (fst (snd w .equiv-proof y))

  secEq : section invEq (w .fst)
  secEq x = λ i → fst (snd (snd w .equiv-proof (fst w x)) (x , (λ j → fst w x)) i)

  retEq : retract invEq (w .fst)
  retEq y = λ i → snd (fst (snd w .equiv-proof y)) i

equivToIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ≃ B → Iso A B
equivToIso {A = A} {B = B} e = iso (e .fst) (invEq e ) (retEq e) (secEq e)

invEquiv : A ≃ B → B ≃ A
invEquiv f = isoToEquiv (iso (invEq f) (fst f) (secEq f) (retEq f))

invEquivIdEquiv : (A : Type ℓ) → invEquiv (idEquiv A) ≡ idEquiv A
invEquivIdEquiv _ = equivEq _ _ refl

compEquiv : A ≃ B → B ≃ C → A ≃ C
compEquiv f g = isoToEquiv
                  (iso (λ x → g .fst (f .fst x))
                       (λ x → invEq f (invEq g x))
                       (λ y → (cong (g .fst) (retEq f (invEq g y))) ∙ (retEq g y))
                       (λ y → (cong (invEq f) (secEq g (f .fst y))) ∙ (secEq f y)))

compEquivIdEquiv : {A B : Type ℓ} (e : A ≃ B) → compEquiv (idEquiv A) e ≡ e
compEquivIdEquiv e = equivEq _ _ refl

compIso : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} →
            Iso A B → Iso B C → Iso A C
compIso i j = equivToIso (compEquiv (isoToEquiv i) (isoToEquiv j))

LiftEquiv : {A : Type ℓ} → A ≃ Lift {i = ℓ} {j = ℓ'} A
LiftEquiv = isoToEquiv (iso lift lower (λ _ → refl) (λ _ → refl))

-- module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}  where
--   invEquivInvol : (f : A ≃ B) → invEquiv (invEquiv f) ≡ f
--   invEquivInvol f i .fst = fst f
--   invEquivInvol f i .snd = propIsEquiv (fst f) (snd (invEquiv (invEquiv f))) (snd f) i

PropEquiv→Equiv : (Aprop : isProp A) (Bprop : isProp B) (f : A → B) (g : B → A) → (A ≃ B)
PropEquiv→Equiv Aprop Bprop f g = isoToEquiv (iso f g (λ b → Bprop (f (g b)) b) λ a → Aprop (g (f a)) a)

homotopyNatural : {f g : A → B} (H : ∀ a → f a ≡ g a) {x y : A} (p : x ≡ y) →
                  H x ∙ cong g p ≡ cong f p ∙ H y
homotopyNatural H p = homotopyNatural' H p ∙ □≡∙ _ _
  where
  homotopyNatural' : {f g : A → B} (H : ∀ a → f a ≡ g a) {x y : A} (p : x ≡ y) →
                     H x ∙ cong g p ≡ cong f p □ H y
  homotopyNatural' {f = f} {g = g} H {x} {y} p i j =
    hcomp (λ k → λ { (i = i0) → compPath-filler (H x) (cong g p) k j
                   ; (i = i1) → compPath'-filler (cong f p) (H y) k j
                   ; (j = i0) → cong f p (i ∧ (~ k))
                   ; (j = i1) → cong g p (i ∨ k) })
          (H (p i) j)

Hfa≡fHa : ∀ {A : Type ℓ} (f : A → A) → (H : ∀ a → f a ≡ a) → ∀ a → H (f a) ≡ cong f (H a)
Hfa≡fHa {A = A} f H a =
  H (f a)                          ≡⟨ rUnit (H (f a)) ⟩
  H (f a) ∙ refl                   ≡⟨ cong (_∙_ (H (f a))) (sym (rCancel (H a))) ⟩
  H (f a) ∙ H a ∙ sym (H a)        ≡⟨ assoc _ _ _ ⟩
  (H (f a) ∙ H a) ∙ sym (H a)      ≡⟨ cong (λ x →  x ∙ (sym (H a))) (homotopyNatural H (H a)) ⟩
  (cong f (H a) ∙ H a) ∙ sym (H a) ≡⟨ sym (assoc _ _ _) ⟩
  cong f (H a) ∙ H a ∙ sym (H a)   ≡⟨ cong (_∙_ (cong f (H a))) (rCancel _) ⟩
  cong f (H a) ∙ refl              ≡⟨ sym (rUnit _) ⟩
  cong f (H a) ∎

equivPi
  : ∀{F : A → Set ℓ} {G : A → Set ℓ'}
  → ((x : A) → F x ≃ G x) → (((x : A) → F x) ≃ ((x : A) → G x))
equivPi k .fst f x = k x .fst (f x)
equivPi k .snd .equiv-proof f
  .fst .fst x = equivCtr (k x) (f x) .fst
equivPi k .snd .equiv-proof f
  .fst .snd i x = equivCtr (k x) (f x) .snd i
equivPi k .snd .equiv-proof f
  .snd (g , p) i .fst x = equivCtrPath (k x) (f x) (g x , λ j → p j x) i .fst
equivPi k .snd .equiv-proof f
  .snd (g , p) i .snd j x = equivCtrPath (k x) (f x) (g x , λ k → p k x) i .snd j

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


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

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

module Reflection.Definition where

open import Data.List.Base using (map)
import Data.List.Properties as Listₚ
import Data.Nat.Properties as ℕₚ
import Data.Nat.Show as NatShow
open import Data.Product using (_×_; <_,_>; uncurry)
open import Data.String as String using (String; _<+>_; intersperse; braces)
open import Function using (_∘′_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Binary using (DecidableEquality)
open import Relation.Binary.PropositionalEquality

import Reflection.Argument as Arg
import Reflection.Name     as Name
import Reflection.Term     as Term

------------------------------------------------------------------------
-- Re-exporting type publically

open import Agda.Builtin.Reflection public
  using    ( Definition
           ; function
           ; data-type
           ; axiom
           )
  renaming ( record-type to record′
           ; data-cons   to constructor′
           ; prim-fun    to primitive′ )

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

function-injective : ∀ {cs cs′} → function cs ≡ function cs′ → cs ≡ cs′
function-injective refl = refl

data-type-injective₁ : ∀ {pars pars′ cs cs′} → data-type pars cs ≡ data-type pars′ cs′ → pars ≡ pars′
data-type-injective₁ refl = refl

data-type-injective₂ : ∀ {pars pars′ cs cs′} → data-type pars cs ≡ data-type pars′ cs′ → cs ≡ cs′
data-type-injective₂ refl = refl

data-type-injective : ∀ {pars pars′ cs cs′} → data-type pars cs ≡ data-type pars′ cs′ → pars ≡ pars′ × cs ≡ cs′
data-type-injective = < data-type-injective₁ , data-type-injective₂ >

record′-injective₁ : ∀ {c c′ fs fs′} → record′ c fs ≡ record′ c′ fs′ → c ≡ c′
record′-injective₁ refl = refl

record′-injective₂ : ∀ {c c′ fs fs′} → record′ c fs ≡ record′ c′ fs′ → fs ≡ fs′
record′-injective₂ refl = refl

record′-injective : ∀ {c c′ fs fs′} → record′ c fs ≡ record′ c′ fs′ → c ≡ c′ × fs ≡ fs′
record′-injective = < record′-injective₁ , record′-injective₂ >

constructor′-injective : ∀ {c c′} → constructor′ c ≡ constructor′ c′ → c ≡ c′
constructor′-injective refl = refl

_≟_ : DecidableEquality Definition
function cs       ≟ function cs′        =
  Dec.map′ (cong function) function-injective (cs Term.≟-Clauses cs′)
data-type pars cs ≟ data-type pars′ cs′ =
  Dec.map′ (uncurry (cong₂ data-type)) data-type-injective
           (pars ℕₚ.≟ pars′ ×-dec Listₚ.≡-dec Name._≟_ cs cs′)
record′ c fs      ≟ record′ c′ fs′      =
  Dec.map′ (uncurry (cong₂ record′)) record′-injective
           (c Name.≟ c′ ×-dec Listₚ.≡-dec (Arg.≡-dec Name._≟_) fs fs′)
constructor′ d    ≟ constructor′ d′     =
  Dec.map′ (cong constructor′) constructor′-injective (d Name.≟ d′)
axiom             ≟ axiom               = yes refl
primitive′        ≟ primitive′          = yes refl

-- antidiagonal
function cs ≟ data-type pars cs₁ = no (λ ())
function cs ≟ record′ c fs = no (λ ())
function cs ≟ constructor′ d = no (λ ())
function cs ≟ axiom = no (λ ())
function cs ≟ primitive′ = no (λ ())
data-type pars cs ≟ function cs₁ = no (λ ())
data-type pars cs ≟ record′ c fs = no (λ ())
data-type pars cs ≟ constructor′ d = no (λ ())
data-type pars cs ≟ axiom = no (λ ())
data-type pars cs ≟ primitive′ = no (λ ())
record′ c fs ≟ function cs = no (λ ())
record′ c fs ≟ data-type pars cs = no (λ ())
record′ c fs ≟ constructor′ d = no (λ ())
record′ c fs ≟ axiom = no (λ ())
record′ c fs ≟ primitive′ = no (λ ())
constructor′ d ≟ function cs = no (λ ())
constructor′ d ≟ data-type pars cs = no (λ ())
constructor′ d ≟ record′ c fs = no (λ ())
constructor′ d ≟ axiom = no (λ ())
constructor′ d ≟ primitive′ = no (λ ())
axiom ≟ function cs = no (λ ())
axiom ≟ data-type pars cs = no (λ ())
axiom ≟ record′ c fs = no (λ ())
axiom ≟ constructor′ d = no (λ ())
axiom ≟ primitive′ = no (λ ())
primitive′ ≟ function cs = no (λ ())
primitive′ ≟ data-type pars cs = no (λ ())
primitive′ ≟ record′ c fs = no (λ ())
primitive′ ≟ constructor′ d = no (λ ())
primitive′ ≟ axiom = no (λ ())


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

-- Quicksort

module Experiment.Induction where

-- agda-stdlib
open import Level
open import Data.List
open import Data.Product
open import Data.Nat as ℕ
open import Data.Nat.Induction as Ind
open import Relation.Binary as B
open import Relation.Unary as U
import      Relation.Unary.Properties as Uₚ
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Function.Base
open import Induction.WellFounded

private
  variable
    a p r : Level


text:
module Syntacticosmos (Gnd : Set)(U : Set)(El : U -> Set) where

open import Basics
open import Pr
open import Nom
import Kind
open Kind Gnd U El public
import Cxt
open Cxt Kind public
import Loc
open Loc Kind public
import Term
open Term Gnd U El public
import Shift
open Shift Gnd U El public
import Eta
open Eta Gnd U El public
import Inst
open Inst Gnd U El public
import Subst
open Subst Gnd U El public

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Cubical.Algebra.MonoidSolver.Examples where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.Monoid.Base
open import Cubical.Algebra.CommMonoid.Base
open import Cubical.Algebra.MonoidSolver.Reflection

private
  variable
    ℓ : Level

module ExamplesMonoid (M : Monoid ℓ) where
  open MonoidStr (snd M)

  _ : ε ≡ ε
  _ = solveMonoid M

  _ : ε · ε · ε ≡ ε
  _ = solveMonoid M

  _ : ∀ x → ε · x  ≡ x
  _ = solveMonoid M

  _ : ∀ x y z → (x · y) · z ≡ x · (y · z)
  _ = solveMonoid M

  _ : ∀ x y z → z · (x · y) · ε · z ≡ z · x · (y · z)
  _ = solveMonoid M

module ExamplesCommMonoid (M : CommMonoid ℓ) where
  open CommMonoidStr (snd M)

  _ : ε ≡ ε
  _ = solveCommMonoid M

  _ : ε · ε · ε ≡ ε
  _ = solveCommMonoid M

  _ : ∀ x → ε · x  ≡ x
  _ = solveCommMonoid M

  _ : ∀ x y z → (x · z) · y ≡ x · (y · z)
  _ = solveCommMonoid M

  _ : ∀ x y  → (x · y) · y · x · (x · y) ≡ x · x · x · (y · y · y)
  _ = solveCommMonoid M

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2019-02-17, issue #3417
--
-- We want to see highlighting for all the warnings,
-- even if the last thing is a hard error.

open import Agda.Builtin.Nat

reachable : Nat → Nat
reachable zer = 0
reachable (suc n) = suc (reachable n)

coverage : Nat → Nat
coverage zero = zero

Termination : Set
Termination = Termination

data Positivity : Set where
  abs : (Positivity → Nat) → Positivity

Universe : Set
Universe = Set

-- Problem was: Termination and Positivity got no highlighting.

max_forks_repo_name: shlevy/agda


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

open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules
open import GSeTT.Uniqueness-Derivations

module MCaTT.Desuspension where

  ↓GC : ∀ (Γ : Pre-Ctx) → Γ ⊢C → Pre-Ctx
  ↓GT : ∀ (Γ : Pre-Ctx) (A : Pre-Ty) → Γ ⊢T A → Pre-Ty
  ↓Gt : ∀ (Γ : Pre-Ctx) (A : Pre-Ty) (x : ℕ) → Γ ⊢t (Var x) # A → ℕ
  count-points : ∀ (Γ : Pre-Ctx) → ℕ

  ↓GC nil _ = nil
  ↓GC (Γ :: (x , ∗)) (cc Γ⊢ _ _) = ↓GC Γ Γ⊢
  ↓GC Γ+@(Γ :: (x , A@(_ ⇒[ _ ] _))) Γ+⊢@(cc Γ⊢ Γ⊢A _) = ↓GC Γ Γ⊢ :: (↓Gt Γ+ A x (var Γ+⊢ (inr (idp , idp))) , ↓GT Γ A Γ⊢A)

  ↓GT Γ ∗ Γ⊢∗ = ∗
  ↓GT Γ (_ ⇒[ ∗ ] _) _ = ∗
  ↓GT Γ (Var x ⇒[ A@(_ ⇒[ _ ] _) ] Var y) (ar Γ⊢A Γ⊢x Γ⊢y) = Var (↓Gt Γ A x Γ⊢x) ⇒[ ↓GT Γ A Γ⊢A ] Var (↓Gt Γ A y Γ⊢y)

  count-points nil = 0
  count-points (Γ :: (x , ∗)) = S (count-points Γ)
  count-points (Γ :: (x , _ ⇒[ _ ] _)) = count-points Γ

-- goes to Prelude
  _-_ : ℕ → ℕ → ℕ
  n - O = n
  O - S m = O
  S n - S m = n - m

  Sn-m : ∀ (n m : ℕ) → m ≤ n → (S n - m) == S (n - m)
  Sn-m n O _ = idp
  Sn-m O (S m) Sm≤0 = ⊥-elim (Sn≰0 _ Sm≤0)
  Sn-m (S n) (S m) (S≤ m≤n) = Sn-m n m m≤n
-- end of Prelude partA x₁ x₂

  ↓Gt (Γ :: (y , B)) A x (var _ (inr (_ , _))) = x - (count-points Γ)
  ↓Gt (Γ :: (y , B)) A x (var (cc Γ⊢ _ _) (inl x∈Γ)) = ↓Gt Γ A x (var Γ⊢ x∈Γ)

  count-points≤length : ∀ (Γ : Pre-Ctx) → count-points Γ ≤ length Γ
  count-points≤length nil = 0≤ 0
  count-points≤length (Γ :: (_ , ∗)) = S≤ (count-points≤length Γ)
  count-points≤length (Γ :: (_ , _ ⇒[ _ ] _)) = n≤m→n≤Sm (count-points≤length Γ)

  ↓length : ∀ (Γ : Pre-Ctx) (Γ⊢ : Γ ⊢C) → (length Γ - count-points Γ) == length (↓GC Γ Γ⊢)
  ↓length nil _ = idp
  ↓length (Γ :: (_ , ∗)) (cc Γ⊢ _ _) = ↓length Γ Γ⊢
  ↓length (Γ :: (x , _ ⇒[ _ ] _)) (cc Γ⊢ _ _) = Sn-m (length Γ) (count-points Γ) (count-points≤length Γ) >> ap S (↓length Γ Γ⊢)

  wk↓GT : ∀ (Γ : Pre-Ctx) (B : Pre-Ty) (y : ℕ) (A : Pre-Ty) (Γ⊢A : Γ ⊢T A) (Γ+⊢A : (Γ :: (y , B)) ⊢T A) → ↓GT Γ A Γ⊢A == ↓GT (Γ :: (y , B)) A Γ+⊢A
  wk↓Gt : ∀ (Γ : Pre-Ctx) (B : Pre-Ty) (y : ℕ) (x : ℕ) (A : Pre-Ty) (Γ⊢x : Γ ⊢t (Var x) # A) (Γ+⊢x : (Γ :: (y , B)) ⊢t (Var x) # A) → ↓Gt Γ A x Γ⊢x == ↓Gt (Γ :: (y , B)) A x Γ+⊢x

  wk↓GT Γ B y ∗ Γ⊢A Γ+⊢A = idp
  wk↓GT Γ B y (_ ⇒[ ∗ ] _) _ _ = idp
  wk↓GT Γ B y (Var x ⇒[ A@(_ ⇒[ _ ] _)] Var x') (ar Γ⊢A Γ⊢x Γ⊢x') (ar Γ+⊢A Γ+⊢x Γ+⊢x') = ⇒= (wk↓GT Γ B y A Γ⊢A Γ+⊢A) (Var= (wk↓Gt Γ B y x A Γ⊢x Γ+⊢x)) (Var= (wk↓Gt Γ B y x' A Γ⊢x' Γ+⊢x'))

  wk↓Gt (Γ :: (z , C)) B y x A (var (cc Γ⊢ _ _) (inl x∈Γ)) (var (cc Γ+⊢ _ _) (inl (inl x∈Γ+))) = wk↓Gt Γ C z x A (var Γ⊢ x∈Γ) (var Γ+⊢ (inl (x∈Γ+)))
  wk↓Gt (Γ :: (.(length Γ) , C)) B .(length (Γ :: (length Γ , C))) .(length Γ) .C (var (cc Γ⊢ _ idp) (inl x∈Γ)) (var (cc _ _ idp) (inl (inr (idp , idp)))) = ⊥-elim (lΓ∉Γ Γ⊢ x∈Γ)
  wk↓Gt (Γ :: (z , C)) B .(length (Γ :: (z , C))) .(length (Γ :: (z , C))) .B (var (cc Γ⊢ _ _) (inl x∈Γ)) (var (cc _ _ idp) (inr (idp , idp))) = ⊥-elim (n∉Γ Γ⊢ (n≤Sn _) x∈Γ)
  wk↓Gt (Γ :: (.(length Γ) , C)) B .(length (Γ :: (length Γ , C))) .(length Γ) .C (var (cc Γ⊢ _ idp) (inr (idp , idp))) (var (cc _ _ idp) (inl (inl lΓ∈Γ))) = ⊥-elim (lΓ∉Γ Γ⊢ lΓ∈Γ)
  wk↓Gt (Γ :: (.(length Γ) , C)) B .(length (Γ :: (length Γ , C))) .(length Γ) .C (var (cc Γ⊢ _ idp) (inr (idp , idp))) (var (cc _ _ idp) (inl (inr _))) = idp
  wk↓Gt (Γ :: (.(length Γ) , C)) B .(length (Γ :: (length Γ , C))) .(length Γ) .C (var (cc Γ⊢ _ idp) (inr (idp , idp))) (var (cc Γ+⊢ _ idp) (inr (contra , _))) = ⊥-elim (n≠Sn _ contra)

  ↓⊢C : ∀ (Γ : Pre-Ctx) (Γ⊢ : Γ ⊢C) → (↓GC Γ Γ⊢) ⊢C
  ↓⊢T : ∀ (Γ : Pre-Ctx) (A : Pre-Ty) (A≠∗ : A ≠ ∗) (Γ⊢ : Γ ⊢C) (Γ⊢A : Γ ⊢T A) → (↓GC Γ Γ⊢) ⊢T (↓GT Γ A Γ⊢A)
  ↓⊢t : ∀ (Γ : Pre-Ctx) (A : Pre-Ty) (x : ℕ) (A≠∗ : A ≠ ∗) (Γ⊢ : Γ ⊢C) (Γ⊢A : Γ ⊢T A) (Γ⊢x : Γ ⊢t (Var x) # A) → (↓GC Γ Γ⊢) ⊢t Var (↓Gt Γ A x Γ⊢x) # (↓GT Γ A Γ⊢A)

  ↓wkt : ∀ (Γ : Pre-Ctx) (C : Pre-Ty) (y : ℕ) {A B : Pre-Ty} {t u : Pre-Tm} (Γ⊢ : Γ ⊢C) (Γ+⊢ : (Γ :: (y , C)) ⊢C) (↓Γ⊢t : ↓GC Γ Γ⊢ ⊢t t # A) → A == B → t == u → ↓GC (Γ :: (y , C)) Γ+⊢ ⊢t u # B
  ↓wkt Γ ∗ y {A = A} {t = t} Γ⊢ (cc Γ⊢' _ _) ↓Γ⊢t idp idp = transport {B = λ p → ↓GC Γ p ⊢t t # A} (has-all-paths-⊢C Γ⊢ Γ⊢') ↓Γ⊢t
  ↓wkt Γ (_ ⇒[ C ] _) y {A = A} {t = t} Γ⊢ Γ+⊢@(cc Γ⊢' _ _) ↓Γ⊢t idp idp = wkt (transport {B = λ p → ↓GC Γ p ⊢t t # A} (has-all-paths-⊢C Γ⊢ Γ⊢') ↓Γ⊢t) (↓⊢C _ Γ+⊢)

  ↓⊢C nil ec = ec
  ↓⊢C (Γ :: (x , ∗)) (cc Γ⊢ _ _) = ↓⊢C Γ Γ⊢
  ↓⊢C (Γ :: (x , A@(_ ⇒[ _ ] _))) (cc Γ⊢ Γ⊢A idp) = cc (↓⊢C Γ Γ⊢) (↓⊢T Γ A (λ{()}) Γ⊢ Γ⊢A)  (↓length Γ Γ⊢)

  ↓⊢T Γ ∗ A≠∗ Γ⊢A = ⊥-elim (A≠∗ idp)
  ↓⊢T Γ (_ ⇒[ ∗ ] _) A≠∗ Γ⊢ (ar Γ⊢A _ _) = ob (↓⊢C Γ Γ⊢)
  ↓⊢T Γ (Var x ⇒[ A@(_ ⇒[ _ ] _) ] Var y) A≠∗ Γ⊢ (ar Γ⊢A Γ⊢x Γ⊢y) = ar (↓⊢T Γ A (λ{()}) Γ⊢ Γ⊢A) (↓⊢t Γ A x (λ{()}) Γ⊢ Γ⊢A Γ⊢x) (↓⊢t Γ A y (λ{()}) Γ⊢ Γ⊢A Γ⊢y)

  ↓⊢t (Γ :: (y , B)) A x A≠∗ Γ+⊢@(cc Γ⊢ x₁ x₂) Γ+⊢A Γ+⊢x@(var _ (inl x∈Γ)) =
    let Γ⊢x = var Γ⊢ x∈Γ in
    let Γ⊢A = Γ⊢t:A→Γ⊢A Γ⊢x in
    ↓wkt Γ B y Γ⊢ Γ+⊢ (↓⊢t Γ A x A≠∗ Γ⊢ Γ⊢A Γ⊢x) (wk↓GT Γ B y A Γ⊢A Γ+⊢A) (Var= (wk↓Gt Γ B y x A Γ⊢x Γ+⊢x))
  ↓⊢t Γ+@(Γ :: (x , ∗)) .∗ .x A≠∗ Γ+⊢@(cc _ _ _) Γ⊢A (var _ (inr (idp , idp))) = ⊥-elim (A≠∗ idp)
  ↓⊢t Γ+@(Γ :: (.(length Γ) , A@(_ ⇒[ _ ] _))) .(_ ⇒[ _ ] _) .(length Γ) A≠∗ Γ+⊢@(cc Γ⊢ Γ⊢A idp) Γ+⊢A@(ar _ _ _) (var (cc _ _ _) (inr (idp , idp))) =
    var (↓⊢C Γ+ Γ+⊢) (inr (idp , (wk↓GT Γ A (length Γ) A Γ⊢A Γ+⊢A ^)))

max_stars_repo_name: ThiBen/catt-formalization

max_issues_repo_name: ThiBen/catt-formalization

max_forks_repo_name: ThiBen/catt-formalization


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

-- Construction of basic species

open import Level
open import Data.Empty
open import Data.Fin.Base as Fin using (Fin)
open import Data.Fin.Properties using (¬Fin0)
open import Data.Fin.Permutation using (↔⇒≡)
open import Data.Nat.Base using (ℕ; suc; zero)
open import Data.Nat.Properties using (_≟_)
open import Data.Product as × using (Σ; proj₁; proj₂; _,_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Data.Sum.Base as ⊎ using (inj₁; inj₂)
open import Data.Sum.Relation.Binary.Pointwise using (_⊎ₛ_; inj₁; inj₂)
open import Data.Unit.Polymorphic using (⊤; tt)
open import Function.Base using () renaming (id to id→)
open import Function.Equality using (_⟨$⟩_; cong; Π) renaming (id to idΠ)
open import Function.Bundles using (Inverse)
open import Relation.Nullary using (Dec; yes; no)
import Function.Inverse as Inv
open import Relation.Binary.Bundles using (Setoid)
import Relation.Binary.PropositionalEquality as ≡
open import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial using (indexedSetoid)

open import Categories.Category.Core using (Category)
open import Categories.Category.Construction.ObjectRestriction using (ObjectRestriction)
open import Categories.Category.Construction.Core using (Core)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Category.Instance.FinSetoids using (FinSetoids; IsFiniteSetoid)
open import Categories.Category.Product
open import Categories.Functor.Core using (Functor)
open import Categories.Functor.Construction.Constant using (const)
open import Categories.Functor.Hom
open import Categories.Morphism.IsoEquiv using (_≃_)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.Category.Species

import Categories.Morphism as Mor

-- Some useful preliminary definitions.  Should be in stdlib
module _ {o ℓ : Level} where
  -- the Setoid version of ⊥
  ⊥-Setoid : Setoid o ℓ
  ⊥-Setoid = record
    { Carrier = Lift o ⊥
    ; _≈_ = λ ()
    ; isEquivalence = record { refl = λ { {()} } ; sym = λ { {()} } ; trans = λ { {()} } } }

  ⊤-Setoid : Setoid o ℓ
  ⊤-Setoid = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤}

  ⊤-FinSetoid : Σ (Setoid o ℓ) IsFiniteSetoid
  ⊤-FinSetoid =
    ⊤-Setoid ,
    1 ,
    record
      { f = λ _ → Fin.zero
      ; f⁻¹ = λ _ → tt
      ; cong₁ = λ _ → ≡.refl
      ; cong₂ = λ _ → tt
      ; inverse = (λ { Fin.zero → ≡.refl}) , λ _ → tt
      }

-- We could have 4 levels, and still define Zero and One′.
-- But X needs o ≡ o′ and ℓ ≡ ℓ′.  And then the 'proper' definition of One makes that all the same.
module _ (o : Level) where
  -- Setoid o ℓ is used a lot, name it too
  S = Setoid o o
  FinSet = FinSetoids o o
  𝔹 = Core FinSet
  Sp = Species o o o o

  open Category Sp
  open Mor FinSet
  open _≅_

  -- convenient alias: a structure is an Object of Species
  -- (which is of course a functor)
  Structure = Obj

  Zero : Structure
  Zero = const ⊥-Setoid

  -- One can be specified in two ways.  The traditional one (which doesn't generalize as well)
  -- uses 'counting' directly.
  One′ : Structure
  One′ = record
    { F₀ = on-singleton
    ; F₁ = map-singleton
    ; identity = λ {A} x≈y → identity′ {A} x≈y -- eta expansion needed
    ; homomorphism = λ {X} {Y} {Z} → homomorphism′ {X} {Y} {Z} -- eta needed
    ; F-resp-≈ = resp
    }
    where

    iso⇒Inverse : (A B : Σ S IsFiniteSetoid) (A≅B : A ≅ B) → Inverse (proj₁ A) (proj₁ B)
    iso⇒Inverse (s , n , p) (s′ , n′ , p′) A≅B = record
      { f = from A≅B ⟨$⟩_
      ; f⁻¹ = to A≅B ⟨$⟩_
      ; cong₁ = cong (from A≅B)
      ; cong₂ = cong (to A≅B)
      ; inverse = (λ x → isoʳ A≅B (Setoid.refl s′ {x})) , λ x → isoˡ A≅B (Setoid.refl s {x})
      }

    iso⇒≡ : {A B : Σ S IsFiniteSetoid} (A≅B : A ≅ B) → proj₁ (proj₂ A) ≡.≡ proj₁ (proj₂ B)
    iso⇒≡ {A@(s , n , p)} {B@(s′ , n′ , p′)} A≅B = ↔⇒≡ ( (translate p′) Inv.∘ (translate X Inv.∘ Inv.sym (translate p)))
      where
      X : Inverse (proj₁ A) (proj₁ B)
      X = iso⇒Inverse A B A≅B
      translate : {a b c d : Level} {X : Setoid a b} {Y : Setoid c d} → Inverse X Y → Inv.Inverse X Y
      translate I = record
        { to = record { _⟨$⟩_ = Inverse.f I ; cong = Inverse.cong₁ I }
        ; from = record { _⟨$⟩_ = Inverse.f⁻¹ I ; cong = Inverse.cong₂ I }
        ; inverse-of = record
          { left-inverse-of = Inverse.inverseʳ I
          ; right-inverse-of = Inverse.inverseˡ I
          }
        }

    -- one can do this in 3 cases structurally, but that leads to 9 cases elsewhere
    -- so a dispatch on size makes sense
    on-singleton : Σ S IsFiniteSetoid → S
    on-singleton (s , n , _) with n ≟ 1
    ... | yes p = s
    ... | no ¬p = ⊥-Setoid

    map-singleton : {A B : Σ S IsFiniteSetoid} → A ≅ B → Π (on-singleton A) (indexedSetoid (on-singleton B))
    map-singleton {s , n , p} {s′ , n′ , p′} A≅B with n ≟ 1 | n′ ≟ 1
    map-singleton A≅B | yes ≡.refl | yes ≡.refl = from A≅B
    map-singleton A≅B | yes ≡.refl | no  n′≢1    = ⊥-elim (n′≢1 (≡.sym (iso⇒≡ A≅B)))
    map-singleton A≅B | no  n≢1    | yes n′≡1    = ⊥-elim (n≢1 (≡.trans (iso⇒≡ A≅B) n′≡1))
    map-singleton A≅B | no  n≢1    | no  n′≢1    = idΠ

    identity′ : {A : Σ S IsFiniteSetoid} {x y : Setoid.Carrier (on-singleton A)} →
      let SA = on-singleton A in
      Setoid._≈_ SA x y → Setoid._≈_ SA (map-singleton {A} {A} ≅.refl ⟨$⟩ x) y
    identity′ {s , ℕ.suc ℕ.zero , p} x≈y = x≈y

    homomorphism′ : {X Y Z : Σ S IsFiniteSetoid} {f : X ≅ Y} {g : Y ≅ Z} {x y : Setoid.Carrier (on-singleton X)} →
      Setoid._≈_ (on-singleton X) x y →
      Setoid._≈_ (on-singleton Z) (map-singleton (≅.trans f g) ⟨$⟩ x) (map-singleton g ⟨$⟩ (map-singleton f ⟨$⟩ y))
    homomorphism′ {f = f} {g} x≈y with iso⇒≡ f | iso⇒≡ g
    homomorphism′ {_ , 1 , _} {f = f} {g} x≈y | ≡.refl | ≡.refl = cong (from g) (cong (from f) x≈y)

    resp : {A B : Σ S IsFiniteSetoid} {f g : A ≅ B} →
      (_≃_ FinSet f g) →
      {x y : Setoid.Carrier (on-singleton A)} →
      Setoid._≈_ (on-singleton A) x y → Setoid._≈_ (on-singleton B) (map-singleton f ⟨$⟩ x) (map-singleton g ⟨$⟩ y)
    resp {_ , 1 , _} {f = f} {g} f≈g x≈y with iso⇒≡ f
    resp {_ , 1 , _} {f = f} {g} f≈g x≈y | ≡.refl = _≃_.from-≈ f≈g x≈y

  -- There is a much nicer specification.
  One : Structure
  One = Hom[ 𝔹 ][ ⊤-FinSetoid ,-]

  -- the 'identity' Functor isn't really, it needs to forget the proof.
  X : Structure
  X = record
    { F₀ = proj₁
    ; F₁ = λ f → record
        { _⟨$⟩_ = from f ⟨$⟩_
        ; cong = cong (from f) }
    ; identity = id→
    ; homomorphism = λ { {f = f} {g} x≈y → cong (from g) (cong (from f) x≈y)}
    ; F-resp-≈ = _≃_.from-≈
    }

  -- generally this should be defined elsewhere
  _+_ : Structure → Structure → Structure
  A + B = record
    { F₀ = λ x → A.₀ x ⊎ₛ B.₀ x
    ; F₁ = λ X≅Y → record
      { _⟨$⟩_ = ⊎.map (A.₁ X≅Y ⟨$⟩_) (B.₁ X≅Y ⟨$⟩_)
      ; cong = λ { (inj₁ x≈y) → inj₁ (cong (A.₁ X≅Y) x≈y )
                 ; (inj₂ x≈y) → inj₂ (cong (B.₁ X≅Y) x≈y)}
      }
    ; identity = λ { (inj₁ x) → inj₁ (A.identity x)
                   ; (inj₂ x) → inj₂ (B.identity x)}
    ; homomorphism = λ { (inj₁ x) → inj₁ (A.homomorphism x)
                       ; (inj₂ x) → inj₂ (B.homomorphism x) }
    ; F-resp-≈ = λ { f≃g (inj₁ x) → inj₁ (A.F-resp-≈ f≃g x)
                   ; f≃g (inj₂ x) → inj₂ (B.F-resp-≈ f≃g x)}
    }
    where
    module A = Functor A
    module B = Functor B

  -- Hadamard product
  _×_ : Structure → Structure → Structure
  A × B = record
    { F₀ = λ x → ×-setoid (A.₀ x) (B.₀ x)
    ; F₁ = λ X≅Y → record
      { _⟨$⟩_ = ×.map (A.₁ X≅Y ⟨$⟩_) (B.₁ X≅Y ⟨$⟩_)
      ; cong = ×.map (cong (A.₁ X≅Y)) (cong (B.₁ X≅Y))
      }
    ; identity = ×.map A.identity B.identity
    ; homomorphism = ×.map A.homomorphism B.homomorphism
    ; F-resp-≈ = λ f≈g → ×.map (A.F-resp-≈ f≈g) (B.F-resp-≈ f≈g)
    }
    where
    module A = Functor A
    module B = Functor B


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

module Data.Binary.Proofs.Semantics where

open import Relation.Binary.PropositionalEquality
open import Data.Binary.Operations.Unary
open import Data.Binary.Proofs.Unary
open import Data.Binary.Definitions
open import Data.Binary.Operations.Semantics
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Relation.Binary.PropositionalEquality.FasterReasoning
import Data.Nat.Properties as ℕ
open import Function
open import Data.Nat.Reasoning

2*-distrib : ∀ x y → 2* (x ℕ.+ y) ≡ 2* x ℕ.+ 2* y
2*-distrib x y =
  begin
    2* (x ℕ.+ y)
  ≡⟨⟩
    (x ℕ.+ y) ℕ.+ (x ℕ.+ y)
  ≡⟨ ℕ.+-assoc x y (x ℕ.+ y)  ⟩
    x ℕ.+ (y ℕ.+ (x ℕ.+ y))
  ≡⟨ x +≫ ℕ.+-comm y (x ℕ.+ y) ⟩
    x ℕ.+ ((x ℕ.+ y) ℕ.+ y)
  ≡⟨ x +≫ ℕ.+-assoc x y y ⟩
    x ℕ.+ (x ℕ.+ (y ℕ.+ y))
  ≡˘⟨ ℕ.+-assoc x x _ ⟩
    2* x ℕ.+ 2* y
  ∎

s2*-distrib : ∀ x y → I ∷⇓ (x ℕ.+ y) ≡ suc (2* x ℕ.+ 2* y)
s2*-distrib x y = cong suc (2*-distrib x y)

max_stars_repo_name: oisdk/agda-binary

max_issues_repo_name: oisdk/agda-binary

max_forks_repo_name: oisdk/agda-binary


text:
module std-reduction where

open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; sig ; []env ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)
open import sn-calculus using (all-ready ; [s,δe]-env ; [x,δe]-env ; δ)

open import std-reduction.Base

open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Relation.Nullary
  using (¬_)
open import Relation.Binary.PropositionalEquality
  using (_≡_)
open _≡_
open import Data.Nat using (_+_ ; zero ; suc)
open import Data.List
  using ([])

infix 4 _⇁_

data _⇁_ : Term → Term → Set where
  std-par-right : ∀ {p q r E θ A} →
    left-most θ E →
    (p' :  halted p) →
    (q' :  done q) →
    r ≐ E ⟦ (p ∥ q) ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ (value-max (dhalted p') q' (inj₁ p')) ⟧e)
  std-par-left : ∀ {p q r E θ A} →
    left-most θ E →
    (p' :  paused p) →
    (q' :  halted q) →
    r ≐ E ⟦ (p ∥ q) ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ (value-max (dpaused p') (dhalted q') (inj₂ q')) ⟧e)
  std-is-present : ∀ {p q r E θ A} →
    left-most θ E →
     ∀ S →
    (S∈ : Env.isSig∈ S θ) →
    Env.sig-stats{S} θ S∈ ≡ Signal.present →
    r ≐ E ⟦ present S ∣⇒ p ∣⇒ q ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ p ⟧e)
  std-is-absent : ∀ {p q r E θ A} →
    left-most θ E →
    ∀ S →
    (S∈ : Env.isSig∈ S θ) →
    Env.sig-stats{S} θ S∈ ≡ Signal.absent →
    r ≐ E ⟦ present S ∣⇒ p ∣⇒ q ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ q ⟧e)
  std-emit : ∀{θ E r} →
    left-most θ E →
    ∀ S →
    (S∈ : (Env.isSig∈ S θ)) →
    (¬S≡a : ¬ (Env.sig-stats{S} θ S∈) ≡ Signal.absent) →
    r ≐ E ⟦ emit S ⟧e →
    (ρ⟨ θ , GO ⟩· r) ⇁ (ρ⟨ (Env.set-sig{S} θ S∈ Signal.present) , GO ⟩· E ⟦ nothin ⟧e)
  std-loop-unroll : ∀{θ E r p A} →
    left-most θ E →
    r ≐ E ⟦ loop p ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ (loopˢ p p) ⟧e)
  std-seq-done : ∀{θ E r q A} →
    left-most θ E →
    r ≐ E ⟦ (nothin >> q) ⟧e →
    ρ⟨ θ , A ⟩· r ⇁ (ρ⟨ θ , A ⟩· E ⟦ q ⟧e)
  std-seq-exit : ∀{θ E r q n A} →
    left-most θ E →
    r ≐ E ⟦ (exit n >> q) ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ (exit n) ⟧e)
  std-loopˢ-exit : ∀{θ E r q n A} →
    left-most θ E →
    r ≐ E ⟦ (loopˢ (exit n) q) ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ (exit n) ⟧e)
  std-suspend-done : ∀{θ E r p S A} →
    left-most θ E →
    (p' : halted p) →
    r ≐ E ⟦ (suspend p S) ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ p ⟧e)
  std-trap-done : ∀{θ E r p A} →
    left-most θ E →
    (p' : halted p) →
    r ≐ E ⟦ (trap p) ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ (↓ p') ⟧e)
  std-raise-signal : ∀{θ E r p S A} →
    left-most θ E →
    r ≐ E ⟦ (signl S p) ⟧e →
     (ρ⟨ θ , A ⟩· r) ⇁
     (ρ⟨ θ , A ⟩·
         E ⟦ (ρ⟨ (Θ SigMap.[ S ↦ Signal.unknown ] ShrMap.empty VarMap.empty) , WAIT ⟩·
               p) ⟧e)
  std-raise-shared : ∀{θ r s e p E A} →
    left-most θ E →
    (e' : all-ready e θ) →
    r ≐ E ⟦ shared s ≔ e in: p ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁
    (ρ⟨ θ , A ⟩·
      E ⟦ (ρ⟨ [s,δe]-env s (δ e') , WAIT ⟩· p) ⟧e)
  std-set-shared-value-old : ∀{θ r s e E} →
    left-most θ E →
    (e' : all-ready e θ) →
    (s∈ : (Env.isShr∈ s θ)) →
    Env.shr-stats{s} θ s∈ ≡ SharedVar.old →
    r ≐ E ⟦ s ⇐ e ⟧e →
    (ρ⟨ θ , GO ⟩· r) ⇁
    (ρ⟨ (Env.set-shr{s} θ s∈ (SharedVar.new) (δ e')) , GO ⟩·
      E ⟦ nothin ⟧e)

  std-set-shared-value-new : ∀{θ r s e E} →
    left-most θ E →
    (e' : all-ready e θ) →
    (s∈ : (Env.isShr∈ s θ)) →
    Env.shr-stats{s} θ s∈ ≡ SharedVar.new →
    r ≐ E ⟦ s ⇐ e ⟧e →
    (ρ⟨ θ , GO ⟩· r) ⇁
    (ρ⟨ (Env.set-shr{s} θ s∈ (SharedVar.new) (Env.shr-vals{s} θ s∈ + δ e')) , GO ⟩·
      E ⟦ nothin ⟧e)

  -- unshared state
  std-raise-var : ∀{θ r x p e E A} →
    left-most θ E →
    (e' : all-ready e θ) →
    r ≐ E ⟦ var x ≔ e in: p ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁
    (ρ⟨ θ , A ⟩·
      E ⟦ (ρ⟨ [x,δe]-env x (δ e') , WAIT ⟩· p) ⟧e)

  std-set-var : ∀{θ r x e E A} →
    left-most θ E →
    (x∈ : (Env.isVar∈ x θ)) →
    (e' : all-ready e θ) →
    r ≐ E ⟦ x ≔ e ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁
    (ρ⟨ (Env.set-var{x} θ x∈ (δ e')) , A ⟩·
      E ⟦ nothin ⟧e)

  -- if
  std-if-false : ∀{θ r p q x E A} →
    left-most θ E →
    (x∈ : (Env.isVar∈ x θ)) →
    Env.var-vals{x} θ x∈ ≡ zero →
    r ≐ E ⟦ if x ∣⇒ p ∣⇒ q ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ q ⟧e)

  std-if-true : ∀{θ r p q x E n A} →
    left-most θ E →
    (x∈ : (Env.isVar∈ x θ)) →
    Env.var-vals{x} θ x∈ ≡ suc n →
    r ≐ E ⟦ if x ∣⇒ p ∣⇒ q ⟧e →
    (ρ⟨ θ , A ⟩· r) ⇁ (ρ⟨ θ , A ⟩· E ⟦ p ⟧e)

  std-merge : ∀{θ₁ θ₂ r p E A₁ A₂} →
    left-most θ₁ E →
    r ≐ E ⟦ ρ⟨ θ₂ , A₂ ⟩· p ⟧e →
    (ρ⟨ θ₁ , A₁ ⟩· r) ⇁ (ρ⟨ (θ₁ ← θ₂) , (A-max A₁ A₂) ⟩· E ⟦ p ⟧e)

  std-absent : ∀{θ p A} →
    blocked-or-done θ A p →
    ¬ (can-set-absent θ p ≡ []) →
    ρ⟨ θ , A ⟩· p ⇁ ρ⟨ (set-all-absent θ (can-set-absent θ p)) , A ⟩· p

  std-readyness : ∀{θ p A} →
    blocked-or-done θ A p →
    (can-set-absent θ p ≡ []) →
    ¬ (can-set-ready θ p ≡ []) →
    ρ⟨ θ , A ⟩· p ⇁ ρ⟨ (set-all-ready θ (can-set-ready θ p)) , A ⟩· p

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-# OPTIONS --without-K #-}
module hott.equivalence.biinvertible where

open import sum
open import equality
open import function.core
open import function.isomorphism.core
open import function.isomorphism.utils
open import function.overloading
open import function.extensionality
open import hott.level.core
open import hott.level.closure
open import hott.equivalence.core
open import hott.equivalence.alternative
open import sets.unit

module _ {i j}{X : Set i}{Y : Set j} where
  InvL : (X → Y) → Set _
  InvL f = Σ (Y → X) λ g → (x : X) → g (f x) ≡ x

  InvR : (X → Y) → Set _
  InvR f = Σ (Y → X) λ g → (y : Y) → f (g y) ≡ y

  BiInv : (X → Y) → Set _
  BiInv f = InvL f × InvR f

_≈₂_ : ∀ {i j} → Set i → Set j → Set _
X ≈₂ Y = Σ (X → Y) BiInv

module _ {i j}{X : Set i}{Y : Set j} where
  ≅⇒b : X ≅ Y → X ≈₂ Y
  ≅⇒b f = apply f , (invert f , _≅_.iso₁ f) , (invert f , _≅_.iso₂ f)

  b⇒≅ : X ≈₂ Y → X ≅ Y
  b⇒≅ (f , (g , α) , (h , β)) = record
    { to = f
    ; from = g
    ; iso₁ = α
    ; iso₂ = λ y → sym (ap (f ∘' g) (β y)) · ap f (α (h y)) · β y }

  module _ (isom : X ≅ Y) where
    private
      f : X → Y
      f = apply isom

      φ : ∀ {k} (Z : Set k) → (X → Z) ≅ (Y → Z)
      φ Z = record
        { to = λ u → u ∘ invert isom
        ; from = λ v → v ∘ f
        ; iso₁ = λ u → funext λ x → ap u (_≅_.iso₁ isom x)
        ; iso₂ = λ v → funext λ y → ap v (_≅_.iso₂ isom y) }

    invl-level : contr (InvL f)
    invl-level = iso-level (Σ-ap-iso refl≅ λ g → sym≅ strong-funext-iso)
                           (proj₂ (≅⇒≈ (sym≅ (φ X))) id)

    private
      ψ : ∀ {k} (Z : Set k) → (Z → X) ≅ (Z → Y)
      ψ Z = record
        { to = λ u → f ∘ u
        ; from = λ v → invert isom ∘ v
        ; iso₁ = λ u → funext λ x → _≅_.iso₁ isom (u x)
        ; iso₂ = λ v → funext λ y → _≅_.iso₂ isom (v y) }

    invr-level : contr (InvR f)
    invr-level = iso-level (Σ-ap-iso refl≅ λ h → sym≅ strong-funext-iso)
                           (proj₂ (≅⇒≈ (ψ Y)) id)

  BiInv-level : (f : X → Y) → h 1 (BiInv f)
  BiInv-level f b₁ b₂ = h↑ (×-contr (invl-level isom) (invr-level isom)) b₁ b₂
    where
      isom : X ≅ Y
      isom = b⇒≅ (f , b₁)

  b⇔≈ : (X ≈₂ Y) ≅ (X ≈ Y)
  b⇔≈ = record
    { to = λ b → ≅⇒≈ (b⇒≅ b)
    ; from = λ φ → (≅⇒b (≈⇒≅ φ))
    ; iso₁ = λ { (f , b) → ap (λ b → f , b) (h1⇒prop (BiInv-level f) _ _) }
    ; iso₂ = λ { (f , e) → ap (λ e → f , e) (h1⇒prop (weak-equiv-h1 f) _ _) } }

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

test : ∀{N M : Nat} → Nat → Nat → Nat
test L K = {!N L M!}
-- Andreas, 2016-07-10, issue 2088
-- Changed behavior:
-- The hidden variables N and M are made visible
-- only the visible L is split.


text:
-- pull in Haskell Ints
module int where

open import bool
open import string
open import list
open import char
open import functions
open import nat

postulate
  int : Set
  int0 : int
  int1 : int
  _+int_ : int → int → int
  _*int_ : int → int → int
  _-int_ : int → int → int
  𝕃char-to-int : 𝕃 char → int
  int-to-𝕃char : int → 𝕃 char
  is-zero-int : int → 𝔹

{-# COMPILE GHC int = type Int #-}
{-# COMPILE GHC int0 = 0 #-}
{-# COMPILE GHC int1 = 1 #-}
{-# COMPILE GHC _+int_ = (+) #-}
{-# COMPILE GHC _*int_ = (*) #-}
{-# COMPILE GHC _-int_ = (-) #-}
{-# COMPILE GHC 𝕃char-to-int = \ x -> read x :: Int #-}
{-# COMPILE GHC int-to-𝕃char = \ x -> show x #-}
{-# COMPILE GHC is-zero-int = (==) 0 #-}

string-to-int : string → int
string-to-int = 𝕃char-to-int ∘ string-to-𝕃char

int-to-string : int → string
int-to-string = 𝕃char-to-string ∘ int-to-𝕃char

int-from-nat : ℕ → int
int-from-nat zero = int0
int-from-nat (suc n) = int1 +int (int-from-nat n)

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --overlapping-instances #-}

module Sort where

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)

open import Data.List using (List; _∷_; [])

open import Data.Variant using (Variants; inj; `_)

-- instance search methods

open import Data.List.Membership.Propositional.Instances
  using (⦃here⦄; ⦃there⦄)
open import Data.List.Relation.Binary.Subset.Propositional.Instances
  using (⦃[]⊆xs⦄; ⦃x∈ys-xs⊆ys⇒x∷xs⊆ys⦄; ⦅_⊆_⦆)
open import Data.Union.Relation.Binary.Subtype.Instances
  using (⦃refl⦄; ⦃generalize⦄; ⦃function⦄; ⌊_⌋)

-- ----------------------------------------------------------------------
-- Example (Injections)

data Sort : Set where
  term type : Sort

_ : Variants Sort (term ∷ [])
_ = ` term

_-Bounds : List Sort → Set
𝒮 -Bounds = Variants Sort 𝒮 → ℕ

Index : {𝒮 : List Sort} → Variants Sort 𝒮 → (𝒮 -Bounds) → Set
Index 𝓈 Γ = Fin (Γ 𝓈)

term-sorts : List Sort
term-sorts = term ∷ type ∷ []

infix 9 #_
data Term : term-sorts -Bounds → Set where
  #_ : ∀ {Γ} → Index (` term) Γ → Term Γ

-- ----------------------------------------------------------------------
-- Example (Subtyping)

type-sorts : List Sort
type-sorts = type ∷ []

infix 9 ~_

data Type : type-sorts -Bounds → Set where
  ~_ : ∀ {Γ} → Index (` type) Γ → Type Γ

it : ∀ {a} {A : Set a} → {{A}} → A
it {{x}} = x

_ : ⦅ type-sorts ⊆ term-sorts ⦆
_ = it

_ : term-sorts -Bounds → Set
_ = ⌊ Type ⌋

infixl 7 _[_]

data Term′ : term-sorts -Bounds → Set where
  #_ : ∀ {Γ} → Index (` term) Γ → Term′ Γ
  _[_] : ∀ {Γ} → Term′ Γ → ⌊ Type ⌋ Γ → Term′ Γ

max_stars_repo_name: johnyob/agda-union

max_issues_repo_name: johnyob/agda-union

max_forks_repo_name: johnyob/agda-union