text:
------------------------------------------------------------------------
-- An up-to technique for weak similarity
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Labelled-transition-system

module Similarity.Weak.Up-to {ℓ} (lts : LTS ℓ) where

open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Equational-reasoning
open import Expansion lts using (Expansion)
open import Relation
open import Similarity.Weak lts
import Similarity.Weak.Equational-reasoning-instances
import Up-to

open LTS lts

------------------------------------------------------------------------
-- The general up-to machinery, instantiated with the StepC container

open Up-to StepC public

------------------------------------------------------------------------
-- An example

-- Up to expansion to the left and weak similarity to the right.
--
-- This is a generalisation of the non-symmetric up-to technique
-- presented by Pous and Sangiorgi in Section 6.5.2.4 of "Enhancements
-- of the bisimulation proof method".

Up-to-expansion-and-weak-similarity : Trans₂ ℓ Proc
Up-to-expansion-and-weak-similarity R =
  Expansion ∞ ⊙ R ⊙ Weak-similarity ∞

-- The relation transformer is monotone.

up-to-expansion-and-weak-similarity-monotone :
  Monotone Up-to-expansion-and-weak-similarity
up-to-expansion-and-weak-similarity-monotone R⊆S =
  Σ-map id (Σ-map id (Σ-map id (Σ-map R⊆S id)))

-- The relation transformer is size-preserving.

up-to-expansion-and-weak-similarity-size-preserving :
  Size-preserving Up-to-expansion-and-weak-similarity
