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

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

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

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

  private
    variable
      U : Set 𝓁

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

  {- Coinductive interpretation -}

  data SCoInd⟦_⟧ {𝓁c 𝓁p 𝓁n : Level} (is : IS {𝓁c} {𝓁p} {𝓁n} U) : U → Size → Set (𝓁 ⊔ 𝓁c ⊔ 𝓁p ⊔ 𝓁n) where
    sfold : ∀{u i} → ISF[ is ] (λ u → Thunk (SCoInd⟦ is ⟧ u) i) u → SCoInd⟦ is ⟧ u i

  {- Coinduction Principle -}

  scoind[_] : ∀{𝓁c 𝓁p 𝓁n 𝓁'}
      → (is : IS {𝓁c} {𝓁p} {𝓁n} U)
      → (S : U → Set 𝓁')
      → S ⊆ ISF[ is ] S     -- S is consistent
      → S ⊆ λ u → ∀{i} → SCoInd⟦ is ⟧ u i
  scoind[ is ] S cn Su with cn Su
  ... | rn , c , refl , pr = sfold (rn , c , refl , λ i → λ where .force → scoind[ is ] S cn (pr i))

  {- Apply Rule -}

  apply-scoind : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → (rn : is .Names) → RClosed (is .rules rn) (λ u → ∀{i} → SCoInd⟦ is ⟧ u i)
  apply-scoind {is = is} rn =
    prefix⇒closed (is .rules rn) {P = λ u → ∀{i} → SCoInd⟦ is ⟧ u i } λ{(c , refl , pr) → sfold (rn , c , refl , λ i → λ where .force → pr i)}

  {- Postfix - Prefix -}

  scoind-postfix : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → (λ u → ∀{i} → SCoInd⟦ is ⟧ u i) ⊆ ISF[ is ] (λ u → ∀{i} → SCoInd⟦ is ⟧ u i)
  scoind-postfix p-scoind with p-scoind
  ... | sfold (rn , c , refl , pr) = rn , c , refl , λ i → (pr i) .force

  scoind-prefix : ∀{𝓁c 𝓁p 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U} → ISF[ is ] (λ u → ∀{i} → SCoInd⟦ is ⟧ u i) ⊆ λ u → ∀{i} → SCoInd⟦ is ⟧ u i
  scoind-prefix (rn , c , refl , pr) = apply-scoind rn c pr

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
{-# OPTIONS --cubical --no-exact-split --safe #-}
module Cubical.Structures.Queue where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.FunExtEquiv
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

open import Cubical.Structures.Pointed

open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Prod.Base hiding (_×_) renaming (_×Σ_ to _×_)

-- Developing Queues as a standard notion of structure, see
-- https://github.com/ecavallo/cubical/blob/queue/Cubical/Experiments/Queue.agda
-- for the original development

variable
 ℓ ℓ' : Level

-- We start fixing a set A on which we define what it means for a type Q to have
-- a Queue structure (wrt. A)
module Queues-on (A : Type ℓ) (Aset : isSet A) where
 -- A Queue structure has three components, the empty Queue, a push function and a pop function
 -- We first deal with push and pop as separate structures
 left-action-structure : Type ℓ → Type ℓ
 left-action-structure X = A → X → X

 Left-Action : Type (ℓ-suc ℓ)
 Left-Action = TypeWithStr ℓ left-action-structure

 left-action-iso : StrIso left-action-structure ℓ
 left-action-iso (X , l) (Y , m) e = ∀ a x → e .fst (l a x) ≡ m a (e .fst x)

 Left-Action-is-SNS : SNS {ℓ} left-action-structure left-action-iso
 Left-Action-is-SNS = SNS-≡→SNS-PathP left-action-iso ((λ _ _ → funExt₂Equiv))

 -- Now for the pop-map as a structure
 -- First, a few preliminary results that we will need later
 pop-map-forward : {X Y : Type ℓ} → (X → Y)
                  →  Unit ⊎ (X × A) → Unit ⊎ (Y × A)
 pop-map-forward f (inl tt) = inl tt
 pop-map-forward f (inr (x , a)) = inr (f x , a)

 pop-map-forward-∘ :{B C D : Type ℓ}
  (g : C → D) (f : B → C)
  → ∀ r → pop-map-forward {X = C} g (pop-map-forward f r) ≡ pop-map-forward (λ b → g (f b)) r
 pop-map-forward-∘ g f (inl tt) = refl
 pop-map-forward-∘ g f (inr (b , a)) = refl

 pop-map-lemma : {X : Type ℓ} → idfun (Unit ⊎ (X × A)) ≡ pop-map-forward (idfun X)
 pop-map-lemma {X = X} = funExt γ
  where
   γ : ∀ z → z ≡ pop-map-forward (idfun X) z
   γ (inl tt) = refl
   γ (inr xa) = refl

 pop-structure : Type ℓ → Type ℓ
 pop-structure X = X → Unit ⊎ (X × A)

 Pop : Type (ℓ-suc ℓ)
 Pop = TypeWithStr ℓ pop-structure

 pop-iso : StrIso pop-structure ℓ
 pop-iso (X , p) (Y , q) e = ∀ x → pop-map-forward (e .fst) (p x) ≡ q (e .fst x)

 Pop-is-SNS : SNS {ℓ} pop-structure pop-iso
 Pop-is-SNS = SNS-≡→SNS-PathP pop-iso (λ p q → (subst (λ f → (∀ x → f (p x) ≡ q x) ≃ (p ≡ q)) pop-map-lemma funExtEquiv))

 -- Now we can do Queues:
 queue-structure : Type ℓ → Type ℓ
 queue-structure Q = Q × (A → Q → Q) × (Q → Unit ⊎ (Q × A))

 Queue : Type (ℓ-suc ℓ)
 Queue = TypeWithStr ℓ queue-structure

 queue-iso : StrIso queue-structure ℓ
 queue-iso (Q₁ , emp₁ , push₁ , pop₁) (Q₂ , emp₂ , push₂ , pop₂) e =
            (e .fst emp₁ ≡ emp₂)
          × (∀ a q → e .fst (push₁ a q) ≡ push₂ a (e .fst q))
          × (∀ q → pop-map-forward (e .fst) (pop₁ q) ≡ pop₂ (e .fst q))

 Queue-is-SNS : SNS {ℓ₁ = ℓ} queue-structure queue-iso
 Queue-is-SNS = join-SNS pointed-structure pointed-iso pointed-is-SNS
             (λ X → (left-action-structure X) × (pop-structure X))
             (λ B C e →  (∀ a q → e .fst (B .snd .fst a q) ≡ C .snd .fst a (e .fst q))
                       × (∀ q → pop-map-forward (e .fst) (B .snd .snd q) ≡ C .snd .snd (e .fst q)))
               (join-SNS left-action-structure left-action-iso Left-Action-is-SNS
                         pop-structure         pop-iso         Pop-is-SNS        )

 -- Should we add further axioms for Queues?
 -- Some suggestions:
 queue-axioms : (Q : Type ℓ) → queue-structure Q → Type ℓ
 queue-axioms Q (emp , push , pop) =   (isSet Q)
                                     × (pop emp ≡ inl tt)
                                     × ∀ a → pop (push a emp) ≡ inr (emp , a)
                                     -- etc.

ext: agda

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
            --no-subtyping #-}

module Agda.Builtin.String.Properties where

open import Agda.Builtin.String
open import Agda.Builtin.Equality

primitive

  primStringToListInjective : ∀ a b → primStringToList a ≡ primStringToList b → a ≡ b

max_stars_repo_name: alexarice/agda

max_issues_repo_name: alexarice/agda

max_forks_repo_name: alexarice/agda


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

module Categories.Category.Instance.SimplicialSet where

open import Level

open import Categories.Category
open import Categories.Category.Instance.Simplex
open import Categories.Category.Construction.Presheaves

SimplicialSet : ∀ o ℓ → Category (suc (o ⊔ ℓ)) (o ⊔ ℓ) (o ⊔ ℓ)
SimplicialSet o ℓ = Presheaves {o′ = o} {ℓ′ = ℓ} Δ

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:
-- 2010-10-05 Andreas

module TerminationRecordPatternCoerce where

data Empty : Set where

record Unit : Set where
  constructor unit

data Bool : Set where
  true false : Bool

T : Bool -> Set
T true = Unit
T false = Empty

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

subst : forall {A a b} -> a == b -> {P : A -> Set} -> P a -> P b
subst refl x = x

-- Thorsten suggests on the Agda list  thread "Coinductive families"
-- to encode lists as records
record List (A : Set) : Set where
  constructor list
  field
    isCons : Bool
    head   : T isCons -> A
    tail   : T isCons -> List A

open List public

-- However, we have to be careful to preserve termination
-- in the presence of a lie

postulate
  lie : {b : Bool} -> T b

-- if the record constructor list was counted as structural increase
-- this function would not be rejected
f : {A : Set} -> (b : Bool) -> (l : List A) -> b == isCons l -> Unit
f .false (list false h t) refl = unit
f .true (list true h t) refl = f (isCons tl) tl refl
  where tl : List _
        tl = t unit
{- dot patterns inside of record patterns not supported!
f true (list .true h t) refl = f (isCons tl) tl refl
  where tl : List _
        tl = t unit
-}

-- however, it is almost like the following
f' : {A : Set} -> (b : Bool) -> (l : List A) -> b == isCons l -> Unit
f' false l p = unit
f' true (list b' h t) p = f' (isCons tl) tl refl
   where tl : List _
         tl = t (subst p {T} unit)

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
{-# OPTIONS --cubical #-}
module Multidimensional.Data.Dir where

open import Multidimensional.Data.Dir.Base public

open import Multidimensional.Data.Dir.Properties public

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


text:
-- Intuitionistic propositional calculus.
-- Kripke-style semantics with exploding abstract worlds.

module IPC.Semantics.KripkeExploding where

open import IPC.Syntax.Common public

-- Intuitionistic Kripke-CPS models, with exploding worlds.

record Model : Set₁ where
  infix 3 _⊪ᵅ_
  field
    World : Set

    -- Intuitionistic accessibility; preorder.
    _≤_    : World → World → Set
    refl≤  : ∀ {w} → w ≤ w
    trans≤ : ∀ {w w′ w″} → w ≤ w′ → w′ ≤ w″ → w ≤ w″

    -- Strong forcing for atomic propositions; monotonic.
    _⊪ᵅ_   : World → Atom → Set
    mono⊪ᵅ : ∀ {P w w′} → w ≤ w′ → w ⊪ᵅ P → w′ ⊪ᵅ P

    -- Exploding.
    _‼_ : World → Ty → Set

open Model {{…}} public

-- Strong forcing and forcing, in a particular world of a particular model.

module _ {{_ : Model}} where
  mutual
    infix 3 _⊪_
    _⊪_ : World → Ty → Set
    w ⊪ α P   = w ⊪ᵅ P
    w ⊪ A ▻ B = ∀ {w′} → w ≤ w′ → w′ ⊩ A → w′ ⊩ B
    w ⊪ A ∧ B = w ⊩ A × w ⊩ B
    w ⊪ ⊤    = 𝟙
    w ⊪ ⊥    = 𝟘
    w ⊪ A ∨ B = w ⊩ A ⊎ w ⊩ B

    infix 3 _⊩_
    _⊩_ : World → Ty → Set
    w ⊩ A = ∀ {C w′} → w ≤ w′ → (∀ {w″} → w′ ≤ w″ → w″ ⊪ A → w″ ‼ C) → w′ ‼ C

  infix 3 _⊩⋆_
  _⊩⋆_ : World → Cx Ty → Set
  w ⊩⋆ ∅     = 𝟙
  w ⊩⋆ Ξ , A = w ⊩⋆ Ξ × w ⊩ A

-- Monotonicity with respect to intuitionistic accessibility.

module _ {{_ : Model}} where
  mutual
    mono⊪ : ∀ {A w w′} → w ≤ w′ → w ⊪ A → w′ ⊪ A
    mono⊪ {α P}   ξ s       = mono⊪ᵅ ξ s
    mono⊪ {A ▻ B} ξ f       = λ ξ′ a → f (trans≤ ξ ξ′) a
    mono⊪ {A ∧ B} ξ (a , b) = mono⊩ {A} ξ a , mono⊩ {B} ξ b
    mono⊪ {⊤}    ξ ∙       = ∙
    mono⊪ {⊥}    ξ ()
    mono⊪ {A ∨ B} ξ (ι₁ a)  = ι₁ (mono⊩ {A} ξ a)
    mono⊪ {A ∨ B} ξ (ι₂ b)  = ι₂ (mono⊩ {B} ξ b)

    mono⊩ : ∀ {A w w′} → w ≤ w′ → w ⊩ A → w′ ⊩ A
    mono⊩ ξ a = λ ξ′ k′ → a (trans≤ ξ ξ′) k′

  mono⊩⋆ : ∀ {Ξ w w′} → w ≤ w′ → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
  mono⊩⋆ {∅}     ξ ∙       = ∙
  mono⊩⋆ {Ξ , A} ξ (γ , a) = mono⊩⋆ {Ξ} ξ γ , mono⊩ {A} ξ a

-- Additional useful equipment.

module _ {{_ : Model}} where
  _⟪$⟫_ : ∀ {A B w} → w ⊪ A ▻ B → w ⊩ A → w ⊩ B
  s ⟪$⟫ a = s refl≤ a

  return : ∀ {A w} → w ⊪ A → w ⊩ A
  return {A} a = λ ξ k → k refl≤ (mono⊪ {A} ξ a)

  bind : ∀ {A B w} → w ⊩ A → (∀ {w′} → w ≤ w′ → w′ ⊪ A → w′ ⊩ B) → w ⊩ B
  bind a k = λ ξ k′ → a ξ (λ ξ′ a′ → k (trans≤ ξ ξ′) a′ refl≤ (λ ξ″ a″ → k′ (trans≤ ξ′ ξ″) a″))

-- Forcing in a particular world of a particular model, for sequents.

module _ {{_ : Model}} where
  infix 3 _⊩_⇒_
  _⊩_⇒_ : World → Cx Ty → Ty → Set
  w ⊩ Γ ⇒ A = w ⊩⋆ Γ → w ⊩ A

  infix 3 _⊩_⇒⋆_
  _⊩_⇒⋆_ : World → Cx Ty → Cx Ty → Set
  w ⊩ Γ ⇒⋆ Ξ = w ⊩⋆ Γ → w ⊩⋆ Ξ

-- Entailment, or forcing in all worlds of all models, for sequents.

infix 3 _⊨_
_⊨_ : Cx Ty → Ty → Set₁
Γ ⊨ A = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒ A

infix 3 _⊨⋆_
_⊨⋆_ : Cx Ty → Cx Ty → Set₁
Γ ⊨⋆ Ξ = ∀ {{_ : Model}} {w : World} → w ⊩ Γ ⇒⋆ Ξ

-- Additional useful equipment, for sequents.

module _ {{_ : Model}} where
  lookup : ∀ {A Γ w} → A ∈ Γ → w ⊩ Γ ⇒ A
  lookup top     (γ , a) = a
  lookup (pop i) (γ , b) = lookup i γ

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module erasure where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import decidable using (Dec; yes; no; Bool; true; false; ⌊_⌋; _∧_; _×-dec_; _∨_; _⊎-dec_; not; ¬?)

-- erasureを使うことで真偽値の論理積とdecidableの論理積が等しくなることの証明
∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
∧-× (yes a) (yes b) = refl
∧-× (yes a) (no b)  = refl
∧-× (no a)  (yes b) = refl
∧-× (no a)  (no b)  = refl

-- erasureを使うことで真偽値の論理和とdecidableの論理和が等しくなることの証明
∨-⊎ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
∨-⊎ (yes a) (yes b) = refl
∨-⊎ (yes a) (no b)  = refl
∨-⊎ (no a)  (yes b) = refl
∨-⊎ (no a)  (no b)  = refl

-- erasureを使うことで真偽値の否定とdecidableの否定が等しくなることの証明
not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
not-¬ (yes a) = refl
not-¬ (no a)  = refl

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
open import Issue2229Reexport1

B = A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical #-}

open import Agda.Primitive.Cubical

postulate
  Id    : ∀ {ℓ} {A : Set ℓ}     → A    → A    → Set ℓ
  Path  : ∀ {ℓ} {A : Set ℓ}     → A    → A    → Set ℓ
  PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

{-# BUILTIN PATH  Path  #-}
{-# BUILTIN PATHP PathP #-}
{-# BUILTIN ID    Id    #-}
{-# BUILTIN CONID conid #-}

reflPath : ∀ {ℓ} {A : Set ℓ} {x : A} → Path x x
reflPath {x = x} = λ i → x

reflId : ∀ {ℓ} {A : Set ℓ} {x : A} → Id x x
reflId {x = x} = conid i1 reflPath

primitive
 primIdJ : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ')
         → P x reflId → {y : A} (p : Id x y) → P y p

Id-comp-Id : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ')
           → (b : P x reflId) → Id (primIdJ P b reflId) b
Id-comp-Id P b = reflId

Id-comp-Path : ∀ {ℓ ℓ'} {A : Set ℓ} {x : A} (P : ∀ y → Id x y → Set ℓ')
             → (b : P x reflId) → Path (primIdJ P b reflId) b
Id-comp-Path P b = λ i → b

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Divisibility and coprimality
------------------------------------------------------------------------

module Data.Integer.Divisibility where

open import Function
open import Data.Integer
open import Data.Integer.Properties
import Data.Nat.Divisibility as ℕ
import Data.Nat.Coprimality as ℕ
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

-- Divisibility.

infix 4 _∣_

_∣_ : Rel ℤ zero
_∣_ = ℕ._∣_ on ∣_∣

-- Coprimality.

Coprime : Rel ℤ zero
Coprime = ℕ.Coprime on ∣_∣

-- If i divides jk and is coprime to j, then it divides k.

coprime-divisor : ∀ i j k → Coprime i j → i ∣ j * k → i ∣ k
coprime-divisor i j k c eq =
  ℕ.coprime-divisor c (subst (ℕ._∣_ ∣ i ∣) (abs-*-commute j k) eq)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Closures of a unary relation with respect to a binary one.
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Unary.Closure.Base {a b} {A : Set a} (R : Rel A b) where

open import Level
open import Relation.Unary using (Pred)

------------------------------------------------------------------------
-- Definitions

-- We start with the definition of □ ("box") which is named after the box
-- modality in modal logic. `□ T x` states that all the elements one step
-- away from `x` with respect to the relation R satisfy `T`.

□ : ∀ {t} → Pred A t → Pred A (a ⊔ b ⊔ t)
□ T x = ∀ {y} → R x y → T y

-- Use cases of □ include:
-- * The definition of the accessibility predicate corresponding to R:
--   data Acc (x : A) : Set (a ⊔ b) where
--     step : □ Acc x → Acc x

-- * The characterization of stability under weakening: picking R to be
--   `Data.List.Relation.Sublist.Inductive`, `∀ {Γ} → Tm Γ → □ T Γ`
--   corresponds to the fact that we have a notion of weakening for `Tm`.

-- Closed: whenever we have a value in one context, we can get one in any
-- related context.

record Closed {t} (T : Pred A t) : Set (a ⊔ b ⊔ t) where
  field next : ∀ {x} → T x → □ T x

------------------------------------------------------------------------
-- Properties

module _ {t} {T : Pred A t} where

  reindex : Transitive R → ∀ {x y} → R x y → □ T x → □ T y
  reindex trans x∼y □Tx y∼z = □Tx (trans x∼y y∼z)

  -- Provided that R is reflexive and Transitive, □ is a comonad
  map : ∀ {u} {U : Pred A u} {x} → (∀ {x} → T x → U x) → □ T x → □ U x
  map f □Tx x~y = f (□Tx x~y)

  extract : Reflexive R → ∀ {x} → □ T x → T x
  extract refl □Tx = □Tx refl

  duplicate : Transitive R → ∀ {x} → □ T x → □ (□ T) x
  duplicate trans □Tx x∼y y∼z = □Tx (trans x∼y y∼z)

-- Provided that R is transitive, □ is the Closure operator
-- i.e. for any `T`, `□ T` is closed.
□-closed : Transitive R → ∀ {t} {T : Pred A t} → Closed (□ T)
□-closed trans = record { next = duplicate trans }


text:
module Base.Prelude.List where

open import Size      using (Size; ↑_)
open import Base.Free using (Free; pure)

data List (Shape : Set) (Pos : Shape → Set) (A : Set) : {Size} → Set where
  cons : ∀ {i : Size} → Free Shape Pos A → Free Shape Pos (List Shape Pos A {i}) → List Shape Pos A {↑ i}
  nil  : List Shape Pos A

pattern Cons mx mxs = pure (cons mx mxs)
pattern Nil         = pure nil

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Maybe type and some operations
------------------------------------------------------------------------

-- The definitions in this file are reexported by Data.Maybe.

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

module Data.Maybe.Base where

open import Level
open import Data.Bool.Base using (Bool; true; false; not)
open import Data.Unit.Base using (⊤)
open import Data.These.Base using (These; this; that; these)
open import Data.Product as Prod using (_×_; _,_)
open import Function.Base
open import Relation.Nullary.Reflects
open import Relation.Nullary

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

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

data Maybe (A : Set a) : Set a where
  nothing : Maybe A
  just    : (x : A) → Maybe A

------------------------------------------------------------------------
-- Some operations

boolToMaybe : Bool → Maybe ⊤
boolToMaybe true  = just _
boolToMaybe false = nothing

is-just : Maybe A → Bool
is-just (just _) = true
is-just nothing  = false

is-nothing : Maybe A → Bool
is-nothing = not ∘ is-just

decToMaybe : Dec A → Maybe A
decToMaybe ( true because [a]) = just (invert [a])
decToMaybe (false because  _ ) = nothing

-- A dependent eliminator.

maybe : ∀ {A : Set a} {B : Maybe A → Set b} →
        ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
maybe j n (just x) = j x
maybe j n nothing  = n

-- A non-dependent eliminator.

maybe′ : (A → B) → B → Maybe A → B
maybe′ = maybe

-- A defaulting mechanism

fromMaybe : A → Maybe A → A
fromMaybe = maybe′ id

-- A safe variant of "fromJust". If the value is nothing, then the
-- return type is the unit type.

module _ {a} {A : Set a} where

  From-just : Maybe A → Set a
  From-just (just _) = A
  From-just nothing  = Lift a ⊤

  from-just : (x : Maybe A) → From-just x
  from-just (just x) = x
  from-just nothing  = _

-- Functoriality: map

map : (A → B) → Maybe A → Maybe B
map f = maybe (just ∘ f) nothing

-- Applicative: ap

ap : Maybe (A → B) → Maybe A → Maybe B
ap nothing  = const nothing
ap (just f) = map f

-- Monad: bind

infixl 1 _>>=_
_>>=_ : Maybe A → (A → Maybe B) → Maybe B
nothing >>= f = nothing
just a  >>= f = f a

-- Alternative: <∣>

_<∣>_ : Maybe A → Maybe A → Maybe A
just x  <∣> my = just x
nothing <∣> my = my

------------------------------------------------------------------------
-- Aligning and zipping

alignWith : (These A B → C) → Maybe A → Maybe B → Maybe C
alignWith f (just a) (just b) = just (f (these a b))
alignWith f (just a) nothing  = just (f (this a))
alignWith f nothing  (just b) = just (f (that b))
alignWith f nothing  nothing  = nothing

zipWith : (A → B → C) → Maybe A → Maybe B → Maybe C
zipWith f (just a) (just b) = just (f a b)
zipWith _ _        _        = nothing

align : Maybe A → Maybe B → Maybe (These A B)
align = alignWith id

zip : Maybe A → Maybe B → Maybe (A × B)
zip = zipWith _,_

------------------------------------------------------------------------
-- Injections.

thisM : A → Maybe B → These A B
thisM a = maybe′ (these a) (this a)

thatM : Maybe A → B → These A B
thatM = maybe′ these that


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Pushout where

open import Cubical.HITs.Pushout.Base public
open import Cubical.HITs.Pushout.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Hopf where

open import Cubical.Core.Glue

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

open import Cubical.Data.Int
open import Cubical.Data.Prod

open import Cubical.HITs.S1
open import Cubical.HITs.S2
open import Cubical.HITs.S3
open import Cubical.HITs.Susp
open import Cubical.HITs.Join
open import Cubical.HITs.Interval
  renaming ( zero to I0 ; one to I1 )

Border : (x : S¹) → (j : I) → Partial (j ∨ ~ j) (Σ Type₀ (λ T → T ≃ S¹))
Border x j (j = i0) = S¹ , rot x , rotIsEquiv x
Border x j (j = i1) = S¹ , idEquiv S¹

-- Hopf fibration using SuspS¹
HopfSuspS¹ : SuspS¹ → Type₀
HopfSuspS¹ north = S¹
HopfSuspS¹ south = S¹
HopfSuspS¹ (merid x j) = Glue S¹ (Border x j)

-- Hopf fibration using S²
-- TODO : prove that it is equivalent to HopfSuspS¹
HopfS² : S² → Type₀
HopfS² base = S¹
HopfS² (surf i j) = Glue S¹ (λ { (i = i0) → _ , idEquiv S¹
                               ; (i = i1) → _ , idEquiv S¹
                               ; (j = i0) → _ , idEquiv S¹
                               ; (j = i1) → _ , _ , rotIsEquiv (loop i) } )

-- Hopf fibration using more direct definition of the rot equivalence
-- TODO : prove that it is equivalent to HopfSuspS¹
HopfS²' : S² → Type₀
HopfS²' base = S¹
HopfS²' (surf i j) = Glue S¹ (λ { (i = i0) → _ , rotLoopEquiv i0
                                ; (i = i1) → _ , rotLoopEquiv i0
                                ; (j = i0) → _ , rotLoopEquiv i0
                                ; (j = i1) → _ , rotLoopEquiv i } )

-- Total space of the fibration
TotalHopf : Type₀
TotalHopf = Σ SuspS¹ HopfSuspS¹

-- Forward direction
filler-1 : I → (j : I) → (y : S¹) → Glue S¹ (Border y j) → join S¹ S¹
filler-1 i j y x = hfill (λ t → λ { (j = i0) → inl (rotInv-1 x y t)
                                  ; (j = i1) → inr x })
                         (inS (push ((unglue (j ∨ ~ j) x) * inv y) (unglue (j ∨ ~ j) x) j)) i

TotalHopf→JoinS¹S¹ : TotalHopf → join S¹ S¹
TotalHopf→JoinS¹S¹ (north , x) = inl x
TotalHopf→JoinS¹S¹ (south , x) = inr x
TotalHopf→JoinS¹S¹ (merid y j , x) = filler-1 i1 j y x

-- Backward direction
JoinS¹S¹→TotalHopf : join S¹ S¹ → TotalHopf
JoinS¹S¹→TotalHopf (inl x) = (north , x)
JoinS¹S¹→TotalHopf (inr x) = (south , x)
JoinS¹S¹→TotalHopf (push y x j) =
  (merid (inv y * x) j
  , glue (λ { (j = i0) → y ; (j = i1) → x }) (rotInv-2 x y j))

-- Now for the homotopies, we will need to fill squares indexed by x y : S¹ with value in S¹
-- Some will be extremeley tough, but happen to be easy when x = y = base
-- therefore, we fill them for x = y = base and then use the connectedness of S¹ × S¹ and
-- the discreteness of ΩS¹ to get general fillers.

-- To proceed with that strategy, we first need a lemma :
-- the sections of the trivial fibration λ (_ : S¹) (_ : S¹) → Int are constant

-- this should be generalized to a constant fibration over a connected space with
-- discrete fiber
fibInt : S¹ → S¹ → Type₀
fibInt _ _ = Int

S¹→HSet : (A : Type₀) (p : isSet A) (F : S¹ → A) (x : S¹) → F base ≡ F x
S¹→HSet A p F base = refl {x = F base}
S¹→HSet A p F (loop i) = f' i
  where
  f : PathP (λ i → F base ≡ F (loop i)) refl (cong F loop)
  f i = λ j → F (loop (i ∧ j))
  L : cong F loop ≡ refl
  L = p (F base) (F base) (f i1) refl
  f' : PathP (λ i → F base ≡ F (loop i)) (refl {x = F base}) (refl {x = F base})
  f' = transport (λ i → PathP (λ j → F base ≡ F (loop j)) refl (L i)) f

constant-loop : (F : S¹ → S¹ → Int) → (x y : S¹) → F base base ≡ F x y
constant-loop F x y = L0 ∙ L1
  where
  p : isSet (S¹ → Int)
  p = hLevelPi 2 (λ _ → isSetInt)
  L : F base ≡ F x
  L = S¹→HSet (S¹ → Int) p F x
  L0 : F base base ≡ F x base
  L0 i = L i base
  L1 : F x base ≡ F x y
  L1 = S¹→HSet Int isSetInt (F x) y

discretefib : (F : S¹ → S¹ → Type₀) → Type₀
discretefib F = (a : (x y : S¹) → F x y) →
        (b : (x y : S¹) → F x y) →
        (a base base ≡ b base base) →
        (x y : S¹) → a x y ≡ b x y

discretefib-fibInt : discretefib fibInt
discretefib-fibInt a b h x y i =
  hcomp (λ t → λ { (i = i0) → constant-loop a x y t
                 ; (i = i1) → constant-loop b x y t })
        (h i)

-- first homotopy

assocFiller-3-aux : I → I → I → I → S¹
assocFiller-3-aux x y j i =
  hfill (λ t → λ { (i = i0) → rotInv-1 (loop y) (loop (~ y) * loop x) t
                 ; (i = i1) → rotInv-3 (loop y) (loop x) t
                 ; (x = i0) (y = i0) → base
                 ; (x = i0) (y = i1) → base
                 ; (x = i1) (y = i0) → base
                 ; (x = i1) (y = i1) → base })
        (inS ((rotInv-2 (loop x) (loop y) i) * (inv (loop (~ y) * loop x)))) j

-- assocFiller-3-endpoint is used only in the type of the next function, to specify the
-- second endpoint.
-- However, I only need the first endpoint, but I cannot specify only one of them as is.
-- TODO : use cubical extension types when available to remove assocFiller-3-endpoint
assocFiller-3-endpoint : (x : S¹) → (y : S¹) → y ≡ y
assocFiller-3-endpoint base base i = base
assocFiller-3-endpoint (loop x) base i = assocFiller-3-aux x i0 i1 i
assocFiller-3-endpoint base (loop y) i = assocFiller-3-aux i0 y i1 i
assocFiller-3-endpoint (loop x) (loop y) i = assocFiller-3-aux x y i1 i

assocFiller-3 : (x : S¹) → (y : S¹) →
                PathP (λ j → rotInv-1 y (inv y * x) j ≡ rotInv-3 y x j)
                      (λ i → ((rotInv-2 x y i) * (inv (inv y * x))))
                      (assocFiller-3-endpoint x y)
assocFiller-3 base base j i = base
assocFiller-3 (loop x) base j i = assocFiller-3-aux x i0 j i
assocFiller-3 base (loop y) j i = assocFiller-3-aux i0 y j i
assocFiller-3 (loop x) (loop y) j i = assocFiller-3-aux x y j i

assoc-3 : (_ y : S¹) → basedΩS¹ y
assoc-3 x y i = assocFiller-3 x y i1 i

fibInt≡fibAssoc-3 : fibInt ≡ (λ _ y → basedΩS¹ y)
fibInt≡fibAssoc-3 i = λ x y → basedΩS¹≡Int y (~ i)

discretefib-fibAssoc-3 : discretefib (λ _ y → basedΩS¹ y)
discretefib-fibAssoc-3 =
  transp (λ i → discretefib (fibInt≡fibAssoc-3 i)) i0 discretefib-fibInt

assocConst-3 : (x y : S¹) → assoc-3 x y ≡ refl
assocConst-3 x y = discretefib-fibAssoc-3 assoc-3 (λ _ _ → refl) refl x y

assocSquare-3 : I → I → S¹ → S¹ → S¹
assocSquare-3 i j x y = hcomp (λ t → λ { (i = i0) → assocFiller-3 x y j i0
                                       ; (i = i1) → assocFiller-3 x y j i1
                                       ; (j = i0) → assocFiller-3 x y i0 i
                                       ; (j = i1) → assocConst-3 x y t i })
                            (assocFiller-3 x y j i)

filler-3 : I → I → S¹ → S¹ → join S¹ S¹
filler-3 i j y x =
  hcomp (λ t → λ { (i = i0) → filler-1 t j (inv y * x)
                                           (glue (λ { (j = i0) → y ; (j = i1) → x })
                                                 (rotInv-2 x y j))
                 ; (i = i1) → push (rotInv-3 y x t) x j
                 ; (j = i0) → inl (assocSquare-3 i t x y)
                 ; (j = i1) → inr x })
        (push ((rotInv-2 x y (i ∨ j)) * (inv (inv y * x))) (rotInv-2 x y (i ∨ j)) j)

JoinS¹S¹→TotalHopf→JoinS¹S¹ : ∀ x → TotalHopf→JoinS¹S¹ (JoinS¹S¹→TotalHopf x) ≡ x
JoinS¹S¹→TotalHopf→JoinS¹S¹ (inl x) i = inl x
JoinS¹S¹→TotalHopf→JoinS¹S¹ (inr x) i = inr x
JoinS¹S¹→TotalHopf→JoinS¹S¹ (push y x j) i = filler-3 i j y x

-- Second homotopy

-- This HIT is the total space of the Hopf fibration but the ends of SuspS¹ have not been
-- glued together yet — which makes it into a cylinder.
-- This allows to write compositions that do not properly match at the endpoints. However,
-- I suspect it is unnecessary. TODO : do without PseudoHopf

PseudoHopf : Type₀
PseudoHopf = (S¹ × Interval) × S¹

PseudoHopf-π1 : PseudoHopf → S¹
PseudoHopf-π1 ((y , _) , _) = y

PseudoHopf-π2 : PseudoHopf → S¹
PseudoHopf-π2 (_ , x) = x

assocFiller-4-aux : I → I → I → I → S¹
assocFiller-4-aux x y j i =
  hfill (λ t → λ { (i = i0) → ((inv (loop y * loop x * loop (~ y))) * (loop y * loop x))
                              * (rotInv-1 (loop x) (loop y) t)
                 ; (i = i1) → (rotInv-4 (loop y) (loop y * loop x) (~ t)) * loop x
                 ; (x = i0) (y = i0) → base
                 ; (x = i0) (y = i1) → base
                 ; (x = i1) (y = i0) → base
                 ; (x = i1) (y = i1) → base })
        (inS (rotInv-2 (loop y * loop x) (loop y * loop x * loop (~ y)) i)) j

-- See assocFiller-3-endpoint
-- TODO : use cubical extension types when available to remove assocFiller-4-endpoint
assocFiller-4-endpoint : (x y : S¹) → basedΩS¹ (((inv (y * x * inv y)) * (y * x)) * x)
assocFiller-4-endpoint base base i = base
assocFiller-4-endpoint (loop x) base i = assocFiller-4-aux x i0 i1 i
assocFiller-4-endpoint base (loop y) i = assocFiller-4-aux i0 y i1 i
assocFiller-4-endpoint (loop x) (loop y) i = assocFiller-4-aux x y i1 i

assocFiller-4 : (x y : S¹) →
                PathP (λ j → ((inv (y * x * inv y)) * (y * x)) * (rotInv-1 x y j) ≡ (rotInv-4 y (y * x) (~ j)) * x)
                      (λ i → (rotInv-2 (y * x) (y * x * inv y) i))
                      (assocFiller-4-endpoint x y)
assocFiller-4 base base j i = base
assocFiller-4 (loop x) base j i = assocFiller-4-aux x i0 j i
assocFiller-4 base (loop y) j i = assocFiller-4-aux i0 y j i
assocFiller-4 (loop x) (loop y) j i = assocFiller-4-aux x y j i

assoc-4 : (x y : S¹) → basedΩS¹ (((inv (y * x * inv y)) * (y * x)) * x)
assoc-4 x y i = assocFiller-4 x y i1 i

fibInt≡fibAssoc-4 : fibInt ≡ (λ x y → basedΩS¹ (((inv (y * x * inv y)) * (y * x)) * x))
fibInt≡fibAssoc-4 i = λ x y → basedΩS¹≡Int (((inv (y * x * inv y)) * (y * x)) * x) (~ i)

discretefib-fibAssoc-4 : discretefib (λ x y → basedΩS¹ (((inv (y * x * inv y)) * (y * x)) * x))
discretefib-fibAssoc-4 =
  transp (λ i → discretefib (fibInt≡fibAssoc-4 i)) i0 discretefib-fibInt

assocConst-4 : (x y : S¹) → assoc-4 x y ≡ refl
assocConst-4 x y = discretefib-fibAssoc-4 assoc-4 (λ _ _ → refl) refl x y

assocSquare-4 : I → I → S¹ → S¹ → S¹
assocSquare-4 i j x y =
  hcomp (λ t → λ { (i = i0) → assocFiller-4 x y j i0
                 ; (i = i1) → assocFiller-4 x y j i1
                 ; (j = i0) → assocFiller-4 x y i0 i
                 ; (j = i1) → assocConst-4 x y t i })
        (assocFiller-4 x y j i)

filler-4-0 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → PseudoHopf
filler-4-0 i j y x =
  let x' = unglue (j ∨ ~ j) x in
  hfill (λ t → λ { (j = i0) → ((inv (y * x * inv y) * (y * x) , I0)
                              , inv (y * x * inv y) * (y * x) * (rotInv-1 x y t))
                 ; (j = i1) → ((inv (x * inv y) * x , I1) , x) })
        (inS ((inv (x' * inv y) * x' , seg j) , rotInv-2 x' (x' * inv y) j)) i

filler-4-1 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → PseudoHopf
filler-4-1 i j y x =
  let x' = unglue (j ∨ ~ j) x in
  hfill (λ t → λ { (j = i0) → ((inv (y * x * inv y) * (y * x) , I0)
                              , (rotInv-4 y (y * x) (~ t)) * x)
                 ; (j = i1) → ((inv (x * inv y) * x , I1) , x) })
        (inS ((inv (x' * inv y) * x' , seg j) , unglue (j ∨ ~ j) x)) i

filler-4-2 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → TotalHopf
filler-4-2 i j y x =
  let x' = unglue (j ∨ ~ j) x in
  hcomp (λ t → λ { (i = i0) → JoinS¹S¹→TotalHopf (filler-1 t j y x)
                 ; (i = i1) → (merid (PseudoHopf-π1 (filler-4-0 t j y x)) j
                              , glue (λ { (j = i0) → rotInv-1 x y t ; (j = i1) → x })
                                     (PseudoHopf-π2 (filler-4-0 t j y x)))
                 ; (j = i0) → (north , rotInv-1 x y t)
                 ; (j = i1) → (south , x) })
        (merid (inv (x' * inv y) * x') j
        , glue (λ { (j = i0) → y * x * inv y ; (j = i1) → x }) (rotInv-2 x' (x' * inv y) j))

filler-4-3 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → PseudoHopf
filler-4-3 i j y x =
  let x' = unglue (j ∨ ~ j) x in
  hcomp (λ t → λ { (i = i0) → filler-4-0 t j y x
                 ; (i = i1) → filler-4-1 t j y x
                 ; (j = i0) → ((inv (y * x * inv y) * (y * x) , I0) , assocSquare-4 i t x y)
                 ; (j = i1) → ((inv (x * inv y) * x , I1) , x) })
        ((inv (x' * inv y) * x' , seg j) , rotInv-2 x' (x' * inv y) (i ∨ j))

filler-4-4 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → PseudoHopf
filler-4-4 i j y x =
  let x' = unglue (j ∨ ~ j) x in
  hcomp (λ t → λ { (i = i0) → filler-4-1 t j y x
                 ; (i = i1) → ((y , seg j) , unglue (j ∨ ~ j) x)
                 ; (j = i0) → ((rotInv-4 y (y * x) i , I0)
                              , (rotInv-4 y (y * x) (i ∨ ~ t)) * x)
                 ; (j = i1) → ((rotInv-4 y x i , I1) , x) })
        ((rotInv-4 y x' i , seg j) , x')

filler-4-5 : (_ j : I) → (y : S¹) → Glue S¹ (Border y j) → TotalHopf
filler-4-5 i j y x =
  hcomp (λ t → λ { (i = i0) → filler-4-2 (~ t) j y x
                 ; (i = i1) → (merid (PseudoHopf-π1 (filler-4-4 t j y x)) j
                              , glue (λ { (j = i0) → x ; (j = i1) → x })
                                     (PseudoHopf-π2 (filler-4-4 t j y x)))
                 ; (j = i0) → (north , x)
                 ; (j = i1) → (south , x) })
        (merid (PseudoHopf-π1 (filler-4-3 i j y x)) j
        , glue (λ { (j = i0) → x ; (j = i1) → x }) (PseudoHopf-π2 (filler-4-3 i j y x)))

TotalHopf→JoinS¹S¹→TotalHopf : ∀ x → JoinS¹S¹→TotalHopf (TotalHopf→JoinS¹S¹ x) ≡ x
TotalHopf→JoinS¹S¹→TotalHopf (north , x) i = (north , x)
TotalHopf→JoinS¹S¹→TotalHopf (south , x) i = (south , x)
TotalHopf→JoinS¹S¹→TotalHopf (merid y j , x) i = filler-4-5 i j y x

JoinS¹S¹≡TotalHopf : join S¹ S¹ ≡ TotalHopf
JoinS¹S¹≡TotalHopf = isoToPath (iso JoinS¹S¹→TotalHopf
                                    TotalHopf→JoinS¹S¹
                                    TotalHopf→JoinS¹S¹→TotalHopf
                                    JoinS¹S¹→TotalHopf→JoinS¹S¹)

S³≡TotalHopf : S³ ≡ TotalHopf
S³≡TotalHopf = S³≡joinS¹S¹ ∙ JoinS¹S¹≡TotalHopf

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
-- Partial Agda bindings for the W3C Geolocation API
-- http://dev.w3.org/geo/api/spec-source.html
-- Not supporting the "read once" API or any of the options yet.

open import FRP.JS.Behaviour using ( Beh ; map )
open import FRP.JS.Geolocation.Coords using ( Coords )
open import FRP.JS.Maybe using ( Maybe )
open import FRP.JS.RSet using ( ⟦_⟧ ; ⟨_⟩ )

module FRP.JS.Geolocation where

postulate
  geolocation : ⟦ Beh ⟨ Maybe Coords ⟩ ⟧

{-# COMPILED_JS geolocation require("agda.frp").geolocation #-}

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:
module Numeral.Finite.Functions where

import Lvl
open import Syntax.Number
open import Lang.Instance
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Finite
open import Numeral.Finite.Bound
open import Numeral.Natural hiding (𝐏)
import      Numeral.Natural.Function as ℕ
import      Numeral.Natural.Function.Proofs as ℕ
open import Numeral.Natural.Oper

-- Maximum function.
-- Returns the greatest number.
max : ∀{a b} → 𝕟(a) → 𝕟(b) → 𝕟(ℕ.max a b)
max        𝟎      𝟎      = 𝟎
max {a}{b} (𝐒(x)) 𝟎      = bound-[≤] (ℕ.max-orderₗ {a}{b}) (𝐒(x))
max {a}{b} 𝟎      (𝐒(y)) = bound-[≤] (ℕ.max-orderᵣ {a}{b}) (𝐒(y))
max        (𝐒(x)) (𝐒(y)) = 𝐒(max x y)

-- Minimum function.
-- Returns the smallest number.
min : ∀{a b} → 𝕟(a) → 𝕟(b) → 𝕟(ℕ.min a b)
min 𝟎      𝟎      = 𝟎
min (𝐒(_)) 𝟎      = 𝟎
min 𝟎      (𝐒(_)) = 𝟎
min (𝐒(x)) (𝐒(y)) = 𝐒(min x y)

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:
import      Lvl
open import Structure.Operator.Vector
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.FiniteDimensional
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {V : Type{ℓᵥ}} ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}} ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ᵥ_ : V → V → V}
  {_⋅ₛᵥ_ : S → V → V}
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄
  where

open VectorSpace(vectorSpace)

open import Data.Tuple using (_⨯_ ; _,_)
open import Functional using (id ; _∘_ ; _∘₂_ ; _$_ ; swap ; _on₂_)
open import Function.Equals
open import Logic
open import Logic.Predicate
open import Numeral.CoordinateVector as Vec using () renaming (Vector to Vec)
open import Numeral.Finite
open import Numeral.Natural
open import Sets.ExtensionalPredicateSet as PredSet using (PredSet ; _∈_ ; [∋]-binaryRelator)
open import Structure.Function.Domain
open import Structure.Operator.Vector.LinearCombination ⦃ vectorSpace = vectorSpace ⦄
open import Syntax.Function

private variable n : ℕ

-- A sequence of vectors is linearly independent when there is no vector that can be represented as a linear combination by the others.
-- Note: Equivalent to: `∀{sf} → (linearCombination(vf)(sf) ≡ 𝟎ᵥ) → (sf ⊜ Vec.fill(𝟎ₛ))`.
LinearlyIndependent : Vec(n)(V) → Stmt
LinearlyIndependent = Injective ∘ linearCombination

-- A sequence of vectors is spanning the vector space when every vector in the vector space can be represented as a linear combination of the set of vectors.
Spanning : Vec(n)(V) → Stmt
Spanning = Surjective ∘ linearCombination

-- A sequence of vectors is a basis when every vector in the vector space can be represented as a unique linear combination of the set of vectors.
-- A sequence of vectors is a basis when they span the vector space and is linearly independent.
Basis : Vec(n)(V) → Stmt
Basis = Bijective ∘ linearCombination

-- A finite dimensional vector space is when there are a finite number of vectors that spans the whole space.
FiniteDimensional : Stmt
FiniteDimensional = ∃(n ↦ ∃(vf ↦ Spanning{n}(vf)))


text:
-- Andreas, 2012-04-20
{-# OPTIONS --show-implicit #-}
module SkipParametersInConstructorReification where

data Bool : Set where
  true false : Bool

data D (A : Set) : Set where
  c : {regArg : A} -> D A

data P : {A : Set} → D A → Set where
  p : P (c {regArg = true})

bla : Set
bla with c {regArg = true}
bla | _ = Bool

fail : P (c {regArg = false})
fail = true

-- What counts here is the error message!
--
--   Bool !=< P {Bool} (c {regArg = false}) of type Set
--
-- the parameter argument of c should be skipped, but the
-- regular argument should show up

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module BBHeap.Equality {A : Set}(_≤_ : A → A → Set) where

open import BBHeap _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_

data _≈_ {b b' : Bound} : BBHeap b → BBHeap b' → Set where
  ≈leaf : leaf {b} ≈ leaf {b'}
  ≈left : {x x' : A}{l r : BBHeap (val x)}{l' r' : BBHeap (val x')}
                   (b≤x : LeB b (val x))
                   (b'≤x' : LeB b' (val x'))
                   (l⋘r : l ⋘ r)
                   (l'⋘r' : l' ⋘ r')
                   → l ≈ l'
                   → r ≈ r'
                   → left b≤x l⋘r ≈ left b'≤x' l'⋘r'
  ≈right : {x x' : A}{l r : BBHeap (val x)}{l' r' : BBHeap (val x')}
                   (b≤x : LeB b (val x))
                   (b'≤x' : LeB b' (val x'))
                   (l⋙r : l ⋙ r)
                   (l'⋙r' : l' ⋙ r')
                   → l ≈ l'
                   → r ≈ r'
                   → right b≤x l⋙r ≈ right b'≤x' l'⋙r'

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
-- Plump ordinals as presented by Shulman
-- https://homotopytypetheory.org/2014/02/22/surreals-plump-ordinals/
--
-- Implementation based on an implementation of Aczel sets by Andreas Abel.
module Ordinal.Shulman where

open import Data.Sum using ([_,_]′)
open import Induction.WellFounded as WfRec using (Acc ; acc ; WellFounded)
open import Level using (Lift ; lift ; lower)
open import Relation.Binary using (IsEquivalence)
open import Relation.Nullary using (¬_)

open import Ordinal.HoTT using (IsOrdinal ; IsExtensional ; _↔_ ; forth ; back)
open import Util.Prelude

-- Definition of ordinals, equality, orders
------------------------------------------------------------------------

-- Ordinals are infinitely branching well-founded trees.
-- The branching type is given at each node.

data Ord ℓ : Set (lsuc ℓ) where
  limSuc : (I : Set ℓ) (els : I → Ord ℓ) → Ord ℓ

-- Branching type

Br : ∀ {ℓ} (a : Ord ℓ) → Set ℓ
Br (limSuc I _) = I

-- Elements

els : ∀ {ℓ} (a : Ord ℓ) (i : Br a) → Ord ℓ
els (limSuc _ f) = f

syntax els a i = a ` i

lift-Ord : ∀ {a ℓ} → Ord ℓ → Ord (a ⊔ℓ ℓ)
lift-Ord {a} (limSuc I f) = limSuc (Lift a I) λ i → lift-Ord {a} (f (lower i))

-- Equality and orders

mutual
  _<_ : ∀ {ℓ} (a b : Ord ℓ) → Set ℓ
  a < limSuc _ f = ∃[ i ] (a ≤ f i)

  _≤_  : ∀ {ℓ} (a b : Ord ℓ) → Set ℓ
  limSuc _ f ≤ b = ∀ i → f i < b

_≅_ : ∀ {ℓ} (a b : Ord ℓ) → Set ℓ
a ≅ b = (a ≤ b) × (b ≤ a)

_≮_ : ∀ {ℓ} (a b : Ord ℓ) → Set ℓ
a ≮ b = ¬ (a < b)

_≇_ : ∀ {ℓ} (a b : Ord ℓ) → Set ℓ
a ≇ b = ¬ (a ≅ b)

-- Intro/Elim rules for </≤ (for nicer proofs below)

<-intro : ∀ {ℓ} {a b : Ord ℓ} → ∃[ i ] (a ≤ (b ` i)) → a < b
<-intro {b = limSuc I f} p = p

<-elim : ∀ {ℓ} {a b : Ord ℓ} → a < b → ∃[ i ] (a ≤ (b ` i))
<-elim {b = limSuc I f} p = p

≤-intro : ∀ {ℓ} {a b : Ord ℓ} → (∀ i → (a ` i) < b) → a ≤ b
≤-intro {a = limSuc I f} p = p

≤-elim : ∀ {ℓ} {a b : Ord ℓ} → a ≤ b → (∀ i → (a ` i) < b)
≤-elim {a = limSuc I f} p = p

-- Reflexivity

≤-refl : ∀ {ℓ} {a : Ord ℓ} → a ≤ a
≤-refl {a = limSuc _ f} i = i , ≤-refl

≅-refl : ∀ {ℓ} {a : Ord ℓ} → a ≅ a
≅-refl = ≤-refl , ≤-refl

-- < implies ≤

<→≤ : ∀ {ℓ} {a b : Ord ℓ} → a < b → a ≤ b
<→≤ {ℓ} {limSuc A fa} {limSuc B fb} (i , fa<fb) j = i , <→≤ (fa<fb j)

-- Transitivity

mutual
  <-trans-≤ : ∀ {ℓ} {a b c : Ord ℓ} → a < b → b ≤ c → a < c
  <-trans-≤ {b = limSuc _ f} (i , p) h = ≤-trans-< p (h i)

  ≤-trans-< : ∀ {ℓ} {a b c : Ord ℓ} → a ≤ b → b < c → a < c
  ≤-trans-< {c = limSuc _ f} p (i , q) = i , ≤-trans p q

  ≤-trans : ∀ {ℓ} {a b c : Ord ℓ} → a ≤ b → b ≤ c → a ≤ c
  ≤-trans {a = limSuc _ f} h q i = <-trans-≤ (h i) q

<-trans : ∀ {ℓ} {a b c : Ord ℓ} → a < b → b < c → a < c
<-trans {ℓ} {a} {b} {limSuc C fc} a<b (i , b≤fci) = i , <→≤ (<-trans-≤ a<b b≤fci)

≅-trans : ∀ {ℓ} {a b c : Ord ℓ} (d : a ≅ b) (e : b ≅ c) → a ≅ c
≅-trans (p , p′) (q , q′) = ≤-trans p q , ≤-trans q′ p′

-- Symmetry

≅-sym : ∀ {ℓ} {a b : Ord ℓ} (p : a ≅ b) → b ≅ a
≅-sym (p , p′) = p′ , p

-- ≅ is an equivalence relation.

≅-equiv : ∀ {ℓ} → IsEquivalence (_≅_ {ℓ})
≅-equiv = record
  { refl = ≅-refl
  ; sym = ≅-sym
  ; trans = ≅-trans
  }

-- < is 'extensional'.

<-ext-≤ : ∀ {ℓ} {a b : Ord ℓ} → (∀ c → c < a → c < b) → a ≤ b
<-ext-≤ {a = limSuc I els} p i = p (els i) (i , ≤-refl)

<-ext : ∀ {ℓ} → IsExtensional {ℓ} _≅_ _<_
<-ext p = <-ext-≤ (λ c → forth (p c)) , <-ext-≤ (λ c → back (p c))

-- Alternative interpretation of ≤ in terms of <

≤-intro′ : ∀ {ℓ} {b c : Ord ℓ} → (∀ {a} → a < b → a < c) → b ≤ c
≤-intro′ {b = limSuc _ f} cast i = cast (i , ≤-refl)

≤-elim′ : ∀ {ℓ} {b c : Ord ℓ} → b ≤ c → ∀ {a} → a < b → a < c
≤-elim′ b≤c a<b = <-trans-≤ a<b b≤c

-- Compatibility of ≤ with ≅

≤-congˡ : ∀ {ℓ} {a b c : Ord ℓ} → a ≅ b → a ≤ c → b ≤ c
≤-congˡ {ℓ}  (a≤b , b≤a) a≤c = ≤-trans b≤a a≤c

≤-congʳ : ∀ {ℓ} {a b c : Ord ℓ} → b ≅ c → a ≤ b → a ≤ c
≤-congʳ (b≤c , c≤b) a≤b = ≤-trans a≤b b≤c

-- Compatibility of < with ≅

<-congʳ : ∀ {ℓ} {a b c : Ord ℓ} → b ≅ c → a < b → a < c
<-congʳ (b≤c , c≤b) a<b = <-trans-≤ a<b b≤c

<-congˡ : ∀ {ℓ} {a b c : Ord ℓ} → a ≅ b → a < c → b < c
<-congˡ (a≤b , b≤a) a<c = ≤-trans-< b≤a a<c

-- Foundation: a ≤ b implies b ≮ a

≤-found : ∀ {ℓ} {a b : Ord ℓ} → a ≤ b → b ≮ a
≤-found {ℓ} {limSuc A fa} {b} a≤b (i , b≤fai) = ≤-found b≤fai (a≤b i)

-- Thus, a ≮ a.

<-irr : ∀ {ℓ} {a : Ord ℓ} → a ≮ a
<-irr = ≤-found ≤-refl

-- Predicates over ordinals (need to respect equality)

IsPred : ∀ {ℓ} (P : Ord ℓ → Set ℓ) → Set (lsuc ℓ)
IsPred {ℓ} P = {a b : Ord ℓ} → a ≅ b → P a → P b

record Pred ℓ : Set (lsuc ℓ) where
  constructor pred
  field
    _!_  : Ord ℓ → Set ℓ
    resp : IsPred _!_

open Pred

-- <-induction.

<-acc-≤ : ∀ {ℓ} {a b : Ord ℓ} → a ≤ b → Acc _<_ b → Acc _<_ a
<-acc-≤ {ℓ} {limSuc A fa} {b} fai<b (acc rs) = acc λ where
  x (i , x≤fai) → rs x (≤-trans-< x≤fai (fai<b i))

<-wf : ∀ {ℓ} → WellFounded (_<_ {ℓ})
<-wf (limSuc I f) = acc λ { x (i , x≤fi) → <-acc-≤ x≤fi (<-wf (f i)) }

<-ind : ∀ {ℓ ℓ′} (P : Ord ℓ → Set ℓ′)
  → (∀ a → (∀ b → b < a → P b) → P a)
  → ∀ a → P a
<-ind = WfRec.All.wfRec <-wf _

-- Ordinals are ordinals (in the sense of the HoTT book).

isOrdinal : ∀ {ℓ} → IsOrdinal (Ord ℓ) ℓ ℓ
isOrdinal = record
  { _≈_ = _≅_
  ; ≈-equiv = ≅-equiv
  ; _<_ = _<_
  ; <-wf = <-wf
  ; <-ext = <-ext
  ; <-trans = <-trans
  }

-- Constructions on ordinals
------------------------------------------------------------------------

-- Zero

ozero : ∀ {ℓ} → Ord ℓ
ozero {ℓ} = limSuc (Lift ℓ ⊥) λ()

-- Successor?

osuc : ∀ {ℓ} → Ord ℓ → Ord ℓ
osuc {ℓ} a = limSuc (Lift ℓ ⊤) λ _ → a

-- Lo and behold!
osuc-mon-< : ∀ {ℓ} {a b : Ord ℓ} → a < b → osuc a < osuc b
osuc-mon-< a<b = _ , λ _ → a<b

osuc-mon-≤ : ∀ {ℓ} {a b : Ord ℓ} → a ≤ b → osuc a ≤ osuc b
osuc-mon-≤ a≤b _ = _ , a≤b

osuc-cong : ∀ {ℓ} {a b : Ord ℓ} → a ≅ b → osuc a ≅ osuc b
osuc-cong (a≤b , b≤a) = osuc-mon-≤ a≤b , osuc-mon-≤ b≤a

-- Maximum/Supremum

_⊔_ : ∀ {ℓ} (a b : Ord ℓ) → Ord ℓ
a ⊔ b = limSuc (_ ⊎ _) λ where
  (inj₁ i) → a ` i
  (inj₂ j) → b ` j

⊔-introˡ : ∀ {ℓ} a {b c : Ord ℓ} → a < b → a < (b ⊔ c)
⊔-introˡ a {limSuc _ f} (i , e) = inj₁ i , e

⊔-introʳ : ∀ {ℓ} a {b c : Ord ℓ} → a < c → a < (b ⊔ c)
⊔-introʳ a {c = limSuc _ g} (i , e) = inj₂ i , e

⊔-≤-introˡ : ∀ {ℓ} a {b c : Ord ℓ} → a ≤ b → a ≤ (b ⊔ c)
⊔-≤-introˡ a a≤b = ≤-intro λ i → ⊔-introˡ _ (≤-elim a≤b i)

⊔-≤-introˡ′ : ∀ {ℓ} {a : Ord ℓ} b → a ≤ (a ⊔ b)
⊔-≤-introˡ′ b = ⊔-≤-introˡ _ ≤-refl

⊔-≤-introʳ : ∀ {ℓ} a {b c : Ord ℓ} → a ≤ c → a ≤ (b ⊔ c)
⊔-≤-introʳ a a≤c = ≤-intro λ i → ⊔-introʳ _ (≤-elim a≤c i)

⊔-≤-introʳ′ : ∀ {ℓ} a {b : Ord ℓ} → b ≤ (a ⊔ b)
⊔-≤-introʳ′ a = ⊔-≤-introʳ _ ≤-refl

⊔-elim : ∀ {ℓ} {a b c : Ord ℓ} → c < (a ⊔ b) → (c < a) ⊎ (c < b)
⊔-elim {a = limSuc _ f}                  (inj₁ i , e) = inj₁ (i , e)
⊔-elim {a = limSuc _ _} {b = limSuc _ g} (inj₂ i , e) = inj₂ (i , e)

⊔-case : ∀ {ℓ} {a b c : Ord ℓ}
  → c < (a ⊔ b)
  → ∀ {q} {Q : Set q}
  → (c < a → Q)
  → (c < b → Q) → Q
⊔-case p left right = [ left , right ]′ (⊔-elim p)

⊔-split : ∀ {ℓ q} {Q : Set q} {a b c : Ord ℓ}
  → (c < a → Q)
  → (c < b → Q)
  → c < (a ⊔ b) → Q
⊔-split left right p = ⊔-case p left right

⊔-mon : ∀ {ℓ} {a a′ b b′ : Ord ℓ} → a ≤ a′ → b ≤ b′ → (a ⊔ b) ≤ (a′ ⊔ b′)
⊔-mon a≤a′ b≤b′ = ≤-intro′
  (⊔-split
    (λ c<a → ⊔-introˡ _ (≤-elim′ a≤a′ c<a))
    (λ c<b → ⊔-introʳ _ (≤-elim′ b≤b′ c<b)))

⊔-cong : ∀ {ℓ} {a a′ b b′ : Ord ℓ} → a ≅ a′ → b ≅ b′ → (a ⊔ b) ≅ (a′ ⊔ b′)
⊔-cong (a≤a′ , a′≤a) (b≤b′ , b′≤b) = ⊔-mon a≤a′ b≤b′ , ⊔-mon a′≤a b′≤b

⊔-<→LEM : ∀ {ℓ}
  → ({α α′ β : Ord ℓ} → α < β → α′ < β → (α ⊔ α′) < β)
  → (A : Set ℓ) → A ⊎ ¬ A
⊔-<→LEM {ℓ} p A
  = let α<β : α < β
        α<β = lift true , ≤-refl
        α′<β : α′ < β
        α′<β = lift false , ≤-refl in
    go (p α<β α′<β)
  where
    oone = osuc ozero
    α = limSuc A λ _ → oone
    α′ = oone
    β = limSuc (Lift ℓ Bool) λ { (lift true) → α ; (lift false) → α′ }

    go : (α ⊔ α′) < β → A ⊎ ¬ A
    go (lift true , α⊔α′≤α) = inj₁ (proj₁ (α⊔α′≤α (inj₂ _)))
    go (lift false , α⊔α′≤α′) = inj₂ λ a → lower (proj₁ (proj₂ (α⊔α′≤α′ (inj₁ a)) _))

-- Supremum of a family of ordinals

⨆ᶠ : ∀ {ℓ} {I : Set ℓ} (f : I → Ord ℓ) → Ord ℓ
⨆ᶠ {ℓ} {I} f = limSuc (∃[ i ] Br (f i)) λ { (i , j) → f i ` j }

⨆ᶠ-intro : ∀ {ℓ} {I : Set ℓ} (f : I → Ord ℓ) {c : Ord ℓ} {i : I}
  → c < f i → c < ⨆ᶠ f
⨆ᶠ-intro f {c} {i} c<fi
  = let j , c≤ = <-elim c<fi in
    (i , j) , c≤

⨆ᶠ-elim : ∀ {ℓ} {I : Set ℓ} (f : I → Ord ℓ) {c : Ord ℓ}
  → c < ⨆ᶠ f → ∃[ i ] (c < f i)
⨆ᶠ-elim _ ((i , j) , e) = i , <-intro (j , e)

⨆ᶠ-mon : ∀ {ℓ} {I : Set ℓ} {f f′ : I → Ord ℓ}
  → (∀ i → f i ≤ f′ i) → ⨆ᶠ f ≤ ⨆ᶠ f′
⨆ᶠ-mon {f = f} {f′} p = ≤-intro′ λ c<⨆ᶠf →
  let i , q = ⨆ᶠ-elim f c<⨆ᶠf in
  ⨆ᶠ-intro f′ (≤-elim′ (p i) q)

⨆ᶠ-cong : ∀ {ℓ} {I : Set ℓ} {f f′ : I → Ord ℓ}
  → (∀ i → f i ≅ f′ i) → ⨆ᶠ f ≅ ⨆ᶠ f′
⨆ᶠ-cong p = ⨆ᶠ-mon (λ i → proj₁ (p i))
          , ⨆ᶠ-mon (λ i → proj₂ (p i))

-- Supremum of all ordinals smaller than some given ordinal

⨆ : ∀ {ℓ} (a : Ord ℓ) → Ord ℓ
⨆ (limSuc _ f) = ⨆ᶠ f

⨆-intro : ∀ {ℓ} {a b : Ord ℓ} → b < a → b ≤ ⨆ a
⨆-intro {a = limSuc A fa} {b = limSuc B fb} (i , b≤fi) = ≤-intro λ j →
  let k , p = <-elim (b≤fi j) in _ , p

⨆-elim : ∀ {ℓ} {a c : Ord ℓ} → c < ⨆ a → ∃[ b ] ((b < a) × (c < b))
⨆-elim {a = limSuc _ f} ((i , j) , c≤) = f i , (i , ≤-refl) , <-intro (_ , c≤)

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


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

open import Cubical.Algebra.Monoid.Base public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
open import Oscar.Prelude

module Oscar.Class.Injectivity where

module _ where

  module _ -- Arity=1
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔬₂} (𝔒₂ : 𝔒₁ → Ø 𝔬₂)
    where
    𝓲njection₁ = (x : 𝔒₁) → 𝔒₂ x
    record 𝓘njection₁ : Ø 𝔬₁ ∙̂ 𝔬₂ where field injection₁ : 𝓲njection₁
    open 𝓘njection₁ ⦃ … ⦄ public
    module _
      {ℓ₂} (_∼₂_ : ∀ {x₁ x₂} → 𝔒₂ x₁ → 𝔒₂ x₂ → Ø ℓ₂)
      {ℓ₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø ℓ₁)
      where
      record [𝓘njectivity₁] : Ø₀ where
        no-eta-equality
        constructor ∁
      module _
        ⦃ _ : 𝓘njection₁ ⦄
        where
        𝓲njectivity₁ = ∀ {x₁ x₂} → injection₁ x₁ ∼₂ injection₁ x₂ → x₁ ∼₁ x₂
        record 𝓘njectivity₁ ⦃ _ : [𝓘njectivity₁] ⦄ : Ø 𝔬₁ ∙̂ 𝔬₂ ∙̂ ℓ₁ ∙̂ ℓ₂ where field injectivity₁ : 𝓲njectivity₁
        open 𝓘njectivity₁ ⦃ … ⦄ public

  injectivity₁[_] : ∀
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔬₂} {𝔒₂ : 𝔒₁ → Ø 𝔬₂}
    {ℓ₂} {_∼₂_ : ∀ {x₁ x₂} → 𝔒₂ x₁ → 𝔒₂ x₂ → Ø ℓ₂}
    {ℓ₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø ℓ₁)
    ⦃ _ : 𝓘njection₁ (λ (x : 𝔒₁) → 𝔒₂ x) ⦄
    ⦃ _ : [𝓘njectivity₁] (λ (x : 𝔒₁) → 𝔒₂ x) _∼₂_ _∼₁_ ⦄
    ⦃ _ : 𝓘njectivity₁ (λ (x : 𝔒₁) → 𝔒₂ x) _∼₂_ _∼₁_ ⦄
    → 𝓲njectivity₁ (λ (x : 𝔒₁) → 𝔒₂ x) _∼₂_ _∼₁_
  injectivity₁[ _ ] = injectivity₁

  module _ -- Arity=2
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔬₂} {𝔒₂ : 𝔒₁ → Ø 𝔬₂}
    {𝔬₃} (𝔒₃ : ∀ x₁ → 𝔒₂ x₁ → Ø 𝔬₃)
    where
    𝓲njection₂ = ∀ x₁ → (x₂ : 𝔒₂ x₁) → 𝔒₃ _ x₂
    record 𝓘njection₂ : Ø 𝔬₁ ∙̂ 𝔬₂ ∙̂ 𝔬₃ where
      constructor ∁
      field injection₂ : 𝓲njection₂
    open 𝓘njection₂ ⦃ … ⦄ public
    module _ -- Fixed=0
      {ℓ₃} (_∼₃_ : ∀ {x₁ x₂} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} → 𝔒₃ _ y₁ → 𝔒₃ _ y₂ → Ø ℓ₃)
      where
      module _ -- Var=1
        {ℓ₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø ℓ₁)
        where
        record [𝓘njectivity₂,₀,₁] : Ø₀ where
          no-eta-equality
          constructor ∁
        module _
          ⦃ _ : 𝓘njection₂ ⦄
          where
          𝓲njectivity₂,₀,₁ = ∀ {x₁ x₂} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} → injection₂ _ y₁ ∼₃ injection₂ _ y₂ → x₁ ∼₁ x₂
          record 𝓘njectivity₂,₀,₁ ⦃ _ : [𝓘njectivity₂,₀,₁] ⦄ : Ø 𝔬₁ ∙̂ 𝔬₂ ∙̂ 𝔬₃ ∙̂ ℓ₁ ∙̂ ℓ₃ where field injectivity₂,₀,₁ : 𝓲njectivity₂,₀,₁
          open 𝓘njectivity₂,₀,₁ ⦃ … ⦄ public
      module _ -- Var=2
        {ℓ₂} (_∼₂_ : ∀ {x₁ x₂} → 𝔒₂ x₁ → 𝔒₂ x₂ → Ø ℓ₂)
        where
        record [𝓘njectivity₂,₀,₂] : Ø₀ where
          no-eta-equality
          constructor ∁
        module _
          ⦃ _ : 𝓘njection₂ ⦄
          where
          𝓲njectivity₂,₀,₂ = ∀ {x₁ x₂ : 𝔒₁} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} → injection₂ _ y₁ ∼₃ injection₂ _ y₂ → y₁ ∼₂ y₂
          record 𝓘njectivity₂,₀,₂ ⦃ _ : [𝓘njectivity₂,₀,₂] ⦄ : Ø 𝔬₁ ∙̂ 𝔬₂ ∙̂ 𝔬₃ ∙̂ ℓ₂ ∙̂ ℓ₃ where field injectivity₂,₀,₂ : 𝓲njectivity₂,₀,₂
          open 𝓘njectivity₂,₀,₂ ⦃ … ⦄ public
    module _ -- Fixed=1
      {ℓ₃} (_∼₃_ : ∀ {x} {y₁ y₂ : 𝔒₂ x} → 𝔒₃ _ y₁ → 𝔒₃ _ y₂ → Ø ℓ₃)
      {ℓ₂} (_∼₂_ : ∀ {x} → 𝔒₂ x → 𝔒₂ x → Ø ℓ₂)
      where
      record [𝓘njectivity₂,₁] : Ø₀ where
        no-eta-equality
        constructor ∁
      module _
        ⦃ _ : 𝓘njection₂ ⦄
        where
        𝓲njectivity₂,₁ = ∀ (x : 𝔒₁) {y₁ y₂ : 𝔒₂ x} → injection₂ _ y₁ ∼₃ injection₂ _ y₂ → y₁ ∼₂ y₂
        record 𝓘njectivity₂,₁ ⦃ _ : [𝓘njectivity₂,₁] ⦄ : Ø 𝔬₁ ∙̂ 𝔬₂ ∙̂ 𝔬₃ ∙̂ ℓ₂ ∙̂ ℓ₃ where field injectivity₂,₁ : 𝓲njectivity₂,₁
        open 𝓘njectivity₂,₁ ⦃ … ⦄ public

  injectivity₂,₀,₁[_] : ∀
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔬₂} {𝔒₂ : 𝔒₁ → Ø 𝔬₂}
    {𝔬₃} {𝔒₃ : ∀ x₁ → 𝔒₂ x₁ → Ø 𝔬₃}
    {ℓ₃} {_∼₃_ : ∀ {x₁ x₂} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} → 𝔒₃ _ y₁ → 𝔒₃ _ y₂ → Ø ℓ₃}
    {ℓ₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø ℓ₁)
    ⦃ _ : 𝓘njection₂ 𝔒₃ ⦄
    ⦃ _ : [𝓘njectivity₂,₀,₁] 𝔒₃ _∼₃_ _∼₁_ ⦄
    ⦃ _ : 𝓘njectivity₂,₀,₁ 𝔒₃ _∼₃_ _∼₁_ ⦄
    → 𝓲njectivity₂,₀,₁ 𝔒₃ _∼₃_ _∼₁_
  injectivity₂,₀,₁[ _ ] = injectivity₂,₀,₁

  injectivity₂,₀,₂[_] : ∀
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔬₂} {𝔒₂ : 𝔒₁ → Ø 𝔬₂}
    {𝔬₃} {𝔒₃ : ∀ x₁ → 𝔒₂ x₁ → Ø 𝔬₃}
    {ℓ₃} {_∼₃_ : ∀ {x₁ x₂} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} → 𝔒₃ _ y₁ → 𝔒₃ _ y₂ → Ø ℓ₃}
    {ℓ₂} (_∼₂_ : ∀ {x₁ x₂} → 𝔒₂ x₁ → 𝔒₂ x₂ → Ø ℓ₂)
    ⦃ _ : 𝓘njection₂ 𝔒₃ ⦄
    ⦃ _ : [𝓘njectivity₂,₀,₂] 𝔒₃ _∼₃_ _∼₂_ ⦄
    ⦃ _ : 𝓘njectivity₂,₀,₂ 𝔒₃ _∼₃_ _∼₂_ ⦄
    → 𝓲njectivity₂,₀,₂ 𝔒₃ _∼₃_ _∼₂_
  injectivity₂,₀,₂[ _ ] = injectivity₂,₀,₂

  injectivity₂,₁[_] : ∀
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔬₂} {𝔒₂ : 𝔒₁ → Ø 𝔬₂}
    {𝔬₃} {𝔒₃ : ∀ x₁ → 𝔒₂ x₁ → Ø 𝔬₃}
    {ℓ₃} {_∼₃_ : ∀ {x} {y₁ y₂ : 𝔒₂ x} → 𝔒₃ _ y₁ → 𝔒₃ _ y₂ → Ø ℓ₃}
    {ℓ₂} (_∼₂_ : ∀ {x} → 𝔒₂ x → 𝔒₂ x → Ø ℓ₂)
    ⦃ _ : [𝓘njectivity₂,₁] 𝔒₃ _∼₃_ _∼₂_ ⦄
    ⦃ _ : 𝓘njection₂ 𝔒₃ ⦄
    ⦃ _ : 𝓘njectivity₂,₁ 𝔒₃ _∼₃_ _∼₂_ ⦄
    → 𝓲njectivity₂,₁ 𝔒₃ _∼₃_ _∼₂_
  injectivity₂,₁[ _ ] = injectivity₂,₁

  module _ -- Arity=3
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔬₂} {𝔒₂ : 𝔒₁ → Ø 𝔬₂}
    {𝔬₃} {𝔒₃ : ∀ x₁ → 𝔒₂ x₁ → Ø 𝔬₃}
    {𝔬₄} (𝔒₄ : ∀ x₁ → (x₂ : 𝔒₂ x₁) → 𝔒₃ _ x₂ → Ø 𝔬₄)
    where
    𝓲njection₃ = ∀ x₁ → (x₂ : 𝔒₂ x₁) → (x₃ : 𝔒₃ _ x₂) → 𝔒₄ _ _ x₃
    record 𝓘njection₃ : Ø 𝔬₁ ∙̂ 𝔬₂ ∙̂ 𝔬₃ ∙̂ 𝔬₄ where
      constructor ∁
      field injection₃ : 𝓲njection₃
    open 𝓘njection₃ ⦃ … ⦄ public
    module _ -- Fixed=0
      {ℓ₄} (_∼₄_ : ∀ {x₁ x₂} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} {z₁ : 𝔒₃ _ y₁} {z₂ : 𝔒₃ _ y₂} → 𝔒₄ _ _ z₁ → 𝔒₄ _ _ z₂ → Ø ℓ₄)
      where
      module _ -- Var=1
        {ℓ₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø ℓ₁)
        where
        record [𝓘njectivity₃,₀,₁] : Ø₀ where
          no-eta-equality
          constructor ∁
        module _
          ⦃ _ : 𝓘njection₃ ⦄
          where
          𝓲njectivity₃,₀,₁ = ∀ {x₁ x₂} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} {z₁ : 𝔒₃ _ y₁} {z₂ : 𝔒₃ _ y₂} → injection₃ _ _ z₁ ∼₄ injection₃ _ _ z₂ → x₁ ∼₁ x₂
          record 𝓘njectivity₃,₀,₁ ⦃ _ : [𝓘njectivity₃,₀,₁] ⦄ : Ø 𝔬₁ ∙̂ 𝔬₂ ∙̂ 𝔬₃ ∙̂ 𝔬₄ ∙̂ ℓ₁ ∙̂ ℓ₄ where field injectivity₃,₀,₁ : 𝓲njectivity₃,₀,₁
          open 𝓘njectivity₃,₀,₁ ⦃ … ⦄ public
      module _ -- Var=2
        {ℓ₂} (_∼₂_ : ∀ {x₁ x₂} → 𝔒₂ x₁ → 𝔒₂ x₂ → Ø ℓ₂)
        where
        record [𝓘njectivity₃,₀,₂] : Ø₀ where
          no-eta-equality
          constructor ∁
        module _
          ⦃ _ : 𝓘njection₃ ⦄
          where
          𝓲njectivity₃,₀,₂ = ∀ {x₁ x₂ : 𝔒₁} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} {z₁ : 𝔒₃ _ y₁} {z₂ : 𝔒₃ _ y₂} → injection₃ _ _ z₁ ∼₄ injection₃ _ _ z₂ → y₁ ∼₂ y₂
          record 𝓘njectivity₃,₀,₂ ⦃ _ : [𝓘njectivity₃,₀,₂] ⦄ : Ø 𝔬₁ ∙̂ 𝔬₂ ∙̂ 𝔬₃ ∙̂ ℓ₂ ∙̂ ℓ₄ where field injectivity₃,₀,₂ : 𝓲njectivity₃,₀,₂
          open 𝓘njectivity₃,₀,₂ ⦃ … ⦄ public

  injectivity₃,₀,₁[_] : ∀
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔬₂} {𝔒₂ : 𝔒₁ → Ø 𝔬₂}
    {𝔬₃} {𝔒₃ : ∀ x₁ → 𝔒₂ x₁ → Ø 𝔬₃}
    {𝔬₄} {𝔒₄ : ∀ x₁ → (x₂ : 𝔒₂ x₁) → 𝔒₃ _ x₂ → Ø 𝔬₄}
    {ℓ₄} {_∼₄_ : ∀ {x₁ x₂} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} {z₁ : 𝔒₃ _ y₁} {z₂ : 𝔒₃ _ y₂} → 𝔒₄ _ _ z₁ → 𝔒₄ _ _ z₂ → Ø ℓ₄}
    {ℓ₁} (_∼₁_ : 𝔒₁ → 𝔒₁ → Ø ℓ₁)
    ⦃ _ : [𝓘njectivity₃,₀,₁] 𝔒₄ _∼₄_ _∼₁_ ⦄
    ⦃ _ : 𝓘njection₃ 𝔒₄ ⦄
    ⦃ _ : 𝓘njectivity₃,₀,₁ 𝔒₄ _∼₄_ _∼₁_ ⦄
    → 𝓲njectivity₃,₀,₁ 𝔒₄ _∼₄_ _∼₁_
  injectivity₃,₀,₁[ _ ] = injectivity₃,₀,₁

  injectivity₃,₀,₂[_] : ∀
    {𝔬₁} {𝔒₁ : Ø 𝔬₁}
    {𝔬₂} {𝔒₂ : 𝔒₁ → Ø 𝔬₂}
    {𝔬₃} {𝔒₃ : ∀ x₁ → 𝔒₂ x₁ → Ø 𝔬₃}
    {𝔬₄} {𝔒₄ : ∀ x₁ → (x₂ : 𝔒₂ x₁) → 𝔒₃ _ x₂ → Ø 𝔬₄}
    {ℓ₄} {_∼₄_ : ∀ {x₁ x₂} {y₁ : 𝔒₂ x₁} {y₂ : 𝔒₂ x₂} {z₁ : 𝔒₃ _ y₁} {z₂ : 𝔒₃ _ y₂} → 𝔒₄ _ _ z₁ → 𝔒₄ _ _ z₂ → Ø ℓ₄}
    {ℓ₂} (_∼₂_ : ∀ {x₁ x₂} → 𝔒₂ x₁ → 𝔒₂ x₂ → Ø ℓ₂)
    ⦃ _ : [𝓘njectivity₃,₀,₂] 𝔒₄ _∼₄_ _∼₂_ ⦄
    ⦃ _ : 𝓘njection₃ 𝔒₄ ⦄
    ⦃ _ : 𝓘njectivity₃,₀,₂ 𝔒₄ _∼₄_ _∼₂_ ⦄
    → 𝓲njectivity₃,₀,₂ 𝔒₄ _∼₄_ _∼₂_
  injectivity₃,₀,₂[ _ ] = injectivity₃,₀,₂


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Example of a Quotient: ℤ as (ℕ × ℕ / ∼)
------------------------------------------------------------------------

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

