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

module Pi1Cat where

-- Proving that Pi with one level of interesting 2 path structure is a
-- symmetric rig 2-groupoid

open import Level using () renaming (zero to lzero)
open import Data.Unit using (tt)
open import Data.Product using (_,_)
open import Function using (flip)

open import Categories.Category using (Category)
open import Categories.Terminal using (OneC)
open import Categories.Groupoid using (Groupoid)
open import Categories.Monoidal using (Monoidal)
open import Categories.Monoidal.Helpers using (module MonoidalHelperFunctors)
open import Categories.Functor using (Functor)
open import Categories.Bifunctor using (Bifunctor)
open import Categories.NaturalIsomorphism using (NaturalIsomorphism)
open import Categories.Monoidal.Braided using (Braided)
open import Categories.Monoidal.Symmetric using (Symmetric)
open import Categories.RigCategory
  using (RigCategory; module BimonoidalHelperFunctors)
open import Categories.Bicategory using (Bicategory)

open import PiU using (U; PLUS; ZERO; TIMES; ONE)
open import PiLevel0
  using (_⟷_; id⟷; _◎_;
        !; !!;
        _⊕_;
        unite₊l; uniti₊l; unite₊r; uniti₊r;
        swap₊;
        assocr₊; assocl₊;
        _⊗_;
        unite⋆l; uniti⋆l; unite⋆r; uniti⋆r;
        swap⋆;
        assocr⋆; assocl⋆;
        absorbl; absorbr; factorzl; factorzr;
        dist; factor; distl; factorl)

open import PiLevel1 using (_⇔_; ⇔Equiv; triv≡; triv≡Equiv; 2!;
 id⇔; trans⇔; _⊡_;
 assoc◎l; idr◎l; idl◎l; linv◎l; rinv◎l;
 id⟷⊕id⟷⇔; hom⊕◎⇔; resp⊕⇔;
 unite₊l⇔r; uniti₊l⇔r; unite₊r⇔r; uniti₊r⇔r;
 assocr⊕r; assocl⊕l; triangle⊕l; pentagon⊕l;
 id⟷⊗id⟷⇔; hom⊗◎⇔; resp⊗⇔;
 uniter⋆⇔l; unitir⋆⇔l; uniter⋆⇔r; unitir⋆⇔r;
 assocr⊗r; assocl⊗l; triangle⊗l; pentagon⊗l;
 swapr₊⇔; unite₊l-coh-l; hexagonr⊕l; hexagonl⊕l;
 swapr⋆⇔; unite⋆l-coh-l; hexagonr⊗l; hexagonl⊗l;
 absorbl⇔l; factorzr⇔l; absorbr⇔l; factorzl⇔l;
 distl⇔l; factorl⇔l; dist⇔l; factor⇔l;
 swap₊distl⇔l; dist-swap⋆⇔l; assocl₊-dist-dist⇔l; assocl⋆-distl⇔l;
 fully-distribute⇔l; absorbr0-absorbl0⇔; absorbr⇔distl-absorb-unite;
 unite⋆r0-absorbr1⇔; absorbl≡swap⋆◎absorbr;
 absorbr⇔[assocl⋆◎[absorbr⊗id⟷]]◎absorbr;
 [id⟷⊗absorbr]◎absorbl⇔assocl⋆◎[absorbl⊗id⟷]◎absorbr;
 elim⊥-A[0⊕B]⇔l; elim⊥-1[A⊕B]⇔l;
-- for bicategory
 idr◎r; idl◎r; assoc◎r
 )

------------------------------------------------------------------------------
-- Pi1 is a category...

Pi1Cat : Category lzero lzero lzero
Pi1Cat = record
  { Obj = U
  ; _⇒_ = _⟷_
  ; _≡_ = _⇔_
  ; id = id⟷
  ; _∘_ = λ y⟷z x⟷y → x⟷y ◎ y⟷z
  ; assoc = assoc◎l
  ; identityˡ = idr◎l
  ; identityʳ = idl◎l
  ; equiv = ⇔Equiv
  ; ∘-resp-≡ = λ f g → g ⊡ f
  }

-- and a groupoid ...

Pi1Groupoid : Groupoid Pi1Cat
Pi1Groupoid = record
  { _⁻¹ = !
  ; iso = record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }

-- additive bifunctor and monoidal structure

⊕-bifunctor : Bifunctor Pi1Cat Pi1Cat Pi1Cat
⊕-bifunctor = record
  { F₀ = λ {(u , v) → PLUS u v}
  ; F₁ = λ {(x⟷y , z⟷w) → x⟷y ⊕ z⟷w }
  ; identity = id⟷⊕id⟷⇔
  ; homomorphism = hom⊕◎⇔
  ; F-resp-≡ = λ {(x , y) → resp⊕⇔ x y}
  }

module ⊎h = MonoidalHelperFunctors Pi1Cat ⊕-bifunctor ZERO

-- note how powerful linv◎l/rinv◎l are in iso below

0⊕x≡x : NaturalIsomorphism ⊎h.id⊗x ⊎h.x
0⊕x≡x = record
  { F⇒G = record { η = λ X → unite₊l ; commute = λ f → unite₊l⇔r }
  ; F⇐G = record { η = λ X → uniti₊l ; commute = λ f → uniti₊l⇔r }
  ; iso = λ X → record { isoˡ = linv◎l; isoʳ = rinv◎l }
  }

x⊕0≡x : NaturalIsomorphism ⊎h.x⊗id ⊎h.x
x⊕0≡x = record
  { F⇒G = record { η = λ X → unite₊r ; commute = λ f → unite₊r⇔r }
  ; F⇐G = record { η = λ X → uniti₊r ; commute = λ f → uniti₊r⇔r }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }

[x⊕y]⊕z≡x⊕[y⊕z] : NaturalIsomorphism ⊎h.[x⊗y]⊗z ⊎h.x⊗[y⊗z]
[x⊕y]⊕z≡x⊕[y⊕z] = record
  { F⇒G = record
    { η = λ X → assocr₊
    ; commute = λ f → assocr⊕r
    }
  ; F⇐G = record
    { η = λ X → assocl₊
    ; commute = λ f → assocl⊕l
    }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }

-- and a monoidal category (additive)

M⊕ : Monoidal Pi1Cat
M⊕ = record
  { ⊗ = ⊕-bifunctor
  ; id = ZERO
  ; identityˡ = 0⊕x≡x
  ; identityʳ = x⊕0≡x
  ; assoc = [x⊕y]⊕z≡x⊕[y⊕z]
  ; triangle = triangle⊕l
  ; pentagon = pentagon⊕l
  }

-- multiplicative bifunctor and monoidal structure

⊗-bifunctor : Bifunctor Pi1Cat Pi1Cat Pi1Cat
⊗-bifunctor = record
  { F₀ = λ {(u , v) → TIMES u v}
  ; F₁ = λ {(x⟷y , z⟷w) → x⟷y ⊗ z⟷w }
  ; identity = id⟷⊗id⟷⇔
  ; homomorphism = hom⊗◎⇔
  ; F-resp-≡ = λ {(x , y) → resp⊗⇔ x y}
  }

module ×h = MonoidalHelperFunctors Pi1Cat ⊗-bifunctor ONE

1⊗x≡x : NaturalIsomorphism ×h.id⊗x ×h.x
1⊗x≡x = record
  { F⇒G = record
    { η = λ X → unite⋆l
    ; commute = λ f → uniter⋆⇔l }
  ; F⇐G = record
    { η = λ X → uniti⋆l
    ; commute = λ f → unitir⋆⇔l }
  ; iso = λ X → record { isoˡ = linv◎l; isoʳ = rinv◎l }
  }

x⊗1≡x : NaturalIsomorphism ×h.x⊗id ×h.x
x⊗1≡x = record
  { F⇒G = record
    { η = λ X → unite⋆r
    ; commute = λ f → uniter⋆⇔r
    }
  ; F⇐G = record
    { η = λ X → uniti⋆r
    ; commute = λ f → unitir⋆⇔r
    }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }

[x⊗y]⊗z≡x⊗[y⊗z] : NaturalIsomorphism ×h.[x⊗y]⊗z ×h.x⊗[y⊗z]
[x⊗y]⊗z≡x⊗[y⊗z] = record
  { F⇒G = record
    { η = λ X → assocr⋆
    ; commute = λ f → assocr⊗r
    }
  ; F⇐G = record
    { η = λ X → assocl⋆
    ; commute = λ f → assocl⊗l
    }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }

-- and a monoidal category (multiplicative)

M⊗ : Monoidal Pi1Cat
M⊗ = record
  { ⊗ = ⊗-bifunctor
  ; id = ONE
  ; identityˡ = 1⊗x≡x
  ; identityʳ = x⊗1≡x
  ; assoc = [x⊗y]⊗z≡x⊗[y⊗z]
  ; triangle = triangle⊗l
  ; pentagon = pentagon⊗l
  }

x⊕y≡y⊕x : NaturalIsomorphism ⊎h.x⊗y ⊎h.y⊗x
x⊕y≡y⊕x = record
  { F⇒G = record { η = λ X → swap₊ ; commute = λ f → swapr₊⇔ }
  ; F⇐G = record { η = λ X → swap₊ ; commute = λ f → swapr₊⇔ }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l } }

BM⊕ : Braided M⊕
BM⊕ = record
  { braid = x⊕y≡y⊕x
  ; unit-coh = unite₊l-coh-l
  ; hexagon₁ = hexagonr⊕l
  ; hexagon₂ = hexagonl⊕l
  }

x⊗y≡y⊗x : NaturalIsomorphism ×h.x⊗y ×h.y⊗x
x⊗y≡y⊗x = record
  { F⇒G = record { η = λ X → swap⋆ ; commute = λ f → swapr⋆⇔ }
  ; F⇐G = record { η = λ X → swap⋆ ; commute = λ f → swapr⋆⇔ }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l } }

BM⊗ : Braided M⊗
BM⊗ = record
  { braid = x⊗y≡y⊗x
  ; unit-coh = unite⋆l-coh-l
  ; hexagon₁ = hexagonr⊗l
  ; hexagon₂ = hexagonl⊗l
  }

-- with both monoidal structures being symmetric

SBM⊕ : Symmetric BM⊕
SBM⊕ = record { symmetry = linv◎l }

SBM⊗ : Symmetric BM⊗
SBM⊗ = record { symmetry = rinv◎l }

module r = BimonoidalHelperFunctors BM⊕ BM⊗

x⊗0≡0 : NaturalIsomorphism r.x⊗0 r.0↑
x⊗0≡0 = record
  { F⇒G = record
    { η = λ X → absorbl
    ; commute = λ f → absorbl⇔l
    }
  ; F⇐G = record
    { η = λ X → factorzr
    ; commute = λ f → factorzr⇔l
    }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }

0⊗x≡0 : NaturalIsomorphism r.0⊗x r.0↑
0⊗x≡0 = record
  { F⇒G = record { η = λ X → absorbr ; commute = λ f → absorbr⇔l }
  ; F⇐G = record { η = λ X → factorzl ; commute = λ f → factorzl⇔l }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }

x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] : NaturalIsomorphism r.x⊗[y⊕z] r.[x⊗y]⊕[x⊗z]
x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] = record
  { F⇒G = record { η = λ _ → distl ; commute = λ f → distl⇔l }
  ; F⇐G = record { η = λ _ → factorl ; commute = λ f → factorl⇔l }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }

[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] : NaturalIsomorphism r.[x⊕y]⊗z r.[x⊗z]⊕[y⊗z]
[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] = record
  { F⇒G = record { η = λ X → dist ; commute = λ f → dist⇔l }
  ; F⇐G = record { η = λ X → factor ; commute = λ f → factor⇔l }
  ; iso = λ X → record { isoˡ = linv◎l ; isoʳ = rinv◎l }
  }

-- and the multiplicative structure distributing over the additive one

Pi1Rig : RigCategory SBM⊕ SBM⊗
Pi1Rig = record
  { distribₗ = x⊗[y⊕z]≡[x⊗y]⊕[x⊗z]
  ; distribᵣ = [x⊕y]⊗z≡[x⊗z]⊕[y⊗z]
  ; annₗ = 0⊗x≡0
  ; annᵣ = x⊗0≡0
  ; laplazaI = swap₊distl⇔l
  ; laplazaII = dist-swap⋆⇔l
  ; laplazaIV = assocl₊-dist-dist⇔l
  ; laplazaVI = assocl⋆-distl⇔l
  ; laplazaIX = fully-distribute⇔l
  ; laplazaX = absorbr0-absorbl0⇔
  ; laplazaXI = absorbr⇔distl-absorb-unite
  ; laplazaXIII = unite⋆r0-absorbr1⇔
  ; laplazaXV = absorbl≡swap⋆◎absorbr
  ; laplazaXVI =  absorbr⇔[assocl⋆◎[absorbr⊗id⟷]]◎absorbr
  ; laplazaXVII = [id⟷⊗absorbr]◎absorbl⇔assocl⋆◎[absorbl⊗id⟷]◎absorbr
  ; laplazaXIX = elim⊥-A[0⊕B]⇔l
  ; laplazaXXIII = elim⊥-1[A⊕B]⇔l
  }

------------------------------------------------------------------------------
-- The morphisms of the Pi1 category have structure; they form a
-- category, something like another Symmetric Rig Groupoid but more
-- general

⟷Cat : (t₁ t₂ : U) → Category lzero lzero lzero
⟷Cat t₁ t₂ = record
  { Obj = t₁ ⟷ t₂
  ; _⇒_ = _⇔_
  ; _≡_ = triv≡
  ; id = id⇔
  ; _∘_ = flip trans⇔
  ; assoc = tt
  ; identityˡ = tt
  ; identityʳ = tt
  ; equiv = triv≡Equiv
  ; ∘-resp-≡ = λ _ _ → tt
  }

⟷Groupoid : (t₁ t₂ : U) → Groupoid (⟷Cat t₁ t₂)
⟷Groupoid t₁ t₂ = record
  { _⁻¹ = 2!
  ; iso = record { isoˡ = tt ; isoʳ = tt }
  }

-- These feel like the right notions of bifunctor but of course they
-- are relating different categories so the rest of the development to
-- RigCategory would need to be generalized if we were to use these
-- definitions of bifunctors.

⊕⟷-bifunctor : (t₁ t₂ t₃ t₄ : U) →
  Bifunctor (⟷Cat t₁ t₂) (⟷Cat t₃ t₄) (⟷Cat (PLUS t₁ t₃) (PLUS t₂ t₄))
⊕⟷-bifunctor t₁ t₂ t₃ t₄ = record
  { F₀ = λ {(f , g) → f ⊕ g }
  ; F₁ = λ {(α , β) → resp⊕⇔ α β }
  ; identity = tt
  ; homomorphism = tt
  ; F-resp-≡ = λ _ → tt
  }

⊗⟷-bifunctor : (t₁ t₂ t₃ t₄ : U) →
  Bifunctor (⟷Cat t₁ t₂) (⟷Cat t₃ t₄) (⟷Cat (TIMES t₁ t₃) (TIMES t₂ t₄))
⊗⟷-bifunctor t₁ t₂ t₃ t₄ = record
  { F₀ = λ {(f , g) → f ⊗ g }
  ; F₁ = λ {(α , β) → resp⊗⇔ α β }
  ; identity = tt
  ; homomorphism = tt
  ; F-resp-≡ = λ _ → tt
  }

------------------------------------------------------------------------------
-- We have a 2-category but NOT a strict one.

idF : {t : U} → Functor {lzero} {lzero} {lzero} OneC (⟷Cat t t)
idF {t} = record
  { F₀ = λ _ → id⟷ {t}
  ; F₁ = λ _ → id⇔
  ; identity = tt
  ; homomorphism = tt
  ; F-resp-≡ = λ _ → tt
  }

∘-bifunctor : {t₁ t₂ t₃ : U} → Bifunctor (⟷Cat t₂ t₃) (⟷Cat t₁ t₂) (⟷Cat t₁ t₃)
∘-bifunctor = record
  { F₀ = λ {(f , g) → g ◎ f}
  ; F₁ = λ {(α , β) → β ⊡ α}
  ; identity = tt
  ; homomorphism = tt
  ; F-resp-≡ = λ _ → tt
  }

Pi1-Bicat : Bicategory lzero lzero lzero lzero
Pi1-Bicat = record
  { Obj = U
  ; _⇒_ = ⟷Cat
  ; id = idF
  ; —∘— = ∘-bifunctor
  ; λᵤ = record
    { F⇒G = record { η = λ X → idr◎l ; commute = λ {f → tt} }
    ; F⇐G = record { η = λ X → idr◎r ; commute = λ {X} {Y} f → tt }
    ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
    }
  ; ρᵤ = record
    { F⇒G = record { η = λ X → idl◎l ; commute = λ {X} {Y} f → tt }
    ; F⇐G = record { η = λ X → idl◎r ; commute = λ {X} {Y} f → tt }
    ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
    }
  ; α = record
    { F⇒G = record { η = λ _ → assoc◎r ; commute = λ {X} {Y} f → tt }
    ; F⇐G = record { η = λ _ → assoc◎l ; commute = λ {X} {Y} f → tt }
    ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
    }
  ; triangle = λ {A} {B} {C} f g → tt
  ; pentagon = λ {A} {B} {C} {D} {E} f g h i → tt
  }

{--
Here is why Pi1 is NOT a strict 2-Category:

Pi1-2Cat : 2-Category lzero lzero lzero lzero
Pi1-2Cat = record
  { Obj = U
  ; _⇒_ = ⟷Cat
  ; id = idF
  ; —∘— = ∘-bifunctor
  ; assoc = {!!}
  ; identityˡ = {!!} }

The definition of 2-Category is STRICT, which means that for proof of
identityˡ requires the following diagram to commute:

Assume the following 1-paths:

c₁ c₂ : A ⟷ B
id_B  : B ⟷ B

and the following 2-paths:

α       : c₁ ⇔ c₂
id_id_B : id_B ⇔ id_B

We can construct the 2-path:

α ⊡ id_id_B : c₁ ◎ id_B ⇔ c₂ ◎ id_B

The property identityˡ requires that there is a 3-path between

  α   and   α ⊡ id_id_B

and indeed there are "equivalent" in some sense as:

  α ⊡ id_id_B : c₁ ◎ id_B ⇔ c₂ ◎ id_B

can be viewed as having the equivalent type:

  α ⊡ id_id_B : c₁ ⇔ c₂

and we identify all 2-paths of the same type.

This reasoning however requires that identityˡ is asserted up to the
2-paths relating c₁ ◎ id_B and c₁ on one hand and c₂ ◎ id_B and c₂ on
the other hand.

Formally the nlab page http://ncatlab.org/nlab/show/2-category
explains this as follows:

  For some purposes, strict 2-categories are too strict: one would
  like to allow composition of morphisms to be associative and unital
  only up to coherent invertible 2-morphisms. A direct generalization
  of the above “enriched” definition produces the classical notion of
  bicategory.

So to conclude what we really need is a weak version of 2-Category
which is known as 'bicategory'.

--}

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums of nullary relations
------------------------------------------------------------------------

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

module Relation.Nullary.Sum where

open import Data.Sum
open import Data.Empty
open import Level
open import Relation.Nullary

-- Some properties which are preserved by _⊎_.

infixr 1 _¬-⊎_ _⊎-dec_

_¬-⊎_ : ∀ {p q} {P : Set p} {Q : Set q} →
        ¬ P → ¬ Q → ¬ (P ⊎ Q)
(¬p ¬-⊎ ¬q) (inj₁ p) = ¬p p
(¬p ¬-⊎ ¬q) (inj₂ q) = ¬q q

_⊎-dec_ : ∀ {p q} {P : Set p} {Q : Set q} →
          Dec P → Dec Q → Dec (P ⊎ Q)
yes p ⊎-dec _     = yes (inj₁ p)
_     ⊎-dec yes q = yes (inj₂ q)
no ¬p ⊎-dec no ¬q = no helper
  where
  helper : _ ⊎ _ → ⊥
  helper (inj₁ p) = ¬p p
  helper (inj₂ q) = ¬q q

ext: agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to addition of integers
------------------------------------------------------------------------

module Data.Integer.Addition.Properties where

open import Algebra
import Algebra.FunctionProperties
open import Algebra.Structures
open import Data.Integer hiding (suc)
open import Data.Nat using (suc; zero) renaming (_+_ to _ℕ+_)
import Data.Nat.Properties as ℕ
open import Relation.Binary.PropositionalEquality

open Algebra.FunctionProperties (_≡_ {A = ℤ})
open CommutativeSemiring ℕ.commutativeSemiring
  using (+-comm; +-assoc; +-identity)

------------------------------------------------------------------------
-- Addition and zero form a commutative monoid

private

  comm : Commutative _+_
  comm -[1+ a ] -[1+ b ] rewrite +-comm a b = refl
  comm (+   a ) (+   b ) rewrite +-comm a b = refl
  comm -[1+ _ ] (+   _ ) = refl
  comm (+   _ ) -[1+ _ ] = refl

  identityˡ : LeftIdentity (+ 0) _+_
  identityˡ -[1+ _ ] = refl
  identityˡ (+   _ ) = refl

  identityʳ : RightIdentity (+ 0) _+_
  identityʳ x rewrite comm x (+ 0) = identityˡ x

  distribˡ-⊖-+-neg : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (suc c ℕ+ a)
  distribˡ-⊖-+-neg _ zero    zero    = refl
  distribˡ-⊖-+-neg _ zero    (suc _) = refl
  distribˡ-⊖-+-neg _ (suc _) zero    = refl
  distribˡ-⊖-+-neg a (suc b) (suc c) = distribˡ-⊖-+-neg a b c

  distribʳ-⊖-+-neg : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (suc a ℕ+ c)
  distribʳ-⊖-+-neg a b c
    rewrite comm -[1+ a ] (b ⊖ c)
          | distribˡ-⊖-+-neg a b c
          | +-comm a c
          = refl

  distribˡ-⊖-+-pos : ∀ a b c → b ⊖ c + + a ≡ b ℕ+ a ⊖ c
  distribˡ-⊖-+-pos _ zero    zero    = refl
  distribˡ-⊖-+-pos _ zero    (suc _) = refl
  distribˡ-⊖-+-pos _ (suc _) zero    = refl
  distribˡ-⊖-+-pos a (suc b) (suc c) = distribˡ-⊖-+-pos a b c

  distribʳ-⊖-+-pos : ∀ a b c → + a + (b ⊖ c) ≡ a ℕ+ b ⊖ c
  distribʳ-⊖-+-pos a b c
    rewrite comm (+ a) (b ⊖ c)
          | distribˡ-⊖-+-pos a b c
          | +-comm a b
          = refl

  assoc : Associative _+_
  assoc (+ zero) y z rewrite identityˡ      y  | identityˡ (y + z) = refl
  assoc x (+ zero) z rewrite identityʳ  x      | identityˡ      z  = refl
  assoc x y (+ zero) rewrite identityʳ (x + y) | identityʳ  y      = refl
  assoc -[1+ a ]  -[1+ b ]  (+ suc c) = sym (distribʳ-⊖-+-neg a c b)
  assoc -[1+ a ]  (+ suc b) (+ suc c) = distribˡ-⊖-+-pos (suc c) b a
  assoc (+ suc a) -[1+ b ]  -[1+ c ]  = distribˡ-⊖-+-neg c a b
  assoc (+ suc a) -[1+ b ] (+ suc c)
    rewrite distribˡ-⊖-+-pos (suc c) a b
          | distribʳ-⊖-+-pos (suc a) c b
          | sym (+-assoc a 1 c)
          | +-comm a 1
          = refl
  assoc (+ suc a) (+ suc b) -[1+ c ]
    rewrite distribʳ-⊖-+-pos (suc a) b c
          | sym (+-assoc a 1 b)
          | +-comm a 1
          = refl
  assoc -[1+ a ] -[1+ b ] -[1+ c ]
    rewrite sym (+-assoc a 1 (b ℕ+ c))
          | +-comm a 1
          | +-assoc a b c
          = refl
  assoc -[1+ a ] (+ suc b) -[1+ c ]
    rewrite distribʳ-⊖-+-neg a b c
          | distribˡ-⊖-+-neg c b a
          = refl
  assoc (+ suc a) (+ suc b) (+ suc c)
    rewrite +-assoc (suc a) (suc b) (suc c)
          = refl

  isSemigroup : IsSemigroup _≡_ _+_
  isSemigroup = record
    { isEquivalence = isEquivalence
    ; assoc         = assoc
    ; ∙-cong        = cong₂ _+_
    }

  isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ (+ 0)
  isCommutativeMonoid = record
    { isSemigroup = isSemigroup
    ; identityˡ   = identityˡ
    ; comm        = comm
    }

commutativeMonoid : CommutativeMonoid _ _
commutativeMonoid = record
  { Carrier             = ℤ
  ; _≈_                 = _≡_
  ; _∙_                 = _+_
  ; ε                   = + 0
  ; isCommutativeMonoid = isCommutativeMonoid
  }


text:
module Structure.Operator.Vector.Proofs where

open import Data.Tuple
open import Functional
open import Function.Equals
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Operator
open import Structure.Operator.Field
open import Structure.Operator.Group
open import Structure.Operator.Monoid
import      Structure.Operator.Names as Names
open import Structure.Operator.Proofs
open import Structure.Operator.Properties
open import Structure.Operator.Vector
open import Structure.Relator.Properties
open import Syntax.Transitivity
open import Type

module _
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ : Lvl.Level}
  {V : Type{ℓᵥ}}
  ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}}
  ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ᵥ_ : V → V → V}
  {_⋅ₛᵥ_ : S → V → V}
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  where

  module _ ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄ where
    open VectorSpace(vectorSpace)

    [⋅ₛᵥ]-absorberₗ : ∀{v} → (𝟎ₛ ⋅ₛᵥ v ≡ 𝟎ᵥ)
    [⋅ₛᵥ]-absorberₗ {v} = cancellationᵣ(_+ᵥ_) ⦃ One.cancellationᵣ-by-associativity-inverse ⦄ $
      (𝟎ₛ ⋅ₛᵥ v) +ᵥ (𝟎ₛ ⋅ₛᵥ v) 🝖-[ [⋅ₛᵥ][+ₛ][+ᵥ]-distributivityᵣ ]-sym
      (𝟎ₛ +ₛ 𝟎ₛ) ⋅ₛᵥ v         🝖-[ congruence₂ₗ(_⋅ₛᵥ_)(v) (identityₗ(_+ₛ_)(𝟎ₛ)) ]
      𝟎ₛ ⋅ₛᵥ v                 🝖-[ identityₗ(_+ᵥ_)(𝟎ᵥ) ]-sym
      𝟎ᵥ +ᵥ (𝟎ₛ ⋅ₛᵥ v)         🝖-end

    [⋅ₛᵥ]-absorberᵣ : ∀{s} → (s ⋅ₛᵥ 𝟎ᵥ ≡ 𝟎ᵥ)
    [⋅ₛᵥ]-absorberᵣ {s} = cancellationᵣ(_+ᵥ_) ⦃ One.cancellationᵣ-by-associativity-inverse ⦄ $
      (s ⋅ₛᵥ 𝟎ᵥ) +ᵥ (s ⋅ₛᵥ 𝟎ᵥ) 🝖-[ distributivityₗ(_⋅ₛᵥ_)(_+ᵥ_) ]-sym
      s ⋅ₛᵥ (𝟎ᵥ +ᵥ 𝟎ᵥ)         🝖-[ congruence₂ᵣ(_⋅ₛᵥ_)(s) (identityₗ(_+ᵥ_)(𝟎ᵥ)) ]
      s ⋅ₛᵥ 𝟎ᵥ                 🝖-[ identityₗ(_+ᵥ_)(𝟎ᵥ) ]-sym
      𝟎ᵥ +ᵥ (s ⋅ₛᵥ 𝟎ᵥ)         🝖-end

    [⋅ₛᵥ]-negation : ∀{v} → ((−ₛ 𝟏ₛ) ⋅ₛᵥ v ≡ −ᵥ v)
    [⋅ₛᵥ]-negation {v} = _⊜_.proof (One.unique-inverseFunctionᵣ-by-id (intro p) [+ᵥ]-inverseᵣ) {v} where
      p : Names.InverseFunctionᵣ(_+ᵥ_) 𝟎ᵥ ((−ₛ 𝟏ₛ) ⋅ₛᵥ_)
      p{v} =
        v +ᵥ ((−ₛ 𝟏ₛ) ⋅ₛᵥ v)          🝖-[ congruence₂ₗ(_+ᵥ_) _ (identityₗ(_⋅ₛᵥ_)(𝟏ₛ)) ]-sym
        (𝟏ₛ ⋅ₛᵥ v) +ᵥ ((−ₛ 𝟏ₛ) ⋅ₛᵥ v) 🝖-[ [⋅ₛᵥ][+ₛ][+ᵥ]-distributivityᵣ ]-sym
        (𝟏ₛ +ₛ (−ₛ 𝟏ₛ))⋅ₛᵥ v          🝖-[ congruence₂ₗ(_⋅ₛᵥ_) v (inverseFunctionᵣ(_+ₛ_) ⦃ [∃]-intro _ ⦃ [+ₛ]-identityᵣ ⦄ ⦄ (−ₛ_)) ]
        𝟎ₛ ⋅ₛᵥ v                      🝖-[ [⋅ₛᵥ]-absorberₗ ]
        𝟎ᵥ                            🝖-end

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- ASR (2016-02-15). In the Makefile in test/compiler founded in the
-- 2.4.2.3 tag, this test used the options `+RTS -H1G -M1.5G -RTS`.

module AllStdLib where

-- Ensure that the entire standard library is compiled.
import README

open import Data.Unit.Base
open import Data.String
open import IO
import IO.Primitive as Prim

main : Prim.IO ⊤
main = run (putStrLn "Hello World!")


text:
module maybe where

open import level
open import eq
open import bool

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data maybe {ℓ}(A : Set ℓ) : Set ℓ where
  just : A → maybe A
  nothing : maybe A

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

_≫=maybe_ : ∀ {ℓ}{A B : Set ℓ} → maybe A → (A → maybe B) → maybe B
nothing ≫=maybe f = nothing
(just x) ≫=maybe f = f x

return-maybe : ∀ {ℓ}{A : Set ℓ} → A → maybe A
return-maybe a = just a

down-≡ : ∀{ℓ}{A : Set ℓ}{a a' : A} → just a ≡ just a' → a ≡ a'
down-≡ refl = refl

isJust : ∀{ℓ}{A : Set ℓ} → maybe A → 𝔹
isJust nothing = ff
isJust (just _) = tt

maybe-extract : ∀{ℓ}{A : Set ℓ} → (x : maybe A) → isJust x ≡ tt → A
maybe-extract (just x) p = x
maybe-extract nothing ()

maybe-map : ∀{ℓ}{A B : Set ℓ} → (A → B) → maybe A → maybe B
maybe-map f (just x) = just (f x)
maybe-map f nothing = nothing

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Reduction {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Reflexivity
open import Definition.LogicalRelation.Properties.Universe
open import Definition.LogicalRelation.Properties.Escape

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Weak head expansion of reducible types.
redSubst* : ∀ {A B l Γ}
          → Γ ⊢ A ⇒* B
          → Γ ⊩⟨ l ⟩ B
          → ∃ λ ([A] : Γ ⊩⟨ l ⟩ A)
          → Γ ⊩⟨ l ⟩ A ≡ B / [A]
redSubst* D (Uᵣ′ l′ l< ⊢Γ) rewrite redU* D =
  Uᵣ′ l′ l< ⊢Γ , U₌ PE.refl
redSubst* D (ℕᵣ [ ⊢B , ⊢ℕ , D′ ]) =
  let ⊢A = redFirst* D
  in  ℕᵣ ([ ⊢A , ⊢ℕ , D ⇨* D′ ]) , ιx (ℕ₌ D′)
redSubst* D (ne′ K [ ⊢B , ⊢K , D′ ] neK K≡K) =
  let ⊢A = redFirst* D
  in  (ne′ K [ ⊢A , ⊢K , D ⇨* D′ ] neK K≡K)
  ,  ιx (ne₌ _ [ ⊢B , ⊢K , D′ ] neK K≡K)
redSubst* D (Πᵣ′ F G [ ⊢B , ⊢ΠFG , D′ ] ⊢F ⊢G A≡A [F] [G] G-ext) =
  let ⊢A = redFirst* D
  in  (Πᵣ′ F G [ ⊢A , ⊢ΠFG , D ⇨* D′ ] ⊢F ⊢G A≡A [F] [G] G-ext)
  ,   (Π₌ _ _ D′ A≡A (λ ρ ⊢Δ → reflEq ([F] ρ ⊢Δ))
        (λ ρ ⊢Δ [a] → reflEq ([G] ρ ⊢Δ [a])))
redSubst* D (emb′ 0<1 x) with redSubst* D x
redSubst* D (emb′ 0<1 x) | y , y₁ = emb′ 0<1 y , ιx y₁

-- Weak head expansion of reducible terms.
redSubst*Term : ∀ {A t u l Γ}
              → Γ ⊢ t ⇒* u ∷ A
              → ([A] : Γ ⊩⟨ l ⟩ A)
              → Γ ⊩⟨ l ⟩ u ∷ A / [A]
              → Γ ⊩⟨ l ⟩ t ∷ A / [A]
              × Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
redSubst*Term t⇒u (Uᵣ′ .⁰ 0<1 ⊢Γ) (Uₜ A [ ⊢t , ⊢u , d ] typeA A≡A [u]) =
  let [d]  = [ ⊢t , ⊢u , d ]
      [d′] = [ redFirst*Term t⇒u , ⊢u , t⇒u ⇨∷* d ]
      q = redSubst* (univ* t⇒u) (univEq (Uᵣ′ ⁰ 0<1 ⊢Γ) (Uₜ A [d] typeA A≡A [u]))
  in Uₜ A [d′] typeA A≡A (proj₁ q)
  ,  Uₜ₌ A A [d′] [d] typeA typeA A≡A (proj₁ q) [u] (proj₂ q)
redSubst*Term t⇒u (ℕᵣ D) (ιx (ℕₜ n [ ⊢u , ⊢n , d ] n≡n prop)) =
  let A≡ℕ  = subset* (red D)
      ⊢t   = conv (redFirst*Term t⇒u) A≡ℕ
      t⇒u′ = conv* t⇒u A≡ℕ
  in ιx (ℕₜ n [ ⊢t , ⊢n , t⇒u′ ⇨∷* d ] n≡n prop)
  , ιx (ℕₜ₌ n n [ ⊢t , ⊢n , t⇒u′ ⇨∷* d ] [ ⊢u , ⊢n , d ]
          n≡n (reflNatural-prop prop))
redSubst*Term t⇒u (ne′ K D neK K≡K) (ιx (neₜ k [ ⊢t , ⊢u , d ] (neNfₜ neK₁ ⊢k k≡k))) =
  let A≡K  = subset* (red D)
      [d]  = [ ⊢t , ⊢u , d ]
      [d′] = [ conv (redFirst*Term t⇒u) A≡K , ⊢u , conv* t⇒u A≡K ⇨∷* d ]
  in ιx (neₜ k [d′] (neNfₜ neK₁ ⊢k k≡k)) , ιx (neₜ₌ k k [d′] [d] (neNfₜ₌ neK₁ neK₁ k≡k))
redSubst*Term {A} {t} {u} {l} {Γ} t⇒u (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                  (Πₜ f [ ⊢t , ⊢u , d ] funcF f≡f [f] [f]₁) =
  let A≡ΠFG = subset* (red D)
      t⇒u′  = conv* t⇒u A≡ΠFG
      [d]  = [ ⊢t , ⊢u , d ]
      [d′] = [ conv (redFirst*Term t⇒u) A≡ΠFG , ⊢u , conv* t⇒u A≡ΠFG ⇨∷* d ]
  in  Πₜ f [d′] funcF f≡f [f] [f]₁
  ,   Πₜ₌ f f [d′] [d] funcF funcF f≡f
          (Πₜ f [d′] funcF f≡f [f] [f]₁)
          (Πₜ f [d] funcF f≡f [f] [f]₁)
          (λ [ρ] ⊢Δ [a] → reflEqTerm ([G] [ρ] ⊢Δ [a]) ([f]₁ [ρ] ⊢Δ [a]))
redSubst*Term t⇒u (emb′ 0<1 x) (ιx [u]) =
  let x = redSubst*Term t⇒u x [u] in
  ιx (proj₁ x) , ιx (proj₂ x)

-- Weak head expansion of reducible types with single reduction step.
redSubst : ∀ {A B l Γ}
         → Γ ⊢ A ⇒ B
         → Γ ⊩⟨ l ⟩ B
         → ∃ λ ([A] : Γ ⊩⟨ l ⟩ A)
         → Γ ⊩⟨ l ⟩ A ≡ B / [A]
redSubst A⇒B [B] = redSubst* (A⇒B ⇨ id (escape [B])) [B]

-- Weak head expansion of reducible terms with single reduction step.
redSubstTerm : ∀ {A t u l Γ}
             → Γ ⊢ t ⇒ u ∷ A
             → ([A] : Γ ⊩⟨ l ⟩ A)
             → Γ ⊩⟨ l ⟩ u ∷ A / [A]
             → Γ ⊩⟨ l ⟩ t ∷ A / [A]
             × Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
redSubstTerm t⇒u [A] [u] = redSubst*Term (t⇒u ⇨ id (escapeTerm [A] [u])) [A] [u]

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module Preliminary where

  open import Prelude public

  ∃_ : ∀ {a b} {A : Set a} (B : A → Set b) → Set (a ⊔ b)
  ∃_ = Σ _

  data IsYes {a} {P : Set a} : Dec P → Set a where
    yes : (p : P) → IsYes (yes p)

  getProof : ∀ {a} {P : Set a} → {d : Dec P} → IsYes d → P
  getProof (yes p) = p

  add-zero : ∀ n → n ≡ n +N 0
  add-zero zero = refl
  add-zero (suc n) = cong suc (add-zero n)

  _≢_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
  a ≢ b = ¬ (a ≡ b)


text:
-- Andreas, 2014-08-19, issue reported by zcarterc
-- {-# OPTIONS -v tc.meta.assign:10 -v tc.constr.findInScope:10 #-}
-- {-# OPTIONS -v tc.constr.findInScope:49 #-}
-- {-# OPTIONS --show-implicit #-}
module Issue1254 where

open import Agda.Primitive

record Inhabited {i : Level} (carrier : Set i) : Set i where
  field
    elem : carrier

open Inhabited {{...}}

record Wrap {i : Level} (carrier : Set i) : Set i where
  field
    wrap-inhabited : Inhabited carrier

instance
  wrap-as-inhabited : ∀ {i : Level} {carrier : Set i} → Wrap carrier → Inhabited carrier
  wrap-as-inhabited cat = Wrap.wrap-inhabited cat

postulate
  Nat : Set
  one : Nat

instance
  monoid-Nat : Wrap Nat
  monoid-Nat = record { wrap-inhabited = record { elem = one } }

-- This is what caused the crash.
op : Nat
op = elem

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module Cubical.Algebra.Group.EilenbergMacLane1 where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.GroupoidLaws renaming (assoc to ∙assoc)
open import Cubical.Foundations.Path
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Data.Unit
open import Cubical.Data.Sigma
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec; elim to trElim)
open import Cubical.HITs.EilenbergMacLane1

private
  variable ℓ : Level

module _ (Ĝ : Group ℓ) where
  private
    G = fst Ĝ
  open GroupStr (snd Ĝ)

  emloop-id : emloop 1g ≡ refl
  emloop-id =
    emloop 1g                                 ≡⟨ rUnit (emloop 1g) ⟩
    emloop 1g ∙ refl                          ≡⟨ cong (emloop 1g ∙_) (rCancel (emloop 1g) ⁻¹) ⟩
    emloop 1g ∙ (emloop 1g ∙ (emloop 1g) ⁻¹)  ≡⟨ ∙assoc _ _ _ ⟩
    (emloop 1g ∙ emloop 1g) ∙ (emloop 1g) ⁻¹  ≡⟨ cong (_∙ emloop 1g ⁻¹)
                                                   ((emloop-comp Ĝ 1g 1g) ⁻¹) ⟩
    emloop (1g · 1g) ∙ (emloop 1g) ⁻¹         ≡⟨ cong (λ g → emloop {Group = Ĝ} g
                                                             ∙ (emloop 1g) ⁻¹)
                                                      (rid 1g) ⟩
    emloop 1g ∙ (emloop 1g) ⁻¹                ≡⟨ rCancel (emloop 1g) ⟩
    refl ∎

  emloop-inv : (g : G) → emloop (inv g) ≡ (emloop g) ⁻¹
  emloop-inv g =
    emloop (inv g)                              ≡⟨ rUnit (emloop (inv g)) ⟩
    emloop (inv g) ∙ refl                       ≡⟨ cong (emloop (inv g) ∙_)
                                                      (rCancel (emloop g) ⁻¹) ⟩
    emloop (inv g) ∙ (emloop g ∙ (emloop g) ⁻¹) ≡⟨ ∙assoc _ _ _ ⟩
    (emloop (inv g) ∙ emloop g) ∙ (emloop g) ⁻¹ ≡⟨ cong (_∙ emloop g ⁻¹)
                                                      ((emloop-comp Ĝ (inv g) g) ⁻¹) ⟩
    emloop (inv g · g) ∙ (emloop g) ⁻¹          ≡⟨ cong (λ h → emloop {Group = Ĝ} h
                                                            ∙ (emloop g) ⁻¹)
                                                      (invl g) ⟩
    emloop 1g ∙ (emloop g) ⁻¹                 ≡⟨ cong (_∙ (emloop g) ⁻¹) emloop-id ⟩
    refl ∙ (emloop g) ⁻¹                      ≡⟨ (lUnit ((emloop g) ⁻¹)) ⁻¹ ⟩
    (emloop g) ⁻¹ ∎

  isGroupoidEM₁ : isGroupoid (EM₁ Ĝ)
  isGroupoidEM₁ = emsquash

  isConnectedEM₁ : isConnected 2 (EM₁ Ĝ)
  isConnectedEM₁ = ∣ embase ∣ , h
    where
      h : (y : hLevelTrunc 2 (EM₁ Ĝ)) → ∣ embase ∣ ≡ y
      h = trElim (λ y → isOfHLevelSuc 1 (isOfHLevelTrunc 2 ∣ embase ∣ y))
            (elimProp Ĝ (λ x → isOfHLevelTrunc 2 ∣ embase ∣ ∣ x ∣) refl)

  {- since we write composition in diagrammatic order,
     and function composition in the other order,
     we need right multiplication here -}
  rightEquiv : (g : G) → G ≃ G
  rightEquiv g = isoToEquiv isom
    where
    isom : Iso G G
    isom .Iso.fun = _· g
    isom .Iso.inv = _· inv g
    isom .Iso.rightInv h =
      (h · inv g) · g ≡⟨ (assoc h (inv g) g) ⁻¹ ⟩
        h · inv g · g ≡⟨ cong (h ·_) (invl g) ⟩
             h · 1g ≡⟨ rid h ⟩ h ∎
    isom .Iso.leftInv h =
      (h · g) · inv g ≡⟨ (assoc h g (inv g)) ⁻¹ ⟩
        h · g · inv g ≡⟨ cong (h ·_) (invr g) ⟩
             h · 1g ≡⟨ rid h ⟩ h ∎

  compRightEquiv : (g h : G)
    → compEquiv (rightEquiv g) (rightEquiv h) ≡ rightEquiv (g · h)
  compRightEquiv g h = equivEq (funExt (λ x → (assoc x g h) ⁻¹))

  CodesSet : EM₁ Ĝ → hSet ℓ
  CodesSet = rec Ĝ (isOfHLevelTypeOfHLevel 2) (G , is-set) RE REComp
    where
      RE : (g : G) → Path (hSet ℓ) (G , is-set) (G , is-set)
      RE g = Σ≡Prop (λ X → isPropIsOfHLevel {A = X} 2) (ua (rightEquiv g))

      lemma₁ : (g h : G) → Square
        (ua (rightEquiv g)) (ua (rightEquiv (g · h)))
        refl (ua (rightEquiv h))
      lemma₁ g h = invEq
                   (Square≃doubleComp (ua (rightEquiv g)) (ua (rightEquiv (g · h)))
                     refl (ua (rightEquiv h)))
                   (ua (rightEquiv g) ∙ ua (rightEquiv h)
                       ≡⟨ (uaCompEquiv (rightEquiv g) (rightEquiv h)) ⁻¹ ⟩
                    ua (compEquiv (rightEquiv g) (rightEquiv h))
                       ≡⟨ cong ua (compRightEquiv g h) ⟩
                    ua (rightEquiv (g · h)) ∎)

      lemma₂ : {A₀₀ A₀₁ : hSet ℓ} (p₀₋ : A₀₀ ≡ A₀₁)
               {A₁₀ A₁₁ : hSet ℓ} (p₁₋ : A₁₀ ≡ A₁₁)
               (p₋₀ : A₀₀ ≡ A₁₀) (p₋₁ : A₀₁ ≡ A₁₁)
               (s : Square (cong fst p₀₋) (cong fst p₁₋) (cong fst p₋₀) (cong fst p₋₁))
               → Square p₀₋ p₁₋ p₋₀ p₋₁
      fst (lemma₂ p₀₋ p₁₋ p₋₀ p₋₁ s i j) = s i j
      snd (lemma₂ p₀₋ p₁₋ p₋₀ p₋₁ s i j) =
        isSet→SquareP {A = (λ i j → isSet (s i j))}
          (λ i j → isProp→isSet (isPropIsOfHLevel 2))
          (cong snd p₀₋) (cong snd p₁₋) (cong snd p₋₀) (cong snd p₋₁) i j

      REComp : (g h : G) → Square (RE g) (RE (g · h)) refl (RE h)
      REComp g h = lemma₂ (RE g) (RE (g · h)) refl (RE h) (lemma₁ g h)
  Codes : EM₁ Ĝ → Type ℓ
  Codes x = CodesSet x .fst

  encode : (x : EM₁ Ĝ) → embase ≡ x → Codes x
  encode x p = subst Codes p 1g

  decode : (x : EM₁ Ĝ) → Codes x → embase ≡ x
  decode = elimSet Ĝ (λ x → isOfHLevelΠ 2 (λ c → isGroupoidEM₁ (embase) x))
    emloop λ g → ua→ λ h → emcomp h g

  decode-encode : (x : EM₁ Ĝ) (p : embase ≡ x) → decode x (encode x p) ≡ p
  decode-encode x p = J (λ y q → decode y (encode y q) ≡ q)
    (emloop (transport refl 1g) ≡⟨ cong emloop (transportRefl 1g) ⟩
     emloop 1g ≡⟨ emloop-id ⟩ refl ∎) p

  encode-decode : (x : EM₁ Ĝ) (c : Codes x) → encode x (decode x c) ≡ c
  encode-decode = elimProp Ĝ (λ x → isOfHLevelΠ 1 (λ c → CodesSet x .snd _ _))
    λ g → encode embase (decode embase g) ≡⟨ refl ⟩
          encode embase (emloop g) ≡⟨ refl ⟩
          transport (ua (rightEquiv g)) 1g ≡⟨ uaβ (rightEquiv g) 1g ⟩
          1g · g ≡⟨ lid g ⟩
          g ∎

  ΩEM₁Iso : Iso (Path (EM₁ Ĝ) embase embase) G
  Iso.fun ΩEM₁Iso = encode embase
  Iso.inv ΩEM₁Iso = emloop
  Iso.rightInv ΩEM₁Iso = encode-decode embase
  Iso.leftInv ΩEM₁Iso = decode-encode embase

  ΩEM₁≡ : (Path (EM₁ Ĝ) embase embase) ≡ G
  ΩEM₁≡ = isoToPath ΩEM₁Iso

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
data A (B : Set) : Set where
module C where
  record D : Set where
module E (F : Set) (G : A F) where
  open C public using (module D)
module H (I : Set) (J : A I) where
  open E I J using ()

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module noetherian where

open import sn-calculus
open import Esterel.Lang
open import Esterel.Lang.Properties
open import Esterel.Context
open import Esterel.Context.Properties
open import Esterel.Environment
open import Esterel.Variable.Signal as Signal using (Signal)
open import Esterel.Variable.Shared as SharedVar using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar using (SeqVar)
open import Data.Nat as Nat
  using (ℕ ; zero ; suc ; _+_ ; _>_ ; _≤′_ ; _≤_ ; _*_ ; ≤′-refl)
open import Data.Nat.Properties
  using (s≤′s ; z≤′n ; m≤′m+n ; n≤′m+n ; ≤⇒pred≤)
open import Data.Nat.Properties.Simple using (+-comm ; +-assoc ; +-suc)
open import Data.MoreNatProp
open import Data.Sum as Sum using (inj₁ ; inj₂ ; _⊎_)
open import Data.Maybe using (just ; nothing)
open import Data.Product using (_×_ ; _,_ ; _,′_ ; proj₁)
open import Agda.Builtin.Equality using (refl ; _≡_)
open import Data.List using (List ; _∷_ ; [])
open import Data.Bool using (Bool ; true ; false)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Relation.Nullary
  using (Dec ; yes ; no ; ¬_)
open import Relation.Binary.PropositionalEquality
  using (sym ; inspect ; Reveal_·_is_ ; trans ; cong)
open import Data.Empty using (⊥-elim ; ⊥)

SM = SigMap.Map Signal.Status
ShM = ShrMap.Map (SharedVar.Status × ℕ)

is-unknownp : Signal.Status -> Bool
is-unknownp x = ⌊ x Signal.≟ₛₜ Signal.unknown ⌋

is-notreadyp : SharedVar.Status × ℕ -> Bool
is-notreadyp (SharedVar.ready , _) = false
is-notreadyp (SharedVar.new   , _) = true
is-notreadyp (SharedVar.old   , _) = true

is-notreadyp-status : SharedVar.Status -> Bool
is-notreadyp-status SharedVar.ready = false
is-notreadyp-status SharedVar.new = true
is-notreadyp-status SharedVar.old = true

is-notreadyp' : SharedVar.Status × ℕ -> Bool
is-notreadyp' x = is-notreadyp-status (proj₁ x)

hunch : ∀ x -> is-notreadyp x ≡ is-notreadyp' x
hunch (SharedVar.ready , proj₃) = refl
hunch (SharedVar.new , proj₃) = refl
hunch (SharedVar.old , proj₃) = refl

numstepsSig : SM -> ℕ
numstepsSig m = SigMap.count is-unknownp m

numstepsShr : ShM -> ℕ
numstepsShr m = ShrMap.count is-notreadyp m

numstepsθ : Env -> ℕ
numstepsθ (Θ sig₁ shr₁ var₁) = (numstepsSig sig₁) + (numstepsShr shr₁)

∥_∥s : Term -> ℕ
∥ nothin ∥s = 0
∥ pause ∥s = 0

{- one for stepping to ρ θ p
   one for (maybe) setting S to absent
   one for (maybe) this ρ mergeing with another one
   (same idea for `shared` and `var`) -}
∥ (signl S p) ∥s = suc (suc (suc (∥ p ∥s)))

∥ (present S ∣⇒ p ∣⇒ q) ∥s = suc (∥ p ∥s + ∥ q ∥s)
∥ (emit S) ∥s = 1
∥ (p ∥ q) ∥s = suc (∥ p ∥s + ∥ q ∥s)
∥ (loop p) ∥s = suc (suc (∥ p ∥s + ∥ p ∥s))
∥ (loopˢ p q) ∥s = suc (∥ p ∥s + ∥ q ∥s)
∥ (p >> q) ∥s = suc (∥ p ∥s + ∥ q ∥s)
∥ (suspend p S) ∥s = suc (∥ p ∥s)
∥ (trap p) ∥s = suc (∥ p ∥s)
∥ (exit x) ∥s = 0
∥ (shared s ≔ e in: p) ∥s = suc (suc (suc (∥ p ∥s)))
∥ (s ⇐ e) ∥s = 1
∥ (var x ≔ e in: p) ∥s = suc (suc (∥ p ∥s))
∥ (x ≔ e) ∥s = 1
∥ (if x ∣⇒ p ∣⇒ q) ∥s = suc (∥ p ∥s + ∥ q ∥s)
∥ (ρ⟨ θ , A ⟩· p) ∥s = suc (numstepsθ θ + ∥ p ∥s)

arith1 : ∀ a b c -> suc b ≤′ c -> suc (suc (a + b)) ≤′ suc (a + c)
arith1 a b c sucb≤′c rewrite sym (+-suc a b) = s≤′s (≤′+r {z = a} sucb≤′c)

arith2 : ∀ x y z -> suc x ≤′ y -> suc (suc (x + z)) ≤′ suc (y + z)
arith2 x y z sucx≤′y = s≤′s (≤′+l{z = z} sucx≤′y)

arith3 : ∀ x y z -> suc x ≤′ y -> suc (suc (z + x)) ≤′ suc (z + y)
arith3 x y z sucx≤′y rewrite sym (+-suc z x) = s≤′s (≤′+r {z = z} sucx≤′y)

arith4 : ∀ x y z -> suc (suc x + y + z) ≤′ suc (x + suc y + z)
arith4 x y z rewrite +-suc x y = s≤′s ≤′-refl

arith5 : ∀ x y -> suc x ≤′ y -> suc (suc (suc (x + x))) ≤′ suc (suc (y + y))
arith5 x y sucx≤′y rewrite sym (+-suc x x) =
  s≤′s (s≤′s (≤′+b x (suc x) y y (suc≤′⇒≤′ x y sucx≤′y)  sucx≤′y))

decompose∥∥s : ∀ E p -> ∥ E ⟦ p ⟧e ∥s ≡ ∥ E ⟦ nothin ⟧e ∥s + ∥ p ∥s
decompose∥∥s [] p = refl
decompose∥∥s (x ∷ E) p with decompose∥∥s E
decompose∥∥s (epar₁ q ∷ E) p | R
  rewrite R p
  | +-assoc (∥ E ⟦ nothin ⟧e ∥s) ∥ p ∥s  ∥ q ∥s
  | +-assoc (∥ E ⟦ nothin ⟧e ∥s) ∥ q ∥s  ∥ p ∥s
  | +-comm (∥ p ∥s) (∥ q ∥s)
  = cong suc refl
decompose∥∥s (epar₂ p ∷ E) p₁ | R
  rewrite R p₁
  | +-assoc ∥ p ∥s ∥ E ⟦ nothin ⟧e ∥s ∥ p₁ ∥s
  = cong suc refl
decompose∥∥s (eseq q ∷ E) p | R
  rewrite R p
  | +-assoc (∥ E ⟦ nothin ⟧e ∥s) ∥ p ∥s  ∥ q ∥s
  | +-assoc (∥ E ⟦ nothin ⟧e ∥s) ∥ q ∥s  ∥ p ∥s
  | +-comm (∥ p ∥s) (∥ q ∥s)
  = cong suc refl
decompose∥∥s (eloopˢ q ∷ E) p | R
  rewrite R p
  | +-assoc (∥ E ⟦ nothin ⟧e ∥s) ∥ p ∥s  ∥ q ∥s
  | +-assoc (∥ E ⟦ nothin ⟧e ∥s) ∥ q ∥s  ∥ p ∥s
  | +-comm (∥ p ∥s) (∥ q ∥s)
  = cong suc refl
decompose∥∥s (esuspend S ∷ E) p | R rewrite R p = refl
decompose∥∥s (etrap ∷ E) p | R rewrite R p = refl

eplug≤ : ∀ p q E ->
  ∥ p ∥s ≤′ ∥ q ∥s ->
  ∥ E ⟦ p ⟧e ∥s ≤′ ∥ E ⟦ q ⟧e ∥s
eplug≤ p q E ∥p∥s≤′∥q∥s
  rewrite decompose∥∥s E p | decompose∥∥s E q
  = ≤′+r{z = ∥ E ⟦ nothin ⟧e ∥s} ∥p∥s≤′∥q∥s

eplug< : ∀ p q E ->
  suc ∥ p ∥s ≤′ ∥ q ∥s ->
  suc (∥ (E ⟦ p ⟧e) ∥s) ≤′ (∥ (E ⟦ q ⟧e) ∥s)
eplug< p q E ∥p∥s<∥q∥s
  rewrite decompose∥∥s E p | decompose∥∥s E q
        | sym (+-suc ∥ E ⟦ nothin ⟧e ∥s  ∥ p ∥s)
  = ≤′+r{z = ∥ E ⟦ nothin ⟧e ∥s} ∥p∥s<∥q∥s

valuemax-norm : ∀ {p q} ->
  (donep : done p) -> (doneq : done q) ->
  (haltedporq : halted p ⊎ halted q) ->
  ∥ value-max donep doneq haltedporq ∥s ≤′ ∥ p ∥s + ∥ q ∥s
valuemax-norm (dhalted hnothin) (dhalted p/halted₁) _ = ≤′-refl
valuemax-norm (dhalted (hexit n)) (dhalted hnothin) _ = ≤′-refl
valuemax-norm (dhalted (hexit n)) (dhalted (hexit m)) _ = ≤′-refl
valuemax-norm (dhalted hnothin) (dpaused p/paused) _ = ≤′-refl
valuemax-norm{q = q} (dhalted (hexit n)) (dpaused p/paused) _ = m≤′m+n 0 ∥ q ∥s
valuemax-norm{p = p} (dpaused p/paused) (dhalted hnothin) _ = m≤′m+n ∥ p ∥s 0
valuemax-norm (dpaused p/paused) (dhalted (hexit n)) _ = z≤′n
valuemax-norm (dpaused p/paused) (dpaused p/paused₁) (inj₁ x) =
  ⊥-elim (halted-paused-disjoint x p/paused)
valuemax-norm (dpaused p/paused) (dpaused p/paused₁) (inj₂ y) =
  ⊥-elim (halted-paused-disjoint y p/paused₁)

halted-norm : ∀ {p} -> (haltedp : halted p) ->  ∥ ↓ haltedp ∥s ≡ 0
halted-norm hnothin = refl
halted-norm (hexit zero) = refl
halted-norm (hexit (suc n)) = refl

noetherian₁ :
  ∀ {p q} ->
  p sn⟶₁ q ->
  (suc (∥ q ∥s)) ≤′ (∥ p ∥s)
noetherian₁ (rpar-done-right{p}{q} haltedp doneq) =
  s≤′s (valuemax-norm (dhalted haltedp) doneq (inj₁ haltedp))
noetherian₁ (rpar-done-left{p}{q} donep haltedq) =
  s≤′s (valuemax-norm donep (dhalted haltedq) (inj₂ haltedq))
noetherian₁ (ris-present{θ}{S = S}{p = p}{q = q}{E = E} S∈ x x₁) with unplug x₁
... | refl =
  arith1 (numstepsθ θ)
         ∥ E ⟦ p ⟧e ∥s
         ∥ E ⟦ present S ∣⇒ p ∣⇒ q ⟧e ∥s
         (eplug< p (present S ∣⇒ p ∣⇒ q) E (s≤′s (m≤′m+n ∥ p ∥s ∥ q ∥s)))

noetherian₁ (ris-absent{θ}{S}{p = p}{q = q}{E = E} S∈ x x₁) with unplug x₁
... | refl =
  arith1 (numstepsθ θ)
         ∥ E ⟦ q ⟧e ∥s
         ∥ E ⟦ present S ∣⇒ p ∣⇒ q ⟧e ∥s
         (eplug< q (present S ∣⇒ p ∣⇒ q) E (s≤′s (n≤′m+n ∥ p ∥s ∥ q ∥s)))

noetherian₁ (remit {θ} {_} {S} {E} S∈ ¬S≡a x) with unplug x
noetherian₁ (remit {θ} {_} {S} {E} S∈ ¬S≡a x) | refl with
    is-unknownp (SigMap.lookup{k = S} (sig θ) S∈)
  | inspect is-unknownp (SigMap.lookup{k = S} (sig θ) S∈)
  | SigMap.lookup{k = S} (sig θ) S∈
  | inspect (SigMap.lookup{k = S} (sig θ)) S∈
... | true  | Reveal_·_is_.[ eq1 ] | Signal.present | Reveal_·_is_.[ eq ]
  rewrite eq = ⊥-elim (false-not-true eq1) where
  false-not-true : false ≡ true -> ⊥
  false-not-true ()
... | false | Reveal_·_is_.[ eq1 ] | Signal.absent  | Reveal_·_is_.[ eq ]
  = ⊥-elim (¬S≡a refl)
... | true  | Reveal_·_is_.[ eq1 ] | Signal.absent  | Reveal_·_is_.[ eq ]
  = ⊥-elim (¬S≡a refl)
... | false | Reveal_·_is_.[ eq1 ] | Signal.unknown | Reveal_·_is_.[ eq ]
  rewrite eq = ⊥-elim (true-not-false eq1) where
  true-not-false : true ≡ false -> ⊥
  true-not-false ()
noetherian₁ (remit {θ} {.(E ⟦ emit S ⟧e)} {S} {E} S∈ ¬S≡a x)
   | refl | false | Reveal_·_is_.[ eq1 ] | Signal.present | Reveal_·_is_.[ eq ]
   with sym (SigMap.getput-m S (sig θ) S∈)
... | updateθ-S-to-present≡θ rewrite eq | updateθ-S-to-present≡θ =
  arith1 (numstepsθ θ)
         ∥ E ⟦ nothin ⟧e ∥s
         ∥ E ⟦ emit S ⟧e ∥s
         (eplug< nothin (emit S) E ≤′-refl)
noetherian₁ (remit {θ} {.(E ⟦ emit S ⟧e)} {S} {E} S∈ ¬S≡a x)
  | refl | true  | Reveal_·_is_.[ eq1 ] | Signal.unknown | Reveal_·_is_.[ eq ]
  rewrite SigMap.change-one-count-goes-down
   (sig θ) is-unknownp
   S S∈ eq1 Signal.present refl =
   s≤′s (s≤′s (≤′+r {z = numstepsθ (set-sig{S} θ S∈ Signal.present)}
                    (eplug≤ nothin (emit S) E (Nat.≤′-step ≤′-refl))))

noetherian₁ rloop-unroll = ≤′-refl
noetherian₁ rseq-done = ≤′-refl
noetherian₁ (rseq-exit{q}) = s≤′s z≤′n
noetherian₁ (rloopˢ-exit{q}) = s≤′s z≤′n
noetherian₁ (rsuspend-done x) = ≤′-refl
noetherian₁ (rtrap-done{p} haltedp)
  rewrite halted-norm haltedp =
  s≤′s z≤′n
noetherian₁ (rraise-signal{p}{S}) = ans where
  oneunknown≡1 : ∀ S ->
     numstepsθ (Θ SigMap.[ S ↦ Signal.unknown ] [] []) ≡ 1
  oneunknown≡1 (zero Signal.ₛ) = refl
  oneunknown≡1 (suc n Signal.ₛ) = oneunknown≡1 (n Signal.ₛ)

  ans : suc (suc (numstepsθ (Θ SigMap.[ S ↦ Signal.unknown ] [] []) +  ∥ p ∥s))
     ≤′ suc (suc (suc ∥ p ∥s))
  ans rewrite oneunknown≡1 S = ≤′-refl

noetherian₁ (rraise-shared{θ}{_}{s}{e}{p}{E} e' x) with unplug x
... | refl =
  arith1 (numstepsθ θ)
         ∥ E ⟦ ρ⟨ [s,δe]-env  s (δ e') , WAIT ⟩· p ⟧e ∥s
         ∥ E ⟦ shared s ≔ e in: p ⟧e ∥s
         (eplug< (ρ⟨ [s,δe]-env s (δ e') , WAIT ⟩· p)
                 (shared s ≔ e in: p) E newθ≡1) where

   silly : ∀ s -> numstepsθ ([s,δe]-env s (δ e')) ≡ 1
   silly (zero SharedVar.ₛₕ) = refl
   silly (suc x₁ SharedVar.ₛₕ) = silly (x₁ SharedVar.ₛₕ)

   newθ≡1 : suc (suc (numstepsθ ([s,δe]-env s (δ e')) + ∥ p ∥s)) ≤′
            suc (suc (suc ∥ p ∥s))
   newθ≡1 rewrite silly s = ≤′-refl

noetherian₁ (rset-shared-value-old{θ}{_}{s}{e}{E} e' s∈ θ[s]≡old x) with unplug x
... | refl  = ans where

  snotready : is-notreadyp (ShrMap.lookup{k = s} (shr θ) s∈) ≡ true
  snotready rewrite hunch (ShrMap.lookup{k = s} (shr θ) s∈)
            | θ[s]≡old = refl

  θsame : numstepsθ (set-shr{s} θ s∈ (SharedVar.new) (δ e'))
        ≡ numstepsθ θ
  θsame rewrite
     ShrMap.change-nothing-count-stays-same
       (shr θ) is-notreadyp s s∈
       (SharedVar.new , δ e') snotready = refl

  ans : suc ∥ (ρ⟨ (set-shr{s} θ s∈ (SharedVar.new) (δ e')) , GO ⟩·
                 E ⟦ nothin ⟧e) ∥s ≤′
        ∥ ρ⟨ θ , GO ⟩· E ⟦ s ⇐ e ⟧e ∥s
  ans rewrite θsame =
    arith1 (numstepsθ θ)
            ∥ E ⟦ nothin ⟧e ∥s
            ∥ E ⟦ s ⇐ e ⟧e ∥s
            (eplug< nothin (s ⇐ e) E ≤′-refl)

noetherian₁ (rset-shared-value-new{θ}{_}{s}{e}{E} e' s∈ θ[s]≡new x) with unplug x
... | refl = ans where

  snotready : is-notreadyp (ShrMap.lookup{k = s} (shr θ) s∈) ≡ true
  snotready rewrite hunch (ShrMap.lookup{k = s} (shr θ) s∈)
            | θ[s]≡new = refl

  θsame : numstepsθ (set-shr{s} θ s∈ (SharedVar.new) (shr-vals{s} θ s∈ + δ e'))
        ≡ numstepsθ θ
  θsame rewrite
     ShrMap.change-nothing-count-stays-same
       (shr θ) is-notreadyp s s∈
       (SharedVar.new , shr-vals{s} θ s∈ + δ e') snotready = refl

  ans : suc ∥ (ρ⟨ (set-shr{s} θ s∈ (SharedVar.new) (shr-vals{s} θ s∈ + δ e')) , GO ⟩·
                 E ⟦ nothin ⟧e) ∥s ≤′
        ∥ ρ⟨ θ , GO ⟩· E ⟦ s ⇐ e ⟧e ∥s
  ans rewrite θsame =
     arith1 (numstepsθ θ)
            ∥ E ⟦ nothin ⟧e ∥s
            ∥ E ⟦ s ⇐ e ⟧e ∥s
            (eplug< nothin (s ⇐ e) E ≤′-refl)

noetherian₁ (rraise-var{θ}{r}{x}{p}{e}{E} e' x₁) with unplug x₁
... | refl =
  arith1 (numstepsθ θ)
         ∥ E ⟦ ρ⟨ [x,δe]-env x (δ e') , WAIT ⟩· p ⟧e ∥s
         ∥ E ⟦ var x ≔ e in: p ⟧e ∥s
         (eplug< (ρ⟨ [x,δe]-env x (δ e') , WAIT ⟩· p)
                 (var x ≔ e in: p)
                 E
                 ≤′-refl)
noetherian₁ (rset-var{θ}{_}{x}{e}{E} x∈ e' x₁) with unplug x₁
... | refl =
  arith1 (numstepsθ θ)
          ∥ E ⟦ nothin ⟧e ∥s
          ∥ E ⟦ x ≔ e ⟧e ∥s
          (eplug< nothin (x ≔ e) E ≤′-refl)
noetherian₁ (rif-false{θ}{p = p}{q = q}{x = x}{E = E} x∈ x₁ x₂) with unplug x₂
... | refl = arith1 (numstepsθ θ)
                    ∥ E ⟦ q ⟧e ∥s
                    ∥ E ⟦ if x ∣⇒ p ∣⇒ q ⟧e ∥s
                    (eplug< q (if x ∣⇒ p ∣⇒ q) E (s≤′s (n≤′m+n ∥ p ∥s ∥ q ∥s)))
noetherian₁ (rif-true{θ}{p = p}{q = q}{x = x}{E = E} x∈ x₁ x₂) with unplug x₂
... | refl = arith1 (numstepsθ θ)
                    ∥ E ⟦ p ⟧e ∥s
                    ∥ E ⟦ if x ∣⇒ p ∣⇒ q ⟧e ∥s
                    (eplug< p (if x ∣⇒ p ∣⇒ q) E (s≤′s (m≤′m+n ∥ p ∥s ∥ q ∥s)))
noetherian₁ (rabsence{θ = θ}{S = S} S∈ θ[S]≡unk S̸S∉Canθ)
    with is-unknownp (SigMap.lookup{k = S} (sig θ) S∈)
       | inspect is-unknownp (SigMap.lookup{k = S} (sig θ) S∈)
... | false | Reveal_·_is_.[ eq ] rewrite θ[S]≡unk
  = ⊥-elim (absurd eq) where
      absurd : true ≡ false -> ⊥
      absurd ()
... | true  | Reveal_·_is_.[ eq ] with
   SigMap.change-one-count-goes-down
     (sig θ) is-unknownp
     S S∈ eq Signal.absent refl
... | thing rewrite thing = ≤′-refl

noetherian₁ (rreadyness {θ}{p}{s} s∈ (inj₁ θs=old) s∉Canθ)
  with is-notreadyp (ShrMap.lookup{k = s} (shr θ) s∈)
     | inspect is-notreadyp (ShrMap.lookup{k = s} (shr θ) s∈)
... | false | Reveal_·_is_.[ eq ]
  rewrite hunch (ShrMap.lookup{k = s} (shr θ) s∈) |  θs=old
  = ⊥-elim (absurd eq) where
       absurd : true ≡ false -> ⊥
       absurd ()
... | true  | Reveal_·_is_.[ eq ] rewrite θs=old with
  ShrMap.change-one-count-goes-down
     (shr θ) is-notreadyp
     s s∈ eq (SharedVar.ready ,′ shr-vals{s} θ s∈) refl
... | thing rewrite thing =
    arith4 (numstepsSig (sig θ))
           (numstepsShr (shr (set-shr{s} θ s∈ (SharedVar.ready)
                                         (shr-vals{s} θ s∈))))
           (∥ p ∥s)

noetherian₁ (rreadyness {θ}{p}{s} s∈ (inj₂ θs=new) s∉Canθ)
  with is-notreadyp (ShrMap.lookup{k = s} (shr θ) s∈)
     | inspect is-notreadyp (ShrMap.lookup{k = s} (shr θ) s∈)
... | false | Reveal_·_is_.[ eq ]
  rewrite hunch (ShrMap.lookup{k = s} (shr θ) s∈) |  θs=new
  = ⊥-elim (absurd eq) where
       absurd : true ≡ false -> ⊥
       absurd ()
... | true  | Reveal_·_is_.[ eq ] rewrite θs=new with
  ShrMap.change-one-count-goes-down
     (shr θ) is-notreadyp
     s s∈ eq (SharedVar.ready ,′ shr-vals{s} θ s∈) refl
... | thing rewrite thing =
    arith4 (numstepsSig (sig θ))
           (numstepsShr (shr (set-shr{s} θ s∈ (SharedVar.ready)
                                         (shr-vals{s} θ s∈))))
           (∥ p ∥s)

noetherian₁ (rmerge{θ₁}{θ₂}{_}{p}{E}{A₁}{A₂} x) with unplug x
... | refl rewrite decompose∥∥s E (ρ⟨ θ₂ , A₂ ⟩· p)
                 | decompose∥∥s E p
  = s≤′s
    (rearrange-things
      (numstepsSig (SigMap.union (sig θ₁) (sig θ₂)))
      (numstepsShr (ShrMap.union (shr θ₁) (shr θ₂)))
      ∥ E ⟦ nothin ⟧e ∥s
      ∥ p ∥s
      (numstepsSig (sig θ₁))
      (numstepsShr (shr θ₁))
      (numstepsSig (sig θ₂))
      (numstepsShr (shr θ₂))
      (≤′+b (numstepsSig (SigMap.union (sig θ₁) (sig θ₂)))
            (numstepsShr (ShrMap.union (shr θ₁) (shr θ₂)))
            (numstepsSig (sig θ₁) + numstepsSig (sig θ₂))
            (numstepsShr (shr θ₁) + numstepsShr (shr θ₂))
            (SigMap.count-merge≤′sum-count
             (sig θ₁) (sig θ₂) is-unknownp)
            (ShrMap.count-merge≤′sum-count
             (shr θ₁) (shr θ₂) is-notreadyp))) where

  rearrange-more :
    ∀ ab cd a b c d ->
      ab + cd ≤′ a + b + (c + d) ->
      ab + cd ≤′ a + c + (b + d)
  rearrange-more ab cd a b c d simple rewrite
     sym (+-assoc (a + c) b d)
   | +-assoc a c b
   | +-comm c b
   | sym (+-assoc a b c)
   | +-assoc (a + b) c d
   = simple

  rearrange-things : ∀ ab cd n p a c b d ->
    ab + cd ≤′ (a + b) + (c + d) ->
    suc (ab + cd + (n + p)) ≤′ a + c + (n + (suc (b + d + p)))
  rearrange-things ab cd n p a c b d simple rewrite
     +-suc n (b + d + p)
   | +-suc (a + c) (n + (b + d + p))
   | +-comm (b + d) p
   | sym (+-assoc n p (b + d))
   | +-comm (n + p) (b + d)
   | sym (+-assoc (a + c) (b + d) (n + p))
   = s≤′s (≤′+l {z = n + p} (rearrange-more ab cd a b c d simple))

csteps : ∀ {p q C C⟦p⟧ C⟦q⟧} ->
  (suc (∥ q ∥s)) ≤′ (∥ p ∥s) ->
  C⟦p⟧ ≐ C ⟦ p ⟧c ->
  C⟦q⟧ ≐ C ⟦ q ⟧c ->
  (suc ∥ C⟦q⟧ ∥s) ≤′ ∥ C⟦p⟧ ∥s
csteps sq≤p dchole dchole = sq≤p
csteps sq≤p (dcpar₁{pp}{pr}{pq} C⟦p⟧=C⟦p⟧c) (dcpar₁{qp}{qr}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith2 ∥ qp ∥s ∥ pp ∥s  ∥ pq ∥s sucnsp≰sp₁
csteps sq≤p (dcpar₂{pp}{pr}{pq} C⟦p⟧=C⟦p⟧c) (dcpar₂{qp}{qr}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith1 ∥ qp ∥s ∥ qq ∥s  ∥ pq ∥s sucnsp≰sp₁
csteps sq≤p (dcseq₁{pp}{pr}{pq} C⟦p⟧=C⟦p⟧c) (dcseq₁{qp}{qr}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith2 ∥ qp ∥s ∥ pp ∥s ∥ pq ∥s sucnsp≰sp₁
csteps sq≤p (dcseq₂{pp}{pr}{pq} C⟦p⟧=C⟦p⟧c) (dcseq₂{qp}{qr}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith1 ∥ pp ∥s ∥ qq ∥s ∥ pq ∥s sucnsp≰sp₁
csteps sq≤p (dcsuspend{p} C⟦p⟧=C⟦p⟧c) (dcsuspend{q} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = s≤′s sucnsp≰sp₁
csteps sq≤p (dctrap{p} C⟦p⟧=C⟦p⟧c) (dctrap{q} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = s≤′s sucnsp≰sp₁
csteps sq≤p (dcsignl{p} C⟦p⟧=C⟦p⟧c) (dcsignl{q} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = s≤′s (s≤′s (s≤′s sucnsp≰sp₁))
csteps sq≤p (dcpresent₁{pp}{pr}{pq} C⟦p⟧=C⟦p⟧c) (dcpresent₁{qp}{qr}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith2 ∥ qp ∥s  ∥ pp ∥s  ∥ pq ∥s  sucnsp≰sp₁
csteps sq≤p (dcpresent₂{pp}{pr}{pq} C⟦p⟧=C⟦p⟧c) (dcpresent₂{qp}{qr}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith1 ∥ pp ∥s ∥ qq ∥s ∥ pq ∥s sucnsp≰sp₁
csteps sq≤p (dcloop{p} C⟦p⟧=C⟦p⟧c) (dcloop{q} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith5 ∥ q ∥s ∥ p ∥s sucnsp≰sp₁
csteps sq≤p (dcloopˢ₁{pp}{pq} C⟦p⟧=C⟦p⟧c) (dcloopˢ₁{qp}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ =  arith2  ∥ qp ∥s  ∥ pp ∥s  ∥ pq ∥s sucnsp≰sp₁
csteps sq≤p (dcloopˢ₂{pp}{pq} C⟦p⟧=C⟦p⟧c) (dcloopˢ₂{qp}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith1 ∥ pp ∥s  ∥ qq ∥s ∥ pq ∥s sucnsp≰sp₁
csteps sq≤p (dcshared{p} C⟦p⟧=C⟦p⟧c) (dcshared{q} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = s≤′s (s≤′s (s≤′s sucnsp≰sp₁))
csteps sq≤p (dcvar{p} C⟦p⟧=C⟦p⟧c) (dcvar{q} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = s≤′s (s≤′s sucnsp≰sp₁)
csteps sq≤p (dcif₁{pp}{pr}{pq} C⟦p⟧=C⟦p⟧c) (dcif₁{qp}{qr}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith2 ∥ qp ∥s  ∥ pp ∥s  ∥ pq ∥s  sucnsp≰sp₁
csteps sq≤p (dcif₂{pp}{pr}{pq} C⟦p⟧=C⟦p⟧c) (dcif₂{qp}{qr}{qq} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith1 ∥ pp ∥s  ∥ qq ∥s  ∥ pq ∥s sucnsp≰sp₁
csteps sq≤p (dcenv{p = p1}{θ = θ} C⟦p⟧=C⟦p⟧c) (dcenv{p = p2} C⟦q⟧=C⟦q⟧c)
  with csteps sq≤p C⟦p⟧=C⟦p⟧c C⟦q⟧=C⟦q⟧c
... | sucnsp≰sp₁ = arith3  ∥ p2 ∥s  ∥ p1 ∥s (numstepsθ θ) sucnsp≰sp₁

noetherian : ∀ {p q} ->
  p sn⟶ q ->
  (suc (∥ q ∥s)) ≤′ (∥ p ∥s)
noetherian (rcontext C dc pinsn⟶₁qin) =
  csteps (noetherian₁ pinsn⟶₁qin) dc Crefl

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


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
-}
-- This is a selection of useful functions and definitions
-- from the standard library that we tend to use a lot.
module LibraBFT.Prelude where

  open import Level
    renaming (suc to ℓ+1; zero to ℓ0; _⊔_ to _ℓ⊔_)
    public

  1ℓ : Level
  1ℓ = ℓ+1 0ℓ

  open import Agda.Builtin.Unit
    public

  open import Function
    using (_∘_; _∘′_; id; case_of_; _on_; typeOf; flip; const; _∋_; _$_)
    public

  identity = id

  infixl 1 _&_
  _&_ = Function._|>_

  open import Data.Unit.NonEta
    public

  open import Data.Empty
    public

  -- NOTE: This function is defined to give extra documentation when discharging
  -- absurd cases where Agda can tell by pattern matching that `A` is not
  -- inhabited. For example:
  -- > absurd (just v ≡ nothing) case impossibleProof of λ ()
  infix 0 absurd_case_of_
  absurd_case_of_ : ∀ {ℓ₁ ℓ₂} (A : Set ℓ₁) {B : Set ℓ₂} → A → (A → ⊥) → B
  absurd A case x of f = ⊥-elim (f x)

  open import Data.Nat
    renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_; _≥?_ to _≥?ℕ_; compare to compareℕ; Ordering to Orderingℕ)
    public

  max = _⊔_
  min = _⊓_

  open import Data.Nat.DivMod using (_/_)
  div = _/_

  open import Data.Nat.Properties
    hiding (≡-irrelevant ; _≟_)
    public

  open import Data.List
    renaming (map to List-map ; filter to List-filter ; lookup to List-lookup;
              tabulate to List-tabulate; foldl to List-foldl)
    hiding (fromMaybe; [_])
    public

  foldl' = List-foldl

  open import Data.List.Properties
    renaming (≡-dec to List-≡-dec; length-map to List-length-map; map-compose to List-map-compose; filter-++ to List-filter-++; length-filter to List-length-filter)
    using (∷-injective; length-++; map-++-commute; sum-++-commute; map-tabulate; tabulate-lookup; ++-identityʳ; ++-identityˡ)
    public

  open import Data.List.Relation.Binary.Subset.Propositional
    renaming (_⊆_ to _⊆List_)
    public

  open import Data.List.Relation.Unary.Any
    using (Any; here; there)
    renaming (lookup to Any-lookup; map to Any-map; satisfied to Any-satisfied
             ;index to Any-index; any to Any-any)
    public

  open import Data.List.Relation.Unary.Any.Properties
    using    (¬Any[])
    renaming ( map⁺       to Any-map⁺
             ; map⁻       to Any-map⁻
             ; concat⁺    to Any-concat⁺
             ; concat⁻    to Any-concat⁻
             ; ++⁻        to Any-++⁻
             ; ++⁺ʳ       to Any-++ʳ
             ; ++⁺ˡ       to Any-++ˡ
             ; singleton⁻ to Any-singleton⁻
             ; tabulate⁺  to Any-tabulate⁺
             ; filter⁻    to Any-filter⁻
             )
    public

  open import Data.List.Relation.Unary.All
    using (All; []; _∷_)
    renaming (head     to All-head;   tail     to All-tail;
              lookup   to All-lookup; tabulate to All-tabulate;
              reduce   to All-reduce; map      to All-map)
    public

  open import Data.List.Relation.Unary.All.Properties
    hiding   (All-map)
    renaming ( tabulate⁻ to All-tabulate⁻
             ; tabulate⁺ to All-tabulate⁺
             ; map⁺      to All-map⁺
             ; map⁻      to All-map⁻
             ; ++⁺       to All-++
             )
    public

  open import Data.List.Membership.Propositional
    using (_∈_; _∉_)
    public

  open import Data.List.Membership.Propositional.Properties
    renaming (∈-filter⁺ to List-∈-filter⁺; ∈-filter⁻ to List-∈-filter⁻)
    public

  open import Data.Vec
    using (Vec; []; _∷_)
    renaming (replicate to Vec-replicate; lookup to Vec-lookup
             ;map to Vec-map; head to Vec-head; tail to Vec-tail
             ;updateAt to Vec-updateAt; tabulate to Vec-tabulate
             ;allFin to Vec-allFin; toList to Vec-toList; fromList to Vec-fromList
             ;_++_ to _Vec-++_)
    public

  open import Data.Vec.Relation.Unary.All
    using ([]; _∷_)
    renaming (All to Vec-All; lookup to Vec-All-lookup)
    public

  open import Data.Vec.Properties
    using ()
    renaming (updateAt-minimal to Vec-updateAt-minimal
             ;[]=⇒lookup to Vec-[]=⇒lookup
             ;lookup⇒[]= to Vec-lookup⇒[]=
             ;lookup∘tabulate to Vec-lookup∘tabulate
             ;≡-dec to Vec-≡-dec)
    public

  open import Data.List.Relation.Binary.Pointwise
    using (decidable-≡)
    public

  open import Data.Bool
    renaming (_≟_ to _≟Bool_)
    hiding (_≤?_; _<_; _<?_; _≤_; not)
    public

  open import Data.Maybe
    renaming (map to Maybe-map; zip to Maybe-zip ; _>>=_ to _Maybe->>=_)
    hiding (align; alignWith; zipWith)
    public

  -- a non-dependent eliminator
  maybeS : ∀ {a b} {A : Set a} {B : Set b} →
           (x : Maybe A) → B → ((x : A) → B) → B
  maybeS {B = B} x f t = maybe {B = const B} t f x

  maybeHsk : ∀ {A B : Set} → B → (A → B) → Maybe A → B
  maybeHsk b a→b = λ where
    nothing  → b
    (just a) → a→b a

  open import Data.Maybe.Relation.Unary.Any
    renaming (Any to Maybe-Any; dec to Maybe-Any-dec)
    hiding (map; zip; zipWith; unzip ; unzipWith)
    public

  maybe-any-⊥ : ∀{a}{A : Set a} → Maybe-Any {A = A} (λ _ → ⊤) nothing → ⊥
  maybe-any-⊥ ()

  headMay : ∀ {A : Set} → List A → Maybe A
  headMay     []  = nothing
  headMay (x ∷ _) = just x

  lastMay : ∀ {A : Set} → List A → Maybe A
  lastMay          []  = nothing
  lastMay     (x ∷ []) = just x
  lastMay (_ ∷ x ∷ xs) = lastMay (x ∷ xs)

  open import Data.Maybe.Properties
    using (just-injective)
    renaming (≡-dec to Maybe-≡-dec)
    public

  open import Data.Fin
    using (Fin; suc; zero; fromℕ; fromℕ< ; toℕ ; cast)
    renaming (_≟_ to _≟Fin_; _≤?_ to _≤?Fin_; _≤_ to _≤Fin_ ; _<_ to _<Fin_;
              inject₁ to Fin-inject₁; inject+ to Fin-inject+; inject≤ to Fin-inject≤)
    public

  fins : (n : ℕ) → List (Fin n)
  fins n = Vec-toList (Vec-allFin n)

  open import Data.Fin.Properties
    using (toℕ-injective; toℕ<n)
    renaming (<-cmp to Fin-<-cmp; <⇒≢ to <⇒≢Fin; suc-injective to Fin-suc-injective)
    public

  open import Relation.Binary.PropositionalEquality
    hiding (decSetoid)
    public

  open import Relation.Binary.HeterogeneousEquality
    using (_≅_)
    renaming (cong to ≅-cong; cong₂ to ≅-cong₂)
    public

  open import Relation.Binary
    public

  data Ordering : Set where
    LT EQ GT : Ordering

  compare : ℕ → ℕ → Ordering
  compare m n
    with <-cmp m n
  ... | tri< a ¬b ¬c = LT
  ... | tri≈ ¬a b ¬c = EQ
  ... | tri> ¬a ¬b c = GT

  ≡-irrelevant : ∀{a}{A : Set a} → Irrelevant {a} {A} _≡_
  ≡-irrelevant refl refl = refl

  to-witness-lemma : ∀{ℓ}{A : Set ℓ}{a : A}{f : Maybe A}(x : Is-just f)
                   → to-witness x ≡ a → f ≡ just a
  to-witness-lemma (just x) refl = refl

  open import Relation.Nullary
    hiding (Irrelevant; proof)
    public

  open import Relation.Nullary.Decidable
    hiding (map)
    public

  open import Data.Sum
    renaming ([_,_] to either; map to ⊎-map; map₁ to ⊎-map₁; map₂ to ⊎-map₂)
    public

  open import Data.Sum.Properties
    using (inj₁-injective ; inj₂-injective)
    public

  ⊎-elimˡ : ∀ {ℓ₀ ℓ₁}{A₀ : Set ℓ₀}{A₁ : Set ℓ₁} → ¬ A₀ → A₀ ⊎ A₁ → A₁
  ⊎-elimˡ ¬a = either (⊥-elim ∘ ¬a) id

  ⊎-elimʳ : ∀ {ℓ₀ ℓ₁}{A₀ : Set ℓ₀}{A₁ : Set ℓ₁} → ¬ A₁ → A₀ ⊎ A₁ → A₀
  ⊎-elimʳ ¬a = either id (⊥-elim ∘ ¬a)

  open import Data.Product
    renaming (map to ×-map; map₂ to ×-map₂; map₁ to ×-map₁; <_,_> to split; swap to ×-swap)
    hiding (zip)
    public

  fst = proj₁

  open import Data.Product.Properties
    public

  module _ {ℓA} {A : Set ℓA} where
    NoneOfKind : ∀ {ℓ} {P : A → Set ℓ} → List A → (p : (a : A) → Dec (P a)) → Set ℓA
    NoneOfKind xs p = List-filter p xs ≡ []

    postulate -- TODO-1: Replace with or prove using library properties?  Move to Lemmas?
      NoneOfKind⇒ : ∀ {ℓ} {P : A → Set ℓ} {Q : A → Set ℓ} {xs : List A}
                  → (p : (a : A) → Dec (P a))
                  → {q : (a : A) → Dec (Q a)}
                  → (∀ {a} → P a → Q a)  -- TODO-1: Use proper notation (Relation.Unary?)
                  → NoneOfKind xs q
                  → NoneOfKind xs p

  infix 4 _<?ℕ_
  _<?ℕ_ : Decidable _<_
  m <?ℕ n = suc m ≤?ℕ n

  infix 0 if-yes_then_else_
  infix 0 if-dec_then_else_
  if-yes_then_else_ : ∀ {ℓA ℓB} {A : Set ℓA} {B : Set ℓB} → Dec A → (A → B) → (¬ A → B) → B
  if-yes (yes prf) then f else _ = f prf
  if-yes (no  prf) then _ else g = g prf

  if-dec_then_else_ : ∀ {ℓA ℓB} {A : Set ℓA} {B : Set ℓB} → Dec A → B → B → B
  if-dec x then f else g = if-yes x then const f else const g

  open import Relation.Nullary.Negation
    using (contradiction; contraposition)
    public

  open import Relation.Binary
    using (Setoid; IsPreorder)
    public

  open import Relation.Unary
    using (_∪_)
    public

  open import Relation.Unary.Properties
    using (_∪?_)
    public

  -- Injectivity for a function of two potentially different types (A and B) via functions to a
  -- common type (C).

  Injective' : ∀ {b c d e}{B : Set b}{C : Set c}{D : Set d} → (hB : B → D) → (hC : C → D) → (_≈_ : B → C → Set e) → Set _
  Injective' {C = C} hB hC _≈_ = ∀ {b c} → hB b ≡ hC c → b ≈ c

  Injective  : ∀ {c d e}{C : Set c}{D : Set d} → (h : C → D) → (_≈_ : Rel C e) → Set _
  Injective h _≈_ = Injective' h h _≈_

  Injective-≡ : ∀ {c d}{C : Set c}{D : Set d} → (h : C → D) → Set _
  Injective-≡ h = Injective h _≡_

  Injective-int : ∀{a b c d e}{A : Set a}{B : Set b}{C : Set c}{D : Set d}
                → (_≈_ : A → B → Set e)
                → (h  : C → D)
                → (f₁ : A → C)
                → (f₂ : B → C)
                → Set (a ℓ⊔ b ℓ⊔ d ℓ⊔ e)
  Injective-int _≈_ h f₁ f₂ = ∀ {a₁} {b₁} → h (f₁ a₁) ≡ h (f₂ b₁) → a₁ ≈ b₁

  NonInjective : ∀{a b c}{A : Set a}{B : Set b}
               → (_≈_ : Rel A c)
               → (A → B) → Set (a ℓ⊔ b ℓ⊔ c)
  NonInjective {A = A} _≈_ f
    = Σ (A × A) (λ { (x₁ , x₂) → ¬ (x₁ ≈ x₂) × f x₁ ≡ f x₂ })

  NonInjective-≡ : ∀{a b}{A : Set a}{B : Set b}
                 → (A → B) → Set (a ℓ⊔ b)
  NonInjective-≡ = NonInjective _≡_

  NonInjective-≡-preds : ∀{a b}{A : Set a}{B : Set b}{ℓ₁ ℓ₂ : Level}
                      → (A → Set ℓ₁)
                      → (A → Set ℓ₂)
                      → (A → B) → Set (a ℓ⊔ b ℓ⊔ ℓ₁ ℓ⊔ ℓ₂)
  NonInjective-≡-preds Pred1 Pred2 f = Σ (NonInjective _≡_ f) λ { ((a₀ , a₁) , _ , _) → Pred1 a₀ × Pred2 a₁ }

  NonInjective-≡-pred : ∀{a b}{A : Set a}{B : Set b}{ℓ : Level}
                      → (P : A → Set ℓ)
                      → (A → B) → Set (a ℓ⊔ b ℓ⊔ ℓ)
  NonInjective-≡-pred Pred = NonInjective-≡-preds Pred Pred

  NonInjective-∘ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
                 → {f : A → B}(g : B → C)
                 → NonInjective-≡  f
                 → NonInjective-≡ (g ∘ f)
  NonInjective-∘ g ((x0 , x1) , (x0≢x1 , fx0≡fx1))
    = ((x0 , x1) , x0≢x1 , (cong g fx0≡fx1))

  --------------------------------------------
  -- Handy fmap and bind for specific types --

  _<M$>_ : ∀{a b}{A : Set a}{B : Set b}
         → (f : A → B)
         → Maybe A → Maybe B
  _<M$>_ = Maybe-map

  <M$>-univ : ∀{a b}{A : Set a}{B : Set b}
            → (f : A → B)(x : Maybe A)
            → {y : B} → f <M$> x ≡ just y
            → ∃[ x' ] (x ≡ just x' × f x' ≡ y)
  <M$>-univ f (just x) refl = x , (refl , refl)

  maybe-lift : {A : Set}
             → {mx : Maybe A}{x : A}
             → (P : A → Set)
             → P x → mx ≡ just x
             → maybe {B = const Set} P ⊥ mx
  maybe-lift {mx = just .x} {x} P px refl = px

  <M$>-nothing : ∀ {a b}{A : Set a}{B : Set b}(f : A → B)
               → f <M$> nothing ≡ nothing
  <M$>-nothing _ = refl

  _<⊎$>_ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
         → (A → B) → C ⊎ A → C ⊎ B
  f <⊎$> (inj₁ hb) = inj₁ hb
  f <⊎$> (inj₂ x)  = inj₂ (f x)

  _⊎⟫=_ : ∀{a b c}{A : Set a}{B : Set b}{C : Set c}
        → C ⊎ A → (A → C ⊎ B) → C ⊎ B
  (inj₁ x) ⊎⟫= _ = inj₁ x
  (inj₂ a) ⊎⟫= f = f a

  -- Syntactic support for more faithful model of Haskell code
  Either : ∀ {a b} → Set a → Set b → Set (a ℓ⊔ b)
  Either A B = A ⊎ B
  pattern Left  x = inj₁ x
  pattern Right x = inj₂ x

  isLeft : ∀ {a b} {A : Set a} {B : Set b} → Either A B → Bool
  isLeft (Left _)  = true
  isLeft (Right _) = false

  isRight : ∀ {a b} {A : Set a} {B : Set b} → Either A B → Bool
  isRight = Data.Bool.not ∘ isLeft

  -- a non-dependent eliminator
  eitherS : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
            (x : Either A B) → ((x : A) → C) → ((x : B) → C) → C
  eitherS eab fa fb = case eab of λ where
    (Left  a) → fa a
    (Right b) → fb b

  module _ {ℓ₀ ℓ₁ ℓ₂ : Level} where
    EL-type = Set ℓ₁ → Set ℓ₂ → Set ℓ₀
    EL-level = ℓ₁ ℓ⊔ ℓ₂ ℓ⊔ ℓ₀

    -- Utility to make passing between `Either` and `EitherD` more convenient
    record EitherLike (E : EL-type) : Set (ℓ+1 EL-level) where
      field
        fromEither : ∀ {A : Set ℓ₁} {B : Set ℓ₂} → Either A B → E A B
        toEither   : ∀ {A : Set ℓ₁} {B : Set ℓ₂} → E A B → Either A B
    open EitherLike ⦃ ... ⦄ public

    EL-func : EL-type → Set (ℓ+1 EL-level)
    EL-func EL = ⦃ mel : EitherLike EL ⦄ → Set EL-level

  instance
    EitherLike-Either : ∀ {ℓ₁ ℓ₂} → EitherLike{ℓ₁ ℓ⊔ ℓ₂}{ℓ₁}{ℓ₂} Either
    EitherLike.fromEither EitherLike-Either = id
    EitherLike.toEither   EitherLike-Either = id

  -- an approximation of Haskell's backtick notation for making infix operators; in Agda, must have
  -- spaces between f and backticks
  flip' : _     -- Avoids warning about definition and syntax declaration being in different scopes
  flip' = flip
  syntax flip' f = ` f `

  open import Data.String as String
    hiding (_==_ ; _≟_ ; concat)

  check : Bool → List String → Either String Unit
  check b t = if b then inj₂ unit else inj₁ (String.intersperse "; " t)

  -- TODO-1: Maybe this belongs somewhere else?  It's in a similar
  -- category as Optics, so maybe should similarly be in a module that
  -- is separate from the main project?
  ------------------
  -- Guard Syntax --
  --
  -- Example Usage:
  --
  -- > f : ℕ → ℕ
  -- > f x = grd‖ x ≟ℕ 10  ≔ 12
  -- >          ‖ otherwise≔ 40 + 2
  --
  --
  -- > g : ℕ ⊎ ℕ → ℕ
  -- > g x = case x of λ
  -- >     { (inj₁ x) → grd‖ x ≤? 10  ≔ 2 * x
  -- >                     ‖ otherwise≔ 42
  -- >     ; (inj₂ y) → y
  -- >     }
  --
  -- To type: ‖  -->  \Vert
  --          ≔  -->  \:=

  record ToBool {a}(A : Set a) : Set a where
    field
      toBool : A → Bool
  open ToBool {{ ... }} public

  not : ∀ {b} {B : Set b} ⦃ _ : ToBool B ⦄ → B → Bool
  not b = Data.Bool.not (toBool b)

  instance
    ToBool-Bool : ToBool Bool
    ToBool-Bool = record { toBool = id }

    ToBool-Dec : ∀{a}{A : Set a} → ToBool (Dec A)
    ToBool-Dec = record { toBool = ⌊_⌋ }

  toWitnessT : ∀{ℓ}{P : Set ℓ}{d : Dec P} → ⌊ d ⌋ ≡ true → P
  toWitnessT {d = yes proof} _ = proof

  toWitnessF : ∀{ℓ}{P : Set ℓ}{d : Dec P} → ⌊ d ⌋ ≡ false → ¬ P
  toWitnessF{d = no proof} _ = proof

  infix 3 _≔_
  data GuardClause {a}{b}(A : Set a) : Set (a ℓ⊔ ℓ+1 b) where
    _≔_ : {B : Set b}{{ bb : ToBool B }} → B → A → GuardClause A

  infix 3 otherwise≔_
  data Guards {a}{b}(A : Set a) : Set (a ℓ⊔ ℓ+1 b) where
   otherwise≔_ : A → Guards A
   clause     : GuardClause{a}{b} A → Guards{a}{b} A → Guards A

  infixr 2 _‖_
  _‖_ : ∀{a}{b}{A : Set a} → GuardClause{a}{b} A → Guards A → Guards A
  _‖_ = clause

  infix 1 grd‖_
  grd‖_ : ∀{a}{b}{A : Set a} → Guards{a}{b} A → A
  grd‖_ (otherwise≔ a) = a
  grd‖_ (clause (b ≔ a) g)  = if toBool b then a else (grd‖ g)

  Any-satisfied-∈ : ∀{a ℓ}{A : Set a}{P : A → Set ℓ}{xs : List A}
                  → Any P xs → Σ A (λ x → P x × x ∈ xs)
  Any-satisfied-∈ (here px) = _ , (px , here refl)
  Any-satisfied-∈ (there p) = let (a , px , prf) = Any-satisfied-∈ p
                               in (a , px , there prf)

  f-sum : ∀{a}{A : Set a} → (A → ℕ) → List A → ℕ
  f-sum f = sum ∘ List-map f

  record Functor  {ℓ₁ ℓ₂ : Level} (F : Set ℓ₁ → Set ℓ₂) : Set (ℓ₂ ℓ⊔ ℓ+1 ℓ₁) where
    infixl 4 _<$>_
    field
      _<$>_ : ∀ {A B : Set ℓ₁} → (A → B) → F A → F B
    fmap = _<$>_

  open Functor ⦃ ... ⦄ public

  record Applicative {ℓ₁ ℓ₂ : Level} (F : Set ℓ₁ → Set ℓ₂) : Set (ℓ₂ ℓ⊔ ℓ+1 ℓ₁) where
    infixl 4 _<*>_
    field
      pure  : ∀ {A : Set ℓ₁} → A → F A
      _<*>_ : ∀ {A B : Set ℓ₁} → F (A → B) → F A → F B

  open Applicative ⦃ ... ⦄ public
  instance
    ApplicativeFunctor : ∀ {ℓ₁ ℓ₂} {F : Set ℓ₁ → Set ℓ₂} ⦃ _ : Applicative F ⦄ → Functor F
    Functor._<$>_ ApplicativeFunctor f xs = pure f <*> xs

  record Monad {ℓ₁ ℓ₂ : Level} (M : Set ℓ₁ → Set ℓ₂) : Set (ℓ₂ ℓ⊔ ℓ+1 ℓ₁) where
    infixl 1 _>>=_ _>>_
    field
      return : ∀ {A : Set ℓ₁} → A → M A
      _>>=_  : ∀ {A B : Set ℓ₁} → M A → (A → M B) → M B

    _>>_ : ∀ {A B : Set ℓ₁} → M A → M B → M B
    m₁ >> m₂ = m₁ >>= λ _ → m₂

  open Monad ⦃ ... ⦄ public

  instance
    MonadApplicative : ∀ {ℓ₁ ℓ₂} {M : Set ℓ₁ → Set ℓ₂} ⦃ _ : Monad M ⦄ → Applicative M
    Applicative.pure MonadApplicative = return
    Applicative._<*>_ MonadApplicative fs xs = do
      f ← fs
      x ← xs
      return (f x)

  instance
    Monad-Either : ∀ {ℓ}{C : Set ℓ} → Monad{ℓ}{ℓ} (Either C)
    Monad.return (Monad-Either{ℓ}{C}) = inj₂
    Monad._>>=_ (Monad-Either{ℓ}{C}) = either (const ∘ inj₁) _&_

    Monad-Maybe : ∀ {ℓ} → Monad {ℓ} {ℓ} Maybe
    Monad.return (Monad-Maybe{ℓ}) = just
    Monad._>>=_  (Monad-Maybe{ℓ}) = _Maybe->>=_

    Monad-List : ∀ {ℓ} → Monad {ℓ}{ℓ} List
    Monad.return Monad-List x = x ∷ []
    Monad._>>=_  Monad-List x f = concat (List-map f x)

  maybeSMP : ∀ {ℓ} {A B : Set} {m : Set → Set ℓ} ⦃ _ : Monad m ⦄ → m (Maybe A) → B → (A → m B) → m B
  maybeSMP ma b f = do
    x ← ma
    case x of λ where
      nothing  → pure b
      (just j) → f j

  fromMaybeM : ∀ {ℓ} {A : Set} {m : Set → Set ℓ} ⦃ _ : Monad m ⦄ → m A → m (Maybe A) → m A
  fromMaybeM ma mma = do
    mma >>= λ where
      nothing  → ma
      (just a) → pure a

  forM_ : ∀ {ℓ} {A B : Set} {M : Set → Set ℓ} ⦃ _ : Monad M ⦄ → List A → (A → M B) → M Unit
  forM_      []  _ = return unit
  forM_ (x ∷ xs) f = f x >> forM_ xs f

  -- NOTE: because 'forM_' is defined above, it is necessary to
  -- call 'forM' with parenthesis (e.g., recursive call in definition)
  -- to disambiguate it for the Agda parser.
  forM : ∀ {ℓ} {A B : Set} {M : Set → Set ℓ} ⦃ _ : Monad M ⦄ → List A → (A → M B) → M (List B)
  forM      []  _ = return []
  forM (x ∷ xs) f = do
    fx  ← f x
    fxs ← (forM) xs f
    return (fx ∷ fxs)

  foldrM : ∀ {ℓ₁ ℓ₂} {A B : Set ℓ₁} {M : Set ℓ₁ → Set ℓ₂} ⦃ _ : Monad M ⦄ → (A → B → M B) → B → List A → M B
  foldrM _ b      []  = return b
  foldrM f b (a ∷ as) = foldrM f b as >>= f a

  foldlM : ∀ {ℓ₁ ℓ₂} {A B : Set ℓ₁} {M : Set ℓ₁ → Set ℓ₂} ⦃ _ : Monad M ⦄ → (B → A → M B) → B → List A → M B
  foldlM _ z      []  = pure z
  foldlM f z (x ∷ xs) = do
    z' ← f z x
    foldlM f z' xs

  foldM = foldlM

  foldM_ : {A B : Set} {M : Set → Set} ⦃ _ : Monad M ⦄ → (B → A → M B) → B → List A → M Unit
  foldM_ f a xs = foldlM f a xs >> pure unit

  open import LibraBFT.Base.Util public

  record Eq {a} (A : Set a) : Set a where
    infix 4 _≟_ _==_ _/=_
    field
      _≟_ : (a b : A) → Dec (a ≡ b)

    _==_   : A → A → Bool
    a == b = toBool $ a ≟ b

    _/=_ : A → A → Bool
    a /= b = not (a == b)
  open Eq ⦃ ... ⦄ public

  elem : ∀ {ℓ} {A : Set ℓ} ⦃ _ : Eq A ⦄ → A → List A → Bool
  elem x = toBool ∘ Any-any (x ≟_)

  instance
    Eq-Nat : Eq ℕ
    Eq._≟_ Eq-Nat = _≟ℕ_

    Eq-Maybe : ∀ {a} {A : Set a} ⦃ _ : Eq A ⦄ → Eq (Maybe A)
    Eq._≟_ Eq-Maybe nothing nothing = yes refl
    Eq._≟_ Eq-Maybe (just _) nothing = no λ ()
    Eq._≟_ Eq-Maybe nothing (just _) = no λ ()
    Eq._≟_ Eq-Maybe (just a) (just b)
       with a ≟ b
    ... | no  proof = no λ where refl → proof refl
    ... | yes refl = yes refl

  infixl 9 _!?_
  _!?_ : {A : Set} → List A → ℕ → Maybe A
  []       !?      _   = nothing
  (x ∷ _ ) !?      0   = just x
  (_ ∷ xs) !? (suc n)  = xs !? n

  -- Like a Haskell list-comprehension for ℕ : [ n | n <- [from .. to] ]
  fromToList : ℕ → ℕ → List ℕ
  fromToList from to with from ≤′? to
  ... | no ¬pr = []
  ... | yes pr = fromToList-le from to pr []
   where
    fromToList-le : ∀ (from to : ℕ) (klel : from ≤′ to) (acc : List ℕ) → List ℕ
    fromToList-le from ._        ≤′-refl       acc = from ∷ acc
    fromToList-le from (suc to) (≤′-step klel) acc = fromToList-le from to klel (suc to ∷ acc)

  _ : fromToList 1 1 ≡ 1 ∷ []
  _ = refl
  _ : fromToList 1 2 ≡ 1 ∷ 2 ∷ []
  _ = refl
  _ : fromToList 2 1 ≡ []
  _ = refl

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-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 --cubical --no-import-sorts --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

-- II
import Cubical.Foundations.Prelude                   as Prelude
import Cubical.Foundations.GroupoidLaws              as GroupoidLaws
import Cubical.Foundations.Path                      as Path
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

-- III
import Cubical.ZCohomology.Base                      as coHom
  renaming (coHomK 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

-- IV
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

-- V
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)

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

-- II.A Important notions in Cubical Agda
open Prelude using ( PathP
                   ; _≡_
                   ; refl
                   ; cong
                   ; funExt)

open GroupoidLaws using (_⁻¹)

open Prelude using ( transport
                   ; subst
                   ; hcomp)

--- II.B Important concepts from HoTT/UF in Cubical Agda

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

-- Suspensions
open Suspension using (Susp)

-- 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 (_⋁_)

-- III.C Univalence

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

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

-- Groups
open Gr using (Group)

----- III. ℤ-COHOMOLOGY IN CUBICAL AGDA -----

-- III.A Eilenberg-MacLane spaces

-- Eilenberg-MacLane spaces Kₙ
open coHom using (K)

-- Proposition 1
open S using (sphereConnected)

-- Lemma 1
open S using (wedgeConSn)

-- 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 =
  (wedgeConSn 0 0 hlev fᵣ fₗ p .fst)
   , ((λ x → sym (wedgeConSn 0 0 hlev fᵣ fₗ p .snd .snd x))
   , λ _ → refl) -- right holds by refl
   , rUnit _
wedgeConSn' zero (suc m) hlev fₗ fᵣ p =
  (wedgeConSn 0 (suc m) hlev fᵣ fₗ p .fst)
  , ((λ _ → refl) -- left holds by refl
  , (λ x → sym (wedgeConSn 0 (suc m) hlev fᵣ fₗ p .snd .fst x)))
  , lUnit _
wedgeConSn' (suc n) m hlev fₗ fᵣ p =
  (wedgeConSn (suc n) m hlev fᵣ fₗ p .fst)
   , ((λ x → sym (wedgeConSn (suc n) m hlev fᵣ fₗ p .snd .snd x))
   , λ _ → refl) -- right holds by refl
   , rUnit _

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

-- 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

-- rUnitₖ (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ₖ (≡ refl ∙ transport refl refl for n = 1
--         and transport refl refl ∙ transport refl refl for n ≥ 2)
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 = sym (lUnit _) ∙ transportRefl refl
n≥2-lCancel≡refl = rCancel _

-- rCancelₖ (≡ transport 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 = transportRefl refl
n≥2-rCancel≡refl = transportRefl refl

-- 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

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

-- Theorem 1 (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 2 (p ∙ q ≡ cong²₊(p,q)) for n = 1 and n ≥ 2 respectively
open GroupStructure using (∙≡+₁ ; ∙≡+₂)

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

-- III.B Group structure on Hⁿ(A)

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

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

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

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

----- IV. THE EILENBERG-STEENROD AXIOMS -----

-- IV.A 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'

-- IV.B Verifying the axioms

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

-- III.C Characterizing Z-cohomology groups using the axioms

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

----- V. CHARACTERIZING COHOMOLOGY GROUPS DIRECTLY -----

-- V.A
-- Proposition 4 and 5 respectively
open HⁿSⁿ using (Hⁿ-Sⁿ≅ℤ ; Hⁿ-Sᵐ≅1)

-- V.B
-- Proposition 6 and 7 respectively
open HⁿT² using (H¹-T²≅ℤ×ℤ ; H²-T²≅ℤ)

-- V.C
-- Proposition 8 and 9 respectively (Hⁿ(𝕂²))
-- ℤ/2ℤ is represented by Bool with the unique group structure
open Hⁿ𝕂² using (H¹-𝕂²≅ℤ ; H²-𝕂²≅Bool)

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

----- VI. COMPUTING WITH THE COHOMOLOGY GROUPS -----

import Cubical.Experiments.ZCohomology.Benchmarks

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module Data.List.Mapping.StringMap where

open import Data.String using (String; stringOrd)
open import Data.List.Mapping stringOrd public
open import Prelude
open import Data.Maybe

-- example : Record (∅ [ "name" ]︓ String [ "age" ]︓ ℕ [ "occ" ]︓ Bool)
-- example =
--   ∅ [ "age"  ]≔ 30
--     [ "occ"  ]≔ true
--     [ "name" ]≔ "Jo"

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.NatMinusOne.Base where

open import Cubical.Core.Primitives
open import Cubical.Data.Nat
open import Cubical.Data.Empty
open import Cubical.Data.Int.Base using (ℤ; pos; negsuc; -_)

record ℕ₋₁ : Type₀ where
  constructor -1+_
  field
    n : ℕ

pattern neg1 = -1+ zero
pattern ℕ→ℕ₋₁ n = -1+ (suc n)

1+_ : ℕ₋₁ → ℕ
1+_ (-1+ n) = n

suc₋₁ : ℕ₋₁ → ℕ₋₁
suc₋₁ (-1+ n) = -1+ (suc n)

-- Natural number and negative integer literals for ℕ₋₁

open import Cubical.Data.Nat.Literals public

instance
  fromNatℕ₋₁ : FromNat ℕ₋₁
  fromNatℕ₋₁ = record { Constraint = λ _ → ⊤ ; fromNat = ℕ→ℕ₋₁ }

instance
  negativeℕ₋₁ : Negative ℕ₋₁
  negativeℕ₋₁ = record { Constraint = λ { (suc (suc _)) → ⊥ ; _ → ⊤ }
                      ; fromNeg = λ { zero → 0 ; (suc zero) → neg1 } }


text:
module Luau.Syntax where

open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Float using (Float)
open import Properties.Dec using (⊥)
open import Luau.Var using (Var)
open import Luau.Addr using (Addr)
open import Luau.Type using (Type)

infixr 5 _∙_

data Annotated : Set where
  maybe : Annotated
  yes : Annotated

data VarDec : Annotated → Set where
  var : Var → VarDec maybe
  var_∈_ : ∀ {a} → Var → Type → VarDec a

name : ∀ {a} → VarDec a → Var
name (var x) = x
name (var x ∈ T) = x

data FunDec : Annotated → Set where
  _⟨_⟩∈_ : ∀ {a} → Var → VarDec a → Type → FunDec a
  _⟨_⟩ : Var → VarDec maybe → FunDec maybe

fun : ∀ {a} → FunDec a → Var
fun (f ⟨ x ⟩∈ T) = f
fun (f ⟨ x ⟩) = f

arg : ∀ {a} → FunDec a → VarDec a
arg (f ⟨ x ⟩∈ T) = x
arg (f ⟨ x ⟩) = x

data BinaryOperator : Set where
  + : BinaryOperator
  - : BinaryOperator
  * : BinaryOperator
  / : BinaryOperator

data Block (a : Annotated) : Set
data Stat (a : Annotated) : Set
data Expr (a : Annotated) : Set

data Block a where
  _∙_ : Stat a → Block a → Block a
  done : Block a

data Stat a where
  function_is_end : FunDec a → Block a → Stat a
  local_←_ : VarDec a → Expr a → Stat a
  return : Expr a → Stat a

data Expr a where
  nil : Expr a
  var : Var → Expr a
  addr : Addr → Expr a
  _$_ : Expr a → Expr a → Expr a
  function_is_end : FunDec a → Block a → Expr a
  block_is_end : Var → Block a → Expr a
  number : Float → Expr a
  binexp : Expr a → BinaryOperator → Expr a → Expr a


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Component functions of permutations found in `Data.Fin.Permutation`
------------------------------------------------------------------------

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

module Data.Fin.Permutation.Components where

open import Data.Fin
open import Data.Fin.Properties
open import Data.Nat as ℕ using (zero; suc; _∸_)
import Data.Nat.Properties as ℕₚ
open import Data.Product using (proj₂)
open import Relation.Nullary using (yes; no)
open import Relation.Binary.PropositionalEquality
open import Algebra.FunctionProperties using (Involutive)
open ≡-Reasoning

--------------------------------------------------------------------------------
--  Functions
--------------------------------------------------------------------------------

-- 'tranpose i j' swaps the places of 'i' and 'j'.

transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n
transpose i j k with k ≟ i
... | yes _ = j
... | no  _ with k ≟ j
...   | yes _ = i
...   | no  _ = k

-- reverse i = n ∸ 1 ∸ i

reverse : ∀ {n} → Fin n → Fin n
reverse {zero}  ()
reverse {suc n} i  = inject≤ (n ℕ- i) (ℕₚ.n∸m≤n (toℕ i) (suc n))

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

transpose-inverse : ∀ {n} (i j : Fin n) {k} →
                    transpose i j (transpose j i k) ≡ k
transpose-inverse i j {k} with k ≟ j
... | yes p rewrite ≡-≟-identity _≟_ {a = i} refl = sym p
... | no ¬p with k ≟ i
transpose-inverse i j {k} | no ¬p | yes q with j ≟ i
... | yes r = trans r (sym q)
... | no ¬r rewrite ≡-≟-identity _≟_ {a = j} refl = sym q
transpose-inverse i j {k} | no ¬p | no ¬q
  rewrite proj₂ (≢-≟-identity _≟_ ¬q)
        | proj₂ (≢-≟-identity _≟_ ¬p) = refl

reverse-prop : ∀ {n} → (i : Fin n) → toℕ (reverse i) ≡ n ∸ suc (toℕ i)
reverse-prop {zero} ()
reverse-prop {suc n} i = begin
  toℕ (inject≤ (n ℕ- i) _)  ≡⟨ toℕ-inject≤ _ _ ⟩
  toℕ (n ℕ- i)              ≡⟨ toℕ‿ℕ- n i ⟩
  n ∸ toℕ i                 ∎

reverse-involutive : ∀ {n} → Involutive _≡_ (reverse {n})
reverse-involutive {zero}  ()
reverse-involutive {suc n} i = toℕ-injective (begin
  toℕ (reverse (reverse i)) ≡⟨ reverse-prop (reverse i) ⟩
  n ∸ (toℕ (reverse i))     ≡⟨ cong (n ∸_) (reverse-prop i) ⟩
  n ∸ (n ∸ (toℕ i))         ≡⟨ ℕₚ.m∸[m∸n]≡n (ℕₚ.≤-pred (toℕ<n i)) ⟩
  toℕ i                     ∎)

reverse-suc : ∀ {n}{i : Fin n} → toℕ (reverse (suc i)) ≡ toℕ (reverse i)
reverse-suc {n} {i} = begin
  toℕ (reverse (suc i))      ≡⟨ reverse-prop (suc i) ⟩
  suc n ∸ suc (toℕ (suc i))  ≡⟨⟩
  n ∸ toℕ (suc i)            ≡⟨⟩
  n ∸ suc (toℕ i)            ≡⟨ sym (reverse-prop i) ⟩
  toℕ (reverse i)            ∎


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

module Cubical.Foundations.Embedding where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism

private
  variable
    ℓ : Level
    A B : Type ℓ
    f : A → B
    w x : A
    y z : B

-- Embeddings are generalizations of injections. The usual
-- definition of injection as:
--
--    f x ≡ f y → x ≡ y
--
-- is not well-behaved with higher h-levels, while embeddings
-- are.
isEmbedding : (A → B) → Type _
isEmbedding f = ∀ w x → isEquiv {A = w ≡ x} (cong f)

isEmbeddingIsProp : isProp (isEmbedding f)
isEmbeddingIsProp {f = f}
  = propPi λ w → propPi λ x → isPropIsEquiv (cong f)

-- If A and B are h-sets, then injective functions between
-- them are embeddings.
--
-- Note: It doesn't appear to be possible to omit either of
-- the `isSet` hypotheses.
injEmbedding
  : {f : A → B}
  → isSet A → isSet B
  → (∀{w x} → f w ≡ f x → w ≡ x)
  → isEmbedding f
injEmbedding {f = f} iSA iSB inj w x
  = isoToIsEquiv (iso (cong f) inj sect retr)
  where
  sect : section (cong f) inj
  sect p = iSB (f w) (f x) _ p

  retr : retract (cong f) inj
  retr p = iSA w x _ p

private
  lemma₀ : (p : y ≡ z) → fiber f y ≡ fiber f z
  lemma₀ {f = f} p = λ i → fiber f (p i)

  lemma₁ : isEmbedding f → ∀ x → isContr (fiber f (f x))
  lemma₁ {f = f} iE x = value , path
    where
    value : fiber f (f x)
    value = (x , refl)

    path : ∀(fi : fiber f (f x)) → value ≡ fi
    path (w , p) i
      = case equiv-proof (iE w x) p of λ
      { ((q , sq) , _)
      → hfill (λ j → λ { (i = i0) → (x , refl)
                      ; (i = i1) → (w , sq j)
                      })
          (inS (q (~ i) , λ j → f (q (~ i ∨ j))))
          i1
      }

-- If `f` is an embedding, we'd expect the fibers of `f` to be
-- propositions, like an injective function.
hasPropFibers : (A → B) → Type _
hasPropFibers f = ∀ y → isProp (fiber f y)

hasPropFibersIsProp : isProp (hasPropFibers f)
hasPropFibersIsProp = propPi (λ _ → isPropIsProp)

isEmbedding→hasPropFibers : isEmbedding f → hasPropFibers f
isEmbedding→hasPropFibers iE y (x , p)
  = subst (λ f → isProp f) (lemma₀ p) (isContr→isProp (lemma₁ iE x)) (x , p)

private
  fibCong→PathP
    : {f : A → B}
    → (p : f w ≡ f x)
    → (fi : fiber (cong f) p)
    → PathP (λ i → fiber f (p i)) (w , refl) (x , refl)
  fibCong→PathP p (q , r) i = q i , λ j → r j i

  PathP→fibCong
    : {f : A → B}
    → (p : f w ≡ f x)
    → (pp : PathP (λ i → fiber f (p i)) (w , refl) (x , refl))
    → fiber (cong f) p
  PathP→fibCong p pp = (λ i → fst (pp i)) , (λ j i → snd (pp i) j)

PathP≡fibCong
  : {f : A → B}
  → (p : f w ≡ f x)
  → PathP (λ i → fiber f (p i)) (w , refl) (x , refl) ≡ fiber (cong f) p
PathP≡fibCong p
  = isoToPath (iso (PathP→fibCong p) (fibCong→PathP p) (λ _ → refl) (λ _ → refl))

hasPropFibers→isEmbedding : hasPropFibers f → isEmbedding f
hasPropFibers→isEmbedding {f = f} iP w x .equiv-proof p
  = subst isContr (PathP≡fibCong p) (isProp→isContrPathP iP p fw fx)
  where
  fw : fiber f (f w)
  fw = (w , refl)

  fx : fiber f (f x)
  fx = (x , refl)

isEmbedding≡hasPropFibers : isEmbedding f ≡ hasPropFibers f
isEmbedding≡hasPropFibers
  = isoToPath
      (iso isEmbedding→hasPropFibers
           hasPropFibers→isEmbedding
           (λ _ → hasPropFibersIsProp _ _)
           (λ _ → isEmbeddingIsProp _ _))

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
module ModuleDoesntExport where

module A where
  postulate C : Set

open A using (B; module P) renaming (D to C)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Level using (Level)

open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open ≡-Reasoning

open import Data.Nat using (ℕ; suc; zero; _+_)
open import Data.Nat.Properties

open import Data.Product using (_,_)
open import Data.Vec using (Vec; foldr; zipWith; map; []; _∷_; _++_; take; drop; splitAt; replicate)
open import Data.Vec.Properties

module FLA.Data.Vec.Properties where

private
  variable
    ℓ : Level
    A B C : Set ℓ
    m n : ℕ

++-identityₗ : (v : Vec A n) → [] ++  v ≡ v
++-identityₗ _ = refl

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Indexed M-types (the dual of indexed W-types aka Petersson-Synek
-- trees).
------------------------------------------------------------------------

module Data.M.Indexed where

open import Level
open import Coinduction
open import Data.Product
open import Data.Container.Indexed.Core
open import Function
open import Relation.Unary

-- The family of indexed M-types.

module _ {ℓ c r} {O : Set ℓ} (C : Container O O c r) where

  data M (o : O) : Set (ℓ ⊔ c ⊔ r) where
    inf : ⟦ C ⟧ (∞ ∘ M) o → M o

  open Container C

  -- Projections.

  head : M ⊆ Command
  head (inf (c , _)) = c

  tail : ∀ {o} (m : M o) (r : Response (head m)) → M (next (head m) r)
  tail (inf (_ , k)) r = ♭ (k r)

  force : M ⊆ ⟦ C ⟧ M
  force (inf (c , k)) = c , λ r → ♭ (k r)

  -- Coiteration.

  coit : ∀ {ℓ} {X : Pred O ℓ} → X ⊆ ⟦ C ⟧ X → X ⊆ M
  coit ψ x = inf (proj₁ cs , λ r → ♯ coit ψ (proj₂ cs r))
    where
    cs = ψ x


text:
{-# OPTIONS --without-K #-}
module function.isomorphism.two-out-of-six where

open import sum
open import equality
open import function.core
open import function.isomorphism.core
open import function.overloading
open import hott.equivalence.core
open import hott.equivalence.biinvertible

module two-out-of-six
         {i j k l}{X : Set i}{Y : Set j}{Z : Set k}{W : Set l}
         (f : X → Y)(g : Y → Z)(h : Z → W)
         (gf-equiv : weak-equiv (g ∘ f))
         (hg-equiv : weak-equiv (h ∘ g)) where
  private
    r : X ≅ Z
    r = ≈⇒≅ (g ∘ f , gf-equiv)

    s : Y ≅ W
    s = ≈⇒≅ (h ∘ g , hg-equiv)

    gl : Z → Y
    gl = invert s ∘ h

    gr : Z → Y
    gr = f ∘ invert r

  g-iso : Y ≅ Z
  g-iso = b⇒≅ (g , (gl , _≅_.iso₁ s) , (gr , _≅_.iso₂ r))

  f-iso : X ≅ Y
  f-iso = record
    { to = f
    ; from = λ y → invert r (g y)
    ; iso₁ = _≅_.iso₁ r
    ; iso₂ = λ y → sym (_≅_.iso₁ g-iso (f (invert r (g y))))
                 · ap (invert g-iso) (_≅_.iso₂ r (g y))
                 · _≅_.iso₁ g-iso y }

  h-iso : Z ≅ W
  h-iso = record
    { to = h
    ; from = λ w → g (invert s w)
    ; iso₁ = λ z → sym (ap (λ z → g (invert s (h z))) (_≅_.iso₂ g-iso z))
                 · ap g (_≅_.iso₁ s (invert g-iso z))
                 · _≅_.iso₂ g-iso z
    ; iso₂ = _≅_.iso₂ s }

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module _ {I : Set} where

postulate
  f : ∀ {T : I → Set} {i} → T i → Set

variable
  i : I
  T : I → Set
  v : T i

t : f v
t = {!!}