text:
open import Nat
open import Prelude
open import core
open import contexts
open import lemmas-consistency
open import lemmas-ground

open import progress-checks

open import canonical-boxed-forms
open import canonical-value-forms
open import canonical-indeterminate-forms

open import ground-decidable
open import htype-decidable

module progress where
  -- this is a little bit of syntactic sugar to avoid many layer nested Inl
  -- and Inrs that you would get from the more literal transcription of the
  -- consequent of progress
  data ok : (d : ihexp) (Δ : hctx) → Set where
    S  : ∀{d Δ} → Σ[ d' ∈ ihexp ] (d ↦ d') → ok d Δ
    I  : ∀{d Δ} → d indet → ok d Δ
    BV : ∀{d Δ} → d boxedval → ok d Δ

  progress : {Δ : hctx} {d : ihexp} {τ : htyp} →
             Δ , ∅ ⊢ d :: τ →
             ok d Δ
    -- constants
  progress TAConst = BV (BVVal VConst)

    -- variables
  progress (TAVar x₁) = abort (somenotnone (! x₁))

    -- lambdas
  progress (TALam _ wt) = BV (BVVal VLam)

    -- applications
  progress (TAAp wt1 wt2)
    with progress wt1 | progress wt2
    -- if the left steps, the whole thing steps
  progress (TAAp wt1 wt2) | S (_ , Step x y z) | _ = S (_ , Step (FHAp1 x) y (FHAp1 z))
    -- if the left is indeterminate, step the right
  progress (TAAp wt1 wt2) | I i | S (_ , Step x y z) = S (_ , Step (FHAp2 x) y (FHAp2  z))
    -- if they're both indeterminate, step when the cast steps and indet otherwise
  progress (TAAp wt1 wt2) | I x | I x₁
    with canonical-indeterminate-forms-arr wt1 x
  progress (TAAp wt1 wt2) | I x | I y | CIFACast (_ , _ , _ , _ , _ , refl , _ , _ ) = S (_ , Step FHOuter ITApCast FHOuter)
  progress (TAAp wt1 wt2) | I x | I y | CIFAEHole (_ , _ , _ , refl , _)             = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  progress (TAAp wt1 wt2) | I x | I y | CIFANEHole (_ , _ , _ , _ , _ , refl , _)    = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  progress (TAAp wt1 wt2) | I x | I y | CIFAAp (_ , _ , _ , _ , _ , refl , _)        = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  progress (TAAp wt1 wt2) | I x | I y | CIFACastHole (_ , refl , refl , refl , _ )   = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
  progress (TAAp wt1 wt2) | I x | I y | CIFAFailedCast (_ , _ , refl , _ )           = I (IAp (λ _ _ _ _ _ ()) x (FIndet y))
    -- similar if the left is indetermiante but the right is a boxed val
  progress (TAAp wt1 wt2) | I x | BV x₁
    with canonical-indeterminate-forms-arr wt1 x
  progress (TAAp wt1 wt2) | I x | BV y | CIFACast (_ , _ , _ , _ , _ , refl , _ , _ ) = S (_ , Step FHOuter ITApCast FHOuter)
  progress (TAAp wt1 wt2) | I x | BV y | CIFAEHole (_ , _ , _ , refl , _)             = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  progress (TAAp wt1 wt2) | I x | BV y | CIFANEHole (_ , _ , _ , _ , _ , refl , _)    = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  progress (TAAp wt1 wt2) | I x | BV y | CIFAAp (_ , _ , _ , _ , _ , refl , _)        = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  progress (TAAp wt1 wt2) | I x | BV y | CIFACastHole (_ , refl , refl , refl , _ )   = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
  progress (TAAp wt1 wt2) | I x | BV y | CIFAFailedCast (_ , _ , refl , _ )           = I (IAp (λ _ _ _ _ _ ()) x (FBoxedVal y))
    -- if the left is a boxed value, inspect the right
  progress (TAAp wt1 wt2) | BV v | S (_ , Step x y z) = S (_ , Step (FHAp2  x) y (FHAp2  z))
  progress (TAAp wt1 wt2) | BV v | I i
    with canonical-boxed-forms-arr wt1 v
  ... | CBFLam (_ , _ , refl , _)             = S (_ , Step FHOuter ITLam FHOuter)
  ... | CBFCastArr (_ , _ , _ , refl , _ , _) = S (_ , Step FHOuter ITApCast FHOuter)
  progress (TAAp wt1 wt2) | BV v | BV v₂
    with canonical-boxed-forms-arr wt1 v
  ... | CBFLam (_ , _ , refl , _)             = S (_ , Step FHOuter ITLam FHOuter)
  ... | CBFCastArr (_ , _ , _ , refl , _ , _) = S (_ , Step FHOuter ITApCast FHOuter)

    -- empty holes are indeterminate
  progress (TAEHole _ _ ) = I IEHole

    -- nonempty holes step if the innards step, indet otherwise
  progress (TANEHole xin wt x₁)
    with progress wt
  ... | S (_ , Step x y z) = S (_ , Step (FHNEHole x) y (FHNEHole z))
  ... | I  x = I (INEHole (FIndet x))
  ... | BV x = I (INEHole (FBoxedVal x))

    -- casts
  progress (TACast wt con)
    with progress wt
    -- step if the innards step
  progress (TACast wt con) | S (_ , Step x y z) = S (_ , Step (FHCast x) y (FHCast z))
    -- if indet, inspect how the types in the cast are realted by consistency:
    -- if they're the same, step by ID
  progress (TACast wt TCRefl)  | I x = S (_ , Step FHOuter ITCastID FHOuter)
    -- if first type is hole
  progress (TACast {τ1 = τ1} wt TCHole1) | I x
    with τ1
  progress (TACast wt TCHole1) | I x | b = I (ICastGroundHole GBase x)
  progress (TACast wt TCHole1) | I x | ⦇-⦈ = S (_ , Step FHOuter ITCastID FHOuter)
  progress (TACast wt TCHole1) | I x | τ11 ==> τ12
    with ground-decidable (τ11 ==> τ12)
  progress (TACast wt TCHole1) | I x₁ | .⦇-⦈ ==> .⦇-⦈ | Inl GHole = I (ICastGroundHole GHole x₁)
  progress (TACast wt TCHole1) | I x₁ | τ11 ==> τ12 | Inr x =  S (_ , Step FHOuter (ITGround (MGArr (ground-arr-not-hole x))) FHOuter)
    -- if second type is hole
  progress (TACast wt (TCHole2 {b})) | I x
    with canonical-indeterminate-forms-hole wt x
  progress (TACast wt (TCHole2 {b})) | I x | CIFHEHole (_ , _ , _ , refl , f)           = I (ICastHoleGround (λ _ _ ()) x GBase)
  progress (TACast wt (TCHole2 {b})) | I x | CIFHNEHole (_ , _ , _ , _ , _ , refl , _ ) = I (ICastHoleGround (λ _ _ ()) x GBase)
  progress (TACast wt (TCHole2 {b})) | I x | CIFHAp (_ , _ , _ , refl , _ )             = I (ICastHoleGround (λ _ _ ()) x GBase)
  progress (TACast wt (TCHole2 {b})) | I x | CIFHCast (_ , τ , refl , _)
    with htype-dec τ b
  progress (TACast wt (TCHole2 {b})) | I x₁ | CIFHCast (_ , .b , refl , _ , grn , _) | Inl refl = S (_ , Step FHOuter (ITCastSucceed grn ) FHOuter)
  progress (TACast wt (TCHole2 {b})) | I x₁ | CIFHCast (_ , _ , refl , π2 , grn , _)  | Inr x =    S (_ , Step FHOuter (ITCastFail grn GBase x) FHOuter)
  progress (TACast wt (TCHole2 {⦇-⦈}))| I x = S (_ , Step FHOuter ITCastID FHOuter)
  progress (TACast wt (TCHole2 {τ11 ==> τ12})) | I x
    with ground-decidable (τ11 ==> τ12)
  progress (TACast wt (TCHole2 {.⦇-⦈ ==> .⦇-⦈})) | I x₁ | Inl GHole
    with canonical-indeterminate-forms-hole wt x₁
  progress (TACast wt (TCHole2 {.⦇-⦈ ==> .⦇-⦈})) | I x | Inl GHole | CIFHEHole (_ , _ , _ , refl , _)          = I (ICastHoleGround (λ _ _ ()) x GHole)
  progress (TACast wt (TCHole2 {.⦇-⦈ ==> .⦇-⦈})) | I x | Inl GHole | CIFHNEHole (_ , _ , _ , _ , _ , refl , _) = I (ICastHoleGround (λ _ _ ()) x GHole)
  progress (TACast wt (TCHole2 {.⦇-⦈ ==> .⦇-⦈})) | I x | Inl GHole | CIFHAp (_ , _ , _ , refl , _ )            = I (ICastHoleGround (λ _ _ ()) x GHole)
  progress (TACast wt (TCHole2 {.⦇-⦈ ==> .⦇-⦈})) | I x | Inl GHole | CIFHCast (_ , ._ , refl , _ , GBase , _)  = S (_ , Step FHOuter (ITCastFail GBase GHole (λ ())) FHOuter )
  progress (TACast wt (TCHole2 {.⦇-⦈ ==> .⦇-⦈})) | I x | Inl GHole | CIFHCast (_ , ._ , refl , _ , GHole , _)  = S (_ , Step FHOuter (ITCastSucceed GHole) FHOuter)
  progress (TACast wt (TCHole2 {τ11 ==> τ12})) | I x₁ | Inr x = S (_ , Step FHOuter (ITExpand (MGArr (ground-arr-not-hole x))) FHOuter)
    -- if both are arrows
  progress (TACast wt (TCArr {τ1} {τ2} {τ1'} {τ2'} c1 c2)) | I x
    with htype-dec (τ1 ==> τ2)  (τ1' ==> τ2')
  progress (TACast wt (TCArr c1 c2)) | I x₁ | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  progress (TACast wt (TCArr c1 c2)) | I x₁ | Inr x = I (ICastArr x x₁)
    -- boxed value cases, inspect how the casts are realted by consistency
    -- step by ID if the casts are the same
  progress (TACast wt TCRefl)  | BV x = S (_ , Step FHOuter ITCastID FHOuter)
    -- if left is hole
  progress (TACast wt (TCHole1 {τ = τ})) | BV x
    with ground-decidable τ
  progress (TACast wt TCHole1) | BV x₁ | Inl g = BV (BVHoleCast g x₁)
  progress (TACast wt (TCHole1 {b})) | BV x₁ | Inr x = abort (x GBase)
  progress (TACast wt (TCHole1 {⦇-⦈})) | BV x₁ | Inr x = S (_ , Step FHOuter ITCastID FHOuter)
  progress (TACast wt (TCHole1 {τ1 ==> τ2})) | BV x₁ | Inr x
    with (htype-dec  (τ1 ==> τ2) (⦇-⦈ ==> ⦇-⦈))
  progress (TACast wt (TCHole1 {.⦇-⦈ ==> .⦇-⦈})) | BV x₂ | Inr x₁ | Inl refl = BV (BVHoleCast GHole x₂)
  progress (TACast wt (TCHole1 {τ1 ==> τ2})) | BV x₂ | Inr x₁ | Inr x = S (_ , Step FHOuter (ITGround (MGArr x)) FHOuter)
    -- if right is hole
  progress {τ = τ} (TACast wt TCHole2) | BV x
    with canonical-boxed-forms-hole wt x
  progress {τ = τ} (TACast wt TCHole2) | BV x | d' , τ' , refl , gnd , wt'
    with htype-dec τ τ'
  progress (TACast wt TCHole2) | BV x₁ | d' , τ , refl , gnd , wt' | Inl refl = S (_  , Step FHOuter (ITCastSucceed gnd) FHOuter)
  progress {τ = τ} (TACast wt TCHole2) | BV x₁ | _ , _ , refl , _ , _ | Inr _
    with ground-decidable τ
  progress (TACast wt TCHole2) | BV x₂ | _ , _ , refl , gnd , _ | Inr x₁ | Inl x = S(_ , Step FHOuter (ITCastFail gnd x (flip x₁)) FHOuter)
  progress (TACast wt TCHole2) | BV x₂ | _ , _ , refl , _ , _ | Inr x₁ | Inr x
    with notground x
  progress (TACast wt TCHole2) | BV x₃ | _ , _ , refl , _ , _ | Inr _ | Inr _ | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  progress (TACast wt TCHole2) | BV x₃ | _ , _ , refl , _ , _ | Inr _ | Inr x | Inr (_ , _ , refl) = S(_ , Step FHOuter (ITExpand (MGArr (ground-arr-not-hole x))) FHOuter )
    -- if both arrows
  progress (TACast wt (TCArr {τ1} {τ2} {τ1'} {τ2'} c1 c2)) | BV x
    with htype-dec (τ1 ==> τ2) (τ1' ==> τ2')
  progress (TACast wt (TCArr c1 c2)) | BV x₁ | Inl refl = S (_ , Step FHOuter ITCastID FHOuter)
  progress (TACast wt (TCArr c1 c2)) | BV x₁ | Inr x = BV (BVArrCast x x₁)

   -- failed casts
  progress (TAFailedCast wt y z w)
    with progress wt
  progress (TAFailedCast wt y z w) | S (d' , Step x a q) = S (_ , Step (FHFailedCast x) a (FHFailedCast q))
  progress (TAFailedCast wt y z w) | I x = I (IFailedCast (FIndet x) y z w)
  progress (TAFailedCast wt y z w) | BV x = I (IFailedCast (FBoxedVal x) y z w)

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
module Main where

import Data.Any
import Data.Boolean
import Data.Either
-- import Data.List
-- import Data.ListNonEmpty
-- import Data.ListSized
import Data.Option
-- import Data.Proofs
import Data.Tuple
import Lang.Instance
import Lang.Irrelevance
import Lang.Size
import Logic
-- import Logic.Classical
-- import Logic.Computability
-- import Logic.Names
-- import Logic.Predicate
-- import Logic.Predicate.Theorems
-- import Logic.Propositional
-- import Logic.Propositional.Theorems
import Lvl
import Numeral.Integer
-- import Numeral.Integer.Proofs
import Numeral.Natural
import Relator.Equals
-- import Relator.Equals.Proofs
import Syntax.Function
-- import Syntax.Number
import Type
import Type.Cubical
import Type.Cubical.Path
import Type.Cubical.Path.Proofs
import Type.Dependent
import Type.Properties.Empty
-- import Type.Properties.Empty.Proofs
import Type.Quotient
-- import Type.Singleton
-- import Type.Singleton.Proofs
-- import Type.Size
-- import Type.Size.Proofs
import Type.Properties.Singleton
-- import Type.Properties.Singleton.Proofs

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --without-K --safe #-}
module Util.HoTT.Homotopy where

open import Relation.Binary using (IsEquivalence)

open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using (cong-app)

module _ {α β} {A : Set α} {B : A → Set β} where

  _~_ : (f g : ∀ a → B a) → Set (α ⊔ℓ β)
  f ~ g = ∀ a → f a ≡ g a

  ~-refl : ∀ {f} → f ~ f
  ~-refl a = refl

  ~-sym : ∀ {f g} → f ~ g → g ~ f
  ~-sym f~g a = sym (f~g a)

  ~-trans : ∀ {f g h} → f ~ g → g ~ h → f ~ h
  ~-trans f~g g~h a = trans (f~g a) (g~h a)

  ~-IsEquivalence : IsEquivalence _~_
  ~-IsEquivalence = record { refl = ~-refl ; sym = ~-sym ; trans = ~-trans }

  ≡→~ : ∀ {f g} → f ≡ g → f ~ g
  ≡→~ = cong-app

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 --cubical --no-import-sorts  #-}

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)-- ¬ᵗ_
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Function.Base using (_∋_; _$_; it; typeOf)
open import Cubical.Foundations.Logic renaming
  ( inl to inlᵖ
  ; inr to inrᵖ
  ; _⇒_ to infixr 0 _⇒_                  -- shifting by -6
  ; _⇔_ to infixr -2 _⇔_                 --
  ; ∃[]-syntax  to infix -4 ∃[]-syntax   --
  ; ∃[∶]-syntax to infix -4 ∃[∶]-syntax  --
  ; ∀[∶]-syntax to infix -4 ∀[∶]-syntax  --
  ; ∀[]-syntax  to infix -4 ∀[]-syntax   --
  )
-- open import Cubical.Data.Unit.Base using (Unit)
open import Cubical.HITs.PropositionalTruncation.Base -- ∣_∣

open import Utils
open import MoreLogic.Reasoning
open import MoreLogic.Definitions renaming
  ( _ᵗ⇒_ to infixr 0 _ᵗ⇒_
  ; ∀ᵖ[∶]-syntax  to infix -4 ∀ᵖ[∶]-syntax
  ; ∀ᵖ〚∶〛-syntax  to infix -4 ∀ᵖ〚∶〛-syntax
  ; ∀ᵖ!〚∶〛-syntax to infix -4 ∀ᵖ!〚∶〛-syntax
  ; ∀〚∶〛-syntax   to infix -4 ∀〚∶〛-syntax
  ; Σᵖ[]-syntax   to infix -4 Σᵖ[]-syntax
  ; Σᵖ[∶]-syntax  to infix -4 Σᵖ[∶]-syntax
  ) hiding (≡ˢ-syntax)
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Consequences
open import MorePropAlgebra.Structures
open import MorePropAlgebra.Bundles

module MorePropAlgebra.Properties.PartiallyOrderedField {ℓ ℓ'} (assumptions : PartiallyOrderedField {ℓ} {ℓ'})
  (let _≡ˢ_ = λ(x y : PartiallyOrderedField.Carrier assumptions) → MoreLogic.Definitions.≡ˢ-syntax x y {PartiallyOrderedField.is-set assumptions}
       infixl 4 _≡ˢ_
  ) where

import MorePropAlgebra.Properties.AlmostPartiallyOrderedField
module AlmostPartiallyOrderedField'Properties  = MorePropAlgebra.Properties.AlmostPartiallyOrderedField   record { PartiallyOrderedField assumptions }
module AlmostPartiallyOrderedField'            =                            AlmostPartiallyOrderedField   record { PartiallyOrderedField assumptions }
-- (      AlmostPartiallyOrderedField')           =                            AlmostPartiallyOrderedField ∋ record { PartiallyOrderedField assumptions }

-- open PartiallyOrderedField assumptions renaming (Carrier to F; _-_ to _-_)

import MorePropAlgebra.Booij2020
open MorePropAlgebra.Booij2020.Chapter4 (record { PartiallyOrderedField assumptions })
open +-<-ext+·-preserves-<⇒ (PartiallyOrderedField.+-<-ext assumptions) (PartiallyOrderedField.·-preserves-< assumptions)
-- open AlmostPartiallyOrderedField'
open MorePropAlgebra.Properties.AlmostPartiallyOrderedField (record { PartiallyOrderedField assumptions })
open AlmostPartiallyOrderedField' using (_#_; _≤_)
open PartiallyOrderedField assumptions renaming (Carrier to F; _-_ to _-_) hiding (_#_; _≤_)

abstract
  #-tight : ∀ a b → [ ¬(a # b) ] → a ≡ b; _ : [ isTightˢ''' _#_ is-set ]; _ = #-tight
  #-tight = isTightˢ'''⇔isAntisymˢ _<_ is-set <-asym .snd ≤-antisym

  +-#-ext : ∀ w x y z → [ (w + x) # (y + z) ] → [ (w # y) ⊔ (x # z) ]; _ : [ is-+-#-Extensional _+_ _#_ ]; _ = +-#-ext
  -- Consider the case w + x < y + z, so that we can use (†) to obtain w < y ∨ x < z,
  --   which gives w # y ∨ x # z in either case.
  +-#-ext w x y z (inl w+x<y+z) = case +-<-ext _ _ _ _ w+x<y+z as (w < y) ⊔ (x < z) ⇒ ((w # y) ⊔ (x # z)) of λ
    { (inl w<y) → inlᵖ (inl w<y)
    ; (inr x<z) → inrᵖ (inl x<z) }
  -- The case w + x > y + z is similar.
  +-#-ext w x y z (inr y+z<w+x) = case +-<-ext _ _ _ _ y+z<w+x as (y < w) ⊔ (z < x) ⇒ ((w # y) ⊔ (x # z)) of λ
    { (inl y<w) → inlᵖ (inr y<w)
    ; (inr z<x) → inrᵖ (inr z<x) }

  ¬≤⇒≢ : ∀ x y → [ ¬(x ≤ y) ] → [ ¬(x ≡ˢ y) ]
  ¬≤⇒≢ x y ¬x≤y x≡y = ¬x≤y (subst (λ p → [ x ≤ p ]) x≡y (≤-refl x))

  ≢⇒¬¬# : ∀ x y → [ ¬(x ≡ˢ y) ] → [ ¬ ¬(x # y) ]
  ≢⇒¬¬# x y x≢y = contraposition (¬ (x # y)) (x ≡ˢ y) (#-tight x y) x≢y

  -- x ≤ y → x # y → x < y
  -- x ≤ y ≡ ¬(y ≤ x)
  -- ¬(x # y) → x ≡ y

  ¬≤⇒¬¬# : ∀ x y → [ (¬(x ≤ y)) ⇒ ¬ ¬ (x # y) ]
  ¬≤⇒¬¬# x y ¬x≤y = ≢⇒¬¬# x y $ ¬≤⇒≢ x y ¬x≤y

  ¬≤≡¬¬< : ∀ x y → ¬(x ≤ y) ≡ ¬ ¬ (y < x)
  ¬≤≡¬¬< x y = refl

  min-≤' : ∀ x y → [ (min x y ≤ x) ⊓ (min x y ≤ y) ]
  min-≤' x y = is-min x y (min x y) .fst (≤-refl (min x y))

  ¬¬<-trans : ∀ x y z → [ ¬ ¬ (x < y) ] → [ ¬ ¬ (y < z) ] → [ ¬ ¬ (x < z) ]
  ¬¬<-trans x y z ¬¬x<y ¬¬y<z = ( contraposition (¬ (x < z)) (¬ ((x < y) ⊓ (y < z)))
                                $ contraposition ((x < y) ⊓ (y < z)) (x < z)
                                $ uncurryₚ (x < y) (y < z) (x < z) (<-trans x y z)
                                ) (⊓¬¬⇒¬¬⊓ (x < y) (y < z) ¬¬x<y ¬¬y<z)

  ¬¬<-irrefl : ∀ x → [ ¬ ¬ ¬(x < x) ]
  ¬¬<-irrefl x = ¬¬-intro (¬(x < x)) (<-irrefl x)

  -- lem : ∀ (x y z : F) → {!   !}
  -- lem x y z = let f : [ x < y ] → [ (x < z) ⊔ (z < y) ]
  --                 f p = <-cotrans x y p z -- contraposition ((z ≤ x) ⊓ (y ≤ z)) (y ≤ x) $
  --                 _ = {!    !}
  --             in {! contraposition (x < y) ((x < z) ⊔ (z < y)) f ∘ deMorgan₂-back (x < z) (z < y)  !}

  -- foo : ∀(x y z w : F) → [ w < min (x · z) (y · z) ] → [ w < min x y · z ]
  -- foo x y z w = {! <-cotrans w (min x y) ? x   !}

  -- foo : ∀(x y z w : F) → [ w < min (x · z) (y · z) ] → [ w < min x y · z ]

  min-<-⊔ : ∀ x y z → [ min x y < z ] → [ (x < z) ⊔ (y < z) ]
  min-<-⊔ x y z mxy<z = case <-cotrans (min x y) z mxy<z x as (min x y < x) ⊔ (x < z) ⇒ (x < z) ⊔ (y < z) of λ
    { (inl p) → case <-cotrans (min x y) z mxy<z y as (min x y < y) ⊔ (y < z) ⇒ (x < z) ⊔ (y < z) of λ
      { (inl q) → -- We know that
                  --   x ≤ min(x, y) ⇔ x ≤ x ∧ x ≤ y,
                  --   y ≤ min(x, y) ⇔ y ≤ x ∧ y ≤ y.
                  -- By the fact that min(x, y) < x and min(x, y) < y, the left hand sides of these claims are false,
                  -- and hence we have ¬(x ≤ y) and ¬(y ≤ x), which together contradict that < is transitive and
                  -- irreflexive.
                  let (mxy≤x , mxy≤y) = is-min x y (min x y) .fst (<-irrefl (min x y))
                      r = contraposition ((x ≤ x) ⊓ (x ≤ y)) (¬ (min x y < x)) (is-min x y x .snd) (¬¬-intro (min x y < x) p)
                      ¬x≤y = implication (x ≤ x) (x ≤ y) r (≤-refl x)
                      s = contraposition ((y ≤ x) ⊓ (y ≤ y)) (¬ (min x y < y)) (is-min x y y .snd) (¬¬-intro (min x y < y) q)
                      ¬y≤x = ¬-⊓-distrib (y ≤ x) (y ≤ y) s .snd (≤-refl y)
                  in  ⊥-elim {A = λ _ → [ (x < z) ⊔ (y < z) ]} $ ¬¬<-irrefl x (¬¬<-trans x y x ¬y≤x ¬x≤y)
      ; (inr q) → inrᵖ q
      }
    ; (inr p) → inlᵖ p
    }

  -- is this provable?
  -- min-≤-⊔ : ∀ x y z → [ min x y ≤ z ] → [ (x ≤ z) ⊔ (y ≤ z) ]
  -- min-≤-⊔ x y z mxy≤z = {!   !}

  -- lem : ∀ w x y z → [ w ≤ (x + z) ] → [ w ≤ (y + z) ] → [ w ≤ (min x y + z) ]
  -- lem w x y z w≤x+z w≤y+z mxy+z<w = {! +-<-ext (min x y) z 0f w  !}

-- Properties.PartiallyOrderedField assumptions
--   opens PartiallyOrderedField assumptions
--     opens IsPartiallyOrderedField is-PartiallyOrderedField public
--       opens IsAlmostPartiallyOrderedField is-AlmostPartiallyOrderedField public
--         contains definition of _#_
--           becomes `_#_`
--   opens MorePropAlgebra.Properties.AlmostPartiallyOrderedField assumptions
--     opens AlmostPartiallyOrderedField assumptions
--       opens IsAlmostPartiallyOrderedField is-AlmostPartiallyOrderedField public
--         contains definition of _#_
--           becomes `AlmostPartiallyOrderedField'._#_`

-- all these become `_#_`
--   _#_
--   PartiallyOrderedField._#_ assumptions
--   IsPartiallyOrderedField._#_ (PartiallyOrderedField.is-PartiallyOrderedField assumptions)
--   IsAlmostPartiallyOrderedField._#_ (IsPartiallyOrderedField.is-AlmostPartiallyOrderedField (PartiallyOrderedField.is-PartiallyOrderedField assumptions))
-- but
--   PartiallyOrderedField._#_ (record { PartiallyOrderedField assumptions })
-- becomes
--   PartiallyOrderedField._#_ record { Carrier = F ; 0f = 0f ; 1f = 1f ; _+_ = _+_ ; -_ = -_ ; _·_ = _·_ ; min = min ; max = max ; _<_ = _<_ ; is-PartiallyOrderedField = is-PartiallyOrderedField }
-- when we define
--   foo = PartiallyOrderedField ∋ (record { PartiallyOrderedField assumptions })
-- then
--   PartiallyOrderedField._#_ foo
-- becomes
--   (foo PartiallyOrderedField.# x)

-- foo = PartiallyOrderedField ∋ (record { PartiallyOrderedField assumptions })
--
-- test : ∀ x y → [ (PartiallyOrderedField._#_ foo) x y ]
-- test = {! ·-inv''  !}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


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

module Math.NumberTheory.Summation.Nat.Properties where

-- agda-stdlib
open import Algebra
import Algebra.Operations.CommutativeMonoid as CommutativeMonoidOperations
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Solver
open import Relation.Binary.PropositionalEquality
open import Function.Base

-- agda-misc
open import Math.NumberTheory.Summation.Generic
open import Math.NumberTheory.Summation.Generic.Properties
import Math.NumberTheory.Summation.Nat.Properties.Lemma as Lemma

-- DO NOT change this line
open MonoidSummation (Semiring.+-monoid *-+-semiring)
open CommutativeMonoidOperations (Semiring.+-commutativeMonoid *-+-semiring)

-- TODO? rename _≈_ to _≡_ this is tedious
open SemiringSummationProperties *-+-semiring public
  renaming
  ( Σ<-const to Σ<-const-×
  ; Σ≤-const to Σ≤-const-×
  ; Σ<range-const to Σ<range-const-×
  ; Σ≤range-const to Σ≤range-const-×
  )

-- TODO move somewhere
private
  m×n≡m*n : ∀ m n → m × n ≡ m * n
  m×n≡m*n zero    n = refl
  m×n≡m*n (suc m) n = cong (n +_) $ m×n≡m*n m n

Σ<-const : ∀ m n → Σ< m (λ _ → n) ≡ m * n
Σ<-const m n = begin-equality
  Σ< m (λ _ → n) ≡⟨ Σ<-const-× m n ⟩
  m × n          ≡⟨ m×n≡m*n m n ⟩
  m * n          ∎
  where open ≤-Reasoning

Σ≤-const : ∀ m n → Σ≤ m (λ _ → n) ≡ suc m * n
Σ≤-const m n = Σ<-const (suc m) n

Σ<range-const : ∀ m n x → Σ<range m n (const x) ≡ (n ∸ m) * x
Σ<range-const m n x = trans (Σ<range-const-× m n x) (m×n≡m*n (n ∸ m) x)

Σ≤range-const : ∀ m n x → Σ≤range m n (const x) ≡ (suc n ∸ m) * x
Σ≤range-const m n x = Σ<range-const m (suc n) x

2*Σ≤[n,id]≡n*[1+n] : ∀ n → 2 * Σ≤ n id ≡ n * (suc n)
2*Σ≤[n,id]≡n*[1+n] zero    = refl
2*Σ≤[n,id]≡n*[1+n] (suc n) = begin-equality
  2 * Σ≤ (suc n) id       ≡⟨⟩
  2 * (Σ≤ n id + suc n)   ≡⟨ *-distribˡ-+ 2 (Σ≤ n id) (suc n) ⟩
  2 * Σ≤ n id + 2 * suc n ≡⟨ cong (_+ 2 * suc n) $ 2*Σ≤[n,id]≡n*[1+n] n ⟩
  n * suc n + 2 * suc n   ≡⟨ sym $ *-distribʳ-+ (suc n) n 2 ⟩
  (n + 2) * suc n         ≡⟨ *-comm (n + 2) (suc n) ⟩
  suc n * (n + 2)         ≡⟨ cong (suc n *_) $ +-comm n 2 ⟩
  suc n * suc (suc n)     ∎
  where open ≤-Reasoning

6*Σ≤[n,^2]≡n*[1+n]*[1+2*n] : ∀ n → 6 * Σ≤ n (_^ 2) ≡ n * (1 + n) * (1 + 2 * n)
6*Σ≤[n,^2]≡n*[1+n]*[1+2*n] 0       = refl
6*Σ≤[n,^2]≡n*[1+n]*[1+2*n] (suc n) = begin-equality
  6 * Σ≤ (suc n) (_^ 2)                          ≡⟨⟩
  6 * (Σ≤ n (_^ 2) + suc n ^ 2)                  ≡⟨ *-distribˡ-+ 6 (Σ≤ n (_^ 2)) (suc n ^ 2) ⟩
  6 *  Σ≤ n (_^ 2) + 6 * (suc n ^ 2)             ≡⟨ cong (_+ 6 * (suc n ^ 2)) $ 6*Σ≤[n,^2]≡n*[1+n]*[1+2*n] n ⟩
   n * (1 + n) * (1 + 2 * n) + 6 * ((1 + n) ^ 2) ≡⟨ Lemma.lemma₁ n ⟩
  (1 + n) * (2 + n) * (1 + 2 * (1 + n))          ∎
  where open ≤-Reasoning

-- Arithmetic sequence
{-
2*Σ<[n,i→d+a*i]≡??? : ∀ n d a → 2 * Σ< n (λ i → d + a * i) ≡ n * (2 * d + a * suc n)
2*Σ<[n,i→d+a*i]≡??? n d a = begin-equality
  2 * Σ< n (λ i → d + a * i)
    ≡⟨ {!   !} ⟩
  2 * (Σ< n (λ _ → d) + Σ< n (λ i → a * i))

  2 * (n * d + a * Σ< n id)
  2 * (n * d) + 2 * (a * Σ< n id)
  2 * n * d + a * (2 * Σ< n id)
  2 * n * d + a * (n * suc n)
  n * (2 * d + a * suc n)
    ∎
  where oepn ≤-Reasoning
-}


text:
-- Andreas, 2013-02-21, example by Andres Sicard Ramirez
module Issue782 where

open import Common.Prelude renaming (zero toz; suc tos; Nat toℕ)

f : ℕ → ℕ
f z     = z
f (s n) = z

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Proving properties without using pattern matching on refl
------------------------------------------------------------------------------

{-# OPTIONS --no-pattern-matching      #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}

module FOT.PA.Axiomatic.Standard.NoPatternMatchingOnRefl where

open import PA.Axiomatic.Standard.Base

------------------------------------------------------------------------------
-- From PA.Axiomatic.Standard.PropertiesI

-- Congruence properties

succCong : ∀ {m n} → m ≡ n → succ m ≡ succ n
succCong {m} h = subst (λ t → succ m ≡ succ t) h refl

+-leftCong : ∀ {m n o} → m ≡ n → m + o ≡ n + o
+-leftCong {m} {o = o} h = subst (λ t → m + o ≡ t + o) h refl

+-rightCong : ∀ {m n o} → n ≡ o → m + n ≡ m + o
+-rightCong {m} {n} h = subst (λ t → m + n ≡ m + t) h refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import Fragment.Algebra.Signature

module Fragment.Algebra.Properties where

open import Fragment.Algebra.Algebra
open import Fragment.Algebra.Free

open import Level using (Level)

open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; []; _∷_)

private
  variable
    a ℓ : Level

mutual
  map-extend : ∀ {Σ O a n} → {A : Set a}
               → Vec (Term Σ A) n
               → Vec (Term (Σ ⦅ O ⦆) A) n
  map-extend []       = []
  map-extend (x ∷ xs) = extend x ∷ map-extend xs

  extend : ∀ {Σ O} → {A : Set a}
           → Term Σ A → Term (Σ ⦅ O ⦆) A
  extend (atom x)    = atom x
  extend (term f xs) = term (oldₒ f) (map-extend xs)

forgetₒ : ∀ {Σ O} → Algebra (Σ ⦅ O ⦆) {a} {ℓ} → Algebra Σ {a} {ℓ}
forgetₒ {Σ = Σ} A = record { ∥_∥/≈           = ∥ A ∥/≈
                           ; ∥_∥/≈-isAlgebra = forget-isAlgebra
                           }
  where forget-⟦_⟧ : Interpretation Σ ∥ A ∥/≈
        forget-⟦ f ⟧ x = A ⟦ oldₒ f ⟧ x

        forget-⟦⟧-cong : Congruence Σ ∥ A ∥/≈ forget-⟦_⟧
        forget-⟦⟧-cong f x = (A ⟦ oldₒ f ⟧-cong) x

        forget-isAlgebra : IsAlgebra Σ ∥ A ∥/≈
        forget-isAlgebra = record { ⟦_⟧     = forget-⟦_⟧
                                  ; ⟦⟧-cong = forget-⟦⟧-cong
                                  }

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-# OPTIONS --type-in-type         #-}
{-# OPTIONS --no-termination-check #-}

-- In this post we'll consider how to define and generalize fixed-point combinators for families of
-- mutually recursive functions. Both in the lazy and strict settings.

module FixN where

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Base
open import Data.Bool.Base

-- This module is parameterized by `even` and `odd` functions and defines the `Test` type
-- which is used below for testing particular `even` and `odd`.
module Test (even : ℕ -> Bool) (odd : ℕ -> Bool) where
  open import Data.List.Base
  open import Data.Product using (_,′_)

  Test : Set
  Test =
      (  map even (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
      ,′ map odd  (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
      )
    ≡ (  true ∷ false ∷ true ∷ false ∷ true ∷ false ∷ []
      ,′ false ∷ true ∷ false ∷ true ∷ false ∷ true ∷ []
      )

-- Brings `Test : (ℕ -> Bool) -> (ℕ -> Bool) -> Set` in scope.
open Test

module Classic where
  open import Data.Product

  -- We can use the most straightforward fixed-point operator in order to get mutual recursion.
  {-# TERMINATING #-}
  fix : ∀ {A} -> (A -> A) -> A
  fix f = f (fix f)

  -- We instantiate `fix` to be defined over a pair of functions. I.e. a generic fixed-point
  -- combinator for a family of two mutually recursive functions has this type signature:
  -- `∀ {A B} -> (A × B -> A × B) -> A × B` which is an instance of `∀ {A} -> (A -> A) -> A`.

  -- Here is the even-and-odd example.
  -- `even` is denoted as the first element of the resulting tuple, `odd` is the second.
  evenAndOdd : (ℕ -> Bool) × (ℕ -> Bool)
  evenAndOdd = fix $ λ p ->
      -- `even` returns `true`  on `0` and calls `odd`  on `suc`
      (λ { 0 -> true  ; (suc n) -> proj₂ p n })
      -- `odd`  returns `false` on `0` and calls `even` on `suc`
    , (λ { 0 -> false ; (suc n) -> proj₁ p n })

  even : ℕ -> Bool
  even = proj₁ evenAndOdd

  odd : ℕ -> Bool
  odd = proj₂ evenAndOdd

  test : Test even odd
  test = refl

  -- And that's all.

  -- This Approach

  -- 1. relies on laziness
  -- 2. relies on tuples
  -- 3. allows to encode a family of arbitrary number of mutually recursive functions
  --      of possibly distinct types

  -- There is one pitfall, though, if we write this in Haskell:

  -- evenAndOdd :: ((Int -> Bool), (Int -> Bool))
  -- evenAndOdd = fix $ \(even, odd) ->
  --     ( (\n -> n == 0 || odd  (n - 1))
  --     , (\n -> n /= 0 && even (n - 1))
  --     )

  -- we'll get an infinite loop, because matching over tuples is strict in Haskell (in Agda it's lazy)
  -- which means that in order to return a tuple, you must first compute it to whnf, which is a loop.
  -- This is what the author of [1] stumpled upon. The fix is simple, though: just use lazy matching
  -- (aka irrefutable pattern) like this:

  -- evenAndOdd = fix $ \(~(even, odd)) -> ...

  -- In general, that's a good approach for a lazy language, but Plutus Core is a strict one (so far),
  -- so we need something else. Besides, we can do some pretty cool generalizations, so let's do them.

module PartlyUncurried2 where
  open import Data.Product

  -- It is clear that we can transform

  -- ∀ {A B} -> (A × B -> A × B) -> A × B

  -- into

  -- ∀ {A B R} -> (A × B -> A × B) -> (A -> B -> R) -> R

  -- by Church-encoding `A × B` into `∀ {R} -> (A -> B -> R) -> R`.
  -- However in our case we can also transform

  -- A × B -> A × B

  -- into

  -- ∀ {Q} -> (A -> B -> Q) -> A -> B -> Q

  -- Ignoring the former transformation right now, but performing the latter we get the following:

  fix2 : ∀ {A B} -> (∀ {Q} -> (A -> B -> Q) -> A -> B -> Q) -> A × B
  fix2 f = f (λ x y -> x) (proj₁ (fix2 f)) (proj₂ (fix2 f))
         , f (λ x y -> y) (proj₁ (fix2 f)) (proj₂ (fix2 f))

  -- `f` is what was of the `A × B -> A × B` type previously, but now instead of receiving a tuple
  -- and defining a tuple, `f` receives a selector and two values of types `A` and `B`. The values
  -- represent the functions being defined, while the selector is needed in order to select one of
  -- these functions.

  -- Consider the example:

  evenAndOdd : (ℕ -> Bool) × (ℕ -> Bool)
  evenAndOdd = fix2 $ λ select even odd -> select
    (λ { 0 -> true  ; (suc n) -> odd  n })
    (λ { 0 -> false ; (suc n) -> even n })

  -- `select` is only instantiated to either `λ x y -> x` or `λ x y -> y` which allow us
  -- to select the branch we want to go in. When defining the `even` function, we want to go in
  -- the first branch and thus instantiate `select` with `λ x y -> x`. When defining `odd`,
  -- we want the second branch and thus instantiate `select` with `λ x y -> y`.
  -- All these instantiations happen in the `fix2` function itself.

  -- It is instructive to inline `fix2` and `select` along with the particular selectors. We get:

  evenAndOdd-inlined : (ℕ -> Bool) × (ℕ -> Bool)
  evenAndOdd-inlined = defineEven (proj₁ evenAndOdd-inlined) (proj₂ evenAndOdd-inlined)
                     , defineOdd  (proj₁ evenAndOdd-inlined) (proj₂ evenAndOdd-inlined)
    where
      defineEven : (ℕ -> Bool) -> (ℕ -> Bool) -> ℕ -> Bool
      defineEven even odd = λ { 0 -> true  ; (suc n) -> odd  n }

      defineOdd  : (ℕ -> Bool) -> (ℕ -> Bool) -> ℕ -> Bool
      defineOdd  even odd = λ { 0 -> false ; (suc n) -> even n }

  -- I.e. each definition is parameterized by both functions and this is just the same fixed point
  -- of a tuple of functions that we've seen before.

  test : Test (proj₁ evenAndOdd) (proj₂ evenAndOdd)
  test = refl

  test-inlined : Test (proj₁ evenAndOdd-inlined) (proj₂ evenAndOdd-inlined)
  test-inlined = refl

module Uncurried where
  -- We can now do another twist and turn `A × B` into `∀ {R} -> (A -> B -> R) -> R` which finally
  -- allows us to get rid of tuples:

  fix2 : ∀ {A B R} -> (∀ {Q} -> (A -> B -> Q) -> A -> B -> Q) -> (A -> B -> R) -> R
  fix2 f k = k (fix2 f (f λ x y -> x)) (fix2 f (f λ x y -> y))

  -- `k` is the continuation that represents a Church-encoded tuple returned as the result.
  -- But... if `k` is just another way to construct a tuple, how are we not keeping `f` outside of
  -- recursion? Previously it was `fix f = f (fix f)` or

  -- fix2 f = f (λ x y -> x) (proj₁ (fix2 f)) (proj₂ (fix2 f))
  --        , f (λ x y -> y) (proj₁ (fix2 f)) (proj₂ (fix2 f))

  -- i.e. `f` is always an outermost call and recursive calls are somewhere inside. But in the
  -- definition above `f` is inside the recursive call. How is that? Watch the hands:

  --   fix2 f k                                                                                [1]
  -- = k (fix2 f (f  λ x y -> x))  (fix2 f (f  λ x y -> y))                                       [2]
  -- ~ k (fix2 f (f (λ x y -> x))) (fix2 f (f (λ x y -> y)))                                      [3]
  -- ~ k (f (λ x y -> x) (fix2 f (f λ x y -> x)) (fix2 f (f λ x y -> y)))
  --     (f (λ x y -> y) (fix2 f (f λ x y -> y)) (fix2 f (f λ x y -> y)))

  -- [1] unfold the definition of `fix2`
  -- [2] add parens around selectors for clarity
  -- [3] unfold the definition of `fix` in both the arguments of `k`

  -- The result is very similar to the one from the previous section
  -- (quoted in the snippet several lines above).

  -- And the test:

  evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
  evenAndOdd = fix2 $ λ select even odd -> select
    (λ { 0 -> true  ; (suc n) -> odd  n })
    (λ { 0 -> false ; (suc n) -> even n })

  test : Test (evenAndOdd λ x y -> x) (evenAndOdd λ x y -> y)
  test = refl

  -- It is straighforward to define a fixed-point combinator for a family of three mutually
  -- recursive functions:

  fix3 : ∀ {A B C R} -> (∀ {Q} -> (A -> B -> C -> Q) -> A -> B -> C -> Q) -> (A -> B -> C -> R) -> R
  fix3 f k = k (fix3 f (f λ x y z -> x)) (fix3 f (f λ x y z -> y)) (fix3 f (f λ x y z -> z))

  -- The pattern is clear and we can abstract it.

module UncurriedGeneral where
  -- The type signatures of the fixed point combinators from the above

  -- ∀ {A B} -> (∀ {Q} -> (A -> B -> Q) -> A -> B -> Q) -> ∀ {R} -> (A -> B -> R) -> R
  -- ∀ {A B C} -> (∀ {Q} -> (A -> B -> C -> Q) -> A -> B -> C -> Q) -> ∀ {R} -> (A -> B -> C -> R) -> R

  -- (`∀ {R}` is moved slightly righter than what it was previously, because it helps readability below)
  -- can be generalized to

  -- ∀ {F} -> (∀ {Q} -> F Q -> F Q) -> ∀ {R} -> F R -> R

  -- with `F` being `λ X -> A -> B -> X` in the first case and `λ X -> A -> B -> C -> X` in the second.
  -- That's fact (1).

  -- Now let's look at the definitions. There we see

  -- fix2 f k = k (fix2 f (f λ x y -> x)) (fix2 f (f λ x y -> y))
  -- fix3 f k = k (fix3 f (f λ x y z -> x)) (fix3 f (f λ x y z -> y)) (fix3 f (f λ x y z -> z))

  -- i.e. each recursive call is parameterized by the `f` that never changes, but also by
  -- the `f` applied to a selector and selectors do change. Thus the

  -- λ selector -> fix2 f (f selector)
  -- λ selector -> fix3 f (f selector)

  -- parts can be abstracted into something like

  -- λ selector -> fixSome f (f selector)

  -- where `fixSome` can be both `fix2` and `fix3` depending on what you instantiate it with.
  -- Then we only need combinators that duplicate the recursive case an appropriate number of times
  -- (2 for `fix2` and 3 for `fix3`) and supply a selector to each of the duplicates. That's fact (2).
  -- And those combinators have to be of the same type, so we can pass them to the generic
  -- fixed-point combinator we're deriving.

  -- To infer the type of those combinators we start by looking at the types of

  -- λ selector -> fix2 f (f selector)
  -- λ selector -> fix3 f (f selector)

  -- which are

  -- ∀ {Q} -> (A -> B -> Q) -> Q
  -- ∀ {Q} -> (A -> B -> C -> Q) -> Q

  -- correspondingly. I.e. the unifying type of

  -- λ selector -> fixSome f (f selector)

  -- is `∀ {Q} -> F Q -> Q`.

  -- Therefore, the combinators receive something of type `∀ {Q} -> F Q -> Q` and return something of
  -- type `∀ {R} -> F R -> R` (the same type, just alpha-converted for convenience), because that's
  -- what `fix2` and `fix3` and thus the generic fixed-point combinator return.
  -- I.e. the whole unifying type of those combinators is

  -- (∀ {R} -> (∀ {Q} -> F Q -> Q) -> F R -> R)

  -- That's fact (3).

  -- Assembling everything together, we arrive at

  fixBy : ∀ {F : Set -> Set}
        -> ((∀ {Q} -> F Q -> Q) -> ∀ {R} -> F R -> R)  -- by fact (3)
        -> (∀ {Q} -> F Q -> F Q) -> ∀ {R} -> F R -> R  -- by fact (1)
  fixBy by f = by (fixBy by f ∘ f)                     -- by fact (2)

  -- Let's now implement particular `by`s:

  by2 : ∀ {A B} -> (∀ {Q} -> (A -> B -> Q) -> Q) -> ∀ {R} -> (A -> B -> R) -> R
  by2 r k = k (r λ x y -> x) (r λ x y -> y)

  by3 : ∀ {A B C} -> (∀ {Q} -> (A -> B -> C -> Q) -> Q) -> ∀ {R} -> (A -> B -> C -> R) -> R
  by3 r k = k (r λ x y z -> x) (r λ x y z -> y) (r λ x y z -> z)

  -- and fixed-points combinators from the previous section in terms of what we derived in this one:

  fix2 : ∀ {A B} -> (∀ {Q} -> (A -> B -> Q) -> A -> B -> Q) -> ∀ {R} -> (A -> B -> R) -> R
  fix2 = fixBy by2

  fix3 : ∀ {A B C} -> (∀ {Q} -> (A -> B -> C -> Q) -> A -> B -> C -> Q) -> ∀ {R} -> (A -> B -> C -> R) -> R
  fix3 = fixBy by3

  -- That's it. One `fixBy` to rule them all. The final test:

  evenAndOdd : ∀ {R} -> ((ℕ -> Bool) -> (ℕ -> Bool) -> R) -> R
  evenAndOdd = fix2 $ λ select even odd -> select
    (λ { 0 -> true  ; (suc n) -> odd  n })
    (λ { 0 -> false ; (suc n) -> even n })

  test : Test (evenAndOdd λ x y -> x) (evenAndOdd λ x y -> y)
  test = refl

module LazinessStrictness where
  open UncurriedGeneral using (fixBy)

  -- So what about strictness? `fixBy` is generic enough to allow both lazy and strict derivatives.
  -- The version of strict `fix2` looks like this in Haskell:

  -- apply :: (a -> b) -> a -> b
  -- apply = ($!)

  -- fix2
  --     :: ((a1 -> b1) -> (a2 -> b2) -> a1 -> b1)
  --     -> ((a1 -> b1) -> (a2 -> b2) -> a2 -> b2)
  --     -> ((a1 -> b1) -> (a2 -> b2) -> r) -> r
  -- fix2 f g k = k
  --     (\x1 -> f `apply` fix2 f g (\x y -> x) `apply` fix2 f g (\x y -> y) `apply` x1)
  --     (\x2 -> g `apply` fix2 f g (\x y -> x) `apply` fix2 f g (\x y -> y) `apply` x2)

  -- This is just like the Z combinator is of type `((a -> b) -> a -> b) -> a -> b`, so that it can
  -- be used to get fixed points of functions in a strict language where the Y combinator loops forever.

  -- The version of `fix2` that works in a strict language can be defined as follows:

  by2' : ∀ {A₁ B₁ A₂ B₂}
       -> (∀ {Q} -> ((A₁ -> B₁) -> (A₂ -> B₂) -> Q) -> Q)
       -> ∀ {R} -> ((A₁ -> B₁) -> (A₂ -> B₂) -> R) -> R
  by2' r k = k (λ x₁ -> r λ f₁ f₂ -> f₁ x₁) (λ x₂ -> r λ f₁ f₂ -> f₂ x₂)

  fix2' : ∀ {A₁ B₁ A₂ B₂}
        -> (∀ {Q} -> ((A₁ -> B₁) -> (A₂ -> B₂) -> Q) -> (A₁ -> B₁) -> (A₂ -> B₂) -> Q)
        -> ∀ {R} -> ((A₁ -> B₁) -> (A₂ -> B₂) -> R) -> R
  fix2' = fixBy by2'

  -- The difference is that in

  by2 : ∀ {A B} -> (∀ {Q} -> (A -> B -> Q) -> Q) -> ∀ {R} -> (A -> B -> R) -> R
  by2 r k = k (r λ x y -> x) (r λ x y -> y)

  -- both calls to `r` are forced before `k` returns, while in `by2'` additional lambdas that bind
  -- `x₁` and `x₂` block the recursive calls from being forced, so `k` at some point can decide not to
  -- recurse anymore (i.e. not to force recursive calls) and return a result instead.

module ComputeUncurriedGeneral where
  -- You might wonder whether we can define a single `fixN` which receives a natural number and
  -- computes the appropriate fixed-point combinator of mutually recursive functions. E.g.

  -- fixN 2 ~> fix2
  -- fixN 3 ~> fix3

  -- So that we do not even need to specify `by2` and `by3` by ourselves. Yes we can do that, see [2]
  -- (the naming is slightly different there).

  -- Moreover, we can assign a type to `fixN` in pure System Fω, see [3].

module References where
  -- [1] "Mutual Recursion in Final Encoding", Andreas Herrmann
  -- https://aherrmann.github.io/programming/2016/05/28/mutual-recursion-in-final-encoding/

  -- [2] https://gist.github.com/effectfully/b3185437da14322c775f4a7691b6fe1f#file-mutualfixgenericcompute-agda

  -- [3] https://gist.github.com/effectfully/b3185437da14322c775f4a7691b6fe1f#file-mutualfixgenericcomputenondep-agda

max_stars_repo_name: jbgi/plutus

max_issues_repo_name: jbgi/plutus

max_forks_repo_name: jbgi/plutus


text:
module Basic.Compiler.CorrectTo where

open import Data.List
open import Relation.Binary.PropositionalEquality

open import Basic.Compiler.Code
open import Basic.AST
open import Basic.BigStep
open import Utils.Decidable

{-
Lemma 3.21

One half of the correctness proof for the compiler.

The proof here is a bit neater than the one in the book. The book uses exercises 3.19 and 3.4
to concatenate instruction lists, while I use my _▷*<>_, which does the same in one step.
Otherwise the proofs are the same, and there's not much space for variations.
-}

𝓒-correct-to :
  ∀ {n}{S : St n}{s s'}
  → ⟨ S , s ⟩⟱ s' → ⟨ 𝓒⟦ S ⟧ˢ , [] , s ⟩▷*⟨ [] , [] , s' ⟩

𝓒-correct-to (ass {_}{x}{a}) = 𝓒-Exp-nat a ▷*<> STORE x ∷ done
𝓒-correct-to skip = NOOP ∷ done
𝓒-correct-to (a , b) = 𝓒-correct-to a ▷*<> 𝓒-correct-to b

𝓒-correct-to (if-true {s = s}{b = b} x p) with 𝓒-Exp-bool {e = []}{s = s} b
... | condition rewrite T→≡true x =
  condition ▷*<> BRANCH-[] ∷ 𝓒-correct-to p

𝓒-correct-to (if-false {s = s}{b = b} x p) with 𝓒-Exp-bool {e = []}{s = s} b
... | condition rewrite F→≡false x =
  condition ▷*<> BRANCH-[] ∷ 𝓒-correct-to p

𝓒-correct-to (while-true {s}{b = b} x p k) with 𝓒-Exp-bool {e = []}{s = s} b
... | condition rewrite T→≡true x =
  LOOP ∷ condition ▷*<> BRANCH-[] ∷ 𝓒-correct-to p ▷*<> 𝓒-correct-to k

𝓒-correct-to (while-false {s}{S}{b} x) with 𝓒-Exp-bool {e = []}{s = s} b
... | condition rewrite F→≡false x =
  LOOP ∷ condition ▷*<> BRANCH-[] ∷ NOOP ∷ done

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
-- Paths in a graph
{-# OPTIONS --safe #-}

module Cubical.Data.Graph.Path where

open import Cubical.Data.Graph.Base
open import Cubical.Data.List.Base hiding (_++_)
open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties
open import Cubical.Data.Sigma.Base hiding (Path)
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude hiding (Path)

module _ {ℓv ℓe : Level} where

  module _ (G : Graph ℓv ℓe) where
    data Path : (v w : Node G) → Type (ℓ-max ℓv ℓe) where
      pnil : ∀ {v} → Path v v
      pcons : ∀ {v w x} → Path v w → Edge G w x → Path v x

    -- Path concatenation
    ccat : ∀ {v w x} → Path v w → Path w x → Path v x
    ccat P pnil = P
    ccat P (pcons Q e) = pcons (ccat P Q) e

    private
      _++_ = ccat
      infixr 20 _++_

    -- Some properties
    pnil++ : ∀ {v w} (P : Path v w) → pnil ++ P ≡ P
    pnil++ pnil = refl
    pnil++ (pcons P e) = cong (λ P → pcons P e) (pnil++ _)

    ++assoc : ∀ {v w x y}
        (P : Path v w) (Q : Path w x) (R : Path x y)
      → (P ++ Q) ++ R ≡ P ++ (Q ++ R)
    ++assoc P Q pnil = refl
    ++assoc P Q (pcons R e) = cong (λ P → pcons P e) (++assoc P Q R)

    -- Paths as lists
    pathToList : ∀ {v w} → Path v w
        → List (Σ[ x ∈ Node G ] Σ[ y ∈ Node G ] Edge G x y)
    pathToList pnil = []
    pathToList (pcons P e) = (_ , _ , e) ∷ (pathToList P)

    -- Path v w is a set
    -- Lemma 4.2 of https://arxiv.org/abs/2112.06609
    module _ (isSetNode : isSet (Node G))
             (isSetEdge : ∀ v w → isSet (Edge G v w)) where

      -- This is called ̂W (W-hat) in the paper
      PathWithLen : ℕ → Node G → Node G → Type (ℓ-max ℓv ℓe)
      PathWithLen 0 v w = Lift {j = ℓe} (v ≡ w)
      PathWithLen (suc n) v w = Σ[ k ∈ Node G ] (PathWithLen n v k × Edge G k w)

      isSetPathWithLen : ∀ n v w → isSet (PathWithLen n v w)
      isSetPathWithLen 0 _ _ = isOfHLevelLift 2 (isProp→isSet (isSetNode _ _))
      isSetPathWithLen (suc n) _ _ = isSetΣ isSetNode λ _ →
          isSet× (isSetPathWithLen _ _ _) (isSetEdge _ _)

      isSet-ΣnPathWithLen : ∀ {v w} → isSet (Σ[ n ∈ ℕ ] PathWithLen n v w)
      isSet-ΣnPathWithLen = isSetΣ isSetℕ (λ _ → isSetPathWithLen _ _ _)

      Path→PathWithLen : ∀ {v w} → Path v w → Σ[ n ∈ ℕ ] PathWithLen n v w
      Path→PathWithLen pnil = 0 , lift refl
      Path→PathWithLen (pcons P e) = suc (Path→PathWithLen P .fst) ,
                                          _ , Path→PathWithLen P .snd , e

      PathWithLen→Path : ∀ {v w} → Σ[ n ∈ ℕ ] PathWithLen n v w → Path v w
      PathWithLen→Path (0 , q) = subst (Path _) (q .lower) pnil
      PathWithLen→Path (suc n , _ , pwl , e) = pcons (PathWithLen→Path (n , pwl)) e

      Path→PWL→Path : ∀ {v w} P → PathWithLen→Path {v} {w} (Path→PathWithLen P) ≡ P
      Path→PWL→Path {v} pnil = substRefl {B = Path v} pnil
      Path→PWL→Path (pcons P x) = cong₂ pcons (Path→PWL→Path _) refl

      isSetPath : ∀ v w → isSet (Path v w)
      isSetPath v w = isSetRetract Path→PathWithLen PathWithLen→Path
                                   Path→PWL→Path isSet-ΣnPathWithLen

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 --rewriting #-}

open import lib.Base
open import lib.PathGroupoid
open import lib.PathFunctor
open import lib.path-seq.Concat
open import lib.path-seq.Reasoning

module lib.path-seq.Inversion {i} {A : Type i} where

seq-! : {a a' : A} → a =-= a' → a' =-= a
seq-! [] = []
seq-! (p ◃∙ s) = seq-! s ∙▹ ! p

seq-!-∙▹ : {a a' a'' : A} (s : a =-= a') (q : a' == a'')
  → seq-! (s ∙▹ q) == ! q ◃∙ seq-! s
seq-!-∙▹ [] q = idp
seq-!-∙▹ (p ◃∙ s) q = ap (_∙▹ ! p) (seq-!-∙▹ s q)

seq-!-seq-! : {a a' : A} (s : a =-= a')
  → seq-! (seq-! s) == s
seq-!-seq-! [] = idp
seq-!-seq-! (p ◃∙ s) =
  seq-! (seq-! s ∙▹ ! p)
    =⟨ seq-!-∙▹ (seq-! s) (! p) ⟩
  ! (! p) ◃∙ seq-! (seq-! s)
    =⟨ ap2 _◃∙_ (!-! p) (seq-!-seq-! s) ⟩
  p ◃∙ s =∎

!-∙-seq : {a a' : A} (s : a =-= a')
  → ! (↯ s) ◃∎ =ₛ seq-! s
!-∙-seq [] = =ₛ-in idp
!-∙-seq (p ◃∙ s) =
  ! (↯ (p ◃∙ s)) ◃∎
    =ₛ₁⟨ ap ! (↯-∙∙ (p ◃∎) s) ⟩
  ! (p ∙ ↯ s) ◃∎
    =ₛ⟨ =ₛ-in {t = ! (↯ s) ◃∙ ! p ◃∎} (!-∙ p (↯ s)) ⟩
  ! (↯ s) ◃∙ ! p ◃∎
    =ₛ⟨ 0 & 1 & !-∙-seq s ⟩
  seq-! s ∙▹ ! p ∎ₛ

∙-!-seq : {a a' : A} (s : a =-= a')
  → seq-! s =ₛ ! (↯ s) ◃∎
∙-!-seq s = !ₛ (!-∙-seq s)

!-=ₛ : {a a' : A} {s t : a =-= a'} (e : s =ₛ t)
  → seq-! s =ₛ seq-! t
!-=ₛ {s = s} {t = t} e =
  seq-! s
    =ₛ⟨ ∙-!-seq s ⟩
  ! (↯ s) ◃∎
    =ₛ₁⟨ ap ! (=ₛ-out e) ⟩
  ! (↯ t) ◃∎
    =ₛ⟨ !-∙-seq t ⟩
  seq-! t ∎ₛ

seq-!-inv-l : {a a' : A} (s : a =-= a')
  → seq-! s ∙∙ s =ₛ []
seq-!-inv-l s = =ₛ-in $
  ↯ (seq-! s ∙∙ s)
    =⟨ ↯-∙∙ (seq-! s) s ⟩
  ↯ (seq-! s) ∙ ↯ s
    =⟨ ap (_∙ ↯ s) (=ₛ-out (∙-!-seq s)) ⟩
  ! (↯ s) ∙ ↯ s
    =⟨ !-inv-l (↯ s) ⟩
  idp =∎

seq-!-inv-r : {a a' : A} (s : a =-= a')
  → s ∙∙ seq-! s =ₛ []
seq-!-inv-r s = =ₛ-in $
  ↯ (s ∙∙ seq-! s)
    =⟨ ↯-∙∙ s (seq-! s) ⟩
  ↯ s ∙ ↯ (seq-! s)
    =⟨ ap (↯ s ∙_) (=ₛ-out (∙-!-seq s)) ⟩
  ↯ s ∙ ! (↯ s)
    =⟨ !-inv-r (↯ s) ⟩
  idp =∎

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module Avionics.List where

open import Data.Bool using (Bool; true; false; T)
open import Data.List as List using (List; []; _∷_; any)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; inspect; [_]; refl)

open import Avionics.Bool using (≡→T)

≡→any : ∀ {a} {A : Set a} (f) (ns : List A)
        → any f ns ≡ true
        → Any (T ∘ f) ns
        --→ Any (λ x → T (f x)) ns
≡→any f [] ()
≡→any f (n ∷ ns) any-f-⟨n∷ns⟩≡true with f n | inspect f n
... | true  | [ fn≡t ] = here (≡→T fn≡t)
... | false | _        = there (≡→any f ns any-f-⟨n∷ns⟩≡true)

any→≡ : ∀ {a} {A : Set a} (f) (ns : List A)
        → Any (T ∘ f) ns
        → any f ns ≡ true
any→≡ f (n ∷ _) (here _) with f n
... | true = refl -- or: T→≡ [*proof*from*here*]
any→≡ f (n ∷ ns) (there Any[T∘f]ns) with f n
... | true = refl
... | false = any→≡ f ns Any[T∘f]ns

any-map : ∀ {A B : Set} {p : B → Set} {ls : List A}
          (f : A → B)
        → Any p (List.map f ls)
        → Any (p ∘ f) ls
--any-map {ls = []} _ ()
any-map {ls = l ∷ ls} f (here pb) = here pb
any-map {ls = l ∷ ls} f (there pb) = there (any-map f pb)

any-map-rev : ∀ {A B : Set} {p : B → Set} {ls : List A}
          (f : A → B)
        → Any (p ∘ f) ls
        → Any p (List.map f ls)
any-map-rev {ls = l ∷ ls} f (here pb) = here pb
any-map-rev {ls = l ∷ ls} f (there pb) = there (any-map-rev f pb)

max_stars_repo_name: RPI-WCL/safety-envelopes-sentinels

max_issues_repo_name: RPI-WCL/safety-envelopes-sentinels

max_forks_repo_name: RPI-WCL/safety-envelopes-sentinels


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Either type which calls out to Haskell via the FFI
------------------------------------------------------------------------

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

module Foreign.Haskell.Either where

open import Level
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)

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

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

data Either (A : Set a) (B : Set b) : Set (a ⊔ b) where
  left  : A → Either A B
  right : B → Either A B

{-# FOREIGN GHC type AgdaEither l1 l2 a b = Either a b #-}
{-# COMPILE GHC Either = data MAlonzo.Code.Foreign.Haskell.Either.AgdaEither (Left | Right) #-}

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

toForeign : A ⊎ B → Either A B
toForeign (inj₁ a) = left a
toForeign (inj₂ b) = right b

fromForeign : Either A B → A ⊎ B
fromForeign (left a)  = inj₁ a
fromForeign (right b) = inj₂ b


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

-- Definition of Monoidal Category

-- Big design decision that differs from the previous version:
-- Do not go through "Functor.Power" to encode variables and work
-- at the level of NaturalIsomorphisms, instead work at the object/morphism
-- level, via the more direct _⊗₀_ _⊗₁_ _⊗- -⊗_.
-- The original design needed quite a few contortions to get things working,
-- but these are simply not needed when working directly with the morphisms.
--
-- Smaller design decision: export some items with long names
-- (unitorˡ, unitorʳ and associator), but internally work with the more classical
-- short greek names (λ, ρ and α respectively).

module Categories.Category.Monoidal where

open import Categories.Category.Monoidal.Core public

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module TicketServer where

open import IO using (run; putStrLn; mapM′; _>>_)
open import Coinduction using (♯_)
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺ using (ℕ⁺; suc; NumberPos)
open import Data.String using (String)
open import Data.List using (List; []; _∷_; map)
open import Data.Colist using (fromList)
open import Function using (_$_; _∘_)

open import Data.Environment
open import nodcap.Base
open import nodcap.Typing
open import nodcap.Norm
open import nodcap.Show renaming (showTerm to show)
open import nodcap.NF.Show renaming (showTerm to showNF)

Ticket UserId Sale Receipt : Type
Ticket  = ⊥ ⊕ ⊥
UserId  = 𝟏 ⊕ 𝟏
Sale    = UserId ⊸ Ticket
Receipt = UserId ⊗ Ticket

ticket₁ ticket₂ : {Γ : Environment} → ⊢ Γ → ⊢ Ticket ∷ Γ
ticket₁ x = sel₁ (wait x)
ticket₂ x = sel₂ (wait x)

sale₁ sale₂ : {Γ : Environment} → ⊢ Γ → ⊢ Sale ∷ Receipt ∷ Γ
sale₁ x
  = recv
  $ exch (bbl [])
  $ ticket₁
  $ exch (bbl [])
  $ send ax (ticket₁ x)
sale₂ x
  = recv
  $ exch (bbl [])
  $ ticket₂
  $ exch (bbl [])
  $ send ax (ticket₂ x)

client₁ client₂ : ⊢ Sale ^ ∷ []
client₁ = send (sel₁ halt) (case halt halt)
client₂ = send (sel₂ halt) (case halt halt)

server : ⊢ ?[ suc (suc zero) ] Sale ∷ Receipt ∷ Receipt ∷ 𝟏 ∷ []
server
  = cont
  $ mk?₁
  $ exch (bwd (_ ∷ []) (_ ∷ []))
  $ sale₁
  $ mk?₁
  $ sale₂
  $ halt

clients : ⊢ ![ 2 ] (Sale ^) ∷ []
clients
  = pool (mk!₁ client₁) (mk!₁ client₂)

main = run (mapM′ putStrLn (fromList strs))
  where
    proc = cut server clients
    strs = "Process:"
         ∷ show proc
         ∷ "Result:"
         ∷ map showNF (nfND proc)

-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
postulate
  A : Set
  F : (A : Set₁) → (A → A → Set) → Set

syntax F A (λ x y → B) = y , y ⟨ A ∼ B ⟩ x

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Cats.Category.Slice where

open import Data.Product using (_,_ ; proj₁ ; proj₂)
open import Level
open import Relation.Binary using (IsEquivalence ; _Preserves₂_⟶_⟶_)

open import Cats.Category

module _ {lo la l≈} (C : Category lo la l≈) (X : Category.Obj C) where

  infixr 9 _∘_
  infixr 4 _≈_

  private
    module C = Category C
    module ≈ = C.≈

  record Obj : Set (lo ⊔ la) where
    constructor mkObj
    field
      {Dom} : C.Obj
      arr : Dom C.⇒ X

  open Obj

  record _⇒_ (f g : Obj) : Set (la ⊔ l≈) where
    field
      dom : Dom f C.⇒ Dom g
      commute : arr f C.≈ arr g C.∘ dom

  open _⇒_

  record _≈_ {A B} (F G : A ⇒ B) : Set l≈ where -- [1]
    constructor ≈-i
    field
      dom : dom F C.≈ dom G

  -- [1] This could also be defined as
  --
  --   F ≈ G = dom F C.≈ dom G
  --
  -- but Agda was then giving me very strange unsolved metas in _/_ below.

  id : ∀ {A} → A ⇒ A
  id = record { dom = C.id ; commute = ≈.sym C.id-r }

  _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)
  _∘_ {F} {G} {H}
    record { dom = F-dom ; commute = F-commute}
    record { dom = G-dom ; commute = G-commute}
      = record
      { dom = F-dom C.∘ G-dom
      ; commute
          = begin
              arr F
            ≈⟨ G-commute ⟩
              arr G C.∘ G-dom
            ≈⟨ C.∘-resp-l F-commute ⟩
              (arr H C.∘ F-dom) C.∘ G-dom
            ≈⟨ C.assoc ⟩
              arr H C.∘ F-dom C.∘ G-dom
            ∎
      }
    where
      open C.≈-Reasoning

  ≈-equiv : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
  ≈-equiv = record
      { refl = ≈-i ≈.refl
      ; sym = λ { (≈-i eq) → ≈-i (≈.sym eq) }
      ; trans = λ { (≈-i eq₁) (≈-i eq₂) → ≈-i (≈.trans eq₁ eq₂) }
      }

  ∘-preserves-≈ : ∀ {A B C} → _∘_ {A} {B} {C} Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
  ∘-preserves-≈ (≈-i eq₁) (≈-i eq₂) = ≈-i (C.∘-resp eq₁ eq₂)

  id-identity-r : ∀ {A B} {F : A ⇒ B} → F ∘ id ≈ F
  id-identity-r = ≈-i C.id-r

  id-identity-l : ∀ {A B} {F : A ⇒ B} → id ∘ F ≈ F
  id-identity-l = ≈-i C.id-l

  ∘-assoc : ∀ {A B C D} {F : C ⇒ D} {G : B ⇒ C} {H : A ⇒ B}
    → (F ∘ G) ∘ H ≈ F ∘ (G ∘ H)
  ∘-assoc = ≈-i C.assoc

  instance _/_ : Category (la ⊔ lo) (l≈ ⊔ la) l≈
  _/_ = record
      { Obj = Obj
      ; _⇒_ = _⇒_
      ; _≈_ = _≈_
      ; id = id
      ; _∘_ = _∘_
      ; equiv = ≈-equiv
      ; ∘-resp = ∘-preserves-≈
      ; id-r = id-identity-r
      ; id-l = id-identity-l
      ; assoc = ∘-assoc
      }

  open Category _/_ using (IsTerminal ; IsUnique ; ∃!-intro)

  One : Obj
  One = mkObj C.id

  One-Terminal : IsTerminal One
  One-Terminal Y@(mkObj f)
      = ∃!-intro F _ F-Unique
    where
      F : Y ⇒ One
      F = record { dom = f ; commute = C.≈.sym C.id-l }

      F-Unique : IsUnique F
      F-Unique {record { dom = g ; commute = commute }} _
          = ≈-i (≈.trans commute C.id-l)

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:
-- An Agda implementation of the n queens program from the nofib
-- benchmark. Very inefficient, uses unary natural numbers instead of
-- machine integers.

module N-queens where

open import Category.Monad
open import Coinduction
open import Data.Bool hiding (_≟_)
open import Data.Char hiding (_≟_)
open import Data.Fin using (#_)
open import Data.Digit
open import Data.Integer as Z using (+_; _⊖_)
open import Data.List as List
open import Data.Maybe as Maybe
open import Data.Nat
open import Data.Nat.Show
open import Data.String as String using (String)
open import Data.Unit hiding (_≟_)
open import Function
open import IO using (IO)
import IO.Primitive as Primitive
open import Relation.Nullary.Decidable

------------------------------------------------------------------------
-- Things missing from the standard library

take_[_…] : ℕ → ℕ → List ℕ
take zero  [ n …] = []
take suc k [ n …] = n ∷ take k [ suc n …]

[_…_] : ℕ → ℕ → List ℕ
[ m              … n              ] with compare m n
[ .(suc (n + k)) … n              ] | greater .n k = []
[ m              … .m             ] | equal .m     = [ m ]
[ m              … .(suc (m + k)) ] | less .m k    = take (2 + k) [ m …]

guard : Bool → List ⊤
guard true  = [ _ ]
guard false = []

postulate
  getArgs′ : Primitive.IO (List String)

{-# IMPORT System.Environment #-}
{-# COMPILED getArgs′ System.Environment.getArgs #-}

getArgs : IO (List String)
getArgs = lift getArgs′
  where open IO

read : List Char → Maybe ℕ
read [] = nothing
read ds = fromDigits ∘ reverse <$> mapM Maybe.monad charToDigit ds
  where
  open RawMonad Maybe.monad

  charToDigit : Char → Maybe (Digit 10)
  charToDigit '0' = just (# 0)
  charToDigit '1' = just (# 1)
  charToDigit '2' = just (# 2)
  charToDigit '3' = just (# 3)
  charToDigit '4' = just (# 4)
  charToDigit '5' = just (# 5)
  charToDigit '6' = just (# 6)
  charToDigit '7' = just (# 7)
  charToDigit '8' = just (# 8)
  charToDigit '9' = just (# 9)
  charToDigit _   = nothing

------------------------------------------------------------------------
-- The main program

nsoln : ℕ → ℕ
nsoln nq = length (gen nq)
  where
  open RawMonad List.monad

  safe : ℕ → ℕ → List ℕ → Bool
  safe x d []      = true
  safe x d (q ∷ l) = not ⌊ x ≟ q ⌋ ∧
                     not ⌊ x ≟ q + d ⌋ ∧
                     not ⌊ + x Z.≟ q ⊖ d ⌋ ∧
                     -- Equivalent to previous line, because x ≥ 1:
                     -- not ⌊ x ≟ q ∸ d ⌋ ∧
                     safe x (1 + d) l

  gen : ℕ → List (List ℕ)
  gen zero    = [ [] ]
  gen (suc n) =
    gen n              >>= λ b →
    [ 1 … nq ]         >>= λ q →
    guard (safe q 1 b) >>
    return (q ∷ b)

main = run (♯ getArgs >>= λ arg → ♯ main′ arg)
  where
  open IO

  main′ : List String → IO ⊤
  main′ (arg ∷ []) with read (String.toList arg)
  ... | just n  = putStrLn (show (nsoln n))
  ... | nothing = return _
  main′ _ = return _

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- Logical equivalences
------------------------------------------------------------------------

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

module Logical-equivalence where

open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)

private
  variable
    a b p      : Level
    @0 A B C D : Type a
    @0 P Q     : A → Type p

------------------------------------------------------------------------
-- Logical equivalence

-- A ⇔ B means that A and B are logically equivalent.

infix 0 _⇔_

record _⇔_ {f t} (From : Type f) (To : Type t) : Type (f ⊔ t) where
  field
    to   : From → To
    from : To → From

------------------------------------------------------------------------
-- Equivalence relation

-- _⇔_ is an equivalence relation.

id : A ⇔ A
id = record
  { to   = P.id
  ; from = P.id
  }

inverse : A ⇔ B → B ⇔ A
inverse A⇔B ._⇔_.to   = let record { from = from } = A⇔B in from
inverse A⇔B ._⇔_.from = let record { to   = to   } = A⇔B in to

infixr 9 _∘_

_∘_ : B ⇔ C → A ⇔ B → A ⇔ C
(f ∘ g) ._⇔_.to =
  let record { to = f-to } = f
      record { to = g-to } = g
  in f-to ⊚ g-to
(f ∘ g) ._⇔_.from =
  let record { from = f-from } = f
      record { from = g-from } = g
  in g-from ⊚ f-from

-- "Equational" reasoning combinators.

infix  -1 finally-⇔
infixr -2 step-⇔

-- For an explanation of why step-⇔ is defined in this way, see
-- Equality.step-≡.

step-⇔ : (@0 A : Type a) → B ⇔ C → A ⇔ B → A ⇔ C
step-⇔ _ = _∘_

syntax step-⇔ A B⇔C A⇔B = A ⇔⟨ A⇔B ⟩ B⇔C

finally-⇔ : (@0 A : Type a) (@0 B : Type b) → A ⇔ B → A ⇔ B
finally-⇔ _ _ A⇔B = A⇔B

syntax finally-⇔ A B A⇔B = A ⇔⟨ A⇔B ⟩□ B □

------------------------------------------------------------------------
-- Preservation lemmas

-- Note that all of the type arguments of these lemmas are erased.

-- _⊎_ preserves logical equivalences.

infixr 2 _×-cong_

_×-cong_ : A ⇔ C → B ⇔ D → A × B ⇔ C × D
A⇔C ×-cong B⇔D =
  let record { to = to₁; from = from₁ } = A⇔C
      record { to = to₂; from = from₂ } = B⇔D
  in
  record
    { to   = Σ-map to₁   to₂
    ; from = Σ-map from₁ from₂
    }

-- ∃ preserves logical equivalences.

∃-cong : (∀ x → P x ⇔ Q x) → ∃ P ⇔ ∃ Q
∃-cong P⇔Q = record
  { to   = λ (x , y) → x , let record { to   = to   } = P⇔Q x in to   y
  ; from = λ (x , y) → x , let record { from = from } = P⇔Q x in from y
  }

-- _⊎_ preserves logical equivalences.

infixr 1 _⊎-cong_

_⊎-cong_ : A ⇔ C → B ⇔ D → A ⊎ B ⇔ C ⊎ D
A⇔C ⊎-cong B⇔D =
  let record { to = to₁; from = from₁ } = A⇔C
      record { to = to₂; from = from₂ } = B⇔D
  in
  record
    { to   = ⊎-map to₁   to₂
    ; from = ⊎-map from₁ from₂
    }

-- The non-dependent function space preserves logical equivalences.

→-cong : A ⇔ C → B ⇔ D → (A → B) ⇔ (C → D)
→-cong A⇔C B⇔D =
  let record { to = to₁; from = from₁ } = A⇔C
      record { to = to₂; from = from₂ } = B⇔D
  in
  record
    { to   = (to₂   ⊚_) ⊚ (_⊚ from₁)
    ; from = (from₂ ⊚_) ⊚ (_⊚ to₁)
    }

-- Π preserves logical equivalences in its second argument.

∀-cong :
  ((x : A) → P x ⇔ Q x) →
  ((x : A) → P x) ⇔ ((x : A) → Q x)
∀-cong P⇔Q = record
  { to   = λ f x → let record { to   = to   } = P⇔Q x in to   (f x)
  ; from = λ f x → let record { from = from } = P⇔Q x in from (f x)
  }

-- The implicit variant of Π preserves logical equivalences in its
-- second argument.

implicit-∀-cong :
  ({x : A} → P x ⇔ Q x) →
  ({x : A} → P x) ⇔ ({x : A} → Q x)
implicit-∀-cong P⇔Q = record
  { to   = λ f → let record { to   = to   } = P⇔Q in to   f
  ; from = λ f → let record { from = from } = P⇔Q in from f
  }

-- ↑ preserves logical equivalences.

↑-cong : B ⇔ C → ↑ a B ⇔ ↑ a C
↑-cong B⇔C =
  let record { to = to; from = from } = B⇔C in
  record
    { to   = λ (lift x) → lift (to   x)
    ; from = λ (lift x) → lift (from x)
    }

-- _⇔_ preserves logical equivalences.

⇔-cong : A ⇔ B → C ⇔ D → (A ⇔ C) ⇔ (B ⇔ D)
⇔-cong {A = A} {B = B} {C = C} {D = D} A⇔B C⇔D = record
  { to   = λ A⇔C →
             B  ⇔⟨ inverse A⇔B ⟩
             A  ⇔⟨ A⇔C ⟩
             C  ⇔⟨ C⇔D ⟩□
             D  □
  ; from = λ B⇔D →
             A  ⇔⟨ A⇔B ⟩
             B  ⇔⟨ B⇔D ⟩
             D  ⇔⟨ inverse C⇔D ⟩□
             C  □
  }

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

open import lib.Basics
open import lib.NType2
open import lib.types.TLevel
open import lib.types.Sigma
open import lib.types.Pi

module lib.types.Groupoid where

record GroupoidStructure {i j} {El : Type i} (Arr : El → El → Type j)
  (_ : ∀ x y → has-level 0 (Arr x y)) : Type (lmax i j) where
  field
    ident : ∀ {x} → Arr x x
    inv : ∀ {x y} → Arr x y → Arr y x
    comp : ∀ {x y z} → Arr x y → Arr y z → Arr x z
    unit-l : ∀ {x y} (a : Arr x y) → comp ident a == a
    assoc : ∀ {x y z w} (a : Arr x y) (b : Arr y z) (c : Arr z w)
              → comp (comp a b) c == comp a (comp b c)
    inv-l : ∀ {x y } (a : Arr x y) → (comp (inv a) a) == ident

  private
    infix 80 _⊙_
    _⊙_ = comp

  abstract
    inv-r  : ∀ {x y} (a : Arr x y) → a ⊙ inv a == ident
    inv-r a =
      a ⊙ inv a                           =⟨ ! $ unit-l (a ⊙ inv a) ⟩
      ident ⊙ (a ⊙ inv a)                 =⟨ ! $ inv-l (inv a) |in-ctx _⊙ (a ⊙ inv a) ⟩
      (inv (inv a) ⊙ inv a) ⊙ (a ⊙ inv a) =⟨ assoc (inv (inv a)) (inv a) (a ⊙ inv a) ⟩
      inv (inv a) ⊙ (inv a ⊙ (a ⊙ inv a)) =⟨ ! $ assoc (inv a) a (inv a) |in-ctx inv (inv a) ⊙_ ⟩
      inv (inv a) ⊙ ((inv a ⊙ a) ⊙ inv a) =⟨ inv-l a |in-ctx (λ h → inv (inv a) ⊙ (h ⊙ inv a)) ⟩
      inv (inv a) ⊙ (ident ⊙ inv a)       =⟨ unit-l (inv a) |in-ctx inv (inv a) ⊙_ ⟩
      inv (inv a) ⊙ inv a                 =⟨ inv-l (inv a) ⟩
      ident                               =∎

    unit-r : ∀ {x y} (a : Arr x y) → a ⊙ ident == a
    unit-r a =
      a ⊙ ident          =⟨ ! (inv-l a) |in-ctx a ⊙_ ⟩
      a ⊙ (inv a ⊙ a)    =⟨ ! $ assoc a (inv a) a ⟩
      (a ⊙ inv a) ⊙ a    =⟨ inv-r a |in-ctx _⊙ a ⟩
      ident ⊙ a          =⟨ unit-l a ⟩
      a                  =∎

record PreGroupoid i j : Type (lsucc (lmax i j)) where
  constructor groupoid
  field
    El : Type i
    Arr : El → El → Type j
    Arr-level : ∀ x y → has-level 0 (Arr x y)
    groupoid-struct : GroupoidStructure Arr Arr-level

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- Andreas, 2017-01-05, issue #2376 reporte by gallais
-- Termination checker should eta-expand clauses to see more.

-- This may have a slight performance penalty when computing call matrices,
-- but not too big, as they are sparse.

open import Agda.Builtin.Nat

-- Arity ~ 300, still does not kill termination checker.
T =
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat →
  Nat → Nat → Nat → Nat → Nat → Nat → Nat → Nat

postulate t : T

f : Nat → T
g : Nat → Nat → T

f = g 0            -- eta-expanded to f x ... = g 0 x ...
g m zero    = t
g m (suc n) = f n

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Generalize where

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

infix 4 _≡_

{-# BUILTIN REWRITE _≡_ #-}

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

postulate   Con     :                       Set
postulate   Ty      : (Γ : Con) →           Set
postulate   Tms     : (Γ Δ : Con) →         Set
postulate   Tm      : (Γ : Con)(A : Ty Γ) → Set

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

variable    {Γ Δ Θ} :              Con
postulate   •       :              Con       -- • is \bub
postulate   _▹_     : ∀ Γ → Ty Γ → Con       -- ▹ is \tw2
infixl 5    _▹_

variable    {A B C} :                  Ty _
postulate   _∘ᵀ_    : Ty Δ → Tms Γ Δ → Ty Γ
infixl 6    _∘ᵀ_

variable    {σ δ ν} :                                 Tms _ _
postulate   _∘_     : Tms Θ Δ → Tms Γ Θ →             Tms Γ Δ
infixr 7    _∘_
postulate   id      :                                 Tms Γ Γ
postulate   ε       :                                 Tms Γ •
postulate   _,_     : (σ : Tms Γ Δ) → Tm Γ (A ∘ᵀ σ) → Tms Γ (Δ ▹ A)
infixl 5    _,_
postulate   π₁      : Tms Γ (Δ ▹ A) →                 Tms Γ Δ

variable    {t u v} :                          Tm _ _
postulate   π₂      : (σ : Tms Γ (Δ ▹ A)) →    Tm Γ (A ∘ᵀ π₁ σ)
postulate   _∘ᵗ_    : Tm Δ A → (σ : Tms Γ Δ) → Tm Γ (A ∘ᵀ σ)
infixl 6    _∘ᵗ_

postulate   ass     :   (σ ∘ δ) ∘ ν ≡ σ ∘ δ ∘ ν
{-# REWRITE ass #-}
postulate   idl     :        id ∘ δ ≡ δ
{-# REWRITE idl #-}
postulate   idr     :        δ ∘ id ≡ δ
{-# REWRITE idr #-}
postulate   εη      :             δ ≡ ε  -- can't rewrite, so we specialize this in the next two cases
postulate   εηid    :            id ≡ ε
{-# REWRITE εηid #-}
postulate   εη∘     :         ε ∘ δ ≡ ε
{-# REWRITE εη∘ #-}
postulate   ,β₁     :    π₁ (δ , t) ≡ δ
{-# REWRITE ,β₁ #-}
postulate   ,β₂     :    π₂ (δ , t) ≡ t
{-# REWRITE ,β₂ #-}
postulate   ,η      : (π₁ δ , π₂ δ) ≡ δ
{-# REWRITE ,η #-}
postulate   [id]ᵀ   :       A ∘ᵀ id ≡ A
{-# REWRITE [id]ᵀ #-}
postulate   [∘]ᵀ    :   A ∘ᵀ δ ∘ᵀ σ ≡ A ∘ᵀ δ ∘ σ
{-# REWRITE [∘]ᵀ #-}
postulate   ,∘      :   (δ , t) ∘ σ ≡ δ ∘ σ , t ∘ᵗ σ
{-# REWRITE ,∘ #-}

postulate   [∘]ᵗ    :   t ∘ᵗ σ ∘ᵗ δ ≡ t ∘ᵗ σ ∘ δ
{-# REWRITE [∘]ᵗ #-}
postulate   π₁∘     :      π₁ δ ∘ σ ≡ π₁ (δ ∘ σ)
{-# REWRITE π₁∘ #-}
postulate   π₂∘     :     π₂ δ ∘ᵗ σ ≡ π₂ (δ ∘ σ)
{-# REWRITE π₂∘ #-}
postulate   ∘id     :       t ∘ᵗ id ≡ t
{-# REWRITE ∘id #-}

_↑_ : ∀ σ A → Tms (Γ ▹ A ∘ᵀ σ) (Δ ▹ A)
σ ↑ A = σ ∘ π₁ id , π₂ id

⟨_⟩ : Tm Γ A → Tms Γ (Γ ▹ A)
⟨ t ⟩ = id , t

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

postulate   U       : Ty Γ
variable    {a b c} : Tm _ U
postulate   El      : Tm Γ U → Ty Γ
postulate   U[]     : U ∘ᵀ σ ≡ U
{-# REWRITE U[] #-}
postulate   El[]    : El a ∘ᵀ σ ≡ El (a ∘ᵗ σ)
{-# REWRITE El[] #-}

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

postulate   Π       : (a : Tm Γ U) → Ty (Γ ▹ El a) → Ty Γ
postulate   Π[]     : Π a B ∘ᵀ σ ≡ Π (a ∘ᵗ σ) (B ∘ᵀ σ ↑ El a)
{-# REWRITE Π[] #-}
postulate   app     : Tm Γ (Π a B) → Tm (Γ ▹ El a) B
postulate   app[]   : app t ∘ᵗ (σ ↑ El a) ≡ app (t ∘ᵗ σ)
{-# REWRITE app[] #-}


text:
-- Andreas, 2020-05-18, issue #3933
--
-- Duplicate imports of the same modules should be cumulative,
-- rather than overwriting the previous scope.

{-# OPTIONS -v scope.import:10 #-}
{-# OPTIONS -v scope:clash:20 #-}

open import Agda.Builtin.Nat using ()

Nat  = Agda.Builtin.Nat.Nat
zero = Agda.Builtin.Nat.zero

import Agda.Builtin.Nat using ()

works : Nat
works = zero

test : Agda.Builtin.Nat.Nat
test = Agda.Builtin.Nat.zero

-- Used to fail since the second import emptied
-- the contents of module Agda.Builtin.Nat.

max_forks_repo_name: shlevy/agda


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Category.Setoids.Facts where

open import Cats.Category.Setoids.Facts.Exponential public using
  (hasExponentials)
open import Cats.Category.Setoids.Facts.Initial public using
  (hasInitial)
open import Cats.Category.Setoids.Facts.Limit public using
  (complete)
open import Cats.Category.Setoids.Facts.Product public using
  (hasProducts ; hasBinaryProducts ; hasFiniteProducts)
open import Cats.Category.Setoids.Facts.Terminal public using
  (hasTerminal)

open import Cats.Category
open import Cats.Category.Setoids using (Setoids)

instance
  isCCC : ∀ {l} → IsCCC (Setoids l l)
  isCCC = record {}

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use Data.List.Relation.Unary.Any
-- directly.
------------------------------------------------------------------------

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

module Data.List.Any where

open import Data.List.Relation.Unary.Any public

{-# WARNING_ON_IMPORT
"Data.List.Any was deprecated in v1.0.
Use Data.List.Relation.Unary.Any instead."
#-}


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

   Copyright (c) 2020, 2021, 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 Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Lemmas
open import LibraBFT.Hash
open import LibraBFT.Base.Types
open import LibraBFT.Base.Encode
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.PKCS
open import LibraBFT.Impl.Base.Types
open import LibraBFT.Impl.Consensus.Types.EpochIndep
open import LibraBFT.Impl.Util.Crypto

-- This module defines the types of messages that the implementation
-- can send, along with properties defining ways in which votes can be
-- represented in them, some useful functions, and definitions of how
-- NetworkMsgs are signed.

module LibraBFT.Impl.NetworkMsg where
  data NetworkMsg : Set where
    P : ProposalMsg → NetworkMsg
    V : VoteMsg     → NetworkMsg
    C : CommitMsg   → NetworkMsg

  P≢V : ∀ {p v} → P p ≢ V v
  P≢V ()

  C≢V : ∀ {c v} → C c ≢ V v
  C≢V ()

  V-inj : ∀ {vm1 vm2} → V vm1 ≡ V vm2 → vm1 ≡ vm2
  V-inj refl = refl

  data _QC∈SyncInfo_ (qc : QuorumCert) (si : SyncInfo) : Set where
     withVoteSIHighQC : si ^∙ siHighestQuorumCert  ≡ qc   → qc QC∈SyncInfo si
     -- Note that we do not use the Lens here, because the Lens returns the siHighestQuorumcert in
     -- case siHighestCommitcert is nothing, and it was easier to directly handle the just case.  We
     -- could use the Lens, and fix the proofs, but it seems simpler this way.
     withVoteSIHighCC : ₋siHighestCommitCert si ≡ just qc → qc QC∈SyncInfo si

  data _QC∈ProposalMsg_ (qc : QuorumCert) (pm : ProposalMsg) : Set where
     inProposal       : pm ^∙ pmProposal ∙ bBlockData ∙ bdQuorumCert ≡ qc → qc QC∈ProposalMsg pm
     inPMSyncInfo     : qc QC∈SyncInfo (pm ^∙ pmSyncInfo)                 → qc QC∈ProposalMsg pm

  data _QC∈CommitMsg_ (qc : QuorumCert) (cm : CommitMsg) : Set where
     withCommitMsg    : cm ^∙ cmCert ≡ qc                                 → qc QC∈CommitMsg cm

  data _QC∈NM_ (qc : QuorumCert) : NetworkMsg → Set where
    inP : ∀ {pm} → qc QC∈ProposalMsg pm                 → qc QC∈NM (P pm)
    inV : ∀ {vm} → qc QC∈SyncInfo    (vm ^∙ vmSyncInfo) → qc QC∈NM (V vm)
    inC : ∀ {cm} → qc QC∈CommitMsg   cm                 → qc QC∈NM (C cm)

  data _⊂Msg_ (v : Vote) : NetworkMsg → Set where
    vote∈vm : ∀ {si}
            → v ⊂Msg (V (VoteMsg∙new v si))
    vote∈qc : ∀ {vs} {qc : QuorumCert} {nm}
            → vs ∈ qcVotes qc
            → rebuildVote qc vs ≈Vote v
            → qc QC∈NM nm
            → v ⊂Msg nm

  getEpoch : NetworkMsg → Epoch
  getEpoch (P p) = p ^∙ pmProposal ∙ bBlockData ∙ bdEpoch
  getEpoch (V (VoteMsg∙new v _)) = v ^∙ vEpoch
  getEpoch (C c) = c ^∙ cmEpoch

  -- Get the message's author, if it has one.  Note that ProposalMsgs don't necessarily have
  -- authors; we care about the (honesty of) the author only for Proposals, not NilBlocks and
  -- Genesis.
  getAuthor : NetworkMsg → Maybe NodeId
  getAuthor (P p)
     with p ^∙ pmProposal ∙ bBlockData ∙ bdBlockType
  ...| Proposal _ auth = just auth
  ...| NilBlock        = nothing
  ...| Genesis         = nothing
  getAuthor (V v) = just (v ^∙ vmVote ∙ vAuthor)
  getAuthor (C c) = just (c ^∙ cmAuthor)

  -----------------------------------------------------------------------
  -- Proof that network records are signable and may carry a signature --
  -----------------------------------------------------------------------

  Signed-pi-CommitMsg : (cm : CommitMsg)
                      → (is1 is2 : (Is-just ∘ ₋cmSigMB) cm)
                      → is1 ≡ is2
  Signed-pi-CommitMsg (CommitMsg∙new _ _ _ _ .(just _)) (just _) (just _) = cong just refl

  instance
   -- A proposal message might carry a signature inside the block it
   -- is proposing.
   sig-ProposalMsg : WithSig ProposalMsg
   sig-ProposalMsg = record
      { Signed         = Signed         ∘ ₋pmProposal
      ; Signed-pi      = Signed-pi-Blk  ∘ ₋pmProposal
      ; isSigned?      = isSigned?      ∘ ₋pmProposal
      ; signature      = signature      ∘ ₋pmProposal
      ; signableFields = signableFields ∘ ₋pmProposal
      }

   sig-VoteMsg : WithSig VoteMsg
   sig-VoteMsg = record
      { Signed         = Signed         ∘ ₋vmVote
      ; Signed-pi      = λ _ _ _ → Unit-pi
      ; isSigned?      = isSigned?      ∘ ₋vmVote
      ; signature      = signature      ∘ ₋vmVote
      ; signableFields = signableFields ∘ ₋vmVote
      }

   sig-CommitMsg : WithSig CommitMsg
   sig-CommitMsg = record
      { Signed         = Is-just ∘ ₋cmSigMB
      ; Signed-pi      = Signed-pi-CommitMsg
      ; isSigned?      = λ cm → Maybe-Any-dec (λ _ → yes tt) (cm ^∙ cmSigMB)
      ; signature      = λ { _ prf → to-witness prf }
      ; signableFields = λ cm → concat ( encode  (cm ^∙ cmEpoch)
                                       ∷ encode  (cm ^∙ cmAuthor)
                                       ∷ encode  (cm ^∙ cmRound)
                                       ∷ encode  (cm ^∙ cmCert)
                                       ∷ [])
      }

  ---------------------------------------------------------
  -- Network Records whose signatures have been verified --
  ---------------------------------------------------------

  -- First we have to have some boilerplate to pattern match
  -- on the type of message to access the 'WithSig' instance
  -- on the fields... a bit ugly, but there's no other way, really.
  -- At least we quarantine them in a private block.
  private
    SignedNM : NetworkMsg → Set
    SignedNM (P x) = Signed x
    SignedNM (V x) = Signed x
    SignedNM (C x) = Signed x

    SignedNM-pi : ∀ (nm : NetworkMsg) → (is1 : SignedNM nm) → (is2 : SignedNM nm) → is1 ≡ is2
    SignedNM-pi (P x) = Signed-pi x
    SignedNM-pi (V x) = Signed-pi x
    SignedNM-pi (C x) = Signed-pi x

    isSignedNM? : (nm : NetworkMsg) → Dec (SignedNM nm)
    isSignedNM? (P x) = isSigned? x
    isSignedNM? (V x) = isSigned? x
    isSignedNM? (C x) = isSigned? x

    signatureNM  : (nm : NetworkMsg) → SignedNM nm → Signature
    signatureNM (P x) prf = signature x prf
    signatureNM (V x) prf = signature x prf
    signatureNM (C x) prf = signature x prf

    signableFieldsNM : NetworkMsg → ByteString
    signableFieldsNM (P x) = signableFields x
    signableFieldsNM (V x) = signableFields x
    signableFieldsNM (C x) = signableFields x

  instance
    sig-NetworkMsg : WithSig NetworkMsg
    sig-NetworkMsg = record
      { Signed         = SignedNM
      ; Signed-pi      = SignedNM-pi
      ; isSigned?      = isSignedNM?
      ; signature      = signatureNM
      ; signableFields = signableFieldsNM
      }

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module Oscar.Data.Fin where

open import Data.Fin public using (Fin; zero; suc)

-- open import Oscar.Data.Fin.Core public

-- --open import Data.Fin hiding (thin; thick; check) public
-- --open import Data.Fin.Properties hiding (thin-injective; thick-thin; thin-check-id) public

-- -- module _ where

-- --   open import Data.Product
-- --   open import Oscar.Data.Vec
-- --   open import Data.Nat
-- --   open import Function

-- --   enumFin⋆ : ∀ n → ∃ λ (F : Vec (Fin n) n) → ∀ f → f ∈ F
-- --   enumFin⋆ n = tabulate⋆ id

-- -- open import Agda.Builtin.Equality
-- -- open import Agda.Builtin.Nat
-- -- open import Relation.Binary.PropositionalEquality
-- -- open import Relation.Nullary
-- -- open import Data.Product
-- -- open import Data.Empty
-- -- open import Function

-- -- previous : ∀ {n} -> Fin (suc (suc n)) -> Fin (suc n)
-- -- previous (suc x) = x
-- -- previous zero = zero

-- -- module Thin where
-- --   fact1 : ∀ {n} x y z -> thin {n} x y ≡ thin x z -> y ≡ z
-- --   fact1 zero y .y refl = refl
-- --   fact1 (suc x) zero zero r = refl
-- --   fact1 (suc x) zero (suc z) ()
-- --   fact1 (suc x) (suc y) zero ()
-- --   fact1 (suc x) (suc y) (suc z) r = cong suc (fact1 x y z (cong previous r))

-- --   fact2 : ∀ {n} x y -> ¬ thin {n} x y ≡ x
-- --   fact2 zero y ()
-- --   fact2 (suc x) zero ()
-- --   fact2 (suc x) (suc y) r = fact2 x y (cong previous r)

-- --   fact3 : ∀{n} x y -> ¬ x ≡ y -> ∃ λ y' -> thin {n} x y' ≡ y
-- --   fact3 zero zero ne = ⊥-elim (ne refl)
-- --   fact3 zero (suc y) _ = y , refl
-- --   fact3 {zero} (suc ()) _ _
-- --   fact3 {suc n} (suc x) zero ne = zero , refl
-- --   fact3 {suc n} (suc x) (suc y) ne with y | fact3 x y (ne ∘ cong suc)
-- --   ... | .(thin x y') | y' , refl = suc y' , refl

-- -- open import Data.Maybe
-- -- open import Category.Functor
-- -- open import Category.Monad
-- -- import Level
-- -- open RawMonad (Data.Maybe.monad {Level.zero})

-- -- open import Data.Sum

-- -- _≡Fin_ : ∀ {n} -> (x y : Fin n) -> Dec (x ≡ y)
-- -- zero ≡Fin zero = yes refl
-- -- zero ≡Fin suc y = no λ ()
-- -- suc x ≡Fin zero = no λ ()
-- -- suc {suc _} x ≡Fin suc y with x ≡Fin y
-- -- ...              | yes r = yes (cong suc r)
-- -- ...              | no r = no λ e -> r (cong previous e)
-- -- suc {zero} () ≡Fin _

-- -- module Thick where
-- --   half1 : ∀ {n} (x : Fin (suc n)) -> check x x ≡ nothing
-- --   half1 zero = refl
-- --   half1 {suc _} (suc x) = cong ((_<$>_ suc)) (half1 x)
-- --   half1 {zero} (suc ())

-- --   half2 : ∀ {n} (x : Fin (suc n)) y -> ∀ y' -> thin x y' ≡ y -> check x y ≡ just y'
-- --   half2 zero zero y' ()
-- --   half2 zero (suc y) .y refl = refl
-- --   half2 {suc n} (suc x) zero zero refl = refl
-- --   half2 {suc _} (suc _) zero (suc _) ()
-- --   half2 {suc n} (suc x) (suc y) zero ()
-- --   half2 {suc n} (suc x) (suc .(thin x y')) (suc y') refl with check x (thin x y') | half2 x (thin x y') y' refl
-- --   ...                                                       | .(just y')          | refl = refl
-- --   half2 {zero} (suc ()) _ _ _

-- --   fact1 : ∀ {n} (x : Fin (suc n)) y r
-- --     -> check x y ≡ r
-- --     -> x ≡ y × r ≡ nothing ⊎ ∃ λ y' -> thin x y' ≡ y × r ≡ just y'
-- --   fact1 x y .(check x y) refl with x ≡Fin y
-- --   fact1 x .x ._ refl | yes refl = inj₁ (refl , half1 x)
-- --   ... | no el with Thin.fact3 x y el
-- --   ...            | y' , thinxy'=y = inj₂ (y' , ( thinxy'=y , half2 x y y' thinxy'=y ))


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

open import lib.Base
open import lib.PathGroupoid

{-
This file contains various basic definitions and lemmas about functions
(non-dependent [Pi] types) that do not belong anywhere else.
-}

module lib.Function where

{- Basic lemmas about pointed maps -}

-- concatenation
⊙∘-pt : ∀ {i j} {A : Type i} {B : Type j}
  {a₁ a₂ : A} (f : A → B) {b : B}
  → a₁ == a₂ → f a₂ == b → f a₁ == b
⊙∘-pt f p q = ap f p ∙ q

infixr 80 _⊙∘_
_⊙∘_ : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  (g : Y ⊙→ Z) (f : X ⊙→ Y) → X ⊙→ Z
(g , gpt) ⊙∘ (f , fpt) = (g ∘ f) , ⊙∘-pt g fpt gpt

⊙∘-unit-l : ∀ {i j} {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
  → ⊙idf Y ⊙∘ f == f
⊙∘-unit-l (f , idp) = idp

⊙∘-unit-r : ∀ {i j} {X : Ptd i} {Y : Ptd j} (f : X ⊙→ Y)
  → f ⊙∘ ⊙idf X == f
⊙∘-unit-r f = idp

{- Homotopy fibers -}

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

  hfiber : (y : B) → Type (lmax i j)
  hfiber y = Σ A (λ x → f x == y)

  {- Note that [is-inj] is not a mere proposition. -}
  is-inj : Type (lmax i j)
  is-inj = (a₁ a₂ : A) → f a₁ == f a₂ → a₁ == a₂

  preserves-≠ : Type (lmax i j)
  preserves-≠ = {a₁ a₂ : A} → a₁ ≠ a₂ → f a₁ ≠ f a₂

module _ {i j} {A : Type i} {B : Type j} {f : A → B} where
  abstract
    inj-preserves-≠ : is-inj f → preserves-≠ f
    inj-preserves-≠ inj ¬p q = ¬p (inj _ _ q)

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

  ∘-is-inj : is-inj g → is-inj f → is-inj (g ∘ f)
  ∘-is-inj g-is-inj f-is-inj a₁ a₂ = f-is-inj a₁ a₂ ∘ g-is-inj (f a₁) (f a₂)

{- Maps between two functions -}

record CommSquare {i₀ i₁ j₀ j₁}
  {A₀ : Type i₀} {A₁ : Type i₁} {B₀ : Type j₀} {B₁ : Type j₁}
  (f₀ : A₀ → B₀) (f₁ : A₁ → B₁) (hA : A₀ → A₁) (hB : B₀ → B₁)
  : Type (lmax (lmax i₀ i₁) (lmax j₀ j₁)) where
  constructor comm-sqr
  field
    commutes : ∀ a₀ → (hB ∘ f₀) a₀ == (f₁ ∘ hA) a₀

open CommSquare public

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import lib.Basics
open import lib.types.Bool

module Graphs.Definition where

{- A graph consists of types of Edges and Vertices together with two endpoint maps. We
   often just talk about the types and the endpoint maps are clear from the context
   (i.e. derived by instance resolution). -}
record Graph {i j : ULevel} (E : Type i) (V : Type j) : Type (lmax i j) where
  constructor graph
  field
    π₀ : E → V
    π₁ : E → V

open Graph ⦃...⦄ public -- see agda documentation on instance arguments

max_stars_repo_name: awswan/nielsenschreier-hott

max_issues_repo_name: awswan/nielsenschreier-hott

max_forks_repo_name: awswan/nielsenschreier-hott


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

module Algebra.Construct.Free.Semilattice.Relation.Unary.All.Def where

open import Prelude hiding (⊥; ⊤)
open import Algebra.Construct.Free.Semilattice.Eliminators
open import Algebra.Construct.Free.Semilattice.Definition
open import Cubical.Foundations.HLevels
open import Data.Empty.UniversePolymorphic
open import HITs.PropositionalTruncation.Sugar
open import HITs.PropositionalTruncation.Properties
open import HITs.PropositionalTruncation
open import Data.Unit.UniversePolymorphic

private
  variable p : Level

dup-◻ : (P : A → Type p) → (x : A) (xs : Type p) → (∥ P x ∥ × ∥ P x ∥ × xs) ⇔ (∥ P x ∥ × xs)
dup-◻ P _ _ .fun = snd
dup-◻ P _ _ .inv (x , xs) = x , x , xs
dup-◻ P _ _ .rightInv (x , xs) = refl
dup-◻ P _ _ .leftInv  (x₁ , x₂ , xs) i .fst = squash x₂ x₁ i
dup-◻ P _ _ .leftInv  (x₁ , x₂ , xs) i .snd = (x₂ , xs)

com-◻ : (P : A → Type p) → (x y : A) (xs : Type p) → (∥ P x ∥ × ∥ P y ∥ × xs) ⇔ (∥ P y ∥ × ∥ P x ∥ × xs)
com-◻ P _ _ _ .fun (x , y , xs) = y , x , xs
com-◻ P _ _ _ .inv (y , x , xs) = x , y , xs
com-◻ P _ _ _ .leftInv  (x , y , xs) = refl
com-◻ P _ _ _ .rightInv (x , y , xs) = refl

◻′ : (P : A → Type p) → A ↘ hProp p
[ ◻′ P ]-set = isSetHProp
([ ◻′ P ] x ∷ (xs , hxs)) .fst = ∥ P x ∥ × xs
([ ◻′ P ] x ∷ (xs , hxs)) .snd y z = ΣProp≡ (λ _  → hxs) (squash (fst y) (fst z))
[ ◻′ P ][] = ⊤ , λ x y _ → x
[ ◻′ P ]-dup x xs = ΣProp≡ (λ _ → isPropIsProp) (isoToPath (dup-◻ P x (xs .fst)))
[ ◻′ P ]-com x y xs = ΣProp≡ (λ _ → isPropIsProp) (isoToPath (com-◻ P x y (xs .fst)))

◻ : (P : A → Type p) → 𝒦 A → Type p
◻ P xs = [ ◻′ P ]↓ xs .fst

isProp-◻ : ∀ {P : A → Type p} {xs} → isProp (◻ P xs)
isProp-◻ {P = P} {xs = xs} = [ ◻′ P ]↓ xs .snd

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

open import Categories.Category

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

open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Categories.Category.Cartesian
open import Categories.Category.Cocartesian
open import Categories.Category.Complete
open import Categories.Category.Complete.Finitely
open import Categories.Category.Cocomplete
open import Categories.Category.Cocomplete.Finitely

open import Categories.Object.Duality
open import Categories.Diagram.Duality
open import Categories.Functor

private
  module C = Category C
  open C

coCartesian⇒Cocartesian : Cartesian C.op → Cocartesian C
coCartesian⇒Cocartesian Car = record
  { initial     = op⊤⇒⊥ C terminal
  ; coproducts  = record
    { coproduct = coProduct⇒Coproduct C product
    }
  }
  where open Cartesian Car

Cocartesian⇒coCartesian : Cocartesian C → Cartesian C.op
Cocartesian⇒coCartesian Co = record
  { terminal  = ⊥⇒op⊤ C initial
  ; products  = record
    { product = Coproduct⇒coProduct C coproduct
    }
  }
  where open Cocartesian Co

coComplete⇒Cocomplete : ∀ {o′ ℓ′ e′} → Complete o′ ℓ′ e′ C.op → Cocomplete o′ ℓ′ e′ C
coComplete⇒Cocomplete Com F = coLimit⇒Colimit C (Com F.op)
  where module F = Functor F

Cocomplete⇒coComplete : ∀ {o′ ℓ′ e′} → Cocomplete o′ ℓ′ e′ C → Complete o′ ℓ′ e′ C.op
Cocomplete⇒coComplete Coc F = Colimit⇒coLimit C (Coc F.op)
  where module F = Functor F

coFinitelyComplete⇒FinitelyCocomplete : FinitelyComplete C.op → FinitelyCocomplete C
coFinitelyComplete⇒FinitelyCocomplete FC = record
  { cocartesian = coCartesian⇒Cocartesian cartesian
  ; coequalizer = λ f g → coEqualizer⇒Coequalizer C (equalizer f g)
  }
  where open FinitelyComplete FC

FinitelyCocomplete⇒coFinitelyComplete : FinitelyCocomplete C → FinitelyComplete C.op
FinitelyCocomplete⇒coFinitelyComplete FC = record
  { cartesian = Cocartesian⇒coCartesian cocartesian
  ; equalizer = λ f g → Coequalizer⇒coEqualizer C (coequalizer f g)
  }
  where open FinitelyCocomplete FC

module DualityConversionProperties where

  private
    op-involutive : Category.op C.op ≡ C
    op-involutive = refl

    coCartesian⇔Cocartesian : ∀(coCartesian : Cartesian C.op)
                            → Cocartesian⇒coCartesian (coCartesian⇒Cocartesian coCartesian)
                              ≡ coCartesian
    coCartesian⇔Cocartesian _ = refl

    coFinitelyComplete⇔FinitelyCocomplete : ∀(coFinComplete : FinitelyComplete C.op) →
      FinitelyCocomplete⇒coFinitelyComplete
        (coFinitelyComplete⇒FinitelyCocomplete coFinComplete) ≡ coFinComplete
    coFinitelyComplete⇔FinitelyCocomplete _ = refl

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Nat

pred : Nat → Nat
pred (suc n) = n
pred zero = zero

data [0-1] : Set where
  𝟎 𝟏 : [0-1]
  int : 𝟎 ≡ 𝟏

-- The following holes can be filled, so they should not cause a
-- typechecking failure.

0=x : ∀ i → 𝟎 ≡ int i
0=x i = \ j → int {!!}

si : {n m : Nat} → suc n ≡ suc m → n ≡ m
si p i = pred (p {!!})

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- This test case seems to be due to Andreas Abel, Andrea Vezzosi and
-- NAD. The code below should be rejected.

open import Agda.Builtin.Size

data SizeLt (i : Size) : Set where
  size : (j : Size< i) → SizeLt i

-- Legal again in 2.5.1
getSize : ∀{i} → SizeLt i → Size
getSize (size j) = j

-- Structurally inductive (c), coinductive via sizes.
data U (i : Size) : Set where
  c : ((s : SizeLt i) → U (getSize s)) → U i

data ⊥ : Set where

empty : U ∞ → ⊥
empty (c f) = empty (f (size ∞))  -- f x <= f < c f

-- If U is a data type this should not be possible:
inh : ∀ i → U i
inh i = c λ{ (size j) → inh j }

absurd : ⊥
absurd = empty (inh ∞)


text:
module hello-world where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.String using (String)

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}

main : IO ⊤
main = putStrLn "Hello world!"


text:
module Bush where

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

{-# BUILTIN NATURAL Nat #-}

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

_^_ : (Set -> Set) -> Nat -> Set -> Set
(F ^ zero)  A = A
(F ^ suc n) A = F ((F ^ n) A)

data Bush (A : Set) : Set where
  leaf : Bush A
  node : A -> (Bush ^ 3) A -> Bush A

elim :
  (P : (A : Set) -> Bush A -> Set) ->
  ((A : Set) -> P A leaf) ->
  ((A : Set)(x : A)(b : (Bush ^ 3) A) ->
    P ((Bush ^ 2) A) b -> P A (node x b)) ->
  (A : Set)(b : Bush A) -> P A b
elim P l n A leaf       = l A
elim P l n A (node x b) = n A x b (elim P l n ((Bush ^ 2) A) b)

iter :
  (P : (A : Set) -> Set) ->
  ((A : Set) -> P A) ->
  ((A : Set) -> A -> P ((Bush ^ 2) A) -> P A) ->
  (A : Set) -> Bush A -> P A
iter P l n A leaf       = l A
iter P l n A (node x b) = n A x (iter P l n ((Bush ^ 2) A) b)

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

_++_ : {A : Set} -> List A -> List A -> List A
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

flatten : {A : Set}(n : Nat) -> (Bush ^ n) A -> List A
flatten zero    x          = x :: []
flatten (suc n) leaf       = []
flatten (suc n) (node x b) = flatten n x ++ flatten (3 + n) b

-- Andreas, 2017-01-01, issue #1899.
-- Normalize field types for positivity checking.
record B (A : Set) : Set where
  coinductive
  field f : (B ^ 3) A


text:
module nodcap.NF.Contract where

open import Function using (_$_)
open import Data.Nat as ℕ using (ℕ; suc; zero)
open import Data.Pos as ℕ⁺
open import Data.List as L using (List; []; _∷_; _++_)
open import Data.Environment
open import nodcap.Base
open import nodcap.NF.Typing

-- Lemma:
--   We can contract n repetitions of A to an instance of ?[ n ] A,
--   by induction on n.
contract : {Γ : Environment} {A : Type} {n : ℕ⁺} →

  ⊢ⁿᶠ replicate⁺ n A ++ Γ →
  ----------------------
  ⊢ⁿᶠ ?[ n ] A ∷ Γ

contract {n = suc zero}    x
  = mk?₁ x
contract {n = suc (suc n)} x
  = cont {m = suc zero}
  $ exch (fwd [] (_ ∷ []))
  $ contract
  $ exch (bwd [] (replicate⁺ (suc n) _))
  $ mk?₁ x