text:
open import FRP.JS.Nat using ( ℕ ; suc ; _+_ )
open import FRP.JS.DOM
open import FRP.JS.RSet
open import FRP.JS.Time using ( Time ; epoch )
open import FRP.JS.Delay using ( _ms )
open import FRP.JS.Behaviour
open import FRP.JS.Bool using ( Bool ; not ; true )
open import FRP.JS.QUnit using ( TestSuite ; ok◇ ; test ; _,_ ; ε )

module FRP.JS.Test.DOM where

withDOW : {A : Set} → ((w : DOW) → A) → A
withDOW f = f unattached

tests : TestSuite
tests =
  ( test "≟*"
    ( ok◇ "[] ≟* []"
      (withDOW λ w → [] {w} ≟* [])
    , ok◇ "[] ++ [] ≟* []"
      (withDOW λ w → [] {left w} ++ [] ≟* []) )
  , test "attr"
    ( ok◇ "attr class [ alpha ] ≟* attr class [ alpha ]"
      (withDOW λ w → attr {w} "class" [ "alpha" ] ≟* attr "class" [ "alpha" ])
    , ok◇ "attr foo [ alpha ] ≟* attr foo [ alpha ]"
      (withDOW λ w → attr {w} "foo" [ "alpha" ] ≟* attr "foo" [ "alpha" ])
    , ok◇ "attr foo [ alpha ] ++ attr bar [ alpha ] ≟* attr foo [ alpha ] ++ attr bar [ alpha ]"
      (withDOW λ w → attr {left w} "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ] ≟* attr "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ])
    , ok◇ "attr class [ beta ] ≟* attr class [ alpha ]"
      (withDOW λ w → not* (attr {w} "class" [ "beta" ] ≟* attr "class" [ "alpha" ]))
    , ok◇ "attr foo [ alpha ] ≟* attr class [ alpha ]"
      (withDOW λ w → not* (attr {w} "foo" [ "alpha" ] ≟* attr "class" [ "alpha" ]))
    , ok◇ "attr foo [ alpha ] ++ attr bar [ alpha ] ≟* attr foo [ alpha ]"
      (withDOW λ w → not* (attr {left w} "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ] ≟* attr "foo" [ "alpha" ])) )
  , test "text"
    ( ok◇ "text [ abc ] ≟* text [ abc ]"
      (withDOW λ w → text {w} [ "abc" ] ≟* text [ "abc" ])
    , ok◇ "text [ a ] ≟* text [ abc ]"
      (withDOW λ w → not* (text {w} [ "a" ] ≟* text [ "abc" ]))
    , ok◇ "[] ≟* text [ abc ]"
      (withDOW λ w → not* ([] ≟* text {w} [ "abc" ]))
    , ok◇ "text [ abc ] ++ [] ≟* text [ abc ]"
      (withDOW λ w → text {left w} [ "abc" ] ++ [] ≟* (text [ "abc" ]))
    , ok◇ "[] ++ text [ abc ] ≟* text [ abc ]"
      (withDOW λ w → [] ++ text {right w} [ "abc" ] ≟* (text [ "abc" ])) )
  , test "element"
    ( ok◇ "element p (text [ abc ]) ≟* element p (text [ abc ])"
      (withDOW λ w → element "p" {w} (text [ "abc" ]) ≟* element "p" (text [ "abc" ]))
    , ok◇ "element p (text [ a ]) ≟* element p (text [ abc ])"
      (withDOW λ w → not* (element "p" {w} (text [ "a" ]) ≟* element "p" (text [ "abc" ])))
    , ok◇ "element div (attr class [ alpha ] ++ text [ abc ]) ≟* element div (attr class [ alpha ] ++ text [ abc ])"
      (withDOW λ w → element "div" {w} (attr "class" [ "alpha" ] ++ text [ "abc" ]) ≟* element "div" {w} (attr "class" [ "alpha" ] ++ text [ "abc" ]))
    , ok◇ "element div (attr class [ beta ] ++ text [ abc ]) ≟* element div (attr class [ alpha ] ++ text [ abc ])"
      (withDOW λ w → not* (element "div" {w} (attr "class" [ "beta" ] ++ text [ "abc" ]) ≟* element "div" {w} (attr "class" [ "alpha" ] ++ text [ "abc" ])))
    , ok◇ "element p (text [ abc ]) ≟* element p (text [ abc ])"
      (withDOW λ w → element "p" {w} (text [ "abc" ]) ≟* element "p" (text [ "abc" ]))
    , ok◇ "element p (text [ a ]) ++ element p (text [ b ]) ≟* element p (text [ a ])"
      (withDOW λ w → not* (element "p" {left w} (text [ "a" ]) ++ element "p" (text [ "b" ]) ≟* element "p" (text [ "a" ])))
      )
  , test "join"
    ( ok◇ "text (join (map [ x ] [ abc ])) ≟* text [ abc ]"
      (withDOW λ w → text {w} (join (map (λ s → [ s ]) [ "abc" ])) ≟* text [ "abc" ])
    , ok◇ "join (map (text [ x ]) [ abc ]) ≟* text [ abc ]"
      (withDOW λ w → join (map (λ s → text {w} [ s ]) [ "abc" ]) ≟* text [ "abc" ])
   , ok◇ "element p (join (map (attr foo [ x ]) [ alpha ]) ++ join (map (attr bar [ x ]) [ alpha ])) ≟* element p (attr foo [ alpha ] ++ attr bar [ alpha ])"
      (withDOW λ w → element "p" {w} (join (map (λ s → attr "foo" [ s ]) [ "alpha" ]) ++ join (map (λ s → attr "bar" [ s ]) [ "alpha" ])) ≟* element "p" (attr "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ]))
   , ok◇ "element p (join (map (attr foo [ x ]) [ beta ]) ++ join (map (attr bar [ x ]) [ alpha ])) ≟* element p (attr foo [ alpha ] ++ attr bar [ alpha ])"
      (withDOW λ w → not* (element "p" {w} (join (map (λ s → attr "foo" [ s ]) [ "beta" ]) ++ join (map (λ s → attr "bar" [ s ]) [ "alpha" ])) ≟* element "p" (attr "foo" [ "alpha" ] ++ attr "bar" [ "alpha" ])))
    , ok◇ "text (join (map [ x ] [ a ])) ≟* text [ abc ]"
      (withDOW λ w → not* (text {w} (join (map (λ s → [ s ]) [ "a" ])) ≟* text [ "abc" ]))
    , ok◇ "join (map (text [ x ]) [ a ]) ≟* text [ abc ]"
      (withDOW λ w → not* (join (map (λ s → text {w} [ s ]) [ "a" ]) ≟* text [ "abc" ])) ) )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
-- Given two abelian groups A, B
--   the set of all group homomorphisms from A to B
-- is itself an abelian group.
-- In other words, Ab is cartesian closed.
-- This is needed to show Ab is an abelian category.

{-# OPTIONS --safe #-}

module Cubical.Algebra.AbGroup.Instances.Hom where

open import Cubical.Algebra.AbGroup.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Properties
open import Cubical.Foundations.Prelude

private
  variable
    ℓ ℓ' : Level

module _ (A : AbGroup ℓ) (B : AbGroup ℓ') where

  -- These names are useful for the proofs
  private
    open IsGroupHom
    open AbGroupStr (A .snd) using () renaming (0g to 0A; _+_ to _⋆_; -_ to inv)
    open AbGroupStr (B .snd) using (_+_; -_; +Comm; +Assoc; +IdR ; +InvR)
                             renaming (0g to 0B)
    open GroupTheory (AbGroup→Group B) using (invDistr) renaming (inv1g to inv0B)

    -- Some lemmas
    idrB : (b : B .fst) → b + 0B ≡ b
    idrB b = +IdR b

    invrB : (b : B .fst) → b + (- b) ≡ 0B
    invrB b = +InvR b

    hom0AB : (f : AbGroupHom A B) → f .fst 0A ≡ 0B
    hom0AB f = hom1g (AbGroupStr→GroupStr (A .snd)) (f .fst)
                     (AbGroupStr→GroupStr (B .snd)) (f .snd .pres·)

    homInvAB : (f : AbGroupHom A B) → (a : A .fst) → f .fst (inv a) ≡ (- f .fst a)
    homInvAB f a = homInv (AbGroupStr→GroupStr (A .snd)) (f .fst)
                          (AbGroupStr→GroupStr (B .snd)) (f .snd .pres·) a

  -- Zero morphism
  zero : AbGroupHom A B
  zero .fst a = 0B
  zero .snd .pres· a a' = sym (idrB _)
  zero .snd .pres1 = refl
  zero .snd .presinv a = sym (inv0B)

  -- Pointwise addition of morphisms
  module _ (f* g* : AbGroupHom A B) where
    private
      f = f* .fst
      g = g* .fst

    HomAdd : AbGroupHom A B
    HomAdd .fst = λ a → f a + g a

    HomAdd .snd .pres· a a' =
        f (a ⋆ a') + g (a ⋆ a')           ≡⟨ cong (_+ g(a ⋆ a')) (f* .snd .pres· _ _) ⟩
        (f a + f a') + g (a ⋆ a')         ≡⟨ cong ((f a + f a') +_) (g* .snd .pres· _ _) ⟩
        (f a + f a') + (g a + g a')       ≡⟨ sym (+Assoc _ _ _) ⟩
        f a + (f a' + (g a + g a'))       ≡⟨ cong (f a +_) (+Assoc _ _ _) ⟩
        f a + ((f a' + g a) + g a')       ≡⟨ cong (λ b → (f a + b + g a')) (+Comm _ _) ⟩
        f a + ((g a + f a') + g a')       ≡⟨ cong (f a +_) (sym (+Assoc _ _ _)) ⟩
        f a + (g a + (f a' + g a'))       ≡⟨ +Assoc _ _ _ ⟩
        (f a + g a) + (f a' + g a')       ∎

    HomAdd .snd .pres1 =
        f 0A + g 0A       ≡⟨ cong (_+ g 0A) (hom0AB f*) ⟩
        0B + g 0A         ≡⟨ cong (0B +_) (hom0AB g*) ⟩
        0B + 0B           ≡⟨ idrB _ ⟩
        0B                ∎

    HomAdd .snd .presinv a =
        f (inv a) + g (inv a)     ≡⟨ cong (_+ g (inv a)) (homInvAB f* _) ⟩
        (- f a) + g (inv a)       ≡⟨ cong ((- f a) +_) (homInvAB g* _) ⟩
        (- f a) + (- g a)         ≡⟨ +Comm _ _ ⟩
        (- g a) + (- f a)         ≡⟨ sym (invDistr _ _) ⟩
        - (f a + g a)             ∎

  -- Pointwise inverse of morphism
  module _ (f* : AbGroupHom A B) where
    private
      f = f* .fst

    HomInv : AbGroupHom A B
    HomInv .fst = λ a → - f a

    HomInv .snd .pres· a a' =
        - f (a ⋆ a')            ≡⟨ cong -_ (f* .snd .pres· _ _) ⟩
        - (f a + f a')          ≡⟨ invDistr _ _ ⟩
        (- f a') + (- f a)      ≡⟨ +Comm _ _ ⟩
        (- f a) + (- f a')      ∎

    HomInv .snd .pres1 =
        - (f 0A)      ≡⟨ cong -_ (f* .snd .pres1) ⟩
        - 0B          ≡⟨ inv0B ⟩
        0B            ∎

    HomInv .snd .presinv a =
        - f (inv a)     ≡⟨ cong -_ (homInvAB f* _) ⟩
        - (- f a)       ∎

  -- Group laws for morphisms
  private
    0ₕ = zero
    _+ₕ_ = HomAdd
    -ₕ_ = HomInv

  -- Morphism addition is associative
  HomAdd-assoc : (f g h : AbGroupHom A B) → (f +ₕ (g +ₕ h)) ≡ ((f +ₕ g) +ₕ h)
  HomAdd-assoc f g h = GroupHom≡ (funExt λ a → +Assoc _ _ _)

  -- Morphism addition is commutative
  HomAdd-comm : (f g : AbGroupHom A B) → (f +ₕ g) ≡ (g +ₕ f)
  HomAdd-comm f g = GroupHom≡ (funExt λ a → +Comm _ _)

  -- zero is right identity
  HomAdd-zero : (f : AbGroupHom A B) → (f +ₕ zero) ≡ f
  HomAdd-zero f = GroupHom≡ (funExt λ a → idrB _)

  -- -ₕ is right inverse
  HomInv-invr : (f : AbGroupHom A B) → (f +ₕ (-ₕ f)) ≡ zero
  HomInv-invr f = GroupHom≡ (funExt λ a → invrB _)

-- Abelian group structure on AbGroupHom A B
open AbGroupStr
HomAbGroupStr : (A : AbGroup ℓ) → (B : AbGroup ℓ') → AbGroupStr (AbGroupHom A B)
HomAbGroupStr A B .0g        = zero A B
HomAbGroupStr A B ._+_       = HomAdd A B
HomAbGroupStr A B .-_        = HomInv A B
HomAbGroupStr A B .isAbGroup = makeIsAbGroup isSetGroupHom
    (HomAdd-assoc A B) (HomAdd-zero A B) (HomInv-invr A B) (HomAdd-comm A B)

HomAbGroup : (A : AbGroup ℓ) → (B : AbGroup ℓ') → AbGroup (ℓ-max ℓ ℓ')
HomAbGroup A B = AbGroupHom A B , HomAbGroupStr A B

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module _ where

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

data Nat+Bool : Set where
  nat  : Nat  → Nat+Bool
  bool : Bool → Nat+Bool

data P : Nat+Bool → Set where
  p : {x : Nat+Bool} → P x

mkBool : ∀ {n b} → P (nat n) → P (bool b)
mkBool {zero}  _ = p {bool _}
mkBool {suc _} _ = p {bool _}

f : {x : Nat+Bool} → P x
f = λ { {nat n}  → g
      ; {bool b} → mkBool g }
  where
    g : P _
    g = p

crash : f {bool true} ≡ p {bool true}
crash = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Definition.Typed.EqRelInstance where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Reduction
open import Definition.Typed.EqualityRelation

open import Tools.Function

-- Judgmental instance of the equality relation

instance eqRelInstance : EqRelSet
eqRelInstance = eqRel _⊢_≡_ _⊢_≡_∷_ _⊢_≡_∷_
                      idᶠ idᶠ idᶠ univ
                      sym sym sym trans trans trans
                      conv conv wkEq wkEqTerm wkEqTerm
                      reduction reductionₜ
                      (refl ∘ᶠ Uⱼ) (refl ∘ᶠ ℕⱼ) (refl ∘ᶠ ℕⱼ)
                      Π-cong Π-cong (refl ∘ᶠ zeroⱼ) suc-cong
                      (λ x x₁ x₂ x₃ x₄ x₅ → η-eq x x₁ x₂ x₅)
                      refl app-cong natrec-cong

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
module NamedWhere where

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

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

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

reverse : {A : Set} -> List A -> List A
reverse {A} xs = rev xs []
  module reverse where
    rev : List A -> List A -> List A
    rev []        ys = ys
    rev (x :: xs) ys = rev xs (x :: ys)

rev : {A : Set} -> List A -> List A -> List A
rev = reverse.rev []

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Metalogic.Classical.Propositional.TruthSemanticsModel {ℓ} (Proposition : Set(ℓ)) where

import      Lvl
open import Data.Boolean
open import Data
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Functional
open import Metalogic.Classical.Propositional.Syntax{ℓ} (Proposition)
  renaming (
    ⊤   to ⊤ₗ ;
    ⊥   to ⊥ₗ ;
    ¬_  to ¬ₗ_ ;
    _∧_ to _∧ₗ_ ;
    _∨_ to _∨ₗ_ ;
    _⇒_ to _⇒ₗ_ )
open import Relator.Equals
open import Relator.Equals.Proofs
open import Sets.BoolSet

-- A model decides whether a proposition is true or false
-- Also known as Interpretation, Structure, Model
record Model : Set(ℓ) where
  field
    interpretProp : Proposition → Bool

-- TODO: Can this be called a "theory" of propositional logic? So that instances of the type Semantics is the "models" of logic?
-- TODO: Now, all the metalogic depends on booleans, which may not be satisfactory
module _ where
  import      Data.Boolean.Operators
  open        Data.Boolean.Operators.Logic

  satisfaction : Model → Formula → Bool
  satisfaction(𝔐)(• prop) = Model.interpretProp(𝔐) (prop)
  satisfaction(𝔐)(⊤ₗ) = 𝑇
  satisfaction(𝔐)(⊥ₗ) = 𝐹
  satisfaction(𝔐)(¬ₗ φ) = ¬(satisfaction(𝔐)(φ))
  satisfaction(𝔐)(φ₁ ∧ₗ φ₂) = (satisfaction(𝔐)(φ₁)) ∧ (satisfaction(𝔐)(φ₂))
  satisfaction(𝔐)(φ₁ ∨ₗ φ₂) = (satisfaction(𝔐)(φ₁)) ∨ (satisfaction(𝔐)(φ₂))
  satisfaction(𝔐)(φ₁ ⇒ₗ φ₂) = ¬(satisfaction(𝔐)(φ₁)) ∨ (satisfaction(𝔐)(φ₂))

  -- Syntactic details with the relation symbol
  record SatisfactionRelation {ℓ₁}{ℓ₂} (Obj : Set(ℓ) → Set(ℓ₁)) : Set(Lvl.𝐒(ℓ Lvl.⊔ ℓ₁ Lvl.⊔ ℓ₂)) where
    field
      _⊧_ : Model → Obj(Formula) → Set(ℓ₂)
  open SatisfactionRelation ⦃ ... ⦄ public

  instance
    -- Satisfaction for a single formula
    formula-satisfaction-relation : SatisfactionRelation(id)
    formula-satisfaction-relation = record{_⊧_ = \𝔐 φ → satisfaction(𝔐)(φ) ≡ 𝑇}

  instance
    -- Satisfaction for a list of formulas
    list-satisfaction-relation : SatisfactionRelation(BoolSet{ℓ})
    list-satisfaction-relation = record{_⊧_ = \𝔐 Γ → (∀{γ} → (γ ∈ Γ) → satisfaction(𝔐)(γ) ≡ 𝑇)}

  -- Entailment
  data _⊨_ (Γ : BoolSet{ℓ}(Formula)) (φ : Formula) : Set(ℓ) where
    [⊨]-intro : (∀{𝔐} → (𝔐 ⊧ Γ) → (𝔐 ⊧ φ)) → (Γ ⊨ φ)

  _⊭_ : BoolSet{ℓ}(Formula) → Formula → Set(ℓ)
  _⊭_ Γ φ = (_⊨_ Γ φ) → Empty{ℓ}

  -- Validity
  valid : Formula → Set(ℓ)
  valid = (∅ ⊨_)

  module Theorems where
    [⊤]-entailment : (∅ ⊨ ⊤ₗ)
    [⊤]-entailment = [⊨]-intro(const [≡]-intro)
    -- ∅ ⊨ ⊤ₗ
    -- ∀{𝔐} → (𝔐 ⊧ ∅) → (𝔐 ⊧ ⊤ₗ)
    -- ∀{𝔐} → (𝔐 ⊧ ∅) → (satisfaction(𝔐)(⊤ₗ) ≡ 𝑇)
    -- ∀{𝔐} → (∀{γ} → (γ ∈ ∅) → satisfaction(𝔐)(γ) ≡ 𝑇) → (satisfaction(𝔐)(⊤ₗ) ≡ 𝑇)

    -- [∧]-entailment : ∀{φ₁ φ₂} → ([ φ₁ ⊰ φ₂ ] ⊨ (φ₁ ∧ₗ φ₂))
    -- [∧]-entailment{φ₁}{φ₂} = [⊨]-intro ([∈]-proof ↦ congruence₁-op(_∧_) ([∈]-proof (use)) ([∈]-proof (skip use)))
    -- [ φ₁ ⊰ φ₂ ] ⊨ (φ₁ ∧ φ₂)
    -- ∀{𝔐} → (𝔐 ⊧ [ φ₁ ⊰ φ₂ ]) → (𝔐 ⊧ (φ₁ ∧ φ₂))
    -- ∀{𝔐} → (𝔐 ⊧ [ φ₁ ⊰ φ₂ ]) → (satisfaction(𝔐)(φ₁ ∧ₗ φ₂) ≡ 𝑇)
    -- ∀{𝔐} → (𝔐 ⊧ [ φ₁ ⊰ φ₂ ]) → (satisfaction(𝔐)(φ₁) ∧ satisfaction(𝔐)(φ₂) ≡ 𝑇)
    -- ∀{𝔐} → (∀{γ} → (γ ∈ [ φ₁ ⊰ φ₂ ]) → satisfaction(𝔐)(γ) ≡ 𝑇) → (satisfaction(𝔐)(φ₁) ∧ satisfaction(𝔐)(φ₂) ≡ 𝑇)

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 Structure.Operator.Monoid.Homomorphism where

import      Lvl
open import Logic
open import Logic.Predicate
open import Structure.Function
open import Structure.Function.Multi
open import Structure.Operator.Monoid
open import Structure.Setoid
open import Type

record Homomorphism
  {ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂}
  {X : Type{ℓ₁}} ⦃ _ : Equiv{ℓₑ₁}(X) ⦄ {_▫X_ : X → X → X} ( structureₗ : Monoid(_▫X_))
  {Y : Type{ℓ₂}} ⦃ _ : Equiv{ℓₑ₂}(Y) ⦄ {_▫Y_ : Y → Y → Y} ( structureᵣ : Monoid(_▫Y_))
  (f : X → Y)
  : Stmt{ℓ₁ Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓ₂ Lvl.⊔ ℓₑ₂} where

  constructor intro

  idₗ = Monoid.id(structureₗ)
  idᵣ = Monoid.id(structureᵣ)

  field
    ⦃ function ⦄ : Function(f)
    ⦃ preserve-op ⦄ : Preserving₂(f)(_▫X_)(_▫Y_)
    ⦃ preserve-id ⦄ : Preserving₀(f)(idₗ)(idᵣ)

_→ᵐᵒⁿᵒⁱᵈ_ : ∀{ℓₗ ℓₗₑ ℓᵣ ℓᵣₑ} → MonoidObject{ℓₗ}{ℓₗₑ} → MonoidObject{ℓᵣ}{ℓᵣₑ} → Type
A →ᵐᵒⁿᵒⁱᵈ B = ∃(Homomorphism(MonoidObject.monoid A)(MonoidObject.monoid B))


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

open import lib.Base
open import lib.PathGroupoid
open import lib.types.Empty
open import lib.types.Nat

module lib.types.TLevel where

⟨_⟩₋₁ : ℕ → ℕ₋₂
⟨ n ⟩₋₁ = S ⟨ n ⟩₋₂

⟨_⟩ : ℕ → ℕ₋₂
⟨ n ⟩ = S (S ⟨ n ⟩₋₂)

infixl 80 _+2+_
_+2+_ : ℕ₋₂ → ℕ₋₂ → ℕ₋₂
⟨-2⟩ +2+ n = n
S m +2+ n = S (m +2+ n)

+2+-unit-r : (m : ℕ₋₂) → m +2+ ⟨-2⟩ == m
+2+-unit-r ⟨-2⟩ = idp
+2+-unit-r (S m) = ap S (+2+-unit-r m)

+2+-βr : (m n : ℕ₋₂) → m +2+ (S n) == S (m +2+ n)
+2+-βr ⟨-2⟩ n = idp
+2+-βr (S m) n = ap S (+2+-βr m n)

+2+-comm : (m n : ℕ₋₂) → m +2+ n == n +2+ m
+2+-comm m ⟨-2⟩ = +2+-unit-r m
+2+-comm m (S n) = +2+-βr m n ∙ ap S (+2+-comm m n)

+2+0 : (n : ℕ₋₂) → n +2+ 0 == S (S n)
+2+0 n = +2+-comm n 0

{- Inequalities -}
infix 40 _<T_
infix 40 _≤T_

data _<T_ : ℕ₋₂ → ℕ₋₂ → Type₀ where
  ltS : {m : ℕ₋₂} → m <T (S m)
  ltSR : {m n : ℕ₋₂} → m <T n → m <T (S n)

_≤T_ : ℕ₋₂ → ℕ₋₂ → Type₀
m ≤T n = Coprod (m == n) (m <T n)

-2<T : (m : ℕ₋₂) → ⟨-2⟩ <T S m
-2<T ⟨-2⟩ = ltS
-2<T (S m) = ltSR (-2<T m)

-2≤T : (m : ℕ₋₂) → ⟨-2⟩ ≤T m
-2≤T ⟨-2⟩ = inl idp
-2≤T (S m) = inr (-2<T m)

<T-trans : {m n k : ℕ₋₂} → m <T n → n <T k → m <T k
<T-trans lt₁ ltS = ltSR lt₁
<T-trans lt₁ (ltSR lt₂) = ltSR (<T-trans lt₁ lt₂)

≤T-refl : {m : ℕ₋₂} → m ≤T m
≤T-refl = inl idp

≤T-trans : {m n k : ℕ₋₂} → m ≤T n → n ≤T k → m ≤T k
≤T-trans {k = k} (inl p₁) lte₂ = transport (λ t → t ≤T k) (! p₁) lte₂
≤T-trans {m = m} lte₁ (inl p₂) = transport (λ t → m ≤T t) p₂ lte₁
≤T-trans (inr lt₁) (inr lt₂) = inr (<T-trans lt₁ lt₂)

<T-ap-S : {m n : ℕ₋₂} → m <T n → S m <T S n
<T-ap-S ltS = ltS
<T-ap-S (ltSR lt) = ltSR (<T-ap-S lt)

≤T-ap-S : {m n : ℕ₋₂} → m ≤T n → S m ≤T S n
≤T-ap-S (inl p) = inl (ap S p)
≤T-ap-S (inr lt) = inr (<T-ap-S lt)

<T-cancel-S : {m n : ℕ₋₂} → S m <T S n → m <T n
<T-cancel-S ltS = ltS
<T-cancel-S (ltSR lt) = <T-trans ltS lt

<T-+2+-l : {m n : ℕ₋₂} (k : ℕ₋₂) → m <T n → (k +2+ m) <T (k +2+ n)
<T-+2+-l ⟨-2⟩ lt = lt
<T-+2+-l (S k) lt = <T-ap-S (<T-+2+-l k lt)

≤T-+2+-l : {m n : ℕ₋₂} (k : ℕ₋₂) → m ≤T n → (k +2+ m) ≤T (k +2+ n)
≤T-+2+-l k (inl p) = inl (ap (λ t → k +2+ t) p)
≤T-+2+-l k (inr lt) = inr (<T-+2+-l k lt)

<T-+2+-r : {m n : ℕ₋₂} (k : ℕ₋₂) → m <T n → (m +2+ k) <T (n +2+ k)
<T-+2+-r k ltS = ltS
<T-+2+-r k (ltSR lt) = ltSR (<T-+2+-r k lt)

≤T-+2+-r : {m n : ℕ₋₂} (k : ℕ₋₂) → m ≤T n → (m +2+ k) ≤T (n +2+ k)
≤T-+2+-r k (inl p) = inl (ap (λ t → t +2+ k) p)
≤T-+2+-r k (inr lt) = inr (<T-+2+-r k lt)

private
  T-get-S : ℕ₋₂ → ℕ₋₂
  T-get-S ⟨-2⟩ = ⟨ 42 ⟩
  T-get-S (S n) = n

  T-S≠⟨-2⟩-type : ℕ₋₂ → Type₀
  T-S≠⟨-2⟩-type ⟨-2⟩ = Empty
  T-S≠⟨-2⟩-type (S n) = Unit

T-S≠⟨-2⟩ : (n : ℕ₋₂) → S n ≠ ⟨-2⟩
T-S≠⟨-2⟩ n p = transport T-S≠⟨-2⟩-type p unit

T-S≠ : (n : ℕ₋₂) → S n ≠ n
T-S≠ ⟨-2⟩ p = T-S≠⟨-2⟩ ⟨-2⟩ p
T-S≠ (S n) p = T-S≠ n (ap T-get-S p)

T-S+2+≠ : (n k : ℕ₋₂) → S (k +2+ n) ≠ n
T-S+2+≠ ⟨-2⟩ k p = T-S≠⟨-2⟩ (k +2+ ⟨-2⟩) p
T-S+2+≠ (S n) k p = T-S+2+≠ n k (ap T-get-S (ap S (! (+2+-βr k n)) ∙ p))

<T-witness : {m n : ℕ₋₂} → (m <T n) → Σ ℕ₋₂ (λ k → S k +2+ m == n)
<T-witness ltS = (⟨-2⟩ , idp)
<T-witness (ltSR lt) = let w' = <T-witness lt in (S (fst w') , ap S (snd w'))

≤T-witness : {m n : ℕ₋₂} → (m ≤T n) → Σ ℕ₋₂ (λ k → k +2+ m == n)
≤T-witness (inl p) = (⟨-2⟩ , p)
≤T-witness (inr lt) = let w' = <T-witness lt in (S (fst w') , snd w')

<T-to-≤T : {m n : ℕ₋₂} → m <T S n → m ≤T n
<T-to-≤T ltS = inl idp
<T-to-≤T (ltSR lt) = inr lt

<T-to-≠ : {m n : ℕ₋₂} → (m <T n) → m ≠ n
<T-to-≠ {m} {n} lt p = T-S+2+≠ m (fst w) (snd w ∙ ! p)
  where w = <T-witness lt

=-to-≮T : {m n : ℕ₋₂} → (m == n) → ¬ (m <T n)
=-to-≮T p lt = <T-to-≠ lt p

<T-to-≯T : {m n : ℕ₋₂} → (m <T n) → ¬ (n <T m)
<T-to-≯T lt gt = =-to-≮T idp (<T-trans lt gt)

<T-to-≱T : {m n : ℕ₋₂} → (m <T n) → ¬ (n ≤T m)
<T-to-≱T lt (inl p) = <T-to-≠ lt (! p)
<T-to-≱T lt (inr gt) = <T-to-≯T lt gt

{-
-2-monotone-< : {m n : ℕ} → (m < n) → (m -2 <T n -2)
-2-monotone-< ltS = ltS
-2-monotone-< (ltSR lt) = ltSR (-2-monotone-< lt)

-2-monotone-≤ : {m n : ℕ} → (m ≤ n) → (m -2 ≤T n -2)
-2-monotone-≤ (inl p) = inl (ap _-2 p)
-2-monotone-≤ (inr lt) = inr (-2-monotone-< lt)
-}

⟨⟩-monotone-< : {m n : ℕ} → (m < n) → (⟨ m ⟩ <T ⟨ n ⟩)
⟨⟩-monotone-< ltS = ltS
⟨⟩-monotone-< (ltSR lt) = ltSR (⟨⟩-monotone-< lt)

⟨⟩-monotone-≤ : {m n : ℕ} → (m ≤ n) → (⟨ m ⟩ ≤T ⟨ n ⟩)
⟨⟩-monotone-≤ (inl p) = inl (ap ⟨_⟩ p)
⟨⟩-monotone-≤ (inr lt) = inr (⟨⟩-monotone-< lt)

minT : ℕ₋₂ → ℕ₋₂ → ℕ₋₂
minT ⟨-2⟩ n = ⟨-2⟩
minT (S m) ⟨-2⟩ = ⟨-2⟩
minT (S m) (S n) = S (minT m n)

minT≤l : (m n : ℕ₋₂) → minT m n ≤T m
minT≤l ⟨-2⟩ n = inl idp
minT≤l (S m) ⟨-2⟩ = -2≤T (S m)
minT≤l (S m) (S n) = ≤T-ap-S (minT≤l m n)

minT≤r : (m n : ℕ₋₂) → minT m n ≤T n
minT≤r ⟨-2⟩ n = -2≤T n
minT≤r (S m) ⟨-2⟩ = inl idp
minT≤r (S m) (S n) = ≤T-ap-S (minT≤r m n)

minT-out : (m n : ℕ₋₂) → Coprod (minT m n == m) (minT m n == n)
minT-out ⟨-2⟩ _ = inl idp
minT-out (S _) ⟨-2⟩ = inr idp
minT-out (S m) (S n) with minT-out m n
minT-out (S m) (S n) | inl p = inl (ap S p)
minT-out (S m) (S n) | inr q = inr (ap S q)

minT-out-l : {m n : ℕ₋₂} → (m ≤T n) → minT m n == m
minT-out-l {m} {n} lte with minT-out m n
minT-out-l lte | inl eqm = eqm
minT-out-l (inl p) | inr eqn = eqn ∙ ! p
minT-out-l {m} {n} (inr lt) | inr eq =
  ⊥-rec (<T-to-≱T (transport (λ k → m <T k) (! eq) lt) (minT≤l m n))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
------------------------------------------------------------------------
-- Propierties of abstract typing contexts
------------------------------------------------------------------------

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

module Data.Context.Properties where

open import Data.Fin using (Fin; zero; suc; lift; raise)
open import Data.Fin.Substitution.ExtraLemmas
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Product using (_×_; _,_)
open import Data.Vec as Vec using (Vec; []; _∷_)
import Data.Vec.Properties as VecProps
open import Function as Fun using (_∘_; flip)
open import Relation.Binary.PropositionalEquality hiding (subst-∘)
open ≡-Reasoning
open import Relation.Unary using (Pred)

open import Data.Context
open import Data.Context.WellFormed

------------------------------------------------------------------------
-- Properties of abstract contexts and context extensions.

-- Properties of the `map' functions.

module _ {ℓ₁ ℓ₂} {T₁ : Pred ℕ ℓ₁} {T₂ : Pred ℕ ℓ₂} where

  -- pointwise equality is a congruence w.r.t. map and mapExt.

  map-cong : ∀ {n} {f g : ∀ {k} → T₁ k → T₂ k} → (∀ {k} → f {k} ≗ g {k}) →
             _≗_ {A = Ctx T₁ n} (map f) (map g)
  map-cong f≗g []        = refl
  map-cong f≗g (_∷_ t Γ) = cong₂ _∷_ (f≗g t) (map-cong f≗g Γ)

  mapExt-cong : ∀ {k m n} {f g : ∀ i → T₁ (i + m) → T₂ (i + n)} →
                (∀ {i} → f i ≗ g i) →
                _≗_ {A = CtxExt T₁ m k} (mapExt {T₂ = T₂} f) (mapExt g)
  mapExt-cong f≗g []            = refl
  mapExt-cong f≗g (_∷_ {l} t Γ) = cong₂ _∷_ (f≗g {l} t) (mapExt-cong f≗g Γ)

module _ {ℓ} {T : Pred ℕ ℓ} where

  -- map and mapExt are functorial.

  map-id : ∀ {n} → _≗_ {A = Ctx T n} (map Fun.id) Fun.id
  map-id []      = refl
  map-id (t ∷ Γ) = cong (t ∷_) (map-id Γ)

  mapExt-id : ∀ {m n} → _≗_ {A = CtxExt T m n} (mapExt λ _ t → t) Fun.id
  mapExt-id []      = refl
  mapExt-id (t ∷ Γ) = cong (t ∷_) (mapExt-id Γ)

module _ {ℓ₁ ℓ₂ ℓ₃} {T₁ : Pred ℕ ℓ₁} {T₂ : Pred ℕ ℓ₂} {T₃ : Pred ℕ ℓ₃} where

  map-∘ : ∀ {n} (f : ∀ {k} → T₂ k → T₃ k) (g : ∀ {k} → T₁ k → T₂ k)
          (Γ : Ctx T₁ n) → map {T₂ = T₃} (f ∘ g) Γ ≡ map {T₁ = T₂} f (map g Γ)
  map-∘ f g []      = refl
  map-∘ f g (t ∷ Γ) = cong (_ ∷_) (map-∘ f g Γ)

  mapExt-∘ : ∀ {k l m n}
             (f : ∀ i → T₂ (i + m) → T₃ (i + n))
             (g : ∀ i → T₁ (i + l) → T₂ (i + m)) →
             (Γ : CtxExt T₁ l k) →
             mapExt {T₂ = T₃} (λ i t → f i (g i t)) Γ ≡
               mapExt {T₁ = T₂} f (mapExt g Γ)
  mapExt-∘ f g []      = refl
  mapExt-∘ f g (t ∷ Γ) = cong (_ ∷_) (mapExt-∘ f g Γ)

-- Lemmas about operations on contexts that require weakening of
-- types.

module WeakenOpsLemmas {ℓ} {T : Pred ℕ ℓ} (extension : Extension T) where

  -- The underlyig operations.
  open WeakenOps extension

  -- Conversion to vector representation commutes with
  -- concatenation.

  toVec-++ : ∀ {m n} (Δ : CtxExt T m n) (Γ : Ctx T m) →
             toVec (Δ ++ Γ) ≡ extToVec Δ (toVec Γ)
  toVec-++ []      Γ = refl
  toVec-++ (t ∷ Δ) Γ =
    cong ((_ ∷_) ∘ Vec.map weaken) (toVec-++ Δ Γ)

  -- Lookup commutes with concatenation.

  lookup-++ : ∀ {m n} (Δ : CtxExt T m n) (Γ : Ctx T m) x →
              lookup (Δ ++ Γ) x ≡ extLookup Δ (toVec Γ) x
  lookup-++ Δ Γ x = cong (flip Vec.lookup x) (toVec-++ Δ Γ)

  -- We can skip the first element when looking up others.

  lookup-suc : ∀ {n} t (Γ : Ctx T n) x →
               lookup (t ∷ Γ) (suc x) ≡ weaken (lookup Γ x)
  lookup-suc t Γ x = VecProps.lookup-map x weaken (toVec Γ)

  extLookup-suc : ∀ {k m n} t (Γ : CtxExt T m n) (ts : Vec (T m) k) x →
                  extLookup (t ∷ Γ) ts (suc x) ≡ weaken (extLookup Γ ts x)
  extLookup-suc t Γ ts x = VecProps.lookup-map x weaken (extToVec Γ ts)

  -- We can skip a spliced-in element when looking up others.

  lookup-lift : ∀ {k m n} (Γ : CtxExt T m n) t (ts : Vec (T m) k) x →
                extLookup Γ ts x ≡ extLookup Γ (t ∷ ts) (lift n suc x)
  lookup-lift             []      t ts x       = refl
  lookup-lift             (u ∷ Δ) t ts zero    = refl
  lookup-lift {n = suc n} (u ∷ Δ) t ts (suc x) = begin
      extLookup (u ∷ Δ) ts (suc x)
    ≡⟨ extLookup-suc u Δ ts x ⟩
      weaken (extLookup Δ ts x)
    ≡⟨ cong weaken (lookup-lift Δ t ts x) ⟩
      weaken (extLookup Δ (t ∷ ts) (lift n suc x))
    ≡⟨ sym (extLookup-suc u Δ (t ∷ ts) (lift n suc x)) ⟩
      extLookup (u ∷ Δ) (t ∷ ts) (suc (lift n suc x))
    ∎

  -- Lookup in the prefix of a concatenation results in weakening.

  lookup-weaken⋆ : ∀ {m} n (Δ : CtxExt T m n) (Γ : Ctx T m) x →
                   lookup (Δ ++ Γ) (raise n x) ≡ weaken⋆ n (lookup Γ x)
  lookup-weaken⋆ zero    []      Γ x = refl
  lookup-weaken⋆ (suc n) (t ∷ Δ) Γ x = begin
      lookup (t ∷ Δ ++ Γ) (suc (raise n x))
    ≡⟨ VecProps.lookup-map (raise n x) weaken (toVec (Δ ++ Γ)) ⟩
      weaken (lookup (Δ ++ Γ) (raise n x))
    ≡⟨ cong weaken (lookup-weaken⋆ n Δ Γ x) ⟩
      weaken (weaken⋆ n (lookup Γ x))
    ∎

-- Lemmas relating conversions of context extensions to vector
-- representation with conversions of the underling entries.

module ConversionLemmas {T₁ T₂ : ℕ → Set}
                        (extension₁ : Extension T₁)
                        (extension₂ : Extension T₂) where
  private
    module W₁ = WeakenOps extension₁
    module W₂ = WeakenOps extension₂

  toVec-map : ∀ {n} (f : ∀ {k} → T₁ k → T₂ k) (Γ : Ctx T₁ n) →
              (∀ {k} (t : T₁ k) → W₂.weaken (f t) ≡ f (W₁.weaken t)) →
              W₂.toVec (map f Γ) ≡ Vec.map f (W₁.toVec Γ)
  toVec-map f []        _   = refl
  toVec-map f (_∷_ t Γ) hyp = cong₂ _∷_ (hyp t) (begin
      Vec.map W₂.weaken (W₂.toVec (map f Γ))
    ≡⟨ cong (Vec.map W₂.weaken) (toVec-map f Γ hyp) ⟩
      (Vec.map W₂.weaken (Vec.map f (W₁.toVec Γ)))
    ≡⟨ sym (VecProps.map-∘ W₂.weaken f (W₁.toVec Γ)) ⟩
      (Vec.map (W₂.weaken ∘ f) (W₁.toVec Γ))
    ≡⟨ VecProps.map-cong hyp (W₁.toVec Γ) ⟩
      (Vec.map (f ∘ W₁.weaken) (W₁.toVec Γ))
    ≡⟨ VecProps.map-∘ f W₁.weaken (W₁.toVec Γ) ⟩
      (Vec.map f (Vec.map W₁.weaken (W₁.toVec Γ)))
    ∎)

  -- Lookup commutes with re-indexing, provided that the reindexing
  -- function commutes with weakening.

  lookup-map : ∀ {n} (f : ∀ {k} → T₁ k → T₂ k) (Γ : Ctx T₁ n) x →
               (∀ {k} (t : T₁ k) → W₂.weaken (f t) ≡ f (W₁.weaken t)) →
               W₂.lookup (map f Γ) x ≡ f (W₁.lookup Γ x)
  lookup-map f Γ x hyp = begin
      W₂.lookup (map f Γ) x
    ≡⟨ cong (flip Vec.lookup x) (toVec-map f Γ hyp) ⟩
      Vec.lookup (Vec.map f (W₁.toVec Γ)) x
    ≡⟨ VecProps.lookup-map x f (W₁.toVec Γ) ⟩
      f (W₁.lookup Γ x)
    ∎

-- Lemmas about well-formed contexts and context extensions.

module ContextFormationLemmas {t ℓ} {T : Pred ℕ t}
                              (_⊢_wf : Wf T T ℓ) where
  open ContextFormation _⊢_wf

  -- Concatenation preserves well-formedness of contexts.

  wf-++-wfExt : ∀ {m n} {Δ : CtxExt T m n} {Γ : Ctx T m} →
                Γ ⊢ Δ wfExt → Γ wf → Δ ++ Γ wf
  wf-++-wfExt []               Γ-wf = Γ-wf
  wf-++-wfExt (t-wf ∷ Δ-wfExt) Γ-wf = t-wf ∷ wf-++-wfExt Δ-wfExt Γ-wf

  -- Splitting of well-formed contexts.
  wf-split : ∀ {m n} {Δ : CtxExt T m n} {Γ : Ctx T m} →
             Δ ++ Γ wf → Γ ⊢ Δ wfExt × Γ wf
  wf-split {Δ = []}    Γ-wf             = [] , Γ-wf
  wf-split {Δ = t ∷ Δ} (t-wf ∷ Δ++Γ-wf) =
    let Δ-wfExt , Γ-wf = wf-split Δ++Γ-wf
    in t-wf ∷ Δ-wfExt , Γ-wf

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
module Haskell.Prim.Monad where

open import Haskell.Prim
open import Haskell.Prim.Applicative
open import Haskell.Prim.Either
open import Haskell.Prim.Foldable
open import Haskell.Prim.Functor
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Monoid
open import Haskell.Prim.String
open import Haskell.Prim.Tuple

--------------------------------------------------
-- Monad

record Monad (m : Set → Set) : Set₁ where
  field
    _>>=_ : m a → (a → m b) → m b
    overlap ⦃ super ⦄ : Applicative m

  return : a → m a
  return = pure

  _>>_ : m a → m b → m b
  m >> m₁ = m >>= λ _ → m₁

  _=<<_ : (a → m b) → m a → m b
  _=<<_ = flip _>>=_

open Monad ⦃ ... ⦄ public

mapM₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → (a → m b) → t a → m ⊤
mapM₋ f = foldr (λ x k → f x >> k) (pure tt)

sequence₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → t (m a) → m ⊤
sequence₋ = foldr _>>_ (pure tt)

instance
  iMonadList : Monad List
  iMonadList ._>>=_ = flip concatMap

  iMonadMaybe : Monad Maybe
  iMonadMaybe ._>>=_ m k = maybe Nothing k m

  iMonadEither : Monad (Either a)
  iMonadEither ._>>=_ m k = either Left k m

  iMonadFun : Monad (λ b → a → b)
  iMonadFun ._>>=_ f k r = k (f r) r

  iMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_)
  iMonadTuple₂ ._>>=_ (a , x) k = first (a <>_) (k x)

  iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_)
  iMonadTuple₃ ._>>=_ (a , b , x) k =
    case k x of λ where
      (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y

  iMonadTuple₄ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →
                 Monad (λ d → Tuple (a ∷ b ∷ c ∷ d ∷ []))
  iMonadTuple₄ ._>>=_ (a ∷ b ∷ c ∷ x ∷ []) k =
    case k x of λ where
      (a₁ ∷ b₁ ∷ c₁ ∷ y ∷ []) → a <> a₁ ∷ b <> b₁ ∷ c <> c₁ ∷ y ∷ []

record MonadFail (m : Set → Set) : Set₁ where
  field
    fail : String → m a
    overlap ⦃ super ⦄ : Monad m

open MonadFail ⦃ ... ⦄ public

instance
  MonadFailList : MonadFail List
  MonadFailList .fail _ = []

  MonadFailMaybe : MonadFail Maybe
  MonadFailMaybe .fail _ = Nothing


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

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

-- This module provides functionality for proving properties about
-- programs written using this RWS monad. The main definitions are:
-- -  RWS-weakestPre, a large elimination that, given an RWS program and a
--    post condition for the program, produces the weakest precondition needed
--    to satisfy that post condition. Branches in code using the constructors
--    `RWS-if` and friends are translated into products, with each component of
--    the product corresponding to a possible branch taken.
-- -  RWS-Contract is the type of proofs that, given a stateful computation and
--    a post condition, the weakest precondition suffices to prove that post
--    condition.
-- -  RWS-contract proves RWS-Contract, i.e., for every stateful computation
--    `m` and post condition `P`, given a proof over a pre-state `pre` the
--    weakest precondition for `P` holds, then postcondition `P` holds for the
--    post-state obtained from running `m` in state `pre`.

module Dijkstra.RWS where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Haskell.Modules.RWS
open import Haskell.Prelude

private
  variable
    Ev Wr St : Set
    A B C    : Set

-- Preconditions are predicates over environments and prestates.
RWS-Pre : (Ev St : Set) → Set₁
RWS-Pre Ev St = (ev : Ev) (pre : St) → Set

-- Postconditions are predicates over a result, poststate, and list of outputs.
RWS-Post : (Wr St A : Set) → Set₁
RWS-Post Wr St A = (x : A) (post : St) (outs : List Wr) → Set

RWS-Post-⇒ : (P Q : RWS-Post Wr St A) → Set
RWS-Post-⇒ P Q = ∀ r st outs → P r st outs → Q r st outs

-- RWS-weakestPre computes a predicate transformer: it maps a RWS
-- computation `m` and desired postcondition `Post` to the weakest precondition
-- needed to prove `P` holds after running `m`.
RWS-PredTrans : (Ev Wr St A : Set) → Set₁
RWS-PredTrans Ev Wr St A = RWS-Post Wr St A → RWS-Pre Ev St

-- When RWS computations are sequenced, e.g., `RWS-bind m λ x → f x`,
-- outputs are concatenated. The postcondition desired for the above sequence
-- becomes a postcondition for `f x` in which the outputs of `m` are prepended
-- to the outputs of `f x`.
RWS-Post++ : ∀ {Wr St A} → RWS-Post Wr St A → List Wr → RWS-Post Wr St A
RWS-Post++ P outs x post outs₁ = P x post (outs ++ outs₁)

-- Consider again the sequence `RWS-bind m₁ λ x → f x`. We also translate a
-- postcondition `P` for the sequence into a postcondition for `m` ---
-- specifically, the post condition we want for `m` is that the weakest
-- precondition for `RWS-Post++ P outs` holds, where `outs` are the outputs of
-- `m`.
RWS-weakestPre-bindPost  : (ev : Ev) (f : A → RWS Ev Wr St B) → RWS-Post Wr St B → RWS-Post Wr St A
RWS-weakestPre-ebindPost : (ev : Ev) (f : A → RWS Ev Wr St (Either C B)) → RWS-Post Wr St (Either C B) → RWS-Post Wr St (Either C A)

RWS-weakestPre : (m : RWS Ev Wr St A) → RWS-PredTrans Ev Wr St A
RWS-weakestPre (RWS-return x) P ev pre = P x pre []
RWS-weakestPre (RWS-bind m f) P ev pre =
  RWS-weakestPre m (RWS-weakestPre-bindPost ev f P) ev pre
RWS-weakestPre (RWS-gets f) P ev pre = P (f pre) pre []
RWS-weakestPre (RWS-put post) P ev pre = P unit post []
RWS-weakestPre RWS-ask P ev pre = P ev pre []
RWS-weakestPre (RWS-tell outs) P ev pre = P unit pre outs
RWS-weakestPre (RWS-if (clause (b ≔ c) gs)) P ev pre =
  (toBool b ≡ true → RWS-weakestPre c P ev pre)
  × (toBool b ≡ false → RWS-weakestPre (RWS-if gs) P ev pre)
RWS-weakestPre (RWS-if (otherwise≔ c)) P ev pre =
  RWS-weakestPre c P ev pre
RWS-weakestPre (RWS-either f₁ f₂ e) P ev pre =
    (∀ x → (e ≡ Left x) →
      RWS-weakestPre (f₁ x) P ev pre)
  × (∀ y → (e ≡ Right y) →
       RWS-weakestPre (f₂ y) P ev pre)
RWS-weakestPre (RWS-ebind m f) P ev pre =
  RWS-weakestPre m (RWS-weakestPre-ebindPost ev f P) ev pre
RWS-weakestPre (RWS-maybe f₁ f₂ m) P ev pre =
  (m ≡ nothing → RWS-weakestPre f₁ P ev pre)
  × (∀ j → m ≡ just j → RWS-weakestPre (f₂ j) P ev pre)

RWS-weakestPre-ebindPost ev f Post (Left r) post outs =
  Post (Left r) post outs
RWS-weakestPre-ebindPost ev f Post (Right r) post outs =
  ∀ c → c ≡ r → RWS-weakestPre (f c) (RWS-Post++ Post outs) ev post

RWS-weakestPre-bindPost ev f Post x post outs =
  ∀ r → r ≡ x → RWS-weakestPre (f r) (RWS-Post++ Post outs) ev post

-- The post condition `P` holds for `m` with environment `ev` and prestate `pre`
RWS-Post-True : (P : RWS-Post Wr St A) (m : RWS Ev Wr St A) (ev : Ev) (pre : St) → Set
RWS-Post-True P m ev pre =
  let (x , post , outs) = RWS-run m ev pre in
  P x post outs

-- For every RWS computation `m`, `RWS-Contract m` is the type of proofs that,
-- for all post conditions `P`, starting environments `ev` and prestates `pre`,
-- to prove that `P` holds after running `m` in `ev` and `pre`, it suffices to
-- provide a proof of the weakest precondition for `P` with respect to `m`,
-- `ev`, and `pre`.
RWS-Contract : (m : RWS Ev Wr St A) → Set₁
RWS-Contract{Ev}{Wr}{St}{A} m =
  (P : RWS-Post Wr St A)
  → (ev : Ev) (pre : St) → RWS-weakestPre m P ev pre
  → RWS-Post-True P m ev pre

-- This proves that `RWS-weakestPre` gives a *sufficient* precondition for
-- establishing a desired postcondition. Note thought that it does not prove
-- that this precondition is the weakest such one; even though this is true, it
-- is not important for our purposes.
RWS-contract : (m : RWS Ev Wr St A) → RWS-Contract m
RWS-contract (RWS-return x₁) P ev pre wp = wp
RWS-contract (RWS-bind m f) P ev pre wp
   with RWS-contract m _ ev pre wp
...| con
   with RWS-run m ev pre
...| x₁ , st₁ , outs₁ =
  RWS-contract (f x₁) _ ev st₁ (con x₁ refl)
RWS-contract (RWS-gets f) P ev pre wp = wp
RWS-contract (RWS-put x₁) P ev pre wp = wp
RWS-contract RWS-ask P ev pre wp = wp
RWS-contract (RWS-tell x₁) P ev pre wp = wp
RWS-contract{Ev}{Wr}{St}{A} (RWS-if gs) P ev pre wp = RWS-contract-if gs P ev pre wp
  where
  RWS-contract-if : (gs : Guards (RWS Ev Wr St A)) → RWS-Contract (RWS-if gs)
  RWS-contract-if (clause (b ≔ c) gs) P ev pre (wp₁ , wp₂)
    with toBool b
  ...| true = RWS-contract c _ ev pre (wp₁ refl)
  ...| false = RWS-contract-if gs _ ev pre (wp₂ refl)
  RWS-contract-if (otherwise≔ x) P ev pre wp =
    RWS-contract x P ev pre wp
RWS-contract (RWS-either f₁ f₂ (Left x)) P ev pre (wp₁ , wp₂) =
  RWS-contract (f₁ x) _ ev pre (wp₁ x refl)
RWS-contract (RWS-either f₁ f₂ (Right y)) P ev pre (wp₁ , wp₂) =
  RWS-contract (f₂ y) _ ev pre (wp₂ y refl)
RWS-contract (RWS-ebind m f) P ev pre wp
   with RWS-contract m _ ev pre wp
...| con
   with RWS-run m ev pre
... | Left x , st₁ , outs₁ = con
... | Right y , st₁ , outs₁ = RWS-contract (f y) _ ev st₁ (con y refl)
RWS-contract (RWS-maybe f₁ f₂ nothing) P ev pre (wp₁ , wp₂)
  = RWS-contract f₁ _ ev pre (wp₁ refl)
RWS-contract (RWS-maybe f₁ f₂ (just x)) P ev pre (wp₁ , wp₂) =
  RWS-contract (f₂ x) _ ev pre (wp₂ x refl)

-- This helper function is primarily used to take a proof concerning one
-- computation `m` and show that that proof implies a property concerning a
-- larger computation which contains `m`.
RWS-⇒
  : ∀ {P Q : RWS-Post Wr St A}
    → ∀ m (ev : Ev) st
    → RWS-weakestPre m P ev st
    → RWS-Post-⇒ P Q
    → RWS-weakestPre m Q ev st
RWS-⇒ (RWS-return x) ev st pre pf = pf x st [] pre
RWS-⇒ (RWS-bind m f) ev st pre pf =
  RWS-⇒
    m ev st pre
    (λ r₁ st₁ outs₁ pf₁ x x≡ →
      RWS-⇒
        (f x) ev st₁ (pf₁ x x≡)
        (λ r₂ st₂ outs₂ pf₂ → pf r₂ st₂ (outs₁ ++ outs₂) pf₂))
RWS-⇒ (RWS-gets f) ev st pre pf = pf _ _ _ pre
RWS-⇒ (RWS-put x)  ev st pre pf = pf _ _ _ pre
RWS-⇒ RWS-ask      ev st pre pf = pf _ _ _ pre
RWS-⇒ (RWS-tell x) ev st pre pf = pf _ _ _ pre
RWS-⇒ (RWS-if (otherwise≔ x)) ev st pre pf = RWS-⇒ x ev st pre pf
RWS-⇒ (RWS-if (clause (b ≔ c) cs)) ev st (pre₁ , pre₂) pf =
  (λ pf' → RWS-⇒ c ev st (pre₁ pf') pf)
  , λ pf' → RWS-⇒ (RWS-if cs) ev st (pre₂ pf') pf
proj₁ (RWS-⇒ (RWS-either f₁ f₂ (Left x)) ev st (pre₁ , pre₂) pf) x₁ x₁≡ =
  RWS-⇒ (f₁ x₁) ev st (pre₁ x₁ x₁≡) pf
proj₂ (RWS-⇒ (RWS-either f₁ f₂ (Left x) ) ev st (pre₁ , pre₂) pf) y ()
proj₁ (RWS-⇒ (RWS-either f₁ f₂ (Right y)) ev st (pre₁ , pre₂) pf) y₁ ()
proj₂ (RWS-⇒ (RWS-either f₁ f₂ (Right y)) ev st (pre₁ , pre₂) pf) y₁ y₁≡ =
  RWS-⇒ (f₂ y₁) ev st (pre₂ y₁ y₁≡) pf
RWS-⇒ (RWS-ebind m f) ev st pre pf =
  RWS-⇒ m ev st pre
        (λ { (Left x₁) st₁ outs x → pf _ _ _ x
             ; (Right y) st₁ outs x → λ c x₁ →
                 RWS-⇒ (f c) ev st₁ (x c x₁) (λ r st₂ outs₁ x₂ → pf r st₂ (outs ++ outs₁) x₂) })
proj₁ (RWS-⇒ (RWS-maybe m f x) ev st (pre₁ , pre₂) pf) ≡nothing = RWS-⇒ m ev st (pre₁ ≡nothing) pf
proj₂ (RWS-⇒ (RWS-maybe m f x) ev st (pre₁ , pre₂) pf) b b≡     = RWS-⇒ (f b) ev st (pre₂ b b≡) pf

RWS-⇒-bind
  : ∀ {P : RWS-Post Wr St A}
      {Q : RWS-Post Wr St B}
    → {f : A → RWS Ev Wr St B}
    → ∀ m ev st
    → RWS-weakestPre m P ev st
    → RWS-Post-⇒ P (RWS-weakestPre-bindPost ev f Q)
    → RWS-weakestPre (RWS-bind m f) Q ev st
RWS-⇒-bind m ev st con pf =
     RWS-⇒ m ev st con pf

RWS-⇒-ebind
  : ∀ {P : RWS-Post Wr St (Either C A)}
      {Q : RWS-Post Wr St (Either C B)}
    → {f : A → RWS Ev Wr St (Either C B)}
    → ∀ m ev st
    → RWS-weakestPre m P ev st
    → RWS-Post-⇒ P (RWS-weakestPre-ebindPost ev f Q)
    → RWS-weakestPre (RWS-ebind m f) Q ev st
RWS-⇒-ebind m ev st con pf =
  RWS-⇒ m ev st con pf


text:
open import Agda.Builtin.Reflection
open import Agda.Builtin.Bool
open import Agda.Builtin.String
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.List

_>>=_ = bindTC

`false `true : Term
`false = con (quote false) []
`true  = con (quote true)  []

macro
  macro? : Name → Term → TC ⊤
  macro? x hole =
    isMacro x >>= λ where
      false → unify hole `false
      true  → unify hole `true

test₁ : macro? macro? ≡ true
test₁ = refl

test₂ : macro? test₁ ≡ false
test₂ = refl

test₃ : macro? true ≡ false
test₃ = refl


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

open import Fragment.Algebra.Signature

module Fragment.Equational.Model.Satisfaction {Σ : Signature} where

open import Fragment.Equational.Theory.Base hiding (Σ)
open import Fragment.Algebra.Algebra Σ
open import Fragment.Algebra.Free Σ
open import Fragment.Algebra.Homomorphism Σ

open import Level using (Level; _⊔_)
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Data.Product using (_,_)
open import Relation.Binary using (Setoid)

private
  variable
    a ℓ : Level

_⊨⟨_⟩_ : ∀ {n} → (A : Algebra {a} {ℓ})
         → Env A n → Eq Σ n → Set ℓ
A ⊨⟨ θ ⟩ (lhs , rhs) =
  ∣ inst A θ ∣ lhs =[ A ] ∣ inst A θ ∣ rhs

_⊨_ : ∀ {n} → Algebra {a} {ℓ} → Eq Σ n → Set (a ⊔ ℓ)
_⊨_ S eq = ∀ θ → S ⊨⟨ θ ⟩ eq

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module Lemmachine.Response where
open import Lemmachine.Response.Status public
open import Data.Product
open import Data.List hiding (_++_)
open import Data.Nat
open import Data.String

data ResponseHeader : Set where
  _,_ : String → String → ResponseHeader

{-# COMPILED_DATA ResponseHeader
    Lemmachine.FFI.ResponseHeader
    Lemmachine.FFI.ResponseHeader
#-}

ResponseHeaders = List ResponseHeader

record Response : Set where
  field
    status : Status
    headers : ResponseHeaders
    body : String

showStatus : Status → String
showStatus OK = "200"
showStatus Created = "201"
showStatus Accepted = "202"
showStatus NoContent = "204"
showStatus MultipleChoices = "300"
showStatus MovedPermanently = "301"
showStatus SeeOther = "303"
showStatus NotModified = "304"
showStatus MovedTemporarily = "307"
showStatus BadRequest = "400"
showStatus Unauthorized = "401"
showStatus Forbidden = "403"
showStatus NotFound = "404"
showStatus MethodNotAllowed = "405"
showStatus NotAcceptable = "406"
showStatus Conflict = "409"
showStatus Gone = "410"
showStatus PreconditionFailed = "412"
showStatus RequestEntityTooLarge = "413"
showStatus RequestURItooLong = "414"
showStatus UnsupportedMediaType = "415"
showStatus NotImplemented = "501"
showStatus ServiceUnavailable = "503"

defaultHtml : Status → String
defaultHtml x = doctype ++ html x where
  doctype = "<!DOCTYPE html>"
  head = "<meta charset=utf-8 /><title>Lemmachine</title>"
  body : Status → String
  body x = "This HTTP status (" ++ showStatus x ++ ") is brought to you by Lemmachine!"
  html : Status → String
  html x = "" ++ head ++ body x ++ ""

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- Andreas, 2019-10-21, issue #4148, reported by omelkonian

{-# OPTIONS -v impossible:100 #-}

postulate
  A : Set

module M (I : Set) where

  postulate
    P : I → Set

  record R (i : I) : Set where
    constructor mk
    field
      f : P i

open module N = M A

data D : ∀ {i} → R i → Set where
  c : ∀ {i} {t : P i} → D (mk t)

test : ∀ {i} {t : R i} → D t → Set₁
test c = Set

-- WAS: internal error in a sanity check in etaExpandRecord'_

-- Should succeed


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

open import lib.Basics
open import lib.types.Group
open import lib.groups.Homomorphism
open import lib.groups.TensorProduct

module lib.types.CRing where

-- 1-approximation of commutative rings without higher coherence conditions.
record CRingStructure {i} (El : Type i)
  : Type i where
  constructor ring-structure
  field
    add-group-struct : GroupStructure El

  open GroupStructure add-group-struct

  zero : El
  zero = ident

  add : El → El → El
  add = comp

  neg : El → El
  neg = inv

  field
    add-comm    : ∀ a b → add a b == add b a
    one         : El
    mult        : El → El → El
    mult-unit-l : ∀ a → mult one a == a
    mult-assoc  : ∀ a b c → mult (mult a b) c == mult a (mult b c)
    mult-comm   : ∀ a b → mult a b == mult b a
    distr-l     : ∀ a b c → mult (add a b) c == add (mult a c) (mult b c)

  private
    infix 80 _⊕_
    _⊕_ = add
    infix 90 _⊗_
    _⊗_ = mult

  add-assoc : ∀ a b c → (a ⊕ b) ⊕ c == a ⊕ (b ⊕ c)
  add-assoc = assoc

  abstract
    mult-unit-r : ∀ a → a ⊗ one == a
    mult-unit-r a =
      a ⊗ one  =⟨ mult-comm a one ⟩
      one ⊗ a  =⟨ mult-unit-l a ⟩
      a        =∎

    distr-r : ∀ a b c → a ⊗ (b ⊕ c) == a ⊗ b ⊕ a ⊗ c
    distr-r a b c =
      a ⊗ (b ⊕ c)    =⟨ mult-comm a (add b c) ⟩
      (b ⊕ c) ⊗ a    =⟨ distr-l b c a ⟩
      b ⊗ a ⊕ c ⊗ a  =⟨ (mult-comm b a) |in-ctx (λ x → add x (mult c a)) ⟩
      a ⊗ b ⊕ c ⊗ a  =⟨ (mult-comm c a) |in-ctx (add (mult a b)) ⟩
      a ⊗ b ⊕ a ⊗ c  =∎

    mult-zero-l : ∀ a → zero ⊗ a == zero
    mult-zero-l a =
      cancel-l (zero ⊗ a) $
        zero ⊗ a ⊕ zero ⊗ a  =⟨ ! (distr-l zero zero a) ⟩
        (zero ⊕ zero) ⊗ a    =⟨ unit-l zero |in-ctx (λ x → x ⊗ a) ⟩
        zero ⊗ a             =⟨ ! (unit-r (zero ⊗ a)) ⟩
        zero ⊗ a ⊕ zero      =∎

    mult-zero-r : ∀ a → a ⊗ zero == zero
    mult-zero-r a =
      a ⊗ zero  =⟨ mult-comm a zero ⟩
      zero ⊗ a  =⟨ mult-zero-l a ⟩
      zero      =∎

record CRing i : Type (lsucc i) where
  constructor ring
  field
    El : Type i
    {{El-level}} : has-level 0 El
    ring-struct : CRingStructure El
  open CRingStructure ring-struct public

  add-group : Group i
  add-group = group El add-group-struct

  add-abgroup : AbGroup i
  add-abgroup = add-group , add-comm

  mult-hom : El → add-group →ᴳ add-group
  mult-hom g = group-hom (mult g) (distr-r g)

  mult-hom-zero : mult-hom zero == cst-hom
  mult-hom-zero = group-hom= (λ= mult-zero-l)

  private
    module R⊗R = TensorProduct add-abgroup add-abgroup
    module UP = R⊗R.UniversalProperty add-abgroup

    mult-bilinear-map : UP.BilinearMap
    mult-bilinear-map =
      record
      { bmap = mult
      ; linearity-l = distr-l
      ; linearity-r = distr-r
      }

  mult-hom' : R⊗R.grp →ᴳ add-group
  mult-hom' = UP.extend mult-bilinear-map

  mult-hom'-β : ∀ a b → GroupHom.f mult-hom' (a R⊗R.⊗ b) == mult a b
  mult-hom'-β = UP.extend-β mult-bilinear-map

Ring₀ : Type (lsucc lzero)
Ring₀ = CRing lzero

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

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

module FOT.PA.Inductive2Mendelson.NoPatternMatchingOnRefl where

open import PA.Inductive.Base

------------------------------------------------------------------------------
-- From PA.Inductive2Mendelson

S₁ :  ∀ {m n o} → m ≡ n → m ≡ o → n ≡ o
S₁ h₁ h₂ = trans (sym h₁) h₂

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

-- 20 May 2013. Requires the predecessor function.
-- S₄ : ∀ {m n} → succ m ≡ succ n → m ≡ n

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data Three : Set -- (AAA) To fix things, move this line...

data One : Set where
  one : Nat → One

data Two : Set where
  two : One → Two

lemma′ : ∀ (m n : Nat) → (one m) ≡ (one n) → m ≡ n
lemma′ m .m refl = refl

lemma : ∀ (m n : Nat) → (two (one m)) ≡ (two (one n)) → m ≡ n
lemma m .m refl = refl
{- Error was:
I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  two (one m) ≟ two (one n)
when checking that the pattern refl has type
two (one m) ≡ two (one n)
-}

-- (BBB) ... to here.

data Three where
  three : Three


text:
open import Categories.Category
open import Categories.Category.CartesianClosed

{-
  The internal language of a given cartesian closed category.
-}
module Internal {o ℓ e} (𝒞 : Category o ℓ e)
  (cartesianClosed : CartesianClosed 𝒞) where

open import Relation.Binary using (Rel)
open import Data.Product using (Σ-syntax; _,_)
open import Level

open import Syntax
open import Theory

open import Categories.Category.Cartesian 𝒞
open import Categories.Category.BinaryProducts 𝒞
open import Categories.Object.Terminal 𝒞

open Category 𝒞
open CartesianClosed cartesianClosed
open Cartesian cartesian
open BinaryProducts products
module T = Terminal terminal

module _ where
  open PType Obj

  data F : Set (o ⊔ ℓ) where
    Inherit : forall {A B : Obj} -> A ⇒ B -> F
    I : Type -> F
    J : Type -> F

  -- The same as ⟦_⟧T in Semantics.agda.
  ⟦_⟧T′ : Type -> Obj
  ⟦ ⌊ A ⌋ ⟧T′ = A
  ⟦ Unit ⟧T′ = T.⊤
  ⟦ A * A₁ ⟧T′ = ⟦ A ⟧T′ × ⟦ A₁ ⟧T′
  ⟦ A => A₁ ⟧T′ = ⟦ A ⟧T′ ⇨ ⟦ A₁ ⟧T′

  sorting : F -> Sorting
  sorting (Inherit {A} {B} f) = record { dom = ⌊ A ⌋ ; cod = ⌊ B ⌋ }
  sorting (I A) = record { dom = ⌊ ⟦ A ⟧T′ ⌋ ; cod = A }
  sorting (J A) = record { dom = A ; cod = ⌊ ⟦ A ⟧T′ ⌋ }

Sg : Signature o (o ⊔ ℓ)
Sg = record { Gr = Obj ; Func = F ; sorting = sorting }

open Signature Sg
open Term Sg

open import Semantics 𝒞 cartesianClosed Sg

open I (λ x → x)

i : forall (A : Type) -> (⟦ ⌊ ⟦ A ⟧T′ ⌋ ⟧T) ⇒ (⟦ A ⟧T)
j : forall (A : Type) -> (⟦ A ⟧T) ⇒ (⟦ ⌊ ⟦ A ⟧T′ ⌋ ⟧T)

i ⌊ A ⌋ = Category.id 𝒞
i Unit = Category.id 𝒞
i (A * A₁) = (i A) ⁂ (i A₁)
i (A => A₁) = λg (i A₁ ∘ (eval′ ∘ (Category.id 𝒞 ⁂ j A)))

j ⌊ A ⌋ = Category.id 𝒞
j Unit = Category.id 𝒞
j (A * A₁) = j A ⁂ j A₁
j (A => A₁) = λg ((j A₁ ∘ (eval′ ∘ (Category.id 𝒞 ⁂ i A))))

S : Structure
S = record { ⟦_⟧G = λ x → x ; ⟦_⟧F = λ { (Inherit f) → f ; (I A) → i A ; (J A) → j A} }

open Structure S

data Ax (Γ : Context) (A : Type) : Rel (Γ ⊢ A) (o ⊔ ℓ ⊔ e) where
  E : forall {e₁ e₂} -> ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧ -> Ax Γ A e₁ e₂

Th : Theory o (o ⊔ ℓ) (o ⊔ ℓ ⊔ e)
Th = record { Sg = Sg ; Ax = Ax }

M : Model 𝒞 cartesianClosed Th
M = S , λ { (E x) → x}

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Examples showing how the notion of Interleaving can be used
------------------------------------------------------------------------

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

module README.Data.Interleaving where

open import Level
open import Data.List.Base hiding (filter)
open import Data.List.Relation.Unary.All
open import Function
open import Relation.Nullary
open import Relation.Unary

-- In its most general form, `Interleaving` is parametrised by two relations
-- `L` (for Left) and `R` (for Right). Given three lists, `xs`, `ys` and `zs`,
-- a proof of `Interleaving xs ys zs` is essentially a diagram explaining how
-- `zs` can be pulled apart into `xs` and `ys` in a way compatible with `L`
-- and `R`. For instance:

-- xs               zs               ys
--
-- x₁ -- L x₁ z₁ -- z₁
-- x₂ -- L x₂ z₂ -- z₂
--                  z₃ -- R z₃ z₁ -- y₁
-- x₃ -- L x₃ z₄ -- z₄
--                  z₅ -- R z₅ y₂ -- y₂

open import Data.List.Relation.Ternary.Interleaving.Propositional

-- The special case we will focus on here is the propositional case: both
-- `L` and ̀R` are propositional equality. Rethinking our previous example,
-- this gives us the proof that [z₁, ⋯, z₅] can be partitioned into
-- [z₁, z₂, z₄] on the one hand and [z₃, z₅] in the other.

-- One possible use case for such a relation is the definition of a very
-- precise filter function. Provided a decidable predicate `P`, it will
-- prove not only that the retained values satisfy `P` but that the ones
-- that didn't make the cut satisfy the negation of P.

-- We can make this formal by defining the following record type:

infix 3 _≡_⊎_
record Filter {a p} {A : Set a} (P : Pred A p) (xs : List A) : Set (a ⊔ p) where
  constructor _≡_⊎_
  field
    -- The result of running filter is two lists:
    -- * the elements we have kept
    -- * and the ones we have thrown away
    -- We leave these implicit: they can be inferred from the rest
    {kept}   : List A
    {thrown} : List A
    -- There is a way for us to recover the original
    -- input by interleaving the two lists
    cover    : Interleaving kept thrown xs
    -- Finally, the partition was made according to the predicate
    allP     : All P kept
    all¬P    : All (∁ P) thrown

-- Once we have this type written down, we can write the function.
-- We use an anonymous module to clean up the function's type.

module _ {a p} {A : Set a} {P : Pred A p} (P? : Decidable P) where

  filter : ∀ xs → Filter P xs
  -- If the list is empty, we are done.
  filter []       = [] ≡ [] ⊎ []
  filter (x ∷ xs) =
    -- otherwise we start by running filter on the tail
    let xs' ≡ ps ⊎ ¬ps = filter xs in
    -- And depending on whether `P` holds of the head,
    -- we cons it to the `kept` or `thrown` list.
    case P? x of λ where -- [1]
      (yes p) → consˡ xs' ≡ p ∷ ps ⊎      ¬ps
      (no ¬p) → consʳ xs' ≡     ps ⊎ ¬p ∷ ¬ps

-- [1] See the following module for explanations of `case_of_` and
--     pattern-matching lambdas
import README.Case


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.RingStructure.RingLaws where
open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.RingStructure.CupProduct

open import Cubical.Homotopy.Loopspace

open import Cubical.HITs.S1 hiding (_·_)
open import Cubical.HITs.Sn
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.Truncation renaming (elim to trElim)

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Pointed.Homogeneous
open import Cubical.Foundations.GroupoidLaws hiding (assoc)
open import Cubical.Data.Int
  renaming (_+_ to _ℤ+_ ; _·_ to _ℤ∙_ ; +Comm to +ℤ-comm
          ; ·Comm to ∙-comm ; +Assoc to ℤ+-assoc ; -_ to -ℤ_)
    hiding (_+'_ ; +'≡+)
open import Cubical.Data.Nat
open import Cubical.Data.Sigma

private
  variable
    ℓ : Level

-- Some boring lemmas
·₀≡·ℤ : (x y : ℤ) → _·₀_ {n = zero} x y ≡ x ℤ∙ y
·₀≡·ℤ (pos zero) y = refl
·₀≡·ℤ (pos (suc n)) y = cong (y ℤ+_) (·₀≡·ℤ (pos n) y)
·₀≡·ℤ (negsuc zero) (pos zero) = refl
·₀≡·ℤ (negsuc zero) (pos (suc n)) = -AntiComm 0 (pos (suc n))
·₀≡·ℤ (negsuc zero) (negsuc n) = -AntiComm 0 (negsuc n)
·₀≡·ℤ (negsuc (suc n)) (pos m) =
   (cong ((_ℤ+ (pos 0 - pos m))) (·₀≡·ℤ (negsuc n) (pos m))
  ∙ cong ((negsuc n ℤ∙ (pos m)) ℤ+_)
         (-AntiComm 0 (pos m) ∙ cong (-ℤ_) (help m)))
  ∙ sym (+ℤ-comm (-ℤ (pos m)) (negsuc n ℤ∙ (pos m)))
    where
    help : (m : ℕ) → (pos m - 0) ≡ pos m
    help zero = refl
    help (suc m) = refl
·₀≡·ℤ (negsuc (suc n)) (negsuc m) =
     +ℤ-comm (_·₀_{n = zero} (negsuc n) (negsuc m)) (pos 0 - (negsuc m))
  ∙∙ cong ((pos 0 - negsuc m) ℤ+_) (·₀≡·ℤ (negsuc n) (negsuc m))
  ∙∙ cong (_ℤ+ (negsuc n ℤ∙ negsuc m)) (help m)
    where
    help : (m : ℕ) → (pos 0 - negsuc m) ≡ pos (suc m)
    help zero = refl
    help (suc n) = cong sucℤ (help n)

comm-·₀ : (x y : ℤ) → _·₀_ {n = 0} x y ≡ y ·₀ x
comm-·₀ x y = ·₀≡·ℤ x y ∙∙ ∙-comm x y ∙∙ sym (·₀≡·ℤ y x)

+'-assoc : (n m l : ℕ) → (n +' (m +' l)) ≡ ((n +' m) +' l)
+'-assoc n m l =
     (λ i → +'≡+ n (+'≡+ m l i) i)
  ∙∙ +-assoc n m l
  ∙∙ (λ i → +'≡+ (+'≡+ n m (~ i)) l (~ i))

-- Zero multiplication

⌣ₖ-0ₖ : (n m : ℕ) → (x : coHomK n)
        → x ⌣ₖ (0ₖ _) ≡ 0ₖ _
⌣ₖ-0ₖ  n m x = snd (⌣ₖ∙ n m x)

0ₖ-⌣ₖ : (n m : ℕ) → (x : coHomK m) →
        (0ₖ _) ⌣ₖ x ≡ 0ₖ _
0ₖ-⌣ₖ n m = funExt⁻ (cong fst (snd (⌣ₖ∙∙ n m)))

⌣ₖ-0ₖ≡0ₖ-⌣ₖ : (n m : ℕ) → ⌣ₖ-0ₖ n m (0ₖ _) ≡ 0ₖ-⌣ₖ n m (0ₖ _)
⌣ₖ-0ₖ≡0ₖ-⌣ₖ zero zero = refl
⌣ₖ-0ₖ≡0ₖ-⌣ₖ zero (suc m) = refl
⌣ₖ-0ₖ≡0ₖ-⌣ₖ (suc n) zero = refl
⌣ₖ-0ₖ≡0ₖ-⌣ₖ (suc zero) (suc m) = refl
⌣ₖ-0ₖ≡0ₖ-⌣ₖ (suc (suc n)) (suc m) = refl

-- Left distributivity

private
  ⌣ₖ-distrFun : -- z ⌣ₖ (x +ₖ y)
    (n m : ℕ) → (x y : coHomK n)
      → coHomK-ptd m →∙ coHomK-ptd (m +' n)
  fst (⌣ₖ-distrFun n m x y) z =
    z ⌣ₖ (x +ₖ y)
  snd (⌣ₖ-distrFun n m x y) =
    0ₖ-⌣ₖ m n (x +ₖ y)

  ⌣ₖ-distrFun2 : -- z ⌣ₖ x +ₖ z ⌣ₖ y
    (n m : ℕ) → (x y : coHomK n)
      → coHomK-ptd m →∙ coHomK-ptd (m +' n)
  fst (⌣ₖ-distrFun2 n m x y) z =
    z ⌣ₖ x +ₖ z ⌣ₖ y
  snd (⌣ₖ-distrFun2 n m x y) =
    cong₂ _+ₖ_ (0ₖ-⌣ₖ m n x) (0ₖ-⌣ₖ m n y) ∙ rUnitₖ _ _

  leftDistr-⌣ₖ· : (n m : ℕ) (x y : coHomK (suc n)) → ⌣ₖ-distrFun (suc n) (suc m) x y ≡ ⌣ₖ-distrFun2 (suc n) (suc m) x y
  leftDistr-⌣ₖ· n m =
    elim2 (λ _ _ → isOfHLevelSuc (2 + n) (hLevHelp n m _ _))
          main
    where
    hLevHelp : (n m : ℕ) (x y : _) → isOfHLevel (2 + n) ( ⌣ₖ-distrFun (suc n) (suc m) x y ≡ ⌣ₖ-distrFun2 (suc n) (suc m) x y)
    hLevHelp n m x y =
      (subst (isOfHLevel (3 + n))
        (λ i → (coHomK-ptd (suc m) →∙ coHomK-ptd (suc (suc (+-comm n m i)))))
          (isOfHLevel↑∙ (suc n) m)) _ _

    left-fst : (n : ℕ) (x : S₊ (suc n)) →
      fst (⌣ₖ-distrFun (suc n) (suc m) ∣ ptSn (suc n) ∣ ∣ x ∣) ≡
      fst (⌣ₖ-distrFun2 (suc n) (suc m) ∣ ptSn (suc n) ∣ ∣ x ∣)
    left-fst zero y =
        (funExt (λ z → sym (lUnitₖ _ (z ⌣ₖ ∣ y ∣)) ∙ λ i → ⌣ₖ-0ₖ _ _ z (~ i) +ₖ z ⌣ₖ ∣ y ∣))
    left-fst (suc n) y =
        (funExt (λ z → sym (lUnitₖ _ (z ⌣ₖ ∣ y ∣)) ∙ λ i → ⌣ₖ-0ₖ _ _ z (~ i) +ₖ z ⌣ₖ ∣ y ∣))

    right-fst : (n : ℕ) (x : S₊ (suc n)) →
      fst (⌣ₖ-distrFun (suc n) (suc m) ∣ x ∣ (0ₖ _)) ≡
      fst (⌣ₖ-distrFun2 (suc n) (suc m) ∣ x ∣ (0ₖ _))
    right-fst n x = funExt (λ z → (cong (z ⌣ₖ_) (rUnitₖ _ ∣ x ∣) ∙∙ sym (rUnitₖ _ _) ∙∙ λ i → z ⌣ₖ ∣ x ∣ +ₖ ⌣ₖ-0ₖ _ (suc n) z (~ i)))

    helper : (n : ℕ) (x : coHomK (suc n)) (p : 0ₖ _ ≡ x)
          → sym (lUnitₖ _ x) ∙ cong (_+ₖ x) p ≡ sym (rUnitₖ _ x) ∙ cong (x +ₖ_) p
    helper n x = J (λ x p → sym (lUnitₖ _ x) ∙ cong (_+ₖ x) p ≡ sym (rUnitₖ _ x) ∙ cong (x +ₖ_) p)
                   (helper' n)
      where
      helper' : (n : ℕ) → (λ i → lUnitₖ (suc n) (0ₖ (suc n)) (~ i)) ∙
               (λ i → 0ₖ (suc n) +ₖ 0ₖ (suc n))
               ≡
               (λ i → rUnitₖ (suc n) (0ₖ (suc n)) (~ i)) ∙
               (λ i → 0ₖ (suc n) +ₖ 0ₖ (suc n))
      helper' zero = refl
      helper' (suc n) = refl

    left-fst≡right-fst : (n : ℕ) → left-fst n (ptSn _) ≡ right-fst n (ptSn _)
    left-fst≡right-fst zero i j z = helper _ (z ⌣ₖ ∣ base ∣) (sym (⌣ₖ-0ₖ _ _ z)) i j
    left-fst≡right-fst (suc n) i j z = helper _ (z ⌣ₖ ∣ north ∣) (sym (⌣ₖ-0ₖ _ (suc (suc n)) z)) i j

    main : (a b : S₊ (suc n)) →
      ⌣ₖ-distrFun (suc n) (suc m) ∣ a ∣ₕ ∣ b ∣ₕ ≡
      ⌣ₖ-distrFun2 (suc n) (suc m) ∣ a ∣ₕ ∣ b ∣ₕ
    main =
      wedgeconFun n n
      (λ x y → subst (λ l → isOfHLevel l ((⌣ₖ-distrFun (suc n) (suc m) ∣ x ∣ ∣ y ∣)
                                           ≡  ⌣ₖ-distrFun2 (suc n) (suc m) ∣ x ∣ ∣ y ∣))
                        (+-suc n (suc n))
                        (isOfHLevelPlus {n = 2 + n} n (hLevHelp n m ∣ x ∣ ∣ y ∣)))
      (λ x → →∙Homogeneous≡ (isHomogeneousKn _) (left-fst n x))
      (λ x → →∙Homogeneous≡ (isHomogeneousKn _) (right-fst n x))
      (cong (→∙Homogeneous≡ (isHomogeneousKn _)) (sym (left-fst≡right-fst n)))

  -- Distributivity for 0 dimensional cases
  leftDistr₀n : (n : ℕ) → (z : coHomK 0) (x y : coHomK n)
    → z ·₀ (x +[ n ]ₖ y) ≡ z ·₀ x +[ n ]ₖ (z ·₀ y)
  leftDistr₀n n (pos zero) x y = sym (rUnitₖ n (0ₖ _))
  leftDistr₀n n (pos (suc z)) x y =
       cong ((x +ₖ y) +ₖ_) (leftDistr₀n n (pos z) x y)
    ∙∙ sym (assocₖ n x y (pos z ·₀ x +[ n ]ₖ (pos z ·₀ y)))
    ∙∙ cong (x +ₖ_) (assocₖ n y (pos z ·₀ x) (pos z ·₀ y)
                 ∙∙ cong (_+ₖ (pos z ·₀ y)) (commₖ n y (pos z ·₀ x))
                 ∙∙ sym (assocₖ n (pos z ·₀ x) y (pos z ·₀ y)))
     ∙ assocₖ n x _ _
  leftDistr₀n n (negsuc zero) x y = -distrₖ n x y
  leftDistr₀n n (negsuc (suc z)) x y =
       cong₂ (_+ₖ_) (leftDistr₀n n (negsuc z) x y) (-distrₖ n x y)
    ∙∙ assocₖ n ((negsuc z ·₀ x) +ₖ (negsuc z ·₀ y)) (-ₖ x) (-ₖ y)
    ∙∙ cong (_-ₖ y) (sym (assocₖ n (negsuc z ·₀ x) (negsuc z ·₀ y) (-ₖ x))
                 ∙∙ cong ((negsuc z ·₀ x) +ₖ_) (commₖ n (negsuc z ·₀ y) (-ₖ x))
                 ∙∙ assocₖ n (negsuc z ·₀ x) (-ₖ x) (negsuc z ·₀ y))
     ∙ sym (assocₖ n (negsuc (suc z) ·₀ x) _ _)

  leftDistrn₀ : (n : ℕ) → (z : coHomK n) (x y : coHomK 0)
    → (x ℤ+ y) ·₀ z ≡ x ·₀ z +[ n ]ₖ (y ·₀ z)
  leftDistrn₀ n z x (pos zero) = sym (rUnitₖ n (x ·₀ z))
  leftDistrn₀ n z x (pos (suc y)) =
       lem (x +pos y)
    ∙∙ cong (z +ₖ_) (leftDistrn₀ n z x (pos y) ∙ commₖ n _ _)
    ∙∙ assocₖ n z _ _
     ∙ commₖ n _ _
    where
    lem : (a : ℤ) → (sucℤ a) ·₀ z ≡ z +ₖ (a ·₀ z)
    lem (pos zero) = refl
    lem (pos (suc a)) = cong (z +ₖ_) (lem (pos a))
    lem (negsuc zero) = sym (rCancelₖ n z)
    lem (negsuc (suc a)) = sym (-cancelLₖ n z (negsuc a ·₀ z)) ∙ sym (assocₖ n z (negsuc a ·₀ z) (-ₖ z))
  leftDistrn₀ n z x (negsuc y) = main y
    where
    help : (x : ℤ) → predℤ x ·₀ z ≡ (x ·₀ z -ₖ z)
    help (pos zero) = sym (lUnitₖ n (-ₖ z))
    help (pos (suc x)) = sym (-cancelLₖ n z (pos x ·₀ z))
    help (negsuc x) = refl

    main : (y : _) → (x ℤ+ negsuc y) ·₀ z ≡  (x ·₀ z) +ₖ (negsuc y ·₀ z)
    main zero = help x
    main (suc y) =
         help (x +negsuc y)
      ∙∙ cong (_-ₖ z) (main y)
      ∙∙ sym (assocₖ n _ _ _)

leftDistr-⌣ₖ : (n m : ℕ) (z : coHomK n) (x y : coHomK m)
          → z ⌣ₖ (x +ₖ y) ≡ (z ⌣ₖ x +ₖ z ⌣ₖ y)
leftDistr-⌣ₖ zero m z x y = leftDistr₀n m z x y
leftDistr-⌣ₖ (suc n) zero z x y = leftDistrn₀ (suc n) z x y
leftDistr-⌣ₖ (suc n) (suc m) z x y = funExt⁻ (cong fst (leftDistr-⌣ₖ· m n x y)) z

-- Right distributivity

private
  ⌣ₖ-distrFun-r : -- (x +ₖ y) ⌣ₖ z
    (n m : ℕ) → (x y : coHomK n)
      → coHomK-ptd m →∙ coHomK-ptd (n +' m)
  fst (⌣ₖ-distrFun-r n m x y) z =
    (x +ₖ y) ⌣ₖ z
  snd (⌣ₖ-distrFun-r n m x y) =
    ⌣ₖ-0ₖ n m (x +ₖ y) -- ⌣ₖ-0ₖ m n (x +ₖ y)

  ⌣ₖ-distrFun2-r :
    (n m : ℕ) → (x y : coHomK n)
      → coHomK-ptd m →∙ coHomK-ptd (n +' m)
  fst (⌣ₖ-distrFun2-r n m x y) z =
    x ⌣ₖ z +ₖ y ⌣ₖ z
  snd (⌣ₖ-distrFun2-r n m x y) =
    cong₂ _+ₖ_ (⌣ₖ-0ₖ n m x) (⌣ₖ-0ₖ n m y) ∙ rUnitₖ _ _

  rightDistr-⌣ₖ· : (n m : ℕ) (x y : coHomK (suc n)) → ⌣ₖ-distrFun-r (suc n) (suc m) x y ≡ ⌣ₖ-distrFun2-r (suc n) (suc m) x y
  rightDistr-⌣ₖ· n m =
    elim2 (λ _ _ → isOfHLevelPath (3 + n) (isOfHLevel↑∙ (suc n) m) _ _)
          main
    where
    fst-left : (n : ℕ) (y : S₊ (suc n)) →
      fst (⌣ₖ-distrFun-r (suc n) (suc m) ∣ ptSn (suc n) ∣ ∣ y ∣) ≡
      fst (⌣ₖ-distrFun2-r (suc n) (suc m) ∣ ptSn (suc n) ∣ ∣ y ∣)
    fst-left n y =
      funExt (λ z
        → cong (_⌣ₖ z) (lUnitₖ _ ∣ y ∣)
        ∙∙ sym (lUnitₖ _ (∣ y ∣ ⌣ₖ z))
        ∙∙ cong (_+ₖ (∣ y ∣ ⌣ₖ z)) (sym (0ₖ-⌣ₖ _ _ z)))

    fst-right : (n : ℕ) (x : S₊ (suc n)) →
      fst (⌣ₖ-distrFun-r (suc n) (suc m) ∣ x ∣ ∣ ptSn (suc n) ∣) ≡
      fst (⌣ₖ-distrFun2-r (suc n) (suc m) ∣ x ∣ ∣ ptSn (suc n) ∣)
    fst-right n x =
      funExt λ z
        → cong (_⌣ₖ z) (rUnitₖ _ ∣ x ∣)
        ∙∙ sym (rUnitₖ _ _)
        ∙∙ cong (∣ x ∣ ⌣ₖ z +ₖ_) (sym (0ₖ-⌣ₖ _ _ z))

    left≡right : (n : ℕ) → fst-left n (ptSn (suc n)) ≡ fst-right n (ptSn (suc n))
    left≡right zero = refl
    left≡right (suc n) = refl

    main : (a b : S₊ (suc n)) →
      ⌣ₖ-distrFun-r (suc n) (suc m) ∣ a ∣ₕ ∣ b ∣ₕ ≡
      ⌣ₖ-distrFun2-r (suc n) (suc m) ∣ a ∣ₕ ∣ b ∣ₕ
    main =
      wedgeconFun n n
        (λ x y → subst (λ l → isOfHLevel l ((⌣ₖ-distrFun-r (suc n) (suc m) ∣ x ∣ ∣ y ∣)
                                           ≡  ⌣ₖ-distrFun2-r (suc n) (suc m) ∣ x ∣ ∣ y ∣))
                        (+-suc n (suc n))
                        (isOfHLevelPlus {n = 2 + n} n (isOfHLevel↑∙ (suc n) m _ _)))
        (λ x → →∙Homogeneous≡ (isHomogeneousKn _) (fst-left n x))
        (λ x → →∙Homogeneous≡ (isHomogeneousKn _) (fst-right n x))
        (cong (→∙Homogeneous≡ (isHomogeneousKn _)) (sym (left≡right n)))

rightDistr-⌣ₖ : (n m : ℕ) (x y : coHomK n) (z : coHomK m)
          → (x +ₖ y) ⌣ₖ z ≡ (x ⌣ₖ z +ₖ y ⌣ₖ z)
rightDistr-⌣ₖ zero zero x y z =
     comm-·₀ (x ℤ+ y) z
  ∙∙ leftDistr-⌣ₖ zero zero z x y
  ∙∙ cong₂ _+ₖ_ (sym (comm-·₀ x z)) (sym (comm-·₀ y z))
rightDistr-⌣ₖ zero (suc m) x y z = leftDistr-⌣ₖ _ zero z x y
rightDistr-⌣ₖ (suc n) zero x y z = leftDistr-⌣ₖ zero (suc n) z x y
rightDistr-⌣ₖ (suc n) (suc m) x y z = (funExt⁻ (cong fst (rightDistr-⌣ₖ· n m x y))) z

-- Associativity

private
-- We need to give the two associators as (doubly) pointed functions
  assocer : (n m k : ℕ) → coHomK (suc n)
    →  coHomK-ptd (suc m)
    →∙ (coHomK-ptd (suc k)
    →∙ coHomK-ptd ((suc n) +' ((suc m) +' (suc k))) ∙)
  fst (fst (assocer n m k x) y) z = x ⌣ₖ (y ⌣ₖ z)
  snd (fst (assocer n m k x) y) = cong (x ⌣ₖ_) (⌣ₖ-0ₖ _ (suc k) y) ∙ ⌣ₖ-0ₖ _ _ x
  snd (assocer n m k x) =
    ΣPathP (funExt (λ z → cong (x ⌣ₖ_) (0ₖ-⌣ₖ (suc m) (suc k) z) ∙ ⌣ₖ-0ₖ (suc n) _ x)
          , help)
    where
    h : (n m k : ℕ) (x : coHomK (suc n)) → cong (_⌣ₖ_ x) (⌣ₖ-0ₖ (suc m) (suc k) (0ₖ _)) ≡
                                  (λ i → x ⌣ₖ 0ₖ-⌣ₖ (suc m) (suc k) (0ₖ _) i)
    h zero zero k x = refl
    h zero (suc m) k x = refl
    h (suc n) zero k x = refl
    h (suc n) (suc m) k x = refl

    help : PathP (λ i → (cong (x ⌣ₖ_) (0ₖ-⌣ₖ (suc m) (suc k) (0ₖ _)) ∙ ⌣ₖ-0ₖ (suc n) _ x) i ≡ 0ₖ _)
               (cong (x ⌣ₖ_) (⌣ₖ-0ₖ (suc m) (suc k) (0ₖ _)) ∙ ⌣ₖ-0ₖ (suc n) _ x) refl
    help = compPathR→PathP
      (cong (_∙ ⌣ₖ-0ₖ (suc n) ((suc m) +' (suc k)) x) (h n m k x)
      ∙∙ rUnit _
      ∙∙ cong ((cong (x ⌣ₖ_) (0ₖ-⌣ₖ (suc m) (suc k) (0ₖ _)) ∙ ⌣ₖ-0ₖ (suc n) _ x) ∙_) (rUnit refl))

  assoc2-sub : (n m k : ℕ) → _ → _
  assoc2-sub n m k = subst coHomK (sym (+'-assoc n m k))

  assoc2-sub-0 : (n m k : ℕ) → assoc2-sub n m k (0ₖ _) ≡ 0ₖ _
  assoc2-sub-0 zero zero zero = refl
  assoc2-sub-0 zero zero (suc zero) = refl
  assoc2-sub-0 zero zero (suc (suc k)) = refl
  assoc2-sub-0 zero (suc zero) zero = refl
  assoc2-sub-0 zero (suc zero) (suc k) = refl
  assoc2-sub-0 zero (suc (suc m)) zero = refl
  assoc2-sub-0 zero (suc (suc m)) (suc k) = refl
  assoc2-sub-0 (suc zero) zero zero = refl
  assoc2-sub-0 (suc zero) zero (suc k) = refl
  assoc2-sub-0 (suc (suc n)) zero zero = refl
  assoc2-sub-0 (suc (suc n)) zero (suc k) = refl
  assoc2-sub-0 (suc zero) (suc m) zero = refl
  assoc2-sub-0 (suc (suc n)) (suc m) zero = refl
  assoc2-sub-0 (suc zero) (suc m) (suc k) = refl
  assoc2-sub-0 (suc (suc n)) (suc m) (suc k) = refl

  assocer2 : (n m k : ℕ)
           → coHomK (suc n)
           → coHomK-ptd (suc m) →∙ (coHomK-ptd (suc k) →∙ coHomK-ptd ((suc n) +' ((suc m) +' (suc k))) ∙)
  fst (fst (assocer2 n m k x) y) z =
    subst coHomK (sym (+'-assoc (suc n) (suc m) (suc k))) ((x ⌣ₖ y) ⌣ₖ z) --
  snd (fst (assocer2 zero m k x) y) =
    cong (subst coHomK (sym (+'-assoc 1 (suc m) (suc k)))) (⌣ₖ-0ₖ _ _ (x ⌣ₖ y))
  snd (fst (assocer2 (suc n) m k x) y) =
    cong (subst coHomK (sym (+'-assoc (2 + n) (suc m) (suc k)))) (⌣ₖ-0ₖ _ _ (x ⌣ₖ y))
  fst (snd (assocer2 zero m k x) i) z =
    subst coHomK (sym (+'-assoc (suc zero) (suc m) (suc k))) (⌣ₖ-0ₖ _ _ x i ⌣ₖ z)
  snd (snd (assocer2 zero m k x) i) j =
    subst coHomK (sym (+'-assoc (suc zero) (suc m) (suc k))) (⌣ₖ-0ₖ _ _ (⌣ₖ-0ₖ _ _ x i) j)
  fst (snd (assocer2 (suc n) m k x) i) z =
    subst coHomK (sym (+'-assoc (2 + n) (suc m) (suc k))) (⌣ₖ-0ₖ _ _ x i ⌣ₖ z)
  snd (snd (assocer2 (suc n) m k x) i) j =
    subst coHomK (sym (+'-assoc (2 + n) (suc m) (suc k))) (⌣ₖ-0ₖ _ _ (⌣ₖ-0ₖ _ _ x i) j)

  assocer-helpFun : (n m : ℕ) → coHomK (suc n) → coHomK-ptd (suc m) →∙ Ω (coHomK-ptd (3 + (n + m)))
  fst (assocer-helpFun n m a) b = Kn→ΩKn+1 _ (a ⌣ₖ b)
  snd (assocer-helpFun n m a) = cong (Kn→ΩKn+1 _) (⌣ₖ-0ₖ (suc n) (suc m) a) ∙ Kn→ΩKn+10ₖ _

  assocer-helpFun2 : (n m : ℕ) → coHomK (suc n) → coHomK-ptd (suc m) →∙ Ω (coHomK-ptd (3 + (n + m)))
  fst (assocer-helpFun2 n m a) b i = (Kn→ΩKn+1 _ a i) ⌣ₖ b
  snd (assocer-helpFun2 n m a) i j = ⌣ₖ-0ₖ _ (suc m) (Kn→ΩKn+1 _ a j) i

-- Key lemma for associativity
assocer-helpFun≡ : (n m : ℕ) → (x : coHomK (suc n)) → assocer-helpFun n m x ≡ assocer-helpFun2 n m x
assocer-helpFun≡ n m =
  trElim (λ _ → isOfHLevelPath (3 + n) (hLev-assocer-helpFun n m) _ _)
         λ a → →∙Homogeneous≡ (subst isHomogeneous Kn≃ΩKn+1∙ (isHomogeneousKn _))
           (funExt (main n a))
  where
  hLev-assocer-helpFun : (n m : ℕ) → isOfHLevel (3 + n) (coHomK-ptd (suc m) →∙ Ω (coHomK-ptd (3 + (n + m))))
  hLev-assocer-helpFun n m =
    subst (isOfHLevel (3 + n)) (cong (coHomK-ptd (suc m) →∙_)
      (Kn≃ΩKn+1∙))
      (isOfHLevel↑∙ (suc n) m)

  main : (n : ℕ) (a : S₊ (suc n)) (b : _)
    → fst (assocer-helpFun n m ∣ a ∣) b ≡ fst (assocer-helpFun2 n m ∣ a ∣) b
  main zero a b k i =
    hcomp
      (λ r → λ {(i = i0) → 0ₖ _
               ; (i = i1) → ∣ rCancel (merid north) r (~ k) ∣
               ; (k = i0) → Kn→ΩKn+1 _ (∣ a ∣ ⌣ₖ b) i
               ; (k = i1) → (Kn→ΩKn+1 _ ∣ a ∣ i) ⌣ₖ b})
      (∣ compPath-filler (merid a) (sym (merid base)) k i ∣ ⌣ₖ b)
  main (suc n) a b k i =
    hcomp
      (λ r → λ {(i = i0) → 0ₖ _
               ; (i = i1) → ∣ rCancel (merid north) r (~ k) ∣
               ; (k = i0) → Kn→ΩKn+1 _ (∣ a ∣ ⌣ₖ b) i
               ; (k = i1) → (Kn→ΩKn+1 _ ∣ a ∣ i) ⌣ₖ b})
      (∣ compPath-filler (merid a) (sym (merid north)) k i ∣ ⌣ₖ b)

assoc-helper : (n m : ℕ) (x : coHomK (suc n)) (y : coHomK (suc m))
             → Kn→ΩKn+1 _ (x ⌣ₖ y) ≡ λ i → (Kn→ΩKn+1 _ x i) ⌣ₖ y
assoc-helper n m x y = funExt⁻ (cong fst (assocer-helpFun≡ n m x)) y

assoc-⌣ₖ· : (n m k : ℕ) → (x : coHomK (suc n)) → assocer n m k x ≡ assocer2 n m k x
assoc-⌣ₖ· n m k =
  trElim (λ _ → isOfHLevelPath (3 + n)
            (transport (λ i → isOfHLevel (3 + n)
                (coHomK-ptd (suc m) →∙ (coHomK-ptd (suc k) →∙ coHomK-ptd (h (~ i)) ∙)))
              (isOfHLevel↑∙∙ m k (suc n))) _ _)
         λ a → →∙Homogeneous≡ (isHomogeneous→∙ (isHomogeneousKn _))
           (funExt λ b → →∙Homogeneous≡ (isHomogeneousKn _)
             (funExt (main n m k a b)))
  where

  h : (suc n) +' ((suc m) +' (suc k)) ≡ suc (suc (suc n + m + k))
  h = cong (2 +_) (+-suc n (m + k)) ∙ λ i → suc (suc (suc (+-assoc n m k i)))

  main : (n m k : ℕ) (a : S₊ (suc n)) (b : coHomK (suc m)) (c : coHomK (suc k))
    → ∣ a ∣ ⌣ₖ b ⌣ₖ c ≡
      (subst coHomK (λ i → +'-assoc (suc n) (suc m) (suc k) (~ i))
        ((∣ a ∣ ⌣ₖ b) ⌣ₖ c))
  main zero m k a b c = goal a ∙ sym (funExt⁻ t ((∣ a ∣ ⌣ₖ b) ⌣ₖ c))
    where
    t : subst coHomK (λ i → +'-assoc 1 (suc m) (suc k) (~ i)) ≡ idfun _
    t = cong (subst coHomK) (isSetℕ _ _ (+'-assoc 1 (suc m) (suc k)) refl) ∙ funExt transportRefl
    goal : (a : _) → ∣ a ∣ ⌣ₖ b ⌣ₖ c ≡ (∣ a ∣ ⌣ₖ b) ⌣ₖ c
    goal base = refl
    goal (loop i) j = assoc-helper m k b c j i
  main (suc n) m k north b c = refl
  main (suc n) m k south b c = refl
  main (suc n) m k (merid a i) b c j = help2 j i
    where
      transpLem : (n m : ℕ) (p : n ≡ m) → subst coHomK p (0ₖ _) ≡ 0ₖ _
      transpLem zero m = J (λ m p → subst coHomK p (0ₖ _) ≡ 0ₖ _) refl
      transpLem (suc zero) m = J (λ m p → subst coHomK p (0ₖ _) ≡ 0ₖ _) refl
      transpLem (suc (suc n)) m = J (λ m p → subst coHomK p (0ₖ _) ≡ 0ₖ _) refl

      transpLem-refl : transpLem (suc (suc (suc (suc (n + m + k)))))
                                    (suc (suc n +' (suc m +' suc k)))
                                    (λ i₃ → +'-assoc (2 + n) (suc m) (suc k) (~ i₃)) ≡ refl
      transpLem-refl = transportRefl refl
      moveTransports : (n m : ℕ) (x : coHomK n) (p : n ≡ m) (q : (suc n) ≡ suc m)
                    → PathP (λ i → transpLem _ _ q (~ i) ≡ transpLem _ _ q (~ i))
                            (Kn→ΩKn+1 _ (subst coHomK p x))
                            (cong (subst coHomK q) (Kn→ΩKn+1 _ x))
      moveTransports n m x =
        J (λ m p → (q : (suc n) ≡ suc m)
                    → PathP (λ i → transpLem _ _ q (~ i) ≡ transpLem _ _ q (~ i))
                            (Kn→ΩKn+1 _ (subst coHomK p x))
                            (cong (subst coHomK q) (Kn→ΩKn+1 _ x)))
          λ q → transport (λ j → PathP (λ i → transpLem (suc n) (suc n) (isSetℕ _ _ refl q j) (~ i)
                                              ≡ transpLem (suc n) (suc n) (isSetℕ _ _ refl q j) (~ i))
                           (Kn→ΩKn+1 _ (subst coHomK refl x))
                           (cong (subst coHomK (isSetℕ _ _ refl q j)) (Kn→ΩKn+1 _ x)))
                 (h2 n x)
        where
        h2 : (n : ℕ) (x : _)
         → PathP  (λ i₁ →
         transpLem (suc n) (suc n) (λ _ → suc n) (~ i₁) ≡
         transpLem (suc n) (suc n) (λ _ → suc n) (~ i₁))
         (Kn→ΩKn+1 n (subst coHomK (λ _ → n) x))
         (λ i₁ → subst coHomK (λ _ → suc n) (Kn→ΩKn+1 n x i₁))
        h2 zero x k i =
          hcomp (λ j → λ {(i = i0) → transportRefl (refl {x = 0ₖ _}) (~ j) k
                         ; (i = i1) → transportRefl (refl {x = 0ₖ _}) (~ j) k
                         ; (k = i0) → Kn→ΩKn+1 _ (transportRefl x j) i
                         ; (k = i1) → transportRefl (Kn→ΩKn+1 _ x i) (~ j)})
                 (Kn→ΩKn+1 _ x i)
        h2 (suc n) x k i =
          hcomp (λ j → λ {(i = i0) → transportRefl (refl {x = 0ₖ _}) (~ j) k
                         ; (i = i1) → transportRefl (refl {x = 0ₖ _}) (~ j) k
                         ; (k = i0) → Kn→ΩKn+1 _ (transport refl x) i
                         ; (k = i1) → transportRefl (Kn→ΩKn+1 _ x i) (~ j)})
                 (Kn→ΩKn+1 _ (transportRefl x k) i)

      finalTransp : (n : ℕ) (a : _) → Kn→ΩKn+1 _ (subst coHomK (λ i₁ → +'-assoc (suc n) (suc m) (suc k) (~ i₁)) ((∣ a ∣ ⌣ₖ b) ⌣ₖ c))
                  ≡ cong (subst coHomK (λ i₁ → +'-assoc (2 + n) (suc m) (suc k) (~ i₁))) (Kn→ΩKn+1 _ ((∣ a ∣ ⌣ₖ b) ⌣ₖ c))
      finalTransp n a =
           rUnit _
        ∙∙ (λ i → (λ j → transpLem (suc (suc (suc (suc (n + m + k)))))
                          (suc (suc n +' (suc m +' suc k)))
                          (λ i₃ → +'-assoc (2 + n) (suc m) (suc k) (~ i₃)) (i ∧ j))
                ∙∙ moveTransports _ _ ((∣ a ∣ ⌣ₖ b) ⌣ₖ c)
                     (sym (+'-assoc (suc n) (suc m) (suc k)))
                     (sym (+'-assoc (2 + n) (suc m) (suc k))) i
                ∙∙ λ j → transpLem (suc (suc (suc (suc (n + m + k)))))
                                    (suc (suc n +' (suc m +' suc k)))
                                    (λ i₃ → +'-assoc (2 + n) (suc m) (suc k) (~ i₃)) (i ∧ ~ j))
        ∙∙ (λ i → transportRefl refl i
                ∙∙ cong (subst coHomK (λ i₁ → +'-assoc (2 + n) (suc m) (suc k) (~ i₁))) (Kn→ΩKn+1 _ ((∣ a ∣ ⌣ₖ b) ⌣ₖ c))
                ∙∙ transportRefl refl i)
         ∙ sym (rUnit _)

      help2 : cong (λ x → (∣ x ∣) ⌣ₖ (b ⌣ₖ c)) (merid a) ≡ cong (assoc2-sub (2 + n) (suc m) (suc k)) (cong (λ x → (∣ x ∣ ⌣ₖ b) ⌣ₖ c) (merid a))
      help2 = ((λ r → Kn→ΩKn+1 _ (main n m k a b c r)))
            ∙∙ finalTransp n a
            ∙∙ λ r i → subst coHomK (sym (+'-assoc (2 + n) (suc m) (suc k))) (assoc-helper _ _ (∣ a ∣ ⌣ₖ b) c r i)

-- Some key distributivity lemmas
-Distₗ : (n m : ℕ) (x : coHomK n) (y : coHomK m) → (-ₖ (x ⌣ₖ y)) ≡ (-ₖ x) ⌣ₖ y
-Distₗ n m x y =
       sym (rUnitₖ _ (-ₖ (x ⌣ₖ y)))
    ∙∙ cong ((-ₖ (x ⌣ₖ y)) +ₖ_) (sym (rCancelₖ _ (x ⌣ₖ y)))
    ∙∙ assocₖ _ (-ₖ (x ⌣ₖ y)) (x ⌣ₖ y) (-ₖ (x ⌣ₖ y))
    ∙∙ cong (_-ₖ (x ⌣ₖ y)) help
    ∙∙ sym (assocₖ _ ((-ₖ x) ⌣ₖ y) (x ⌣ₖ y) (-ₖ (x ⌣ₖ y)))
    ∙∙ cong ((-ₖ x) ⌣ₖ y +ₖ_) (rCancelₖ _ (x ⌣ₖ y))
    ∙∙ rUnitₖ _ ((-ₖ x) ⌣ₖ y)
  where
  help : (-ₖ (x ⌣ₖ y)) +ₖ (x ⌣ₖ y) ≡ (-ₖ x) ⌣ₖ y +ₖ (x ⌣ₖ y)
  help = lCancelₖ _ _
      ∙∙ sym (0ₖ-⌣ₖ _ _ y)
       ∙ cong (_⌣ₖ y) (sym (lCancelₖ _ x))
      ∙∙ rightDistr-⌣ₖ _ _ (-ₖ x) x y

-Distᵣ : (n m : ℕ) (x : coHomK n) (y : coHomK m) → (-ₖ (x ⌣ₖ y)) ≡ x ⌣ₖ (-ₖ y)
-Distᵣ n m x y =
  sym (rUnitₖ _ (-ₖ (x ⌣ₖ y)))
    ∙∙ cong ((-ₖ (x ⌣ₖ y)) +ₖ_) (sym (rCancelₖ _ (x ⌣ₖ y)))
    ∙∙ assocₖ _ (-ₖ (x ⌣ₖ y)) (x ⌣ₖ y) (-ₖ (x ⌣ₖ y))
    ∙∙ cong (_-ₖ (x ⌣ₖ y)) help
    ∙∙ sym (assocₖ _ (x ⌣ₖ (-ₖ y)) (x ⌣ₖ y) (-ₖ (x ⌣ₖ y)))
    ∙∙ cong (x ⌣ₖ (-ₖ y) +ₖ_) (rCancelₖ _ (x ⌣ₖ y))
    ∙∙ rUnitₖ _ (x ⌣ₖ (-ₖ y))
  where
  help : (-ₖ (x ⌣ₖ y)) +ₖ (x ⌣ₖ y) ≡ x ⌣ₖ (-ₖ y) +ₖ (x ⌣ₖ y)
  help = lCancelₖ _ _
      ∙∙ sym (⌣ₖ-0ₖ _ _ x)
      ∙∙ cong (x ⌣ₖ_) (sym (lCancelₖ _ y))
       ∙ leftDistr-⌣ₖ _ _ x (-ₖ y) y

assoc₀ : (m k : ℕ) (x : ℤ) (y : coHomK m) (z : coHomK k) → _⌣ₖ_{n = zero} x (y ⌣ₖ z) ≡ (_⌣ₖ_{n = zero} {m = m} x y) ⌣ₖ z
assoc₀ m k x y z = main x
  where
  h : subst coHomK (sym (+'-assoc zero m k)) ≡ idfun _
  h = cong (subst coHomK) (isSetℕ _ _ _ refl) ∙ funExt transportRefl
  mainPos : (x : ℕ) → _⌣ₖ_ {n = zero} (pos x) (y ⌣ₖ z) ≡ ((_⌣ₖ_ {n = zero} {m = m} (pos x) y) ⌣ₖ z)
  mainPos zero = sym (0ₖ-⌣ₖ _ _ z) ∙ cong (_⌣ₖ z) (sym (0ₖ-⌣ₖ _ _ y))
  mainPos (suc n) =
      cong (y ⌣ₖ z +ₖ_) (mainPos n)
    ∙∙ sym (rightDistr-⌣ₖ _ _ y (_⌣ₖ_ {n = zero} {m = m} (pos n) y) z)
    ∙∙ (λ i → (y +ₖ (_⌣ₖ_ {n = zero} {m = m} (pos n) y)) ⌣ₖ z)

  main : (x : ℤ) → x ⌣ₖ y ⌣ₖ z ≡ ((_⌣ₖ_ {n = zero} {m = m} x y) ⌣ₖ z)
  main (pos n) = mainPos n
  main (negsuc n) =
       (λ i → _⌣ₖ_ {n = zero} (+ℤ-comm (negsuc n) 0 i) (y ⌣ₖ z))
    ∙∙ sym (-Distₗ zero _ (pos (suc n)) (y ⌣ₖ z))
     ∙ cong (-ₖ_) (mainPos (suc n))
    ∙∙ -Distₗ _ _ (pos (suc n) ⌣ₖ y) z
    ∙∙ cong (_⌣ₖ z) ((-Distₗ zero _ (pos (suc n)) y))
    ∙∙ λ i → (_⌣ₖ_ {n = zero} (+ℤ-comm (negsuc n) 0 (~ i)) y) ⌣ₖ z

assoc-⌣ₖ : (n m k : ℕ) (x : coHomK n) (y : coHomK m) (z : coHomK k)
  → x ⌣ₖ y ⌣ₖ z ≡ subst coHomK (sym (+'-assoc n m k)) ((x ⌣ₖ y) ⌣ₖ z)
assoc-⌣ₖ zero m k x y z = assoc₀ _ _ x y z ∙ sym (funExt⁻ h ((x ⌣ₖ y) ⌣ₖ z))
  where
  h : subst coHomK (sym (+'-assoc zero m k)) ≡ idfun _
  h = cong (subst coHomK) (isSetℕ _ _ _ refl) ∙ funExt transportRefl

assoc-⌣ₖ (suc n) zero k x y z =
     help y
  ∙∙ sym (transportRefl ((x ⌣ₖ y) ⌣ₖ z))
  ∙∙ λ i → transport (λ j → coHomK ((isSetℕ _ _ ((sym (+'-assoc (suc n) zero k))) refl (~ i) j)))
       ((_⌣ₖ_ {m = zero} x y) ⌣ₖ z)
  where
  helpPos : (y : ℕ) → x ⌣ₖ (_⌣ₖ_ {n = zero} (pos y) z) ≡
      ((_⌣ₖ_ {m = zero} x (pos y)) ⌣ₖ z)
  helpPos zero =
    (⌣ₖ-0ₖ _ _ x)
     ∙∙ (sym (0ₖ-⌣ₖ _ _ z))
     ∙∙ cong (_⌣ₖ z) (sym (⌣ₖ-0ₖ _ _ x))
  helpPos (suc y) =
    leftDistr-⌣ₖ _ _ x z (_⌣ₖ_{n = zero} (pos y) z)
    ∙∙ cong ((x ⌣ₖ z) +ₖ_) (helpPos y)
    ∙∙ sym (rightDistr-⌣ₖ _ _ x (_⌣ₖ_{n = zero} (pos y) x) z)

  help : (y : ℤ) → x ⌣ₖ (_⌣ₖ_ {n = zero} y z) ≡
      ((_⌣ₖ_ {m = zero} x y) ⌣ₖ z)
  help (pos n) = helpPos n
  help (negsuc n) =
       (λ i → x ⌣ₖ (_⌣ₖ_ {n = zero} (+ℤ-comm (negsuc n) 0 i) z))
    ∙∙ cong (x ⌣ₖ_) (sym (-Distₗ zero _ (pos (suc n)) z))
    ∙∙ sym (-Distᵣ _ _ x _)
    ∙∙ cong -ₖ_ (helpPos (suc n))
    ∙∙ -Distₗ _ _ _ z
    ∙∙ cong (_⌣ₖ z) (-Distᵣ _ zero x (pos (suc n)))
    ∙∙ λ i → (_⌣ₖ_ {m = zero} x (+ℤ-comm (negsuc n) 0 (~ i))) ⌣ₖ z
assoc-⌣ₖ (suc n) (suc m) zero x y z =
    (assoc-⌣ₖ (suc n) zero (suc m) x z y)
  ∙∙ cong (subst coHomK (sym (+'-assoc (suc n) zero (suc m))))
     (sym (assoc₀ _ _ z x y))
  ∙∙ (funExt⁻ (sym h) (_⌣ₖ_ {n = zero} z (x ⌣ₖ y)))
  where
  h : subst coHomK (sym (+'-assoc (suc n) (suc m) zero))
    ≡ subst coHomK (λ i → +'-assoc (suc n) zero (suc m) (~ i))
  h = cong (subst coHomK) (isSetℕ _ _ _ _)
assoc-⌣ₖ (suc n) (suc m) (suc k) x y z =
  funExt⁻ (cong fst (funExt⁻ (cong fst (assoc-⌣ₖ· n m k x)) y)) z

-- Ring laws for ⌣
module _ {A : Type ℓ} (n m : ℕ) where
  ⌣-0ₕ : (f : coHom n A) → (f ⌣ 0ₕ m) ≡ 0ₕ _
  ⌣-0ₕ = sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
                λ f → cong ∣_∣₂ (funExt λ x → ⌣ₖ-0ₖ n m (f x))

  0ₕ-⌣ : (f : coHom m A) → (0ₕ n ⌣ f) ≡ 0ₕ _
  0ₕ-⌣ = sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
                λ f → cong ∣_∣₂ (funExt λ x → 0ₖ-⌣ₖ n m (f x))

  leftDistr-⌣ : (f : coHom n A) (g h : coHom m A)
              → f ⌣ (g +ₕ h) ≡ f ⌣ g +ₕ f ⌣ h
  leftDistr-⌣ =
    sElim (λ _ → isSetΠ2 λ _ _ → isOfHLevelPath 2 squash₂ _ _)
      λ f → sElim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
        λ g h → cong ∣_∣₂ (funExt λ x → leftDistr-⌣ₖ n m (f x) (g x) (h x))

  rightDistr-⌣ : (g h : coHom n A) (f : coHom m A) → (g +ₕ h) ⌣ f ≡ g ⌣ f +ₕ h ⌣ f
  rightDistr-⌣ =
    sElim2 (λ _ _ → isSetΠ (λ _ → isOfHLevelPath 2 squash₂ _ _))
      λ g h → sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
        λ f → cong ∣_∣₂ (funExt λ x → rightDistr-⌣ₖ n m (g x) (h x) (f x))

  assoc-⌣ : (l : ℕ) (f : coHom n A) (g : coHom m A) (h : coHom l A)
          → f ⌣ g ⌣ h ≡ subst (λ x → coHom x A) (sym (+'-assoc n m l)) ((f ⌣ g) ⌣ h)
  assoc-⌣ l =
    sElim (λ _ → isSetΠ2 λ _ _ → isOfHLevelPath 2 squash₂ _ _)
      λ f → sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 squash₂ _ _)
        λ g → sElim (λ _ → isOfHLevelPath 2 squash₂ _ _) λ h →
          cong ∣_∣₂ ((funExt (λ x → assoc-⌣ₖ n m l (f x) (g x) (h x)
                   ∙ cong (subst coHomK (sym (+'-assoc n m l)))
                     λ i → (f (transportRefl x (~ i)) ⌣ₖ g (transportRefl x (~ i)))
                         ⌣ₖ (h (transportRefl x (~ i))))))

-- Additive unit(s)
0⌣ :  ∀ {ℓ} {A : Type ℓ} (n m : ℕ) (x : coHom n A)
     → x ⌣ (0ₕ m) ≡ 0ₕ _
0⌣ n m = sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
                λ f → cong ∣_∣₂ (funExt λ x → ⌣ₖ-0ₖ n m (f x))

⌣0 :  ∀ {ℓ} {A : Type ℓ} (n m : ℕ) (x : coHom n A)
     → (0ₕ m) ⌣ x ≡ 0ₕ _
⌣0 n m = sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
                λ f → cong ∣_∣₂ (funExt λ x → 0ₖ-⌣ₖ m n (f x))

-- Multiplicative unit
1⌣ : ∀ {ℓ} {A : Type ℓ} → coHom 0 A
1⌣ = ∣ (λ _ → 1) ∣₂

private
  n+'0 : (n : ℕ) → n +' 0 ≡ n
  n+'0 zero = refl
  n+'0 (suc n) = refl

lUnit⌣ₖ : (n : ℕ) (x : coHomK n) → _⌣ₖ_ {n = 0} (pos 1) x ≡ x
lUnit⌣ₖ zero = λ _ → refl
lUnit⌣ₖ (suc n) x = rUnitₖ _ x

lUnit⌣ : ∀ {ℓ} {A : Type ℓ} (n : ℕ) (x : coHom n A)
  → x ⌣ 1⌣ ≡ subst (λ n → coHom n A) (sym (n+'0 n)) x
lUnit⌣ zero = sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
  λ f → cong ∣_∣₂ (funExt (λ x → comm-·₀ (f x) (pos 1))) ∙ sym (transportRefl ∣ f ∣₂)
lUnit⌣ (suc n) =
  sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
  λ f → cong ∣_∣₂ (funExt (λ x → cong (f x +ₖ_) (0ₖ-⌣ₖ zero _ (f x)) ∙ rUnitₖ _ (f x)))
       ∙ sym (transportRefl ∣ f ∣₂)

rUnit⌣ : ∀ {ℓ} {A : Type ℓ} (n : ℕ) (x : coHom n A)
       → 1⌣ ⌣ x ≡ x
rUnit⌣ zero = sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
               λ f → refl
rUnit⌣ (suc n) =
  sElim (λ _ → isOfHLevelPath 2 squash₂ _ _)
               λ f → cong ∣_∣₂ (funExt λ x → rUnitₖ _ (f x))

-ₕDistᵣ : ∀ {ℓ} {A : Type ℓ} (n m : ℕ)
  (x : coHom n A) (y : coHom m A) → (-ₕ (x ⌣ y)) ≡ x ⌣ (-ₕ y)
-ₕDistᵣ n m =
  sElim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
    λ f g → cong ∣_∣₂ (funExt λ x → -Distᵣ n m (f x) (g x))

-- TODO : Graded ring structure

max_stars_repo_name: ecavallo/cubical

max_issues_repo_name: ecavallo/cubical

max_forks_repo_name: ecavallo/cubical


text:
data Nat : Set where
  zero : Nat
  suc : Nat → Nat

interleaved mutual

  data Even : Nat → Set
  data Odd  : Nat → Set

  -- base cases: 0 is Even, 1 is Odd
  constructor
    even-zero : Even zero
    odd-one   : Odd (suc zero)

  -- step case: suc switches the even/odd-ness
  constructor
    even-suc : ∀ {n} → Odd n → Even (suc n)
    odd-suc  : ∀ {n} → Even n → Odd (suc n)

max_forks_repo_name: shlevy/agda


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

open import HoTT
open import homotopy.Bouquet
open import homotopy.PushoutSplit
open import homotopy.DisjointlyPointedSet
open import cw.CW

module cw.WedgeOfCells {i} {n} (skel : Skeleton {i} (S n)) where

Xₙ/Xₙ₋₁ : Type i
Xₙ/Xₙ₋₁ = Cofiber (cw-incl-last skel)

⊙Xₙ/Xₙ₋₁ : Ptd i
⊙Xₙ/Xₙ₋₁ = ⊙[ Xₙ/Xₙ₋₁ , cfbase ]

private
  cells : Type i
  cells = cells-last skel

  attaching : cells → (Sphere n → ⟦ skel ⟧₋₁)
  attaching = attaching-last skel

  {- this is also a cofiber -}
  BigWedgeSusp : Type i
  BigWedgeSusp = Attached {A = ⊤} {B = cells} {C = Sphere n} (λ _ _ → unit)

  ⊙BigWedgeSusp : Ptd i
  ⊙BigWedgeSusp = ⊙[ BigWedgeSusp , cfbase ]

private
  module SphereToBigWedgeSusp (a : cells) = SuspRec {A = Sphere n}
    (cfbase :> BigWedgeSusp) (cfcod a) (λ s → cfglue (a , s))

  module BouquetToBigWedgeSusp =
    BigWedgeRec {A = cells} {X = Bouquet-family cells (S n)}
    cfbase SphereToBigWedgeSusp.f (λ _ → idp)

  module BigWedgeSuspEquivQuotient = PushoutLSplit (uncurry attaching) (λ _ → unit) fst

Bouquet-to-Xₙ/Xₙ₋₁ : Bouquet cells (S n) → Xₙ/Xₙ₋₁
Bouquet-to-Xₙ/Xₙ₋₁ = BigWedgeSuspEquivQuotient.split ∘ BouquetToBigWedgeSusp.f

abstract
  Bouquet-to-Xₙ/Xₙ₋₁-in-merid-β : ∀ (a : cells) x
    → ap (Bouquet-to-Xₙ/Xₙ₋₁ ∘ bwin a) (merid x)
    == cfglue (attaching a x) ∙' ap cfcod (spoke a x)
  Bouquet-to-Xₙ/Xₙ₋₁-in-merid-β a x =
      ap-∘ BigWedgeSuspEquivQuotient.split (SphereToBigWedgeSusp.f a) (merid x)
    ∙ ap (ap BigWedgeSuspEquivQuotient.split) (SphereToBigWedgeSusp.merid-β a x)
    ∙ BigWedgeSuspEquivQuotient.split-glue-β (a , x)

private
  Bouquet-to-BigWedgeSusp-is-equiv : is-equiv BouquetToBigWedgeSusp.f
  Bouquet-to-BigWedgeSusp-is-equiv = is-eq to from to-from from-to
    where
    to = BouquetToBigWedgeSusp.f

    module From = AttachedRec {A = ⊤}
      (λ _ → bwbase :> Bouquet cells (S n))
      (λ a → bwin a south) (λ a s → bwglue a ∙ ap (bwin a) (merid s))
    from = From.f

    abstract
      from-to : ∀ b → from (to b) == b
      from-to = BigWedge-elim
        idp
        (λ a → Susp-elim (bwglue a) idp
          (λ s → ↓-='-from-square $
            ( ap-∘ from (SphereToBigWedgeSusp.f a) (merid s)
            ∙ ap (ap from) (SphereToBigWedgeSusp.merid-β a s)
            ∙ From.spoke-β a s)
            ∙v⊡ (tl-square (bwglue a) ⊡h vid-square)))
        (λ a → ↓-∘=idf-from-square from to $
          ap (ap from) (BouquetToBigWedgeSusp.glue-β a) ∙v⊡ br-square (bwglue a))

      to-from : ∀ c → to (from c) == c
      to-from = Attached-elim
        (λ _ → idp) (λ a → idp)
        (λ a s → ↓-∘=idf-in' to from $
            ap (ap to) (From.spoke-β a s)
          ∙ ap-∙ to (bwglue a) (ap (bwin a) (merid s))
          ∙ ap2 _∙_ (BouquetToBigWedgeSusp.glue-β a)
                    ( ∘-ap to (bwin a) (merid s)
                    ∙ SphereToBigWedgeSusp.merid-β a s))

  Bouquet-equiv-BigWedgeSusp : Bouquet cells (S n) ≃ BigWedgeSusp
  Bouquet-equiv-BigWedgeSusp = BouquetToBigWedgeSusp.f , Bouquet-to-BigWedgeSusp-is-equiv

Bouquet-equiv-Xₙ/Xₙ₋₁ : Bouquet cells (S n) ≃ Xₙ/Xₙ₋₁
Bouquet-equiv-Xₙ/Xₙ₋₁ = BigWedgeSuspEquivQuotient.split-equiv ∘e Bouquet-equiv-BigWedgeSusp

Bouquet-⊙equiv-Xₙ/Xₙ₋₁ : ⊙Bouquet cells (S n) ⊙≃ ⊙Xₙ/Xₙ₋₁
Bouquet-⊙equiv-Xₙ/Xₙ₋₁ = ≃-to-⊙≃ Bouquet-equiv-Xₙ/Xₙ₋₁ idp


text:
{-# OPTIONS --without-K #-}
module hott.level.closure where

open import hott.level.closure.core public
open import hott.level.closure.lift public
open import hott.level.closure.extra public

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: HoTT/M-types


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Refinement type: a value together with an erased proof.
------------------------------------------------------------------------

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

module Data.Refinement where

open import Level
open import Data.Erased as Erased using (Erased)
open import Function.Base
open import Relation.Unary

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

record Refinement {a p} (A : Set a) (P : A → Set p) : Set (a ⊔ p) where
  constructor _,_
  field value : A
        proof : Erased (P value)
open Refinement public

-- The syntax declaration below is meant to mimick set comprehension.
-- It is attached to Refinement-syntax, to make it easy to import
-- Data.Refinement without the special syntax.

infix 2 Refinement-syntax
Refinement-syntax = Refinement
syntax Refinement-syntax A (λ x → P) = [ x ∈ A ∣ P ]

module _ {P : A → Set p} {Q : B → Set q} where

  map : (f : A → B) → ∀[ P ⇒ f ⊢ Q ] →
        [ a ∈ A ∣ P a ] → [ b ∈ B ∣ Q b ]
  map f prf (a , p) = f a , Erased.map prf p

module _ {P : A → Set p} {Q : A → Set q} where

  refine : ∀[ P ⇒ Q ] → [ a ∈ A ∣ P a ] → [ a ∈ A ∣ Q a ]
  refine = map id


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.Prelude
open import LibraBFT.Impl.Consensus.Types

-- This module defines the LBFT monad used by our (fake/simple,
-- for now) "implementation", along with some utility functions
-- to facilitate reasoning about it.

module LibraBFT.Impl.Util.Util where
  open import Optics.All
  open import LibraBFT.Impl.Util.RWST ℓ-RoundManager public
  ----------------
  -- LBFT Monad --
  ----------------

  -- Global 'LBFT'; works over the whole state.
  LBFT : Set → Set
  LBFT = RWST Unit Output RoundManager

  LBFT-run : ∀ {A} → LBFT A → RoundManager → (A × RoundManager × List Output)
  LBFT-run m = RWST-run m unit

  LBFT-post : ∀ {A} → LBFT A → RoundManager → RoundManager
  LBFT-post m rm = proj₁ (proj₂ (LBFT-run m rm))

  LBFT-outs : ∀ {A} → LBFT A → RoundManager → List Output
  LBFT-outs m rm = proj₂ (proj₂ (LBFT-run m rm))

  -- Local 'LBFT' monad; which operates only over the part of
  -- the state that /depends/ on the ec; not the part
  -- of the state that /defines/ the ec.
  --
  -- This is very convenient to define functions that
  -- do not alter the ec.

  LBFT-ec : EpochConfig → Set → Set
  LBFT-ec ec = RWST Unit Output (RoundManagerWithEC ec)

  -- Lifting a function that does not alter the pieces that
  -- define the epoch config is easy
  liftEC : {A : Set}(f : ∀ ec → LBFT-ec ec A) → LBFT A
  liftEC f = rwst λ _ st
    → let ec                 = α-EC (₋rmEC st , ₋rmEC-correct st)
          res , stec' , acts = RWST-run (f ec) unit (₋rmWithEC st)
       in res , record st { ₋rmWithEC = stec' } , acts

  -- Type that captures a proof that a computation in the LBFT monad
  -- satisfies a given contract.
  LBFT-Contract : ∀{A} → LBFT A
                → (RoundManager → Set)
                → (RoundManager → Set)
                → Set
  LBFT-Contract f Pre Post =
    ∀ rm → Pre rm × Post (proj₁ (proj₂ (RWST-run f unit rm)))

  -- Because we made RWST work for different level State types, but broke use
  -- and modify' because Lens does not support different levels, we define use
  -- and modify' here for RoundManager.  This will work as long as we can keep
  -- RoundManager in Set.  If we ever need to make RoundManager at some higher
  -- Level, we will have to consider making Lens level-agnostic.  Preliminary
  -- exploration by @cwjnkins showed this to be somewhat painful in particular
  -- around composition, so we are not pursuing it for now.
  use : ∀ {A} → Lens RoundManager A → LBFT A
  use f = RWST-bind get (RWST-return ∘ (_^∙ f))

  modify' : ∀ {A} → Lens RoundManager A → A → LBFT Unit
  modify' l val = modify λ x → x [ l := val ]

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


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

module leibniz-equality where

open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Function
open import Cubical.Data.Equality

open import equalities
open import leibniz
open Leibniz

liftIso : ∀ {a b} {A : Type a} {B : Type b} → Iso {a} {b} A B → Iso {ℓ-max a b} {ℓ-max a b} A B
liftIso {a} f = iso fun inv (λ x i → rightInv x i) (λ x i → leftInv x i)
  where open Iso f

module FinalEquality {A : Set} where
  open MainResult A

  ≐≅≡ : ∀ {a b} → Iso (a ≐ b) (a ≡p b)
  ≐≅≡ = iso j i (ptoc ∘ ji) (ptoc ∘ ij)

  ≐≡≡' : ∀ {a b} → (a ≐ b) ≡c (a ≡p b)
  ≐≡≡' = let lifted = liftIso ≐≅≡  in isoToPath lifted

  ≐≡≡ : _≐_ {A} ≡c _≡p_
  ≐≡≡ i x y = ≐≡≡' {x} {y} i

  open IsEquality
  open equalities

  instance
    ≐-IsEquality : IsEquality {A = A} _≐_
    ≐-IsEquality = eq λ {x} {y} → ≐≡≡' ∙ λ i → ≡p-IsEquality {ℓ-zero} .≣-≡-≡ {x} {y} i

max_stars_repo_name: guilhermehas/Equality

max_issues_repo_name: guilhermehas/Equality

max_forks_repo_name: guilhermehas/Equality


text:
{-# OPTIONS --no-positivity-check #-}
module IIDr where

open import LF
open import IID

OPr : (I : Set) -> Set1
OPr I = I -> OP I One

rArgs : {I : Set}(γ : OPr I)(U : I -> Set)(i : I) -> Set
rArgs γ U i = Args (γ i) U

-- The type of IIDrs
data Ur {I : Set}(γ : OPr I)(i : I) : Set where
  intror : rArgs γ (Ur γ) i -> Ur γ i

-- The elimination rule
elim-Ur : {I : Set}(γ : OPr I)(C : (i : I) -> Ur γ i -> Set) ->
	  ((i : I)(a : rArgs γ (Ur γ) i) -> IndHyp (γ i) (Ur γ) C a -> C i (intror a)) ->
	  (i : I)(u : Ur γ i) -> C i u
elim-Ur γ C m i (intror a) = m i a (induction (γ i) (Ur γ) C (elim-Ur γ C m) a)

-- Large elimination
elim-Ur₁ : {I : Set}(γ : OPr I)(C : (i : I) -> Ur γ i -> Set1) ->
	   ((i : I)(a : rArgs γ (Ur γ) i) -> IndHyp₁ (γ i) (Ur γ) C a -> C i (intror a)) ->
	   (i : I)(u : Ur γ i) -> C i u
elim-Ur₁ γ C m i (intror a) = m i a (induction₁ (γ i) (Ur γ) C (elim-Ur₁ γ C m) a)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2019-01-20, re #2597.
-- Undocumented language change introduced by patch 31a5982f38 (released in 2.5.3):
-- Hiding of argument now treated as part of name when inserting implicits.

-- Patch introduced in src/full/Agda/TypeChecking/Implicit.hs
--
-- ... | x == y && sameHiding hidingx a = impInsert $ reverse hs
--     | x == y && sameHiding hidingx a = BadImplicits
--
-- Intended was most likely
--     | x == y && not (sameHiding hidingx a) = BadImplicits
--
-- The patch makes this code legal:

test : {{X : Set}} {X : Set} → Set
test {X = X} = X

-- Succeeds in 2.5.3.
-- Fails in 2.5.2 with error:
-- Unexpected implicit argument
-- when checking that the clause test {X = X} = X has type
-- {{X : Set}} {X = X₁ : Set} → Set


text:
{-# OPTIONS --without-K #-}
module NTypes.Coproduct where

open import NTypes
open import PathOperations
open import PathStructure.Coproduct
open import Types

⊎-isSet : ∀ {A : Set} {B : Set} →
  isSet A → isSet B → isSet (A ⊎ B)
⊎-isSet {A = A} {B = B} A-set B-set x y p q =
  case (λ x → (y : A ⊎ B) (p q : x ≡ y) → p ≡ q)
  (λ a y p q → case
    (λ y → (p q : inl a ≡ y) → p ≡ q)
    (λ a′ p q
      → split-eq p ⁻¹
      · ap (ap inl)
        (A-set _ _
          (lower (tr (F (inl a)) p (lift refl)))
          (lower (tr (F (inl a)) q (lift refl)))
        )
      · split-eq q
      )
    (λ _  p q → 0-elim
      (lower (split-path p)))
    y p q)
  (λ b y p q → case
    (λ y → (p q : inr b ≡ y) → p ≡ q)
    (λ _  p q → 0-elim
      (lower (split-path p)))
    (λ b′ p q
      → split-eq p ⁻¹
      · ap (ap inr)
        (B-set _ _
          (lower (tr (F (inr b)) p (lift refl)))
          (lower (tr (F (inr b)) q (lift refl)))
        )
      · split-eq q
      )
    y p q)
  x y p q
  where
  split-eq : {x y : A ⊎ B} → _
  split-eq {x = x} {y = y} =
    π₂ (π₂ (π₂ (split-merge-eq {x = x} {y = y})))

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
------------------------------------------------------------------------
-- Some results that could not be placed in Function-universe because
-- they make use of --sized-types
------------------------------------------------------------------------

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

open import Equality

module Function-universe.Size
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open Derived-definitions-and-properties eq

open import Prelude
open import Prelude.Size

import Bijection eq as B
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq

private
  variable
    S   : Size-universe
    p q : Level
    P   : S → Type p
    k   : Kind

-- Π-types with something from the size universe in the domain can be
-- expressed using something from Type in the domain.

Π-size-≃ :
  ((i : S) → P i) ≃
  ((i : S in-type) → P (size i))
Π-size-≃ = Eq.↔→≃
  (λ p i → p (size i))
  (λ p i → p (record { size = i }))
  refl
  refl

-- Implicit Π-types with something from the size universe in the
-- domain can be expressed using something from Type in the domain.

implicit-Π-size-≃ :
  ({i : S} → P i) ≃
  ({i : S in-type} → P (size i))
implicit-Π-size-≃ = Eq.↔→≃
  (λ p {i} → p {size i})
  (λ p {i} → p {record { size = i }})
  refl
  refl

-- Implicit Π-types with something from the size universe in the
-- domain are equivalent to explicit Π-types.

implicit-Π-size-≃-Π-size :
  ({i : S} → P i) ≃ ((i : S) → P i)
implicit-Π-size-≃-Π-size {P = P} =
  (∀ {i} → P i)         ↔⟨ implicit-Π-size-≃ ⟩
  (∀ {i} → P (size i))  ↔⟨ B.implicit-Π↔Π ⟩
  (∀ i → P (size i))    ↔⟨ inverse Π-size-≃ ⟩□
  (∀ i → P i)           □

-- A preservation lemma for Π-types with something from the size
-- universe in the domain.

∀-size-cong :
  {P : S → Type p} {Q : S → Type q} →
  Extensionality? k lzero (p ⊔ q) →
  (∀ i → P i ↝[ k ] Q i) →
  (∀ i → P i) ↝[ k ] (∀ i → Q i)
∀-size-cong {P = P} {Q = Q} ext P↝Q =
  (∀ i → P i)         ↔⟨ Π-size-≃ ⟩
  (∀ i → P (size i))  ↝⟨ ∀-cong ext (λ i → P↝Q (size i)) ⟩
  (∀ i → Q (size i))  ↔⟨ inverse Π-size-≃ ⟩□
  (∀ i → Q i)         □

-- A preservation lemma for implicit Π-types with something from the
-- size universe in the domain.

implicit-∀-size-cong :
  {P : S → Type p} {Q : S → Type q} →
  Extensionality? k lzero (p ⊔ q) →
  (∀ {i} → P (size i) ↝[ k ] Q (size i)) →
  (∀ {i} → P i) ↝[ k ] (∀ {i} → Q i)
implicit-∀-size-cong {P = P} {Q = Q} ext P↝Q =
  (∀ {i} → P i)         ↔⟨ implicit-Π-size-≃ ⟩
  (∀ {i} → P (size i))  ↝⟨ implicit-∀-cong ext P↝Q ⟩
  (∀ {i} → Q (size i))  ↔⟨ inverse implicit-Π-size-≃ ⟩□
  (∀ {i} → Q i)         □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality