text:
------------------------------------------------------------------------
-- Parsing of mixfix operators
------------------------------------------------------------------------

-- This module defines a grammar for the precedence graph g.

open import RecursiveDescent.Hybrid.Mixfix.Expr

module RecursiveDescent.Hybrid.Mixfix (g : PrecedenceGraph) where

import Data.Vec as Vec
import Data.List as List
open List using (List; []; _∷_; foldr; foldl)
import Data.Vec1 as Vec1
open Vec1 using (Vec₁)
open import Data.Product renaming (_,_ to pair)
open import Data.Product.Record using (_,_)
open import Data.Bool
open import Data.Unit
open import Data.Nat
open import Data.Function hiding (_⟨_⟩_)
import Data.String as String

open import RecursiveDescent.Hybrid.Mixfix.Fixity
open import RecursiveDescent.Index
open import RecursiveDescent.Hybrid
open import RecursiveDescent.Hybrid.Simple
open import RecursiveDescent.Hybrid.Lib
open Token String.decSetoid

-- Note that, even though grammar below is not recursive, these
-- functions are (mutually). Fortunately the recursion is structural,
-- though. Note also that the reason for not using the implementation
--
--   grammar (nodes ts) = choiceMap (\t -> ! node t) ts
--
-- is that this would lead to a definition of node-corners which
-- was not structurally recursive.

nodes-corners : PrecedenceGraph -> Corners
nodes-corners []       = _
nodes-corners (p ∷ ps) = _

node-corners : PrecedenceTree -> Corners
node-corners (precedence ops ps) = _

-- Nonterminals.

data NT : ParserType where
  -- Expressions.
  expr : NT _ Expr

  -- Expressions corresponding to zero or more nodes in the precedence
  -- graph: operator applications where the outermost operator has one
  -- of the precedences ps. The graph g is used for internal
  -- expressions.
  nodes : (ps : PrecedenceGraph) -> NT (false , nodes-corners ps) Expr

  -- Expressions corresponding to one node in the precedence graph:
  -- operator applications where the outermost operator has
  -- precedence p. The graph g is used for internal expressions.
  node : (p : PrecedenceTree) -> NT (false , node-corners p) Expr

-- The parser type used in this module.

P : Index -> Set -> Set1
P = Parser NamePart NT

-- A vector containing parsers recognising the name parts of the
-- operator.

nameParts : forall {fix arity} -> Operator fix arity ->
            Vec₁ (P _ NamePart) (1 + arity)
nameParts (operator ns) = Vec1.map₀₁ sym ns

-- Internal parts (all name parts plus internal expressions) of
-- operators of the given precedence and fixity.

internal : forall {fix}
           (ops : List (∃ (Operator fix))) -> P _ (Internal fix)
internal =
  choiceMap (\op' -> let op = proj₂ op' in
                     _∙_ op <$> (! expr between nameParts op))

-- The grammar.

grammar : Grammar NamePart NT
grammar expr                       = ! nodes g
grammar (nodes [])                 = fail
grammar (nodes (p ∷ ps))           = ! node p ∣ ! nodes ps
grammar (node (precedence ops ps)) =
     ⟪_⟫              <$>      ⟦ closed   ⟧
  ∣ _⟨_⟩_             <$>  ↑ ⊛ ⟦ infx non ⟧ ⊛ ↑
  ∣ flip (foldr _$_)  <$>      preRight +   ⊛ ↑
  ∣ foldl (flip _$_)  <$>  ↑ ⊛ postLeft +
  where
  -- ⟦ fix ⟧ parses the internal parts of operators with the
  -- current precedence level and fixity fix.
  ⟦_⟧ = \(fix : Fixity) -> internal (ops fix)

  -- Operator applications where the outermost operator binds
  -- tighter than the current precedence level.
  ↑ = ! nodes ps

  -- Right associative and prefix operators.
  preRight =  ⟪_⟩_ <$> ⟦ prefx ⟧
           ∣ _⟨_⟩_ <$> ↑ ⊛ ⟦ infx right ⟧

  -- Left associative and postfix operators.
  postLeft = flip _⟨_⟫                   <$> ⟦ postfx ⟧
           ∣ (\op e₂ e₁ -> e₁ ⟨ op ⟩ e₂) <$> ⟦ infx left ⟧ ⊛ ↑

-- An expression parser.

parseExpr : List NamePart -> List Expr
parseExpr = parse-complete (! expr) grammar

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Refactoring where
open import ParseTree hiding (after)
open import Data.List
open import Data.String hiding (_++_)
open import Data.Sum hiding (map)
open import Data.Product
open import ScopeParseTree
open import MatchUpNames
open import ScopeState
open import Data.Nat
open import InterpretCommand
open import Data.Maybe
open import Data.Vec using (toList  ; lookup ; Vec)
open import Data.Fin
open import AgdaHelperFunctions
open import PushArgument renaming (pushArgument to push)
open import IO.Primitive using (IO)
open import Typing
open import Data.Bool
open import ExtractFunction using (extract)
open import ExplicitImplicitConversion

doNothing : List ParseTree -> List ParseTree
doNothing x = x

{-# COMPILE GHC doNothing as doNothing #-}

scopeList : ScopeState (List ParseTree)
scopeList = do
  env {numVars} vars maxScopes scopes current <- get
  let decl = Data.Vec.map getDeclared scopes
  let scopeDec =  Data.Vec.map ( λ x -> Data.List.map (λ y -> Data.Vec.lookup y vars) x) decl
  fail $ Data.String.concat $ Data.List.map concatSpace $ Data.Vec.toList scopeDec
  where concatSpace : List String -> String
        concatSpace l =  (Data.String.concat l) Data.String.++ "\n"

varList : ScopeState (List ParseTree)
varList = do
  env vars maxScopes scopes current <- get
  fail $ Data.String.concat $ Data.Vec.toList vars

scopeOnly : List ParseTree -> IO (String ⊎ List ParseTree)
scopeOnly program = runScopeState (matchUpNames after scopeParseTreeList $ program) newEnv

{-# COMPILE GHC scopeOnly as scopeOnly #-}

checkCommand' : List ParseTree -> ℕ -> ScopeState String
checkCommand' list n = do
  let afterScoping = scopeOnly list
  newList <- scopeParseTreeList list
  just decl <- return $ getDeclarationIDForPoint newList n
    where nothing -> fail "Cursor is not in renameable instance"
  getNameForId decl

checkCommand : List ParseTree -> ℕ -> IO (String ⊎ String)
checkCommand list n = runScopeState (checkCommand' list n ) newEnv

{-# COMPILE GHC checkCommand as checkCommand #-}

rename' : List ParseTree -> ℕ -> String -> ScopeState (List ParseTree)
rename' program point newName = do
    scoped <- scopeParseTreeList program
    just decl <- return $ getDeclarationIDForPoint scoped point
      where nothing -> fail "Cursor is not in renameable instance"
    noerror <- replaceID decl newName
    matchUpNames scoped

rename : List ParseTree -> ℕ -> String -> IO (String ⊎ List ParseTree)
rename program point newName = runScopeState (rename' program point newName) newEnv

{-# COMPILE GHC rename as rename #-}

pushArgument' : List ParseTree -> ℕ -> ScopeState (List ParseTree)
pushArgument' program point = do
  scoped <- scopeParseTreeList program
  funcID , argNumber <- getFuncIdAndArgNumber scoped point
  push scoped funcID argNumber
pushArgument : List ParseTree -> ℕ -> IO (String ⊎ List ParseTree)
pushArgument program point = runScopeState (pushArgument' program point) newEnv

{-# COMPILE GHC pushArgument as pushArgument #-}

changeExplicitness' : List ParseTree -> ℕ -> ScopeState (List ParseTree)
changeExplicitness' program point = do
  scoped <- scopeParseTreeList program
  funcID , argNumber <- getFuncIdAndArgNumber scoped point
  convert scoped funcID argNumber

toggleExplicitness : List ParseTree -> ℕ -> IO (String ⊎ List ParseTree)
toggleExplicitness program point = runScopeState (changeExplicitness' program point) newEnv

{-# COMPILE GHC toggleExplicitness as toggleExplicitness #-}

extractFunction : List ParseTree -> ℕ -> ℕ -> String -> IO (String ⊎ List ParseTree)
extractFunction program startPoint endPoint filename = runScopeState (extract program startPoint endPoint filename) newEnv

{-# COMPILE GHC extractFunction as extractFunction #-}

ext: agda


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

open import Sets.EquivalenceRelations
open import Groups.Definition
open import Orders
open import Rings.Definition
open import Numbers.Integers.Integers
open import Numbers.Integers.Multiplication
open import Setoids.Setoids
open import LogicalFormulae
open import Sets.FinSet
open import Functions
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Order
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.WithK
open import Numbers.Modulo.Definition
open import Numbers.Modulo.Addition
open import Numbers.Modulo.Group
open import Rings.Examples.Examples
open import Numbers.Primes.PrimeNumbers
open import Groups.Lemmas
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Groups.Isomorphisms.Definition
open import Groups.Cyclic.Definition
open import Groups.QuotientGroup.Definition
open import Groups.Subgroups.Definition
open import Groups.Subgroups.Normal.Definition

module Groups.Examples.Examples where

trivialGroup : Group (reflSetoid (FinSet 1)) λ _ _ → fzero
Group.+WellDefined trivialGroup _ _ = refl
Group.0G trivialGroup = fzero
Group.inverse trivialGroup _ = fzero
Group.+Associative trivialGroup = refl
Group.identRight trivialGroup {fzero} = refl
Group.identRight trivialGroup {fsucc ()}
Group.identLeft trivialGroup {fzero} = refl
Group.identLeft trivialGroup {fsucc ()}
Group.invLeft trivialGroup = refl
Group.invRight trivialGroup = refl

elementPowZ : (n : ℕ) → (elementPower ℤGroup (nonneg 1) (nonneg n)) ≡ nonneg n
elementPowZ zero = refl
elementPowZ (succ n) rewrite elementPowZ n = refl

ℤCyclic : CyclicGroup ℤGroup
CyclicGroup.generator ℤCyclic = nonneg 1
CyclicGroup.cyclic ℤCyclic {nonneg x} = (nonneg x , elementPowZ x)
CyclicGroup.cyclic ℤCyclic {negSucc x} = (negSucc x , ans)
  where
    ans : (Group.inverse ℤGroup ((nonneg 1) +Z elementPower ℤGroup (nonneg 1) (nonneg x))) ≡ negSucc x
    ans rewrite elementPowZ x = refl

elementPowZn : (n : ℕ) → {pr : 0 <N succ (succ n)} → (power : ℕ) → (powerLess : power <N succ (succ n)) → {p : 1 <N succ (succ n)} → elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power) ≡ record { x = power ; xLess = powerLess }
elementPowZn n zero powerLess = equalityZn _ _ refl
elementPowZn n {pr} (succ power) powerLess {p} with TotalOrder.totality ℕTotalOrder (ℤn.x (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power))) (succ n)
elementPowZn n {pr} (succ power) powerLess {p} | inl (inl x) = equalityZn _ _ (applyEquality succ v)
  where
    t : elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) }) (nonneg power) ≡ record { x = power ; xLess = PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess }
    t = elementPowZn n {pr} power (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess) {succPreservesInequality (succIsPositive n)}
    u : elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power) ≡ record { x = power ; xLess = PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess }
    u rewrite <NRefl p (succPreservesInequality (succIsPositive n)) = t
    v : ℤn.x (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power)) ≡ power
    v rewrite u = refl
elementPowZn n {pr} (succ power) powerLess {p} | inl (inr x) with elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power)
elementPowZn n {pr} (succ power) powerLess {p} | inl (inr x) | record { x = x' ; xLess = xLess } = exFalso (noIntegersBetweenXAndSuccX _ x xLess)
elementPowZn n {pr} (succ power) powerLess {p} | inr x with inspect (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = p }) (nonneg power))
elementPowZn n {pr} (succ power) powerLess {p} | inr x | record { x = x' ; xLess = p' } with≡ inspected rewrite elementPowZn n {pr} power (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (a<SuccA power) powerLess) {p} | x = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) powerLess)

ℤnCyclic : (n : ℕ) → (pr : 0 <N n) → CyclicGroup (ℤnGroup n pr)
ℤnCyclic zero ()
CyclicGroup.generator (ℤnCyclic (succ zero) pr) = record { x = 0 ; xLess = pr }
CyclicGroup.cyclic (ℤnCyclic (succ zero) pr) {record { x = zero ; xLess = xLess }} rewrite <NRefl xLess (succIsPositive 0) | <NRefl pr (succIsPositive 0) = (nonneg 0 , refl)
CyclicGroup.cyclic (ℤnCyclic (succ zero) _) {record { x = succ x ; xLess = xLess }} = exFalso (zeroNeverGreater (canRemoveSuccFrom<N xLess))
ℤnCyclic (succ (succ n)) pr = record { generator = record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) } ; cyclic = λ {x} → ans x }
  where
    ans : (z : ℤn (succ (succ n)) pr) → Sg ℤ (λ i → (elementPower (ℤnGroup (succ (succ n)) pr) (record { x = 1 ; xLess = succPreservesInequality (succIsPositive n) }) i) ≡ z)
    ans record { x = x ; xLess = xLess } = nonneg x , elementPowZn n x xLess

multiplyByNHom : (n : ℕ) → GroupHom ℤGroup ℤGroup (λ i → i *Z nonneg n)
GroupHom.groupHom (multiplyByNHom n) {x} {y} = lemma1
  where
    open Setoid (reflSetoid ℤ)
    open Group ℤGroup
    lemma : nonneg n *Z (x +Z y) ≡ (nonneg n) *Z x +Z nonneg n *Z y
    lemma = Ring.*DistributesOver+ ℤRing {nonneg n} {x} {y}
    lemma1 : (x +Z y) *Z nonneg n ≡ x *Z nonneg n +Z y *Z nonneg n
    lemma1 rewrite Ring.*Commutative ℤRing {x +Z y} {nonneg n} | Ring.*Commutative ℤRing {x} {nonneg n} | Ring.*Commutative ℤRing {y} {nonneg n} = lemma
GroupHom.wellDefined (multiplyByNHom n) {x} {.x} refl = refl

modNExampleGroupHom : (n : ℕ) → (pr : 0 <N n) → GroupHom ℤGroup (ℤnGroup n pr) (mod n pr)
GroupHom.groupHom (modNExampleGroupHom n 0<n) {x} {y} = {!!}
GroupHom.wellDefined (modNExampleGroupHom n 0<n) {x} {.x} refl = refl

intoZn : {n : ℕ} → {pr : 0 <N n} → (x : ℕ) → (x<n : x <N n) → mod n pr (nonneg x) ≡ record { x = x ; xLess = x<n }
intoZn {zero} {()}
intoZn {succ n} {0<n} x x<n with divisionAlg (succ n) x
intoZn {succ n} {0<n} x x<n | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl y ; quotSmall = quotSmall } = equalityZn _ _ (modIsUnique (record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl y ; quotSmall = quotSmall }) (record { quot = 0 ; rem = x ; pr = ans ; remIsSmall = inl x<n ; quotSmall = inl (succIsPositive n)}))
  where
    ans : n *N 0 +N x ≡ x
    ans rewrite multiplicationNIsCommutative n 0 = refl
intoZn {succ n} {0<n} x x<n | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }

quotientZn : (n : ℕ) → (pr : 0 <N n) → GroupIso (quotientGroupByHom ℤGroup (modNExampleGroupHom n pr)) (ℤnGroup n pr) (mod n pr)
GroupHom.groupHom (GroupIso.groupHom (quotientZn n pr)) = GroupHom.groupHom (modNExampleGroupHom n pr)
GroupHom.wellDefined (GroupIso.groupHom (quotientZn n pr)) {x} {y} x~y = need
  where
    given : mod n pr (x +Z (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
    given = x~y
    given' : (mod n pr x) +n (mod n pr (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
    given' = transitivity (equalityCommutative (GroupHom.groupHom (modNExampleGroupHom n pr))) given
    given'' : (mod n pr x) +n Group.inverse (ℤnGroup n pr) (mod n pr y) ≡ record { x = 0 ; xLess = pr}
    given'' = transitivity (applyEquality (λ i → mod n pr x +n i) (equalityCommutative (homRespectsInverse (modNExampleGroupHom n pr)))) given'
    need : mod n pr x ≡ mod n pr y
    need = transferToRight (ℤnGroup n pr) given''
SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (quotientZn n pr))) {x} {y} x=y = {!!}
SetoidSurjection.wellDefined (SetoidBijection.surj (GroupIso.bij (quotientZn n pr))) {x} {y} = SetoidInjection.wellDefined (SetoidBijection.inj (GroupIso.bij (quotientZn n pr))) {x} {y}
SetoidInjection.injective (SetoidBijection.inj (GroupIso.bij (quotientZn n pr))) {x} {y} fx~fy = need
  where
    given : mod n pr x +n Group.inverse (ℤnGroup n pr) (mod n pr y) ≡ record { x = 0 ; xLess = pr }
    given = transferToRight'' (ℤnGroup n pr) fx~fy
    given' : mod n pr (x +Z (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
    given' = identityOfIndiscernablesLeft _≡_ given (equalityCommutative (transitivity (GroupHom.groupHom (modNExampleGroupHom n pr) {x}) (applyEquality (λ i → mod n pr x +n i) (homRespectsInverse (modNExampleGroupHom n pr)))))
    need' : (mod n pr x) +n (mod n pr (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr }
    need' rewrite equalityCommutative (GroupHom.groupHom (modNExampleGroupHom n pr) {x} {Group.inverse ℤGroup y}) = given'
    need : mod n pr (x +Z (Group.inverse ℤGroup y)) ≡ record { x = 0 ; xLess = pr}
    need = identityOfIndiscernablesLeft _≡_ need' (equalityCommutative (GroupHom.groupHom (modNExampleGroupHom n pr)))
SetoidSurjection.surjective (SetoidBijection.surj (GroupIso.bij (quotientZn n pr))) {record { x = x ; xLess = xLess }} = nonneg x , intoZn x xLess

trivialGroupHom : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) → GroupHom trivialGroup G (λ _ → Group.0G G)
GroupHom.groupHom (trivialGroupHom {S = S} G) = symmetric identRight
  where
    open Setoid S
    open Group G
    open Equivalence eq
GroupHom.wellDefined (trivialGroupHom {S = S} G) _ = Equivalence.reflexive (Setoid.eq S)


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Monoidal.Cartesian where

open import Data.Product using (proj₁; proj₂) renaming (_×_ to _×₀_)
open import Data.Fin using (zero)

open import Categories.Category
open import Categories.Monoidal
open import Categories.Object.BinaryProducts
open import Categories.Object.Products
open import Categories.Object.Products.Properties
  renaming (module Properties to ProductProperties)
open import Categories.Object.Terminal
open import Categories.Bifunctor using (Bifunctor)
import Categories.Morphisms
open import Categories.Square
import Categories.Monoidal.Cartesian.Pentagon as Pentagon

Cartesian : ∀ {o ℓ e} (C : Category o ℓ e) → Products C → Monoidal C
Cartesian C Ps = record
  { ⊗ = ⊗
  ; id = ⊤
  ; identityˡ = record
    { F⇒G = record
      { η = λ X → π₂
      ; commute = λ f → commute₂
      }
    ; F⇐G = record
      { η = λ X → ⟨ ! , id ⟩
      ; commute = λ f → unitˡ-natural
      }
    ; iso = λ X → _≅_.iso unitˡ
    }
  ; identityʳ = record
    { F⇒G = record
      { η = λ X → π₁
      ; commute = λ f → commute₁
      }
    ; F⇐G = record
      { η = λ X → ⟨ id , ! ⟩
      ; commute = λ f → unitʳ-natural
      }
    ; iso = λ X → _≅_.iso unitʳ
    }
  ; assoc = record
    { F⇒G = record
      { η = λ X → assocˡ
      ; commute = λ f → assocˡ∘⁂
      }
    ; F⇐G = record
      { η = λ X → assocʳ
      ; commute = λ f → assocʳ∘⁂
      }
    ; iso = λ X → record
      { isoˡ = Iso.isoʳ (_≅_.iso ×-assoc)
      ; isoʳ = Iso.isoˡ (_≅_.iso ×-assoc)
      }
    }
  ; triangle = λ {X} → triangle {X}
  ; pentagon = pentagon
  }
  where
  open Categories.Morphisms C
  open Category C
  open Products Ps renaming (terminal to T₀; binary to P₀)
  open ProductProperties C Ps
  open Terminal T₀ using (⊤; !; !-unique; !-unique₂)

  open BinaryProducts P₀
  open Pentagon.Law C P₀ using (pentagon)

  ⊗ : Bifunctor C C C
  ⊗ = record
    { F₀ = λ p → proj₁ p × proj₂ p
    ; F₁ = λ x → proj₁ x ⁂ proj₂ x
    ; identity = identity
    ; homomorphism = Equiv.sym ⁂∘⁂
    ; F-resp-≡ = λ {A B F G} x → F-resp-≡ {A} {B} {F} {G} x
    }
    where
    .identity : ∀ {A : Obj ×₀ Obj} → (id {proj₁ A} ⁂ id {proj₂ A}) ≡ id
    identity = universal (id-comm {f = π₁}) (id-comm {f = π₂})

    .F-resp-≡ : ∀ {A B F G} F≡G → _
    F-resp-≡ {F = F} {G} x = ⟨⟩-cong₂ (∘-resp-≡ˡ (proj₁ x)) (∘-resp-≡ˡ (proj₂ x))

  -- The implicit x is actually used implicitly by the rest of the expression, so don't take it out,
  -- or Agda will complain about something referring to something to which it has no access.
  -- The connection between the mentioned x and the rest of the type is given by the caller way up
  -- there, so if that were not using these the triangle and pentagon laws would be yellow.
  .triangle : ∀ {x} → first π₁ ≡ second π₂ ∘ assocˡ
  triangle =
    begin
      first π₁
    ↓⟨ ⟨⟩-congʳ identityˡ ⟩
      ⟨ π₁ ∘ π₁ , π₂ ⟩
    ↑⟨ ⟨⟩-congʳ commute₂ ⟩
      ⟨ π₁ ∘ π₁ , π₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
    ↑⟨ second∘⟨⟩ ⟩
      second π₂ ∘ assocˡ
    ∎
    where
    open HomReasoning
    open Equiv

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --sized-types #-}
open import Relation.Binary.Core

module Heapsort.Impl1.Correctness.Permutation {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import BBHeap _≤_ hiding (forget ; flatten)
open import BBHeap.Heapify _≤_ tot≤ trans≤
open import BBHeap.Insert _≤_ tot≤ trans≤
open import BBHeap.Subtyping _≤_ trans≤
open import BHeap _≤_ hiding (forget) renaming (flatten to flatten')
open import BHeap.Order _≤_
open import BHeap.Order.Properties _≤_
open import BHeap.Properties _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List
open import Data.Nat renaming (_≤_ to _≤ₙ_)
open import Data.Sum
open import Heapsort.Impl1 _≤_ tot≤ trans≤
open import List.Permutation.Base A
open import List.Permutation.Base.Equivalence A
open import List.Permutation.Base.Concatenation A
open import OList _≤_
open import Order.Total _≤_ tot≤
open import Relation.Binary

open DecTotalOrder decTotalOrder hiding (refl)

lemma-flatten-flatten' : {b : Bound}(h : BHeap b)(accₕ : Acc h) → forget (flatten h accₕ) ∼ flatten' h
lemma-flatten-flatten' lf _ = ∼[]
lemma-flatten-flatten' (nd b≤x l r) (acc rs) = ∼x /head /head (trans∼ (lemma-flatten-flatten' (merge tot≤ l r) (rs (merge tot≤ l r) (lemma-merge≤′ tot≤ b≤x l r))) (lemma-merge∼ tot≤ l r))

lemma-flatten'-flatten : {b : Bound}(h : BHeap b)(accₕ : Acc h) → (flatten' h) ∼ (forget (flatten h accₕ))
lemma-flatten'-flatten h tₕ = sym∼ (lemma-flatten-flatten' h tₕ)

lemma-subtyping≡ : {b b' : Bound}(b'≤b : LeB b' b)(h : BBHeap b) → (flatten' (relax (subtyping b'≤b h))) ≡ flatten' (relax h)
lemma-subtyping≡ b'≤b leaf = refl
lemma-subtyping≡ b'≤b (left {l = l} {r = r} b≤x l⋘r) rewrite lemma-subtyping≡ b≤x l | lemma-subtyping≡ b≤x r = refl
lemma-subtyping≡ b'≤b (right {l = l} {r = r} b≤x l⋙r) rewrite lemma-subtyping≡ b≤x l | lemma-subtyping≡ b≤x r = refl

lemma-insert∼ : {b : Bound}{x : A}(b≤x : LeB b (val x))(h : BBHeap b) → (x ∷ flatten' (relax h)) ∼ (flatten' (relax (insert b≤x h)))
lemma-insert∼ b≤x leaf = refl∼
lemma-insert∼ {x = x} b≤x (left {x = y} {l = l} {r = r} b≤y l⋘r)
    with tot≤ x y
... | inj₁ x≤y
    with lemma-insert⋘ (lexy refl≤) l⋘r
... | inj₁ lᵢ⋘r
           rewrite lemma-subtyping≡ {val y} {val x} (lexy x≤y) (insert {val y} {y} (lexy refl≤) l)
                     | lemma-subtyping≡ {val y} {val x} (lexy x≤y) r
                     = ∼x /head /head (lemma++∼r (lemma-insert∼ (lexy refl≤) l))
... | inj₂ lᵢ⋗r
           rewrite  lemma-subtyping≡ {val y} {val x} (lexy x≤y) (insert {val y} {y} (lexy refl≤) l)
                      | lemma-subtyping≡ {val y} {val x} (lexy x≤y) r
                      = ∼x /head /head (lemma++∼r (lemma-insert∼ (lexy refl≤) l))
lemma-insert∼ {x = x} b≤x (left {x = y} {l = l} {r = r} b≤y l⋘r) | inj₂ y≤x
    with lemma-insert⋘ (lexy y≤x) l⋘r
... | inj₁ lᵢ⋘r = ∼x (/tail /head) /head (lemma++∼r (lemma-insert∼ (lexy y≤x) l))
... | inj₂ lᵢ⋗r = ∼x (/tail /head) /head (lemma++∼r (lemma-insert∼ (lexy y≤x) l))
lemma-insert∼ {x = x} b≤x (right {x = y} {l = l} {r = r} b≤y l⋙r)
    with tot≤ x y
... | inj₁ x≤y
    with lemma-insert⋙ (lexy refl≤) l⋙r
... | inj₁ l⋙rᵢ
           rewrite lemma-subtyping≡ {val y} {val x} (lexy x≤y) (insert {val y} {y} (lexy refl≤) r)
                     | lemma-subtyping≡ {val y} {val x} (lexy x≤y) l
                     = ∼x /head /head (trans∼ (∼x /head (lemma++/ {xs = flatten' (relax l)}) refl∼) (lemma++∼l {xs = flatten' (relax l)} (lemma-insert∼ (lexy refl≤) r)))
... | inj₂ l≃rᵢ
           rewrite lemma-subtyping≡ {val y} {val x} (lexy x≤y) (insert {val y} {y} (lexy refl≤) r)
                     | lemma-subtyping≡ {val y} {val x} (lexy x≤y) l
                     = ∼x /head /head (trans∼ (∼x /head (lemma++/ {xs = flatten' (relax l)}) refl∼) (lemma++∼l {xs = flatten' (relax l)} (lemma-insert∼ (lexy refl≤) r)))
lemma-insert∼ {x = x} b≤x (right {x = y} {l = l} {r = r} b≤y l⋙r) | inj₂ y≤x
    with lemma-insert⋙ (lexy y≤x) l⋙r
... | inj₁ l⋙rᵢ = ∼x (/tail /head) /head (trans∼ (∼x /head (lemma++/ {xs = flatten' (relax l)}) refl∼) (lemma++∼l {xs = flatten' (relax l)} (lemma-insert∼ (lexy y≤x) r)))
... | inj₂ l≃rᵢ = ∼x (/tail /head) /head (trans∼ (∼x /head (lemma++/ {xs = flatten' (relax l)}) refl∼) (lemma++∼l {xs = flatten' (relax l)} (lemma-insert∼ (lexy y≤x) r)))

theorem-heapsort∼ : (xs : List A) → xs ∼ forget (heapsort xs)
theorem-heapsort∼ [] = ∼[]
theorem-heapsort∼ (x ∷ xs) = trans∼ (trans∼ (∼x /head /head (trans∼ (theorem-heapsort∼ xs) (lemma-flatten-flatten' h' accₕ'))) (lemma-insert∼ lebx h)) (lemma-flatten'-flatten (hᵢ) accₕᵢ)
              where h = heapify xs
                    h' = relax h
                    accₕ' = ≺-wf h'
                    hᵢ = relax (insert lebx h)
                    accₕᵢ = ≺-wf hᵢ

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
open import Common.Prelude
open import Common.Equality

test : "foo" ≡ "bar" → Set₁
test refl = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- 2012-02-22
module CorrectPrintingOfVariablesInSortCheckingForData where

data Bool : Set where
  true false : Bool

if_then_else_ : {A : Set2} → Bool → A → A → A
if true then a else b = a
if false then a else b = b

data foo : (y : Bool) → if y then Set else Set

data foo where
  bar : foo true

-- This should print
--   if y then Set else Set != Set of type Set₁
-- and not
--   if @0 then ...

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring -- for length
open import Lists.Definition
open import Lists.Fold.Fold

module Lists.Length where

length : {a : _} {A : Set a} (l : List A) → ℕ
length [] = zero
length (x :: l) = succ (length l)

length' : {a : _} {A : Set a} → (l : List A) → ℕ
length' = fold (λ _ → succ) 0

length=length' : {a : _} {A : Set a} (l : List A) → length l ≡ length' l
length=length' [] = refl
length=length' (x :: l) = applyEquality succ (length=length' l)


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

-- Bifunctor, aka a Functor from C × D to E
open import Level

open import Categories.Category
open import Categories.Functor
open import Categories.Functor.Construction.Constant
open import Categories.Category.Product

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

Bifunctor : Category o ℓ e → Category o′ ℓ′ e′ → Category o″ ℓ″ e″ → Set _
Bifunctor C D E = Functor (Product C D) E

overlap-× : ∀ (H : Bifunctor D₁ D₂ C) (F : Functor E D₁) (G : Functor E D₂) → Functor E C
overlap-× H F G = H ∘F (F ※ G)

reduce-× : ∀ (H : Bifunctor D₁ D₂ C) (F : Functor E₁ D₁) (G : Functor E₂ D₂) → Bifunctor E₁ E₂ C
reduce-× H F G = H ∘F (F ⁂ G)

flip-bifunctor : Bifunctor C D E → Bifunctor D C E
flip-bifunctor b = b ∘F Swap

appˡ : Bifunctor C D E → Category.Obj C → Functor D E
appˡ F c = F ∘F constˡ c

appʳ : Bifunctor C D E → Category.Obj D → Functor C E
appʳ F d = F ∘F constʳ d

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

module Agda.Builtin.Sigma where

open import Agda.Primitive

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

infixr 4 _,_

{-# BUILTIN SIGMA Σ #-}

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
------------------------------------------------------------------------
-- Code for converting Vec₁ n A → B to and from n-ary functions
------------------------------------------------------------------------

-- I want universe polymorphism.

module Data.Vec.N-ary1 where

open import Data.Nat
open import Data.Vec1
open import Relation.Binary.PropositionalEquality1

------------------------------------------------------------------------
-- N-ary functions

N-ary : ℕ → Set₁ → Set₁ → Set₁
N-ary zero    A B = B
N-ary (suc n) A B = A → N-ary n A B

------------------------------------------------------------------------
-- Conversion

curryⁿ : ∀ {n A B} → (Vec₁ A n → B) → N-ary n A B
curryⁿ {zero}  f = f []
curryⁿ {suc n} f = λ x → curryⁿ (λ xs → f (x ∷ xs))

_$ⁿ_ : ∀ {n A B} → N-ary n A B → (Vec₁ A n → B)
f $ⁿ []       = f
f $ⁿ (x ∷ xs) = f x $ⁿ xs

------------------------------------------------------------------------
-- N-ary function equality

Eq : ∀ {A B} n → (B → B → Set₁) → (f g : N-ary n A B) → Set₁
Eq zero    _∼_ f g = f ∼ g
Eq (suc n) _∼_ f g = ∀ x → Eq n _∼_ (f x) (g x)

------------------------------------------------------------------------
-- Some lemmas

-- The two functions are inverses.

left-inverse : ∀ {n A B} (f : Vec₁ A n → B) →
               ∀ xs → curryⁿ f $ⁿ xs ≡₁ f xs
left-inverse f []       = refl
left-inverse f (x ∷ xs) = left-inverse (λ xs → f (x ∷ xs)) xs

data Lift {A : Set₁} (R : A → A → Set) x y : Set₁ where
  lift : R x y → Lift R x y

right-inverse : ∀ {A B} n (f : N-ary n A B) →
                Eq n (Lift _≡₁_) (curryⁿ (_$ⁿ_ {n} f)) f
right-inverse zero    f = lift refl
right-inverse (suc n) f = λ x → right-inverse n (f x)

-- Conversion preserves equality.

curryⁿ-pres : ∀ {n A B _∼_} (f g : Vec₁ A n → B) →
              (∀ xs → f xs ∼ g xs) →
              Eq n _∼_ (curryⁿ f) (curryⁿ g)
curryⁿ-pres {zero}  f g hyp = hyp []
curryⁿ-pres {suc n} f g hyp = λ x →
  curryⁿ-pres (λ xs → f (x ∷ xs)) (λ xs → g (x ∷ xs))
              (λ xs → hyp (x ∷ xs))

curryⁿ-pres⁻¹ : ∀ {n A B _∼_} (f g : Vec₁ A n → B) →
                Eq n _∼_ (curryⁿ f) (curryⁿ g) →
                ∀ xs → f xs ∼ g xs
curryⁿ-pres⁻¹ f g hyp []       = hyp
curryⁿ-pres⁻¹ f g hyp (x ∷ xs) =
  curryⁿ-pres⁻¹ (λ xs → f (x ∷ xs)) (λ xs → g (x ∷ xs)) (hyp x) xs

appⁿ-pres : ∀ {n A B _∼_} (f g : N-ary n A B) →
            Eq n _∼_ f g →
            (xs : Vec₁ A n) → (f $ⁿ xs) ∼ (g $ⁿ xs)
appⁿ-pres f g hyp []       = hyp
appⁿ-pres f g hyp (x ∷ xs) = appⁿ-pres (f x) (g x) (hyp x) xs

appⁿ-pres⁻¹ : ∀ {n A B _∼_} (f g : N-ary n A B) →
              ((xs : Vec₁ A n) → (f $ⁿ xs) ∼ (g $ⁿ xs)) →
              Eq n _∼_ f g
appⁿ-pres⁻¹ {zero}  f g hyp = hyp []
appⁿ-pres⁻¹ {suc n} f g hyp = λ x →
  appⁿ-pres⁻¹ (f x) (g x) (λ xs → hyp (x ∷ xs))

max_issues_repo_name: larrytheliquid/Lemmachine


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

module PlainPi where

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality

infixr 70 _×ᵤ_
infixr 60 _+ᵤ_
infixr 50 _⊚_

------------------------------------------------------------------------------
-- Pi

data 𝕌 : Set
⟦_⟧ : (A : 𝕌) → Set
data _⟷_ : 𝕌 → 𝕌 → Set
eval : {A B : 𝕌} → (A ⟷ B) → ⟦ A ⟧ → ⟦ B ⟧

data 𝕌 where
  𝟘       : 𝕌
  𝟙       : 𝕌
  _+ᵤ_    : 𝕌 → 𝕌 → 𝕌
  _×ᵤ_    : 𝕌 → 𝕌 → 𝕌

⟦ 𝟘 ⟧ = ⊥
⟦ 𝟙 ⟧ = ⊤
⟦ t₁ +ᵤ t₂ ⟧ = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ t₁ ×ᵤ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

data _⟷_ where
  unite₊l : {t : 𝕌} → 𝟘 +ᵤ t ⟷ t
  uniti₊l : {t : 𝕌} → t ⟷ 𝟘 +ᵤ t
  unite₊r : {t : 𝕌} → t +ᵤ 𝟘 ⟷ t
  uniti₊r : {t : 𝕌} → t ⟷ t +ᵤ 𝟘
  swap₊   : {t₁ t₂ : 𝕌} → t₁ +ᵤ t₂ ⟷ t₂ +ᵤ t₁
  assocl₊ : {t₁ t₂ t₃ : 𝕌} → t₁ +ᵤ (t₂ +ᵤ t₃) ⟷ (t₁ +ᵤ t₂) +ᵤ t₃
  assocr₊ : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) +ᵤ t₃ ⟷ t₁ +ᵤ (t₂ +ᵤ t₃)
  unite⋆l : {t : 𝕌} → 𝟙 ×ᵤ t ⟷ t
  uniti⋆l : {t : 𝕌} → t ⟷ 𝟙 ×ᵤ t
  unite⋆r : {t : 𝕌} → t ×ᵤ 𝟙 ⟷ t
  uniti⋆r : {t : 𝕌} → t ⟷ t ×ᵤ 𝟙
  swap⋆   : {t₁ t₂ : 𝕌} → t₁ ×ᵤ t₂ ⟷ t₂ ×ᵤ t₁
  assocl⋆ : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ ×ᵤ t₃) ⟷ (t₁ ×ᵤ t₂) ×ᵤ t₃
  assocr⋆ : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₂) ×ᵤ t₃ ⟷ t₁ ×ᵤ (t₂ ×ᵤ t₃)
  absorbr : {t : 𝕌} → 𝟘 ×ᵤ t ⟷ 𝟘
  absorbl : {t : 𝕌} → t ×ᵤ 𝟘 ⟷ 𝟘
  factorzr : {t : 𝕌} → 𝟘 ⟷ t ×ᵤ 𝟘
  factorzl : {t : 𝕌} → 𝟘 ⟷ 𝟘 ×ᵤ t
  dist    : {t₁ t₂ t₃ : 𝕌} → (t₁ +ᵤ t₂) ×ᵤ t₃ ⟷ (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃)
  factor  : {t₁ t₂ t₃ : 𝕌} → (t₁ ×ᵤ t₃) +ᵤ (t₂ ×ᵤ t₃) ⟷ (t₁ +ᵤ t₂) ×ᵤ t₃
  distl   : {t₁ t₂ t₃ : 𝕌} → t₁ ×ᵤ (t₂ +ᵤ t₃) ⟷ (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃)
  factorl : {t₁ t₂ t₃ : 𝕌 } → (t₁ ×ᵤ t₂) +ᵤ (t₁ ×ᵤ t₃) ⟷ t₁ ×ᵤ (t₂ +ᵤ t₃)
  id⟷     : {t : 𝕌} → t ⟷ t
  _⊚_     : {t₁ t₂ t₃ : 𝕌} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ +ᵤ t₂ ⟷ t₃ +ᵤ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : 𝕌} → (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (t₁ ×ᵤ t₂ ⟷ t₃ ×ᵤ t₄)

eval unite₊l (inj₂ v) = v
eval uniti₊l v  = inj₂ v
eval unite₊r (inj₁ v) = v
eval uniti₊r v  = inj₁ v
eval swap₊ (inj₁ v) = inj₂ v
eval swap₊ (inj₂ v) = inj₁ v
eval assocl₊ (inj₁ v) = inj₁ (inj₁ v)
eval assocl₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
eval assocl₊ (inj₂ (inj₂ v)) = inj₂ v
eval assocr₊ (inj₁ (inj₁ v)) = inj₁ v
eval assocr₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
eval assocr₊ (inj₂ v) = inj₂ (inj₂ v)
eval unite⋆l (tt , v) = v
eval uniti⋆l v = (tt , v)
eval unite⋆r (v , tt) = v
eval uniti⋆r v = (v , tt)
eval swap⋆ (v₁ , v₂)          = (v₂ , v₁)
eval assocl⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
eval assocr⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
eval absorbl ()
eval absorbr ()
eval factorzl ()
eval factorzr ()
eval dist (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
eval dist (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
eval factor (inj₁ (v₁ , v₃)) = (inj₁ v₁ , v₃)
eval factor (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)
eval distl (v , inj₁ v₁) = inj₁ (v , v₁)
eval distl (v , inj₂ v₂) = inj₂ (v , v₂)
eval factorl (inj₁ (v , v₁)) = (v , inj₁ v₁)
eval factorl (inj₂ (v , v₂)) = (v , inj₂ v₂)
eval id⟷ v = v
eval (c₁ ⊚ c₂) v = eval c₂ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₁ v) = inj₁ (eval c₁ v)
eval (c₁ ⊕ c₂) (inj₂ v) = inj₂ (eval c₂ v)
eval (c₁ ⊗ c₂) (v₁ , v₂) = (eval c₁ v₁ , eval c₂ v₂)

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Transformation where

open import Data.Integer using (ℤ; +_; _-_; -_)
open import Data.List    using (List; _∷_; []; map; reverse)
open import Data.Product using (_,_)

open import Note         using (Note; tone; rest)
open import Pitch        using (Pitch; transposePitch)
open import Interval     using (PitchPair)

retrograde : List Note → List Note
retrograde = reverse

-- Create a list of intervals between all adjacent tones, ignoring rests.
intervals : List Note → List ℤ
intervals [] = []
intervals (rest _ ∷ ns) = intervals ns
intervals (tone d p ∷ ns) = intervals' p ns where
  intervals' : Pitch → List Note → List ℤ
  intervals' p []                              = []
  intervals' p (rest d ∷ ns)                   = intervals' p ns
  intervals' p (tone d q ∷ ns) = (+ q) - (+ p) ∷ intervals' q ns

inversion : List Note → List Note
inversion []                 = []
inversion    (rest d   ∷ ns) = rest d   ∷ inversion ns
inversion xs@(tone d p ∷ ns) = tone d p ∷ inversion' p is ns where
  is : List ℤ
  is = map (-_) (intervals xs)

  inversion' : Pitch → List ℤ → List Note → List Note
  inversion' p []         ns              = ns
  inversion' _ (_ ∷ _)    []              = []
  inversion' p is@(_ ∷ _) (rest d ∷ ns)   = rest d ∷ inversion' p is ns
  inversion' p (i ∷ is)   (tone d _ ∷ ns) = let q = transposePitch i p in (tone d q) ∷ inversion' q is ns

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
------------------------------------------------------------------------------
-- Properties of the divisibility relation
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.Divisibility.By0.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Divisibility.By0
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.PropertiesATP
open import FOTC.Data.Nat.PropertiesATP

------------------------------------------------------------------------------
-- Any positive number divides 0.
postulate S∣0 : ∀ n → succ₁ n ∣ zero
{-# ATP prove S∣0 #-}

-- 0 divides 0.
postulate 0∣0 : zero ∣ zero
{-# ATP prove 0∣0 #-}

-- The divisibility relation is reflexive.
postulate ∣-refl : ∀ {n} → N n → n ∣ n
{-# ATP prove ∣-refl *-leftIdentity #-}

-- If x divides y and z then x divides y ∸ z.
postulate
  x∣y→x∣z→x∣y∸z-helper : ∀ {m n o k k'} → N m → N k → N k' →
                         n ≡ k * m →
                         o ≡ k' * m →
                         n ∸ o ≡ (k ∸ k') * m
{-# ATP prove x∣y→x∣z→x∣y∸z-helper *∸-leftDistributive #-}

x∣y→x∣z→x∣y∸z : ∀ {m n o} → N m → N n → N o → m ∣ n → m ∣ o → m ∣ n ∸ o
x∣y→x∣z→x∣y∸z Nm Nn No (k , Nk , h₁) (k' , Nk' , h₂) =
  k ∸ k' , ∸-N Nk Nk' , x∣y→x∣z→x∣y∸z-helper Nm Nk Nk' h₁ h₂

-- If x divides y and z then x divides y + z.
postulate
  x∣y→x∣z→x∣y+z-helper : ∀ {m n o k k'} → N m → N k → N k' →
                         n ≡ k * m →
                         o ≡ k' * m →
                         n + o ≡ (k + k') * m
{-# ATP prove x∣y→x∣z→x∣y+z-helper *+-leftDistributive #-}

x∣y→x∣z→x∣y+z : ∀ {m n o} → N m → N n → N o → m ∣ n → m ∣ o → m ∣ n + o
x∣y→x∣z→x∣y+z Nm Nn No (k , Nk , h₁) (k' , Nk' , h₂) =
  k + k' , +-N Nk Nk' , x∣y→x∣z→x∣y+z-helper Nm Nk Nk' h₁ h₂

-- If x divides y and y is positive, then x ≤ y.
postulate x∣S→x≤S-helper₁ : ∀ {m n} → succ₁ n ≡ zero * m → ⊥
{-# ATP prove x∣S→x≤S-helper₁ #-}

-- Nice proof by the ATPa.
postulate x∣S→x≤S-helper₂ : ∀ {m n o} → N m → N n → N o →
                            succ₁ n ≡ succ₁ o * m →
                            m ≤ succ₁ n
{-# ATP prove x∣S→x≤S-helper₂ x≤x+y *-N #-}

x∣S→x≤S : ∀ {m n} → N m → N n → m ∣ (succ₁ n) → m ≤ succ₁ n
x∣S→x≤S Nm Nn (.zero , nzero , Sn≡0*m) = ⊥-elim (x∣S→x≤S-helper₁ Sn≡0*m)
x∣S→x≤S Nm Nn (.(succ₁ k) , nsucc {k} Nk , Sn≡Sk*m) =
  x∣S→x≤S-helper₂ Nm Nn Nk Sn≡Sk*m

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

--(Binary) product of objects and morphisms

module Categories.Object.Product {o ℓ e} (C : Category o ℓ e) where

open import Categories.Object.Product.Core C public
open import Categories.Object.Product.Morphisms C public


text:
module examplesPaperJFP.finn where

open import Data.Nat

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

mutual
  data Even : ℕ → Set where
    0p    : Even 0
    sucp  : {n : ℕ}  →  Odd n   →  Even  (suc  n)

  data Odd : ℕ → Set where
    sucp  : {n : ℕ}  →  Even n  →  Odd   (suc  n)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

module CombiningProofs.WhereTranslation where

open import FOTC.Base
open import FOTC.Data.Nat

-- See Issue https://github.com/asr/apia/issues/81 .
+-rightIdentityA : D → Set
+-rightIdentityA i = i + zero ≡ i
{-# ATP definition +-rightIdentityA #-}

+-rightIdentity : ∀ {n} → N n → n + zero ≡ n
+-rightIdentity Nn = N-ind +-rightIdentityA A0 is Nn
  where
  postulate A0 : +-rightIdentityA zero
  {-# ATP prove A0 #-}

  postulate is : ∀ {i} → +-rightIdentityA i → +-rightIdentityA (succ₁ i)
  {-# ATP prove is #-}

A' : ∀ {n} → (Nn : N n) → D → Set
A' Nn i = i + zero ≡ i
-- {-# ATP definition A' #-}

postulate A0' : ∀ {n} → (Nn : N n) → A' Nn zero
-- {-# ATP prove A0' #-}

postulate is' : ∀ {n} → (Nn : N n) → ∀ {i} → A' Nn i → A' Nn (succ₁ i)
-- {-# ATP prove is' #-}


text:
-- (Pre)abelian categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Abelian.Base where

open import Cubical.Categories.Additive.Base
open import Cubical.Categories.Category.Base
open import Cubical.Categories.Morphism
open import Cubical.Data.Sigma.Base
open import Cubical.Foundations.Prelude

private
  variable
    ℓ ℓ' : Level

-- (Co)kernels
module _ (C : PreaddCategory ℓ ℓ') where
  open PreaddCategory C

  module _ {x y : ob} (f : Hom[ x , y ]) where

    -- Kernels
    record IsKernel {k : ob} (ker : Hom[ k , x ]) : Type (ℓ-max ℓ ℓ') where
      field
        ker⋆f : ker ⋆ f ≡ 0h
        univ : ∀ (w : ob) (t : Hom[ w , x ])
          → (t ⋆ f ≡ 0h) → ∃![ u ∈ Hom[ w , k ] ] (u ⋆ ker ≡ t)

    record Kernel : Type (ℓ-max ℓ ℓ') where
      constructor kernel
      field
        k : ob
        ker : Hom[ k , x ]
        isKer : IsKernel ker

      open IsKernel isKer public

    -- Cokernels
    record IsCokernel {c : ob} (coker : Hom[ y , c ]) : Type (ℓ-max ℓ ℓ') where
      field
        f⋆coker : f ⋆ coker ≡ 0h
        univ : ∀ (w : ob) (t : Hom[ y , w ])
          → (f ⋆ t ≡ 0h) → ∃![ u ∈ Hom[ c , w ] ] (coker ⋆ u ≡ t)

    record Cokernel : Type (ℓ-max ℓ ℓ') where
      field
        c : ob
        coker : Hom[ y , c ]
        isCoker : IsCokernel coker

      open IsCokernel isCoker public

-- Preabelian categories
record PreabCategoryStr (C : AdditiveCategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  open AdditiveCategory C
  field
    hasKernels : {x y : ob} → (f : Hom[ x , y ]) → Kernel preaddcat f
    hasCokernels : {x y : ob} → (f : Hom[ x , y ]) → Cokernel preaddcat f

  -- Convenient ker/coker functions
  ker = λ {x y} (f : Hom[ x , y ]) → hasKernels f .Kernel.ker
  coker = λ {x y} (f : Hom[ x , y ]) → hasCokernels f .Cokernel.coker

record PreAbCategory (ℓ ℓ' : Level) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    additive : AdditiveCategory ℓ ℓ'
    preAbStr : PreabCategoryStr additive

  open AdditiveCategory additive public
  open PreabCategoryStr preAbStr public

-- Abelian categories
record AbelianCategoryStr (C : PreAbCategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
  open PreAbCategory C

  private
    _=ker_ : ∀ {k x y} → Hom[ k , x ] → Hom[ x , y ] → Type (ℓ-max ℓ ℓ')
    m =ker f = IsKernel preaddcat f m

    _=coker_ : ∀ {c x y} → Hom[ y , c ] → Hom[ x , y ] → Type (ℓ-max ℓ ℓ')
    e =coker f = IsCokernel preaddcat f e

  field
    monNormal : {x y : ob} → (m : Hom[ x , y ]) → isMonic cat m
      → Σ[ z ∈ ob ] Σ[ f ∈ Hom[ y , z ] ] (m =ker f)

    epiNormal : {x y : ob} → (e : Hom[ x , y ]) → isEpic cat e
      → Σ[ w ∈ ob ] Σ[ f ∈ Hom[ w , x ] ] (e =coker f)

record AbelianCategory (ℓ ℓ' : Level): Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    preAb : PreAbCategory ℓ ℓ'
    abelianStr : AbelianCategoryStr preAb

  open PreAbCategory preAb public
  open AbelianCategoryStr abelianStr public

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
module Prelude.Eq where

open import Prelude.Level

infix 4 _==_

data _==_ {l : Level}{A : Set l} (x : A) : A → Set l where
  refl : x == x

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

{-# BUILTIN EQUALITY _==_  #-}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


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

open import lib.Basics
open import lib.NType2
open import lib.types.Group
open import lib.types.Sigma
open import lib.types.Truncation

module lib.groups.SubgroupProp where

record SubgroupProp {i} (G : Group i) j : Type (lmax i (lsucc j)) where
  private
    module G = Group G
  field
    prop : G.El → Type j
    level : ∀ g → is-prop (prop g)
    -- In theory being inhabited implies that the identity is included,
    -- but in practice let's just prove the identity case.
    ident : prop G.ident
    diff : ∀ {g₁ g₂} → prop g₁ → prop g₂ → prop (G.diff g₁ g₂)

  subEl-prop : SubtypeProp G.El j
  subEl-prop = prop , level
  SubEl = Subtype subEl-prop

  abstract
    {-
      ident : prop G.ident
      ident = transport prop (G.inv-r (fst inhab)) (diff (snd inhab) (snd inhab))
    -}

    inv : ∀ {g} → prop g → prop (G.inv g)
    inv pg = transport prop (G.unit-l _) (diff ident pg)

    comp : ∀ {g₁ g₂} → prop g₁ → prop g₂ → prop (G.comp g₁ g₂)
    comp {g₁} {g₂} pg₁ pg₂ =
      transport prop (ap (G.comp g₁) (G.inv-inv g₂)) (diff pg₁ (inv pg₂))

is-fullᴳ : ∀ {i j} {G : Group i} → SubgroupProp G j → Type (lmax i j)
is-fullᴳ P = ∀ g → SubgroupProp.prop P g

-- Normal subgroups

is-normal : ∀ {i j} {G : Group i} → SubgroupProp G j → Type (lmax i j)
is-normal {G = G} P = ∀ g₁ {g₂} → P.prop g₂ → P.prop (Group.conj G g₁ g₂)
  where module P = SubgroupProp P

NormalSubgroupProp : ∀ {i} (G : Group i) j → Type (lmax i (lsucc j))
NormalSubgroupProp {i} G j = Σ (SubgroupProp G j) is-normal

module NormalSubgroupProp {i j} {G : Group i} (normal-prop : NormalSubgroupProp G j) where
  private
    module G = Group G

  propᴳ : SubgroupProp G j
  propᴳ = fst normal-prop
  open SubgroupProp propᴳ public

  conj : is-normal propᴳ
  conj = snd normal-prop

  abstract
    comm : ∀ g₁ g₂ → prop (G.comp g₁ g₂) → prop (G.comp g₂ g₁)
    comm g₁ g₂ pg₁g₂ = transport prop
      ( ap (λ g → G.comp g (G.inv g₂)) (! (G.assoc g₂ g₁ g₂))
      ∙ G.assoc (G.comp g₂ g₁) g₂ (G.inv g₂)
      ∙ ap (G.comp (G.comp g₂ g₁)) (G.inv-r g₂)
      ∙ G.unit-r (G.comp g₂ g₁))
      (conj g₂ pg₁g₂)
    {- So far this is not used.
    unconj : ∀ g₁ g₂ → prop (G.conj g₁ g₂) → prop g₂
    unconj g₁ g₂ pg₁g₂ = transport prop path (conj (G.inv g₁) pg₁g₂) where
      path : G.conj (G.inv g₁) (G.conj g₁ g₂) == g₂
      path = ! (G.conj-comp-l (G.inv g₁) g₁ g₂) ∙ ap (λ g → G.conj g g₂) (G.inv-l g₁) ∙ G.conj-unit-l g₂
    -}

abstract
  comm-is-normal : ∀ {i j} {G : Group i} (P : SubgroupProp G j)
    → (∀ g₁ g₂ → SubgroupProp.prop P (Group.comp G g₁ g₂)
               → SubgroupProp.prop P (Group.comp G g₂ g₁))
    → is-normal P
  comm-is-normal {G = G} P P-comm g₁ {g₂} Pg₂ =
    transport! P.prop (G.assoc g₁ g₂ (G.inv g₁)) $
      P-comm (G.diff g₂ g₁) g₁ $
        transport! P.prop
          ( G.assoc g₂ (G.inv g₁) g₁
          ∙ ap (G.comp g₂) (G.inv-l g₁)
          ∙ G.unit-r g₂)
          Pg₂
    where module G = Group G
          module P = SubgroupProp P

  sub-abelian-is-normal : ∀ {i j} {G : Group i}
    → (G-is-abelian : is-abelian G)
    → (P : SubgroupProp G j)
    → is-normal P
  sub-abelian-is-normal {G = G} G-is-abelian P =
    comm-is-normal P λ g₁ g₂ Pg₁g₂ → transport P.prop (G.comm g₁ g₂) Pg₁g₂
    where module G = AbGroup (G , G-is-abelian)
          module P = SubgroupProp P

sub-abelian-normal : ∀ {i j} {G : Group i}
  → (G-is-abelian : is-abelian G)
  → SubgroupProp G j
  → NormalSubgroupProp G j
sub-abelian-normal G-is-abelian P = P , sub-abelian-is-normal G-is-abelian P

{- Subgroups of subgroups -}

infix 40 _⊆ᴳ_
_⊆ᴳ_ : ∀ {i j k} {G : Group i}
  → SubgroupProp G j → SubgroupProp G k → Type (lmax i (lmax j k))
P ⊆ᴳ Q = ∀ g → P.prop g → Q.prop g
  where module P = SubgroupProp P
        module Q = SubgroupProp Q

{- triviality -}

trivial-propᴳ : ∀ {i} (G : Group i) → SubgroupProp G i
trivial-propᴳ {i} G = record {M} where
  module G = Group G
  module M where
    prop : G.El → Type i
    prop g = g == G.ident

    ident : prop G.ident
    ident = idp

    level : ∀ g → is-prop (prop g)
    level g = G.El-level g G.ident

    abstract
      diff : {g₁ g₂ : G.El} → prop g₁ → prop g₂ → prop (G.diff g₁ g₂)
      diff g₁=id g₂=id = ap2 G.comp g₁=id (ap G.inv g₂=id ∙ G.inv-ident)
                       ∙ G.unit-r G.ident

is-trivial-propᴳ : ∀ {i j} {G : Group i} → SubgroupProp G j → Type (lmax i j)
is-trivial-propᴳ {G = G} P = P ⊆ᴳ trivial-propᴳ G

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import Generics.Prelude
open import Generics.Telescope
open import Generics.Desc
open import Generics.Mu

module Generics.Mu.Fold
  {P I n} {D : DataDesc P I n}
  {c} (X : ⟦ P , I ⟧xtel → Set c)
  (alg : ∀ {pi} → ⟦ D ⟧Data X pi → X pi) where

private
  variable
    p : ⟦ P ⟧tel tt
    V : ExTele P
    i : ⟦ I ⟧tel p
    v : ⟦ V ⟧tel p

fold : μ D (p , i) → X (p , i)

foldIndArg : (C : ConDesc P V I)
             (x : ⟦ C ⟧IndArgω (μ D) (p , v))
           → ⟦ C ⟧IndArg X (p , v)
foldIndArg (var _) x = fold x
foldIndArg (π ia _ C) x = fun< ia > λ s → foldIndArg C (x s)
foldIndArg (A ⊗ B) (xa , xb) = foldIndArg A xa , foldIndArg B xb

foldCon : (C : ConDesc P V I)
          (x : ⟦ C ⟧Conω (μ D) (p , v , i))
        → ⟦ C ⟧Con X (p , v , i)
foldCon (var _) (liftω refl) = refl
foldCon (π _ _ C) (s , x) = (s , foldCon C x)
foldCon (A ⊗ B) (xa , xb) = foldIndArg A xa , foldCon B xb

fold ⟨ k , x ⟩ = alg (k , foldCon (lookupCon D k) x)

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


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

module Cubical.Data.SumFin.Properties where

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

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Unit
import Cubical.Data.Fin as Fin
open import Cubical.Data.Nat
open import Cubical.Data.SumFin.Base as SumFin
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation

private
  variable
    ℓ : Level
    k : ℕ

SumFin→Fin : Fin k → Fin.Fin k
SumFin→Fin = SumFin.elim (λ {k} _ → Fin.Fin k) Fin.fzero Fin.fsuc

Fin→SumFin : Fin.Fin k → Fin k
Fin→SumFin = Fin.elim (λ {k} _ → Fin k) fzero fsuc

Fin→SumFin-fsuc : (fk : Fin.Fin k) → Fin→SumFin (Fin.fsuc fk) ≡ fsuc (Fin→SumFin fk)
Fin→SumFin-fsuc = Fin.elim-fsuc (λ {k} _ → Fin k) fzero fsuc

SumFin→Fin→SumFin : (fk : Fin k) → Fin→SumFin (SumFin→Fin fk) ≡ fk
SumFin→Fin→SumFin = SumFin.elim (λ fk → Fin→SumFin (SumFin→Fin fk) ≡ fk)
                                refl λ {k} {fk} eq →
  Fin→SumFin (Fin.fsuc (SumFin→Fin fk)) ≡⟨ Fin→SumFin-fsuc (SumFin→Fin fk) ⟩
  fsuc (Fin→SumFin (SumFin→Fin fk))     ≡⟨ cong fsuc eq ⟩
  fsuc fk                               ∎

Fin→SumFin→Fin : (fk : Fin.Fin k) → SumFin→Fin (Fin→SumFin fk) ≡ fk
Fin→SumFin→Fin = Fin.elim (λ fk → SumFin→Fin (Fin→SumFin fk) ≡ fk)
                          refl λ {k} {fk} eq →
  SumFin→Fin (Fin→SumFin (Fin.fsuc fk)) ≡⟨ cong SumFin→Fin (Fin→SumFin-fsuc fk) ⟩
  Fin.fsuc (SumFin→Fin (Fin→SumFin fk)) ≡⟨ cong Fin.fsuc eq ⟩
  Fin.fsuc fk                           ∎

SumFin≃Fin : ∀ k → Fin k ≃ Fin.Fin k
SumFin≃Fin _ =
  isoToEquiv (iso SumFin→Fin Fin→SumFin Fin→SumFin→Fin SumFin→Fin→SumFin)

SumFin≡Fin : ∀ k → Fin k ≡ Fin.Fin k
SumFin≡Fin k = ua (SumFin≃Fin k)

-- Closure properties of SumFin under type constructors

private
  _⋆_ = compEquiv

infixr 30 _⋆_

SumFin⊎≃ : (m n : ℕ) → (Fin m ⊎ Fin n) ≃ (Fin (m + n))
SumFin⊎≃ 0 n = ⊎-swap-≃ ⋆ ⊎-⊥-≃
SumFin⊎≃ (suc m) n = ⊎-assoc-≃ ⋆ ⊎-equiv (idEquiv ⊤) (SumFin⊎≃ m n)

SumFinΣ≃ : (n : ℕ)(f : Fin n → ℕ) → (Σ (Fin n) (λ x → Fin (f x))) ≃ (Fin (totalSum f))
SumFinΣ≃ 0 f = ΣEmpty _
SumFinΣ≃ (suc n) f =
    Σ⊎≃
  ⋆ ⊎-equiv (ΣUnit (λ tt → Fin (f (inl tt)))) (SumFinΣ≃ n (λ x → f (inr x)))
  ⋆ SumFin⊎≃ (f (inl tt)) (totalSum (λ x → f (inr x)))

SumFin×≃ : (m n : ℕ) → (Fin m × Fin n) ≃ (Fin (m · n))
SumFin×≃ m n = SumFinΣ≃ m (λ _ → n) ⋆ pathToEquiv (λ i → Fin (totalSumConst {m = m} n i))

SumFinΠ≃ : (n : ℕ)(f : Fin n → ℕ) → ((x : Fin n) → Fin (f x)) ≃ (Fin (totalProd f))
SumFinΠ≃ 0 f = isContr→≃Unit (isContrΠ⊥) ⋆ invEquiv (⊎-⊥-≃)
SumFinΠ≃ (suc n) f =
    Π⊎≃
  ⋆ Σ-cong-equiv (ΠUnit (λ tt → Fin (f (inl tt)))) (λ _ → SumFinΠ≃ n (λ x → f (inr x)))
  ⋆ SumFin×≃ (f (inl tt)) (totalProd (λ x → f (inr x)))

isNotZero : ℕ → ℕ
isNotZero 0 = 0
isNotZero (suc n) = 1

SumFin∥∥≃ : (n : ℕ) → ∥ Fin n ∥ ≃ Fin (isNotZero n)
SumFin∥∥≃ 0 = propTruncIdempotent≃ (isProp⊥)
SumFin∥∥≃ (suc n) =
    isContr→≃Unit (inhProp→isContr ∣ inl tt ∣ isPropPropTrunc)
  ⋆ isContr→≃Unit (isContrUnit) ⋆ invEquiv (⊎-⊥-≃)

max_stars_repo_name: FernandoLarrain/cubical


text:
module Basic.Compiler.Code where

open import Basic.AST
open import Basic.BigStep
open import Utils.Decidable
open import Utils.Monoid

open import Data.Fin using (Fin; #_)
open import Data.Vec hiding (_∷ʳ_; _++_; [_])
open import Data.Nat
open import Data.Bool renaming (not to notBool; if_then_else_ to ifBool_then_else)
open import Data.List hiding ([_])
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Product
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Empty
open import Algebra
import Level as L
private
  module LM {a A} = Algebra.Monoid (Data.List.monoid {a} A)

{-
Chapter 3.1 and 3.2.

Semantics of an abstract machine and specification of the translation from
While syntax to the abstract machine syntax.
-}

{-
Definition of the stack and the AM

We follow the book closely here.

"nat-inj" and "bool-inj" just establish injectivity of context entry
constructors.

That we have to prove them is something of a limitation of the current Agda.
In contrast, Coq derives injectivity of constructors automatically.
-}

data StackEntry : Set where
  nat  : ℕ → StackEntry
  bool : Bool → StackEntry

nat-inj : ∀ {n m} → (StackEntry ∋ nat n) ≡ nat m → n ≡ m
nat-inj refl = refl

bool-inj : ∀ {b b'} → (StackEntry ∋ bool b) ≡ bool b' → b ≡ b'
bool-inj refl = refl

Stack : Set
Stack = List StackEntry

mutual
  data Inst (n : ℕ) : Set where
    PUSH : ℕ → Inst n
    FETCH STORE : Fin n → Inst n
    ADD MUL SUB TRUE FALSE EQ LTE LT AND NOT NOOP : Inst n
    BRANCH LOOP : Code n → Code n → Inst n

  Code : ℕ → Set
  Code = List ∘ Inst

-- Semantics
------------------------------------------------------------

data ⟨_,_,_⟩▷⟨_,_,_⟩ {n} : Code n → Stack → State n → Code n → Stack → State n → Set where

  PUSH :
                    ∀ n {c e s}
    → --------------------------------------------
      ⟨ PUSH n ∷ c , e , s ⟩▷⟨ c , nat n ∷ e , s ⟩

  ADD :
                              ∀ a b {c e s}
    → ---------------------------------------------------------------
      ⟨ ADD ∷ c , nat a ∷ nat b ∷ e , s ⟩▷⟨ c , nat (a + b) ∷ e , s ⟩

  MUL :
                              ∀ a b {c e s}
    → ----------------------------------------------------------------
      ⟨ MUL ∷ c , nat a ∷ nat b ∷ e , s ⟩▷⟨ c , nat (a * b) ∷ e , s ⟩

  SUB :
                              ∀ a b {c e s}
    → ----------------------------------------------------------------
      ⟨ SUB ∷ c , nat a ∷ nat b ∷ e , s ⟩▷⟨ c , nat (a ∸ b) ∷ e , s ⟩

  TRUE :
                         ∀ {c e s}
    → -----------------------------------------------
      ⟨ TRUE ∷ c , e , s ⟩▷⟨ c , bool true ∷ e , s ⟩

  FALSE :
                         ∀ {c e s}
    → ------------------------------------------------
      ⟨ FALSE ∷ c , e , s ⟩▷⟨ c , bool false ∷ e , s ⟩

  EQ :
                               ∀ a b {c e s}
    → -------------------------------------------------------------------
      ⟨ EQ ∷ c , nat a ∷ nat b ∷ e , s ⟩▷⟨ c , bool ⌊ a ≡⁇ b ⌋ ∷ e , s ⟩

  LT :
                               ∀ a b {c e s}
    → -------------------------------------------------------------------
      ⟨ LT ∷ c , nat a ∷ nat b ∷ e , s ⟩▷⟨ c , bool ⌊ a <⁇ b ⌋ ∷ e , s ⟩

  LTE :
                               ∀ a b {c e s}
    → --------------------------------------------------------------------
      ⟨ LTE ∷ c , nat a ∷ nat b ∷ e , s ⟩▷⟨ c , bool ⌊ a ≤⁇ b ⌋ ∷ e , s ⟩

  AND :
                               ∀ a b {c e s}
    → -------------------------------------------------------------------
      ⟨ AND ∷ c , bool a ∷ bool b ∷ e , s ⟩▷⟨ c , bool (a ∧ b) ∷ e , s ⟩

  NOT :
                             ∀ b {c e s}
    → -----------------------------------------------------------
      ⟨ NOT ∷ c , bool b ∷ e , s ⟩▷⟨ c , bool (notBool b) ∷ e , s ⟩

  FETCH :
                             ∀ x {c e s}
    → ---------------------------------------------------------
      ⟨ FETCH x ∷ c , e , s ⟩▷⟨ c , nat (lookup x s) ∷ e , s ⟩

  STORE :
                         ∀ x {n c e s}
    → ------------------------------------------------------
      ⟨ STORE x ∷ c , nat n ∷ e , s ⟩▷⟨ c , e , s [ x ]≔ n ⟩

  BRANCH :
       ∀ {c₁ c₂ c t e s} → let c' = (ifBool t then c₁ else c₂) <> c in
      --------------------------------------------------------------
          ⟨ BRANCH c₁ c₂ ∷ c , bool t ∷ e , s ⟩▷⟨ c' , e , s ⟩

  NOOP :
                   ∀ {c e s}
    → ------------------------------------
       ⟨ NOOP ∷ c , e , s ⟩▷⟨ c , e , s ⟩

  LOOP :
        ∀ {c₁ c₂ c e s} → let c' = c₁ <> BRANCH (c₂ ∷ʳ LOOP c₁ c₂ ) (NOOP ∷ []) ∷ c in
      -----------------------------------------------------------------------------------
                     ⟨ LOOP c₁ c₂ ∷ c , e , s ⟩▷⟨ c' , e , s ⟩

-- Computation sequences
------------------------------------------------------------

infixr 5 _∷_
data ⟨_,_,_⟩▷*⟨_,_,_⟩ {n} : Code n → Stack → State n → Code n → Stack → State n → Set where

  done :
                 ∀ {e s}
    → ---------------------------------
      ⟨ [] , e , s ⟩▷*⟨ [] , e , s ⟩

  {- We define "being stuck" explicitly as a configuration from which no transitions exist -}
  stuck :
       ∀ {c cs e s} → (∀ c' e' s' → ¬ ⟨ c ∷ cs , e , s ⟩▷⟨ c' , e' , s' ⟩)
    → ------------------------------------------------------------
                   ⟨ c ∷ cs , e , s ⟩▷*⟨ c ∷ cs , e , s ⟩

  _∷_ :
                          ∀ {c e s c' e' s' c'' e'' s''} →
       ⟨ c , e , s ⟩▷⟨ c' , e' , s' ⟩ → ⟨ c' , e' , s' ⟩▷*⟨ c'' , e'' , s'' ⟩
    → ------------------------------------------------------------------------
                      ⟨ c , e , s ⟩▷*⟨ c'' , e'' , s'' ⟩

{- We will need the length of computation sequences for the compiler correctness proof -}
▷*-length : ∀ {n}{c c' e e'}{s s' : State n} → ⟨ c , e , s ⟩▷*⟨ c' , e' , s' ⟩ → ℕ
▷*-length done      = 0
▷*-length (stuck x) = 0
▷*-length (x ∷ p)   = suc (▷*-length p)

-- Determinism (exercise 3.6)
------------------------------------------------------------

▷-deterministic :
  ∀ {n}{c c' c'' e e' e''}{s s' s'' : State n}
  → ⟨ c , e , s ⟩▷⟨ c' , e' , s' ⟩ → ⟨ c , e , s ⟩▷⟨ c'' , e'' , s'' ⟩
  → (c' ≡ c'') × (e' ≡ e'') × (s' ≡ s'')
▷-deterministic (PUSH n₁) (PUSH .n₁)  = refl , refl , refl
▷-deterministic (ADD a b) (ADD .a .b) = refl , refl , refl
▷-deterministic (MUL a b) (MUL .a .b) = refl , refl , refl
▷-deterministic (SUB a b) (SUB .a .b) = refl , refl , refl
▷-deterministic TRUE      TRUE        = refl , refl , refl
▷-deterministic FALSE     FALSE       = refl , refl , refl
▷-deterministic (EQ a b)  (EQ .a .b)  = refl , refl , refl
▷-deterministic (LT a b)  (LT .a .b)  = refl , refl , refl
▷-deterministic (LTE a b) (LTE .a .b) = refl , refl , refl
▷-deterministic (AND a b) (AND .a .b) = refl , refl , refl
▷-deterministic (NOT b)   (NOT .b)    = refl , refl , refl
▷-deterministic (FETCH x) (FETCH .x)  = refl , refl , refl
▷-deterministic (STORE x) (STORE .x)  = refl , refl , refl
▷-deterministic BRANCH    BRANCH      = refl , refl , refl
▷-deterministic NOOP      NOOP        = refl , refl , refl
▷-deterministic LOOP      LOOP        = refl , refl , refl

▷*-deterministic :
  ∀ {n}{c c' c'' e e' e''}{s s' s'' : State n}
  → ⟨ c , e , s ⟩▷*⟨ c' , e' , s' ⟩ → ⟨ c , e , s ⟩▷*⟨ c'' , e'' , s'' ⟩
  → (c' ≡ c'') × (e' ≡ e'') × (s' ≡ s'')
▷*-deterministic done done = refl , refl , refl
▷*-deterministic done (() ∷ p2)
▷*-deterministic (stuck x) (stuck x₁) = refl , refl , refl
▷*-deterministic (stuck x) (x₁ ∷ p2) = ⊥-elim (x _ _ _ x₁)
▷*-deterministic (() ∷ p1) done
▷*-deterministic (x ∷ p1) (stuck x₁) = ⊥-elim (x₁ _ _ _ x)
▷*-deterministic (x ∷ p1) (x₁ ∷ p2) with ▷-deterministic x x₁
... | eq1 , eq2 , eq3 rewrite eq1 | eq2 | eq3 = ▷*-deterministic p1 p2

-- Compilation (chapter 3.2)
------------------------------------------------------------

𝓒⟦_⟧ᵉ : ∀ {n t} → Exp n t → Code n
𝓒⟦ lit x       ⟧ᵉ = PUSH x ∷ []
𝓒⟦ add a b     ⟧ᵉ = 𝓒⟦ b ⟧ᵉ <> 𝓒⟦ a ⟧ᵉ ∷ʳ ADD
𝓒⟦ mul a b     ⟧ᵉ = 𝓒⟦ b ⟧ᵉ <> 𝓒⟦ a ⟧ᵉ ∷ʳ MUL
𝓒⟦ sub a b     ⟧ᵉ = 𝓒⟦ b ⟧ᵉ <> 𝓒⟦ a ⟧ᵉ ∷ʳ SUB
𝓒⟦ var x       ⟧ᵉ = FETCH x ∷ []
𝓒⟦ tt          ⟧ᵉ = TRUE ∷ []
𝓒⟦ ff          ⟧ᵉ = FALSE ∷ []
𝓒⟦ eq  a b     ⟧ᵉ = 𝓒⟦ b ⟧ᵉ <> 𝓒⟦ a ⟧ᵉ ∷ʳ EQ
𝓒⟦ lte a b     ⟧ᵉ = 𝓒⟦ b ⟧ᵉ <> 𝓒⟦ a ⟧ᵉ ∷ʳ LTE
𝓒⟦ lt  a b     ⟧ᵉ = 𝓒⟦ b ⟧ᵉ <> 𝓒⟦ a ⟧ᵉ ∷ʳ LT
𝓒⟦ Exp.and a b ⟧ᵉ = 𝓒⟦ b ⟧ᵉ <> 𝓒⟦ a ⟧ᵉ ∷ʳ AND
𝓒⟦ not e       ⟧ᵉ = 𝓒⟦ e ⟧ᵉ ∷ʳ NOT

𝓒⟦_⟧ˢ : ∀ {n} → St n → Code n
𝓒⟦ x := e                 ⟧ˢ = 𝓒⟦ e ⟧ᵉ ∷ʳ STORE x
𝓒⟦ skip                   ⟧ˢ = NOOP ∷ []
𝓒⟦ s₁ , s₂                ⟧ˢ = 𝓒⟦ s₁ ⟧ˢ <> 𝓒⟦ s₂ ⟧ˢ
𝓒⟦ if b then st₁ else st₂ ⟧ˢ = 𝓒⟦ b ⟧ᵉ ∷ʳ BRANCH 𝓒⟦ st₁ ⟧ˢ 𝓒⟦ st₂ ⟧ˢ
𝓒⟦ while b do st          ⟧ˢ = LOOP 𝓒⟦ b ⟧ᵉ 𝓒⟦ st ⟧ˢ ∷ []

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

{-
Some additional lemmas needed to the compiler correctness proofs.
-}

{- A weaker variant of exercise 3.4 -}
weaken-step-code :
  ∀ {n}{c c' c'' e e'}{s s' : State n}
  → ⟨ c        , e , s ⟩▷⟨ c'        , e' , s' ⟩
  → ⟨ c <> c'' , e , s ⟩▷⟨ c' <> c'' , e' , s' ⟩
weaken-step-code (PUSH n₁) = PUSH n₁
weaken-step-code (ADD a b) = ADD a b
weaken-step-code (MUL a b) = MUL a b
weaken-step-code (SUB a b) = SUB a b
weaken-step-code TRUE      = TRUE
weaken-step-code FALSE     = FALSE
weaken-step-code (EQ a b)  = EQ a b
weaken-step-code (LT a b)  = LT a b
weaken-step-code (LTE a b) = LTE a b
weaken-step-code (AND a b) = AND a b
weaken-step-code (NOT b)   = NOT b
weaken-step-code (FETCH x) = FETCH x
weaken-step-code (STORE x) = STORE x
weaken-step-code {c'' = c''}(BRANCH {c₁}{c₂}{c}{t})
  rewrite LM.assoc (ifBool t then c₁ else c₂) c c'' = BRANCH
weaken-step-code {c'' = c''}(LOOP {c₁}{c₂}{c})
  rewrite LM.assoc c₁ (BRANCH (c₂ ∷ʳ LOOP c₁ c₂) (NOOP ∷ []) ∷ c) c'' = LOOP
weaken-step-code NOOP = NOOP

{-
This lemma is not in the book, but it's very convenient to use in the following
proofs. It's just the analogue of Basic.SmallStep.append for the computation
sequences here.
-}
infixr 5 _▷*<>_
_▷*<>_ :
  ∀ {n c c' e e' e''}{s s' s'' : State n}
  → ⟨ c       , e  , s  ⟩▷*⟨ [] , e'  , s'  ⟩
  → ⟨ c'      , e' , s' ⟩▷*⟨ [] , e'' , s'' ⟩
  → ⟨ c <> c' , e  , s  ⟩▷*⟨ [] , e'' , s'' ⟩
_▷*<>_ done        p2 = p2
_▷*<>_ (step ∷ p1) p2 = weaken-step-code step ∷ p1 ▷*<> p2

{- Lemma 3.18 -}
𝓒-Exp-nat :
  ∀ {n e}{s : State n} exp -> ⟨ 𝓒⟦ exp ⟧ᵉ , e , s ⟩▷*⟨ [] , nat (⟦ exp ⟧ᵉ s) ∷ e , s ⟩
𝓒-Exp-nat (lit x)   = PUSH x ∷ done
𝓒-Exp-nat (add a b) = (𝓒-Exp-nat b ▷*<> 𝓒-Exp-nat a) ▷*<> (ADD _ _ ∷ done)
𝓒-Exp-nat (mul a b) = (𝓒-Exp-nat b ▷*<> 𝓒-Exp-nat a) ▷*<> (MUL _ _ ∷ done)
𝓒-Exp-nat (sub a b) = (𝓒-Exp-nat b ▷*<> 𝓒-Exp-nat a) ▷*<> (SUB _ _ ∷ done)
𝓒-Exp-nat (var x)   = FETCH x ∷ done

{- Lemma 3.19 -}
𝓒-Exp-bool :
  ∀ {n e}{s : State n} exp -> ⟨ 𝓒⟦ exp ⟧ᵉ , e , s ⟩▷*⟨ [] , bool (⟦ exp ⟧ᵉ s) ∷ e , s ⟩
𝓒-Exp-bool tt            = TRUE ∷ done
𝓒-Exp-bool ff            = FALSE ∷ done
𝓒-Exp-bool (eq a b)      = (𝓒-Exp-nat  b ▷*<> 𝓒-Exp-nat a) ▷*<> EQ  _ _ ∷ done
𝓒-Exp-bool (lte a b)     = (𝓒-Exp-nat  b ▷*<> 𝓒-Exp-nat a) ▷*<> LTE _ _ ∷ done
𝓒-Exp-bool (lt a b)      = (𝓒-Exp-nat  b ▷*<> 𝓒-Exp-nat a) ▷*<> LT  _ _ ∷ done
𝓒-Exp-bool (Exp.and a b) = (𝓒-Exp-bool b ▷*<> 𝓒-Exp-bool a) ▷*<> AND _ _ ∷ done
𝓒-Exp-bool (not e)       = 𝓒-Exp-bool  e ▷*<> NOT _ ∷ done

{-
A "smart constructor" that gets rid of the trailing (++[]) at the end of the branch.
This is not mentioned in the book, because it (rightfully) assumes that appendding an
empty list to the end of a list results in the same list, while here we have to make
this property explicit
-}

BRANCH-[] :
  ∀ {n c₁ c₂ e t}{s : State n} → let c' = ifBool t then c₁ else c₂ in
  ⟨ BRANCH c₁ c₂ ∷ [] , bool t ∷ e , s ⟩▷⟨ c' , e , s ⟩
BRANCH-[] {n}{c₁}{c₂}{e}{t}{s} =
  subst
    (λ b → ⟨ BRANCH c₁ c₂ ∷ [] , bool t ∷ e , s ⟩▷⟨ b , e , s ⟩)
    (proj₂ LM.identity (ifBool t then c₁ else c₂))
    BRANCH

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
module ListNat where
  data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

  data List (a : Set) : Set where
    []   : List a
    _::_ : a -> List a -> List a

  infixr 30 _::_

  [1,0,2] = one :: zero :: succ one :: []
    where one = succ zero

max_stars_repo_name: andrejtokarcik/agda-semantics

max_issues_repo_name: andrejtokarcik/agda-semantics

max_forks_repo_name: andrejtokarcik/agda-semantics


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

module Cubical.Structures.Subtype where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.NatPlusOne
open import Cubical.Data.Nat
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' : Level

-- The type of Subtypes of a type
Subtype : {ℓ : Level} → (ℓ' : Level) → Type ℓ → Type (ℓ-max ℓ (ℓ-suc ℓ'))
Subtype ℓ' A = A → (hProp ℓ')

-- Coercion from Subtype to Type
Subtype→Type : {ℓ ℓ' : Level} {A : Type ℓ} (B : Subtype ℓ' A) → Type (ℓ-max ℓ ℓ')
Subtype→Type {A = A} B = Σ[ a ∈ A ] (fst (B a))

-- if A has Level n > 0 then so do all of its subtypes -}
subtypePreservesHLevel : {ℓ ℓ' : Level} {A : Type ℓ} {n : ℕ₊₁} (p : isOfHLevel (ℕ₊₁→ℕ n) A) (B : Subtype ℓ' A) → isOfHLevel (ℕ₊₁→ℕ n) (Subtype→Type B)
subtypePreservesHLevel {n = one} p B = isPropΣ p λ a → snd (B a)
subtypePreservesHLevel {n = 1+ (suc n)} p B = isOfHLevelΣ (suc (suc n)) p λ a → isProp→isOfHLevelSuc (suc n) (snd (B a))

-- if two terms x and y of the original type A are equal by q, and p and p' witness that x , y are in
-- the subtype then p ≡ p' over q
subtypeWitnessIrrelevance : {A : Type ℓ} (B : Subtype ℓ' A) {xp yp : Subtype→Type B} (q : fst xp ≡ fst yp) → xp ≡ yp
subtypeWitnessIrrelevance B q = Σ≡Prop (λ a → B a .snd) q

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --without-K #-}
module higher.circle.properties where

open import sum
open import equality
open import function.isomorphism
open import sets.empty
open import sets.bool
open import hott.equivalence
open import hott.univalence
open import higher.circle.core

non-simply-connected : ¬ (loop ≡ refl)
non-simply-connected loop-trivial = inv-non-trivial inv-trivial
  where
    not-iso : Bool ≅' Bool
    not-iso = iso not not H H , γ
      where
        H : (x : Bool) → not (not x) ≡ x
        H true = refl
        H false = refl

        γ : (x : Bool) → ap not (H x) ≡ H (not x)
        γ true = refl
        γ false = refl

    abstract
      not-is-equiv : weak-equiv not
      not-is-equiv = proj₂ (≅'⇒≈ not-iso)

    not-equiv : Bool ≈ Bool
    not-equiv = not , not-is-equiv

    inv : Bool ≡ Bool
    inv = ≈⇒≡ not-equiv

    inv-non-trivial : ¬ (inv ≡ refl)
    inv-non-trivial q = distinct absurd
      where
        open ≡-Reasoning

        distinct : false ≡ true → ⊥
        distinct ()

        absurd : false ≡ true
        absurd = begin
            false
          ≡⟨ refl ⟩
            not true
          ≡⟨ ap (λ g → g true)
                  (sym (uni-coherence not-equiv)) ⟩
            coerce inv true
          ≡⟨ ap (λ z → coerce z true) q ⟩
            coerce refl true
          ≡⟨ refl ⟩
            true
          ∎

    f : S¹ → Set
    f = elim Bool inv

    f' : base ≡ base → Bool ≡ Bool
    f' p = ap f p

    β₂ : f' loop ≡ inv
    β₂ = β-loop Bool inv

    inv-trivial : inv ≡ refl
    inv-trivial = begin
        inv
      ≡⟨ sym β₂ ⟩
        f' loop
      ≡⟨ ap f' loop-trivial ⟩
        refl
      ∎
      where
        open ≡-Reasoning

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- Andreas, 2015-07-13  Better parse errors for illegal type signatures

1 : Set1
1 = Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
{-# OPTIONS --without-K #-}
module Model.Quantification where

open import Model.RGraph as RG using (RGraph)
open import Model.Size as MS using (_<_ ; ⟦_⟧Δ ; ⟦_⟧n ; ⟦_⟧σ)
open import Model.Type.Core
open import Source.Size.Substitution.Theory
open import Source.Size.Substitution.Universe as SS using (Sub⊢ᵤ)
open import Util.HoTT.Equiv
open import Util.HoTT.FunctionalExtensionality
open import Util.HoTT.HLevel
open import Util.Prelude hiding (_∘_)
open import Util.Relation.Binary.PropositionalEquality using
  ( Σ-≡⁺ ; subst-sym-subst ; subst-subst-sym )

import Source.Size as SS
import Source.Type as ST

open RGraph
open RG._⇒_
open SS.Ctx
open SS.Sub⊢ᵤ

record ⟦∀⟧′ {Δ} n (T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ) (δ : Obj ⟦ Δ ⟧Δ) : Set where
  no-eta-equality
  field
    arr : ∀ m (m<n : m < ⟦ n ⟧n .fobj δ) → Obj T (δ , m , m<n)
    param : ∀ m m<n m′ m′<n → eq T _ (arr m m<n) (arr m′ m′<n)

open ⟦∀⟧′ public

⟦∀⟧′Canon : ∀ {Δ} n (T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ) (δ : Obj ⟦ Δ ⟧Δ) → Set
⟦∀⟧′Canon n T δ
  = Σ[ f ∈ (∀ m (m<n : m < ⟦ n ⟧n .fobj δ) → Obj T (δ , m , m<n)) ]
      (∀ m m<n m′ m′<n → eq T _ (f m m<n) (f m′ m′<n))

⟦∀⟧′≅⟦∀⟧′Canon : ∀ {Δ n T δ} → ⟦∀⟧′ {Δ} n T δ ≅ ⟦∀⟧′Canon n T δ
⟦∀⟧′≅⟦∀⟧′Canon = record
  { forth = λ { record { arr = x ; param = y } → x , y }
  ; isIso = record
    { back = λ x → record { arr = proj₁ x ; param = proj₂ x }
    ; back∘forth = λ { record {} → refl }
    ; forth∘back = λ _ → refl
    }
  }

abstract
  ⟦∀⟧′Canon-IsSet : ∀ {Δ n T δ} → IsSet (⟦∀⟧′Canon {Δ} n T δ)
  ⟦∀⟧′Canon-IsSet {T = T} = Σ-IsSet
    (∀-IsSet λ m → ∀-IsSet λ m<n → λ _ _ → T .Obj-IsSet _ _)
    (λ f → IsOfHLevel-suc 1 (∀-IsProp λ m → ∀-IsProp λ m<n → ∀-IsProp λ m′
      → ∀-IsProp λ m′<n → T .eq-IsProp))

  ⟦∀⟧′-IsSet : ∀ {Δ n T δ} → IsSet (⟦∀⟧′ {Δ} n T δ)
  ⟦∀⟧′-IsSet {Δ} {n} {T} {δ}
    = ≅-pres-IsOfHLevel 2 (≅-sym ⟦∀⟧′≅⟦∀⟧′Canon) (⟦∀⟧′Canon-IsSet {Δ} {n} {T} {δ})

  ⟦∀⟧′-≡⁺ : ∀ {Δ n T δ} (f g : ⟦∀⟧′ {Δ} n T δ)
    → (∀ m m<n → f .arr m m<n ≡ g .arr m m<n)
    → f ≡ g
  ⟦∀⟧′-≡⁺ {T = T} record{} record{} f≈g = ≅-Injective ⟦∀⟧′≅⟦∀⟧′Canon (Σ-≡⁺
    ( (funext λ m → funext λ m<n → f≈g m m<n)
    , funext λ m → funext λ m<n → funext λ m′ → funext λ m<n′ → T .eq-IsProp _ _))

⟦∀⟧′-resp-≈⟦Type⟧ : ∀ {Δ n T U}
  → T ≈⟦Type⟧ U
  → ∀ {δ} → ⟦∀⟧′ {Δ} n T δ ≅ ⟦∀⟧′ n U δ
⟦∀⟧′-resp-≈⟦Type⟧ T≈U = record
  { forth = λ f → record
    { arr = λ m m<n → T≈U .forth .fobj (f .arr m m<n)
    ; param = λ m m<n m′ m′<n → T≈U .forth .feq _ (f .param m m<n m′ m′<n)
    }
  ; isIso = record
    { back = λ f → record
      { arr = λ m m<n → T≈U .back .fobj (f .arr m m<n)
      ; param = λ m m<n m′ m′<n → T≈U .back .feq _ (f .param m m<n m′ m′<n)
      }
    ; back∘forth = λ x → ⟦∀⟧′-≡⁺ _ _ λ m m<n → T≈U .back-forth .≈⁻ _ _
    ; forth∘back = λ x → ⟦∀⟧′-≡⁺ _ _ λ m m<n → T≈U .forth-back .≈⁻ _ _
    }
  }

⟦∀⟧ : ∀ {Δ} n (T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ) → ⟦Type⟧ ⟦ Δ ⟧Δ
⟦∀⟧ n T = record
  { ObjHSet = λ δ → HLevel⁺ (⟦∀⟧′ n T δ) ⟦∀⟧′-IsSet
  ; eqHProp = λ _ f g → ∀-HProp _ λ m → ∀-HProp _ λ m<n → ∀-HProp _ λ m′
      → ∀-HProp _ λ m′<n → T .eqHProp _ (f .arr m m<n) (g .arr m′ m′<n)
  ; eq-refl = λ f → f .param
  }

⟦∀⟧-resp-≈⟦Type⟧ : ∀ {Δ} n {T U : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ}
  → T ≈⟦Type⟧ U
  → ⟦∀⟧ n T ≈⟦Type⟧ ⟦∀⟧ n U
⟦∀⟧-resp-≈⟦Type⟧ n T≈U = record
  { forth = record
    { fobj = ⟦∀⟧′-resp-≈⟦Type⟧ T≈U .forth
    ; feq = λ δ≈δ′ x≈y a a₁ a₂ a₃ → T≈U .forth .feq _ (x≈y a a₁ a₂ a₃)
    }
  ; back = record
    { fobj = ⟦∀⟧′-resp-≈⟦Type⟧ T≈U .back
    ; feq = λ δ≈δ′ x≈y a a₁ a₂ a₃ → T≈U .back .feq _ (x≈y a a₁ a₂ a₃)
    }
  ; back-forth = ≈⁺ λ δ x → ⟦∀⟧′-resp-≈⟦Type⟧ T≈U .back∘forth _
  ; forth-back = ≈⁺ λ δ x → ⟦∀⟧′-resp-≈⟦Type⟧ T≈U .forth∘back _
  }

absₛ : ∀ {Δ n} {Γ : ⟦Type⟧ ⟦ Δ ⟧Δ} {T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ}
  → subT ⟦ SS.Wk ⟧σ Γ ⇒ T
  → Γ ⇒ ⟦∀⟧ n T
absₛ {Δ} {n} {Γ} {T} f = record
  { fobj = λ {δ} x → record
    { arr = λ m m<n → f .fobj x
    ; param = λ m m<n m′ m′<n → f .feq _ (Γ .eq-refl x)
    }
  ; feq = λ _ x≈y m m′ m<nγ m′<nγ′ → f .feq _ x≈y
  }

appₛ : ∀ {Δ n m} {Γ : ⟦Type⟧ ⟦ Δ ⟧Δ} {T : ⟦Type⟧ ⟦ Δ ∙ n ⟧Δ}
  → (m<n : m SS.< n)
  → Γ ⇒ ⟦∀⟧ n T
  → Γ ⇒ subT ⟦ SS.Sing m<n ⟧σ T
appₛ {m = m} {T = T} m<n f = record
  { fobj = λ {δ} x → f .fobj x .arr (⟦ m ⟧n .fobj δ) (MS.⟦<⟧ m<n)
  ; feq = λ δ≈δ′ {x y} x≈y → f .feq _ x≈y _ _ _ _
  }

subT-⟦∀⟧ : ∀ {Δ Ω n σ} (⊢σ : σ ∶ Δ ⇒ᵤ Ω) (T : ⟦Type⟧ ⟦ Ω ∙ n ⟧Δ)
  → ⟦∀⟧ (n [ σ ]ᵤ)
      (subT (⟦_⟧σ {Ω = Ω ∙ n} (Lift ⊢σ refl)) T)
  ≈⟦Type⟧ subT ⟦ ⊢σ ⟧σ (⟦∀⟧ n T)
subT-⟦∀⟧ {Δ} {Ω} {n} {σ} ⊢σ T = record
  { forth = record
    { fobj = λ {γ} f → record
      { arr = λ m m<n
          → transportObj T
              (MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl)
              (f .arr m (subst (m <_) (sym (MS.⟦sub⟧ ⊢σ n)) m<n))
      ; param = λ m m<n m′ m′<n
          → transportObj-resp-eq T _ _ (f .param _ _ _ _)
      }
    ; feq = λ γ≈γ′ f≈g a a₁ a₂ a₃ → transportObj-resp-eq T _ _ (f≈g _ _ _ _)
    }
  ; back = record
    { fobj = λ {γ} f → record
      { arr = λ m m<n
          → transportObj T
              (MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl)
              (f .arr m (subst (m <_) (MS.⟦sub⟧ ⊢σ n) m<n))
      ; param = λ m m<n m′ m′<n
          → transportObj-resp-eq T _ _ (f .param _ _ _ _)
      }
    ; feq = λ γ≈γ′ f≈g a a₁ a₂ a₃ → transportObj-resp-eq T _ _ (f≈g _ _ _ _)
    }
  ; back-forth = ≈⁺ λ γ f → ⟦∀⟧′-≡⁺ _ _ λ m m<n
      → trans
          (transportObj∘transportObj T
            (MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl)
            (MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl))
          (trans
            (cong
              (λ p → transportObj T
                (trans
                  (MS.⟦Δ∙n⟧-≡⁺ Ω n
                    (subst (m <_) (MS.⟦sub⟧ ⊢σ n) p)
                    (subst (m <_) (MS.⟦sub⟧ ⊢σ n) m<n)
                    refl refl)
                  (MS.⟦Δ∙n⟧-≡⁺ Ω n
                    (subst (m <_) (MS.⟦sub⟧ ⊢σ n) m<n)
                    (subst (m <_) (MS.⟦sub⟧ ⊢σ n) m<n)
                    refl refl))
                (f .arr m p))
              (subst-sym-subst (MS.⟦sub⟧ ⊢σ n)))
            (transportObj-refl T _))
  ; forth-back = ≈⁺ λ γ f → ⟦∀⟧′-≡⁺ _ _ λ m m<n
      → trans
          (transportObj∘transportObj T
            (MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl)
            (MS.⟦Δ∙n⟧-≡⁺ Ω n _ _ refl refl))
          (trans
            (cong
              (λ p → transportObj T
                (trans
                  (MS.⟦Δ∙n⟧-≡⁺ Ω n p p refl refl)
                  (MS.⟦Δ∙n⟧-≡⁺ Ω n p m<n refl refl))
                (f .arr m p))
              (subst-subst-sym (MS.⟦sub⟧ ⊢σ n)))
            (transportObj-refl T _))
  }

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
module Tactic.Nat.Subtract.Refute where

open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.Quote
open import Tactic.Reflection.Substitute
open import Tactic.Reflection
open import Control.Monad.State

open import Tactic.Nat.Reflect
open import Tactic.Nat.NF
open import Tactic.Nat.Exp
open import Tactic.Nat.Auto
open import Tactic.Nat.Auto.Lemmas
open import Tactic.Nat.Simpl.Lemmas
open import Tactic.Nat.Simpl
open import Tactic.Nat.Reflect

open import Tactic.Nat.Subtract.Exp
open import Tactic.Nat.Subtract.Reflect
open import Tactic.Nat.Subtract.Lemmas
open import Tactic.Nat.Less.Lemmas

data Impossible : Set where

invalidEquation : ⊤
invalidEquation = _

private
  0≠suc : ∀ n → 0 ≡ Nat.suc n → ⊥
  0≠suc n ()

  n≮0 : {n : Nat} → n < 0 → ⊥
  n≮0 (diff k ())

  lem-refute : ∀ n nf ρ → 0 ≡ ⟦ (suc n , []) ∷ nf ⟧ns (atomEnvS ρ) → ⊥
  lem-refute n nf ρ eq = erase-⊥ $ 0≠suc (n + ⟦ nf ⟧n (atomEnvS ρ)) $
    eq ⟨≡⟩ ns-sound ((suc n , []) ∷ nf) (atomEnvS ρ) ⟨≡⟩ auto

refutation-proof : ∀ {a} {A : Set a} eqn ρ → Maybe (⟦ eqn ⟧eqn ρ → A)
refutation-proof (a :≡ b) ρ with cancel (normSub a) (normSub b) | complicateSubEq a b ρ
refutation-proof (a :≡ b) ρ | [] , (suc n , []) ∷ v | compl = just λ eq → ⊥-elim $ lem-refute n v ρ (compl eq)
refutation-proof (a :≡ b) ρ | (suc n , []) ∷ v , [] | compl = just λ eq → ⊥-elim $ lem-refute n v ρ (sym (compl eq))
refutation-proof (a :≡ b) ρ | _ , _ | _ = nothing

refutation-proof (a :< b) ρ with cancel (normSub a) (normSub b) | complicateSubLess a b ρ
refutation-proof (a :< b) ρ | v , [] | compl = just λ eq → ⊥-elim $ erase-⊥ $ n≮0 (compl eq)
refutation-proof (a :< b) ρ | _ , _  | _     = nothing

-- Some trickery to make tactics call be erased
get-absurd-proof : ∀ {a} {A : Set a} (prf : Maybe (A → ⊥)) → QED {x = prf} → A → ⊥
get-absurd-proof = get-proof

get-refute-proof : ∀ {a b} {A : Set a} {B : Set b} (prf : Maybe (A → ⊥)) → QED {x = prf} → A → B
get-refute-proof eq x y = ⊥-elim (get-absurd-proof eq x y)
{-# INLINE get-refute-proof #-}

refutesub-tactic : Term → TC Term
refutesub-tactic prf =
  inferNormalisedType prf >>= λ a →
  caseM termToSubEqn a of λ
  { nothing → pure $ failedProof (quote invalidEquation) a
  ; (just (eqn , Γ)) → pure $
    applyTerm (safe
      (getProof (quote cantProve) a $
        def (quote refutation-proof)
            $ vArg (` eqn)
            ∷ vArg (quotedEnv Γ)
            ∷ []) _) (vArg prf ∷ [])
  }

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --allow-unsolved-metas #-}

module simple where

module Nat where

  data Nat : Set where
    zero : Nat
    suc  : Nat -> Nat

  _+_ : Nat -> Nat -> Nat
  zero  + m = m
  suc n + m = suc (n + m)

module N = Nat

z  = N._+_ (N.suc N.zero) (N.suc N.zero)
zz = Nat._+_ (Nat.suc Nat.zero) (Nat.suc Nat.zero)

module List (A : Set) where

  infixr 15 _::_ _++_

  data List : Set where
    nil  : List
    _::_ : A -> List -> List

  _++_ : List -> List -> List
  nil       ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

module TestList where

  open Nat
  module ListNat = List Nat
  open ListNat using (_++_; _::_; nil)

  zzz = (zero :: nil) ++ (suc zero :: nil)

module EvenOdd where

  mutual
    data Even : Set where
      evenZero : Even
      evenSuc  : Odd -> Even

    data Odd : Set where
      oddSuc : Even -> Odd

module Monad where

  data Monad (m : Set -> Set) : Set1 where
    monad : ({a : Set} -> a -> m a) ->
            ({a b : Set} -> m a -> (a -> m b) -> m b) ->
            Monad m

  return : {m : Set -> Set} -> {a : Set} -> Monad m -> a -> m a
  return (monad ret _) x = ret x

module Stack where

  abstract
    data Stack (A : Set) : Set where
      snil : Stack A
      scons : A -> Stack A -> Stack A

  module Ops where

    abstract
      empty : {A : Set} -> Stack A
      empty = snil

      push : {A : Set} -> A -> Stack A -> Stack A
      push x s = scons x s

    unit : {A : Set} -> A -> Stack A
    unit x = push x empty

module TestStack where

  open Stack using (Stack)
  open Stack.Ops
  open Nat

  zzzz : Stack Nat
  zzzz = push zero (unit (suc zero))

module TestIdentity where

  postulate
    A   : Set
    idA : A -> A
    F   : Set -> Set
    H   : (A B : Set) -> Set
    id0 : (A : Set) -> A -> A
    idH : {A : Set} -> A -> A
    fa  : F A
    a   : A

  test1 = id0 (F A) fa
  test2 = idH fa
  test3 = id0 _ fa
  test4 = idH {! foo bar !}
  -- test5 = id id      -- we can't do this (on purpose)!

  id = \{A : Set}(x : A) -> x
  test = id a

module prop where

  postulate
    _\/_  : Set -> Set -> Set
    inl   : {P Q : Set} -> P -> P \/ Q
    inr   : {P Q : Set} -> Q -> P \/ Q
    orE   : {P Q R : Set} -> P \/ Q -> (P -> R) -> (Q -> R) -> R
    False : Set
    _==>_ : Set -> Set -> Set
    impI  : {P Q : Set} -> (P -> Q) -> P ==> Q
    impE  : {P Q : Set} -> P ==> Q -> P -> Q

  Not = \(P : Set) -> P ==> False

  notnotEM = \(P : Set) ->
    impI (\ (nEM : Not (P \/ Not P)) ->
            impE nEM (
                inr (
                  impI (\ p ->
                    impE nEM (inl p)
                  )
                )
              )
            )

module Tests where

  infix 5 _==_
  postulate
    _==_ : {A : Set} -> A -> A -> Set
    refl : {A : Set} -> {x : A} -> x == x

  open TestList.ListNat
  open Nat

  test1 : TestList.zzz == zero :: suc zero :: nil
  test1 = refl

max_forks_repo_name: Agda-zh/agda


text:
module Numeral.Natural.LinearSearch where

open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.List
import      Data.List.Functions as List
open import Data.List.Relation.Membership using (_∈_)
open import Data.List.Relation.Membership.Proofs
open import Data.List.Relation.Quantification
open import Data.List.Relation.Quantification.Proofs
open import Data.List.Sorting
open import Functional
open import Logic.Propositional
open import Numeral.Finite
import      Numeral.Finite.LinearSearch as 𝕟
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Relation.Order
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Function

private variable a b n i j : ℕ
private variable f : ℕ → Bool

{-
findBoundedMin : ℕ → ℕ → (ℕ → Bool) → Option(ℕ)
findBoundedMin a b f = Option.map 𝕟-to-ℕ (𝕟.findMin{b −₀ a}(f ∘ (_+ a) ∘ 𝕟-to-ℕ))

findBoundedMin-None-correctness : (a < b) → (findBoundedMin a b f ≡ None) ↔ (∀{i} → (a ≤ i) → (i < b) → IsFalse(f(i)))
findBoundedMin-None-correctness{a}{b}{f} ab
  with [↔]-intro l r ← 𝕟.findMin-None-correctness{b −₀ a}{f ∘ (_+ a) ∘ 𝕟-to-ℕ}
  = [↔]-intro (\p → congruence₁(Option.map 𝕟-to-ℕ) (l (\{i} → p ([≤]-of-[+]ᵣ {𝕟-to-ℕ i}) {![<]-with-[+]-weak ([∨]-introₗ ([∧]-intro ? ?))!}))) (\p{i} ai ib → {!r ? {?}!})
-}

findBoundedAll : ℕ → ℕ → (ℕ → Bool) → List(ℕ)
findBoundedAll a b f = List.map ((_+ a) ∘ 𝕟-to-ℕ) (𝕟.findAll{b −₀ a} (f ∘ (_+ a) ∘ 𝕟-to-ℕ))

findBoundedAll-correctness : AllElements(IsTrue ∘ f)(findBoundedAll a b f)
findBoundedAll-correctness {f} {a} {b} with 𝕟.findAll{b −₀ a} (f ∘ (_+ a) ∘ 𝕟-to-ℕ) | 𝕟.findAll-correctness{b −₀ a}{f ∘ (_+ a) ∘ 𝕟-to-ℕ}
... | ∅     | ∅      = ∅
... | _ ⊰ _ | p ⊰ ps = p ⊰ AllElements-mapᵣ ((_+ a) ∘ 𝕟-to-ℕ) id ps

postulate findBoundedAll-completeness : IsTrue(f(i)) → (a ≤ i) → (i < b) → (i ∈ findBoundedAll a b f)
-- findBoundedAll-completeness {f}{i}{a}{b} ai ib fi = {![∈]-map {f = 𝕟-to-ℕ} (𝕟.findAll-completeness{b −₀ a}{f ∘ (_+ a) ∘ 𝕟-to-ℕ}{ℕ-to-𝕟 (i −₀ a) ⦃ ? ⦄} ?)!}

postulate findBoundedAll-emptyness : (∀{i} → (a ≤ i) → (i < b) → IsFalse(f(i))) ↔ (findBoundedAll a b f ≡ ∅)

postulate findBoundedAll-sorted : Sorted(_≤?_)(findBoundedAll a b f)

postulate findBoundedAll-membership : (i ∈ findBoundedAll a b f) ↔ ((a ≤ i) ∧ (i < b) ∧ IsTrue(f(i)))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --allow-unsolved-metas #-}

record R : Set₁ where
  field
    A : Set
    f : A → A

record Double {a} (A : Set a) : Set a where
  field
    double : A → A

open Double {{...}}

-- Type error (incomplete patterns in Patterns.Match)
doubleR : Double R
R.A (double {{doubleR}} x)   = R.A x
R.f (double {{doubleR}} x) z = R.f x (R.f x z)

-- Internal error (incomplete patterns in Reduce.Fast)
doubleR₁ : Double R
R.A (double {{doubleR₁}} x)   = R.A x
R.f (double {{doubleR₁}} x) z = {!R.f x (R.f x z)!}


text:
{-

This files contains:
- Facts about constructions on finite sets, especially when they preserve finiteness.

-}
{-# OPTIONS --safe #-}

module Cubical.Data.FinSet.Constructors where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)
open import Cubical.Foundations.Univalence

open import Cubical.HITs.PropositionalTruncation as Prop

open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

open import Cubical.Data.Fin.LehmerCode as LehmerCode
open import Cubical.Data.SumFin
open import Cubical.Data.FinSet.Base
open import Cubical.Data.FinSet.Properties
open import Cubical.Data.FinSet.FiniteChoice

open import Cubical.Relation.Nullary

open import Cubical.Functions.Fibration
open import Cubical.Functions.Embedding
open import Cubical.Functions.Surjection

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

module _
  (X : Type ℓ)(p : isFinOrd X) where

  isFinOrd∥∥ : isFinOrd ∥ X ∥
  isFinOrd∥∥ = _ , propTrunc≃ (p .snd) ⋆ SumFin∥∥≃ _

  isFinOrd≃ : isFinOrd (X ≃ X)
  isFinOrd≃ = _ , equivComp (p .snd) (p .snd) ⋆ SumFin≃≃ _

module _
  (X : Type ℓ )(p : isFinOrd X)
  (Y : Type ℓ')(q : isFinOrd Y) where

  isFinOrd⊎ : isFinOrd (X ⊎ Y)
  isFinOrd⊎ = _ , ⊎-equiv (p .snd) (q .snd) ⋆ SumFin⊎≃ _ _

  isFinOrd× : isFinOrd (X × Y)
  isFinOrd× = _ , Σ-cong-equiv (p .snd) (λ _ → q .snd) ⋆ SumFin×≃ _ _

module _
  (X : Type ℓ )(p : isFinOrd X)
  (Y : X → Type ℓ')(q : (x : X) → isFinOrd (Y x)) where

  private
    e = p .snd

    f : (x : X) → ℕ
    f x = q x .fst

  isFinOrdΣ : isFinOrd (Σ X Y)
  isFinOrdΣ = _ ,
      Σ-cong-equiv {B' = λ x → Y (invEq e x)} e (transpFamily p)
    ⋆ Σ-cong-equiv-snd (λ x → q (invEq e x) .snd)
    ⋆ SumFinΣ≃ _ _

  isFinOrdΠ : isFinOrd ((x : X) → Y x)
  isFinOrdΠ = _ ,
      equivΠ {B' = λ x → Y (invEq e x)} e (transpFamily p)
    ⋆ equivΠCod (λ x → q (invEq e x) .snd)
    ⋆ SumFinΠ≃ _ _

-- closedness under several type constructors

module _
  (X : FinSet ℓ)
  (Y : X .fst → FinSet ℓ') where

  isFinSetΣ : isFinSet (Σ (X .fst) (λ x → Y x .fst))
  isFinSetΣ = rec2 isPropIsFinSet
    (λ p q → isFinOrd→isFinSet (isFinOrdΣ (X .fst) (_ , p) (λ x → Y x .fst) q))
    (X .snd .snd) (choice X (λ x → isFinOrd (Y x .fst)) (λ x → isFinSet→isFinSet' (Y x .snd)))

  isFinSetΠ : isFinSet ((x : X .fst) → Y x .fst)
  isFinSetΠ = rec2 isPropIsFinSet
    (λ p q → isFinOrd→isFinSet (isFinOrdΠ (X .fst) (_ , p) (λ x → Y x .fst) q))
    (X .snd .snd) (choice X (λ x → isFinOrd (Y x .fst)) (λ x → isFinSet→isFinSet' (Y x .snd)))

module _
  (X : FinSet ℓ)
  (Y : X .fst → FinSet ℓ')
  (Z : (x : X .fst) → Y x .fst → FinSet ℓ'') where

  isFinSetΠ2 : isFinSet ((x : X .fst) → (y : Y x .fst) → Z x y .fst)
  isFinSetΠ2 = isFinSetΠ X (λ x → _ , isFinSetΠ (Y x) (Z x))

module _
  (X : FinSet ℓ)
  (Y : X .fst → FinSet ℓ')
  (Z : (x : X .fst) → Y x .fst → FinSet ℓ'')
  (W : (x : X .fst) → (y : Y x .fst) → Z x y .fst → FinSet ℓ''') where

  isFinSetΠ3 : isFinSet ((x : X .fst) → (y : Y x .fst) → (z : Z x y .fst) → W x y z .fst)
  isFinSetΠ3 = isFinSetΠ X (λ x → _ , isFinSetΠ2 (Y x) (Z x) (W x))

module _
  (X : FinSet ℓ) where

  isFinSet≡ : (a b : X .fst) → isFinSet (a ≡ b)
  isFinSet≡ a b = isDecProp→isFinSet (isFinSet→isSet (X .snd) a b) (isFinSet→Discrete (X .snd) a b)

  isFinSet∥∥ : isFinSet ∥ X .fst ∥
  isFinSet∥∥ = Prop.rec isPropIsFinSet (λ p → isFinOrd→isFinSet (isFinOrd∥∥ (X .fst) (_ , p))) (X .snd .snd)

  isFinSetIsContr : isFinSet (isContr (X .fst))
  isFinSetIsContr = isFinSetΣ X (λ x → _ , (isFinSetΠ X (λ y → _ , isFinSet≡ x y)))

  isFinSetIsProp : isFinSet (isProp (X .fst))
  isFinSetIsProp = isFinSetΠ2 X (λ _ → X) (λ x x' → _ , isFinSet≡ x x')

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ')
  (f : X .fst → Y .fst) where

  isFinSetFiber : (y : Y .fst) → isFinSet (fiber f y)
  isFinSetFiber y = isFinSetΣ X (λ x → _ , isFinSet≡ Y (f x) y)

  isFinSetIsEquiv : isFinSet (isEquiv f)
  isFinSetIsEquiv =
    EquivPresIsFinSet
      (invEquiv (isEquiv≃isEquiv' f))
      (isFinSetΠ Y (λ y → _ , isFinSetIsContr (_ , isFinSetFiber y)))

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ') where

  isFinSet⊎ : isFinSet (X .fst ⊎ Y .fst)
  isFinSet⊎ = card X + card Y ,
    map2 (λ p q → isFinOrd⊎ (X .fst) (_ , p) (Y .fst) (_ , q) .snd) (X .snd .snd) (Y .snd .snd)

  isFinSet× : isFinSet (X .fst × Y .fst)
  isFinSet× = card X · card Y ,
    map2 (λ p q → isFinOrd× (X .fst) (_ , p) (Y .fst) (_ , q) .snd) (X .snd .snd) (Y .snd .snd)

  isFinSet→ : isFinSet (X .fst → Y .fst)
  isFinSet→ = isFinSetΠ X (λ _ → Y)

  isFinSet≃ : isFinSet (X .fst ≃ Y .fst)
  isFinSet≃ = isFinSetΣ (_ , isFinSet→) (λ f → _ , isFinSetIsEquiv X Y f)

module _
  (X Y : FinSet ℓ ) where

  isFinSetType≡ : isFinSet (X .fst ≡ Y .fst)
  isFinSetType≡ = EquivPresIsFinSet (invEquiv univalence) (isFinSet≃ X Y)

module _
  (X : FinSet ℓ) where

  isFinSetAut : isFinSet (X .fst ≃ X .fst)
  isFinSetAut = LehmerCode.factorial (card X) ,
    Prop.map (λ p → isFinOrd≃ (X .fst) (card X , p) .snd) (X .snd .snd)

  isFinSetTypeAut : isFinSet (X .fst ≡ X .fst)
  isFinSetTypeAut = EquivPresIsFinSet (invEquiv univalence) isFinSetAut

module _
  (X : FinSet ℓ) where

  isFinSet¬ : isFinSet (¬ (X .fst))
  isFinSet¬ = isFinSet→ X (Fin 0 , isFinSetFin)

module _
  (X : FinSet ℓ) where

  isFinSetNonEmpty : isFinSet (NonEmpty (X .fst))
  isFinSetNonEmpty = isFinSet¬ (_ , isFinSet¬ X)

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ')
  (f : X .fst → Y .fst) where

  isFinSetIsEmbedding : isFinSet (isEmbedding f)
  isFinSetIsEmbedding =
    isFinSetΠ2 X (λ _ → X)
      (λ a b → _ , isFinSetIsEquiv (_ , isFinSet≡ X a b) (_ , isFinSet≡ Y (f a) (f b)) (cong f))

  isFinSetIsSurjection : isFinSet (isSurjection f)
  isFinSetIsSurjection =
    isFinSetΠ Y (λ y → _ , isFinSet∥∥ (_ , isFinSetFiber X Y f y))

module _
  (X : FinSet ℓ )
  (Y : FinSet ℓ') where

  isFinSet↪ : isFinSet (X .fst ↪ Y .fst)
  isFinSet↪ = isFinSetΣ (_ , isFinSet→ X Y) (λ f → _ , isFinSetIsEmbedding X Y f)

  isFinSet↠ : isFinSet (X .fst ↠ Y .fst)
  isFinSet↠ = isFinSetΣ (_ , isFinSet→ X Y) (λ f → _ , isFinSetIsSurjection X Y f)

-- a criterion of being finite set

module _
  (X : Type ℓ)(Y : FinSet ℓ')
  (f : X → Y .fst)
  (h : (y : Y .fst) → isFinSet (fiber f y)) where

  isFinSetTotal : isFinSet X
  isFinSetTotal = EquivPresIsFinSet (invEquiv (totalEquiv f)) (isFinSetΣ Y (λ y → _ , h y))

-- a criterion of fibers being finite sets, more general than the previous result

module _
  (X : FinSet ℓ)
  (Y : Type ℓ')(h : Discrete Y)
  (f : X. fst → Y) where

  isFinSetFiberDisc : (y : Y) → isFinSet (fiber f y)
  isFinSetFiberDisc y = isFinSetΣ X (λ x → _ , isDecProp→isFinSet (Discrete→isSet h _ _) (h (f x) y))


text:
module Prelude.Int where

open import Prelude.Unit
open import Prelude.Empty
open import Prelude.Nat
open import Prelude.Number
open import Prelude.String
open import Prelude.Semiring
open import Prelude.Equality
open import Prelude.Equality.Inspect
open import Prelude.Equality.Unsafe using (eraseEquality)
open import Prelude.Ord
open import Prelude.Decidable
open import Prelude.Function
open import Prelude.Nat.Properties
open import Prelude.Int.Properties

open import Prelude.Int.Core public

open import Agda.Builtin.Int public

private
  subInt-cancel-r : (a b c : Int) → a - b ≡ c → c + b ≡ a
  subInt-cancel-r a b c refl =
    addInt-assoc a (negate b) b ʳ⟨≡⟩
    a +_ $≡ (addInt-commute (negate b) b ⟨≡⟩ subInt-equal b _ refl) ⟨≡⟩
    addInt-zero-r a

  lem-equal : (a b : Int) → a - b ≡ 0 → a ≡ b
  lem-equal a b eq = subInt-cancel-r a b 0 eq ʳ⟨≡⟩ addInt-zero-l b

  lem-less : (a b c : Int) → a - b ≡ c → negate c + a ≡ b
  lem-less a b c eq = subInt-cancel-r b a (negate c) (negate-subInt a b ʳ⟨≡⟩ negate $≡ eq)

-- Eq --

instance
  EqInt : Eq Int
  Eq._==_ EqInt = eqInt
    where
      eqInt : (a b : Int) → Dec (a ≡ b)
      eqInt a b with inspect (a - b)
      eqInt a b | pos zero    with≡ eq = yes (lem-equal a b eq)
      eqInt a b | pos (suc n) with≡ eq = no λ a=b → case subInt-equal _ _ a=b ʳ⟨≡⟩ eq of λ ()
      eqInt a b | negsuc n    with≡ eq = no λ a=b → case subInt-equal _ _ a=b ʳ⟨≡⟩ eq of λ ()

-- Ord --

data LessInt (a b : Int) : Set where
  diff : (k : Nat) (eq : b ≡ pos (suc k) + a) → LessInt a b

compareInt : (a b : Int) → Comparison LessInt a b
compareInt a b with inspect (a - b)
compareInt a b | pos zero        with≡ eq = equal           (eraseEquality (lem-equal a b eq))
compareInt a b | c@(pos (suc k)) with≡ eq = greater (diff k (eraseEquality (sym (subInt-cancel-r a b c eq))))
compareInt a b | c@(negsuc k)    with≡ eq = less    (diff k (eraseEquality (sym (lem-less a b c eq))))
{-# INLINE compareInt #-}

private
  from-eq : ∀ x y → x ≡ y → LessInt x (1 + y)
  from-eq x y eq = diff 0 (eraseEquality (1 +_ $≡ sym eq))

  from-lt : ∀ x y → LessInt x y → LessInt x (1 + y)
  from-lt (pos n)    _ (diff k eq) = diff (suc k) (eraseEquality (1 +_ $≡ eq))
  from-lt (negsuc n) _ (diff k eq) = diff (suc k) (eraseEquality (
    1 +_ $≡ eq ⟨≡⟩ addInt-pos 1 (suc k -NZ suc n) ⟨≡⟩ʳ
    -NZ-suc-l (suc k) (suc n)))

  from-leq : ∀ x y → LessInt x (1 + y) → LessEq LessInt x y
  from-leq x y (diff zero eq) = equal (eraseEquality (addInt-inj₂ 1 x y (sym eq)))
  from-leq x y (diff (suc k) eq) =
    less (diff k (eraseEquality (sucInt-inj y (_+_ (pos (suc k)) x)
                                  (addInt-pos 1 y ʳ⟨≡⟩ eq ⟨≡⟩ addInt-sucInt-l (pos (suc k)) x))))

instance
  OrdInt : Ord Int
  Ord._<_         OrdInt = _
  Ord._≤_         OrdInt a b = LessInt a (1 + b)
  Ord.compare     OrdInt = compareInt
  Ord.eq-to-leq   OrdInt = from-eq _ _
  Ord.lt-to-leq   OrdInt = from-lt _ _
  Ord.leq-to-lteq OrdInt = from-leq _ _

-- Ord/Laws --

private
  lessInt-antirefl : (a : Int) → a < a → ⊥
  lessInt-antirefl a (diff k eq) = case addInt-inj₁ 0 (pos (suc k)) a (addInt-zero-l a ⟨≡⟩ eq) of λ ()

  lessInt-antisym : (a b : Int) → a < b → b < a → ⊥
  lessInt-antisym a b (diff k refl) (diff j eq) =
    case addInt-inj₁ 0 (pos (suc j) + pos (suc k)) a
           (addInt-zero-l a ⟨≡⟩ eq ⟨≡⟩ addInt-assoc (pos (suc j)) (pos (suc k)) a)
    of λ ()

  lessInt-trans : {a b c : Int} → a < b → b < c → a < c
  lessInt-trans {a} (diff k eq) (diff j eq₁) = diff (j + suc k) (eraseEquality $
    case eq of λ where
      refl → case eq₁ of λ where
        refl → addInt-assoc (pos (suc j)) (pos (suc k)) a)

instance
  OrdIntLaws : Ord/Laws Int
  Ord/Laws.super OrdIntLaws = it
  less-antirefl {{OrdIntLaws}} = lessInt-antirefl _
  less-trans    {{OrdIntLaws}} = lessInt-trans


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

open import Cubical.Algebra.Lattice.Base public
open import Cubical.Algebra.Lattice.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
{-# OPTIONS --without-K  #-}
module algebra.semigroup.morphism where

open import level
open import algebra.semigroup.core
open import equality.core
open import hott.level

module _ {i}{j}
         {X : Set i}⦃ sX : IsSemigroup X ⦄
         {Y : Set j}⦃ sY : IsSemigroup Y ⦄ where
  open IsSemigroup ⦃ ... ⦄

  IsSemigroupMorphism : (X → Y) → Set (i ⊔ j)
  IsSemigroupMorphism f = (x₁ x₂ : X) → f (x₁ * x₂) ≡ f x₁ * f x₂

  is-semigroup-morphism-level : (f : X → Y) → h 1 (IsSemigroupMorphism f)
  is-semigroup-morphism-level f = Π-level λ x₁ → Π-level λ x₂ → is-set _ _