text:
{-

This files contains:
- Lots of useful properties about (this) decidable predicates on finite sets.
  (P.S. We use the alternative definition of decidability for computational effectivity.)

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

module Cubical.Data.FinSet.DecidablePredicate where

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

open import Cubical.HITs.PropositionalTruncation as Prop

open import Cubical.Data.Bool
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sigma

open import Cubical.Data.Fin
open import Cubical.Data.SumFin renaming (Fin to SumFin)
open import Cubical.Data.FinSet.Base
open import Cubical.Data.FinSet.Properties

open import Cubical.Relation.Nullary
open import Cubical.Relation.Nullary.DecidablePropositions
  hiding (DecProp) renaming (DecProp' to DecProp)

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

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

  isDecProp¬' : isDecProp (¬ X)
  isDecProp¬' = _ ,  invEquiv (preCompEquiv (p .snd)) ⋆ SumFin¬ _

  isDecProp∥∥' : isDecProp ∥ X ∥
  isDecProp∥∥' = _ , propTrunc≃ (p .snd) ⋆ SumFin∥∥DecProp _

module _
  (X : Type ℓ )(p : isFinOrd X)
  (P : X → Type ℓ')
  (dec : (x : X) → isDecProp (P x)) where

  private
    e = p .snd

  isFinOrdSub : isFinOrd (Σ X P)
  isFinOrdSub = _ ,
      Σ-cong-equiv {B' = λ x → P (invEq e x)} e (transpFamily p)
    ⋆ Σ-cong-equiv-snd (λ x → dec (invEq e x) .snd)
    ⋆ SumFinSub≃ _ (fst ∘ dec ∘ invEq e)

  isDecProp∃' : isDecProp ∥ Σ X P ∥
  isDecProp∃' = _ ,
      Prop.propTrunc≃ (
        Σ-cong-equiv {B' = λ x → P (invEq e x)} e (transpFamily p)
      ⋆ Σ-cong-equiv-snd (λ x → dec (invEq e x) .snd))
    ⋆ SumFin∃≃ _ (fst ∘ dec ∘ invEq e)

  isDecProp∀' : isDecProp ((x : X) → P x)
  isDecProp∀' = _ ,
      equivΠ {B' = λ x → P (invEq e x)} e (transpFamily p)
    ⋆ equivΠCod (λ x → dec (invEq e x) .snd)
    ⋆ SumFin∀≃ _ (fst ∘ dec ∘ invEq e)

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

  private
    e = p .snd

  isDecProp≡' : isDecProp (a ≡ b)
  isDecProp≡' .fst = SumFin≡ _ (e .fst a) (e .fst b)
  isDecProp≡' .snd = congEquiv e ⋆ SumFin≡≃ _ _ _

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

  isFinSetSub : isFinSet (Σ (X .fst) (λ x → P x .fst))
  isFinSetSub = Prop.rec isPropIsFinSet
    (λ p → isFinOrd→isFinSet (isFinOrdSub (X .fst) (_ , p) (λ x → P x .fst) (λ x → P x .snd)))
    (X .snd .snd)

  isDecProp∃ : isDecProp ∥ Σ (X .fst) (λ x → P x .fst) ∥
  isDecProp∃ = Prop.rec isPropIsDecProp
    (λ p → isDecProp∃' (X .fst) (_ , p) (λ x → P x .fst) (λ x → P x .snd)) (X .snd .snd)

  isDecProp∀ : isDecProp ((x : X .fst) → P x .fst)
  isDecProp∀ = Prop.rec isPropIsDecProp
    (λ p → isDecProp∀' (X .fst) (_ , p) (λ x → P x .fst) (λ x → P x .snd)) (X .snd .snd)

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

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

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

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

module _
  (X : FinSet ℓ) where

  isDecProp≡ : (a b : X .fst) → isDecProp (a ≡ b)
  isDecProp≡ a b = Prop.rec isPropIsDecProp
    (λ p → isDecProp≡' (X .fst) (_ , p) a b) (X .snd .snd)

module _
  (P : DecProp ℓ )
  (Q : DecProp ℓ') where

  isDecProp× : isDecProp (P .fst × Q .fst)
  isDecProp× .fst = P .snd .fst and Q .snd .fst
  isDecProp× .snd = Σ-cong-equiv (P .snd .snd) (λ _ → Q .snd .snd) ⋆ Bool→Type×≃ _ _

module _
  (X : FinSet ℓ) where

  isDecProp¬ : isDecProp (¬ (X .fst))
  isDecProp¬ = Prop.rec isPropIsDecProp
    (λ p → isDecProp¬' (X .fst) (_ , p)) (X .snd .snd)

  isDecProp∥∥ : isDecProp ∥ X .fst ∥
  isDecProp∥∥ = Prop.rec isPropIsDecProp
    (λ p → isDecProp∥∥' (X .fst) (_ , p)) (X .snd .snd)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
open import Relation.Ternary.Separation

module Relation.Ternary.Separation.Construct.ListOf
  {a} (A : Set a)
  {{ r : RawSep A }}
  {{ _ : IsSep r }}
  where

open import Level
open import Data.Product
open import Data.List
open import Data.List.Properties using (++-isMonoid)
open import Data.List.Relation.Binary.Equality.Propositional
open import Data.List.Relation.Binary.Permutation.Inductive

open import Relation.Binary.PropositionalEquality as P hiding ([_])
open import Relation.Unary hiding (_∈_; _⊢_)

open import Relation.Ternary.Separation.Morphisms

private
  Carrier = List A
  variable
    xˡ xʳ x y z : A
    xsˡ xsʳ xs ys zs : Carrier

data Split : (xs ys zs : Carrier) → Set a where
  divide   : xˡ ⊎ xʳ ≣ x → Split xs ys zs → Split (xˡ ∷ xs) (xʳ ∷ ys) (x ∷ zs)
  to-left  : Split xs ys zs → Split (z ∷ xs) ys (z ∷ zs)
  to-right : Split xs ys zs → Split xs (z ∷ ys) (z ∷ zs)
  []       : Split [] [] []

-- Split yields a separation algebra
instance
  splits : RawSep Carrier
  RawSep._⊎_≣_ splits = Split

  split-is-sep : IsSep splits

  -- commutes
  IsSep.⊎-comm split-is-sep (divide τ σ) = divide (⊎-comm τ) (⊎-comm σ)
  IsSep.⊎-comm split-is-sep (to-left σ)  = to-right (⊎-comm σ)
  IsSep.⊎-comm split-is-sep (to-right σ) = to-left (⊎-comm σ)
  IsSep.⊎-comm split-is-sep [] = []

  -- reassociates
  IsSep.⊎-assoc split-is-sep σ₁ (to-right σ₂) with ⊎-assoc σ₁ σ₂
  ... | _ , σ₄ , σ₅ = -, to-right σ₄ , to-right σ₅
  IsSep.⊎-assoc split-is-sep (to-left σ₁) (divide τ σ₂) with ⊎-assoc σ₁ σ₂
  ... | _ , σ₄ , σ₅ = -, divide τ σ₄ , to-right σ₅
  IsSep.⊎-assoc split-is-sep (to-right σ₁) (divide τ σ₂)  with ⊎-assoc σ₁ σ₂
  ... | _ , σ₄ , σ₅ = -, to-right σ₄ , divide τ σ₅
  IsSep.⊎-assoc split-is-sep (divide τ σ₁) (to-left σ) with ⊎-assoc σ₁ σ
  ... | _ , σ₄ , σ₅ = -, divide τ σ₄ , to-left σ₅
  IsSep.⊎-assoc split-is-sep (to-left σ₁) (to-left σ)  with ⊎-assoc σ₁ σ
  ... | _ , σ₄ , σ₅ = -, to-left σ₄ , σ₅
  IsSep.⊎-assoc split-is-sep (to-right σ₁) (to-left σ) with ⊎-assoc σ₁ σ
  ... | _ , σ₄ , σ₅ = -, to-right σ₄ , to-left σ₅
  IsSep.⊎-assoc split-is-sep [] [] = -, [] , []
  IsSep.⊎-assoc split-is-sep (divide lr σ₁) (divide rl σ₂) with ⊎-assoc σ₁ σ₂ | ⊎-assoc lr rl
  ... | _ , σ₃ , σ₄ | _ , τ₃ , τ₄ = -, divide τ₃ σ₃ , divide τ₄ σ₄

  split-is-unital : IsUnitalSep splits []
  IsUnitalSep.⊎-idˡ split-is-unital {[]}                           = []
  IsUnitalSep.⊎-idˡ split-is-unital {x ∷ Φ}                        = to-right ⊎-idˡ
  IsUnitalSep.⊎-id⁻ˡ split-is-unital (to-right σ) rewrite ⊎-id⁻ˡ σ = refl
  IsUnitalSep.⊎-id⁻ˡ split-is-unital []                            = refl

  split-has-concat : IsConcattative splits
  IsConcattative._∙_ split-has-concat = _++_
  IsConcattative.⊎-∙ₗ split-has-concat {Φₑ = []} σ = σ
  IsConcattative.⊎-∙ₗ split-has-concat {Φₑ = x ∷ Φₑ} σ = to-left (⊎-∙ₗ σ)

  split-separation : Separation _
  split-separation = record { Carrier = List A }

  split-monoidal : MonoidalSep _
  split-monoidal = record { monoid = ++-isMonoid }

  list-positive : IsPositive splits
  list-positive = record
    { ⊎-εˡ = λ where [] → refl }

unspliceᵣ : ∀ {xs ys zs : Carrier} {y} → xs ⊎ (y ∷ ys) ≣ zs → ∃ λ zs₁ → xs ⊎ [ y ] ≣ zs₁ × zs₁ ⊎ ys ≣ zs
unspliceᵣ σ with ⊎-unassoc σ (⊎-∙ {Φₗ = [ _ ]})
... | _ , σ₁ , σ₂ = -, σ₁ , σ₂

ext: agda


text:
module drawingProgram where

open import Unit
open import Data.Bool.Base
open import Data.Char.Base renaming (primCharEquality to charEquality)
open import Data.Nat.Base hiding (_≟_;_⊓_; _+_; _*_)
open import Data.List.Base hiding (_++_)
open import Data.Integer.Base hiding (suc)
open import Data.String.Base
open import Data.Maybe.Base
open import NativeIO

open import Function

open import Size renaming (Size to AgdaSize)

open import SizedIO.Base
open import SizedIO.IOGraphicsLib hiding (GraphicsCommands; GraphicsResponses; GraphicsInterface; IOGraphics; getWindowEvent; openWindow; drawInWindow; closeWindow; translateIOGraphicsLocal; translateIOGraphics)

open import NativeInt
-- open import NativeIOSafe

data GraphicsCommands  :  Set where
  closeWindow         : Window            → GraphicsCommands
  maybeGetWindowEvent : Window            → GraphicsCommands
  getWindowEvent      : Window            → GraphicsCommands
  openWindowNotEx     : String → Size    → GraphicsCommands
  openWindow          : String → (Maybe Point) → (Maybe Size)
                        → RedrawMode → (Maybe Word32) → GraphicsCommands
  timeGetTime         :                      GraphicsCommands
  drawInWindow        : Window → Graphic → GraphicsCommands
  print               : String →             GraphicsCommands

GraphicsResponses  :                       GraphicsCommands → Set
GraphicsResponses (maybeGetWindowEvent w) = Maybe Event
GraphicsResponses (getWindowEvent w)      = Event
GraphicsResponses (closeWindow w)         = Unit
GraphicsResponses (openWindowNotEx s s')  = Window
GraphicsResponses (openWindow s p s' r w) = Window
GraphicsResponses timeGetTime             = Word32
GraphicsResponses _                       = Unit

GraphicsInterface            :  IOInterface
Command   GraphicsInterface  =  GraphicsCommands
Response  GraphicsInterface  =  GraphicsResponses

IOGraphics : AgdaSize → Set → Set
IOGraphics i = IO GraphicsInterface i

translateIOGraphicsLocal : (c : GraphicsCommands) → NativeIO (GraphicsResponses c)
translateIOGraphicsLocal (maybeGetWindowEvent w) = nativeMaybeGetWindowEvent w
translateIOGraphicsLocal (getWindowEvent w)      = nativeGetWindowEvent w
translateIOGraphicsLocal (closeWindow w)         = nativeCloseWindow w
translateIOGraphicsLocal (openWindowNotEx str size)   = nativeOpenWindow str size
translateIOGraphicsLocal (openWindow str point size mode word) = nativeOpenWindowEx str point size mode word
translateIOGraphicsLocal timeGetTime             = nativeTimeGetTime
translateIOGraphicsLocal (drawInWindow w g)      = nativeDrawInWindow w g
translateIOGraphicsLocal (print s)             = nativePutStrLn s

translateIOGraphics : {A : Set} → IOGraphics ∞ A → NativeIO A
translateIOGraphics = translateIO translateIOGraphicsLocal

integerLess     :  ℤ →  ℤ → Bool
integerLess x y with ∣(y - (x ⊓ y))∣
... | zero = true
... | z = false

line : Point → Point → Graphic
line p  newpoint = withColor red (polygon
                       (nativePoint x y
                        ∷ nativePoint a b
                        ∷ nativePoint (a + xAddition) (b + yAddition)
                        ∷ nativePoint (x + xAddition) (y + yAddition)
                        ∷ [] ) )
  where
  x = nativeProj1Point p
  y = nativeProj2Point p
  a = nativeProj1Point newpoint
  b = nativeProj2Point newpoint

  diffx = + ∣ (a - x) ∣
  diffy = + ∣ (b - y) ∣

  diffx*3 = diffx * (+ 3)
  diffy*3 = diffy * (+ 3)

  condition = (integerLess diffx diffy*3) ∧ (integerLess diffy diffx*3)

  xAddition = if condition then + 2 else + 1
  yAddition = if condition then + 2 else + 1

State = Maybe Point

loop                 :  ∀{i} → Window → State → IOGraphics i Unit
force (loop w s)     =  do'  (getWindowEvent w)
  λ{  (Key c t)     →  if charEquality c 'x' then do (closeWindow w) return
                        else  loop w s
   ; (MouseMove p₂) →  case s of
                        λ{ nothing  → loop w (just p₂) ;
                          (just p₁) → do (drawInWindow w (line p₁ p₂)) λ _ →
                                       loop w (just p₂)     }
   ; _               →  loop w  s  }

program : ∀{i} → IOGraphics i Unit
program =
  do (openWindow "Drawing Program" nothing (just (size (+ 1000) (+ 1000)))
       nativeDrawGraphic nothing) λ window →
  loop window nothing

main : NativeIO Unit
main = nativeRunGraphics (translateIOGraphics program)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

open import Categories.Category

-- Lifts a 1-Category into a bicategory

module Categories.Bicategory.Construction.1-Category
  {o ℓ e} b (C : Category o ℓ e) where

open import Level using (Lift; lift)
open import Data.Unit using (⊤; tt)
open import Data.Product using (uncurry)
open import Relation.Binary using (Setoid)

open import Categories.Bicategory
open import Categories.Category.Construction.0-Groupoid using (0-Groupoid)
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Instance.Cats using (module Product)
open import Categories.Category.Groupoid using (Groupoid; IsGroupoid)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Construction.Constant using (const)
open import Categories.Functor.Bifunctor using (Bifunctor)

private module C = Category C
open C hiding (id)

1-Category : Bicategory ℓ e b o
1-Category = record
  { enriched = record
    { Obj     = Obj
    ; hom     = hom
    ; id      = id
    ; ⊚       = ⊚
    ; ⊚-assoc = ⊚-assoc
    ; unitˡ   = unitˡ
    ; unitʳ   = unitʳ
    }
  ; triangle = lift tt
  ; pentagon = lift tt
  }
  where
    open Monoidal (Product.Cats-Monoidal {ℓ} {e} {b})
    open Category.Commutation (Cats ℓ e b)

    -- Since we are doing Setoid-enriched category theory, we don't
    -- lift homsets to discrete hom-categories, but hom-setoids to
    -- thin hom-groupoids.

    hom : C.Obj → C.Obj → Category ℓ e b
    hom A B = Groupoid.category (0-Groupoid b (hom-setoid {A} {B}))

    id : ∀ {A} → Functor unit (hom A A)
    id = const C.id

    ⊚ : ∀ {A B C} → Bifunctor (hom B C) (hom A B) (hom A C)
    ⊚ {A} {B} {C} = record
      { F₀ = uncurry _∘_
      ; F₁ = uncurry ∘-resp-≈
      ; identity     = lift tt
      ; homomorphism = lift tt
      ; F-resp-≈     = λ _ → lift tt
      }

    ⊚-assoc : ∀ {A B C D} →
      [ (hom C D ⊗₀ hom B C) ⊗₀ hom A B ⇒ hom A D ]⟨
        ⊚ ⊗₁ idF          ⇒⟨ hom B D ⊗₀ hom A B ⟩
        ⊚
      ≈ associator.from   ⇒⟨ hom C D ⊗₀ (hom B C ⊗₀ hom A B) ⟩
        idF ⊗₁ ⊚          ⇒⟨ hom C D ⊗₀ hom A C ⟩
        ⊚
      ⟩
    ⊚-assoc = record
      { F⇒G = record { η = λ _ →     assoc ; commute = λ _ → lift tt }
      ; F⇐G = record { η = λ _ → sym-assoc ; commute = λ _ → lift tt }
      ; iso = λ _ → record { isoˡ = lift tt ; isoʳ = lift tt }
      }

    unitˡ : ∀ {A B} →
      [ unit ⊗₀ hom A B ⇒ hom A B ]⟨
        id ⊗₁ idF    ⇒⟨ hom B B ⊗₀ hom A B ⟩
        ⊚
      ≈ unitorˡ.from
      ⟩
    unitˡ = record
      { F⇒G = record { η = λ _ →           identityˡ ; commute = λ _ → lift tt }
      ; F⇐G = record { η = λ _ → Equiv.sym identityˡ ; commute = λ _ → lift tt }
      ; iso = λ _ → record { isoˡ = lift tt ; isoʳ = lift tt }
      }

    unitʳ : ∀ {A B} →
      [ hom A B ⊗₀ unit ⇒ hom A B ]⟨
        idF ⊗₁ id    ⇒⟨ hom A B ⊗₀ hom A A ⟩
        ⊚
      ≈ unitorʳ.from
      ⟩
    unitʳ = record
      { F⇒G = record { η = λ _ →           identityʳ ; commute = λ _ → lift tt }
      ; F⇐G = record { η = λ _ → Equiv.sym identityʳ ; commute = λ _ → lift tt }
      ; iso = λ _ → record { isoˡ = lift tt ; isoʳ = lift tt }
      }

open Bicategory 1-Category

-- The hom-categories are hom-groupoids

hom-isGroupoid : ∀ {A B} → IsGroupoid (hom A B)
hom-isGroupoid = Groupoid.isGroupoid (0-Groupoid b hom-setoid)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------
-- Lexicographic products of binary relations
------------------------------------------------------------------------

-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a strict partial order.

module Relation.Binary.Product.StrictLex where

open import Data.Function
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Relation.Nullary.Product
open import Relation.Nullary.Sum
open import Relation.Binary
open import Relation.Binary.Consequences
open import Relation.Binary.Product.Pointwise as Pointwise
  using (_×-Rel_)

private
 module Dummy {a₁ a₂ : Set} where

  ×-Lex : (≈₁ <₁ : Rel a₁) → (≤₂ : Rel a₂) → Rel (a₁ × a₂)
  ×-Lex ≈₁ <₁ ≤₂ = (<₁ on₁ proj₁) -⊎- (≈₁ on₁ proj₁) -×- (≤₂ on₁ proj₂)

  -- Some properties which are preserved by ×-Lex (under certain
  -- assumptions).

  ×-reflexive : ∀ ≈₁ ∼₁ {≈₂} ≤₂ →
                ≈₂ ⇒ ≤₂ → (≈₁ ×-Rel ≈₂) ⇒ (×-Lex ≈₁ ∼₁ ≤₂)
  ×-reflexive _ _ _ refl₂ = λ x≈y →
    inj₂ (proj₁ x≈y , refl₂ (proj₂ x≈y))

  _×-irreflexive_ : ∀ {≈₁ <₁} → Irreflexive ≈₁ <₁ →
                    ∀ {≈₂ <₂} → Irreflexive ≈₂ <₂ →
                    Irreflexive (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
  (ir₁ ×-irreflexive ir₂) x≈y (inj₁ x₁<y₁) = ir₁ (proj₁ x≈y) x₁<y₁
  (ir₁ ×-irreflexive ir₂) x≈y (inj₂ x≈<y)  =
    ir₂ (proj₂ x≈y) (proj₂ x≈<y)

  ×-transitive :
    ∀ {≈₁ <₁} → IsEquivalence ≈₁ → <₁ Respects₂ ≈₁ → Transitive <₁ →
    ∀ {≤₂} → Transitive ≤₂ →
    Transitive (×-Lex ≈₁ <₁ ≤₂)
  ×-transitive {≈₁ = ≈₁} {<₁ = <₁} eq₁ resp₁ trans₁
               {≤₂ = ≤₂} trans₂ {x} {y} {z} = trans {x} {y} {z}
    where
    module Eq₁ = IsEquivalence eq₁

    trans : Transitive (×-Lex ≈₁ <₁ ≤₂)
    trans (inj₁ x₁<y₁) (inj₁ y₁<z₁) = inj₁ (trans₁ x₁<y₁ y₁<z₁)
    trans (inj₁ x₁<y₁) (inj₂ y≈≤z)  =
      inj₁ (proj₁ resp₁ (proj₁ y≈≤z) x₁<y₁)
    trans (inj₂ x≈≤y)  (inj₁ y₁<z₁) =
      inj₁ (proj₂ resp₁ (Eq₁.sym $ proj₁ x≈≤y) y₁<z₁)
    trans (inj₂ x≈≤y)  (inj₂ y≈≤z)  =
      inj₂ ( Eq₁.trans (proj₁ x≈≤y) (proj₁ y≈≤z)
           , trans₂    (proj₂ x≈≤y) (proj₂ y≈≤z) )

  ×-antisymmetric :
    ∀ {≈₁ <₁} → Symmetric ≈₁ → Irreflexive ≈₁ <₁ → Asymmetric <₁ →
    ∀ {≈₂ ≤₂} → Antisymmetric ≈₂ ≤₂ →
    Antisymmetric (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ ≤₂)
  ×-antisymmetric {≈₁ = ≈₁} {<₁ = <₁} sym₁ irrefl₁ asym₁
                  {≈₂ = ≈₂} {≤₂ = ≤₂} antisym₂ {x} {y} =
    antisym {x} {y}
    where
    antisym : Antisymmetric (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ ≤₂)
    antisym (inj₁ x₁<y₁) (inj₁ y₁<x₁) =
      ⊥-elim {_ × _} $ asym₁ x₁<y₁ y₁<x₁
    antisym (inj₁ x₁<y₁) (inj₂ y≈≤x)  =
      ⊥-elim {_ × _} $ irrefl₁ (sym₁ $ proj₁ y≈≤x) x₁<y₁
    antisym (inj₂ x≈≤y)  (inj₁ y₁<x₁) =
      ⊥-elim {_ × _} $ irrefl₁ (sym₁ $ proj₁ x≈≤y) y₁<x₁
    antisym (inj₂ x≈≤y)  (inj₂ y≈≤x)  =
      proj₁ x≈≤y , antisym₂ (proj₂ x≈≤y) (proj₂ y≈≤x)

  ×-asymmetric :
    ∀ {≈₁ <₁} → Symmetric ≈₁ → <₁ Respects₂ ≈₁ → Asymmetric <₁ →
    ∀ {<₂} → Asymmetric <₂ →
    Asymmetric (×-Lex ≈₁ <₁ <₂)
  ×-asymmetric {≈₁ = ≈₁} {<₁ = <₁} sym₁ resp₁ asym₁
               {<₂ = <₂} asym₂ {x} {y} = asym {x} {y}
    where
    irrefl₁ : Irreflexive ≈₁ <₁
    irrefl₁ = asym⟶irr resp₁ sym₁ asym₁

    asym : Asymmetric (×-Lex ≈₁ <₁ <₂)
    asym (inj₁ x₁<y₁) (inj₁ y₁<x₁) = asym₁ x₁<y₁ y₁<x₁
    asym (inj₁ x₁<y₁) (inj₂ y≈<x)  = irrefl₁ (sym₁ $ proj₁ y≈<x) x₁<y₁
    asym (inj₂ x≈<y)  (inj₁ y₁<x₁) = irrefl₁ (sym₁ $ proj₁ x≈<y) y₁<x₁
    asym (inj₂ x≈<y)  (inj₂ y≈<x)  = asym₂ (proj₂ x≈<y) (proj₂ y≈<x)

  ×-≈-respects₂ :
    ∀ {≈₁ <₁} → IsEquivalence ≈₁ → <₁ Respects₂ ≈₁ →
    ∀ {≈₂ <₂} → <₂ Respects₂ ≈₂ →
    (×-Lex ≈₁ <₁ <₂) Respects₂ (≈₁ ×-Rel ≈₂)
  ×-≈-respects₂ {≈₁ = ≈₁} {<₁ = <₁} eq₁ resp₁
                {≈₂ = ≈₂} {<₂ = <₂}     resp₂ =
    (λ {x y z} → resp¹ {x} {y} {z}) ,
    (λ {x y z} → resp² {x} {y} {z})
    where
    < = ×-Lex ≈₁ <₁ <₂

    open IsEquivalence eq₁ renaming (sym to sym₁; trans to trans₁)

    resp¹ : ∀ {x} → (< x) Respects (≈₁ ×-Rel ≈₂)
    resp¹ y≈y' (inj₁ x₁<y₁) = inj₁ (proj₁ resp₁ (proj₁ y≈y') x₁<y₁)
    resp¹ y≈y' (inj₂ x≈<y)  =
      inj₂ ( trans₁ (proj₁ x≈<y) (proj₁ y≈y')
           , proj₁ resp₂ (proj₂ y≈y') (proj₂ x≈<y) )

    resp² : ∀ {y} → (flip₁ < y) Respects (≈₁ ×-Rel ≈₂)
    resp² x≈x' (inj₁ x₁<y₁) = inj₁ (proj₂ resp₁ (proj₁ x≈x') x₁<y₁)
    resp² x≈x' (inj₂ x≈<y)  =
      inj₂ ( trans₁ (sym₁ $ proj₁ x≈x') (proj₁ x≈<y)
           , proj₂ resp₂ (proj₂ x≈x') (proj₂ x≈<y) )

  ×-decidable : ∀ {≈₁ <₁} → Decidable ≈₁ → Decidable <₁ →
                ∀ {≤₂} → Decidable ≤₂ →
                Decidable (×-Lex ≈₁ <₁ ≤₂)
  ×-decidable dec-≈₁ dec-<₁ dec-≤₂ = λ x y →
    dec-<₁ (proj₁ x) (proj₁ y)
      ⊎-dec
    (dec-≈₁ (proj₁ x) (proj₁ y)
       ×-dec
     dec-≤₂ (proj₂ x) (proj₂ y))

  ×-total : ∀ {≈₁ <₁} → Total <₁ →
            ∀ {≤₂} →
            Total (×-Lex ≈₁ <₁ ≤₂)
  ×-total {≈₁ = ≈₁} {<₁ = <₁} total₁ {≤₂ = ≤₂} = total
    where
    total : Total (×-Lex ≈₁ <₁ ≤₂)
    total x y with total₁ (proj₁ x) (proj₁ y)
    ... | inj₁ x₁<y₁ = inj₁ (inj₁ x₁<y₁)
    ... | inj₂ x₁>y₁ = inj₂ (inj₁ x₁>y₁)

  ×-compare : ∀ {≈₁ <₁} → Symmetric ≈₁ → Trichotomous ≈₁ <₁ →
              ∀ {≈₂ <₂} → Trichotomous ≈₂ <₂ →
              Trichotomous (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
  ×-compare {≈₁} {<₁} sym₁ compare₁ {≈₂} {<₂} compare₂ = cmp
    where
    cmp : Trichotomous (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
    cmp (x₁ , x₂) (y₁ , y₂) with compare₁ x₁ y₁
    ... | tri< x₁<y₁ x₁≉y₁ x₁≯y₁ = tri< (inj₁ x₁<y₁) (x₁≉y₁ ∘ proj₁)
                                        [ x₁≯y₁ , x₁≉y₁ ∘ sym₁ ∘ proj₁ ]
    ... | tri> x₁≮y₁ x₁≉y₁ x₁>y₁ = tri> [ x₁≮y₁ , x₁≉y₁ ∘ proj₁ ]
                                        (x₁≉y₁ ∘ proj₁) (inj₁ x₁>y₁)
    ... | tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁ with compare₂ x₂ y₂
    ...   | tri< x₂<y₂ x₂≉y₂ x₂≯y₂ = tri< (inj₂ (x₁≈y₁ , x₂<y₂))
                                          (x₂≉y₂ ∘ proj₂)
                                          [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]
    ...   | tri> x₂≮y₂ x₂≉y₂ x₂>y₂ = tri> [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
                                          (x₂≉y₂ ∘ proj₂)
                                          (inj₂ (sym₁ x₁≈y₁ , x₂>y₂))
    ...   | tri≈ x₂≮y₂ x₂≈y₂ x₂≯y₂ = tri≈ [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
                                          (x₁≈y₁ , x₂≈y₂)
                                          [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]

  -- Some collections of properties which are preserved by ×-Lex.

  _×-isPreorder_ : ∀ {≈₁ ∼₁} → IsPreorder ≈₁ ∼₁ →
                   ∀ {≈₂ ∼₂} → IsPreorder ≈₂ ∼₂ →
                   IsPreorder (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ ∼₁ ∼₂)
  _×-isPreorder_ {≈₁ = ≈₁} {∼₁ = ∼₁} pre₁ {∼₂ = ∼₂} pre₂ = record
    { isEquivalence = Pointwise._×-isEquivalence_
                        (isEquivalence pre₁) (isEquivalence pre₂)
    ; reflexive     = λ {x y} →
                      ×-reflexive ≈₁ ∼₁ ∼₂ (reflexive pre₂) {x} {y}
    ; trans         = λ {x y z} →
                      ×-transitive
                        (isEquivalence pre₁) (∼-resp-≈ pre₁) (trans pre₁)
                        {≤₂ = ∼₂} (trans pre₂) {x} {y} {z}
    ; ∼-resp-≈      = ×-≈-respects₂ (isEquivalence pre₁)
                                        (∼-resp-≈ pre₁)
                                        (∼-resp-≈ pre₂)
    }
    where open IsPreorder

  _×-isStrictPartialOrder_ :
    ∀ {≈₁ <₁} → IsStrictPartialOrder ≈₁ <₁ →
    ∀ {≈₂ <₂} → IsStrictPartialOrder ≈₂ <₂ →
    IsStrictPartialOrder (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
  _×-isStrictPartialOrder_ {<₁ = <₁} spo₁ {<₂ = <₂} spo₂ =
    record
      { isEquivalence = Pointwise._×-isEquivalence_
                          (isEquivalence spo₁) (isEquivalence spo₂)
      ; irrefl        = λ {x y} →
                        _×-irreflexive_ {<₁ = <₁} (irrefl spo₁)
                                        {<₂ = <₂} (irrefl spo₂) {x} {y}
      ; trans         = λ {x y z} →
                        ×-transitive
                          {<₁ = <₁} (isEquivalence spo₁) (<-resp-≈ spo₁)
                                    (trans spo₁)
                          {≤₂ = <₂} (trans spo₂) {x} {y} {z}
      ; <-resp-≈      = ×-≈-respects₂ (isEquivalence spo₁)
                                          (<-resp-≈ spo₁)
                                          (<-resp-≈ spo₂)
      }
    where open IsStrictPartialOrder

  _×-isStrictTotalOrder_ :
    ∀ {≈₁ <₁} → IsStrictTotalOrder ≈₁ <₁ →
    ∀ {≈₂ <₂} → IsStrictTotalOrder ≈₂ <₂ →
    IsStrictTotalOrder (≈₁ ×-Rel ≈₂) (×-Lex ≈₁ <₁ <₂)
  _×-isStrictTotalOrder_ {<₁ = <₁} spo₁ {<₂ = <₂} spo₂ =
    record
      { isEquivalence = Pointwise._×-isEquivalence_
                          (isEquivalence spo₁) (isEquivalence spo₂)
      ; trans         = λ {x y z} →
                        ×-transitive
                          {<₁ = <₁} (isEquivalence spo₁) (<-resp-≈ spo₁)
                                    (trans spo₁)
                          {≤₂ = <₂} (trans spo₂) {x} {y} {z}
      ; compare       = ×-compare (Eq.sym spo₁) (compare spo₁)
                                                (compare spo₂)
      ; <-resp-≈      = ×-≈-respects₂ (isEquivalence spo₁)
                                      (<-resp-≈ spo₁)
                                      (<-resp-≈ spo₂)
      }
    where open IsStrictTotalOrder

open Dummy public

-- "Packages" (e.g. preorders) can also be combined.

_×-preorder_ : Preorder → Preorder → Preorder
p₁ ×-preorder p₂ = record
  { isPreorder = isPreorder p₁ ×-isPreorder isPreorder p₂
  } where open Preorder

_×-strictPartialOrder_ :
  StrictPartialOrder → StrictPartialOrder → StrictPartialOrder
s₁ ×-strictPartialOrder s₂ = record
  { isStrictPartialOrder = isStrictPartialOrder s₁
                             ×-isStrictPartialOrder
                           isStrictPartialOrder s₂
  } where open StrictPartialOrder

_×-strictTotalOrder_ :
  StrictTotalOrder → StrictTotalOrder → StrictTotalOrder
s₁ ×-strictTotalOrder s₂ = record
  { isStrictTotalOrder = isStrictTotalOrder s₁
                           ×-isStrictTotalOrder
                         isStrictTotalOrder s₂
  } where open StrictTotalOrder

max_issues_repo_name: larrytheliquid/Lemmachine


text:
module Issue556 (A : Set) (x : A) where

y : A
y = x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Issue1025 where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

postulate mySpace : Set
postulate myPoint : mySpace

data Foo : myPoint ≡ myPoint → Set where
  foo : Foo refl

test : {e : myPoint ≡ myPoint} → (a : Foo e) → (i : a ≡ a) → i ≡ refl
test foo refl = {!!}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Non empty trie, basic type and operations
------------------------------------------------------------------------

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

open import Relation.Binary using (StrictTotalOrder)

module Data.Trie.NonEmpty {k e r} (S : StrictTotalOrder k e r) where

open import Level
open import Size
open import Category.Monad
open import Data.Product as Prod using (∃; uncurry; -,_)
open import Data.List.Base as List using (List; []; _∷_; _++_)
open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; concatMap)
open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′) hiding (module Maybe)
open import Data.These as These using (These; this; that; these)
open import Function as F
import Function.Identity.Categorical as Identity
open import Relation.Unary using (_⇒_; IUniversal)

open StrictTotalOrder S
  using (module Eq)
  renaming (Carrier to Key)

open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid
open import Data.AVL.Value hiding (Value)
open import Data.AVL.Value ≋-setoid using (Value)
open import Data.AVL.NonEmpty S as Tree⁺ using (Tree⁺)
open Value

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

-- A Trie⁺ is a tree branching over an alphabet of Keys. It stores values
-- indexed over the Word (i.e. List Key) that was read to reach them.
-- Each node in the Trie⁺ contains either a value, a non-empty Tree of
-- sub-Trie⁺ reached by reading an extra letter, or both.

Word : Set k
Word = List Key

eat : ∀ {v} → Value v → Word → Value v
family   (eat V ks) = family   V ∘′ (ks ++_)
respects (eat V ks) = respects V ∘′ ++⁺ ≋-refl

data Trie⁺ {v} (V : Value v) : Size → Set (v ⊔ k ⊔ e ⊔ r)
Tries⁺ : ∀ {v} (V : Value v) (i : Size) → Set (v ⊔ k ⊔ e ⊔ r)

map : ∀ {v w} (V : Value v) (W : Value w) {i} →
      ∀[ family V ⇒ family W ] →
      Trie⁺ V i → Trie⁺ W i

data Trie⁺ V where
  node : ∀ {i} → These (family V []) (Tries⁺ V i) → Trie⁺ V (↑ i)

Tries⁺ V j = Tree⁺ $ MkValue (λ k → Trie⁺ (eat V (k ∷ [])) j)
                   $ λ eq → map _ _ (respects V (eq ∷ ≋-refl))

map V W f (node t) = node $ These.map f (Tree⁺.map (map _ _ f)) t

------------------------------------------------------------------------
-- Query

lookup : ∀ {v} {V : Value v} ks → Trie⁺ V ∞ →
         Maybe (These (family V ks) (Tries⁺ (eat V ks) ∞))
lookup []       (node nd) = just (These.map₂ (Tree⁺.map id) nd)
lookup (k ∷ ks) (node nd) = let open Maybe in do
  ts ← These.fromThat nd
  t  ← Tree⁺.lookup k ts
  lookup ks t

module _ {v} {V : Value v} where

  lookupValue : ∀ (ks : Word) → Trie⁺ V ∞ → Maybe (family V ks)
  lookupValue ks t = lookup ks t Maybe.>>= These.fromThis

  lookupTries⁺ : ∀ ks → Trie⁺ V ∞ → Maybe (Tries⁺ (eat V ks) ∞)
  lookupTries⁺ ks t = lookup ks t Maybe.>>= These.fromThat

  lookupTrie⁺ : ∀ k → Trie⁺ V ∞ → Maybe (Trie⁺ (eat V (k ∷ [])) ∞)
  lookupTrie⁺ k t = lookupTries⁺ [] t Maybe.>>= Tree⁺.lookup k

------------------------------------------------------------------------
-- Construction

singleton : ∀ {v} {V : Value v} ks → family V ks → Trie⁺ V ∞
singleton []       v = node (this v)
singleton (k ∷ ks) v = node (that (Tree⁺.singleton k (singleton ks v)))

insertWith : ∀ {v} {V : Value v} ks → (Maybe (family V ks) → family V ks) →
             Trie⁺ V ∞ → Trie⁺ V ∞
insertWith []       f (node nd) =
  node (These.fold (this ∘ f ∘ just) (these (f nothing)) (these ∘ f ∘ just) nd)
insertWith {v} {V} (k ∷ ks) f (node {j} nd) = node $
  These.fold (λ v → these v (Tree⁺.singleton k end))
             (that ∘′ rec)
             (λ v → these v ∘′ rec)
             nd
  where

  end : Trie⁺ (eat V (k ∷ [])) ∞
  end = singleton ks (f nothing)

  rec : Tries⁺ V ∞ → Tries⁺ V ∞
  rec = Tree⁺.insertWith k (maybe′ (insertWith ks f) end)

module _ {v} {V : Value v} where

  private Val = family V

  insert : ∀ ks → Val ks → Trie⁺ V ∞ → Trie⁺ V ∞
  insert ks = insertWith ks ∘′ F.const

  fromList⁺ : List⁺ (∃ Val) → Trie⁺ V ∞
  fromList⁺ = List⁺.foldr (uncurry insert) (uncurry singleton)

toList⁺ : ∀ {v} {V : Value v} {i} → let Val = Value.family V in
          Trie⁺ V i → List⁺ (∃ Val)
toList⁺ (node nd) = These.mergeThese List⁺._⁺++⁺_
                    $ These.map fromVal fromTries⁺ nd
  where

  fromVal    = [_] ∘′ -,_
  fromTries⁺ = concatMap (uncurry λ k → List⁺.map (Prod.map (k ∷_) id) ∘′ toList⁺)
             ∘′ Tree⁺.toList⁺

------------------------------------------------------------------------
-- Modification

-- Deletion

deleteWith : ∀ {v} {V : Value v} {i} ks →
             (∀ {i} → Trie⁺ (eat V ks) i → Maybe (Trie⁺ (eat V ks) i)) →
             Trie⁺ V i → Maybe (Trie⁺ V i)
deleteWith []       f t           = f t
deleteWith (k ∷ ks) f t@(node nd) = let open RawMonad Identity.monad in do
  just ts ← These.fromThat nd where _ → just t
  -- This would be a lot cleaner if we had
  -- Tree⁺.updateWith : ∀ k → (Maybe (V k) → Maybe (V k)) → AVL → AVL
  -- Instead we lookup the subtree, update it and either put it back in
  -- or delete the corresponding leaf depending on whether the result is successful.
  just t′ ← Tree⁺.lookup k ts where _ → just t
  Maybe.map node ∘′ Maybe.align (These.fromThis nd) $′ case deleteWith ks f t′ of λ where
    nothing  → Tree⁺.delete k ts
    (just u) → just (Tree⁺.insert k u ts)

module _ {v} {V : Value v} where

  deleteTrie⁺ : ∀ {i} (ks : Word) → Trie⁺ V i → Maybe (Trie⁺ V i)
  deleteTrie⁺ ks = deleteWith ks (F.const nothing)

  deleteValue : ∀ {i} (ks : Word) → Trie⁺ V i → Maybe (Trie⁺ V i)
  deleteValue ks = deleteWith ks $ λ where
    (node nd) → Maybe.map node $′ These.deleteThis nd

  deleteTries⁺ : ∀ {i} (ks : Word) → Trie⁺ V i → Maybe (Trie⁺ V i)
  deleteTries⁺ ks = deleteWith ks $ λ where
    (node nd) → Maybe.map node $′ These.deleteThat nd


text:
module Basic where

open import Prelude

data List (A : Set) : Set

data List A where
  nil  : List A
  cons : A -> List A -> List A

append : {A : Set} -> List A -> List A -> List A
append nil ys = ys
append (cons x xs) ys = cons x (append xs ys)

record Equiv {A : Set} (R : A -> A -> Set) : Set
record Equiv {A} R where
  constructor equiv
  field
    ref : (x : A) -> R x x
    sym : (x : A) (y : A) -> R x y -> R y x
    trans : {x y z : A} -> R x y -> R y z -> R x z

open Equiv

trans1 : {A : Set}{R : A -> A -> Set}{x y z : A} -> Equiv R -> R x y -> R y z -> R x z
trans1 eq p q = trans eq p q

postulate
  symId   : {A : Set} (x y : A) -> x == y -> y == x
  transId : {A : Set} {x y z : A} -> x == y -> y == z -> x == z

equivId : {A : Set} -> Equiv {A} (\x y -> x == y)
equivId {A} = equiv (\x -> refl) symId (\ x y z -> transId)

record Sigma (A : Set) (B : A -> Set) : Set
record Sigma A B where
  constructor pair
  field fst : A
        snd : B fst

record True : Set
record True where
  constructor tt

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-

This file contains:

- An implementation of the free groupoid (a free group that has no limitiations
  over the high dimensional path structure). An intermediate construction used
  to calculate the fundamental group of a Bouquet.

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

module Cubical.HITs.FreeGroupoid.Base where

open import Cubical.Foundations.Prelude

private
  variable
    ℓ : Level

data FreeGroupoid (A : Type ℓ) : Type ℓ where
  η     : A → FreeGroupoid A
  _·_     : FreeGroupoid A → FreeGroupoid A → FreeGroupoid A
  ε     : FreeGroupoid A
  inv   : FreeGroupoid A → FreeGroupoid A
  assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z
  idr   : ∀ x → x ≡ x · ε
  idl   : ∀ x → x ≡ ε · x
  invr  : ∀ x → x · (inv x) ≡ ε
  invl  : ∀ x → (inv x) · x ≡ ε

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

module encode-decode where

import 05-identity-types
open 05-identity-types public

record Lift {i j : Level} (A : UU i) : UU (i ⊔ j) where
  field
    raise : A

module Coprod where
  code-left : {i j : Level} {A : UU i} {B : UU j} → A → (coprod A B) → (UU i)
  code-left a₀ (inl a) = Id a₀ a
  code-left a₀ (inr b) = Lift 𝟘

  code-right : {i j : Level} {A : UU i} {B : UU j} → B → (coprod A B) → (UU j)
  code-right b₀ (inr b) = Id b₀ b
  code-right b₀ (inl a) = Lift 𝟘

  encode-left : {i j : Level} {A : UU i} {B : UU j} → (a₀ : A) → (x : coprod A B) → (p : Id (inl a₀) x) → (code-left a₀ x)
  encode-left a₀ x p = tr (code-left a₀) p refl

  decode-left : {i j : Level} {A : UU i} {B : UU j} → (a₀ : A) → (x : coprod A B) → (c : (code-left a₀ x)) → Id (inl a₀) x
  decode-left a₀ (inl a) refl = refl
  decode-left a₀ (inr b) c    = ind-empty (Lift.raise c)

module Nats where
  code : ℕ → ℕ → (UU lzero)
  code zero-ℕ     zero-ℕ     = 𝟙
  code (succ-ℕ m) zero-ℕ     = Lift 𝟘
  code zero-ℕ     (succ-ℕ n) = Lift 𝟘
  code (succ-ℕ m) (succ-ℕ n) = code m n

  recursion : (n : ℕ) → code n n
  recursion zero-ℕ     = star
  recursion (succ-ℕ n) = recursion n

  encode : (m n : ℕ) → (Id m n) → (code m n)
  encode m n p = tr (code m) p (recursion m)

  decode : (m n : ℕ) → (code m n) → (Id m n)
  decode zero-ℕ     zero-ℕ     s = refl
  decode (succ-ℕ m) zero-ℕ     e = ind-empty (Lift.raise e)
  decode zero-ℕ     (succ-ℕ n) e = ind-empty (Lift.raise e)
  decode (succ-ℕ m) (succ-ℕ n) c = ap succ-ℕ (decode m n c)

  -- This doesn't work.
  constant-fn : (n : ℕ) → code n n
  constant-fn n = star

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
------------------------------------------------------------------------------
-- Properties of the mirror function
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Program.Mirror.Type
open import FOTC.Program.Mirror.Forest.PropertiesI as ForestP
open import FOTC.Program.Mirror.Forest.TotalityI
open import FOTC.Program.Mirror.Mirror
open import FOTC.Program.Mirror.Tree.TotalityI

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

mirror-involutive : ∀ {t} → Tree t → mirror · (mirror · t) ≡ t
helper            : ∀ {ts} → Forest ts →
                    reverse (map mirror (reverse (map mirror ts))) ≡ ts

mirror-involutive (tree d fnil) =
  mirror · (mirror · (node d []))
    ≡⟨ subst (λ x → mirror · (mirror · (node d [])) ≡ mirror · x)
             (mirror-eq d [])
             refl
    ⟩
  mirror · node d (reverse (map mirror []))
    ≡⟨ subst (λ x → mirror · node d (reverse (map mirror [])) ≡
                    mirror · node d (reverse x))
             (map-[] mirror)
             refl
    ⟩
  mirror · node d (reverse [])
    ≡⟨ subst (λ x → mirror · node d (reverse []) ≡ mirror · node d x)
             (rev-[] [])
             refl
    ⟩
  mirror · node d []
    ≡⟨ mirror-eq d [] ⟩
  node d (reverse (map mirror []))
    ≡⟨ subst (λ x → node d (reverse (map mirror [])) ≡
                    node d (reverse x))
             (map-[] mirror)
             refl
    ⟩
  node d (reverse [])
    ≡⟨ subst (λ x → node d (reverse []) ≡ node d x) (rev-[] []) refl ⟩
  node d [] ∎

mirror-involutive (tree d (fcons {t} {ts} Tt Fts)) =
  mirror · (mirror · node d (t ∷ ts))
    ≡⟨ subst (λ x → mirror · (mirror · node d (t ∷ ts)) ≡ mirror · x)
             (mirror-eq d (t ∷ ts))
             refl
    ⟩
  mirror · node d (reverse (map mirror (t ∷ ts)))
    ≡⟨ subst (λ x → mirror · node d (reverse (map mirror (t ∷ ts))) ≡ x)
             (mirror-eq d (reverse (map mirror (t ∷ ts))))
             refl
    ⟩
  node d (reverse (map mirror (reverse (map mirror (t ∷ ts)))))
    ≡⟨ subst (λ x → node d (reverse (map mirror (reverse (map mirror (t ∷ ts))))) ≡
                    node d x)
             (helper (fcons Tt Fts))
             refl
    ⟩
  node d (t ∷ ts) ∎

helper fnil =
  reverse (map mirror (reverse (map mirror [])))
    ≡⟨ reverseCong (mapCong₂ (reverseCong (map-[] mirror))) ⟩
  reverse (map mirror (reverse []))
    ≡⟨ reverseCong (mapCong₂ (rev-[] [])) ⟩
  reverse (map mirror [])
    ≡⟨ reverseCong (map-[] mirror) ⟩
  reverse []
    ≡⟨ rev-[] [] ⟩
  [] ∎

helper (fcons {t} {ts} Tt Fts) =
  reverse (map mirror (reverse (map mirror (t ∷ ts))))
    ≡⟨ reverseCong (mapCong₂ (reverseCong (map-∷ mirror t ts))) ⟩
  reverse (map mirror (reverse (mirror · t ∷ map mirror ts)))
    ≡⟨ reverseCong (mapCong₂
                     (ForestP.reverse-∷ (mirror-Tree Tt)
                                        (map-Forest mirror mirror-Tree Fts)))
    ⟩
  reverse (map mirror (reverse (map mirror ts) ++ (mirror · t ∷ [])))
    ≡⟨ reverseCong (ForestP.map-++
                     mirror
                     mirror-Tree
                       (reverse-Forest (map-Forest mirror mirror-Tree Fts))
                       (mirror · t ∷ [])) ⟩

  reverse (map mirror (reverse (map mirror ts)) ++
          (map mirror (mirror · t ∷ [])))
    ≡⟨ subst (λ x → (reverse (map mirror (reverse (map mirror ts)) ++
                                         (map mirror (mirror · t ∷ [])))) ≡ x)
             (ForestP.reverse-++
               (map-Forest mirror mirror-Tree
                           (reverse-Forest
                           (map-Forest mirror mirror-Tree Fts)))
               (map-Forest mirror mirror-Tree
                           (fcons (mirror-Tree Tt) fnil)))
             refl
    ⟩
  reverse (map mirror (mirror · t ∷ [])) ++
  reverse (map mirror (reverse (map mirror ts)))
    ≡⟨ subst (λ x → reverse (map mirror (mirror · t ∷ [])) ++ n₁ ≡
                    reverse x ++ n₁)
             (map-∷ mirror (mirror · t) [])
             refl
    ⟩
  reverse (mirror · (mirror · t) ∷ map mirror []) ++ n₁
    ≡⟨ subst (λ x → reverse (mirror · (mirror · t) ∷ map mirror []) ++ n₁ ≡
                    reverse (mirror · (mirror · t) ∷ x) ++ n₁)
             (map-[] mirror)
             refl
    ⟩
  reverse (mirror · (mirror · t) ∷ []) ++ n₁
    ≡⟨ ++-leftCong (reverse-[x]≡[x] (mirror · (mirror · t))) ⟩
  (mirror · (mirror · t) ∷ []) ++ n₁
    ≡⟨ ++-∷ (mirror · (mirror · t)) [] n₁ ⟩
  mirror · (mirror · t) ∷ [] ++ n₁
    ≡⟨ subst (λ x → mirror · (mirror · t) ∷ [] ++ n₁ ≡
                    mirror · (mirror · t) ∷ x)
             (++-leftIdentity n₁)
             refl
    ⟩
  mirror · (mirror · t) ∷ reverse (map mirror (reverse (map mirror ts)))
    ≡⟨ ∷-leftCong (mirror-involutive Tt) ⟩
  t ∷ reverse (map mirror (reverse (map mirror ts)))
    ≡⟨ ∷-rightCong (helper Fts) ⟩
  t ∷ ts ∎
  where
  n₁ : D
  n₁ = reverse (map mirror (reverse (map mirror ts)))

  Fn₁ : Forest n₁
  Fn₁ = rev-Forest
          (map-Forest mirror mirror-Tree
                      (reverse-Forest (map-Forest mirror mirror-Tree Fts)))
          fnil

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module UnequalTerms where

data Zero : Set where
data One  : Set where one : One

err1 : Zero
err1 = one

err2 : One -> One
err2 = \(x : Zero) -> one


text:
-- Andreas, 2015-02-26
-- {-# OPTIONS -v interaction:100 #-}

data D : Set where
  c : D

goal : D
goal = {! !}  -- C-c C-r gave a parse error here, as there was a (single) space.

g1 : D
g1 = {!  !}

g2 : D
g2 = {!   !}

-- works now


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Code related to vector equality over propositional equality that
-- makes use of heterogeneous equality
------------------------------------------------------------------------

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

module Data.Vec.Relation.Binary.Equality.Propositional.WithK
  {a} {A : Set a} where

open import Data.Vec
open import Data.Vec.Relation.Binary.Equality.Propositional {A = A}
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.HeterogeneousEquality as H using (_≅_)

≋⇒≅ : ∀ {m n} {xs : Vec A m} {ys : Vec A n} →
      xs ≋ ys → xs ≅ ys
≋⇒≅ p with length-equal p
... | refl = H.≡-to-≅ (≋⇒≡ p)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Construct.Constant where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels using (hProp)

open import Cubical.Relation.Binary
open import Cubical.Structures.Carrier

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

Const : ∀ {a b ℓ} {A : Type a} {B : Type b} → hProp ℓ → REL A B ℓ
Const I = λ _ _ → I

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

module _ {a c} {A : Type a} {C : hProp c} where

  reflexive : ⟨ C ⟩ → Reflexive {A = A} (Const C)
  reflexive c = c

  symmetric : Symmetric {A = A} (Const C)
  symmetric c = c

  transitive : Transitive {A = A} (Const C)
  transitive c d = c

  isPartialEquivalence : IsPartialEquivalence {A = A} (Const C)
  isPartialEquivalence = record
    { symmetric  = λ {x} {y} → symmetric {x} {y}
    ; transitive = λ {x} {y} {z} → transitive {x} {y} {z}
    }

  partialEquivalence : PartialEquivalence A c
  partialEquivalence = record { isPartialEquivalence = isPartialEquivalence }

  isEquivalence : ⟨ C ⟩ → IsEquivalence {A = A} (Const C)
  isEquivalence c = record
    { isPartialEquivalence = isPartialEquivalence
    ; reflexive            = λ {x} → reflexive c {x}
    }

  equivalence : ⟨ C ⟩ → Equivalence A c
  equivalence x = record { isEquivalence = isEquivalence x }


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

module Erased-cubical-Pattern-matching-Cubical where

data D : Set where
  c₁ c₂ : D

max_stars_repo_name: sseefried/agda


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

module Numeral.Natural.Equiv.Path where

open import Data.Boolean.Equiv.Path
open import Functional
open import Logic.Propositional
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural
open import Relator.Equals.Proofs.Equivalence using () renaming ([≡]-equiv to Id-equiv ; [≡]-symmetry to Id-symmetry ; [≡]-to-function to Id-to-function ; [≡]-function to Id-function)
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Relator.Properties
open import Type.Cubical.Path.Equality
open import Type.Cubical.Path
open import Type.Identity

instance
  𝐒-injective : Injective(𝐒)
  Injective.proof 𝐒-injective p = congruence₁(𝐏) p

ℕ-Path-to-Id : ∀{x y : ℕ} → (Path x y) → (Id x y)
ℕ-Path-to-Id {𝟎}   {𝟎}   p = intro
ℕ-Path-to-Id {𝟎}   {𝐒 y}   = [⊥]-elim ∘ Bool-different-values ∘ congruence₁(positive?)
ℕ-Path-to-Id {𝐒 x} {𝟎}     = [⊥]-elim ∘ Bool-different-values ∘ symmetry(Path) ∘ congruence₁(positive?)
ℕ-Path-to-Id {𝐒 x} {𝐒 y} p = congruence₁ ⦃ Id-equiv ⦄ ⦃ Id-equiv ⦄ (ℕ.𝐒) ⦃ Id-function ⦄ (ℕ-Path-to-Id {x}{y} (injective(ℕ.𝐒) p))

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:
module List.Order.Bounded {A : Set}(_≤_ : A → A → Set)  where

open import Bound.Total A
open import Bound.Total.Order _≤_
open import Data.List

data _≤*_ : List A → Bound → Set where
  lenx : {t : Bound} → [] ≤* t
  lecx : {t : Bound}{x : A}{xs : List A} → LeB (val x) t → xs ≤* t → (x ∷ xs) ≤* t

data _*≤_ : Bound → List A → Set where
  genx : {b : Bound} → b *≤ []
  gecx : {b : Bound}{x : A}{xs : List A} → LeB b (val x) → b *≤ xs → b *≤ (x ∷ xs)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{-# OPTIONS --safe --without-K #-}
module Source.Size.Substitution.Theory where

open import Source.Size
open import Source.Size.Substitution.Canonical as SC using (Sub⊢)
open import Source.Size.Substitution.Universe as SU using (⟨_⟩ ; Sub⊢ᵤ)
open import Util.Prelude

record SubTheory (A : Ctx → Set) : Set where
  infixl 5 _[_] _[_]ᵤ
  field
    _[_] : A Ω → SC.Sub Δ Ω → A Δ
    [Id] : ∀ {Δ} (a : A Δ) → a [ SC.Id ] ≡ a
    [>>] : ∀ {Δ Δ′ Δ″} (σ : SC.Sub Δ Δ′) (τ : SC.Sub Δ′ Δ″) a
      → a [ σ SC.>> τ ] ≡ a [ τ ] [ σ ]

  abstract
    [Id]′ : ∀ {Δ} {σ : SC.Sub Δ Δ} a
      → σ ≡ SC.Id
      → a [ σ ] ≡ a
    [Id]′ a refl = [Id] a

    [>>]′ : ∀ {Δ Δ′ Δ″} (ι : SC.Sub Δ Δ″) (σ : SC.Sub Δ Δ′) (τ : SC.Sub Δ′ Δ″) a
      → ι ≡ σ SC.>> τ
      → a [ ι ] ≡ a [ τ ] [ σ ]
    [>>]′ ι σ τ a refl = [>>] σ τ a

    [>>]″ :  ∀ {Δ Δ′ Δ″} (σ : SC.Sub Δ Δ′) (τ : SC.Sub Δ′ Δ″)
      → ∀ (σ′ : SC.Sub Δ Ω) (τ′ : SC.Sub Ω Δ″) a
      → σ SC.>> τ ≡ σ′ SC.>> τ′
      → a [ τ ] [ σ ] ≡ a [ τ′ ] [ σ′ ]
    [>>]″ σ τ σ′ τ′ a eq
      = trans (sym ([>>] σ τ a)) (trans (cong (λ σ → a [ σ ]) eq) ([>>] σ′ τ′ a))

  _[_]ᵤ : A Ω → SU.Sub Δ Ω → A Δ
  a [ σ ]ᵤ = a [ ⟨ σ ⟩ ]

  abstract
    []ᵤ-resp-≈ : ∀ {Δ Ω} {σ τ : SU.Sub Δ Ω}
      → σ SU.≈ τ
      → ∀ a
      → a [ σ ]ᵤ ≡ a [ τ ]ᵤ
    []ᵤ-resp-≈ (SU.≈⁺ p) a = cong (λ σ → a [ σ ]) p

    [Id]ᵤ : ∀ {Δ} (a : A Δ) → a [ SU.Id ]ᵤ ≡ a
    [Id]ᵤ a = [Id] a

    [Id]ᵤ′ : ∀ {Δ} {σ : SU.Sub Δ Δ} (a : A Δ)
      → σ SU.≈ SU.Id
      → a [ σ ]ᵤ ≡ a
    [Id]ᵤ′ a (SU.≈⁺ p) = [Id]′ a p

    [>>]ᵤ : ∀ {Δ Δ′ Δ″} (σ : SU.Sub Δ Δ′) (τ : SU.Sub Δ′ Δ″) (a : A Δ″)
      → a [ σ SU.>> τ ]ᵤ ≡ a [ τ ]ᵤ [ σ ]ᵤ
    [>>]ᵤ σ τ a = [>>] _ _ _

    [>>]ᵤ′ : ∀ {Δ Δ′ Δ″} (ι : SU.Sub Δ Δ″) (σ : SU.Sub Δ Δ′) (τ : SU.Sub Δ′ Δ″) a
      → ι SU.≈ σ SU.>> τ
      → a [ ι ]ᵤ ≡ a [ τ ]ᵤ [ σ ]ᵤ
    [>>]ᵤ′ ι σ τ a (SU.≈⁺ p) = [>>]′ ⟨ ι ⟩ ⟨ σ ⟩ ⟨ τ ⟩ a p

    [>>]ᵤ″ :  ∀ {Δ Δ′ Δ″} (σ : SU.Sub Δ Δ′) (τ : SU.Sub Δ′ Δ″)
      → ∀ (σ′ : SU.Sub Δ Ω) (τ′ : SU.Sub Ω Δ″) a
      → σ SU.>> τ SU.≈ σ′ SU.>> τ′
      → a [ τ ]ᵤ [ σ ]ᵤ ≡ a [ τ′ ]ᵤ [ σ′ ]ᵤ
    [>>]ᵤ″ σ τ σ′ τ′ a (SU.≈⁺ p) = [>>]″ ⟨ σ ⟩ ⟨ τ ⟩ ⟨ σ′ ⟩ ⟨ τ′ ⟩ a p

open SubTheory {{...}} public

instance
  SubTheory-Size : SubTheory Size
  SubTheory-Size = record
    { _[_] = λ n σ → SC.sub σ n
    ; [Id] = λ n → SC.sub-Id n refl
    ; [>>] = λ σ τ n → SC.sub->> n refl
    }

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


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

module LateExpansionOfRecordMeta where

postulate
  I : Set
  i : I
  A : I → Set
  a : A i

data D : Set₁ where
  d : (P : A i → Set) → P a → D

record R (P : A i → Set) : Set where
  field
    p : P a

record ID : Set₁ where
  field
    P   : (i : I) → A i → Set
    isR : R (P i)

at : ID → D
at id = d (ID.P id i) (R.p (ID.isR id))

postulate
  T  : D → Set
  F  : (id : ID) → T (at id) → Set
  id : ID

foo : T (at id) → Set
foo t = F _ t

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module lib.libraryString where

open import Data.String
open import Data.Bool
open import Agda.Builtin.String using ( primStringEquality )
open import Data.String public using ()
                               renaming (toList to primStringToList;
                                        _++_  to _++Str_)

_==Str_ : String → String → Bool
_==Str_ = primStringEquality


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

module Light.Variable.Levels where

open import Light.Level using (Level)

variable ℓ aℓ bℓ cℓ dℓ eℓ fℓ gℓ hℓ : Level

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module ReasoningEx where

open import Prelude
open import T
open import Contexts
open import Eq
open import Eq.Theory
open import Eq.ObsTheory

---- some example programs
-- boy, de bruijn indexes are unreadable
w = weaken-closed

plus-rec : ∀{Γ} → TExp Γ nat → TExp Γ nat → TExp Γ nat
plus-rec n m = rec n m (suc (var Z))

t-plus1 : TCExp (nat ⇒ nat ⇒ nat)
t-plus1 = Λ (Λ (plus-rec (var Z) (var (S Z))))
t-plus2 : TCExp (nat ⇒ nat ⇒ nat)
t-plus2 = Λ (Λ (plus-rec (var (S Z)) (var Z)))

plus-adds : ∀{Γ} → (n : Nat) (m : Nat) →
            Γ ⊢ plus-rec (t-numeral n) (t-numeral m) ≅ t-numeral (n +n m) :: nat
plus-adds Z m = obs-contains-def def-rec-z
plus-adds {Γ} (S n) m with
  (def-rec-s {Γ} {e = (t-numeral n)} {e0 = t-numeral m} {es = suc (var Z)})
-- If I don't name the def eq thing above and use it directly, agda uses all my core.
... | bullshit-workaround with obs-contains-def bullshit-workaround
... | step-eq with obs-congruence (plus-adds {Γ} n m) (suc ∘)
... | reccase = obs-trans step-eq reccase

help : (n : Nat) → ObservEq (nat :: []) nat
                   (rec (t-numeral n) (var Z) (suc (var Z)))
                   (rec (var Z) (t-numeral n) (suc (var Z)))
help n = {!!}

plus-commutes : [] ⊢ t-plus1 ≅ t-plus2 :: nat ⇒ nat ⇒ nat
plus-commutes with
  def-cong (def-beta {e = Λ (plus-rec (var Z) (var (S Z)))} {e' = var (S Z)}) (∘ $e var Z) |
  def-cong (def-beta {e = Λ (plus-rec (var (S Z)) (var Z))} {e' = var (S Z)}) (∘ $e var Z)
... | beq1 | beq2 with def-beta {e = plus-rec (var Z) (var (S (S Z)))} {e' = var Z} |
                       def-beta {e = plus-rec (var (S (S Z))) (var Z)} {e' = var Z}
... | beq1' | beq2' with obs-contains-def (def-trans beq1 beq1') | obs-contains-def (def-trans beq2 beq2')
... | oeq1 | oeq2 with function-induction-obs help
... | main-eq with obs-trans oeq1 (obs-trans main-eq (obs-sym oeq2))
... | lol = function-ext-obs (function-ext-obs lol)

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
{-# OPTIONS --rewriting --confluence-check #-}
module Issue4333.N where

open import Issue4333.M
open import Issue4333.N0
open import Issue4333.N1

postulate
  of-type : (X : Set) (x : X) → Set

-- Subject reduction violated for b₁' = b.
_ = of-type (B a₁') b₁'
_ = of-type (B a₀') b


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

open import HoTT

module homotopy.ConstantToSetFactorization
  {i j} {A : Type i} {B : Type j} (B-is-set : is-set B)
  (f : A → B) (f-is-const : ∀ a₁ a₂ → f a₁ == f a₂) where

  private
    Skel = SetQuotient {A = A} (λ _ _ → Unit)

    abstract
      Skel-has-all-paths : has-all-paths Skel
      Skel-has-all-paths =
        SetQuot-elim (λ _ → Π-is-set λ _ → =-preserves-set SetQuotient-is-set)
          (λ a₁ →
            SetQuot-elim {P = λ s₂ → q[ a₁ ] == s₂}
              (λ _ → =-preserves-set SetQuotient-is-set)
              (λ _ → quot-rel _)
              (λ _ → prop-has-all-paths-↓ (SetQuotient-is-set _ _)))
          (λ {a₁ a₂} _ → ↓-cst→app-in λ s₂ →
              prop-has-all-paths-↓ (SetQuotient-is-set _ _))

    Skel-is-prop : is-prop Skel
    Skel-is-prop = all-paths-is-prop Skel-has-all-paths

    Skel-lift : Skel → B
    Skel-lift = SetQuot-rec B-is-set f (λ {a₁ a₂} _ → f-is-const a₁ a₂)

  cst-extend : Trunc -1 A → B
  cst-extend = Skel-lift ∘ Trunc-rec Skel-is-prop q[_]

  -- The beta rule.
  -- This is definitionally true, so you don't need it.
  cst-extend-β : cst-extend ∘ [_] == f
  cst-extend-β = idp

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Cats.Functor.Representable where

open import Data.Product using (_×_ ; _,_)
open import Relation.Binary using (Setoid)

open import Cats.Bifunctor using (Bifunctor)
open import Cats.Category
open import Cats.Category.Op using (_ᵒᵖ)
open import Cats.Category.Setoids as Setoids using (Setoids ; ≈-intro)
open import Cats.Util.Simp using (simp!)
open import Cats.Util.SetoidReasoning

import Relation.Binary.PropositionalEquality as ≡

module Build {lo la l≈} (C : Category lo la l≈) where

  open Category C renaming (Hom to Homset)
  open Setoids._⇒_ using (arr ; resp)

  private
    module S = Category (Setoids la l≈)

  fmap : ∀ {A B A′ B′} → (A′ ⇒ A) × (B ⇒ B′) → Homset A B S.⇒ Homset A′ B′
  fmap {A} {B} {A′} {B′} (f , g) = record
      { arr = λ h → g ∘ h ∘ f
      ; resp = λ h≈i → ∘-resp-r (∘-resp-l h≈i)
      }

  Hom : Bifunctor (C ᵒᵖ) C (Setoids la l≈)
  Hom = record
      { fobj = λ { (A , B) → Homset A B }
      ; fmap = fmap
      ; fmap-resp = λ where
          (f≈g , h≈i) → ≈-intro λ x≈y → ∘-resp h≈i (∘-resp x≈y f≈g)
      ; fmap-id = ≈-intro λ x≈y → ≈.trans id-l (≈.trans id-r x≈y)
      ; fmap-∘ = λ where
          {A , B} {A′ , B′} {A″ , B″} {f , f′} {g , g′} → ≈-intro λ {x} {y} x≈y →
            begin⟨ Homset A″ B″ ⟩
              f′ ∘ (g′ ∘ x ∘ g) ∘ f
            ≈⟨ simp! C ⟩
              (f′ ∘ g′) ∘ x ∘ g ∘ f
            ≈⟨ ∘-resp-r (∘-resp-l x≈y) ⟩
              (f′ ∘ g′) ∘ y ∘ g ∘ f
            ∎
      }

open Build public using () renaming (Hom to Hom[_])

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --without-K #-}
module Computability.Prelude where

open import Data.Bool public using (Bool; false; true)
open import Data.Empty public using (⊥; ⊥-elim)
open import Data.Nat public using (ℕ; zero; suc; _+_; _*_)
open import Data.Product public using (Σ; Σ-syntax; _×_; _,_; proj₁; proj₂)
open import Data.Sum public using (_⊎_)
open import Data.Unit public using (⊤)
open import Relation.Binary.PropositionalEquality public using (_≡_; refl)
open import Level public using (Level) renaming (zero to lzero; suc to lsuc)

max_stars_repo_name: jesyspa/computability-in-agda

max_issues_repo_name: jesyspa/computability-in-agda

max_forks_repo_name: jesyspa/computability-in-agda


text:
module UniDB.Morph.Bla where

open import UniDB.Spec
open import UniDB.Morph.WeakenOne
open import UniDB.Morph.Sub
open import UniDB.Morph.ShiftsPrime
open import UniDB.Morph.Subs

-- mutual
--   data BlaSubst (T : STX) : MOR where
--     blasubst : {γ₁ γ₂ : Dom} → BlaSubst T γ₁ γ₂

mutual
  data BlaWeak* (T : STX) : MOR where
    reflW : {γ : Dom}     → BlaWeak* T γ γ
    inclW : {γ₁ γ₂ : Dom} → BlaWeak+ T γ₁ γ₂ → BlaWeak* T γ₁ γ₂
    skipW : {γ₁ γ₂ : Dom} → Bla T γ₁ γ₂ → BlaWeak* T (suc γ₁) (suc γ₂)

  data BlaWeak+ (T : STX) : MOR where
    stepW : {γ₁ γ₂ γ₃ : Dom} → Weaken₁ γ₁ γ₂ → BlaWeak* T γ₂ γ₃ → BlaWeak T γ₁ γ₃

  data BlaSubs* (T : STX) : MOR where
    reflS : {γ : Dom}     → BlaSubs* T γ γ
    inclS : {γ₁ γ₂ : Dom} → BlaSubs+ T γ₁ γ₂ → BlaSubs* T γ₁ γ₂
    skipS : {γ₁ γ₂ : Dom} → Bla T γ₁ γ₂ → BlaSubs* T (suc γ₁) (suc γ₂)

  data BlaSubs+ (T : STX) : MOR where
    stepS : {γ₁ γ₂ γ₃ : Dom} → BlaSubs* T γ₁ γ₂ → Single T γ₂ γ₃ → BlaWeak T γ₁ γ₃

  data Bla (T : STX) : MOR where
    refl : {γ : Dom} → Shifts* γ γ
    incl : {γ₁ γ₂ : Dom} (ξ : Shifts+ γ₁ γ₂) → Shifts* γ₁ γ₂

  data Shifts+ : MOR where
    step : {γ₁ γ₂ : Dom} (ξ : Shifts* γ₁ γ₂) → Shifts+ γ₁ (suc γ₂)
    skip : {γ₁ γ₂ : Dom} (ξ : Shifts+ γ₁ γ₂) → Shifts+ (suc γ₁) (suc γ₂)

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


text:
open import Categories.Category using (Category)
import Categories.Category.CartesianClosed

open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.List using (List; []; _∷_)
open import Data.Product using (Σ; Σ-syntax; proj₁; proj₂)

open import Syntax

open import Level using (_⊔_; suc)

module Semantics {o ℓ e}
  (𝒞 : Category o ℓ e)
  (CC : Categories.Category.CartesianClosed.CartesianClosed 𝒞)
  {ℓ₁ ℓ₂}
  (Sg : Signature ℓ₁ ℓ₂)
  where
  open Categories.Category.CartesianClosed 𝒞
  open import Categories.Category.Cartesian 𝒞
  open import Categories.Category.BinaryProducts 𝒞
  open import Categories.Object.Terminal 𝒞
  open import Categories.Object.Product 𝒞

  open Category 𝒞

  open CartesianClosed CC
  open Cartesian cartesian
  open BinaryProducts products
  private module T = Terminal terminal

  open Signature Sg
  open Term Sg

  module I (⟦_⟧G : Gr -> Obj) where
    ⟦_⟧T : Type -> Obj
    ⟦ ⌊ g ⌋ ⟧T = ⟦ g ⟧G
    ⟦ Unit ⟧T = T.⊤
    ⟦ A * A₁ ⟧T = ⟦ A ⟧T × ⟦ A₁ ⟧T
    ⟦ A => A₁ ⟧T = ⟦ A ⟧T ⇨ ⟦ A₁ ⟧T

  record Structure : Set (o ⊔ ℓ ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      ⟦_⟧G : Gr -> Obj

    open I ⟦_⟧G public

    field
      ⟦_⟧F : (f : Func) -> ⟦ dom f ⟧T ⇒ ⟦ cod f ⟧T

    ⟦_⟧C : Context -> Obj
    ⟦ [] ⟧C = T.⊤
    ⟦ A ∷ Γ ⟧C = ⟦ Γ ⟧C × ⟦ A ⟧T

    ⟦_⟧ : forall {Γ A} -> Γ ⊢ A -> ⟦ Γ ⟧C ⇒ ⟦ A ⟧T
    ⟦_⟧S : forall {Γ Γ′} -> Γ ⊨ Γ′ -> ⟦ Γ ⟧C ⇒ ⟦ Γ′ ⟧C

    ⟦ func f e ⟧ = ⟦ f ⟧F ∘ ⟦ e ⟧
    ⟦ var ⟧ = π₂
    ⟦ unit ⟧ = T.!
    ⟦ pair e e₁ ⟧ = ⟨ ⟦ e ⟧ , ⟦ e₁ ⟧ ⟩
    ⟦ fst e ⟧ = π₁ ∘ ⟦ e ⟧
    ⟦ snd e ⟧ = π₂ ∘ ⟦ e ⟧
    ⟦ abs e ⟧ = λg ⟦ e ⟧
    ⟦ app e e₁ ⟧ = eval′ ∘ ⟨ ⟦ e ⟧ , ⟦ e₁ ⟧ ⟩
    ⟦ e [ γ ] ⟧ = ⟦ e ⟧ ∘ ⟦ γ ⟧S

    ⟦ id ⟧S = Category.id 𝒞
    ⟦ γ ∙ γ₁ ⟧S = ⟦ γ ⟧S ∘ ⟦ γ₁ ⟧S
    ⟦ weaken ⟧S = π₁
    ⟦ ext γ e ⟧S = ⟨ ⟦ γ ⟧S , ⟦ e ⟧ ⟩
    ⟦ ! ⟧S = T.!

  ⟦_⟧G_ : Gr -> (M : Structure) -> Obj
  ⟦_⟧G_ g M = Structure.⟦_⟧G M g

  ⟦_⟧T_ : Type -> (M : Structure) -> Obj
  ⟦_⟧T_ A M = Structure.⟦_⟧T M A

  ⟦_⟧F_ : (f : Func) -> (M : Structure) -> Structure.⟦_⟧T M (dom f) ⇒ Structure.⟦_⟧T M (cod f)
  ⟦_⟧F_ f M = Structure.⟦_⟧F M f

  ⟦_⟧_ : forall {Γ A} -> Γ ⊢ A -> (M : Structure) -> Structure.⟦_⟧C M Γ ⇒ Structure.⟦_⟧T M A
  ⟦_⟧_ e M = Structure.⟦_⟧ M e

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
{-# OPTIONS --without-K #-}
module Util.Induction.WellFounded where

open import Induction.WellFounded public using
  ( Acc ; acc ; WellFounded ; module Subrelation ; module InverseImage
  ; module TransitiveClosure ; module Lexicographic )

open import Relation.Binary using (Rel)

open import Util.HoTT.FunctionalExtensionality using (funext)
open import Util.HoTT.HLevel using (IsProp ; ∀-IsProp)
open import Util.Prelude

module _ {α β} {A : Set α} {_<_ : Rel A β} where

  Acc-IsProp : ∀ {x} → IsProp (Acc _<_ x)
  Acc-IsProp (acc rs₀) (acc rs₁)
    = cong acc (funext λ y → funext λ y<x → Acc-IsProp _ _)

  WellFounded-IsProp : IsProp (WellFounded _<_)
  WellFounded-IsProp = ∀-IsProp λ _ → Acc-IsProp

  wfInd-acc : ∀ {γ} (P : A → Set γ)
    → (∀ x → (∀ y → y < x → P y) → P x)
    → ∀ x → Acc _<_ x → P x
  wfInd-acc P f x (acc rs) = f x (λ y y<x → wfInd-acc P f y (rs y y<x))

  mutual
    wfIndΣ-acc : ∀ {γ} (P : A → Set γ)
      → (Q : ∀ x y → P x → P y → Set)
      → (f : ∀ x
          → (g : ∀ y → y < x → P y)
          → (∀ y y<x z z<x → Q y z (g y y<x) (g z z<x))
          → P x)
      → (∀ x g g-resp y h h-resp
          → (∀ z z<x z′ z′<y → Q z z′ (g z z<x) (h z′ z′<y))
          → Q x y (f x g g-resp) (f y h h-resp))
      → ∀ x → Acc _<_ x → P x
    wfIndΣ-acc P Q f f-resp x (acc rs)
      = f x
         (λ y y<x → wfIndΣ-acc P Q f f-resp y (rs y y<x))
         (λ y y<x z z<x
            → wfIndΣ-acc-resp P Q f f-resp y (rs y y<x) z (rs z z<x))

    wfIndΣ-acc-resp : ∀ {γ} (P : A → Set γ)
      → (Q : ∀ x y → P x → P y → Set)
      → (f : ∀ x
          → (g : ∀ y → y < x → P y)
          → (∀ y y<x z z<x → Q y z (g y y<x) (g z z<x))
          → P x)
      → (f-resp : ∀ x g g-resp y h h-resp
          → (∀ z z<x z′ z′<y → Q z z′ (g z z<x) (h z′ z′<y))
          → Q x y (f x g g-resp) (f y h h-resp))
      → ∀ x x-acc y y-acc
      → Q x y (wfIndΣ-acc P Q f f-resp x x-acc) (wfIndΣ-acc P Q f f-resp y y-acc)
    wfIndΣ-acc-resp P Q f f-resp x (acc rsx) y (acc rsy)
      = f-resp _ _ _ _ _ _ λ z z<x z′ z′<y
          → wfIndΣ-acc-resp P Q f f-resp z (rsx z z<x) z′ (rsy z′ z′<y)

  module Build (<-wf : WellFounded _<_) where

    wfInd : ∀ {γ} (P : A → Set γ)
      → (∀ x → (∀ y → y < x → P y) → P x)
      → ∀ x → P x
    wfInd P f x = wfInd-acc P f x (<-wf x)

    wfRec : ∀ {γ} {B : Set γ}
      → (∀ x → (∀ y → y < x → B) → B)
      → A → B
    wfRec = wfInd _

    wfInd-unfold : ∀ {γ} (P : A → Set γ)
      → (f : ∀ x → (∀ y → y < x → P y) → P x)
      → (x : A)
      → wfInd P f x ≡ f x (λ y _ → wfInd P f y)
    wfInd-unfold P f x with <-wf x
    ... | acc rs
      = cong (f x)
          (funext λ y → funext λ y<x →
            cong (wfInd-acc P f y) (Acc-IsProp (rs y y<x) (<-wf y)))

    wfRec-unfold : ∀ {γ} {B : Set γ}
      → (f : ∀ x → (∀ y → y < x → B) → B)
      → (x : A)
      → wfRec f x ≡ f x (λ y _ → wfRec f y)
    wfRec-unfold = wfInd-unfold _

    wfInd-ind : ∀ {γ} {P : A → Set γ}
      → (Q : ∀ x → P x → Set)
      → {f : ∀ x → (∀ y → y < x → P y) → P x}
      → (∀ x g
          → (∀ y y<x → Q y (g y y<x))
          → Q x (f x g))
      → {x : A}
      → Q x (wfInd P f x)
    wfInd-ind {P = P} Q {f} f-resp
      = wfInd (λ x → Q x (wfInd P f x))
          (λ x rec → subst (Q x) (sym (wfInd-unfold P f x))
            (f-resp _ _ rec))
          _

    module _ {γ} (P : A → Set γ)
      (Q : ∀ x y → P x → P y → Set)
      (f : ∀ x
        → (g : ∀ y → y < x → P y)
        → (∀ y y<x z z<x → Q y z (g y y<x) (g z z<x))
        → P x)
      (f-resp : ∀ x g g-resp y h h-resp
        → (∀ z z<x z′ z′<y → Q z z′ (g z z<x) (h z′ z′<y))
        → Q x y (f x g g-resp) (f y h h-resp))
      where

      wfIndΣ : Σ[ f ∈ (∀ x → P x) ] (∀ x y → Q x y (f x) (f y))
      wfIndΣ
        = (λ x → wfIndΣ-acc P Q f f-resp x (<-wf x))
        , λ x y → wfIndΣ-acc-resp P Q f f-resp x (<-wf x) y (<-wf y)

      wfIndΣ-unfold : ∀ {x}
        → wfIndΣ .proj₁ x
        ≡ f x (λ y y<x → wfIndΣ .proj₁ y)
            (λ y y<x z z<x → wfIndΣ .proj₂ y z)
      wfIndΣ-unfold {x} with <-wf x
      ... | acc rs
        = go rs (λ y y<x → <-wf y)
        where
          go : (p q : (y : A) → y < x → Acc _<_ y)
            → f x (λ y y<x → wfIndΣ-acc P Q f f-resp y (p y y<x))
                (λ y y<x z z<x
                  → wfIndΣ-acc-resp P Q f f-resp y (p y y<x) z (p z z<x))
            ≡ f x (λ y y<x → wfIndΣ-acc P Q f f-resp y (q y y<x))
                (λ y y<x z z<x
                  → wfIndΣ-acc-resp P Q f f-resp y (q y y<x) z (q z z<x))
          go p q
            rewrite (funext λ y → funext λ y<x → Acc-IsProp (p y y<x) (q y y<x))
            = refl

      wfIndΣ′ : Σ[ g ∈ (∀ x → P x) ]
        Σ[ g-param ∈ (∀ x y → Q x y (g x) (g y)) ]
          (∀ {x} → g x ≡ f x (λ y y<x → g y) (λ y y<x z z<x → g-param y z))
      wfIndΣ′ = wfIndΣ .proj₁ , wfIndΣ .proj₂ , wfIndΣ-unfold

  open Build public

module _ {α β γ δ} {A : Set α} {B : Set β} where

  ×-Rel : Rel A γ → Rel B δ → Rel (A × B) (γ ⊔ℓ δ)
  ×-Rel R S (a , b) (a′ , b′) = R a a′ × S b b′

  ×-wellFounded : {R : Rel A γ} {S : Rel B δ}
    → WellFounded R → WellFounded S → WellFounded (×-Rel R S)
  ×-wellFounded {R} {S} R-wf S-wf (a , b) = ×-acc (R-wf a) (S-wf b)
    where
      ×-acc : ∀ {x y} → Acc R x → Acc S y → Acc (×-Rel R S) (x , y)
      ×-acc (acc rsa) (acc rsb)
        = acc (λ { (a , b) (a<x , b<y) → ×-acc (rsa a a<x) (rsb b b<y) })

-- This is not in Build because the implementation uses wfInd at
-- (×-Rel _<_ _<_), but within Build, we can only use wfInd at
-- _<_.
wfInd-ind₂ : ∀ {α β} {A : Set α} {_<_ : Rel A β}
  → (<-wf : WellFounded _<_)
  → ∀ {γ} {P : A → Set γ}
  → (R : ∀ x y → P x → P y → Set)
  → {f : ∀ x → (∀ y → y < x → P y) → P x}
  → (∀ x x′ g g′
      → (∀ y y′ y<x y′<x → R y y′ (g y y<x) (g′ y′ y′<x))
      → R x x′ (f x g) (f x′ g′))
  → {x x′ : A}
  → R x x′ (wfInd <-wf P f x) (wfInd <-wf P f x′)
wfInd-ind₂ <-wf {P = P} R {f} f-resp
  = wfInd (×-wellFounded <-wf <-wf)
      (λ { (x , x′) → R x x′ (wfInd <-wf P f x) (wfInd <-wf P f x′)})
      (λ where
        (x , y) rec
          → subst₂ (R x y)
              (sym (wfInd-unfold <-wf P f x))
              (sym (wfInd-unfold <-wf P f y))
              (f-resp x y _ _ λ x′ y′ x′<x y′<y → rec (x′ , y′) (x′<x , y′<y)))
      _


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Rational as ℚ using (ℚ)
open import Data.List
open import Relation.Binary.PropositionalEquality

module autoencoderError-output where

private
  VEHICLE_PROJECT_FILE = "TODO_projectFile"

encode : Tensor ℚ (5 ∷ []) → Tensor ℚ (2 ∷ [])
encode = evaluate record
  { projectFile = VEHICLE_PROJECT_FILE
  ; networkUUID = "TODO_networkUUID"
  }

decode : Tensor ℚ (2 ∷ []) → Tensor ℚ (5 ∷ [])
decode = evaluate record
  { projectFile = VEHICLE_PROJECT_FILE
  ; networkUUID = "TODO_networkUUID"
  }

abstract
  identity : ∀ (x : Tensor ℚ (5 ∷ [])) → decode (encode x) ≡ x
  identity = checkProperty record
    { projectFile  = VEHICLE_PROJECT_FILE
    ; propertyUUID = "TODO_propertyUUID"
    }

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: wenkokke/vehicle


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

{-
Imports everything that is not imported by something else.
This is not supposed to be used anywhere, this is just a simple way to
do `make all'

This file is intentionally named index.agda so that
Agda will generate index.html.

  favonia:
  On 2017/05/08, I further partition the results into multiple
  independent index[n].agda files because the garbage collection
  is not really working.
-}

module index1 where

{- some group theory results -}
import groups.ReducedWord
import groups.ProductRepr
import groups.CoefficientExtensionality

{- homotopy groups of circles -}
import homotopy.LoopSpaceCircle
import homotopy.PinSn
import homotopy.HopfJunior
import homotopy.Hopf

{- cohomology -}
import cohomology.EMModel
import cohomology.Sigma
import cohomology.Coproduct
import cohomology.Torus
import cohomology.InverseInSusp
import cohomology.MayerVietoris
-- import cohomology.MayerVietorisExact -- FIXME

{- prop * prop is still a prop -}
import homotopy.PropJoinProp

{- a space with preassigned homotopy groups -}
import homotopy.SpaceFromGroups

{- pushout 3x3 lemma -}
{- These takes lots of time and memory to check. -}
-- import homotopy.3x3.Commutes -- commented out because this does not run on travis.
-- import homotopy.JoinAssoc3x3 -- commented out because this does not run on travis.

{- covering spaces -}
import homotopy.GroupSetsRepresentCovers
import homotopy.AnyUniversalCoverIsPathSet
import homotopy.PathSetIsInitalCover
import homotopy.CircleCover

{- van kampen -}
-- see index3.agda

{- blakers massey -}
-- see index3.agda

{- cw complexes -}
-- see index2.agda

-- There are some unported theorems

-- import Spaces.IntervalProps
-- import Algebra.F2NotCommutative
-- import Spaces.LoopSpaceDecidableWedgeCircles
-- import Homotopy.PullbackIsPullback
-- import Homotopy.PushoutIsPushout
-- import Homotopy.Truncation
-- import Sets.QuotientUP

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import lib.Basics
open import lib.NConnected
open import lib.NType2
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Truncation
open import lib.types.Unit
open import lib.types.Bool
open import lib.types.Suspension
open import lib.types.IteratedSuspension

module lib.types.Circle where

{-
Idea :

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

I’m using Dan Licata’s trick to have a higher inductive type with definitional
reduction rule for [base]
-}

{-
  favonia (2016/05): Now [Circle] is defined as [Sphere 1].
-}

module _ where
  -- (already defined in IteratedSuspension.agda)
  -- S¹ : Type₀
  -- S¹ = Sphere 1

  base : S¹
  base = north

  loop : base == base
  loop = σloop ⊙Bool false

  module S¹Elim {i} {P : S¹ → Type i} (base* : P base)
    (loop* : base* == base* [ P ↓ loop ]) where

    private
      north* = base*
      south* = transport P (merid false) base*
      merid*-general :
        ∀ {x : S¹} (p q : base == x)
          (loop* :  base* == base* [ P ↓ p ∙ ! q ]) (b : Bool)
        → base* == transport P p base* [ P ↓ Bool-rec q p b ]
      merid*-general idp q loop* false = idp
      merid*-general idp q loop* true = !ᵈ' loop*

      merid* : ∀ (b : Bool) → north* == south* [ P ↓ merid b ]
      merid* false = merid*-general (merid false) (merid true) loop* false
      merid* true = merid*-general (merid false) (merid true) loop* true

      module SE = SuspElim north* south* merid*

    f : Π S¹ P
    f = SE.f

    private
      merid*-general-lemma :
        ∀ {x : S¹} (p q : base == x) (loop* :  base* == base* [ P ↓ p ∙ ! q ])
        → merid*-general p q loop* false ◃ !ᵈ (merid*-general p q loop* true) == loop*
      merid*-general-lemma idp q loop* = idp◃ _ ∙ !ᵈ-!ᵈ' loop*

    loop-β : apd f loop == loop*
    loop-β =
      apd f loop
        =⟨ apd-∙ f (merid false) (! (merid true)) ⟩
      apd f (merid false) ◃ apd f (! (merid true))
        =⟨ apd-! f (merid true) |in-ctx apd f (merid false) ◃_ ⟩
      apd f (merid false) ◃ !ᵈ (apd f (merid true))
        =⟨ SE.merid-β false |in-ctx _◃ !ᵈ (apd f (merid true)) ⟩
      merid* false ◃ !ᵈ (apd f (merid true))
        =⟨ SE.merid-β true |in-ctx (λ p → merid* false ◃ !ᵈ p) ⟩
      merid* false ◃ !ᵈ (merid* true)
        =⟨ merid*-general-lemma (merid false) (merid true) loop* ⟩
      loop*
        =∎

open S¹Elim public using () renaming (f to S¹-elim)

module S¹Rec {i} {A : Type i} (base* : A) (loop* : base* == base*) where

  private
    module M = S¹Elim base* (↓-cst-in loop*)

  f : S¹ → A
  f = M.f

  loop-β : ap f loop == loop*
  loop-β = apd=cst-in {f = f} M.loop-β

open S¹Rec public using () renaming (f to S¹-rec)

S¹-rec-η : ∀ {i} {A : Type i} (f : S¹ → A)
  → ∀ x → S¹-rec (f base) (ap f loop) x == f x
S¹-rec-η f = S¹-elim idp (↓-='-in' $ ! $ S¹Rec.loop-β (f base) (ap f loop))

module S¹RecType {i} (A : Type i) (e : A ≃ A) where

  open S¹Rec A (ua e) public

  coe-loop-β : (a : A) → coe (ap f loop) a == –> e a
  coe-loop-β a =
    coe (ap f loop) a   =⟨ loop-β |in-ctx (λ u → coe u a) ⟩
    coe (ua e) a        =⟨ coe-β e a ⟩
    –> e a =∎

  coe!-loop-β : (a : A) → coe! (ap f loop) a == <– e a
  coe!-loop-β a =
    coe! (ap f loop) a   =⟨ loop-β |in-ctx (λ u → coe! u a) ⟩
    coe! (ua e) a        =⟨ coe!-β e a ⟩
    <– e a =∎

  ↓-loop-out : {a a' : A} → a == a' [ f ↓ loop ] → –> e a == a'
  ↓-loop-out {a} {a'} p =
    –> e a              =⟨ ! (coe-loop-β a) ⟩
    coe (ap f loop) a   =⟨ to-transp p ⟩
    a' =∎

  import lib.types.Generic1HIT as Generic1HIT
  module S¹G = Generic1HIT Unit Unit (idf _) (idf _)
  module P = S¹G.RecType (cst A) (cst e)

  private
    generic-S¹ : Σ S¹ f == Σ S¹G.T P.f
    generic-S¹ = eqv-tot where

      module To = S¹Rec (S¹G.cc tt) (S¹G.pp tt)
      to = To.f

      module From = S¹G.Rec (cst base) (cst loop)
      from : S¹G.T → S¹
      from = From.f

      abstract
        to-from : (x : S¹G.T) → to (from x) == x
        to-from = S¹G.elim (λ _ → idp) (λ _ → ↓-∘=idf-in' to from
          (ap to (ap from (S¹G.pp tt)) =⟨ From.pp-β tt |in-ctx ap to ⟩
           ap to loop                  =⟨ To.loop-β ⟩
           S¹G.pp tt =∎))

        from-to : (x : S¹) → from (to x) == x
        from-to = S¹-elim idp (↓-∘=idf-in' from to
          (ap from (ap to loop)   =⟨ To.loop-β |in-ctx ap from ⟩
           ap from (S¹G.pp tt)    =⟨ From.pp-β tt ⟩
           loop =∎))

      eqv : S¹ ≃ S¹G.T
      eqv = equiv to from to-from from-to

      eqv-fib : f == P.f [ (λ X → (X → Type _)) ↓ ua eqv ]
      eqv-fib =
        ↓-app→cst-in (λ {t} p → S¹-elim {P = λ t → f t == P.f (–> eqv t)} idp
          (↓-='-in'
            (ap (P.f ∘ (–> eqv)) loop   =⟨ ap-∘ P.f to loop ⟩
             ap P.f (ap to loop)        =⟨ To.loop-β |in-ctx ap P.f ⟩
             ap P.f (S¹G.pp tt)         =⟨ P.pp-β tt ⟩
             ua e                       =⟨ ! loop-β ⟩
             ap f loop =∎))
        t ∙ ap P.f (↓-idf-ua-out eqv p))

      eqv-tot : Σ S¹ f == Σ S¹G.T P.f
      eqv-tot = ap (uncurry Σ) (pair= (ua eqv) eqv-fib)

  import lib.types.Flattening as Flattening
  module FlatteningS¹ = Flattening
    Unit Unit (idf _) (idf _) (cst A) (cst e)
  open FlatteningS¹ public hiding (flattening-equiv; module P)

  flattening-S¹ : Σ S¹ f == Wt
  flattening-S¹ = generic-S¹ ∙ ua FlatteningS¹.flattening-equiv

instance
  S¹-conn : is-connected 0 S¹
  S¹-conn = Sphere-conn 1


text:
module _ where

open import Common.Prelude
open import Common.Reflection

postulate
  stuck : TC ⊤

macro
  not-so-good : Tactic
  not-so-good hole = stuck

fail : Nat
fail = not-so-good


text: import Issue2447.Type-error

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Cubical.Categories.Monoidal.Base where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Constructions.BinProduct
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.Functor.BinProduct
open import Cubical.Categories.Morphism
open import Cubical.Categories.NaturalTransformation.Base
open import Cubical.Foundations.Prelude

module _ {ℓ ℓ' : Level} (C : Category ℓ ℓ') where
  open Category C

  private
    record TensorStr : Type (ℓ-max ℓ ℓ') where
      field
        ─⊗─ : Functor (C × C) C
        unit : ob

      open Functor

      -- Useful tensor product notation
      _⊗_ : ob → ob → ob
      x ⊗ y = ─⊗─ .F-ob (x , y)

      _⊗ₕ_ : ∀ {x y z w} → Hom[ x , y ] → Hom[ z , w ]
           → Hom[ x ⊗ z , y ⊗ w ]
      f ⊗ₕ g = ─⊗─ .F-hom (f , g)

  record StrictMonStr : Type (ℓ-max ℓ ℓ') where
    field
      tenstr : TensorStr

    open TensorStr tenstr public

    field
      -- Axioms - strict
      assoc : ∀ x y z →  x ⊗ (y ⊗ z) ≡ (x ⊗ y) ⊗ z
      idl : ∀ x →  unit ⊗ x ≡ x
      idr : ∀ x →  x ⊗ unit ≡ x

  record MonoidalStr : Type (ℓ-max ℓ ℓ') where
    field
      tenstr : TensorStr

    open TensorStr tenstr public

    private
      -- Private names to make the axioms below look nice
      x⊗[y⊗z] : Functor (C × C × C) C
      x⊗[y⊗z] = ─⊗─ ∘F (𝟙⟨ C ⟩ ×F ─⊗─)

      [x⊗y]⊗z : Functor (C × C × C) C
      [x⊗y]⊗z = ─⊗─ ∘F (─⊗─ ×F 𝟙⟨ C ⟩) ∘F (×C-assoc C C C)

      x = 𝟙⟨ C ⟩
      1⊗x = ─⊗─ ∘F (rinj C C unit)
      x⊗1 = ─⊗─ ∘F (linj C C unit)

    field
      -- "Axioms" - up to natural isomorphism
      α : x⊗[y⊗z] ≅ᶜ [x⊗y]⊗z
      η : 1⊗x ≅ᶜ x
      ρ : x⊗1 ≅ᶜ x

    open NatIso

    -- More nice notations
    α⟨_,_,_⟩ : (x y z : ob) → Hom[ x ⊗ (y ⊗ z) , (x ⊗ y) ⊗ z ]
    α⟨ x , y , z ⟩ = α .trans ⟦ ( x , y , z ) ⟧

    η⟨_⟩ : (x : ob) → Hom[ unit ⊗ x , x ]
    η⟨ x ⟩ = η .trans ⟦ x ⟧

    ρ⟨_⟩ : (x : ob) → Hom[ x ⊗ unit , x ]
    ρ⟨ x ⟩ = ρ .trans ⟦ x ⟧

    field
      -- Coherence conditions
      pentagon : ∀ w x y z →
        id ⊗ₕ α⟨ x , y , z ⟩  ⋆  α⟨ w , x ⊗ y , z ⟩  ⋆  α⟨ w , x , y ⟩ ⊗ₕ id
            ≡   α⟨ w , x , y ⊗ z ⟩  ⋆  α⟨ w ⊗ x , y , z ⟩

      triangle : ∀ x y →
        α⟨ x , unit , y ⟩  ⋆  ρ⟨ x ⟩ ⊗ₕ id  ≡  id ⊗ₕ η⟨ y ⟩

    open isIso

    -- Inverses of α, η, ρ for convenience
    α⁻¹⟨_,_,_⟩ : (x y z : ob) → Hom[ (x ⊗ y) ⊗ z , x ⊗ (y ⊗ z) ]
    α⁻¹⟨ x , y , z ⟩ = α .nIso (x , y , z) .inv

    η⁻¹⟨_⟩ : (x : ob) → Hom[ x , unit ⊗ x ]
    η⁻¹⟨ x ⟩ = η .nIso (x) .inv

    ρ⁻¹⟨_⟩ : (x : ob) → Hom[ x , x ⊗ unit ]
    ρ⁻¹⟨ x ⟩ = ρ .nIso (x) .inv

record StrictMonCategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    C : Category ℓ ℓ'
    sms : StrictMonStr C

  open Category C public
  open StrictMonStr sms public

record MonoidalCategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    C : Category ℓ ℓ'
    monstr : MonoidalStr C

  open Category C public
  open MonoidalStr monstr public

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --copatterns #-}

module SplitResult where

open import Common.Product

test : {A B : Set} (a : A) (b : B) → A × B
test a b = {!!}

testFun : {A B : Set} (a : A) (b : B) → A × B
testFun = {!!}


text:
-- | NOTE: This module can only represent file paths which are valid strings.
-- On Linux, a file path may be an arbitrary sequence of bytes, but using anything
-- except utf8 for file paths is a terrible idea.
--
-- What should happen if we come across a non utf8 path from an untrusted source?
-- crash -> denial-of-service
-- ignore -> maybe security holes
--
-- Currently, the behaviour for non-textual file paths is undefined.
module System.FilePath where

open import Prelude.Unit
open import Prelude.String

data Kind : Set where
  Rel : Kind
  Abs : Kind

abstract
  record Path (kind : Kind) : Set where
    constructor mkPath
    field
      path : String

  open import Prelude.Monoid
  open Path

  _//_ : ∀ {k} → Path k → Path Rel → Path k
  x // y = mkPath (path x <> "/" <> path y)

  _∙_ : ∀ {k} → Path k → String → Path k
  p ∙ ext = mkPath (path p <> "." <> ext)

  toString : ∀ {k} → Path k → String
  toString p = path p

  relative : String → Path Rel
  relative = mkPath

  absolute : String → Path Abs
  absolute = mkPath

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


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

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing
open import Cubical.HITs.Ints.BiInvInt
  renaming (
    _+_ to _+ℤ_;
    -_ to _-ℤ_;
    +-assoc to +ℤ-assoc;
    +-comm to +ℤ-comm
  )

BiInvIntAsCommRing : CommRing {ℓ-zero}
BiInvIntAsCommRing =
  makeCommRing
    zero (suc zero) _+ℤ_ _·_ _-ℤ_
    isSetBiInvInt
    +ℤ-assoc +-zero +-invʳ +ℤ-comm
    ·-assoc ·-identityʳ
    (λ x y z → sym (·-distribˡ x y z))
    ·-comm

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2020 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types

open import LibraBFT.Abstract.Types

open import LibraBFT.Yasm.Base
open import LibraBFT.Yasm.AvailableEpochs using (AvailableEpochs) renaming (lookup'' to EC-lookup)
import LibraBFT.Yasm.AvailableEpochs as AE

-- This module provides some definitions and properties that facilitate
-- proofs of properties about a distributed system modeled by Yasm.System
-- paramaterized by some SystemParameters.

module LibraBFT.Yasm.Properties (parms : SystemParameters) where
 open import LibraBFT.Yasm.System parms
 open SystemParameters parms
 open EpochConfig

 -- A ValidPartForPK collects the assumptions about what a /part/ in the outputs of an honest verifier
 -- satisfies: (i) the epoch field is consistent with the existent epochs and (ii) the verifier is
 -- a member of the associated epoch config, and (iii) has the given PK in that epoch.
 record ValidPartForPK {e}(𝓔s : AvailableEpochs e)(part : Part)(pk : PK) : Set₁ where
   constructor mkValidPartForPK
   field
     vp-epoch           : part-epoch part < e
     vp-ec              : EpochConfig
     vp-ec-≡            : AE.lookup'' 𝓔s vp-epoch ≡ vp-ec
     vp-member          : Member vp-ec
     vp-key             : getPubKey vp-ec vp-member ≡ pk
 open ValidPartForPK public

 -- A valid part remains valid when new epochs are added
 ValidPartForPK-stable-epoch : ∀{e part pk}{𝓔s : AvailableEpochs e}(𝓔 : EpochConfigFor e)
                          → ValidPartForPK 𝓔s part pk
                          → ValidPartForPK (AE.append 𝓔 𝓔s) part pk
 ValidPartForPK-stable-epoch {pk = pk} {𝓔s} 𝓔 (mkValidPartForPK e ec refl emem vpk) = record
   { vp-epoch           = ≤-step e
   ; vp-ec              = ec
   ; vp-ec-≡            = AE.lookup''-≤-step-lemma 𝓔s 𝓔 e
   ; vp-member          = emem
   ; vp-key             = vpk
   }

 -- A valid part remains valid
 ValidPartForPK-stable : ∀{e e'}{st : SystemState e}{st' : SystemState e'}
                    → Step* st st' → ∀{part pk}
                    → ValidPartForPK (availEpochs st) part pk
                    → ValidPartForPK (availEpochs st') part pk
 ValidPartForPK-stable step-0 v = v
 ValidPartForPK-stable (step-s st (step-epoch 𝓔)) v
   = ValidPartForPK-stable-epoch 𝓔 (ValidPartForPK-stable st v)
 ValidPartForPK-stable (step-s st (step-peer _)) v
   = ValidPartForPK-stable st v

 -- We say that an implementation produces only valid parts iff all parts of every message in the
 -- output of a 'StepPeerState' are either: (i) a valid new part (i.e., the part is valid and has
 -- not been included in a previously sent message with the same signature), or (ii) the part been
 -- included in a previously sent message with the same signature.
 StepPeerState-AllValidParts : Set₁
 StepPeerState-AllValidParts = ∀{e s m part pk outs α}{𝓔s : AvailableEpochs e}{st : SystemState e}
   → (r : ReachableSystemState st)
   → Meta-Honest-PK pk
   → StepPeerState α 𝓔s (msgPool st) (Map-lookup α (peerStates st)) s outs
   → m ∈ outs → part ⊂Msg m → (ver : WithVerSig pk part)
                                 -- NOTE: this doesn't DIRECTLY imply that nobody else has sent a
                                 -- message with the same signature just that the author of the part
                                 -- hasn't.
   → (ValidPartForPK 𝓔s part pk × ¬ (MsgWithSig∈ pk (ver-signature ver) (msgPool st)))
   ⊎ MsgWithSig∈ pk (ver-signature ver) (msgPool st)

 -- A /part/ was introduced by a specific step when:
 IsValidNewPart : ∀{e e'}{pre : SystemState e}{post : SystemState e'} → Signature → PK → Step pre post → Set₁
 IsValidNewPart _ _ (step-epoch _) = Lift (ℓ+1 0ℓ) ⊥
 -- said step is a /step-peer/ and
 IsValidNewPart {pre = pre} sig pk (step-peer pstep)
    -- the part has never been seen before
    = ¬ (MsgWithSig∈ pk sig (msgPool pre))
    × Σ (MsgWithSig∈ pk sig (msgPool (StepPeer-post pstep)))
        (λ m → ValidPartForPK (availEpochs pre) (msgPart m) pk)

 -- When we can prove that the implementation provided by 'parms' at the
 -- top of this module satisfies 'StepPeerState-AllValidParts', we can
 -- prove a number of useful structural properties:

 -- TODO-2: Refactor into a file (LibraBFT.Yasm.Properties.Structural) later on
 -- if this grows too large.
 module Structural (sps-avp      : StepPeerState-AllValidParts) where

     -- We can unwind the state and highlight the step where a part was
     -- originally sent. This 'unwind' function combined with Any-Step-elim
     -- enables a powerful form of reasoning. The 'honestVoteEpoch' below
     -- exemplifies this well.
     unwind : ∀{e}{st : SystemState e}(tr : ReachableSystemState st)
            → ∀{p m σ pk} → Meta-Honest-PK pk
            → p ⊂Msg m → (σ , m) ∈ msgPool st → (ver : WithVerSig pk p)
            → Any-Step ((IsValidNewPart (ver-signature ver) pk)) tr
     unwind (step-s tr (step-epoch _))    hpk p⊂m m∈sm sig
       = step-there (unwind tr hpk p⊂m m∈sm sig)
     unwind (step-s tr (step-peer {pid = β} {outs = outs} {pre = pre} sp)) hpk p⊂m m∈sm sig
       with Any-++⁻ (List-map (β ,_) outs) {msgPool pre} m∈sm
     ...| inj₂ furtherBack = step-there (unwind tr hpk p⊂m furtherBack sig)
     ...| inj₁ thisStep
       with sp
     ...| step-cheat fm isCheat
       with thisStep
     ...| here refl
       with isCheat p⊂m sig
     ...| inj₁ abs    = ⊥-elim (hpk abs)
     ...| inj₂ sentb4
       with unwind tr {p = msgPart sentb4} hpk (msg⊆ sentb4) (msg∈pool sentb4) (msgSigned sentb4)
     ...| res rewrite msgSameSig sentb4 = step-there res
     unwind (step-s tr (step-peer {pid = β} {outs = outs} {pre = pre} sp)) hpk p⊂m m∈sm sig
        | inj₁ thisStep
        | step-honest x
       with Any-satisfied-∈ (Any-map⁻ thisStep)
     ...| (m , refl , m∈outs)
       with sps-avp tr hpk x m∈outs p⊂m sig
     ...| inj₂ sentb4 with unwind tr {p = msgPart sentb4} hpk (msg⊆ sentb4) (msg∈pool sentb4) (msgSigned sentb4)
     ...| res rewrite msgSameSig sentb4 = step-there res

     unwind (step-s tr (step-peer {pid = β} {outs = outs} {pre = pre} sp)) {p} hpk p⊂m m∈sm sig
        | inj₁ thisStep
        | step-honest x
        | (m , refl , m∈outs)
        | inj₁ (valid-part , notBefore) =
               step-here tr (notBefore , MsgWithSig∈-++ˡ (mkMsgWithSig∈ _ _ p⊂m β thisStep sig refl)
                                       , valid-part)

     -- Unwind is inconvenient to use by itself because we have to do
     -- induction on Any-Step-elim. The 'honestPartValid' property below
     -- provides a fairly general result conveniently: for every part
     -- verifiable with an honest PK, there is a msg with the same
     -- signature that is valid for some pid.

     honestPartValid : ∀ {e st} → ReachableSystemState {e} st → ∀ {pk nm v sender}
                     → Meta-Honest-PK pk
                     → v ⊂Msg nm → (sender , nm) ∈ msgPool st → (ver : WithVerSig pk v)
                     → Σ (MsgWithSig∈ pk (ver-signature ver) (msgPool st))
                         (λ msg → (ValidPartForPK (availEpochs st) (msgPart msg) pk))
     honestPartValid {e} {st} r {pk = pk} hpk v⊂m m∈pool ver
     -- We extract two pieces of important information from the place where the part 'v'
     -- was first sent: (a) there is a message with the same signature /in the current pool/
     -- and (b) its epoch is less than e.
        = Any-Step-elim (λ { {st = step-epoch _} ()
                           ; {st = step-peer ps} (_ , new , valid) tr
                             →  MsgWithSig∈-Step* tr new
                                , ValidPartForPK-stable tr
                                    (subst (λ P → ValidPartForPK _ P pk)
                                           (MsgWithSig∈-Step*-part tr new) valid)
                           })
                        (unwind r hpk v⊂m m∈pool ver)

     -- Unforgeability is also an important property stating that every part that is
     -- verified with an honest public key has either been sent by α or is a replay
     -- of another message sent before.
     ext-unforgeability'
       : ∀{e α m part pk}{st : SystemState e} → ReachableSystemState st
       -- If a message m has been sent by α, containing part
       → (α , m) ∈ msgPool st → part ⊂Msg m
       -- And the part can be verified with an honest public key,
       → (sig : WithVerSig pk part) → Meta-Honest-PK pk
       -- then either the part is a valid part by α (meaning that α can
       -- sign the part itself) or a message with the same signature has
       -- been sent previously.
       → ValidPartForPK (availEpochs st) part pk
       ⊎ MsgWithSig∈ pk (ver-signature sig) (msgPool st)
     ext-unforgeability' (step-s st (step-epoch 𝓔)) m∈sm p⊆m sig hpk
       = ⊎-map (ValidPartForPK-stable-epoch 𝓔) id (ext-unforgeability' st m∈sm p⊆m sig hpk)
     ext-unforgeability' {part = part} (step-s st (step-peer {pid = β} {outs = outs} {pre = pre} sp)) m∈sm p⊆m sig hpk
       with Any-++⁻ (List-map (β ,_) outs) {msgPool pre} m∈sm
     ...| inj₂ furtherBack = MsgWithSig∈-++ʳ <⊎$> (ext-unforgeability' st furtherBack p⊆m sig hpk)
     ...| inj₁ thisStep
       with sp
     ...| step-cheat fm isCheat
       with thisStep
     ...| here refl
       with isCheat p⊆m sig
     ...| inj₁ abs    = ⊥-elim (hpk abs)
     ...| inj₂ sentb4 = inj₂ (MsgWithSig∈-++ʳ sentb4)
     ext-unforgeability' {m = m} {part = part} (step-s st (step-peer {pid = β} {outs = outs} {pre = pre} sp)) m∈sm p⊆m sig hpk
        | inj₁ thisStep
        | step-honest x
       with Any-satisfied-∈ (Any-map⁻ thisStep)
     ...| (m , refl , m∈outs) = ⊎-map proj₁ MsgWithSig∈-++ʳ (sps-avp st hpk x m∈outs p⊆m sig)

     -- The ext-unforgeability' property can be collapsed in a single clause.

     -- TODO-2: so far, ext-unforgeability is used only to get a MsgWithSig∈ that is passed to
     -- msgWithSigSentByAuthor, which duplicates some of the reasoning in the proof of
     -- ext-unforgeability'; should these properties possibly be combined into one simpler proof?
     ext-unforgeability
       : ∀{e α₀ m part pk}{st : SystemState e} → ReachableSystemState st
       → (α₀ , m) ∈ msgPool st → part ⊂Msg m
       → (sig : WithVerSig pk part) → Meta-Honest-PK pk
       → MsgWithSig∈ pk (ver-signature sig) (msgPool st)
     ext-unforgeability {_} {α₀} {m} {st = st} rst m∈sm p⊂m sig hpk
       with ext-unforgeability' rst m∈sm p⊂m sig hpk
     ...| inj₁ p
        = mkMsgWithSig∈ _ _ p⊂m α₀ m∈sm sig refl
     ...| inj₂ sentb4 = sentb4

     ¬cheatForgeNew : ∀ {e pid pk vsig mst outs m}{st : SystemState e}
                    → (sp : StepPeer st pid mst outs)
                    → outs ≡ m ∷ []
                    → (ic : isCheat sp)
                    → Meta-Honest-PK pk
                    → MsgWithSig∈ pk vsig ((pid , m) ∷ msgPool st)
                    → MsgWithSig∈ pk vsig (msgPool st)
     ¬cheatForgeNew sc@(step-cheat fm isCheat) refl _ hpk mws
        with msg∈pool mws
     ...| there m∈pool = mkMsgWithSig∈ (msgWhole mws) (msgPart mws) (msg⊆ mws) (msgSender mws) m∈pool (msgSigned mws) (msgSameSig mws)
     ...| here m∈pool
        with isCheat (subst (msgPart mws ⊂Msg_) (cong proj₂ m∈pool) (msg⊆ mws)) (msgSigned mws)
     ...| inj₁ dis = ⊥-elim (hpk dis)
     ...| inj₂ mws' rewrite msgSameSig mws = mws'

     msgWithSigSentByAuthor : ∀ {e pk sig}{st : SystemState e}
                            → ReachableSystemState st
                            → Meta-Honest-PK pk
                            → MsgWithSig∈ pk sig (msgPool st)
                            → Σ (MsgWithSig∈ pk sig (msgPool st))
                                λ mws → ValidPartForPK (availEpochs st) (msgPart mws) pk
     msgWithSigSentByAuthor step-0 _ ()
     msgWithSigSentByAuthor (step-s {pre = pre} preach (step-epoch 𝓔)) hpk mws
       rewrite step-epoch-does-not-send pre 𝓔
          with msgWithSigSentByAuthor preach hpk mws
     ...| mws' , vpb =  mws' , ValidPartForPK-stable {st = pre} (step-s step-0 (step-epoch 𝓔)) vpb
     msgWithSigSentByAuthor {pk = pk} (step-s {pre = pre} preach (step-peer theStep@(step-cheat fm cheatCons))) hpk mws
        with (¬cheatForgeNew theStep refl unit hpk mws)
     ...| mws'
        with msgWithSigSentByAuthor preach hpk mws'
     ...| mws'' , vpb'' = MsgWithSig∈-++ʳ mws'' , vpb''
     msgWithSigSentByAuthor {e} (step-s {pre = pre} preach (step-peer {pid = pid} {outs = outs} (step-honest sps))) hpk mws
       with Any-++⁻ (List-map (pid ,_) outs) {msgPool pre} (msg∈pool mws)
     ...| inj₂ furtherBack
       with msgWithSigSentByAuthor preach hpk (MsgWithSig∈-transp mws furtherBack)
     ...| mws' , vpb' =  MsgWithSig∈-++ʳ mws' , vpb'

     msgWithSigSentByAuthor {e} (step-s {pre = pre} preach (step-peer {pid = pid} {outs = outs} (step-honest sps))) hpk mws
        | inj₁ thisStep
        with Any-satisfied-∈ (Any-map⁻ thisStep)
     ...| (m' , refl , m∈outs)
        with sps-avp preach hpk sps m∈outs (msg⊆ mws) (msgSigned mws)
     ...| inj₁ (vpbα₀ , _) = mws , vpbα₀
     ...| inj₂ mws'
        with msgWithSigSentByAuthor preach hpk mws'
     ...| mws'' , vpb'' rewrite sym (msgSameSig mws) = MsgWithSig∈-++ʳ mws'' , vpb''


text:
module Issue3080 where

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data Fin (m : Nat) : Set where
  fzero' : (n : Nat) (p : m ≡ suc n) → Fin m
  fsuc'  : (n : Nat) (p : m ≡ suc n) (i : Fin n) → Fin m

lift : (m : Nat) (i : Fin m) → Fin (suc m)
lift m (fzero' n p)  = {!p!}
lift m (fsuc' n p i) = {!p!} -- Split on p here

module PatternSynonyms where

  pattern fzero n      = fzero' n refl
  pattern fsuc  n i    = fsuc'  n refl i

-- Splitting produces
--
--   lift .(suc n) (.Issue3080.PatternSynonyms.fsuc n i) = ?
--
-- which fails to parse.


text:
open import Relation.Binary.Core

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

open import Data.List
open import Data.Sum
open import InsertSort.Impl1 _≤_ tot≤
open import List.Sorted _≤_

lemma-insert-sorted : {xs : List A}(x : A) → Sorted xs → Sorted (insert x xs)
lemma-insert-sorted {xs = .[]} x nils = singls x
lemma-insert-sorted {xs = .([ y ])} x  (singls y)
    with tot≤ x y
... | inj₁ x≤y  = conss x≤y (singls y)
... | inj₂ y≤x  = conss y≤x (singls x)
lemma-insert-sorted x (conss {y} {z} {ys} y≤z szys)
    with tot≤ x y
... | inj₁ x≤y = conss x≤y (conss y≤z szys)
... | inj₂ y≤x
    with tot≤ x z | lemma-insert-sorted x szys
... | inj₁ x≤z | _ = conss y≤x (conss x≤z szys)
... | inj₂ z≤x | h = conss y≤z h

theorem-insertSort-sorted : (xs : List A) → Sorted (insertSort xs)
theorem-insertSort-sorted [] = nils
theorem-insertSort-sorted (x ∷ xs) = lemma-insert-sorted x (theorem-insertSort-sorted xs)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers represented in binary natively in Agda.
------------------------------------------------------------------------

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

module Data.Nat.Binary where

open import Data.Nat.Binary.Base public
open import Data.Nat.Binary.Properties public using (_≟_)


text:
open import Common.Prelude
open import Common.Reflection

module TermSplicingLooping where

mutual
  f : Set -> Set
  f = unquote (give (def (quote f) []))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module Categories.Category.Instance.Properties.Setoids.Complete where

open import Level
open import Data.Product using (Σ; proj₁; proj₂; _,_; Σ-syntax; _×_; -,_)
open import Function.Equality using (Π)
open import Relation.Binary using (Setoid; Rel)

open import Categories.Category using (Category; _[_,_])
open import Categories.Functor
open import Categories.Category.Instance.Setoids
open import Categories.Category.Complete

import Categories.Category.Construction.Cones as Co

open Π using (_⟨$⟩_)

Setoids-Complete : (o ℓ e c ℓ′ : Level) → Complete o ℓ e (Setoids (c ⊔ ℓ ⊔ o ⊔ ℓ′) (o ⊔ ℓ′))
Setoids-Complete o ℓ e c ℓ′ {J} F =
  record
  { terminal = record
    { ⊤        = record
      { N     = record
        { Carrier       = Σ (∀ j → F₀.Carrier j)
                            (λ S → ∀ {X Y} (f : J [ X , Y ]) → [ F₀ Y ] F₁ f ⟨$⟩ S X ≈ S Y)
        ; _≈_           = λ { (S₁ , _) (S₂ , _) → ∀ j → [ F₀ j ] S₁ j ≈ S₂ j }
        ; isEquivalence = record
          { refl  = λ j → F₀.refl j
          ; sym   = λ a≈b j → F₀.sym j (a≈b j)
          ; trans = λ a≈b b≈c j → F₀.trans j (a≈b j) (b≈c j)
          }
        }
      ;  apex = record
        { ψ = λ j → record
          { _⟨$⟩_ = λ { (S , _) → S j }
          ; cong  = λ eq → eq j
          }
        ; commute = λ { {X} {Y} X⇒Y {_ , eq} {y} f≈g → F₀.trans Y (eq X⇒Y) (f≈g Y) }
        }
      }
    ; ⊤-is-terminal = record
      { !        = λ {K} →
        let module K = Cone K
        in record
        { arr     = record
          { _⟨$⟩_ = λ x → (λ j → K.ψ j ⟨$⟩ x) , λ f → K.commute f (Setoid.refl K.N)
          ; cong  = λ a≈b j → Π.cong (K.ψ j) a≈b
          }
        ; commute = λ x≈y → Π.cong (K.ψ _) x≈y
        }
      ; !-unique = λ {K} f x≈y j →
        let module K = Cone K
        in F₀.sym j (Cone⇒.commute f (Setoid.sym K.N x≈y))
      }
    }
  }
  where open Functor F
        open Co F
        module J    = Category J
        module F₀ j = Setoid (F₀ j)
        [_]_≈_ = Setoid._≈_

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories