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

   Copyright (c) 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.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
------------------------------------------------------------------------------
open import Data.String                         using (String)

module LibraBFT.Impl.IO.OBM.Messages where

record ECPWire : Set where
  constructor ECPWire∙new
  field
    --_ecpwWhy    : Text           -- for log visualization
    --_ecpwEpoch  : Epoch          -- for log visualization; epoch of sender
    --_ecpwRound  : Round          -- for log visualization; round of sender
    _ecpwECP      : EpochChangeProof
-- instance S.Serialize ECPWire

record EpRRqWire : Set where
  constructor EpRRqWire∙new
  field
    --_eprrqwWhy  : Text           -- for log visualization
    --_eprrqEpoch : Epoch          -- for log visualization; epoch of sender
    --_eprrqRound : Round          -- for log visualization; round of sender
    _eprrqEpRRq   : EpochRetrievalRequest
-- instance S.Serialize EpRRqWire

data Input : Set where
  IBlockRetrievalRequest    : Instant                  →          BlockRetrievalRequest  → Input
  IBlockRetrievalResponse   : Instant                  →          BlockRetrievalResponse → Input
  IEpochChangeProof         :           AccountAddress →          ECPWire                → Input
  IEpochRetrievalRequest    :           AccountAddress →          EpRRqWire              → Input
  IInit                     : Instant                                                    → Input
  IProposal                 : Instant → AccountAddress →          ProposalMsg            → Input
  IReconfigLocalEpochChange :                                   ReconfigEventEpochChange → Input
  ISyncInfo                 : Instant → AccountAddress →          SyncInfo               → Input
  ITimeout                  : Instant → String {-String is ThreadId-} → Epoch → Round    → Input
  IVote                     : Instant → AccountAddress →          VoteMsg                → Input


text:
------------------------------------------------------------------------------
-- Totality properties of the division
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module FOTC.Program.Division.TotalityATP where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.Inequalities
open import FOTC.Program.Division.Division
open import FOTC.Program.Division.Specification

------------------------------------------------------------------------------
-- The division is total when the dividend is less than the divisor.
postulate div-x<y-N : ∀ {i j} → i < j → N (div i j)
{-# ATP prove div-x<y-N #-}

-- The division is total when the dividend is greater or equal than
-- the divisor.

--  N (div (i ∸ j) j)       i ≮j → div i j ≡ succ (div (i ∸ j) j)
------------------------------------------------------------------
--                   N (div i j)

postulate div-x≮y-N : ∀ {i j} →
                      (divSpec (i ∸ j) j (div (i ∸ j) j)) →
                      i ≮ j →
                      N (div i j)
{-# ATP prove div-x≮y-N #-}

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module L0E where

open import Common

-- Syntax

data Conj : Set  where
  and or : Conj

data N : Set where
  Saddie Liz Hank : N

data Vᵢ : Set where
  snores sleeps is-boring : Vᵢ

data Vₜ : Set where
  loves hates is-taller-than : Vₜ

data Neg : Set where
  it-is-not-the-case-that : Neg

data VP : Set where
  iv : Vᵢ -> VP
  tv : Vₜ -> N -> VP

data S : Set where
 sconjs : S -> Conj -> S -> S
 negs : Neg -> S -> S
 predvp : N -> VP -> S

example1 : S
example1 = predvp Saddie (iv snores)

example2 : S
example2 = predvp Liz (iv sleeps)

example3 : S
example3 = negs it-is-not-the-case-that (predvp Hank (iv snores))

example41 example42 : S
example41 = sconjs (sconjs (predvp Saddie (iv sleeps)) or (predvp Liz (iv is-boring))) and (predvp Hank (iv snores))
example42 = sconjs (predvp Saddie (iv sleeps)) or (sconjs (predvp Liz (iv is-boring)) and (predvp Hank (iv snores)))

example5 : S
example5 = negs it-is-not-the-case-that (negs it-is-not-the-case-that (predvp Saddie (iv sleeps)))

-- Semantics

data Individual : Set where
  Anwar_Sadat : Individual
  Queen_Elizabeth_II : Individual
  Henry_Kissinger : Individual

⟦_⟧N : N -> Individual
⟦ Saddie ⟧N = Anwar_Sadat
⟦ Liz ⟧N = Queen_Elizabeth_II
⟦ Hank ⟧N = Henry_Kissinger

⟦_⟧̬̬̌Vᵢ : Vᵢ -> Individual -> Bool
⟦ snores ⟧̬̬̌Vᵢ Anwar_Sadat = true
⟦ snores ⟧̬̬̌Vᵢ Queen_Elizabeth_II = true
⟦ snores ⟧̬̬̌Vᵢ Henry_Kissinger = false

⟦ sleeps ⟧̬̬̌Vᵢ Anwar_Sadat = true
⟦ sleeps ⟧̬̬̌Vᵢ Queen_Elizabeth_II = false
⟦ sleeps ⟧̬̬̌Vᵢ Henry_Kissinger = false

⟦ is-boring ⟧̬̬̌Vᵢ Anwar_Sadat = true
⟦ is-boring ⟧̬̬̌Vᵢ Queen_Elizabeth_II = true
⟦ is-boring ⟧̬̬̌Vᵢ Henry_Kissinger = true

⟦_⟧Vₜ : Vₜ -> Individual -> Individual -> Bool
⟦ loves ⟧Vₜ Anwar_Sadat _ = true
⟦ loves ⟧Vₜ Queen_Elizabeth_II Anwar_Sadat = false
⟦ loves ⟧Vₜ Queen_Elizabeth_II Queen_Elizabeth_II = true
⟦ loves ⟧Vₜ Queen_Elizabeth_II Henry_Kissinger = false
⟦ loves ⟧Vₜ Henry_Kissinger Anwar_Sadat = true
⟦ loves ⟧Vₜ Henry_Kissinger Queen_Elizabeth_II = false
⟦ loves ⟧Vₜ Henry_Kissinger Henry_Kissinger = true

⟦ hates ⟧Vₜ Anwar_Sadat _ = false
⟦ hates ⟧Vₜ Queen_Elizabeth_II Anwar_Sadat = true
⟦ hates ⟧Vₜ Queen_Elizabeth_II Queen_Elizabeth_II = false
⟦ hates ⟧Vₜ Queen_Elizabeth_II Henry_Kissinger = true
⟦ hates ⟧Vₜ Henry_Kissinger Anwar_Sadat = false
⟦ hates ⟧Vₜ Henry_Kissinger Queen_Elizabeth_II = true
⟦ hates ⟧Vₜ Henry_Kissinger Henry_Kissinger = false

⟦ is-taller-than ⟧Vₜ Anwar_Sadat Anwar_Sadat = false
⟦ is-taller-than ⟧Vₜ Anwar_Sadat Queen_Elizabeth_II = true
⟦ is-taller-than ⟧Vₜ Anwar_Sadat Henry_Kissinger = false
⟦ is-taller-than ⟧Vₜ Queen_Elizabeth_II _ = false
⟦ is-taller-than ⟧Vₜ Henry_Kissinger Anwar_Sadat = true
⟦ is-taller-than ⟧Vₜ Henry_Kissinger Queen_Elizabeth_II = true
⟦ is-taller-than ⟧Vₜ Henry_Kissinger Henry_Kissinger = false

⟦_⟧VP : VP -> Individual -> Bool
⟦ iv v ⟧VP = ⟦ v ⟧̬̬̌Vᵢ
⟦ tv v n ⟧VP = ⟦ v ⟧Vₜ ⟦ n ⟧N

⟦_⟧S : S -> Bool
⟦ sconjs x and x₂ ⟧S = ⟦ x ⟧S && ⟦ x₂ ⟧S
⟦ sconjs x or x₂ ⟧S = ⟦ x ⟧S || ⟦ x₂ ⟧S
⟦ negs x x₁ ⟧S = neg ⟦ x₁ ⟧S
⟦ predvp x x₁ ⟧S = ⟦ x₁ ⟧VP ⟦ x ⟧N

max_stars_repo_name: daherb/Agda-Montague

max_issues_repo_name: daherb/Agda-Montague

max_forks_repo_name: daherb/Agda-Montague


text:
-- There was a problem with open public in parameterised modules.
module Issue165 where

postulate X : Set

module M where
  postulate P : Set

module R₀ (X : Set) where
  open M public

module R₁ (X : Set) where
  open R₀ X public

open R₁ X
postulate p : P

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- In this file we consider the special of localising at a single
-- element f : R (or rather the set of powers of f). This is also
-- known as inverting f.
-- We then prove that localising first at an element f and at an element
-- g (or rather the image g/1) is the same as localising at the product f·g
-- This fact has an important application in algebraic geometry where it's
-- used to define the structure sheaf of a commutative ring.

{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Localisation.InvertingElements where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.Transport
open import Cubical.Functions.FunExtEquiv

import Cubical.Data.Empty as ⊥
open import Cubical.Data.Bool
open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Vec
open import Cubical.Data.Sigma.Base
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Localisation.Base
open import Cubical.Algebra.CommRing.Localisation.UniversalProperty
open import Cubical.Algebra.RingSolver.ReflectionSolving

open import Cubical.HITs.SetQuotients as SQ
open import Cubical.HITs.PropositionalTruncation as PT

open Iso

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

module _(R' : CommRing ℓ) where
 open isMultClosedSubset
 private R = fst R'
 open CommRingStr (snd R')
 open Exponentiation R'

 [_ⁿ|n≥0] : R → ℙ R
 [ f ⁿ|n≥0] g = (∃[ n ∈ ℕ ] g ≡ f ^ n) , isPropPropTrunc
 -- Σ[ n ∈ ℕ ] (s ≡ f ^ n) × (∀ m → s ≡ f ^ m → n ≤ m) maybe better, this isProp:
 -- (n,s≡fⁿ,p) (m,s≡fᵐ,q) then n≤m by p and  m≤n by q => n≡m

 powersFormMultClosedSubset : (f : R) → isMultClosedSubset R' [ f ⁿ|n≥0]
 powersFormMultClosedSubset f .containsOne = PT.∣ zero , refl ∣
 powersFormMultClosedSubset f .multClosed =
             PT.map2 λ (m , p) (n , q) → (m +ℕ n) , (λ i → (p i) · (q i)) ∙ ·-of-^-is-^-of-+ f m n

 R[1/_] : R → Type ℓ
 R[1/ f ] = Loc.S⁻¹R R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)

 R[1/_]AsCommRing : R → CommRing ℓ
 R[1/ f ]AsCommRing = Loc.S⁻¹RAsCommRing R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)

 -- A useful lemma: (gⁿ/1)≡(g/1)ⁿ in R[1/f]
 ^-respects-/1 : {f g : R} (n : ℕ) → [ (g ^ n) , 1r , PT.∣ 0 , (λ _ → 1r) ∣ ] ≡
     Exponentiation._^_ R[1/ f ]AsCommRing [ g , 1r , powersFormMultClosedSubset _ .containsOne ] n
 ^-respects-/1 zero = refl
 ^-respects-/1 {f} {g} (suc n) = eq/ _ _ ( (1r , powersFormMultClosedSubset f .containsOne)
                                         , cong (1r · (g · (g ^ n)) ·_) (·Lid 1r))
                           ∙ cong (CommRingStr._·_ (R[1/ f ]AsCommRing .snd)
                           [ g , 1r , powersFormMultClosedSubset f .containsOne ]) (^-respects-/1 n)

 -- A slight improvement for eliminating into propositions
 InvElPropElim : {f : R} {P : R[1/ f ] → Type ℓ'}
               → (∀ x →  isProp (P x))
               → (∀ (r : R) (n : ℕ) → P [ r , (f ^ n) , PT.∣ n , refl ∣ ])    -- ∀ r n → P (r/fⁿ)
              ----------------------------------------------------------
               → (∀ x → P x)
 InvElPropElim {f = f} {P = P} PisProp base = elimProp (λ _ → PisProp _) []-case
  where
  S[f] = Loc.S R' [ f ⁿ|n≥0] (powersFormMultClosedSubset f)
  []-case : (a : R × S[f]) → P [ a ]
  []-case (r , s , s∈S[f]) = PT.rec (PisProp _) Σhelper s∈S[f]
   where
   Σhelper : Σ[ n ∈ ℕ ] s ≡ f ^ n → P [ r , s , s∈S[f] ]
   Σhelper (n , p) = subst P (cong [_] (≡-× refl (Σ≡Prop (λ _ → isPropPropTrunc) (sym p)))) (base r n)

 -- For predicates over the set of powers
 powersPropElim : {f : R} {P : R → Type ℓ'}
                → (∀ x →  isProp (P x))
                → (∀ n → P (f ^ n))
               ------------------------------
                → ∀ s → s ∈ [ f ⁿ|n≥0] → P s
 powersPropElim {f = f} {P = P} PisProp base s =
                PT.rec (PisProp s) λ (n , p) → subst P (sym p) (base n)

module DoubleLoc (R' : CommRing ℓ) (f g : (fst R')) where
 open isMultClosedSubset
 open CommRingStr (snd R')
 open CommRingTheory R'
 open Exponentiation R'
 open RingTheory (CommRing→Ring R')
 open CommRingStr (snd (R[1/_]AsCommRing R' f)) renaming ( _·_ to _·ᶠ_ ; 1r to 1ᶠ
                                                         ; _+_ to _+ᶠ_ ; 0r to 0ᶠ
                                                         ; ·Lid to ·ᶠ-lid ; ·Rid to ·ᶠ-rid
                                                         ; ·Assoc to ·ᶠ-assoc ; ·-comm to ·ᶠ-comm)
 open IsRingHom

 private
  R = fst R'
  R[1/f] = R[1/_] R' f
  R[1/f]AsCommRing = R[1/_]AsCommRing R' f
  R[1/fg] = R[1/_] R' (f · g)
  R[1/fg]AsCommRing = R[1/_]AsCommRing R' (f · g)
  R[1/f][1/g] = R[1/_] (R[1/_]AsCommRing R' f)
                                [ g , 1r , powersFormMultClosedSubset R' f .containsOne ]
  R[1/f][1/g]AsCommRing = R[1/_]AsCommRing (R[1/_]AsCommRing R' f)
                                [ g , 1r , powersFormMultClosedSubset R' f .containsOne ]
  R[1/f][1/g]ˣ = R[1/f][1/g]AsCommRing ˣ

 _/1/1 : R → R[1/f][1/g]
 r /1/1 = [ [ r , 1r , PT.∣ 0 , refl ∣ ] , 1ᶠ , PT.∣ 0 , refl ∣ ]

 /1/1AsCommRingHom : CommRingHom R' R[1/f][1/g]AsCommRing
 fst /1/1AsCommRingHom = _/1/1
 snd /1/1AsCommRingHom = makeIsRingHom refl lem+ lem·
   where
   lem+ : _
   lem+ r r' =
     cong [_]
       (≡-×
         (cong [_]
           (≡-×
             (cong₂ _+_
               (sym (·Rid _) ∙ (λ i → (·Rid r (~ i)) · (·Rid 1r (~ i))))
               (sym (·Rid _) ∙ (λ i → (·Rid r' (~ i)) · (·Rid 1r (~ i)))))
             (Σ≡Prop (λ _ → isPropPropTrunc)
               (sym (·Lid _) ∙ (λ i → (·Lid 1r (~ i)) · (·Lid 1r (~ i)))))))
         (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·ᶠ-lid 1ᶠ))))

   lem· : _
   lem· r r' =
     cong [_]
       (≡-×
         (cong [_] (≡-× refl (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·Lid _)))))
         (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·ᶠ-lid 1ᶠ))))

 -- this will give us a map R[1/fg] → R[1/f][1/g] by the universal property of localisation
 fⁿgⁿ/1/1∈R[1/f][1/g]ˣ : (s : R) → s ∈ ([_ⁿ|n≥0] R' (f · g)) → s /1/1 ∈ R[1/f][1/g]ˣ
 fⁿgⁿ/1/1∈R[1/f][1/g]ˣ = powersPropElim R' (λ s → R[1/f][1/g]ˣ (s /1/1) .snd) ℕcase
  where
  ℕcase : (n : ℕ) → ((f · g) ^ n) /1/1 ∈ R[1/f][1/g]ˣ
  ℕcase n = [ [ 1r , (f ^ n) , PT.∣ n , refl ∣ ]
            , [ (g ^ n) , 1r , PT.∣ 0 , refl ∣ ] --denominator
            , PT.∣ n , ^-respects-/1 _ n ∣ ]
            , eq/ _ _ ((1ᶠ , powersFormMultClosedSubset _ _ .containsOne)
            , eq/ _ _ ((1r , powersFormMultClosedSubset _ _ .containsOne) , path))
   where
   eq1 : ∀ x → 1r · (1r · (x · 1r) · 1r) · (1r · 1r · (1r · 1r)) ≡ x
   eq1 = solve R'

   eq2 : ∀ x y → x · y ≡ 1r · (1r · 1r · (1r · y)) · (1r · (1r · x) · 1r)
   eq2 = solve R'

   path : 1r · (1r · ((f · g) ^ n · 1r) · 1r) · (1r · 1r · (1r · 1r))
        ≡ 1r · (1r · 1r · (1r · g ^ n)) · (1r · (1r · f ^ n) · 1r)
   path = 1r · (1r · ((f · g) ^ n · 1r) · 1r) · (1r · 1r · (1r · 1r)) ≡⟨ eq1 ((f · g) ^ n) ⟩
          (f · g) ^ n                                                 ≡⟨ ^-ldist-· _ _ _ ⟩
          f ^ n · g ^ n                                               ≡⟨ eq2 (f ^ n) (g ^ n) ⟩
          1r · (1r · 1r · (1r · g ^ n)) · (1r · (1r · f ^ n) · 1r)    ∎

 -- the main result: localising at one element and then at another is
 -- the same as localising at the product.
 -- takes forever to compute without experimental lossy unification
 R[1/fg]≡R[1/f][1/g] : R[1/fg]AsCommRing ≡ R[1/f][1/g]AsCommRing
 R[1/fg]≡R[1/f][1/g] = S⁻¹RChar R' ([_ⁿ|n≥0] R' (f · g))
                         (powersFormMultClosedSubset R' (f · g)) _ /1/1AsCommRingHom pathtoR[1/fg]
  where
  open PathToS⁻¹R
  pathtoR[1/fg] : PathToS⁻¹R R' ([_ⁿ|n≥0] R' (f · g)) (powersFormMultClosedSubset R' (f · g))
                             R[1/f][1/g]AsCommRing /1/1AsCommRingHom
  φS⊆Aˣ pathtoR[1/fg] = fⁿgⁿ/1/1∈R[1/f][1/g]ˣ

  kerφ⊆annS pathtoR[1/fg] r p = toGoal helperR[1/f]
   where
   open RingTheory (CommRing→Ring R[1/f]AsCommRing) renaming ( 0RightAnnihilates to 0ᶠRightAnnihilates
                                                         ; 0LeftAnnihilates to 0ᶠ-leftNullifies)
   open Exponentiation R[1/f]AsCommRing renaming (_^_ to _^ᶠ_)
                                        hiding (·-of-^-is-^-of-+ ; ^-ldist-·)

   S[f] = Loc.S R' ([_ⁿ|n≥0] R' f) (powersFormMultClosedSubset R' f)
   S[fg] = Loc.S R' ([_ⁿ|n≥0] R' (f · g)) (powersFormMultClosedSubset R' (f · g))
   g/1 : R[1/_] R' f
   g/1 = [ g , 1r , powersFormMultClosedSubset R' f .containsOne ]
   S[g/1] = Loc.S R[1/f]AsCommRing
                  ([_ⁿ|n≥0] R[1/f]AsCommRing g/1)
                  (powersFormMultClosedSubset R[1/f]AsCommRing g/1)
   r/1 : R[1/_] R' f
   r/1 = [ r , 1r , powersFormMultClosedSubset R' f .containsOne ]

   -- this is the crucial step, modulo truncation we can take p to be generated
   -- by the quotienting relation of localisation. Note that we wouldn't be able
   -- to prove our goal if kerφ⊆annS was formulated with a Σ instead of a ∃
   ∥r/1,1/1≈0/1,1/1∥ : ∃[ u ∈ S[g/1] ] fst u ·ᶠ r/1 ·ᶠ 1ᶠ ≡ fst u ·ᶠ 0ᶠ ·ᶠ 1ᶠ
   ∥r/1,1/1≈0/1,1/1∥ = Iso.fun (SQ.isEquivRel→TruncIso (Loc.locIsEquivRel _ _ _) _ _) p

   helperR[1/f] : ∃[ n ∈ ℕ ] [ g ^ n · r , 1r , PT.∣ 0 , refl ∣ ] ≡ 0ᶠ
   helperR[1/f] = PT.rec isPropPropTrunc
                  (uncurry (uncurry (powersPropElim R[1/f]AsCommRing
                                    (λ _ → isPropΠ (λ _ → isPropPropTrunc)) baseCase)))
                  ∥r/1,1/1≈0/1,1/1∥
    where
    baseCase : ∀ n → g/1 ^ᶠ n ·ᶠ r/1 ·ᶠ 1ᶠ ≡ g/1 ^ᶠ n ·ᶠ 0ᶠ ·ᶠ 1ᶠ
                   → ∃[ n ∈ ℕ ] [ g ^ n · r , 1r , PT.∣ 0 , refl ∣ ] ≡ 0ᶠ
    baseCase n q = PT.∣ n , path ∣
     where
     path : [ g ^ n · r , 1r , PT.∣ 0 , refl ∣ ] ≡ 0ᶠ
     path = [ g ^ n · r , 1r , PT.∣ 0 , refl ∣ ]

          ≡⟨ cong [_] (≡-× refl (Σ≡Prop (λ _ → isPropPropTrunc) (sym (·Rid _)))) ⟩

            [ g ^ n , 1r , PT.∣ 0 , refl ∣ ] ·ᶠ r/1

          ≡⟨ cong (_·ᶠ r/1) (^-respects-/1 _ n) ⟩

            g/1 ^ᶠ n ·ᶠ r/1

          ≡⟨ sym (·ᶠ-rid _) ⟩

            g/1 ^ᶠ n ·ᶠ r/1 ·ᶠ 1ᶠ

          ≡⟨ q ⟩

            g/1 ^ᶠ n ·ᶠ 0ᶠ ·ᶠ 1ᶠ

          ≡⟨ cong (_·ᶠ 1ᶠ) (0ᶠRightAnnihilates _) ∙ 0ᶠ-leftNullifies 1ᶠ ⟩

            0ᶠ ∎

   toGoal : ∃[ n ∈ ℕ ] [ g ^ n · r , 1r , PT.∣ 0 , refl ∣ ] ≡ 0ᶠ
          → ∃[ u ∈ S[fg] ] fst u · r ≡ 0r
   toGoal = PT.rec isPropPropTrunc Σhelper
    where
    Σhelper : Σ[ n ∈ ℕ ] [ g ^ n · r , 1r , PT.∣ 0 , refl ∣ ] ≡ 0ᶠ
            → ∃[ u ∈ S[fg] ] fst u · r ≡ 0r
    Σhelper (n , q) = PT.map Σhelper2 helperR
     where
     -- now, repeat the above strategy with q
     ∥gⁿr≈0∥ : ∃[ u ∈ S[f] ] fst u · (g ^ n · r) · 1r ≡ fst u · 0r · 1r
     ∥gⁿr≈0∥ = Iso.fun (SQ.isEquivRel→TruncIso (Loc.locIsEquivRel _ _ _) _ _) q

     helperR : ∃[ m ∈ ℕ ] f ^ m · g ^ n · r ≡ 0r
     helperR = PT.rec isPropPropTrunc
               (uncurry (uncurry (powersPropElim R'
                                 (λ _ → isPropΠ (λ _ → isPropPropTrunc)) baseCase)))
               ∥gⁿr≈0∥
      where
      baseCase : (m : ℕ) → f ^ m · (g ^ n · r) · 1r ≡ f ^ m · 0r · 1r
               → ∃[ m ∈ ℕ ] f ^ m · g ^ n · r ≡ 0r
      baseCase m q' = PT.∣ m , path ∣
       where
       path : f ^ m · g ^ n · r ≡ 0r
       path = (λ i → ·Rid (·Assoc (f ^ m) (g ^ n) r (~ i)) (~ i))
            ∙∙ q' ∙∙ (λ i → ·Rid (0RightAnnihilates (f ^ m) i) i)

     Σhelper2 : Σ[ m ∈ ℕ ] f ^ m · g ^ n · r ≡ 0r
              → Σ[ u ∈ S[fg] ] fst u · r ≡ 0r
     Σhelper2 (m , q') = (((f · g) ^ l) , PT.∣ l , refl ∣) , path
      where
      l = max m n

      path : (f · g) ^ l · r ≡ 0r
      path = (f · g) ^ l · r

           ≡⟨ cong (_· r) (^-ldist-· _ _ _) ⟩

             f ^ l · g ^ l · r

           ≡⟨ cong₂ (λ x y → f ^ x · g ^ y · r) (sym (≤-∸-+-cancel {m = m} left-≤-max))
                                                (sym (≤-∸-+-cancel {m = n} right-≤-max)) ⟩

             f ^ (l ∸ m +ℕ m) · g ^ (l ∸ n +ℕ n) · r

           ≡⟨ cong₂ (λ x y → x · y · r) (sym (·-of-^-is-^-of-+ _ _ _))
                                        (sym (·-of-^-is-^-of-+ _ _ _)) ⟩

             f ^ (l ∸ m) · f ^ m · (g ^ (l ∸ n) · g ^ n) · r

           ≡⟨ cong (_· r) (·-commAssocSwap _ _ _ _) ⟩

             f ^ (l ∸ m) · g ^ (l ∸ n) · (f ^ m · g ^ n) · r

           ≡⟨ sym (·Assoc _ _ _) ⟩

             f ^ (l ∸ m) · g ^ (l ∸ n) · (f ^ m · g ^ n · r)

           ≡⟨ cong (f ^ (l ∸ m) · g ^ (l ∸ n) ·_) q' ⟩

             f ^ (l ∸ m) · g ^ (l ∸ n) · 0r

           ≡⟨ 0RightAnnihilates _ ⟩

             0r ∎

  surχ pathtoR[1/fg] = InvElPropElim _ (λ _ → isPropPropTrunc) toGoal
   where
   open Exponentiation R[1/f]AsCommRing renaming (_^_ to _^ᶠ_)
                                               hiding (·-of-^-is-^-of-+ ; ^-ldist-·)
   open CommRingStr (snd R[1/f][1/g]AsCommRing) renaming (_·_ to _·R[1/f][1/g]_)
                    hiding (1r ; ·Lid ; ·Rid ; ·Assoc)
   open Units R[1/f][1/g]AsCommRing
   g/1 : R[1/_] R' f
   g/1 = [ g , 1r , powersFormMultClosedSubset R' f .containsOne ]
   S[fg] = Loc.S R' ([_ⁿ|n≥0] R' (f · g)) (powersFormMultClosedSubset R' (f · g))

   baseCase : (r : R) (m n : ℕ) → ∃[ x ∈ R × S[fg] ] (x .fst /1/1)
       ≡ [ [ r , f ^ m , PT.∣ m , refl ∣ ]
         , [ g ^ n , 1r , PT.∣ 0 , refl ∣ ] , PT.∣ n , ^-respects-/1 _ n ∣ ]
       ·R[1/f][1/g] (x .snd .fst /1/1)
   baseCase r m n = PT.∣ ((r · f ^ (l ∸ m) · g ^ (l ∸ n)) -- x .fst
               , (f · g) ^ l , PT.∣ l , refl ∣)      -- x .snd
               , eq/ _ _ ((1ᶠ , PT.∣ 0 , refl ∣) , eq/ _ _ ((1r , PT.∣ 0 , refl ∣) , path)) ∣
               -- reduce equality of double fractions into equality in R
    where
    eq1 : ∀ r flm gln gn fm
        → 1r · (1r · (r · flm · gln) · (gn · 1r)) · (1r · (fm · 1r) · 1r)
        ≡ r · flm · (gln · gn) · fm
    eq1 = solve R'

    eq2 : ∀ r flm gl fm → r · flm · gl · fm ≡  r · (flm · fm ) · gl
    eq2 = solve R'

    eq3 : ∀ r fgl → r · fgl ≡ 1r · (1r · (r · fgl) · 1r) · (1r · 1r · (1r · 1r))
    eq3 = solve R'

    l = max m n

    path : 1r · (1r · (r · f ^ (l ∸ m) · g ^ (l ∸ n)) · (g ^ n · 1r)) · (1r · (f ^ m · 1r) · 1r)
         ≡ 1r · (1r · (r · (f · g) ^ l) · 1r) · (1r · 1r · (1r · 1r))
    path = 1r · (1r · (r · f ^ (l ∸ m) · g ^ (l ∸ n)) · (g ^ n · 1r)) · (1r · (f ^ m · 1r) · 1r)

         ≡⟨ eq1 r  (f ^ (l ∸ m)) (g ^ (l ∸ n)) (g ^ n) (f ^ m) ⟩

           r · f ^ (l ∸ m) · (g ^ (l ∸ n) · g ^ n) · f ^ m

         ≡⟨ cong (λ x → r · f ^ (l ∸ m) · x · f ^ m) (·-of-^-is-^-of-+ _ _ _) ⟩

           r · f ^ (l ∸ m) · g ^ (l ∸ n +ℕ n) · f ^ m

         ≡⟨ cong (λ x → r · f ^ (l ∸ m) · g ^ x · f ^ m) (≤-∸-+-cancel right-≤-max) ⟩

           r · f ^ (l ∸ m) · g ^ l · f ^ m

         ≡⟨ eq2 r (f ^ (l ∸ m)) (g ^ l) (f ^ m) ⟩

           r · (f ^ (l ∸ m) · f ^ m) · g ^ l

         ≡⟨ cong (λ x → r · x · g ^ l) (·-of-^-is-^-of-+ _ _ _) ⟩

           r · f ^ (l ∸ m +ℕ m) · g ^ l

         ≡⟨ cong (λ x → r · f ^ x · g ^ l) (≤-∸-+-cancel left-≤-max) ⟩

           r · f ^ l · g ^ l

         ≡⟨ sym (·Assoc _ _ _) ⟩

           r · (f ^ l · g ^ l)

         ≡⟨ cong (r ·_) (sym (^-ldist-· _ _ _)) ⟩

           r · (f · g) ^ l

         ≡⟨ eq3 r ((f · g) ^ l) ⟩

           1r · (1r · (r · (f · g) ^ l) · 1r) · (1r · 1r · (1r · 1r)) ∎

   base-^ᶠ-helper : (r : R) (m n : ℕ) → ∃[ x ∈ R × S[fg] ] (x .fst /1/1)
       ≡ [ [ r , f ^ m , PT.∣ m , refl ∣ ]
         , g/1 ^ᶠ n , PT.∣ n , refl ∣ ] ·R[1/f][1/g] (x .snd .fst /1/1)
   base-^ᶠ-helper r m n = subst (λ y →  ∃[ x ∈ R × S[fg] ] (x .fst /1/1)
                          ≡ [ [ r , f ^ m , PT.∣ m , refl ∣ ] , y ] ·R[1/f][1/g] (x .snd .fst /1/1))
                     (Σ≡Prop (λ _ → isPropPropTrunc) (^-respects-/1 _ n)) (baseCase r m n)

   indStep : (r : R[1/_] R' f) (n : ℕ) → ∃[ x ∈ R × S[fg] ]
         (x .fst /1/1) ≡ [ r , g/1 ^ᶠ n , PT.∣ n , refl ∣ ] ·R[1/f][1/g] (x .snd .fst /1/1)
   indStep = InvElPropElim _ (λ _ → isPropΠ λ _ → isPropPropTrunc) base-^ᶠ-helper

   toGoal : (r : R[1/_] R' f) (n : ℕ) → ∃[ x ∈ R × S[fg] ]
            (x .fst /1/1) ·R[1/f][1/g]
            ((x .snd .fst /1/1) ⁻¹) ⦃ φS⊆Aˣ pathtoR[1/fg] (x .snd .fst) (x .snd .snd) ⦄
          ≡ [ r , g/1 ^ᶠ n , PT.∣ n , refl ∣ ]
   toGoal r n = PT.map Σhelper (indStep r n)
    where
    Σhelper : Σ[ x ∈ R × S[fg] ]
               (x .fst /1/1) ≡ [ r , g/1 ^ᶠ n , PT.∣ n , refl ∣ ] ·R[1/f][1/g] (x .snd .fst /1/1)
            → Σ[ x ∈ R × S[fg] ]
               (x .fst /1/1) ·R[1/f][1/g] ((x .snd .fst /1/1) ⁻¹)
               ⦃ φS⊆Aˣ pathtoR[1/fg] (x .snd .fst) (x .snd .snd) ⦄
               ≡ [ r , g/1 ^ᶠ n , PT.∣ n , refl ∣ ]
    Σhelper ((r' , s , s∈S[fg]) , p) = (r' , s , s∈S[fg])
                                     , ⁻¹-eq-elim ⦃ φS⊆Aˣ pathtoR[1/fg] s s∈S[fg] ⦄ p

 -- In this module we construct the map R[1/fg]→R[1/f][1/g] directly
 -- and show that it is equal (although not judgementally) to the map induced
 -- by the universal property of localisation, i.e. transporting along the path
 -- constructed above. Given that this is the easier direction, we can see that
 -- it is pretty cumbersome to prove R[1/fg]≡R[1/f][1/g] directly,
 -- which illustrates the usefulness of S⁻¹RChar quite well.
 private
  module check where
   φ : R[1/fg] → R[1/f][1/g]
   φ = SQ.rec squash/ ϕ ϕcoh
     where
     S[fg] = Loc.S R' ([_ⁿ|n≥0] R' (f · g)) (powersFormMultClosedSubset R' (f · g))

     curriedϕΣ : (r s : R) → Σ[ n ∈ ℕ ] s ≡ (f · g) ^ n → R[1/f][1/g]
     curriedϕΣ r s (n , s≡fg^n) = [ [ r , (f ^ n) , PT.∣ n , refl ∣ ]
                                  , [ (g ^ n) , 1r , PT.∣ 0 , refl ∣ ] --denominator
                                  , PT.∣ n , ^-respects-/1 R' n ∣ ]

     curriedϕ : (r s : R) → ∃[ n ∈ ℕ ] s ≡ (f · g) ^ n → R[1/f][1/g]
     curriedϕ r s = elim→Set (λ _ → squash/) (curriedϕΣ r s) coh
      where
      coh : (x y : Σ[ n ∈ ℕ ] s ≡ (f · g) ^ n) → curriedϕΣ r s x ≡ curriedϕΣ r s y
      coh (n , s≡fg^n) (m , s≡fg^m) = eq/ _ _ ((1ᶠ , PT.∣ 0 , refl ∣) ,
                                      eq/ _ _ ( (1r , powersFormMultClosedSubset R' f .containsOne)
                                              , path))
       where
       eq1 : ∀ r gm  fm → 1r · (1r · r · gm) · (1r · fm · 1r) ≡ r · (gm · fm)
       eq1 = solve R'

       path : 1r · (1r · r · (g ^ m)) · (1r · (f ^ m) · 1r)
            ≡ 1r · (1r · r · (g ^ n)) · (1r · (f ^ n) · 1r)
       path = 1r · (1r · r · (g ^ m)) · (1r · (f ^ m) · 1r)

            ≡⟨ eq1 r (g ^ m) (f ^ m) ⟩

              r · (g ^ m · f ^ m)

            ≡⟨ cong (r ·_) (sym (^-ldist-· g f m)) ⟩

              r · ((g · f) ^ m)

            ≡⟨ cong (λ x → r · (x ^ m)) (·-comm _ _) ⟩

              r · ((f · g) ^ m)

            ≡⟨ cong (r ·_) ((sym s≡fg^m) ∙ s≡fg^n) ⟩

              r · ((f · g) ^ n)

            ≡⟨ cong (λ x → r · (x ^ n)) (·-comm _ _) ⟩

              r · ((g · f) ^ n)

            ≡⟨ cong (r ·_) (^-ldist-· g f n) ⟩

              r · (g ^ n · f ^ n)

            ≡⟨ sym (eq1 r (g ^ n) (f ^ n)) ⟩

              1r · (1r · r · (g ^ n)) · (1r · (f ^ n) · 1r) ∎

     ϕ : R × S[fg] → R[1/f][1/g]
     ϕ = uncurry2 curriedϕ -- λ (r / (fg)ⁿ) → ((r / fⁿ) / gⁿ)

     curriedϕcohΣ : (r s r' s' u : R) → (p : u · r · s' ≡ u · r' · s)
                                      → (α : Σ[ n ∈ ℕ ] s ≡ (f · g) ^ n)
                                      → (β : Σ[ m ∈ ℕ ] s' ≡ (f · g) ^ m)
                                      → (γ : Σ[ l ∈ ℕ ] u ≡ (f · g) ^ l)
                                      → ϕ (r , s , PT.∣ α ∣) ≡ ϕ (r' , s' , PT.∣ β ∣)
     curriedϕcohΣ r s r' s' u p (n , s≡fgⁿ) (m , s'≡fgᵐ) (l , u≡fgˡ) =
      eq/ _ _ ( ( [ (g ^ l) , 1r , powersFormMultClosedSubset R' f .containsOne ]
                , PT.∣ l , ^-respects-/1 R' l ∣)
              , eq/ _ _ ((f ^ l , PT.∣ l , refl ∣) , path))
      where
      eq1 : ∀ fl gl r gm fm
          → fl · (gl · r · gm) · (1r · fm · 1r) ≡ fl · gl · r · (gm · fm)
      eq1 = solve R'

      path : f ^ l · (g ^ l · transp (λ i → R) i0 r · transp (λ i → R) i0 (g ^ m))
                   · (1r · transp (λ i → R) i0 (f ^ m) · transp (λ i → R) i0 1r)
           ≡ f ^ l · (g ^ l · transp (λ i → R) i0 r' · transp (λ i → R) i0 (g ^ n))
                   · (1r · transp (λ i → R) i0 (f ^ n) · transp (λ i → R) i0 1r)
      path = f ^ l · (g ^ l · transp (λ i → R) i0 r · transp (λ i → R) i0 (g ^ m))
                   · (1r · transp (λ i → R) i0 (f ^ m) · transp (λ i → R) i0 1r)

           ≡⟨ (λ i → f ^ l · (g ^ l · transportRefl r i · transportRefl (g ^ m) i)
                           · (1r · transportRefl (f ^ m) i · transportRefl 1r i)) ⟩

             f ^ l · (g ^ l · r · g ^ m) · (1r · f ^ m · 1r)

           ≡⟨ eq1 (f ^ l) (g ^ l) r (g ^ m) (f ^ m) ⟩

             f ^ l · g ^ l · r · (g ^ m · f ^ m)

           ≡⟨ (λ i → ^-ldist-· f g l (~ i) · r · ^-ldist-· g f m (~ i)) ⟩

             (f · g) ^ l · r · (g · f) ^ m

           ≡⟨ cong (λ x → (f · g) ^ l · r · x ^ m) (·-comm _ _) ⟩

             (f · g) ^ l · r · (f · g) ^ m

           ≡⟨ (λ i → u≡fgˡ (~ i) · r · s'≡fgᵐ (~ i)) ⟩

             u · r · s'

           ≡⟨ p ⟩

             u · r' · s

           ≡⟨ (λ i → u≡fgˡ i · r' · s≡fgⁿ i) ⟩

             (f · g) ^ l · r' · (f · g) ^ n

           ≡⟨ cong (λ x → (f · g) ^ l · r' · x ^ n) (·-comm _ _) ⟩

             (f · g) ^ l · r' · (g · f) ^ n

           ≡⟨ (λ i → ^-ldist-· f g l i · r' · ^-ldist-· g f n i) ⟩

             f ^ l · g ^ l · r' · (g ^ n · f ^ n)

           ≡⟨ sym (eq1 (f ^ l) (g ^ l) r' (g ^ n) (f ^ n)) ⟩

             f ^ l · (g ^ l · r' · g ^ n) · (1r · f ^ n · 1r)

           ≡⟨ (λ i → f ^ l · (g ^ l · transportRefl r' (~ i) · transportRefl (g ^ n) (~ i))
                           · (1r · transportRefl (f ^ n) (~ i) · transportRefl 1r (~ i))) ⟩

             f ^ l · (g ^ l · transp (λ i → R) i0 r' · transp (λ i → R) i0 (g ^ n))
                   · (1r · transp (λ i → R) i0 (f ^ n) · transp (λ i → R) i0 1r) ∎

     curriedϕcoh : (r s r' s' u : R) → (p : u · r · s' ≡ u · r' · s)
                                     → (α : ∃[ n ∈ ℕ ] s ≡ (f · g) ^ n)
                                     → (β : ∃[ m ∈ ℕ ] s' ≡ (f · g) ^ m)
                                     → (γ : ∃[ l ∈ ℕ ] u ≡ (f · g) ^ l)
                                     → ϕ (r , s , α) ≡ ϕ (r' , s' , β)
     curriedϕcoh r s r' s' u p = PT.elim (λ _ → isPropΠ2 (λ _ _ → squash/ _ _))
                           λ α → PT.elim (λ _ → isPropΠ (λ _ → squash/ _ _))
                           λ β → PT.rec (squash/ _ _)
                           λ γ →  curriedϕcohΣ r s r' s' u p α β γ

     ϕcoh : (a b : R × S[fg])
          → Loc._≈_ R' ([_ⁿ|n≥0] R' (f · g)) (powersFormMultClosedSubset R' (f · g)) a b
          → ϕ a ≡ ϕ b
     ϕcoh (r , s , α) (r' , s' , β) ((u , γ) , p) =  curriedϕcoh r s r' s' u p α β γ

   -- the map induced by the universal property
   open S⁻¹RUniversalProp R' ([_ⁿ|n≥0] R' (f · g)) (powersFormMultClosedSubset R' (f · g))
   χ : R[1/fg] → R[1/f][1/g]
   χ = S⁻¹RHasUniversalProp R[1/f][1/g]AsCommRing /1/1AsCommRingHom fⁿgⁿ/1/1∈R[1/f][1/g]ˣ .fst .fst .fst

   -- the sanity check:
   -- both maps send a fraction r/(fg)ⁿ to a double fraction,
   -- where numerator and denominator are almost the same fraction respectively.
   -- unfortunately the proofs that the denominators are powers are quite different for
   -- the two maps, but of course we can ignore them.
   -- The definition of χ introduces a lot of (1r ·_). Perhaps most surprisingly,
   -- we have to give the path eq1 for the equality of the numerator of the numerator.
   φ≡χ : ∀ r → φ r ≡ χ r
   φ≡χ = InvElPropElim _ (λ _ → squash/ _ _) ℕcase
    where
    ℕcase : (r : R) (n : ℕ)
          → φ [ r , (f · g) ^ n , PT.∣ n , refl ∣ ] ≡ χ [ r , (f · g) ^ n , PT.∣ n , refl ∣ ]
    ℕcase r n = cong [_] (ΣPathP --look into the components of the double-fractions
              ( cong [_] (ΣPathP (eq1 , Σ≡Prop (λ x → S'[f] x .snd) (sym (·Lid _))))
              , Σ≡Prop (λ x → S'[f][g] x .snd) --ignore proof that denominator is power of g/1
              ( cong [_] (ΣPathP (sym (·Lid _) , Σ≡Prop (λ x → S'[f] x .snd) (sym (·Lid _)))))))
     where
     S'[f] = ([_ⁿ|n≥0] R' f)
     S'[f][g] = ([_ⁿ|n≥0] R[1/f]AsCommRing [ g , 1r , powersFormMultClosedSubset R' f .containsOne ])

     eq1 : transp (λ i → fst R') i0 r ≡ r · transp (λ i → fst R') i0 1r
     eq1 = transportRefl r ∙∙ sym (·Rid r) ∙∙ cong (r ·_) (sym (transportRefl 1r))

max_stars_repo_name: dolio/cubical

max_issues_repo_name: dolio/cubical

max_forks_repo_name: dolio/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Base where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients.Base
open import Cubical.HITs.PropositionalTruncation.Base

Rel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
Rel A B ℓ' = A → B → Type ℓ'

PropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
PropRel A B ℓ' = Σ[ R ∈ Rel A B ℓ' ] ∀ a b → isProp (R a b)

idPropRel : ∀ {ℓ} (A : Type ℓ) → PropRel A A ℓ
idPropRel A .fst a a' = ∥ a ≡ a' ∥
idPropRel A .snd _ _ = squash

invPropRel : ∀ {ℓ ℓ'} {A B : Type ℓ}
  → PropRel A B ℓ' → PropRel B A ℓ'
invPropRel R .fst b a = R .fst a b
invPropRel R .snd b a = R .snd a b

compPropRel : ∀ {ℓ ℓ' ℓ''} {A B C : Type ℓ}
  → PropRel A B ℓ' → PropRel B C ℓ'' → PropRel A C (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
compPropRel R S .fst a c = ∥ Σ[ b ∈ _ ] (R .fst a b × S .fst b c) ∥
compPropRel R S .snd _ _ = squash

graphRel : ∀ {ℓ} {A B : Type ℓ} → (A → B) → Rel A B ℓ
graphRel f a b = f a ≡ b

module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
  isRefl : Type (ℓ-max ℓ ℓ')
  isRefl = (a : A) → R a a

  isSym : Type (ℓ-max ℓ ℓ')
  isSym = (a b : A) → R a b → R b a

  isTrans : Type (ℓ-max ℓ ℓ')
  isTrans = (a b c : A)  → R a b → R b c → R a c

  record isEquivRel : Type (ℓ-max ℓ ℓ') where
    constructor equivRel
    field
      reflexive : isRefl
      symmetric : isSym
      transitive : isTrans

  isPropValued : Type (ℓ-max ℓ ℓ')
  isPropValued = (a b : A) → isProp (R a b)

  isEffective : Type (ℓ-max ℓ ℓ')
  isEffective =
    (a b : A) → isEquiv (eq/ {R = R} a b)

EquivRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
EquivRel A ℓ' = Σ[ R ∈ Rel A A ℓ' ] BinaryRelation.isEquivRel R

EquivPropRel : ∀ {ℓ} (A : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
EquivPropRel A ℓ' = Σ[ R ∈ PropRel A A ℓ' ] BinaryRelation.isEquivRel (R .fst)


text:
{-# OPTIONS --exact-split #-}
-- {-# OPTIONS -v tc.cover:10 #-}

postulate
  A : Set

record I : Set where
  constructor i
  field
    f : A

data Wrap : (j : I) → Set where
  con : (j : I) → Wrap j

postulate
  C : Set
  anything : C

test : (X : I) -> Wrap X -> C
test (i ._) (con x) = anything


text:
{-# OPTIONS --cubical-compatible #-}
open import Common.Prelude
open import Common.Equality

KNat : {x : Nat} (e : x ≡ x) → e ≡ refl
KNat refl = refl

KEqNat : {x : Nat} {e : x ≡ x} (p : e ≡ e) → p ≡ refl
KEqNat refl = refl

KListNat : {x : List Nat} (e : x ≡ x) → e ≡ refl
KListNat refl = refl

data D (A : Set) : Nat → Set where
  c : (x : A)(y : Nat) → D A y

-- Jesper 2015-12-18: this test case doesn't work yet with the new unifier
-- We need generalization of indices when applying the injectivity rule
--test : {A : Set} {x₁ x₂ : A} {y : Nat} → c x₁ y ≡ c x₂ y → Set
--test refl = Nat


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

open import Base
open import Integers
open import Homotopy.Truncation
open import Spaces.Spheres
open import Spaces.Suspension
open import Homotopy.Connected
open import Homotopy.ConnectedSuspension
open import Homotopy.Pointed
open import Homotopy.HomotopyGroups

module Spaces.PikSn where

abstract
  Sⁿ-S-is-connected : (n : ℕ) → is-connected ⟨ n ⟩ (Sⁿ (S n))
  Sⁿ-S-is-connected n =
    suspension-is-connected-S (Sⁿ n) ind-hyp (proj (⋆Sⁿ n)) where
      ind-hyp : is-connected (n -1) (Sⁿ n)
      ind-hyp with n
      ind-hyp | O = inhab-prop-is-contr (proj true) (τ-is-truncated _ _)
      ind-hyp | S n = Sⁿ-S-is-connected n

Sⁿ⋆ : (n : ℕ) → pType₀
Sⁿ⋆ n = ⋆[ Sⁿ n , ⋆Sⁿ n ]

abstract
  πk-Sⁿ-is-contr : (k n : ℕ) (lt : k < n)
    → is-contr⋆ (πⁿ k (Sⁿ⋆ n))
  πk-Sⁿ-is-contr k O ()
  πk-Sⁿ-is-contr k (S n) lt = connected-πⁿ k n lt _ (Sⁿ-S-is-connected n)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

module RewritingNat where

open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

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

_+_ : Nat → Nat → Nat
zero + n = n
(suc m) + n = suc (m + n)

plusAssoc : ∀ x {y z : Nat} → ((x + y) + z) ≡ (x + (y + z))
plusAssoc zero = refl
plusAssoc (suc x) {y} {z} rewrite plusAssoc x {y} {z} = refl

plus0T : Set
plus0T = ∀{x} → (x + zero) ≡ x

plusSucT : Set
plusSucT = ∀{x y} → (x + (suc y)) ≡ suc (x + y)

postulate
  plus0p : plus0T
  {-# REWRITE plus0p #-}

  plusSucp : plusSucT

{-# REWRITE plusSucp plusAssoc #-}

plus0 : plus0T
plus0 = refl

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

-- Needs REWRITE plus0p plusSucp
reverseAcc : ∀{A n m} → Vec A n → Vec A m → Vec A (n + m)
reverseAcc [] acc = acc
reverseAcc (x ∷ xs) acc = reverseAcc xs (x ∷ acc)

append : ∀{A n m} → Vec A n → Vec A m → Vec A (n + m)
append []       ys = ys
append (x ∷ xs) ys = x ∷ append xs ys

-- Note: appendAssoc needs REWRITE plusAssoc to be well-typed.
appendAssoc : ∀{A n m l} (u : Vec A n) {v : Vec A m}{w : Vec A l} →
  append (append u v) w ≡ append u (append v w)
appendAssoc [] = refl
appendAssoc (x ∷ xs) {v} {w} rewrite appendAssoc xs {v} {w} = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

   Copyright (c) 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 Dijkstra.EitherD
open import LibraBFT.Impl.Consensus.EpochManagerTypes
open import LibraBFT.Impl.Handle
open        InitHandler
import      LibraBFT.Impl.IO.OBM.GenKeyFile           as GenKeyFile
import      LibraBFT.Impl.IO.OBM.Properties.Start     as Start
import      LibraBFT.Impl.Properties.Util             as Util
import      LibraBFT.Impl.Types.BlockInfo             as BlockInfo
import      LibraBFT.Impl.Types.ValidatorSigner       as ValidatorSigner
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import LibraBFT.ImplShared.Interface.Output
open import Optics.All
open import Util.Prelude
open import Yasm.Types as YT

module LibraBFT.Impl.Handle.InitProperties where

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

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

open Util.Invariants
open Util.InitProofDefs

module getEmRmSpec
  (em : EpochManager)
  where

  Contract : EitherD-Post ErrLog RoundManager
  Contract (Left x)   = ⊤
  Contract (Right rm) = rm IsNormalRoundManagerOf em

  contract' : EitherD-weakestPre (getEmRm-ed-abs em) Contract
  contract' rewrite getEmRm-ed-abs≡
     with em ^∙ emProcessor | inspect (_^∙ emProcessor) em
  ...| nothing | _ = tt
  ...| just (RoundProcessorRecovery x) | _     = tt
  ...| just (RoundProcessorNormal   x) | [ refl ] = refl

module initializeSpec
  (now : Instant)
  (nfl : GenKeyFile.NfLiwsVsVvPe)
  where

  contract' : EitherD-weakestPre (initialize-ed-abs now nfl) (InitContract nothing)
  contract' rewrite initialize-ed-abs≡ =
    Start.startViaConsensusProviderSpec.contract'
      now
      nfl
      (TxTypeDependentStuffForNetwork∙new proposalGenerator (StateComputer∙new BlockInfo.gENESIS_VERSION))

module initEMWithOutputSpec
  (bsi : BootstrapInfo)
  (vs  : ValidatorSigner)
  where

  contract' : EitherD-weakestPre (initEMWithOutput-ed-abs bsi vs) (InitContract nothing)
  contract' rewrite initEMWithOutput-ed-abs≡ = initializeSpec.contract' now (mkNfLiwsVsVvPe bsi vs)

module initRMWithOutputSpec
  (bsi : BootstrapInfo)
  (vs  : ValidatorSigner)
  where

  Contract : EitherD-Post ErrLog (RoundManager × List Output)
  Contract (Left x)            = ⊤
  Contract (Right (rm , outs)) = InitContractOk nothing rm outs

  open initRMWithOutput-ed bsi vs

  contract-step₁ : ∀ {em lo}
                   → EMInitCond nothing (em , lo)
                   → EitherD-weakestPre (step₁ (em , lo)) Contract
  contract-step₁ {em} {lo} (rm , inrm , cntrctOk) =
    EitherD-⇒-bind (getEmRm-ed-abs em)
                   (getEmRmSpec.contract' em)
                   P⇒Q
     where
       P⇒Q : EitherD-Post-⇒ (getEmRmSpec.Contract em)
                            (EitherD-weakestPre-bindPost (λ rm → RightD (rm , lo)) Contract)
       P⇒Q (Left x) _ = tt
       P⇒Q (Right rm') pf .rm' refl rewrite IsNormalRoundManagerOf-inj {em} inrm pf = cntrctOk

  contract' : EitherD-weakestPre (initRMWithOutput-ed-abs bsi vs) Contract
  contract' rewrite initRMWithOutput-ed-abs≡ =
    EitherD-⇒-bind (initEMWithOutput-ed-abs bsi vs)
                   (initEMWithOutputSpec.contract' bsi vs)
                   P⇒Q
      where
      P⇒Q : EitherD-Post-⇒ (InitContract nothing) _
      P⇒Q (Left x) _ = tt
      P⇒Q (Right (em , lo)) pf .(em , lo) refl = contract-step₁ pf

  contract : Contract (initRMWithOutput-e-abs bsi vs)
  contract rewrite initRMWithOutput≡ {bsi} {vs} =
    EitherD-contract (initRMWithOutput-ed-abs bsi vs) Contract contract'

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

module initHandlerSpec
  (pid : Author)
  (bsi : BootstrapInfo)
  where

  record ContractOk (rm : RoundManager) (acts : List (YT.Action NetworkMsg)) : Set where
    constructor mkContractOk
    field
      rmInv       : Util.Invariants.RoundManagerInv rm
      sdLVnothing : InitSdLV≡ rm nothing
      sigs∈bs     : InitSigs∈bs rm
      isInitPM    : InitIsInitPM acts
      -- TODO-3: We will eventually need to know that our ValidatorSigner is for the correct peer,
      -- because it will be needed to prove impl-sps-avp : StepPeerState-AllValidParts

  Contract : Maybe (RoundManager × List (YT.Action NetworkMsg)) → Set
  Contract nothing            = ⊤
  Contract (just (rm , acts)) = ContractOk rm acts

  -- TODO-2: this property is more succinctly/elegantly stated as Contract (initHandler pid bsi),
  -- and can be proved by starting the proof as follows:
  --
  -- contract : Contract (initHandler pid bsi)
  -- contract with initHandler pid bsi | inspect (initHandler pid) bsi
  -- ...| nothing | _ = tt
  -- ...| just (rm , acts) | [ hndl≡just ]
  --
  -- However, this breaks a bunch of proofs that use this, so not doing it for now.
  contract : ∀ {x} → initHandler pid bsi ≡ x → Contract x
  contract {nothing} hndl≡nothing rewrite sym hndl≡nothing = tt
  contract {just (rm , acts)} hndl≡just
    with ValidatorSigner.obmGetValidatorSigner pid  (bsi ^∙ bsiVSS)
  ...| Left _ = absurd nothing ≡ just _ case hndl≡just  of λ ()
  ...| Right vs
    with initRMWithOutputSpec.contract bsi vs
  ...| initRMWithOutputContractOk
    with initRMWithOutput-e-abs bsi vs
  ...| Left _ = absurd nothing ≡ just (rm , acts) case hndl≡just of λ ()
  ...| Right rm×outs rewrite sym (cong proj₂ (just-injective hndl≡just)) |
                                 (cong proj₁ (just-injective hndl≡just)) =
       mkContractOk
         (InitContractOk.rmInv       initRMWithOutputContractOk)
         (InitContractOk.sdLV≡       initRMWithOutputContractOk)
         (InitContractOk.sigs∈bs     initRMWithOutputContractOk)
         (InitContractOk.isInitPM    initRMWithOutputContractOk)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Generalised notion of interleaving two lists into one in an
-- order-preserving manner
------------------------------------------------------------------------

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

module Data.List.Relation.Ternary.Interleaving where

open import Level
open import Data.List.Base as List using (List; []; _∷_; _++_)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
open import Data.Product as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

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

module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
         (L : REL A C l) (R : REL B C r) where

  data Interleaving : List A → List B → List C → Set (a ⊔ b ⊔ c ⊔ l ⊔ r) where
    []   : Interleaving [] [] []
    _∷ˡ_ : ∀ {a c l r cs} → L a c → Interleaving l r cs → Interleaving (a ∷ l) r (c ∷ cs)
    _∷ʳ_ : ∀ {b c l r cs} → R b c → Interleaving l r cs → Interleaving l (b ∷ r) (c ∷ cs)

------------------------------------------------------------------------
-- Operations

module _ {a b c l r} {A : Set a} {B : Set b} {C : Set c}
         {L : REL A C l} {R : REL B C r} where

-- injections

  left : ∀ {as cs} → Pointwise L as cs → Interleaving L R as [] cs
  left []       = []
  left (l ∷ pw) = l ∷ˡ left pw

  right : ∀ {bs cs} → Pointwise R bs cs → Interleaving L R [] bs cs
  right []       = []
  right (r ∷ pw) = r ∷ʳ right pw

-- swap

  swap : ∀ {cs l r} → Interleaving L R l r cs → Interleaving R L r l cs
  swap []        = []
  swap (l ∷ˡ sp) = l ∷ʳ swap sp
  swap (r ∷ʳ sp) = r ∷ˡ swap sp

-- extract the "proper" equality split from the pointwise relations

  break : ∀ {cs l r} → Interleaving L R l r cs → ∃ $ uncurry $ λ csl csr →
          Interleaving _≡_ _≡_ csl csr cs × Pointwise L l csl × Pointwise R r csr
  break []        = -, [] , [] , []
  break (l ∷ˡ sp) = let (_ , eq , pwl , pwr) = break sp in
                    -, P.refl ∷ˡ eq , l ∷ pwl , pwr
  break (r ∷ʳ sp) = let (_ , eq , pwl , pwr) = break sp in
                    -, P.refl ∷ʳ eq , pwl , r ∷ pwr

-- map

module _ {a b c l r p q} {A : Set a} {B : Set b} {C : Set c}
         {L : REL A C l} {R : REL B C r} {P : REL A C p} {Q : REL B C q} where

  map : ∀ {cs l r} → L ⇒ P → R ⇒ Q → Interleaving L R l r cs → Interleaving P Q l r cs
  map L⇒P R⇒Q []        = []
  map L⇒P R⇒Q (l ∷ˡ sp) = L⇒P l ∷ˡ map L⇒P R⇒Q sp
  map L⇒P R⇒Q (r ∷ʳ sp) = R⇒Q r ∷ʳ map L⇒P R⇒Q sp

module _ {a b c l r p} {A : Set a} {B : Set b} {C : Set c}
         {L : REL A C l} {R : REL B C r} where

  map₁ : ∀ {P : REL A C p} {as l r} → L ⇒ P →
         Interleaving L R l r as → Interleaving P R l r as
  map₁ L⇒P = map L⇒P id

  map₂ : ∀ {P : REL B C p} {as l r} → R ⇒ P →
         Interleaving L R l r as → Interleaving L P l r as
  map₂ = map id

------------------------------------------------------------------------
-- Special case: The second and third list have the same type

module _ {a b l r} {A : Set a} {B : Set b} {L : REL A B l} {R : REL A B r} where

-- converting back and forth with pointwise

  split : ∀ {as bs} → Pointwise (λ a b → L a b ⊎ R a b) as bs →
          ∃₂ λ asr asl → Interleaving L R asl asr bs
  split []            = [] , [] , []
  split (inj₁ l ∷ pw) = Prod.map _ (Prod.map _ (l ∷ˡ_)) (split pw)
  split (inj₂ r ∷ pw) = Prod.map _ (Prod.map _ (r ∷ʳ_)) (split pw)

  unsplit : ∀ {l r as} → Interleaving L R l r as →
            ∃ λ bs → Pointwise (λ a b → L a b ⊎ R a b) bs as
  unsplit []        = -, []
  unsplit (l ∷ˡ sp) = Prod.map _ (inj₁ l ∷_) (unsplit sp)
  unsplit (r ∷ʳ sp) = Prod.map _ (inj₂ r ∷_) (unsplit sp)


text:
module Plain.Terms where

open import Data.Nat
open import Data.Fin

record Signature (n : ℕ) : Set where
  field
    -- symbols are encoded as numbers in Fin n
    -- arity
    ar : Fin n → ℕ

open Signature public

-- | Countable set of Variables
Var : Set
Var = ℕ

open import Data.Vec as V
open import Size
-- | Term in with a signature Σ with variables var
data Term {i : Size} {j : Size< i} {n : ℕ}
  (Σ : Signature n) (var : Set) : Set where
   FNode : {k : Size< j}
     → (f : Fin n) → Vec (Term {j} {k} {n} Σ var) (ar Σ f)
     → Term {i} {j} {n} Σ var
   VNode :  (v : var) → Term {i} {j} {n} Σ var

open import Data.Empty

-- | Ground Terms
GTerm : {n : ℕ} → (Σ : Signature n) → Set
GTerm Σ =  Term Σ ⊥

open import Data.List as L

-- | Horn clause
--
data Clause {n : ℕ} (Σ : Signature n) : Set where
  _:-_ : (Term Σ Var) → List (Term Σ Var)  → Clause Σ

cHead : {n : ℕ} → {Σ : Signature n} → Clause Σ → Term Σ Var
cHead (a :- _) = a

cBody : {n : ℕ} → {Σ : Signature n} → Clause Σ → List (Term Σ Var)
cBody (_ :- bs) = bs

record Program {n : ℕ} (Σ : Signature n) : Set where
  field
    prg : List (Clause Σ) -- → Program Σ

--unPrg : {n : ℕ} → {Σ : Signature n} → Program Σ → List (Clause Σ)
--unPrg (prg cls) = cls

record GSubst {n : ℕ} (Σ : Signature n) : Set₁ where
  field
    subst : (Var → GTerm Σ)

open GSubst

-- | substitution application
app : {i : Size} → {j : Size< i} →
  {n : ℕ} → {Σ : Signature n}
  → GSubst Σ → Term {i} {j} Σ Var → GTerm Σ
app σ (FNode f fs) = FNode f (V.map (app σ) fs)
app σ (VNode v) = subst σ v

max_stars_repo_name: frantisekfarka/lp-mod

max_issues_repo_name: frantisekfarka/lp-mod

max_forks_repo_name: frantisekfarka/lp-mod


text:
module spaceShipSimpleVar where

open import Unit
open import Data.List.Base hiding ([])
open import Data.Bool.Base
open import Data.Integer
open import Data.Product hiding (map)
open import NativeIO

open import StateSizedIO.GUI.WxBindingsFFI
open import StateSizedIO.GUI.WxGraphicsLib
open import StateSized.GUI.ShipBitMap
open import SizedIO.Base
open import StateSizedIO.GUI.BaseStateDependent
open import StateSizedIO.GUI.VariableList

VarType = ℤ

varInit : VarType
varInit = (+ 150)

onPaint : ∀{i} → VarType → DC → Rect → IO GuiLev1Interface i VarType
onPaint z dc rect      =  do (drawBitmap dc ship (z , (+ 150)) true) λ _ →
                          return z

moveSpaceShip  : ∀{i} → Frame → VarType → IO GuiLev1Interface i VarType
moveSpaceShip  fra z   =  return (z + + 20)

callRepaint    : ∀{i} → Frame → VarType → IO GuiLev1Interface i VarType
callRepaint    fra z   =  do (repaint fra) λ _ → return z

buttonHandler : ∀{i} → Frame → List (VarType  → IO GuiLev1Interface i VarType)
buttonHandler fra = moveSpaceShip fra ∷ [ callRepaint fra ]

program : ∀{i} → IOˢ GuiLev2Interface i (λ _ → Unit) []
program =  doˢ (level1C makeFrame)           λ fra →
           doˢ (level1C (makeButton fra))    λ bt →
           doˢ (level1C (addButton fra bt))  λ _ →
           doˢ (createVar varInit)           λ _ →
           doˢ (setButtonHandler bt (buttonHandler fra)) λ _ →
           doˢ (setOnPaint       fra [ onPaint  ])
           returnˢ

main : NativeIO Unit
main = start (translateLev2 program)

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{- Formal verification of authenticated append-only skiplists in Agda, version 1.0.

   Copyright (c) 2020 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 Data.Empty
open import Data.Sum
open import Data.Fin using (Fin; toℕ ; fromℕ ; fromℕ≤)
open import Data.Fin.Properties using (toℕ<n; toℕ-injective)
open import Data.Nat renaming (_≟_ to _≟ℕ_; _≤?_ to _≤?ℕ_)
open import Data.Nat.Properties
open import Data.List renaming (map to List-map)
open import Data.List.Relation.Unary.Any
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

-- This module pulls in the definitions from AAOSL.Hops and uses
-- them to construct a DepRel based on the dependency relation
-- defined there, showing that this concrete AAOSL enjoys the
-- properties we have proved for abstract ones

module AAOSL.Concrete where

 open import Data.Nat.Even
 open import Data.Nat.Encode
 open import AAOSL.Lemmas
 open import AAOSL.Hops
 open import AAOSL.Abstract.Hash
 open import AAOSL.Abstract.DepRel

 ---------------------------------------------------
 -- Translating the proofs about Hops into a DepRel,
 -- as required by AAOSL.Abstract.Advancement

 getHop : ∀{j}(h : Fin (lvlOf j)) → H (toℕ h) j (j ∸ 2 ^ toℕ h)
 getHop {j} h = h-correct j (toℕ h) (toℕ<n {lvlOf j} h)

 hop-prog : {m : ℕ} (h : Fin (lvlOf m)) → m ∸ (2 ^ toℕ h) ≢ m
 hop-prog {zero} ()
 hop-prog {suc m} h = ∸-≢ (2 ^ toℕ h) (1≤2^n (toℕ h)) (lvlOf-correct (toℕ<n h))

 hop-≤ : {m : ℕ} (h : Fin (lvlOf m)) → m ∸ (2 ^ toℕ h) ≤ m
 hop-≤ {zero} ()
 hop-≤ {suc m} h = m∸n≤m (suc m) (2 ^ toℕ h)

 lvlOfsuc : ∀ m → 0 < lvlOf (suc m)
 lvlOfsuc m with even? (suc m)
 ...| yes _ = s≤s z≤n
 ...| no  _ = s≤s z≤n

 -- This proves that ℕ makes a skiplog dependency relation
 -- by connecting the indexes by their largest power of two.
 skiplog-dep-rel : DepRel
 skiplog-dep-rel = record
   { lvlof          = lvlOf
   ; lvlof-z        = refl
   ; lvlof-s        = lvlOfsuc
   ; hop-tgt        = λ {m} h → m ∸ 2 ^ toℕ h
   ; hop-tgt-inj    = λ {m} {h} {h'} prf
                    → toℕ-injective (2^-injective {toℕ h} {toℕ h'}
                                      (∸-inj (2 ^ toℕ h) (2 ^ toℕ h')
                                             (lvlOf-correct (toℕ<n h))
                                             (lvlOf-correct (toℕ<n h'))
                                      prf))
   ; hop-<         = λ h → ≤∧≢⇒< (hop-≤ h) (hop-prog h)
   ; hops-nested-or-nonoverlapping
      = λ {h₁} {h₂} {h₃} {h₄} a b
        → no-overlap-< (getHop h₃) (getHop h₄) a b
  }

 -- This, in turn, enables us to bring the abstract module into
 -- scope with everything instantiated minus the hash functions.
 module _
    (hash    : ByteString → Hash)
    (hash-cr : ∀{x y} → hash x ≡ hash y → Collision hash x y ⊎ x ≡ y)
  where

  open import AAOSL.Abstract.Advancement hash hash-cr encodeℕ encodeℕ-inj skiplog-dep-rel
  open import AAOSL.Abstract.EvoCR hash hash-cr encodeℕ encodeℕ-inj skiplog-dep-rel


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Algebra.SymmetricGroup where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Data.Nat using (ℕ ; suc ; zero)
open import Cubical.Data.Fin using (Fin ; isSetFin)
open import Cubical.Data.Empty
open import Cubical.Relation.Nullary using (¬_)

open import Cubical.Structures.Group
open import Cubical.Structures.NAryOp

private
  variable
    ℓ ℓ' : Level

Symmetric-Group : (X : Type ℓ) → isSet X → Group
Symmetric-Group X isSetX =
  (X ≃ X) ,
  compEquiv ,
  (isOfHLevel≃ 2 isSetX isSetX , compEquiv-assoc) ,
  idEquiv X , (λ f → compEquivEquivId f , compEquivIdEquiv f) , λ f → invEquiv f , invEquiv-is-rinv f , invEquiv-is-linv f

-- Finite symmetrics groups

Sym : ℕ → Group
Sym n = Symmetric-Group (Fin n) isSetFin


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.Instances.Polynomials.MultivariatePoly where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Sigma
open import Cubical.Data.Vec
open import Cubical.Data.Vec.OperationsNat

open import Cubical.Algebra.Monoid.Instances.NatVec
open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.GradedRing.DirectSumHIT
open import Cubical.Algebra.GradedRing.Instances.Polynomials
open import Cubical.Algebra.CommRing.Instances.Int

private variable
  ℓ : Level

-----------------------------------------------------------------------------
-- General Nth polynome

open GradedRing-⊕HIT-index
open GradedRing-⊕HIT-⋆
open ExtensionCommRing

module _
  (ACommRing@(A , Astr) : CommRing ℓ)
  (n : ℕ)
  where

  open CommRingStr Astr
  open RingTheory (CommRing→Ring ACommRing)

  PolyCommRing : CommRing ℓ
  PolyCommRing = ⊕HITgradedRing-CommRing
                 (NatVecMonoid n)
                 (λ _ → A)
                 (λ _ → snd (Ring→AbGroup (CommRing→Ring ACommRing)))
                 1r _·_ 0LeftAnnihilates 0RightAnnihilates
                 (λ a b c → ΣPathP ((+n-vec-assoc _ _ _) , (·Assoc _ _ _)))
                 (λ a → ΣPathP ((+n-vec-rid _) , (·IdR _)))
                 (λ a → ΣPathP((+n-vec-lid _) , (·IdL _)))
                 ·DistR+
                 ·DistL+
                 λ x y → ΣPathP ((+n-vec-comm _ _) , (·Comm _ _))

-----------------------------------------------------------------------------
-- Notation and syntax in the case 1,2,3 and ℤ

module _
  (Ar@(A , Astr) : CommRing ℓ)
  (n : ℕ)
  where

  Poly : Type ℓ
  Poly = fst (PolyCommRing Ar n)

-- Possible renaming when you import
-- (PolyCommRing to A[X1,···,Xn] ; Poly to A[x1,···,xn])

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-

This file contains:

- Definitions equivalences

- Glue types

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Core.Glue where

open import Cubical.Core.Primitives

open import Agda.Builtin.Cubical.Glue public
  using ( isEquiv       -- ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ ⊔ ℓ')

        ; equiv-proof   -- ∀ (y : B) → isContr (fiber f y)

        ; _≃_           -- ∀ {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') → Type (ℓ ⊔ ℓ')

        ; equivFun      -- ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ≃ B → A → B

        ; equivProof    -- ∀ {ℓ ℓ'} (T : Type ℓ) (A : Type ℓ') (w : T ≃ A) (a : A) φ →
                        -- Partial φ (fiber (equivFun w) a) → fiber (equivFun w) a

        ; primGlue      -- ∀ {ℓ ℓ'} (A : Type ℓ) {φ : I} (T : Partial φ (Type ℓ'))
                        -- → (e : PartialP φ (λ o → T o ≃ A)) → Type ℓ'

        ; prim^unglue   -- ∀ {ℓ ℓ'} {A : Type ℓ} {φ : I} {T : Partial φ (Type ℓ')}
                        -- → {e : PartialP φ (λ o → T o ≃ A)} → primGlue A T e → A

        -- The ∀ operation on I. This is commented out as it is not currently used for anything
        -- ; primFaceForall -- (I → I) → I
        )
  renaming ( prim^glue   to glue         -- ∀ {ℓ ℓ'} {A : Type ℓ} {φ : I} {T : Partial φ (Type ℓ')}
                                         -- → {e : PartialP φ (λ o → T o ≃ A)}
                                         -- → PartialP φ T → A → primGlue A T e

           ; pathToEquiv to lineToEquiv  -- ∀ {ℓ : I → Level} (P : (i : I) → Type (ℓ i)) → P i0 ≃ P i1
           )

private
  variable
    ℓ ℓ' : Level

-- Uncurry Glue to make it more pleasant to use
Glue : (A : Type ℓ) {φ : I}
       → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A))
       → Type ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

-- Make the φ argument of prim^unglue explicit
unglue : {A : Type ℓ} (φ : I) {T : Partial φ (Type ℓ')}
         {e : PartialP φ (λ o → T o ≃ A)} → primGlue A T e → A
unglue φ = prim^unglue {φ = φ}

-- People unfamiliar with [Glue], [glue] and [uglue] can find the types below more
-- informative as they demonstrate the computational behavior.
--
-- Full inference rules can be found in Section 6 of CCHM:
-- https://arxiv.org/pdf/1611.02108.pdf
-- Cubical Type Theory: a constructive interpretation of the univalence axiom
-- Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg
private

  Glue-S : (A : Type ℓ) {φ : I}
         → (Te : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ A))
         → Sub (Type ℓ') φ (λ { (φ = i1) → Te 1=1 .fst })
  Glue-S A Te = inS (Glue A Te)

  glue-S :
   ∀ {A : Type ℓ} {φ : I}
   → {T : Partial φ (Type ℓ')} {e : PartialP φ (λ o → T o ≃ A)}
   → (t : PartialP φ T)
   → Sub A φ (λ { (φ = i1) → e 1=1 .fst (t 1=1) })
   → Sub (primGlue A T e) φ (λ { (φ = i1) → t 1=1 })
  glue-S t s = inS (glue t (outS s))

  unglue-S :
    ∀ {A : Type ℓ} (φ : I)
    {T : Partial φ (Type ℓ')} {e : PartialP φ (λ o → T o ≃ A)}
    → (x : primGlue A T e)
    → Sub A φ (λ { (φ = i1) → e 1=1 .fst x })
  unglue-S φ x = inS (prim^unglue {φ = φ} x)


text:
-- Andreas, 2018-03-03, termination bug found by Nisse
-- caused by a missing call to `instantiate`.

-- {-# OPTIONS -vtc:20 -vterm:20 #-}

{-# BUILTIN SIZEUNIV SizeU #-}
{-# BUILTIN SIZE     Size   #-}
{-# BUILTIN SIZELT   Size<_ #-}
{-# BUILTIN SIZEINF  ∞      #-}

record Unit (i : Size) : Set where
  coinductive
  field
    force : (j : Size< i) → Unit j

postulate
  tail : Unit ∞ → Unit ∞
  id   : ∀ i → Unit i → Unit i

u : ∀ i → Unit i
u i = tail (id _ λ { .Unit.force j → u j })

-- Should not termination check.


text:
-- Andreas, 2019-05-30, issue #3823
-- Named where module M should be in scope in rhs.
-- This enables to use it in expressions like record{M}.

open import Agda.Builtin.Equality

record R : Set₂ where
  field
    A : Set₁

r : R
r = record {M}
  module M where
    A = Set

-- ERROR WAS:
-- No module M in scope
-- when scope checking record { M }

test : r ≡ record {A = Set}
test = refl

-- Should succeed.

-- Should also work with module parameters.

s : Set₁ → R
s B = record {L}
  module L where
    A = B

-- With rewrite:

postulate
  B : Set
  a b : B
  a≡b : a ≡ b
  P : B → Set

record W : Set where
  field
    wrap : P b

w : P a → W
w p rewrite a≡b = record {N}
  module N where
    wrap = p

-- Should also succeed in the presence of `rewrite`.

module N' = N  -- See issue #3824.

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Empty type
------------------------------------------------------------------------

module Data.Empty where

open import Level

data ⊥ : Set where

{-# IMPORT Data.FFI #-}
{-# COMPILED_DATA ⊥ Data.FFI.AgdaEmpty #-}

⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()


text:
module Relation.Equivalence.Univalence where

open import Basics
open import Level
open import Relation.Equality
open import Data.Product

-- For any A and B, a quasi-inverse of f is a triple with
--    ∘ A way back (an inverse for the homomorphism)
--    ∘ Homotopies:
--        ⊚ α : f ∘ g ∼ id
--        ⊚ β : g ∘ f ∼ id
-- For now, because I am lazy, the presence of a quasi-inverse will count
-- as our definition of equivalence for now.  Sorry.
record IsEquiv {i j}{A : Set i}{B : Set j}(to : A → B) : Set (i ⊔ j) where
  field
    from : B → A
    iso₁ : (x : A) → from (to x) ≡ x
    iso₂ : (y : B) → to (from y) ≡ y

-- Example 2.4.7: Identity is an equivalence.
id-is-equiv : ∀ {i} (A : Set i) → IsEquiv (id {i}{A})
id-is-equiv {i} A = record
  { from = id {i}{A}
  ; iso₁ = λ _ → refl
  ; iso₂ = λ _ → refl
  }

-- Type equivalence is also an equivalence, just on the Universe because:
--    ∘ id-is-equiv works for it, therefore A ≃ A
--    ∘ With A ≃ B, we can always make B ≃ A
--    ∘ With A ≃ B and B ≃ C we have A ≃ C
_≃_ : ∀ {i j} (A : Set i) (B : Set j) → Set (i ⊔ j)
A ≃ B = Σ (A → B) IsEquiv

postulate -- Just kidding
  ua : ∀ {i} {{A : Set i}}{{B : Set i}} → (A ≃ B) ≃ (A ≡ B)
-- ^This says "equivalent types may be identified"

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module Example where

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

postulate
  case-Nat : (P : Nat -> Set) -> P zero ->
	     ((n:Nat) -> P (suc n)) ->
	     (n : Nat) -> P n

-- test : Nat -> Nat
test = case-Nat _ zero (\n -> n)

{-
data Size : Set where
  empty	   : Size
  nonempty : Size
  whatever : Size

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

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

data Monad (M:Set -> Set) : Set1 where
  monad : Monad M

postulate
  build : {M:Set -> Set} -> Monad M -> {C:Size -> Set} -> (A:Set) ->
	  (A -> C nonempty) ->
	  ((n:Size) -> List (C n) -> M (List A)) ->
	  List A -> M (C whatever)

test : (A:Set) -> Nat
test A = build monad A (\x -> x) (\n xs -> xs) nil
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import LogicalFormulae
open import Setoids.Setoids
open import Functions.Definition
open import Functions.Lemmas
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Integers.Integers
open import Numbers.Rationals.Definition
open import Sets.FinSet.Definition
open import Sets.FinSet.Lemmas
open import Sets.Cardinality.Finite.Definition
open import Groups.Definition
open import Groups.Groups
open import Groups.Abelian.Definition
open import Groups.FiniteGroups.Definition
open import Rings.Definition
open import Numbers.Modulo.Group
open import Numbers.Modulo.Definition
open import Semirings.Definition

module Groups.LectureNotes.Lecture1 where

ℤIsGroup : _
ℤIsGroup = ℤGroup

ℚIsGroup : _
ℚIsGroup = Ring.additiveGroup ℚRing

-- TODO: R is a group with +

integersMinusNotGroup : Group (reflSetoid ℤ) (_-Z_) → False
integersMinusNotGroup record { +WellDefined = wellDefined ; 0G = identity ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } with multAssoc {nonneg 3} {nonneg 2} {nonneg 1}
integersMinusNotGroup record { +WellDefined = wellDefined ; 0G = identity ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | ()

negSuccInjective : {a b : ℕ} → (negSucc a ≡ negSucc b) → a ≡ b
negSuccInjective {a} {.a} refl = refl

nonnegInjective : {a b : ℕ} → (nonneg a ≡ nonneg b) → a ≡ b
nonnegInjective {a} {.a} refl = refl

integersTimesNotGroup : Group (reflSetoid ℤ) (_*Z_) → False
integersTimesNotGroup record { +WellDefined = wellDefined ; 0G = (nonneg zero) ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } with multIdentLeft {negSucc 1}
... | ()
integersTimesNotGroup record { +WellDefined = wellDefined ; 0G = (nonneg (succ zero)) ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } with invLeft {nonneg zero}
... | bl with inverse (nonneg zero)
integersTimesNotGroup record { +WellDefined = wellDefined ; 0G = (nonneg (succ zero)) ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | () | nonneg zero
integersTimesNotGroup record { +WellDefined = wellDefined ; 0G = (nonneg (succ zero)) ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | p | nonneg (succ x) = naughtE (nonnegInjective (transitivity (applyEquality nonneg (equalityCommutative (Semiring.productZeroRight ℕSemiring x))) p))
integersTimesNotGroup record { +WellDefined = wellDefined ; 0G = (nonneg (succ zero)) ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | () | negSucc x
integersTimesNotGroup record { +WellDefined = wellDefined ; 0G = (nonneg (succ (succ x))) ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } with succInjective (negSuccInjective (multIdentLeft {negSucc 1}))
... | ()
integersTimesNotGroup record { +WellDefined = wellDefined ; 0G = (negSucc x) ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } with multIdentLeft {nonneg 2}
integersTimesNotGroup record { +WellDefined = wellDefined ; 0G = (negSucc x) ; inverse = inverse ; +Associative = multAssoc ; identRight = multIdentRight ; identLeft = multIdentLeft ; invLeft = invLeft ; invRight = invRight } | ()

-- TODO: Q is not a group with *Q
-- TODO: Q without 0 is a group with *Q
-- TODO: {1, -1} is a group with *

ℤnIsGroup : (n : ℕ) → (0<n : 0 <N n) → _
ℤnIsGroup n pr = ℤnGroup n pr

-- Groups example 8.9 from lecture 1
data Weird : Set where
  e : Weird
  a : Weird
  b : Weird
  c : Weird

_+W_ : Weird → Weird → Weird
e +W t = t
a +W e = a
a +W a = e
a +W b = c
a +W c = b
b +W e = b
b +W a = c
b +W b = e
b +W c = a
c +W e = c
c +W a = b
c +W b = a
c +W c = e

+WAssoc : {x y z : Weird} → (x +W (y +W z)) ≡ (x +W y) +W z
+WAssoc {e} {y} {z} = refl
+WAssoc {a} {e} {z} = refl
+WAssoc {a} {a} {e} = refl
+WAssoc {a} {a} {a} = refl
+WAssoc {a} {a} {b} = refl
+WAssoc {a} {a} {c} = refl
+WAssoc {a} {b} {e} = refl
+WAssoc {a} {b} {a} = refl
+WAssoc {a} {b} {b} = refl
+WAssoc {a} {b} {c} = refl
+WAssoc {a} {c} {e} = refl
+WAssoc {a} {c} {a} = refl
+WAssoc {a} {c} {b} = refl
+WAssoc {a} {c} {c} = refl
+WAssoc {b} {e} {z} = refl
+WAssoc {b} {a} {e} = refl
+WAssoc {b} {a} {a} = refl
+WAssoc {b} {a} {b} = refl
+WAssoc {b} {a} {c} = refl
+WAssoc {b} {b} {e} = refl
+WAssoc {b} {b} {a} = refl
+WAssoc {b} {b} {b} = refl
+WAssoc {b} {b} {c} = refl
+WAssoc {b} {c} {e} = refl
+WAssoc {b} {c} {a} = refl
+WAssoc {b} {c} {b} = refl
+WAssoc {b} {c} {c} = refl
+WAssoc {c} {e} {z} = refl
+WAssoc {c} {a} {e} = refl
+WAssoc {c} {a} {a} = refl
+WAssoc {c} {a} {b} = refl
+WAssoc {c} {a} {c} = refl
+WAssoc {c} {b} {e} = refl
+WAssoc {c} {b} {a} = refl
+WAssoc {c} {b} {b} = refl
+WAssoc {c} {b} {c} = refl
+WAssoc {c} {c} {e} = refl
+WAssoc {c} {c} {a} = refl
+WAssoc {c} {c} {b} = refl
+WAssoc {c} {c} {c} = refl

weirdGroup : Group (reflSetoid Weird) _+W_
Group.+WellDefined weirdGroup = reflGroupWellDefined
Group.0G weirdGroup = e
Group.inverse weirdGroup t = t
Group.+Associative weirdGroup {r} {s} {t} = +WAssoc {r} {s} {t}
Group.identRight weirdGroup {e} = refl
Group.identRight weirdGroup {a} = refl
Group.identRight weirdGroup {b} = refl
Group.identRight weirdGroup {c} = refl
Group.identLeft weirdGroup {e} = refl
Group.identLeft weirdGroup {a} = refl
Group.identLeft weirdGroup {b} = refl
Group.identLeft weirdGroup {c} = refl
Group.invLeft weirdGroup {e} = refl
Group.invLeft weirdGroup {a} = refl
Group.invLeft weirdGroup {b} = refl
Group.invLeft weirdGroup {c} = refl
Group.invRight weirdGroup {e} = refl
Group.invRight weirdGroup {a} = refl
Group.invRight weirdGroup {b} = refl
Group.invRight weirdGroup {c} = refl

weirdAb : AbelianGroup weirdGroup
AbelianGroup.commutative weirdAb {e} {e} = refl
AbelianGroup.commutative weirdAb {e} {a} = refl
AbelianGroup.commutative weirdAb {e} {b} = refl
AbelianGroup.commutative weirdAb {e} {c} = refl
AbelianGroup.commutative weirdAb {a} {e} = refl
AbelianGroup.commutative weirdAb {a} {a} = refl
AbelianGroup.commutative weirdAb {a} {b} = refl
AbelianGroup.commutative weirdAb {a} {c} = refl
AbelianGroup.commutative weirdAb {b} {e} = refl
AbelianGroup.commutative weirdAb {b} {a} = refl
AbelianGroup.commutative weirdAb {b} {b} = refl
AbelianGroup.commutative weirdAb {b} {c} = refl
AbelianGroup.commutative weirdAb {c} {e} = refl
AbelianGroup.commutative weirdAb {c} {a} = refl
AbelianGroup.commutative weirdAb {c} {b} = refl
AbelianGroup.commutative weirdAb {c} {c} = refl

weirdProjection : Weird → FinSet 4
weirdProjection a = ofNat 0 (le 3 refl)
weirdProjection b = ofNat 1 (le 2 refl)
weirdProjection c = ofNat 2 (le 1 refl)
weirdProjection e = ofNat 3 (le zero refl)

weirdProjectionSurj : Surjection weirdProjection
weirdProjectionSurj fzero = a , refl
weirdProjectionSurj (fsucc fzero) = b , refl
weirdProjectionSurj (fsucc (fsucc fzero)) = c , refl
weirdProjectionSurj (fsucc (fsucc (fsucc fzero))) = e , refl
weirdProjectionSurj (fsucc (fsucc (fsucc (fsucc ()))))

weirdProjectionInj : (x y : Weird) → weirdProjection x ≡ weirdProjection y → Setoid._∼_ (reflSetoid Weird) x y
weirdProjectionInj e e fx=fy = refl
weirdProjectionInj e a ()
weirdProjectionInj e b ()
weirdProjectionInj e c ()
weirdProjectionInj a e ()
weirdProjectionInj a a fx=fy = refl
weirdProjectionInj a b ()
weirdProjectionInj a c ()
weirdProjectionInj b e ()
weirdProjectionInj b a ()
weirdProjectionInj b b fx=fy = refl
weirdProjectionInj b c ()
weirdProjectionInj c e ()
weirdProjectionInj c a ()
weirdProjectionInj c b ()
weirdProjectionInj c c fx=fy = refl

weirdFinite : FiniteGroup weirdGroup (FinSet 4)
SetoidToSet.project (FiniteGroup.toSet weirdFinite) = weirdProjection
SetoidToSet.wellDefined (FiniteGroup.toSet weirdFinite) x y = applyEquality weirdProjection
SetoidToSet.surj (FiniteGroup.toSet weirdFinite) = weirdProjectionSurj
SetoidToSet.inj (FiniteGroup.toSet weirdFinite) = weirdProjectionInj
FiniteSet.size (FiniteGroup.finite weirdFinite) = 4
FiniteSet.mapping (FiniteGroup.finite weirdFinite) = id
FiniteSet.bij (FiniteGroup.finite weirdFinite) = idIsBijective

weirdOrder : groupOrder weirdFinite ≡ 4
weirdOrder = refl

-- TODO: dihedral groups
-- TODO: matrix groups on R
-- TODO: general linear groups on R


text:
-- The empty type; also used as absurd proposition (``Falsity'').

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

module Tools.Empty where

data ⊥ : Set where

-- Ex falsum quod libet.

⊥-elim : ∀ {a} {A : Set a} → ⊥ → A
⊥-elim ()

⊥-elimω : ∀ {A : Agda.Primitive.Setω} → ⊥ → A
⊥-elimω ()

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

-- Natural numbers

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

{-# BUILTIN NATURAL Nat #-}

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

-- Finite sets

data Fin : Nat -> Set where
  fzero : forall {n} ->          Fin (suc n)
  fsuc  : forall {n} -> Fin n -> Fin (suc n)

fin : forall {n} (k : Nat) -> Fin (suc (k + n))
fin zero    = fzero
fin (suc i) = fsuc (fin i)

-- Lists

infixl 0 _,_

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

-- List membership

data LMem {X : Set} (a : X) : List X -> Set where
  lzero : forall {l}               -> LMem a (l , a)
  lsuc  : forall {l b} -> LMem a l -> LMem a (l , b)

-- Vectors

data Vec (X : Set) : Nat -> Set where
  []  :                               Vec X zero
  _,_ : forall {n} -> Vec X n -> X -> Vec X (suc n)

proj : forall {X n} -> Vec X n -> Fin n -> X
proj []      ()
proj (_ , a) fzero    = a
proj (v , _) (fsuc i) = proj v i

-- Vector membership

data VMem {X : Set} (a : X) : forall {n} -> Fin n -> Vec X n -> Set where
  mzero : forall {n}     {v : Vec X n}               -> VMem a fzero    (v , a)
  msuc  : forall {n i b} {v : Vec X n} -> VMem a i v -> VMem a (fsuc i) (v , b)

fmem : forall {X n} -> (i : Fin n) -> {v : Vec X n} -> VMem (proj v i) i v
fmem {_} {zero}  ()
fmem {_} {suc n} fzero    {_ , a} = mzero
fmem {_} {suc n} (fsuc i) {v , _} = msuc (fmem i)

mem : forall {X n} -> (k : Nat) -> {v : Vec X (suc (k + n))} -> VMem (proj v (fin k)) (fin k) v
mem i = fmem (fin i)

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Deep Embedding for Propositional Logic.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula ( n : ℕ ) where

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

open import Data.PropFormula.Dec n         public
open import Data.PropFormula.Properties n  public
open import Data.PropFormula.Syntax n      public
open import Data.PropFormula.Theorems n    public

open import Data.Bool public
  using    ( Bool; true; false; not )
  renaming ( _∧_ to _&&_; _∨_ to _||_ )

open import Data.Fin  public using ( Fin; zero; suc; #_ )
open import Data.List public using ( List; []; _∷_; _++_; [_] )
open import Data.Vec  public using ( Vec; lookup )

open import Function  public using ( _$_ )

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

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
module W where

open import Function using (_∘_)
open import Data.Bool using (Bool; true; false)
open import Data.Product
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)

data W (S : Set) (P : S → Set) : Set where
    max : (s : S) → (f : P s → W S P) → W S P

-- data ℕ : Set where
--     zero : ℕ             _^0
--     succ : ℕ → ℕ        ∣ℕ∣

ℕ : Set
ℕ = W Bool f
    where   f : Bool → Set
            f true = ⊤ -- 1
            f false = ⊥ -- 0

zero : ℕ
zero = max false ⊥-elim

succ : ℕ → ℕ
succ n = max true (λ _ → n)

_+_ : ℕ → ℕ → ℕ
(max true f) + y = max true (λ _ → f tt + y)
(max false f) + y = y

-- data Tree : Set where
--     leaf : Tree                   _^0
--     node : Tree → Tree → Tree    |ℕ| x |ℕ|

Tree : Set
Tree = W Bool λ { true → Bool ; false → ⊥ }

leaf : Tree
leaf = max false ⊥-elim       -- _^0

node : Tree → Tree → Tree
node l r = max true λ { true → l      -- ∣Tree∣^2
                     ; false → r }

data LW (S : Set) (LP : S → Set × Set) : Set where
     lmax : (s : Σ S (proj₁ ∘ LP)) → (proj₂ (LP (proj₁ s)) → LW S LP) → LW S LP

List : (X : Set) → Set
List X = LW Bool (λ { true → X , ⊤      -- cons
                    ; false → ⊤ , ⊥ })  -- nil

nil : {X : Set} → List X
nil = lmax (false , tt) ⊥-elim

cons : {X : Set} → (x : X) → List X → List X
cons {X} x xs = lmax (true , x) λ _ → xs

-- induction principle on W-types
indW : (S : Set)
     → (P : S → Set)
     → (C : W S P → Set)    --  property
     → (c : (s : S)                     -- given a shape
          → (f : P s → W S P)           -- and a bunch of kids
          → (h : (p : P s) → C (f p))   -- if C holds for all kids
          → C (max s f))                -- C holds for (max s f)
     → (x : W S P)
     → C x
indW S P C step (max s f) = step s f (λ p → {!   !} S P C step (f p))

indℕ : (C : ℕ → Set) → C zero → ((n : ℕ) → C n → C (succ n)) → (x : ℕ) → C x
indℕ C base step (max true f) = step (f tt) (indℕ C base step (f tt))
indℕ C base step (max false f) = {! base  !}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
-- Andreas, 2015-07-13  Better parse errors for illegal type signatures

-1 : Set1
-1 = Set


text:
------------------------------------------------------------------------
-- The one-step truncation HIT with an erased higher constructor
------------------------------------------------------------------------

{-# OPTIONS --erased-cubical --safe #-}

-- The module is parametrised by a notion of equality. The higher
-- constructor of the HIT defining the one-step truncation operator
-- uses path equality, but the supplied notion of equality is used for
-- many other things.

import Equality.Path as P

module H-level.Truncation.Propositional.One-step.Erased
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq hiding (elim)

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

open import Bijection equality-with-J using (_↔_)
open import Equality.Decidable-UIP equality-with-J using (Constant)
import Equality.Decidable-UIP P.equality-with-J as PD
open import Equality.Path.Isomorphisms eq
open import Equivalence equality-with-J as Eq using (_≃_)
open import Equivalence.Erased.Cubical eq as EEq using (_≃ᴱ_)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import H-level.Closure equality-with-J
open import Surjection equality-with-J using (_↠_)

private
  variable
    a b p   : Level
    A B     : Type a
    P       : A → Type p
    e r x y : A
    n       : ℕ

------------------------------------------------------------------------
-- The type

-- One-step truncation.
--
-- This definition is based on that in van Doorn's "Constructing the
-- Propositional Truncation using Non-recursive HITs", but has an
-- erased higher constructor.

data ∥_∥¹ᴱ (A : Type a) : Type a where
  ∣_∣             : A → ∥ A ∥¹ᴱ
  @0 ∣∣-constantᴾ : PD.Constant (∣_∣ {A = A})

-- The function ∣_∣ is constant (in erased contexts).

@0 ∣∣-constant : Constant (∣_∣ {A = A})
∣∣-constant x y = _↔_.from ≡↔≡ (∣∣-constantᴾ x y)

------------------------------------------------------------------------
-- Eliminators

-- A dependent eliminator, expressed using paths.

record Elimᴾ {A : Type a} (P : ∥ A ∥¹ᴱ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ             : ∀ x → P ∣ x ∣
    @0 ∣∣-constantʳ :
      (x y : A) →
      P.[ (λ i → P (∣∣-constantᴾ x y i)) ] ∣∣ʳ x ≡ ∣∣ʳ y

open Elimᴾ public

elimᴾ : Elimᴾ P → (x : ∥ A ∥¹ᴱ) → P x
elimᴾ {A = A} {P = P} e = helper
  where
  module E = Elimᴾ e

  helper : (x : ∥ A ∥¹ᴱ) → P x
  helper ∣ x ∣                = E.∣∣ʳ x
  helper (∣∣-constantᴾ x y i) = E.∣∣-constantʳ x y i

-- A non-dependent eliminator, expressed using paths.

record Recᴾ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ             : A → B
    @0 ∣∣-constantʳ : PD.Constant ∣∣ʳ

open Recᴾ public

recᴾ : Recᴾ A B → ∥ A ∥¹ᴱ → B
recᴾ r = elimᴾ λ where
    .∣∣ʳ          → R.∣∣ʳ
    .∣∣-constantʳ → R.∣∣-constantʳ
  where
  module R = Recᴾ r

-- A dependent eliminator.

record Elim {A : Type a} (P : ∥ A ∥¹ᴱ → Type p) : Type (a ⊔ p) where
  no-eta-equality
  field
    ∣∣ʳ             : ∀ x → P ∣ x ∣
    @0 ∣∣-constantʳ :
      (x y : A) → subst P (∣∣-constant x y) (∣∣ʳ x) ≡ ∣∣ʳ y

open Elim public

elim : Elim P → (x : ∥ A ∥¹ᴱ) → P x
elim e = elimᴾ λ where
    .∣∣ʳ              → E.∣∣ʳ
    .∣∣-constantʳ x y → subst≡→[]≡ (E.∣∣-constantʳ x y)
  where
  module E = Elim e

-- A "computation" rule.

@0 elim-∣∣-constant :
  dcong (elim e) (∣∣-constant x y) ≡ Elim.∣∣-constantʳ e x y
elim-∣∣-constant = dcong-subst≡→[]≡ (refl _)

-- A non-dependent eliminator.

record Rec (A : Type a) (B : Type b) : Type (a ⊔ b) where
  no-eta-equality
  field
    ∣∣ʳ             : A → B
    @0 ∣∣-constantʳ : Constant ∣∣ʳ

open Rec public

rec : Rec A B → ∥ A ∥¹ᴱ → B
rec r = recᴾ λ where
    .∣∣ʳ              → R.∣∣ʳ
    .∣∣-constantʳ x y → _↔_.to ≡↔≡ (R.∣∣-constantʳ x y)
  where
  module R = Rec r

-- A "computation" rule.

@0 rec-∣∣-constant :
  cong (rec r) (∣∣-constant x y) ≡ Rec.∣∣-constantʳ r x y
rec-∣∣-constant = cong-≡↔≡ (refl _)

-- A variant of rec.

rec′ : (f : A → B) → @0 Constant f → ∥ A ∥¹ᴱ → B
rec′ f c = rec λ where
  .Rec.∣∣ʳ          → f
  .Rec.∣∣-constantʳ → c

------------------------------------------------------------------------
-- Some preservation lemmas

-- A map function for ∥_∥¹ᴱ.

∥∥¹ᴱ-map : (A → B) → ∥ A ∥¹ᴱ → ∥ B ∥¹ᴱ
∥∥¹ᴱ-map f = rec λ where
  .∣∣ʳ x            → ∣ f x ∣
  .∣∣-constantʳ x y → ∣∣-constant (f x) (f y)

-- The truncation operator preserves logical equivalences.

∥∥¹ᴱ-cong-⇔ : A ⇔ B → ∥ A ∥¹ᴱ ⇔ ∥ B ∥¹ᴱ
∥∥¹ᴱ-cong-⇔ A⇔B = record
  { to   = ∥∥¹ᴱ-map (_⇔_.to   A⇔B)
  ; from = ∥∥¹ᴱ-map (_⇔_.from A⇔B)
  }

private

  -- A lemma used below.

  @0 ∥∥¹ᴱ-cong-lemma :
    (f : A → B) (g : B → A) (eq : ∀ x → f (g x) ≡ x) →
    subst (λ z → ∥∥¹ᴱ-map f (∥∥¹ᴱ-map g z) ≡ z)
      (∣∣-constant x y) (cong ∣_∣ (eq x)) ≡
    cong ∣_∣ (eq y)
  ∥∥¹ᴱ-cong-lemma {x = x} {y = y} f g eq =
    subst
      (λ z → ∥∥¹ᴱ-map f (∥∥¹ᴱ-map g z) ≡ z)
      (∣∣-constant x y) (cong ∣_∣ (eq x))                           ≡⟨ subst-in-terms-of-trans-and-cong ⟩

    trans (sym (cong (∥∥¹ᴱ-map f ∘ ∥∥¹ᴱ-map g) (∣∣-constant x y)))
      (trans (cong ∣_∣ (eq x)) (cong id (∣∣-constant x y)))         ≡⟨ cong₂ (λ p q → trans (sym p) (trans (cong ∣_∣ (eq x)) q))
                                                                         (trans (sym $ cong-∘ _ _ _) $
                                                                          trans (cong (cong (∥∥¹ᴱ-map f)) rec-∣∣-constant) $
                                                                          rec-∣∣-constant)
                                                                         (sym $ cong-id _) ⟩
    trans (sym (∣∣-constant (f (g x)) (f (g y))))
      (trans (cong ∣_∣ (eq x)) (∣∣-constant x y))                   ≡⟨ cong (λ f → trans _ (trans (cong ∣_∣ (f _)) _)) $ sym $
                                                                       _≃_.left-inverse-of (Eq.extensionality-isomorphism bad-ext) eq ⟩
    trans (sym (∣∣-constant (f (g x)) (f (g y))))
      (trans (cong ∣_∣ (ext⁻¹ (⟨ext⟩ eq) x)) (∣∣-constant x y))     ≡⟨ elim₁
                                                                         (λ {f} eq → trans (sym (∣∣-constant (f x) (f y)))
                                                                                (trans (cong ∣_∣ (ext⁻¹ eq x)) (∣∣-constant x y)) ≡
                                                                                cong ∣_∣ (ext⁻¹ eq y))
                                                                         (
      trans (sym (∣∣-constant x y))
        (trans (cong ∣_∣ (ext⁻¹ (refl id) x)) (∣∣-constant x y))          ≡⟨ cong (trans _) $
                                                                             trans (cong (flip trans _) $
                                                                                trans (cong (cong _) $ cong-refl _) $
                                                                                cong-refl _) $
                                                                             trans-reflˡ _ ⟩

      trans (sym (∣∣-constant x y)) (∣∣-constant x y)                     ≡⟨ trans-symˡ _ ⟩

      refl _                                                              ≡⟨ trans (sym $ cong-refl _) $
                                                                             cong (cong _) $ sym $ cong-refl _ ⟩∎
      cong ∣_∣ (ext⁻¹ (refl _) y)                                         ∎)
                                                                         _ ⟩

    cong ∣_∣ (ext⁻¹ (⟨ext⟩ eq) y)                                   ≡⟨ cong (λ f → cong ∣_∣ (f _)) $
                                                                       _≃_.left-inverse-of (Eq.extensionality-isomorphism bad-ext) eq ⟩∎
    cong ∣_∣ (eq y)                                                 ∎

-- The truncation operator preserves split surjections.

∥∥¹ᴱ-cong-↠ : A ↠ B → ∥ A ∥¹ᴱ ↠ ∥ B ∥¹ᴱ
∥∥¹ᴱ-cong-↠ A↠B = record
  { logical-equivalence = ∥∥¹ᴱ-cong-⇔ (_↠_.logical-equivalence A↠B)
  ; right-inverse-of    = elim λ where
      .∣∣ʳ x            → cong ∣_∣ (_↠_.right-inverse-of A↠B x)
      .∣∣-constantʳ x y →
        ∥∥¹ᴱ-cong-lemma (_↠_.to A↠B) (_↠_.from A↠B)
          (_↠_.right-inverse-of A↠B)
  }

-- The truncation operator preserves bijections.

∥∥¹ᴱ-cong-↔ : A ↔ B → ∥ A ∥¹ᴱ ↔ ∥ B ∥¹ᴱ
∥∥¹ᴱ-cong-↔ A↔B = record
  { surjection      = ∥∥¹ᴱ-cong-↠ (_↔_.surjection A↔B)
  ; left-inverse-of = elim λ where
      .∣∣ʳ x            → cong ∣_∣ (_↔_.left-inverse-of A↔B x)
      .∣∣-constantʳ x y →
        ∥∥¹ᴱ-cong-lemma (_↔_.from A↔B) (_↔_.to A↔B)
          (_↔_.left-inverse-of A↔B)
  }

-- The truncation operator preserves equivalences.

∥∥¹ᴱ-cong-≃ : A ≃ B → ∥ A ∥¹ᴱ ≃ ∥ B ∥¹ᴱ
∥∥¹ᴱ-cong-≃ = from-isomorphism ∘ ∥∥¹ᴱ-cong-↔ ∘ from-isomorphism

-- The truncation operator preserves equivalences with erased proofs.

∥∥¹ᴱ-cong-≃ᴱ : A ≃ᴱ B → ∥ A ∥¹ᴱ ≃ᴱ ∥ B ∥¹ᴱ
∥∥¹ᴱ-cong-≃ᴱ A≃B =
  EEq.[≃]→≃ᴱ (EEq.[proofs] (∥∥¹ᴱ-cong-≃ (EEq.≃ᴱ→≃ A≃B)))

------------------------------------------------------------------------
-- Iterated applications of the one-step truncation operator

-- Applies the one-step truncation the given number of times, from the
-- "outside".
--
-- This definition and the next one are taken from van Doorn's
-- "Constructing the Propositional Truncation using Non-recursive
-- HITs".

∥_∥¹ᴱ-out-^ : Type a → ℕ → Type a
∥ A ∥¹ᴱ-out-^ zero    = A
∥ A ∥¹ᴱ-out-^ (suc n) = ∥ ∥ A ∥¹ᴱ-out-^ n ∥¹ᴱ

-- A "constructor" for ∥_∥¹ᴱ-out-^.

∣_∣-out-^ : A → ∀ n → ∥ A ∥¹ᴱ-out-^ n
∣ x ∣-out-^ zero    = x
∣ x ∣-out-^ (suc n) = ∣ ∣ x ∣-out-^ n ∣

-- A rearrangement lemma.

∥∥¹ᴱ-out-^+≃ :
  ∀ m → ∥ A ∥¹ᴱ-out-^ (m + n) ≃ ∥ ∥ A ∥¹ᴱ-out-^ n ∥¹ᴱ-out-^ m
∥∥¹ᴱ-out-^+≃                 zero    = F.id
∥∥¹ᴱ-out-^+≃ {A = A} {n = n} (suc m) =
  ∥ ∥ A ∥¹ᴱ-out-^ (m + n) ∥¹ᴱ          ↝⟨ ∥∥¹ᴱ-cong-≃ (∥∥¹ᴱ-out-^+≃ m) ⟩□
  ∥ ∥ ∥ A ∥¹ᴱ-out-^ n ∥¹ᴱ-out-^ m ∥¹ᴱ  □

-- ∥_∥¹ᴱ commutes with ∥_∥¹ᴱ-out-^ n.

∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute :
  ∀ n → ∥ ∥ A ∥¹ᴱ-out-^ n ∥¹ᴱ ↔ ∥ ∥ A ∥¹ᴱ ∥¹ᴱ-out-^ n
∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute         zero    = F.id
∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute {A = A} (suc n) =
  ∥ ∥ ∥ A ∥¹ᴱ-out-^ n ∥¹ᴱ ∥¹ᴱ  ↝⟨ ∥∥¹ᴱ-cong-↔ (∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute n) ⟩□
  ∥ ∥ ∥ A ∥¹ᴱ ∥¹ᴱ-out-^ n ∥¹ᴱ  □

private

  -- The lemma above is defined using _↔_ rather than _≃_ because the
  -- following equalities hold by definition when _↔_ is used, but (at
  -- the time of writing) the second one does not hold when _≃_ is
  -- used.

  _ :
    {x : A} →
    _↔_.left-inverse-of (∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute 0) ∣ x ∣ ≡ refl ∣ x ∣
  _ = refl _

  _ :
    {A : Type a} {x : ∥ A ∥¹ᴱ-out-^ (suc n)} →
    _↔_.left-inverse-of (∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute (1 + n)) ∣ x ∣ ≡
    cong ∣_∣ (_↔_.left-inverse-of (∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute n) x)
  _ = refl _

-- A variant of ∥_∥¹ᴱ-out-^ which applies the one-step truncation the
-- given number of times from the "inside".

∥_∥¹ᴱ-in-^ : Type a → ℕ → Type a
∥ A ∥¹ᴱ-in-^ zero    = A
∥ A ∥¹ᴱ-in-^ (suc n) = ∥ ∥ A ∥¹ᴱ ∥¹ᴱ-in-^ n

-- The two variants of ∥_∥¹ᴱ^ are pointwise equivalent.

∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ : ∀ n → ∥ A ∥¹ᴱ-out-^ n ≃ ∥ A ∥¹ᴱ-in-^ n
∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^         zero    = F.id
∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ {A = A} (suc n) =
  ∥ ∥ A ∥¹ᴱ-out-^ n ∥¹ᴱ  ↔⟨ ∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute n ⟩
  ∥ ∥ A ∥¹ᴱ ∥¹ᴱ-out-^ n  ↝⟨ ∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ n ⟩□
  ∥ ∥ A ∥¹ᴱ ∥¹ᴱ-in-^ n   □

-- ∥_∥¹ᴱ commutes with ∥_∥¹ᴱ-in-^ n.

∥∥¹ᴱ-∥∥¹ᴱ-in-^-commute : ∀ n → ∥ ∥ A ∥¹ᴱ-in-^ n ∥¹ᴱ ≃ ∥ ∥ A ∥¹ᴱ ∥¹ᴱ-in-^ n
∥∥¹ᴱ-∥∥¹ᴱ-in-^-commute {A = A} n =
  ∥ ∥ A ∥¹ᴱ-in-^ n ∥¹ᴱ   ↝⟨ ∥∥¹ᴱ-cong-≃ (inverse $ ∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ n) ⟩
  ∥ ∥ A ∥¹ᴱ-out-^ n ∥¹ᴱ  ↔⟨⟩
  ∥ A ∥¹ᴱ-out-^ (suc n)  ↝⟨ ∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ (suc n) ⟩
  ∥ A ∥¹ᴱ-in-^ (suc n)   ↔⟨⟩
  ∥ ∥ A ∥¹ᴱ ∥¹ᴱ-in-^ n   □

-- A "constructor" for ∥_∥¹ᴱ-in-^.

∣_,_∣-in-^ : ∀ n → ∥ A ∥¹ᴱ-in-^ n → ∥ A ∥¹ᴱ-in-^ (suc n)
∣ zero  , x ∣-in-^ = ∣ x ∣
∣ suc n , x ∣-in-^ = ∣ n , x ∣-in-^

-- ∣_,_∣-in-^ is related to ∣_∣.

∣∣≡∣,∣-in-^ :
  ∀ n {x : ∥ A ∥¹ᴱ-out-^ n} →
  _≃_.to (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ (suc n)) ∣ x ∣ ≡
  ∣ n , _≃_.to (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ n) x ∣-in-^
∣∣≡∣,∣-in-^ zero    {x = x} = ∣ x ∣  ∎
∣∣≡∣,∣-in-^ (suc n) {x = x} =
  _≃_.to (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ (2 + n)) ∣ x ∣            ≡⟨⟩

  _≃_.to (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ (1 + n))
    ∣ _↔_.to (∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute n) x ∣             ≡⟨ ∣∣≡∣,∣-in-^ n ⟩∎

  ∣ n , _≃_.to (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ n)
          (_↔_.to (∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute n) x) ∣-in-^  ∎

-- A variant of ∣∣≡∣,∣-in-^.

∣,∣-in-^≡∣∣ :
  ∀ n {x : ∥ A ∥¹ᴱ-in-^ n} →
  _≃_.from (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ (suc n)) ∣ n , x ∣-in-^ ≡
  ∣ _≃_.from (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ n) x ∣
∣,∣-in-^≡∣∣ zero    {x = x} = ∣ x ∣  ∎
∣,∣-in-^≡∣∣ (suc n) {x = x} =
  _≃_.from (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ (2 + n)) ∣ 1 + n , x ∣-in-^  ≡⟨⟩

  _↔_.from (∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute (1 + n))
    (_≃_.from (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ (1 + n)) ∣ n , x ∣-in-^)  ≡⟨ cong (_↔_.from (∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute (1 + n))) $ ∣,∣-in-^≡∣∣ n ⟩∎

  _↔_.from (∥∥¹ᴱ-∥∥¹ᴱ-out-^-commute (1 + n))
    ∣ _≃_.from (∥∥¹ᴱ-out-^≃∥∥¹ᴱ-in-^ n) x ∣                   ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --universe-polymorphism #-}
module Coind where

open import Common.IO
open import Common.Level
open import Common.Nat
open import Common.Unit
open import Common.Coinduction renaming (♯_ to sharp; ♭ to flat)

{-
infix 1000 sharp_

postulate
  Infinity  : ∀ {a} (A : Set a) → Set a
  sharp_ : ∀ {a} {A : Set a} → A → Infinity A
  flat  : ∀ {a} {A : Set a} → Infinity A → A

{-# BUILTIN INFINITY Infinity  #-}
{-# BUILTIN SHARP    sharp_ #-}
{-# BUILTIN FLAT     flat  #-}
-}

data Stream (A : Set) : Set where
  _::_ : (x : A) (xs : ∞ (Stream A)) → Stream A

ones : Stream Nat
ones = 1 :: (sharp ones)

twos : Stream Nat
twos = 2 :: (sharp twos)

incr : Nat -> Stream Nat
incr n = n :: (sharp (incr (n + 1)))

printStream : Nat -> Stream Nat -> IO Unit
printStream zero _ = putStrLn ""
printStream (suc steps) (n :: ns) =
    printNat n ,,
    printStream steps (flat ns)

main : IO Unit
main =
    printStream 10 twos ,,
    printStream 10 ones ,,
    printStream 10 (incr zero)


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Definition of Bool datatype, which represents logical true and   --
-- false.                                                           --
----------------------------------------------------------------------

module Basics.Bool where

data Bool : Set where
  false : Bool
  true  : Bool

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decidable propositional membership over lists
------------------------------------------------------------------------

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

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

module Data.List.Membership.DecPropositional
  {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) where

------------------------------------------------------------------------
-- Re-export contents of propositional membership

open import Data.List.Membership.Propositional {A = A} public
open import Data.List.Membership.DecSetoid (decSetoid _≟_) public
  using (_∈?_)


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

open import Data.Product using (_,_)

open import Cats.Category
open import Cats.Category.Fun as Fun using (_↝_)
open import Cats.Category.Constructions.Product using (HasBinaryProducts)
open import Cats.Functor using (Functor)
open import Cats.Trans using (Trans)

import Cats.Category.Fun.Facts.Terminal as Terminal

open Functor
open Trans

module Build {lo la l≈ lo′ la′ l≈′}
  (C : Category lo la l≈) (D : Category lo′ la′ l≈′)
  {{D× : HasBinaryProducts D}}
  where

  infixr 2 _×_ _×′_ ⟨_,_⟩

  private
    module D = Category D
    module D× = HasBinaryProducts D×
    open D.≈
    open Category (C ↝ D)

  _×_ : (F G : Obj) → Obj
  F × G = record
    { fobj = λ c → fobj F c D×.× fobj G c
    ; fmap = λ f → D×.⟨ fmap F f × fmap G f ⟩
    ; fmap-resp = λ f≈g → D×.⟨×⟩-resp (fmap-resp F f≈g) (fmap-resp G f≈g)
    ; fmap-id = trans (D×.⟨×⟩-resp (fmap-id F) (fmap-id G)) D×.⟨×⟩-id
    ; fmap-∘ = trans D×.⟨×⟩-∘ (D×.⟨×⟩-resp (fmap-∘ F) (fmap-∘ G))
    }

  projl : ∀ {F G} → F × G ⇒ F
  projl = record
    { component = λ c → D×.projl
    ; natural = D×.⟨×⟩-projl
    }

  projr : ∀ {F G} → F × G ⇒ G
  projr = record
    { component = λ c → D×.projr
    ; natural = D×.⟨×⟩-projr
    }

  ⟨_,_⟩ : ∀ {F G X} → X ⇒ F → X ⇒ G → X ⇒ F × G
  ⟨_,_⟩ α β = record
    { component = λ c → D×.⟨ component α c , component β c ⟩
    ; natural = λ {c} {d} {f} →
        trans D×.⟨,⟩-∘
          (trans (D×.⟨,⟩-resp (natural α) (natural β))
            (sym D×.⟨×⟩-⟨,⟩))
    }

  ⟨,⟩-projl : ∀ {F G X} {α : X ⇒ F} (β : X ⇒ G)
    → α ≈ projl ∘ ⟨ α , β ⟩
  ⟨,⟩-projl β = Fun.≈-intro (sym D×.⟨,⟩-projl)

  ⟨,⟩-projr : ∀ {F G X} (α : X ⇒ F) {β : X ⇒ G}
    → β ≈ projr ∘ ⟨ α , β ⟩
  ⟨,⟩-projr α = Fun.≈-intro (sym D×.⟨,⟩-projr)

  ⟨,⟩-unique : ∀ {F G X} {α : X ⇒ F} {β : X ⇒ G} {u}
    → α ≈ projl ∘ u
    → β ≈ projr ∘ u
    → ⟨ α , β ⟩ ≈ u
  ⟨,⟩-unique (Fun.≈-intro pl) (Fun.≈-intro pr)
    = Fun.≈-intro (D×.⟨,⟩-unique pl pr)

  isBinaryProduct : ∀ {F G} → IsBinaryProduct (F × G) projl projr
  isBinaryProduct α β = record
    { arr = ⟨ α , β ⟩
    ; prop = (⟨,⟩-projl β , ⟨,⟩-projr α)
    ; unique = λ { (eql , eqr) → ⟨,⟩-unique eql eqr }
    }

  _×′_ : (F G : Obj) → BinaryProduct F G
  F ×′ G = mkBinaryProduct projl projr isBinaryProduct

private
  open module Build′ {lo la l≈ lo′ la′ l≈′}
    {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
    = Build C D
    public

instance
  hasBinaryProducts : ∀ {lo la l≈ lo′ la′ l≈′}
    → {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
    → {{D× : HasBinaryProducts D}}
    → HasBinaryProducts (C ↝ D)
  hasBinaryProducts = record { _×′_ = _×′_ }

  hasFiniteProducts : ∀ {lo la l≈ lo′ la′ l≈′}
    → {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
    → {{D× : HasFiniteProducts D}}
    → HasFiniteProducts (C ↝ D)
  hasFiniteProducts = record { hasTerminal = Terminal.hasTerminal }
                      -- record {} doesn't work for some reason.

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats