text:
{-
This module contains:
- constant displayed structures of URG structures
- products of URG structures
-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.Constant where

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

open import Cubical.Data.Sigma

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties

open import Cubical.Relation.Binary

private
  variable
    ℓA ℓ≅A ℓB ℓ≅B ℓC ℓ≅C ℓ≅A×B : Level

-- The constant displayed structure of a URG structure 𝒮-B over 𝒮-A
𝒮ᴰ-const : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
           {B : Type ℓB} (𝒮-B : URGStr B ℓ≅B)
           → URGStrᴰ 𝒮-A (λ _ → B) ℓ≅B
𝒮ᴰ-const {A = A} 𝒮-A {B} 𝒮-B
  = urgstrᴰ (λ b _ b' → b ≅ b') ρ uni
    where
      open URGStr 𝒮-B

-- the total structure of the constant structure gives
-- nondependent product of URG structures
_×𝒮_ : {A : Type ℓA} (StrA : URGStr A ℓ≅A)
         {B : Type ℓB} (StrB : URGStr B ℓ≅B)
         → URGStr (A × B) (ℓ-max ℓ≅A ℓ≅B)
_×𝒮_ StrA {B} StrB = ∫⟨ StrA ⟩ (𝒮ᴰ-const StrA StrB)

-- any displayed structure defined over a
-- structure on a product can also be defined
-- over the swapped product
×𝒮-swap :  {A : Type ℓA} {B : Type ℓB} {C : A × B → Type ℓC}
         {ℓ≅A×B ℓ≅ᴰ : Level}
         {StrA×B : URGStr (A × B) ℓ≅A×B}
         (StrCᴰ : URGStrᴰ StrA×B C ℓ≅ᴰ)
         → URGStrᴰ (𝒮-transport Σ-swap-≃ StrA×B)
                   (λ (b , a) → C (a , b))
                   ℓ≅ᴰ
×𝒮-swap {C = C} {ℓ≅ᴰ = ℓ≅ᴰ} {StrA×B = StrA×B} StrCᴰ =
  make-𝒮ᴰ (λ c p c' → c ≅ᴰ⟨ p ⟩ c')
              ρᴰ
              λ (b , a) c → isUnivalent→contrRelSingl (λ c c' → c ≅ᴰ⟨ URGStr.ρ StrA×B (a , b) ⟩ c')
                                                        ρᴰ
                                                        uniᴰ
                                                        c
              where
                open URGStrᴰ StrCᴰ

ext: agda

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

open import Categories.Category

-- Some basic facts about Spans in some category 𝒞.
--
-- For the Category instances for these, you can look at the following modules
--    Categories.Category.Construction.Spans
--    Categories.Bicategory.Construction.Spans
module Categories.Category.Diagram.Span {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Function using (_$_)

open import Categories.Diagram.Pullback 𝒞
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open HomReasoning
open Equiv

open Pullback

private
  variable
    A B C D E : Obj

--------------------------------------------------------------------------------
-- Spans, and Span morphisms

infixr 9 _∘ₛ_

record Span (X Y : Obj) : Set (o ⊔ ℓ) where
  field
    M : Obj
    dom : M ⇒ X
    cod : M ⇒ Y

open Span

id-span : Span A A
id-span {A} = record
  { M = A
  ; dom = id
  ; cod = id
  }

record Span⇒ {X Y} (f g : Span X Y) : Set (o ⊔ ℓ ⊔ e) where
  field
    arr : M f ⇒ M g
    commute-dom : dom g ∘ arr ≈ dom f
    commute-cod : cod g ∘ arr ≈ cod f

open Span⇒

id-span⇒ : ∀ {f : Span A B} → Span⇒ f f
id-span⇒ = record
  { arr = id
  ; commute-dom = identityʳ
  ; commute-cod = identityʳ
  }

_∘ₛ_ : ∀ {f g h : Span A B} → (α : Span⇒ g h) → (β : Span⇒ f g) → Span⇒ f h
_∘ₛ_ {f = f} {g = g} {h = h} α β = record
  { arr = arr α ∘ arr β
  ; commute-dom = begin
    dom h ∘ arr α ∘ arr β ≈⟨ pullˡ (commute-dom α) ⟩
    dom g ∘ arr β ≈⟨ commute-dom β ⟩
    dom f ∎
  ; commute-cod = begin
    cod h ∘ arr α ∘ arr β ≈⟨ pullˡ (commute-cod α) ⟩
    cod g ∘ arr β ≈⟨ commute-cod β ⟩
    cod f ∎
  }

--------------------------------------------------------------------------------
-- Span Compositions

module Compositions (_×ₚ_ : ∀ {X Y Z} (f : X ⇒ Z) → (g : Y ⇒ Z) → Pullback f g) where

  _⊚₀_ : Span B C → Span A B → Span A C
  f ⊚₀ g =
    let g×ₚf = (cod g) ×ₚ (dom f)
    in record
        { M = P g×ₚf
        ; dom = dom g ∘ p₁ g×ₚf
        ; cod = cod f ∘ p₂ g×ₚf
        }

  _⊚₁_ : {f f′ : Span B C} {g g′ : Span A B} → Span⇒ f f′ → Span⇒ g g′ → Span⇒ (f ⊚₀ g) (f′ ⊚₀ g′)
  _⊚₁_  {f = f} {f′ = f′} {g = g} {g′ = g′} α β =
    let pullback = (cod g) ×ₚ (dom f)
        pullback′ = (cod g′) ×ₚ (dom f′)
    in record
      { arr = universal pullback′ {h₁ = arr β ∘ p₁ pullback} {h₂ = arr α ∘ p₂ pullback} $ begin
          cod g′ ∘ arr β ∘ p₁ pullback ≈⟨ pullˡ (commute-cod β) ⟩
          cod g ∘ p₁ pullback          ≈⟨ commute pullback ⟩
          dom f ∘ p₂ pullback          ≈⟨ pushˡ (⟺ (commute-dom α)) ⟩
          dom f′ ∘ arr α ∘ p₂ pullback ∎
      ; commute-dom = begin
          (dom g′ ∘ p₁ pullback′) ∘ universal pullback′ _ ≈⟨ pullʳ (p₁∘universal≈h₁ pullback′) ⟩
          dom g′ ∘ arr β ∘ p₁ pullback                    ≈⟨ pullˡ (commute-dom β) ⟩
          dom g ∘ p₁ pullback                             ∎
      ; commute-cod = begin
          (cod f′ ∘ p₂ pullback′) ∘ universal pullback′ _ ≈⟨ pullʳ (p₂∘universal≈h₂ pullback′) ⟩
          cod f′ ∘ arr α ∘ p₂ pullback                    ≈⟨ pullˡ (commute-cod α) ⟩
          cod f ∘ p₂ pullback                             ∎
      }

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:
------------------------------------------------------------------------------
-- Issue in the translation of definitions using λ-terms.
------------------------------------------------------------------------------

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

module Issue2b where

postulate
  D   : Set
  _≡_ : D → D → Set

-- The translations of foo₁ and foo₂ should be the same.
foo₁ : D → D → D
foo₁ d _ = d
{-# ATP definition foo₁ #-}

foo₂ : D → D → D
foo₂ = λ d _ → d
{-# ATP definition foo₂ #-}

postulate bar₁ : ∀ d e → d ≡ foo₁ d e
{-# ATP prove bar₁ #-}

postulate bar₂ : ∀ d e → d ≡ foo₂ d e
{-# ATP prove bar₂ #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.Ring {r₁ r₂} (R : Ring r₁ r₂) where

import Algebra.Properties.AbelianGroup as AGP
open import Function
import Relation.Binary.Reasoning.Setoid as EqR

open Ring R
open EqR setoid

open AGP +-abelianGroup public
  renaming ( ⁻¹-involutive to -‿involutive
           ; left-identity-unique to +-left-identity-unique
           ; right-identity-unique to +-right-identity-unique
           ; identity-unique to +-identity-unique
           ; left-inverse-unique to +-left-inverse-unique
           ; right-inverse-unique to +-right-inverse-unique
           ; ⁻¹-∙-comm to -‿+-comm
           )

-‿*-distribˡ : ∀ x y → - x * y ≈ - (x * y)
-‿*-distribˡ x y = begin
  - x * y                        ≈⟨ sym $ +-identityʳ _ ⟩
  - x * y + 0#                   ≈⟨ +-congˡ $ sym (-‿inverseʳ _) ⟩
  - x * y + (x * y + - (x * y))  ≈⟨ sym $ +-assoc _ _ _  ⟩
  - x * y + x * y + - (x * y)    ≈⟨ +-congʳ $ sym (distribʳ _ _ _) ⟩
  (- x + x) * y + - (x * y)      ≈⟨ +-congʳ $ *-congʳ $ -‿inverseˡ _ ⟩
  0# * y + - (x * y)             ≈⟨ +-congʳ $ zeroˡ _ ⟩
  0# + - (x * y)                 ≈⟨ +-identityˡ _ ⟩
  - (x * y)                      ∎

-‿*-distribʳ : ∀ x y → x * - y ≈ - (x * y)
-‿*-distribʳ x y = begin
  x * - y                        ≈⟨ sym $ +-identityˡ _ ⟩
  0# + x * - y                   ≈⟨ +-congʳ $ sym (-‿inverseˡ _) ⟩
  - (x * y) + x * y + x * - y    ≈⟨ +-assoc _ _ _  ⟩
  - (x * y) + (x * y + x * - y)  ≈⟨ +-congˡ $ sym (distribˡ _ _ _)  ⟩
  - (x * y) + x * (y + - y)      ≈⟨ +-congˡ $ *-congˡ $ -‿inverseʳ _ ⟩
  - (x * y) + x * 0#             ≈⟨ +-congˡ $ zeroʳ _ ⟩
  - (x * y) + 0#                 ≈⟨ +-identityʳ _ ⟩
  - (x * y)                      ∎


text:
open import FRP.JS.Bool using ( Bool )
open import FRP.JS.RSet using ( RSet ; ⟦_⟧ ; ⟨_⟩ ; _⇒_ )
open import FRP.JS.Behaviour using ( Beh ; map2 )
open import FRP.JS.Event using ( Evt ; ∅ ; _∪_ ; map )
open import FRP.JS.Product using ( _∧_ ; _,_ )
open import FRP.JS.String using ( String )

module FRP.JS.DOM where

infixr 2 _≟*_
infixr 4 _++_ _+++_

postulate
  Mouse Keyboard : RSet
  EventType : RSet → Set
  click : EventType Mouse
  press : EventType Keyboard

{-# COMPILED_JS click "click" #-}
{-# COMPILED_JS press "press" #-}

postulate
  DOW : Set
  unattached : DOW
  left right : DOW → DOW
  child : String → DOW → DOW
  events : ∀ {A} → EventType A → DOW → ⟦ Evt A ⟧

{-# COMPILED_JS unattached require("agda.frp").unattached() #-}
{-# COMPILED_JS left function(w) { return w.left(); } #-}
{-# COMPILED_JS right function(w) { return w.right(); } #-}
{-# COMPILED_JS child function(a) { return function(w) { return w.child(a); }; } #-}
{-# COMPILED_JS events function(A) { return function(t) { return function(w) { return function(s) { return w.events(t); }; }; }; } #-}

postulate
  DOM : DOW → RSet
  text : ∀ {w} → ⟦ Beh ⟨ String ⟩ ⇒ Beh (DOM w) ⟧
  attr : ∀ {w} → String → ⟦ Beh ⟨ String ⟩ ⇒ Beh (DOM w) ⟧
  element : ∀ a {w} → ⟦ Beh (DOM (child a w)) ⇒ Beh (DOM w) ⟧
  [] : ∀ {w} → ⟦ Beh (DOM w) ⟧
  _++_ : ∀ {w} → ⟦ Beh (DOM (left w)) ⇒ Beh (DOM (right w)) ⇒ Beh (DOM w) ⟧

{-# COMPILED_JS attr function(w) { return function(k) { return function(s) { return function(b) { return b.attribute(k); }; }; }; } #-}
{-# COMPILED_JS text function(w) { return function(s) { return function(b) { return b.text(); }; }; } #-}
{-# COMPILED_JS element function(a) { return function(w) { return function(s) { return function(b) { return w.element(a,b); }; }; }; } #-}
{-# COMPILED_JS [] function(w) { return require("agda.frp").empty; } #-}
{-# COMPILED_JS _++_ function(w) { return function(s) { return function(a) { return function(b) { return a.concat(b); }; }; }; } #-}

listen : ∀ {A w} → EventType A → ⟦ Beh (DOM w) ⇒ Evt A ⟧
listen {A} {w} t b = events t w

{-# COMPILED_JS listen function(A) { return function(w) { return function(t) { return function(s) { return function(b) { return w.events(t); }; }; }; }; } #-}

private
  postulate
    _≟_ : ∀ {w} → ⟦ DOM w ⇒ DOM w ⇒ ⟨ Bool ⟩ ⟧

  {-# COMPILED_JS _≟_ function(w) { return function(s) { return function(a) { return function(b) { return a.equals(b); }; }; }; } #-}

_≟*_ : ∀ {w} → ⟦ Beh (DOM w) ⇒ Beh (DOM w) ⇒ Beh ⟨ Bool ⟩ ⟧
_≟*_  = map2 _≟_

[+] : ∀ {A w} → ⟦ Beh (DOM w) ∧ Evt A ⟧
[+] = ([] , ∅)

_+++_ : ∀ {A w} → ⟦ (Beh (DOM (left w)) ∧ Evt A) ⇒ (Beh (DOM (right w)) ∧ Evt A) ⇒ (Beh (DOM w) ∧ Evt A) ⟧
(dom₁ , evt₁) +++ (dom₂ , evt₂) = ((dom₁ ++ dom₂) , (evt₁ ∪ evt₂))

text+ : ∀ {A w} → ⟦ Beh ⟨ String ⟩ ⇒ (Beh (DOM w) ∧ Evt A) ⟧
text+ msg = (text msg , ∅)

attr+ : ∀ {A w} → String → ⟦ Beh ⟨ String ⟩ ⇒ (Beh (DOM w) ∧ Evt A) ⟧
attr+ key val = (attr key val , ∅)

element+ : ∀ a {A w} → ⟦ (Beh (DOM (child a w)) ∧ Evt A) ⇒ (Beh (DOM w) ∧ Evt A) ⟧
element+ a (dom , evt) = (element a dom , evt)

listen+ : ∀ {A B w} → EventType A → ⟦ A ⇒ B ⟧ → ⟦ (Beh (DOM w) ∧ Evt B) ⇒ (Beh (DOM w) ∧ Evt B) ⟧
listen+ t f (dom , evt) = (dom , map f (listen t dom) ∪ evt)

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 --safe --warning=error --without-K #-}

open import Setoids.Setoids
open import Rings.Definition
open import Rings.Homomorphisms.Definition

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

module Rings.Isomorphisms.Definition {a b c d : _} {A : Set a} {S : Setoid {a} {b} A} {_+1_ _*1_ : A → A → A} (R1 : Ring S _+1_ _*1_) {B : Set c} {T : Setoid {c} {d} B} {_+2_ _*2_ : B → B → B} (R2 : Ring T _+2_ _*2_) where

record RingIso (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
  field
    ringHom : RingHom R1 R2 f
    bijective : SetoidBijection S T f

record RingsIsomorphic : Set (a ⊔ b ⊔ c ⊔ d) where
  field
    f : A → B
    iso : RingIso f


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.SymmetricGroup where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Data.Nat using (ℕ ; suc ; zero)
open import Cubical.Data.Fin using (Fin ; isSetFin)
open import Cubical.Data.Empty
open import Cubical.Relation.Nullary using (¬_)

open import Cubical.Algebra.Group

private
  variable
    ℓ : Level

Symmetric-Group : (X : Type ℓ) → isSet X → Group {ℓ}
Symmetric-Group X isSetX = makeGroup (idEquiv X) compEquiv invEquiv (isOfHLevel≃ 2 isSetX isSetX)
  compEquiv-assoc compEquivEquivId compEquivIdEquiv invEquiv-is-rinv invEquiv-is-linv

-- Finite symmetrics groups

Sym : ℕ → Group
Sym n = Symmetric-Group (Fin n) isSetFin

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Issue258 where

data D (A : Set) : Set where
  d : D A

foo : Set → Set
foo A with d {A}
foo A | p = A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Structure.Operator.Properties where

import      Lvl
open import Functional
open import Lang.Instance
open import Logic
open import Logic.Predicate
open import Logic.Propositional
import      Structure.Operator.Names as Names
open import Structure.Setoid
open import Syntax.Function
open import Type

private variable ℓ ℓₑ ℓ₁ ℓ₂ ℓ₃ ℓₑ₁ ℓₑ₂ ℓₑ₃ : Lvl.Level

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫_ : T₁ → T₁ → T₂) where
  record Commutativity : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ₂} where
    constructor intro
    field proof : Names.Commutativity(_▫_)
  commutativity = inst-fn Commutativity.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫_ : T₁ → T₂ → T₂) (id : T₁) where
  record Identityₗ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ₂} where
    constructor intro
    field proof : Names.Identityₗ(_▫_)(id)
  identityₗ = inst-fn Identityₗ.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫_ : T₁ → T₂ → T₂) (null : T₂) where
  record Absorberᵣ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ₂} where
    constructor intro
    field proof : Names.Absorberᵣ(_▫_)(null)
  absorberᵣ = inst-fn Absorberᵣ.proof

module _ {T₁ : Type{ℓ₁}} ⦃ _ : Equiv{ℓₑ₁}(T₁) ⦄ {T₂ : Type{ℓ₂}} (_▫_ : T₁ → T₂ → T₁) (id : T₂) where
  record Identityᵣ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ₁} where
    constructor intro
    field proof : Names.Identityᵣ(_▫_)(id)
  identityᵣ = inst-fn Identityᵣ.proof

module _ {T₁ : Type{ℓ₁}} ⦃ _ : Equiv{ℓₑ₁}(T₁) ⦄ {T₂ : Type{ℓ₂}} (_▫_ : T₁ → T₂ → T₁) (null : T₁) where
  record Absorberₗ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ₁} where
    constructor intro
    field proof : Names.Absorberₗ(_▫_)(null)
  absorberₗ = inst-fn Absorberₗ.proof

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) (id : T) where
  record Identity : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
    constructor intro
    field
      instance ⦃ left ⦄  : Identityₗ(_▫_)(id)
      instance ⦃ right ⦄ : Identityᵣ(_▫_)(id)
  identity-left = inst-fn (Identityₗ.proof ∘ Identity.left)
  identity-right = inst-fn (Identityᵣ.proof ∘ Identity.right)

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) where
  record Idempotence : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
    constructor intro
    field proof : Names.Idempotence(_▫_)
  idempotence = inst-fn Idempotence.proof

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) (id : T) where
  record Absorber : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
    constructor intro
    field
      instance ⦃ left ⦄  : Absorberₗ(_▫_)(id)
      instance ⦃ right ⦄ : Absorberᵣ(_▫_)(id)
  absorber-left = inst-fn (Absorberₗ.proof ∘ Absorber.left)
  absorber-right = inst-fn (Absorberᵣ.proof ∘ Absorber.right)

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) ⦃ identityₗ : ∃(Identityₗ(_▫_)) ⦄ where
  module _ (x : T) where
    module _ (inv : T) where
      record InverseElementₗ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
        constructor intro
        field proof : Names.InverseElementₗ(_▫_)([∃]-witness identityₗ)(x)(inv)
      inverseElementₗ = inst-fn InverseElementₗ.proof
    InvertibleElementₗ = ∃(InverseElementₗ)

  module _ (inv : T → T) where
    record InverseFunctionₗ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
      constructor intro
      field proof : Names.InverseFunctionₗ(_▫_)([∃]-witness identityₗ)(inv)
    inverseFunctionₗ = inst-fn InverseFunctionₗ.proof
  Invertibleₗ = ∃(InverseFunctionₗ)

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) ⦃ identityᵣ : ∃(Identityᵣ(_▫_)) ⦄ where
  module _ (x : T) where
    module _ (inv : T) where
      record InverseElementᵣ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
        constructor intro
        field proof : Names.InverseElementᵣ(_▫_)([∃]-witness identityᵣ)(x)(inv)
      inverseElementᵣ = inst-fn InverseElementᵣ.proof
    InvertibleElementᵣ = ∃(InverseElementᵣ)

  module _ (inv : T → T) where
    record InverseFunctionᵣ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
      constructor intro
      field proof : Names.InverseFunctionᵣ(_▫_)([∃]-witness identityᵣ)(inv)
    inverseFunctionᵣ = inst-fn InverseFunctionᵣ.proof
  Invertibleᵣ = ∃(InverseFunctionᵣ)

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) ⦃ identity : ∃(Identity(_▫_)) ⦄ where
  module _ (x : T) where
    module _ (inv : T) where
      InverseElement : Stmt
      InverseElement =
        InverseElementₗ(_▫_) ⦃ [∃]-map-proof Identity.left  identity ⦄ (x)(inv) ∧
        InverseElementᵣ(_▫_) ⦃ [∃]-map-proof Identity.right identity ⦄ (x)(inv)
    InvertibleElement = ∃(InverseElement)

  module _ (inv : T → T) where
    import Logic.IntroInstances

    record InverseFunction : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
      constructor intro
      field
        instance ⦃ left ⦄  : InverseFunctionₗ(_▫_) ⦃ [∃]-map-proof Identity.left  identity ⦄ (inv)
        instance ⦃ right ⦄ : InverseFunctionᵣ(_▫_) ⦃ [∃]-map-proof Identity.right identity ⦄ (inv)
    inverseFunction-left  = inst-fn (InverseFunctionₗ.proof ∘ InverseFunction.left)
    inverseFunction-right = inst-fn (InverseFunctionᵣ.proof ∘ InverseFunction.right)
  Invertible = ∃(InverseFunction)
  -- TODO: Add some kind of inverse function

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) ⦃ absorberₗ : ∃(Absorberₗ(_▫_)) ⦄ where
  module _ (opp : T → T) where
    record ComplementFunctionₗ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
      constructor intro
      field proof : Names.InverseFunctionₗ(_▫_)([∃]-witness absorberₗ)(opp)
    oppositeFunctionₗ = inst-fn ComplementFunctionₗ.proof

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) ⦃ absorberᵣ : ∃(Absorberᵣ(_▫_)) ⦄ where
  module _ (opp : T → T) where
    record ComplementFunctionᵣ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
      constructor intro
      field proof : Names.InverseFunctionᵣ(_▫_)([∃]-witness absorberᵣ)(opp)
    oppositeFunctionᵣ = inst-fn ComplementFunctionᵣ.proof

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) ⦃ absorber : ∃(Absorber(_▫_)) ⦄ where
  module _ (opp : T → T) where
    record ComplementFunction : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
      constructor intro
      field
        instance ⦃ left ⦄  : ComplementFunctionₗ(_▫_) ⦃ [∃]-map-proof Absorber.left  absorber ⦄ (opp)
        instance ⦃ right ⦄ : ComplementFunctionᵣ(_▫_) ⦃ [∃]-map-proof Absorber.right absorber ⦄ (opp)

module _{T : Type{ℓ}} ⦃ _ : Equiv{ℓₑ}(T) ⦄ (_▫_ : T → T → T) where
  record Associativity : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ} where
    constructor intro
    field proof : Names.Associativity(_▫_)
  associativity = inst-fn Associativity.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫₁_ : T₁ → T₂ → T₂) (_▫₂_ : T₂ → T₂ → T₂) where
  record Distributivityₗ : Stmt{Lvl.of(Type.of(_▫₁_)) Lvl.⊔ Lvl.of(Type.of(_▫₂_)) Lvl.⊔ ℓₑ₂} where
    constructor intro
    field proof : Names.Distributivityₗ(_▫₁_)(_▫₂_)
  distributivityₗ = inst-fn Distributivityₗ.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫₁_ : T₂ → T₁ → T₂) (_▫₂_ : T₂ → T₂ → T₂) where
  record Distributivityᵣ : Stmt{Lvl.of(Type.of(_▫₁_)) Lvl.⊔ Lvl.of(Type.of(_▫₂_)) Lvl.⊔ ℓₑ₂} where
    constructor intro
    field proof : Names.Distributivityᵣ(_▫₁_)(_▫₂_)
  distributivityᵣ = inst-fn Distributivityᵣ.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₃}(T₃) ⦄ (_▫_ : T₁ → T₂ → T₃) where
  record Cancellationₗ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ₂ Lvl.⊔ ℓₑ₃} where
    constructor intro
    field proof : Names.Cancellationₗ(_▫_)
  cancellationₗ = inst-fn Cancellationₗ.proof

module _ {T₁ : Type{ℓ₁}} ⦃ _ : Equiv{ℓₑ₁}(T₁) ⦄ {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₃}(T₃) ⦄ (_▫_ : T₁ → T₂ → T₃) where
  record Cancellationᵣ : Stmt{Lvl.of(Type.of(_▫_)) Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓₑ₃} where
    constructor intro
    field proof : Names.Cancellationᵣ(_▫_)
  cancellationᵣ = inst-fn Cancellationᵣ.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₁}(T₁) ⦄ (_▫₁_ : T₁ → T₃ → T₁) (_▫₂_ : T₁ → T₂ → T₃) where
  record Absorptionₗ : Stmt{Lvl.of(Type.of(_▫₁_)) Lvl.⊔ Lvl.of(Type.of(_▫₂_)) Lvl.⊔ ℓₑ₁} where
    constructor intro
    field proof : Names.Absorptionₗ(_▫₁_)(_▫₂_)
  absorptionₗ = inst-fn Absorptionₗ.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫₁_ : T₃ → T₂ → T₂) (_▫₂_ : T₁ → T₂ → T₃) where
  record Absorptionᵣ : Stmt{Lvl.of(Type.of(_▫₁_)) Lvl.⊔ Lvl.of(Type.of(_▫₂_)) Lvl.⊔ ℓₑ₂} where
    constructor intro
    field proof : Names.Absorptionᵣ(_▫₁_)(_▫₂_)
  absorptionᵣ = inst-fn Absorptionᵣ.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫₁_ : T₁ → T₂ → T₃) (_▫₂_ : T₁ → T₃ → T₂) where
  record InverseOperatorₗ : Stmt{Lvl.of(Type.of(_▫₁_)) Lvl.⊔ Lvl.of(Type.of(_▫₂_)) Lvl.⊔ ℓₑ₂} where
    constructor intro
    field proof : Names.InverseOperatorₗ(_▫₁_)(_▫₂_)
  inverseOperₗ = inst-fn InverseOperatorₗ.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} {T₃ : Type{ℓ₃}} ⦃ _ : Equiv{ℓₑ₁}(T₁) ⦄ (_▫₁_ : T₁ → T₂ → T₃) (_▫₂_ : T₃ → T₂ → T₁) where
  record InverseOperatorᵣ : Stmt{Lvl.of(Type.of(_▫₁_)) Lvl.⊔ Lvl.of(Type.of(_▫₂_)) Lvl.⊔ ℓₑ₁} where
    constructor intro
    field proof : Names.InverseOperatorᵣ(_▫₁_)(_▫₂_)
  inverseOperᵣ = inst-fn InverseOperatorᵣ.proof

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫_ : T₁ → T₂ → T₂) (inv : T₁ → T₁) where
  InversePropertyₗ = InverseOperatorₗ(_▫_)(a ↦ b ↦ inv(a) ▫ b)
  module InversePropertyₗ = InverseOperatorₗ{_▫₁_ = _▫_}{_▫₂_ = a ↦ b ↦ inv(a) ▫ b}
  inversePropₗ = inverseOperₗ(_▫_)(a ↦ b ↦ inv(a) ▫ b)

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫_ : T₂ → T₁ → T₂) (inv : T₁ → T₁) where
  InversePropertyᵣ = InverseOperatorᵣ(_▫_)(a ↦ b ↦ a ▫ inv(b))
  module InversePropertyᵣ = InverseOperatorᵣ{_▫₁_ = _▫_}{_▫₂_ = a ↦ b ↦ a ▫ inv(b)}
  inversePropᵣ = inverseOperᵣ(_▫_)(a ↦ b ↦ a ▫ inv(b))

module _ {T₁ : Type{ℓ₁}} {T₂ : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(T₂) ⦄ (_▫_ : T₁ → T₁ → T₂) where
  record Central(x : T₁) : Stmt{ℓ₁ Lvl.⊔ ℓₑ₂} where
    constructor intro
    field proof : ∀{y : T₁} → (x ▫ y ≡ y ▫ x)

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:
open import Common.Prelude
open import TestHarness

module TestBool where

not : Bool → Bool
not true  = false
not false = true
{-# COMPILED_JS not function (x) { return !x; } #-}

_∧_ : Bool → Bool → Bool
true  ∧ x = x
false ∧ x = false
{-# COMPILED_JS _∧_ function (x) { return function (y) { return x && y; }; } #-}

_∨_ : Bool → Bool → Bool
true  ∨ x = true
false ∨ x = x
{-# COMPILED_JS _∨_ function (x) { return function (y) { return x || y; }; } #-}

_↔_ : Bool → Bool → Bool
true  ↔ true  = true
false ↔ false = true
_     ↔ _     = false
{-# COMPILED_JS _↔_ function (x) { return function (y) { return x === y; }; } #-}

tests : Tests
tests _ = (
    assert true "tt" ,
    assert (not false) "!ff" ,
    assert (true ∧ true) "tt∧tt" ,
    assert (not (true ∧ false)) "!(tt∧ff)" ,
    assert (not (false ∧ false)) "!(ff∧ff)" ,
    assert (not (false ∧ true)) "!(ff∧tt)" ,
    assert (true ∨ true) "tt∨tt" ,
    assert (true ∨ false) "tt∨ff" ,
    assert (false ∨ true) "ff∨tt" ,
    assert (not (false ∨ false)) "!(ff∧ff)" ,
    assert (true ↔ true) "tt=tt" ,
    assert (not (true ↔ false)) "tt≠ff" ,
    assert (not (false ↔ true)) "ff≠tt" ,
    assert (false ↔ false) "ff=ff"
 )

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module AllStdLib where

-- Ensure that the entire standard library is compiled.
import README

open import Data.Unit.Polymorphic using (⊤)
open import Data.String
open import IO using (putStrLn; run)
open import IO.Primitive using (IO; _>>=_)

import DivMod
import HelloWorld
import HelloWorldPrim
import ShowNat
import TrustMe
import Vec
import dimensions

infixr 1 _>>_
_>>_ : ∀ {A B : Set} → IO A → IO B → IO B
m >> m₁ = m >>= λ _ → m₁

main : IO ⊤
main = do
  run (putStrLn "Hello World!")
  DivMod.main
  HelloWorld.main
  HelloWorldPrim.main
  ShowNat.main
  TrustMe.main
  Vec.main
  dimensions.main

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
module rummy where

open import Data.Nat

-- The suit type
data Suit : Set where
  ♣ : Suit
  ♢ : Suit
  ♥ : Suit
  ♠ : Suit

-- A card consists of a value and a suite.
data Card : ℕ → Suit → Set where
  _of_ : (n : ℕ) (s : Suit) → Card n s

-- Common names for cards

A : ℕ; A = 1
K : ℕ; K = 13
Q : ℕ; Q = 12
J : ℕ; J = 11

--
-- The clubs suit
--

A♣  : Card A  ♣; A♣  = A  of ♣
2♣  : Card 2  ♣; 2♣  = 2  of ♣
3♣  : Card 3  ♣; 3♣  = 3  of ♣
4♣  : Card 4  ♣; 4♣  = 4  of ♣
5♣  : Card 5  ♣; 5♣  = 5  of ♣
6♣  : Card 6  ♣; 6♣  = 6  of ♣
7♣  : Card 7  ♣; 7♣  = 7  of ♣
8♣  : Card 8  ♣; 8♣  = 8  of ♣
9♣  : Card 9  ♣; 9♣  = 9  of ♣
10♣ : Card 10 ♣; 10♣ = 10 of ♣
J♣  : Card J  ♣; J♣  = J  of ♣
Q♣  : Card Q  ♣; Q♣  = Q  of ♣
K♣  : Card K  ♣; K♣  = K  of ♣

--
-- The diamond suit
--

A♢  : Card A  ♢; A♢  = A  of ♢
2♢  : Card 2  ♢; 2♢  = 2  of ♢
3♢  : Card 3  ♢; 3♢  = 3  of ♢
4♢  : Card 4  ♢; 4♢  = 4  of ♢
5♢  : Card 5  ♢; 5♢  = 5  of ♢
6♢  : Card 6  ♢; 6♢  = 6  of ♢
7♢  : Card 7  ♢; 7♢  = 7  of ♢
8♢  : Card 8  ♢; 8♢  = 8  of ♢
9♢  : Card 9  ♢; 9♢  = 9  of ♢
10♢ : Card 10 ♢; 10♢ = 10 of ♢
J♢  : Card J  ♢; J♢  = J  of ♢
Q♢  : Card Q  ♢; Q♢  = Q  of ♢
K♢  : Card K  ♢; K♢  = K  of ♢

--
-- The heart suit
--

A♥  : Card A  ♥; A♥  = A  of ♥
2♥  : Card 2  ♥; 2♥  = 2  of ♥
3♥  : Card 3  ♥; 3♥  = 3  of ♥
4♥  : Card 4  ♥; 4♥  = 4  of ♥
5♥  : Card 5  ♥; 5♥  = 5  of ♥
6♥  : Card 6  ♥; 6♥  = 6  of ♥
7♥  : Card 7  ♥; 7♥  = 7  of ♥
8♥  : Card 8  ♥; 8♥  = 8  of ♥
9♥  : Card 9  ♥; 9♥  = 9  of ♥
10♥ : Card 10 ♥; 10♥ = 10 of ♥
J♥  : Card J  ♥; J♥  = J  of ♥
Q♥  : Card Q  ♥; Q♥  = Q  of ♥
K♥  : Card K  ♥; K♥  = K  of ♥

--
-- The spade suit
--

A♠  : Card A  ♠; A♠  = A  of ♠
2♠  : Card 2  ♠; 2♠  = 2  of ♠
3♠  : Card 3  ♠; 3♠  = 3  of ♠
4♠  : Card 4  ♠; 4♠  = 4  of ♠
5♠  : Card 5  ♠; 5♠  = 5  of ♠
6♠  : Card 6  ♠; 6♠  = 6  of ♠
7♠  : Card 7  ♠; 7♠  = 7  of ♠
8♠  : Card 8  ♠; 8♠  = 8  of ♠
9♠  : Card 9  ♠; 9♠  = 9  of ♠
10♠ : Card 10 ♠; 10♠ = 10 of ♠
J♠  : Card J  ♠; J♠  = J  of ♠
Q♠  : Card Q  ♠; Q♠  = Q  of ♠
K♠  : Card K  ♠; K♠  = K  of ♠

-- A run of length ℓ.
data Run  (suit : Suit) : (start ℓ : ℕ) → Set where
  [] : {start : ℕ} → Run  suit  start 0

  _,_ : {n ℓ : ℕ}
       → Card n suit
       → Run    suit (1 + n)     ℓ
       → Run    suit    n     (1 + ℓ)

-- A group of length ℓ.
data Group : (value ℓ : ℕ) → Set where
  [] : {value : ℕ} → Group value 0

  _,_ : {suit : Suit} {value ℓ : ℕ}
       → Card   value  suit
       → Group  value    ℓ
       → Group  value    (1 + ℓ)

-- Some pretty functions for creating runs. You can create a run as
-- follows:
--
-- myrun = ⟨ A♣ , 2♣ , 3♣ ⟩
--

⟨_ : {suit : Suit} {n ℓ : ℕ} → Run suit n ℓ → Run suit n ℓ
⟨ r = r

_⟩ : {suit : Suit} {n : ℕ} → Card n suit → Run suit n 1
c ⟩ = c , []

-- Some pretty functions for creating groups. You can create a group
-- group as follows:
--
-- mygroup = ⟦ A♣ , A♥ , A♢ ⟧
--

⟦_ : {value ℓ : ℕ} → Group value ℓ → Group value ℓ
⟦ g = g

_⟧ : {suit : Suit} {n : ℕ} → Card n suit → Group n 1
c ⟧ = c , []

infixr 2 _⟩ _⟧ _,_
infixl 1 ⟨_ ⟦_

mygroup = ⟦ A♣ , A♣ , A♠ ⟧
myrun   = ⟨ A♣ , 2♣ , 3♣ ⟩

max_stars_repo_name: piyush-kurur/sample-code

max_issues_repo_name: piyush-kurur/sample-code

max_forks_repo_name: piyush-kurur/sample-code


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

module Light.Implementation.Standard.Data.These where

open import Light.Library.Data.These using (Library ; Dependencies)

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            open import Data.These using (These ; this ; that ; these) public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Setoids.Setoids

module Setoids.Subset {a b : _} {A : Set a} (S : Setoid {a} {b} A) where

open Setoid S
open Equivalence eq

subset : {c : _} (pred : A → Set c) → Set (a ⊔ b ⊔ c)
subset pred = ({x y : A} → x ∼ y → pred x → pred y)

subsetSetoid : {c : _} {pred : A → Set c} → (subs : subset pred) → Setoid (Sg A pred)
Setoid._∼_ (subsetSetoid subs) (x , predX) (y , predY) = Setoid._∼_ S x y
Equivalence.reflexive (Setoid.eq (subsetSetoid subs)) {a , b} = reflexive
Equivalence.symmetric (Setoid.eq (subsetSetoid subs)) {a , prA} {b , prB} x = symmetric x
Equivalence.transitive (Setoid.eq (subsetSetoid subs)) {a , prA} {b , prB} {c , prC} x y = transitive x y


text:
------------------------------------------------------------------------------
-- Equality reasoning on FOL
------------------------------------------------------------------------------

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

-- This module only re-export the preorder reasoning instanced on the
-- propositional equality.

module Common.FOL.Relation.Binary.EqReasoning where

open import Common.FOL.FOL-Eq using ( _≡_ ; refl ; trans )

import Common.Relation.Binary.PreorderReasoning
open module ≡-Reasoning =
  Common.Relation.Binary.PreorderReasoning _≡_ refl trans public
    renaming ( _∼⟨_⟩_ to _≡⟨_⟩_ )

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module slots where

open import slots.defs
open import slots.bruteforce

max_stars_repo_name: semenov-vladyslav/slots-agda

max_issues_repo_name: semenov-vladyslav/slots-agda

max_forks_repo_name: semenov-vladyslav/slots-agda


text:
{-

Definition of the circle as a HIT with a proof that Ω(S¹) ≡ ℤ

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.S1.Base where

open import Cubical.Core.Glue

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Nat
  hiding (_+_ ; _*_ ; +-assoc ; +-comm)
open import Cubical.Data.Int

data S¹ : Type₀ where
  base : S¹
  loop : base ≡ base

-- Check that transp is the identity function for S¹
module _ where
  transpS¹ : ∀ (φ : I) (u0 : S¹) → transp (λ _ → S¹) φ u0 ≡ u0
  transpS¹ φ u0 = refl

  compS1 : ∀ (φ : I) (u : ∀ i → Partial φ S¹) (u0 : S¹ [ φ ↦ u i0 ]) →
    comp (λ _ → S¹) u (outS u0) ≡ hcomp u (outS u0)
  compS1 φ u u0 = refl

helix : S¹ → Type₀
helix base     = Int
helix (loop i) = sucPathInt i

ΩS¹ : Type₀
ΩS¹ = base ≡ base

encode : ∀ x → base ≡ x → helix x
encode x p = subst helix p (pos zero)

winding : ΩS¹ → Int
winding = encode base

intLoop : Int → ΩS¹
intLoop (pos zero)       = refl
intLoop (pos (suc n))    = intLoop (pos n) ∙ loop
intLoop (negsuc zero)    = sym loop
intLoop (negsuc (suc n)) = intLoop (negsuc n) ∙ sym loop

decodeSquare : (n : Int) → PathP (λ i → base ≡ loop i) (intLoop (predInt n)) (intLoop n)
decodeSquare (pos zero) i j    = loop (i ∨ ~ j)
decodeSquare (pos (suc n)) i j = hfill (λ k → λ { (j = i0) → base
                                                ; (j = i1) → loop k } )
                                       (inS (intLoop (pos n) j)) i
decodeSquare (negsuc n) i j = hcomp (λ k → λ { (i = i1) → intLoop (negsuc n) j
                                             ; (j = i0) → base
                                             ; (j = i1) → loop (i ∨ ~ k) })
                                    (intLoop (negsuc n) j)

decode : (x : S¹) → helix x → base ≡ x
decode base         = intLoop
decode (loop i) y j =
  let n : Int
      n = unglue (i ∨ ~ i) y
  in hcomp (λ k → λ { (i = i0) → intLoop (predSuc y k) j
                    ; (i = i1) → intLoop y j
                    ; (j = i0) → base
                    ; (j = i1) → loop i })
           (decodeSquare n i j)

decodeEncode : (x : S¹) (p : base ≡ x) → decode x (encode x p) ≡ p
decodeEncode x p = J (λ y q → decode y (encode y q) ≡ q) (λ _ → refl) p

isSetΩS¹ : isSet ΩS¹
isSetΩS¹ p q r s j i =
  hcomp (λ k → λ { (i = i0) → decodeEncode base p k
                 ; (i = i1) → decodeEncode base q k
                 ; (j = i0) → decodeEncode base (r i) k
                 ; (j = i1) → decodeEncode base (s i) k })
        (decode base (isSetInt (winding p) (winding q) (cong winding r) (cong winding s) j i))

-- This proof does not rely on rewriting hcomp with empty systems in
-- Int as ghcomp has been implemented!
windingIntLoop : (n : Int) → winding (intLoop n) ≡ n
windingIntLoop (pos zero)       = refl
windingIntLoop (pos (suc n))    = cong sucInt (windingIntLoop (pos n))
windingIntLoop (negsuc zero)    = refl
windingIntLoop (negsuc (suc n)) = cong predInt (windingIntLoop (negsuc n))

ΩS¹≡Int : ΩS¹ ≡ Int
ΩS¹≡Int = isoToPath (iso winding intLoop windingIntLoop (decodeEncode base))

-- intLoop and winding are group homomorphisms
private
  intLoop-sucInt : (z : Int) → intLoop (sucInt z) ≡ intLoop z ∙ loop
  intLoop-sucInt (pos n)          = refl
  intLoop-sucInt (negsuc zero)    = sym (lCancel loop)
  intLoop-sucInt (negsuc (suc n)) =
      rUnit (intLoop (negsuc n))
    ∙ (λ i → intLoop (negsuc n) ∙ lCancel loop (~ i))
    ∙ assoc (intLoop (negsuc n)) (sym loop) loop

  intLoop-predInt : (z : Int) → intLoop (predInt z) ≡ intLoop z ∙ sym loop
  intLoop-predInt (pos zero)    = lUnit (sym loop)
  intLoop-predInt (pos (suc n)) =
      rUnit (intLoop (pos n))
    ∙ (λ i → intLoop (pos n) ∙ (rCancel loop (~ i)))
    ∙ assoc (intLoop (pos n)) loop (sym loop)
  intLoop-predInt (negsuc n)    = refl

intLoop-hom : (a b : Int) → (intLoop a) ∙ (intLoop b) ≡ intLoop (a + b)
intLoop-hom a (pos zero)       = sym (rUnit (intLoop a))
intLoop-hom a (pos (suc n))    =
    assoc (intLoop a) (intLoop (pos n)) loop
  ∙ (λ i → (intLoop-hom a (pos n) i) ∙ loop)
  ∙ sym (intLoop-sucInt (a + pos n))
intLoop-hom a (negsuc zero)    = sym (intLoop-predInt a)
intLoop-hom a (negsuc (suc n)) =
    assoc (intLoop a) (intLoop (negsuc n)) (sym loop)
  ∙ (λ i → (intLoop-hom a (negsuc n) i) ∙ (sym loop))
  ∙ sym (intLoop-predInt (a + negsuc n))

winding-hom : (a b : ΩS¹) → winding (a ∙ b) ≡ (winding a) + (winding b)
winding-hom a b i =
  hcomp (λ t → λ { (i = i0) → winding (decodeEncode base a t ∙ decodeEncode base b t)
                 ; (i = i1) → windingIntLoop (winding a + winding b) t })
        (winding (intLoop-hom (winding a) (winding b) i))

-- Based homotopy group

basedΩS¹ : (x : S¹) → Type₀
basedΩS¹ x = x ≡ x

-- Proof that the homotopy group is actually independent on the basepoint
-- first, give a quasi-inverse to the basechange basedΩS¹→ΩS¹ for any loop i
-- (which does *not* match at endpoints)
private
  ΩS¹→basedΩS¹-filler : I → I → ΩS¹ → I → S¹
  ΩS¹→basedΩS¹-filler l i x j =
    hfill (λ t → λ { (j = i0) → loop (i ∧ t)
                   ; (j = i1) → loop (i ∧ t) })
          (inS (x j)) l

  basedΩS¹→ΩS¹-filler : (_ i : I) → basedΩS¹ (loop i) → I → S¹
  basedΩS¹→ΩS¹-filler l i x j =
    hfill (λ t → λ { (j = i0) → loop (i ∧ (~ t))
                   ; (j = i1) → loop (i ∧ (~ t)) })
          (inS (x j)) l

ΩS¹→basedΩS¹ : (i : I) → ΩS¹ → basedΩS¹ (loop i)
ΩS¹→basedΩS¹ i x j = ΩS¹→basedΩS¹-filler i1 i x j

basedΩS¹→ΩS¹ : (i : I) → basedΩS¹ (loop i) → ΩS¹
basedΩS¹→ΩS¹ i x j = basedΩS¹→ΩS¹-filler i1 i x j

basedΩS¹→ΩS¹→basedΩS¹ : (i : I) → (x : basedΩS¹ (loop i))
                        → ΩS¹→basedΩS¹ i (basedΩS¹→ΩS¹ i x) ≡ x
basedΩS¹→ΩS¹→basedΩS¹ i x j k =
  hcomp (λ t → λ { (j = i1) → basedΩS¹→ΩS¹-filler (~ t) i x k
                 ; (j = i0) → ΩS¹→basedΩS¹ i (basedΩS¹→ΩS¹ i x) k
                 ; (k = i0) → loop (i ∧ (t ∨ (~ j)))
                 ; (k = i1) → loop (i ∧ (t ∨ (~ j))) })
        (ΩS¹→basedΩS¹-filler (~ j) i (basedΩS¹→ΩS¹ i x) k)

ΩS¹→basedΩS¹→ΩS¹ : (i : I) → (x : ΩS¹)
                        → basedΩS¹→ΩS¹ i (ΩS¹→basedΩS¹ i x) ≡ x
ΩS¹→basedΩS¹→ΩS¹ i x j k =
  hcomp (λ t → λ { (j = i1) → ΩS¹→basedΩS¹-filler (~ t) i x k
                 ; (j = i0) → basedΩS¹→ΩS¹ i (ΩS¹→basedΩS¹ i x) k
                 ; (k = i0) → loop (i ∧ ((~ t) ∧ j))
                 ; (k = i1) → loop (i ∧ ((~ t) ∧ j)) })
        (basedΩS¹→ΩS¹-filler (~ j) i (ΩS¹→basedΩS¹ i x) k)

-- from the existence of our quasi-inverse, we deduce that the basechange is an equivalence
-- for all loop i

basedΩS¹→ΩS¹-isequiv : (i : I) → isEquiv (basedΩS¹→ΩS¹ i)
basedΩS¹→ΩS¹-isequiv i = isoToIsEquiv (iso (basedΩS¹→ΩS¹ i) (ΩS¹→basedΩS¹ i)
                 (ΩS¹→basedΩS¹→ΩS¹ i) (basedΩS¹→ΩS¹→basedΩS¹ i))

-- now extend the basechange so that both ends match
-- (and therefore we get a basechange for any x : S¹)

private
  loop-conjugation : basedΩS¹→ΩS¹ i1 ≡ λ x → x
  loop-conjugation i x =
    let p = (doubleCompPath-elim loop x (sym loop))
            ∙ (λ i → (lUnit loop i ∙ x) ∙ sym loop)
    in
    ((sym (decodeEncode base (basedΩS¹→ΩS¹ i1 x)))
    ∙ (λ t → intLoop (winding (p t)))
    ∙ (λ t → intLoop (winding-hom (intLoop (pos (suc zero)) ∙ x)
                                  (intLoop (negsuc zero)) t))
    ∙ (λ t → intLoop ((winding-hom (intLoop (pos (suc zero))) x t)
                      + (windingIntLoop (negsuc zero) t)))
    ∙ (λ t → intLoop (((windingIntLoop (pos (suc zero)) t) + (winding x)) + (negsuc zero)))
    ∙ (λ t → intLoop ((+-comm (pos (suc zero)) (winding x) t) + (negsuc zero)))
    ∙ (λ t → intLoop (+-assoc (winding x) (pos (suc zero)) (negsuc zero) (~ t)))
    ∙ (decodeEncode base x)) i

  refl-conjugation : basedΩS¹→ΩS¹ i0 ≡ λ x → x
  refl-conjugation i x j =
    hfill (λ t → λ { (j = i0) → base
                   ; (j = i1) → base })
          (inS (x j)) (~ i)

  basechange : (x : S¹) → basedΩS¹ x → ΩS¹
  basechange base y = y
  basechange (loop i) y =
    hcomp (λ t → λ { (i = i0) → refl-conjugation t y
                   ; (i = i1) → loop-conjugation t y })
          (basedΩS¹→ΩS¹ i y)

  -- for any loop i, the old basechange is equal to the new one
  basedΩS¹→ΩS¹≡basechange : (i : I) → basedΩS¹→ΩS¹ i ≡ basechange (loop i)
  basedΩS¹→ΩS¹≡basechange i j y =
    hfill (λ t → λ { (i = i0) → refl-conjugation t y
                   ; (i = i1) → loop-conjugation t y })
          (inS (basedΩS¹→ΩS¹ i y)) j

  -- so for any loop i, the extended basechange is an equivalence
  basechange-isequiv-aux : (i : I) → isEquiv (basechange (loop i))
  basechange-isequiv-aux i =
    transport (λ j → isEquiv (basedΩS¹→ΩS¹≡basechange i j)) (basedΩS¹→ΩS¹-isequiv i)

  -- as being an equivalence is contractible, basechange is an equivalence for all x : S¹
  basechange-isequiv : (x : S¹) → isEquiv (basechange x)
  basechange-isequiv base = basechange-isequiv-aux i0
  basechange-isequiv (loop i) =
    hcomp (λ t → λ { (i = i0) → basechange-isequiv-aux i0
                   ; (i = i1) → isPropIsEquiv (basechange base) (basechange-isequiv-aux i1)
                                              (basechange-isequiv-aux i0) t })
          (basechange-isequiv-aux i)

  basedΩS¹≡ΩS¹ : (x : S¹) → basedΩS¹ x ≡ ΩS¹
  basedΩS¹≡ΩS¹ x = ua (basechange x , basechange-isequiv x)

basedΩS¹≡Int : (x : S¹) → basedΩS¹ x ≡ Int
basedΩS¹≡Int x = (basedΩS¹≡ΩS¹ x) ∙ ΩS¹≡Int

-- Some tests
module _ where
 private
  test-winding-pos : winding (intLoop (pos 5)) ≡ pos 5
  test-winding-pos = refl

  test-winding-neg : winding (intLoop (negsuc 5)) ≡ negsuc 5
  test-winding-neg = refl

-- the inverse when S¹ is seen as a group

inv : S¹ → S¹
inv base = base
inv (loop i) = loop (~ i)

-- rot, used in the Hopf fibration

rotLoop : (a : S¹) → a ≡ a
rotLoop base       = loop
rotLoop (loop i) j =
  hcomp (λ k → λ { (i = i0) → loop (j ∨ ~ k)
                 ; (i = i1) → loop (j ∧ k)
                 ; (j = i0) → loop (i ∨ ~ k)
                 ; (j = i1) → loop (i ∧ k)}) base

rot : S¹ → S¹ → S¹
rot base x     = x
rot (loop i) x = rotLoop x i

_*_ : S¹ → S¹ → S¹
a * b = rot a b

infixl 30 _*_

-- rot i j = filler-rot i j i1
filler-rot : I → I → I → S¹
filler-rot i j = hfill (λ k → λ { (i = i0) → loop (j ∨ ~ k)
                   ; (i = i1) → loop (j ∧ k)
                   ; (j = i0) → loop (i ∨ ~ k)
                   ; (j = i1) → loop (i ∧ k) }) (inS base)

isPropFamS¹ : ∀ {ℓ} (P : S¹ → Type ℓ) (pP : (x : S¹) → isProp (P x)) (b0 : P base) →
              PathP (λ i → P (loop i)) b0 b0
isPropFamS¹ P pP b0 i = pP (loop i) (transp (λ j → P (loop (i ∧ j))) (~ i) b0)
                                    (transp (λ j → P (loop (i ∨ ~ j))) i b0) i

rotIsEquiv : (a : S¹) → isEquiv (rot a)
rotIsEquiv base = idIsEquiv S¹
rotIsEquiv (loop i) = isPropFamS¹ (λ x → isEquiv (rot x))
                                  (λ x → isPropIsEquiv (rot x))
                                  (idIsEquiv _) i

-- more direct definition of the rot (loop i) equivalence

rotLoopInv : (a : S¹) → PathP (λ i → rotLoop (rotLoop a (~ i)) i ≡ a) refl refl
rotLoopInv a i j =
  hcomp
    (λ k → λ {
      (i = i0) → a;
      (i = i1) → rotLoop a (j ∧ ~ k);
      (j = i0) → rotLoop (rotLoop a (~ i)) i;
      (j = i1) → rotLoop a (i ∧ ~ k)})
    (rotLoop (rotLoop a (~ i ∨ j)) i)

rotLoopEquiv : (i : I) → S¹ ≃ S¹
rotLoopEquiv i =
  isoToEquiv
    (iso (λ a → rotLoop a i)
         (λ a → rotLoop a (~ i))
         (λ a → rotLoopInv a i)
         (λ a → rotLoopInv a (~ i)))

-- some cancellation laws, used in the Hopf fibration
private
  rotInv-aux-1 : I → I → I → I → S¹
  rotInv-aux-1 j k i =
    hfill (λ l → λ { (k = i0) → (loop (i ∧ ~ l)) * loop j
                   ; (k = i1) → loop j
                   ; (i = i0) → (loop k * loop j) * loop (~ k)
                   ; (i = i1) → loop (~ k ∧ ~ l) * loop j })
          (inS ((loop (k ∨ i) * loop j) * loop (~ k)))

  rotInv-aux-2 : I → I → I → S¹
  rotInv-aux-2 i j k =
     hcomp (λ l → λ { (k = i0) → inv (filler-rot (~ i) (~ j) l)
                    ; (k = i1) → loop (j ∧ l)
                    ; (i = i0) → filler-rot k j l
                    ; (i = i1) → loop (j ∧ l)
                    ; (j = i0) → loop (i ∨ k ∨ (~ l))
                    ; (j = i1) → loop ((i ∨ k) ∧ l) })
           (base)

  rotInv-aux-3 : I → I → I → I → S¹
  rotInv-aux-3 j k i =
    hfill (λ l → λ { (k = i0) → rotInv-aux-2 i j l
                   ; (k = i1) → loop j
                   ; (i = i0) → loop (k ∨ l) * loop j
                   ; (i = i1) → loop k * (inv (loop (~ j) * loop k)) })
          (inS (loop k * (inv (loop (~ j) * loop (k ∨ ~ i)))))

  rotInv-aux-4 : I → I → I → I → S¹
  rotInv-aux-4 j k i =
    hfill (λ l → λ { (k = i0) → rotInv-aux-2 i j l
                   ; (k = i1) → loop j
                   ; (i = i0) → loop j * loop (k ∨ l)
                   ; (i = i1) → (inv (loop (~ j) * loop k)) * loop k })
          (inS ((inv (loop (~ j) * loop (k ∨ ~ i))) * loop k))

rotInv-1 : (a b : S¹) → b * a * inv b ≡ a
rotInv-1 base base i = base
rotInv-1 base (loop k) i = rotInv-aux-1 i0 k i i1
rotInv-1 (loop j) base i = loop j
rotInv-1 (loop j) (loop k) i = rotInv-aux-1 j k i i1

rotInv-2 : (a b : S¹) → inv b * a * b ≡ a
rotInv-2 base base i = base
rotInv-2 base (loop k) i = rotInv-aux-1 i0 (~ k) i i1
rotInv-2 (loop j) base i = loop j
rotInv-2 (loop j) (loop k) i = rotInv-aux-1 j (~ k) i i1

rotInv-3 : (a b : S¹) → b * (inv (inv a * b)) ≡ a
rotInv-3 base base i = base
rotInv-3 base (loop k) i = rotInv-aux-3 i0 k (~ i) i1
rotInv-3 (loop j) base i = loop j
rotInv-3 (loop j) (loop k) i = rotInv-aux-3 j k (~ i) i1

rotInv-4 : (a b : S¹) → inv (b * inv a) * b ≡ a
rotInv-4 base base i = base
rotInv-4 base (loop k) i = rotInv-aux-4 i0 k (~ i) i1
rotInv-4 (loop j) base i = loop j
rotInv-4 (loop j) (loop k) i = rotInv-aux-4 j k (~ i) i1

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
{-# OPTIONS --no-pattern-matching #-}

id : {A : Set} (x : A) → A
id x = x

data Unit : Set where
  unit : Unit

fail : Unit → Set
fail unit = Unit
-- Expected error: Pattern matching is disabled


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

open import lib.Basics
open import lib.types.Pi
open import lib.types.Pointed

module lib.types.Cospan where

record Cospan {i j k : ULevel} : Type (lsucc (lmax (lmax i j) k)) where
  constructor cospan
  field
    A : Type i
    B : Type j
    C : Type k
    f : A → C
    g : B → C

record ⊙Cospan {i j k : ULevel} : Type (lsucc (lmax (lmax i j) k)) where
  constructor ⊙cospan
  field
    X : Ptd i
    Y : Ptd j
    Z : Ptd k
    f : fst (X ⊙→ Z)
    g : fst (Y ⊙→ Z)

⊙cospan-out : ∀ {i j k} → ⊙Cospan {i} {j} {k} → Cospan {i} {j} {k}
⊙cospan-out (⊙cospan X Y Z f g) =
  cospan (fst X) (fst Y) (fst Z) (fst f) (fst g)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-

Constant structure: _ ↦ A

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Constant where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv

open import Cubical.Foundations.SIP

private
  variable
    ℓ ℓ' : Level

-- Structured isomorphisms

module _ (A : Type ℓ') where

  ConstantStructure : Type ℓ → Type ℓ'
  ConstantStructure _ = A

  ConstantEquivStr : StrEquiv {ℓ} ConstantStructure ℓ'
  ConstantEquivStr (_ , a) (_ , a') _ = a ≡ a'

  constantUnivalentStr : UnivalentStr {ℓ} ConstantStructure ConstantEquivStr
  constantUnivalentStr e = idEquiv _

  constantEquivAction : EquivAction {ℓ} ConstantStructure
  constantEquivAction e = idEquiv _

  constantTransportStr : TransportStr {ℓ} constantEquivAction
  constantTransportStr e _ = sym (transportRefl _)


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Values for standard evaluation of MTerm
------------------------------------------------------------------------
import Parametric.Syntax.Type as Type
import Parametric.Syntax.MType as MType
import Parametric.Denotation.Value as Value

module Parametric.Denotation.MValue
    (Base : Type.Structure)
    (⟦_⟧Base : Value.Structure Base)
  where

open import Base.Denotation.Notation

open Type.Structure Base
open MType.Structure Base
open Value.Structure Base ⟦_⟧Base

open import Data.Product hiding (map)
open import Data.Sum hiding (map)
open import Data.Unit
open import Level
open import Function hiding (const)

module Structure where
  ⟦_⟧ValType : (τ : ValType) → Set
  ⟦_⟧CompType : (τ : CompType) → Set

  ⟦ U c ⟧ValType = ⟦ c ⟧CompType
  ⟦ B ι ⟧ValType = ⟦ base ι ⟧
  ⟦ vUnit ⟧ValType = ⊤
  ⟦ τ₁ v× τ₂ ⟧ValType = ⟦ τ₁ ⟧ValType × ⟦ τ₂ ⟧ValType
  ⟦ τ₁ v+ τ₂ ⟧ValType = ⟦ τ₁ ⟧ValType ⊎ ⟦ τ₂ ⟧ValType

  ⟦ F τ ⟧CompType = ⟦ τ ⟧ValType
  ⟦ σ ⇛ τ ⟧CompType = ⟦ σ ⟧ValType → ⟦ τ ⟧CompType

  instance
    -- This means: Overload ⟦_⟧ to mean ⟦_⟧ValType.
    meaningOfValType : Meaning ValType
    meaningOfValType = meaning ⟦_⟧ValType

    meaningOfCompType : Meaning CompType
    meaningOfCompType = meaning ⟦_⟧CompType

  -- We also provide: Environments of values (but not of computations).
  open import Base.Denotation.Environment ValType ⟦_⟧ValType public
    using ()
    renaming ( ⟦_⟧Var to ⟦_⟧ValVar
             ; ⟦_⟧Context to ⟦_⟧ValContext
             ; meaningOfContext to meaningOfValContext
             )

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
-- Logical consistency of IPL

open import Library

module Consistency (Base : Set) where

import Formulas    ; open module Form = Formulas     Base
import Derivations ; open module Der  = Derivations  Base
import NfModelMonad; open module NfM  = NfModelMonad Base
open Normalization caseTreeMonad using (norm)

-- No variable in the empty context.

noVar : ∀{A} → Hyp A ε → ⊥
noVar ()

-- No neutral in the empty context.

noNe :  ∀{A} → Ne ε A → ⊥
noNe (hyp ())
noNe (impE t u) = noNe t
noNe (andE₁ t)  = noNe t
noNe (andE₂ t)  = noNe t

-- No normal proof of False in the empty context.

noNf : Nf ε False → ⊥
noNf (orE t t₁ t₂) = noNe t
noNf (falseE t)    = noNe t

-- No proof of False in the empty context.

consistency : ε ⊢ False → ⊥
consistency = noNf ∘ norm

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


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

open import LogicalFormulae
open import Numbers.Naturals.Definition

module Sets.FinSet.Definition where

data FinSet : (n : ℕ) → Set where
  fzero : {n : ℕ} → FinSet (succ n)
  fsucc : {n : ℕ} → FinSet n → FinSet (succ n)

fsuccInjective : {n : ℕ} → {a b : FinSet n} → fsucc a ≡ fsucc b → a ≡ b
fsuccInjective refl = refl

data FinNotEquals : {n : ℕ} → (a b : FinSet (succ n)) → Set where
  fne2 : (a b : FinSet 2) → ((a ≡ fzero) && (b ≡ fsucc (fzero))) || ((b ≡ fzero) && (a ≡ fsucc (fzero))) → FinNotEquals {1} a b
  fneN : {n : ℕ} → (a b : FinSet (succ (succ (succ n)))) → (((a ≡ fzero) && (Sg (FinSet (succ (succ n))) (λ c → b ≡ fsucc c))) || ((Sg (FinSet (succ (succ n))) (λ c → a ≡ fsucc c)) && (b ≡ fzero))) || (Sg (FinSet (succ (succ n)) && FinSet (succ (succ n))) (λ t → (a ≡ fsucc (_&&_.fst t)) & (b ≡ fsucc (_&&_.snd t)) & FinNotEquals (_&&_.fst t) (_&&_.snd t))) → FinNotEquals {succ (succ n)} a b


text:
-- Andreas, 2017-07-28, issue #1126 reported by Saizan is fixed

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ
{-# BUILTIN NATURAL ℕ #-}

data Unit : Set where
  unit : Unit

slow : ℕ → Unit
slow zero = unit
slow (suc n) = slow n

postulate
  IO : Set → Set
{-# COMPILE GHC IO = type IO #-}
{-# BUILTIN IO IO #-}

postulate
  return  : ∀ {A} → A → IO A
{-# COMPILE GHC return = (\ _ -> return) #-}
{-# COMPILE JS return =
    function(u0) { return function(u1) { return function(x) { return function(cb) { cb(x); }; }; }; } #-}

{-# FOREIGN OCaml
  let return _ x world = Lwt.return x
#-}
{-# COMPILE OCaml return = return #-}

force : Unit → IO Unit
force unit = return unit

n = 3000000000

main : IO Unit
main = force (slow n)

-- Should terminate instantaneously.

max_stars_repo_name: xekoukou/agda-ocaml

max_issues_repo_name: xekoukou/agda-ocaml

max_forks_repo_name: xekoukou/agda-ocaml


text:
module Base.Prelude.Pair where

open import Base.Free using (Free; pure)

data Pair (Shape : Set) (Pos : Shape → Set) (A B : Set) : Set where
  pair : Free Shape Pos A → Free Shape Pos B → Pair Shape Pos A B

pattern Pair′ ma mb = pure (pair ma mb)

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
-- Quicksort

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

module Algorithms.List.Sort.Quick where

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

private
  variable
    a p r : Level

module _ {A : Set a} {P : U.Pred A p} (P? : U.Decidable P) where
  partition₁-defn : ∀ xs → proj₁ (partition P? xs) ≡ filter P? xs
  partition₁-defn xs = P.cong proj₁ (Listₚ.partition-defn P? xs)

  partition₂-defn : ∀ xs → proj₂ (partition P? xs) ≡ filter (Uₚ.∁? P?) xs
  partition₂-defn xs = P.cong proj₂ (Listₚ.partition-defn P? xs)

  length-partition₁ : ∀ xs → length (proj₁ (partition P? xs)) ℕ.≤ length xs
  length-partition₁ xs =
    P.subst (ℕ._≤ length xs)
            (P.sym $ P.cong length $ partition₁-defn xs)
            (Listₚ.length-filter P? xs)

  length-partition₂ : ∀ xs → length (proj₂ (partition P? xs)) ℕ.≤ length xs
  length-partition₂ xs =
    P.subst (ℕ._≤ length xs)
            (P.sym $ P.cong length $ partition₂-defn xs)
            (Listₚ.length-filter (Uₚ.∁? P?) xs)

module Quicksort {A : Set a} {_≤_ : Rel A r} (_≤?_ : B.Decidable _≤_) where
  split : A → List A → List A × List A
  split x xs = partition (λ y → y ≤? x) xs

  _L<_ : Rel (List A) _
  _L<_ = ℕ._<_ on length

  sort-acc : ∀ xs → Acc _L<_ xs → List A
  sort-acc []       _        = []
  sort-acc (x ∷ xs) (acc rs) =
    sort-acc ys (rs _ (ℕ.s≤s $ length-partition₁ (_≤? x) xs)) ++
    [ x ] ++
    sort-acc zs (rs _ (ℕ.s≤s $ length-partition₂ (_≤? x) xs))
    where
    splitted = split x xs
    ys = proj₁ splitted
    zs = proj₂ splitted

  L<-wf : WellFounded _L<_
  L<-wf = InverseImage.wellFounded length Ind.<-wellFounded

  -- Quicksort
  sort : List A → List A
  sort xs = sort-acc xs (L<-wf xs)


text:
module F2 where

open import Data.Empty
open import Data.Unit
open import Data.Sum hiding (map; [_,_])
open import Data.Product hiding (map; ,_)
open import Function using (flip)
open import Relation.Binary.Core
  using (IsEquivalence; Reflexive; Symmetric; Transitive)
open import Relation.Binary

open import Groupoid

infix  2  _∎      -- equational reasoning
infixr 2  _≡⟨_⟩_  -- equational reasoning

---------------------------------------------------------------------------
-- Paths

-- these are individual paths so to speak
-- should we represent a path like swap+ as a family explicitly:
-- swap+ : (x : A) -> x ⇛ swapF x
-- I guess we can: swap+ : (x : A) -> case x of inj1 -> swap1 x else swap2 x
{--
Use pointed types instead of singletons
If A={x0,x1,x2}, 1/A has three values:
(x0<-x0, x0<-x1, x0<-x2)
(x1<-x0, x1<-x1, x1<-x2)
(x2<-x0, x2<-x1, x2<-x2)
It is a fake choice between x0, x1, and x2 (some negative information). You base
yourself at x0 for example and enforce that any other value can be mapped to x0.
So think of a value of type 1/A as an uncertainty about which value of A we
have. It could be x0, x1, or x2 but at the end it makes no difference. There is
no choice.

You can manipulate a value of type 1/A (x0<-x0, x0<-x1, x0<-x2) by with a
path to some arbitrary path to b0 for example:

(b0<-x0<-x0, b0<-x0<-x1, b0<-x0<-x2)

eta_3 will give (x0<-x0, x0<-x1, x0<-x2, x0) for example but any other
combination is equivalent.

epsilon_3 will take (x0<-x0, x0<-x1, x0<-x2) and one actual xi which is now
certain; we can resolve our previous uncertainty by following the path from
xi to x0 thus eliminating the fake choice we seemed to have.

Explain connection to negative information.

Knowing head or tails is 1 bits. Giving you a choice between heads and tails
and then cooking this so that heads=tails takes away your choice.

--}

data _⇛_ : {A B : Set} → (x : A) → (y : B) → Set₁ where
  -- +
  unite₊⇛    : {A : Set} {x : A} → _⇛_ {⊥ ⊎ A} {A} (inj₂ x) x
  uniti₊⇛    : {A : Set} {x : A} → _⇛_ {A} {⊥ ⊎ A} x (inj₂ x)
  swap₁₊⇛    : {A B : Set} {x : A} → _⇛_ {A ⊎ B} {B ⊎ A} (inj₁ x) (inj₂ x)
  swap₂₊⇛    : {A B : Set} {y : B} → _⇛_ {A ⊎ B} {B ⊎ A} (inj₂ y) (inj₁ y)
  assocl₁₊⇛  : {A B C : Set} {x : A} →
               _⇛_ {A ⊎ (B ⊎ C)} {(A ⊎ B) ⊎ C} (inj₁ x) (inj₁ (inj₁ x))
  assocl₂₁₊⇛ : {A B C : Set} {y : B} →
               _⇛_ {A ⊎ (B ⊎ C)} {(A ⊎ B) ⊎ C} (inj₂ (inj₁ y)) (inj₁ (inj₂ y))
  assocl₂₂₊⇛ : {A B C : Set} {z : C} →
               _⇛_ {A ⊎ (B ⊎ C)} {(A ⊎ B) ⊎ C} (inj₂ (inj₂ z)) (inj₂ z)
  assocr₁₁₊⇛ : {A B C : Set} {x : A} →
               _⇛_ {(A ⊎ B) ⊎ C} {A ⊎ (B ⊎ C)} (inj₁ (inj₁ x)) (inj₁ x)
  assocr₁₂₊⇛ : {A B C : Set} {y : B} →
               _⇛_ {(A ⊎ B) ⊎ C} {A ⊎ (B ⊎ C)} (inj₁ (inj₂ y)) (inj₂ (inj₁ y))
  assocr₂₊⇛  : {A B C : Set} {z : C} →
               _⇛_ {(A ⊎ B) ⊎ C} {A ⊎ (B ⊎ C)} (inj₂ z) (inj₂ (inj₂ z))
  -- *
  unite⋆⇛    : {A : Set} {x : A} → _⇛_ {⊤ × A} {A} (tt , x) x
  uniti⋆⇛    : {A : Set} {x : A} → _⇛_ {A} {⊤ × A} x (tt , x)
  swap⋆⇛     : {A B : Set} {x : A} {y : B} → _⇛_ {A × B} {B × A} (x , y) (y , x)
  assocl⋆⇛   : {A B C : Set} {x : A} {y : B} {z : C} →
               _⇛_ {A × (B × C)} {(A × B) × C} (x , (y , z)) ((x , y) , z)
  assocr⋆⇛   : {A B C : Set} {x : A} {y : B} {z : C} →
               _⇛_ {(A × B) × C} {A × (B × C)} ((x , y) , z) (x , (y , z))
  -- distributivity
  dist₁⇛     : {A B C : Set} {x : A} {z : C} →
               _⇛_ {(A ⊎ B) × C} {(A × C) ⊎ (B × C)} (inj₁ x , z) (inj₁ (x , z))
  dist₂⇛     : {A B C : Set} {y : B} {z : C} →
               _⇛_ {(A ⊎ B) × C} {(A × C) ⊎ (B × C)} (inj₂ y , z) (inj₂ (y , z))
  factor₁⇛   : {A B C : Set} {x : A} {z : C} →
               _⇛_ {(A × C) ⊎ (B × C)} {(A ⊎ B) × C} (inj₁ (x , z)) (inj₁ x , z)
  factor₂⇛   : {A B C : Set} {y : B} {z : C} →
               _⇛_ {(A × C) ⊎ (B × C)} {(A ⊎ B) × C}
                   (inj₂ (y , z)) (inj₂ y , z)
  dist0⇛     : {A : Set} {• : ⊥} {x :  A} → _⇛_ {⊥ × A} {⊥} (• , x) •
  factor0⇛   : {A : Set} {• : ⊥} {x : A} → _⇛_ {⊥} {⊥ × A} • (• , x)
  -- congruence
  id⇛        : {A : Set} → (x : A) → x ⇛ x
  sym⇛       : {A B : Set} {x : A} {y : B} → x ⇛ y → y ⇛ x
  trans⇛     : {A B C : Set} {x : A} {y : B} {z : C} → x ⇛ y → y ⇛ z → x ⇛ z
  plus₁⇛     : {A B C D : Set} {x : A} {z : C} →
               x ⇛ z → _⇛_ {A ⊎ B} {C ⊎ D} (inj₁ x) (inj₁ z)
  plus₂⇛     : {A B C D : Set} {y : B} {w : D} →
               y ⇛ w → _⇛_ {A ⊎ B} {C ⊎ D} (inj₂ y) (inj₂ w)
  times⇛     : {A B C D : Set} {x : A} {y : B} {z : C} {w : D} →
               x ⇛ z → y ⇛ w → _⇛_ {A × B} {C × D} (x , y) (z , w)

-- permute
-- for any given type, we should be able to generate permutations mapping any
-- point to any other type

-- Introduce equational reasoning syntax to simplify proofs

_≡⟨_⟩_ : {A B C : Set} (x : A) {y : B} {z : C} → (x ⇛ y) → (y ⇛ z) → (x ⇛ z)
_ ≡⟨ p ⟩ q = trans⇛ p q

bydef : {A : Set} {x : A} → (x ⇛ x)
bydef {A} {x} = id⇛ x

_∎ : {A : Set} (x : A) → x ⇛ x
_∎ x = id⇛ x

data Singleton {A : Set} : A → Set where
  singleton : (x : A) → Singleton x

mutual

  ap : {A B : Set} {x : A} {y : B} → x ⇛ y → Singleton x → Singleton y
  ap {.(⊥ ⊎ A)} {A} {.(inj₂ x)} {x} unite₊⇛ (singleton .(inj₂ x)) =
    singleton x
  ap uniti₊⇛ (singleton x) = singleton (inj₂ x)
  ap (swap₁₊⇛ {A} {B} {x}) (singleton .(inj₁ x)) = singleton (inj₂ x)
  ap (swap₂₊⇛ {A} {B} {y}) (singleton .(inj₂ y)) = singleton (inj₁ y)
  ap (assocl₁₊⇛ {A} {B} {C} {x}) (singleton .(inj₁ x)) =
    singleton (inj₁ (inj₁ x))
  ap (assocl₂₁₊⇛ {A} {B} {C} {y}) (singleton .(inj₂ (inj₁ y))) =
    singleton (inj₁ (inj₂ y))
  ap (assocl₂₂₊⇛ {A} {B} {C} {z}) (singleton .(inj₂ (inj₂ z))) =
    singleton (inj₂ z)
  ap (assocr₁₁₊⇛ {A} {B} {C} {x}) (singleton .(inj₁ (inj₁ x))) =
    singleton (inj₁ x)
  ap (assocr₁₂₊⇛ {A} {B} {C} {y}) (singleton .(inj₁ (inj₂ y))) =
    singleton (inj₂ (inj₁ y))
  ap (assocr₂₊⇛ {A} {B} {C} {z}) (singleton .(inj₂ z)) =
    singleton (inj₂ (inj₂ z))
  ap {.(⊤ × A)} {A} {.(tt , x)} {x} unite⋆⇛ (singleton .(tt , x)) =
    singleton x
  ap uniti⋆⇛ (singleton x) = singleton (tt , x)
  ap (swap⋆⇛ {A} {B} {x} {y}) (singleton .(x , y)) = singleton (y , x)
  ap (assocl⋆⇛ {A} {B} {C} {x} {y} {z}) (singleton .(x , (y , z))) =
    singleton ((x , y) , z)
  ap (assocr⋆⇛ {A} {B} {C} {x} {y} {z}) (singleton .((x , y) , z)) =
    singleton (x , (y , z))
  ap (dist₁⇛ {A} {B} {C} {x} {z}) (singleton .(inj₁ x , z)) =
    singleton (inj₁ (x , z))
  ap (dist₂⇛ {A} {B} {C} {y} {z}) (singleton .(inj₂ y , z)) =
    singleton (inj₂ (y , z))
  ap (factor₁⇛ {A} {B} {C} {x} {z}) (singleton .(inj₁ (x , z))) =
    singleton (inj₁ x , z)
  ap (factor₂⇛ {A} {B} {C} {y} {z}) (singleton .(inj₂ (y , z))) =
    singleton (inj₂ y , z)
  ap {.(⊥ × A)} {.⊥} {.(• , x)} {•} (dist0⇛ {A} {.•} {x}) (singleton .(• , x)) =
    singleton •
  ap factor0⇛ (singleton ())
  ap (id⇛ .x) (singleton x) = singleton x
  ap (sym⇛ c) (singleton x) = apI c (singleton x)
  ap (trans⇛ c₁ c₂) (singleton x) = ap c₂ (ap c₁ (singleton x))
  ap (plus₁⇛ {A} {B} {C} {D} {x} {z} c) (singleton .(inj₁ x))
    with ap c (singleton x)
  ... | singleton .z = singleton (inj₁ z)
  ap (plus₂⇛ {A} {B} {C} {D} {y} {w} c) (singleton .(inj₂ y))
    with ap c (singleton y)
  ... | singleton .w = singleton (inj₂ w)
  ap (times⇛ {A} {B} {C} {D} {x} {y} {z} {w} c₁ c₂) (singleton .(x , y))
    with ap c₁ (singleton x) | ap c₂ (singleton y)
  ... | singleton .z | singleton .w = singleton (z , w)

  apI : {A B : Set} {x : A} {y : B} → x ⇛ y → Singleton y → Singleton x
  apI unite₊⇛ (singleton x) = singleton (inj₂ x)
  apI {A} {.(⊥ ⊎ A)} {x} uniti₊⇛ (singleton .(inj₂ x)) = singleton x
  apI (swap₁₊⇛ {A} {B} {x}) (singleton .(inj₂ x)) = singleton (inj₁ x)
  apI (swap₂₊⇛ {A} {B} {y}) (singleton .(inj₁ y)) = singleton (inj₂ y)
  apI (assocl₁₊⇛ {A} {B} {C} {x}) (singleton .(inj₁ (inj₁ x))) =
    singleton (inj₁ x)
  apI (assocl₂₁₊⇛ {A} {B} {C} {y}) (singleton .(inj₁ (inj₂ y))) =
    singleton (inj₂ (inj₁ y))
  apI (assocl₂₂₊⇛ {A} {B} {C} {z}) (singleton .(inj₂ z)) =
    singleton (inj₂ (inj₂ z))
  apI (assocr₁₁₊⇛ {A} {B} {C} {x}) (singleton .(inj₁ x)) =
    singleton (inj₁ (inj₁ x))
  apI (assocr₁₂₊⇛ {A} {B} {C} {y}) (singleton .(inj₂ (inj₁ y))) =
    singleton (inj₁ (inj₂ y))
  apI (assocr₂₊⇛ {A} {B} {C} {z}) (singleton .(inj₂ (inj₂ z))) =
    singleton (inj₂ z)
  apI unite⋆⇛ (singleton x) = singleton (tt , x)
  apI {A} {.(⊤ × A)} {x} uniti⋆⇛ (singleton .(tt , x)) = singleton x
  apI (swap⋆⇛ {A} {B} {x} {y}) (singleton .(y , x)) = singleton (x , y)
  apI (assocl⋆⇛ {A} {B} {C} {x} {y} {z}) (singleton .((x , y) , z)) =
    singleton (x , (y , z))
  apI (assocr⋆⇛ {A} {B} {C} {x} {y} {z}) (singleton .(x , (y , z))) =
    singleton ((x , y) , z)
  apI (dist₁⇛ {A} {B} {C} {x} {z}) (singleton .(inj₁ (x , z))) =
    singleton (inj₁ x , z)
  apI (dist₂⇛ {A} {B} {C} {y} {z}) (singleton .(inj₂ (y , z))) =
    singleton (inj₂ y , z)
  apI (factor₁⇛ {A} {B} {C} {x} {z}) (singleton .(inj₁ x , z)) =
    singleton (inj₁ (x , z))
  apI (factor₂⇛ {A} {B} {C} {y} {z}) (singleton .(inj₂ y , z)) =
    singleton (inj₂ (y , z))
  apI dist0⇛ (singleton ())
  apI {.⊥} {.(⊥ × A)} {•} (factor0⇛ {A} {.•} {x}) (singleton .(• , x)) =
    singleton •
  apI (id⇛ .x) (singleton x) = singleton x
  apI (sym⇛ c) (singleton x) = ap c (singleton x)
  apI {A} {B} {x} {y} (trans⇛ c₁ c₂) (singleton .y) =
    apI c₁ (apI c₂ (singleton y))
  apI (plus₁⇛ {A} {B} {C} {D} {x} {z} c) (singleton .(inj₁ z))
    with apI c (singleton z)
  ... | singleton .x = singleton (inj₁ x)
  apI (plus₂⇛ {A} {B} {C} {D} {y} {w} c) (singleton .(inj₂ w))
    with apI c (singleton w)
  ... | singleton .y = singleton (inj₂ y)
  apI (times⇛ {A} {B} {C} {D} {x} {y} {z} {w} c₁ c₂) (singleton .(z , w))
    with apI c₁ (singleton z) | apI c₂ (singleton w)
  ... | singleton .x | singleton .y = singleton (x , y)

-- Path induction

pathInd :
  (C : (A : Set) → (B : Set) → (x : A) → (y : B) → x ⇛ y → Set) →
  (c : (A : Set) → (x : A) → C A A x x (id⇛ x)) →
  -- add more cases, one for each constructor
  (A : Set) → (B : Set) → (x : A) → (y : B) → (p : x ⇛ y) → C A B x y p
pathInd C c .(⊥ ⊎ B) B .(inj₂ y) y unite₊⇛ = {!!}
pathInd C c A .(⊥ ⊎ A) x .(inj₂ x) uniti₊⇛ = {!!}
pathInd C c .(A ⊎ B) .(B ⊎ A) .(inj₁ x) .(inj₂ x) (swap₁₊⇛ {A} {B} {x}) = {!!}
pathInd C c .(A ⊎ B) .(B ⊎ A) .(inj₂ y) .(inj₁ y) (swap₂₊⇛ {A} {B} {y}) = {!!}
pathInd C c .(A ⊎ B ⊎ C₁) .((A ⊎ B) ⊎ C₁) .(inj₁ x) .(inj₁ (inj₁ x))
  (assocl₁₊⇛ {A} {B} {C₁} {x}) = {!!}
pathInd C c .(A ⊎ B ⊎ C₁) .((A ⊎ B) ⊎ C₁) .(inj₂ (inj₁ y)) .(inj₁ (inj₂ y))
  (assocl₂₁₊⇛ {A} {B} {C₁} {y}) = {!!}
pathInd C c .(A ⊎ B ⊎ C₁) .((A ⊎ B) ⊎ C₁) .(inj₂ (inj₂ z)) .(inj₂ z)
  (assocl₂₂₊⇛ {A} {B} {C₁} {z}) = {!!}
pathInd C c .((A ⊎ B) ⊎ C₁) .(A ⊎ B ⊎ C₁) .(inj₁ (inj₁ x)) .(inj₁ x)
  (assocr₁₁₊⇛ {A} {B} {C₁} {x}) = {!!}
pathInd C c .((A ⊎ B) ⊎ C₁) .(A ⊎ B ⊎ C₁) .(inj₁ (inj₂ y)) .(inj₂ (inj₁ y))
  (assocr₁₂₊⇛ {A} {B} {C₁} {y}) = {!!}
pathInd C c .((A ⊎ B) ⊎ C₁) .(A ⊎ B ⊎ C₁) .(inj₂ z) .(inj₂ (inj₂ z))
  (assocr₂₊⇛ {A} {B} {C₁} {z}) = {!!}
pathInd C c .(Σ ⊤ (λ x₁ → B)) B .(tt , y) y unite⋆⇛ = {!!}
pathInd C c A .(Σ ⊤ (λ x₁ → A)) x .(tt , x) uniti⋆⇛ = {!!}
pathInd C c .(Σ A (λ x₁ → B)) .(Σ B (λ x₁ → A)) .(x , y) .(y , x)
  (swap⋆⇛ {A} {B} {x} {y}) = {!!}
pathInd C c .(Σ A (λ x₁ → Σ B (λ x₂ → C₁))) .(Σ (Σ A (λ x₁ → B)) (λ x₁ → C₁))
  .(x , y , z) .((x , y) , z) (assocl⋆⇛ {A} {B} {C₁} {x} {y} {z}) = {!!}
pathInd C c .(Σ (Σ A (λ x₁ → B)) (λ x₁ → C₁)) .(Σ A (λ x₁ → Σ B (λ x₂ → C₁)))
  .((x , y) , z) .(x , y , z) (assocr⋆⇛ {A} {B} {C₁} {x} {y} {z}) = {!!}
pathInd C c .(Σ (A ⊎ B) (λ x₁ → C₁)) .(Σ A (λ x₁ → C₁) ⊎ Σ B (λ x₁ → C₁))
  .(inj₁ x , z) .(inj₁ (x , z)) (dist₁⇛ {A} {B} {C₁} {x} {z}) = {!!}
pathInd C c .(Σ (A ⊎ B) (λ x₁ → C₁)) .(Σ A (λ x₁ → C₁) ⊎ Σ B (λ x₁ → C₁))
  .(inj₂ y , z) .(inj₂ (y , z)) (dist₂⇛ {A} {B} {C₁} {y} {z}) = {!!}
pathInd C c .(Σ A (λ x₁ → C₁) ⊎ Σ B (λ x₁ → C₁)) .(Σ (A ⊎ B) (λ x₁ → C₁))
  .(inj₁ (x , z)) .(inj₁ x , z) (factor₁⇛ {A} {B} {C₁} {x} {z}) = {!!}
pathInd C c .(Σ A (λ x₁ → C₁) ⊎ Σ B (λ x₁ → C₁)) .(Σ (A ⊎ B) (λ x₁ → C₁))
  .(inj₂ (y , z)) .(inj₂ y , z) (factor₂⇛ {A} {B} {C₁} {y} {z}) = {!!}
pathInd C c .(Σ ⊥ (λ x₁ → A)) .⊥ .(y , x) y (dist0⇛ {A} {.y} {x}) = {!!}
pathInd C c .⊥ .(Σ ⊥ (λ x₁ → A)) x .(x , x₁) (factor0⇛ {A} {.x} {x₁}) = {!!}
pathInd C c A .A x .x (id⇛ .x) = c A x
pathInd C c A B x y (sym⇛ p) = {!!}
pathInd C c A B x y (trans⇛ p p₁) = {!!}
pathInd C c .(A ⊎ B) .(C₁ ⊎ D) .(inj₁ x) .(inj₁ z)
  (plus₁⇛ {A} {B} {C₁} {D} {x} {z} p) = {!!}
pathInd C c .(A ⊎ B) .(C₁ ⊎ D) .(inj₂ y) .(inj₂ w)
  (plus₂⇛ {A} {B} {C₁} {D} {y} {w} p) = {!!}
pathInd C c .(Σ A (λ x₁ → B)) .(Σ C₁ (λ x₁ → D)) .(x , y) .(z , w)
  (times⇛ {A} {B} {C₁} {D} {x} {y} {z} {w} p p₁) = {!!}

------------------------------------------------------------------------------
-- Now interpret a path (x ⇛ y) as a value of type (1/x , y)

Recip : {A : Set} → (base : A) → (x : A) → Set₁
Recip {A} base = λ x → (x ⇛ base)

η : {A : Set} {base : A} → ⊤ → Recip base × Singleton base
η {A} {base} tt = (λ x → ? , singleton base)

{--
If A={x0,x1,x2}, 1/A has three values:
(x0<-x0, x0<-x1, x0<-x2)

η : {A : Set} {x : A} → ⊤ → Recip x × Singleton x
η {A} {x} tt = (id⇛ x , singleton x)

ε : {A : Set} {x : A} → Recip x × Singleton x → ⊤
ε {A} {x} (rx , singleton .x) = tt -- makes no sense

apr : {A B : Set} {x : A} {y : B} → (x ⇛ y) → Recip y → Recip x
apr {A} {B} {x} {y} p ry =
  x
    ≡⟨ p ⟩
  y
    ≡⟨ ry ⟩
  y
    ≡⟨ sym⇛ p ⟩
  x ∎

ε : {A B : Set} {x : A} {y : B} → Recip x → Singleton y → x ⇛ y
ε rx (singleton y) = rx y

pathV : {A B : Set} {x : A} {y : B} → (x ⇛ y) → Recip x × Singleton y
pathV unite₊⇛ = {!!}
pathV uniti₊⇛ = {!!}
--  swap₁₊⇛ : {A B : Set} {x : A} → _⇛_ {A ⊎ B} {B ⊎ A} (inj₁ x) (inj₂ x)
pathV (swap₁₊⇛ {A} {B} {x}) = ((λ x' → {!!}) , singleton (inj₂ x))
pathV swap₂₊⇛ = {!!}
pathV assocl₁₊⇛ = {!!}
pathV assocl₂₁₊⇛ = {!!}
pathV assocl₂₂₊⇛ = {!!}
pathV assocr₁₁₊⇛ = {!!}
pathV assocr₁₂₊⇛ = {!!}
pathV assocr₂₊⇛ = {!!}
pathV unite⋆⇛ = {!!}
pathV uniti⋆⇛ = {!!}
pathV swap⋆⇛ = {!!}
pathV assocl⋆⇛ = {!!}
pathV assocr⋆⇛ = {!!}
pathV dist₁⇛ = {!!}
pathV dist₂⇛ = {!!}
pathV factor₁⇛ = {!!}
pathV factor₂⇛ = {!!}
pathV dist0⇛ = {!!}
pathV factor0⇛ = {!!}
pathV {A} {.A} {x} (id⇛ .x) = {!!}
pathV (sym⇛ p) = {!!}
pathV (trans⇛ p p₁) = {!!}
pathV (plus₁⇛ p) = {!!}
pathV (plus₂⇛ p) = {!!}
pathV (times⇛ p p₁) = {!!}

data _⇛_ : {A B : Set} → (x : A) → (y : B) → Set₁ where
------------------------------------------------------------------------------
-- pi types with exactly one level of reciprocals
-- interpretation of B1 types as 1-groupoids

data B0 : Set where
  ZERO : B0
  ONE : B0
  PLUS0 : B0 → B0 → B0
  TIMES0 : B0 → B0 → B0

⟦_⟧₀ : B0 → Set
⟦ ZERO ⟧₀ = ⊥
⟦ ONE ⟧₀ = ⊤
⟦ PLUS0 b₁ b₂ ⟧₀ = ⟦ b₁ ⟧₀ ⊎ ⟦ b₂ ⟧₀
⟦ TIMES0 b₁ b₂ ⟧₀ = ⟦ b₁ ⟧₀ × ⟦ b₂ ⟧₀

data B1 : Set where
  LIFT0  : B0 → B1
  PLUS1  : B1 → B1 → B1
  TIMES1 : B1 → B1 → B1
  RECIP1 : B0 → B1

open 1Groupoid

⟦_⟧₁ : B1 → 1Groupoid
⟦ LIFT0 b0 ⟧₁ = discrete ⟦ b0 ⟧₀
⟦ PLUS1 b₁ b₂ ⟧₁ = ⟦ b₁ ⟧₁ ⊎G ⟦ b₂ ⟧₁
⟦ TIMES1 b₁ b₂ ⟧₁ =  ⟦ b₁ ⟧₁ ×G ⟦ b₂ ⟧₁
⟦ RECIP1 b0 ⟧₁ = {!!} -- allPaths (ı₀ b0)

ı₁ : B1 → Set
ı₁ b = set ⟦ b ⟧₁

test10 = ⟦ LIFT0 ONE ⟧₁
test11 = ⟦ LIFT0 (PLUS0 ONE ONE) ⟧₁
test12 = ⟦ RECIP1 (PLUS0 ONE ONE) ⟧₁

-- interpret isos as functors

data _⟷₁_ : B1 → B1 → Set where
  -- +
  swap₊   : { b₁ b₂ : B1 } → PLUS1 b₁ b₂ ⟷₁ PLUS1 b₂ b₁
  assocl₊ : { b₁ b₂ b₃ : B1 } → PLUS b₁ (PLUS b₂ b₃) ⟷₁ PLUS (PLUS b₁ b₂) b₃
  assocr₊ : { b₁ b₂ b₃ : B1 } → PLUS (PLUS b₁ b₂) b₃ ⟷₁ PLUS b₁ (PLUS b₂ b₃)
  -- *
  unite⋆  : { b : B1 } → TIMES1 (LIFT0 ONE) b ⟷₁ b
  uniti⋆  : { b : B1 } → b ⟷₁ TIMES1 (LIFT0 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₃)
  -- * distributes over +
  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₃
  -- congruence
  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₄)
  η⋆ : (b : B0) → LIFT0 ONE ⟷₁ TIMES1 (LIFT0 b) (RECIP1 b)
  ε⋆ : (b : B0) → TIMES1 (LIFT0 b) (RECIP1 b) ⟷₁ LIFT0 ONE

record 1-functor (A B : 1Groupoid) : Set where
  constructor 1F
  private module A = 1Groupoid A
  private module B = 1Groupoid B

  field
    F₀ : set A → set B
    F₁ : ∀ {X Y : set A} → A [ X , Y ] → B [ F₀ X , F₀ Y ]
    -- identity : ∀ {X} → B._≈_ (F₁ (A.id {X})) B.id
    -- F-resp-≈ : ∀ {X Y} {F G : A [ X , Y ]} → A._≈_ F G → B._≈_ (F₁ F) (F₁ G)

open 1-functor public

ipath : (b : B1) → ı₁ b → ı₁ b → Set
ipath b x y = Path {ı₁ b} x y

swap⊎ : {A B : Set} → A ⊎ B → B ⊎ A
swap⊎ (inj₁ a) = inj₂ a
swap⊎ (inj₂ b) = inj₁ b

intro1⋆ : {b : B1} {x y : ı₁ b} → ipath b x y → ipath (TIMES1 (LIFT0 ONE) b) (tt , x) (tt , y)
intro1⋆ (y ⇛ z) = (tt , y) ⇛ (tt , z)

objη⋆ : (b : B0) → ı₁ (LIFT0 ONE) → ı₁ (TIMES1 (LIFT0 b) (RECIP1 b))
objη⋆ b tt = point b , point b

objε⋆ : (b : B0) → ı₁ (TIMES1 (LIFT0 b) (RECIP1 b)) → ı₁ (LIFT0 ONE)
objε⋆ b (x , y) = tt

elim1∣₁ : (b : B1) → ı₁ (TIMES1 (LIFT0 ONE) b) → ı₁ b
elim1∣₁ b (tt , x) = x

intro1∣₁ : (b : B1) → ı₁ b → ı₁ (TIMES1 (LIFT0 ONE) b)
intro1∣₁ b x = (tt , x)

swapF : {b₁ b₂ : B1} →
      let G = ⟦ b₁ ⟧₁ ⊎G ⟦ b₂ ⟧₁
          G' = ⟦ b₂ ⟧₁ ⊎G ⟦ b₁ ⟧₁ in
      {X Y : set G} → G [ X , Y ] → G' [ swap⊎ X , swap⊎ Y ]
swapF {X = inj₁ _} {inj₁ _} f = f
swapF {X = inj₁ _} {inj₂ _} ()
swapF {X = inj₂ _} {inj₁ _} ()
swapF {X = inj₂ _} {inj₂ _} f = f

eta : (b : B0) → List (ipath (LIFT0 ONE)) → List (ipath (TIMES1 (LIFT0 b) (RECIP1 b)))
-- note how the input list is not used at all!
eta b _ = prod (λ a a' → _↝_ (a , tt) (a' , tt)) (elems0 b) (elems0 b)

eps : (b : B0) → ipath (TIMES1 (LIFT0 b) (RECIP1 b)) → ipath (LIFT0 ONE)
eps b0 (a ⇛ b) = tt ⇛ tt

Funite⋆ : {b₁ : B1} → ∀ {X Y : set (discrete (ı₀ ONE) ×G ⟦ b₁ ⟧₁)} →  DPath (proj₁ X) (proj₁ Y) ×  (_↝_ ⟦ b₁ ⟧₁) (proj₂ X) (proj₂ Y) →  _↝_ ⟦ b₁ ⟧₁ (proj₂ X) (proj₂ Y)
Funite⋆ {b₁} {tt , _} {tt , _} (reflD , y) = y

Funiti⋆ : {b₁ : B1} → ∀ {X Y : set (discrete (ı₀ ONE) ×G ⟦ b₁ ⟧₁)} →  _↝_ ⟦ b₁ ⟧₁ (proj₂ X) (proj₂ Y) → DPath (proj₁ X) (proj₁ Y) ×  (_↝_ ⟦ b₁ ⟧₁) (proj₂ X) (proj₂ Y)
Funiti⋆ y = reflD , y

mutual
  eval : {b₁ b₂ : B1} → (b₁ ⟷₁ b₂) → 1-functor ⟦ b₁ ⟧₁ ⟦ b₂ ⟧₁
  eval (swap₊ {b₁} {b₂}) = 1F swap⊎ (λ {X Y} → swapF {b₁} {b₂} {X} {Y})
  eval (unite⋆ {b}) = 1F (elim1∣₁ b) (Funite⋆ {b})
  eval (uniti⋆ {b}) = 1F (intro1∣₁ b) (Funiti⋆ {b})
--  eval (η⋆ b) = F₁ (objη⋆ b) (eta b )
--  eval (ε⋆ b) = F₁ (objε⋆ b) (map (eps b))

  evalB : {b₁ b₂ : B1} → (b₁ ⟷₁ b₂) → 1-functor ⟦ b₂ ⟧₁ ⟦ b₁ ⟧₁
  evalB (swap₊ {b₁} {b₂}) = 1F swap⊎ ((λ {X Y} → swapF {b₂} {b₁} {X} {Y}))
  evalB (unite⋆ {b}) = 1F (intro1∣₁ b) (Funiti⋆ {b})
  evalB (uniti⋆ {b}) = 1F (elim1∣₁ b) (Funite⋆ {b})
--  evalB (η⋆ b) = F₁ (objε⋆ b) (map (eps b))
--  evalB (ε⋆ b) = F₁ (objη⋆ b) (eta b)

eval assocl₊ = ? -- : { b₁ b₂ b₃ : B } → PLUS b₁ (PLUS b₂ b₃) ⟷₁ PLUS (PLUS b₁ b₂) b₃
eval assocr₊ = ? -- : { b₁ b₂ b₃ : B } → PLUS (PLUS b₁ b₂) b₃ ⟷₁ PLUS b₁ (PLUS b₂ b₃)
eval uniti⋆ = ? -- : { b : B } → b ⟷₁ TIMES ONE b
eval swap⋆ = ? --  : { b₁ b₂ : B } → TIMES b₁ b₂ ⟷₁ TIMES b₂ b₁
eval assocl⋆ = ? -- : { b₁ b₂ b₃ : B } → TIMES b₁ (TIMES b₂ b₃) ⟷₁ TIMES (TIMES b₁ b₂) b₃
eval assocr⋆ = ? -- : { b₁ b₂ b₃ : B } → TIMES (TIMES b₁ b₂) b₃ ⟷₁ TIMES b₁ (TIMES b₂ b₃)
eval dist = ? -- : { b₁ b₂ b₃ : B } → TIMES (PLUS b₁ b₂) b₃ ⟷₁ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
eval factor = ? -- : { b₁ b₂ b₃ : B } → PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⟷₁ TIMES (PLUS b₁ b₂) b₃
eval id⟷₁ = ? --  : { b : B } → b ⟷₁ b
eval (sym c) = ? -- : { b₁ b₂ : B } → (b₁ ⟷₁ b₂) → (b₂ ⟷₁ b₁)
eval (c₁ ∘ c₂) = ? -- : { b₁ b₂ b₃ : B } → (b₁ ⟷₁ b₂) → (b₂ ⟷₁ b₃) → (b₁ ⟷₁ b₃)
eval (c₁ ⊕ c₂) = ? -- : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟷₁ b₃) → (b₂ ⟷₁ b₄) → (PLUS b₁ b₂ ⟷₁ PLUS b₃ b₄)
eval (c₁ ⊗ c₂) = ? -- : { b₁ b₂ b₃ b₄ : B } → (b₁ ⟷₁ b₃) → (b₂ ⟷₁ b₄) → (TIMES b₁ b₂ ⟷₁ TIMES b₃ b₄)

-- lid⇛ : {A B : Set} {x : A} {y : B} → (trans⇛ (id⇛ x) (x ⇛ y)) ⇛ (x ⇛ y)
-- lid⇛ {A} {B} {x} {y} =
--  pathInd ?

ap : {A B : Set} → (f : A → B) → {a a' : A} → Path a a' → Path (f a) (f a')
ap f (a ⇛ a') = (f a) ⇛ (f a')

_∙⇛_ : {A : Set} {a b c : A} → Path b c → Path a b → Path a c
(b ⇛ c) ∙⇛ (a ⇛ .b) = a ⇛ c

_⇚ : {A : Set} {a b : A} → Path a b → Path b a
(x ⇛ y) ⇚ = y ⇛ x

lid⇛ : {A : Set} {x y : A} (α : Path x y) → (id⇛ y ∙⇛ α) ≣⇛ α
lid⇛ (x ⇛ y) = refl⇛

rid⇛ : {A : Set} {x y : A} (α : Path x y) → (α ∙⇛ id⇛ x) ≣⇛ α
rid⇛ (x ⇛ y) = refl⇛

assoc⇛ : {A : Set} {w x y z : A} (α : Path y z) (β : Path x y) (δ : Path w x) → ((α ∙⇛ β) ∙⇛ δ) ≣⇛ (α ∙⇛ (β ∙⇛ δ))
assoc⇛ (y ⇛ z) (x ⇛ .y) (w ⇛ .x) = refl⇛

l⇚ : {A : Set}  {x y : A} (α : Path x y) → ((α ⇚) ∙⇛ α) ≣⇛ id⇛ x
l⇚ (x ⇛ y) = refl⇛

r⇚ : {A : Set} {x y : A} (α : Path x y) → (α ∙⇛ (α ⇚)) ≣⇛ id⇛ y
r⇚ (x ⇛ y) = refl⇛

sym⇛ : {A : Set} {x y : A} {α β : Path x y} → α ≣⇛ β → β ≣⇛ α
sym⇛ refl⇛ = refl⇛

trans⇛ : {A : Set} {x y : A} {α β δ : Path x y} → α ≣⇛ β → β ≣⇛ δ → α ≣⇛ δ
trans⇛ refl⇛ refl⇛ = refl⇛

equiv≣⇛ : {A : Set} {x y : A} → IsEquivalence {_} {_} {Path x y} (_≣⇛_)
equiv≣⇛ = record { refl = refl⇛; sym = sym⇛; trans = trans⇛ }

resp≣⇛ : {A : Set} {x y z : A} {f h : Path y z} {g i : Path x y} →
  f ≣⇛ h → g ≣⇛ i → (f ∙⇛ g) ≣⇛ (h ∙⇛ i)
resp≣⇛ refl⇛ refl⇛ = refl⇛

record 0-type : Set₁ where
  constructor G₀
  field
    ∣_∣₀ : Set

open 0-type public

plus : 0-type → 0-type → 0-type
plus t₁ t₂ = G₀ (∣ t₁ ∣₀ ⊎ ∣ t₂ ∣₀)

times : 0-type → 0-type → 0-type
times t₁ t₂ = G₀ (∣ t₁ ∣₀ × ∣ t₂ ∣₀)

⟦_⟧₀ : B0 → 0-type
⟦ ONE ⟧₀ = G₀ ⊤
⟦ PLUS0 b₁ b₂ ⟧₀ = plus ⟦ b₁ ⟧₀ ⟦ b₂ ⟧₀
⟦ TIMES0 b₁ b₂ ⟧₀ = times ⟦ b₁ ⟧₀ ⟦ b₂ ⟧₀

ı₀ : B0 → Set
ı₀ b = ∣ ⟦ b ⟧₀ ∣₀

point : (b : B0) → ı₀ b
point ONE = tt
point (PLUS0 b _) = inj₁ (point b)
point (TIMES0 b₀ b₁) = point b₀ , point b₁

allPaths : Set → 1Groupoid
allPaths a =  record
    { set = a
    ; _↝_ = Path
    ; _≈_ = _≣⇛_
    ; id = λ {x} → id⇛ x
    ; _∘_ = _∙⇛_
    ; _⁻¹ = _⇚
    ; lneutr = lid⇛
    ; rneutr = rid⇛
    ; assoc = assoc⇛
    ; linv = l⇚
    ; rinv = r⇚
    ; equiv = equiv≣⇛
    ;  ∘-resp-≈ = resp≣⇛}

--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
open import ExtractSac as ES using ()
open import Extract (ES.kompile-fun)

open import Data.Nat
open import Data.Nat.Properties
open import Data.List as L using (List; []; _∷_)
open import Data.Vec as V using (Vec; []; _∷_)
open import Data.Fin using (Fin; zero; suc; #_)

open import Relation.Binary.PropositionalEquality

open import Reflection

open import Structures
open import Function

test-13f : ∀ {n} → Vec ℕ n → Vec ℕ (n + n * n) → ℕ
test-13f [] _      = 0
test-13f (x ∷ a) b = x
test₁₃ : kompile test-13f [] [] ≡ ok _
test₁₃ = refl

test-14f : ∀ {n} → Vec ℕ n → Vec ℕ (n) → Vec ℕ n
test-14f [] _ = []
test-14f (x ∷ a) (y ∷ b) = x + y ∷ test-14f a b
test₁₄ : kompile test-14f [] [] ≡ ok _
test₁₄ = refl

-- Note that rewrite helper function would generate
-- the equality type amongst its arguments.
test-15f : ∀ {a b} → Fin (a + b) → Fin (b + a)
test-15f {a}{b} x rewrite (+-comm a b) = x

test₁₅ : let fs = L.[ quote +-comm ] in
         kompile test-15f fs fs  ≡ ok _
test₁₅ = refl

module absurd-patterns where
  test-16f : ∀ {n} → Fin n → Fin n
  test-16f {0}     ()
  test-16f {suc n} i  = i

  test₁₆ : kompile test-16f [] []  ≡ ok _
  test₁₆ = refl

  -- Ugh, when we found an absurd pattern, the rest of the
  -- patterns may or may not be present (which seem to make no sense).
  -- If they are present, then other (missing) constructors are inserted
  -- automatically.  Therefore, extracted code for the function below
  -- would look rather scary.
  test-17f : ∀ {n} → Fin (n ∸ 1) → ℕ → ℕ → Fin n
  test-17f {0}       () (suc (suc k))
  test-17f {1}       ()
  test-17f {suc (suc n)} i m mm = zero

  test₁₇ : kompile test-17f [] []  ≡ ok _
  test₁₇ = refl

-- Dot patterns
test-18f : ∀ m n → m ≡ n → Fin (suc m)
test-18f zero    .zero    refl = zero
test-18f (suc m) .(suc m) refl = suc (test-18f m m refl)

test₁₈ : kompile test-18f [] []  ≡ ok _
test₁₈ = refl

-- Increment the first column of the 2-d array expressed in vectors
test-19f : ∀ {m n} → Vec (Vec ℕ n) m → Vec (Vec ℕ n) m
test-19f []               = []
test-19f ([] ∷ xss)       = [] ∷ test-19f xss
test-19f ((x ∷ xs) ∷ xss) = (x + 1 ∷ xs) ∷ test-19f xss

test₁₉ : kompile test-19f [] []  ≡ ok _
test₁₉ = refl

max_stars_repo_name: ashinkarov/agda-extractor

max_issues_repo_name: ashinkarov/agda-extractor

max_forks_repo_name: ashinkarov/agda-extractor


text:
{-# OPTIONS --without-K #-}
-- Specific constructions on top of summation functions

module Explore.Summable where

open import Type
open import Function.NP
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_ ; _≗_ ; _≗₂_)
open import Explore.Core
open import Explore.Properties
open import Explore.Product
open import Data.Product
open import Data.Nat.NP
open import Data.Nat.Properties
open import Data.Two
open Data.Two.Indexed

module FromSum {a} {A : ★_ a} (sum : Sum A) where
  Card : ℕ
  Card = sum (const 1)

  count : Count A
  count f = sum (𝟚▹ℕ ∘ f)

  sum-lin⇒sum-zero : SumLin sum → SumZero sum
  sum-lin⇒sum-zero sum-lin = sum-lin (λ _ → 0) 0

  sum-mono⇒sum-ext : SumMono sum → SumExt sum
  sum-mono⇒sum-ext sum-mono f≗g = ℕ≤.antisym (sum-mono (ℕ≤.reflexive ∘ f≗g)) (sum-mono (ℕ≤.reflexive ∘ ≡.sym ∘ f≗g))

  sum-ext+sum-hom⇒sum-mono : SumExt sum → SumHom sum → SumMono sum
  sum-ext+sum-hom⇒sum-mono sum-ext sum-hom {f} {g} f≤°g =
      sum f                         ≤⟨ m≤m+n _ _ ⟩
      sum f + sum (λ x → g x ∸ f x) ≡⟨ ≡.sym (sum-hom _ _) ⟩
      sum (λ x → f x + (g x ∸ f x)) ≡⟨ sum-ext (m+n∸m≡n ∘ f≤°g) ⟩
      sum g ∎ where open ≤-Reasoning

module FromSumInd {a} {A : ★_ a}
                  {sum : Sum A}
                  (sum-ind : SumInd sum) where
  open FromSum sum public

  sum-ext : SumExt sum
  sum-ext = sum-ind (λ s → s _ ≡ s _) ≡.refl (≡.ap₂ _+_)

  sum-zero : SumZero sum
  sum-zero = sum-ind (λ s → s (const 0) ≡ 0) ≡.refl (≡.ap₂ _+_) (λ _ → ≡.refl)

  sum-hom : SumHom sum
  sum-hom f g = sum-ind (λ s → s (f +° g) ≡ s f + s g)
                        ≡.refl
                        (λ {s₀} {s₁} p₀ p₁ → ≡.trans (≡.ap₂ _+_ p₀ p₁) (+-interchange (s₀ _) (s₀ _) _ _))
                        (λ _ → ≡.refl)

  sum-mono : SumMono sum
  sum-mono = sum-ind (λ s → s _ ≤ s _) z≤n _+-mono_

  sum-lin : SumLin sum
  sum-lin f zero    = sum-zero
  sum-lin f (suc k) = ≡.trans (sum-hom f (λ x → k * f x)) (≡.ap₂ _+_ (≡.refl {x = sum f}) (sum-lin f k))

  module _ (f g : A → ℕ) where
    open ≡.≡-Reasoning

    sum-⊓-∸ : sum f ≡ sum (f ⊓° g) + sum (f ∸° g)
    sum-⊓-∸ = sum f                          ≡⟨ sum-ext (f ⟨ a≡a⊓b+a∸b ⟩° g) ⟩
              sum ((f ⊓° g) +° (f ∸° g))     ≡⟨ sum-hom (f ⊓° g) (f ∸° g) ⟩
              sum (f ⊓° g) + sum (f ∸° g) ∎

    sum-⊔-⊓ : sum f + sum g ≡ sum (f ⊔° g) + sum (f ⊓° g)
    sum-⊔-⊓ = sum f + sum g               ≡⟨ ≡.sym (sum-hom f g) ⟩
              sum (f +° g)                ≡⟨ sum-ext (f ⟨ a+b≡a⊔b+a⊓b ⟩° g) ⟩
              sum (f ⊔° g +° f ⊓° g)      ≡⟨ sum-hom (f ⊔° g) (f ⊓° g) ⟩
              sum (f ⊔° g) + sum (f ⊓° g) ∎

    sum-⊔ : sum (f ⊔° g) ≤ sum f + sum g
    sum-⊔ = ℕ≤.trans (sum-mono (f ⟨ ⊔≤+ ⟩° g)) (ℕ≤.reflexive (sum-hom f g))

  count-ext : CountExt count
  count-ext f≗g = sum-ext (≡.cong 𝟚▹ℕ ∘ f≗g)

  sum-const : ∀ k → sum (const k) ≡ Card * k
  sum-const k
      rewrite ℕ°.*-comm Card k
            | ≡.sym (sum-lin (const 1) k)
            | proj₂ ℕ°.*-identity k = ≡.refl

  module _ f g where
    count-∧-not : count f ≡ count (f ∧° g) + count (f ∧° not° g)
    count-∧-not rewrite sum-⊓-∸ (𝟚▹ℕ ∘ f) (𝟚▹ℕ ∘ g)
                      | sum-ext (f ⟨ 𝟚▹ℕ-⊓ ⟩° g)
                      | sum-ext (f ⟨ 𝟚▹ℕ-∸ ⟩° g)
                      = ≡.refl

    count-∨-∧ : count f + count g ≡ count (f ∨° g) + count (f ∧° g)
    count-∨-∧ rewrite sum-⊔-⊓ (𝟚▹ℕ ∘ f) (𝟚▹ℕ ∘ g)
                    | sum-ext (f ⟨ 𝟚▹ℕ-⊔ ⟩° g)
                    | sum-ext (f ⟨ 𝟚▹ℕ-⊓ ⟩° g)
                    = ≡.refl

    count-∨≤+ : count (f ∨° g) ≤ count f + count g
    count-∨≤+ = ℕ≤.trans (ℕ≤.reflexive (sum-ext (≡.sym ∘ (f ⟨ 𝟚▹ℕ-⊔ ⟩° g))))
                         (sum-⊔ (𝟚▹ℕ ∘ f) (𝟚▹ℕ ∘ g))

module FromSum×
         {a} {A : Set a}
         {b} {B : Set b}
         {sumᴬ     : Sum A}
         (sum-indᴬ : SumInd sumᴬ)
         {sumᴮ     : Sum B}
         (sum-indᴮ : SumInd sumᴮ) where

  module |A| = FromSumInd sum-indᴬ
  module |B| = FromSumInd sum-indᴮ
  open Operators

  sumᴬᴮ = sumᴬ ×ˢ sumᴮ

  sum-∘proj₁≡Card* : ∀ f → sumᴬᴮ (f ∘ proj₁) ≡ |B|.Card * sumᴬ f
  sum-∘proj₁≡Card* f
      rewrite |A|.sum-ext (|B|.sum-const ∘ f)
            = |A|.sum-lin f |B|.Card

  sum-∘proj₂≡Card* : ∀ f → sumᴬᴮ (f ∘ proj₂) ≡ |A|.Card * sumᴮ f
  sum-∘proj₂≡Card* = |A|.sum-const ∘ sumᴮ

  sum-∘proj₁ : ∀ {f} {g} → sumᴬ f ≡ sumᴬ g → sumᴬᴮ (f ∘ proj₁) ≡ sumᴬᴮ (g ∘ proj₁)
  sum-∘proj₁ {f} {g} sumf≡sumg
      rewrite sum-∘proj₁≡Card* f
            | sum-∘proj₁≡Card* g
            | sumf≡sumg = ≡.refl

  sum-∘proj₂ : ∀ {f} {g} → sumᴮ f ≡ sumᴮ g → sumᴬᴮ (f ∘ proj₂) ≡ sumᴬᴮ (g ∘ proj₂)
  sum-∘proj₂ sumf≡sumg = |A|.sum-ext (const sumf≡sumg)

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

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The lifting of a non-strict order to incorporate new extrema
------------------------------------------------------------------------

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

-- This module is designed to be used with
-- Relation.Nullary.Construct.Add.Extrema

open import Relation.Binary

module Relation.Binary.Construct.Add.Extrema.NonStrict
  {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) where

open import Function
open import Relation.Nullary.Construct.Add.Extrema
import Relation.Nullary.Construct.Add.Infimum as I
import Relation.Binary.Construct.Add.Infimum.NonStrict as AddInfimum
import Relation.Binary.Construct.Add.Supremum.NonStrict as AddSupremum
import Relation.Binary.Construct.Add.Extrema.Equality as Equality

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

private
  module Inf = AddInfimum _≤_
  module Sup = AddSupremum Inf._≤₋_

open Sup using () renaming (_≤⁺_ to _≤±_) public

-------------------------------------------------------------------------
-- Useful pattern synonyms

pattern ⊥±≤⊥±    = Sup.[ Inf.⊥₋≤ I.⊥₋ ]
pattern ⊥±≤[_] l = Sup.[ Inf.⊥₋≤ I.[ l ] ]
pattern [_] p    = Sup.[ Inf.[ p ] ]
pattern ⊥±≤⊤±    = ⊥±    Sup.≤⊤⁺
pattern [_]≤⊤± k = [ k ] Sup.≤⊤⁺
pattern ⊤±≤⊤±    = ⊤±    Sup.≤⊤⁺

⊥±≤_ : ∀ k → ⊥± ≤± k
⊥±≤ ⊥±    = ⊥±≤⊥±
⊥±≤ [ k ] = ⊥±≤[ k ]
⊥±≤ ⊤±    = ⊥±≤⊤±

_≤⊤± : ∀ k → k ≤± ⊤±
⊥±    ≤⊤± = ⊥±≤⊤±
[ k ] ≤⊤± = [ k ]≤⊤±
⊤±    ≤⊤± = ⊤±≤⊤±

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

[≤]-injective : ∀ {k l} → [ k ] ≤± [ l ] → k ≤ l
[≤]-injective = Inf.[≤]-injective ∘′ Sup.[≤]-injective

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  ≤±-reflexive : (_≈_ ⇒ _≤_) → (_≈±_ ⇒ _≤±_)
  ≤±-reflexive = Sup.≤⁺-reflexive ∘′ Inf.≤₋-reflexive

  ≤±-antisym : Antisymmetric _≈_ _≤_ → Antisymmetric _≈±_ _≤±_
  ≤±-antisym = Sup.≤⁺-antisym ∘′ Inf.≤₋-antisym

≤±-trans : Transitive _≤_ → Transitive _≤±_
≤±-trans = Sup.≤⁺-trans ∘′ Inf.≤₋-trans

≤±-minimum : Minimum _≤±_ ⊥±
≤±-minimum = ⊥±≤_

≤±-maximum : Maximum _≤±_ ⊤±
≤±-maximum = _≤⊤±

≤±-dec : Decidable _≤_ → Decidable _≤±_
≤±-dec = Sup.≤⁺-dec ∘′ Inf.≤₋-dec

≤±-total : Total _≤_ → Total _≤±_
≤±-total = Sup.≤⁺-total ∘′ Inf.≤₋-total

≤±-irrelevant : Irrelevant _≤_ → Irrelevant _≤±_
≤±-irrelevant = Sup.≤⁺-irrelevant ∘′ Inf.≤₋-irrelevant

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

module _ {e} {_≈_ : Rel A e} where

  open Equality _≈_

  ≤±-isPreorder : IsPreorder _≈_ _≤_ → IsPreorder _≈±_ _≤±_
  ≤±-isPreorder = Sup.≤⁺-isPreorder ∘′ Inf.≤₋-isPreorder

  ≤±-isPartialOrder : IsPartialOrder _≈_ _≤_ → IsPartialOrder _≈±_ _≤±_
  ≤±-isPartialOrder = Sup.≤⁺-isPartialOrder ∘′ Inf.≤₋-isPartialOrder

  ≤±-isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ → IsDecPartialOrder _≈±_ _≤±_
  ≤±-isDecPartialOrder = Sup.≤⁺-isDecPartialOrder ∘′ Inf.≤₋-isDecPartialOrder

  ≤±-isTotalOrder : IsTotalOrder _≈_ _≤_ → IsTotalOrder _≈±_ _≤±_
  ≤±-isTotalOrder = Sup.≤⁺-isTotalOrder ∘′ Inf.≤₋-isTotalOrder

  ≤±-isDecTotalOrder : IsDecTotalOrder _≈_ _≤_ → IsDecTotalOrder _≈±_ _≤±_
  ≤±-isDecTotalOrder = Sup.≤⁺-isDecTotalOrder ∘′ Inf.≤₋-isDecTotalOrder


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

open import Categories.Category

module Categories.Functor.Construction.SubCategory.Properties {o ℓ e} (C : Category o ℓ e) where

open Category C
open Equiv

open import Level
open import Function.Base       using () renaming (id to id→)
open import Function.Surjection using (Surjection) renaming (id to id↠)

open import Categories.Category.SubCategory C
open import Categories.Functor.Construction.SubCategory C
open import Categories.Functor.Properties

private
  variable
    ℓ′ i : Level
    I : Set i
    U : I → Obj

SubFaithful : ∀ (sub : SubCat {i} {ℓ′} I) → Faithful (Sub sub)
SubFaithful _ _ _ = id→

FullSubFaithful : Faithful (FullSub {U = U})
FullSubFaithful _ _ = id→

FullSubFull : Full (FullSub {U = U})
FullSubFull = Surjection.surjective id↠

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:
-- The simpler case of index inductive definitions. (no induction-recursion)
module IID where

open import LF

-- A code for an IID
-- I - index set
-- E = I for general IIDs
-- E = One for restricted IIDs
data OP (I : Set)(E : Set) : Set1 where
  ι : E -> OP I E
  σ : (A : Set)(γ : A -> OP I E) -> OP I E
  δ : (A : Set)(i : A -> I)(γ : OP I E) -> OP I E

-- The type of constructor arguments. Parameterised over
--  U - the inductive type
-- This is the F of the simple polynomial type μF
Args : {I : Set}{E : Set} -> OP I E ->
     (U : I -> Set) -> Set
Args (ι e)     U = One
Args (σ A γ)   U = A × \a -> Args (γ a) U
Args (δ A i γ) U = ((a : A) -> U (i a)) × \_ -> Args γ U

-- Computing the index
index : {I : Set}{E : Set}(γ : OP I E)(U : I -> Set) -> Args γ U -> E
index (ι e)     U _ = e
index (σ A γ)   U a = index (γ (π₀ a)) U (π₁ a)
index (δ A i γ) U a = index γ U (π₁ a)

-- The assumptions of a particular inductive occurrence in a value.
IndArg : {I : Set}{E : Set}
       (γ : OP I E)(U : I -> Set) ->
       Args γ U -> Set
IndArg (ι e)     U _ = Zero
IndArg (σ A γ)   U a = IndArg (γ (π₀ a)) U (π₁ a)
IndArg (δ A i γ) U a = A + IndArg γ U (π₁ a)

-- Given the assumptions of an inductive occurence in a value we can compute
-- its index.
IndIndex : {I : Set}{E : Set}
          (γ : OP I E)(U : I -> Set) ->
          (a : Args γ U) -> IndArg γ U a -> I
IndIndex (ι e)     U _	      ()
IndIndex (σ A γ)   U arg c       = IndIndex (γ (π₀ arg)) U (π₁ arg) c
IndIndex (δ A i γ) U arg (inl a) = i a
IndIndex (δ A i γ) U arg (inr a) = IndIndex γ U (π₁ arg) a

-- Given the assumptions of an inductive occurrence in a value we can compute
-- its value.
Ind : {I : Set}{E : Set}
      (γ : OP I E)(U : I -> Set) ->
      (a : Args γ U)(v : IndArg γ U a) -> U (IndIndex γ U a v)
Ind (ι e)     U _	      ()
Ind (σ A γ)   U arg c       = Ind (γ (π₀ arg)) U (π₁ arg) c
Ind (δ A i γ) U arg (inl a) = (π₀ arg) a
Ind (δ A i γ) U arg (inr a) = Ind γ U (π₁ arg) a

-- The type of induction hypotheses. Basically
--  forall assumptions, the predicate holds for an inductive occurrence with
--  those assumptions
IndHyp : {I : Set}{E : Set}
      (γ : OP I E)(U : I -> Set) ->
      (F : (i : I) -> U i -> Set)(a : Args γ U) -> Set
IndHyp γ U F a = (v : IndArg γ U a) -> F (IndIndex γ U a v) (Ind γ U a v)

IndHyp₁ : {I : Set}{E : Set}
      (γ : OP I E)(U : I -> Set) ->
      (F : (i : I) -> U i -> Set1)(a : Args γ U) -> Set1
IndHyp₁ γ U F a = (v : IndArg γ U a) -> F (IndIndex γ U a v) (Ind γ U a v)

-- If we can prove a predicate F for any values, we can construct the inductive
-- hypotheses for a given value.
-- Termination note: g will only be applied to values smaller than a
induction :
  {I : Set}{E : Set}
  (γ : OP I E)(U : I -> Set)
  (F : (i : I) -> U i -> Set)
  (g : (i : I)(u : U i) -> F i u)
  (a : Args γ U) -> IndHyp γ U F a
induction γ U F g a = \hyp -> g (IndIndex γ U a hyp) (Ind γ U a hyp)

induction₁ :
  {I : Set}{E : Set}
  (γ : OP I E)(U : I -> Set)
  (F : (i : I) -> U i -> Set1)
  (g : (i : I)(u : U i) -> F i u)
  (a : Args γ U) -> IndHyp₁ γ U F a
induction₁ γ U F g a = \hyp -> g (IndIndex γ U a hyp) (Ind γ U a hyp)

max_stars_repo_name: asr/agda-kanso


text:
module start where

open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Function hiding (id)

injective : {A B : Set} → (f : A → B) → Set
injective f = ∀ a₁ a₂ → f a₁ ≡ f a₂ → a₁ ≡ a₂

surjective : {A B : Set} → (f : A → B) → Set
surjective f = ∀ b → ∃ (λ a → f a ≡ b)

bijective : {A B : Set} → (f : A → B) → Set
bijective f = injective f × surjective f

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

lemma-suc-inj : ∀ {a₁ a₂} → suc a₁ ≡ suc a₂ → a₁ ≡ a₂
lemma-suc-inj refl = refl

suc-injective : injective suc
suc-injective a₁ a₂ = lemma-suc-inj

id : {A : Set} → A → A
id x = x

lemma-id-inj : ∀ {A} {a₁ a₂ : A} → id a₁ ≡ id a₂ → a₁ ≡ a₂
lemma-id-inj refl = refl

id-injective : ∀ {A} → injective (id {A})
id-injective a₁ a₂ = lemma-id-inj

lemma-id-surj : ∀ {A} (b : A) → ∃ (λ a → id a ≡ b)
lemma-id-surj b = b , refl

id-surjective : ∀ {A} → surjective (id {A})
id-surjective = lemma-id-surj

bijective→injective : ∀ {A B} {f : A → B} → bijective f → injective f
bijective→injective b = proj₁ b

bijective→surjective : ∀ {A B} {f : A → B} → bijective f → surjective f
bijective→surjective b = proj₂ b

left-inverse : ∀ {A B} → (f : A → B) → Set
left-inverse f = ∃ (λ g → g ∘ f ≡ id)

right-inverse : ∀ {A B} → (f : A → B) → Set
right-inverse f = ∃ (λ g → f ∘ g ≡ id)

infix 5 _s~_
_s~_ : {A : Set} {a b c : A} → a ≡ b → a ≡ c → c ≡ b
_s~_ refl refl = refl

infix 5 _~_
_~_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
_~_ = trans

lemma-left-id₁ : ∀ {A B : Set} (g : B → A) (f : A → B) → g ∘ f ≡ id → (∀ a → g (f a) ≡ a)
lemma-left-id₁ g f idcomp a = cong (λ f₁ → f₁ a) idcomp

lemma-left-id : ∀ {A B : Set} (a₁ a₂ : A) (g : B → A) (f : A → B) → g ∘ f ≡ id → g (f a₁) ≡ g (f a₂) → a₁ ≡ a₂
lemma-left-id a₁ a₂ g f idcomp comp = (comp ~ lemma-left-id₁ g f idcomp a₂) s~ lemma-left-id₁ g f idcomp a₁

lemma-left-inj : ∀ {A B : Set} (a₁ a₂ : A) → (f : A → B) → ∃ (λ g → g ∘ f ≡ id) → f a₁ ≡ f a₂ → a₁ ≡ a₂
lemma-left-inj a₁ a₂ f (g , idcomp) eq = lemma-left-id a₁ a₂ g f idcomp (cong (λ x → g x) eq)

left-inverse→injective : ∀ {A B} (f : A → B) → left-inverse f → injective f
left-inverse→injective f left-inv a₁ a₂ fas = lemma-left-inj a₁ a₂ f left-inv fas

right-inverse→surjective : ∀ {A B} (f : A → B) → right-inverse f → surjective f
right-inverse→surjective f (g , right) b = g b , cong (λ f₁ → f₁ b) right

postulate extensionality : {A : Set} {B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

id-unique : ∀ {A : Set} → (f : A → A) → (∀ a → f a ≡ a) → f ≡ id
id-unique f fa-prop = extensionality {f = f} {g = id} fa-prop

surjective→right-inverse : ∀ {A B} (f : A → B) → surjective f → right-inverse f
surjective→right-inverse f right = g , id-unique (f ∘ g) (λ b → proj₂ (right b))
  where g = λ b → proj₁ (right b)

max_stars_repo_name: Chobbes/AbstractAgdabra

max_issues_repo_name: Chobbes/AbstractAgdabra

max_forks_repo_name: Chobbes/AbstractAgdabra


text:
module DataDef where

data ⊤
  : Set
  where

  tt
    : ⊤

data ⊤'
  (x : ⊤)
  : Set
  where

  tt
    : ⊤' x

data D
  {y : ⊤}
  (y' : ⊤' y)
  : Set

data D {z} _ where

postulate

  d
    : D {tt} tt

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


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

module Dodo.Unary.Unique where

-- Stdlib imports
open import Level using (Level)
open import Relation.Unary using (Pred)
open import Relation.Binary using (Rel)
-- Local imports
open import Dodo.Nullary.Unique

-- # Definitions #

-- | At most one element satisfies the predicate
Unique₁ : ∀ {a ℓ₁ ℓ₂ : Level} {A : Set a}
  → Rel A ℓ₁ → Pred A ℓ₂ → Set _
Unique₁ _≈_ P = ∀ {x y} → P x → P y → x ≈ y

-- | For every `x`, there exists at most one inhabitant of `P x`.
UniquePred : ∀ {a ℓ : Level} {A : Set a}
  → Pred A ℓ → Set _
UniquePred P = ∀ x → Unique (P x)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
-- Minimal implicational modal logic, de Bruijn approach, initial encoding

module Bi.BoxMp where

open import Lib using (List; []; _,_; LMem; lzero; lsuc)

-- Types

infixr 0 _=>_
data Ty : Set where
  UNIT :             Ty
  _=>_ : Ty -> Ty -> Ty
  BOX  : Ty       -> Ty

-- Context and truth/validity judgements

Cx : Set
Cx = List Ty

isTrue : Ty -> Cx -> Set
isTrue a tc = LMem a tc

isValid : Ty -> Cx -> Set
isValid a vc = LMem a vc

-- Terms

module BoxMp where
  infixl 1 _$_
  infixr 0 lam=>_
  data Tm (vc tc : Cx) : Ty -> Set where
    var    : forall {a}   -> isTrue a tc                     -> Tm vc tc a
    lam=>_ : forall {a b} -> Tm vc (tc , a) b                -> Tm vc tc (a => b)
    _$_    : forall {a b} -> Tm vc tc (a => b) -> Tm vc tc a -> Tm vc tc b
    var#   : forall {a}   -> isValid a vc                    -> Tm vc tc a
    box    : forall {a}   -> Tm vc [] a                      -> Tm vc tc (BOX a)
    unbox' : forall {a b} -> Tm vc tc (BOX a)  -> Tm (vc , a) tc b -> Tm vc tc b

  syntax unbox' x' x = unbox x' => x

  v0 : forall {vc tc a} -> Tm vc (tc , a) a
  v0 = var lzero

  v1 : forall {vc tc a b} -> Tm vc (tc , a , b) a
  v1 = var (lsuc lzero)

  v2 : forall {vc tc a b c} -> Tm vc (tc , a , b , c) a
  v2 = var (lsuc (lsuc lzero))

  v0# : forall {vc tc a} -> Tm (vc , a) tc a
  v0# = var# lzero

  v1# : forall {vc tc a b} -> Tm (vc , a , b) tc a
  v1# = var# (lsuc lzero)

  v2# : forall {vc tc a b c} -> Tm (vc , a , b , c) tc a
  v2# = var# (lsuc (lsuc lzero))

  Thm : Ty -> Set
  Thm a = forall {vc tc} -> Tm vc tc a
open BoxMp public

-- Example theorems

rNec : forall {a} -> Thm a -> Thm (BOX a)
rNec x =
  box x

aK : forall {a b} -> Thm (BOX (a => b) => BOX a => BOX b)
aK =
  lam=>
    lam=>
      (unbox v1 =>
        unbox v0 =>
          box (v1# $ v0#))

aT : forall {a} -> Thm (BOX a => a)
aT =
  lam=>
    (unbox v0 => v0#)

a4 : forall {a} -> Thm (BOX a => BOX (BOX a))
a4 =
  lam=>
    (unbox v0 => box (box v0#))

t1 : forall {a} -> Thm (a => BOX (a => a))
t1 =
  lam=> box (lam=> v0)

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


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

module PiU where

open import Data.Nat using (ℕ; _+_; _*_)

------------------------------------------------------------------------------
-- Define the ``universe'' for Pi.  All versions of Pi share the same
-- universe.  Where they differ is in what combinators exist between
-- members of the universe.
--
-- ZERO is a type with no elements
-- ONE is a type with one element 'tt'
-- PLUS ONE ONE is a type with elements 'false' and 'true'
-- and so on for all finite types built from ZERO, ONE, PLUS, and TIMES
--
-- We also have that U is a type with elements ZERO, ONE, PLUS ONE ONE,
--   TIMES BOOL BOOL, etc.

data U : Set where
  ZERO  : U
  ONE   : U
  PLUS  : U → U → U
  TIMES : U → U → U

-- defines the size of a finite type

toℕ : U → ℕ
toℕ ZERO = 0
toℕ ONE = 1
toℕ (PLUS t₁ t₂) = toℕ t₁ + toℕ t₂
toℕ (TIMES t₁ t₂) = toℕ t₁ * toℕ t₂

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


text:
module Using where

module Dummy where
  data DummySet1 : Set where ds1 : DummySet1
  data DummySet2 : Set where ds2 : DummySet2

open Dummy
  using (DummySet1)

open Dummy -- checking that newline + comment is allowed before "using"
  using (DummySet2)

-- Andreas, 2020-06-06, issue #4704
-- Allow repetions in `using` directives, but emit warning.
open Dummy
  using (DummySet1; DummySet1)
  using (DummySet1)

-- EXPECTED: dead code highlighting for 2nd and 3rd occurrence and warning:
-- Duplicates in using directive: DummySet1 DummySet1
-- when scope checking the declaration
--   open Dummy using (DummySet1; DummySet1; DummySet1)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Data.Binary.Conversion where

open import Data.Binary.Definition
open import Data.Binary.Increment
import Data.Nat as ℕ
open import Data.Nat using (ℕ; suc; zero)

⟦_⇑⟧ : ℕ → 𝔹
⟦ zero  ⇑⟧ = 0ᵇ
⟦ suc n ⇑⟧ = inc ⟦ n ⇑⟧

⟦_⇓⟧ : 𝔹 → ℕ
⟦ 0ᵇ ⇓⟧ = 0
⟦ 1ᵇ xs ⇓⟧ = 1 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2
⟦ 2ᵇ xs ⇓⟧ = 2 ℕ.+ ⟦ xs ⇓⟧ ℕ.* 2

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --warning=error #-}

module AbstractModuleMacro where

import Common.Issue481ParametrizedModule as P

abstract
  module M = P Set