module Relation.Binary.HeterogeneousEquality.Quotients.Examples where

open import Relation.Binary.HeterogeneousEquality.Quotients
open import Level using (0ℓ)
open import Relation.Binary
open import Relation.Binary.HeterogeneousEquality hiding (isEquivalence)
import Relation.Binary.PropositionalEquality as ≡
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Function
open ≅-Reasoning

ℕ² = ℕ × ℕ

_∼_ : ℕ² → ℕ² → Set
(x , y) ∼ (x' , y') = x + y' ≅ x' + y

infix 10 _∼_

∼-trans : ∀ {i j k} → i ∼ j → j ∼ k → i ∼ k
∼-trans {x₁ , y₁} {x₂ , y₂} {x₃ , y₃} p q =
  ≡-to-≅ $ +-cancelˡ-≡ y₂ $ ≅-to-≡ $ begin
  y₂ + (x₁ + y₃) ≡⟨ ≡.sym (+-assoc y₂ x₁ y₃) ⟩
  y₂ + x₁ + y₃   ≡⟨ ≡.cong (_+ y₃) (+-comm y₂ x₁) ⟩
  x₁ + y₂ + y₃   ≅⟨ cong (_+ y₃) p ⟩
  x₂ + y₁ + y₃   ≡⟨ ≡.cong (_+ y₃) (+-comm x₂ y₁) ⟩
  y₁ + x₂ + y₃   ≡⟨ +-assoc y₁ x₂ y₃ ⟩
  y₁ + (x₂ + y₃) ≅⟨ cong (y₁ +_) q ⟩
  y₁ + (x₃ + y₂) ≡⟨ +-comm y₁ (x₃ + y₂) ⟩
  x₃ + y₂ + y₁   ≡⟨ ≡.cong (_+ y₁) (+-comm x₃ y₂) ⟩
  y₂ + x₃ + y₁   ≡⟨ +-assoc y₂ x₃ y₁ ⟩
  y₂ + (x₃ + y₁) ∎