up-to-expansion-and-weak-similarity-size-preserving =
  _⇔_.from (monotone→⇔ up-to-expansion-and-weak-similarity-monotone)
    (λ where
       {x = p , q} (r , p≳r , s , r≼s , s≼q) →
         p  ∼⟨ p≳r ⟩
         r  ∼′⟨ r≼s ⟩ ≼:
         s  ∼⟨ s≼q ⟩■
         q)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
{-# OPTIONS --without-K #-}
module pointed.equality where

open import sum
open import equality.core
open import function.extensionality
open import function.isomorphism.core
open import function.isomorphism.utils
open import pointed.core

pmap-eq : ∀ {i j}{X : Set i}{Y : Set j}{x₀ : X}{y₀ : Y}
        → {f : X → Y}{p : f x₀ ≡ y₀}
        → {g : X → Y}{q : g x₀ ≡ y₀}
        → (Σ ((x : X) → f x ≡ g x) λ γ → p ≡ γ x₀ · q)
        ≅ _≡_ {A = PMap (X , x₀) (Y , y₀)} (f , p) (g , q)
pmap-eq {X = X}{Y}{x₀}{y₀} = Σ-ap-iso' strong-funext-iso lem ·≅ Σ-split-iso
  where
    lem : {f : X → Y}{p : f x₀ ≡ y₀}
        → {g : X → Y}{q : g x₀ ≡ y₀}
        → (h : f ≡ g)
        → (p ≡ funext-inv h x₀ · q)
        ≅ (subst (λ u → u x₀ ≡ y₀) h p ≡ q)
    lem refl = refl≅

ext: agda

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Unit.Pointed where

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

open import Cubical.Data.Unit

private
  variable
    ℓ : Level

Unit∙ : Pointed ℓ
Unit∙ = Unit* , tt*

max_stars_repo_name: FernandoLarrain/cubical


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

module Data.Bits.Fold where

open import Data.Bits
open import Strict
open import Prelude

module _ {a} {A : Type a} (zer : A → A) (one : A → A) (base : A) where
  foldr-bits : Bits → A
  foldr-bits [] = base
  foldr-bits (0∷ xs) = zer (foldr-bits xs)
  foldr-bits (1∷ xs) = one (foldr-bits xs)

foldr-universal : ∀ (h : Bits → A) z o e →
                    (h [] ≡ e) →
                    (∀ xs → h (0∷ xs) ≡ z (h xs)) →
                    (∀ xs → h (1∷ xs) ≡ o (h xs)) →
                    ∀ xs → h xs ≡ foldr-bits z o e xs
foldr-universal h z o e base zer one [] = base
foldr-universal h z o e base zer one (0∷ xs) = zer xs ; cong z (foldr-universal h z o e base zer one xs)
foldr-universal h z o e base zer one (1∷ xs) = one xs ; cong o (foldr-universal h z o e base zer one xs)

module _ {a} {A : Type a} (zer : A → A) (one : A → A) where
  foldl-go : Bits → A → A
  foldl-go []      base = base
  foldl-go (0∷ xs) base = foldl-go xs $! zer base
  foldl-go (1∷ xs) base = foldl-go xs $! one base

  foldl-bits : A → Bits → A
  foldl-bits = λ base xs → foldl-go xs $! base
  {-# INLINE foldl-bits #-}

foldl-universal : ∀ (h : Bits → A → A) z o e →
                  (∀ xs bs → h (0∷ xs) bs ≡ h xs (z bs)) →
                  (∀ xs bs → h (1∷ xs) bs ≡ h xs (o bs)) →
                  (∀ bs → h [] bs ≡ bs) →
                  ∀ xs → h xs e ≡ foldl-bits z o e xs
foldl-universal h z o e zer one bs [] = bs e ; sym ($!-≡ (foldl-go z o []) e)
foldl-universal h z o e zer one bs (0∷ xs) = zer xs e ; foldl-universal h z o (z e) zer one bs xs ; sym ($!-≡ (foldl-go z o (0∷ xs)) e)
foldl-universal h z o e zer one bs (1∷ xs) = one xs e ; foldl-universal h z o (o e) zer one bs xs ; sym ($!-≡ (foldl-go z o (1∷ xs)) e)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Setoids.Subset
open import Setoids.Setoids
open import Setoids.Orders
open import Fields.Fields
open import Rings.Orders.Total.Definition
open import Rings.Orders.Total.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Definition
open import Fields.Orders.LeastUpperBounds.Definition
open import Numbers.ClassicalReals.RealField
open import Groups.Definition
open import Groups.Homomorphisms.Definition
open import Rings.Homomorphisms.Definition
open import Sets.EquivalenceRelations
open import Semirings.Definition

open import Numbers.Naturals.Semiring
open import Numbers.Integers.Definition
open import Numbers.Integers.RingStructure.Ring

module Numbers.ClassicalReals.RealField.AllIsomorphic (ℝ : RealField) where

open RealField ℝ
open Ring R
open Group additiveGroup
open Setoid S
open Equivalence eq
open import Rings.Lemmas R
open import Groups.Lemmas additiveGroup

fromN : ℕ → A
fromN zero = 0R
fromN (succ n) = 1R + fromN n

fromNPreserves+ : (a b : ℕ) → fromN (a +N b) ∼ (fromN a) + (fromN b)
fromNPreserves+ zero b = symmetric identLeft
fromNPreserves+ (succ a) b = transitive (+WellDefined reflexive (fromNPreserves+ a b)) +Associative

fromNPreserves* : (a b : ℕ) → fromN (a *N b) ∼ (fromN a) * (fromN b)
fromNPreserves* zero b = symmetric (transitive *Commutative timesZero)
fromNPreserves* (succ a) b = transitive (transitive (fromNPreserves+ b (a *N b)) (+WellDefined (symmetric identIsIdent) (fromNPreserves* a b))) (symmetric *DistributesOver+')

fromNWellDefined : {a b : ℕ} → a ≡ b → fromN a ∼ fromN b
fromNWellDefined refl = reflexive

fromZ : ℤ → A
fromZ (nonneg x) = fromN x
fromZ (negSucc x) = inverse (fromN (succ x))

private
  lemma : (a : ℕ) → (b : ℕ) → (1R + fromN (succ a *N b +N a)) ∼ ((1R + fromN a) * (1R + fromN b))
  lemma a b = transitive (transitive (transitive (+WellDefined reflexive (transitive (fromNPreserves+ ((succ a) *N b) a) (transitive groupIsAbelian (+WellDefined reflexive (transitive (fromNPreserves+ b (a *N b)) (+WellDefined (symmetric identIsIdent) (fromNPreserves* a b))))))) +Associative) (+WellDefined (transitive (symmetric identIsIdent) *Commutative) (symmetric *DistributesOver+'))) (symmetric *DistributesOver+)

fromZPreserves+ : (a b : ℤ) → fromZ (a +Z b) ∼ (fromZ a) + (fromZ b)
fromZPreserves+ (nonneg zero) (nonneg y) = symmetric identLeft
fromZPreserves+ (nonneg (succ x)) (nonneg y) = transitive (+WellDefined reflexive (fromNPreserves+ x y)) +Associative
fromZPreserves+ (nonneg zero) (negSucc y) = symmetric identLeft
fromZPreserves+ (nonneg (succ x)) (negSucc zero) = transitive (transitive (transitive (transitive (symmetric identLeft) (+WellDefined (symmetric invLeft) reflexive)) (symmetric +Associative)) (+WellDefined (inverseWellDefined (symmetric identRight)) reflexive)) (groupIsAbelian)
fromZPreserves+ (nonneg (succ x)) (negSucc (succ y)) = transitive (fromZPreserves+ (nonneg x) (negSucc y)) (transitive (transitive (transitive (transitive (transitive (transitive (transitive (symmetric identLeft) +Associative) groupIsAbelian) (+WellDefined reflexive (+WellDefined (symmetric invLeft) reflexive))) (+WellDefined reflexive (symmetric +Associative))) +Associative) groupIsAbelian) (+WellDefined reflexive (symmetric invContravariant)))
fromZPreserves+ (negSucc zero) (nonneg zero) = symmetric identRight
fromZPreserves+ (negSucc zero) (nonneg (succ y)) = transitive (transitive (symmetric identLeft) (+WellDefined (symmetric (transitive (+WellDefined reflexive (symmetric identRight)) invLeft)) reflexive)) (symmetric +Associative)
fromZPreserves+ (negSucc (succ x)) (nonneg zero) = symmetric identRight
fromZPreserves+ (negSucc (succ x)) (nonneg (succ y)) = transitive (fromZPreserves+ (negSucc x) (nonneg y)) (transitive (transitive (+WellDefined reflexive (transitive (symmetric identLeft) (transitive (+WellDefined (symmetric invLeft) reflexive) (symmetric +Associative)))) +Associative) (+WellDefined (symmetric invContravariant) reflexive))
fromZPreserves+ (negSucc x) (negSucc y) = transitive (transitive invContravariant (transitive (+WellDefined invContravariant reflexive) (transitive (+WellDefined (transitive (transitive (+WellDefined (transitive (inverseWellDefined (fromNPreserves+ x y)) invContravariant) reflexive) (symmetric +Associative)) groupIsAbelian) reflexive) (symmetric +Associative)))) (+WellDefined (symmetric invContravariant) (symmetric invContravariant))

fromZPreserves* : (a b : ℤ) → fromZ (a *Z b) ∼ (fromZ a) * (fromZ b)
fromZPreserves* (nonneg a) (nonneg b) = fromNPreserves* a b
fromZPreserves* (nonneg zero) (negSucc b) = symmetric (transitive *Commutative timesZero)
fromZPreserves* (nonneg (succ a)) (negSucc b) = transitive (inverseWellDefined (lemma a b)) (symmetric ringMinusExtracts)
fromZPreserves* (negSucc a) (nonneg zero) = symmetric timesZero
fromZPreserves* (negSucc a) (nonneg (succ b)) = transitive (inverseWellDefined (transitive (+WellDefined reflexive (fromNWellDefined {(a +N b *N a) +N b} {(b +N a *N b) +N a} (transitivity (Semiring.commutative ℕSemiring _ b) (transitivity (applyEquality (b +N_) (transitivity (Semiring.commutative ℕSemiring a _) (applyEquality (_+N a) (multiplicationNIsCommutative b a)))) (Semiring.+Associative ℕSemiring b _ a))))) (lemma a b))) (symmetric ringMinusExtracts')
fromZPreserves* (negSucc a) (negSucc b) = transitive (transitive (+WellDefined reflexive (fromNWellDefined {b +N a *N succ b} {(b +N a *N b) +N a} (transitivity (applyEquality (b +N_) (transitivity (multiplicationNIsCommutative a (succ b)) (transitivity (Semiring.commutative ℕSemiring a _) (applyEquality (_+N a) (multiplicationNIsCommutative b a))))) (Semiring.+Associative ℕSemiring b _ a)))) (lemma a b)) (symmetric twoNegativesTimes)

ringHom : RingHom ℤRing R fromZ
RingHom.preserves1 ringHom = identRight
RingHom.ringHom ringHom {r} {s} = fromZPreserves* r s
GroupHom.groupHom (RingHom.groupHom ringHom) {r} {s} = fromZPreserves+ r s
GroupHom.wellDefined (RingHom.groupHom ringHom) refl = reflexive


text:
-- {-# OPTIONS --allow-unsolved-metas #-}
module GUIgeneric.GUIFeaturesPart5 where

open import GUIgeneric.Prelude renaming (addButton to addButton')

open import GUIgeneric.GUIDefinitions renaming (add to add'; add' to add)
open import GUIgeneric.GUI
open import GUIgeneric.GUIExampleLib
open import StateSizedIO.GUI.WxGraphicsLibLevel3 renaming (addButton to addButton')
open import GUIgeneric.GUIFeatures
open import GUIgeneric.GUIFeaturesPart2 hiding ( main ; main1 )
open import GUIgeneric.GUIFeaturesPart3 hiding ( main ; Tea ; Cancel)
open import GUIgeneric.GUIFeaturesPart4 hiding ( main ; cancelNewStateSM ; cancelStateAdded ; cancelFeatureAdded  )
open import GUIgeneric.GUIExample hiding (main )

data StatesBasicVM : Set where
  pay change soda serveSoda  open' close : StatesBasicVM

basicVM : FMachine StatesBasicVM
basicVM  .Features = ⊤
basicVM  .AddStateF = ⊥
basicVM  .GUIF f (inj₁ pay)        =
         simpleSMState "Pay" (inj₁ change)
basicVM  .GUIF f (inj₁ change)     =
         simpleSMState "Get Change" (inj₁ soda)
basicVM  .GUIF f (inj₁ soda)       =
         simpleSMState "Soda" (inj₁ serveSoda)
basicVM  .GUIF f (inj₁ serveSoda)  =
         simpleSMState "Serve Soda" (inj₁ open')
basicVM  .GUIF f (inj₁ open')      =
         simpleSMState "Open" (inj₁ close)
basicVM  .GUIF f (inj₁ close)      =
         simpleSMState "Close" (inj₁ pay)
basicVM  .GUIF f (inj₂ ())

newState : {A B : Set} → A ⊎ B ⊎ ⊤
newState = (inj₂ (inj₂ tt))

{- handler for the new state to be added to the tea machine -}
teaNewStateSM :  (fm : FMachine StatesBasicVM)
                 →    SMachineState
                      (StatesBasicVM ⊎ fm .AddStateF ⊎ ⊤)
                      newState
teaNewStateSM fm = simpleSMState "Serve Tea" (inj₁ open')

{- add the new state to the feature machine -}
TeaMAddNewState :  FMachine StatesBasicVM
                   → FMachine StatesBasicVM
TeaMAddNewState fm =
  addOneStateFMachine fm (teaNewStateSM fm)

{- add a dummy feature "FeatureTea" to the feature machine -}
TeaMAddFeature :  FMachine StatesBasicVM
                  → FMachine StatesBasicVM
TeaMAddFeature fm = addDummyFeatures
                         (TeaMAddNewState fm)
                         FeatureTea

{- redefine in the feature machine one button -}
Tea :  FMachine StatesBasicVM
       → FMachine StatesBasicVM
Tea fm .Features   = TeaMAddFeature fm .Features
Tea fm .AddStateF  = TeaMAddFeature fm .AddStateF
Tea fm .GUIF (f , yesTea) (inj₁ soda) =
      addBtn2StateMachine
      (  TeaMAddFeature fm .GUIF
         (f , yesTea) (inj₁ soda))
         "Tea" newState
Tea fm .GUIF f  s = TeaMAddFeature fm .GUIF f s

{- handler for the new state to be added to the cancel machine -}
cancelNewStateSM : (fm : FMachine StatesBasicVM) →
                    SMachineState (StatesBasicVM ⊎ fm .AddStateF ⊎ ⊤) newState
cancelNewStateSM fm = simpleSMState "Cancelling" (inj₁ pay)

{- add the state to the old feature machine -}
cancelStateAdded : FMachine StatesBasicVM → FMachine StatesBasicVM
cancelStateAdded fm = addOneStateFMachine fm (cancelNewStateSM fm)

{- add a dummy feature "FeatureCancel" to the feature machine -}
cancelFeatureAdded : FMachine StatesBasicVM → FMachine StatesBasicVM
cancelFeatureAdded fm = addDummyFeatures
                         (cancelStateAdded fm)
                         FeatureCancel

{- redefine in the feature machine one button -}
Cancel :  FMachine StatesBasicVM
          → FMachine StatesBasicVM
Cancel fm .Features = cancelFeatureAdded fm .Features
Cancel fm .AddStateF  = cancelFeatureAdded fm .AddStateF
Cancel fm .GUIF (f , yesCancel) (inj₁ soda) =
      addBtn2StateMachine (cancelFeatureAdded fm .GUIF (f , yesCancel) (inj₁ soda))
                          "Cancel" newState
Cancel fm .GUIF f  s = cancelFeatureAdded fm .GUIF f s

{- add the Dummy free feature -}
FreeMAddFeature : FMachine StatesBasicVM
                  → FMachine StatesBasicVM
FreeMAddFeature fm = addDummyFeatures fm FeatureFree

{- redefine the pay button to free in case feature free is yesFree -}
Free :  FMachine StatesBasicVM
        → FMachine StatesBasicVM
Free fm .Features   = FreeMAddFeature fm .Features
Free fm .AddStateF  = FreeMAddFeature fm .AddStateF
Free fm .GUIF (f , yesFree) (inj₁ pay) =
      simpleSMState "Free" (inj₁ soda)
Free fm .GUIF (f , yesFree) (inj₁ open') =
      simpleSMState "Skip" (inj₁ pay)
Free fm .GUIF f  s  = FreeMAddFeature fm .GUIF f s

main1 : NativeIO Unit
main1 = compileFeatureVM (Tea (Cancel basicVM)) ((_ , yesCancel) , yesTea) (inj₁ pay)

main2 : NativeIO Unit
main2 = compileFeatureVM (Free basicVM) (_ , yesFree) (inj₁ pay) --

multiFeatureMachine : FMachine StatesBasicVM
multiFeatureMachine = Free (Cancel (Tea basicVM))

main : NativeIO Unit
main = compileFeatureVM
       multiFeatureMachine
       (((_ , yesTea) , yesCancel) , noFree) (inj₁ pay)

max_stars_repo_name: stephanadls/state-dependent-gui

max_issues_repo_name: stephanadls/state-dependent-gui

max_forks_repo_name: stephanadls/state-dependent-gui


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

module Relation.Binary.Bool where

open import Prelude

-- record TotalOrder {e} (E : Type e) : Type e where
--   field
--     _≤?_ : E → E → Bool

--   _≤_ : E → E → Type


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

open import Definition.Typed.EqualityRelation

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

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties.Reflexivity

open import Tools.Product
import Tools.PropositionalEquality as PE

import Data.Fin as Fin
import Data.Nat as Nat

-- Reducible types are well-formed.
escape : ∀ {l Γ A r} → Γ ⊩⟨ l ⟩ A ^ r → Γ ⊢ A ^ r
escape (Uᵣ′ _ _ _ _ _ PE.refl [[ ⊢A , ⊢B , D ]]) = ⊢A
escape (ℕᵣ [[ ⊢A , ⊢B , D ]]) = ⊢A
escape (Emptyᵣ [[ ⊢A , ⊢B , D ]]) = ⊢A
escape (ne′ K [[ ⊢A , ⊢B , D ]] neK K≡K) = ⊢A
escape (Πᵣ′ rF lF lG _ _ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) = ⊢A
escape (∃ᵣ′ F G [[ ⊢A , ⊢B , D ]] ⊢F ⊢G A≡A [F] [G] G-ext) = ⊢A
escape {ι ¹} (emb X A) = escape A
escape {∞} (emb X A) = escape A

-- Reducible type equality respect the equality relation.
escapeEq : ∀ {l Γ A B r} → ([A] : Γ ⊩⟨ l ⟩ A ^ r)
            → Γ ⊩⟨ l ⟩ A ≡ B ^ r / [A]
            → Γ ⊢ A ≅ B ^ r
escapeEq (Uᵣ′ _ _ _ ⁰ _ PE.refl [[ ⊢A , ⊢B , D ]]) D′ = ≅-red D D′ Uₙ Uₙ (≅-univ (≅-U⁰refl (wf ⊢A)))
escapeEq (Uᵣ′ _ _ _ ¹ _ PE.refl [[ ⊢A , ⊢B , D ]]) D′ = ≅-red D D′ Uₙ Uₙ (≅-U¹refl (wf ⊢A))
escapeEq (ℕᵣ [[ ⊢A , ⊢B , D ]]) D′ = ≅-red D D′ ℕₙ ℕₙ (≅-univ (≅ₜ-ℕrefl (wf ⊢A)))
escapeEq (Emptyᵣ [[ ⊢A , ⊢B , D ]]) D′ = ≅-red D D′ Emptyₙ Emptyₙ (≅-univ ((≅ₜ-Emptyrefl (wf ⊢A))))
escapeEq (ne′ K D neK K≡K) (ne₌ M D′ neM K≡M) =
  ≅-red (red D) (red D′) (ne neK) (ne neM) (~-to-≅ K≡M)
escapeEq (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
             (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ≅-red (red D) D′ Πₙ Πₙ A≡B
escapeEq (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
             (∃₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ≅-red (red D) D′ ∃ₙ ∃ₙ A≡B
escapeEq {ι ¹} (emb X A) A≡B = escapeEq A A≡B
escapeEq {∞} (emb X A) A≡B = escapeEq A A≡B

-- Reducible terms are well-formed.
escapeTerm : ∀ {l Γ A t r} → ([A] : Γ ⊩⟨ l ⟩ A ^ r)
              → Γ ⊩⟨ l ⟩ t ∷ A ^ r / [A]
              → Γ ⊢ t ∷ A ^ r
escapeTerm (Uᵣ′ _ _ _ _ l< PE.refl D) (Uₜ A [[ ⊢t , ⊢u , d ]] typeA A≡A [A]) = conv ⊢t (sym (subset* (red D)))
escapeTerm (ℕᵣ D) (ℕₜ n [[ ⊢t , ⊢u , d ]] t≡t prop) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (Emptyᵣ D) (Emptyₜ (ne ⊢t)) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm {r = [ ! , l ]} (ne′ K D neK K≡K) (neₜ k [[ ⊢t , ⊢u , d ]] nf) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm {r = [ % , l ]} (ne′ K D neK K≡K) (neₜ d) = d
escapeTerm {r = [ ! , l ] } (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
               (f , [[ ⊢t , ⊢u , d ]] , funcF , f≡f , [f] , [f]₁) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm {r = [ % , l ]} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ⊢t = conv ⊢t (sym (subset* (red D)))
escapeTerm (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) ⊢t = conv ⊢t (sym (subset* (red D)))
escapeTerm {ι ¹} (emb X A) t = escapeTerm A t
escapeTerm {∞} (emb X A) t = escapeTerm A t

-- Reducible term equality respect the equality relation.
escapeTermEq : ∀ {l Γ A t u r} → ([A] : Γ ⊩⟨ l ⟩ A ^ r)
                → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ r / [A]
                → Γ ⊢ t ≅ u ∷ A ^ r
escapeTermEq (Uᵣ′ _ _ _ _ l< PE.refl D) (Uₜ₌ (Uₜ A d typeA A≡A [t]) (Uₜ B d′ typeB B≡B [u]) A≡B [A≡B]) = ≅ₜ-red (red D) (redₜ d) (redₜ d′) Uₙ (typeWhnf typeA) (typeWhnf typeB) A≡B
escapeTermEq (ℕᵣ D) (ℕₜ₌ k k′ d d′ k≡k′ prop) =
  let natK , natK′ = split prop
  in  ≅ₜ-red (red D) (redₜ d) (redₜ d′) ℕₙ
             (naturalWhnf natK) (naturalWhnf natK′) k≡k′
escapeTermEq (Emptyᵣ D) (Emptyₜ₌ (ne ⊢t ⊢u)) =
  ~-to-≅ₜ (~-irrelevance ((conv ⊢t (sym (subset* (red D)))))  ((conv ⊢u (sym (subset* (red D))))))
escapeTermEq {r = [ ! , l ]} (ne′ K D neK K≡K)
                 (neₜ₌ k m d d′ (neNfₜ₌ neT neU t≡u)) =
  ≅ₜ-red (red D) (redₜ d) (redₜ d′) (ne neK) (ne neT) (ne neU)
         (~-to-≅ₜ t≡u)
escapeTermEq {r = [ % , l ]} (ne′ K D neK K≡K)
                 (neₜ₌ d d′) = ~-to-≅ₜ (~-irrelevance d d′)
escapeTermEq {r = [ ! , l ]} (Πᵣ′ rF lF lG _ _  F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                 (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g]) =
  ≅ₜ-red (red D) (redₜ d) (redₜ d′) Πₙ (functionWhnf funcF) (functionWhnf funcG) f≡g
escapeTermEq {r = [ % , l ] } (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (⊢t , ⊢u) = ~-to-≅ₜ (~-irrelevance ((conv ⊢t (sym (subset* (red D))))) ((conv ⊢u (sym (subset* (red D))))))
escapeTermEq (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (⊢t , ⊢u) = ~-to-≅ₜ (~-irrelevance ((conv ⊢t (sym (subset* (red D))))) ((conv ⊢u (sym (subset* (red D))))))
escapeTermEq {ι ¹} (emb X A) t≡u = escapeTermEq A t≡u
escapeTermEq {∞} (emb X A) t≡u = escapeTermEq A t≡u

escapeEqRefl : ∀ {l Γ A r}
            → ([A] : Γ ⊩⟨ l ⟩ A ^ r)
            → Γ ⊢ A ≅ A ^ r
escapeEqRefl [A] = escapeEq [A] (reflEq [A])

escapeEqReflTerm : ∀ {l Γ A t r}
            → ([A] : Γ ⊩⟨ l ⟩ A ^ r)
            → ([t] : Γ ⊩⟨ l ⟩ t ∷ A ^ r / [A])
            → Γ ⊢ t ≅ t ∷ A ^ r
escapeEqReflTerm [A] [t] = escapeTermEq [A] (reflEqTerm [A] [t])

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

-- We do not parameterize this module since we do not have access to _+_ or _*_
-- for the fields that we want (real numbers)

module FLA.Algebra.Structures where

open import Level using (Level) renaming (suc to lsuc)
open import Data.Sum using (_⊎_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)

private
  variable
    ℓ : Level
    A : Set ℓ

record Field (A : Set ℓ) : Set ℓ where

  infixl 6 _+_
  infixl 7 _*_
  infixl 9 -_
  infixl 10 _⁻¹

  field
    _+_ : A → A → A
    _*_ : A → A → A

    0ᶠ   : A
    1ᶠ   : A
    -_   : A → A -- + inverse
    _⁻¹  : A → A -- * inverse

    +-assoc   : (a b c : A) → a + (b + c) ≡ (a + b) + c
    +-comm    : (a b : A)   → a + b ≡ b + a
    +0ᶠ       : (a : A)     → a + 0ᶠ ≡ a
    +-inv     : (a : A)     → - a + a ≡ 0ᶠ
    *-assoc   : (a b c : A) → a * (b * c) ≡ (a * b) * c
    *-comm    : (a b : A)   → a * b ≡ b * a
    *1ᶠ       : (a : A)     → a * 1ᶠ ≡ a
    *-inv     : (a : A)     → (a ≢ 0ᶠ) → a ⁻¹ * a ≡ 1ᶠ
    *-distr-+ : (a b c : A) → a * (b + c) ≡ a * b + a * c

record TotalOrder (A : Set ℓ) : Set (lsuc ℓ) where

  infixl 5 _≤_

  field
    _≤_ : A → A → Set ℓ

    total : (x y : A) → x ≤ y ⊎ y ≤ x
    trans : (x y z : A) → x ≤ y → y ≤ z → x ≤ z
    anti-sym : (x y : A) → x ≤ y → y ≤ x → x ≡ y

record TotalOrderField (A : Set ℓ) : Set (lsuc ℓ) where

  field
    ⦃ F ⦄ : Field A
    ⦃ TO ⦄ : TotalOrder A

  open Field F public
  open TotalOrder TO public

  field
    x≤y→z+x≤z+y : (x y z : A) → x ≤ y → z + x ≤ z + y
    0≤x→0≤y→0≤x*y : (x y : A) → 0ᶠ ≤ x → 0ᶠ ≤ y → 0ᶠ ≤ x * y

-- record CompleteOrderedField (A : Set ℓ) : Set (lsuc ℓ) where
--   field
--     ⦃ TOF ⦄ : TotalOrderField A

--   open LinearlyOrderedField LinOrdField
--
--   UpperBound : Data.Set.NonEmpty A → Data.Set
--   Supremum : (∀ (v : UpperBound(A)) → ∃ [u ∈ UpperBound(A)] [u ≤ v])
--   completeness : (S : Data.Set.NonEmpty A)
--                → (ub: ∃ [y ∈ A] (λ x ∈ S → x ≤ y))
--                → Supremum A
--   completeness : every non-empty subset of F, bounded above, has a
--     supremum in F. If A is a non-empty subset of R, and if A has an upper
--     bound, then A has a least upper bound u, such that for every upper
--     bound v of A, u ≤ v.
--   apparently completeness implies the archimedian principle.

{-
If we want the reals, we need a few things

Linearly ordered set on F, ∀ x, y, z ∈ F
  Totality : x ≤ y or y ≤ x
  Transitivity : if x ≤ y and y ≤ z then x ≤ z
  Anti-symmetry : if x ≤ y and y ≤ x, then x ≡ y

Linearly ordered field (F, +, *, ≤) if
  x ≤ y then z + x ≤ z + y
  0 ≤ x and 0 ≤ y then 0 ≤ x*y

Complete ordered field (F, +, *, ≤) if
  (F, +, *, ≤) is a linearly ordered field
  Completeness : every non-empty subset of F, bounded above, has a supremum in F

Archimedian property:
  (F, +, *, ≤) is a complete ordered field
  r, s ∈ F. r > 0 ∃ n ∈ ℕ. s < r + ... + r (n times)

  Roughly speaking, it is the property of having no infinitely large or
  infinitely small elements

  Axiom of Archimedies is a formulation of this property for ordered fields:
    ∀ ε ∈ F. ε > 0 → ∃ n ∈ ℕ . 1/n < ε

Cauchy sequences representation of the reals and the Dedekind representation
of the reals are both Archimedian completely ordered fields and hence
isomorphic to the reals. Note there is a proof that all Archimedian complete
ordered fields are isomorphic.

References:
[1]: https://www.cs.swan.ac.uk/~csetzer/articlesFromOthers/chiMing/chiMingChuangExtractionOfProgramsForExactRealNumberComputation.pdf
[2]: https://en.wikipedia.org/wiki/Axiomatic_theory_of_real_numbers
-}

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:
{-# OPTIONS --safe #-}
module Cubical.Categories.Constructions.FullSubcategory where
-- Full subcategory (not necessarily injective on objects)

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Categories.Category
open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId)

private
  variable
    ℓC ℓC' ℓD ℓD' ℓE ℓE' ℓP ℓQ ℓR : Level

module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP) where
  private
    module C = Category C
  open Category
  open Functor

  FullSubcategory : Category (ℓ-max ℓC ℓP) ℓC'
  ob FullSubcategory = Σ[ x ∈ C.ob ] P x
  Hom[_,_] FullSubcategory (x , p) (y , q) = C.Hom[ x , y ]
  id FullSubcategory = C.id
  _⋆_ FullSubcategory = C._⋆_
  ⋆IdL FullSubcategory = C.⋆IdL
  ⋆IdR FullSubcategory = C.⋆IdR
  ⋆Assoc FullSubcategory = C.⋆Assoc
  isSetHom FullSubcategory = C.isSetHom

  FullInclusion : Functor FullSubcategory C
  F-ob FullInclusion = fst
  F-hom FullInclusion = idfun _
  F-id FullInclusion = refl
  F-seq FullInclusion f g = refl

module _ (C : Category ℓC ℓC')
         (D : Category ℓD ℓD') (Q : Category.ob D → Type ℓQ) where
  private
    module C = Category C
    module D = Category D
  open Category
  open Functor

  ToFullSubcategory  : (F : Functor C D) → ((c : C.ob) → Q (F-ob F c)) → Functor C (FullSubcategory D Q)
  F-ob (ToFullSubcategory F f) c = F-ob F c , f c
  F-hom (ToFullSubcategory F f) = F-hom F
  F-id (ToFullSubcategory F f) = F-id F
  F-seq (ToFullSubcategory F f) = F-seq F

module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP)
         (D : Category ℓD ℓD') (Q : Category.ob D → Type ℓQ) where
  private
    module C = Category C
    module D = Category D
  open Category
  open Functor

  MapFullSubcategory : (F : Functor C D) → ((c : C.ob) → P c → Q (F-ob F c))
    → Functor (FullSubcategory C P) (FullSubcategory D Q)
  MapFullSubcategory F f = ToFullSubcategory (FullSubcategory C P) D Q
    (funcComp F (FullInclusion C P) )
    λ (c , p) → f c p

module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP) where
  private
    module C = Category C
  open Category
  open Functor

  MapFullSubcategory-id :
    MapFullSubcategory C P C P (funcId C) (λ c p → p) ≡ funcId (FullSubcategory C P)
  MapFullSubcategory-id = Functor≡
    (λ (c , p) → refl)
    (λ γ → refl)

module _ (C : Category ℓC ℓC') (P : Category.ob C → Type ℓP)
         (D : Category ℓD ℓD') (Q : Category.ob D → Type ℓQ)
         (E : Category ℓE ℓE') (R : Category.ob E → Type ℓR) where
  private
    module C = Category C
    module D = Category D
    module E = Category E
  open Category
  open Functor

  MapFullSubcategory-seq :
    (F : Functor C D) → (f : (c : C.ob) → P c → Q (F-ob F c)) →
    (G : Functor D E) → (g : (d : D.ob) → Q d → R (F-ob G d)) →
    MapFullSubcategory C P E R (funcComp G F) (λ c p → g (F-ob F c) (f c p)) ≡
    funcComp
      (MapFullSubcategory D Q E R G g)
      (MapFullSubcategory C P D Q F f)
  MapFullSubcategory-seq F f G g = Functor≡
    (λ (c , p) → refl)
    (λ γ → refl)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.ListedFiniteSet where

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

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED.
------------------------------------------------------------------------

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

module Algebra.FunctionProperties.Consequences.Core
  {a} {A : Set a} where

{-# WARNING_ON_IMPORT
"Algebra.FunctionProperties.Consequences.Core was deprecated in v1.3.
Use Algebra.Consequences.Base instead."
#-}

open import Algebra.Consequences.Base public


text:
module OldO where

open import Data.Product
open import Function renaming (_∘_ to _○_)

open import Circle

------------------------------------------------------------------------------
-- Abstract interpretation:
-- natural numbers with paths equating all even numbers in one
-- connected component and all odd numbers in another connected
-- component

-- module with 0,1,2,3,4 ... this is the concrete domain

data N : Set where
  Zero  : N
  One   : N
  Two   : N
  Three : N
  Four  : N

recN : (C : Set) → C → C → C → C → C → N → C
recN C c0 c1 c2 c3 c4 Zero = c0
recN C c0 c1 c2 c3 c4 One = c1
recN C c0 c1 c2 c3 c4 Two = c2
recN C c0 c1 c2 c3 c4 Three = c3
recN C c0 c1 c2 c3 c4 Four = c4

indN : (C : N → Set) → C Zero → C One → C Two → C Three → C Four → (n : N) → C n
indN C c0 c1 c2 c3 c4 Zero = c0
indN C c0 c1 c2 c3 c4 One = c1
indN C c0 c1 c2 c3 c4 Two = c2
indN C c0 c1 c2 c3 c4 Three = c3
indN C c0 c1 c2 c3 c4 Four = c4

-- module for the abstract domain {even, odd} except that we don't define it
-- this way: we simply add paths between the even elements and paths between
-- the odd elements

module Parity where

  private
    data N* : Set where
      Zero*  : N*
      One*   : N*
      Two*   : N*
      Three* : N*
      Four*  : N*

  NA : Set
  NA = N*

  zero : NA
  zero = Zero*

  one : NA
  one = One*

  two : NA
  two = Two*

  three : NA
  three = Three*

  four : NA
  four = Four*

  postulate
    even02 : Zero* ≡ Two*
    even04 : Zero* ≡ Four*
    odd13  : One* ≡ Three*

  recNA : (C : Set) → (c0 c1 c2 c3 c4 : C) →
    (ceven02 : c0 ≡ c2) → (ceven04 : c0 ≡ c4) → (codd13 : c1 ≡ c3) →
    NA → C
  recNA C c0 c1 c2 c3 c4 _ _ _ Zero* = c0
  recNA C c0 c1 c2 c3 c4 _ _ _ One* = c1
  recNA C c0 c1 c2 c3 c4 _ _ _ Two* = c2
  recNA C c0 c1 c2 c3 c4 _ _ _ Three* = c3
  recNA C c0 c1 c2 c3 c4 _ _ _ Four* = c4

  postulate
    αrecNA02 : (C : Set) → (c0 c1 c2 c3 c4 : C) →
      (ceven02 : c0 ≡ c2) → (ceven04 : c0 ≡ c4) → (codd13 : c1 ≡ c3) →
      ap (recNA C c0 c1 c2 c3 c4 ceven02 ceven04 codd13) even02 ≡ ceven02

    αrecNA04 : (C : Set) → (c0 c1 c2 c3 c4 : C) →
      (ceven02 : c0 ≡ c2) → (ceven04 : c0 ≡ c4) → (codd13 : c1 ≡ c3) →
      ap (recNA C c0 c1 c2 c3 c4 ceven02 ceven04 codd13) even04 ≡ ceven04

    αrecNA13 : (C : Set) → (c0 c1 c2 c3 c4 : C) →
      (ceven02 : c0 ≡ c2) → (ceven04 : c0 ≡ c4) → (codd13 : c1 ≡ c3) →
      ap (recNA C c0 c1 c2 c3 c4 ceven02 ceven04 codd13) odd13 ≡ codd13

  indNA : (C : NA → Set) →
    (c0 : C Zero*) →
    (c1 : C One*) →
    (c2 : C Two*) →
    (c3 : C Three*) →
    (c4 : C Four*) →
    (ceven02 : transport C even02 c0 ≡ c2) →
    (ceven04 : transport C even04 c0 ≡ c4) →
    (codd13 : transport C odd13 c1 ≡ c3) →
    (n : NA) → C n
  indNA C c0 c1 c2 c3 c4 ceven02 ceven04 codd13 Zero* = c0
  indNA C c0 c1 c2 c3 c4 ceven02 ceven04 codd13 One* = c1
  indNA C c0 c1 c2 c3 c4 ceven02 ceven04 codd13 Two* = c2
  indNA C c0 c1 c2 c3 c4 ceven02 ceven04 codd13 Three* = c3
  indNA C c0 c1 c2 c3 c4 ceven02 ceven04 codd13 Four* = c4

open Parity

-- Now we define functions back and forth

abs : N → NA
abs = recN NA zero one two three four

con : NA → N
con = recNA N Zero One Zero One Zero (refl Zero) (refl Zero) (refl One)

conEven02 : ap con even02 ≡ refl Zero
conEven02 = αrecNA02 N Zero One Zero One Zero (refl Zero) (refl Zero) (refl One)

conEven04 : ap con even04 ≡ refl Zero
conEven04 = αrecNA04 N Zero One Zero One Zero (refl Zero) (refl Zero) (refl One)

conOdd13 : ap con odd13 ≡ refl One
conOdd13 = αrecNA13 N Zero One Zero One Zero (refl Zero) (refl Zero) (refl One)

-- Compose both ways

absconeven02 : ap (abs ○ con) even02 ≡ refl zero
absconeven02 =
  ap (abs ○ con) even02
    ≡⟨ {!!} ⟩
  ap abs (ap con even02)
    ≡⟨ {!!} ⟩
  ap abs (refl Zero)
    ≡⟨ {!!} ⟩
  refl zero ∎

absconeven04 : ap (abs ○ con) even04 ≡ refl zero
absconeven04 =
  ap (abs ○ con) even04
    ≡⟨ {!!} ⟩
  ap abs (ap con even04)
    ≡⟨ {!!} ⟩
  ap abs (refl Zero)
    ≡⟨ {!!} ⟩
  refl zero ∎

absconodd13 : ap (abs ○ con) odd13 ≡ refl one
absconodd13 =
  ap (abs ○ con) odd13
    ≡⟨ {!!} ⟩
  ap abs (ap con odd13)
    ≡⟨ {!!} ⟩
  ap abs (refl One)
    ≡⟨ {!!} ⟩
  refl one ∎

αeven02 : transport (λ x → (abs ○ con) x ≡ x) even02 (refl zero) ≡ even02
αeven02 =
  transport (λ x → (abs ○ con) x ≡ x) even02 (refl zero)
    ≡⟨ {!!} ⟩
  ! (ap (abs ○ con) even02) ∘ refl zero ∘ ap id even02
    ≡⟨ {!!} ⟩
  ! (ap (abs ○ con) even02) ∘ refl zero ∘ even02
    ≡⟨ {!!} ⟩
  ! (ap (abs ○ con) even02) ∘ even02
    ≡⟨ {!!} ⟩
  refl zero ∘ even02
    ≡⟨ {!!} ⟩
  even02 ∎

αeven04 : transport (λ x → (abs ○ con) x ≡ x) even04 (refl zero) ≡ even04
αeven04 =
  transport (λ x → (abs ○ con) x ≡ x) even04 (refl zero)
    ≡⟨ {!!} ⟩
  even04 ∎

αodd13 : transport (λ x → (abs ○ con) x ≡ x) odd13 (refl one) ≡ odd13
αodd13 =
  transport (λ x → (abs ○ con) x ≡ x) odd13 (refl one)
    ≡⟨ {!!} ⟩
  odd13 ∎

-- Galois connections...

αN : con ○ abs ○ con ○ abs ∼ con ○ abs
αN = indN (λ x → (con ○ abs ○ con ○ abs) x ≡ (con ○ abs) x)
     (refl Zero) (refl One) (refl Zero) (refl One) (refl Zero)

αNA : abs ○ con ∼ id
αNA = indNA (λ x → (abs ○ con) x ≡ x)
        (refl zero) (refl one) even02 odd13 even04
        αeven02 αeven04 αodd13

-- Computations on N and NA can be related
-- Concrete computation

incN : N → N
incN Zero = One
incN One = Two
incN Two = Three
incN Three = Four
incN Four = Zero

addN : N → N → N
addN Zero b = b
addN a Zero = a
addN One One = Two
addN One Two = Three
addN One Three = Four
addN One Four = Zero
addN Two One = Three
addN Two Two = Four
addN Two Three = Zero
addN Two Four = One
addN Three One = Four
addN Three Two = Zero
addN Three Three = One
addN Three Four = Two
addN Four One = Zero
addN Four Two = One
addN Four Three = Two
addN Four Four = Three

-- we can apply an operation in the abstract domain and report the
-- approximate result

absF : (N → N) → (NA → NA)
absF f = abs ○ f ○ con

approx : (N → N) → (N → N)
approx f n = con ((absF f) (abs n))

test0 : approx incN Zero ≡ One
test0 = refl One

test1 : approx incN One ≡ Zero
test1 = refl Zero

test2 : approx incN Two ≡ One
test2 = refl One

test3 : approx incN Three ≡ Zero
test3 = refl Zero

test4 : approx incN Four ≡ One
test4 = refl One

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Data.Finite where

open import Prelude
open import Data.Fin

𝒞 : Type a → Type a
𝒞 A = ∃ n × ∥ A ≃ Fin n ∥

ℂ : Type _
ℂ = Σ[ T ⦂ Type ] × 𝒞 T


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

   Copyright (c) 2020, 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Impl.Consensus.BlockStorage.BlockStore
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Crypto
open import Optics.All
open import Util.ByteString
open import Util.PKCS
open import Util.Prelude
open import Yasm.Base
open import Yasm.System ℓ-RoundManager ℓ-VSFP ConcSysParms

-- This module contains the machinery we use for tracking hash collisions for the hash function
-- postulated in LibraBFT.ImplShared.Util.Crypto.  (Note that, although we call it sha256 to remind
-- ourselves that this *represents* a real hash function, in fact it is just postulated and could
-- represent any hash function.)  We prove our correctness conditions modulo hash collisions of this
-- function, which is used to derive IDs for Blocks.  Therefore, how we model and reason about such
-- collisions is critical to the validity of our proofs.
--
-- A common approach is to simply assume (e.g., postulate or state as an axiom) that the function is
-- injective.  While this is a reasonable pragmatic approach, it does raise an important issue.
-- Because practical hash functions have unbounded domains and finite codomains, they are not
-- injective.  Therefore, assuming that the function represented by the postulated one is injective
-- amounts to making an unsatisfiable assumption, from which anything can be proved (false implies
-- anything).  For this reason, it is not sufficient to show that the desired property holds unless
-- a hash collision *exists*.  Instead, we must construct evidence of a *specific* hash collision
-- (i.e., two values and evidence that their hashes are the same but the values themselves are
-- different).  Such evidence is captured by the type NonInjective-≡ sha256.  Below we elaborate on
-- some subtleties and tradeoffs with what we prove in which contexts.
--
-- First, when we are dealing with *abstract* Records (as in the Abstract and Concrete modules), it
-- is trivial to construct an injectivity failure of Block IDs, simply by constructing two different
-- abstract Blocks that have the same ID.  In that context, it is important that we prove our
-- correctness conditions modulo injectivity failures between Blocks that are actually represented
-- in the specific ReachableSystemState about which we're reasoning (because that allows the
-- injectivity failure of IDs of the *abstract* Blocks to be related back to concrete blocks whose
-- IDs are derived using the hash function).
--
-- In contrast, it is far from trivial to construct a specific collision for the *postulated*
-- sha256-cr function.  It would be possible to prove that *some* collision *exists* by using a
-- pigeonhole principle counting argument.  In principle, one could then construct a specific
-- collision by generating 2 ^ 256 + 1 distinct Records (in case the postulated hash function is
-- assumed to produce 256-bit hashes), and asking for each pair of them whether they hash to the
-- same value.  We could eliminate the possibility that none of these pairs provides a collision
-- using the counting argument.
--
-- One could not do this "accidentally" (as could potentially occur with Abstract records), and
-- furthermore, by examining all proofs that use meta-no-collision, it is not difficult to see that
-- the specific collisions are all produced from Records introduced by the proof obligations (i.e.,
-- Records that are in the ReachableSystemState under consideration).  Therefore, we do not consider
-- it necessary to explicitly associate any collisions for the postulated hash function with the
-- ReachableSystemState.
--
-- Having received feedback from some people who were uncomfortable with this argument, we have put
-- some effort into explicitly tying each collision to data "in the system" in the
-- ReachableSystemState in question.  Our exploration convinces us that it's possible, but
-- reinforces our view that it is not worthwhile; we elaborate on this in comments below.
--
-- Our current position is to keep for illustrative purposes our work so far on explicitly tying
-- some hash collisions to particular Records in the system for some cases, but to continue to
-- simply construct the evidence of the collision in other cases.  The two approaches can coexist
-- because proofs can "bail out" when finding a hash collision between Records the proof is
-- considering by invoking either of the postulated functions below (meta-no-collision-in-sys and
-- meta-no-collsion).  Both state that there is no collision, so providing evidence of a specific
-- collision is sufficient to bail out of the proof of a condition that might not hold in case of a
-- collision.  The first requires the specific elements contributing to the collision to be
-- precisely located within the current ReachableSystemState, while the second requires only
-- evidence of the collision's existence, without specific information about where its elements came
-- from.  Below we explain our initial approach for meta-no-collision-in-sys, overview some examples
-- demonstrating the additional proof burden it creates, and also discuss what would be needed to
-- complete this effort, if it were deemed worthwhile.

module LibraBFT.ImplShared.Util.HashCollisions
  (iiah  : SystemInitAndHandlers ℓ-RoundManager ConcSysParms)
  where

  open WithInitAndHandlers iiah

  -- By placing the constructs below within a module that takes a ReachableSystemState as a module
  -- parameter, we ensure that a proof that wants to "bail out" due to a hash collision must specify
  -- a ReachableSystemState and show that the specific collision is between elements represented in
  -- that state.

  module PerReachableState {st} (r : ReachableSystemState st) where

    -- The following datatypes are used in the definition of HashCollisionFound below to enumerate
    -- the ways in which hash collisions that would undermine correctness can arise in the given
    -- state st.  Note that we do not need to capture all ways in which a ByteString might be
    -- represented, only those for which our proofs require injectivity properties.  Our initial
    -- work requires capturing hash collisions only for Block IDs.

    data _∈Block_ : BSL → Block → Set where
      inB : ∀ {b} → blockData-bsl (b ^∙ bBlockData) ∈Block b
    open _∈Block_

    data _∈ProposalMsg_ (bsl : BSL) (pm : ProposalMsg) : Set where
      inPM : bsl ∈Block (pm ^∙ pmProposal) → bsl ∈ProposalMsg pm
    open _∈ProposalMsg_

    data _∈nm (bsl : BSL) : Set where
      inP : ∀ {sndr pm} → (sndr , P pm) ∈ msgPool st → bsl ∈ProposalMsg pm → bsl ∈nm
    open _∈nm

    -- We could refine this further (∈BlockTree, ∈btIdToBlock), but I don't think we need to.
    data _∈BS_ (bsl : BSL) (bs : BlockStore) : Set where
      inBS : ∀ {eb} → (getBlock (hashBSL bsl) bs ≡ just eb) → bsl ∈Block (eb ^∙ ebBlock) → bsl ∈BS bs

    data _∈RM_ (bsl : BSL) (rm : RoundManager) : Set where
      inRM : bsl ∈BS (rm ^∙ lBlockStore) → bsl ∈RM rm

    -- So far, HashCollisionFound includes two constructors, one (msgRmHC) for a collision between a
    -- ByteString represented in a message that has been sent (∈nm) and one represented in the
    -- RoundManager of some peer.  The other (msgmsgHC) is unused so far, but would be needed if we
    -- were to take this work further; it is for cases in which there is a collision between two
    -- elements in messages that have been sent.

    data HashCollisionFound : Set where
      msgRmHC  : ∀ {bs1 bs2 pid}
               → bs1 ∈nm
               → initialised st pid ≡ initd
               → bs2 ∈RM (peerStates st pid)
               → hashBSL bs1 ≡ hashBSL bs2
               → bs1 ≢ bs2
               → HashCollisionFound
      msgmsgHC : ∀ {bs1 bs2}
               → bs1 ∈nm
               → bs2 ∈nm
               → hashBSL bs1 ≡ hashBSL bs2
               → bs1 ≢ bs2
               → HashCollisionFound

    -- By postulating the lack of existence of HashCollisionFound, we enable any proof to "bail out"
    -- only if it can construct a *specific* hash collision that is "in the system" represented by
    -- the specific ReachableSystemState, according to the specific notions thereof captured by the
    -- constructors for this type.

    postulate -- Valid assumption: there are no hash collisions among values found in the system
      meta-no-collision-in-sys : ¬ HashCollisionFound

    -- Discussion
    --
    -- As noted above, we have applied this approach to some proofs but not others.  In particular,
    -- there are still a number of proofs that use meta-no-collision (below), which does not require
    -- the constructed collision to be explicitly placed in context of the ReachableSystemState.
    --
    -- We have used meta-no-collision-in-sys for the case of a peer handling a proposal.  The
    -- proposal contains a Block which has an ID, which is supposed to be the hash of some parts of
    -- the proposal.  This condition is verified when the proposal message is first received (see
    -- verifyWellFormed in LibraBFT.Impl.Consensus.ConsensusTypes.Block), and the knowledge that it
    -- verified correctly is needed all the way down the stack when the receiving peer inserts the
    -- block into its BlockTree.  If an ExecutedBlock is found in the BlockTree associated with the
    -- ID of the new Block, then the algorithm assumes it's the same Block (because both the new
    -- Block and the one inserted previously in the BlockTree have been verified as hashing to the
    -- same ID).  If there were a collision (i.e., these two Blocks that hash to the same ID
    -- actually have different bits that are hashed to derive the ID), then incorrect behaviour
    -- would be possible.
    --
    -- To use meta-no-collision-in-sys, we need to construct a value of HashCollisionFound in
    -- context of the ReachableSystemState under consideration (but see note below).  This requires
    -- carrying the fact that the hash of the newly proposed Block matches its ID from the
    -- above-mentioned verification all the way down the stack, where it is needed to invoke an
    -- assumption about the lack of collisions between the new Block and one previously stored when
    -- proving the Contract for insertBlockESpec. (This is the NOHC1 argument given to the blocks≈
    -- field insertBlockESpec.ContrackOk.)  Then, each Contract up the stack must receive a similar
    -- argument enabling it to invoke the Contract of the next function down the stack.  See, for
    -- example, the ebBlock≈ field of executeAndInsertBlockESpec.ContractOk, the voteAttemptCorrect
    -- field of processProposalMsgMSpec.Contract (and others in the same file), and similarly for
    -- handleProposalSpec.Contract.  Then this argument must be provided by higher level properties
    -- that wish to invoke the lower-level contracts.  Because the higher-level properties are in
    -- context of a specific ReachableSystemState, they can construct a proof of the absence of the
    -- potential collision by using meta-no-collision-in-sys for that ReachableSystemState.
    --
    -- As can be seen, connecting a potential hash collision to a specific ReachableSystemState is a
    -- fair amount of work, which complicates proofs.  As explained above, we do not think it is
    -- worthwhile to continue this effort, just to show that we can.  One issue we would want to
    -- address if taking this work further would be to *ensure* that the ReachableSystemState
    -- for which a potential collision is considered is the same one about which we're proving the
    -- given property.  This already is the case in our proofs, but our conditions don't *ensure*
    -- that it is because, in principle, when calling nohc to use meta-no-collision-in-sys to
    -- eliminate an assumed collision, we could provide *any* ReachableSystemState.  To require it
    -- to be the same ReachableSystemState, we would need to explicitly express for each relevant
    -- property that it holds unless there is collision in *that state*.  So, for example, the
    -- conclusion of the IncreasingRoundObligation property would have to become something like the
    -- following (where pre is the state about which IncreasingRoundObligation is proved):
    --
    --     HashCollisionFound pre
    --   ⊎ v' ^∙ vRound < v ^∙ vRound
    --   ⊎ VoteForRound∈ pk (v ^∙ vRound) (v ^∙ vEpoch) (v ^∙ vProposedId) (msgPool pre)
    --
    -- The first disjunct is not currently necessary because there is no requirement to place the
    -- HashCollisionFound in the same ReachableSystemState.  We would then need to propagate those
    -- disjuncts from one proof to another, making even more work and complicating proofs and
    -- properties further.  Importantly, doing so would provide no additional benefit over what we
    -- have done already, exactly because it is not practical to construct a collision for the
    -- postulated hash function anyway (and we could not do so "accidentally"): giving ourselves the
    -- freedom to associate it with a diffferent ReachabeSystemState does not change that.  This
    -- underlines the point that requiring the collision to be associated with a
    -- ReachableSystemState creates quite a bit of work, and provides little benefit.

    postulate  -- valid assumption.  Note that this does *not* say that no collisions *exist*; it
               -- says a proof cannot escape its obligations unless it can provide specfic evidence
               -- of a collision; as explained above, doing so other than from Records presented to
               -- the proof (because they are in the system state under consideration) is
               -- impractical and impossible to do "accidentally"
      meta-no-collision : ¬ (NonInjective-≡ sha256)

    sameSig⇒sameVoteDataNoCol : ∀ {v1 v2 : Vote} {pk}
                              → WithVerSig pk v1
                              → WithVerSig pk v2
                              → v1 ^∙ vSignature ≡ v2 ^∙ vSignature
                              → v2 ^∙ vVoteData ≡ v1 ^∙ vVoteData
    sameSig⇒sameVoteDataNoCol {v1} {v2} wvs1 wvs2 refl
       with sameSig⇒sameVoteData {v1} {v2} wvs1 wvs2 refl
    ...| inj₁ hb = ⊥-elim (meta-no-collision hb)
    ...| inj₂ x = x


text:
-- Andreas, 2020-03-27, issue #4534
-- Better error message for quote.

open import Agda.Builtin.Reflection

_ : Name
_ = quote Set

-- Can only quote defined names, but encountered Set
-- when checking that the expression quote Set has type Name

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Classical.SequentCalculus (𝔏 : Signature) where
open Signature(𝔏)

open import Data.List
open import Data.List.Functions using () renaming (singleton to · ; _++_ to _∪_)
open import Data.List.Relation.Permutation
open import Formalization.PredicateLogic.Syntax(𝔏)
open import Formalization.PredicateLogic.Syntax.Substitution(𝔏)
open import Functional as Fn
import      Lvl
open import Numeral.Finite
open import Numeral.Natural
open import Type

private variable ℓ : Lvl.Level
private variable n vars : ℕ

_∪·_ : ∀{T : Type{ℓ}} → List(T) → T → List(T)
_∪·_ = Fn.swap(_⊰_)
infixl 1000 _∪·_

module _ where
  private variable Γ Γ₁ Γ₂ Γ₃ Δ Δ₁ Δ₂ Δ₃ : List(Formula(vars))
  private variable φ φ₁ φ₂ ψ A B C : Formula(vars)
  private variable p : Prop(n)

  data _⇒_ : List(Formula(vars)) → List(Formula(vars)) → Type{Lvl.𝐒(ℓₚ Lvl.⊔ ℓₒ)} where
    axiom : ((· φ) ⇒ (· φ))

    weakenₗ : (Γ ⇒ Δ) → ((Γ ∪· A) ⇒ Δ)
    permuteₗ : .(Γ₁ permutes Γ₂) → (Γ₁ ⇒ Δ) → (Γ₂ ⇒ Δ)
    contractₗ : ((Γ ∪· A ∪· A) ⇒ Δ) → ((Γ ∪· A) ⇒ Δ)
    ⊥ₗ : (Γ ∪· ⊥) ⇒ ∅
    ∧ₗₗ : ((Γ ∪· A) ⇒ Δ) → ((Γ ∪· (A ∧ B)) ⇒ Δ)
    ∧ₗᵣ : ((Γ ∪· B) ⇒ Δ) → ((Γ ∪· (A ∧ B)) ⇒ Δ)
    ∨ₗ : ((Γ ∪· A) ⇒ Δ) → ((Γ ∪· B) ⇒ Δ) → ((Γ ∪· (A ∨ B)) ⇒ Δ)
    ⟶ₗ : (Γ ⇒ (Δ ∪· A)) → ((Γ ∪· B) ⇒ Δ) → ((Γ ∪· (A ⟶ B)) ⇒ Δ)
    Ɐₗ : ∀{t} → ((Γ ∪· (substitute0 t A)) ⇒ Δ) → ((Γ ∪· (Ɐ A)) ⇒ Δ)
    ∃ₗ : ∀{v}{n} → ((Γ ∪· (substituteN n (var v) A)) ⇒ Δ) → ((Γ ∪· (∃ A)) ⇒ Δ)

    weakenᵣ : (Γ ⇒ Δ) → (Γ ⇒ (Δ ∪· A))
    permuteᵣ : .(Δ₁ permutes Δ₂) → (Γ ⇒ Δ₁) → (Γ ⇒ Δ₂)
    contractᵣ : (Γ ⇒ (Δ ∪· A ∪· A)) → (Γ ⇒ (Δ ∪· A))
    ⊤ᵣ : ∅ ⇒ (Δ ∪· ⊤)
    ∧ᵣ : (Γ ⇒ (Δ ∪· A)) → (Γ ⇒ (Δ ∪· B)) → (Γ ⇒ (Δ ∪· (A ∧ B)))
    ∨ᵣₗ : (Γ ⇒ (Δ ∪· A)) → (Γ ⇒ (Δ ∪· (A ∨ B)))
    ∨ᵣᵣ : (Γ ⇒ (Δ ∪· B)) → (Γ ⇒ (Δ ∪· (A ∨ B)))
    ⟶ᵣ : ((Γ ∪· A) ⇒ (Δ ∪· B)) → (Γ ⇒ (Δ ∪· (A ⟶ B)))
    Ɐᵣ : ∀{v}{n} → (Γ ⇒ (Δ ∪· (substituteN n (var v) A))) → (Γ ⇒ (Δ ∪· (Ɐ A)))
    ∃ᵣ : ∀{t} → (Γ ⇒ (Δ ∪· (substitute0 t A))) → (Γ ⇒ (Δ ∪· (∃ A)))

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module FreezingTest where

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

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

force : let one : ℕ
            one = _         -- this meta is not frozen after the end of let
        in  one ≡ suc zero
force = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
postulate
  C : Set
  anything : C

record I : Set where
  constructor c
  field
    f : C

data Wrap : (j : I) → Set where
  wrap : ∀ {j} → Wrap j

works1 : ∀ {j} → Wrap j → C
works1 {c ._} (wrap {j = c _}) with anything
... | z = z


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some examples showing where the natural numbers and some related
-- operations and properties are defined, and how they can be used
------------------------------------------------------------------------

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

module README.Data.Nat where

-- The natural numbers and various arithmetic operations are defined
-- in Data.Nat.

open import Data.Nat using (ℕ; _+_; _*_)

-- _*_ has precedence 7 over precedence 6 of _+_
-- precedence of both defined in module Agda.Builtin.Nat
ex₁ : ℕ
ex₁ = 1 + 3 * 4

-- Propositional equality and some related properties can be found
-- in Relation.Binary.PropositionalEquality.

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

ex₂ : 3 + 5 ≡ 2 * 4
ex₂ = refl

-- Data.Nat.Properties contains a number of properties about natural
-- numbers.

open import Data.Nat.Properties using (*-comm; +-identityʳ)

ex₃ : ∀ m n → m * n ≡ n * m
ex₃ m n = *-comm m n

-- The module ≡-Reasoning in Relation.Binary.PropositionalEquality
-- provides some combinators for equational reasoning.

open Relation.Binary.PropositionalEquality using (cong; module ≡-Reasoning)

ex₄ : ∀ m n → m * (n + 0) ≡ n * m
ex₄ m n = begin
  m * (n + 0)  ≡⟨ cong (_*_ m) (+-identityʳ n) ⟩
  m * n        ≡⟨ *-comm m n ⟩
  n * m        ∎
  where open ≡-Reasoning

-- The module SemiringSolver in Data.Nat.Solver contains a solver
-- for natural number equalities involving variables, constants, _+_
-- and _*_.

open import Data.Nat.Solver using (module +-*-Solver)
open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)

ex₅ : ∀ m n → m * (n + 0) ≡ n * m
ex₅ = solve 2 (λ m n → m :* (n :+ con 0)  :=  n :* m) refl


text:
module test.IntegerOverflow where

open import Type
open import Declarative
open import Builtin
open import Builtin.Constant.Type
open import Builtin.Constant.Term Ctx⋆ Kind * # _⊢⋆_ con size⋆
open import Agda.Builtin.Sigma
open import Data.Integer
open import Data.Nat
open import Data.Empty

-- zerepoch/zerepoch-core/test/data/integerOverflow.plc

-- This term is impossible as terms are intrinsically sized

-- completeting this definition requires an element of the empty type
{-
intOverflow : ∀{Γ} → Γ ⊢ con integer (size⋆ 1)
intOverflow = con (integer 1 (ℤ.pos 128) (-≤+ Σ., +≤+ (gen _ _ {!!})))
-}

max_stars_repo_name: Quantum-One-DLT/zerepoch

max_issues_repo_name: Quantum-One-DLT/zerepoch

max_forks_repo_name: Quantum-One-DLT/zerepoch


text:
---------------------------------------------------------------------
-- This file contains the definition of heterogenous equality and  --
-- related facts.  A lot of this code is old, and could be written --
-- better.   This equality is mainly used for object equivalence.  --
--                                                                 --
-- Some of it came from the paper:                                 --
--   "Monads Need Not Be Endofunctors" by Altenkirch et al.        --
--                                                                 --
-- See: http://www.cs.nott.ac.uk/~txa/publ/Relative_Monads.pdf     --
---------------------------------------------------------------------

module Equality.Eq where

open import Level

open import Relation.Relation

open import Relation.Binary.PropositionalEquality public renaming (sym to prop-sym ; trans to prop-trans; refl to prop-refl)

data _≅_ {l : Level} {A : Set l} (a : A) : {A' : Set l} → A' → Set l where
  refl : a ≅ a

postulate ext : ∀{i j}{A : Set i}{B B' : A → Set j}{f : ∀ a → B a}{g : ∀ a → B' a} →
                (∀ a → f a ≅ g a) → f ≅ g

postulate prop-ext : ∀{i j}{A : Set i}{B : A → Set j}{f : ∀ a → B a}{g : ∀ a → B a} →
                (∀ a → f a ≡ g a) → f ≡ g

≅-to-≡ : ∀{l : Level}{A : Set l}{a b : A} → a ≅ b → a ≡ b
≅-to-≡ refl = prop-refl

-- this could just be derived from ext
postulate iext : ∀{i j}{A : Set i}{B B' : A → Set j}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
                 (∀ a → f {a} ≅ g {a}) →
                 _≅_ {_}{ {a : A} → B a} f { {a : A} → B' a} g

sym : ∀{l : Level}{A : Set l }{a b : A} → a ≅ b → b ≅ a
sym refl = refl

trans : ∀{l : Level}{A : Set l}{a b c : A} → a ≅ b → b ≅ c → a ≅ c
trans refl refl = refl

isEqRel : ∀{l : Level}{A : Set l} → EqRel {A = A}  (λ x y → x ≅ y)
isEqRel {l} {A} = record { parEqPf = record { symPf = sym; transPf = trans }; refPf = refl }

ir : ∀{l : Level}{A A' : Set l}{a : A}{a' : A'}{p q : a ≅ a'} → p ≅ q
ir {p = refl}{q = refl} = refl

eqApp : ∀{l l' : Level}{A : Set l}{B : Set l'}{f : A → B}{b c : A} → b ≅ c → (f b) ≅ (f c)
eqApp refl = refl

subst≅ : {l l' : Level}{A : Set l}{a b : A}{P : A → Set l'} → a ≅ b → P a → P b
subst≅ refl x = x

-- Cite from relative monads paper.
deqApp : ∀{l : Level}{A : Set l}{B : A → Set l}(f : ∀ a → B a){a a' : A}
  → a ≅ a' → f a ≅ f a'
deqApp f refl = refl

feqApp : ∀{l l' : Level}{A : Set l}{B : Set l'}{f f' : A → B}{b c : A} → f ≅ f' → b ≅ c → (f b) ≅ (f' c)
feqApp refl refl = refl

ifeqApp : ∀{i j}{A : Set i}{B : A → Set j}{f f' : {x : A} → B x}(a : A) → _≅_ {_}{ {a : A} → B a} f { {a : A} → B a} f' → f {a} ≅ f' {a}
ifeqApp a refl = refl

ieqApp : ∀{x y}{A : Set x}{B : A → Set y}(f : ∀ {a} → B a){a a' : A} → a ≅ a' → f {a} ≅ f {a'}
ieqApp f refl = refl

-- Cite from relative monads paper.
eqApp2 : ∀{i j k}{A : Set i}{B : A → Set j}{C : Set k}{a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' →
            (f : (a : A) → B a → C) → f a b ≅ f a' b'
eqApp2 refl refl f = refl

eqApp3 : ∀{x y z w}{A : Set x}{B : A → Set y}{C : (a : A) → B a → Set z}{E : Set w}
             (f : (a : A)(b : B a)(c : C a b) → E) →
             {a a' : A} → a ≅ a' →
             {b : B a}{b' : B a'} → b ≅ b' →
             {c : C a b}{c' : C a' b'} → c ≅ c' →
             f a b c ≅ f a' b' c'
eqApp3 f refl refl refl = refl

depfeqApp3a : ∀{l}{A : Set l}{B : Set (suc l)}{C : A → Set (suc l)}{D : Set (suc l)}
        (f  : (x : A)(y : B)(z : C x) → D) →
        (f' : (x : A)(y : B)(z : C x) → D) →
        f ≅ f' →
        {a : A}{b : B} {c : C a} →
        f a b c ≅ f' a b c
depfeqApp3a {_}{A}{B}{C} f f' p {a}{b}{c} =
        feqApp {f = f a b} {f' = f' a b} (feqApp {f = f a} {f' = f' a} (eqApp {f = λ h → h a} p) refl) refl

depfeqApp3b : ∀{l}{A : Set l}{B : A → Set (suc l)}{C : A → Set (suc l)}{D : Set (suc l)}
        (f  : (x : A)(y : B x)(z : C x) → D) →
        (f' : (x : A)(y : B x)(z : C x) → D) →
        f ≅ f' →
        {a : A}{b : B a} {c : C a} →
        f a b c ≅ f' a b c
depfeqApp3b {_}{A}{B}{C} f f' p {a}{b}{c} =
        feqApp {f = f a b} {f' = f' a b} (feqApp {f = f a} {f' = f' a} (eqApp {f = λ h → h a} p) refl) refl

depfeqApp3c : ∀{l}{A : Set l}{B : A → A → Set (suc l)}{C : A → Set (suc l)}{D : Set (suc l)}
        (f  : (x : A)(y : B x x)(z : C x) → D) →
        (f' : (x : A)(y : B x x)(z : C x) → D) →
        f ≅ f' →
        {a : A}{b : B a a} {c : C a} →
        f a b c ≅ f' a b c
depfeqApp3c {_}{A}{B}{C} f f' p {a}{b}{c} =
            feqApp {f = f a b} {f' = f' a b} (feqApp {f = f a} {f' = f' a} (eqApp {f = λ h → h a} p) refl) refl

depfeqApp3d : ∀{l}{A : Set l}{B : A → A → Set (suc l)}{C : A → A → Set (suc l)}{D : Set (suc l)}
        (f  : (x : A)(y : B x x)(z : C x x) → D) →
        (f' : (x : A)(y : B x x)(z : C x x) → D) →
        f ≅ f' →
        {a : A}{b : B a a} {c : C a a} →
        f a b c ≅ f' a b c
depfeqApp3d {_}{A}{B}{C} f f' p {a}{b}{c} =
            feqApp {f = f a b} {f' = f' a b} (feqApp {f = f a} {f' = f' a} (eqApp {f = λ h → h a} p) refl) refl

depfeqApp3e : ∀{l}{A : Set l}{B : Set (suc l)}{C : A → A → Set (suc l)}{D : Set (suc l)}
        (f  : (x : A)(y : B)(z : C x x) → D) →
        (f' : (x : A)(y : B)(z : C x x) → D) →
        f ≅ f' →
        {a : A}{b : B} {c : C a a} →
        f a b c ≅ f' a b c
depfeqApp3e {_}{A}{B}{C} f f' p {a}{b}{c} =
            feqApp {f = f a b} {f' = f' a b} (feqApp {f = f a} {f' = f' a} (eqApp {f = λ h → h a} p) refl) refl

depfeqAppa : ∀{l l' l'' l'''}{A : Set l}{B : Set l'}{C : A → B → Set l''}{D : A → B → Set  l'''}{a : A}
        (f  : (x : A)(y : B)(z : C x y) → D x y) →
        (f' : (x : A)(y : B)(z : C x y) → D x y) →
        f ≅ f' →
        f a ≅ f' a
depfeqAppa {l}{l'}{l''}{l'''}{A}{B}{C}{D}{a} f f' p = eqApp {f = λ h → h a} p

depfeqApp2a : ∀{l l' l'' l'''}{A : Set l}{B : Set  l'}{C : A → B → Set  l''}{D : A → B → Set l'''}{a : A}
        (f  : (y : B)(z : C a y) → D a y) →
        (f' : (y : B)(z : C a y) → D a y) →
        f ≅ f' →
        {b : B} {c : C a b} →
        f b c ≅ f' b c
depfeqApp2a f f' p {b} {c} = feqApp {f = f b} {f' = f' b} (eqApp {f = λ h → h b} p) refl

depfeqApp3f : ∀{l l' l'' l'''}{A : Set l}{B : Set l'}{C : A → B → Set l''}{D : A → B → Set l'''}
        (f  : (x : A)(y : B)(z : C x y) → D x y) →
        (f' : (x : A)(y : B)(z : C x y) → D x y) →
        f ≅ f' →
        {a : A}{b : B} {c : C a b} →
        f a b c ≅ f' a b c
depfeqApp3f {_}{_}{_}{_}{A}{B}{C}{D} f f' p {a}{b}{c} =
                         depfeqApp2a {A = A} {B = B}{C = λ o1 o2 → C o1 o2}
                           {D = λ o1₁ o2₁ → D o1₁ o2₁} (f a) (f' a) (eqApp {f = λ h → h a} p) {b} {c}

depfeqApp3g : ∀{l l' l'' l'''}{A : Set l}{B : Set l'}{C : A → B → Set l''}{D D' : A → B → Set l'''}
        (f  : (x : A)(y : B)(z : C x y) → D x y) →
        (f' : (x : A)(y : B)(z : C x y) → D' x y) →
        D ≅ D' →
        f ≅ f' →
        {a : A}{b : B} {c : C a b} →
        f a b c ≅ f' a b c
depfeqApp3g {_}{_}{_}{_}{A}{B}{C}{D} f f' refl p {a}{b}{c} =
                         depfeqApp2a {A = A} {B = B} {C = λ o1₁ o2₁ → C o1₁ o2₁} {D = λ o1 o2 → D o1 o2} (f a) (f' a) (eqApp {f = λ h → h a} p) {b} {c}

idepfeqApp2a : ∀{l l' l'' l''' l''''}{A : Set l}{B : Set  l'}{C : Set l''}{D : A → B → C → Set  l'''}{E : A → B → C → Set l''''}{a : A}
        (f  : {x : B}{y : C}(z : D a x y) → E a x y) →
        (f' : {x : B}{y : C}(z : D a x y) → E a x y) →
        (∀{x y} → f {x}{y}  ≅ f' {x}{y}) →
        {b : B}{c : C}{m : D a b c} →
        f {b}{c} m ≅ f' {b} {c} m
idepfeqApp2a {l}{l'}{l''}{l'''}{l''''}{A}{B}{C}{D}{E}{a} f f' p {b}{c}{m} =
             feqApp {f = f {b} {c}} {f' = f' {b} {c}} {m} {m} (ext (λ h → feqApp {f = f {b} {c}} {f' = f' {b} {c}} {h} {h} (p {b}{c}) refl)) refl

depfeqApp2b : ∀{l l' l''}{A : Set l}{D : A → A → Set l'}{E E' : A → A → Set l''}
        (f  : (x : A)(y : A)(z : A) → (m1 : D y z) → (m2 : D x y) → E x z) →
        {f'  : (x : A)(y : A)(z : A) → (m1 : D y z) → (m2 : D x y) → E' x z} →
        E ≅ E' →
        f ≅ f' →
        {a a' b b' c c' : A}{m1 : D b c}{m2 : D a b}{m1' : D  b' c'}{m2' : D a' b'} →
        a ≅ a' → b ≅ b' → c ≅ c' → m1 ≅ m1' → m2 ≅ m2' →
        f a b c m1 m2 ≅ f' a' b' c' m1' m2'
depfeqApp2b {_}{_}{_}{A}{D}{E} f refl refl {a = a}{b = b}{c = c}{m1 = m1}{m2 = m2}  refl refl refl refl refl =
  eqApp {f = f a b c m1} {m2}{m2} refl

feqApp3 : ∀{l}{A : Set l}{B : A → Set (suc l)}{C : A → Set (suc l)}{D : Set (suc l)}
        (f  : (x : A)(y : B x)(z : C x) → D) →
        (f' : (x : A)(y : B x)(z : C x) → D) →
        f ≅ f' →
        {a : A}{b : B a} {c : C a} →
        f a b c ≅ f' a b c
feqApp3 {_}{A}{B}{C} f f' p {a}{b}{c} =
        feqApp {f = f a b} {f' = f' a b} (feqApp {f = f a} {f' = f' a} (eqApp {f = λ h → h a} p) refl) refl

coerce : ∀{l}{A B : Set l} → A ≅ B → A → B
coerce refl a = a

p : ∀{m}{A B : Set m}{a : A}{b : B} → (q : B ≅ A) → _≅_ {m} {A} a {A} (coerce q b) → _≅_ {m} {A} a {B} b
p refl refl = refl

eqApp4 : ∀{x y z v w}{A : Set x}{B : A → Set y}{C : (a : A) → B a → Set z}{D : (a : A)(b : B a) → C a b  → Set v}{E : Set w}
             (f : (a : A)(b : B a)(c : C a b) → D a b c → E) →
             {a a' : A} → a ≅ a' →
             {b : B a}{b' : B a'} → b ≅ b' →
             {c : C a b}{c' : C a' b'} → c ≅ c' →
             {d : D a b c}{d' : D a' b' c'} → d ≅ d' →
             f a b c d ≅ f a' b' c' d'
eqApp4 f refl refl refl refl = refl

funCong : ∀{l m : Level}{A : Set l}{B : Set m}{f g : A → B}{a : A}{b : B}
  → (p : f ≅ g) → (q : f a ≅ b)
  → (w : g a ≅ b) → q ≅ w
funCong refl q w = ir

funCong2 : ∀{l : Level}{A B B' X Y : Set l}{f : ∀{X Y} → A → B}{g : ∀{X Y} → A → B'}{a : A}{b : B}
  → (r : B ≅ B') → (p : (λ {X}{Y} → f {X}{Y}) ≅ (λ {X}{Y} → g {X}{Y})) → (q : f {X}{Y} a ≅ b)
  → (w : g {X}{Y} a ≅ b) → q ≅ w
funCong2 refl refl q w = ir

fixtypes : ∀{x}{A A' : Set x}{a a' : A}{a'' a''' : A'}{p : a ≅ a'}{q : a'' ≅ a'''} → a ≅ a'' → a' ≅ a''' → p ≅ q
fixtypes refl refl = ir

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Oscar.Prelude
open import Oscar.Class.Transitivity

module Oscar.Class.Congruity where

module _ where

  module _
    {ℓ} (_∼_ : ∀ {𝔬} {𝔒 : Ø 𝔬} → 𝔒 → 𝔒 → Ø ℓ)
    𝔵 𝔶
    where
    𝓬ongruity = ∀ {𝔛 : Ø 𝔵} {𝔜 : Ø 𝔶} {x₁ x₂} (f : 𝔛 → 𝔜) → x₁ ∼ x₂ → f x₁ ∼ f x₂
    record 𝓒ongruity : Ø ℓ ∙̂ ↑̂ (𝔵 ∙̂ 𝔶) where
      field congruity : 𝓬ongruity

  open 𝓒ongruity ⦃ … ⦄ public

  module _
    {ℓ} (_∼_ : ∀ {𝔬} {𝔒 : Ø 𝔬} → 𝔒 → 𝔒 → Ø ℓ)
    {𝔵 𝔶} (𝔛 : Ø 𝔵) (𝔜 : Ø 𝔶)
    where
    𝓬ongruity' = ∀ {x₁ x₂} (f : 𝔛 → 𝔜) → x₁ ∼ x₂ → f x₁ ∼ f x₂
    record 𝓒ongruity' : Ø ℓ ∙̂ ↑̂ (𝔵 ∙̂ 𝔶) where
      field congruity' : 𝓬ongruity'

  open 𝓒ongruity' ⦃ … ⦄ public

  module _
    {ℓ} {𝔬} (_∼_ : ∀ {𝔒 : Ø 𝔬} → 𝔒 → 𝔒 → Ø ℓ)
    (𝔛 𝔜 : Ø 𝔬)
    where
    𝓬ongruity'' = ∀ {x₁ x₂} (f : 𝔛 → 𝔜) → x₁ ∼ x₂ → f x₁ ∼ f x₂
    record 𝓒ongruity'' : Ø ℓ ∙̂ 𝔬 where
      field congruity'' : 𝓬ongruity''

  open 𝓒ongruity'' ⦃ … ⦄ public

-- a functional replacement of 𝓒ongruity₂ (but note the additional requirement of 𝓣ransitivity)
congruity2 : ∀ {ℓ} {_∼_ : ∀ {x} {X : Ø x} → X → X → Ø ℓ}
    {𝔵 𝔶 𝔷}
    ⦃ _ : 𝓒ongruity _∼_ 𝔵 (𝔶 ∙̂ 𝔷) ⦄
    ⦃ _ : 𝓒ongruity _∼_ (𝔶 ∙̂ 𝔷) 𝔷 ⦄
    ⦃ _ : 𝓒ongruity _∼_ 𝔶 (𝔵 ∙̂ 𝔷) ⦄
    ⦃ _ : 𝓒ongruity _∼_ (𝔵 ∙̂ 𝔷) 𝔷 ⦄
    ⦃ _ : ∀ {x} {X : Ø x} → Transitivity.class (_∼_ {X = X}) ⦄
    → ∀ {𝔛 : Ø 𝔵} {𝔜 : Ø 𝔶} {ℨ : Ø 𝔷} {x₁ x₂} {y₁ y₂} (f : 𝔛 → 𝔜 → ℨ) → x₁ ∼ x₂ → y₁ ∼ y₂ → f x₁ y₁ ∼ f x₂ y₂
congruity2 {𝔛 = 𝔛}{𝔜}{ℨ}{x₁}{x₂}{y₁}{y₂} f x₁∼x₂ y₁∼y₂ =
  let fx1=fx2 = congruity f x₁∼x₂ in
  let g2 = λ (fx : 𝔜 → ℨ) → fx y₂ in
  let fx1y2=fx2y2 = congruity g2 fx1=fx2 in
  let e = flip f in
  let ey1=ey2 = congruity e y₁∼y₂ in
  let h1 = λ (ex : 𝔛 → ℨ) → ex x₁ in
  let fx1y1=fx1y2 = congruity h1 ey1=ey2 in
  transitivity fx1y1=fx1y2 fx1y2=fx2y2

module _ where

  record 𝓒ongruity₂
    {ℓ} (_∼_ : ∀ {x} {X : Ø x} → X → X → Ø ℓ)
    𝔵 𝔶 𝔷
    : Ø ℓ ∙̂ ↑̂ (𝔵 ∙̂ 𝔶 ∙̂ 𝔷) where
    field congruity₂ : ∀ {𝔛 : Ø 𝔵} {𝔜 : Ø 𝔶} {ℨ : Ø 𝔷} {x₁ x₂} {y₁ y₂} (f : 𝔛 → 𝔜 → ℨ) → x₁ ∼ x₂ → y₁ ∼ y₂ → f x₁ y₁ ∼ f x₂ y₂

  open 𝓒ongruity₂ ⦃ … ⦄ public

module _ where

  module _
    𝔬 𝔭
    {ℓ} (_∼̇_ : ∀ {⋆ : Ø 𝔬} {⋆̇ : ⋆ → Ø 𝔭} → ((𝓞 : ⋆) → ⋆̇ 𝓞) → ((𝓞 : ⋆) → ⋆̇ 𝓞) → Ø ℓ)
    (let infix 4 _∼̇_ ; _∼̇_ = _∼̇_)
    where
    record 𝓒̇ongruity : Ø ↑̂ (𝔬 ∙̂ 𝔭) ∙̂ ℓ where
      field ċongruity : ∀ {⋆ : Ø 𝔬} {⋆̇ : ⋆ → Ø 𝔭} {f₁ f₂ : (𝓞 : ⋆) → ⋆̇ 𝓞} (G : ∀ {𝓞 : ⋆} → ⋆̇ 𝓞 → ⋆̇ 𝓞) → f₁ ∼̇ f₂ → G ∘ f₁ ∼̇ G ∘ f₂

  open 𝓒̇ongruity ⦃ … ⦄ public


text:
module Issue478b where

record Ko (Q : Set) : Set₁ where
  field
    T : Set

  foo : T
  foo = Set

-- This previously said Set₁ !=< T r

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.GradedRing.DirectSumFun where

{-
   This file give a graded ring construction in the case of the fun direct sum.
   Because of the current proofs this is done only in the case where
   - Idx is ℕ and for a monoid on it
   - For the usual ∸ of the Nat library

   The proof consists in :
   - Defining a _prod_ operation on the structure
   - Proving the underlying equivalence respect it
   - Transporting the proof of RingStr
   - Deducing an equivalence proof
-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels

open import Cubical.Relation.Nullary

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat renaming (_+_ to _+ℕ_ ; _∸_ to _-ℕ_ )
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma
open import Cubical.Data.Sum

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.DirectSum.Equiv-DSHIT-DSFun
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base
open import Cubical.Algebra.DirectSum.DirectSumHIT.Properties
open import Cubical.Algebra.DirectSum.DirectSumFun.Base
open import Cubical.Algebra.AbGroup.Instances.NProd
open import Cubical.Algebra.AbGroup.Instances.DirectSumFun
open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.Base
open import Cubical.Algebra.GradedRing.DirectSumHIT
open import Cubical.Algebra.CommRing

open import Cubical.HITs.PropositionalTruncation as PT

private variable
  ℓ ℓ' : Level

open AbGroupStr
open AbGroupTheory

-----------------------------------------------------------------------------
-- Def, notation, lemma

module _

  -- monoid
  (_+n_ : ℕ → ℕ → ℕ) -- need to instantiate on +'
  (isM : IsMonoid 0 _+n_)
  (_+≡_ : (n m : ℕ) →  n +n m ≡ n +ℕ m) -- needed for the behaviour under -ℕ
  --
  (G : ℕ → Type ℓ)
  (Gstr : (n : ℕ) → AbGroupStr (G n))
  where

  sameFiber+ : {i n : ℕ} → i ≤ n → i +ℕ (n -ℕ i) ≡ n
  sameFiber+ {zero} {zero} p = refl
  sameFiber+ {zero} {suc n} p = refl
  sameFiber+ {suc i} {zero} p = ⊥.rec (¬-<-zero p)
  sameFiber+ {suc i} {suc n} p = cong suc (sameFiber+ (pred-≤-pred p))

  sameFiber : {i n : ℕ} → (i ≤ n) → i +n (n -ℕ i) ≡ n
  sameFiber {i} {n} p = (i +≡ (n -ℕ i)) ∙ sameFiber+ p

  open SubstLemma ℕ G Gstr
  open IsMonoid isM using ()
    renaming
    ( ·Assoc to +nAssoc
    ; ·IdR   to +nIdR
    ; ·IdL   to +nIdL   )

  open AbGroupStr (snd (NProd-AbGroup G Gstr)) using ()
    renaming
    ( 0g     to 0Fun
    ; _+_    to _+Fun_
    ; is-set to isSetFun )

  module _
    (1⋆      : G 0)
    (_⋆_     : {k l : ℕ} → G k → G l → G (k +n l))
    (0-⋆     : {k l : ℕ} → (b : G l) → (0g (Gstr k)) ⋆ b ≡ 0g (Gstr (k +n l)))
    (⋆-0     : {k l : ℕ} → (a : G k) → a ⋆ (0g (Gstr l)) ≡ 0g (Gstr (k +n l)))
    (⋆Assoc  : {k l m : ℕ} → (a : G k) → (b : G l) → (c : G m) →
                _≡_ {A = Σ[ k ∈ ℕ ] G k} ((k +n (l +n m)) , (a ⋆ (b ⋆ c))) (((k +n l) +n m) , ((a ⋆ b) ⋆ c)))
    (⋆IdR    : {k : ℕ} → (a : G k) → _≡_ {A = Σ[ k ∈ ℕ ] G k} ( k +n 0 , a ⋆ 1⋆ ) (k , a))
    (⋆IdL    : {l : ℕ} → (b : G l) → _≡_ {A = Σ[ k ∈ ℕ ] G k} ( 0 +n l , 1⋆ ⋆ b ) (l , b))
    (⋆DistR+ : {k l : ℕ} → (a : G k) → (b c : G l) →
               a ⋆ ((Gstr l) ._+_ b c) ≡ Gstr (k +n l) ._+_ (a ⋆ b) (a ⋆ c))
    (⋆DistL+ : {k l : ℕ} → (a b : G k) → (c : G l) →
               ((Gstr k) ._+_ a b) ⋆ c ≡ Gstr (k +n l) ._+_ (a ⋆ c) (b ⋆ c))
    where

-----------------------------------------------------------------------------
-- Definition of 1

    -- import for pres
    open Equiv-Properties G Gstr using
      ( substG
      ; fun-trad
      ; fun-trad-eq
      ; fun-trad-neq
      ; ⊕HIT→Fun
      ; ⊕HIT→⊕Fun
      ; ⊕HIT→⊕Fun-pres+)

    1Fun : (n : ℕ) → G n
    1Fun zero = 1⋆
    1Fun (suc n) = 0g (Gstr (suc n))

    1⊕Fun : ⊕Fun G Gstr
    1⊕Fun = 1Fun , ∣ 0 , helper ∣₁
      where
      helper : AlmostNullProof G Gstr 1Fun 0
      helper zero r = ⊥.rec (¬-<-zero r)
      helper (suc n) r = refl

    ⊕HIT→Fun-pres1 : (n : ℕ) → ⊕HIT→Fun (base 0 1⋆) n ≡ 1Fun n
    ⊕HIT→Fun-pres1 zero with discreteℕ 0 0
    ... | yes p = cong (λ X → subst G X 1⋆) (isSetℕ _ _ _ _) ∙ transportRefl _
    ... | no ¬p = ⊥.rec (¬p refl)
    ⊕HIT→Fun-pres1 (suc n) with discreteℕ (suc n) 0
    ... | yes p = ⊥.rec (snotz p)
    ... | no ¬p = refl

    ⊕HIT→⊕Fun-pres1 : ⊕HIT→⊕Fun (base 0 1⋆) ≡ 1⊕Fun
    ⊕HIT→⊕Fun-pres1 = ΣPathTransport→PathΣ _ _
                       ((funExt (λ n → ⊕HIT→Fun-pres1 n)) , (squash₁ _ _))

-----------------------------------------------------------------------------
-- Definition of the ring product

    sumFun : (i n : ℕ) → (i ≤ n) → (f g : (n : ℕ) → G n) → G n
    sumFun zero n r f g = subst G (sameFiber r) ((f 0) ⋆ (g (n -ℕ 0)))
    sumFun (ℕ.suc i) n r f g = Gstr n ._+_ (subst G (sameFiber r) ((f (suc i)) ⋆ (g (n -ℕ suc i))))
                                            (sumFun i n (≤-trans ≤-sucℕ r) f g)

    _prodFun_ : (f g : (n : ℕ) → G n) → (n : ℕ) → G n
    _prodFun_ f g n = sumFun n n ≤-refl f g

    -- Proof that it is an almost null sequence
    prodAn : (f g : (n : ℕ) → G n) → AlmostNull G Gstr f → AlmostNull G Gstr g → AlmostNull G Gstr (f prodFun g)
    prodAn f g (k , nf) (l , ng) = (k +ℕ l) , λ n pp → sumF0 n n pp ≤-refl
      where
      sumF0 : (i n : ℕ) → (pp : k +ℕ l < n) → (r : i ≤ n) → sumFun i n r f g ≡ 0g (Gstr n)
      sumF0 zero n pp r = cong (subst G (sameFiber r))
                               (cong (λ X → f 0 ⋆ X) (ng (n -ℕ zero) (<-k+-trans pp)) ∙ ⋆-0 _) ∙ subst0g _
      sumF0 (suc i) n pp r with splitℕ-≤ (suc i) k
      ... | inl x = cong₂ (Gstr n ._+_)
                        (cong (subst G (sameFiber r))
                              (cong (λ X → f (suc i) ⋆ X) (ng (n -ℕ suc i)
                                    -- Goal  : l < n - suc i
                                    -- Proof : l = k + l - k < n - k < n - suc i
                                    (subst (λ X → X < n -ℕ suc i) (∸+ l k)
                                            (≤<-trans (≤-∸-≥ (k +ℕ l) (suc i) k x)
                                            (<-∸-< (k +ℕ l) n (suc i) pp (≤<-trans x (<-+k-trans pp))))))
                              ∙ ⋆-0 (f (suc i))))
                        (sumF0 i n pp (≤-trans ≤-sucℕ r))
                  ∙ +IdR (Gstr n) _
                  ∙ subst0g _

      ... | inr x = cong₂ (Gstr n ._+_)
                          (cong (subst G (sameFiber r))
                                (cong (λ X → X ⋆ g (n -ℕ (suc i))) (nf (suc i) x)
                                ∙ 0-⋆ _))
                          (sumF0 i n pp (≤-trans ≤-sucℕ r))
                    ∙ +IdR (Gstr n) _
                    ∙ subst0g _

    _prodF_ : ⊕Fun G Gstr → ⊕Fun G Gstr → ⊕Fun G Gstr
    _prodF_(f , Anf) (g , Ang) = (f prodFun g) , helper Anf Ang
      where
      helper :  AlmostNullP G Gstr f →  AlmostNullP G Gstr g →  AlmostNullP G Gstr (f prodFun g)
      helper = PT.rec2 squash₁ (λ x y → ∣ (prodAn f g x y) ∣₁)

-----------------------------------------------------------------------------
-- Some Ring properties that are needed

    -- lemma for 0 case
    prodFunAnnihilL : (f : (n : ℕ) → G n) → 0Fun prodFun f ≡ 0Fun
    prodFunAnnihilL f = funExt (λ n → sumF0 n n ≤-refl)
      where
      sumF0 : (i n : ℕ) → (r : i ≤ n) → sumFun i n r 0Fun f ≡ 0g (Gstr n)
      sumF0 zero n r = cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _
      sumF0 (suc i) n r = cong₂ (Gstr n ._+_)
                                (cong (subst G (sameFiber r)) (0-⋆ _))
                                (sumF0 i n (≤-trans ≤-sucℕ r))
                          ∙ +IdR (Gstr n) _
                          ∙ subst0g _

    prodFunAnnihilR : (f : (n : ℕ) → (G n)) → f prodFun 0Fun ≡ 0Fun
    prodFunAnnihilR f = funExt (λ n → sumF0 n n ≤-refl)
      where
      sumF0 : (i n : ℕ) → (r : i ≤ n) → sumFun i n r f 0Fun ≡ 0g (Gstr n)
      sumF0 zero n r = cong (subst G (sameFiber r)) (⋆-0 _) ∙ subst0g _
      sumF0 (suc i) n r = cong₂ (Gstr n ._+_)
                                (cong (subst G (sameFiber r)) (⋆-0 _))
                                (sumF0 i n (≤-trans ≤-sucℕ r))
                          ∙ +IdR (Gstr n) _
                          ∙ subst0g _

    prodFunDistR : (f g h : (n : ℕ) → G n) → f prodFun (g +Fun h) ≡ (f prodFun g) +Fun (f prodFun h)
    prodFunDistR f g h = funExt (λ n → sumFAssoc n n ≤-refl)
     where
     sumFAssoc : (i n : ℕ) → (r : i ≤ n) → sumFun i n r f (g +Fun h) ≡ (Gstr n) ._+_ (sumFun i n r f g) (sumFun i n r f h)
     sumFAssoc zero n r = cong (subst G (sameFiber r)) (⋆DistR+ _ _ _)
                          ∙ sym (subst+ _ _ _)
     sumFAssoc (suc i) n r = cong₂ (Gstr n ._+_)
                                   (cong (subst G (sameFiber r)) (⋆DistR+ _ _ _) ∙ sym (subst+ _ _ _))
                                   (sumFAssoc i n (≤-trans ≤-sucℕ r))
                             ∙ comm-4 ((G n) , (Gstr n)) _ _ _ _

    prodFunDistL : (f g h : (n : ℕ) → G n) → (f +Fun g) prodFun h ≡ (f prodFun h) +Fun (g prodFun h)
    prodFunDistL f g h = funExt (λ n → sumFAssoc n n ≤-refl)
     where
     sumFAssoc : (i n : ℕ) → (r : i ≤ n) → sumFun i n r (f +Fun g) h ≡ (Gstr n) ._+_ (sumFun i n r f h) (sumFun i n r g h)
     sumFAssoc zero n r = cong (subst G (sameFiber r)) (⋆DistL+ _ _ _)
                          ∙ sym (subst+ _ _ _)
     sumFAssoc (suc i) n r = cong₂ (Gstr n ._+_)
                                   (cong (subst G (sameFiber r)) (⋆DistL+ _ _ _) ∙ sym (subst+ _ _ _))
                                   (sumFAssoc i n (≤-trans ≤-sucℕ r))
                             ∙ comm-4 ((G n) , (Gstr n)) _ _ _ _

-----------------------------------------------------------------------------
-- Preserving the product

   -- A substitution lemma
    subst⋆ : {m n k l : ℕ} → (p : m ≡ n) → (q : k ≡ l) → (r : m +n k ≡ n +n l) →
                  (a : G m) → (b : G k) → subst G p a ⋆ subst G q b ≡ subst G r (a ⋆ b)
    subst⋆ p q r a b = J (λ n p → subst G p a ⋆ subst G q b ≡ subst G (cong₂ _+n_ p q) (a ⋆ b))
                              (J (λ l q → subst G refl a ⋆ subst G q b ≡ subst G (cong₂ _+n_ refl q) (a ⋆ b))
                                 (cong₂ _⋆_ (transportRefl _) (transportRefl _) ∙ sym (transportRefl _))
                                 q)
                               p
                             ∙ cong (λ X → subst G X (a ⋆ b)) (isSetℕ _ _ _ _)

    -- Proving the base case
    open GradedRing-⊕HIT-index (ℕ , (monoidstr 0 _+n_ isM)) G Gstr
    open GradedRing-⊕HIT-⋆ 1⋆ _⋆_ 0-⋆ ⋆-0 ⋆Assoc ⋆IdR ⋆IdL ⋆DistR+ ⋆DistL+

    sumFun≠ : (k : ℕ) → (a : G k) → (l : ℕ) →  (b : G l) →
              (i n : ℕ) → (r : i ≤ n) → (¬pp : k +n l ≡ n → ⊥) →
              sumFun i n r (fun-trad k a) (fun-trad l b) ≡ 0g (Gstr n)
    sumFun≠ k a l b zero n r ¬pp with discreteℕ k 0 | discreteℕ l n
    ... | yes p | yes q = ⊥.rec (¬pp ((k +≡ l) ∙ cong₂ _+ℕ_ p q) )
    ... | yes p | no ¬q = cong (subst G (sameFiber r)) (⋆-0 _) ∙ subst0g _
    ... | no ¬p | yes q = cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _
    ... | no ¬p | no ¬q = cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _
    sumFun≠ k a l b (suc i) n r ¬pp with discreteℕ k (suc i) | discreteℕ l (n -ℕ (suc i))
    ... | yes p | yes q = ⊥.rec (¬pp (cong₂ _+n_ p q ∙ sameFiber r))
    ... | yes p | no ¬q = cong₂ (Gstr n ._+_)
                                (cong (subst G (sameFiber r)) (⋆-0 _))
                                (sumFun≠ k a l b i n (≤-trans ≤-sucℕ r) ¬pp)
                          ∙ +IdR (Gstr n) _
                          ∙ subst0g _
    ... | no ¬p | yes q = cong₂ (Gstr n ._+_)
                                (cong (subst G (sameFiber r)) (0-⋆ _))
                                (sumFun≠ k a l b i n (≤-trans ≤-sucℕ r) ¬pp)
                          ∙ +IdR (Gstr n) _
                          ∙ subst0g _
    ... | no ¬p | no ¬q = cong₂ (Gstr n ._+_)
                                (cong (subst G (sameFiber r)) (0-⋆ _))
                                (sumFun≠ k a l b i n (≤-trans ≤-sucℕ r) ¬pp)
                          ∙ +IdR (Gstr n) _
                          ∙ subst0g _

    -- If k +n l ≡ n then, we unwrap the sum until we reach k.
    -- Before it is 0, in k the value, then it is 0
    sumFun< : (k : ℕ) → (a : G k) → (l : ℕ) →  (b : G l) →
              (i n : ℕ) → (r : i ≤ n) → (i < k) →
              sumFun i n r (fun-trad k a) (fun-trad l b) ≡ 0g (Gstr n)
    sumFun< k a l b zero n r pp with discreteℕ k 0
    ... | yes p = ⊥.rec (<→≢ pp (sym p))
    ... | no ¬p = cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _
    sumFun< k a l b (suc i) n r pp with discreteℕ k (suc i)
    ... | yes p = ⊥.rec (<→≢ pp (sym p))
    ... | no ¬p = cong₂ (Gstr n ._+_)
                        (cong (subst G (sameFiber r)) (0-⋆ _))
                        (sumFun< k a l b i n (≤-trans ≤-sucℕ r) (<-trans ≤-refl pp))
                  ∙ +IdR (Gstr n) _
                  ∙ subst0g _

    sumFun≤ : (k : ℕ) → (a : G k) → (l : ℕ) →  (b : G l ) →
              (i n : ℕ) → (r : i ≤ n) → (pp : k +n l ≡ n) → (k ≤ i) →
              sumFun i n r (fun-trad k a) (fun-trad l b) ≡ subst G pp (a ⋆ b)
    sumFun≤ k a l b zero n r pp rr with discreteℕ k 0 | discreteℕ l n
    ... | yes p | yes q = cong (subst G (sameFiber r)) (subst⋆ p q (pp ∙ sym (+nIdL _)) a b)
                          ∙ sym (substComposite G _ _ _)
                          ∙ cong (λ X → subst G X (a ⋆ b)) (isSetℕ _ _ _ _)
    ... | yes p | no ¬q = ⊥.rec (¬q (sym (+nIdL l) ∙ cong (λ X → X +n l) (sym p) ∙ pp))
    ... | no ¬p | yes q = ⊥.rec (¬p (≤0→≡0 rr))
    ... | no ¬p | no ¬q = ⊥.rec (¬p (≤0→≡0 rr))
    sumFun≤ k a l b (suc i) n r pp rr with discreteℕ k (suc i) | discreteℕ l (n -ℕ suc i)
    ... | yes p | yes q = cong₂ (Gstr n ._+_)
                                (cong (subst G (sameFiber r))
                                      (subst⋆ p q (pp ∙ sym (sameFiber r)) a b)
                                      ∙ sym (substComposite G _ _ _))
                                (sumFun< k a l b i n (≤-trans ≤-sucℕ r) (0 , (sym p)))
                          ∙ +IdR (Gstr n) _
                          ∙ cong (λ X → subst G X (a ⋆ b)) (isSetℕ _ _ _ _)
    ... | yes p | no ¬q = ⊥.rec (¬q (inj-m+ (sym ((suc i) +≡ l)
                                            ∙ cong (λ X → X +n l) (sym p)
                                            ∙ pp
                                            ∙ sym (sameFiber r)
                                            ∙ ((suc i) +≡ (n -ℕ suc i)))))
    ... | no ¬p | yes q = ⊥.rec (¬p (inj-+m (sym (k +≡ (n -ℕ suc i))
                                              ∙ cong (λ X → k +n X) (sym q)
                                              ∙ pp
                                              ∙ sym (sameFiber r)
                                              ∙ ((suc i) +≡ (n -ℕ suc i)))))
    ... | no ¬p | no ¬q = cong₂ (Gstr n ._+_)
                                (cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _)
                                (sumFun≤ k a l b i n (≤-trans ≤-sucℕ r) pp (≤-suc-≢ rr ¬p))
                          ∙ +IdL (Gstr n) _

     -- If k +n l ≢ n, then it is both zero
     -- Otherwise, it coincide in (k,l)
    sumFBase : (k : ℕ) → (a : G k) → (l : ℕ) →  (b : G l) → (n : ℕ) →
               fun-trad (k +n l) (a ⋆ b) n ≡ sumFun n n ≤-refl (fun-trad k a) (fun-trad l b)
    sumFBase k a l b n with discreteℕ (k +n l) n
    ... | yes p = sym (sumFun≤ k a l b n n ≤-refl p (l , (+-comm l k ∙ sym (k +≡ l) ∙ p)))
    ... | no ¬p = sym (sumFun≠ k a l b n n ≤-refl ¬p)

    -- Proof that ⊕HIT→⊕Fun preserve the cup product
    ⊕HIT→Fun-pres-prodFun : (x y : ⊕HIT ℕ G Gstr) → ⊕HIT→Fun (x prod y) ≡ ((⊕HIT→Fun x) prodFun (⊕HIT→Fun y))
    ⊕HIT→Fun-pres-prodFun = DS-Ind-Prop.f _ _ _ _
                         (λ x → isPropΠ (λ _ → isSetFun _ _))
                         (λ y → sym (prodFunAnnihilL (⊕HIT→Fun y)))
                         (λ k a → DS-Ind-Prop.f _ _ _ _ (λ _ → isSetFun _ _)
                                   (sym (prodFunAnnihilR (⊕HIT→Fun (base k a))))
                                   (λ l b → funExt λ n → sumFBase k a l b n)
                                   λ {U V} ind-U ind-V → cong₂ _+Fun_ ind-U ind-V
                                                          ∙ sym (prodFunDistR _ _ _))
                         λ {U} {V} ind-U ind-V y → cong₂ _+Fun_ (ind-U y) (ind-V y)
                                                    ∙ sym (prodFunDistL _ _ _)

    ⊕HIT→⊕Fun-pres-prodF : (x y : ⊕HIT ℕ G Gstr) → ⊕HIT→⊕Fun (x prod y) ≡ ((⊕HIT→⊕Fun x) prodF (⊕HIT→⊕Fun y))
    ⊕HIT→⊕Fun-pres-prodF x y = ΣPathTransport→PathΣ _ _
                                ((⊕HIT→Fun-pres-prodFun x y) , (squash₁ _ _))

-----------------------------------------------------------------------------
-- Graded Ring Structure

    open AbGroupStr (snd (⊕Fun-AbGr G Gstr)) using ()
        renaming
      ( 0g       to 0⊕Fun
      ; _+_      to _+⊕Fun_
      ; -_       to -⊕Fun_
      ; is-set   to isSet⊕Fun)

    open IsGroupHom

    ⊕FunGradedRing-Ring : Ring ℓ
    ⊕FunGradedRing-Ring = InducedRing ⊕HITgradedRing-Ring
                                      0⊕Fun 1⊕Fun _+⊕Fun_ _prodF_ -⊕Fun_
                                      (fst (Equiv-DirectSum G Gstr))
                                      (pres1 (snd (Equiv-DirectSum G Gstr)))
                                      ⊕HIT→⊕Fun-pres1
                                      (pres· (snd (Equiv-DirectSum G Gstr)))
                                      ⊕HIT→⊕Fun-pres-prodF
                                      (presinv (snd (Equiv-DirectSum G Gstr)))

    RingEquiv-DirectSumGradedRing : RingEquiv ⊕HITgradedRing-Ring ⊕FunGradedRing-Ring
    RingEquiv-DirectSumGradedRing = InducedRingEquiv ⊕HITgradedRing-Ring
                                      0⊕Fun 1⊕Fun _+⊕Fun_ _prodF_ -⊕Fun_
                                      (fst (Equiv-DirectSum G Gstr))
                                      (pres1 (snd (Equiv-DirectSum G Gstr)))
                                      ⊕HIT→⊕Fun-pres1
                                      (pres· (snd (Equiv-DirectSum G Gstr)))
                                      ⊕HIT→⊕Fun-pres-prodF
                                      (presinv (snd (Equiv-DirectSum G Gstr)))

    ⊕Fun-GradedRing : GradedRing ℓ-zero ℓ
    ⊕Fun-GradedRing = makeGradedRing
                      ⊕FunGradedRing-Ring
                      (ℕ , (monoidstr 0 _+n_ isM))
                      G Gstr
                      1⋆ _⋆_
                      0-⋆ ⋆-0
                      ⋆Assoc ⋆IdR ⋆IdL
                      ⋆DistR+ ⋆DistL+
                      (RingEquivs.invRingEquiv RingEquiv-DirectSumGradedRing)

-----------------------------------------------------------------------------
-- CommRing extension

    module _
      (⋆Comm : {k l : ℕ} → (a : G k) → (b : G l) →
               _≡_ {A = Σ[ k ∈ ℕ ] G k} ((k +n l) , (a ⋆ b)) ((l +n k) , (b ⋆ a)))
      where

      open ExtensionCommRing ⋆Comm

      ⊕FunGradedRing-CommRing : CommRing ℓ
      ⊕FunGradedRing-CommRing = InducedCommRing ⊕HITgradedRing-CommRing
                                        0⊕Fun 1⊕Fun _+⊕Fun_ _prodF_ -⊕Fun_
                                        (fst (Equiv-DirectSum G Gstr))
                                        (pres1 (snd (Equiv-DirectSum G Gstr)))
                                        ⊕HIT→⊕Fun-pres1
                                        (pres· (snd (Equiv-DirectSum G Gstr)))
                                        ⊕HIT→⊕Fun-pres-prodF
                                        (presinv (snd (Equiv-DirectSum G Gstr)))

      CommRingEquiv-DirectSumGradedRing : CommRingEquiv ⊕HITgradedRing-CommRing ⊕FunGradedRing-CommRing
      CommRingEquiv-DirectSumGradedRing = InducedCommRingEquiv ⊕HITgradedRing-CommRing
                                        0⊕Fun 1⊕Fun _+⊕Fun_ _prodF_ -⊕Fun_
                                        (fst (Equiv-DirectSum G Gstr))
                                        (pres1 (snd (Equiv-DirectSum G Gstr)))
                                        ⊕HIT→⊕Fun-pres1
                                        (pres· (snd (Equiv-DirectSum G Gstr)))
                                        ⊕HIT→⊕Fun-pres-prodF
                                        (presinv (snd (Equiv-DirectSum G Gstr)))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Notation for adding an additional point to any set
------------------------------------------------------------------------

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

module Relation.Nullary.Construct.Add.Point where

open import Data.Maybe.Base using ()
  renaming (Maybe to Pointed; nothing to ∙; just to [_])
  public


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

open import M-types.Base.Core

module M-types.Base.Prod where
    ∏ : (X : Ty ℓ₀) → (Y : X → Ty ℓ₁) → Ty (ℓ-max ℓ₀ ℓ₁)
    ∏ X Y = (x : X) → Y x

    ∏-syntax : (X : Ty ℓ₀) → (Y : X → Ty ℓ₁) → Ty (ℓ-max ℓ₀ ℓ₁)
    ∏-syntax = ∏
    infix 2 ∏-syntax
    syntax ∏-syntax X (λ x → Y) = ∏[ x ∈ X ] Y

    id : {X : Ty ℓ} →
        (X → X)
    id = λ x → x

    infixr 9 _∘_
    _∘_ : {X : Ty ℓ₀} {Y : X → Ty ℓ₁} {Z : {x : X} → Y x → Ty ℓ₂} →
        ∏[ g ∈ ({x : X} → ∏[ y ∈ Y x ] Z y) ]
        ∏[ f ∈ (∏[ x ∈ X ] Y x) ]
        ∏[ x ∈ X ] Z (f x)
    f ∘ g = λ x → f (g x)

max_stars_repo_name: DDOtten/M-types

max_issues_repo_name: DDOtten/M-types

max_forks_repo_name: DDOtten/M-types


text:
{-# OPTIONS --cumulativity #-}

open import Agda.Primitive

module _ (a ℓ : Level) where

mutual
  X : Level
  X = _

  X<=a : Set X → Set a
  X<=a A = A

  test : Set₁
  test with (lsuc ℓ)
  ... | _ = Set
    where
      a<=X : Set a → Set X
      a<=X A = A


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

open import HoTT
open import lib.types.TwoSemiCategory

module homotopy.HSpace where

-- This is just an approximation because
-- not all higher cells are killed.
record HSpaceStructure {i} (X : Ptd i) : Type i where
  constructor hSpaceStructure
  field
    ⊙μ : (X ⊙× X) ⊙→ X

  μ : de⊙ X → de⊙ X → de⊙ X
  μ = curry (fst ⊙μ)

  field
    ⊙unit-l : ⊙μ ⊙∘ ⊙×-inr X X ⊙∼ ⊙idf X
    ⊙unit-r : ⊙μ ⊙∘ ⊙×-inl X X ⊙∼ ⊙idf X

  unit-l : ∀ x → μ (pt X) x == x
  unit-l = fst ⊙unit-l

  unit-r : ∀ x → μ x (pt X) == x
  unit-r = fst ⊙unit-r

  coh : unit-l (pt X) == unit-r (pt X)
  coh = ! (↓-idf=cst-out (snd ⊙unit-l) ∙ ∙-unit-r _)
      ∙ (↓-idf=cst-out (snd ⊙unit-r) ∙ ∙-unit-r _)

record AlternativeHSpaceStructure {i} (X : Ptd i) : Type i where
  constructor hSpaceStructure
  field
    μ : de⊙ X → de⊙ X → de⊙ X
    unit-l : ∀ x → μ (pt X) x == x
    unit-r : ∀ x → μ x (pt X) == x
    coh : unit-l (pt X) == unit-r (pt X)

  ⊙μ : (X ⊙× X) ⊙→ X
  ⊙μ = uncurry μ , unit-l (pt X)

  ⊙unit-l : ⊙μ ⊙∘ ⊙×-inr X X ⊙∼ ⊙idf X
  ⊙unit-l = unit-l , ↓-idf=cst-in' idp

  ⊙unit-r : ⊙μ ⊙∘ ⊙×-inl X X ⊙∼ ⊙idf X
  ⊙unit-r = unit-r , ↓-idf=cst-in' coh

from-alt-h-space : ∀ {i} {X : Ptd i} → AlternativeHSpaceStructure X → HSpaceStructure X
from-alt-h-space hss = record {AlternativeHSpaceStructure hss}

to-alt-h-space : ∀ {i} {X : Ptd i} → HSpaceStructure X → AlternativeHSpaceStructure X
to-alt-h-space hss = record {HSpaceStructure hss}

module ConnectedHSpace {i} {X : Ptd i} {{_ : is-connected 0 (de⊙ X)}}
  (hX : HSpaceStructure X) where

  open HSpaceStructure hX public

  {-
  Given that [X] is 0-connected, to prove that each [μ x] is an equivalence we
  only need to prove that one of them is. But for [x] = [pt X], [μ x] is the
  identity so we’re done.
  -}

  l-is-equiv : ∀ x → is-equiv (λ y → μ y x)
  l-is-equiv = prop-over-connected {a = pt X}
    (λ x → (is-equiv (λ y → μ y x) , is-equiv-is-prop))
    (transport! is-equiv (λ= unit-r) (idf-is-equiv _))

  r-is-equiv : ∀ x → is-equiv (λ y → μ x y)
  r-is-equiv = prop-over-connected {a = pt X}
    (λ x → (is-equiv (λ y → μ x y) , is-equiv-is-prop))
    (transport! is-equiv (λ= unit-l) (idf-is-equiv _))

  l-equiv : de⊙ X → de⊙ X ≃ de⊙ X
  l-equiv x = _ , l-is-equiv x

  r-equiv : de⊙ X → de⊙ X ≃ de⊙ X
  r-equiv x = _ , r-is-equiv x

module _ {i} {X : Ptd i} (hX : HSpaceStructure X) where

  module hX = HSpaceStructure hX

  associator : Type i
  associator = ∀ a b c → hX.μ (hX.μ a b) c == hX.μ a (hX.μ b c)

  coh-unit-l-eq : associator → de⊙ X → de⊙ X → Type i
  coh-unit-l-eq assoc a b =
    assoc (pt X) a b ◃∙
    hX.unit-l (hX.μ a b) ◃∎
    =ₛ
    ap (λ x → hX.μ x b) (hX.unit-l a) ◃∎

  coh-unit-l : associator → Type i
  coh-unit-l assoc = ∀ a b → coh-unit-l-eq assoc a b

  coh-unit-r-eq : associator → de⊙ X → de⊙ X → Type i
  coh-unit-r-eq assoc a b =
    hX.unit-r (hX.μ a b) ◃∎
    =ₛ
    assoc a b (pt X) ◃∙
    ap (hX.μ a) (hX.unit-r b) ◃∎

  coh-unit-r : associator → Type i
  coh-unit-r assoc = ∀ a b → coh-unit-r-eq assoc a b

  coh-unit-l-r-pentagon : associator → Type i
  coh-unit-l-r-pentagon assoc = ∀ a' →
    hX.unit-r (hX.μ (pt X) a') ◃∙
    hX.unit-l a' ◃∎
    =ₛ
    assoc (pt X) a' (pt X) ◃∙
    hX.unit-l (hX.μ a' (pt X)) ◃∙
    hX.unit-r a' ◃∎

  coh-unit-l-to-unit-l-r-pentagon : (assoc : associator)
    → coh-unit-l assoc → coh-unit-l-r-pentagon assoc
  coh-unit-l-to-unit-l-r-pentagon assoc c a' =
    hX.unit-r (hX.μ (pt X) a') ◃∙
    hX.unit-l a' ◃∎
      =ₛ⟨ !ₛ (homotopy-naturality-to-idf (λ x → hX.μ x (pt X)) hX.unit-r (hX.unit-l a')) ⟩
    ap (λ x → hX.μ x (pt X)) (hX.unit-l a') ◃∙
    hX.unit-r a' ◃∎
      =ₛ⟨ 0 & 1 & !ₛ (c a' (pt X)) ⟩
    assoc (pt X) a' (pt X) ◃∙
    hX.unit-l (hX.μ a' (pt X)) ◃∙
    hX.unit-r a' ◃∎ ∎ₛ

  coh-unit-r-to-unit-l-r-pentagon : (assoc : associator)
    → coh-unit-r assoc → coh-unit-l-r-pentagon assoc
  coh-unit-r-to-unit-l-r-pentagon assoc c a' =
    hX.unit-r (hX.μ (pt X) a') ◃∙
    hX.unit-l a' ◃∎
      =ₛ⟨ 0 & 1 & c (pt X) a' ⟩
    assoc (pt X) a' (pt X) ◃∙
    ap (hX.μ (pt X)) (hX.unit-r a') ◃∙
    hX.unit-l a' ◃∎
      =ₛ⟨ 1 & 3 &
          homotopy-naturality-to-idf (hX.μ (pt X))
                                     hX.unit-l
                                     (hX.unit-r a') ⟩
    assoc (pt X) a' (pt X) ◃∙
    hX.unit-l (hX.μ a' (pt X)) ◃∙
    hX.unit-r a' ◃∎ ∎ₛ

  coh-assoc-pentagon-eq : (assoc : associator) → (a b c d : de⊙ X) → Type i
  coh-assoc-pentagon-eq assoc a b c d =
    assoc (hX.μ a b) c d ◃∙ assoc a b (hX.μ c d) ◃∎
    =ₛ
    ap (λ s → hX.μ s d) (assoc a b c) ◃∙ assoc a (hX.μ b c) d ◃∙ ap (hX.μ a) (assoc b c d) ◃∎

  coh-assoc-pentagon : (assoc : associator) → Type i
  coh-assoc-pentagon assoc = ∀ a b c d → coh-assoc-pentagon-eq assoc a b c d

  HSpace-2-semi-category : {{X-level : has-level 1 (de⊙ X)}}
    → (assoc : associator)
    → coh-assoc-pentagon assoc
    → TwoSemiCategory lzero i
  HSpace-2-semi-category assoc assoc-coh =
    record
    { El = ⊤
    ; Arr = λ _ _ → de⊙ X
    ; Arr-level = λ _ _ → ⟨⟩
    ; two-semi-cat-struct =
      record
      { comp = hX.μ
      ; assoc = assoc
      ; pentagon-identity = assoc-coh
      }
    }

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda