text:
module MinMax where

open import Prelude
open import Logic.Base
open import Logic.Relations
open import Logic.Identity using (_≡_)
import Logic.ChainReasoning
open import DecidableOrder as DecOrder

module Min {A : Set}(Ord : DecidableOrder A) where

  open DecidableOrder Ord

  min : A → A → A
  min a b with decide a b
  ... | \/-IL _ = a
  ... | \/-IR _ = b

  data CaseMin x y : A → Set where
    leq : x ≤ y → CaseMin x y x
    geq : x ≥ y → CaseMin x y y

  case-min′ : ∀ x y → CaseMin x y (min x y)
  case-min′ x y with decide x y
  ... | \/-IL xy  = leq xy
  ... | \/-IR ¬xy with total x y
  ...   | \/-IL xy = elim-False (¬xy xy)
  ...   | \/-IR yx = geq yx

  case-min : (P : A → Set)(x y : A) →
            (x ≤ y → P x) →
            (y ≤ x → P y) → P (min x y)
  case-min P x y ifx ify with min x y | case-min′ x y
  ... | .x | leq xy = ifx xy
  ... | .y | geq yx = ify yx

  min-glb : ∀ x y z → z ≤ x → z ≤ y → z ≤ min x y
  min-glb x y z zx zy with min x y | case-min′ x y
  ... | .x | leq _ = zx
  ... | .y | geq _ = zy

  min-left : ∀ x y → min x y ≤ x
  min-left x y with min x y | case-min′ x y
  ... | .x | leq _  = refl _
  ... | .y | geq yx = yx

  min-right : ∀ x y → min x y ≤ y
  min-right x y with min x y | case-min′ x y
  ... | .x | leq xy = xy
  ... | .y | geq _  = refl _

  min-sym : ∀ x y → min x y ≡ min y x
  min-sym x y = antisym _ _ (lem x y) (lem y x)
    where
      lem : ∀ a b → min a b ≤ min b a
      lem a b with min b a | case-min′ b a
      ... | .b | leq _ = min-right _ _
      ... | .a | geq _ = min-left _ _

Dual : {A : Set} → DecidableOrder A → DecidableOrder A
Dual Ord = record
    { _≤_     = _≥_
    ; refl    = refl
    ; antisym = \x y xy yx   → antisym _ _ yx xy
    ; trans   = \x y z xy yz → trans _ _ _ yz xy
    ; total   = \x y         → total _ _
    ; decide  = \x y         → decide _ _
    }
  where
    open DecidableOrder Ord

module Max {A : Set}(Ord : DecidableOrder A)
      = Min (Dual Ord) renaming
              ( min       to max
              ; case-min  to case-max
              ; case-min′ to case-max′
              ; CaseMin   to CaseMax
              ; module CaseMin to CaseMax
              ; leq       to geq
              ; geq       to leq
              ; min-glb   to max-lub
              ; min-sym   to max-sym
              ; min-right to max-right
              ; min-left  to max-left
              )

module MinMax {A : Set}(Ord : DecidableOrder A) where
  open DecidableOrder Ord public
  open Min Ord public
  open Max Ord public

module DistributivityA {A : Set}(Ord : DecidableOrder A) where

  open MinMax Ord

  min-max-distr : ∀ x y z → min x (max y z) ≡ max (min x y) (min x z)
  min-max-distr x y z = antisym _ _ left right
    where
      open Logic.ChainReasoning.Mono.Homogenous _≤_ refl trans

      left : min x (max y z) ≤ max (min x y) (min x z)
      left with max y z | case-max′ y z
      ... | .z | Min.geq _ = max-right _ _
      ... | .y | Min.leq _ = max-left _ _

      right : max (min x y) (min x z) ≤ min x (max y z)
--      right with max (min x y) (min x z) | case-max′ (min x y) (min x z)
      right = case-max (\w → w ≤ min x (max y z)) (min x y) (min x z)
                       (\_ → case-max (\w → min x y ≤ min x w) y z
                                (\_  → refl _)
                                (\yz → min-glb x z _ (min-left x y)
                                          ( chain>
                                            min x y === y  by  min-right x y
                                                    === z  by  yz
                                          )
                                )
                       )
                       (\_ → case-max (\w → min x z ≤ min x w) y z
                                (\zy → min-glb x y _ (min-left x z)
                                          ( chain>
                                            min x z === z  by  min-right x z
                                                    === y  by  zy
                                          )
                                )
                                (\_  → refl _)
                       )

module DistributivityB {A : Set}(Ord : DecidableOrder A) where

  open DistributivityA (Dual Ord) public renaming (min-max-distr to max-min-distr)

module Distributivity {A : Set}(Ord : DecidableOrder A) where

  open DistributivityA Ord public
  open DistributivityB Ord public

-- Testing
postulate
  X    : Set
  OrdX : DecidableOrder X

-- open DecidableOrder OrdX
open MinMax OrdX -- hiding (_≤_)
open Distributivity OrdX

open Logic.ChainReasoning.Mono.Homogenous

-- Displayforms doesn't work for MinMax._≤_ (reduces to DecidableOrder._≤_)
test : ∀ x y → min x y ≤ x
test x y = min-left x y

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Pruning where

le2 : {B : Set} -> (A : Set) -> A -> (C : Set) -> C -> (A -> C -> B) -> B
le2 _ x _ y f = f x y

test : le2 Set _ (Set -> Set) _ (\ H -> (\M -> (z : Set) -> H == M z))
test z = refl

{-
let : {B : Set} -> (A : Set) -> A -> (A -> B) -> B
let A x f = f x

test : let Set _ (\ H -> let (Set -> Set) _ (\ M -> (z : Set) -> H == M z))
test z = refl
-}

ext: agda

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


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

open import Relation.Binary.PropositionalEquality
import Relation.Binary.Reasoning.Setoid as SetoidR

import Categories.Category as Category
import Categories.Category.Cartesian as Cartesian
open import Categories.Object.Terminal using (Terminal)
open import Categories.Object.Product using (Product)

open import MultiSorted.AlgebraicTheory
import MultiSorted.Substitution as Substitution
import MultiSorted.Product as Product

module MultiSorted.SyntacticCategory
  {ℓt}
  {𝓈 ℴ}
  {Σ : Signature {𝓈} {ℴ}}
  (T : Theory ℓt Σ) where

  open Theory T
  open Substitution T

  -- The syntactic category

  𝒮 : Category.Category 𝓈 (lsuc ℴ) (lsuc (ℓt ⊔ 𝓈 ⊔ ℴ))
  𝒮 =
    record
      { Obj = Context
      ; _⇒_ = _⇒s_
      ; _≈_ = _≈s_
      ; id =  id-s
      ; _∘_ =  _∘s_
      ; assoc = λ {_ _ _ _ _ _ σ} x → subst-∘s (σ x)
      ; sym-assoc =  λ {_ _ _ _ _ _ σ} x → eq-symm (subst-∘s (σ x))
      ; identityˡ = λ x → eq-refl
      ; identityʳ = λ {A B f} x → tm-var-id
      ; identity² = λ x → eq-refl
      ; equiv = record
                 { refl = λ x → eq-refl
                 ; sym = λ ξ y → eq-symm (ξ y)
                 ; trans = λ ζ ξ y → eq-tran (ζ y) (ξ y)}
      ; ∘-resp-≈ = ∘s-resp-≈s
      }

  -- We use the product structure which gives back the context directly
  prod-𝒮 : Context → Context
  prod-𝒮 Γ = Γ

  π-𝒮 : ∀ {Γ} (x : var Γ) → Γ ⇒s ctx-slot (sort-of Γ x)
  π-𝒮 x _ = tm-var x

  tuple-𝒮 : ∀ Γ {Δ} → (∀ (x : var Γ) → Δ ⇒s ctx-slot (sort-of Γ x)) → Δ ⇒s Γ
  tuple-𝒮 Γ ts = λ x → ts x var-var

  project-𝒮 : ∀ {Γ Δ} {x : var Γ} {ts : ∀ (y : var Γ) → Δ ⇒s ctx-slot (sort-of Γ y)} →
              π-𝒮 x ∘s tuple-𝒮 Γ ts ≈s ts x
  project-𝒮 {Γ} {Δ} {x} {ts} var-var = eq-refl

  unique-𝒮 : ∀ {Γ Δ} {ts : ∀ (x : var Γ) → Δ ⇒s ctx-slot (sort-of Γ x)} {g : Δ ⇒s Γ} →
             (∀ x → π-𝒮 x ∘s g ≈s ts x) → tuple-𝒮 Γ ts ≈s g
  unique-𝒮 ξ x = eq-symm (ξ x var-var)

  producted-𝒮 : Product.Producted 𝒮 {Σ = Σ} ctx-slot
  producted-𝒮 =
    record
      { prod = prod-𝒮
      ; π =  π-𝒮
      ; tuple = tuple-𝒮
      ; project = λ {Γ Δ x ts} → project-𝒮 {ts = ts}
      ; unique = unique-𝒮
      }

  -- The terminal object is the empty context
  ⊤-𝒮 : Context
  ⊤-𝒮 = ctx-empty

  !-𝒮 : ∀ {Γ} → Γ ⇒s ⊤-𝒮
  !-𝒮 ()

  !-unique-𝒮 : ∀ {Γ} (σ : Γ ⇒s ⊤-𝒮) → !-𝒮 ≈s σ
  !-unique-𝒮 σ ()

  terminal-𝒮 : Terminal 𝒮
  terminal-𝒮 =
    record
      { ⊤ = ⊤-𝒮
      ; ⊤-is-terminal =
          record { ! = !-𝒮
                 ; !-unique = !-unique-𝒮 } }

  -- Binary product is context contatenation
  product-𝒮 : ∀ {Γ Δ} → Product 𝒮 Γ Δ
  product-𝒮 {Γ} {Δ} =
    record
      { A×B =  ctx-concat Γ Δ
      ; π₁ = λ x → tm-var (var-inl x)
      ; π₂ = λ x → tm-var (var-inr x)
      ; ⟨_,_⟩ = ⟨_,_⟩s
      ; project₁ = λ x → eq-refl
      ; project₂ = λ x → eq-refl
      ; unique = λ {Θ σ σ₁ σ₂} ξ₁ ξ₂ z → u Θ σ σ₁ σ₂ ξ₁ ξ₂ z
      }
    where u : ∀ Θ (σ : Θ ⇒s ctx-concat Γ Δ) (σ₁ : Θ ⇒s Γ) (σ₂ : Θ ⇒s Δ) →
                  ((λ x → σ (var-inl x)) ≈s σ₁) → ((λ y → σ (var-inr y)) ≈s σ₂) → ⟨ σ₁ , σ₂ ⟩s ≈s σ
          u Θ σ σ₁ σ₂ ξ₁ ξ₂ (var-inl z) = eq-symm (ξ₁ z)
          u Θ σ σ₁ σ₂ ξ₁ ξ₂ (var-inr z) = eq-symm (ξ₂ z)

  -- The cartesian structure of the syntactic category
  cartesian-𝒮 : Cartesian.Cartesian 𝒮
  cartesian-𝒮 =
    record
      { terminal = terminal-𝒮
      ; products = record { product = product-𝒮 } }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
{- --- 4. Lists --- -}

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

infixr 5 _∷_

open import Data.Nat
open import Relation.Binary.PropositionalEquality

{- 4.1 Length -}

length : {A : Set} → List A → ℕ
length [] = 0
length (x ∷ l) = 1 + (length l)

{- 4.2 List reversal -}

concat : {A : Set} → List A → List A → List A
concat [] l = l
concat (x ∷ k) l = x ∷ (concat k l)

concat-length : {A : Set} → (k l : List A) → length (concat k l) ≡ (length k) + (length l)
concat-length [] l = refl
concat-length (x ∷ k) l rewrite concat-length k l = refl

concat-assoc : {A : Set} → (j k l : List A) → concat (concat j k) l ≡ concat j (concat k l)
concat-assoc [] k l = refl
concat-assoc (x ∷ j) k l rewrite concat-assoc j k l = refl

{- 4.3 List reversal -}

snoc : {A : Set} → A -> List A → List A
snoc a [] = a ∷ []
snoc a (x ∷ l) = x ∷ (snoc a l)

rev : {A : Set} → List A → List A
rev [] = []
rev (x ∷ l) = snoc x (rev l)

snoc-length : {A : Set} → (a : A) → (l : List A) → length (snoc a l) ≡ suc (length l)
snoc-length a [] = refl
snoc-length a (x ∷ l) rewrite snoc-length a l = refl

rev-length : {A : Set} → (l : List A) → (length (rev l)) ≡ (length l)
rev-length [] = refl
rev-length (x ∷ l) rewrite snoc-length x (rev l) | rev-length l = refl

snoc-rev : {A : Set} → (a : A) → (l : List A) → rev (snoc a l) ≡ a ∷ (rev l)
snoc-rev a [] = refl
snoc-rev a (x ∷ l) rewrite snoc-rev a l = refl

double-rev : {A : Set} → (l : List A) → rev (rev l) ≡ l
double-rev [] = refl
double-rev (x ∷ l) rewrite snoc-rev x (rev l) | double-rev l = refl

{- 4.4 Filtering -}
open import Data.Bool

filter : {A : Set} → (p : A → Bool) → (l : List A) → List A
filter p [] = []
filter p (x ∷ l) with p x
filter p (x ∷ l) | false = filter p l
filter p (x ∷ l) | true = x ∷ (filter p l)

empty-list : {A : Set} → (l : List A) → filter (λ _ → false) l ≡ []
empty-list [] = refl
empty-list (x ∷ l) = empty-list l

identity-list : {A : Set} → (l : List A) → filter (λ _ → true) l ≡ l
identity-list [] = refl
identity-list (x ∷ l) rewrite identity-list l = refl

max_stars_repo_name: erwinkn/program-eq-proof

max_issues_repo_name: erwinkn/program-eq-proof

max_forks_repo_name: erwinkn/program-eq-proof


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category; module Definitions)

-- Definition of the "Twisted Arrow" Category of a Category 𝒞
module Categories.Category.Construction.TwistedArrow {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Data.Product using (_,_; _×_; map; zip)
open import Function.Base using (_$_; flip)
open import Relation.Binary.Core using (Rel)

import Categories.Morphism as M
open M 𝒞
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open Definitions 𝒞
open HomReasoning

private
  variable
    A B C : Obj

record Morphism : Set (o ⊔ ℓ) where
  field
    {dom} : Obj
    {cod} : Obj
    arr   : dom ⇒ cod

record Morphism⇒ (f g : Morphism) : Set (ℓ ⊔ e) where
  constructor mor⇒
  private
    module f = Morphism f
    module g = Morphism g

  field
    {dom⇐} : g.dom ⇒ f.dom
    {cod⇒} : f.cod ⇒ g.cod
    square : cod⇒ ∘ f.arr ∘ dom⇐ ≈ g.arr

TwistedArrow : Category (o ⊔ ℓ) (ℓ ⊔ e) e
TwistedArrow = record
  { Obj       = Morphism
  ; _⇒_       = Morphism⇒
  ; _≈_       = λ f g → dom⇐ f ≈ dom⇐ g × cod⇒ f ≈ cod⇒ g
  ; id        = mor⇒ (identityˡ ○ identityʳ)
  ; _∘_       = λ {A} {B} {C} m₁ m₂ → mor⇒ {A} {C} (∘′ m₁ m₂  ○ square m₁)
  ; assoc     = sym-assoc , assoc
  ; sym-assoc = assoc , sym-assoc
  ; identityˡ = identityʳ , identityˡ
  ; identityʳ = identityˡ , identityʳ
  ; identity² = identity² , identity²
  ; equiv     = record
    { refl  = refl , refl
    ; sym   = map sym sym
    ; trans = zip trans trans
    }
  ; ∘-resp-≈  = zip (flip ∘-resp-≈) ∘-resp-≈
  }
  where
  open Morphism⇒
  open Equiv
  open HomReasoning
  ∘′ : ∀ {A B C} (m₁ : Morphism⇒ B C) (m₂ : Morphism⇒ A B) →
    (cod⇒ m₁ ∘ cod⇒ m₂) ∘ Morphism.arr A ∘ (dom⇐ m₂ ∘ dom⇐ m₁) ≈ cod⇒ m₁ ∘ Morphism.arr B ∘ dom⇐ m₁
  ∘′ {A} {B} {C} m₁ m₂ = begin
    (cod⇒ m₁ ∘ cod⇒ m₂) ∘ Morphism.arr A ∘ (dom⇐ m₂ ∘ dom⇐ m₁) ≈⟨ pullʳ sym-assoc ⟩
    cod⇒ m₁ ∘ (cod⇒ m₂ ∘ Morphism.arr A) ∘ (dom⇐ m₂ ∘ dom⇐ m₁) ≈⟨ refl⟩∘⟨ (pullˡ assoc) ⟩
    cod⇒ m₁ ∘ (cod⇒ m₂ ∘ Morphism.arr A ∘ dom⇐ m₂) ∘ dom⇐ m₁   ≈⟨ (refl⟩∘⟨ square m₂ ⟩∘⟨refl) ⟩
    cod⇒ m₁ ∘ Morphism.arr B ∘ dom⇐ m₁ ∎

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:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --guardedness #-}

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

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

  private
    variable
      U : Set 𝓁

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

  {- Generalized inference systems -}

  FCoInd⟦_,_⟧ : ∀{𝓁c 𝓁p 𝓁n 𝓁n'} → (I : IS {𝓁c} {𝓁p} {𝓁n} U) → (C : IS {𝓁c} {𝓁p} {𝓁n'} U) → U → Set _
  FCoInd⟦ I , C ⟧ = CoInd⟦ I ⊓ Ind⟦ I ∪ C ⟧ ⟧

  {- Bounded Coinduction Principle -}

  bdc-lem : ∀{𝓁c 𝓁p 𝓁n 𝓁' 𝓁''}
      → (I : IS {𝓁c} {𝓁p} {𝓁n} U)
      → (S : U → Set 𝓁')
      → (Q : U → Set 𝓁'')
      → S ⊆ Q
      → S ⊆ ISF[ I ] S
      → S ⊆ ISF[ I ⊓ Q ] S
  bdc-lem _ _ _ bd cn Su with cn Su
  ... | rn , c , refl , pr = rn , (c , bd Su) , refl , pr

  bounded-coind[_,_] : ∀{𝓁c 𝓁p 𝓁n 𝓁n' 𝓁'}
      → (I : IS {𝓁c} {𝓁p} {𝓁n} U)
      → (C : IS {𝓁c} {𝓁p} {𝓁n'} U)
      → (S : U → Set 𝓁')
      → S ⊆ Ind⟦ I ∪ C ⟧      -- S is bounded w.r.t. I ∪ C
      → S ⊆ ISF[ I ] S        -- S is consistent w.r.t. I
      → S ⊆ FCoInd⟦ I , C ⟧
  bounded-coind[ I , C ] S bd cn Su = coind[ I ⊓ Ind⟦ I ∪ C ⟧ ] S (bdc-lem I S Ind⟦ I ∪ C ⟧ bd cn) Su

  {- Get Ind from FCoInd -}

  fcoind-to-ind : ∀{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      → FCoInd⟦ is , cois ⟧ ⊆ Ind⟦ is ∪ cois ⟧
  fcoind-to-ind co with CoInd⟦_⟧.unfold co
  ... | _ , (_ , sd) , refl , _ = sd

  {- Apply Rule -}

  apply-fcoind : ∀{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      → (rn : is .Names) → RClosed (is .rules rn) FCoInd⟦ is , cois ⟧
  apply-fcoind rn c pr = apply-coind rn (c , apply-ind (inj₁ rn) c λ i → fcoind-to-ind (pr i)) pr

  {- Postfix - Prefix -}

  fcoind-postfix : ∀{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      → FCoInd⟦ is , cois ⟧ ⊆ ISF[ is ] FCoInd⟦ is , cois ⟧
  fcoind-postfix FCoInd with FCoInd .CoInd⟦_⟧.unfold
  ... | rn , (c , _) , refl , pr = rn , c , refl , pr

  fcoind-prefix : ∀{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      → ISF[ is ] FCoInd⟦ is , cois ⟧ ⊆ FCoInd⟦ is , cois ⟧
  fcoind-prefix (rn , c , refl , pr) = apply-fcoind rn c pr

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


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

open import Categories.Category

module Categories.Diagram.Equalizer.Limit {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Data.Nat.Base using (ℕ)
open import Data.Fin.Base hiding (lift)
open import Data.Fin.Patterns

open import Categories.Category.Lift
open import Categories.Category.Finite.Fin
open import Categories.Category.Finite.Fin.Instance.Parallel
open import Categories.Diagram.Equalizer C
open import Categories.Diagram.Limit
open import Categories.Functor.Core

import Categories.Category.Construction.Cones as Co
import Categories.Morphism.Reasoning as MR

private
  module C = Category C
  open C
  open MR C
  open HomReasoning
  open Equiv

module _ {o′ ℓ′ e′} {F : Functor (liftC o′ ℓ′ e′ Parallel) C} where
  private
    module F = Functor F
    open F

  limit⇒equalizer : Limit F → Equalizer {B = F₀ (lift 1F)} (F₁ (lift 0F)) (F₁ (lift 1F))
  limit⇒equalizer L = record
    { obj       = apex
    ; arr       = proj (lift 0F)
    ; equality  = limit-commute (lift 0F) ○ ⟺ (limit-commute (lift 1F))
    ; equalize  = λ {_} {h} eq → rep record
      { apex = record
        { ψ       = λ { (lift 0F) → h
                      ; (lift 1F) → F₁ (lift 1F) ∘ h }
        ; commute = λ { {lift 0F} {lift 0F} (lift 0F) → elimˡ identity
                      ; {lift 0F} {lift 1F} (lift 0F) → eq
                      ; {lift 0F} {lift 1F} (lift 1F) → refl
                      ; {lift 1F} {lift 1F} (lift 0F) → elimˡ identity }
        }
      }
    ; universal = ⟺ commute
    ; unique    = λ {_} {h i} eq → ⟺ (terminal.!-unique record
      { arr = i
      ; commute = λ { {lift 0F} → ⟺ eq
                    ; {lift 1F} → begin
                      proj (lift 1F) ∘ i                ≈˘⟨ pullˡ (limit-commute (lift 1F)) ⟩
                      F₁ (lift 1F) ∘ proj (lift 0F) ∘ i ≈˘⟨ refl⟩∘⟨ eq ⟩
                      F₁ (lift 1F) ∘ h                  ∎ }
      })
    }
    where open Limit L

module _ o′ ℓ′ e′ {X Y} (f g : X ⇒ Y) where

  equalizer⇒limit-F : Functor (liftC o′ ℓ′ e′ Parallel) C
  equalizer⇒limit-F = record
    { F₀           = λ { (lift 0F) → X
                       ; (lift 1F) → Y }
    ; F₁           = λ { {lift 0F} {lift 0F} (lift 0F) → C.id
                       ; {lift 0F} {lift 1F} (lift 0F) → f
                       ; {lift 0F} {lift 1F} (lift 1F) → g
                       ; {lift 1F} {lift 1F} (lift 0F) → C.id }
    ; identity     = λ { {lift 0F} → refl
                       ; {lift 1F} → refl }
    ; homomorphism = λ { {lift 0F} {lift 0F} {lift 0F} {lift 0F} {lift 0F} → ⟺ identity²
                       ; {lift 0F} {lift 0F} {lift 1F} {lift 0F} {lift 0F} → ⟺ identityʳ
                       ; {lift 0F} {lift 0F} {lift 1F} {lift 0F} {lift 1F} → ⟺ identityʳ
                       ; {lift 0F} {lift 1F} {lift 1F} {lift 0F} {lift 0F} → ⟺ identityˡ
                       ; {lift 0F} {lift 1F} {lift 1F} {lift 1F} {lift 0F} → ⟺ identityˡ
                       ; {lift 1F} {lift 1F} {lift 1F} {lift 0F} {lift 0F} → ⟺ identity² }
    ; F-resp-≈     = λ { {lift 0F} {lift 0F} {lift 0F} {lift 0F} _ → refl
                       ; {lift 0F} {lift 1F} {lift 0F} {lift 0F} _ → refl
                       ; {lift 0F} {lift 1F} {lift 1F} {lift 1F} _ → refl
                       ; {lift 1F} {lift 1F} {lift 0F} {lift 0F} _ → refl }
    }

module _ o′ ℓ′ e′ {X Y} {f g : X ⇒ Y} (e : Equalizer f g) where
  open Equalizer e
  private
    F = equalizer⇒limit-F o′ ℓ′ e′ f g

  equalizer⇒limit : Limit F
  equalizer⇒limit = record
    { terminal = record
      { ⊤        = record
        { N    = obj
        ; apex = record
          { ψ       = λ { (lift 0F) → arr
                        ; (lift 1F) → g ∘ arr }
          ; commute = λ { {lift 0F} {lift 0F} (lift 0F) → identityˡ
                        ; {lift 0F} {lift 1F} (lift 0F) → equality
                        ; {lift 0F} {lift 1F} (lift 1F) → refl
                        ; {lift 1F} {lift 1F} (lift 0F) → identityˡ }
          }
        }
      ; !        = λ {K} →
        let open Co.Cone F K
        in record
        { arr     = equalize (commute (lift 0F) ○ ⟺ (commute (lift 1F)))
        ; commute = λ { {lift 0F} → ⟺ universal
                      ; {lift 1F} → pullʳ (⟺ universal) ○ commute (lift 1F) }
        }
      ; !-unique = λ f →
        let open Co.Cone⇒ F f
        in ⟺ (unique (⟺ commute))
      }
    }

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


text:
module Main where

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

open import Coinduction
open import Data.String
open import Data.Unit using (⊤)
open import IO
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

-- Check that trustMe works.

testTrustMe : IO ⊤
testTrustMe with "apa" ≟ "apa"
... | yes refl = putStrLn "Yes!"
... | no  _    = putStrLn "No."

-- Check that ∞ can be used as an "expression".

testInf : Set → Set
testInf = ∞

main = run testTrustMe

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2016-08-26, issue 2152
-- Option --allow-unsolved-metas is not --safe

Unsolved : Set
Unsolved = ?

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Test.Factorial where

open import Data.Nat

factorial : ℕ -> ℕ
factorial zero = 1
factorial n@(suc n') = n * factorial n'

max_stars_repo_name: yanok/normalize-via-instances

max_issues_repo_name: yanok/normalize-via-instances

max_forks_repo_name: yanok/normalize-via-instances


text:
-- Andreas, 2018-05-09, issue 2636, reported by nad

-- {-# OPTIONS -v tc.pos:10 #-}

id : (A : Set₁) → A → A
id A x = x

A : Set₁
A = Set
  where
  F : Set₁ → Set₁
  F X = X

  data D : Set₁ where
    c : F D → D

  lemma : F (D → Set) → D → Set
  lemma fp d = id (F (D → Set)) fp d

-- Problem was:
-- Positivity checker for D complained when lemma was present.


text:
module Inductive.Examples.Ord where

open import Inductive
open import Tuple

open import Data.Fin
open import Data.Product
open import Data.List
open import Data.Vec hiding (lookup)

open import Inductive.Examples.Nat

Ord : Set
Ord = Inductive (([] , []) ∷ (([] , ((Nat ∷ []) ∷ [])) ∷ []))

zeroₒ : Ord
zeroₒ = construct Fin.zero [] []

supₒ : (Nat → Ord) → Ord
supₒ f = construct (Fin.suc Fin.zero) [] ((λ x → f (lookup Fin.zero x)) ∷ [])

max_stars_repo_name: mr-ohman/general-induction

max_issues_repo_name: mr-ohman/general-induction

max_forks_repo_name: mr-ohman/general-induction


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Change contexts
--
-- This module specifies how a context of values is merged
-- together with the corresponding context of changes.
--
-- In the PLDI paper, instead of merging the contexts together, we just
-- concatenate them. For example, in the "typing rule" for Derive
-- in Sec. 3.2 of the paper, we write in the conclusion of the rule:
-- "Γ, ΔΓ ⊢ Derive(t) : Δτ". Simple concatenation is possible because
-- the paper uses named variables and assumes that no user variables
-- start with "d". In this formalization, we use de Bruijn indices, so
-- it is easier to alternate values and their changes in the context.
------------------------------------------------------------------------

module Base.Change.Context
    {Type : Set}
    (ΔType : Type → Type) where

open import Base.Syntax.Context Type

-- Transform a context of values into a context of values and
-- changes.
ΔContext : Context → Context
ΔContext ∅ = ∅
ΔContext (τ • Γ) = ΔType τ • τ • ΔContext Γ

-- like ΔContext, but ΔType τ and τ are swapped
ΔContext′ : Context → Context
ΔContext′ ∅ = ∅
ΔContext′ (τ • Γ) = τ • ΔType τ • ΔContext′ Γ

-- This sub-context relationship explains how to go back from
-- ΔContext Γ to Γ: You have to drop every other binding.
Γ≼ΔΓ : ∀ {Γ} → Γ ≼ ΔContext Γ
Γ≼ΔΓ {∅} = ∅
Γ≼ΔΓ {τ • Γ} = drop ΔType τ • keep τ • Γ≼ΔΓ

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module GGT.Group.Bundles
  {a b ℓ}
  where

open import Algebra.Bundles using (Group)
open import Relation.Unary
open import Relation.Binary
open import Level
open import GGT.Group.Structures

record SubGroup (G : Group a ℓ) : Set (a ⊔ suc b ⊔ ℓ) where
  open Group G public
  field
    P : Pred Carrier b
    isSubGroup : IsSubGroup G P

  open IsSubGroup isSubGroup public
  -- imports ~
  -- xy-1 ∈ H => xy-1 = h => h'xy-1 = h'' => h'x = h''y -- right cosets
  -- x ↦ ω · x = ω · yx-1 · x = ω · y

cosetʳRel : {G : Group a ℓ} → (SubGroup G) → Setoid a b

cosetʳRel {G} H = record { Carrier = Carrier;
                           _≈_ = _∼_;
                           isEquivalence = iseq} where
                  open SubGroup H
                  open import GGT.Group.Facts G
                  iseq = record {refl  = cosetRelRefl isSubGroup ;
                                 sym   = cosetRelSym isSubGroup ;
                                 trans = cosetRelTrans isSubGroup }

syntax cosetʳRel {G} H = H \\ G

max_stars_repo_name: zampino/ggt

max_issues_repo_name: zampino/ggt

max_forks_repo_name: zampino/ggt


text:
------------------------------------------------------------------------
-- Code related to the paper "Compiling Programs with Erased
-- Univalence"
--
-- Nils Anders Danielsson
--
-- The paper is coauthored with Andreas Abel and Andrea Vezzosi.
------------------------------------------------------------------------

-- Most of the code referenced below can be found in modules that are
-- parametrised by a notion of equality. One can use them both with
-- Cubical Agda paths and with the Cubical Agda identity type family.

-- Note that the code does not follow the paper exactly. For instance,
-- some definitions use bijections (functions with quasi-inverses)
-- instead of equivalences.

-- An attempt has been made to track uses of univalence by passing
-- around explicit proofs of the univalence axiom (except in certain
-- README modules). However, some library code that is used does not
-- adhere to this convention (note that univalence is provable in
-- Cubical Agda), so perhaps some use of univalence is not tracked in
-- this way. On the other hand some library code that is not defined
-- in Cubical Agda passes around explicit proofs of function
-- extensionality.

-- Some other differences are mentioned below.

-- Note that there is a known problem with guarded corecursion in
-- Agda. Due to "quantifier inversion" (see "Termination Checking in
-- the Presence of Nested Inductive and Coinductive Types" by Thorsten
-- Altenkirch and myself) certain types may not have the expected
-- semantics when the option --guardedness is used. I expect that the
-- results would still hold if this bug were fixed, but because I do
-- not know what the rules of a fixed version of Agda would be I do
-- not know if any changes to the code would be required.

{-# OPTIONS --guardedness #-}

module README.Compiling-Programs-with-Erased-Univalence where

import Coherently-constant
import Colimit.Sequential
import Colimit.Sequential.Very-erased
import Equality.Path
import Equality.Path.Univalence
import Equivalence
import Equivalence.Erased
import Equivalence.Erased.Basics
import Equivalence.Erased.Contractible-preimages
import Equivalence.Half-adjoint
import Erased.Basics
import Erased.Cubical
import Erased.Level-1
import Erased.Stability
import H-level.Truncation.Propositional
import H-level.Truncation.Propositional.Completely-erased
import H-level.Truncation.Propositional.Erased
import H-level.Truncation.Propositional.Non-recursive
import H-level.Truncation.Propositional.Non-recursive.Erased
import H-level.Truncation.Propositional.One-step
import Preimage
import Univalence-axiom

import Lens.Non-dependent.Higher
import Lens.Non-dependent.Higher.Erased
import Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant
import Lens.Non-dependent.Higher.Coinductive
import Lens.Non-dependent.Higher.Coinductive.Erased
import Lens.Non-dependent.Higher.Coinductive.Small
import Lens.Non-dependent.Higher.Coinductive.Small.Erased

import README.Fst-snd

------------------------------------------------------------------------
-- 2: Cubical Agda

-- The functions cong and ext.

cong = Equality.Path.cong
ext  = Equality.Path.⟨ext⟩

-- The propositional truncation operator.
--
-- The current module uses --erased-cubical, so this operator, which
-- is defined using --cubical, can only be used in erased contexts.

@0 ∥_∥ : _
∥_∥ = H-level.Truncation.Propositional.∥_∥

-- The map function. This function is not defined in the same way as
-- in the paper, it is defined using a non-dependent eliminator.

@0 map : _
map = H-level.Truncation.Propositional.∥∥-map

-- The propositional truncation operator with an erased truncation
-- constructor.

∥_∥ᴱ = H-level.Truncation.Propositional.Erased.∥_∥ᴱ

-- Half adjoint equivalences. Note that, unlike in the paper, _≃_ is
-- defined as a record type.

Is-equivalence = Equivalence.Half-adjoint.Is-equivalence
_≃_            = Equivalence._≃_

-- Univalence. (This type family is not defined in exactly the same
-- way as in the paper.)

Univalence = Univalence-axiom.Univalence

-- A proof of univalence. The proof uses glue.

@0 univ : _
univ = Equality.Path.Univalence.univ

------------------------------------------------------------------------
-- 3: Postulating Erased Univalence

-- Erased.

Erased = Erased.Basics.Erased

-- []-cong for paths.

[]-cong = Erased.Cubical.[]-cong-Path

------------------------------------------------------------------------
-- 6.1: Equivalences with Erased Proofs

-- Equivalences with erased proofs. Note that, unlike in the paper,
-- _≃ᴱ_ is defined as a record type.

Is-equivalenceᴱ = Equivalence.Erased.Basics.Is-equivalenceᴱ
_≃ᴱ_            = Equivalence.Erased.Basics._≃ᴱ_
to              = Equivalence.Erased.Basics._≃ᴱ_.to
from            = Equivalence.Erased.Basics._≃ᴱ_.from
@0 to-from : _
to-from         = Equivalence.Erased.Basics._≃ᴱ_.right-inverse-of
@0 from-to : _
from-to         = Equivalence.Erased.Basics._≃ᴱ_.left-inverse-of

-- Erased≃ is stated a little differently.

Erased≃ = Erased.Level-1.Erased↔

-- Lemmas 41 and 42 are proved in modules parametrised by definitions
-- of []-cong, in the latter case []-cong is also assumed to satisfy
-- certain properties (that hold for the definition mentioned above).
-- Some definitions below are also defined in such modules.

Lemma-41 = Erased.Level-1.[]-cong₁.Erased-cong-≃
Lemma-42 = Equivalence.Erased.[]-cong.Σ-cong-≃ᴱ-Erased

-- The functions substᴱ and subst.

substᴱ = Erased.Level-1.[]-cong₁.substᴱ
subst  = Equality.Path.subst

-- Lemmas 45–47.

Lemma-45 = Equivalence.Erased.[]-cong.drop-⊤-left-Σ-≃ᴱ-Erased
Lemma-46 = Equivalence.Erased.Σ-cong-≃ᴱ
Lemma-47 = Equivalence.Erased.drop-⊤-left-Σ-≃ᴱ

------------------------------------------------------------------------
-- 6.2: A Non-recursive Definition of the Propositional Truncation
-- Operator

-- ∥_∥¹ and Colimit.

@0 ∥_∥¹ : _
∥_∥¹ = H-level.Truncation.Propositional.One-step.∥_∥¹
@0 Colimit : _
Colimit = Colimit.Sequential.Colimit

-- Lemma 50.

@0 Lemma-50 : _
Lemma-50 = Colimit.Sequential.universal-property

-- ∥_∥¹-out and ∥_∥ᴺ.

@0 ∥_∥¹-out : _
∥_∥¹-out = H-level.Truncation.Propositional.One-step.∥_∥¹-out-^
@0 ∥_∥ᴺ : _
∥_∥ᴺ = H-level.Truncation.Propositional.Non-recursive.∥_∥

-- ∥_∥ᴺ and ∥_∥ are pointwise equivalent.

@0 ∥∥ᴺ≃∥∥ : _
∥∥ᴺ≃∥∥ = H-level.Truncation.Propositional.Non-recursive.∥∥≃∥∥

-- Colimitᴱ.

Colimitᴱ = Colimit.Sequential.Very-erased.Colimitᴱ

-- Lemma 54.

Lemma-54 = Colimit.Sequential.Very-erased.universal-property

-- ∥_∥ᴺᴱ.

∥_∥ᴺᴱ = H-level.Truncation.Propositional.Non-recursive.Erased.∥_∥ᴱ

-- Lemma 56 (or rather its inverse).

Lemma-56 = H-level.Truncation.Propositional.Erased.∥∥ᴱ≃∥∥ᴱ

------------------------------------------------------------------------
-- 6.3: Higher Lenses with Erased Proofs

-- Lensᴱ, get and set.

@0 Lensᴱ : _
Lensᴱ = Lens.Non-dependent.Higher.Lens
@0 get : _
get = Lens.Non-dependent.Higher.Lens.get
@0 set : _
set = Lens.Non-dependent.Higher.Lens.set

-- Lensᴱᴱ.

Lensᴱᴱ = Lens.Non-dependent.Higher.Erased.Lens

-- The function _⁻¹_.

_⁻¹_ = Preimage._⁻¹_

-- Lens^C (defined using a record type).

@0 Lens^C : _
Lens^C = Lens.Non-dependent.Higher.Coinductive.Small.Lens

-- Coherently-constant^C.

@0 Coherently-constant^C : _
Coherently-constant^C =
  Lens.Non-dependent.Higher.Coinductive.Small.Coherently-constant

-- Lens^CE (with the field name get⁻¹-coherently-constant instead of
-- cc).

Lens^CE = Lens.Non-dependent.Higher.Coinductive.Small.Erased.Lens

------------------------------------------------------------------------
-- 6.4: The Definitions Are Equivalent

-- Lemma 65 (or rather its inverse), and a proof (in an erased
-- context) showing that Lemma 65 preserves getters and setters.
--
-- Lemma 65 and some other lemmas use arguments of type Block s (for
-- some string s). This type is equivalent to the unit type. These
-- arguments are used to block definitions from being unfolded by the
-- type-checker.

Lemma-65 =
  Lens.Non-dependent.Higher.Coinductive.Small.Erased.Lens≃ᴱLensᴱ
@0 Lemma-65-preserves-getters-and-setters : _
Lemma-65-preserves-getters-and-setters =
  Lens.Non-dependent.Higher.Coinductive.Small.Erased.Lens≃ᴱLensᴱ-preserves-getters-and-setters

-- Lens₁ᴱ and Lens₂ᴱ.

Lens₁ᴱ = Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant.Lens
Lens₂ᴱ = Lens.Non-dependent.Higher.Coinductive.Erased.Lens

-- The function _⁻¹ᴱ_.

_⁻¹ᴱ_ = Equivalence.Erased.Contractible-preimages._⁻¹ᴱ_

-- Coherently-constant₁ᴱ, Coherently-constant, Coherently-constant₂ᴱ,
-- Coherently-constant₂^C and constant.

Coherently-constant₁ᴱ =
  Lens.Non-dependent.Higher.Capriotti.Variant.Erased.Variant.Coherently-constant
@0 Coherently-constant : _
Coherently-constant = Coherently-constant.Coherently-constant
Coherently-constant₂ᴱ =
  Lens.Non-dependent.Higher.Coinductive.Erased.Coherently-constant
@0 Coherently-constant₂^C : _
Coherently-constant₂^C =
  Lens.Non-dependent.Higher.Coinductive.Coherently-constant
@0 constant : _
constant = Lens.Non-dependent.Higher.Coinductive.constant

-- Lemmas 74–77.

Lemma-74 = Erased.Stability.[]-cong.Erased-other-singleton≃ᴱ⊤
Lemma-75 = Lens.Non-dependent.Higher.Coinductive.Erased.∥∥ᴱ→≃
Lemma-76 = Equivalence.Erased.other-singleton-with-Π-≃ᴱ-≃ᴱ-⊤
Lemma-77 = H-level.Truncation.Propositional.Erased.Σ-Π-∥∥ᴱ-Erased-≡-≃

------------------------------------------------------------------------
-- 6.5: Compilation of Lenses

-- A slightly more general variant of sndᴱ.

sndᴱ = Lens.Non-dependent.Higher.Erased.snd

-- Lemma 79.

Lemma-79 =
  H-level.Truncation.Propositional.Completely-erased.Erased-∥∥×≃

-- A slightly more general variant of snd^C.

snd^C = README.Fst-snd.snd-with-space-leak

-- Lemma 81.

Lemma-81 =
  Lens.Non-dependent.Higher.Coinductive.Small.Erased.with-other-setter

-- A slightly more general variant of the variant of snd^C with a
-- changed setter.

snd^C-with-changed-setter = README.Fst-snd.snd

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
module ASN1.X509 where

open import Data.Word8 using (Word8; _and_; _or_; _==_) renaming (primWord8fromNat to to𝕎; primWord8toNat to from𝕎)
open import Data.ByteString using (ByteString; Strict; pack; fromChunks; toStrict)
open import Data.ByteString.Utf8 using (packStrict)
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_; _*_)
open import Data.List using (List; []; _∷_; foldl)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_)
open import Data.String using (String)

open import ASN1.Untyped
import ASN1.BER as BER

AlgorithmIdentifier : List ℕ → AST → AST
AlgorithmIdentifier oid params = SEQUENCE (OBJECT-IDENTIFIER oid ∷ params ∷ [])

AttributeTypeAndValue : List ℕ → AST → AST
AttributeTypeAndValue type value = SEQUENCE (OBJECT-IDENTIFIER type ∷ value ∷ [])

id-at-commonName : List ℕ
id-at-commonName = 2 ∷ 5 ∷ 4 ∷ 3 ∷ []

CommonName : String → AST
CommonName cn = AttributeTypeAndValue id-at-commonName (UTF8String cn)

RDN : String → AST
RDN cn = SET (CommonName cn ∷ [])

RDNSequence : String → AST
RDNSequence cn = SEQUENCE (RDN cn ∷ [])

Name : String → AST
Name cn = RDNSequence cn

Validity : (from to : String) → AST
Validity from to = SEQUENCE (GeneralizedTime from ∷ GeneralizedTime to ∷ [])

bign-with-hbelt-oid : List ℕ
bign-with-hbelt-oid = 1 ∷ 2 ∷ 112 ∷ 0 ∷ 2 ∷ 0 ∷ 34 ∷ 101 ∷ 45 ∷ 12 ∷ []

bign-pubkey-oid : List ℕ
bign-pubkey-oid = 1 ∷ 2 ∷ 112 ∷ 0 ∷ 2 ∷ 0 ∷ 34 ∷ 101 ∷ 45 ∷ 2 ∷ 1 ∷ []

bign-curve256v1-oid : List ℕ
bign-curve256v1-oid = 1 ∷ 2 ∷ 112 ∷ 0 ∷ 2 ∷ 0 ∷ 34 ∷ 101 ∷ 45 ∷ 3 ∷ 1 ∷ []

SubjectPublicKeyInfo : ByteString Strict → AST
SubjectPublicKeyInfo pub = SEQUENCE
  ( AlgorithmIdentifier bign-pubkey-oid (OBJECT-IDENTIFIER bign-curve256v1-oid)
  ∷ BIT-STRING 0 pub ∷ [])

Extension : OID → (critical : Bool) → ByteString Strict → AST
Extension oid true value = SEQUENCE (OBJECT-IDENTIFIER oid ∷ BOOLEAN true ∷ OCTET-STRING value ∷ [])
Extension oid false value = SEQUENCE (OBJECT-IDENTIFIER oid ∷ OCTET-STRING value ∷ [])

module mkCert
  (issuer-cn : String)
  (subject-cn : String)
  (validity-from : String)
  (validity-to : String)
  (pub : ByteString Strict)
  (sign : ByteString Strict → ByteString Strict) -- tbs → sig
  where

  sa version serial issuer validity subject spki : AST
  sa = AlgorithmIdentifier bign-with-hbelt-oid NULL
  version = EXPLICIT (to𝕎 0) (INTEGER 2) -- v3
  serial = INTEGER 1
  issuer = Name issuer-cn
  validity = Validity validity-from validity-to
  subject = Name subject-cn
  spki = SubjectPublicKeyInfo pub
  {-
  ku
  eku
  skid
  ikid
  -- id-ce = 2 ∷ 5 ∷ 29 ∷ []
  -}
  id-ce-arc : OID → OID
  id-ce-arc tail = 2 ∷ 5 ∷ 29 ∷ tail
  id-kp-arc : OID → OID
  id-kp-arc tail = 1 ∷ 3 ∷ 6 ∷ 1 ∷ 5 ∷ 5 ∷ 7 ∷ 3 ∷ tail

  ku-oid : OID
  ku-oid = id-ce-arc (15 ∷ [])
  data KeyUsage : Set where
    digitalSignature nonRepudation keyEncipherment dataEncipherment
      keyAgreement keyCertSign cRLSign encipherOnly decipherOnly : KeyUsage
  pattern contentCommitment = nonRepudation
  ku : List KeyUsage → AST
  ku kus = Extension ku-oid true (BER.encode″ (BIT-STRING 7 (pack (w₀ ∷ w₁ ∷ [])))) where
    kuIdx : KeyUsage → ℕ
    kuIdx digitalSignature = 0
    kuIdx nonRepudation = 1
    kuIdx keyEncipherment = 2
    kuIdx dataEncipherment = 3
    kuIdx keyAgreement = 4
    kuIdx keyCertSign = 5
    kuIdx cRLSign = 6
    kuIdx encipherOnly = 7
    kuIdx decipherOnly = 8

    i₀ i₁ : KeyUsage → Word8
    i₀ digitalSignature = to𝕎 0x80
    i₀ nonRepudation = to𝕎 0x40
    i₀ keyEncipherment = to𝕎 0x20
    i₀ dataEncipherment = to𝕎 0x10
    i₀ keyAgreement = to𝕎 0x08
    i₀ keyCertSign = to𝕎 0x04
    i₀ cRLSign = to𝕎 0x02
    i₀ encipherOnly = to𝕎 0x01
    i₀ decipherOnly = to𝕎 0
    i₁ digitalSignature = to𝕎 0
    i₁ nonRepudation = to𝕎 0
    i₁ keyEncipherment = to𝕎 0
    i₁ dataEncipherment = to𝕎 0
    i₁ keyAgreement = to𝕎 0
    i₁ keyCertSign = to𝕎 0
    i₁ cRLSign = to𝕎 0
    i₁ encipherOnly = to𝕎 0
    i₁ decipherOnly = to𝕎 0x80

    f₀ f₁ : Word8 → KeyUsage → Word8
    f₀ w u = w or (i₀ u)
    f₁ w u = w or (i₁ u)
    w₀ w₁ : Word8
    w₀ = foldl f₀ (to𝕎 0) kus
    w₁ = foldl f₁ (to𝕎 0) kus

  id-kp-serverAuth id-kp-clientAuth : OID
  id-kp-serverAuth = id-kp-arc (1 ∷ [])
  id-kp-clientAuth = id-kp-arc (2 ∷ [])

  eku-oid : OID
  eku-oid = id-ce-arc (37 ∷ [])
  eku : AST
  eku = Extension eku-oid false (BER.encode″ (SEQUENCE (OBJECT-IDENTIFIER id-kp-serverAuth ∷ OBJECT-IDENTIFIER id-kp-clientAuth ∷ [])))

  bc-oid : OID
  bc-oid = id-ce-arc (19 ∷ [])
  bc : AST
  bc = Extension bc-oid true (BER.encode″ (SEQUENCE (BOOLEAN is-ca-true ∷ []))) where
    is-ca-true : Bool
    is-ca-true = true

  exts : AST
  exts = EXPLICIT (tag 3) (SEQUENCE (bc ∷ ku (keyAgreement ∷ []) ∷ eku ∷ []))

  tbs : AST
  tbs = SEQUENCE (version ∷ serial ∷ sa ∷ issuer ∷ validity ∷ subject ∷ spki ∷ exts ∷ [])
  tbs′ : ByteString Strict
  tbs′ = toStrict (fromChunks (BER.encode tbs))
  sig : ByteString Strict
  sig = sign tbs′

  sv : AST
  sv = BIT-STRING 0 sig
  cert : AST
  cert = SEQUENCE (tbs ∷ sa ∷ sv ∷ [])


text:
{-

Elementary transformation specific to coefficient ℤ

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.IntegerMatrix.Elementaries where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Nat hiding (_+_ ; _·_)
open import Cubical.Data.FinData

open import Cubical.Relation.Nullary

open import Cubical.Algebra.RingSolver.Reflection
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤ to Ringℤ)

open import Cubical.Algebra.Matrix
open import Cubical.Algebra.Matrix.CommRingCoefficient
open import Cubical.Algebra.Matrix.RowTransformation

private
  variable
    ℓ : Level
    m n : ℕ

-- It seems there are bugs when applying ring solver to integers.
-- The following is a work-around.
private
  module Helper {ℓ : Level}(𝓡 : CommRing ℓ) where
    open CommRingStr (𝓡 .snd)

    helper1 : (a b x y g : 𝓡 .fst) → (a · x - b · - y) · g ≡ a · (x · g) + b · (y · g)
    helper1 = solve 𝓡

    helper2 : (a b : 𝓡 .fst) → a ≡ 1r · a + 0r · b
    helper2 = solve 𝓡

open Helper Ringℤ

module ElemTransformationℤ where

  open import Cubical.Foundations.Powerset

  open import Cubical.Data.Int using (·rCancel)
  open import Cubical.Data.Int.Divisibility

  private
    ℤ = Ringℤ .fst

  open CommRingStr      (Ringℤ .snd)
  open Sum              (CommRing→Ring Ringℤ)

  open Coefficient Ringℤ
  open LinearTransformation Ringℤ
  open Bézout

  open SimRel
  open Sim

  open isLinear
  open isLinear2×2

  -- The Bézout step to simplify one row

  module _
    (x y : ℤ)(b : Bézout x y) where

    bézout2Mat : Mat 2 2
    bézout2Mat zero zero = b .coef₁
    bézout2Mat zero one  = b .coef₂
    bézout2Mat one  zero = - (div₂ b)
    bézout2Mat one  one  = div₁ b

    module _
      (p : ¬ x ≡ 0) where

      open Units Ringℤ

      private
        detEq : det2×2 bézout2Mat · b .gcd ≡ b .gcd
        detEq =
            helper1 (b .coef₁) (b .coef₂) _ _ _
          ∙ (λ t → b .coef₁ · divideEq (b .isCD .fst) t + b .coef₂ · divideEq (b .isCD .snd) t)
          ∙ b .identity

        det≡1 : det2×2 bézout2Mat ≡ 1
        det≡1 = ·rCancel _ _ _ (detEq ∙ sym (·Lid _)) (¬m≡0→¬gcd≡0 b p)

      isInvBézout2Mat : isInv bézout2Mat
      isInvBézout2Mat = isInvMat2x2 bézout2Mat (subst (λ r → r ∈ Rˣ) (sym det≡1) RˣContainsOne)

  module _
    (M : Mat 2 (suc n)) where

    private
      b = bézout (M zero zero) (M one zero)

    bézout2Rows : Mat 2 (suc n)
    bézout2Rows zero i =   b .coef₁ · M zero i +  b .coef₂ · M one i
    bézout2Rows one  i = - (div₂ b) · M zero i +    div₁ b · M one i

    bézout2Rows-vanish : bézout2Rows one zero ≡ 0
    bézout2Rows-vanish = div·- b

    bézout2Rows-div₁ : (n : ℤ) → M zero zero ∣ n → bézout2Rows zero zero ∣ n
    bézout2Rows-div₁ n p = subst (λ a → a ∣ n) (sym (b .identity)) (∣-trans (b .isCD .fst) p)

    bézout2Rows-div₂ : (n : ℤ) → M one  zero ∣ n → bézout2Rows zero zero ∣ n
    bézout2Rows-div₂ n p = subst (λ a → a ∣ n) (sym (b .identity)) (∣-trans (b .isCD .snd) p)

    bézout2Rows-nonZero : ¬ M zero zero ≡ 0 → ¬ bézout2Rows zero zero ≡ 0
    bézout2Rows-nonZero p r =
      p (sym (∣-zeroˡ (subst (λ a → a ∣ M zero zero) r (bézout2Rows-div₁ (M zero zero) (∣-refl refl)))))

    bézout2Rows-inv : ¬ M zero zero ≡ 0 → M zero zero ∣ M one zero → M zero ≡ bézout2Rows zero
    bézout2Rows-inv p q t j =
      let (c₁≡1 , c₂≡0) = bézout∣ _ _ p q in
      (helper2 (M zero j) (M one j) ∙ (λ t → c₁≡1 (~ t) · M zero j + c₂≡0 (~ t) · M one j)) t

    bézout2Rows-commonDiv : (a : ℤ)
      → ((j : Fin (suc n)) → a ∣ M zero j)
      → ((j : Fin (suc n)) → a ∣ M one  j)
      →  (i : Fin 2)(j : Fin (suc n)) → a ∣ bézout2Rows i j
    bézout2Rows-commonDiv a p q zero j = ∣-+ (∣-right· {n =   b .coef₁} (p j)) (∣-right· {n = b .coef₂} (q j))
    bézout2Rows-commonDiv a p q one  j = ∣-+ (∣-right· {n = - (div₂ b)} (p j)) (∣-right· {n =   div₁ b} (q j))

  module _
    (M : Mat (suc m) (suc n)) where

    bézoutRows : Mat (suc m) (suc n)
    bézoutRows = transRows bézout2Rows M

    bézoutRows-vanish : (i : Fin m) → bézoutRows (suc i) zero ≡ 0
    bézoutRows-vanish = transRowsIndP' _ (λ v → v zero ≡ 0) bézout2Rows-vanish M

    bézoutRows-div₁-helper : (n : ℤ) → M zero zero ∣ n → bézoutRows zero zero ∣ n
    bézoutRows-div₁-helper n = transRowsIndP _ (λ v → v zero ∣ n) (λ M → bézout2Rows-div₁ M n) M

    bézoutRows-div₂-helper : (n : ℤ) → (i : Fin m) → M (suc i) zero ∣ n → bézoutRows zero zero ∣ n
    bézoutRows-div₂-helper n =
      transRowsIndPQ' _ (λ v → v zero ∣ n) (λ v → v zero ∣ n)
        (λ M → bézout2Rows-div₁ M n) (λ M → bézout2Rows-div₂ M n) M

    bézoutRows-div : (i : Fin (suc m)) → bézoutRows zero zero ∣ M i zero
    bézoutRows-div zero    = bézoutRows-div₁-helper _   (∣-refl refl)
    bézoutRows-div (suc i) = bézoutRows-div₂-helper _ i (∣-refl refl)

    bézoutRows-nonZero : ¬ M zero zero ≡ 0 → ¬ bézoutRows zero zero ≡ 0
    bézoutRows-nonZero p r = p (sym (∣-zeroˡ (subst (λ a → a ∣ M zero zero) r (bézoutRows-div zero))))

    bézoutRows-inv : ¬ M zero zero ≡ 0 → ((i : Fin m) → M zero zero ∣ M (suc i) zero) → M zero ≡ bézoutRows zero
    bézoutRows-inv = transRowsIndPRelInv _ (λ V → ¬ V zero ≡ 0) (λ U V → U zero ∣ V zero) bézout2Rows-inv M

    bézoutRows-commonDiv₀ : (a : ℤ)
      → ((j : Fin (suc n)) → a ∣ M zero j)
      → ((i : Fin m)(j : Fin (suc n)) → a ∣ M (suc i) j)
      →  (j : Fin (suc n)) → a ∣ bézoutRows zero j
    bézoutRows-commonDiv₀ a =
      transRowsIndP₀ _ (λ V → ((j : Fin (suc n)) → a ∣ V j))
        (λ N s s' → bézout2Rows-commonDiv N a s s' zero)
        (λ N s s' → bézout2Rows-commonDiv N a s s' one) _

    bézoutRows-commonDiv₁ : (a : ℤ)
      → ((j : Fin (suc n)) → a ∣ M zero j)
      → ((i : Fin m)(j : Fin (suc n)) → a ∣ M (suc i) j)
      →  (i : Fin m)(j : Fin (suc n)) → a ∣ bézoutRows (suc i) j
    bézoutRows-commonDiv₁ a =
      transRowsIndP₁ _ (λ V → ((j : Fin (suc n)) → a ∣ V j))
        (λ N s s' → bézout2Rows-commonDiv N a s s' zero)
        (λ N s s' → bézout2Rows-commonDiv N a s s' one) _

    bézoutRows-commonDiv :
        ((i : Fin (suc m))(j : Fin (suc n)) → M zero zero ∣ M i j)
      →  (i : Fin (suc m))(j : Fin (suc n)) → M zero zero ∣ bézoutRows i j
    bézoutRows-commonDiv p zero    = bézoutRows-commonDiv₀ _ (p zero) (p ∘ suc)
    bézoutRows-commonDiv p (suc i) = bézoutRows-commonDiv₁ _ (p zero) (p ∘ suc) i

    bézoutRows-commonDivInv :
        ¬ M zero zero ≡ 0
      → ((i : Fin (suc m))(j : Fin (suc n)) → M zero zero ∣ M i j)
      →  (i : Fin (suc m))(j : Fin (suc n)) → bézoutRows zero zero ∣ bézoutRows i j
    bézoutRows-commonDivInv h p i j =
      let inv = (λ t → bézoutRows-inv h (λ i → p (suc i) zero) t zero) in
      subst (_∣ bézoutRows i j) inv (bézoutRows-commonDiv p i j)

  isLinear2Bézout2Rows : isLinear2×2 (bézout2Rows {n = n})
  isLinear2Bézout2Rows .transMat M = bézout2Mat _ _ (bézout (M zero zero) (M one zero))
  isLinear2Bézout2Rows .transEq  M t zero j = mul2 (isLinear2Bézout2Rows .transMat M) M zero j (~ t)
  isLinear2Bézout2Rows .transEq  M t one  j = mul2 (isLinear2Bézout2Rows .transMat M) M one  j (~ t)

  isLinearBézoutRows : isLinear (bézoutRows {m = m} {n = n})
  isLinearBézoutRows = isLinearTransRows _ isLinear2Bézout2Rows _

  isInv2Bézout2Rows : (M : Mat 2 (suc n))(p : ¬ M zero zero ≡ 0) → isInv (isLinear2Bézout2Rows .transMat M)
  isInv2Bézout2Rows _ p = isInvBézout2Mat _ _ _ p

  isInvBézout2Rows : (M : Mat (suc m) (suc n))(p : ¬ M zero zero ≡ 0) → isInv (isLinearBézoutRows .transMat M)
  isInvBézout2Rows = isInvTransRowsInd _ _ (λ V → ¬ V zero ≡ 0) bézout2Rows-nonZero isInv2Bézout2Rows

  -- Using Bézout identity to eliminate the first column/row

  record RowsImproved (M : Mat (suc m) (suc n)) : Type where
    field
      sim : Sim M

      div     : (i : Fin (suc m)) → sim .result zero zero ∣ M i zero
      vanish  : (i : Fin m) → sim .result (suc i) zero ≡ 0
      nonZero : ¬ sim .result zero zero ≡ 0

  record ColsImproved (M : Mat (suc m) (suc n)) : Type where
    field
      sim : Sim M

      div     : (j : Fin (suc n)) → sim .result zero zero ∣ M zero j
      vanish  : (j : Fin n) → sim .result zero (suc j) ≡ 0
      nonZero : ¬ sim .result zero zero ≡ 0

  open RowsImproved
  open ColsImproved

  improveRows : (M : Mat (suc m) (suc n))(p : ¬ M zero zero ≡ 0) → RowsImproved M
  improveRows M _ .sim .result   = bézoutRows M
  improveRows M _ .sim .simrel .transMatL = isLinearBézoutRows .transMat M
  improveRows _ _ .sim .simrel .transMatR = 𝟙
  improveRows _ _ .sim .simrel .transEq   = isLinearBézoutRows .transEq _ ∙ sym (⋆rUnit _)
  improveRows _ p .sim .simrel .isInvTransL = isInvBézout2Rows _ p
  improveRows _ p .sim .simrel .isInvTransR = isInv𝟙
  improveRows _ _ .div     = bézoutRows-div     _
  improveRows _ _ .vanish  = bézoutRows-vanish  _
  improveRows M p .nonZero = bézoutRows-nonZero M p

  improveCols : (M : Mat (suc m) (suc n))(p : ¬ M zero zero ≡ 0) → ColsImproved M
  improveCols M _ .sim .result    = (bézoutRows (M ᵗ))ᵗ
  improveCols _ _ .sim .simrel .transMatL = 𝟙
  improveCols M _ .sim .simrel .transMatR = (isLinearBézoutRows .transMat (M ᵗ))ᵗ
  improveCols M _ .sim .simrel .transEq     =
    let P = isLinearBézoutRows .transMat (M ᵗ) in
      (λ t → (isLinearBézoutRows .transEq (M ᵗ) t)ᵗ)
    ∙ compᵗ P (M ᵗ)
    ∙ (λ t → idemᵗ M t ⋆ P ᵗ)
    ∙ (λ t → ⋆lUnit M (~ t) ⋆ P ᵗ)
  improveCols _ _ .sim .simrel .isInvTransL = isInv𝟙
  improveCols M p .sim .simrel .isInvTransR =
    isInvᵗ {M = isLinearBézoutRows .transMat (M ᵗ)} (isInvBézout2Rows (M ᵗ) p)
  improveCols _ _ .div     = bézoutRows-div     _
  improveCols _ _ .vanish  = bézoutRows-vanish  _
  improveCols M p .nonZero = bézoutRows-nonZero (M ᵗ) p

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
postulate
  A   : Set
  _+_ : A → A → A

f₁ : A → A → A
f₁ x y = {!_+ x!}  -- ? + x

f₂ : A → A → A
f₂ x y = {!x +_!}  -- x + ?

f₃ : A → A → A
f₃ x = {!_+ x!}  -- λ section → section + x

f₄ : A → A → A
f₄ x y = {!λ z → z + x!} -- ? + x

f₅ : A → A → A
f₅ x y = {!λ a b → b + x!}  -- ? + x

f₆ : A → A → A
f₆ x y = {!λ a → a + (a + x)!} -- (λ a → a + (a + x)) ?

f₇ : A → A → A
f₇ x y = {!λ a → x + (y + a)!}  -- x + (y + ?)

f₈ : A → A → A
f₈ x = {!λ a b → a + b!} -- λ b → ? + b


text:
open import Relation.Binary hiding (_⇒_)

module Experiments.Category {ℓ₁ ℓ₂ ℓ₃} (APO : Preorder ℓ₁ ℓ₂ ℓ₃) where

open import Level
open Preorder APO renaming (_∼_ to _≤_)

open import Function as Fun using (flip)
open import Relation.Unary using (Pred)
open import Data.Product as Prod using (_,_; _×_)
open import Relation.Binary.PropositionalEquality as PEq using (_≡_; cong)
open PEq.≡-Reasoning
open import Function.Inverse using (Inverse)
open import Algebra.FunctionProperties

record IsMP {ℓ}(P : Pred Carrier ℓ) : Set (ℓ ⊔ ℓ₁ ⊔ ℓ₃) where
  field
    monotone : ∀ {c c'} → c ≤ c' → P c → P c'

    monotone-refl  : ∀ {c} p → monotone (refl {c}) p PEq.≡ p
    monotone-trans : ∀ {c c' c''} p (c~c' : c ≤ c')(c'~c'' : c' ≤ c'') →
                     monotone (trans c~c' c'~c'') p
                     PEq.≡
                     monotone c'~c'' (monotone c~c' p)

-- monotone predicates over a fixed carrier
record MP ℓ : Set (suc ℓ ⊔ ℓ₁ ⊔ ℓ₃) where
  constructor mp
  field
    pred  : Pred Carrier ℓ
    is-mp : IsMP pred

  open IsMP is-mp public

MP₀ = MP zero

-- application
_·_ : ∀ {ℓ} → MP ℓ → Carrier → Set _
(mp P _) · c = P c

-- monotone-predicate equality
_≗_ : ∀ {ℓ₁} → MP ℓ₁ → MP ℓ₁ → Set _
P ≗ Q = ∀ {c} → P · c PEq.≡ Q · c

import Data.Unit as Unit

Const : ∀ {ℓ}(P : Set ℓ) → MP ℓ
Const P = mp (λ _ → P) (record {
    monotone = λ x p → p ;
    monotone-refl = λ p → PEq.refl ;
    monotone-trans = λ p c~c' c'~c'' → PEq.refl
  })

⊤ : MP zero
⊤ = Const Unit.⊤

-- we package the Agda function that represents morphisms
-- in this category in a record such that P ⇒ Q doesn't get
-- reduced to the simple underlying type of `apply`
infixl 30 _⇒_
record _⇒_ {p q}(P : MP p)(Q : MP q) : Set (p ⊔ q ⊔ ℓ₁ ⊔ ℓ₃) where
  constructor mk⇒

  field
    apply         : ∀ {c} → P · c → Q · c

    monotone-comm : ∀ {c c'}(c~c' : c ≤ c'){p : P · c} →
                    apply {c'} (MP.monotone P c~c' p) PEq.≡ MP.monotone Q c~c' (apply p)

open _⇒_ public

-- Const identifies objects that are terminal for this category
terminal : ∀ {ℓ a}{A : Set a}{P : MP ℓ} → A → P ⇒ Const A
terminal x = mk⇒ (λ _ → x) λ c~c' → λ {p} → PEq.refl

infixl 100 _∘_
_∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃}{P : MP ℓ₁}{Q : MP ℓ₂}{R : MP ℓ₃} → Q ⇒ R → P ⇒ Q → P ⇒ R
_∘_ {P = P}{Q}{R} F G = mk⇒
  (λ p → apply F (apply G p))
  (λ c~c' →
    begin _
      ≡⟨ PEq.cong (λ e → apply F e) (monotone-comm G c~c') ⟩
    apply F (MP.monotone Q c~c' (apply G _))
      ≡⟨ monotone-comm F c~c' ⟩
    _ ∎
  )

id : ∀ {ℓ}(P : MP ℓ) → P ⇒ P
id P = mk⇒ Fun.id (λ _ → PEq.refl)

-- morphism equality
infixl 20 _⇒≡_
_⇒≡_  : ∀ {ℓ₁ ℓ₂}{P : MP ℓ₁}{Q : MP ℓ₂}(F G : P ⇒ Q) → Set _
_⇒≡_ {P = P}{Q} F G = ∀ {c}(p : P · c) → apply F p PEq.≡ apply G p

-- extensionality for morphisms
-- This should be provable from proof-irrelevance + extensionality.
⇒-Ext : ∀ (ℓ₁ ℓ₂ : Level) → Set _
⇒-Ext ℓ₁ ℓ₂ = ∀ {P : MP ℓ₁}{Q : MP ℓ₂}{F G : P ⇒ Q} → F ⇒≡ G → F PEq.≡ G

-- isomorphism
record _≅_ {ℓ}(P Q : MP ℓ) : Set (ℓ₁ ⊔ ℓ ⊔ ℓ₃) where
  field
    to    : P ⇒ Q
    from  : Q ⇒ P
    left-inv  : to ∘ from ⇒≡ id Q
    right-inv : from ∘ to ⇒≡ id P

∘-assoc : ∀ {p q r s}{P : MP p}{Q : MP q}{R : MP r}{S : MP s}
            {F : R ⇒ S}{G : Q ⇒ R}{H : P ⇒ Q} →
            F ∘ (G ∘ H) ⇒≡ (F ∘ G) ∘ H
∘-assoc _ = PEq.refl

∘-left-id : ∀ {P Q : MP ℓ₁}{F : P ⇒ Q} → (id Q) ∘ F ⇒≡ F
∘-left-id _ = PEq.refl

∘-right-id : ∀ {P Q : MP ℓ₁}{F : P ⇒ Q} → F ∘ (id P) ⇒≡ F
∘-right-id p = PEq.refl

module Product where
  -- within the category

  infixl 40 _⊗_
  _⊗_ : ∀ {ℓ₁ ℓ₂} → MP ℓ₁ → MP ℓ₂ → MP (ℓ₁ ⊔ ℓ₂)
  P ⊗ Q = mp
      (λ c → (P · c) × (Q · c))
      (record {
        monotone = λ{ c~c' (p , q) →
            MP.monotone P c~c' p
          , MP.monotone Q c~c' q
        };
        monotone-refl = λ _ → PEq.cong₂ _,_ (MP.monotone-refl P _) (MP.monotone-refl Q _) ;
        monotone-trans = λ _ _ _ → PEq.cong₂ _,_ (MP.monotone-trans P _ _ _) (MP.monotone-trans Q _ _ _)
      })

  ⟨_,_⟩ : ∀ {y p q}{Y : MP y}{P : MP p}{Q : MP q} → Y ⇒ P → Y ⇒ Q → Y ⇒ P ⊗ Q
  ⟨ F , G ⟩ = mk⇒
    (λ x → apply F x , apply G x)
    (λ c~c' → PEq.cong₂ _,_ (monotone-comm F c~c') (monotone-comm G c~c'))

  π₁ : ∀ {ℓ₁ ℓ₂}{P : MP ℓ₁}{Q : MP ℓ₂} → P ⊗ Q ⇒ P
  π₁ = mk⇒ (λ{ (pc , qc) → pc}) (λ c~c' → PEq.refl)

  π₂ : ∀ {ℓ₁ ℓ₂}{P : MP ℓ₁}{Q : MP ℓ₂} → P ⊗ Q ⇒ Q
  π₂ = mk⇒ (λ{ (pc , qc) → qc}) (λ c~c' → PEq.refl)

  swap : ∀ {ℓ₁ ℓ₂}(P : MP ℓ₁)(Q : MP ℓ₂) → P ⊗ Q ⇒ Q ⊗ P
  swap _ _ = mk⇒ Prod.swap λ c~c' → PEq.refl

  comm : ∀ {ℓ₁ ℓ₂ ℓ₃}(P : MP ℓ₁)(Q : MP ℓ₂)(R : MP ℓ₃) → (P ⊗ Q) ⊗ R ⇒ P ⊗ (Q ⊗ R)
  comm _ _ _ = mk⇒
    (λ{ ((p , q) , r) → p , (q , r) })
    (λ c~c' → PEq.refl)

  xmap : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄}{P : MP ℓ₁}{Q : MP ℓ₂}{R : MP ℓ₃}{S : MP ℓ₄} →
         (F : P ⇒ R)(G : Q ⇒ S) → P ⊗ Q ⇒ R ⊗ S
  xmap F G = ⟨ F ∘ π₁ , G ∘ π₂ ⟩

  uncurry₁ : ∀ {ℓ₁ ℓ₂ ℓ₃}{A : Set ℓ₁}{P : MP ℓ₂}{Q : MP ℓ₃} →
             (A → P ⇒ Q) → (Const A ⊗ P ⇒ Q)
  uncurry₁ {A = A}{P}{Q} f = mk⇒
    (λ{ (a , p) → apply (f a) p })
    (λ{ c~c' {a , p} → monotone-comm (f a) c~c' })

  module ⊗-Properties where
    π₁-comm : ∀ {y p q}{Y : MP y}{P : MP p}{Q : MP q}{F : Y ⇒ P}{G : Y ⇒ Q} →
            π₁ ∘ ⟨ F , G ⟩ ⇒≡ F
    π₁-comm _ = PEq.refl

    π₂-comm : ∀ {y p q}{Y : MP y}{P : MP p}{Q : MP q}{F : Y ⇒ P}{G : Y ⇒ Q} →
            π₂ ∘ ⟨ F , G ⟩ ⇒≡ G
    π₂-comm _ = PEq.refl

    unique : ∀ {y p q}{Y : MP y}{P : MP p}{Q : MP q}{g : Y ⇒ (P ⊗ Q)} → ⟨ π₁ ∘ g , π₂ ∘ g ⟩ ⇒≡ g
    unique _ = PEq.refl

module Forall (funext : ∀ {a b} → PEq.Extensionality a b) where
  -- ∀-quantification over Set

  Forall : ∀ {ℓ₁ ℓ₂}{I : Set ℓ₁}(P : I → MP ℓ₂) → MP _
  Forall {I = I} P = mp
    (λ c → ∀ (i : I) → P i · c)
    (record {
      monotone = λ x x₁ i → MP.monotone (P i) x (x₁ i) ;
      monotone-refl = λ p → funext λ i → MP.monotone-refl (P i) (p i) ;
      monotone-trans = λ p c~c' c'~c'' → funext λ i → MP.monotone-trans (P i) (p i) c~c' c'~c'' })

module ListAll where
  -- quantification over the elements in a list

  open import Data.Nat
  open import Data.List
  import Data.List.All as All
  open import Data.List.All.Properties
  open import Data.List.All.Properties.Extra

  module _ {a p} {A : Set a} {P : A → Set p} where

    map-id' : ∀ {xs} (pxs : All.All P xs) → All.map {P = P} {Q = P} (λ x → x) pxs ≡ pxs
    map-id' All.[]         = PEq.refl
    map-id' (px All.∷ pxs) = cong (px All.∷_)  (map-id' pxs)

  All : ∀ {ℓ₁}{I : Set ℓ₁}(P : I → MP ℓ₂) → List I → MP _
  All P xs = mp
    (λ c → All.All (λ x → P x · c) xs)
    (record {
      monotone = λ c~c' ps → All.map (λ {i} x → MP.monotone (P i) c~c' x ) ps ;
      monotone-refl = λ p → (begin
        All.map (λ {i} x → MP.monotone (P i) refl x) p
          ≡⟨ map-cong p (λ {i} px → MP.monotone-refl (P i) px) ⟩
        All.map (λ x → x) p
          ≡⟨ map-id' p ⟩
        p ∎) ;
      monotone-trans = λ p c~c' c'~c'' → (begin
       All.map (λ {i} x → MP.monotone (P i) (trans c~c' c'~c'') x) p
         ≡⟨ map-cong p (λ {i} p → MP.monotone-trans (P i) p c~c' c'~c'') ⟩
       All.map (λ {i} x → MP.monotone (P i) c'~c'' (MP.monotone (P i) c~c' x)) p
         ≡⟨ PEq.sym (map-map p) ⟩
       All.map (λ {i} x → MP.monotone (P i) c'~c'' x) (All.map (λ {i} x → MP.monotone (P i) c~c' x) p)
       ∎) })

module Exists where
  -- ∃-quantification over Set

  Exists : ∀ {ℓ₁ ℓ₂}{I : Set ℓ₁}(P : I → MP ℓ₂) → MP _
  Exists {I = I} P = mp (λ x → Prod.∃ λ (i : I) → P i · x) (record {
      monotone = λ{ c~c' (i , px) → i , MP.monotone (P i) c~c' px } ;
      monotone-refl = λ{
        (i , px) → PEq.cong (λ u → i , u) (MP.monotone-refl (P i) px) };
      monotone-trans = (λ {
        (i , px) p q → PEq.cong (λ u → i , u) (MP.monotone-trans (P i) px p q)})
    })

  elim : ∀ {ℓ₁ ℓ₂ ℓ₃}{I : Set ℓ₁}{P : I → MP ℓ₂}{Q : MP ℓ₃} →
         (∀ {i} → P i ⇒ Q) → Exists P ⇒ Q
  elim {P = P}{Q} F = mk⇒
    (λ{ (i , pi) → apply F pi})
    (λ{ c~c' {(i , pi)} → monotone-comm F c~c' })

  open Product
  ∃-⊗-comm : ∀ {ℓ₁ ℓ₂ ℓ₃}{I : Set ℓ₁}(P : I → MP ℓ₂)(Q : MP ℓ₃) →
             Exists (λ i → P i) ⊗ Q ⇒ Exists (λ i → P i ⊗ Q)
  ∃-⊗-comm _ _ = mk⇒
    (λ{ ((i , pi) , q) → (i , pi , q)})
    (λ c~c' → PEq.refl)

module Monoid where
  -- identifies _⊗_ as a tensor/monoidal product
  open Product

  -- associator
  assoc : ∀ {p q r}{P : MP p}{Q : MP q}{R : MP r} → (P ⊗ Q) ⊗ R ≅ P ⊗ (Q ⊗ R)
  assoc = record {
    to = mk⇒ (λ{ ((p , q) , r) → p , (q , r) }) (λ c~c' → PEq.refl) ;
    from = mk⇒ (λ{ (p , (q , r)) → (p , q) , r }) (λ c~c' → PEq.refl) ;
    left-inv = λ _ → PEq.refl ;
    right-inv = λ _ → PEq.refl }

  -- left unitor
  ⊗-left-id : ∀ {p}{P : MP p} → ⊤ ⊗ P ≅ P
  ⊗-left-id = record {
    to = π₂ {P = ⊤} ;
    from = ⟨ mk⇒ (λ x → Unit.tt) (λ c~c' → PEq.refl) , id _ ⟩ ;
    left-inv = λ p → PEq.refl ;
    right-inv = λ p → PEq.refl }

  -- right unitor
  ⊗-right-id : ∀ {p}{P : MP p} → P ⊗ ⊤ ≅ P
  ⊗-right-id = record {
    to = π₁ {Q = ⊤} ;
    from = ⟨ mk⇒ (λ {c} z → z) (λ c~c' → PEq.refl) , mk⇒ (λ {c} _ → Unit.tt) (λ c~c' → PEq.refl) ⟩ ;
    left-inv = λ p → PEq.refl ;
    right-inv = λ p → PEq.refl }

  -- TODO: coherence conditions

module Exponential
  (trans-assoc : ∀ {c c' c'' c'''}{p : c ≤ c'}{q : c' ≤ c''}{r : c'' ≤ c'''} →
                 trans (trans p q) r PEq.≡ trans p (trans q r))
  (trans-refl₁ : ∀ {c c'}{p : c ≤ c'} → trans refl p PEq.≡ p)
  (trans-refl₂ : ∀ {c c'}{p : c ≤ c'} → trans p refl PEq.≡ p)
  where

  -- for convencience we assume extensionality for morphisms here for now
  postulate ⇒-ext : ∀ {ℓ₁ ℓ₂} → ⇒-Ext ℓ₁ ℓ₂

  open Product

  -- the preorder that we have defined monotonicity by is itself
  -- a monotone predicate
  ≤mono : Carrier → MP _
  ≤mono c = mp (λ c' → c ≤ c' ) (record {
    monotone = flip trans  ;
    monotone-refl = λ _ → trans-refl₂ ;
    monotone-trans = λ _ _ _ → PEq.sym trans-assoc })

  -- ... such that we can define the notion of a monotone function as follows:
  Mono⇒ : ∀ {ℓ ℓ₂}(P : MP ℓ)(Q : MP ℓ₂)(c : Carrier) → Set _
  Mono⇒ P Q c = ≤mono c ⊗ P ⇒ Q
  -- the intuition here comes from the naive interpretation
  -- of the type of curry: (X ⊗ P ⇒ Q) → X ⇒ (Const (P ⇒ Q)).
  -- unfolding the return type you would get something like the following Agda type:
  --   ∀ c → X · c → (∀ c' → P · c' → Q · c')
  -- this is too weak, because c' and c are unrelated and thus we can't combine
  -- X · c and P · c' into a product (X ⊗ P) · c'.
  -- The above Mono⇒ fixes this by simply requiring the relation c ≤ c' as
  -- an additional argument.

  infixl 80 _^_
  _^_ : ∀ {ℓ₁ ℓ₂}(Q : MP ℓ₁)(P : MP ℓ₂) → MP _
  Q ^ P = mp
    (Mono⇒ P Q)
    (record {
      monotone = λ c~c' φ →
        mk⇒
          (λ p → apply φ (trans c~c' (Prod.proj₁ p) , Prod.proj₂ p))
          (λ{ c~c'' {w , p} → (begin
            apply φ (trans c~c' (MP.monotone (≤mono _) c~c'' w) , (MP.monotone P c~c'' p))
              ≡⟨ PEq.cong (λ u → apply φ (u , MP.monotone P c~c'' p)) (PEq.sym trans-assoc) ⟩
            apply φ (MP.monotone (≤mono _ ⊗ P) c~c'' (trans c~c' w , p))
              ≡⟨ monotone-comm φ c~c'' ⟩
            MP.monotone Q c~c'' (apply φ (trans c~c' w , p))
          ∎)});
      monotone-refl  = λ φ → ⇒-ext (λ p → PEq.cong (λ u → apply φ (u , (Prod.proj₂ p))) trans-refl₁);
      monotone-trans = λ φ w₀ w₁ → ⇒-ext λ p → PEq.cong (λ u → apply φ (u , Prod.proj₂ p)) trans-assoc
    })

  curry : ∀ {ℓ₁ ℓ₂ ℓ₃}{X : MP ℓ₁}{Y : MP ℓ₂}{Z : MP ℓ₃}(F : (X ⊗ Y) ⇒ Z) → X ⇒ (Z ^ Y)
  curry {X = X}{Y}{Z} F = mk⇒
    (λ xc → mk⇒
      (λ{ (w , yc) → apply F ((MP.monotone X w xc) , yc)})
      (λ{ c~c' {w , yc} → (begin
        apply F (MP.monotone X (trans w c~c') xc , MP.monotone Y c~c' yc)
          ≡⟨ PEq.cong (λ u → apply F (u , _)) (MP.monotone-trans X xc w c~c') ⟩
        apply F (MP.monotone X c~c' (MP.monotone X w xc) , MP.monotone Y c~c' yc)
          ≡⟨ monotone-comm F c~c' ⟩
        MP.monotone Z c~c' (apply F (MP.monotone X w xc , yc))
      ∎ )}))
    λ c~c' {xc} → ⇒-ext λ p →
      PEq.cong (λ u → apply F (u , _)) (PEq.sym (MP.monotone-trans X xc c~c' (Prod.proj₁ p)))

  ε : ∀ {ℓ₁ ℓ₂}{Y : MP ℓ₁}{Z : MP ℓ₂} → (Z ^ Y) ⊗ Y ⇒ Z
  ε {Y = Y}{Z} = mk⇒
    (λ zʸ×y → apply (Prod.proj₁ zʸ×y) (refl , Prod.proj₂ zʸ×y) )
    λ{ c~c' {φ@(F , p)} → (begin
      (apply F (trans c~c' refl , MP.monotone Y c~c' p))
        ≡⟨ PEq.cong (λ u → apply F (u , _)) trans-refl₂ ⟩
      (apply F (c~c' , MP.monotone Y c~c' p))
        ≡⟨ PEq.sym (PEq.cong (λ u → apply F (u , _)) trans-refl₁) ⟩
      (apply F (trans refl c~c' , MP.monotone Y c~c' p))
        ≡⟨ PEq.refl ⟩
      (apply F (MP.monotone (≤mono _ ⊗ Y) c~c' (refl , p)))
        ≡⟨ monotone-comm F c~c' ⟩
      MP.monotone Z c~c' (apply F (refl , p))
    ∎ )}

  uncurry : ∀ {ℓ₁ ℓ₂ ℓ₃}{X : MP ℓ₁}{Y : MP ℓ₂}{Z : MP ℓ₃}(F : X ⇒ (Z ^ Y)) → (X ⊗ Y) ⇒ Z
  uncurry {X = x}{Y}{Z} F = ε ∘ xmap F (id Y)

module Sum where
  open import Data.Sum as Sum using (_⊎_)

  infixl 30 _⊕_
  _⊕_ : ∀ {ℓ₁ ℓ₂} → MP ℓ₁ → MP ℓ₂ → MP (ℓ₁ ⊔ ℓ₂)
  P ⊕ Q = mp
      (λ c → (P · c) ⊎ (Q · c))
      (record {
        monotone = λ{
          c≤c' (Sum.inj₁ p) → Sum.inj₁ (MP.monotone P c≤c' p) ;
          c≤c' (Sum.inj₂ q) → Sum.inj₂ (MP.monotone Q c≤c' q)
        } ;
        monotone-refl = λ{
          (Sum.inj₁ p) → PEq.cong Sum.inj₁ (MP.monotone-refl P p) ;
          (Sum.inj₂ q) → PEq.cong Sum.inj₂ (MP.monotone-refl Q q) };
        monotone-trans = λ{
          (Sum.inj₁ p) c≤c' c'≤c'' → PEq.cong Sum.inj₁ (MP.monotone-trans P p c≤c' c'≤c'') ;
          (Sum.inj₂ q) c≤c' c'≤c'' → PEq.cong Sum.inj₂ (MP.monotone-trans Q q c≤c' c'≤c'') }
      })

  -- canonical injections
  inj₁ : ∀ {ℓ₁ ℓ₂}{P : MP ℓ₁}(Q : MP ℓ₂) → P ⇒ (P ⊕ Q)
  inj₁ Q = mk⇒ Sum.inj₁ λ c~c' → PEq.refl

  inj₂ : ∀ {ℓ₁ ℓ₂}(P : MP ℓ₁){Q : MP ℓ₂} → Q ⇒ (P ⊕ Q)
  inj₂ Q = mk⇒ Sum.inj₂ λ c~c' → PEq.refl

  [_,_] : ∀ {ℓ₁ ℓ₂ ℓ₃}{P : MP ℓ₁}{Q : MP ℓ₂}{R : MP ℓ₃} → P ⇒ R → Q ⇒ R → (P ⊕ Q) ⇒ R
  [_,_] F G = mk⇒
    (λ{ (Sum.inj₁ x) → apply F x ; (Sum.inj₂ y) → apply G y})
    (λ{
      c~c' {Sum.inj₁ x} → monotone-comm F c~c' ;
      c~c' {Sum.inj₂ y} → monotone-comm G c~c'
    })

  -- TODO [_,_] is unique

  [g,*]∘inj₁ : ∀ {ℓ₁ ℓ₂ ℓ₃}{P : MP ℓ₁}{Q : MP ℓ₂}{R : MP ℓ₃} → (F : P ⇒ R)(G : Q ⇒ R) → [ F , G ] ∘ inj₁ _ ⇒≡ F
  [g,*]∘inj₁ F G p = PEq.refl

  [*,g]∘inj₂ : ∀ {ℓ₁ ℓ₂ ℓ₃}{P : MP ℓ₁}{Q : MP ℓ₂}{R : MP ℓ₃} → (F : P ⇒ R)(G : Q ⇒ R) → [ F , G ] ∘ inj₂ _ ⇒≡ G
  [*,g]∘inj₂ F G p = PEq.refl


text:
{-# OPTIONS --safe #-}
{-
  Successor structures for spectra, chain complexes and fiber sequences.
  This is an idea from Floris van Doorn's phd thesis.
-}
module Cubical.Structures.Successor where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Int
open import Cubical.Data.Nat

private
  variable
    ℓ : Level

record SuccStr (ℓ : Level) : Type (ℓ-suc ℓ) where
  field
    Index : Type ℓ
    succ : Index → Index

open SuccStr

ℤ+ : SuccStr ℓ-zero
ℤ+ .Index = ℤ
ℤ+ .succ = sucℤ

ℕ+ : SuccStr ℓ-zero
ℕ+ .Index = ℕ
ℕ+ .succ = suc

max_stars_repo_name: FernandoLarrain/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums (disjoint unions)
------------------------------------------------------------------------

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

module Data.Sum.Base where

open import Data.Bool.Base using (true; false)
open import Function.Base using (_∘_; _-[_]-_ ; id)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary using (Dec; yes; no; _because_; ¬_)
open import Level using (Level; _⊔_)

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

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

infixr 1 _⊎_

data _⊎_ (A : Set a) (B : Set b) : Set (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

------------------------------------------------------------------------
-- Functions

[_,_] : ∀ {C : A ⊎ B → Set c} →
        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
        ((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y

[_,_]′ : (A → C) → (B → C) → (A ⊎ B → C)
[_,_]′ = [_,_]

fromInj₁ : (B → A) → A ⊎ B → A
fromInj₁ = [ id ,_]′

fromInj₂ : (A → B) → A ⊎ B → B
fromInj₂ = [_, id ]′

swap : A ⊎ B → B ⊎ A
swap (inj₁ x) = inj₂ x
swap (inj₂ x) = inj₁ x

map : (A → C) → (B → D) → (A ⊎ B → C ⊎ D)
map f g = [ inj₁ ∘ f , inj₂ ∘ g ]

map₁ : (A → C) → (A ⊎ B → C ⊎ B)
map₁ f = map f id

map₂ : (B → D) → (A ⊎ B → A ⊎ D)
map₂ = map id

infixr 1 _-⊎-_
_-⊎-_ : (A → B → Set c) → (A → B → Set d) → (A → B → Set (c ⊔ d))
f -⊎- g = f -[ _⊎_ ]- g

-- Conversion back and forth with Dec

fromDec : Dec A → A ⊎ ¬ A
fromDec ( true because  [p]) = inj₁ (invert  [p])
fromDec (false because [¬p]) = inj₂ (invert [¬p])

toDec : A ⊎ ¬ A → Dec A
toDec (inj₁ p)  = yes p
toDec (inj₂ ¬p) = no ¬p


text:
------------------------------------------------------------------------
-- Localisation
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- Following "Modalities in Homotopy Type Theory" by Rijke, Shulman
-- and Spitters.

-- The module is parametrised by a notion of equality. The higher
-- constructors of the HIT defining localisation use path equality,
-- but the supplied notion of equality is used for many other things.

import Equality.Path as P

module Localisation
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

open import Prelude as P

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq hiding (ext)
open import Pushout eq as Pushout using (Pushout)

private
  variable
    a b c p q r : Level
    A B C       : Type a
    P Q R       : A → Type p
    e f g x y   : A

------------------------------------------------------------------------
-- Localisation

-- A first approximation to localisation.
--
-- This is a slight generalisation of the HIT that Rijke et al. call
-- 𝓙: they require all types to live in the same universe.

data Localisation′
       {A : Type a} {P : A → Type p} {Q : A → Type q}
       (f : ∀ x → P x → Q x) (B : Type b) :
       Type (a ⊔ b ⊔ p ⊔ q) where
  [_]   : B → Localisation′ f B
  ext   : (P x → Localisation′ f B) →
          (Q x → Localisation′ f B)
  ext≡ᴾ : ext g (f x y) P.≡ g y

-- A variant of ext≡ᴾ.

ext≡ :
  {f : (x : A) → P x → Q x} {g : P x → Localisation′ f B} →
  ext g (f x y) ≡ g y
ext≡ = _↔_.from ≡↔≡ ext≡ᴾ

-- Localisation.

Localisation :
  {A : Type a} {P : A → Type p} {Q : A → Type q} →
  (∀ x → P x → Q x) →
  Type b → Type (a ⊔ b ⊔ p ⊔ q)
Localisation {p = p} {q = q} {A = A} {P = P} {Q = Q} f =
  Localisation′ f̂
  where
  P̂ : A ⊎ A → Type (p ⊔ q)
  P̂ = P.[ ↑ q ∘ P
        , (λ x → Pushout (record { left = f x; right = f x }))
        ]

  Q̂ : A ⊎ A → Type q
  Q̂ = P.[ Q , Q ]

  f̂ : (x : A ⊎ A) → P̂ x → Q̂ x
  f̂ = P.[ (λ x → f x ∘ lower)
        , (λ x → Pushout.rec id id (refl ∘ f x))
        ]

------------------------------------------------------------------------
-- Some eliminators for Localisation′

-- A dependent eliminator, expressed using paths.

record Elimᴾ
         {A : Type a} {P : A → Type p} {Q : A → Type q}
         (f : ∀ x → P x → Q x) (B : Type b)
         (R : Localisation′ f B → Type r) :
         Type (a ⊔ b ⊔ p ⊔ q ⊔ r) where
  no-eta-equality
  field
    []ʳ   : ∀ x → R [ x ]
    extʳ  : (∀ y → R (g y)) → ∀ y → R (ext {x = x} g y)
    ext≡ʳ : (h : (y : P x) → R (g y)) →
            P.[ (λ i → R (ext≡ᴾ {g = g} {y = y} i)) ] extʳ h (f x y) ≡
            h y

open Elimᴾ public

elimᴾ : Elimᴾ f B R → (x : Localisation′ f B) → R x
elimᴾ {f = f} {B = B} {R = R} e = helper
  where
  module E = Elimᴾ e

  helper : (x : Localisation′ f B) → R x
  helper [ x ]             = E.[]ʳ x
  helper (ext g y)         = E.extʳ (λ y → helper (g y)) y
  helper (ext≡ᴾ {g = g} i) = E.ext≡ʳ (λ y → helper (g y)) i

-- A non-dependent eliminator, expressed using paths.

record Recᴾ
         {A : Type a} {P : A → Type p} {Q : A → Type q}
         (f : ∀ x → P x → Q x) (B : Type b)
         (C : Type c) :
         Type (a ⊔ b ⊔ p ⊔ q ⊔ c) where
  no-eta-equality
  field
    []ʳ   : B → C
    extʳ  : (P x → C) → Q x → C
    ext≡ʳ : (g : P x → C) → extʳ g (f x y) P.≡ g y

open Recᴾ public

recᴾ : Recᴾ f B C → Localisation′ f B → C
recᴾ r = elimᴾ λ where
    .[]ʳ   → R.[]ʳ
    .extʳ  → R.extʳ
    .ext≡ʳ → R.ext≡ʳ
  where
  module R = Recᴾ r

-- A dependent eliminator.

record Elim
         {A : Type a} {P : A → Type p} {Q : A → Type q}
         (f : ∀ x → P x → Q x) (B : Type b)
         (R : Localisation′ f B → Type r) :
         Type (a ⊔ b ⊔ p ⊔ q ⊔ r) where
  no-eta-equality
  field
    []ʳ   : ∀ x → R [ x ]
    extʳ  : (∀ y → R (g y)) → ∀ y → R (ext {x = x} g y)
    ext≡ʳ : (h : (y : P x) → R (g y)) →
            subst R (ext≡ {y = y} {g = g}) (extʳ h (f x y)) ≡ h y

open Elim public

elim : Elim f B R → (x : Localisation′ f B) → R x
elim e = elimᴾ λ where
    .[]ʳ   → E.[]ʳ
    .extʳ  → E.extʳ
    .ext≡ʳ → subst≡→[]≡ ∘ E.ext≡ʳ
  where
  module E = Elim e

-- A "computation" rule.

elim-ext≡ :
  dcong (elim e) (ext≡ {y = y} {g = g}) ≡
  Elim.ext≡ʳ e (elim e ∘ g)
elim-ext≡ = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec
         {A : Type a} {P : A → Type p} {Q : A → Type q}
         (f : ∀ x → P x → Q x) (B : Type b)
         (C : Type c) :
         Type (a ⊔ b ⊔ p ⊔ q ⊔ c) where
  no-eta-equality
  field
    []ʳ   : B → C
    extʳ  : (P x → C) → Q x → C
    ext≡ʳ : (g : P x → C) → extʳ g (f x y) ≡ g y

open Rec public

rec : Rec f B C → Localisation′ f B → C
rec r = recᴾ λ where
    .[]ʳ   → R.[]ʳ
    .extʳ  → R.extʳ
    .ext≡ʳ → _↔_.to ≡↔≡ ∘ R.ext≡ʳ
  where
  module R = Rec r

-- A "computation" rule.

rec-ext≡ :
  {f : ∀ x → P x → Q x}
  {r : Rec f B C}
  {g : P x → Localisation′ f B} →
  cong (rec r) (ext≡ {y = y} {g = g}) ≡
  Rec.ext≡ʳ r (rec r ∘ g)
rec-ext≡ = cong-≡↔≡ (refl _)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
-- Andreas, 2015-03-17

open import Common.Size

data ⊥ : Set where

data D (i : Size) : Set where
  c : Size< i → D i

-- This definition of size predecessor should be forbidden...
module _ (i : Size) where
  postulate
    pred : Size< i

-- ...otherwise the injectivity test loops here.
iter : ∀ i → D i → ⊥
iter i (c j) = iter j (c (pred j))

loop : Size → ⊥
loop i = iter i (c (pred i))

absurd : ⊥
absurd = FIXME loop ∞

-- Testcase temporarily mutilated, original error
-- -Issue1428c.agda:13,5-19
-- -We don't like postulated sizes in parametrized modules.
-- +Issue1428c.agda:23,10-15
-- +Not in scope:
-- +  FIXME at Issue1428c.agda:23,10-15
-- +when scope checking FIXME

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
module DeMorgan where

open import Definitions

deMorgan : {A B : Set} → ¬ A ∧ ¬ B → ¬ (A ∨ B)
deMorgan = {!!}

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


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

module M-types.Base where
    open import M-types.Base.Core public
    open import M-types.Base.Sum public
    open import M-types.Base.Prod public
    open import M-types.Base.Eq public
    open import M-types.Base.Equi public
    open import M-types.Base.Rel public
    open import M-types.Base.Contr public
    open import M-types.Base.Axiom public

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
module Injections where

open import Data.Product
open import Relation.Nullary
open import Data.Empty
open import Data.Sum

open import Support.Equality
open ≡-Reasoning

open import Vars public
open import Injections.Type public

invert : ∀ {A : Set} {xs ys : List A} (i : Inj xs ys) → ∀ {t} (y : ys ∋ t) → Dec (∃ \ x → i $ x ≡ y)
invert []              y = no (λ { (() , _)})
invert ( z ∷ i [ pf ]) y with z ≅∋? y
invert (.y ∷ i [ pf ]) y | yes refl` = yes (zero , refl)
invert ( z ∷ i [ pf ]) y | no  z≢y   with invert i y
invert ( z ∷ i [ pf ]) y | no  z≢y   | yes (x , i$x≡y) = yes (suc x , i$x≡y)
invert ( z ∷ i [ pf ]) y | no  z≢y   | no  ¬[i⁻¹y]     = no  (neither z≢y ¬[i⁻¹y])
  where
    neither : ∀ {t} {y : _ ∋ t} → ¬ z ≅∋ y → ¬ (∃ \ x → i $ x ≡ y) → ¬ Σ (_ ∷ _ ∋ _) (λ x → (z ∷ i [ pf ]) $ x ≡ y)
    neither ¬1 ¬2 (zero  , p) = ¬1 (refl , ≡-to-≅ p)
    neither ¬1 ¬2 (suc x , p) = ¬2 (x , p)

abstract
  _∘i_ : ∀ {A : Set}{xs ys zs : List A} → Inj ys zs → Inj xs ys → Inj xs zs
  f ∘i g = quo (λ x x₁ → f $ (g $ x₁)) {λ x x₁ → injective g _ _ (injective f _ _ x₁)}

mutual
  id-i : ∀ {A : Set}{xs : List A} → Inj xs xs
  id-i = quo (\ _ x → x) {\ _ e → e}

  Inj-thin : ∀ {A : Set}{x : A}{xs ys} → (v : ys ∋ x) -> Inj xs (ys - v) → Inj xs ys
  Inj-thin v f = quo (λ x x₁ → thin v x (f $ x₁)) {λ x x₁ → injective f _ _ (thin-inj v x₁)}

abstract
  id-i$ : ∀ {A : Set}{xs : List A} -> ∀ {x}(v : xs ∋ x) -> id-i $ v ≡ v
  id-i$ v = iso2 _ _ v

  right-id : ∀ {A : Set}{xs ys : List A} → (i : Inj xs ys) → i ∘i id-i ≡ i
  right-id i = begin quo (λ x z → i $ (id-i $ z)) ≡⟨ quo-ext (λ x v → cong (_$_ i) (iso2 _ _ v)) ⟩
                     quo (λ x → _$_ i)            ≡⟨ iso1 i (λ x eq → injective i _ _ eq) ⟩
                     i                            ∎

  left-id : ∀ {A : Set}{xs ys : List A} → (i : Inj xs ys) → id-i ∘i i ≡ i
  left-id i = begin quo (λ x z → id-i $ (i $ z)) ≡⟨ quo-ext (λ x v → (iso2 _ _ (i $ v))) ⟩
                    quo (λ x → _$_ i)            ≡⟨ iso1 i (λ x eq → injective i _ _ eq) ⟩
                    i                            ∎

  apply-∘ : ∀ {A : Set}{xs ys zs : List A} → (j : Inj ys zs) → (i : Inj xs ys) → ∀ {x} {v : x ∈ xs} → (j ∘i i) $ v ≡ j $ (i $ v)
  apply-∘ j i {x}{v} = iso2 _ _ v

  assoc-∘i : ∀ {A : Set}{xs ys ws zs : List A} {f : Inj ws zs}{g : Inj _ ws}{h : Inj xs ys} → f ∘i (g ∘i h) ≡ (f ∘i g) ∘i h
  assoc-∘i {f = f}{g = g}{h = h} = quo-ext λ x v →
      begin f $ (quo (λ x₁ x₂ → g $ (h $ x₂)) $ v) ≡⟨ cong (_$_ f) (iso2 _ _ v) ⟩
            f $ (g $ (h $ v))                      ≡⟨ sym (iso2 _ _ (h $ v)) ⟩
            quo (λ x₁ x₂ → f $ (g $ x₂)) $ (h $ v) ∎

  cong-$ : ∀ {A : Set}{xs ys : List A} {f g : _} {inj1 inj2} → quo {_} {xs} {ys} f {inj1} ≡ quo g {inj2} → ∀ {s} (x : xs ∋ s) → f s x ≡ g s x
  cong-$ {A} {xs} {ys} {f} {g} eq x = begin f _ x     ≡⟨ sym (iso2 f _ x) ⟩
                                            quo f $ x ≡⟨ cong (λ f₁ → f₁ $ x) eq ⟩
                                            quo g $ x ≡⟨ iso2 g _ x ⟩
                                            g _ x     ∎

  ∘i-inj : ∀ {A : Set}{xs ys zs : List A} → (i : Inj ys zs) (j1 j2 : Inj xs ys) → (i ∘i j1) ≡ (i ∘i j2) → j1 ≡ j2
  ∘i-inj i j1 j2 eq = begin j1                 ≡⟨ sym (iso1 j1 (λ x x₁ → injective j1 _ _ x₁)) ⟩
                            quo (λ x → _$_ j1) ≡⟨ quo-ext (λ x v → injective i _ _ (cong-$ eq v)) ⟩
                            quo (λ x → _$_ j2) ≡⟨ iso1 j2 (λ x x₁ → injective j2 _ _ x₁) ⟩
                            j2                 ∎

  Inj-thin-$ : ∀ {A : Set}{x : A}{xs ys} → (v : ys ∋ x) -> (f : Inj xs (ys - v)) -> ∀ {y}(u : xs ∋ y) -> Inj-thin v f $ u ≡ thin v _ (f $ u)
  Inj-thin-$ v f u = iso2 _ _ u

  Inj-thin-inj : ∀ {A : Set}{x : A}{xs ys} → (v : ys ∋ x) -> (f g : Inj xs (ys - v)) -> Inj-thin v f ≡ Inj-thin v g -> f ≡ g
  Inj-thin-inj v f g eq = ext-$ f g (λ x v₁ → thin-inj v (cong-$ {inj1 = λ x₁ x₂ → injective f _ _ (thin-inj v x₂)} {inj2 = λ x₁ x₂ → injective g _ _ (thin-inj v x₂)} eq v₁)) -- XXX regression

  Inj-thin-∘i : ∀ {A : Set}{x : A}{zs xs ys} → (v : ys ∋ x) -> (f : Inj xs (ys - v)) (m : Inj zs xs) -> Inj-thin v f ∘i m ≡ Inj-thin v (f ∘i m)
  Inj-thin-∘i v f m = quo-ext (λ x v₁ → trans (iso2 _ _ (m $ v₁)) (cong (thin v x) (sym (iso2 _ _ v₁))))

  v∉Inj-thinv : ∀ {A : Set}{x : A}{xs ys} → (v : ys ∋ x) -> (f : Inj xs (ys - v)) -> v ∉ Inj-thin v f
  v∉Inj-thinv v f = ∉Im$-∉ (λ x x₁ → thin v _ (f $ x₁)) v (λ b → x∉thinx v (f $ b))

test : ∀ {A : Set} {xs ys} → (f : ∀ (x : A) → x ∈ xs → x ∈ ys){inj1 inj2 : ∀ x → {i j : x ∈ xs} → f x i ≡ f x j → i ≡ j} → quo f {inj1} ≡ quo f {inj2}
test f = refl

weak : ∀ {A : Set}{x : A}{xs ys} → Inj xs ys → Inj xs (x ∷ ys)
weak f = Inj-thin zero f

apply-weakid : ∀ {A : Set}{xs : List A}{x y}(i : xs ∋ x) -> weak {x = y} id-i $ i ≡ suc i
apply-weakid i = begin
   quo (λ x v → thin zero x (id-i $ v)) $ i ≡⟨ iso2 _ _ i ⟩
   suc (id-i $ i)                           ≡⟨ cong suc (id-i$ i) ⟩
   suc i                                    ∎

_∷[]_ : ∀ {A : Set}{x : A}{xs ys} → (v : ys ∋ x) -> Inj xs (ys - v) → Inj (x ∷ xs) ys
v ∷[] f = v ∷ Inj-thin v f [ v∉Inj-thinv v f ]

cons : ∀ {A : Set}{x : A}{xs ys} → Inj xs ys → Inj (x ∷ xs) (x ∷ ys)
cons z = zero ∷[] z

abstract

  cons-id : ∀ {A : Set}{x : A}{xs} -> cons id-i ≡ id-i {_} {x ∷ xs}
  cons-id = cong-∷[] refl (quo-ext (λ x v → cong suc (id-i$ v)))

  cons-∘i : ∀ {A : Set}{xs ys zs : List A}{x} → (j : Inj ys zs) → (i : Inj xs ys) → cons {A} {x} (j ∘i i) ≡ cons j ∘i cons i
  cons-∘i j i = cong-∷[] refl (begin
    quo (λ x z → suc (proj₁ (quo' (λ v v₁ → j $ (i $ v₁))) $ z))
      ≡⟨ quo-ext {injg = λ x x₁ → injective i _ _ (injective (weak j) _ _ x₁)} (λ x v →
          begin suc (proj₁ (quo' (λ v₁ v₂ → j $ (i $ v₂))) $ v) ≡⟨ cong suc (iso2 _ _ v) ⟩
                suc (j $ (i $ v))                               ≡⟨ sym (iso2 _ _ (i $ v)) ⟩
                quo (λ x₁ x₂ → suc (j $ x₂)) $ (i $ v)          ∎) ⟩
    quo (λ x v → cons j $ suc (i $ v))                       ≡⟨ sym (quo-ext (λ x₁ v → cong (_$_ (cons j)) (iso2 (λ _ x → suc (i $ x)) _ v))) ⟩
    quo (λ x v → cons j $ (quo (λ z x₁ → suc (i $ x₁)) $ v)) ∎)

∘-ext : ∀ {A : Set}{xs ys zs ws : List A} {f : Inj ys zs}{g : Inj xs ys}{f1 : Inj ws zs}{g1 : Inj xs ws} -> f ∘i g ≡ f1 ∘i g1
        -> (∀ x (v : xs ∋ x) -> f $ (g $ v) ≡ f1 $ (g1 $ v))
∘-ext eq = (\ x v -> trans (sym (apply-∘ _ _)) (trans (cong (\ f -> f $ v) eq) ((apply-∘ _ _))))

ext-∘ : ∀ {A : Set}{xs ys zs ws : List A} {f : Inj ys zs}{g : Inj xs ys}{f1 : Inj ws zs}{g1 : Inj xs ws} ->
  (∀ x (v : xs ∋ x) -> f $ (g $ v) ≡ f1 $ (g1 $ v)) -> f ∘i g ≡ f1 ∘i g1
ext-∘ eq = ext-$ _ _ (\ x v -> trans (apply-∘ _ _) (trans (eq x v) (sym (apply-∘ _ _))))

-- Transforming pointwise representations of universal morphisms into Inj ones.
Equ-universal-quote : ∀ {A : Set} {xs ys : List A} → (i j : Inj xs ys) → ∀ {E} → (e : Inj E xs) ->
               (∀ a (y : xs ∋ a) -> i $ y ≡ j $ y -> ∃ \ z -> y ≡ e $ z) ->
                {as : List A} (h : Inj as xs) → i ∘i h ≡ j ∘i h → Σ (Inj as E) (λ z → e ∘i z ≡ h )
Equ-universal-quote {A} {xs} {ys} i j {E} e c {as} h eq =
  quo u {λ x {v} {w} eq1 → injective h v w (begin h $ v     ≡⟨ proj₂ (f x v) ⟩
                                                  e $ u x v ≡⟨ cong (_$_ e) eq1 ⟩
                                                  e $ u x w ≡⟨ sym (proj₂ (f x w)) ⟩
                                                  h $ w     ∎)}
  , ext-$ (e ∘i quo u) h (λ x v → begin
          (e ∘i quo u) $ v ≡⟨ apply-∘ _ _ ⟩
          e $ (quo u $ v)  ≡⟨ cong (_$_ e) (iso2 _ _ v) ⟩
          e $ u x v        ≡⟨ sym (proj₂ (f x v)) ⟩
          h $ v            ∎)
  where
   f : ∀ a (y : as ∋ a) -> ∃ \ z -> h $ y ≡ e $ z
   f a y = c a (h $ y) (∘-ext eq a y)
   u = (λ x v → proj₁ (f x v))

Pull-universal-quote : ∀ {A : Set} {X Y Z : List A} → (i : Inj X Z)(j : Inj Y Z) -> ∀ {P} -> (p₁ : Inj P X) (p₂ : Inj P Y)
                 -> (∀ (a : A) (y : Y ∋ a)(x : X ∋ a) -> i $ x ≡ j $ y -> (∃ \ z -> p₁ $ z ≡ x × p₂ $ z ≡ y))
                 -> ∀ {Q} -> (q₁ : Inj Q X) (q₂ : Inj Q Y) -> i ∘i q₁ ≡ j ∘i q₂ -> ∃ \ u -> q₁ ≡ p₁ ∘i u × q₂ ≡ p₂ ∘i u
Pull-universal-quote i j p₁ p₂ uni {Q} q₁ q₂ commutes =
     quo u {λ x {v} {w} eq → injective q₁ v w (begin q₁ $ v      ≡⟨ sym (proj₁ (proj₂ (f x v))) ⟩
                                                     p₁ $ u x v  ≡⟨ cong (_$_ p₁) eq ⟩
                                                     p₁ $ u x w  ≡⟨ proj₁ (proj₂ (f x w)) ⟩
                                                     q₁ $ w      ∎)}
     , ext-$ q₁ (p₁ ∘i quo u) (λ x v → begin
             q₁ $ v            ≡⟨ sym (proj₁ (proj₂ (f x v))) ⟩
             p₁ $ u x v        ≡⟨ cong (_$_ p₁) (sym (iso2 _ _ v)) ⟩
             p₁ $ (quo u $ v)  ≡⟨ sym (apply-∘ _ _) ⟩
             (p₁ ∘i quo u) $ v ∎)
     , ext-$ q₂ (p₂ ∘i quo u) (λ x v → begin
             q₂ $ v            ≡⟨ sym (proj₂ (proj₂ (f x v))) ⟩
             p₂ $ u x v        ≡⟨ cong (_$_ p₂) (sym (iso2 _ _ v)) ⟩
             p₂ $ (quo u $ v)  ≡⟨ sym (apply-∘ _ _) ⟩
             (p₂ ∘i quo u) $ v ∎)
  where
    f : ∀ a (v : Q ∋ a) -> (∃ \ z -> p₁ $ z ≡ q₁ $ v × p₂ $ z ≡ q₂ $ v)
    f a v = uni a (q₂ $ v) (q₁ $ v) (∘-ext commutes a v)
    u : ∀ a (v : Q ∋ a) -> _
    u a v = proj₁ (f a v)

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


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

module Polynomial.Simple.Reflection where

open import Agda.Builtin.Reflection
open import Reflection.Helpers

open import Polynomial.Simple.Solver renaming (solve to solve-fn)
open AlmostCommutativeRing

open import Data.Nat.Table

open import Data.Fin   as Fin   using (Fin)
open import Data.Vec   as Vec   using (Vec; _∷_; [])
open import Data.List  as List  using (List; _∷_; [])
open import Data.Maybe as Maybe using (Maybe; just; nothing; fromMaybe)
open import Agda.Builtin.Nat    using (_<_)
open import Data.Nat            using (ℕ; suc; zero)
open import Data.Bool           using (Bool; if_then_else_; true; false)
open import Data.Unit           using (⊤)
open import Data.String         using (String)
open import Data.Product        using (_,_)
open import Function

module Internal where
  _∈Ring : Term → TC Term
  ring ∈Ring = checkType ring (def (quote AlmostCommutativeRing) (unknown ⟨∷⟩ unknown ⟨∷⟩ []))

  vars : Term → Maybe Table
  vars = go []
    where
    go : Table → Term → Maybe Table
    go t (con (quote List._∷_) (_ ∷ _ ∷ var i [] ⟨∷⟩ xs ⟨∷⟩ _)) = go (insert i t) xs
    go t (con (quote List.List.[]) _) = just t
    go _ _ = nothing

  module OverRing (ring : Term) where
    _∈List⟨Carrier⟩ : Term → TC Term
    t ∈List⟨Carrier⟩ =
      checkType t
        (quote List ⟨ def ⟩ 1 ⋯⟅∷⟆ def (quote Carrier) (2 ⋯⟅∷⟆ ring ⟨∷⟩ []) ⟨∷⟩ []) >>= normalise

    record Ring⇓ : Set where
      constructor +⇒_*⇒_^⇒_-⇒_
      field +′ *′ ^′ -′ : Maybe Name

    ring⇓ : TC Ring⇓
    ring⇓ = ⦇ +⇒ ⟦ quote _+_ ⇓⟧ₙ *⇒ ⟦ quote _*_ ⇓⟧ₙ ^⇒ ⟦ quote _^_ ⇓⟧ₙ -⇒ ⟦ quote -_ ⇓⟧ₙ ⦈
      where
      ⟦_⇓⟧ₙ : Name → TC (Maybe Name)
      ⟦ nm ⇓⟧ₙ =
        normalise (nm ⟨ def ⟩ 2 ⋯⟅∷⟆ ring ⟨∷⟩ [])
          <&> λ where (def f args) → just f
                      _ → nothing

    module _ (nms : Ring⇓) where
      open Ring⇓ nms

      module _ (numVars : ℕ) where

        -- This function applies the hidden arguments that the constructors
        -- that Expr needs. The first is the universe level, the second is the
        -- type it contains, and the third is the number of variables it's
        -- indexed by. All three of these could likely be inferred, but to
        -- make things easier we supply the third because we know it.
        infixr 5 E⟅∷⟆_
        E⟅∷⟆_ : List (Arg Term) → List (Arg Term)
        E⟅∷⟆ xs = 1 ⋯⟅∷⟆
                  (quote Carrier ⟨ def ⟩ 2 ⋯⟅∷⟆ ring ⟨∷⟩ []) ⟅∷⟆
                  ℕ′ numVars ⟅∷⟆
                  xs

        -- A constant expression.
        Κ′ : Term → Term
        Κ′ x = quote Κ ⟨ con ⟩ E⟅∷⟆ x ⟨∷⟩ []

        _⇓≟_ : Maybe Name → Name → Bool
        nothing ⇓≟ _ = false
        just x  ⇓≟ y = primQNameEquality x y
        {-# INLINE _⇓≟_ #-}

        module ToExpr (Ι′ : ℕ → Maybe Term) where
          mutual
            -- Application of a ring operator often doesn't have a type as
            -- simple as "Carrier → Carrier → Carrier": there may be hidden
            -- arguments, etc. Here, we do our best to handle those cases,
            -- by just taking the last two explicit arguments.
            E⟨_⟩₂ : Name → List (Arg Term) → Term
            E⟨ nm ⟩₂ (x ⟨∷⟩ y ⟨∷⟩ []) = nm ⟨ con ⟩ E⟅∷⟆ E x ⟨∷⟩ E y ⟨∷⟩ []
            E⟨ nm ⟩₂ (x ∷ xs) = E⟨ nm ⟩₂ xs
            E⟨ nm ⟩₂ _ = unknown

            E⟨_⟩₁ : Name → List (Arg Term) → Term
            E⟨ nm ⟩₁ (x ⟨∷⟩ []) = nm ⟨ con ⟩ E⟅∷⟆ E x ⟨∷⟩ []
            E⟨ nm ⟩₁ (x ∷ xs) = E⟨ nm ⟩₁ xs
            E⟨ _ ⟩₁ _ = unknown

            E⟨^⟩ : List (Arg Term) → Term
            E⟨^⟩ (x ⟨∷⟩ y ⟨∷⟩ []) = quote _⊛_ ⟨ con ⟩ E⟅∷⟆ E x ⟨∷⟩ y ⟨∷⟩ []
            E⟨^⟩ (x ∷ xs) = E⟨^⟩ xs
            E⟨^⟩ _ = unknown

            -- When trying to figure out the shape of an expression, one of
            -- the difficult tasks is recognizing where constants in the
            -- underlying ring are used. If we were only dealing with ℕ, we
            -- might look for its constructors: however, we want to deal with
            -- arbitrary types which implement AlmostCommutativeRing. If the
            -- Term type contained type information we might be able to
            -- recognize it there, but it doesn't.
            --
            -- We're in luck, though, because all other cases in the following
            -- function *are* recognizable. As a result, the "catch-all" case
            -- will just assume that it has a constant expression.
            E : Term → Term
            E (def (quote _+_) xs) = E⟨ quote _⊕_ ⟩₂ xs
            E (def (quote _*_) xs) = E⟨ quote _⊗_ ⟩₂ xs
            E (def (quote _^_) xs) = E⟨^⟩ xs
            E (def (quote -_) xs) = E⟨ quote ⊝_ ⟩₁ xs
            E (def nm xs) = if +′ ⇓≟ nm then E⟨ quote _⊕_ ⟩₂ xs else
                            if *′ ⇓≟ nm then E⟨ quote _⊗_ ⟩₂ xs else
                            if ^′ ⇓≟ nm then E⟨^⟩ xs else
                            if -′ ⇓≟ nm then E⟨ quote ⊝_ ⟩₁ xs else
                            Κ′ (def nm xs)
            E (con (quote ℕ.suc) (x ⟨∷⟩ [])) = quote _⊕_ ⟨ con ⟩ E⟅∷⟆ Κ′ (ℕ′ (ℕ.suc ℕ.zero)) ⟨∷⟩ E x ⟨∷⟩ []
            E v@(var x _) = fromMaybe (Κ′ v) (Ι′ x)
            E t = Κ′ t

        callSolver : Vec String numVars → Term → Term → List (Arg Type)
        callSolver nms lhs rhs =
            2 ⋯⟅∷⟆ ring ⟨∷⟩ ℕ′ numVars ⟨∷⟩
            vlams nms (quote _⊜_ ⟨ def ⟩ 2 ⋯⟅∷⟆ ring ⟨∷⟩ ℕ′ numVars ⟨∷⟩ E lhs ⟨∷⟩ E rhs ⟨∷⟩ []) ⟨∷⟩
            hlams nms (quote refl ⟨ def ⟩ 2 ⋯⟅∷⟆ ring ⟨∷⟩ 1 ⋯⟅∷⟆ []) ⟨∷⟩
            []
          where
          Ι′ : ℕ → Maybe Term
          Ι′ i = if i < numVars then just (var i []) else nothing
          open ToExpr Ι′

        constructSoln : Table → Term → Term → Term
        constructSoln t lhs rhs =
            quote trans ⟨ def ⟩ 2 ⋯⟅∷⟆ ring ⟨∷⟩ 3 ⋯⟅∷⟆
              (quote sym ⟨ def ⟩ 2 ⋯⟅∷⟆ ring ⟨∷⟩ 2 ⋯⟅∷⟆
                  (quote Ops.correct ⟨ def ⟩ 2 ⋯⟅∷⟆ ring ⟨∷⟩ 1 ⋯⟅∷⟆ E lhs ⟨∷⟩ ρ ⟨∷⟩ []) ⟨∷⟩ [])
              ⟨∷⟩
              (quote Ops.correct ⟨ def ⟩ 2 ⋯⟅∷⟆ ring ⟨∷⟩ 1 ⋯⟅∷⟆ E rhs ⟨∷⟩ ρ ⟨∷⟩ []) ⟨∷⟩
              []
          where
          Ι′ : ℕ → Maybe Term
          Ι′ i = Maybe.map (λ x → quote Ι ⟨ con ⟩ E⟅∷⟆ Fin′ x ⟨∷⟩ []) (member i t)

          open ToExpr Ι′
          ρ : Term
          ρ = curriedTerm t
open Internal

-- This is the main macro you'll probably be using. Call it like this:
--
--   lemma : ∀ x y → x + y ≈ y + x
--   lemma = solve TypeRing
--
-- where TypRing is your implementation of AlmostCommutativeRing. (Find some
-- example implementations in Polynomial.Solver.Ring.AlmostCommutativeRing.Instances).
macro
  solve : Name → Term → TC ⊤
  solve ring hole = do
    ring′ ← def ring [] ∈Ring
    commitTC
    let open OverRing ring′
    nms ← ring⇓
    hole′ ← inferType hole >>= reduce
    let i , k , xs = underPi hole′
    just (lhs ∷ rhs ∷ []) ← pure (getArgs 2 xs)
      where nothing → typeError (strErr "Malformed call to solve." ∷
                                 strErr "Expected target type to be like: ∀ x y → x + y ≈ y + x." ∷
                                 strErr "Instead: " ∷
                                 termErr hole′ ∷
                                 [])
    unify hole (quote solve-fn ⟨ def ⟩ callSolver nms i k lhs rhs)

-- Use this macro when you want to solve something *under* a lambda. For example:
-- say you have a long proof, and you just want the solver to deal with an
-- intermediate step. Call it like so:
--
--   lemma₃ : ∀ x y → x + y * 1 + 3 ≈ 2 + 1 + y + x
--   lemma₃ x y = begin
--     x + y * 1 + 3 ≈⟨ +-comm x (y * 1) ⟨ +-cong ⟩ refl ⟩
--     y * 1 + x + 3 ≈⟨ solveOver (x ∷ y ∷ []) Int.ring ⟩
--     3 + y + x     ≡⟨ refl ⟩
--     2 + 1 + y + x ∎
--
-- The first argument is the free variables, and the second is the
-- ring implementation (as before).
--
-- One thing to note here is that we need to be able to infer *both* sides of
-- the equality, which the normal equaltional reasoning combinators don't let you
-- do. You'll need the combinators defined in Relation.Binary.Reasoning.Inference.
-- These are just as powerful as the others, but have slightly better inference properties.

solveOver-macro : Term → Name → Term → TC ⊤
solveOver-macro i ring hole = do
  ring′ ← def ring [] ∈Ring
  commitTC
  let open OverRing ring′
  nms ← ring⇓
  i′ ← i ∈List⟨Carrier⟩
  commitTC
  hole′ ← inferType hole >>= reduce
  just vars′ ← pure (vars i′)
    where nothing → typeError (strErr "Malformed call to solveOver." ∷
                                strErr "First argument should be a list of free variables." ∷
                                strErr "Instead: " ∷
                                termErr i′ ∷
                                [])
  just (lhs ∷ rhs ∷ []) ← pure (getArgs 2 hole′)
    where nothing → typeError (strErr "Malformed call to solveOver." ∷
                                strErr "First argument should be a list of free variables." ∷
                                strErr "Instead: " ∷
                                termErr hole′ ∷
                                [])
  unify hole (constructSoln nms (List.length vars′) vars′ lhs rhs)

macro
  solveOver : Term → Name → Term → TC ⊤
  solveOver = solveOver-macro

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
open import Relation.Binary.PropositionalEquality using (_≡_)

module AKS.Primality.Base where

open import AKS.Nat using (ℕ; _<_)
open import AKS.Nat.GCD using (_∣_; _∤_)

record IsPrime (p : ℕ) : Set where
  constructor IsPrime✓
  field
    1<p : 1 < p
    ∀i∣p[i≡p] : ∀ {i} → 1 < i → i ∣ p → i ≡ p

record IsComposite (c : ℕ) : Set where
  constructor IsComposite✓
  field
    p : ℕ
    p<c : p < c
    p-isPrime : IsPrime p
    p∣c : p ∣ c

record Prime : Set where
  constructor Prime✓
  field
    prime : ℕ
    isPrime : IsPrime prime

record Composite : Set where
  constructor Composite✓
  field
    composite : ℕ
    isComposite : IsComposite composite

data Compositionality (n : ℕ) : Set where
  Composite✓ : IsComposite n → Compositionality n
  Prime✓ : (∀ {p} → p < n → IsPrime p → p ∤ n) → Compositionality n

data Primality (n : ℕ) : Set where
  Composite✓ : IsComposite n → Primality n
  Prime✓ : IsPrime n → Primality n

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
module Properties.StepBeta where

open import Data.List
open import Data.List.All
open import Data.Product

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel
open import Values
open import Session
open import Schedule

open import ProcessSyntax
open import ProcessRun

open import Properties.Base

-- V: (λx.e)v = e[v/x]
-- let f = λx.e in let r = f v in E --> [let x = v in] let r = e in E

mklhs : ∀ {Φ tin tout} (e : Expr (tin ∷ []) tout) (E : Expr (tout ∷ Φ) TUnit) → Expr (tin ∷ Φ) TUnit
mklhs {Φ} e E =
  letbind (rght (split-all-right Φ)) (ulambda [] [] [] e)
  (letbind (left (left (split-all-right Φ))) (app (left (rght [])) (here []) (here []))
  E)

mkrhs : ∀ {Φ tin tout} (e : Expr (tin ∷ []) tout) (E : Expr (tout ∷ Φ) TUnit) → Expr (tin ∷ Φ) TUnit
mkrhs {Φ} e E =
  letbind (left (split-all-right Φ)) e E

reductionT : Set
reductionT = ∀ {tin tout}
  (e : Expr (tin ∷ []) tout) (E : Expr (tout ∷ []) TUnit)
  (v : Val [] tin)
  → let ϱ = vcons ss-[] v (vnil []-inactive) in
    let lhs = run (left []) ss-[] (mklhs e E) ϱ (halt []-inactive UUnit) in
    let rhs = run (left []) ss-[] (mkrhs e E) ϱ (halt []-inactive UUnit) in
    restart (restart lhs) ≡ rhs

reduction : reductionT
reduction e E v
  with split-env (rght []) (vcons ss-[] v (vnil []-inactive))
... | sperght
  = refl

-- open reduction

reduction-open-type : Set
reduction-open-type = ∀ {Φ tin tout}
  (e : Expr (tin ∷ []) tout) (E : Expr (tout ∷ Φ) TUnit)
  (ϱ : VEnv [] (tin ∷ Φ))
  → let lhs = run (left (split-all-left Φ)) ss-[] (mklhs e E) ϱ (halt []-inactive UUnit) in
    let rhs = run (left (split-all-left Φ)) ss-[] (mkrhs e E) ϱ (halt []-inactive UUnit) in
    restart (restart lhs) ≡ rhs

reduction-open : reduction-open-type
reduction-open {Φ} e E (vcons ss-[] v ϱ)
  rewrite split-rotate-lemma {Φ}
  | split-env-right-lemma0 ϱ
  with ssplit-compose3 ss-[] ss-[]
... | ssc3
  rewrite split-env-right-lemma0 ϱ
  | split-rotate-lemma {Φ}
  = refl

-- open reduction with split between closure and context

mktype' : Set
mktype' =  ∀ {Φ Φ₁ Φ₂ tin tout}
  (sp : Split Φ Φ₁ Φ₂) (un-Φ₁ : All Unr Φ₁) (e : Expr (tin ∷ Φ₁) tout) (E : Expr (tout ∷ Φ₂) TUnit)
  → Expr (tin ∷ Φ) TUnit

mklhs' : mktype'
mklhs' {Φ} {Φ₁} {Φ₂} sp un-Φ₁ e E =
  letbind (rght sp) (ulambda (split-all-left Φ₁) un-Φ₁ [] e)
  (letbind (left (left (split-all-right Φ₂))) (app (left (rght [])) (here []) (here []))
  E)

mkrhs' : mktype'
mkrhs' {Φ} {Φ₁} {Φ₂} sp un-Φ₁ e E =
  letbind (left sp) e E

reduction-open-type' : Set
reduction-open-type' = ∀ {Φ Φ₁ Φ₂ tin tout}
  (sp : Split Φ Φ₁ Φ₂) (un-Φ₁ : All Unr Φ₁)
  (e : Expr (tin ∷ Φ₁) tout) (E : Expr (tout ∷ Φ₂) TUnit)
  (ϱ : VEnv [] (tin ∷ Φ))
  → let lhs = run (left (split-all-left Φ)) ss-[] (mklhs' sp un-Φ₁ e E) ϱ (halt []-inactive UUnit) in
    let rhs = run (left (split-all-left Φ)) ss-[] (mkrhs' sp un-Φ₁ e E) ϱ (halt []-inactive UUnit) in
    restart (restart lhs) ≡ rhs

-- this runs into the split-from-disjoint, which was hacked into function application
-- it's not clear if there's a way round
-- hence the proposition needs to be proved with a more specific assumption
{-
reduction-open' : reduction-open-type'
reduction-open' {Φ} {Φ₁} {Φ₂} sp un-Φ₁ e E (vcons ss-[] v ϱ)
  rewrite split-rotate-lemma' sp
  with split-env sp ϱ
... | ([] , []) , ss-[] , ϱ₁ , ϱ₂
  rewrite split-env-left-lemma0 ϱ₁
  with ssplit-compose3 ss-[] ss-[]
... | ssc3
  rewrite split-env-right-lemma0 ϱ₂
  with ssplit-compose3 ss-[] ss-[]
... | ssc3'
  rewrite split-rotate-lemma {Φ₂}
  = {!!}
-}

-- straightforward generalization of the inspect pattern
record Reveal2_·_·_is_ {A B : Set} {C : A → B → Set}
                    (f : (x : A) (y : B) → C x y) (x : A) (y : B) (z : C x y) :
                    Set₁ where
  constructor [[_]]
  field eq : f x y ≡ z

inspect2 : ∀ {A B : Set} {C : A → B → Set}
          (f : (x : A) (y : B) → C x y) (x : A) (y : B) → Reveal2 f · x · y is f x y
inspect2 f x y = [[ refl ]]

reduction-open-type'' : Set
reduction-open-type'' = ∀ {Φ₁ Φ₂ tin tout} →
  let Φ,sp = split-from-disjoint Φ₁ Φ₂ in
  let Φ = proj₁ Φ,sp in
  let sp = proj₂ Φ,sp in
  (un-Φ₁ : All Unr Φ₁)
  (e : Expr (tin ∷ Φ₁) tout) (E : Expr (tout ∷ Φ₂) TUnit)
  (ϱ : VEnv [] (tin ∷ Φ))
  → let lhs = run (left (split-all-left Φ)) ss-[] (mklhs' sp un-Φ₁ e E) ϱ (halt []-inactive UUnit) in
    let rhs = run (left (split-all-left Φ)) ss-[] (mkrhs' sp un-Φ₁ e E) ϱ (halt []-inactive UUnit) in
    restart (restart lhs) ≡ rhs

reduction-open'' : reduction-open-type''
reduction-open'' {Φ₁} {Φ₂} un-Φ₁ e E (vcons ss-[] v ϱ)
  with split-from-disjoint Φ₁ Φ₂ | inspect2 split-from-disjoint Φ₁ Φ₂
... | Φ , sp | [[ eq ]]
  rewrite split-rotate-lemma' sp
  with split-env sp ϱ
... | ([] , []) , ss-[] , ϱ₁ , ϱ₂
  rewrite split-env-left-lemma0 ϱ₁
  with ssplit-compose3 ss-[] ss-[]
... | ssc3
  rewrite split-env-right-lemma0 ϱ₂
  with ssplit-compose3 ss-[] ss-[]
... | ssc3'
  rewrite split-rotate-lemma {Φ₂} | eq
  = refl

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session