∼-isEquivalence : IsEquivalence _∼_
∼-isEquivalence = record
  { refl  = refl
  ; sym   = sym
  ; trans = λ {i} {j} {k} → ∼-trans {i} {j} {k}
  }

ℕ²-∼-setoid : Setoid 0ℓ 0ℓ
ℕ²-∼-setoid = record { isEquivalence = ∼-isEquivalence }

module Integers (quot : Quotients 0ℓ 0ℓ) where

  Int : Quotient ℕ²-∼-setoid
  Int = quot _

  open Quotient Int renaming (Q to ℤ)

  _+²_ : ℕ² → ℕ² → ℕ²
  (x₁ , y₁) +² (x₂ , y₂) = x₁ + x₂ , y₁ + y₂

  +²-cong : ∀{a b a' b'} → a ∼ a' → b ∼ b' → a +² b ∼ a' +² b'
  +²-cong {a₁ , b₁} {c₁ , d₁} {a₂ , b₂} {c₂ , d₂} ab∼cd₁ ab∼cd₂ = begin
    (a₁ + c₁) + (b₂ + d₂) ≡⟨ ≡.cong (_+ (b₂ + d₂)) (+-comm a₁ c₁) ⟩
    (c₁ + a₁) + (b₂ + d₂) ≡⟨ +-assoc c₁ a₁ (b₂ + d₂) ⟩
    c₁ + (a₁ + (b₂ + d₂)) ≡⟨ ≡.cong (c₁ +_) (≡.sym (+-assoc a₁ b₂ d₂)) ⟩
    c₁ + (a₁ + b₂ + d₂)   ≅⟨ cong (λ n → c₁ + (n + d₂)) ab∼cd₁ ⟩
    c₁ + (a₂ + b₁ + d₂)   ≡⟨ ≡.cong (c₁ +_) (+-assoc a₂ b₁ d₂) ⟩
    c₁ + (a₂ + (b₁ + d₂)) ≡⟨ ≡.cong (λ n → c₁ + (a₂ + n)) (+-comm b₁ d₂) ⟩
    c₁ + (a₂ + (d₂ + b₁)) ≡⟨ ≡.sym (+-assoc c₁ a₂ (d₂ + b₁)) ⟩
    (c₁ + a₂) + (d₂ + b₁) ≡⟨ ≡.cong (_+ (d₂ + b₁)) (+-comm c₁ a₂) ⟩
    (a₂ + c₁) + (d₂ + b₁) ≡⟨ +-assoc a₂ c₁ (d₂ + b₁) ⟩
    a₂ + (c₁ + (d₂ + b₁)) ≡⟨ ≡.cong (a₂ +_) (≡.sym (+-assoc c₁ d₂ b₁)) ⟩
    a₂ + (c₁ + d₂ + b₁)   ≅⟨ cong (λ n → a₂ + (n + b₁)) ab∼cd₂ ⟩
    a₂ + (c₂ + d₁ + b₁)   ≡⟨ ≡.cong (a₂ +_) (+-assoc c₂ d₁ b₁) ⟩
    a₂ + (c₂ + (d₁ + b₁)) ≡⟨ ≡.cong (λ n → a₂ + (c₂ + n)) (+-comm d₁ b₁) ⟩
    a₂ + (c₂ + (b₁ + d₁)) ≡⟨ ≡.sym (+-assoc a₂ c₂ (b₁ + d₁)) ⟩
    (a₂ + c₂) + (b₁ + d₁) ∎

  module _ (ext : ∀ {a b} {A : Set a} {B₁ B₂ : A → Set b} {f₁ : ∀ a → B₁ a}
                  {f₂ : ∀ a → B₂ a} → (∀ a → f₁ a ≅ f₂ a) → f₁ ≅ f₂) where

    _+ℤ_ : ℤ → ℤ → ℤ
    _+ℤ_ = Properties₂.lift₂ ext Int Int (λ i j → abs (i +² j))
         $ λ {a} {b} {c} p p' → compat-abs (+²-cong {a} {b} {c} p p')

    zero² : ℕ²
    zero² = 0 , 0

    zeroℤ : ℤ
    zeroℤ = abs zero²

    +²-identityʳ : (i : ℕ²) → (i +² zero²) ∼ i
    +²-identityʳ (x , y) = begin
      (x + 0) + y ≡⟨ ≡.cong (_+ y) (+-identityʳ x) ⟩
      x + y       ≡⟨ ≡.cong (x +_) (≡.sym (+-identityʳ y)) ⟩
      x + (y + 0) ∎

    +ℤ-on-abs≅abs-+₂ : ∀ a b → abs a +ℤ abs b ≅ abs (a +² b)
    +ℤ-on-abs≅abs-+₂ = Properties₂.lift₂-conv ext Int Int _
                     $ λ {a} {b} {c} p p′ → compat-abs (+²-cong {a} {b} {c} p p′)

    +ℤ-identityʳ : ∀ i → i +ℤ zeroℤ ≅ i
    +ℤ-identityʳ = lift _ eq (≅-heterogeneous-irrelevantʳ _ _ ∘ compat-abs) where

      eq : ∀ a → abs a +ℤ zeroℤ ≅ abs a
      eq a = begin
        abs a +ℤ zeroℤ      ≡⟨⟩
        abs a +ℤ abs zero²  ≅⟨ +ℤ-on-abs≅abs-+₂ a zero² ⟩
        abs (a +² zero²)    ≅⟨ compat-abs (+²-identityʳ a) ⟩
        abs a               ∎

    +²-identityˡ : (i : ℕ²) → (zero² +² i) ∼ i
    +²-identityˡ i = refl

    +ℤ-identityˡ : (i : ℤ)  → zeroℤ +ℤ i ≅ i
    +ℤ-identityˡ = lift _ eq (≅-heterogeneous-irrelevantʳ _ _ ∘ compat-abs) where

      eq : ∀ a → zeroℤ +ℤ abs a ≅ abs a
      eq a = begin
        zeroℤ +ℤ abs a     ≡⟨⟩
        abs zero² +ℤ abs a ≅⟨ +ℤ-on-abs≅abs-+₂ zero² a ⟩
        abs (zero² +² a)   ≅⟨ compat-abs (+²-identityˡ a) ⟩
        abs a              ∎

    +²-assoc : (i j k : ℕ²) → (i +² j) +² k ∼ i +² (j +² k)
    +²-assoc (a , b) (c , d) (e , f) = begin
      ((a + c) + e) + (b + (d + f)) ≡⟨ ≡.cong (_+ (b + (d + f))) (+-assoc a c e) ⟩
      (a + (c + e)) + (b + (d + f)) ≡⟨ ≡.cong ((a + (c + e)) +_) (≡.sym (+-assoc b d f)) ⟩
      (a + (c + e)) + ((b + d) + f) ∎

    +ℤ-assoc : ∀ i j k → (i +ℤ j) +ℤ k ≅ i +ℤ (j +ℤ k)
    +ℤ-assoc = Properties₃.lift₃ ext Int Int Int eq compat₃ where

      eq : ∀ i j k → (abs i +ℤ abs j) +ℤ abs k ≅ abs i +ℤ (abs j +ℤ abs k)
      eq i j k = begin
        (abs i +ℤ abs j) +ℤ abs k ≅⟨ cong (_+ℤ abs k) (+ℤ-on-abs≅abs-+₂ i j) ⟩
        (abs (i +² j) +ℤ abs k)   ≅⟨ +ℤ-on-abs≅abs-+₂ (i +² j) k ⟩
        abs ((i +² j) +² k)       ≅⟨ compat-abs (+²-assoc i j k) ⟩
        abs (i +² (j +² k))       ≅⟨ sym (+ℤ-on-abs≅abs-+₂ i (j +² k)) ⟩
        (abs i +ℤ abs (j +² k))   ≅⟨ cong (abs i +ℤ_) (sym (+ℤ-on-abs≅abs-+₂ j k)) ⟩
        abs i +ℤ (abs j +ℤ abs k) ∎

      compat₃ : ∀ {a a′ b b′ c c′} → a ∼ a′ → b ∼ b′ → c ∼ c′ → eq a b c ≅ eq a′ b′ c′
      compat₃ p q r = ≅-heterogeneous-irrelevantˡ _ _
                    $ cong₂ _+ℤ_ (cong₂ _+ℤ_ (compat-abs p) (compat-abs q))
                    $ compat-abs r


text:
{-# OPTIONS --cubical --safe --postfix-projections #-}

module Data.Fin.Properties where

open import Prelude
open import Data.Fin.Base
import Data.Nat.Properties as ℕ
open import Data.Nat.Properties using (+-comm)
open import Data.Nat
open import Function.Injective
open import Agda.Builtin.Nat renaming (_<_ to _<ᵇ_)

private
  variable
    n m : ℕ

suc-natfin : Σ[ m ⦂ ℕ ] × (m ℕ.< n) → Σ[ m ⦂ ℕ ] × (m ℕ.< suc n)
suc-natfin (m , p) = suc m , p

Fin-to-Nat-lt : Fin n → Σ[ m ⦂ ℕ ] × (m ℕ.< n)
Fin-to-Nat-lt {n = suc n} f0 = zero , tt
Fin-to-Nat-lt {n = suc n} (fs x) = suc-natfin (Fin-to-Nat-lt x)

Fin-from-Nat-lt : ∀ m → m ℕ.< n → Fin n
Fin-from-Nat-lt {n = suc n} zero p = f0
Fin-from-Nat-lt {n = suc n} (suc m) p = fs (Fin-from-Nat-lt m p)

Fin-Nat-lt-rightInv : ∀ m → (p : m ℕ.< n) → Fin-to-Nat-lt {n = n} (Fin-from-Nat-lt m p) ≡ (m , p)
Fin-Nat-lt-rightInv {n = suc n} zero p = refl
Fin-Nat-lt-rightInv {n = suc n} (suc m) p = cong (suc-natfin {n = n}) (Fin-Nat-lt-rightInv {n = n} m p)

Fin-Nat-lt-leftInv : (x : Fin n) → uncurry Fin-from-Nat-lt (Fin-to-Nat-lt x) ≡ x
Fin-Nat-lt-leftInv {n = suc n} f0 = refl
Fin-Nat-lt-leftInv {n = suc n} (fs x) = cong fs (Fin-Nat-lt-leftInv x)

Fin-Nat-lt : Fin n ⇔ Σ[ m ⦂ ℕ ] × (m ℕ.< n)
Fin-Nat-lt .fun = Fin-to-Nat-lt
Fin-Nat-lt .inv = uncurry Fin-from-Nat-lt
Fin-Nat-lt .rightInv = uncurry Fin-Nat-lt-rightInv
Fin-Nat-lt .leftInv = Fin-Nat-lt-leftInv

FinToℕ : Fin n → ℕ
FinToℕ {n = suc n} f0     = zero
FinToℕ {n = suc n} (fs x)  = suc (FinToℕ x)

FinToℕ-injective : ∀ {k} {m n : Fin k} → FinToℕ m ≡ FinToℕ n → m ≡ n
FinToℕ-injective {suc k} {f0}  {f0}  _ = refl
FinToℕ-injective {suc k} {f0}  {fs x} p = ⊥-elim (ℕ.znots p)
FinToℕ-injective {suc k} {fs m} {f0}  p = ⊥-elim (ℕ.snotz p)
FinToℕ-injective {suc k} {fs m} {fs x} p = cong fs (FinToℕ-injective (ℕ.injSuc p))

pred : Fin (suc n) → Fin (suc (ℕ.pred n))
pred f0 = f0
pred {n = suc n} (fs m) = m

discreteFin : ∀ {k} → Discrete (Fin k)
discreteFin {k = suc _} f0 f0 = yes refl
discreteFin {k = suc _} f0 (fs fk) = no (ℕ.znots ∘ cong FinToℕ)
discreteFin {k = suc _} (fs fj) f0 = no (ℕ.snotz ∘ cong FinToℕ)
discreteFin {k = suc _} (fs fj) (fs fk) =
  iff-dec (cong fs iff cong (λ { f0 → fk ; (fs x) → x})) (discreteFin fj fk)

isSetFin : isSet (Fin n)
isSetFin = Discrete→isSet discreteFin

FinFromℕ : (n m : ℕ) → T (n <ᵇ m) → Fin m
FinFromℕ zero (suc m) p = f0
FinFromℕ (suc n) (suc m) p = fs (FinFromℕ n m p)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
open import Level
open import Relation.Binary.PropositionalEquality

import Categories.Category

open import Syntax

module Renaming where

  open Equality

  -- the set of renamings

  infix 5 _→ʳ_

  _→ʳ_ : VShape → VShape → Set
  γ →ʳ δ = var γ → var δ

  -- equality of renamings

  infix 5 _≡ʳ_

  _≡ʳ_ : ∀ {γ δ} → (ρ : γ →ʳ δ) → (t : γ →ʳ δ) → Set
  ρ ≡ʳ σ = ∀ x → ρ x ≡ σ x

  -- equality is an equivalence relation

  ≡ʳ-refl : ∀ {γ δ} → {ρ : γ →ʳ δ} → ρ ≡ʳ ρ
  ≡ʳ-refl x = refl

  ≡ʳ-sym : ∀ {γ δ} → {ρ τ : γ →ʳ δ} → ρ ≡ʳ τ → τ ≡ʳ ρ
  ≡ʳ-sym ξ x = sym (ξ x)

  ≡ʳ-trans : ∀ {γ δ} → {ρ τ χ : γ →ʳ δ} → ρ ≡ʳ τ → τ ≡ʳ χ → ρ ≡ʳ χ
  ≡ʳ-trans ζ ξ x = trans (ζ x) (ξ x)

  -- 𝟘 is the weakly initial shape

  𝟘-initial : ∀ {γ} → 𝟘 →ʳ γ
  𝟘-initial ()

  -- identity renaming

  𝟙ʳ : ∀ {γ} → γ →ʳ γ
  𝟙ʳ x = x

  -- composition of renamings

  infixl 7 _∘ʳ_

  _∘ʳ_ : ∀ {γ δ η} → (δ →ʳ η) → (γ →ʳ δ) → (γ →ʳ η)
  (ρ ∘ʳ τ) x =  ρ (τ x)

  -- join of renamings

  infix 6 [_,_]ʳ

  [_,_]ʳ : ∀ {γ δ η} → (γ →ʳ η) → (δ →ʳ η) → (γ ⊕ δ →ʳ η)
  [ ρ , τ ]ʳ (var-left x) = ρ x
  [ ρ , τ ]ʳ (var-right y) = τ y

  -- renaming extension
  ⇑ʳ : ∀ {γ δ η} → (γ →ʳ δ) → (γ ⊕ η →ʳ δ ⊕ η)
  ⇑ʳ ρ (var-left x) =  var-left (ρ x)
  ⇑ʳ ρ (var-right y) = var-right y

  -- extension preserves equality

  ⇑ʳ-resp-≡ʳ : ∀ {γ δ η} {ρ τ : γ →ʳ δ} → ρ ≡ʳ τ → ⇑ʳ {η = η} ρ ≡ʳ ⇑ʳ τ
  ⇑ʳ-resp-≡ʳ ξ (var-left x) = cong var-left (ξ x)
  ⇑ʳ-resp-≡ʳ ξ (var-right y) = refl

  -- extension respects identity

  ⇑ʳ-resp-𝟙ʳ : ∀ {γ δ} → ⇑ʳ {η = δ} (𝟙ʳ {γ = γ})  ≡ʳ 𝟙ʳ
  ⇑ʳ-resp-𝟙ʳ (var-left x) = refl
  ⇑ʳ-resp-𝟙ʳ (var-right x) = refl

  -- extension commutes with composition

  ⇑ʳ-resp-∘ʳ : ∀ {β γ δ η} {ρ : β →ʳ γ} {τ : γ →ʳ δ} → ⇑ʳ {η = η} (τ ∘ʳ ρ) ≡ʳ ⇑ʳ τ ∘ʳ ⇑ʳ ρ
  ⇑ʳ-resp-∘ʳ (var-left x) = refl
  ⇑ʳ-resp-∘ʳ (var-right y) = refl

  module _ {𝕊 : Signature} where
    open Expression 𝕊

    -- the action of a renaming on an expression

    infixr 6 [_]ʳ_

    [_]ʳ_ : ∀ {𝕄} {cl} {γ} {δ} (ρ : γ →ʳ δ) → Expr 𝕄 cl γ → Expr 𝕄 cl δ
    [ ρ ]ʳ (expr-var x) = expr-var (ρ x)
    [ ρ ]ʳ (expr-symb S es) = expr-symb S (λ i → [ ⇑ʳ ρ ]ʳ (es i))
    [ ρ ]ʳ (expr-meta M ts) = expr-meta M (λ i → [ ρ ]ʳ (ts i))
    [ ρ ]ʳ expr-eqty = expr-eqty
    [ ρ ]ʳ expr-eqtm = expr-eqtm

    -- the action respects equality of renamings and equality of terms

    []ʳ-resp-≈ : ∀ {𝕄} {cl} {γ} {δ} (ρ : γ →ʳ δ) {t u : Expr 𝕄 cl γ} → t ≈ u → [ ρ ]ʳ t ≈ [ ρ ]ʳ u
    []ʳ-resp-≈ ρ (≈-≡ ξ) = ≈-≡ (cong [ ρ ]ʳ_ ξ)
    []ʳ-resp-≈ ρ (≈-symb ξ) = ≈-symb (λ i → []ʳ-resp-≈ (⇑ʳ ρ) (ξ i))
    []ʳ-resp-≈ ρ (≈-meta ξ) = ≈-meta (λ i → []ʳ-resp-≈ ρ (ξ i))

    []ʳ-resp-≡ʳ : ∀ {𝕄} {cl} {γ} {δ} {ρ τ : γ →ʳ δ} (t : Expr cl 𝕄 γ) → ρ ≡ʳ τ → [ ρ ]ʳ t ≈ [ τ ]ʳ t
    []ʳ-resp-≡ʳ (expr-var x) ξ = ≈-≡ (cong expr-var (ξ x))
    []ʳ-resp-≡ʳ (expr-symb S es) ξ = ≈-symb (λ i → []ʳ-resp-≡ʳ (es i) (⇑ʳ-resp-≡ʳ ξ))
    []ʳ-resp-≡ʳ (expr-meta M ts) ξ = ≈-meta (λ i → []ʳ-resp-≡ʳ (ts i) ξ)
    []ʳ-resp-≡ʳ expr-eqty ξ = ≈-eqty
    []ʳ-resp-≡ʳ expr-eqtm ξ = ≈-eqtm

    -- the action is functorial

    [𝟙ʳ] : ∀ {cl 𝕄 γ} {t : Expr cl 𝕄 γ} → [ 𝟙ʳ ]ʳ t ≈ t
    [𝟙ʳ] {t = expr-var x} = ≈-refl
    [𝟙ʳ] {t = expr-symb S es} = ≈-symb (λ i → ≈-trans ([]ʳ-resp-≡ʳ (es i) ⇑ʳ-resp-𝟙ʳ) [𝟙ʳ])
    [𝟙ʳ] {t = expr-meta M ts} = ≈-meta (λ i → [𝟙ʳ])
    [𝟙ʳ] {t = expr-eqty} = ≈-eqty
    [𝟙ʳ] {t = expr-eqtm} = ≈-eqtm

    [∘ʳ] : ∀ {cl 𝕄} {γ δ η} {ρ : γ →ʳ δ} {τ : δ →ʳ η} (t : Expr cl 𝕄 γ) → [ τ ∘ʳ ρ ]ʳ t ≈ [ τ ]ʳ [ ρ ]ʳ t
    [∘ʳ] (expr-var x) = ≈-refl
    [∘ʳ] (expr-symb S es) = ≈-symb (λ i → ≈-trans ([]ʳ-resp-≡ʳ (es i) ⇑ʳ-resp-∘ʳ) ([∘ʳ] (es i)))
    [∘ʳ] (expr-meta M ts) = ≈-meta (λ i → [∘ʳ] (ts i))
    [∘ʳ] expr-eqty = ≈-eqty
    [∘ʳ] expr-eqtm = ≈-eqtm

    []ʳ-id : ∀ {cl 𝕄 γ} {ρ : γ →ʳ γ} {t : Expr cl 𝕄 γ} → ρ ≡ʳ 𝟙ʳ → [ ρ ]ʳ t ≈ t
    []ʳ-id ξ = ≈-trans ([]ʳ-resp-≡ʳ _ ξ) [𝟙ʳ]

  -- the categorical structure

  module _ where
    open Categories.Category

    Renamings : Category zero zero zero
    Renamings =
      record
        { Obj = VShape
        ; _⇒_ = _→ʳ_
        ; _≈_ = _≡ʳ_
        ; id = 𝟙ʳ
        ; _∘_ = _∘ʳ_
        ; assoc = λ _ → refl
        ; sym-assoc = λ _ → refl
        ; identityˡ = λ _ → refl
        ; identityʳ = λ _ → refl
        ; identity² = λ _ → refl
        ; equiv = record { refl = ≡ʳ-refl ; sym = ≡ʳ-sym ; trans = ≡ʳ-trans }
        ; ∘-resp-≈ = λ {_} {_} {_} {ρ} {_} {_} {τ} ζ ξ x → trans (cong ρ (ξ x)) (ζ (τ x))
        }


text:
{-

Equalizer of functions f g : S X ⇉ T X such that f and g act on relation structures

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.RelationalStructure
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients
open import Cubical.HITs.PropositionalTruncation as Trunc
open import Cubical.Relation.Binary.Base

private
  variable
    ℓ ℓ₁ ℓ₁' ℓ₂ ℓ₂' : Level

EqualizerStructure : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  (f g : ∀ X → S X → T X)
  → Type ℓ → Type (ℓ-max ℓ₁ ℓ₂)
EqualizerStructure {S = S} f g X = Σ[ s ∈ S X ] f X s ≡ g X s

EqualizerRelStr : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  {f g : ∀ X → S X → T X}
  → StrRel S ℓ₁' → StrRel T ℓ₂' → StrRel (EqualizerStructure f g) ℓ₁'
EqualizerRelStr ρ₁ ρ₂ R (s , _) (s' , _) = ρ₁ R s s'

equalizerSuitableRel : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  {f g : ∀ X → S X → T X}
  {ρ₁ : StrRel S ℓ₁'} {ρ₂ : StrRel T ℓ₂'}
  (αf : ∀ {X Y} {R : X → Y → Type ℓ} {s s'} → ρ₁ R s s' → ρ₂ R (f X s) (f Y s'))
  (αg : ∀ {X Y} {R : X → Y → Type ℓ} {s s'} → ρ₁ R s s' → ρ₂ R (g X s) (g Y s'))
  → SuitableStrRel S ρ₁
  → SuitableStrRel T ρ₂
  → SuitableStrRel (EqualizerStructure f g) (EqualizerRelStr ρ₁ ρ₂)
equalizerSuitableRel {f = f} {g} {ρ₁} {ρ₂} αf αg θ₁ θ₂ .quo (X , s , p) (R , qer) r =
  ( ((quo₁ .fst .fst , sym step₀ ∙ step₁) , quo₁ .fst .snd)
  , λ {((s' , _) , r') →
    Σ≡Prop (λ _ → θ₁ .prop (λ _ _ → squash/ _ _) _ _)
      (Σ≡Prop (λ _ → θ₂ .set squash/ _ _)
        (cong fst (quo₁ .snd (s' , r'))))}
  )
  where
  quo₁ = θ₁ .quo (X , s) (R , qer) r
  quo₂ = θ₂ .quo (X , f X s) (R , qer) (αf r)

  step₀ : quo₂ .fst .fst ≡ f (X / R .fst) (quo₁ .fst .fst)
  step₀ =
    cong fst
      (quo₂ .snd
        (f _ (quo₁ .fst .fst) , αf (quo₁ .fst .snd)))

  step₁ : quo₂ .fst .fst ≡ g (X / R .fst) (quo₁ .fst .fst)
  step₁ =
    cong fst
      (quo₂ .snd
        ( g _ (quo₁ .fst .fst)
        , subst (λ t → ρ₂ (graphRel [_]) t (g _ (quo₁ .fst .fst))) (sym p) (αg (quo₁ .fst .snd))
        ))
equalizerSuitableRel _ _ θ₁ _ .symmetric R = θ₁ .symmetric R
equalizerSuitableRel _ _ θ₁ _ .transitive R R' = θ₁ .transitive R R'
equalizerSuitableRel _ _ θ₁ θ₂ .set setX =
  isSetΣ (θ₁ .set setX) λ _ → isOfHLevelPath 2 (θ₂ .set setX) _ _
equalizerSuitableRel _ _ θ₁ _ .prop propR _ _ = θ₁ .prop propR _ _

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

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

module Graphs.Complement {a b c : _} {V' : Set a} {V : Setoid {a} {b} V'} (G : Graph c V) where

open Graph G
open Setoid V
open Equivalence eq

complement : Graph (b ⊔ c) V
Graph._<->_ complement x y = ((x <-> y) → False) && ((x ∼ y) → False)
Graph.noSelfRelation complement x (pr1 ,, pr2) = pr2 reflexive
Graph.symmetric complement (x!-y ,, x!=y) = (λ pr → x!-y (Graph.symmetric G pr)) ,, λ pr → x!=y (Equivalence.symmetric eq pr)
Graph.wellDefined complement x=y r=s (x!-r ,, x!=r) = (λ y-s → x!-r (wellDefined (Equivalence.symmetric eq x=y) (Equivalence.symmetric eq r=s) y-s)) ,, λ y=s → x!=r (transitive x=y (transitive y=s (Equivalence.symmetric eq r=s)))


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.Instances.Bool where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure

open import Cubical.Relation.Nullary

open import Cubical.Data.Bool
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sum hiding (map ; rec)

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Semigroup

open GroupStr
open IsGroup
open IsMonoid
open IsSemigroup

BoolGroup : Group₀
fst BoolGroup = Bool
1g (snd BoolGroup) = true
(snd BoolGroup · false) false = true
(snd BoolGroup · false) true = false
(snd BoolGroup · true) y = y
inv (snd BoolGroup) x = x
is-set (isSemigroup (isMonoid (isGroup (snd BoolGroup)))) = isSetBool
·Assoc (isSemigroup (isMonoid (isGroup (snd BoolGroup)))) false false false = refl
·Assoc (isSemigroup (isMonoid (isGroup (snd BoolGroup)))) false false true = refl
·Assoc (isSemigroup (isMonoid (isGroup (snd BoolGroup)))) false true false = refl
·Assoc (isSemigroup (isMonoid (isGroup (snd BoolGroup)))) false true true = refl
·Assoc (isSemigroup (isMonoid (isGroup (snd BoolGroup)))) true false false = refl
·Assoc (isSemigroup (isMonoid (isGroup (snd BoolGroup)))) true false true = refl
·Assoc (isSemigroup (isMonoid (isGroup (snd BoolGroup)))) true true false = refl
·Assoc (isSemigroup (isMonoid (isGroup (snd BoolGroup)))) true true true = refl
·IdR (isMonoid (isGroup (snd BoolGroup))) false = refl
·IdR (isMonoid (isGroup (snd BoolGroup))) true = refl
·IdL (isMonoid (isGroup (snd BoolGroup))) false = refl
·IdL (isMonoid (isGroup (snd BoolGroup))) true = refl
·InvR (isGroup (snd BoolGroup)) false = refl
·InvR (isGroup (snd BoolGroup)) true = refl
·InvL (isGroup (snd BoolGroup)) false = refl
·InvL (isGroup (snd BoolGroup)) true = refl

-- Proof that any Group equivalent to Bool as types is also isomorphic to Bool as groups.
open GroupStr renaming (·Assoc to ·AssocG)

module _ {ℓ : Level} {A : Group ℓ} (e : Iso (fst A) Bool) where
  private
    discreteA : Discrete (typ A)
    discreteA = isoPresDiscrete (invIso e) _≟_

    _·A_ = GroupStr._·_ (snd A)
    -A_ = GroupStr.inv (snd A)

    IsoABool : Iso Bool (typ A)
    IsoABool with (Iso.fun e (1g (snd A))) ≟ true
    ... | yes p = invIso e
    ... | no p = compIso notIso (invIso e)

    true→1 : Iso.fun IsoABool true ≡ 1g (snd A)
    true→1 with (Iso.fun e (1g (snd A))) ≟ true
    ... | yes p = sym (cong (Iso.inv e) p) ∙ Iso.leftInv e _
    ... | no p = sym (cong (Iso.inv e) (¬true→false (Iso.fun e (1g (snd A))) p))
               ∙ Iso.leftInv e (1g (snd A))

    decA : (x : typ A) → (x ≡ 1g (snd A)) ⊎ (x ≡ Iso.fun IsoABool false)
    decA x with (Iso.inv IsoABool x) ≟ false | discreteA x (1g (snd A))
    ... | yes p | yes q = inl q
    ... | yes p | no q  = inr (sym (Iso.rightInv IsoABool x) ∙ cong (Iso.fun (IsoABool)) p)
    ... | no p  | no q  = inr (⊥.rec (q (sym (Iso.rightInv IsoABool x)
                                   ∙∙ cong (Iso.fun IsoABool) (¬false→true _ p)
                                   ∙∙ true→1)))
    ... | no p  | yes q = inl q

  ≅Bool : GroupIso BoolGroup A
  ≅Bool .fst = IsoABool
  ≅Bool .snd = makeIsGroupHom homHelp
    where
    homHelp : _
    homHelp false false with discreteA (Iso.fun IsoABool false) (1g (snd A))
                           | (decA ((Iso.fun IsoABool false) ·A Iso.fun IsoABool false))
    ... | yes p | _     = true→1 ∙∙ sym (GroupStr.·IdR (snd A) (1g (snd A))) ∙∙ cong₂ (_·A_) (sym p) (sym p)
    ... | no p  | inl x = true→1 ∙ sym x
    ... | no p  | inr x = true→1 ∙∙ sym (helper _ x) ∙∙ sym x
      where
      helper : (x : typ A) → x ·A x ≡ x → x ≡ (1g (snd A))
      helper x p = sym (GroupStr.·IdR (snd A) x)
                ∙∙ cong (x ·A_) (sym ((snd A) .·InvR x))
                ∙∙ ·AssocG (snd A) x x (-A x) ∙∙ cong (_·A (-A x)) p
                ∙∙ (snd A) .·InvR x
    homHelp false true = sym (GroupStr.·IdR (snd A) _) ∙ cong (Iso.fun IsoABool false ·A_) (sym true→1)
    homHelp true y = sym (GroupStr.·IdL (snd A) _) ∙ cong (_·A (Iso.fun IsoABool y)) (sym true→1)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Andreas, 2012-10-30 Sections
-- Reported by guillaume.brunerie, Oct 24 2012
module Issue735 where

import Common.Level
open import Common.Prelude using (Nat; zero; suc)

module _ {a} (A : Set a) where

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

module _ {a} {A : Set a} where

    _++_ : List → List → List
    []       ++ ys = ys
    (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

-- should not work, we cannot cut a section in two
-- correct is: List A

test : List Nat
test = (5 ∷ []) ++ (3 ∷ [])


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

open import lib.Basics
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.Paths
open import lib.types.Unit
open import lib.types.Empty

module lib.Equivalences2 where

{- Pre- and post- composition with equivalences are equivalences -}
module _ {i j k} {A : Type i} {B : Type j} {C : Type k}
         {h : A → B} (e : is-equiv h) where

  pre∘-is-equiv : is-equiv (λ (k : B → C) → k ∘ h)
  pre∘-is-equiv = is-eq f g f-g g-f
    where f = λ k → k ∘ h
          g = λ k → k ∘ is-equiv.g e
          f-g = λ k → ap (λ q → λ x → k (q x)) (λ= $ is-equiv.g-f e)
          g-f = λ k → ap (λ q → λ x → k (q x)) (λ= $ is-equiv.f-g e)

  post∘-is-equiv : is-equiv (λ (k : C → A) → h ∘ k)
  post∘-is-equiv = is-eq f g f-g g-f
    where f = λ k → h ∘ k
          g = λ k → is-equiv.g e ∘ k
          f-g = λ k → ap (λ q → q ∘ k) (λ= $ is-equiv.f-g e)
          g-f = λ k → ap (λ q → q ∘ k) (λ= $ is-equiv.g-f e)

{- The same thing on the abstraction level of equivalences -}
module _ {i j k} {A : Type i} {B : Type j} {C : Type k}
         (e : A ≃ B) where

  pre∘-equiv : (B → C) ≃ (A → C)
  pre∘-equiv = (_ , pre∘-is-equiv (snd e))

  post∘-equiv : (C → A) ≃ (C → B)
  post∘-equiv = (_ , post∘-is-equiv (snd e))

is-contr-map : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  → Type (lmax i j)
is-contr-map {A = A} {B = B} f = (y : B) → is-contr (Σ A (λ x → f x == y))

equiv-is-contr-map : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  → (is-equiv f → is-contr-map f)
equiv-is-contr-map e y =
   equiv-preserves-level ((equiv-Σ-fst (λ z → z == y) e) ⁻¹) (pathto-is-contr y)

contr-map-is-equiv : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  → (is-contr-map f → is-equiv f)
contr-map-is-equiv {f = f} cm = is-eq _
  (λ b → fst (fst (cm b)))
  (λ b → snd (fst (cm b)))
  (λ a → ap fst (snd (cm (f a)) (a , idp)))

fiber=-eqv : ∀ {i j} {A : Type i} {B : Type j} {h : A → B} {y : B}
  (r s : Σ A (λ x → h x == y))
  → (r == s) ≃ Σ (fst r == fst s) (λ γ → ap h γ ∙ snd s == snd r)
fiber=-eqv r s = equiv-Σ-snd (λ γ → !-equiv ∘e (↓-app=cst-eqv ⁻¹)) ∘e ((=Σ-eqv r s)⁻¹)

module _ {i j} {A : Type i} {B : Type j} where

  linv : (A → B) → Type (lmax i j)
  linv f = Σ (B → A) (λ g → (∀ x → g (f x) == x))

  rinv : (A → B) → Type (lmax i j)
  rinv f = Σ (B → A) (λ g → (∀ y → f (g y) == y))

  lcoh : (f : A → B) → linv f → Type (lmax i j)
  lcoh f (g , g-f) = Σ (∀ y → f (g y) == y)
                       (λ f-g → ∀ y → ap g (f-g y) == g-f (g y))

  rcoh : (f : A → B) → rinv f → Type (lmax i j)
  rcoh f (g , f-g) = Σ (∀ x → g (f x) == x)
                       (λ g-f → ∀ x → ap f (g-f x) == f-g (f x))

module _ {i j} {A : Type i} {B : Type j} {f : A → B} (e : is-equiv f) where

  equiv-linv-is-contr : is-contr (linv f)
  equiv-linv-is-contr = equiv-preserves-level (equiv-Σ-snd (λ _ → λ=-equiv ⁻¹))
                          (equiv-is-contr-map (pre∘-is-equiv e) (idf A))

  equiv-rinv-is-contr : is-contr (rinv f)
  equiv-rinv-is-contr = equiv-preserves-level (equiv-Σ-snd (λ _ → λ=-equiv ⁻¹))
                          (equiv-is-contr-map (post∘-is-equiv e) (idf B))

module _ {i j} {A : Type i} {B : Type j} {f : A → B} where

  rcoh-eqv : (v : rinv f)
    → rcoh f v ≃ Π A (λ x → (fst v (f x) , snd v (f x)) == (x , idp {a = f x}))
  rcoh-eqv v = equiv-Π-r (λ x → ((fiber=-eqv {h = f} _ _)⁻¹) ∘e apply-unit-r x) ∘e choice ⁻¹
    where
      apply-unit-r : ∀ x → Σ _ (λ γ → ap f γ == _) ≃ Σ _ (λ γ → ap f γ ∙ idp == _)
      apply-unit-r x = equiv-Σ-snd $
        λ γ → coe-equiv (ap (λ q → q == snd v (f x)) (! (∙-unit-r _)))

  lcoh-eqv : (v : linv f)
    → lcoh f v ≃ Π B (λ y → (f (fst v y) , snd v (fst v y)) == (y , idp))
  lcoh-eqv v = equiv-Π-r (λ y → ((fiber=-eqv {h = fst v} _ _)⁻¹) ∘e apply-unit-r y) ∘e choice ⁻¹
    where
      apply-unit-r : ∀ y → Σ _ (λ γ → ap (fst v) γ == _) ≃ Σ _ (λ γ → ap (fst v) γ ∙ idp == _)
      apply-unit-r y = equiv-Σ-snd $
        λ γ → coe-equiv (ap (λ q → q == snd v (fst v y)) (! (∙-unit-r _)))

equiv-rcoh-is-contr : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
                      (e : is-equiv f) → (v : rinv f) → is-contr (rcoh f v)
equiv-rcoh-is-contr {f = f} e v = equiv-preserves-level ((rcoh-eqv v)⁻¹)
  (Π-level (λ x → =-preserves-level -2 (equiv-is-contr-map e (f x))))

rinv-and-rcoh-eqv-is-equiv : ∀ {i j} {A : Type i} {B : Type j} {h : A → B}
  → Σ (rinv h) (rcoh h) ≃ is-equiv h
rinv-and-rcoh-eqv-is-equiv {h = h} = equiv f g (λ _ → idp) (λ _ → idp)
  where f : Σ (rinv h) (rcoh h) → is-equiv h
        f s = record {g = fst (fst s); f-g = snd (fst s);
                      g-f = fst (snd s); adj = snd (snd s)}
        g : is-equiv h → Σ (rinv h) (rcoh h)
        g t = ((is-equiv.g t , is-equiv.f-g t) , (is-equiv.g-f t , is-equiv.adj t))

is-equiv-is-prop : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  → is-prop (is-equiv f)
is-equiv-is-prop _ = inhab-to-contr-is-prop $ λ e →
  equiv-preserves-level rinv-and-rcoh-eqv-is-equiv
    (Σ-level (equiv-rinv-is-contr e) (equiv-rcoh-is-contr e))

∘e-unit-r : ∀ {i} {A B : Type i} (e : A ≃ B) → (e ∘e ide A) == e
∘e-unit-r e =
  pair= idp (prop-has-all-paths (is-equiv-is-prop (fst e)) _ _)

ua-∘e : ∀ {i} {A B : Type i}
  (e₁ : A ≃ B) {C : Type i} (e₂ : B ≃ C) → ua (e₂ ∘e e₁) == ua e₁ ∙ ua e₂
ua-∘e =
  equiv-induction
    (λ {A} {B} e₁ → ∀ {C} → ∀ (e₂ : B ≃ C) → ua (e₂ ∘e e₁) == ua e₁ ∙ ua e₂)
    (λ A → λ e₂ → ap ua (∘e-unit-r e₂) ∙ ap (λ w → (w ∙ ua e₂)) (! (ua-η idp)))

{- Type former equivalences involving Empty may require λ=. -}
module _ {j} {B : Empty → Type j} where
  Σ₁-Empty : Σ Empty B ≃ Empty
  Σ₁-Empty = equiv (⊥-rec ∘ fst) ⊥-rec ⊥-elim (⊥-rec ∘ fst)

  Π₁-Empty : Π Empty B ≃ Unit
  Π₁-Empty = equiv (cst tt) (cst ⊥-elim) (λ _ → contr-has-all-paths Unit-is-contr _ _) (λ _ → λ= ⊥-elim)

Σ₂-Empty : ∀ {i} {A : Type i} → Σ A (λ _ → Empty) ≃ Empty
Σ₂-Empty = equiv (⊥-rec ∘ snd) ⊥-rec ⊥-elim (⊥-rec ∘ snd)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import Agda.Builtin.Coinduction
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Equality

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

from : Nat → Colist Nat
from n = let sn = suc n in n ∷ ♯ (from sn)

take : {A : Set} → Nat → Colist A → List A
take zero    xs = []
take (suc n) [] = []
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)

check : take 3 (from 5) ≡ 5 ∷ 6 ∷ 7 ∷ []
check = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Issue308a where

data D : Set where
  d : D → D

syntax d x = d d x

f : D → D
f x = d d x


text:
{-
  A counterexample from Section 5.1 of Andreas Abel's dissertation [1],
  showing that the types of recursive functions must be (semi-)continuous,
  i.e. `loop` below should be disallowed.
  In the example, `loop` is not used as-is, but rather the size involved
  is instantiated to the infinite size in order to pass in `plus2`.

  The conditions on ω-instantiating from John Hughes' paper [2] is
  essentially a stricter condition than Abel's semi-continuity on where
  size variables may appear in the type.

  [1] A Polymorphic Lambda-Calculus with Sized Higher-Order Types
  [2] Proving the Correctness of Reactive Systems using Sized Types
-}

data Size : Set where
  ∘ : Size
  ↑_ : Size → Size

data Nat : Size → Set where
  zero : ∀ {s} → Nat (↑ s)
  succ : ∀ {s} → Nat s → Nat (↑ s)

data NatInf : Set where
  ⟦_⟧ : ∀ {s} → Nat s → NatInf

zero∘ : Nat (↑ ∘)
zero∘ = zero {∘}

shift : ∀ {s} → (NatInf → Nat (↑ (↑ s))) → NatInf → Nat (↑ s)
shift f ⟦ n ⟧ with f ⟦ succ n ⟧
... | zero = zero
... | succ m = m

plus2 : NatInf → NatInf
plus2 ⟦ n ⟧ = ⟦ succ (succ n) ⟧

loop : ∀ {s} → Nat s → (NatInf → Nat (↑ s)) → NatInf
loop _ f with f ⟦ zero∘ ⟧
... | zero          = ⟦ zero∘ ⟧
... | succ zero     = ⟦ zero∘ ⟧
... | succ (succ k) = loop k (shift f)

{-
  Interpreting Nat^∞ as a size-paired natural, we need to somehow
  derive an infinity-instantiated version (`loopInf`) using `loop`,
  but we cannot produce a `NatInf → Nat (↑ s)` out of `NatInf → NatInf`:
  doing so amounts to proving `∃s. Nat s → ∀s. Nat s`.
-}

-- loop cannot be instantiated with an infinite size
postulate loopInf : NatInf → (NatInf → NatInf) → NatInf

uhoh : NatInf
uhoh = loopInf ⟦ zero∘ ⟧ plus2

max_stars_repo_name: ionathanch/msc-thesis

max_issues_repo_name: ionathanch/msc-thesis

max_forks_repo_name: ionathanch/msc-thesis


text:
module Esterel.Lang.CanFunction.Properties where

{-
Basic properties of the Can function and utilities used in the reasoning,
such as Can does not look at shared variables and sequential variables; Can can
only output free variables; Can will capture free emit S and s ⇐ e (and more).
-}
open import Esterel.Lang.CanFunction.Base hiding ([_↦_]) public

{-
The equivalent "goodness" of can w.r.t. the rmerge reduction. Specifically, here
are the main lemmas:

  can-irr : ∀ {BV} {FV} θ₁ θ₂ q →
    CorrectBinding q BV FV →
    (distinct' (proj₁ FV) (proj₁ (Dom θ₂))) →
    Can q θ₁ ≡ Can q (θ₁ ← θ₂)
  can-irr θ₁ θ₂ q cbq FV≠Domθ₂

  canθₛ-mergeˡ : ∀ {E θ' r p BV FV} sigs θ →
    CorrectBinding p BV FV →
    p ≐ E ⟦ ρ θ' · r ⟧e →
    ∀ S' →
      Signal.unwrap S' ∉ SigMap.keys (Env.sig θ') →
      Signal.unwrap S' ∈ Canθₛ (SigMap.union sigs (Env.sig θ')) 0 (E ⟦ r ⟧e) θ →
      Signal.unwrap S' ∈ Canθₛ sigs 0 p θ

  canθₛ-mergeʳ : ∀ sigs θ' r θ →
    distinct' (proj₁ (Dom θ)) (SigMap.keys sigs) →
    ∀ S' →
      Signal.unwrap S' ∈ Canθₛ (SigMap.union sigs (Env.sig θ')) 0 r θ →
      Signal.unwrap S' ∈ Canθₛ (Env.sig θ') 0 r θ

These lemma says that when updating or extending the environent,
if the program does not refer to the updated variables, then
the Can function will not change and the Canθ function will
have some sort of monotonicity.

-}
open import Esterel.Lang.CanFunction.MergePotentialRuleCan public
open import Esterel.Lang.CanFunction.MergePotentialRuleTheta public

{-
The subset "goodness" of can w.r.t. other ρθ-reductions. For each of the 7 non-merge
ρθ-reductions, there are two corresponding Can subset lemmas.
-}
open import Esterel.Lang.CanFunction.NonMergePotentialRules public

{-
The compatible closure context C⟦_⟧c respects the monotonicity of the potential
function. For example, Can is monotonic w.r.t. to _sn⟶₁_, hence also _sn⟶_ by the
lemmas in this file.
-}
open import Esterel.Lang.CanFunction.Plug public

open import utility

open import Esterel.Lang
  using (Term ; emit ; _⇐_)
open import Esterel.Context
  using (_≐_⟦_⟧e)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Lang.CanFunction
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open import Function
  using (_∘_)
open import Relation.Nullary
  using (¬_)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module io-test2 where

open import io
open import list
open import string
open import unit

main : IO ⊤
main = getArgs >>= cont
          where cont : 𝕃 string → IO ⊤
                cont [] = return triv
                cont (x :: xs) = (readFiniteFile x) >>= putStr

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial