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

open import Setoids.Setoids
open import Groups.FreeGroup.Definition
open import Groups.Definition
open import Decidable.Sets
open import Numbers.Naturals.Order
open import LogicalFormulae
open import Semirings.Definition

module Groups.FreeGroup.Group {a : _} {A : Set a} (decA : DecidableSet A) where

open import Groups.FreeGroup.Word decA

prepend : ReducedWord → FreeCompletion A → ReducedWord
prepend empty x = prependLetter x empty (wordEmpty refl)
prepend (prependLetter (ofLetter y) w pr) (ofLetter x) = prependLetter (ofLetter x) (prependLetter (ofLetter y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofLetter x} {ofInv x} λ ()))
prepend (prependLetter (ofInv y) w pr) (ofLetter x) with decA x y
... | inl x=y = w
... | inr x!=y = prependLetter (ofLetter x) (prependLetter (ofInv y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofLetter x} {ofLetter y} λ pr → x!=y (ofLetterInjective pr)))
prepend (prependLetter (ofLetter y) w pr) (ofInv x) with decA x y
... | inl x=y = w
... | inr x!=y = prependLetter (ofInv x) (prependLetter (ofLetter y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA λ pr → x!=y (ofInvInjective pr)))
prepend (prependLetter (ofInv y) w pr) (ofInv x) = prependLetter (ofInv x) (prependLetter (ofInv y) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofInv x} {ofLetter x} (λ ())))

_+W_ : ReducedWord → ReducedWord → ReducedWord
empty +W b = b
prependLetter letter a x +W b = prepend (a +W b) letter

prependValid : (w : ReducedWord) (l : A) → (x : PrependIsValid w (ofLetter l)) → prepend w (ofLetter l) ≡ prependLetter (ofLetter l) w x
prependValid empty l (wordEmpty refl) = refl
prependValid (prependLetter (ofLetter l2) w x) l pr = prependLetterRefl
prependValid (prependLetter (ofInv l2) w x) l pr with decA l l2
prependValid (prependLetter (ofInv l2) w x) .l2 (wordEnding _ x1) | inl refl = exFalso (freeCompletionEqualFalse' decA x1 refl)
... | inr l!=l2 = prependLetterRefl

prependValid' : (w : ReducedWord) (l : A) → (x : PrependIsValid w (ofInv l)) → prepend w (ofInv l) ≡ prependLetter (ofInv l) w x
prependValid' empty l (wordEmpty refl) = refl
prependValid' (prependLetter (ofLetter l2) w x) l pr with decA l l2
prependValid' (prependLetter (ofLetter l2) w x) .l2 (wordEnding _ x1) | inl refl = exFalso (freeCompletionEqualFalse' decA x1 refl)
... | inr l!=l2 = prependLetterRefl
prependValid' (prependLetter (ofInv l2) w x) l pr = prependLetterRefl

prependInv : (w : ReducedWord) (l : A) → prepend (prepend w (ofLetter l)) (ofInv l) ≡ w
prependInv empty l with decA l l
... | inl l=l = refl
... | inr l!=l = exFalso (l!=l refl)
prependInv (prependLetter (ofLetter l2) w x) l with decA l l
... | inl l=l = refl
... | inr l!=l = exFalso (l!=l refl)
prependInv (prependLetter (ofInv l2) w x) l with decA l l2
prependInv (prependLetter (ofInv l2) w x) .l2 | inl refl = prependValid' w l2 x
... | inr l!=l2 with decA l l
prependInv (prependLetter (ofInv l2) w x) l | inr l!=l2 | inl refl = refl
prependInv (prependLetter (ofInv l2) w x) l | inr l!=l2 | inr bad = exFalso (bad refl)

prependInv' : (w : ReducedWord) (l : A) → prepend (prepend w (ofInv l)) (ofLetter l) ≡ w
prependInv' empty l with decA l l
... | inl l=l = refl
... | inr l!=l = exFalso (l!=l refl)
prependInv' (prependLetter (ofLetter l2) w x) l with decA l l2
prependInv' (prependLetter (ofLetter l2) w x) .l2 | inl refl = prependValid w l2 x
... | inr l!=l2 with decA l l
... | inl refl = refl
... | inr l!=l = exFalso (l!=l refl)
prependInv' (prependLetter (ofInv l2) w x) l with decA l l
prependInv' (prependLetter (ofInv l2) w x) l | inl refl = refl
prependInv' (prependLetter (ofInv l2) w x) l | inr l!=l = exFalso (l!=l refl)

prependAndAdd : (a b : ReducedWord) (l : FreeCompletion A) → prepend (a +W b) l ≡ (prepend a l) +W b
prependAndAdd empty b l = refl
prependAndAdd (prependLetter (ofLetter x) w pr) b (ofLetter y) = refl
prependAndAdd (prependLetter (ofLetter x) w pr) b (ofInv y) with decA y x
prependAndAdd (prependLetter (ofLetter x) w pr) b (ofInv .x) | inl refl = prependInv _ _
... | inr y!=x = refl
prependAndAdd (prependLetter (ofInv x) w pr) b (ofLetter y) with decA y x
prependAndAdd (prependLetter (ofInv x) w pr) b (ofLetter .x) | inl refl = prependInv' _ _
... | inr y!=x = refl
prependAndAdd (prependLetter (ofInv x) w pr) b (ofInv y) = refl

+WAssoc : (a b c : ReducedWord) → (a +W (b +W c)) ≡ ((a +W b) +W c)
+WAssoc empty b c = refl
+WAssoc (prependLetter letter a x) b c rewrite equalityCommutative (prependAndAdd (a +W b) c letter) | +WAssoc a b c = refl

inverseW : ReducedWord → ReducedWord
inverseW empty = empty
inverseW (prependLetter letter w x) = (inverseW w) +W prependLetter (freeInverse letter) empty (wordEmpty refl)

identRightW : (a : ReducedWord) → a +W empty ≡ a
identRightW empty = refl
identRightW (prependLetter (ofLetter l) a x) rewrite identRightW a = prependValid a l x
identRightW (prependLetter (ofInv l) a x) rewrite identRightW a = prependValid' a l x

invLeftW : (a : ReducedWord) → (inverseW a) +W a ≡ empty
invLeftW empty = refl
invLeftW (prependLetter (ofLetter l) a x) rewrite equalityCommutative (+WAssoc (inverseW a) (prependLetter (ofInv l) empty (wordEmpty refl)) (prependLetter (ofLetter l) a x)) = t
  where
    t : (inverseW a +W (prepend (prependLetter (ofLetter l) a x) (ofInv l))) ≡ empty
    t with decA l l
    ... | inl refl = invLeftW a
    ... | inr l!=l = exFalso (l!=l refl)
invLeftW (prependLetter (ofInv l) a x) rewrite equalityCommutative (+WAssoc (inverseW a) (prependLetter (ofLetter l) empty (wordEmpty refl)) (prependLetter (ofInv l) a x)) = t
  where
    t : (inverseW a +W (prepend (prependLetter (ofInv l) a x) (ofLetter l))) ≡ empty
    t with decA l l
    ... | inl refl = invLeftW a
    ... | inr l!=l = exFalso (l!=l refl)

invRightW : (a : ReducedWord) → a +W (inverseW a) ≡ empty
invRightW empty = refl
invRightW (prependLetter (ofLetter l) a x) rewrite +WAssoc a (inverseW a) (prependLetter (ofInv l) empty (wordEmpty refl)) | invRightW a = t
  where
    t : prepend (prependLetter (ofInv l) empty (wordEmpty refl)) (ofLetter l) ≡ empty
    t with decA l l
    ... | inl refl = refl
    ... | inr l!=l = exFalso (l!=l refl)
invRightW (prependLetter (ofInv l) a x) rewrite +WAssoc a (inverseW a) (prependLetter (ofLetter l) empty (wordEmpty refl)) | invRightW a = t
  where
    t : prepend (prependLetter (ofLetter l) empty (wordEmpty refl)) (ofInv l) ≡ empty
    t with decA l l
    ... | inl refl = refl
    ... | inr l!=l = exFalso (l!=l refl)

freeGroup : Group (reflSetoid ReducedWord) _+W_
Group.+WellDefined freeGroup refl refl = refl
Group.0G freeGroup = empty
Group.inverse freeGroup = inverseW
Group.+Associative freeGroup {a} {b} {c} = +WAssoc a b c
Group.identRight freeGroup {a} = identRightW a
Group.identLeft freeGroup {a} = refl
Group.invLeft freeGroup {a} = invLeftW a
Group.invRight freeGroup {a} = invRightW a


text:
module Type.Category.IntensionalFunctionsCategory{ℓ} where

open import Data
open import Functional
open import Logic.Propositional
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Category
open import Structure.Categorical.Properties
open import Structure.Operator
open import Type
open import Type.Properties.Singleton

-- The type category is a category containing all types of a single universe level in the language.
-- The objects are all sets/types.
-- The morphisms are all functions where the domain/codomain-pair are from these objects.
typeIntensionalFnCategory : Category{Obj = Type{ℓ}}(_→ᶠ_)
Category._∘_            typeIntensionalFnCategory = _∘_
Category.id             typeIntensionalFnCategory = id
BinaryOperator.congruence (Category.binaryOperator typeIntensionalFnCategory) [≡]-intro [≡]-intro = [≡]-intro
Category.associativity  typeIntensionalFnCategory = Morphism.intro [≡]-intro
Category.identity       typeIntensionalFnCategory = [∧]-intro (Morphism.intro [≡]-intro) (Morphism.intro [≡]-intro)

typeIntensionalFnCategoryObject : CategoryObject
typeIntensionalFnCategoryObject = intro typeIntensionalFnCategory

Unit-terminalObject : Object.Terminal{Obj = Type{ℓ}}(_→ᶠ_) (Unit)
IsUnit.unit       Unit-terminalObject = const <>
IsUnit.uniqueness Unit-terminalObject = [≡]-intro

ext: agda

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 --universe-polymorphism #-}
module Categories.Monoidal where

open import Level

open import Categories.Category

open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalIsomorphism
open import Categories.NaturalTransformation using (_∘₁_) renaming (_≡_ to _≡ⁿ_)

open import Categories.Monoidal.Helpers

record Monoidal {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  private module C = Category C
  open C hiding (id; identityˡ; identityʳ; assoc)

  field
    ⊗  : Bifunctor C C C
    id : Obj

  open MonoidalHelperFunctors C ⊗ id

  field
    identityˡ : NaturalIsomorphism id⊗x x
    identityʳ : NaturalIsomorphism x⊗id x
    assoc : NaturalIsomorphism [x⊗y]⊗z x⊗[y⊗z]

  open Coherence identityˡ identityʳ assoc

  field
    .triangle : TriangleLeftSide ≡ⁿ (TriangleRightSide ∘₁ TriangleTopSide)
    .pentagon : (PentagonNESide ∘₁ PentagonNWSide) ≡ⁿ (PentagonSESide ∘₁ (PentagonSSide ∘₁ PentagonSWSide))

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
-- Andreas, 2016-02-16, issue 1777, reported by Martin Stone Davis

data D : Set where
  c : D

record R : Set where
  field f : D

test : R → D
test record { f = x } with x
... | y = {!y!}

-- Splitting on y should give
-- test record { f = x } | c = ?

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
open import Nat
open import Prelude
open import binders-disjoint-checks
open import judgemental-erase
open import lemmas-matching
open import moveerase
open import statics-core
open import synth-unicity

module sensibility where
  mutual
    -- if an action transforms a zexp in a synthetic posistion to another zexp,
    -- they have the same type up erasure of the cursor
    actsense-synth : {Γ : tctx} {e e' : zexp} {e◆ e'◆ : hexp} {t t' : htyp} {α : action} →
                     erase-e e e◆  →
                     erase-e e' e'◆ →
                     Γ ⊢ e => t ~ α ~> e' => t' →
                     Γ ⊢ e◆ => t →
                     Γ ⊢ e'◆ => t'
    -- in the movement case, we defer to the movement erasure theorem
    actsense-synth er er' (SAMove x) wt with erasee-det (moveerasee' er x) er'
    ... | refl = wt

    -- in all the nonzipper cases, the cursor must be at the top for the
    -- action rule to apply, so we just build the new derivation
    -- directly. no recursion is needed; these are effectively base cases.
    actsense-synth _ EETop SADel _ = SEHole
    actsense-synth EETop (EEAscR ETTop) SAConAsc wt = SAsc (ASubsume wt TCRefl)
    actsense-synth _ EETop (SAConVar p) _ = SVar p
    actsense-synth EETop (EEHalfLamL ETTop) (SAConLam x) SEHole = SLam x SEHole
    actsense-synth EETop (EEApR EETop) (SAConApArr x) wt = SAp wt x (ASubsume SEHole TCHole1)
    actsense-synth EETop (EEApR EETop) (SAConApOtw x) wt =
      SAp (SNEHole wt) MAHole (ASubsume SEHole TCRefl)
    actsense-synth _ EETop SAConNumlit _ = SNum
    actsense-synth EETop (EEPlusR EETop) (SAConPlus1 TCRefl) wt =
      SPlus (ASubsume wt TCRefl) (ASubsume SEHole TCHole1)
    actsense-synth EETop (EEPlusR EETop) (SAConPlus1 TCHole2) wt =
      SPlus (ASubsume wt TCHole1) (ASubsume SEHole TCHole1)
    actsense-synth EETop (EEPlusR EETop) (SAConPlus2 _) wt =
      SPlus (ASubsume (SNEHole wt) TCHole1) (ASubsume SEHole TCHole1)
    actsense-synth EETop (EENEHole EETop) (SAConNEHole) wt = SNEHole wt
    actsense-synth _ EETop (SAFinish x) _ = x
    actsense-synth EETop (EEAscR (ETPlusL ETTop)) SAConInl SEHole =
      SAsc (AInl MSSum (ASubsume SEHole TCRefl))
    actsense-synth EETop (EEAscR (ETPlusR ETTop)) SAConInr SEHole =
      SAsc (AInr MSSum (ASubsume SEHole TCRefl))
    actsense-synth EETop (EEAscL (EECase2 EETop)) (SAConCase1 c d e₁) f =
      SAsc (ACase c d e₁ f (ASubsume SEHole TCRefl) (ASubsume SEHole TCRefl))
    actsense-synth EETop (EEAscL (EECase1 (EENEHole EETop))) (SAConCase2 c d e₁) f =
      SAsc (ACase c d MSHole (SNEHole f) (ASubsume SEHole TCRefl) (ASubsume SEHole TCRefl))
    actsense-synth EETop (EEPairL EETop) SAConPair SEHole = SPair SEHole SEHole
    actsense-synth EETop EETop (SAConFst1 pr) wt = SFst wt pr
    actsense-synth EETop (EEFst er) (SAConFst2 inc) wt with erase-e◆ er
    ... | refl = SFst (SNEHole wt) MPHole
    actsense-synth EETop EETop (SAConSnd1 pr) wt = SSnd wt pr
    actsense-synth EETop (EESnd er) (SAConSnd2 inc) wt with erase-e◆ er
    ... | refl = SSnd (SNEHole wt) MPHole

    --- zipper cases. in each, we recur on the smaller action derivation
    --- following the zipper structure, then reassemble the result
    actsense-synth (EEAscL er) (EEAscL er') (SAZipAsc1 x) (SAsc x₁)
      with actsense-ana er er' x x₁
    ... | ih = SAsc ih
    actsense-synth (EEAscR x₁) (EEAscR x) (SAZipAsc2 x₂ x₃ x₄ x₅) (SAsc x₆)
      with eraset-det x x₃
    ... | refl = SAsc x₅
    actsense-synth (EEHalfLamL x₆) (EEHalfLamL x₇) (SAZipLam1 x x₁ x₂ x₃ x₄ x₅) (SLam x₈ wt)
      with eraset-det x₁ x₆ | eraset-det x₂ x₇
    ... | refl | refl = SLam x₈ x₅
    actsense-synth (EEHalfLamR er) (EEHalfLamR er') (SAZipLam2 x x₁ x₂ x₃) (SLam x₄ wt)
      with actsense-synth x₁ er' x₃ x₂
    ... | ih = SLam x₄ ih
    actsense-synth er (EEApL er') (SAZipApArr x x₁ x₂ act x₃) wt
      with actsense-synth x₁ er' act x₂
    ... | ih = SAp ih x x₃
    actsense-synth (EEApR er) (EEApR er') (SAZipApAna x x₁ x₂) (SAp wt x₃ x₄)
      with synthunicity x₁ wt
    ... | refl with ▸arr-unicity x x₃
    ... | refl with actsense-ana er er' x₂ x₄
    ... | ih = SAp wt x ih
    actsense-synth (EEPlusL er) (EEPlusL er') (SAZipPlus1 x) (SPlus x₁ x₂)
      with actsense-ana er er' x x₁
    ... | ih = SPlus ih x₂
    actsense-synth (EEPlusR er) (EEPlusR er') (SAZipPlus2 x) (SPlus x₁ x₂)
      with actsense-ana er er' x x₂
    ... | ih = SPlus x₁ ih
    actsense-synth er (EENEHole er') (SAZipNEHole x x₁ act) wt
      with actsense-synth x er' act x₁
    ... | ih = SNEHole ih
    actsense-synth (EEPairL er) (EEPairL er') (SAZipPair1 x₁ x₂ y x₃) (SPair z₁ z₂)
      with actsense-synth er er' y z₁
    ... | ih = SPair ih z₂
    actsense-synth (EEPairR er) (EEPairR er') (SAZipPair2 x₁ x₂ x₃ y) (SPair z₁ z₂)
      with actsense-synth er er' y z₂
    ... | ih = SPair z₁ ih
    actsense-synth (EEFst er) (EEFst er') (SAZipFst x₁ x₂ x₃ x₄ y) (SFst z₁ z₂)
      with actsense-synth x₃ er' y x₄
    ... | ih = SFst ih x₂
    actsense-synth (EESnd er) (EESnd er') (SAZipSnd x₁ x₂ x₃ x₄ y) (SSnd z₁ z₂)
      with actsense-synth x₃ er' y x₄
    ... | ih = SSnd ih x₂

    -- if an action transforms an zexp in an analytic posistion to another zexp,
    -- they have the same type up erasure of the cursor.
    actsense-ana  : {Γ : tctx} {e e' : zexp} {e◆ e'◆ : hexp} {t : htyp} {α : action} →
                  erase-e e  e◆ →
                  erase-e e' e'◆ →
                  Γ ⊢ e ~ α ~> e' ⇐ t →
                  Γ ⊢ e◆ <= t →
                  Γ ⊢ e'◆ <= t
    -- in the subsumption case, punt to the other theorem
    actsense-ana er1 er2 (AASubsume x x₁ x₂ x₃) _ = ASubsume (actsense-synth x er2 x₂ x₁) x₃

    -- for movement, appeal to the movement-erasure theorem
    actsense-ana er1 er2 (AAMove x) wt with erasee-det (moveerasee' er1 x) er2
    ... | refl = wt

    -- in the nonzipper cases, we again know where the hole must be, so we
    -- force it and then build the relevant derivation directly.
    actsense-ana EETop EETop AADel wt = ASubsume SEHole TCHole1
    actsense-ana EETop (EEAscR ETTop) AAConAsc wt = ASubsume (SAsc wt) TCRefl
    actsense-ana EETop (EENEHole EETop) (AAConVar x₁ p) wt = ASubsume (SNEHole (SVar p)) TCHole1
    actsense-ana EETop (EELam EETop) (AAConLam1 x₁ x₂) wt = ALam x₁ x₂ (ASubsume SEHole TCHole1)
    actsense-ana EETop (EENEHole EETop) (AAConNumlit x) wt = ASubsume (SNEHole SNum) TCHole1
    actsense-ana EETop EETop (AAFinish x) wt = x
    actsense-ana EETop (EENEHole (EEAscR (ETArrL ETTop))) (AAConLam2 x _) (ASubsume SEHole q) =
      ASubsume (SNEHole (SAsc (ALam x MAArr (ASubsume SEHole TCRefl)))) q

    -- all subsumptions in the right derivation are bogus, because there's no
    -- rule for lambdas synthetically
    actsense-ana (EELam _) (EELam _) (AAZipLam _ _ _) (ASubsume () _)

    -- that leaves only the zipper cases for lambda, where we force the
    -- forms and then recurr into the body of the lambda being checked.
    actsense-ana (EELam er1) (EELam er2) (AAZipLam x₁ x₂ act) (ALam x₄ x₅ wt)
      with ▸arr-unicity x₂ x₅
    ... | refl with actsense-ana er1 er2 act wt
    ... | ih = ALam x₄ x₅ ih

      -- constructing injections
    actsense-ana EETop (EEInl EETop) (AAConInl1 e) _ = AInl e (ASubsume SEHole TCHole1)
    actsense-ana EETop (EENEHole (EEAscR (ETPlusL ETTop))) (AAConInl2 e) _ =
      ASubsume (SNEHole (SAsc (AInl MSSum (ASubsume SEHole TCRefl)))) TCHole1
    actsense-ana EETop (EEInr EETop) (AAConInr1 e) _ = AInr e (ASubsume SEHole TCHole1)
    actsense-ana EETop (EENEHole (EEAscR (ETPlusL ETTop))) (AAConInr2 e) _ =
      ASubsume (SNEHole (SAsc (AInr MSSum (ASubsume SEHole TCRefl)))) TCHole1

      -- constructing case
    actsense-ana EETop (EECase1 EETop) (AAConCase a b) wt =
      ACase a b MSHole SEHole (ASubsume SEHole TCHole1) (ASubsume SEHole TCHole1)

      -- the ASubsume cases are all impossible, by forcing the form via the erasure
    actsense-ana (EEInl _) (EEInl _) (AAZipInl _ _ ) (ASubsume () _)
    actsense-ana (EEInr _) (EEInr _) (AAZipInr _ _) (ASubsume () _)
    actsense-ana (EECase1 _) (EECase1 _) (AAZipCase1 _ _ _ _ _ _ _ _) (ASubsume () _)
    actsense-ana (EECase2 _) (EECase2 _) (AAZipCase2 _ _ _ _ _) (ASubsume () _)
    actsense-ana (EECase3 _) (EECase3 _) (AAZipCase3 _ _ _ _ _) (ASubsume () _)

      -- zipper cases for sum types
    actsense-ana (EEInl er1) (EEInl er2) (AAZipInl m1 b) (AInl m2 wt)
      with ▸sum-unicity m1 m2
    ... | refl with actsense-ana er1 er2 b wt
    ... | wt' = AInl m1 wt'
    actsense-ana (EEInr er1) (EEInr er2) (AAZipInr m1 b) (AInr m2 wt)
          with ▸sum-unicity m1 m2
    ... | refl with actsense-ana er1 er2 b wt
    ... | wt' = AInr m1 wt'
    actsense-ana (EECase1 er1) (EECase1 er2) (AAZipCase1 x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈)
                 (ACase x₉ x₁₀ x₁₁ x₁₂ wt wt₁)
      with actsense-synth x₃ (rel◆ _)  x₅ x₄
    ... | ih = ACase x₉ x₁₀ x₆ (lem-synth-erase ih er2) x₇ x₈
    actsense-ana (EECase2 er1) (EECase2 er2) (AAZipCase2 x₁ x₂ s1 x₄ x₅)
                 (ACase x₇ x₈ x₉ s2 wt wt₁)
      with synthunicity s1 s2
    ... | refl with ▸sum-unicity x₉ x₄
    ... | refl with actsense-ana er1 er2 x₅ wt
    ... | ih = ACase x₇ x₈ x₉ s2 ih wt₁
    actsense-ana (EECase3 er1) (EECase3 er2) (AAZipCase3 x₁ x₃ s1 x₄ x₆)
                 (ACase x₇ x₈ x₉ s2 wt wt₁)
     with synthunicity s2 s1
    ... | refl with ▸sum-unicity x₉ x₄
    ... | refl with actsense-ana er1 er2 x₆ wt₁
    ... | ih = ACase x₇ x₈ x₉ s2 wt ih

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
------------------------------------------------------------------------
-- A function that runs computations
------------------------------------------------------------------------

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

open import Prelude hiding (⊥)

module Partiality-monad.Inductive.Approximate {a} {A : Type a} where

open import Equality.Propositional.Cubical

open import H-level.Truncation.Propositional equality-with-paths

open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Eliminators

-- Runs the computation. The given number is used to decide which
-- element to choose in sequences that are encountered.

approximate : A ⊥ → ℕ → ∥ Maybe A ∥
approximate x n = ⊥-rec-⊥
  (record
     { pe = ∣ nothing ∣
     ; po = λ x → ∣ just x ∣
     ; pl = λ _ rec → rec n
     ; pp = λ _ → truncation-is-proposition
     })
  x

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module Categories.PushOuts where

open import Library
open import Categories

open Cat

record Square {a}{b}{C : Cat {a}{b}}{X Y Z}(f : Hom C Z X)(g : Hom C Z Y) : Set (a ⊔ b) where
  constructor square
  field W    : Obj C
        h    : Hom C X W
        k    : Hom C Y W
        scom : comp C h f ≅ comp C k g

record SqMap {a}{b}{C : Cat {a}{b}}{X Y Z : Obj C}{f : Hom C Z X}{g : Hom C Z Y}
             (sq sq' : Square {a}{b}{C} f g) : Set (a ⊔ b) where
  constructor sqmap
  open Square
  field sqMor     : Hom C (W sq) (W sq')
        leftTr   : comp C sqMor (h sq) ≅ h sq'
        rightTr  : comp C sqMor (k sq) ≅ k sq'
open SqMap

record PushOut {a}{b}{C : Cat {a}{b}}{X Y Z}(f : Hom C Z X)(g : Hom C Z Y) : Set (a ⊔ b) where
  constructor pushout
  field sq : Square {a}{b}{C} f g
        uniqPush : (sq' : Square f g) → Σ (SqMap sq sq')
          \ u → (u' : SqMap sq sq') → sqMor u ≅ sqMor u'

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
-- Overlapping instances are only allowed if all valid candidates are
-- overappable.

module _ where

postulate
  A : Set

record B : Set where
  field overlap {{a}} : A

record C : Set where
  field overlap {{a}} : A

record D : Set where
  field {{a}} : A

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

work : {{b : B}} {{c : C}} → A
work = it

-- One variable candidate
fail₁ : {{a : A}} {{b : B}} → A
fail₁ = it

-- One non-overlappable field candidate
fail₂ : {{c : C}} {{d : D}} → A
fail₂ = it

instance postulate a : A

-- One top-level candidate
fail₃ : {{b : B}} → A
fail₃ = it

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS -v tc.unquote:30 #-}
open import Common.Prelude
open import Common.Reflection
open import Agda.Builtin.Sigma

data Box : Bool → Set where
  box : (b : Bool) → Box b

works : (b : Bool) → Box b → Bool
works b (box .b) = unquote (give (var 0 []))

works₂ : (b : Bool) → Box b → Bool
unquoteDef works₂ = defineFun works₂ (clause
  ( ("b" , vArg unknown) ∷ [])
  ( vArg (var 0)
  ∷ vArg (con (quote box)
        (vArg (dot unknown) ∷ []))
  ∷ [])
  (var 0 []) ∷ [])

works₃ : (b : Bool) → Box b → (x y : Bool) → Bool
unquoteDef works₃ = defineFun works₃ (clause
  ( ("y" , vArg unknown)
  ∷ ("x" , vArg unknown)
  ∷ ("b" , vArg unknown)
  ∷ [])
  ( vArg (var 2)
  ∷ vArg (con (quote box)
        (vArg (dot unknown) ∷ []))
  ∷ vArg (var 1)
  ∷ vArg (var 0)
  ∷ [])
  (var 2 []) ∷ [])

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.Equiv.Poly1-Poly where

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

open import Cubical.Data.Nat renaming (_+_ to _+n_; _·_ to _·n_)
open import Cubical.Data.Vec renaming ( [] to <> ; _∷_ to _::_)

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Univariate.Base
open import Cubical.Algebra.Polynomials.Univariate.Properties
open import Cubical.Algebra.CommRing.Instances.UnivariatePoly

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.Polynomials.Multivariate.Properties
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly

private variable
  ℓ : Level

module Equiv-Poly1-Poly: (A' : CommRing ℓ) where
  private
    A = fst A'

  open PolyMod A'
    renaming
    ( Poly               to Poly:
    ; isSetPoly          to isSetPoly:
    )

  open PolyModTheory A'
    renaming
    ( 0P                 to 0P:
    ; Poly-              to Poly:-
    ; _Poly+_            to _Poly:+_
    ; Poly+Lid           to Poly:+Lid
    ; Poly+Rid           to Poly:+Rid
    ; Poly+Assoc         to Poly:+Assoc
    ; Poly+Inverses      to Poly:+Inverses
    ; Poly+Comm          to Poly:+Comm
    ; _Poly*_            to _Poly:*_
    ; 1P                 to 1P:
    ; 0PRightAnnihilates to 0PRightAnnihilates:
    ; 0PLeftAnnihilates  to 0PLeftAnnihilates:
    ; Poly*Lid           to Poly:*Lid
    ; Poly*Rid           to Poly:*Rid
    ; Poly*Associative   to Poly:*Assoc
    ; Poly*Commutative   to Poly:*Comm
    ; prod-Xn-0P         to prod-Xn-0P:
    )

  open Nth-Poly-structure A' 1

-- Notation P, Q, R... for Poly 1
-- x, y, w... for Poly:
-- a,b,c... for A

-----------------------------------------------------------------------------
-- direct

  trad-base : (v : Vec ℕ 1) → A → Poly:
  trad-base (n :: <>) a = prod-Xn n [ a ]

  trad-base-neutral : (v : Vec ℕ 1) → trad-base v 0r ≡ []
  trad-base-neutral (n :: <>) = cong (prod-Xn n) drop0 ∙ prod-Xn-0P: n

  trad-base-add : (v : Vec ℕ 1) → (a b : A) → (trad-base v a) Poly:+ (trad-base v b) ≡ trad-base v (a + b)
  trad-base-add (n :: <>) a b = prod-Xn-sum n (a ∷ []) (b ∷ [])

  Poly1→Poly: : Poly A' 1 → Poly:
  Poly1→Poly: = Poly-Rec-Set.f A' 1 Poly: isSetPoly:
                 []
                 trad-base
                 (λ x y → x Poly:+ y)
                 Poly:+Assoc
                 Poly:+Rid
                 Poly:+Comm
                 trad-base-neutral
                 trad-base-add

  Poly1→Poly:-gmorph : (P Q : Poly A' 1) → Poly1→Poly: (P Poly+ Q) ≡ (Poly1→Poly: P) Poly:+ (Poly1→Poly: Q)
  Poly1→Poly:-gmorph P Q = refl

-----------------------------------------------------------------------------
-- converse

  Poly:→Poly1-int : (n : ℕ) → Poly: → Poly A' 1
  Poly:→Poly1-int n [] = 0P
  Poly:→Poly1-int n (a ∷ x) = (base (n :: <>) a) Poly+ Poly:→Poly1-int (suc n) x
  Poly:→Poly1-int n (drop0 i) = ((cong (λ X → X Poly+ 0P) (base-0P (n :: <>))) ∙ (Poly+-Rid 0P)) i

  Poly:→Poly1 : Poly: → Poly A' 1
  Poly:→Poly1 x = Poly:→Poly1-int 0 x

  Poly:→Poly1-int-gmorph : (x y : Poly:) → (n : ℕ) → Poly:→Poly1-int n (x Poly:+ y) ≡ (Poly:→Poly1-int n x) Poly+ (Poly:→Poly1-int n y)
  Poly:→Poly1-int-gmorph = ElimProp.f
                        (λ x → (y : Poly:) → (n : ℕ) → Poly:→Poly1-int n (x Poly:+ y) ≡ (Poly:→Poly1-int n x Poly+ Poly:→Poly1-int n y))
                        (λ y n → (cong (Poly:→Poly1-int n) (Poly:+Lid y)) ∙ (sym (Poly+-Lid (Poly:→Poly1-int n y))))
                        (λ a x ind-x → ElimProp.f
                                        (λ y → (n : ℕ) → Poly:→Poly1-int n ((a ∷ x) Poly:+ y) ≡ (Poly:→Poly1-int n (a ∷ x) Poly+ Poly:→Poly1-int n y))
                                        (λ n → sym (Poly+-Rid (Poly:→Poly1-int n (a ∷ x))))
                                        (λ b y ind-y n → sym (
                                                          (Poly-com-adv (base (n :: <>) a) (Poly:→Poly1-int (suc n) x) (base (n :: <>) b) (Poly:→Poly1-int (suc n) y))
                                                          ∙
                                                          (cong₂ _Poly+_ (base-Poly+ (n :: <>) a b) (sym (ind-x y (suc n))))) )
                                        λ {y} p q i n j → trunc
                                                          (Poly:→Poly1-int n ((a ∷ x) Poly:+ y))
                                                          (Poly:→Poly1-int n (a ∷ x) Poly+ Poly:→Poly1-int n y)
                                                          (p n) (q n) i j )
                        λ {x} p q i y n j → trunc (Poly:→Poly1-int n (x Poly:+ y)) (Poly:→Poly1-int n x Poly+ Poly:→Poly1-int n y) (p y n) (q y n) i j

  Poly:→Poly1-gmorph : (x y : Poly:) → Poly:→Poly1 (x Poly:+ y) ≡ (Poly:→Poly1 x) Poly+ (Poly:→Poly1 y)
  Poly:→Poly1-gmorph x y = Poly:→Poly1-int-gmorph x y 0

-----------------------------------------------------------------------------
-- section

  e-sect-int : (x : Poly:) → (n : ℕ) → Poly1→Poly: (Poly:→Poly1-int n x) ≡ prod-Xn n x
  e-sect-int = ElimProp.f
               (λ z → (n : ℕ) → Poly1→Poly: (Poly:→Poly1-int n z) ≡ prod-Xn n z)
               (λ n → sym (prod-Xn-0P: n))
               (λ a x ind-x n → ((prod-Xn n [ a ] ) Poly:+ (Poly1→Poly: (Poly:→Poly1-int (suc n) x)))
                                    ≡⟨ cong (λ X → prod-Xn n [ a ] Poly:+ X) (ind-x (suc n)) ⟩
                                 (prod-Xn n (a ∷ []) Poly:+ ( 0r ∷ prod-Xn n x))
                                    ≡⟨ prod-Xn-∷ n a x ⟩
                                 prod-Xn n (a ∷ x) ∎)
               (λ {x} p q i n j → isSetPoly: (Poly1→Poly: (Poly:→Poly1-int n x)) (prod-Xn n x) (p n) (q n) i j)

  e-sect : (x : Poly:) → Poly1→Poly: (Poly:→Poly1 x) ≡ x
  e-sect x = e-sect-int x 0

-----------------------------------------------------------------------------
-- retraction

  idde : (m n : ℕ) → (a : A) → Poly:→Poly1-int n (prod-Xn m [ a ]) ≡ base ((n +n m) :: <>) a
  idde zero n a = Poly+-Rid (base (n :: <>) a) ∙ cong (λ X → base (X :: <>) a) (sym (+-zero n))
  idde (suc m) n a = cong (λ X → X Poly+ Poly:→Poly1-int (suc n) (prod-Xn m (a ∷ []))) (base-0P (n :: <>))
                     ∙ Poly+-Lid (Poly:→Poly1-int (suc n) (prod-Xn m (a ∷ [])))
                     ∙ idde m (suc n) a
                     ∙ cong (λ X → base (X :: <>) a) (sym (+-suc n m))

  idde-v : (v : Vec ℕ 1) → (a : A) → Poly:→Poly1-int 0 (trad-base v a) ≡ base v a
  idde-v (n :: <>) a = (idde n 0 a)

  e-retr : (P : Poly A' 1) → Poly:→Poly1 (Poly1→Poly: P) ≡ P
  e-retr = Poly-Ind-Prop.f A' 1
           (λ P → Poly:→Poly1 (Poly1→Poly: P) ≡ P)
           (λ _ → trunc _ _)
           refl
           (λ v a → idde-v v a)
           λ {P Q} ind-P ind-Q → cong Poly:→Poly1 (Poly1→Poly:-gmorph P Q)
                                 ∙
                                 Poly:→Poly1-gmorph (Poly1→Poly: P) (Poly1→Poly: Q)
                                 ∙
                                 cong₂ _Poly+_ ind-P ind-Q

-----------------------------------------------------------------------------
-- Ring morphism

  map-1P : Poly1→Poly: 1P ≡ 1P:
  map-1P = refl

  trad-base-prod : (v v' : Vec ℕ 1) → (a a' : A) → trad-base (v +n-vec v') (a · a') ≡
                                                      (trad-base v a Poly:* trad-base v' a')
  trad-base-prod (k :: <>) (l :: <>) a a' = sym ((prod-Xn-prod k l  [ a ]  [ a' ]) ∙ cong (λ X → prod-Xn (k +n l) [ X ]) (+Rid (a · a')))

  Poly1→Poly:-rmorph : (P Q : Poly A' 1) → Poly1→Poly: (P Poly* Q) ≡ (Poly1→Poly: P) Poly:* (Poly1→Poly: Q)
  Poly1→Poly:-rmorph = Poly-Ind-Prop.f A' 1
                        (λ P → (Q : Poly A' 1) → Poly1→Poly: (P Poly* Q) ≡ (Poly1→Poly: P Poly:* Poly1→Poly: Q))
                        (λ P p q i Q j → isSetPoly: (Poly1→Poly: (P Poly* Q)) (Poly1→Poly: P Poly:* Poly1→Poly: Q) (p Q) (q Q) i j)
                        (λ Q → refl)
                        (λ v a → Poly-Ind-Prop.f A' 1
                                  (λ P → Poly1→Poly: (base v a Poly* P) ≡ (Poly1→Poly: (base v a) Poly:* Poly1→Poly: P))
                                  (λ _ → isSetPoly: _ _)
                                  (sym (0PLeftAnnihilates: (trad-base v a)))
                                  (λ v' a' → trad-base-prod v v' a a')
                                  λ {U V} ind-U ind-V → (cong₂ _Poly:+_ ind-U ind-V)
                                                         ∙ sym (Poly*LDistrPoly+ (Poly1→Poly: (base v a)) (Poly1→Poly: U) (Poly1→Poly: V)))
                        λ {U V} ind-U ind-V Q → (cong₂ _Poly:+_ (ind-U Q) (ind-V Q))
                                                 ∙ sym (Poly*RDistrPoly+ (Poly1→Poly: U) (Poly1→Poly: V) (Poly1→Poly: Q))

-- -----------------------------------------------------------------------------
-- -- Ring Equivalences

module _ (A' : CommRing ℓ) where

  open Equiv-Poly1-Poly: A'

  CRE-Poly1-Poly: : CommRingEquiv (PolyCommRing A' 1) (UnivariatePoly A')
  fst CRE-Poly1-Poly: = isoToEquiv is
    where
    is : Iso _ _
    Iso.fun is = Poly1→Poly:
    Iso.inv is = Poly:→Poly1
    Iso.rightInv is = e-sect
    Iso.leftInv is = e-retr
  snd CRE-Poly1-Poly: = makeIsRingHom map-1P Poly1→Poly:-gmorph Poly1→Poly:-rmorph

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
test.id : (A:Set) -> (x:A) -> A
test.id A x = x

nat.plus : (x:Nat) -> (y:Nat) -> Nat
nat.plus (nat.suc x) y = nat.suc (nat.plus x y)
nat.plus nat.zero y = y

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
import      Lvl
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.Subspaces.Image
  {ℓₛ ℓₛₑ}
  {S : Type{ℓₛ}}
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  where

open import Logic.Predicate
open import Sets.ExtensionalPredicateSet as PredSet using (PredSet ; _∈_ ; [∋]-binaryRelator)
open import Structure.Container.SetLike as SetLike using (SetElement)
open import Structure.Function.Multi
open import Structure.Operator
open import Structure.Operator.Properties
open import Structure.Operator.Vector
open import Structure.Operator.Vector.LinearMap
open import Structure.Operator.Vector.Proofs
open import Structure.Operator.Vector.Subspace
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Implication
open import Syntax.Transitivity

open VectorSpace ⦃ … ⦄
open VectorSpaceVObject ⦃ … ⦄ using (_+ᵥ_; _⋅ₛᵥ_)
open VectorSpaceVObject       using (Vector)

private variable ℓ ℓᵥ ℓᵥₑ : Lvl.Level
private variable V W : VectorSpaceVObject {ℓᵥ = ℓᵥ} {ℓᵥₑ = ℓᵥₑ} ⦃ equiv-S = equiv-S ⦄ (_+ₛ_)(_⋅ₛ_)
private variable F : V →ˡⁱⁿᵉᵃʳᵐᵃᵖ W

image : (V →ˡⁱⁿᵉᵃʳᵐᵃᵖ W) → PredSet(Vector(W))
image {V = V}{W = W} ([∃]-intro f) = PredSet.⊶ f

image-subspace : Subspace(image(F))
SetLike.FunctionProperties._closed-under₂_.proof (Subspace.add-closure (image-subspace {_} {_} {V} {_} {_} {W} {F = F@([∃]-intro f)})) {x} {y} xim yim =
  • (
    xim             ⇒
    x ∈ image(F)    ⇒-[]
    ∃(a ↦ f(a) ≡ x) ⇒-end
  )
  • (
    yim             ⇒
    y ∈ image(F)    ⇒-[]
    ∃(a ↦ f(a) ≡ y) ⇒-end
  )                      ⇒₂-[ [∃]-map₂ (_+ᵥ_) (p ↦ q ↦ (preserving₂(f)(_+ᵥ_)(_+ᵥ_) 🝖 congruence₂(_+ᵥ_) p q)) ]
  ∃(a ↦ f(a) ≡ x +ᵥ y)   ⇒-[]
  (x +ᵥ y) ∈ image(F)    ⇒-end
  where
    instance _ = V
    instance _ = W
SetLike.FunctionProperties._closed-under₁_.proof (Subspace.mul-closure (image-subspace {_} {_} {V} {_} {_} {W} {F = F@([∃]-intro f)}) {s}) {v} vim =
  vim ⇒
  v ∈ image(F)                ⇒-[]
  ∃(x ↦ f(x) ≡ v)             ⇒-[ [∃]-map-proof (congruence₂ᵣ(_⋅ₛᵥ_)(s)) ]
  ∃(x ↦ s ⋅ₛᵥ f(x) ≡ s ⋅ₛᵥ v) ⇒-[ [∃]-map (s ⋅ₛᵥ_) (preserving₁(f)(s ⋅ₛᵥ_)(s ⋅ₛᵥ_) 🝖_) ]
  ∃(x ↦ f(x) ≡ s ⋅ₛᵥ v)       ⇒-[]
  (s ⋅ₛᵥ v) ∈ image(F)        ⇒-end
  where
    instance _ = V
    instance _ = W


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

open import HoTT
open import cw.CW
open import cw.FinCW
open import cw.FinBoundary
open import cohomology.Theory

{- The reason that RephraseDualizedFirstFinBoundary did not handle this case
   is because [FinSkeleton n] does not compute. -}

module cw.cohomology.cochainequiv.DualizedFirstBoundary (OT : OrdinaryTheory lzero)
  (⊙fin-skel : ⊙FinSkeleton 1) where

open OrdinaryTheory OT

private
  fin-skel = ⊙FinSkeleton.skel ⊙fin-skel
  I = AttachedFinSkeleton.numCells fin-skel

  I₋₁ = AttachedFinSkeleton.skel fin-skel

abstract
  rephrase-dualized-first-boundary-in-degree : ∀ g <I
    →  FormalSum-extend (C2-abgroup 0) g (GroupHom.f (fboundary-last fin-skel) fs[ inl <I :: nil ])
    == Group.sum (C2 0) (λ <I₋₁ → Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁))
  rephrase-dualized-first-boundary-in-degree g <I =
    FormalSum-extend (C2-abgroup 0) g (GroupHom.f (fboundary-last fin-skel) fs[ inl <I :: nil ])
      =⟨ ap (FormalSum-extend (C2-abgroup 0) g) $
          app= (is-equiv.g-f (FreeAbGroup-extend-is-equiv (FreeAbGroup (Fin I₋₁))) (fboundary'-last fin-skel)) <I ⟩
    FormalSum-extend (C2-abgroup 0) g
      (Group.sum (FreeAbGroup.grp (Fin I₋₁))
        (λ <I₋₁ → Group.exp (FreeAbGroup.grp (Fin I₋₁)) fs[ inl <I₋₁ :: nil ] (fdegree-last fin-skel <I <I₋₁)))
      =⟨ GroupHom.pres-sum (FreeAbGroup-extend (C2-abgroup 0) g)
          (λ <I₋₁ → Group.exp (FreeAbGroup.grp (Fin I₋₁)) fs[ inl <I₋₁ :: nil ] (fdegree-last fin-skel <I <I₋₁)) ⟩
    Group.sum (C2 0)
      (λ <I₋₁ →
        (FormalSum-extend (C2-abgroup 0) g
          (Group.exp (FreeAbGroup.grp (Fin I₋₁)) fs[ inl <I₋₁ :: nil ] (fdegree-last fin-skel <I <I₋₁))))
      =⟨ ap (Group.sum (C2 0))
          (λ= λ <I₋₁ →
            GroupHom.pres-exp (FreeAbGroup-extend (C2-abgroup 0) g)
              fs[ inl <I₋₁ :: nil ]
              (fdegree-last fin-skel <I <I₋₁)) ⟩
    Group.sum (C2 0)
      (λ <I₋₁ →
        (Group.exp (C2 0)
          (FormalSum-extend (C2-abgroup 0) g fs[ inl <I₋₁ :: nil ])
          (fdegree-last fin-skel <I <I₋₁)))
      =⟨ ap (Group.sum (C2 0))
          (λ= λ <I₋₁ → ap (λ g → Group.exp (C2 0) g (fdegree-last fin-skel <I <I₋₁)) $
            app= (is-equiv.g-f (FreeAbGroup-extend-is-equiv (C2-abgroup 0)) g) <I₋₁) ⟩
    Group.sum (C2 0) (λ <I₋₁ → (Group.exp (C2 0) (g <I₋₁) (fdegree-last fin-skel <I <I₋₁)))
      =∎

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import SOAS.Common
open import SOAS.Families.Core
open import Categories.Object.Initial
open import SOAS.Coalgebraic.Strength
import SOAS.Metatheory.MetaAlgebra

-- Initial-algebra semantics
module SOAS.Metatheory.Semantics {T : Set}
  (⅀F : Functor 𝔽amiliesₛ 𝔽amiliesₛ) (⅀:Str : Strength ⅀F)
  (𝔛 : Familyₛ) (open SOAS.Metatheory.MetaAlgebra ⅀F 𝔛)
  (𝕋:Init : Initial 𝕄etaAlgebras)
  where

open import SOAS.Context
open import SOAS.Variable
open import SOAS.Construction.Structure as Structure
open import SOAS.Abstract.Hom
import SOAS.Abstract.Coalgebra as →□ ; open →□.Sorted
import SOAS.Abstract.Box as □ ; open □.Sorted

open import SOAS.Metatheory.Algebra ⅀F

open Strength ⅀:Str

private
  variable
    Γ Δ Θ Π : Ctx
    α β : T
    𝒫 𝒬 𝒜 : Familyₛ

open Initial 𝕋:Init

open Object ⊥ public renaming (𝐶 to 𝕋 ; ˢ to 𝕋ᵃ)
open MetaAlg 𝕋ᵃ public renaming (𝑎𝑙𝑔 to 𝕒𝕝𝕘 ; 𝑣𝑎𝑟 to 𝕧𝕒𝕣 ; 𝑚𝑣𝑎𝑟 to 𝕞𝕧𝕒𝕣 ;
                                  𝑚≈₁ to 𝕞≈₁ ; 𝑚≈₂ to 𝕞≈₂)

module Semantics (𝒜ᵃ : MetaAlg 𝒜) where

  open Morphism (! {𝒜 ⋉ 𝒜ᵃ}) public renaming (𝑓 to 𝕤𝕖𝕞 ; ˢ⇒ to 𝕤𝕖𝕞ᵃ⇒)
  open MetaAlg⇒ 𝕤𝕖𝕞ᵃ⇒ public renaming (⟨𝑎𝑙𝑔⟩ to ⟨𝕒⟩ ; ⟨𝑣𝑎𝑟⟩ to ⟨𝕧⟩ ; ⟨𝑚𝑣𝑎𝑟⟩ to ⟨𝕞⟩)
  open MetaAlg 𝒜ᵃ
  module 𝒜 = MetaAlg 𝒜ᵃ

  eq : {g h : 𝕋 ⇾̣ 𝒜} (gᵃ : MetaAlg⇒ 𝕋ᵃ 𝒜ᵃ g) (hᵃ : MetaAlg⇒ 𝕋ᵃ 𝒜ᵃ h) (t : 𝕋 α Γ)
     → g t ≡ h t
  eq {g = g}{h} gᵃ hᵃ t  = !-unique₂ (g ⋉ gᵃ) (h ⋉ hᵃ) {x = t}

  -- The interpretation is equal to any other pointed meta-Λ-algebra
  𝕤𝕖𝕞! : {g : 𝕋 ⇾̣ 𝒜}(gᵃ : MetaAlg⇒ 𝕋ᵃ 𝒜ᵃ g)(t : 𝕋 α Γ) → 𝕤𝕖𝕞 t ≡ g t
  𝕤𝕖𝕞! {g = g} gᵃ t = !-unique (g ⋉ gᵃ) {x = t}

-- Corollaries: every meta-algebra endo-homomorphism is the identity, including 𝕤𝕖𝕞
eq-id : {g : 𝕋 ⇾̣ 𝕋} (gᵃ : MetaAlg⇒ 𝕋ᵃ 𝕋ᵃ g) (t : 𝕋 α Γ) →
        g t ≡ t
eq-id gᵃ t = Semantics.eq 𝕋ᵃ gᵃ (idᵃ 𝕋ᵃ) t

𝕤𝕖𝕞-id : {t : 𝕋 α Γ} → Semantics.𝕤𝕖𝕞 𝕋ᵃ t ≡ t
𝕤𝕖𝕞-id {t = t} = eq-id (Semantics.𝕤𝕖𝕞ᵃ⇒ 𝕋ᵃ) t

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-# OPTIONS --without-K --rewriting #-}
open import HoTT.Base
open import HoTT.HLevel

module HoTT.HLevel.Truncate where

open variables

postulate _↦_ : ∀ {a} {A : Set a} → A → A → Set a
{-# BUILTIN REWRITE _↦_ #-}

postulate
  ∥_∥ : 𝒰 i → 𝒰 i
  ∣_∣ : A → ∥ A ∥
  instance ∥-hlevel : hlevel 1 ∥ A ∥
  ∥-rec : ⦃ hlevel 1 B ⦄ → (A → B) → ∥ A ∥ → B
  ∥-β : ⦃ _ : hlevel 1 B ⦄ → (f : A → B) (x : A) → ∥-rec f ∣ x ∣ ↦ f x
{-# REWRITE ∥-β #-}

{-
  data Squash (A : 𝒰 i) : 𝒰 i where
    squash : A → Squash A

∥_∥ : 𝒰 i → 𝒰 i
∥_∥ = Squash

∣_∣ : A → ∥ A ∥
∣_∣ = squash

postulate instance ∥-hlevel : hlevel 1 ∥ A ∥

∥-rec : {B : 𝒰 i} → ⦃ hlevel 1 B ⦄ → (A → B) → ∥ A ∥ → B
∥-rec f (squash x) = f x
-}

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module Issue296 where

postulate
  Unit : Set
  IO   : Set → Set
  foo  : ((A B : Set) → Unit) → IO Unit
  bar  : (A B : Set) → Unit

{-# BUILTIN IO IO #-}
{-# COMPILE GHC IO = type IO #-}
{-# COMPILE GHC Unit = type () #-}
{-# COMPILE GHC bar = undefined #-}

main : IO Unit
main = foo bar


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

open import HoTT
open import groups.Cokernel
open import groups.Exactness
open import groups.ExactSequence
open import cohomology.Theory

open import cw.CW
open import cw.WedgeOfCells

module cw.cohomology.reconstructed.TipCoboundary {i} (OT : OrdinaryTheory i)
  (⊙skel : ⊙Skeleton {i} 1) where

open OrdinaryTheory OT
open import cohomology.LongExactSequence cohomology-theory 0 (⊙cw-incl-last ⊙skel)
open import cw.cohomology.WedgeOfCells OT ⊙skel
open import cw.cohomology.reconstructed.TipAndAugment OT (⊙cw-init ⊙skel)

CX₁/X₀-is-abelian = CXₙ/Xₙ₋₁-is-abelian 1

cw-co∂-head' : CX₀ 0 →ᴳ CXₙ/Xₙ₋₁ 1
cw-co∂-head' = co∂

⊙cw-∂-head'-before-Susp : ⊙Xₙ/Xₙ₋₁ (⊙Skeleton.skel ⊙skel) ⊙→ ⊙Susp (⊙cw-head ⊙skel)
⊙cw-∂-head'-before-Susp = ⊙∂-before-Susp

cw-∂-head'-before-Susp : Xₙ/Xₙ₋₁ (⊙Skeleton.skel ⊙skel) → Susp (cw-head (⊙Skeleton.skel ⊙skel))
cw-∂-head'-before-Susp = ∂-before-Susp

abstract
  cw-∂-head'-before-Susp-glue-β : ∀ x → ap cw-∂-head'-before-Susp (cfglue x) == merid x
  cw-∂-head'-before-Susp-glue-β = ∂-before-Susp-glue-β

cw-co∂-head : C2×CX₀ 0 →ᴳ CXₙ/Xₙ₋₁ 1
cw-co∂-head = record {f = GroupHom.f cw-co∂-head' ∘ snd; pres-comp = lemma}
  where abstract lemma = ∘ᴳ-pres-comp cw-co∂-head' (×ᴳ-snd {G = C2 0} {H = CX₀ 0})

abstract
  -- This relies on the [lemma] above being non-abstract within this scope.
  co∂-head-incl-exact : is-exact cw-co∂-head (C-fmap 1 (⊙cfcod' (⊙cw-incl-last ⊙skel)))
  co∂-head-incl-exact = pre∘-is-exact
    (×ᴳ-snd {G = C2 0} {H = CX₀ 0})
    (×ᴳ-snd-is-surj {G = C2 0} {H = CX₀ 0})
    (exact-seq-index 1 C-cofiber-exact-seq)

module CokerCo∂Head where
  grp = Coker cw-co∂-head CX₁/X₀-is-abelian
  open Group grp public


text:
------------------------------------------------------------------------------
-- Reasoning partially about functions
------------------------------------------------------------------------------

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

-- We cannot reasoning partially about partial functions intended to
-- operate in total values.

module FOT.FOTC.Data.Nat.AddPartialRightIdentity where

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

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

-- How proceed?
+-partialRightIdentity : ∀ n → n + zero ≡ n
+-partialRightIdentity n = {!!}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text: test = forall _Set_ → Set


text:
open import Prelude

module List where
  data List (A : Set) : Set where
    [] : List A
    _::_ : (a : A) (as : List A) → List A

  -- list append, structural on the left
  _++_ : {A : Set} → List A → List A → List A
  [] ++ l₂ = l₂
  (h :: l₁) ++ l₂ = h :: (l₁ ++ l₂)

  -- list membership, as a proposition
  data _inList_ {A : Set} : A → List A → Set where
    InH : {a : A} {as : List A} → a inList (a :: as)
    InT : {a a' : A} {as : List A} → a inList as → a inList (a' :: as)

  -- if everything isn't in a list, it's the empty list
  ∅∈l→l==[] : {A : Set} {l : List A} → ((a : A) → a inList l → ⊥) → l == []
  ∅∈l→l==[] {l = []} h = refl
  ∅∈l→l==[] {l = a' :: as} h = abort (h a' InH)

  -- if a isn't in a cons, it's not in the tail either
  a∉a'::as→a∉as : {A : Set} {as : List A} {a a' : A} →
                  (a inList (a' :: as) → ⊥) →
                   a inList as →
                   ⊥
  a∉a'::as→a∉as h h' = h (InT h')

  -- if x isn't in either side of an append, it's not in the result
  not-in-append-comm : {A : Set} {x : A} {l₁ l₂ : List A} →
                       dec A →
                       (x inList l₁ → ⊥) →
                       (x inList l₂ → ⊥) →
                       x inList (l₁ ++ l₂) → ⊥
  not-in-append-comm {l₁ = []} dec h₁ h₂ h₃ = h₂ h₃
  not-in-append-comm {x = x} {a₁ :: _} dec h₁ h₂ h₃   with  dec a₁ x
  not-in-append-comm {l₁ = l₁} dec h₁ h₂ h₃          | Inl h = h₁ (tr (λ y → y inList l₁) h InH)
  not-in-append-comm dec h₁ h₂ InH                   | Inr h = abort (h refl)
  not-in-append-comm dec h₁ h₂ (InT h₃)              | Inr h = not-in-append-comm dec (a∉a'::as→a∉as h₁) h₂ h₃

  remove-all : {A : Set} → dec A → List A → A → List A
  remove-all dec [] a = []
  remove-all dec (a' :: as) a
    with dec a a' | remove-all dec as a
  ...  | Inl _      | l'                    = l'
  ...  | Inr _      | l'                    = a' :: l'

  -- (homomorphism) removing distributes over append
  remove-all-append-comm : {A : Set} →
                           (dec : dec A) →
                           (l₁ l₂ : List A) →
                           (a : A) →
                           remove-all dec l₁ a ++ remove-all dec l₂ a == remove-all dec (l₁ ++ l₂) a
  remove-all-append-comm dec [] l₂ a = refl
  remove-all-append-comm dec (a₁ :: as₁) l₂ a with dec a a₁ | remove-all-append-comm dec as₁ l₂ a
  remove-all-append-comm dec (a₁ :: as₁) l₂ a    | Inl refl   | h                                      = h
  remove-all-append-comm dec (a₁ :: as₁) l₂ a    | Inr _      | h                                      = ap1 (λ y → a₁ :: y) h

  -- an element isn't in the list that results from removing all instances of it
  remove-all-not-in : {A : Set} →
                      (dec : dec A) →
                      (l : List A) →
                      (a : A) →
                      a inList remove-all dec l a →
                      ⊥
  remove-all-not-in dec [] a ()
  remove-all-not-in dec (a' :: as) a h with    dec a a'
  remove-all-not-in dec (a' :: as) a h       | Inl refl   = remove-all-not-in dec as a' h
  remove-all-not-in dec (a' :: as) .a' InH   | Inr a≠a'   = a≠a' refl
  remove-all-not-in dec (a' :: as) a (InT h) | Inr a≠a'   = remove-all-not-in dec as a h

  -- an element that was never in a list still isn't once you remove any element.
  a∉l→a∉remove-all-l-a' : {A : Set} →
                            {l : List A} →
                            {a a' : A} →
                            (dec : dec A) →
                            (a inList l → ⊥) →
                            a inList remove-all dec l a' →
                            ⊥
  a∉l→a∉remove-all-l-a' {l = []} {a} _ h₁ h₂ = h₁ h₂
  a∉l→a∉remove-all-l-a' {l = lh :: lt} {a} {a'} dec h₁ h₂   with  dec a lh | dec a' lh
  a∉l→a∉remove-all-l-a' {l = lh :: lt} {a} dec h₁ h₂       | Inl a==lh  | _            = h₁ (tr (λ y → a inList (y :: lt) ) a==lh InH)
  a∉l→a∉remove-all-l-a' {l = lh :: lt} dec h₁ h₂       | Inr _      | Inl _        = a∉l→a∉remove-all-l-a' dec (a∉a'::as→a∉as h₁) h₂
  a∉l→a∉remove-all-l-a' {l = lh :: lt} dec h₁ InH    | Inr a≠lh   | Inr _        = a≠lh refl
  a∉l→a∉remove-all-l-a' {l = lh :: lt} dec h₁ (InT h₂) | Inr _      | Inr _        = a∉l→a∉remove-all-l-a' dec (a∉a'::as→a∉as h₁) h₂

  -- if an element is in an append, it's in one side or the other
  inList++ : {A : Set} {x : A} → ∀{l1 l2} → dec A → x inList (l1 ++ l2) → (x inList l1) + (x inList l2)
  inList++ {l1 = []} dec xin = Inr xin
  inList++ {x = x} {l1 = a :: l1} dec inl with dec x a
  inList++ {x = .a} {a :: l1} dec inl | Inl refl = Inl InH
  inList++ {x = .a} {a :: l1} dec InH | Inr x₁ = abort (x₁ refl)
  inList++ {x = x} {a :: l1} dec (InT inl) | Inr x₁ with inList++ {l1 = l1} dec inl
  inList++ {x = x} {a :: l1} dec (InT inl) | Inr x₁ | Inl x₂ = Inl (InT x₂)
  inList++ {x = x} {a :: l1} dec (InT inl) | Inr x₁ | Inr x₂ = Inr x₂

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
-- Andreas, 2012-01-13
module Issue555a where

-- Do we want to allow this?
data Exp : Set → Set1
data Exp Γ where -- needs to report that too many parameters are given
  var : Exp Γ
  bla : {Δ : Set} → Exp Δ → Exp (Δ → Γ) → Exp Γ

-- A declared index is turned into a parameter by the definition.

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

data Vec : Set → ℕ → Set
data Vec A where
  nil : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)


text:
open import SOAS.Common

{-
Framework for constructing categories of objects with extra structure.
The definitions required to construct a category is:
* the category of carrier objects (e.g. sets, presheaves, etc.)
* the extra operations and laws that the carrier objects are equipped with
* the preservation properties of morphisms between the structures
* proofs that the identities and composition of the carrier category preserve
  the extra structure
-}

module SOAS.Construction.Structure
  (CarrierCat : Category 1ℓ 0ℓ 0ℓ)
  (HasStruct : Category.Obj CarrierCat → Set) where

private module ℂ = Category CarrierCat

-- The carrier of the structure, e.g. sets, presheaves, etc.
Carrier : Set₁
Carrier = ℂ.Obj

infix 1 _⋉_

-- Objects in the category for the structure: a carrier object together with
-- the algebraic structure
record Object : Set₁ where
  constructor _⋉_
  field
    𝐶 : Carrier
    ˢ : HasStruct 𝐶

open Object public

-- Properties of the morphisms between two objects, usually concerning
-- the preservation of the extra operations
MorphismProps : Set₁
MorphismProps = {𝐶₁ 𝐶₂ : Carrier}
              → HasStruct 𝐶₁
              → HasStruct 𝐶₂
              → CarrierCat [ 𝐶₁ , 𝐶₂ ] → Set

-- Morphisms in the category for the algebraic structure: an underlying
-- morphism with preservation properties of the extra structure
record Morphism (IsHomomorphism : MorphismProps) (O₁ O₂ : Object) : Set where
  constructor _⋉_
  field
    𝑓   : CarrierCat [ 𝐶 O₁ , 𝐶 O₂ ]
    ˢ⇒ : IsHomomorphism (ˢ O₁)(ˢ O₂) 𝑓

open Morphism public

-- Properties required to turn the objects and morphisms into a category; namely
-- that the identity and composition in the carrier category are homomorphisms
record CategoryProps : Set₁ where
  field
    IsHomomorphism  : MorphismProps
    id-hom   : {𝐶 : Carrier}{𝐶ˢ : HasStruct 𝐶} → IsHomomorphism 𝐶ˢ 𝐶ˢ ℂ.id
    comp-hom : {𝐶 𝐷 𝐸 : Carrier}
               {𝐶ˢ : HasStruct 𝐶}{𝐷ˢ : HasStruct 𝐷}{𝐸ˢ : HasStruct 𝐸} →
               (𝑔 : CarrierCat [ 𝐷 , 𝐸 ])(𝑓 : CarrierCat [ 𝐶 , 𝐷 ]) →
               (𝑔ʰ : IsHomomorphism 𝐷ˢ 𝐸ˢ 𝑔)(𝑓ʰ : IsHomomorphism 𝐶ˢ 𝐷ˢ 𝑓) →
               IsHomomorphism 𝐶ˢ 𝐸ˢ (𝑔 ℂ.∘ 𝑓)

module _ (P : CategoryProps) where
  open CategoryProps P

  -- Category generated from the algebraic structure
  StructCat : Category 1ℓ 0ℓ 0ℓ
  StructCat = categoryHelper (record
    { Obj = Object
    ; _⇒_ = Morphism IsHomomorphism
    ; _≈_ = λ g₁ g₂ → 𝑓 g₁ ℂ.≈ 𝑓 g₂
    ; id = ℂ.id ⋉ id-hom
    ; _∘_ = λ{ (𝑔 ⋉ 𝑔ˢ⇒) (𝑓 ⋉ 𝑓ˢ⇒) → (𝑔 ℂ.∘ 𝑓) ⋉ (comp-hom 𝑔 𝑓 𝑔ˢ⇒ 𝑓ˢ⇒)}
    ; assoc = ℂ.assoc
    ; identityˡ = ℂ.identityˡ
    ; identityʳ = ℂ.identityʳ
    ; equiv = record { refl = ℂ.Equiv.refl ; sym = ℂ.Equiv.sym ; trans = ℂ.Equiv.trans }
    ; ∘-resp-≈ = ℂ.∘-resp-≈
    })

  -- Forget the structure of a carrier object
  Forget :  Object → Carrier
  Forget (𝐶 ⋉ _) = 𝐶

  -- Forgetful functor from the structure category to the carrier category
  ForgetF : Functor StructCat CarrierCat
  ForgetF = record
    { F₀ = Forget
    ; F₁ = λ (𝑓 ⋉ _) → 𝑓
    ; identity = ℂ.Equiv.refl
    ; homomorphism = ℂ.Equiv.refl
    ; F-resp-≈ = λ x → x
    }
    where
    open ≡-Reasoning

  -- Free constructions with respect to the forgetful functor
  module Free where
    open import SOAS.Construction.Free ForgetF public


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

open import Categories.Category.Core

module Categories.Morphism.Extremal.Properties {o ℓ e} (𝒞 : Category o ℓ e) where

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

open import Categories.Diagram.Equalizer 𝒞
open import Categories.Diagram.Coequalizer 𝒞

open import Categories.Morphism 𝒞
open import Categories.Morphism.Extremal 𝒞
open import Categories.Morphism.Properties 𝒞
open import Categories.Morphism.Reasoning 𝒞
open import Categories.Morphism.Regular 𝒞

open Category 𝒞
open HomReasoning

private
  variable
    A B : Obj
    f g : A ⇒ B

--------------------------------------------------------------------------------
-- Extremal Epimorphisms

RegularEpi⇒IsExtremalEpi : ∀ {A B} {f : A ⇒ B} (e : RegularEpi f) → IsExtremalEpi (RegularEpi⇒Epi e)
RegularEpi⇒IsExtremalEpi {A = A} {B = B} {f = f} regular {X = X} {i = i} {g = k} i-mono f≈i∘k =
  record
    { inv = i⁻¹
    ; iso = record
      { isoˡ = isoˡ
      ; isoʳ = isoʳ
      }
    }
  where
    open RegularEpi regular renaming (g to r; h to s)
    open IsCoequalizer coequalizer

    i⁻¹ : B ⇒ X
    i⁻¹ = coequalize $ i-mono (k ∘ s) (k ∘ r) $ begin
        i ∘ k ∘ s ≈⟨ pullˡ (⟺ f≈i∘k) ⟩
        f ∘ s     ≈⟨ equality ⟩
        f ∘ r     ≈⟨ pushˡ f≈i∘k ⟩
        i ∘ k ∘ r ∎

    isoʳ : i ∘ i⁻¹ ≈ id
    isoʳ = RegularEpi⇒Epi regular (i ∘ i⁻¹) id $ begin
      (i ∘ i⁻¹) ∘ f ≈⟨ pullʳ (⟺ universal) ⟩
      i ∘ k         ≈˘⟨ f≈i∘k ⟩
      f             ≈˘⟨ identityˡ ⟩
      id ∘ f        ∎

    isoˡ : i⁻¹ ∘ i ≈ id
    isoˡ = i-mono (i⁻¹ ∘ i) id $ begin
      i ∘ i⁻¹ ∘ i ≈⟨ cancelˡ isoʳ ⟩
      i           ≈˘⟨ identityʳ ⟩
      i ∘ id      ∎

RegularEpi⇒ExtremalEpi : (e : RegularEpi f) → ExtremalEpi f
RegularEpi⇒ExtremalEpi e = record
  { epi = RegularEpi⇒Epi e
  ; extremal = RegularEpi⇒IsExtremalEpi e
  }

ExtremalEpi-∘₂ : ExtremalEpi (f ∘ g) → ExtremalEpi f
ExtremalEpi-∘₂ fg-extremal = record
  { epi = Epi-∘₂ epi
  ; extremal = λ i-mono eq → extremal i-mono (pushˡ eq)
  }
  where
    open ExtremalEpi fg-extremal

ExtremalEpi-∘ : ∀ {A B C} {f : B ⇒ C} {g : A ⇒ B} → ExtremalEpi f → RegularEpi g → ExtremalEpi (f ∘ g)
ExtremalEpi-∘ {A = A} {B = B} {C = C} {f = f} {g = g} f-extremal g-regular = record
  { epi = fg-epi
  ; extremal = fg-extremal
  }
  where
    module f-extremal = ExtremalEpi f-extremal
    module g-regular = RegularEpi g-regular
    open IsCoequalizer g-regular.coequalizer

    g-epi : Epi g
    g-epi = RegularEpi⇒Epi g-regular

    fg-epi : Epi (f ∘ g)
    fg-epi = Epi-∘ f-extremal.epi g-epi

    fg-extremal : IsExtremalEpi fg-epi
    fg-extremal {X = X} {i = i} {g = h} i-mono f∘g≈i∘h =
      f-extremal.extremal i-mono $ g-epi _ _ $ begin
        f ∘ g       ≈⟨ f∘g≈i∘h ⟩
        i ∘ h       ≈⟨ pushʳ universal ⟩
        (i ∘ k) ∘ g ∎
      where
        k : B ⇒ X
        k = coequalize $ i-mono _ _ $ begin
          i ∘ h ∘ g-regular.h ≈⟨ extendʳ (⟺ f∘g≈i∘h) ⟩
          f ∘ g ∘ g-regular.h ≈⟨ refl⟩∘⟨ equality ⟩
          f ∘ g ∘ g-regular.g ≈⟨ extendʳ f∘g≈i∘h ⟩
          i ∘ h ∘ g-regular.g ∎

ExtremalEpi+Mono⇒IsIso : ExtremalEpi f → Mono f → IsIso f
ExtremalEpi+Mono⇒IsIso {f = f} f-extremal f-mono = extremal f-mono (⟺ identityʳ)
  where
    open ExtremalEpi f-extremal

--------------------------------------------------------------------------------
-- Extremal Monomorphisms

RegularMono⇒IsExtremalMono : ∀ {A B} {f : A ⇒ B} (m : RegularMono f) → IsExtremalMono (RegularMono⇒Mono m)
RegularMono⇒IsExtremalMono {A = A} {B = B} {f = f} regular {X = X} {g = k} {i = i} i-epi f≈k∘i =
  record
    { inv = i⁻¹
    ; iso = record
      { isoˡ = isoˡ
      ; isoʳ = isoʳ
      }
    }
    where
      open RegularMono regular renaming (g to r; h to s)
      open IsEqualizer equalizer

      i⁻¹ : X ⇒ A
      i⁻¹ = equalize $ i-epi (s ∘ k) (r ∘ k) $ begin
        (s ∘ k) ∘ i ≈⟨ pullʳ (⟺ f≈k∘i) ⟩
        s ∘ f       ≈⟨ equality ⟩
        r ∘ f       ≈⟨ pushʳ f≈k∘i ⟩
        (r ∘ k) ∘ i ∎

      isoˡ : i⁻¹ ∘ i ≈ id
      isoˡ = RegularMono⇒Mono regular (i⁻¹ ∘ i) id $ begin
        f ∘ i⁻¹ ∘ i ≈⟨ pullˡ (⟺ universal) ⟩
        k ∘ i       ≈˘⟨ f≈k∘i ⟩
        f           ≈˘⟨ identityʳ ⟩
        f ∘ id      ∎

      isoʳ : i ∘ i⁻¹ ≈ id
      isoʳ = i-epi (i ∘ i⁻¹) id $ begin
        (i ∘ i⁻¹) ∘ i ≈⟨ cancelʳ isoˡ ⟩
        i             ≈˘⟨ identityˡ ⟩
        id ∘ i        ∎

RegularMono⇒ExtremalMono : RegularMono f → ExtremalMono f
RegularMono⇒ExtremalMono m = record
  { mono = RegularMono⇒Mono m
  ; extremal = RegularMono⇒IsExtremalMono m
  }

ExtremalMono-∘₂ : ExtremalMono (f ∘ g) → ExtremalMono g
ExtremalMono-∘₂ fg-extremal = record
  { mono = Mono-∘₂ mono
  ; extremal = λ i-epi eq → extremal i-epi (pushʳ eq)
  }
  where
    open ExtremalMono fg-extremal

ExtremalMono-∘ : ∀ {A B C} {f : B ⇒ C} {g : A ⇒ B} → RegularMono f → ExtremalMono g → ExtremalMono (f ∘ g)
ExtremalMono-∘ {A = A} {B = B} {f = f} {g = g} f-regular g-extremal = record
  { mono = fg-mono
  ; extremal = fg-extremal
  }
  where
    module f-regular = RegularMono f-regular
    open IsEqualizer f-regular.equalizer
    module g-extremal = ExtremalMono g-extremal

    f-mono : Mono f
    f-mono = (RegularMono⇒Mono f-regular)

    fg-mono : Mono (f ∘ g)
    fg-mono = Mono-∘ f-mono g-extremal.mono

    fg-extremal : IsExtremalMono fg-mono
    fg-extremal {X = X} {g = h} {i = e} e-epi f∘g≈h∘e =
      g-extremal.extremal e-epi $ f-mono _ _ $ begin
      f ∘ g     ≈⟨ f∘g≈h∘e ⟩
      h ∘ e     ≈⟨ pushˡ universal ⟩
      f ∘ k ∘ e ∎
      where
        k : X ⇒ B
        k = equalize $ e-epi _ _ $ begin
          (f-regular.h ∘ h) ∘ e ≈⟨ extendˡ (⟺ f∘g≈h∘e) ⟩
          (f-regular.h ∘ f) ∘ g ≈⟨ equality ⟩∘⟨refl ⟩
          (f-regular.g ∘ f) ∘ g ≈⟨ extendˡ f∘g≈h∘e ⟩
          (f-regular.g ∘ h) ∘ e ∎

ExtremalMono+Epi⇒IsIso : ExtremalMono f → Epi f → IsIso f
ExtremalMono+Epi⇒IsIso {f = f} f-extremal f-epi = extremal f-epi (⟺ identityˡ)
  where
    open ExtremalMono f-extremal

--------------------------------------------------------------------------------
-- Extremal Morphisms in Balanced Categories
-- https://ncatlab.org/nlab/show/balanced+category

module _ (balanced : ∀ {A B} {f : A ⇒ B} → Mono f → Epi f → IsIso f) where

  Mono+Epi⇒IsExtremalEpi : (e : Epi f) → IsExtremalEpi e
  Mono+Epi⇒IsExtremalEpi {f = f} f-epi {i = i} {g = g} i-mono f≈i∘g = balanced i-mono i-epi
    where
      i-epi : Epi i
      i-epi g₁ g₂ g₁∘i≈g₂∘i = f-epi g₁ g₂ $ begin
        g₁ ∘ f       ≈⟨ pushʳ f≈i∘g ⟩
        (g₁ ∘ i) ∘ g ≈⟨ g₁∘i≈g₂∘i ⟩∘⟨refl ⟩
        (g₂ ∘ i) ∘ g ≈⟨ pullʳ (⟺ f≈i∘g) ⟩
        g₂ ∘ f ∎

  Mono+Epi⇒IsExtremalMono : (m : Mono f) → IsExtremalMono m
  Mono+Epi⇒IsExtremalMono {f = f} f-mono {g = g} {i = i} i-epi f≈g∘i = balanced i-mono i-epi
    where
      i-mono : Mono i
      i-mono g₁ g₂ i∘g₁≈i∘g₂ = f-mono g₁ g₂ $ begin
        f ∘ g₁     ≈⟨ pushˡ f≈g∘i ⟩
        g ∘ i ∘ g₁ ≈⟨ refl⟩∘⟨ i∘g₁≈i∘g₂ ⟩
        g ∘ i ∘ g₂ ≈⟨ pullˡ (⟺ f≈g∘i) ⟩
        f ∘ g₂     ∎

max_stars_repo_name: maxsnew/agda-categories

max_issues_repo_name: maxsnew/agda-categories

max_forks_repo_name: maxsnew/agda-categories


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

open import Cubical.Foundations.Prelude
open import Cubical.Data.Int renaming (Int to IntType ; _+_ to _+Int_ ; _-_ to _-Int_; -_ to -Int_ ; _·_ to _·Int_)
open import Cubical.Algebra.Group.Base

open GroupStr

Int : Group₀
fst Int = IntType
1g (snd Int) = 0
_·_ (snd Int) = _+Int_
inv (snd Int) = _-Int_ 0
isGroup (snd Int) = isGroupInt
  where
  abstract
    isGroupInt : IsGroup (pos 0) _+Int_ (_-Int_ (pos 0))
    isGroupInt = makeIsGroup isSetInt +-assoc (λ x → refl) (λ x → +-comm 0 x)
                              (λ x → +-comm x (pos 0 -Int x) ∙ minusPlus x 0) (λ x → minusPlus x 0)

max_stars_repo_name: jespercockx/cubical

max_issues_repo_name: jespercockx/cubical

max_forks_repo_name: jespercockx/cubical


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

-- This module implements the dependent Σ-type.
module hott.core.sigma where

open import hott.core.universe

record Σ {ℓ₀ ℓ₁}
         {A : Type ℓ₀}
         (B : A → Type ℓ₁) : Type (ℓ₀ ⊔ ℓ₁) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

-- The product type is just the non-dependent Σ-type.
_×_ : ∀{ℓ₀ ℓ₁} (A : Type ℓ₀)
       (B : Type ℓ₁) →  Type (ℓ₀ ⊔ ℓ₁)
A × B = Σ λ (_ : A) → B

-- Since the , constructor is infixr, we can write (a , (b , c)) as
-- just (a , b , c). The convention that we follow for tuples is that
-- of a list. We assign the paring function the least precedence
-- because we would like to write all other stuff inside the tuple
-- naturally e.g. (p ≡ q , q ≡ r) etc. We ensure that no other
-- operator has 0 precedence.
infixr 0 _,_
infixr 0 _×_

-- The projection to the first component.
fst : ∀{ℓ₀ ℓ₁} {A : Type ℓ₀} {B : A → Type ℓ₁}
    → Σ B → A
fst = Σ.proj₁

-- The projection to the second component.
snd : ∀{ℓ₀ ℓ₁} {A : Type ℓ₀} {B : A → Type ℓ₁}
    → (σ : Σ B) →  B (fst σ)
snd = Σ.proj₂

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


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

open import Categories.Category.Core
open import Categories.Comonad

-- verbatim dual of Categories.Adjoint.Construction.EilenbergMoore
module Categories.Adjoint.Construction.CoEilenbergMoore {o ℓ e} {C : Category o ℓ e} (M : Comonad C) where

open import Categories.Category.Construction.CoEilenbergMoore M
open import Categories.Adjoint
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
open import Categories.NaturalTransformation.Core
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
open import Categories.Morphism.Reasoning C

private
  module C = Category C
  module M = Comonad M
  open M.F
  open C
  open HomReasoning
  open Equiv

Forgetful : Functor CoEilenbergMoore C
Forgetful = record
  { F₀           = Comodule.A
  ; F₁           = Comodule⇒.arr
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = λ eq → eq
  }

Cofree : Functor C CoEilenbergMoore
Cofree = record
 { F₀ = λ A → record
  { A = F₀ A
  ; coaction = M.δ.η A
  ; commute = M.sym-assoc
  ; identity = Comonad.identityʳ M
  }
 ; F₁ = λ f → record
  { arr = F₁ f
  ; commute = M.δ.commute f
  }
 ; identity = identity
 ; homomorphism = homomorphism
 ; F-resp-≈ = F-resp-≈
 }

UC≃M : Forgetful ∘F Cofree ≃ M.F
UC≃M = niHelper (record
 { η = λ _ → F₁ C.id
 ; η⁻¹ = λ _ → F₁ C.id
 ; commute = λ f → [ M.F ]-resp-square id-comm-sym
 ; iso = λ _ → record
    { isoˡ = elimˡ identity ○ identity
    ; isoʳ = elimˡ identity ○ identity
    }
 })

Forgetful⊣Cofree : Forgetful ⊣ Cofree
Forgetful⊣Cofree = record
 { unit = record
  { η = λ X → let module X = Comodule X
      in record
        { arr     = X.coaction
        ; commute = ⟺ X.commute
        }
  ; commute = Comodule⇒.commute
  ; sym-commute = λ f → ⟺ (Comodule⇒.commute f)
  }
 ; counit = record
  { η = M.ε.η
  ; commute = M.ε.commute
  ; sym-commute = M.ε.sym-commute
  }
 ; zig = λ {A} → Comodule.identity A
 ; zag = λ {B} → Comonad.identityˡ M
 }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------------
-- Axiomatic Peano arithmetic base
------------------------------------------------------------------------------

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

module PA.Axiomatic.Standard.Base where

infixl 7 _*_
infixl 6 _+_

------------------------------------------------------------------------------
-- First-order logic with equality.
open import Common.FOL.FOL-Eq public renaming ( D to ℕ )

-- Common definitions.
open import Common.DefinitionsATP

-- Non-logical constants
postulate
  zero    : ℕ
  succ    : ℕ → ℕ
  _+_ _*_ : ℕ → ℕ → ℕ

-- Proper axioms
-- From (Machover 1996, p. 263) and (Hájek and Pudlák 1998, p. 28):
--
-- PA₁. 0 ≠ n'
-- PA₂. m' = n' → m = n
-- PA₃. 0 + n = n
-- PA₄. m' + n = (m + n)'
-- PA₅. 0 * n = 0
-- PA₆. m' * n = n + (m * n)
-- Axiom of induction:
-- φ(0) → (∀n.φ(n) → φ(succ n)) → ∀n.φ(n), for any formulae φ

postulate
  PA₁ : ∀ {n} → zero ≢ succ n
  PA₂ : ∀ {m n} → succ m ≡ succ n → m ≡ n
  PA₃ : ∀ n → zero + n ≡ n
  PA₄ : ∀ m n → succ m + n ≡ succ (m + n)
  PA₅ : ∀ n → zero * n ≡ zero
  PA₆ : ∀ m n → succ m * n ≡ n + m * n
{-# ATP axioms PA₁ PA₂ PA₃ PA₄ PA₅ PA₆ #-}

-- The axiom of induction is an axiom schema, therefore we do not
-- translate it to TPTP.
postulate
  ℕ-ind : (A : ℕ → Set) → A zero → (∀ n → A n → A (succ n)) → ∀ n → A n

------------------------------------------------------------------------------
-- References
--
-- Machover, Moshé (1996). Set theory, Logic and their
-- Limitations. Cambridge University Press.

-- Hájek, Petr and Pudlák, Pavel (1998). Metamathematics of
-- First-Order Arithmetic. 2nd printing. Springer.


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

module Data.ByteString.IO where

import Data.ByteString.Primitive as Prim
open import Data.ByteString

open import Data.Word8 using (Word8)
open import Data.Nat using (ℕ)
open import Data.Colist using (Colist)
open import Data.List using (List)
open import Data.String using (String)

open import IO using (IO; _>>_; _>>=_; lift; return)
open import Data.Unit using (⊤)
open import Coinduction using (♯_)

readBinaryFile : ∀ {k} → String → IO (ByteString k)
readBinaryFile {Lazy} f = lift (Prim.readBinaryFileLazy f)
readBinaryFile {Strict} f = lift (Prim.readBinaryFileStrict f)

readBinaryFile′ : ∀ {k} → String → IO (ByteStringRep k)
readBinaryFile′ {k} f = ♯ readBinaryFile f >>= (λ bs → ♯ return (unpack bs))

writeBinaryFile : ∀ {k} → String → ByteString k → IO ⊤
writeBinaryFile {Lazy} f s =
  ♯ lift (Prim.writeBinaryFileLazy f s) >>
  ♯ return _
writeBinaryFile {Strict} f s =
  ♯ lift (Prim.writeBinaryFileStrict f s) >>
  ♯ return _

writeBinaryFile′ : ∀ {k} → String → ByteStringRep k → IO ⊤
writeBinaryFile′ {k} f bs = writeBinaryFile f (pack bs)

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
------------------------------------------------------------------------------
-- Mutual recursive functions
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.MutualRecursiveFunctions where

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

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

postulate
  even : D → D
  odd  : D → D

  even-0 : even zero            ≡ true
  even-S : ∀ d → even (succ₁ d) ≡ odd d

  odd-0 : odd zero            ≡ false
  odd-S : ∀ d → odd (succ₁ d) ≡ even d
{-# ATP axioms even-0 even-S odd-0 odd-S #-}

postulate even-2 : even 2' ≡ true
{-# ATP prove even-2 #-}

postulate even-3 : even 3' ≡ false
{-# ATP prove even-3 #-}

postulate odd-2 : odd 2' ≡ false
{-# ATP prove odd-2 #-}

postulate odd-3 : odd 3' ≡ true
{-# ATP prove odd-3 #-}


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

module Mergesort.Impl1 {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Bound.Lower A
open import Bound.Lower.Order  _≤_
open import Data.Product
open import Data.Sum
open import Size
open import SList
open import SOList.Lower _≤_

deal : {ι : Size} → SList A {ι} → SList A {ι} × SList A {ι}
deal snil = (snil , snil)
deal (x ∙ snil) = (x ∙ snil , snil)
deal (x ∙ (y ∙ xs))
    with deal xs
... | (ys , zs) = (x ∙ ys , y ∙ zs)

merge : {ι ι' : Size}{b : Bound} → SOList {ι} b  → SOList {ι'} b → SOList b
merge onil ys = ys
merge xs onil = xs
merge (:< {x = x} b≤x xs)  (:< {x = y} b≤y ys)
    with tot≤ x y
... | inj₁ x≤y = :< b≤x (merge xs (:< (lexy x≤y) ys))
... | inj₂ y≤x = :< b≤y (merge (:< (lexy y≤x) xs) ys)

mergesort : {ι : Size} → SList A {↑ ι} → SOList bot
mergesort snil = onil
mergesort (x ∙ snil) = :< {x = x} lebx onil
mergesort (x ∙ (y ∙ xs))
    with deal xs
... | (ys , zs) = merge (mergesort (x ∙ ys)) (mergesort (y ∙ zs))

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


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

open import Categories.Category

module Categories.Category.BicartesianClosed {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open import Categories.Category.CartesianClosed 𝒞
open import Categories.Category.Cocartesian 𝒞

record BicartesianClosed : Set (levelOfTerm 𝒞) where
  field
    cartesianClosed : CartesianClosed
    cocartesian     : Cocartesian

  module cartesianClosed = CartesianClosed cartesianClosed
  module cocartesian     = Cocartesian cocartesian

  open cartesianClosed public
  open cocartesian public

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
open import Prelude

open import Data.Nat
open import Data.Nat.Properties
open import Induction.Nat

module Implicits.Resolution.GenericFinite.Examples.MaximumDepth
  where

open import Implicits.Resolution.GenericFinite.TerminationCondition

_<′?_ : (x y : ℕ) → Dec (x <′ y)
x <′? y with (suc x) ≤? y
x <′? y | yes p = yes (≤⇒≤′ p)
x <′? y | no ¬p = no (λ p → ¬p (≤′⇒≤ p))

MaxDepthCondition : TerminationCondition
MaxDepthCondition = record
  {  TCtx = ℕ
  ; _<_  = _<′_
  ; _<?_  = _<′?_
  ; step = λ n _ _ _ _ → n ∸ 1
  ; wf-< = <-well-founded
  }


text:
-- Andreas, 2016-10-03, re issue #2231
-- Testing whether the
{-# OPTIONS --guardedness-preserving-type-constructors #-}
-- stuff works in abstract blocks

-- {-# OPTIONS -v term:30 -v tc.term.expr.coind:100 #-}

module AbstractGuardednessPreservingTypeConstructors where

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}

-- Preliminaries.

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

data Bool : Set where
  true false : Bool

data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

-- Σ cannot be a record type below.

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (x : A) → B x → Σ A B

syntax Σ A (λ x → B) = Σ[ x ∶ A ] B

data Rec (A : ∞ Set) : Set where
  fold : ♭ A → Rec A

abstract

  -- Corecursive definition of the natural numbers.

  ℕ : Set
  ℕ = ⊤ ⊎ Rec (♯ ℕ)

  zero : ℕ
  zero = inj₁ _

  suc : ℕ → ℕ
  suc n = inj₂ (fold n)

  ℕ-rec : (P : ℕ → Set) →
          P zero →
          (∀ n → P n → P (suc n)) →
          ∀ n → P n
  ℕ-rec P z s (inj₁ _)        = z
  ℕ-rec P z s (inj₂ (fold n)) = s n (ℕ-rec P z s n)

  -- Corecursive definition of the W-type.

  W : (A : Set) → (A → Set) → Set
  W A B = Rec (♯ (Σ[ x ∶ A ] (B x → W A B)))

  syntax W A (λ x → B) = W[ x ∶ A ] B

  sup : {A : Set} {B : A → Set} (x : A) (f : B x → W A B) → W A B
  sup x f = fold (x , f)

  W-rec : {A : Set} {B : A → Set}
          (P : W A B → Set) →
          (∀ {x} {f : B x → W A B} → (∀ y → P (f y)) → P (sup x f)) →
          ∀ x → P x
  W-rec P h (fold (x , f)) = h (λ y → W-rec P h (f y))

-- Induction-recursion encoded as corecursion-recursion.

-- The following definitions are needed on the type level, so we cannot make them abstract.

data Label : Set where
  ′0 ′1 ′2 ′σ ′π ′w : Label

mutual

  U : Set
  U = Σ Label U′

  U′ : Label → Set
  U′ ′0 = ⊤
  U′ ′1 = ⊤
  U′ ′2 = ⊤
  U′ ′σ = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
  U′ ′π = Rec (♯ (Σ[ a ∶ U ] (El a → U)))
  U′ ′w = Rec (♯ (Σ[ a ∶ U ] (El a → U)))

  El : U → Set
  El (′0 , _)            = ⊥
  El (′1 , _)            = ⊤
  El (′2 , _)            = Bool
  El (′σ , fold (a , b)) = Σ[ x ∶ El a ]  El (b x)
  El (′π , fold (a , b)) =   (x : El a) → El (b x)
  El (′w , fold (a , b)) = W[ x ∶ El a ]  El (b x)

-- The recursor can be abstract.

abstract

  U-rec : (P : ∀ u → El u → Set) →
          P (′1 , _) tt →
          P (′2 , _) true →
          P (′2 , _) false →
          (∀ {a b x y} →
           P a x → P (b x) y → P (′σ , fold (a , b)) (x , y)) →
          (∀ {a b f} →
           (∀ x → P (b x) (f x)) → P (′π , fold (a , b)) f) →
          (∀ {a b x f} →
           (∀ y → P (′w , fold (a , b)) (f y)) →
           P (′w , fold (a , b)) (sup x f)) →
          ∀ u (x : El u) → P u x
  U-rec P P1 P2t P2f Pσ Pπ Pw = rec
    where
    rec : ∀ u (x : El u) → P u x
    rec (′0 , _)            ()
    rec (′1 , _)            _              = P1
    rec (′2 , _)            true           = P2t
    rec (′2 , _)            false          = P2f
    rec (′σ , fold (a , b)) (x , y)        = Pσ (rec _ x) (rec _ y)
    rec (′π , fold (a , b)) f              = Pπ (λ x → rec _ (f x))
    rec (′w , fold (a , b)) (fold (x , f)) = Pw (λ y → rec _ (f y))

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
{-# OPTIONS --allow-unsolved-metas #-}
module nat where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary
open import  Relation.Binary.PropositionalEquality
open import  Relation.Binary.Core
open import Relation.Binary.Definitions
open import  logic

nat-<> : { x y : ℕ } → x < y → y < x → ⊥
nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x

nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x

nat-<≡ : { x : ℕ } → x < x → ⊥
nat-<≡  (s≤s lt) = nat-<≡ lt

nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
nat-≡< refl lt = nat-<≡ lt

¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
¬a≤a  (s≤s lt) = ¬a≤a  lt

a<sa : {la : ℕ} → la < suc la
a<sa {zero} = s≤s z≤n
a<sa {suc la} = s≤s a<sa

refl-≤s : {x : ℕ } → x ≤ suc x
refl-≤s {zero} = z≤n
refl-≤s {suc x} = s≤s (refl-≤s {x})

a≤sa : {x : ℕ } → x ≤ suc x
a≤sa {zero} = z≤n
a≤sa {suc x} = s≤s (a≤sa {x})

=→¬< : {x : ℕ  } → ¬ ( x < x )
=→¬< {zero} ()
=→¬< {suc x} (s≤s lt) = =→¬< lt

>→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x

<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
<-∨ {zero} {zero} (s≤s z≤n) = case1 refl
<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n)
<-∨ {suc x} {zero} (s≤s ())
<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt
<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)

n≤n : (n : ℕ) →  n Data.Nat.≤ n
n≤n zero = z≤n
n≤n (suc n) = s≤s (n≤n n)

<→m≤n : {m n : ℕ} → m  < n →  m Data.Nat.≤ n
<→m≤n {zero} lt = z≤n
<→m≤n {suc m} {zero} ()
<→m≤n {suc m} {suc n} (s≤s lt) = s≤s (<→m≤n lt)

max : (x y : ℕ) → ℕ
max zero zero = zero
max zero (suc x) = (suc x)
max (suc x) zero = (suc x)
max (suc x) (suc y) = suc ( max x y )

-- _*_ : ℕ → ℕ → ℕ
-- _*_ zero _ = zero
-- _*_ (suc n) m = m + ( n * m )

exp : ℕ → ℕ → ℕ
exp _ zero = 1
exp n (suc m) = n * ( exp n m )

minus : (a b : ℕ ) →  ℕ
minus a zero = a
minus zero (suc b) = zero
minus (suc a) (suc b) = minus a b

_-_ = minus

m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
m+= {i} {j} {zero} refl = refl
m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )

+m= : {i j  m : ℕ } → i + m ≡ j + m → i ≡ j
+m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )

less-1 :  { n m : ℕ } → suc n < m → n < m
less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)

sa=b→a<b :  { n m : ℕ } → suc n ≡ m → n < m
sa=b→a<b {0} {suc zero} refl = s≤s z≤n
sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)

minus+n : {x y : ℕ } → suc x > y  → minus x y + y ≡ x
minus+n {x} {zero} _ = trans (sym (+-comm zero  _ )) refl
minus+n {zero} {suc y} (s≤s ())
minus+n {suc x} {suc y} (s≤s lt) = begin
           minus (suc x) (suc y) + suc y
        ≡⟨ +-comm _ (suc y)    ⟩
           suc y + minus x y
        ≡⟨ cong ( λ k → suc k ) (
           begin
                 y + minus x y
              ≡⟨ +-comm y  _ ⟩
                 minus x y + y
              ≡⟨ minus+n {x} {y} lt ⟩
                 x
           ∎
           ) ⟩
           suc x
        ∎  where open ≡-Reasoning

sn-m=sn-m : {m n : ℕ } →  m ≤ n → suc n - m ≡ suc ( n - m )
sn-m=sn-m {0} {n} z≤n = refl
sn-m=sn-m {suc m} {suc n} (s≤s m<n) = sn-m=sn-m m<n

si-sn=i-n : {i n : ℕ } → n < i  → suc (i - suc n) ≡ (i - n)
si-sn=i-n {i} {n} n<i = begin
   suc (i - suc n) ≡⟨ sym (sn-m=sn-m n<i )  ⟩
   suc i - suc n ≡⟨⟩
   i - n
   ∎  where
      open ≡-Reasoning

n-m<n : (n m : ℕ ) →  n - m ≤ n
n-m<n zero zero = z≤n
n-m<n (suc n) zero = s≤s (n-m<n n zero)
n-m<n zero (suc m) = z≤n
n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s

n-n-m=m : {m n : ℕ } → m ≤ n  → m ≡ (n - (n - m))
n-n-m=m {0} {zero} z≤n = refl
n-n-m=m {0} {suc n} z≤n = n-n-m=m {0} {n} z≤n
n-n-m=m {suc m} {suc n} (s≤s m≤n) = sym ( begin
   suc n - ( n - m )    ≡⟨ sn-m=sn-m (n-m<n  n m) ⟩
   suc (n - ( n - m ))  ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩
   suc m
   ∎  ) where
      open ≡-Reasoning

0<s : {x : ℕ } → zero < suc x
0<s {_} = s≤s z≤n

<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
<-minus-0 {x} {suc _} {zero} lt = lt
<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt

<-minus : {x y z : ℕ } → x + z < y + z → x < y
<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )

x≤x+y : {z y : ℕ } → z ≤ z + y
x≤x+y {zero} {y} = z≤n
x≤x+y {suc z} {y} = s≤s  (x≤x+y {z} {y})

<-plus : {x y z : ℕ } → x < y → x + z < y + z
<-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
<-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)

<-plus-0 : {x y z : ℕ } → x < y → z + x < z + y
<-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )

≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
≤-plus {0} {y} {zero} z≤n = z≤n
≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y
≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )

≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y
≤-plus-0 {x} {y} {zero} lt = lt
≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )

x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z
x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )

*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z
*≤ lt = *-mono-≤ lt ≤-refl

*< : {x y z : ℕ } → x < y → x * suc z < y * suc z
*< {zero} {suc y} lt = s≤s z≤n
*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)

<to<s : {x y  : ℕ } → x < y → x < suc y
<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)

<tos<s : {x y  : ℕ } → x < y → suc x < suc y
<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)

≤to< : {x y  : ℕ } → x < y → x ≤ y
≤to< {zero} {suc y} (s≤s z≤n) = z≤n
≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y}  lt)

x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)

open import Data.Product

minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
minus<=0 {0} {zero} z≤n = refl
minus<=0 {0} {suc y} z≤n = refl
minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le

minus>0 : {x y : ℕ } → x < y → 0 < minus y x
minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt

distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z)
distr-minus-* {x} {zero} {z} = refl
distr-minus-* {x} {suc y} {z} with <-cmp x y
distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
          minus x (suc y) * z
        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
           0 * z
        ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
          minus (x * z) (z + y * z)
        ∎  where
            open ≡-Reasoning
            le : x * z ≤ z + y * z
            le  = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
               lemma : x * z ≤ y * z
               lemma = *≤ {x} {y} {z} (≤to< a)
distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
          minus x (suc y) * z
        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
           0 * z
        ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
          minus (x * z) (z + y * z)
        ∎  where
            open ≡-Reasoning
            lt : {x z : ℕ } →  x * z ≤ z + x * z
            lt {zero} {zero} = z≤n
            lt {suc x} {zero} = lt {x} {zero}
            lt {x} {suc z} = ≤-trans lemma refl-≤s where
               lemma : x * suc z ≤   z + x * suc z
               lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z})
distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
           minus x (suc y) * z + suc y * z
        ≡⟨ sym (proj₂ *-distrib-+ z  (minus x (suc y) )  _) ⟩
           ( minus x (suc y) + suc y ) * z
        ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c))  ⟩
           x * z
        ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
           minus (x * z) (suc y * z) + suc y * z
        ∎ ) where
            open ≡-Reasoning
            lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
            lt {x} {y} {z} le = *≤ le

minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
           minus (minus x y) z + z
        ≡⟨ minus+n {_} {z} lemma ⟩
           minus x y
        ≡⟨ +m= {_} {_} {y} ( begin
              minus x y + y
           ≡⟨ minus+n {_} {y} lemma1 ⟩
              x
           ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩
              minus x (z + y) + (z + y)
           ≡⟨ sym ( +-assoc (minus x (z + y)) _  _ ) ⟩
              minus x (z + y) + z + y
           ∎ ) ⟩
           minus x (z + y) + z
        ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y )  ⟩
           minus x (y + z) + z
        ∎  ) where
             open ≡-Reasoning
             lemma1 : suc x > y
             lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt )
             lemma : suc (minus x y) > z
             lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y}  lemma1 ))  gt )

minus-* : {M k n : ℕ } → n < k  → minus k (suc n) * M ≡ minus (minus k n * M ) M
minus-* {zero} {k} {n} lt = begin
           minus k (suc n) * zero
        ≡⟨ *-comm (minus k (suc n)) zero ⟩
           zero * minus k (suc n)
        ≡⟨⟩
           0 * minus k n
        ≡⟨ *-comm 0 (minus k n) ⟩
           minus (minus k n * 0 ) 0
        ∎  where
        open ≡-Reasoning
minus-* {suc m} {k} {n} lt with <-cmp k 1
minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl
minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl
minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl
minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt
minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c
minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
           minus k (suc n) * M
        ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
           minus (k * M ) ((suc n) * M)
        ≡⟨⟩
           minus (k * M ) (M + n * M  )
        ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
           minus (k * M ) ((n * M) + M )
        ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩
           minus (minus (k * M ) (n * M)) M
        ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
           minus (minus k n * M ) M
        ∎  where
             M = suc m
             lemma : {n k m : ℕ } → n < k  → suc (k * suc m) > suc m + n * suc m
             lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
             lemma {suc n} {suc k} {m} lt = begin
                         suc (suc m + suc n * suc m)
                      ≡⟨⟩
                         suc ( suc (suc n) * suc m)
                      ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
                         suc (suc k * suc m)
                      ∎   where open ≤-Reasoning
             open ≡-Reasoning

open import Data.List

ℕL-inject : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → h ≡ h1
ℕL-inject refl = refl

ℕL-inject-t : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → x ≡ y
ℕL-inject-t refl = refl

ℕL-eq? : (x y : List ℕ ) → Dec (x ≡ y )
ℕL-eq? [] [] = yes refl
ℕL-eq? [] (x ∷ y) = no (λ ())
ℕL-eq? (x ∷ x₁) [] = no (λ ())
ℕL-eq? (h ∷ x) (h1 ∷ y) with h ≟ h1 | ℕL-eq? x y
... | yes y1 | yes y2 = yes ( cong₂ (λ j k → j ∷ k ) y1 y2 )
... | yes y1 | no n = no (λ e → n (ℕL-inject-t e))
... | no n  | t = no (λ e → n (ℕL-inject e))

max_stars_repo_name: shinji-kono/Galois

max_issues_repo_name: shinji-kono/Galois

max_forks_repo_name: shinji-kono/Galois


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

module Categories.Functor.Instance.UnderlyingQuiver where

-- The forgetful functor from categories to its underlying quiver
-- **except** that this functor only goes from **StrictCats**,
-- i.e. where Functor equivalence is propositional equality, not
-- NaturalIsomorphism.

open import Level using (Level)
-- open import Function using (_$_; flip)
open import Relation.Binary.PropositionalEquality
  using (refl)
open import Relation.Binary.PropositionalEquality.Subst.Properties
  using (module Transport)
open import Data.Quiver using (Quiver)
open import Data.Quiver.Morphism using (Morphism; _≃_)

open import Categories.Category.Core using (Category)
open import Categories.Category.Instance.Quivers using (Quivers)
open import Categories.Category.Instance.StrictCats
open import Categories.Functor using (Functor)
open import Categories.Functor.Equivalence using (_≡F_)
import Categories.Morphism.HeterogeneousIdentity as HId

private
  variable
    o ℓ e o′ ℓ′ e′ : Level
    A B : Category o ℓ e

Underlying₀ : Category o ℓ e → Quiver o ℓ e
Underlying₀ C = record { Category C }

Underlying₁ : Functor A B → Morphism (Underlying₀ A) (Underlying₀ B)
Underlying₁ F = record { Functor F }

private
 ≡F-resp-≃ : {F G : Functor A B} → F ≡F G → Underlying₁ F ≃ Underlying₁ G
 ≡F-resp-≃ {B = B} {F} {G} F≈G = record
    { F₀≡ = λ {X} → eq₀ F≈G X
    ; F₁≡ = λ {x} {y} {f} →
      let open Category B using (_∘_)
          open HId B
          UB = Underlying₀ B
          open Transport (Quiver._⇒_ UB) using (_▸_; _◂_)
          module F = Functor F using (₁)
          module G = Functor G using (₁)
          open Quiver.EdgeReasoning (Underlying₀ B)
      in begin
        F.₁ f ▸ eq₀ F≈G y         ≈⟨ hid-subst-cod (F.₁ f) (eq₀ F≈G y) ⟩
        hid (eq₀ F≈G y) ∘ F.₁ f   ≈⟨ eq₁ F≈G f ⟩
        G.₁ f ∘ hid (eq₀ F≈G x)   ≈˘⟨ hid-subst-dom (eq₀ F≈G x) (G.₁ f) ⟩
        eq₀ F≈G x ◂ G.₁ f         ∎
    }
    where open _≡F_

Underlying : Functor (StrictCats o ℓ e) (Quivers o ℓ e)
Underlying = record
  { F₀ = Underlying₀
  ; F₁ = Underlying₁
  ; identity = λ {A} → record { F₀≡ = refl ; F₁≡ = Category.Equiv.refl A }
  ; homomorphism = λ where {Z = Z} → record { F₀≡ = refl ; F₁≡ = Category.Equiv.refl Z }
  ; F-resp-≈ = ≡F-resp-≃
  }

max_stars_repo_name: sstucki/agda-categories

max_issues_repo_name: sstucki/agda-categories

max_forks_repo_name: sstucki/agda-categories


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

open import Basics
open import Pr
open import Nom
import Kind
open Kind Gnd U El
import Cxt
open Cxt Kind
import Loc
open Loc Kind
import Term
open Term Gnd U El
import Shift
open Shift Gnd U El

data Sawn (G : Cxt)(C : Kind)(L : Loc)(R : Kind) : Kind -> Set where
  snil : Sawn G C L R R
  scons : {S T : Kind} -> Sawn G C L R (S |> T) ->
                          G [ L / Term C ]- S ->
                          Sawn G C L R T
  sarg : {A : U}{K : El A -> Kind} ->
         Sawn G C L R (Pi A K) -> (a : El A) ->
         Sawn G C L R (K a)

stitch : {G : Cxt}{C : Kind}{Z : Gnd}{L : Loc}{R S : Kind} ->
         Sawn G C L R S -> G [ L / Args C Z ]- S -> G [ L / Args C Z ]- R
stitch snil s = s
stitch (scons r s) t = stitch r (s G& t)
stitch (sarg r a) t = stitch r (a G^ t)

sawsh : {G : Cxt}{C : Kind}{L M : Loc} ->
        ({T : Kind} -> G [ L / Head ]- T -> G [ M / Head ]- T) ->
        {R S : Kind} -> Sawn G C L R S -> Sawn G C M R S
sawsh rho snil = snil
sawsh rho (scons r s) = scons (sawsh rho r) (shift rho s)
sawsh rho (sarg r a) = sarg (sawsh rho r) a

long : {G : Cxt}{C : Kind}{L : Loc}(S : Kind){T : Kind} ->
       G [ L / Head ]- T ->
       Sawn G C L T S ->
       G [ L / Term C ]- S
long (Ty Z)   h s = h G$ (stitch s Gnil)
long (Pi A K) h s = Gfn A \ a -> long (K a) h (sarg s a)
long (S |> T) h s =
  G\\ (long T (popH h) (scons (sawsh popH s) (long S (# top -! _) snil)))

var : {G : Cxt}{C : Kind}(x : Nom){Gx : [| G Has x |]} ->
      G [ EL / Term C ]- (wit ((G ?- x) {Gx}))
var {G} x {Gx} with (G ?- x) {Gx}
... | [ T / g ] = long T (` x -! g) snil


text:
module Structure.Groupoid.Groupoids where

open import Data
open import Data.Proofs
open import Functional
open import Logic
import      Lvl
import      Relator.Equals as Eq
open import Structure.Setoid
open import Structure.Groupoid
open import Structure.Categorical.Proofs
open import Structure.Categorical.Properties
open import Structure.Operator
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ : Lvl.Level
private variable Obj A B : Type{ℓ}
private variable _▫_ : Obj → Obj → Type{ℓ}
private variable f : A → B

emptyGroupoid : Groupoid{ℓ₁}{ℓ₂}{ℓₑ}(empty-morphism) ⦃ \{} ⦄
Groupoid._∘_            emptyGroupoid = empty-comp
Groupoid.id             emptyGroupoid = empty-id
Groupoid.inv            emptyGroupoid = empty-inv
Groupoid.binaryOperator emptyGroupoid {}
Groupoid.associativity  emptyGroupoid = empty-associativity ⦃ \{} ⦄
Groupoid.identity       emptyGroupoid = empty-identity ⦃ \{} ⦄
Groupoid.inverter       emptyGroupoid = empty-inverter ⦃ \{} ⦄

singleGroupoid : ∀{ℓₒ ℓᵢ ℓₚₐ₁ ℓₚₐ₂ ℓₚᵢ₁ ℓₚᵢ₂ ℓₚᵢ₃ ℓᵢₙ : Lvl.Level} → Groupoid{ℓ₁}{ℓ₂}(single-morphism)
Groupoid._∘_ (singleGroupoid{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}) = single-comp{ℓ₂}{ℓₒ}
Groupoid.id  (singleGroupoid{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}) = single-id{ℓ₂}{ℓᵢ}
Groupoid.inv (singleGroupoid{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}) = single-inv{ℓ₂}{ℓᵢ}
BinaryOperator.congruence (Groupoid.binaryOperator singleGroupoid) Eq.[≡]-intro Eq.[≡]-intro = Eq.[≡]-intro
Groupoid.associativity (singleGroupoid{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}) = single-associativity{ℓ₂}{ℓ₂}{ℓₚₐ₁}{ℓ₁}{ℓₚₐ₂}
Groupoid.identity      (singleGroupoid{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}) = single-identity{ℓ₂}{ℓ₂}{ℓₚᵢ₁}{ℓ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}
Groupoid.inverter      (singleGroupoid{ℓ₁}{ℓ₂}{ℓₒ}{ℓᵢ}{ℓₚₐ₁}{ℓₚₐ₂}{ℓₚᵢ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}{ℓᵢₙ}) = single-inverter{ℓ₂}{ℓ₂}{ℓₚᵢ₁}{ℓ₁}{ℓₚᵢ₂}{ℓₚᵢ₃}{ℓᵢₙ}

on₂-groupoid : ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}{ℓ}(x ▫ y) ⦄ → Groupoid{Obj = B}(_▫_) ⦃ morphism-equiv ⦄ → (f : A → B) → Groupoid((_▫_) on₂ f)
Groupoid._∘_ (on₂-groupoid C _) = Groupoid._∘_ C
Groupoid.id  (on₂-groupoid C _) = Groupoid.id  C
Groupoid.inv (on₂-groupoid C _) = Groupoid.inv C
BinaryOperator.congruence (Groupoid.binaryOperator (on₂-groupoid C _)) = BinaryOperator.congruence(Groupoid.binaryOperator C)
Groupoid.associativity (on₂-groupoid C f) = on₂-associativity f (Groupoid.associativity C)
Groupoid.identity      (on₂-groupoid C f) = on₂-identity f (Groupoid.identity C)
Groupoid.inverter      (on₂-groupoid C f) = on₂-inverter f (Groupoid.inverter C)

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:
-- Andreas, 2012-10-18
module Issue481a where

open import Common.Issue481ParametrizedModule Set1

--  ommon.Issue481ParametrizedModule should not be in scope
module PM = Common.Issue481ParametrizedModule

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The free monad construction on containers
------------------------------------------------------------------------

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

module Data.Container.FreeMonad where

open import Level
open import Data.Sum using (inj₁; inj₂ ; [_,_]′)
open import Data.Product
open import Data.Container
open import Data.Container.Combinator using (const; _⊎_)
open import Data.W
open import Category.Monad

infixl 1 _⋆C_
infix  1 _⋆_

------------------------------------------------------------------------
-- The free monad construction over a container and a set is, in
-- universal algebra terminology, also known as the term algebra over a
-- signature (a container) and a set (of variable symbols). The return
-- of the free monad corresponds to variables and the bind operator
-- corresponds to (parallel) substitution.

-- A useful intuition is to think of containers describing single
-- operations and the free monad construction over a container and a set
-- describing a tree of operations as nodes and elements of the set as
-- leafs. If one starts at the root, then any path will pass finitely
-- many nodes (operations described by the container) and eventually end
-- up in a leaf (element of the set) -- hence the Kleene star notation
-- (the type can be read as a regular expression).

_⋆C_ : ∀ {x s p} → Container s p → Set x → Container (s ⊔ x) p
C ⋆C X = const X ⊎ C

_⋆_ : ∀ {x s p} → Container s p → Set x → Set (x ⊔ s ⊔ p)
C ⋆ X = μ (C ⋆C X)

module _ {s p} {C : Container s p} where

  inn : ∀ {x} {X : Set x} → ⟦ C ⟧ (C ⋆ X) → C ⋆ X
  inn (s , f) = sup (inj₂ s , f)

  rawMonad : ∀ {x} → RawMonad {s ⊔ p ⊔ x} (C ⋆_)
  rawMonad = record { return = return; _>>=_ = _>>=_ }
    where
    return : ∀ {X} → X → C ⋆ X
    return x = sup (inj₁ x , λ ())

    _>>=_ : ∀ {X Y} → C ⋆ X → (X → C ⋆ Y) → C ⋆ Y
    sup (inj₁ x , _) >>= k = k x
    sup (inj₂ s , f) >>= k = inn (s , λ p → f p >>= k)


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base

module HoTT.Transport.Coproduct where

private
  variable
    i : Level
    X : 𝒰 i
    A B : X → 𝒰 i
    x₁ x₂ : X

transport-+ : (p : x₁ == x₂) →
              transport (λ x → A x + B x) p ~
              +-rec (inl ∘ transport A p) (inr ∘ transport B p)
transport-+ refl (inl a) = refl
transport-+ refl (inr b) = refl


text:
{-# OPTIONS --verbose=10 #-}

module inorder where

  open import Data.Nat
  open import Data.Vec
  open import Agda.Builtin.Sigma
  open import Data.Product
  open import Data.Fin using (fromℕ)

  open import trees
  open import optics
  open import lemmas

  inorderTree : {A : Set} -> Tree A -> Σ[ n ∈ ℕ ] Vec A n × (Vec A n -> Tree A)
  inorderTree empty = (0 , ([] , λ _ -> empty))
  inorderTree {A} (node t x t₁) with inorderTree t | inorderTree t₁
  ...                              | (n₁ , (g₁ , p₁)) | (n₂ , (g₂ , p₂)) =
    (n₁ + (1 + n₂) , (g₁ ++ (x ∷ g₂) ,
      λ v -> node (p₁ (take n₁ v)) (head (drop n₁ v)) (righttree v)))
      where
        righttree :  Vec A (n₁ + (1 + n₂)) -> Tree A
        -- righttree v = p₂ (drop 1 (drop n₁ v))
        righttree v rewrite +-suc n₁ n₂ = p₂ (drop (1 + n₁) v)

  inorder : {A : Set} -> Traversal (Tree A) (Tree A) A A
  inorder = record{ extract = inorderTree }

  module tests where
    tree1 : Tree ℕ
    tree1 = node (node empty 1 empty) 3 empty

    open Traversal

    inorder1 : Vec ℕ 2
    inorder1 = get inorder tree1

    updatedinorder1 : Tree ℕ
    updatedinorder1 = put inorder tree1  (2 ∷ 3 ∷ [])

max_stars_repo_name: hablapps/safeoptics

max_issues_repo_name: hablapps/safeoptics

max_forks_repo_name: hablapps/safeoptics


text:
open import Function      using (flip; _∘_; _$_)
open import Auto.Counting
open import Data.Nat      using (ℕ)
open import Data.List     using (List; _∷_; [])
open import Data.Product  using (∃; _,_; proj₂)
open import Data.Maybe
open import Data.Sum      using (inj₁; inj₂; isInj₂)

module Auto.Example.Sublists where

infix 3 _⊆_

data _⊆_ {a} {A : Set a} : List A → List A → Set a where
  stop : [] ⊆ []
  drop : ∀ {xs y ys} → xs ⊆ ys →     xs ⊆ y ∷ ys
  keep : ∀ {x xs ys} → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys

refl : ∀ {a} {A : Set a} {xs : List A} → xs ⊆ xs
refl {xs = []}     = stop
refl {xs = x ∷ xs} = keep refl

trans : ∀ {a} {A : Set a} {xs ys zs : List A} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs
trans       p   stop    = p
trans       p  (drop q) = drop (trans p q)
trans (drop p) (keep q) = drop (trans p q)
trans (keep p) (keep q) = keep (trans p q)

hintdb₁ : HintDB
hintdb₁ = ε << quote drop
            << quote keep
            << quote trans

lemma₁ : {ws xs ys zs : List ℕ}
       → ws ⊆ 1 ∷ xs → xs ⊆ ys → ys ⊆ zs → ws ⊆ 1 ∷ 2 ∷ zs
lemma₁ = tactic (auto dfs 10 hintdb₁)

lemma₂ : {ws xs ys zs : List ℕ}
       → ws ⊆ 1 ∷ xs → xs ⊆ ys → ys ⊆ zs → ws ⊆     2 ∷ zs
lemma₂ = tactic (auto dfs 10 hintdb₁)

{-
db₂ : HintDB
db₂ = ε << quote trans
        << quote keep
        << quote drop

test₂ : {A : Set} {ws xs ys zs : List A} → ws ⊆ xs → ys ⊆ zs → ws ⊆ zs
test₂ = tactic (auto dfs 10 db₁)
-}

max_stars_repo_name: wenkokke/AutoInAgda

max_issues_repo_name: wenkokke/AutoInAgda

max_forks_repo_name: wenkokke/AutoInAgda


text:
module Issue1441 where

open import Common.Nat
open import Common.Unit
open import Common.IO

data Sing : (n : Nat) → Set where
  sing : ∀ n → Sing n

data D : Set → Set where
  c : ∀ n → D (Sing n)

test : (A : Set) → D A → Nat
test .(Sing n) (c n) = n

main : IO Unit
main = printNat (test (Sing 1) (c 1))

-- should succeed and print 1

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Common.Size

postulate
  A : Set
  f : Size → A

-- k < j ==> ∃ l < j
works : ∀ i (j : Size< (↑ i)) (k : Size< j) → (((l : Size< j) → A) → A) → A
works i j k ret = ret λ l → f l

-- k < j <= i ==> ∃ l < i
test1 : ∀ i (j : Size< (↑ i)) (k : Size< j) → (((l : Size< i) → A) → A) → A
test1 i j k ret = ret λ l → f l

-- k' < k < j <= i + 1 ==> ∃ l < i
test : ∀ i (j : Size< (↑ ↑ i)) (k : Size< j) (k' : Size< k) → (((l : Size< i) → A) → A) → A
test i j k k' ret = ret λ l → f l

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda