text:
-- The type checker was a little too eager to prune metavariables in
-- order to get the occurs check to pass. In this particular case it
-- got the constraint
--   _41 A B x == B (_42 A B (x , y))
-- and tried to make it work by pruning the third argument to _42. The
-- correct solution _42 A B p := fst p was thus lost.
module Issue458 where

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

uncurry : {A : Set} {B : A → Set} {P : Σ A B → Set} →
          ((x : A) (y : B x) → P (x , y)) →
          (p : Σ A B) → P p
uncurry f (x , y) = f x y

fst : {A : Set} {B : A → Set} → Σ A B → A
fst = uncurry λ x y → x

snd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p)
snd = uncurry λ x y → y

-- Bug.agda:15,7-24
-- Cannot instantiate the metavariable _50 to .B x since it contains
-- the variable x which is not in scope of the metavariable
-- when checking that the expression uncurry (λ x y → y) has type
-- (p : Σ .A .B) → .B (fst p)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The state monad
------------------------------------------------------------------------

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

module Category.Monad.State where

open import Category.Applicative.Indexed
open import Category.Monad
open import Function.Identity.Categorical as Id using (Identity)
open import Category.Monad.Indexed
open import Data.Product
open import Data.Unit
open import Function
open import Level

------------------------------------------------------------------------
-- Indexed state

IStateT : ∀ {i f} {I : Set i} → (I → Set f) → (Set f → Set f) → IFun I f
IStateT S M i j A = S i → M (A × S j)

------------------------------------------------------------------------
-- Indexed state applicative

StateTIApplicative : ∀ {i f} {I : Set i} (S : I → Set f) {M} →
                     RawMonad M → RawIApplicative (IStateT S M)
StateTIApplicative S Mon = record
  { pure = λ a s → return (a , s)
  ; _⊛_  = λ f t s → do
     (f′ , s′)  ← f s
     (t′ , s′′) ← t s′
     return (f′ t′ , s′′)
  } where open RawMonad Mon

StateTIApplicativeZero : ∀ {i f} {I : Set i} (S : I → Set f) {M} →
                         RawMonadZero M → RawIApplicativeZero (IStateT S M)
StateTIApplicativeZero S Mon = record
  { applicative = StateTIApplicative S monad
  ; ∅           = const ∅
  } where open RawMonadZero Mon

StateTIAlternative : ∀ {i f} {I : Set i} (S : I → Set f) {M} →
                     RawMonadPlus M → RawIAlternative (IStateT S M)
StateTIAlternative S Mon = record
  { applicativeZero = StateTIApplicativeZero S monadZero
  ; _∣_             = λ m n s → m s ∣ n s
  } where open RawMonadPlus Mon

------------------------------------------------------------------------
-- Indexed state monad

StateTIMonad : ∀ {i f} {I : Set i} (S : I → Set f) {M} →
               RawMonad M → RawIMonad (IStateT S M)
StateTIMonad S Mon = record
  { return = λ x s → return (x , s)
  ; _>>=_  = λ m f s → m s >>= uncurry f
  } where open RawMonad Mon

StateTIMonadZero : ∀ {i f} {I : Set i} (S : I → Set f) {M} →
                   RawMonadZero M → RawIMonadZero (IStateT S M)
StateTIMonadZero S Mon = record
  { monad           = StateTIMonad S (RawMonadZero.monad Mon)
  ; applicativeZero = StateTIApplicativeZero S Mon
  } where open RawMonadZero Mon

StateTIMonadPlus : ∀ {i f} {I : Set i} (S : I → Set f) {M} →
                   RawMonadPlus M → RawIMonadPlus (IStateT S M)
StateTIMonadPlus S Mon = record
  { monad       = StateTIMonad S monad
  ; alternative = StateTIAlternative S Mon
  } where open RawMonadPlus Mon

------------------------------------------------------------------------
-- State monad operations

record RawIMonadState {i f} {I : Set i} (S : I → Set f)
                      (M : IFun I f) : Set (i ⊔ suc f) where
  field
    monad : RawIMonad M
    get   : ∀ {i} → M i i (S i)
    put   : ∀ {i j} → S j → M i j (Lift f ⊤)

  open RawIMonad monad public

  modify : ∀ {i j} → (S i → S j) → M i j (Lift f ⊤)
  modify f = get >>= put ∘ f

StateTIMonadState : ∀ {i f} {I : Set i} (S : I → Set f) {M} →
                    RawMonad M → RawIMonadState S (IStateT S M)
StateTIMonadState S Mon = record
  { monad = StateTIMonad S Mon
  ; get   = λ s   → return (s , s)
  ; put   = λ s _ → return (_ , s)
  }
  where open RawIMonad Mon

------------------------------------------------------------------------
-- Ordinary state monads

RawMonadState : ∀ {f} → Set f → (Set f → Set f) → Set _
RawMonadState S M = RawIMonadState {I = ⊤} (λ _ → S) (λ _ _ → M)

module RawMonadState {f} {S : Set f} {M : Set f → Set f}
                     (Mon : RawMonadState S M) where
  open RawIMonadState Mon public

StateT : ∀ {f} → Set f → (Set f → Set f) → Set f → Set f
StateT S M = IStateT {I = ⊤} (λ _ → S) M _ _

StateTMonad : ∀ {f} (S : Set f) {M} → RawMonad M → RawMonad (StateT S M)
StateTMonad S = StateTIMonad (λ _ → S)

StateTMonadZero : ∀ {f} (S : Set f) {M} →
                  RawMonadZero M → RawMonadZero (StateT S M)
StateTMonadZero S = StateTIMonadZero (λ _ → S)

StateTMonadPlus : ∀ {f} (S : Set f) {M} →
                  RawMonadPlus M → RawMonadPlus (StateT S M)
StateTMonadPlus S = StateTIMonadPlus (λ _ → S)

StateTMonadState : ∀ {f} (S : Set f) {M} →
                   RawMonad M → RawMonadState S (StateT S M)
StateTMonadState S = StateTIMonadState (λ _ → S)

State : ∀ {f} → Set f → Set f → Set f
State S = StateT S Identity

StateMonad : ∀ {f} (S : Set f) → RawMonad (State S)
StateMonad S = StateTMonad S Id.monad

StateMonadState : ∀ {f} (S : Set f) → RawMonadState S (State S)
StateMonadState S = StateTMonadState S Id.monad

LiftMonadState : ∀ {f S₁} (S₂ : Set f) {M} →
                 RawMonadState S₁ M →
                 RawMonadState S₁ (StateT S₂ M)
LiftMonadState S₂ Mon = record
  { monad = StateTIMonad (λ _ → S₂) monad
  ; get   = λ s → get >>= λ x → return (x , s)
  ; put   = λ s′ s → put s′ >> return (_ , s)
  }
  where open RawIMonadState Mon

ext: agda


text:
{-# OPTIONS --without-K --safe #-}
module Experiment.EvenOdd where

open import Data.List
open import Data.List.Relation.Unary.All
open import Data.Product hiding (map)
open import Data.Sum as Sum hiding (map)
open import Data.Nat
open import Data.Nat.GeneralisedArithmetic
import Data.Nat.Properties as ℕₚ
open import Function.Base
open import Relation.Binary.PropositionalEquality

data RoseTree {a} (A : Set a) : Set a where
  node : A → List (RoseTree A) → RoseTree A

unnode : ∀ {a} {A : Set a} → RoseTree A → A × List (RoseTree A)
unnode (node x rs) = x , rs

foldRoseTree : ∀ {a b} {A : Set a} {B : Set b} →
               (A → List B → B) → RoseTree A → B
foldRoseTrees : ∀ {a b} {A : Set a} {B : Set b} →
                (A → List B → B) → List (RoseTree A) → List B
foldRoseTree f (node x rs) = f x (foldRoseTrees f rs)
foldRoseTrees f []       = []
foldRoseTrees f (x ∷ rs) = foldRoseTree f x ∷ foldRoseTrees f rs

mapRoseTree : ∀ {a b} {A : Set a} {B : Set b} →
              (A → B) → RoseTree A → RoseTree B
mapRoseTree f r = foldRoseTree (λ x rs → node (f x) rs) r

data Parity : Set where
  even odd : Parity

data Pos : Set where
  one  : Pos
  node : Parity → Pos → List Pos → Pos

op : Parity → Parity
op even = odd
op odd  = even

induction : ∀ {p} {P : Pos → Set p} →
            P one →
            (∀ pa x xs → P x → All P xs → P (node pa x xs)) →
            ∀ n → P n
induction-node : ∀ {p} {P : Pos → Set p} →
                 P one →
                 (∀ pa x xs → P x → All P xs → P (node pa x xs)) →
                 ∀ ns → All P ns
induction P1 Pn one            = P1
induction P1 Pn (node pa n ns) = Pn pa n ns (induction P1 Pn n) (induction-node P1 Pn ns)
induction-node P1 Pn []       = []
induction-node P1 Pn (x ∷ ns) = induction P1 Pn x ∷ induction-node P1 Pn ns

recursion : ∀ {a} {A : Set a} → A → (Parity → A → List A → A) → Pos → A
recursion o n p = induction o (λ pa _ _ x AllAxs → n pa x (reduce id AllAxs)) p

ℕ⁺ : Set
ℕ⁺ = Σ ℕ (λ n → n ≢ 0)

1ℕ⁺ : ℕ⁺
1ℕ⁺ = 1 , (λ ())

2ℕ⁺ : ℕ⁺
2ℕ⁺ = 2 , (λ ())

sucℕ⁺ : ℕ⁺ → ℕ⁺
sucℕ⁺ (n , _) = suc n , λ ()

_+ℕ⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺
(m , m≢0) +ℕ⁺ (n , n≢0) = (m + n) , (λ m+n≡0 → m≢0 (ℕₚ.m+n≡0⇒m≡0 m m+n≡0) )

private
  m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0
  m*n≡0⇒m≡0∨n≡0 zero    {zero}  m+n≡0 = inj₁ refl
  m*n≡0⇒m≡0∨n≡0 zero    {suc n} m+n≡0 = inj₁ refl
  m*n≡0⇒m≡0∨n≡0 (suc m) {zero}  m+n≡0 = inj₂ refl

_*ℕ⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺
(m , m≢0) *ℕ⁺ (n , n≢0) =
  (m * n) , λ m*n≡0 → Sum.[ m≢0 , n≢0 ] (m*n≡0⇒m≡0∨n≡0 m m*n≡0)

private
  m^n≡0⇒m≡0 : ∀ m n → m ^ n ≡ 0 → m ≡ 0
  m^n≡0⇒m≡0 zero    (suc n) m^n≡0 = refl
  m^n≡0⇒m≡0 (suc m) (suc n) m^n≡0 with m*n≡0⇒m≡0∨n≡0 (suc m) m^n≡0
  ... | inj₂ sm^n≡0 = m^n≡0⇒m≡0 (suc m) n sm^n≡0

_^ℕ⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺
(m , m≢0) ^ℕ⁺ (n , n≢0) = (m ^ n) , λ m^n≡0 → m≢0 (m^n≡0⇒m≡0 m n m^n≡0)

_⊓ℕ⁺_ : ℕ⁺ → ℕ⁺ → ℕ⁺
(m , m≢0) ⊓ℕ⁺ (n , n≢0) = (m ⊓ n) , {!   !}

oℕ : ℕ → ℕ
oℕ n = 2 * n

iℕ : ℕ → ℕ
iℕ n = 1 + 2 * n

oℕ⁺ : ℕ⁺ → ℕ⁺
oℕ⁺ n = 2ℕ⁺ *ℕ⁺ n

iℕ⁺ : ℕ⁺ → ℕ⁺
iℕ⁺ n = sucℕ⁺ (2ℕ⁺ *ℕ⁺ n)

o^ℕ⁺ : ℕ⁺ → ℕ⁺ → ℕ⁺
o^ℕ⁺ (m , _) x = fold x oℕ⁺ m

i^ℕ⁺ : ℕ⁺ → ℕ⁺ → ℕ⁺
i^ℕ⁺ (m , _) x = fold x iℕ⁺ m

toℕ⁺ : Pos → ℕ⁺
toℕ⁺ = recursion 1ℕ⁺ f
  where
  f : Parity → ℕ⁺ → List ℕ⁺ → ℕ⁺
  f even x []       = o^ℕ⁺ x 1ℕ⁺
  f even x (y ∷ xs) = o^ℕ⁺ x (f odd y xs)
  f odd  x []       = i^ℕ⁺ x 1ℕ⁺
  f odd  x (y ∷ xs) = i^ℕ⁺ x (f even y xs)


text:
module BBHeap.Compound {A : Set}(_≤_ : A → A → Set) where

open import BBHeap _≤_
open import Bound.Lower A
open import Bound.Lower.Order _≤_

data Compound {b : Bound} : BBHeap b → Set where
  cl : {x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x))(l⋘r : l ⋘ r) → Compound (left b≤x l⋘r)
  cr : {x : A}{l r : BBHeap (val x)}(b≤x : LeB b (val x))(l⋙r : l ⋙ r) → Compound (right b≤x l⋙r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Test where

import Data.Bits
import Data.Bool
import Data.Char
import Data.Fin
import Data.Integer
import Data.Interval
import Data.List
import Data.Map
import Data.Maybe
import Data.Nat
import Data.Nat.Properties
import Data.Permutation
import Data.PigeonHole
import Data.Rational
import Data.Real.Base
import Data.Real.CReal
import Data.Real.Complete
import Data.Real.Gauge
import Data.Show
import Data.String
import Data.Tuple
import Data.Vec
import Logic.Base
import Logic.ChainReasoning
import Logic.Congruence
import Logic.Equivalence
import Logic.Identity
import Logic.Leibniz
import Logic.Operations
import Logic.Relations
import Logic.Structure.Applicative
import Logic.Structure.Monoid
import Prelude

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

Please do not move this file. Changes should only be made if
necessary.

This file contains pointers to the code examples and main results from
the paper:

Synthetic Cohomology Theory in Cubical Agda

-}

-- The "--safe" flag ensures that there are no postulates or
-- unfinished goals
{-# OPTIONS --safe #-}
module Cubical.Papers.ZCohomology where

-- Misc.
open import Cubical.Data.Int hiding (_+_)
open import Cubical.Data.Nat
open import Cubical.Foundations.Everything
open import Cubical.HITs.S1
open import Cubical.Data.Sum
open import Cubical.Data.Sigma

-- 2
open import Cubical.Core.Glue                                as Glue
import Cubical.Foundations.Prelude                           as Prelude
import Cubical.Foundations.GroupoidLaws                      as GroupoidLaws
import Cubical.Foundations.Path                              as Path
import Cubical.Foundations.Pointed                           as Pointed
  renaming (Pointed to Type∙)
open import Cubical.HITs.S1                                  as S1
open import Cubical.HITs.Susp                                as Suspension
open import Cubical.HITs.Sn                                  as Sn
open import Cubical.Homotopy.Loopspace                       as Loop
open import Cubical.Foundations.HLevels                      as n-types
open import Cubical.HITs.Truncation                          as Trunc
open import Cubical.Homotopy.Connected                       as Connected
import Cubical.HITs.Pushout                                  as Push
import Cubical.HITs.Wedge                                    as ⋁
import Cubical.Foundations.Univalence                        as Unival
import Cubical.Foundations.SIP                               as StructIdPrinc
import Cubical.Algebra.Group                                 as Gr
import Cubical.Algebra.Group.GroupPath                       as GrPath

-- 3
import Cubical.ZCohomology.Base                              as coHom
  renaming (coHomK to K ; coHomK-ptd to K∙)
import Cubical.HITs.Sn.Properties                            as S
import Cubical.ZCohomology.GroupStructure                    as GroupStructure
import Cubical.ZCohomology.Properties                        as Properties
  renaming (Kn→ΩKn+1 to σ ; ΩKn+1→Kn to σ⁻¹)
import Cubical.Experiments.ZCohomologyOld.Properties as oldCohom

-- 4
import Cubical.ZCohomology.RingStructure.CupProduct          as Cup
import Cubical.ZCohomology.RingStructure.RingLaws            as ⌣Ring
import Cubical.ZCohomology.RingStructure.GradedCommutativity as ⌣Comm
import Cubical.Foundations.Pointed.Homogeneous               as Homogen

-- 5
import Cubical.HITs.Torus                                    as 𝕋²
  renaming (Torus to 𝕋²)
import Cubical.HITs.KleinBottle                              as 𝕂²
  renaming (KleinBottle to 𝕂²)
import Cubical.HITs.RPn                                      as ℝP
  renaming (RP² to ℝP²)
import Cubical.ZCohomology.Groups.Sn                         as HⁿSⁿ
  renaming (Hⁿ-Sᵐ≅0 to Hⁿ-Sᵐ≅1)
import Cubical.ZCohomology.Groups.Torus                      as HⁿT²
import Cubical.ZCohomology.Groups.Wedge                      as Hⁿ-wedge
import Cubical.ZCohomology.Groups.KleinBottle                as Hⁿ𝕂²
import Cubical.ZCohomology.Groups.RP2                        as HⁿℝP²
  renaming (H¹-RP²≅0 to H¹-RP²≅1)
import Cubical.ZCohomology.Groups.CP2                        as HⁿℂP²
  renaming (CP² to ℂP² ; ℤ→HⁿCP²→ℤ to g)
  {- Remark: ℂP² is defined as the pushout S² ← TotalHopf → 1 in
  the formalisation. TotalHopf is just the total space from the Hopf
  fibration. We have TotalHopf ≃ S³, and the map TotalHopf → S²
  is given by taking the first projection. This is equivalent to the
  description given in the paper, since h : S³ → S² is given by
  S³ ≃ TotalHopf → S² -}

-- Appendix
import Cubical.Homotopy.EilenbergSteenrod                    as ES-axioms
import Cubical.ZCohomology.EilenbergSteenrodZ                as satisfies-ES-axioms
  renaming (coHomFunctor to H^~ ; coHomFunctor' to Ĥ)
import Cubical.ZCohomology.MayerVietorisUnreduced            as MayerVietoris

----- 2. HOMOTOPY TYPE THEORY IN CUBICAL AGDA -----

-- 2.1 Important notions in Cubical Agda
open Prelude using ( PathP
                   ; _≡_
                   ; refl
                   ; cong
                   ; cong₂
                   ; funExt)

open GroupoidLaws using (_⁻¹)

open Prelude using ( transport
                   ; subst
                   ; hcomp)

--- 2.2 Important concepts from HoTT/UF in Cubical Agda

-- Pointed Types
open Pointed using (Type∙)

-- The circle, 𝕊¹
open S1 using (S¹)

-- Suspensions
open Suspension using (Susp)

-- (Pointed) n-spheres, 𝕊ⁿ
open Sn using (S₊∙)

-- Loop spaces
open Loop using (Ω^_)

-- Eckmann-Hilton argument
open Loop using (Eckmann-Hilton)

-- n-types Note that we start indexing from 0 in the Cubical Library
-- (so (-2)-types as referred to as 0-types, (-1) as 1-types, and so
-- on)
open n-types using (isOfHLevel)

-- truncations
open Trunc using (hLevelTrunc)

-- elimination principle
open Trunc using (elim)

-- elimination principle for paths
truncPathElim : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (n : ℕ)
              → {B : Path (hLevelTrunc (suc n) A) ∣ x ∣ ∣ y ∣ → Type ℓ'}
              → ((q : _) → isOfHLevel n (B q))
              → ((p : x ≡ y) → B (cong ∣_∣ p))
              → (q : _) → B q
truncPathElim zero hlev ind q = hlev q .fst
truncPathElim (suc n) {B = B} hlev ind q =
  subst B (Iso.leftInv (Trunc.PathIdTruncIso _) q)
    (help (ΩTrunc.encode-fun ∣ _ ∣ ∣ _ ∣ q))
  where
  help : (q : _) → B (ΩTrunc.decode-fun ∣ _ ∣ ∣ _ ∣ q)
  help = Trunc.elim (λ _ → hlev _) ind

-- Connectedness
open Connected using (isConnected)

-- Pushouts
open Push using (Pushout)

-- Wedge sum
open ⋁ using (_⋁_)

-- 2.3 Univalence

-- Univalence and the ua function respectively
open Unival using (univalence ; ua)

-- Glue types
open Glue using (Glue)

-- The structure identity principle and the sip function
-- respectively
open StructIdPrinc using (SIP ; sip)

-- Groups
open Gr using (Group)

-- Isomorphic groups are path equal
open GrPath using (GroupPath)

----- 3. ℤ-COHOMOLOGY IN CUBICAL AGDA -----

-- 3.1 Eilenberg-MacLane spaces

-- Eilenberg-MacLane spaces Kₙ (unpointed and pointed respectively)
open coHom using (K ; K∙)

-- Proposition 7
open S using (sphereConnected)

-- Lemma 8
open S using (wedgeconFun; wedgeconLeft ; wedgeconRight)

-- restated to match the formulation in the paper
wedgeConSn' : ∀ {ℓ} (n m : ℕ) {A : (S₊ (suc n)) → (S₊ (suc m)) → Type ℓ}
            → ((x : S₊ (suc n)) (y : S₊ (suc m)) → isOfHLevel ((suc n) + (suc m)) (A x y))
            → (fₗ : (x : _) → A x (ptSn (suc m)))
            → (fᵣ : (x : _) → A (ptSn (suc n)) x)
            → (p : fₗ (ptSn (suc n)) ≡ fᵣ (ptSn (suc m)))
            → Σ[ F ∈ ((x : S₊ (suc n)) (y : S₊ (suc m)) → A x y) ]
                (Σ[ (left , right) ∈ ((x : S₊ (suc n)) → fₗ x ≡ F x (ptSn (suc m)))
                                   × ((x : S₊ (suc m)) → fᵣ x ≡ F (ptSn (suc n)) x) ]
                  p ≡ left (ptSn (suc n)) ∙ (right (ptSn (suc m))) ⁻¹)
wedgeConSn' zero zero hlev fₗ fᵣ p =
  (wedgeconFun 0 0 hlev fᵣ fₗ p)
   , ((λ x → sym (wedgeconRight 0 0 hlev fᵣ fₗ p x))
   , λ _ → refl) -- right holds by refl
   , rUnit _
wedgeConSn' zero (suc m) hlev fₗ fᵣ p =
  (wedgeconFun 0 (suc m) hlev fᵣ fₗ p)
  , ((λ _ → refl) -- left holds by refl
  , (λ x → sym (wedgeconLeft 0 (suc m) hlev fᵣ fₗ p x)))
  , lUnit _
wedgeConSn' (suc n) m hlev fₗ fᵣ p =
  (wedgeconFun (suc n) m hlev fᵣ fₗ p)
   , ((λ x → sym (wedgeconRight (suc n) m hlev fᵣ fₗ p x))
   , λ _ → refl) -- right holds by refl
   , rUnit _

-- +ₖ (addition) and 0ₖ
open GroupStructure using (_+ₖ_ ; 0ₖ)

-- The function σ : Kₙ → ΩKₙ₊₁
open Properties using (σ)

-- -ₖ (subtraction)
open GroupStructure using (-ₖ_)

-- Group laws for +ₖ
open GroupStructure using ( rUnitₖ ; lUnitₖ
                          ; rCancelₖ ; lCancelₖ
                          ; commₖ
                          ; assocₖ)

-- All group laws are equal to refl at 0ₖ
-- rUnitₖ (definitional)
0-rUnit≡refl : rUnitₖ 0 (0ₖ 0) ≡ refl
1-rUnit≡refl : rUnitₖ 1 (0ₖ 1) ≡ refl
0-rUnit≡refl = refl
1-rUnit≡refl = refl
n≥2-rUnit≡refl : {n : ℕ} → rUnitₖ (2 + n) (0ₖ (2 + n)) ≡ refl
n≥2-rUnit≡refl = refl

-- lUnitₖ (definitional)
0-lUnit≡refl : lUnitₖ 0 (0ₖ 0) ≡ refl
1-lUnit≡refl : lUnitₖ 1 (0ₖ 1) ≡ refl
n≥2-lUnit≡refl : {n : ℕ} → lUnitₖ (2 + n) (0ₖ (2 + n)) ≡ refl
0-lUnit≡refl = refl
1-lUnit≡refl = refl
n≥2-lUnit≡refl = refl

-- assocₖ (definitional)
0-assoc≡refl : assocₖ 0 (0ₖ 0) (0ₖ 0) (0ₖ 0) ≡ refl
1-assoc≡refl : assocₖ 1 (0ₖ 1) (0ₖ 1) (0ₖ 1) ≡ refl
n≥2-assoc≡refl : {n : ℕ} → assocₖ (2 + n) (0ₖ (2 + n)) (0ₖ (2 + n)) (0ₖ (2 + n)) ≡ refl
0-assoc≡refl = refl
1-assoc≡refl = refl
n≥2-assoc≡refl = refl

-- commₖ (≡ refl ∙ refl for n ≥ 2)
0-comm≡refl : commₖ 0 (0ₖ 0) (0ₖ 0) ≡ refl
1-comm≡refl : commₖ 1 (0ₖ 1) (0ₖ 1) ≡ refl
n≥2-comm≡refl : {n : ℕ} → commₖ (2 + n) (0ₖ (2 + n)) (0ₖ (2 + n)) ≡ refl
0-comm≡refl = refl
1-comm≡refl = refl
n≥2-comm≡refl = sym (rUnit refl)

-- lCancelₖ (definitional)
0-lCancel≡refl : lCancelₖ 0 (0ₖ 0) ≡ refl
1-lCancel≡refl : lCancelₖ 1 (0ₖ 1) ≡ refl
n≥2-lCancel≡refl : {n : ℕ} → lCancelₖ (2 + n) (0ₖ (2 + n)) ≡ refl
0-lCancel≡refl = refl
1-lCancel≡refl = refl
n≥2-lCancel≡refl = refl

-- rCancelₖ (≡ (refl ∙ refl) ∙ refl for n ≥ 1)
0-rCancel≡refl : rCancelₖ 0 (0ₖ 0) ≡ refl
1-rCancel≡refl : rCancelₖ 1 (0ₖ 1) ≡ refl
n≥2-rCancel≡refl : {n : ℕ} → rCancelₖ (2 + n) (0ₖ (2 + n)) ≡ refl
0-rCancel≡refl = refl
1-rCancel≡refl = refl
n≥2-rCancel≡refl i = rUnit (rUnit refl (~ i)) (~ i)

-- Proof that there is a unique h-structure on Kₙ
-- +ₖ defines an h-Structure on Kₙ
open GroupStructure using (_+ₖ_ ; 0ₖ ; rUnitₖ ; lUnitₖ ; lUnitₖ≡rUnitₖ)

-- and so does Brunerie's addition
open oldCohom using (_+ₖ_ ; 0ₖ ; rUnitₖ ; lUnitₖ ; rUnitlUnit0)

-- consequently both additions agree
open GroupStructure using (+ₖ-unique)
open oldCohom using (addLemma)
additionsAgree : (n : ℕ) → GroupStructure._+ₖ_ {n = n} ≡ oldCohom._+ₖ_ {n = n}
additionsAgree zero i x y = oldCohom.addLemma x y (~ i)
additionsAgree (suc n) i x y =
  +ₖ-unique n (GroupStructure._+ₖ_) (oldCohom._+ₖ_)
              (GroupStructure.rUnitₖ (suc n)) (GroupStructure.lUnitₖ (suc n))
              (oldCohom.rUnitₖ (suc n)) (oldCohom.lUnitₖ (suc n))
              (sym (lUnitₖ≡rUnitₖ (suc n)))
              (rUnitlUnit0 (suc n)) x y i

-- Theorem 9 (Kₙ ≃ ΩKₙ₊₁)
open Properties using (Kn≃ΩKn+1)

-- σ and σ⁻¹ are morphisms
-- (for σ⁻¹ this is proved directly without using the fact that σ is a morphism)
open Properties using (Kn→ΩKn+1-hom ; ΩKn+1→Kn-hom)

-- Lemma 10 (p ∙ q ≡ cong²₊(p,q)) for n = 1 and n ≥ 2 respectively
open GroupStructure using (∙≡+₁ ; ∙≡+₂)

-- Lemma 11 (cong²₊ is commutative) and Theorem 12 respectively
open GroupStructure using (cong+ₖ-comm ; isCommΩK)

-- 3.2 Group structure on Hⁿ(A)

-- +ₕ (addition), -ₕ and 0ₕ
open GroupStructure using (_+ₕ_ ; -ₕ_ ; 0ₕ)

-- Cohomology group structure
open GroupStructure using ( rUnitₕ ; lUnitₕ
                          ; rCancelₕ ; lCancelₕ
                          ; commₕ
                          ; assocₕ)

-------------------------------------------------------------------- MOVE?
-- Reduced cohomology, group structure
open GroupStructure using (coHomRedGroupDir)

-- Equality of unreduced and reduced cohmology
open Properties using (coHomGroup≡coHomRedGroup)
--------------------------------------------------------------------

----- 4. The Cup Product and Cohomology Ring -----
-- 4.1
-- Lemma 13
open Properties using (isOfHLevel↑∙)

-- ⌣ₖ
open Cup using (_⌣ₖ_)

-- ⌣ₖ is pointed in both arguments
open ⌣Ring using (0ₖ-⌣ₖ ; ⌣ₖ-0ₖ)

-- The cup product
open Cup using (_⌣_)

-- 4.2
-- Lemma 14
Lem14 : ∀ {ℓ} {A : Type∙ ℓ} (n : ℕ) (f g : A →∙ K∙ n) → fst f ≡ fst g → f ≡ g
Lem14 n f g p = Homogen.→∙Homogeneous≡ (Properties.isHomogeneousKn n) p

-- Proposition 15
open ⌣Ring using (leftDistr-⌣ₖ ; rightDistr-⌣ₖ)

-- Lemma 16
open ⌣Ring using (assocer-helpFun≡)

-- Proposition 17
open ⌣Ring using (assoc-⌣ₖ)

-- Proposition 18
open ⌣Comm using (gradedComm-⌣ₖ)

-- Ring structure on ⌣
open ⌣Ring using (leftDistr-⌣ ; rightDistr-⌣
                ; assoc-⌣ ; 1⌣
                ; rUnit⌣ ; lUnit⌣
                ; ⌣0 ; 0⌣)
open ⌣Comm using (gradedComm-⌣)

----- 5. CHARACTERIZING ℤ-COHOMOLOGY GROUPS -----

-- 5.1
-- Proposition 19
open HⁿSⁿ using (Hⁿ-Sⁿ≅ℤ)

-- 5.2
-- The torus
open 𝕋² using (𝕋²)

-- Propositions 20 and 21 respectively
open HⁿT² using (H¹-T²≅ℤ×ℤ ; H²-T²≅ℤ)

-- 5.3
-- The Klein bottle
open 𝕂² using (𝕂²)

-- The real projective plane
open ℝP using (ℝP²)

-- Proposition 22 and 23 respectively
-- ℤ/2ℤ is represented by Bool with the unique group structure
-- Lemma 23 is used implicitly in H²-𝕂²≅Bool
open Hⁿ𝕂² using (H¹-𝕂²≅ℤ ; H²-𝕂²≅Bool)

-- First and second cohomology groups of ℝP² respectively
open HⁿℝP² using (H¹-RP²≅1 ; H²-RP²≅Bool)

-- 5.4
-- The complex projective plane
open HⁿℂP² using (ℂP²)

-- Second and fourth cohomology groups ℂP² respectively
open HⁿℂP² using (H²CP²≅ℤ ;  H⁴CP²≅ℤ)

-- 6 Proving by computations in Cubical Agda
-- Proof of m = n = 1 case of graded commutativity (post truncation elimination):
-- Uncomment and give it a minute. The proof is currently not running very fast.

{-
open ⌣Comm using (-ₖ^_·_ )
n=m=1 : (a b : S¹)
    → _⌣ₖ_ {n = 1} {m = 1} ∣ a ∣ ∣ b ∣
     ≡ (-ₖ (_⌣ₖ_ {n = 1} {m = 1} ∣ b ∣ ∣ a ∣))
n=m=1 base base = refl
n=m=1 base (loop i) k = -ₖ (Properties.Kn→ΩKn+10ₖ _ (~ k) i)
n=m=1 (loop i) base k = Properties.Kn→ΩKn+10ₖ _ k i
n=m=1 (loop i) (loop j) k = -- This hcomp is just a simple rewriting to get paths in Ω²K₂
  hcomp (λ r → λ { (i = i0) → -ₖ Properties.Kn→ΩKn+10ₖ _ (~ k ∨ ~ r) j
                  ; (i = i1) → -ₖ Properties.Kn→ΩKn+10ₖ _ (~ k ∨ ~ r) j
                  ; (j = i0) → Properties.Kn→ΩKn+10ₖ _ (k ∨ ~ r) i
                  ; (j = i1) → Properties.Kn→ΩKn+10ₖ _ (k ∨ ~ r) i
                  ; (k = i0) →
                    doubleCompPath-filler
                      (sym (Properties.Kn→ΩKn+10ₖ _))
                      (λ j i →  _⌣ₖ_ {n = 1} {m = 1} ∣ loop i ∣ ∣ loop j ∣)
                      (Properties.Kn→ΩKn+10ₖ _)
                      (~ r) j i
                  ; (k = i1) →
                    -ₖ doubleCompPath-filler
                      (sym (Properties.Kn→ΩKn+10ₖ _))
                      (λ j i →  _⌣ₖ_ {n = 1} {m = 1} ∣ loop i ∣ ∣ loop j ∣)
                      (Properties.Kn→ΩKn+10ₖ _)
                      (~ r) i j})
        ((main
       ∙ sym (cong-∙∙ (cong (-ₖ_)) (sym (Properties.Kn→ΩKn+10ₖ _))
             (λ j i →  (_⌣ₖ_ {n = 1} {m = 1} ∣ loop i ∣ ∣ loop j ∣))
             (Properties.Kn→ΩKn+10ₖ _))) k i j)
  where
  open import Cubical.Foundations.Equiv.HalfAdjoint
  t : Iso (typ ((Ω^ 2) (K∙ 2))) ℤ
  t = compIso (congIso (invIso (Properties.Iso-Kn-ΩKn+1 1)))
       (invIso (Properties.Iso-Kn-ΩKn+1 0))

  p₁ = flipSquare ((sym (Properties.Kn→ΩKn+10ₖ _))
                      ∙∙ (λ j i →  _⌣ₖ_ {n = 1} {m = 1} ∣ loop i ∣ ∣ loop j ∣)
                      ∙∙ (Properties.Kn→ΩKn+10ₖ _))
  p₂ = (cong (cong (-ₖ_))
            ((sym (Properties.Kn→ΩKn+10ₖ _))))
                      ∙∙ (λ j i →  -ₖ (_⌣ₖ_ {n = 1} {m = 1} ∣ loop i ∣ ∣ loop j ∣))
                      ∙∙ (cong (cong (-ₖ_)) (Properties.Kn→ΩKn+10ₖ _))

  computation : Iso.fun t p₁ ≡ Iso.fun t p₂
  computation = refl

  main : p₁ ≡ p₂
  main = p₁                         ≡⟨ sym (Iso.leftInv t p₁) ⟩
        (Iso.inv t (Iso.fun t p₁))  ≡⟨ cong (Iso.inv t) computation ⟩
        Iso.inv t (Iso.fun t p₂)    ≡⟨ Iso.leftInv t p₂ ⟩
        p₂ ∎
-}

-- 𝕋² ≠ S² ∨ S¹ ∨ S¹
open HⁿT² using (T²≠S²⋁S¹⋁S¹)

-- Second "Brunerie number"
open HⁿℂP² using (g)
brunerie2 : ℤ
brunerie2 = g 1

----- A. Proofs -----

-- A.2 Proofs for Section 4

-- Lemma 27
open Homogen using (→∙Homogeneous≡)

-- Lemma 28
open Homogen using (isHomogeneous→∙)

-- Lemma 29
open Properties using (isHomogeneousKn)

-- Lemma 30, parts 1-3 respectively
open Path using (sym≡flipSquare ; sym-cong-sym≡id ; sym≡cong-sym)

-- Lemma 31
open ⌣Comm using (cong-ₖ-gen-inr)

-- A.3 Proofs for Section 5

-- Proposition 32
open HⁿSⁿ using (Hⁿ-Sᵐ≅1)

----- B. THE EILENBERG-STEENROD AXIOMS -----

-- B.1 The axioms in HoTT/UF

-- The axioms are defined as a record type
open ES-axioms.coHomTheory

-- Proof of the claim that the alternative reduced cohomology functor
-- Ĥ is the same as the usual reduced cohomology functor
_ : ∀ {ℓ} → satisfies-ES-axioms.H^~ {ℓ} ≡ satisfies-ES-axioms.Ĥ
_ = satisfies-ES-axioms.coHomFunctor≡coHomFunctor'

-- B.2 Verifying the axioms

-- Propositions 35 and 36.
_ : ∀ {ℓ} → ES-axioms.coHomTheory {ℓ} satisfies-ES-axioms.H^~
_ = satisfies-ES-axioms.isCohomTheoryZ

-- B.3 Characterizing Z-cohomology groups using the axioms

-- Theorem 37
open MayerVietoris.MV using ( Ker-i⊂Im-d ; Im-d⊂Ker-i
                            ; Ker-Δ⊂Im-i ; Im-i⊂Ker-Δ
                            ; Ker-d⊂Im-Δ ; Im-Δ⊂Ker-d)

----- C. BENCHMARKING COMPUTATIONS WITH THE COHOMOLOGY GROUPS -----

import Cubical.Experiments.ZCohomology.Benchmarks


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

module tests.compileCoreLibrary where
open import hott.core
open import hott.core.theorems
open import hott.topology
open import hott.topology.theorems
open import io.placeholder

main : IO Unit
main = dummyMain

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
-- NBE for Gödel System T
module NBE where

module Prelude where

  -- Zero and One -----------------------------------------------------------

  data Zero : Set where

  data One : Set where
    unit : One

  -- Natural numbers --------------------------------------------------------

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

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

-- Props ------------------------------------------------------------------

  data True : Prop where
    tt : True

  data False : Prop where

  postulate
    falseE : (A:Set) -> False -> A

  infix 3 /\

  data (/\)(P Q:Prop) : Prop where
    andI : P -> Q -> P /\ Q

module Fin where

  open Prelude

  -- Finite sets ------------------------------------------------------------

  data Suc (A:Set) : Set where
    fzero_ : Suc A
    fsuc_  : A -> Suc A

  mutual

    data Fin (n:Nat) : Set where
      finI : Fin_ n -> Fin n

    Fin_ : Nat -> Set
    Fin_  zero   = Zero
    Fin_ (suc n) = Suc (Fin n)

  fzero : {n:Nat} -> Fin (suc n)
  fzero = finI fzero_

  fsuc : {n:Nat} -> Fin n -> Fin (suc n)
  fsuc i = finI (fsuc_ i)

  finE : {n:Nat} -> Fin n -> Fin_ n
  finE (finI i) = i

module Vec where

  open Prelude
  open Fin

  infixr 15 ::

  -- Vectors ----------------------------------------------------------------

  data Nil : Set where
    nil_ : Nil

  data Cons (A As:Set) : Set where
    cons_ : A -> As -> Cons A As

  mutual

    data Vec (A:Set)(n:Nat) : Set where
      vecI : Vec_ A n -> Vec A n

    Vec_ : Set -> Nat -> Set
    Vec_ A  zero   = Nil
    Vec_ A (suc n) = Cons A (Vec A n)

  nil : {A:Set} -> Vec A zero
  nil = vecI nil_

  (::) : {A:Set} -> {n:Nat} -> A -> Vec A n -> Vec A (suc n)
  x :: xs = vecI (cons_ x xs)

  vecE : {A:Set} -> {n:Nat} -> Vec A n -> Vec_ A n
  vecE (vecI xs) = xs

  vec : {A:Set} -> (n:Nat) -> A -> Vec A n
  vec  zero   _ = nil
  vec (suc n) x = x :: vec n x

  map : {n:Nat} -> {A B:Set} -> (A -> B) -> Vec A n -> Vec B n
  map {zero}  f (vecI nil_)	    = nil
  map {suc n} f (vecI (cons_ x xs)) = f x :: map f xs

  (!) : {n:Nat} -> {A:Set} -> Vec A n -> Fin n -> A
  (!) {suc n} (vecI (cons_ x _ )) (finI fzero_)    = x
  (!) {suc n} (vecI (cons_ _ xs)) (finI (fsuc_ i)) = xs ! i

  tabulate : {n:Nat} -> {A:Set} -> (Fin n -> A) -> Vec A n
  tabulate {zero}  f = nil
  tabulate {suc n} f = f fzero :: tabulate (\x -> f (fsuc x))

module Syntax where

  open Prelude
  open Fin

  -- Types ------------------------------------------------------------------

  infixr 8 =>

  data Type : Set where
    nat  : Type
    (=>) : Type -> Type -> Type

  -- Terms ------------------------------------------------------------------

  data Term (n:Nat) : Set where
    eZero : Term n
    eSuc  : Term n
    eApp  : Term n -> Term n -> Term n
    eLam  : Term (suc n) -> Term n
    eVar  : Fin n -> Term n

module NormalForms where

  open Prelude
  open Syntax
  open Fin

  mutual

    -- Normal terms -----------------------------------------------------------

    data Normal (n:Nat) : Set where
      nZero    : Normal n
      nSuc     : Normal n -> Normal n
      nLam     : Normal (suc n) -> Normal n
      nNeutral : Neutral n -> Normal n
      nStuck   : Normal n		-- type error

    -- Neutral terms ----------------------------------------------------------

    data Neutral (n:Nat) : Set where
      uVar : Fin n -> Neutral n
      uApp : Neutral n -> Normal n -> Neutral n

  nVar : {n:Nat} -> Fin n -> Normal n
  nVar i = nNeutral (uVar i)

  nApp : {n:Nat} -> Neutral n -> Normal n -> Normal n
  nApp u n = nNeutral (uApp u n)

module Rename where

  open Prelude
  open Fin
  open Vec
  open NormalForms

  -- Renamings --------------------------------------------------------------

  Ren : Nat -> Nat -> Set
  Ren m n = Vec (Fin n) m

  id : {n:Nat} -> Ren n n
  id = tabulate (\i -> i)

  compose : {l m n:Nat} -> Ren m n -> Ren l m -> Ren l n
  compose {l}{m}{n} ρ γ = map (\i -> ρ ! i) γ

  lift : {m n:Nat} -> Ren m n -> Ren (suc m) (suc n)
  lift ρ = fzero :: map fsuc ρ

  mutual

    rename : {m n:Nat} -> Ren m n -> Normal m -> Normal n
    rename ρ nZero	  = nZero
    rename ρ (nSuc n)	  = nSuc (rename ρ n)
    rename ρ (nLam n)	  = nLam (rename (lift ρ) n)
    rename ρ (nNeutral u) = nNeutral (renameNe ρ u)
    rename ρ  nStuck	  = nStuck

    renameNe : {m n:Nat} -> Ren m n -> Neutral m -> Neutral n
    renameNe ρ (uVar i)	  = uVar (ρ ! i)
    renameNe ρ (uApp u n) = uApp (renameNe ρ u) (rename ρ n)

  up : {n:Nat} -> Ren n (suc n)
  up = map fsuc id

module Subst where

  open Prelude
  open Fin
  open Vec
  open NormalForms
  open Rename using (Ren; rename; up)

  -- Substitutions ----------------------------------------------------------

  Sub : Nat -> Nat -> Set
  Sub m n = Vec (Normal n) m

  id : {n:Nat} -> Sub n n
  id = tabulate nVar

  ren2sub : {m n:Nat} -> Ren m n -> Sub m n
  ren2sub ρ = map nVar ρ

  lift : {m n:Nat} -> Sub m n -> Sub (suc m) (suc n)
  lift σ = nVar fzero :: map (rename up) σ

  mutual

    app : {n:Nat} -> Normal n -> Normal n -> Normal n
    app  nZero	     _ = nStuck
    app (nSuc _)     _ = nStuck
    app  nStuck	     _ = nStuck
    app (nLam u)     v = subst (v :: id) u
    app (nNeutral n) v = nApp n v

    subst : {m n:Nat} -> Sub m n -> Normal m -> Normal n
    subst σ  nZero	 = nZero
    subst σ (nSuc v)	 = nSuc (subst σ v)
    subst σ (nLam v)	 = nLam (subst (lift σ) v)
    subst σ (nNeutral n) = substNe σ n
    subst σ  nStuck	 = nStuck

    substNe : {m n:Nat} -> Sub m n -> Neutral m -> Normal n
    substNe σ (uVar i)	 = σ ! i
    substNe σ (uApp n v) = substNe σ n `app` subst σ v

  compose : {l m n:Nat} -> Sub m n -> Sub l m -> Sub l n
  compose σ δ = map (subst σ) δ

module TypeSystem where

  open Prelude
  open Fin
  open Vec
  open Syntax

  mutual
    EqType : Type -> Type -> Prop
    EqType  nat	    nat	       = True
    EqType (τ => τ') (σ => σ') = τ == σ /\ τ' == σ'
    EqType  _	    _	       = False

    infix 5 ==
    data (==) (τ0 τ1:Type) : Prop where
      eqTypeI : EqType τ0 τ1 -> τ0 == τ1

  eqSubst : {σ τ:Type} -> (C:Type -> Set) -> σ == τ -> C τ -> C σ
  eqSubst {nat}{nat} C _ x = x
  eqSubst {σ => τ}{σ' => τ'} C (eqTypeI (andI eqσ eqτ)) x =
    eqSubst (\μ -> C (μ => τ)) eqσ (
      eqSubst (\η -> C (σ' => η)) eqτ x
    )

  Context : Nat -> Set
  Context n = Vec Type n

  mutual

    HasType : {n:Nat} -> Context n -> Term n -> Type -> Set
    HasType Γ eZero	   τ = ZeroType Γ τ
    HasType Γ eSuc	   τ = SucType  Γ τ
    HasType Γ (eVar i)	   τ = VarType  Γ i τ
    HasType Γ (eApp e1 e2) τ = AppType  Γ e1 e2 τ
    HasType Γ (eLam e)	   τ = LamType  Γ e τ

    data ZeroType {n:Nat}(Γ:Context n)(τ:Type) : Set where
      zeroType : τ == nat -> HasType Γ eZero τ

    data SucType {n:Nat}(Γ:Context n)(τ:Type) : Set where
      sucType : τ == (nat => nat) -> HasType Γ eSuc τ

    data VarType {n:Nat}(Γ:Context n)(i:Fin n)(τ:Type) : Set where
      varType : τ == (Γ ! i) -> HasType Γ (eVar i) τ

    data AppType {n:Nat}(Γ:Context n)(e1 e2:Term n)(τ:Type) : Set where
      appType : (σ:Type) -> HasType Γ e1 (σ => τ) -> HasType Γ e2 σ -> HasType Γ (eApp e1 e2) τ

    data LamType {n:Nat}(Γ:Context n)(e:Term (suc n))(τ:Type) : Set where
      lamType : (τ0 τ1:Type) -> τ == (τ0 => τ1) -> HasType (τ0 :: Γ) e τ1 -> HasType Γ (eLam e) τ

module NBE where

  open Prelude
  open Syntax
  open Fin
  open Vec
  open TypeSystem

  mutual

    D_ : Nat -> Type -> Set
    D_ n nat      = NatD n
    D_ n (σ => τ) = FunD n σ τ

    data D (n:Nat)(τ:Type) : Set where
      dI : D_ n τ -> D n τ

    data NatD (n:Nat) : Set where
      zeroD_ :		  D_ n nat
      sucD_  : D n nat -> D_ n nat
      neD_   : Term n  -> D_ n nat

    -- Will this pass the positivity check?
    data FunD (n:Nat)(σ τ:Type) : Set where
      lamD_  : (D n σ -> D n τ) -> D_ n (σ => τ)

  zeroD : {n:Nat} -> D n nat
  zeroD = dI zeroD_

  sucD : {n:Nat} -> D n nat -> D n nat
  sucD d = dI (sucD_ d)

  neD : {n:Nat} -> Term n -> D n nat
  neD t = dI (neD_ t)

  lamD : {n:Nat} -> {σ τ:Type} -> (D n σ -> D n τ) -> D n (σ => τ)
  lamD f = dI (lamD_ f)

  coerce : {n:Nat} -> {τ0 τ1:Type} -> τ0 == τ1 -> D n τ1 -> D n τ0
  coerce {n} = eqSubst (D n)

  mutual

    down : {τ:Type} -> {n:Nat} -> D n τ -> Term n
    down {σ => τ} (dI (lamD_ f)) = eLam (down {τ} ?)  -- doesn't work!
    down {nat}	  (dI zeroD_)    = eZero
    down {nat}	  (dI (sucD_ d)) = eSuc `eApp` down d
    down {nat}	  (dI (neD_ t))  = t

    up : {n:Nat} -> (τ:Type) -> Term n -> D n τ
    up (σ => τ) t = lamD (\d -> up τ (t `eApp` down d))
    up  nat	t = neD t

  Valuation : {m:Nat} -> Nat -> Context m -> Set
  Valuation {zero}  n  _		 = Nil
  Valuation {suc m} n (vecI (cons_ τ Γ)) = Cons (D n τ) (Valuation n Γ)

  (!!) : {m n:Nat} -> {Γ:Context m} -> Valuation n Γ -> (i:Fin m) -> D n (Γ ! i)
  (!!) {suc _} {_} {vecI (cons_ _ _)} (cons_ v ξ) (finI fzero_) = v
  (!!) {suc _} {_} {vecI (cons_ _ _)} (cons_ v ξ) (finI (fsuc_ i)) = ξ !! i

  ext : {m n:Nat} -> {τ:Type} -> {Γ:Context m} -> Valuation n Γ -> D n τ -> Valuation n (τ :: Γ)
  ext ξ v = cons_ v ξ

  app : {σ τ:Type} -> {n:Nat} -> D n (σ => τ) -> D n σ -> D n τ
  --app (dI (lamD_ f)) d = f d
  app (lamD f) d = f d

  eval : {n:Nat} -> {Γ:Context n} -> (e:Term n) -> (τ:Type) -> HasType Γ e τ -> Valuation n Γ -> D n τ
  eval (eVar i)   τ (varType eq)	  ξ = coerce eq (ξ !! i)
  eval (eApp r s) τ (appType σ dr ds)	  ξ = eval r (σ => τ) dr ξ `app` eval s σ ds ξ
  eval (eLam r)	  τ (lamType τ0 τ1 eq dr) ξ = coerce eq (lamD (\d -> ?))  -- doesn't work either
  eval  eZero	  τ (zeroType eq)	  ξ = coerce eq zeroD
  eval  eSuc	  τ (sucType eq)	  ξ = coerce eq (lamD sucD)

module Eval where

  open Prelude
  open Fin
  open Vec
  open Syntax
  open NormalForms
  open Rename using (up; rename)
  open Subst
  open TypeSystem

  eval : {n:Nat} -> (Γ:Context n) -> (e:Term n) -> (τ:Type) -> HasType Γ e τ -> Normal n
  eval Γ eZero	      τ  _		    = nZero
  eval Γ eSuc	      τ  _		    = nLam (nSuc (nVar fzero))
  eval Γ (eVar i)     τ  _		    = nVar i
  eval Γ (eApp e1 e2) τ (appType σ d1 d2)   = eval Γ e1 (σ => τ) d1 `app` eval Γ e2 σ d2
  eval Γ (eLam e)     τ (lamType τ0 τ1 _ d) = nLam (eval (τ0 :: Γ) e τ1 d)

open Prelude
open Fin
open Vec
open Syntax


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

open import M-types.Base.Core
open import M-types.Base.Sum
open import M-types.Base.Prod
open import M-types.Base.Eq

module M-types.Base.Equi where
    Qinv : {X : Ty ℓ₀} {Y : Ty ℓ₁} →
        ∏[ f ∈ (X → Y)] Ty (ℓ-max ℓ₀ ℓ₁)
    Qinv {_} {_} {X} {Y} f = ∑[ g ∈ (Y → X) ]
        (∏[ x ∈ X ] g (f x) ≡ x) ×
        (∏[ y ∈ Y ] f (g y) ≡ y)

    IsEqui : {X : Ty ℓ₀} {Y : Ty ℓ₁} →
        ∏[ f ∈ (X → Y) ] Ty (ℓ-max ℓ₀ ℓ₁)
    IsEqui {_} {_} {X} {Y} f =
        (∑[ g ∈ (Y → X) ] ∏[ x ∈ X ] g (f x) ≡ x) ×
        (∑[ g ∈ (Y → X) ] ∏[ y ∈ Y ] f (g y) ≡ y)

    infixr 8 _≃_
    _≃_ : ∏[ X ∈ Ty ℓ₀ ] ∏[ Y ∈ Ty ℓ₁ ] Ty (ℓ-max ℓ₀ ℓ₁)
    X ≃ Y = ∑[ f ∈ (X → Y) ] IsEqui f

    Qinv→IsEqui : {X : Ty ℓ₀} {Y : Ty ℓ₁} {f : X → Y} →
        Qinv f → IsEqui f
    Qinv→IsEqui (g , hom₀ , hom₁) = ((g , hom₀) , (g , hom₁))

    IsEqui→Qinv : {X : Ty ℓ₀} {Y : Ty ℓ₁} {f : X → Y} →
        IsEqui f → Qinv f
    IsEqui→Qinv {_} {_} {_} {_} {f} ((g₀ , hom₀) , (g₁ , hom₁)) =
        (
            g₀ ,
            hom₀ ,
            λ y → ap f (ap g₀ (hom₁ y)⁻¹ · hom₀ (g₁ y)) · hom₁ y
        )

    inv : {X : Ty ℓ₀} {Y : Ty ℓ₁} →
        ∏[ equi ∈ X ≃ Y ] (Y → X)
    inv (fun , isEqui) = pr₀ (IsEqui→Qinv isEqui)

    hom₀ : {X : Ty ℓ₀} {Y : Ty ℓ₁} →
        ∏[ equi ∈ X ≃ Y ] ∏[ x ∈ X ] inv equi (fun equi x) ≡ x
    hom₀ (fun , isEqui) = pr₀ (pr₁ (IsEqui→Qinv isEqui))

    hom₁ : {X : Ty ℓ₀} {Y : Ty ℓ₁} →
        ∏[ equi ∈ X ≃ Y ] ∏[ y ∈ Y ] fun equi (inv equi y) ≡ y
    hom₁ (fun , isEqui) = pr₁ (pr₁ (IsEqui→Qinv isEqui))

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.James where

open import Cubical.HITs.James.Base public
open import Cubical.HITs.James.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Agda.Primitive
open import Agda.Builtin.Nat

module Test₁ where

  record ⊤ {a} : Set a where
    constructor tt

  data G : (A : Set) → ⊤ {_} → Set where
    d : (x : ⊤) → G ⊤ x

  test : (g : G ⊤ tt) → Set
  test (d x) = ⊤

module Test₂ where

  postulate A : Set
            a : A

  record R {a} : Set a where
    constructor mkR
    field x : A

  data G : (A : Set) → R {_} → Set where
    d : (x : R) → G R x

  test : (g : G R (mkR a)) → R
  test (d x) = x

module Test₃ where

  postulate A : Set
            a : A

  record R {a} : Set a where
    constructor mkR
    field x y : A

  data G : (A : Set) → R {_} → Set where
    d : (x : R) → G R x

  -- Forced: mkR x y
  test₁ : ∀ x y → (g : G R (mkR x y)) → Set
  test₁ x y (d (mkR x y)) = A

  -- .(mkR x y) turns into z with x = .(R.x z) and y = .(R.y z)
  test₂ : ∀ x y → (g : G R (mkR x y)) → Set
  test₂ x y (d .(mkR x y)) = A

  test₃ : ∀ x y → (g : G R (mkR x y)) → Set
  test₃ .(R.x z) .(R.y z) (d z) = A


text:
module MetaOccursInItself where

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

data One : Set where one : One

postulate
  f : (A : Set) -> (A -> List A) -> One

err : One
err = f _ (\x -> x)

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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

module Light.Implementation.Data.Boolean where

open import Light.Library.Data.Boolean using (Library ; Dependencies)
open import Light.Variable.Sets
open import Light.Library.Data.Unit as Unit using (Unit ; unit)
open import Light.Level using (lift)
open import Light.Library.Relation.Decidable using (Decidable ; yes ; no)
open import Light.Library.Relation.Binary.Equality using (_≈_ ; wrap)
open import Light.Library.Relation.Binary using (reflexivity)
import Light.Implementation.Relation.Binary.Equality.Propositional
import Light.Implementation.Relation.Decidable
import Light.Package
import Light.Implementation.Relation.Binary.Equality.Propositional.Decidable as DecidablePropositional
import Light.Implementation.Data.Empty
import Light.Implementation.Data.Unit

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            data Boolean : Set where true false : Boolean

            {-# COMPILE JS
                  Boolean = (a, cons) => a ? cons.true() : cons.false()
            #-}
            {-# COMPILE JS true = !0 #-}
            {-# COMPILE JS false = !1 #-}

            -- TODO: Optimize operations using JS operators.

            if_then_else_ : Boolean → 𝕒 → 𝕒 → 𝕒
            if true then a else _ = a
            if false then _ else a = a

            postulate ¬_ : Boolean → Boolean
            postulate _∧_ _∨_ _⇢_ : Boolean → Boolean → Boolean

            true‐is‐true = lift unit
            false‐is‐false = lift unit

            private _≈?_ : ∀ (a b : Boolean) → Decidable (a ≈ b)
            false ≈? false = yes reflexivity
            false ≈? true = no λ ()
            true ≈? false = no λ ()
            true ≈? true = yes reflexivity

            equals = record { equals = wrap (record { are = λ a b → a ≈? b }) }

            module EqualityProperties = DecidablePropositional.Main _≈?_

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

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

module index3 where

{- van kampen -}
import homotopy.VanKampen

{- blakers massey -}
import homotopy.BlakersMassey

{- cogroups and suspensions -}
import homotopy.Cogroup

{- modalities -}
import homotopy.ModalWedgeExtension

{- conjecture 3.5.3 in favonia's thesis -}
import groups.Int

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module System.Directory where

open import System.FilePath
open import Prelude
open import Container.Traversable

{-# FOREIGN GHC import System.Directory #-}

private
  module Internal where
    postulate
      listContents : String → IO (List String)
      doesFileExist : String → IO Bool
    {-# COMPILE GHC listContents  = getDirectoryContents #-}
    {-# COMPILE GHC doesFileExist = doesFileExist #-}

abstract

  listContents : ∀ {k} → Path k → IO (List (Path k))
  listContents p = fmap (p //_ ∘ relative) <$> Internal.listContents (toString p)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
open import Algebra.Bundles using (CommutativeRing)

module Algebra.Module.Diff
  {r ℓr} {CR : CommutativeRing r ℓr}
  where

open import Assume using (assume)
import Data.Nat as ℕ
open ℕ using (ℕ; zero; suc)

open import Relation.Binary using (Rel)

open import Algebra.Module using (Module)
open Module

open import Function using (_∘_)
open import Data.Product using (proj₁; proj₂; _,_)

open import Algebra.Module.Morphism.Module using (→-module'; →-module; ⊸-module; _⊸_)
open import Algebra.Module.Construct.DirectProduct using () renaming (⟨module⟩ to ×-module)
open import Level using (_⊔_; Level)

private
  variable
    ma mℓa mb mℓb mc mℓc : Level

D-module : (MA : Module CR ma mℓa) (MB : Module CR mb mℓb) → Module CR _ _
D-module MA MB = →-module' MA (×-module MB (⊸-module MA MB))

instance
  D-module' : {MA : Module CR ma mℓa} {MB : Module CR mb mℓb} → Module CR _ _
  D-module' {MA = MA} {MB = MB} = →-module' MA (×-module MB (⊸-module MA MB))

D : (MA : Module CR ma mℓa) (MB : Module CR mb mℓb) → Set (r ⊔ ma ⊔ mℓa ⊔ mb ⊔ mℓb)
D MA MB = Carrierᴹ (→-module' MA (×-module MB (⊸-module MA MB)))

compose
  : {MA : Module CR ma mℓa} {MB : Module CR mb mℓb} {MC : Module CR mc mℓc}
  → D MB MC → D MA MB → D MA MC
compose {MA = MA} {MB = MB} {MC = MC} dbc dab a =
  let (b , a⊸b) = dab a
      (c , b⊸c) = dbc b
  in c , ⊸-compose b⊸c a⊸b
  where
    ⊸-compose : MB ⊸ MC → MA ⊸ MB → MA ⊸ MC
    ⊸-compose (b→c , b→c-ishom) (a→b , a→b-ishom) = b→c ∘ a→b , assume

run
  : ∀ {ma mℓa mb mℓb} {MA : Module CR ma mℓa} {MB : Module CR mb mℓb}
  → D MA MB → Carrierᴹ MA → Carrierᴹ MB
run f = proj₁ ∘ f

∇_[_]∙_
  : ∀ {ma mℓa mb mℓb} {MA : Module CR ma mℓa} {MB : Module CR mb mℓb}
  → D MA MB → Carrierᴹ MA → Carrierᴹ MA → Carrierᴹ MB
∇_[_]∙_ f = proj₁ ∘ proj₂ ∘ f

grad
  : ∀ {ma mℓa mb mℓb} {MA : Module CR ma mℓa} {MB : Module CR mb mℓb}
  → D MA MB → Carrierᴹ MA → Carrierᴹ MA → Carrierᴹ MB
grad f = proj₁ ∘ proj₂ ∘ f

max_stars_repo_name: cspollard/diff

max_issues_repo_name: cspollard/diff

max_forks_repo_name: cspollard/diff


text:
-- 2014-01-15 Andreas, reported by fredrik.forsberg

data Unit : Set where
  tt : Unit

foo : Unit
foo = {!!}
-- Refine here should give tt

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Conversion where
open import Agda.Builtin.Nat

nonDependent : Nat -> Nat -> Nat
nonDependent a b = a

dependent : {A : Set} -> A -> A
dependent a = a

stuff : {A : Set} -> {B : Nat} -> Nat -> Nat
stuff zero = zero
stuff (suc c) = dependent c


text:
module Cats.Category.Setoids.Facts.Products where

open import Data.Product as P using (_,_ ; <_,_>)
open import Relation.Binary using (Setoid)
open import Relation.Binary.Product.Pointwise using (×-setoid)

open import Cats.Category
open import Cats.Category.Setoids as Setoids using (Setoids ; ≈-intro ; ≈-elim)
open import Cats.Util.Conv

open Setoid using (Carrier ; refl ; sym ; trans) renaming (_≈_ to _≣_)

-- The existence of binary products, proven below, already follows from the
-- existence of general products, proven further below. We still construct them
-- explicitly because the definitions in this module are much easier to work
-- with.
module BuildBinary l l≈ where

  infixr 2 _×_

  open Category (Setoids l l≈)
  open Setoids._⇒_ using (resp)

  _×_ : Obj → Obj → Obj
  _×_ = ×-setoid

  projl : ∀ {A B} → A × B ⇒ A
  projl {A} {B} = record
      { arr = P.proj₁
      ; resp = λ { (eq₁ , eq₂) → eq₁ }
      }

  projr : ∀ {A B} → A × B ⇒ B
  projr {A} {B} = record
      { arr = P.proj₂
      ; resp = λ { (eq₁ , eq₂) → eq₂ }
      }

  ⟨_,_⟩ : ∀ {X A B} → X ⇒ A → X ⇒ B → X ⇒ A × B
  ⟨_,_⟩ {A = A} {B} xl xr = record
      { arr = < xl ⃗ , xr ⃗ >
      ; resp = λ eq → resp xl eq , resp xr eq
      }

  isBinaryProduct : ∀ {A B} → IsBinaryProduct (A × B) projl projr
  isBinaryProduct xl xr = record
    { arr = ⟨ xl , xr ⟩
    ; prop = (≈-intro λ eq → resp xl eq) , (≈-intro λ eq → resp xr eq)
    ; unique = λ { (eq₁ , eq₂) → ≈-intro λ x≈y → ≈-elim eq₁ x≈y , ≈-elim eq₂ x≈y }
    }

  _×′_ : ∀ A B → BinaryProduct A B
  A ×′ B = mkBinaryProduct projl projr isBinaryProduct

instance
  hasBinaryProducts : ∀ l l≈ → HasBinaryProducts (Setoids l l≈)
  hasBinaryProducts l l≈ .HasBinaryProducts._×′_ = BuildBinary._×′_ l l≈

module Build l {I : Set l} where

  open Category (Setoids l l)
  open Setoids._⇒_ using (resp)

  Π : (O : I → Obj) → Obj
  Π O = record
      { Carrier = ∀ i → Carrier (O i)
      ; _≈_ = λ f g → ∀ i → _≣_ (O i) (f i) (g i)
      ; isEquivalence = record
          { refl = λ i → refl (O i)
          ; sym = λ eq i → sym (O i) (eq i)
          ; trans = λ eq₁ eq₂ i → trans (O i) (eq₁ i) (eq₂ i)
          }
      }

  proj : ∀ {O : I → Obj} i → Π O ⇒ O i
  proj i = record
      { arr = λ f → f i
      ; resp = λ eq → eq i
      }

  isProduct : ∀ {O : I → Obj} → IsProduct O (Π O) proj
  isProduct x = record
      { arr = record
          { arr = λ a i → (x i ⃗) a
          ; resp = λ eq i → resp (x i) eq
          }
      ; prop = λ i → ≈-intro λ eq → resp (x i) eq
      ; unique = λ x-candidate → ≈-intro λ eq i → ≈-elim (x-candidate i) eq
      }

  Π′ : (O : I → Obj) → Product O
  Π′ O = record { prod = Π O ; proj = proj ; isProduct = isProduct }

instance
  hasProducts : ∀ l → HasProducts l (Setoids l l)
  hasProducts l = record { Π′ = Build.Π′ 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:
data Id (A : Set) : Set where
  wrap : A → Id A

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A → Maybe A

maybe : {A : Set} {B : Maybe A → Set} →
        ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
maybe j n (just x) = j x
maybe j n nothing  = n

record MaybeT (M : Set → Set) (A : Set) : Set where
  constructor wrap
  field
    run : M (Maybe A)

open MaybeT public

postulate
  R : Set
  r : R

module M (_ : R) where

  record Monad (M : Set → Set) : Set₁ where
    field
      return : ∀ {A} → A → M A
      _>>=_  : ∀ {A B} → M A → (A → M B) → M B

  open Monad ⦃ … ⦄ public

  instance

    transform : {M : Set → Set} ⦃ is-raw-monad : Monad M ⦄ →
                Monad (MaybeT M)
    run (Monad.return transform x)   = return (just x)
    run (Monad._>>=_  transform x f) =
      run x >>= maybe (λ x → run (f x)) (return nothing)

open M r

instance

  id-raw-monad : Monad Id
  Monad.return id-raw-monad            = wrap
  Monad._>>=_  id-raw-monad (wrap x) f = f x

postulate
  _∼_      : {A : Set} → Id A → Id A → Set
  refl     : {A : Set} (x : Id A) → x ∼ x
  trans    : {A : Set} {x y z : Id A} → x ∼ y → y ∼ z → x ∼ z
  id       : {A : Set} {x : Id A} (y : Id A) → x ∼ y → x ∼ y
  >>=-cong : {A : Set} (x : Id A) {f g : A → Id A} →
             (∀ z → f z ∼ g z) → (x >>= f) ∼ (x >>= g)
  assoc    : {A : Set} (x : Id A) (f : A → Id A) (g : A → Id A) →
             (x >>= (λ x → f x >>= g)) ∼ ((x >>= f) >>= g)

fails :
  {A : Set}
  (x : MaybeT Id A) (f : A → MaybeT Id A) (g : A → MaybeT Id A) →
  run (x >>= λ x → f x >>= g) ∼ run ((x >>= f) >>= g)
fails x f g =
  trans (>>=-cong (run x) (maybe (λ _ → refl _) (refl _)))
        (id (run ((x >>= f) >>= g))
            (assoc (run x) _ _))


text:
module ZisRing where

open import Data.Product using (_×_; _,_)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
  as PropEq using (_≡_; refl; cong; sym)

open import Integer10 -- 整数の定義

-- ---------- record ----------
record IsSemiGroup (A : Set) (_∙_ : A → A → A) : Set where
  field
    assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)
record IsMonoid (A : Set) (_∙_ : A → A → A) (e : A) : Set where
  field
    isSemiGroup : IsSemiGroup A _∙_
    identity : (∀ x → e ∙ x ≡ x) × (∀ x → x ∙ e ≡ x)
record IsGroup (A : Set) (_∙_ : A → A → A) (e : A) (iF : A → A) : Set where
  field
    isMonoid : IsMonoid A _∙_ e
    inv : (∀ x → (iF x) ∙ x ≡ e) × (∀ x → x ∙ (iF x) ≡ e)
record IsAbelianGroup (A : Set) (_∙_ : A → A → A) (e : A) (iF : A → A) : Set where
  field
    isGroup : IsGroup A _∙_ e iF
    comm : ∀ x y → x ∙ y ≡ y ∙ x
record IsRing (A : Set) (_⊕_ _⊗_ : A → A → A) (eP eT : A) (iF : A → A) : Set where
  field
    ⊕isAbelianGroup : IsAbelianGroup A _⊕_ eP iF
    ⊗isMonoid : IsMonoid A _⊗_ eT
    isDistR : (x y z : A) → (x ⊕ y) ⊗ z ≡ (x ⊗ z) ⊕ (y ⊗ z)
    isDistL : (x y z : A) → x ⊗ (y ⊕ z) ≡ (x ⊗ y) ⊕ (x ⊗ z)
-- ----------------------------

-- Z,+が半群であること
lemma5 : (x : ℤ) → x + zero ≡ x
lemma5 zero = refl
lemma5 (succ _) = refl
lemma5 (pred _) = refl
postulate -- ここだけ
  succPred : (x : ℤ) → succ (pred x) ≡ x
  predSucc : (x : ℤ) → pred (succ x) ≡ x
mutual
  succOut1 : (x y : ℤ) → succ x + y ≡ succ (x + y)
  succOut1 x zero = cong succ (sym (lemma5 x))
  succOut1 x (succ y) rewrite succOut1 x y
                                            | succOut2 x y = refl
  succOut1 x (pred y) rewrite predOut2 x y
                                            | succPred (x + y) = refl
  succOut2 : (x y : ℤ) → x + succ y ≡ succ (x + y)
  succOut2 zero y = refl
  succOut2 (succ x) y = refl
  succOut2 (pred x) y rewrite predOut1 x y
                                            | succPred (x + y) = refl
  predOut1 : (x y : ℤ) → pred x + y ≡ pred (x + y)
  predOut1 x zero = cong pred (sym (lemma5 x))
  predOut1 x (succ y) rewrite succOut2 x y
                                            | predSucc (x + y) = refl
  predOut1 x (pred y) rewrite predOut1 x y
                                            | predOut2 x y = refl
  predOut2 : (x y : ℤ) → x + pred y ≡ pred (x + y)
  predOut2 zero y = refl
  predOut2 (succ x) y rewrite succOut1 x y
                                            | predSucc (x + y) = refl
  predOut2 (pred x) y = refl

ℤ+-assoc : ∀ x y z → (x + y) + z ≡ x + (y + z)
ℤ+-assoc zero y z = refl
ℤ+-assoc (succ x) y z rewrite succOut1 x y
                                             | succOut1 (x + y) z
                                             | succOut1 x (y + z) = cong succ (ℤ+-assoc x y z)
ℤ+-assoc (pred x) y z rewrite predOut1 x y
                                             | predOut1 (x + y) z
                                             | predOut1 x (y + z) = cong pred (ℤ+-assoc x y z)
ℤ+-isSemiGroup : IsSemiGroup ℤ _+_
ℤ+-isSemiGroup = record { assoc = ℤ+-assoc }

-- Z,+がモノイドであること
ℤ+Zero-isMonoid : IsMonoid ℤ _+_ zero
ℤ+Zero-isMonoid = record { isSemiGroup = ℤ+-isSemiGroup ;
                                              identity = (zero+x≡x , x+zero≡x) }
  where
    zero+x≡x : ∀ x → zero + x ≡ x
    zero+x≡x _ = refl
    x+zero≡x : ∀ x → x + zero ≡ x
    x+zero≡x = lemma5

-- Z,+が群であること
leftInv : ∀ x → (opposite x + x) ≡ zero
leftInv zero = refl
leftInv (succ x) = leftInv x
leftInv (pred x) = leftInv x
rightInv : ∀ x → (x + opposite x) ≡ zero
rightInv zero = refl
rightInv (succ x) = rightInv x
rightInv (pred x) = rightInv x
ℤ+ZeroOpposite-isGroup : IsGroup ℤ _+_ zero opposite
ℤ+ZeroOpposite-isGroup = record { isMonoid = ℤ+Zero-isMonoid ;
                                                           inv = (leftInv , rightInv) }

-- Z,+がアーベル群であること
ℤ+ZeroOpposite-Comm : ∀ x y → (x + y) ≡ (y + x)
ℤ+ZeroOpposite-Comm zero y = sym (lemma5 y)
ℤ+ZeroOpposite-Comm (succ x) y rewrite succOut1 x y
                                                                 | succOut2 y x
          = cong succ (ℤ+ZeroOpposite-Comm x y)
ℤ+ZeroOpposite-Comm (pred x) y rewrite predOut1 x y
                                                                 | predOut2 y x
          = cong pred (ℤ+ZeroOpposite-Comm x y)
ℤ+ZeroOpposite-isAbelianGroup : IsAbelianGroup ℤ _+_ zero opposite
ℤ+ZeroOpposite-isAbelianGroup
  = record { isGroup = ℤ+ZeroOpposite-isGroup ;
                    comm = ℤ+ZeroOpposite-Comm }

-- Z,*が半群であること
lemma7 : (x y z : ℤ) → x * (y + z) ≡ (x * y) + (x * z)
lemma7 x y zero rewrite lemma5 y | lemma5 (x * y) = refl
lemma7 x y (succ z) rewrite succOut2 y z | lemma7 x y z
  = ℤ+-assoc (x * y) (x * z) x
lemma7 x y (pred z) rewrite predOut2 y z | lemma7 x y z
  = ℤ+-assoc (x * y) (x * z) (opposite x)
lemma8-3 : (x y : ℤ) → opposite x + opposite y ≡ opposite (x + y)
lemma8-3 x zero rewrite lemma5 (opposite x) | lemma5 x = refl
lemma8-3 x (succ y) rewrite predOut2 (opposite x) (opposite y)
                                            | succOut2 x y = cong pred (lemma8-3 x y)
lemma8-3 x (pred y) rewrite succOut2 (opposite x) (opposite y)
                                            | predOut2 x y = cong succ (lemma8-3 x y)
lemma8-5 : (x y : ℤ) → opposite x + y ≡ opposite (x + (opposite y))
lemma8-5 x zero rewrite lemma5 (opposite x) | lemma5 x = refl
lemma8-5 x (succ y) rewrite succOut2 (opposite x) y
                                           | predOut2 x (opposite y) = cong succ (lemma8-5 x y)
lemma8-5 x (pred y) rewrite predOut2 (opposite x) y
                                           | succOut2 x (opposite y) = cong pred (lemma8-5 x y)
lemma8-2 : (x y : ℤ) → x * opposite y ≡ opposite (x * y)
lemma8-2 x zero = refl
lemma8-2 x (succ y) rewrite lemma8-2 x y | lemma8-3 (x * y) x = refl
lemma8-2 x (pred y) rewrite lemma8-2 x y | lemma8-5 (x * y) x = refl
ℤ*-isSemiGroup : IsSemiGroup ℤ _*_
ℤ*-isSemiGroup = record { assoc = ℤ*-assoc }
  where
    ℤ*-assoc : ∀ x y z → ((x * y) * z) ≡ (x * (y * z))
    ℤ*-assoc x y zero = refl
    ℤ*-assoc x y (succ z) rewrite lemma7 x (y * z) y
      = cong (_+ (x * y)) (ℤ*-assoc x y z)
    ℤ*-assoc x y (pred z) rewrite lemma7 x (y * z) (opposite y)
                                                | lemma8-2 x y
      = cong (_+ opposite (x * y)) (ℤ*-assoc x y z)

-- Z,*がモノイドであること
one = succ zero
ℤ*One-isMonoid : IsMonoid ℤ _*_ one
ℤ*One-isMonoid = record { isSemiGroup = ℤ*-isSemiGroup ;
                                              identity = (one*x≡x , x*one≡x) }
  where
    one*x≡x : ∀ x → (succ zero) * x ≡ x
    one*x≡x zero = refl
    one*x≡x (succ x) rewrite succOut2 (succ zero * x) zero
                                          | lemma5 (succ zero * x) = cong succ (one*x≡x x)
    one*x≡x (pred x) rewrite predOut2 (succ zero * x) zero
                                          | lemma5 (succ zero * x) = cong pred (one*x≡x x)
    x*one≡x : ∀ x → x * one ≡ x
    x*one≡x _ = refl

-- Zが環であること
ℤ+ZeroOppo-*One-isRing : IsRing ℤ _+_ _*_ zero one opposite
ℤ+ZeroOppo-*One-isRing
  = record { ⊕isAbelianGroup = ℤ+ZeroOpposite-isAbelianGroup ;
                    ⊗isMonoid = ℤ*One-isMonoid ;
                    isDistR = isDistR-Z ;
                    isDistL = lemma7 }
    where
      lemma9 : ∀ a b c d → ((a + b) + (c + d)) ≡ ((a + c) + (b + d))
      lemma9 zero b c d rewrite sym (ℤ+-assoc b c d)
                                               | ℤ+ZeroOpposite-Comm b c
         = ℤ+-assoc c b d
      lemma9 (succ a) b c d rewrite succOut1 a b
                                              | succOut1 (a + b) (c + d)
                                              | succOut1 a c
                                              | succOut1 (a + c) (b + d)
         = cong succ (lemma9 a b c d)
      lemma9 (pred a) b c d  rewrite predOut1 a b
                                              | predOut1 (a + b) (c + d)
                                              | predOut1 a c
                                              | predOut1 (a + c) (b + d)
         = cong pred (lemma9 a b c d)
      isDistR-Z : ∀ x y z → ((x + y) * z) ≡ ((x * z) + (y * z))
      isDistR-Z x y zero = refl
      isDistR-Z x y (succ z) rewrite isDistR-Z x y z = lemma9 (x * z) (y * z) x y
      isDistR-Z x y (pred z) rewrite sym (lemma8-3 x y) | isDistR-Z x y z
        = lemma9 (x * z) (y * z) (opposite x) (opposite y)

-- (-1) * (-1) = (+1) その2
-- 「反数の反数」を使ってはいけないらしい
-- (-1) * 0 ≡ (-1) * (-1) + (-1)
-- rewrite x * 0 ≡ 0
-- x ≡ y → x + 1 ≡ y + 1
-- rewrite 0 + 1 ≡ 1
-- 結合法則 rewrite (x + y) + z ≡ x + (y + z)
-- rewrite (-1) + 1 ≡ 0
-- rewrite x + 0 ≡ x
-- 左辺と右辺を入れ替える

-₁ = pred zero
seed2 : (x : ℤ) → x * zero ≡ x * -₁ + x
seed2 x rewrite leftInv x = refl
lemma1 : (-₁ * zero ≡ -₁ * -₁ + -₁) → (zero ≡ -₁ * -₁ + -₁)
lemma1 prf = prf
lemma2 : (zero ≡ -₁ * -₁ + -₁) → (zero + one ≡ -₁ * -₁ + -₁ + one)
lemma2 prf = cong (_+ one) prf
lemma3 : (zero + one ≡ -₁ * -₁ + -₁ + one) → (one ≡ -₁ * -₁)
lemma3 prf = prf
lemma4 : (one ≡ -₁ * -₁) → (-₁ * -₁ ≡ one)
lemma4 p = sym p

theorem2 : pred zero * pred zero ≡ succ zero
theorem2 = (lemma4 ∘ lemma3 ∘ lemma2 ∘ lemma1) (seed2 -₁)


text:
{-

This file contains:

- Definition of the Bouquet of circles of a type aka wedge of A circles

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

module Cubical.HITs.Bouquet.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed

private
  variable
    ℓ : Level

data Bouquet (A : Type ℓ) : Type ℓ where
  base : Bouquet A
  loop : A → base ≡ base

Bouquet∙ : Type ℓ → Pointed ℓ
Bouquet∙ A = Bouquet A , base


text:
-- Only forced indices can be large.

data Img {a b} {A : Set a} {B : Set b} (f : A → B) : B → Set where
  inv : ∀ x → Img f (f x)


text:
module Proof where

open import Agda.Primitive hiding (_⊔_)
open import Reflection
open import Data.Fin hiding (_+_)
open import Data.Fin.Properties using (eq? ; _≟_ )
open import Data.Nat hiding (eq? ; _⊔_)
open import Data.Nat.Properties
open import Data.List
open import Data.String hiding (setoid)
open import Data.Bool
open import Data.Vec
open import Relation.Binary
open import Relation.Binary.EqReasoning
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong ; setoid )
import Relation.Binary.Indexed as I
open import Function using (_∘_ ; _$_ ; _∋_ ; id ; const)
open import Function.Equality using (_⟶_ ;  _⟨$⟩_ ; Π )
open import Function.LeftInverse hiding (_∘_)
open import Function.Injection using (_↣_ ; Injective ; Injection )
open import Function.Surjection using (_↠_ ; Surjective ; Surjection)
open import Function.Bijection using (Bijection ; Bijective ; id )
open import Relation.Nullary
open import Relation.Nullary.Negation

open import Helper.Fin
open import Serializer
open import Serializer.Fin
open import Serializer.Bool

data Test : Set where
  A : Bool -> Test
  B : Fin 2 -> Bool -> Test
  C : Fin 2 -> Test

open Serializer.Serializer {{...}}

fromTest : Test -> Fin 8
fromTest (A x) = +₁ 6 2 (+₁ 2 4 (from x))
fromTest (B x x₁) = +₁ 6 2 (+₂ 2 4 (× 2 2 (from x) (from x₁)))
fromTest (C x) = +₂ 6 2 (from x)

test : Fin 4 -> Test
test x with ⨂ 2 2 x
test .(× 2 2 i j) | is× i j = B (to i) (to j)

toTest : Fin 8 -> Test
toTest x = [ (\y -> [ (\z -> A $ to z) , test ] (⨁ 2 4 y) ) , (\y -> C $ to y) ] (⨁ 6 2 x)

--from-cong : Setoid._≈_ (setoid Test) I.=[ fromTest ]⇒ Setoid._≈_ (setoid (Fin 8))
--from-cong refl = refl

from-preserves-eq : setoid Test ⟶ setoid (Fin 8)
from-preserves-eq = record { _⟨$⟩_ = fromTest ; cong = (\{ {i} {.i} refl → refl }) }

from-injective : Injective from-preserves-eq
from-injective {A x} {A x₁} p with from-bool-injective ∘ +-eq₁ ∘ +-eq₁ $ p
from-injective {A x} {A .x} p | refl = refl
from-injective {A x} {B x₁ x₂} p = contradiction (+-eq₁ p) ¬+-eq₁
from-injective {A x} {C x₁} p = contradiction p ¬+-eq₁
from-injective {B x x₁} {A x₂} p = contradiction (+-eq₁ p) ¬+-eq₂
from-injective {B x x₁} {B y y₁} p with +-eq₂ {2} {4} ∘ +-eq₁ $ p
... | p2 with from-bool-injective (×-equal₁ {x₁ = x} {x₂ = y} p2) | ×-equal₂ {x₁ = x} {x₂ = y} p2
from-injective {B x x₁} {B .x .x₁} p | p2 | refl | refl = refl
from-injective {B x x₁} {C x₂} p = contradiction p ¬+-eq₁
from-injective {C x} {A x₁} p = contradiction p ¬+-eq₂
from-injective {C x} {B x₁ x₂} p = contradiction p ¬+-eq₂
from-injective {C x} {C .x} refl = refl

from-surjective : Surjective from-preserves-eq
from-surjective = record { from = preserves-eq-inv ; right-inverse-of = inv }
  where
--    cong-inverse : Setoid._≈_ (setoid (Fin 8)) I.=[ toTest ]⇒ Setoid._≈_ (setoid Test)
--    cong-inverse refl = refl

    preserves-eq-inv : setoid (Fin 8) ⟶ setoid Test
    preserves-eq-inv = record { _⟨$⟩_ = toTest ; cong = (\{ {i} {.i} refl → refl }) }

    inv : preserves-eq-inv RightInverseOf from-preserves-eq
    inv x with ⨁ 6 2 x
    inv .(+₁ 6 2 i) | is+₁ i with ⨁ 2 4 i
    inv ._ | is+₁ ._ | is+₁ i
      rewrite (Surjective.right-inverse-of (Bijective.surjective (Bijection.bijective (bijection {Bool})))) i = refl
    inv ._ | is+₁ ._ | is+₂ j with ⨂ 2 2 j
    inv ._ | is+₁ ._ | is+₂ ._ | is× i j
      rewrite (Surjective.right-inverse-of (Bijective.surjective (Bijection.bijective (bijection {Fin 2})))) i
        | (Surjective.right-inverse-of (Bijective.surjective (Bijection.bijective (bijection {Bool})))) j = refl
    inv ._ | is+₂ j = refl

from-injection : Test ↣ Fin 8
from-injection = record { to = from-preserves-eq ; injective = from-injective }

from-surjection : Test ↠ Fin 8
from-surjection = record { to = from-preserves-eq ; surjective = from-surjective }

from-bijection : Bijection (setoid Test) (setoid (Fin 8))
from-bijection = record { to = from-preserves-eq ; bijective = record { injective = from-injective ; surjective = from-surjective } }

instance
  serializerTest : Serializer Test
  serializerTest = record {
    size = 8 ;
    from = fromTest ;
    to = toTest ;
    bijection = from-bijection
    }

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


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
-}
{-# OPTIONS --allow-unsolved-metas #-}
open import Optics.All
open import LibraBFT.Prelude
open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Encode
open import LibraBFT.Base.KVMap as KVMap
open import LibraBFT.Base.Types
open import Data.String using (String)

-- This module defines types for an out-of-date implementation, based
-- on a previous version of LibraBFT.  It will be updated to model a
-- more recent version in future.
--
-- One important trick here is that the EventProcessor type separayes
-- types that /define/ the EpochConfig and types that /use/ the
-- /EpochConfig/. The advantage of doing this separation can be seen
-- in Util.Util.liftEC, where we define a lifting of a function that
-- does not change the bits that define the EpochConfig into the whole
-- state.  This enables a more elegant approach for reasoning about
-- functions that do not change parts of the state responsible for
-- defining the epoch config.  However, the separation is not perfect,
-- so sometimes fields may be modified in EpochIndep even though there
-- is no epoch change.

module LibraBFT.Impl.Consensus.Types where
  open import LibraBFT.Impl.Base.Types                       public
  open import LibraBFT.Impl.NetworkMsg                       public
  open import LibraBFT.Abstract.Types.EpochConfig UID NodeId public
  open import LibraBFT.Impl.Consensus.Types.EpochIndep       public
  open import LibraBFT.Impl.Consensus.Types.EpochDep         public

  -- The parts of the state of a peer that are used to
  -- define the EpochConfig are the SafetyRules and ValidatorVerifier:
  record EventProcessorEC : Set where
    constructor mkEventProcessorPreEC
    field
      ₋epSafetyRules  : SafetyRules
      ₋epValidators   : ValidatorVerifier
  open EventProcessorEC public
  unquoteDecl epSafetyRules epValidators = mkLens (quote EventProcessorEC)
    (epSafetyRules ∷ epValidators ∷ [])

  epEpoch : Lens EventProcessorEC EpochId
  epEpoch = epSafetyRules ∙ srPersistentStorage ∙ psEpoch

  epLastVotedRound : Lens EventProcessorEC Round
  epLastVotedRound = epSafetyRules ∙ srPersistentStorage ∙ psLastVotedRound

  -- We need enough authors to withstand the desired number of
  -- byzantine failures.  We enforce this with a predicate over
  -- 'EventProcessorEC'.
  EventProcessorEC-correct : EventProcessorEC → Set
  EventProcessorEC-correct epec =
    let numAuthors = kvm-size (epec ^∙ epValidators ∙ vvAddressToValidatorInfo)
        qsize      = epec ^∙ epValidators ∙ vvQuorumVotingPower
        bizF       = numAuthors ∸ qsize
     in suc (3 * bizF) ≤ numAuthors

  EventProcessorEC-correct-≡ : (epec1 : EventProcessorEC)
                             → (epec2 : EventProcessorEC)
                             → (epec1 ^∙ epValidators) ≡ (epec2 ^∙ epValidators)
                             → EventProcessorEC-correct epec1
                             → EventProcessorEC-correct epec2
  EventProcessorEC-correct-≡ epec1 epec2 refl = id

  -- Given a well-formed set of definitions that defines an EpochConfig,
  -- α-EC will compute this EpochConfig by abstracting away the unecessary
  -- pieces from EventProcessorEC.
  -- TODO-2: update and complete when definitions are updated to more recent version
  α-EC : Σ EventProcessorEC EventProcessorEC-correct → EpochConfig
  α-EC (epec , ok) =
    let numAuthors = kvm-size (epec ^∙ epValidators ∙ vvAddressToValidatorInfo)
        qsize      = epec ^∙ epValidators ∙ vvQuorumVotingPower
        bizF       = numAuthors ∸ qsize
     in (mkEpochConfig {! someHash?!}
                (epec ^∙ epEpoch) numAuthors {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!})

  postulate
    α-EC-≡ : (epec1  : EventProcessorEC)
           → (epec2  : EventProcessorEC)
           → (vals≡  : (epec1 ^∙ epValidators) ≡ (epec2 ^∙ epValidators))
           → (epoch≡ : (epec1 ^∙ epEpoch)      ≡ (epec2 ^∙ epEpoch))
           → (epec1-corr : EventProcessorEC-correct epec1)
           → α-EC (epec1 , epec1-corr) ≡ α-EC (epec2 , EventProcessorEC-correct-≡ epec1 epec2 vals≡ epec1-corr)
  {-
  α-EC-≡ epec1 epec2 refl refl epec1-corr = refl
  -}

  -- Finally, the EventProcessor is split in two pieces: those
  -- that are used to make an EpochConfig versus those that
  -- use an EpochConfig.
  record EventProcessor : Set where
    constructor mkEventProcessor
    field
      ₋epEC           : EventProcessorEC
      ₋epEC-correct   : EventProcessorEC-correct ₋epEC
      ₋epWithEC       : EventProcessorWithEC (α-EC (₋epEC , ₋epEC-correct))
     -- If we want to add pieces that neither contribute to the
     -- construction of the EC nor need one, they should be defined in
     -- EventProcessor directly
  open EventProcessor public

  α-EC-EP : EventProcessor → EpochConfig
  α-EC-EP ep = α-EC ((₋epEC ep) , (₋epEC-correct ep))

  ₋epHighestQC : (ep : EventProcessor) → QuorumCert
  ₋epHighestQC ep = ₋btHighestQuorumCert ((₋epWithEC ep) ^∙ (lBlockTree (α-EC-EP ep)))

  epHighestQC : Lens EventProcessor QuorumCert
  epHighestQC = mkLens' ₋epHighestQC
                        (λ (mkEventProcessor ec ecc (mkEventProcessorWithEC (mkBlockStore bsInner))) qc
                          → mkEventProcessor ec ecc (mkEventProcessorWithEC (mkBlockStore (record bsInner {₋btHighestQuorumCert = qc}))))

  ₋epHighestCommitQC : (ep : EventProcessor) → QuorumCert
  ₋epHighestCommitQC ep = ₋btHighestCommitCert ((₋epWithEC ep) ^∙ (lBlockTree (α-EC-EP ep)))

  epHighestCommitQC : Lens EventProcessor QuorumCert
  epHighestCommitQC = mkLens' ₋epHighestCommitQC
                        (λ (mkEventProcessor ec ecc (mkEventProcessorWithEC (mkBlockStore bsInner))) qc
                          → mkEventProcessor ec ecc (mkEventProcessorWithEC (mkBlockStore (record bsInner {₋btHighestCommitCert = qc}))))

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
module InstanceArguments where

postulate A₁ A₂ B : Set
          f₁ : {{a : A₁}} → B
          f₂ : {{a : A₂}} → B
          a₁ : A₁

-- resolve from signature
test₁ : B
test₁ = f₁

-- resolve from context
test₂ : {{a : A₂}} → B
test₂ = f₂

postulate F : Set → Set
          fA₁ : F A₁
          fA₂ : F A₂
          f₃ : {A : Set} → {{fA : F A}} → A → B

test₃ : B
test₃ = f₃ a₁

record Rec (t : Set) : Set₁ where
       field
         v : t

open module RecWI {t : Set} {{r : Rec t}} = Rec r

postulate testT₁ : Set
          testV₁ : testT₁
          testT₂ : Set
          testV₂ : testT₂

testRec₁ : Rec testT₁
testRec₁ = record { v = testV₁ }
testRec₂ : Rec testT₂
testRec₂ = record { v = testV₂ }

-- needs constraint checking in instance argument resolution
test : testT₂
test = v

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


text:
-- Andreas, 2015-06-11
-- testing with in copattern matching with dependent record

-- {-# OPTIONS -v tc.with:20 #-}

open import Common.Prelude
open import Common.Equality

data Dec P : Set where
  yes : (p : P) → Dec P
  no  : (¬p : P → ⊥) → Dec P

postulate
  _≟_ : (n m : Nat) → Dec (n ≡ m)
  boring : {A : Set} → A

record R : Set₁ where
  field
    Car  : Set
    el   : Car
    same : (x : Car) → Dec (x ≡ el)

test : (n : Nat) → R
R.Car  (test n) = Nat
R.el   (test n) = n
R.same (test zero) zero = yes refl
R.same (test zero) (suc x) = no λ()
R.same (test (suc n)) zero = no λ()
R.same (test (suc n)) (suc x) with n ≟ x
R.same (test (suc n)) (suc .n) | yes refl = yes refl
R.same (test (suc n)) (suc x) | no ¬p = no boring


text:
module Prelude.Monad.Indexed {i} {I : Set i} where

open import Agda.Primitive
open import Prelude.Function
open import Prelude.Functor
open import Prelude.Applicative.Indexed {I = I}

record IMonad {a b} (M : I → I → Set a → Set b) : Set (i ⊔ lsuc a ⊔ b) where
  infixr 1 _=<<_
  infixl 1 _>>=_ _>>_
  field
    _>>=_ : ∀ {A B i j k} → M i j A → (A → M j k B) → M i k B
    overlap {{super}} : IApplicative M

  _>>_ : ∀ {A B i j k} → M i j A → M j k B → M i k B
  m₁ >> m₂ = m₁ >>= λ _ → m₂

  _=<<_ : ∀ {A B i j k} → (A → M j k B) → M i j A → M i k B
  _=<<_ = flip _>>=_

return : ∀ {a b} {A : Set a} {M : I → I → Set a → Set b} {{_ : IMonad M}}
         {i : I} → A → M i i A
return = pure

open IMonad {{...}} public

{-# DISPLAY IMonad._>>=_  _ = _>>=_  #-}
{-# DISPLAY IMonad._=<<_  _ = _=<<_  #-}
{-# DISPLAY IMonad._>>_   _ = _>>_   #-}

join : ∀ {a} {M : I → I → Set a → Set a} {{_ : IMonad M}} {A : Set a}
       {i j k} → M i j (M j k A) → M i k A
join = _=<<_ id

-- Level polymorphic monads
record IMonad′ {a b} (M : ∀ {a} → I → I → Set a → Set a) : Set (i ⊔ lsuc (a ⊔ b)) where
  field
    _>>=′_ : {A : Set a} {B : Set b} {i j k : I} → M i j A → (A → M j k B) → M i k B
    overlap {{super}} : IApplicative′ {a} {b} M

  _>>′_ : {A : Set a} {B : Set b} {i j k : I} → M i j A → M j k B → M i k B
  m >>′ m′ = m >>=′ λ _ → m′

open IMonad′ {{...}} public


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

open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Rings.IntegralDomains.Definition

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

module Rings.Irreducibles.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where

open Setoid S
open Ring R
open import Rings.Units.Definition R

record Irreducible (r : A) : Set (a ⊔ b) where
  field
    nonzero : (r ∼ 0R) → False
    nonunit : (Unit r) → False
    irreducible : (x y : A) → (x * y) ∼ r → (Unit x → False) → Unit y


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

open import HoTT

module groups.ReducedWord {i} {A : Type i} (dec : has-dec-eq A) where

  is-reduced : Word A → Type i
  is-reduced nil                   = Lift ⊤
  is-reduced (_     :: nil)        = Lift ⊤
  is-reduced (inl x :: inl y :: w) = is-reduced (inl y :: w)
  is-reduced (inl x :: inr y :: w) = (x ≠ y) × is-reduced (inr y :: w)
  is-reduced (inr x :: inl y :: w) = (x ≠ y) × is-reduced (inl y :: w)
  is-reduced (inr x :: inr y :: w) = is-reduced (inr y :: w)

  -- Everything is a set.

  A-is-set : is-set A
  A-is-set = dec-eq-is-set dec

  PlusMinus-has-dec-eq : has-dec-eq (PlusMinus A)
  PlusMinus-has-dec-eq (inl x) (inl y) with dec x y
  PlusMinus-has-dec-eq (inl x) (inl y) | inl p  = inl $ ap inl p
  PlusMinus-has-dec-eq (inl x) (inl y) | inr ¬p = inr $ ¬p ∘ lower ∘ Coprod=-in
  PlusMinus-has-dec-eq (inl x) (inr y) = inr $ lower ∘ Coprod=-in
  PlusMinus-has-dec-eq (inr x) (inl y) = inr $ lower ∘ Coprod=-in
  PlusMinus-has-dec-eq (inr x) (inr y) with dec x y
  PlusMinus-has-dec-eq (inr x) (inr y) | inl p  = inl $ ap inr p
  PlusMinus-has-dec-eq (inr x) (inr y) | inr ¬p = inr $ ¬p ∘ lower ∘ Coprod=-in

  Word-has-dec-eq : has-dec-eq (Word A)
  Word-has-dec-eq nil nil = inl idp
  Word-has-dec-eq nil (_ :: w) = inr $ lower ∘ List=-in
  Word-has-dec-eq (_ :: v) nil = inr $ lower ∘ List=-in
  Word-has-dec-eq (x :: v) (y :: w) with PlusMinus-has-dec-eq x y
  Word-has-dec-eq (x :: v) (y :: w) | inl x=y with Word-has-dec-eq v w
  Word-has-dec-eq (x :: v) (y :: w) | inl x=y | inl v=w = inl $ List=-out (x=y , v=w)
  Word-has-dec-eq (x :: v) (y :: w) | inl x=y | inr v≠w = inr $ v≠w ∘ snd ∘ List=-in
  Word-has-dec-eq (x :: v) (y :: w) | inr x≠y = inr $ x≠y ∘ fst ∘ List=-in

  instance
    Word-is-set : is-set (Word A)
    Word-is-set = dec-eq-is-set Word-has-dec-eq

  is-reduced-is-prop : {w : Word A} → is-prop (is-reduced w)
  is-reduced-is-prop {nil}                 = ⟨⟩
  is-reduced-is-prop {x    :: nil}         = ⟨⟩
  is-reduced-is-prop {inl x :: inl y :: l} = is-reduced-is-prop {inl y :: l}
  is-reduced-is-prop {inl x :: inr y :: l} = ⟨⟩ where instance _ = is-reduced-is-prop {inr y :: l}
  is-reduced-is-prop {inr x :: inl y :: l} = ⟨⟩ where instance _ = is-reduced-is-prop {inl y :: l}
  is-reduced-is-prop {inr x :: inr y :: l} = is-reduced-is-prop {inr y :: l}

  is-reduced-prop : SubtypeProp (Word A) i
  is-reduced-prop = is-reduced , λ w → is-reduced-is-prop {w}

  -- The subtype

  ReducedWord : Type i
  ReducedWord = Subtype is-reduced-prop

  instance
    ReducedWord-is-set : is-set ReducedWord
    ReducedWord-is-set = Subtype-level is-reduced-prop where instance _ = is-reduced-is-prop

  -- Identifications in [ReducedWord].

  ReducedWord= : ReducedWord → ReducedWord → Type i
  ReducedWord= = Subtype= is-reduced-prop

  ReducedWord=-out : {x y : ReducedWord} → ReducedWord= x y → x == y
  ReducedWord=-out = Subtype=-out is-reduced-prop

  -- The group structure of reduced words

  private
    rw-unit : ReducedWord
    rw-unit = nil , lift tt

    abstract
      tail-is-reduced : ∀ x w → is-reduced (x :: w) → is-reduced w
      tail-is-reduced x nil red = lift tt
      tail-is-reduced (inl x) (inl y :: w) red = red
      tail-is-reduced (inl x) (inr y :: w) red = snd red
      tail-is-reduced (inr x) (inl y :: w) red = snd red
      tail-is-reduced (inr x) (inr y :: w) red = red

    rw-cons : PlusMinus A → ReducedWord → ReducedWord
    rw-cons x (nil , _) = (x :: nil) , lift tt
    rw-cons (inl x) ((inl y :: l) , red) = (inl x :: inl y :: l) , red
    rw-cons (inl x) ((inr y :: l) , red) with dec x y
    rw-cons (inl x) ((inr y :: l) , red) | inl p = l , tail-is-reduced (inr y) l red
    rw-cons (inl x) ((inr y :: l) , red) | inr ¬p = (inl x :: inr y :: l) , (¬p , red)
    rw-cons (inr x) ((inl y :: l) , red) with dec x y
    rw-cons (inr x) ((inl y :: l) , red) | inl p = l , tail-is-reduced (inl y) l red
    rw-cons (inr x) ((inl y :: l) , red) | inr ¬p = (inr x :: inl y :: l) , (¬p , red)
    rw-cons (inr x) ((inr y :: l) , red) = (inr x :: inr y :: l) , red

    rw-++' : Word A → ReducedWord → ReducedWord
    rw-++' w₁ rw₂ = foldr rw-cons rw₂ w₁

    reduce : Word A → ReducedWord
    reduce w = rw-++' w rw-unit

    rw-++ : ReducedWord → ReducedWord → ReducedWord
    rw-++ rw₁ rw₂ = rw-++' (fst rw₁) rw₂

    abstract
      -- assoc
      rw-cons-reduced : ∀ x w
        → (red : is-reduced w)
        → (red' : is-reduced (x :: w))
        → rw-cons x (w , red) == (x :: w) , red'
      rw-cons-reduced x nil _ _ = ReducedWord=-out idp
      rw-cons-reduced (inl x) (inl y :: w) _ red' = ReducedWord=-out idp
      rw-cons-reduced (inl x) (inr y :: w) _ red' with dec x y
      rw-cons-reduced (inl x) (inr y :: w) _ red' | inl p = ⊥-rec $ fst red' $ p
      rw-cons-reduced (inl x) (inr y :: w) _ red' | inr ¬p = ReducedWord=-out idp
      rw-cons-reduced (inr x) (inl y :: w) _ red' with dec x y
      rw-cons-reduced (inr x) (inl y :: w) _ red' | inl p = ⊥-rec $ fst red' $ p
      rw-cons-reduced (inr x) (inl y :: w) _ red' | inr ¬p = ReducedWord=-out idp
      rw-cons-reduced (inr x) (inr y :: w) _ red' = ReducedWord=-out idp

      rw-cons-flip : ∀ x w red red'
        → rw-cons x ((flip x :: w) , red) == w , red'
      rw-cons-flip (inl x) w _ _ with dec x x
      rw-cons-flip (inl x) w _ _ | inl x=x = ReducedWord=-out idp
      rw-cons-flip (inl x) w _ _ | inr x≠x = ⊥-rec (x≠x idp)
      rw-cons-flip (inr x) w _ _ with dec x x
      rw-cons-flip (inr x) w _ _ | inl x=x = ReducedWord=-out idp
      rw-cons-flip (inr x) w _ _ | inr x≠x = ⊥-rec (x≠x idp)

      rw-cons-cons-flip : ∀ x rw
        → rw-cons x (rw-cons (flip x) rw) == rw
      rw-cons-cons-flip x (nil , red) = rw-cons-flip x nil _ red
      rw-cons-cons-flip (inl x) ((inl y :: w) , red) with dec x y
      rw-cons-cons-flip (inl x) ((inl y :: w) , red) | inl x=y =
          rw-cons-reduced (inl x) w _ (transport! (λ z → is-reduced (inl z :: w)) x=y red)
        ∙ ReducedWord=-out (ap (λ z → inl z :: w) x=y)
      rw-cons-cons-flip (inl x) ((inl y :: w) , red) | inr x≠y =
        rw-cons-flip (inl x) (inl y :: w) (x≠y , red) red
      rw-cons-cons-flip (inl x) ((inr y :: w) , red) = rw-cons-flip (inl x) (inr y :: w) red red
      rw-cons-cons-flip (inr x) ((inl y :: w) , red) = rw-cons-flip (inr x) (inl y :: w) red red
      rw-cons-cons-flip (inr x) ((inr y :: w) , red) with dec x y
      rw-cons-cons-flip (inr x) ((inr y :: w) , red) | inl x=y =
          rw-cons-reduced (inr x) w _ (transport! (λ z → is-reduced (inr z :: w)) x=y red)
        ∙ ReducedWord=-out (ap (λ z → inr z :: w) x=y)
      rw-cons-cons-flip (inr x) ((inr y :: w) , red) | inr x≠y =
        rw-cons-flip (inr x) (inr y :: w) (x≠y , red) red

      rw-++-cons : ∀ x rw₁ rw₂
        →  rw-++ (rw-cons x rw₁) rw₂
        == rw-cons x (rw-++ rw₁ rw₂)
      rw-++-cons x       (nil           , _) rw₂ = idp
      rw-++-cons (inl x) ((inl y :: w₁) , _) rw₂ = idp
      rw-++-cons (inl x) ((inr y :: w₁) , _) rw₂ with dec x y
      rw-++-cons (inl x) ((inr y :: w₁) , _) rw₂ | inl p rewrite p =
        ! (rw-cons-cons-flip (inl y) (rw-++' w₁ rw₂))
      rw-++-cons (inl x) ((inr y :: w₁) , _) rw₂ | inr ¬p = idp
      rw-++-cons (inr x) ((inl y :: w₁) , _) rw₂ with dec x y
      rw-++-cons (inr x) ((inl y :: w₁) , _) rw₂ | inl p rewrite p =
        ! (rw-cons-cons-flip (inr y) (rw-++' w₁ rw₂))
      rw-++-cons (inr x) ((inl y :: w₁) , _) rw₂ | inr ¬p = idp
      rw-++-cons (inr x) ((inr y :: w₁) , _) rw₂ = idp

      rw-++-assoc' : ∀ w₁ rw₂ rw₃
        →  rw-++ (rw-++' w₁ rw₂) rw₃
        == rw-++' w₁ (rw-++' (fst rw₂) rw₃)
      rw-++-assoc' nil rw₂ rw = idp
      rw-++-assoc' (x :: w₁) rw₂ rw₃ =
          rw-++-cons x (rw-++' w₁ rw₂) rw₃
        ∙ ap (rw-cons x) (rw-++-assoc' w₁ rw₂ rw₃)

    -- inv
    abstract
      head2-is-reduced : ∀ x y w → is-reduced (x :: y :: w) → is-reduced (x :: y :: nil)
      head2-is-reduced (inl x) (inl y) w red = lift tt
      head2-is-reduced (inl x) (inr y) w red = fst red , lift tt
      head2-is-reduced (inr x) (inl y) w red = fst red , lift tt
      head2-is-reduced (inr x) (inr y) w red = lift tt

      cons-is-reduced : ∀ x y w → is-reduced (x :: y :: nil) → is-reduced (y :: w)
        → is-reduced (x :: y :: w)
      cons-is-reduced (inl x) (inl y) _ _    red₂ = red₂
      cons-is-reduced (inl x) (inr y) _ red₁ red₂ = fst red₁ , red₂
      cons-is-reduced (inr x) (inl y) _ red₁ red₂ = fst red₁ , red₂
      cons-is-reduced (inr x) (inr y) _ _    red₂ = red₂

      ++-is-reduced : ∀ w₁ x w₂ → is-reduced (w₁ ++ (x :: nil)) → is-reduced (x :: w₂)
        → is-reduced ((w₁ ++ (x :: nil)) ++ w₂)
      ++-is-reduced nil            _ _  _    red₂ = red₂
      ++-is-reduced (x :: nil)     y w₂ red₁ red₂ = cons-is-reduced x y w₂ red₁ red₂
      ++-is-reduced (x :: y :: w₁) z w₂ red₁ red₂ =
        cons-is-reduced x y ((w₁ ++ (z :: nil)) ++ w₂)
          (head2-is-reduced x y (w₁ ++ (z :: nil)) red₁)
          (++-is-reduced (y :: w₁) z w₂ (tail-is-reduced x (y :: w₁ ++ (z :: nil)) red₁) red₂)

      swap2-is-reduced : ∀ x y → is-reduced (x :: y :: nil) → is-reduced (y :: x :: nil)
      swap2-is-reduced (inl x) (inl y) red = lift tt
      swap2-is-reduced (inl x) (inr y) red = fst red ∘ ! , lift tt
      swap2-is-reduced (inr x) (inl y) red = fst red ∘ ! , lift tt
      swap2-is-reduced (inr x) (inr y) red = lift tt

      reverse-is-reduced : ∀ w → is-reduced w → is-reduced (reverse w)
      reverse-is-reduced nil red = red
      reverse-is-reduced (x :: nil) red = red
      reverse-is-reduced (x :: y :: w) red =
        ++-is-reduced
          (reverse w) y (x :: nil)
          (reverse-is-reduced (y :: w) (tail-is-reduced x (y :: w) red))
          (swap2-is-reduced x y (head2-is-reduced x y w red))

      flip2-is-reduced : ∀ x y → is-reduced (x :: y :: nil) → is-reduced (flip x :: flip y :: nil)
      flip2-is-reduced (inl x) (inl y) red = red
      flip2-is-reduced (inl x) (inr y) red = red
      flip2-is-reduced (inr x) (inl y) red = red
      flip2-is-reduced (inr x) (inr y) red = red

      Word-flip-is-reduced : ∀ w → is-reduced w → is-reduced (Word-flip w)
      Word-flip-is-reduced nil           red = red
      Word-flip-is-reduced (x :: nil)    red = red
      Word-flip-is-reduced (x :: y :: w) red =
        cons-is-reduced (flip x) (flip y) (Word-flip w)
          (flip2-is-reduced x y (head2-is-reduced x y w red))
          (Word-flip-is-reduced (y :: w) (tail-is-reduced x (y :: w) red))

    rw-inv : ReducedWord → ReducedWord
    rw-inv (w , red) = reverse (Word-flip w) , reverse-is-reduced (Word-flip w) (Word-flip-is-reduced w red)

    abstract
      rw-inv-l-lemma : ∀ w₁ x w₂ (red₂ : is-reduced (x :: w₂)) (red₂' : is-reduced w₂)
        →  rw-++' (w₁ ++ (flip x :: nil)) ((x :: w₂) , red₂)
        == rw-++' w₁ (w₂ , red₂')
      rw-inv-l-lemma nil (inl x) w₂ _ _ with dec x x
      rw-inv-l-lemma nil (inl x) w₂ _ _ | inl p = ReducedWord=-out idp
      rw-inv-l-lemma nil (inl x) w₂ _ _ | inr ¬p = ⊥-rec (¬p idp)
      rw-inv-l-lemma nil (inr x) w₂ _ _ with dec x x
      rw-inv-l-lemma nil (inr x) w₂ _ _ | inl p = ReducedWord=-out idp
      rw-inv-l-lemma nil (inr x) w₂ _ _ | inr ¬p = ⊥-rec (¬p idp)
      rw-inv-l-lemma (x :: w₁) y w₂ red₂ red₂' =
        ap (rw-cons x) (rw-inv-l-lemma w₁ y w₂ red₂ red₂')

      rw-inv-l' : ∀ w (red : is-reduced w)
        → rw-++' (reverse (Word-flip w)) (w , red) == nil , lift tt
      rw-inv-l' nil _ = idp
      rw-inv-l' (x :: w) red =
          rw-inv-l-lemma (reverse (Word-flip w)) x w red (tail-is-reduced x w red)
        ∙ rw-inv-l' w (tail-is-reduced x w red)

      suffix-is-reduced : ∀ w₁ w₂ → is-reduced (w₁ ++ w₂) → is-reduced w₂
      suffix-is-reduced nil w₂ red = red
      suffix-is-reduced (x :: w₁) w₂ red = suffix-is-reduced w₁ w₂ $ tail-is-reduced x (w₁ ++ w₂) red

  ReducedWord-group-struct : GroupStructure ReducedWord
  ReducedWord-group-struct = record
    { ident = nil , lift tt
    ; inv = rw-inv
    ; comp = rw-++
    ; unit-l = λ _ → idp
    ; assoc = λ rw → rw-++-assoc' (fst rw)
    ; inv-l = uncurry rw-inv-l'
    }

  ReducedWord-group : Group i
  ReducedWord-group = group _ ReducedWord-group-struct

  private
    abstract
      QuotWordRel-cons : ∀ x w₂ (red₂ : is-reduced w₂)
        → QuotWordRel (x :: w₂) (fst (rw-cons x (w₂ , red₂)))
      QuotWordRel-cons x nil _ = qwr-refl idp
      QuotWordRel-cons (inl x) (inl y :: w) _ = qwr-refl idp
      QuotWordRel-cons (inl x) (inr y :: w) _ with dec x y
      QuotWordRel-cons (inl x) (inr y :: w) _ | inl x=y rewrite x=y = qwr-flip (inl y) w
      QuotWordRel-cons (inl x) (inr y :: w) _ | inr x≠y = qwr-refl idp
      QuotWordRel-cons (inr x) (inl y :: w) _ with dec x y
      QuotWordRel-cons (inr x) (inl y :: w) _ | inl x=y rewrite x=y = qwr-flip (inr y) w
      QuotWordRel-cons (inr x) (inl y :: w) _ | inr x≠y = qwr-refl idp
      QuotWordRel-cons (inr x) (inr y :: w) _ = qwr-refl idp

      QuotWordRel-++ : ∀ w₁ rw₂
        → QuotWordRel (w₁ ++ fst rw₂) (fst (rw-++' w₁ rw₂))
      QuotWordRel-++ nil _ = qwr-refl idp
      QuotWordRel-++ (x :: w₁) rw₂ =
        qwr-trans (qwr-cons x (QuotWordRel-++ w₁ rw₂)) $
        uncurry (QuotWordRel-cons x) (rw-++' w₁ rw₂)

  -- freeness
  ReducedWord-to-FreeGroup : ReducedWord-group →ᴳ FreeGroup A
  ReducedWord-to-FreeGroup = group-hom (λ rw → qw[ fst rw ])
    (λ rw₁ rw₂ → ! $ quot-rel $ QuotWordRel-++ (fst rw₁) rw₂)

  private
    abstract
      reduce-emap : ∀ {w₁ w₂} → QuotWordRel w₁ w₂ → reduce w₁ == reduce w₂
      reduce-emap (qwr-refl p) = ap reduce p
      reduce-emap (qwr-trans qwr₁ qwr₂) = reduce-emap qwr₁ ∙ reduce-emap qwr₂
      reduce-emap (qwr-sym qwr) = ! (reduce-emap qwr)
      reduce-emap (qwr-cons x qwr) = ap (rw-cons x) (reduce-emap qwr)
      reduce-emap (qwr-flip x w) = rw-cons-cons-flip x (reduce w)

    to = GroupHom.f ReducedWord-to-FreeGroup

    from : QuotWord A → ReducedWord
    from = QuotWord-rec reduce reduce-emap

    abstract
      QuotWordRel-reduce : ∀ w
        → QuotWordRel w (fst (reduce w))
      QuotWordRel-reduce nil = qwr-refl idp
      QuotWordRel-reduce (x :: w) =
        qwr-trans (qwr-cons x (QuotWordRel-reduce w)) $
        uncurry (QuotWordRel-cons x) (reduce w)

      to-from : ∀ qw → to (from qw) == qw
      to-from = QuotWord-elim
        (λ w → ! $ quot-rel $ QuotWordRel-reduce w)
        (λ _ → prop-has-all-paths-↓)

      from-to : ∀ rw → from (to rw) == rw
      from-to = Group.unit-r ReducedWord-group

  ReducedWord-iso-FreeGroup : ReducedWord-group ≃ᴳ FreeGroup A
  ReducedWord-iso-FreeGroup = ReducedWord-to-FreeGroup , is-eq to from to-from from-to


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Base definitions for the left-biased universe-sensitive functor and
-- monad instances for the Product type.
--
-- To minimize the universe level of the RawFunctor, we require that
-- elements of B are "lifted" to a copy of B at a higher universe level
-- (a ⊔ b). See the Data.Product.Categorical.Examples for how this is
-- done.
------------------------------------------------------------------------

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

open import Level

module Data.Product.Categorical.Left.Base
  {a} (A : Set a) (b : Level) where

open import Data.Product using (_×_; map₂; proj₁; proj₂; <_,_>)
open import Category.Functor using (RawFunctor)
open import Category.Comonad using (RawComonad)

------------------------------------------------------------------------
-- Definitions

Productₗ : Set (a ⊔ b) → Set (a ⊔ b)
Productₗ B = A × B

functor : RawFunctor Productₗ
functor = record { _<$>_ = λ f → map₂ f }

comonad : RawComonad Productₗ
comonad = record
  { extract = proj₂
  ; extend  = < proj₁ ,_>
  }


text:
module Data.Maybe.Instance where

open import Category.FAM
open import Data.Maybe
open import Function using (_∘_; id)
open import Relation.Binary.PropositionalEquality

instance
    MaybeFunctor : ∀ {ℓ} → Functor {ℓ} Maybe
    MaybeFunctor {ℓ} = record
        { _<$>_ = map
        ; isFunctor = record
            { identity = identity
            ; homo = homo
            }
        }
        where
            identity : ∀ {A : Set ℓ} (a : Maybe A) → map id a ≡ a
            identity (just x) = refl
            identity nothing = refl

            homo : ∀ {A B C : Set ℓ} (f : B → C) (g : A → B)
                (a : Maybe A) → map (f ∘ g) a ≡ map f (map g a)
            homo _ _ (just x) = refl
            homo _ _ nothing = refl

    MaybeApplicative : ∀ {ℓ} → Applicative {ℓ} Maybe
    MaybeApplicative {ℓ} = record
        { pure = just
        ; _⊛_ = ap
        ; isApplicative = record
            { identity = identity
            ; compose = compose
            ; homo = λ _ _ → refl
            ; interchange = interchange
            }
        }
        where
            open ≡-Reasoning
            open import Function

            ap : {A B : Set ℓ} → Maybe (A → B) → Maybe A → Maybe B
            ap (just f) x = map f x
            ap nothing  x = nothing

            identity : {A : Set ℓ} (x : Maybe A) → map id x ≡ x
            identity (just x) = refl
            identity nothing = refl

            compose : {A B C : Set ℓ} (fs : Maybe (B → C)) (gs : Maybe (A → B))
                → (xs : Maybe A)
                → ap (ap (map _∘′_ fs) gs) xs ≡ ap fs (ap gs xs)
            compose {A} {B} {C} (just fs) (just gs) (just xs) = refl
            compose {A} {B} {C} (just fs) (just gs) nothing   = refl
            compose {A} {B} {C} (just fs) nothing   (just xs) = refl
            compose {A} {B} {C} (just fs) nothing   nothing   = refl
            compose {A} {B} {C} nothing   (just gs) (just xs) = refl
            compose {A} {B} {C} nothing   (just gs) nothing   = refl
            compose {A} {B} {C} nothing   nothing   (just xs) = refl
            compose {A} {B} {C} nothing   nothing   nothing   = refl

            interchange : {A B : Set ℓ} (fs : Maybe (A → B)) (x : A) → ap fs (just x) ≡ ap (just (λ f → f x)) fs
            interchange {A} {B} (just f) x = refl
            interchange {A} {B} nothing x = refl

max_stars_repo_name: banacorn/FAM

max_issues_repo_name: banacorn/FAM

max_forks_repo_name: banacorn/FAM


text:
open import Coinduction using ( ♭ )
open import Data.Product using ( _,_ )
open import Relation.Binary using ( Poset )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; sym ; trans ; cong ; subst₂ ) renaming ( setoid to ≡-setoid )
open import System.IO.Transducers using ( _⇒_ ; inp ; out ; done ; ⟦_⟧ ; _≃_ ; _≲_ ; _⟫_ )
open import System.IO.Transducers.Session using ( Session )
open import System.IO.Transducers.Trace using ( Trace ; [] ; _∷_ ; _⊑_ )
open import System.IO.Transducers.Properties.Category using ( ⟫-semantics )

import Relation.Binary.PartialOrderReasoning

module System.IO.Transducers.Properties.TwoCategory where

-- The category is poset-enriched, with order inherited from prefix order on traces.

-- Reflexivity

⊑-refl : ∀ {S} (as : Trace S) → (as ⊑ as)
⊑-refl [] = []
⊑-refl (a ∷ as) = (a ∷ ⊑-refl as)

≡-impl-⊑ : ∀ {S} {as bs : Trace S} → (as ≡ bs) → (as ⊑ bs)
≡-impl-⊑ refl = ⊑-refl _

≲-refl : ∀ {S T} (f : Trace S → Trace T) → (f ≲ f)
≲-refl f as = ⊑-refl (f as)

≃-impl-≲ : ∀ {S T} {f g : Trace S → Trace T} → (f ≃ g) → (f ≲ g)
≃-impl-≲ f≃g as = ≡-impl-⊑ (f≃g as)

-- Transitivity

⊑-trans : ∀ {S} {as bs cs : Trace S} → (as ⊑ bs) → (bs ⊑ cs) → (as ⊑ cs)
⊑-trans []       bs        = []
⊑-trans (a ∷ as) (.a ∷ bs) = (a ∷ ⊑-trans as bs)

≲-trans : ∀ {S T} {f g h : Trace S → Trace T} → (f ≲ g) → (g ≲ h) → (f ≲ h)
≲-trans f≲g g≲h as = ⊑-trans (f≲g as) (g≲h as)

-- Antisymmetry

⊑-antisym : ∀ {S} {as bs : Trace S} → (as ⊑ bs) → (bs ⊑ as) → (as ≡ bs)
⊑-antisym [] [] = refl
⊑-antisym (a ∷ as) (.a ∷ bs) = cong (_∷_ a) (⊑-antisym as bs)

≲-antisym : ∀ {S T} {f g : Trace S → Trace T} → (f ≲ g) → (g ≲ f) → (f ≃ g)
≲-antisym f≲g g≲f as = ⊑-antisym (f≲g as) (g≲f as)

-- ⊑ and ≲ form posets

⊑-poset : Session → Poset _ _ _
⊑-poset S = record
  { Carrier = Trace S
  ; _≈_ = _≡_
  ; _≤_ = _⊑_
  ; isPartialOrder = record
    { antisym = ⊑-antisym
    ; isPreorder = record
      { reflexive = ≡-impl-⊑
      ; trans = ⊑-trans
      ; ∼-resp-≈ = ((λ bs≡cs → subst₂ _⊑_ refl bs≡cs) , (λ as≡bs → subst₂ _⊑_ as≡bs refl))
      ; isEquivalence = Relation.Binary.Setoid.isEquivalence (≡-setoid (Trace S))
      }
    }
  }

≲-poset : Session → Session → Poset _ _ _
≲-poset S T = record
  { Carrier = (Trace S → Trace T)
  ; _≈_ = _≃_
  ; _≤_ = _≲_
  ; isPartialOrder = record
    { antisym = ≲-antisym
    ; isPreorder = record
      { reflexive = ≃-impl-≲
      ; trans = ≲-trans
      ; ∼-resp-≈ = (λ P≃Q P≲R as → subst₂ _⊑_ refl (P≃Q as) (P≲R as)) , λ Q≃R Q≲P as → subst₂ _⊑_ (Q≃R as) refl (Q≲P as)
      ; isEquivalence = record
        { refl = λ as → refl
        ; sym = λ P≃Q as → sym (P≃Q as)
        ; trans = λ P≃Q Q≃R as → trans (P≃Q as) (Q≃R as)
        }
      }
    }
  }

-- Inequational reasoning

module ⊑-Reasoning {S} where
  open Relation.Binary.PartialOrderReasoning (⊑-poset S) public renaming ( _≤⟨_⟩_ to _⊑⟨_⟩_ ; _≈⟨_⟩_ to _≡⟨_⟩_ )

module ≲-Reasoning {S T} where
  open Relation.Binary.PartialOrderReasoning (≲-poset S T) public renaming ( _≤⟨_⟩_ to _≲⟨_⟩_ ; _≈⟨_⟩_ to _≃⟨_⟩_ )

open ⊑-Reasoning

-- Processes are ⊑-monotone

P-monotone : ∀ {S T as bs} → (P : S ⇒ T) → (as ⊑ bs) → (⟦ P ⟧ as ⊑ ⟦ P ⟧ bs)
P-monotone (inp F)   []          = []
P-monotone (inp F)   (a ∷ as⊑bs) = P-monotone (♭ F a) as⊑bs
P-monotone (out b P) as⊑bs       = b ∷ P-monotone P as⊑bs
P-monotone done      as⊑bs       = as⊑bs

-- Composition is ≲-monotone

⟫-monotone : ∀ {S T U} (P₁ P₂ : S ⇒ T) (Q₁ Q₂ : T ⇒ U) →
  (⟦ P₁ ⟧ ≲ ⟦ P₂ ⟧) → (⟦ Q₁ ⟧ ≲ ⟦ Q₂ ⟧) →
    (⟦ P₁ ⟫ Q₁ ⟧ ≲ ⟦ P₂ ⟫ Q₂ ⟧)
⟫-monotone P₁ P₂ Q₁ Q₂ P₁≲P₂ Q₁≲Q₂ as =
  begin
    ⟦ P₁ ⟫ Q₁ ⟧ as
  ≡⟨ ⟫-semantics P₁ Q₁ as ⟩
    ⟦ Q₁ ⟧ (⟦ P₁ ⟧ as)
  ⊑⟨ P-monotone Q₁ (P₁≲P₂ as) ⟩
    ⟦ Q₁ ⟧ (⟦ P₂ ⟧ as)
  ⊑⟨ Q₁≲Q₂ (⟦ P₂ ⟧ as) ⟩
    ⟦ Q₂ ⟧ (⟦ P₂ ⟧ as)
  ≡⟨ sym (⟫-semantics P₂ Q₂ as) ⟩
    ⟦ P₂ ⟫ Q₂ ⟧ as
  ∎

max_stars_repo_name: ilya-fiveisky/agda-system-io

max_issues_repo_name: ilya-fiveisky/agda-system-io

max_forks_repo_name: ilya-fiveisky/agda-system-io