text:
open import Nat
open import Prelude
open import List
open import judgemental-erase
open import lemmas-matching
open import statics-core
open import synth-unicity

module moveerase where
  -- type actions don't change the term other than moving the cursor
  -- around
  moveeraset : {t t' : ztyp} {δ : direction} →
               (t + move δ +> t') →
               (t ◆t) == (t' ◆t)
  moveeraset TMArrChild1 = refl
  moveeraset TMArrChild2 = refl
  moveeraset TMArrParent1 = refl
  moveeraset TMArrParent2 = refl
  moveeraset (TMArrZip1 {t2 = t2} m) = ap1 (λ x → x ==> t2) (moveeraset m)
  moveeraset (TMArrZip2 {t1 = t1} m) = ap1 (λ x → t1 ==> x) (moveeraset m)
  moveeraset TMPlusChild1 = refl
  moveeraset TMPlusChild2 = refl
  moveeraset TMPlusParent1 = refl
  moveeraset TMPlusParent2 = refl
  moveeraset (TMPlusZip1 {t2 = t2} m) = ap1 (λ x → x ⊕ t2) (moveeraset m)
  moveeraset (TMPlusZip2 {t1 = t1} m) = ap1 (λ x → t1 ⊕ x) (moveeraset m)
  moveeraset TMProdChild1 = refl
  moveeraset TMProdChild2 = refl
  moveeraset TMProdParent1 = refl
  moveeraset TMProdParent2 = refl
  moveeraset (TMProdZip1 {t2 = t2} m) = ap1 (λ x → x ⊠ t2) (moveeraset m)
  moveeraset (TMProdZip2 {t1 = t1} m) = ap1 (λ x → t1 ⊠ x) (moveeraset m)

  -- the actual movements don't change the erasure
  moveerase : {e e' : zexp} {δ : direction} →
              (e + move δ +>e e') →
              (e ◆e) == (e' ◆e)
  moveerase EMAscChild1 = refl
  moveerase EMAscChild2 = refl
  moveerase EMAscParent1 = refl
  moveerase EMAscParent2 = refl
  moveerase EMLamChild1 = refl
  moveerase EMLamParent = refl
  moveerase EMHalfLamChild1 = refl
  moveerase EMHalfLamChild2 = refl
  moveerase EMHalfLamParent1 = refl
  moveerase EMHalfLamParent2 = refl
  moveerase EMPlusChild1 = refl
  moveerase EMPlusChild2 = refl
  moveerase EMPlusParent1 = refl
  moveerase EMPlusParent2 = refl
  moveerase EMApChild1 = refl
  moveerase EMApChild2 = refl
  moveerase EMApParent1 = refl
  moveerase EMApParent2 = refl
  moveerase EMNEHoleChild1 = refl
  moveerase EMNEHoleParent = refl
  moveerase EMInlChild1 = refl
  moveerase EMInlParent = refl
  moveerase EMInrChild1 = refl
  moveerase EMInrParent = refl
  moveerase EMCaseParent1 = refl
  moveerase EMCaseParent2 = refl
  moveerase EMCaseParent3 = refl
  moveerase EMCaseChild1 = refl
  moveerase EMCaseChild2 = refl
  moveerase EMCaseChild3 = refl
  moveerase EMPairChild1 = refl
  moveerase EMPairChild2 = refl
  moveerase EMPairParent1 = refl
  moveerase EMPairParent2 = refl
  moveerase EMFstChild1 = refl
  moveerase EMFstParent = refl
  moveerase EMSndChild1 = refl
  moveerase EMSndParent = refl

  -- this form is essentially the same as above, but for judgemental
  -- erasure, which is sometimes more convenient.
  moveerasee' : {e e' : zexp} {e◆ : hexp} {δ : direction} →
                erase-e e e◆ →
                e + move δ +>e e' →
                erase-e e' e◆
  moveerasee' er1 m with erase-e◆ er1
  ... | refl = ◆erase-e _ _ (! (moveerase m))

  moveeraset' : ∀{t t◆ t'' δ} →
                erase-t t t◆ →
                t + move δ +> t'' →
                erase-t t'' t◆
  moveeraset' er m with erase-t◆ er
  moveeraset' er m | refl = ◆erase-t _ _ (! (moveeraset m))

  -- movements don't change either the type or expression under expression
  -- actions
  mutual
    moveerase-synth : ∀{Γ e e' e◆ t t' δ } →
                      erase-e e e◆ →
                      Γ ⊢ e◆ => t →
                      Γ ⊢ e => t ~ move δ ~> e' => t' →
                      (e ◆e) == (e' ◆e) × t == t'
    moveerase-synth er wt (SAMove x) = moveerase x , refl
    moveerase-synth (EEPlusL er) (SPlus x x₁) (SAZipPlus1 x₂) =
      ap1 (λ q → q ·+ _) (moveerase-ana er x x₂)  , refl
    moveerase-synth (EEPlusR er) (SPlus x x₁) (SAZipPlus2 x₂) =
      ap1 (λ q → _ ·+ q) (moveerase-ana er x₁ x₂) , refl
    moveerase-synth (EEAscL er) (SAsc x) (SAZipAsc1 x₁) =
      ap1 (λ q → q ·: _) (moveerase-ana er x x₁) , refl
    moveerase-synth er wt (SAZipAsc2 x x₁ x₂ x₃)
      with moveeraset x
    ... | qq = ap1 (λ q → _ ·: q) qq , eq-ert-trans qq x₂ x₁
    moveerase-synth (EEHalfLamL x) (SLam x₁ wt) (SAZipLam1 x₂ x₃ x₄ x₅ x₆ x₇)
      with erase-t◆ x₃
    ... | refl with erase-t◆ x₄
    ... | refl with moveeraset x₅
    ... | qq rewrite qq with synthunicity x₇ x₆
    ... | refl = refl , refl
    moveerase-synth (EEHalfLamR er) (SLam x wt) (SAZipLam2 x₁ x₂ x₃ x₄)
      with moveerase-synth x₂ x₃ x₄
    ... | qq , refl rewrite qq = refl , refl
    moveerase-synth (EEApL er) (SAp wt x x₁) (SAZipApArr x₂ x₃ x₄ d x₅)
      with erasee-det x₃ er
    ... | refl with synthunicity wt x₄
    ... | refl with moveerase-synth er x₄ d
    ... | pp , refl with ▸arr-unicity x x₂
    ... | refl = (ap1 (λ q → q ∘ _) pp ) , refl
    moveerase-synth (EEApR er) (SAp wt x x₁) (SAZipApAna x₂ x₃ x₄)
      with synthunicity x₃ wt
    ... | refl with ▸arr-unicity x x₂
    ... | refl = ap1 (λ q → _ ∘ q)  (moveerase-ana er x₁ x₄ ) , refl
    moveerase-synth er wt (SAZipNEHole x x₁ d) =
      ap1 ⦇⌜_⌟⦈[ _ ] (π1 (moveerase-synth x x₁ d)) , refl
    moveerase-synth er wt (SAZipPair1 x x₁ x₂ x₃) with moveerase-synth x x₁ x₂
    ... | π1 , refl = (ap1 (λ q → ⟨ q , _ ⟩) π1) , refl
    moveerase-synth er wt (SAZipPair2 x x₁ x₂ x₃) with moveerase-synth x₁ x₂ x₃
    ... | π1 , refl = (ap1 (λ q → ⟨ _ , q ⟩) π1) , refl
    moveerase-synth er wt (SAZipFst x x₁ x₂ x₃ x₄)
      with moveerase-synth x₂ x₃ x₄
    ... | π1 , refl with ▸prod-unicity x₁ x
    ... | refl = (ap1 fst π1) , refl
    moveerase-synth er wt (SAZipSnd x x₁ x₂ x₃ x₄)
      with moveerase-synth x₂ x₃ x₄
    ... | π1 , refl with ▸prod-unicity x₁ x
    ... | refl = (ap1 snd π1) , refl

    moveerase-ana : ∀{Γ e e' e◆ t δ } →
                    erase-e e e◆ →
                    Γ ⊢ e◆ <= t →
                    Γ ⊢ e ~ move δ ~> e' ⇐ t →
                    (e ◆e) == (e' ◆e)
    moveerase-ana er wt (AASubsume x x₁ x₂ x₃) = π1 (moveerase-synth x x₁ x₂)
    moveerase-ana er wt (AAMove x) = moveerase x
    moveerase-ana (EELam er) (ASubsume () x₂) _
    moveerase-ana (EELam er) (ALam x₁ x₂ wt) (AAZipLam x₃ x₄ d) with ▸arr-unicity x₂ x₄
    ... | refl =  ap1 (λ q → ·λ _ q) (moveerase-ana er wt d)
    moveerase-ana (EEInl er) (ASubsume () x₁) (AAZipInl x₂ d)
    moveerase-ana (EEInl er) (AInl x wt) (AAZipInl x₁ d) with ▸sum-unicity x x₁
    ... | refl =  ap1 inl (moveerase-ana er wt d)
    moveerase-ana (EEInr er) (ASubsume () x₁) (AAZipInr x₂ d)
    moveerase-ana (EEInr er) (AInr x wt) (AAZipInr x₁ d) with ▸sum-unicity x x₁
    ... | refl = ap1 inr (moveerase-ana er wt d)
    moveerase-ana er wt (AAZipCase1 x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈) =
      ap1 (λ q → case q _ _ _ _) (π1(moveerase-synth x₃ x₄ x₅))
    moveerase-ana (EECase2 er) (ASubsume () x₂) (AAZipCase2 x₃ x₄ x₅ x₆ d)
    moveerase-ana (EECase2 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) (AAZipCase2 x₅ x₆ x₇ x₈ d)
      with synthunicity x₄ x₇
    ... | refl with ▸sum-unicity x₃ x₈
    ... | refl = ap1 (λ q → case _ _ q _ _) (moveerase-ana er wt d)
    moveerase-ana (EECase3 er) (ASubsume () x₂) (AAZipCase3 x₃ x₄ x₅ x₆ d)
    moveerase-ana (EECase3 er) (ACase x₁ x₂ x₃ x₄ wt wt₁) (AAZipCase3 x₅ x₆ x₇ x₈ d)
      with synthunicity x₄ x₇
    ... | refl with ▸sum-unicity x₃ x₈
    ... | refl = ap1 (λ q → case _ _ _ _ q) (moveerase-ana er wt₁ d)

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some code related to indexed AVL trees that relies on the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

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

module Data.AVL.Indexed.WithK
       {k r} (Key : Set k) {_<_ : Rel Key r}
       (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder }

open import Data.Product
open import Data.AVL.Indexed strictTotalOrder as AVL hiding (Value)

module _ {v} {V′ : Key → Set v} where

  private
    V : AVL.Value v
    V = AVL.MkValue V′ (subst V′)

  node-injectiveˡ : ∀ {hˡ hʳ h l u k}
    {lk₁ : Tree V l [ proj₁ k ] hˡ} {lk₂ : Tree V l [ proj₁ k ] hˡ}
    {ku₁ : Tree V [ proj₁ k ] u hʳ} {ku₂ : Tree V [ proj₁ k ] u hʳ}
    {bal₁ bal₂ : hˡ ∼ hʳ ⊔ h} →
    node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → lk₁ ≡ lk₂
  node-injectiveˡ refl = refl

  node-injectiveʳ : ∀ {hˡ hʳ h l u k}
    {lk₁ : Tree V l [ proj₁ k ] hˡ} {lk₂ : Tree V l [ proj₁ k ] hˡ}
    {ku₁ : Tree V [ proj₁ k ] u hʳ} {ku₂ : Tree V [ proj₁ k ] u hʳ}
    {bal₁ bal₂ : hˡ ∼ hʳ ⊔ h} →
    node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → ku₁ ≡ ku₂
  node-injectiveʳ refl = refl

  node-injective-bal : ∀ {hˡ hʳ h l u k}
    {lk₁ : Tree V l [ proj₁ k ] hˡ} {lk₂ : Tree V l [ proj₁ k ] hˡ}
    {ku₁ : Tree V [ proj₁ k ] u hʳ} {ku₂ : Tree V [ proj₁ k ] u hʳ}
    {bal₁ bal₂ : hˡ ∼ hʳ ⊔ h} →
    node k lk₁ ku₁ bal₁ ≡ node k lk₂ ku₂ bal₂ → bal₁ ≡ bal₂
  node-injective-bal refl = refl

ext: agda


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

open import Cubical.Algebra.Semigroup.Base public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


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

open import lib.Basics
open import lib.NType2
open import lib.types.Empty
open import lib.types.Group
open import lib.types.Int
open import lib.types.List
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Sigma

module lib.types.Word {i} where

module _ (A : Type i) where

  PlusMinus : Type i
  PlusMinus = Coprod A A

  Word : Type i
  Word = List PlusMinus

module _ {A : Type i} where

  flip : PlusMinus A → PlusMinus A
  flip (inl a) = inr a
  flip (inr a) = inl a

  flip-flip : ∀ x → flip (flip x) == x
  flip-flip (inl x) = idp
  flip-flip (inr x) = idp

  Word-flip : Word A → Word A
  Word-flip = map flip

  Word-flip-flip : ∀ w → Word-flip (Word-flip w) == w
  Word-flip-flip nil = idp
  Word-flip-flip (x :: l) = ap2 _::_ (flip-flip x) (Word-flip-flip l)

  Word-inverse : Word A → Word A
  Word-inverse = reverse ∘ Word-flip

  Word-inverse-inverse : ∀ w → Word-inverse (Word-inverse w) == w
  Word-inverse-inverse w =
    Word-inverse (Word-inverse w)
      =⟨ reverse-map flip (Word-inverse w) ⟩
    Word-flip (reverse (reverse (Word-flip w)))
      =⟨ ap Word-flip (reverse-reverse (Word-flip w)) ⟩
    Word-flip (Word-flip w)
      =⟨ Word-flip-flip w ⟩
    w =∎

  Word-exp : A → ℤ → Word A
  Word-exp a (pos 0) = nil
  Word-exp a (pos (S n)) = inl a :: Word-exp a (pos n)
  Word-exp a (negsucc 0) = inr a :: nil
  Word-exp a (negsucc (S n)) = inr a :: Word-exp a (negsucc n)

module _ {A : Type i} {j} (G : Group j) where
  private
    module G = Group G

  module _ (f : A → G.El) where
    PlusMinus-extendᴳ : PlusMinus A → G.El
    PlusMinus-extendᴳ (inl a) = f a
    PlusMinus-extendᴳ (inr a) = G.inv (f a)

    PlusMinus-extendᴳ-flip : ∀ x → PlusMinus-extendᴳ (flip x) == G.inv (PlusMinus-extendᴳ x)
    PlusMinus-extendᴳ-flip (inl a) = idp
    PlusMinus-extendᴳ-flip (inr a) = ! (G.inv-inv (f a))

    Word-extendᴳ : Word A → G.El
    Word-extendᴳ = foldr' G.comp G.ident ∘ map PlusMinus-extendᴳ

  abstract
    Word-extendᴳ-++ : ∀ f l₁ l₂
      → Word-extendᴳ f (l₁ ++ l₂) == G.comp (Word-extendᴳ f l₁) (Word-extendᴳ f l₂)
    Word-extendᴳ-++ f nil l₂ = ! $ G.unit-l _
    Word-extendᴳ-++ f (x₁ :: nil) nil = ! (G.unit-r _)
    Word-extendᴳ-++ f (x₁ :: nil) (x₂ :: l₂) = idp
    Word-extendᴳ-++ f (x₁ :: l₁@(_ :: _)) l₂ =
      G.comp (PlusMinus-extendᴳ f x₁) (Word-extendᴳ f (l₁ ++ l₂))
        =⟨ ap (G.comp (PlusMinus-extendᴳ f x₁)) (Word-extendᴳ-++ f l₁ l₂) ⟩
      G.comp (PlusMinus-extendᴳ f x₁) (G.comp (Word-extendᴳ f l₁) (Word-extendᴳ f l₂))
        =⟨ ! (G.assoc _ _ _) ⟩
      G.comp (G.comp (PlusMinus-extendᴳ f x₁) (Word-extendᴳ f l₁)) (Word-extendᴳ f l₂) =∎

module _ {A : Type i} {j} (G : AbGroup j) where
  private
    module G = AbGroup G

  abstract
    PlusMinus-extendᴳ-comp : ∀ (f g : A → G.El) x
      → PlusMinus-extendᴳ G.grp (λ a → G.comp (f a) (g a)) x
      == G.comp (PlusMinus-extendᴳ G.grp f x) (PlusMinus-extendᴳ G.grp g x)
    PlusMinus-extendᴳ-comp f g (inl a) = idp
    PlusMinus-extendᴳ-comp f g (inr a) = G.inv-comp (f a) (g a) ∙ G.comm (G.inv (g a)) (G.inv (f a))

    Word-extendᴳ-comp : ∀ (f g : A → G.El) l
      → Word-extendᴳ G.grp (λ a → G.comp (f a) (g a)) l
      == G.comp (Word-extendᴳ G.grp f l) (Word-extendᴳ G.grp g l)
    Word-extendᴳ-comp f g nil = ! (G.unit-l G.ident)
    Word-extendᴳ-comp f g (x :: nil) = PlusMinus-extendᴳ-comp f g x
    Word-extendᴳ-comp f g (x :: l@(_ :: _)) =
      G.comp (PlusMinus-extendᴳ G.grp (λ a → G.comp (f a) (g a)) x)
             (Word-extendᴳ G.grp (λ a → G.comp (f a) (g a)) l)
        =⟨ ap2 G.comp (PlusMinus-extendᴳ-comp f g x) (Word-extendᴳ-comp f g l) ⟩
      G.comp (G.comp (PlusMinus-extendᴳ G.grp f x) (PlusMinus-extendᴳ G.grp g x))
             (G.comp (Word-extendᴳ G.grp f l) (Word-extendᴳ G.grp g l))
        =⟨ G.interchange (PlusMinus-extendᴳ G.grp f x) (PlusMinus-extendᴳ G.grp g x)
                         (Word-extendᴳ G.grp f l) (Word-extendᴳ G.grp g l) ⟩
      G.comp (G.comp (PlusMinus-extendᴳ G.grp f x) (Word-extendᴳ G.grp f l))
             (G.comp (PlusMinus-extendᴳ G.grp g x) (Word-extendᴳ G.grp g l)) =∎

module RelationRespectingFunctions (A : Type i) {m} (R : Rel (Word A) m) {j} (G : Group j) where

  private
    module G = Group G

  respects-rel : (A → G.El) → Type (lmax (lmax i j) m)
  respects-rel f = ∀ {l₁ l₂} → R l₁ l₂ → Word-extendᴳ G f l₁ == Word-extendᴳ G f l₂

  abstract
    respects-rel-is-prop : ∀ f → is-prop (respects-rel f)
    respects-rel-is-prop f =
      Πi-level $ λ l₁ →
      Πi-level $ λ l₂ →
      Π-level  $ λ r →
      has-level-apply G.El-level _ _

  record RelationRespectingFunction : Type (lmax (lmax i j) m) where
    constructor rel-res-fun
    field
      f : A → G.El
      respects : respects-rel f

  RelationRespectingFunction= : {lf lg : RelationRespectingFunction}
    → RelationRespectingFunction.f lf == RelationRespectingFunction.f lg
    → lf == lg
  RelationRespectingFunction= {rel-res-fun f f-respect} {rel-res-fun .f g-respect} idp =
    ap (rel-res-fun f) (prop-path (respects-rel-is-prop f) f-respect g-respect)

{- For the empty relation, this is exactly the type of functions -}
module _ (A : Type i) {j} (G : Group j) where

  private
    module G = Group G
  open RelationRespectingFunctions A empty-rel G

  every-function-respects-empty-rel : ∀ (f : A → G.El) → RelationRespectingFunction
  every-function-respects-empty-rel f = rel-res-fun f (λ {_} {_} ())

  every-function-respects-empty-rel-equiv : (A → G.El) ≃ RelationRespectingFunction
  every-function-respects-empty-rel-equiv =
    equiv every-function-respects-empty-rel
          RelationRespectingFunction.f
          (λ lf → RelationRespectingFunction= idp)
          (λ f → idp)

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

open import HoTT
open import cw.CW
open import cw.FinCW
open import cw.FinBoundary
open import cohomology.Theory
open import cohomology.ChainComplex

module cw.cohomology.ReconstructedCochainsEquivCellularCochains
  (OT : OrdinaryTheory lzero) where

  open OrdinaryTheory OT
  open import cw.cohomology.cellular.ChainComplex as CCC
  open import cw.cohomology.reconstructed.cochain.Complex OT as RCC
  open import cw.cohomology.ReconstructedCochainsIsoCellularCochains OT
  open import cw.cohomology.cochainequiv.AugmentCommSquare OT
  open import cw.cohomology.cochainequiv.FirstCoboundaryCommSquare OT
  open import cw.cohomology.cochainequiv.HigherCoboundaryCommSquare OT

  private
    frcc-comm-fccc-Type : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n)
      {m} (m≤n? : Dec (m ≤ n)) (Sm≤n? : Dec (S m ≤ n))
      (coboundary : AbGroup.grp (RCC.cochain-template ⊙⦉ ⊙fin-skel ⦊ m≤n?)
                 →ᴳ AbGroup.grp (RCC.cochain-template ⊙⦉ ⊙fin-skel ⦊ Sm≤n?))
      (boundary : AbGroup.grp (CCC.chain-template ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊ Sm≤n?)
               →ᴳ AbGroup.grp (CCC.chain-template ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊ m≤n?))
      → Type₀
    frcc-comm-fccc-Type {n} ⊙fin-skel {m} m≤n? Sm≤n? coboundary boundary =
      CommSquareᴳ
        coboundary
        (pre∘ᴳ-hom (C2-abgroup 0) boundary)
        (GroupIso.f-hom (rcc-iso-ccc-template ⊙⦉ ⊙fin-skel ⦊ m≤n?
          (⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero)))
        (GroupIso.f-hom (rcc-iso-ccc-template ⊙⦉ ⊙fin-skel ⦊ Sm≤n?
          (⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero)))

    CCC-boundary-template' : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n)
      → {m : ℕ} (m≤n? : Dec (m ≤ n)) (Sm≤n? : Dec (S m ≤ n))
      →  AbGroup.grp (CCC.chain-template ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊ Sm≤n?)
      →ᴳ AbGroup.grp (CCC.chain-template ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊ m≤n?)
    CCC-boundary-template' ⊙fin-skel =
      CCC.boundary-template ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
        (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
        (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))

    RCC-coboundary-template' : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n)
      → {m : ℕ} (m≤n? : Dec (m ≤ n)) (Sm≤n? : Dec (S m ≤ n))
      →  AbGroup.grp (RCC.cochain-template ⊙⦉ ⊙fin-skel ⦊ m≤n?)
      →ᴳ AbGroup.grp (RCC.cochain-template ⊙⦉ ⊙fin-skel ⦊ Sm≤n?)
    RCC-coboundary-template' ⊙fin-skel = RCC.coboundary-template ⊙⦉ ⊙fin-skel ⦊

    abstract
      {- This can be directly generalized to the non-finite cases. -}
      frcc-comm-fccc-above : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n)
          {m} (m≤n? : Dec (m ≤ n)) (Sm≰n : ¬ (S m ≤ n))
        → frcc-comm-fccc-Type ⊙fin-skel m≤n? (inr Sm≰n)
            (RCC-coboundary-template' ⊙fin-skel m≤n? (inr Sm≰n))
            (CCC-boundary-template' ⊙fin-skel m≤n? (inr Sm≰n))
      frcc-comm-fccc-above ⊙fin-skel m≤n? Sm≰n =
        (comm-sqrᴳ λ g → group-hom= $ λ= λ _ →
          ! $ GroupHom.pres-ident
            (GroupIso.f
              (rcc-iso-ccc-template ⊙⦉ ⊙fin-skel ⦊ m≤n?
              (⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero)) g))

      frcc-comm-fccc-nth-zero : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n) (0≤n : 0 ≤ n) (1≤n : 1 ≤ n)
        → frcc-comm-fccc-Type ⊙fin-skel (inl 0≤n) (inl 1≤n)
            (RCC-coboundary-template' ⊙fin-skel (inl 0≤n) (inl 1≤n))
            (CCC-boundary-template' ⊙fin-skel (inl 0≤n) (inl 1≤n))
      frcc-comm-fccc-nth-zero ⊙fin-skel (inl idp) (inl 1=0) = ⊥-rec (ℕ-S≠O O 1=0)
      frcc-comm-fccc-nth-zero ⊙fin-skel (inl idp) (inr ())
      frcc-comm-fccc-nth-zero ⊙fin-skel (inr ltS) (inl 1=1) =
        transport!
          (λ 1=1 → frcc-comm-fccc-Type ⊙fin-skel (inl lteS) (inl (inl 1=1))
              (RCC-coboundary-template' ⊙fin-skel (inl lteS) (inl (inl 1=1)))
              (CCC-boundary-template' ⊙fin-skel (inl lteS) (inl (inl 1=1))))
          (prop-has-all-paths 1=1 idp)
          (coe!
            (ap2 (λ p₁ p₂ → frcc-comm-fccc-Type ⊙fin-skel {m = O} (inl (inr ltS)) (inl (inl idp)) p₁ p₂)
              (RCC.coboundary-first-template-β ⊙⦉ ⊙fin-skel ⦊)
              (CCC.boundary-template-β ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
                (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
                (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))))
            (fst (first-coboundary-comm-sqrᴳ ⊙fin-skel)))
      frcc-comm-fccc-nth-zero ⊙fin-skel (inr ltS) (inr (ltSR ()))
      frcc-comm-fccc-nth-zero ⊙fin-skel (inr (ltSR 0<n)) (inl 1=Sn) = ⊥-rec (<-to-≠ (<-ap-S 0<n) 1=Sn)
      frcc-comm-fccc-nth-zero ⊙fin-skel (inr (ltSR ltS)) (inr 1<2) =
        transport!
          (λ 1<2 → frcc-comm-fccc-Type ⊙fin-skel (inl (inr (ltSR ltS))) (inl (inr 1<2))
            (RCC-coboundary-template' ⊙fin-skel (inl (inr (ltSR ltS))) (inl (inr 1<2)))
            (CCC-boundary-template' ⊙fin-skel (inl (inr (ltSR ltS))) (inl (inr 1<2))))
          (prop-has-all-paths 1<2 ltS)
          (coe!
            (ap2 (λ p₁ p₂ → frcc-comm-fccc-Type ⊙fin-skel (inl (inr (ltSR ltS))) (inl (inr ltS)) p₁ p₂)
              (RCC.coboundary-first-template-descend-from-two ⊙⦉ ⊙fin-skel ⦊)
              (CCC.boundary-template-descend-from-two-above ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
                (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
                (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))))
            (frcc-comm-fccc-nth-zero (⊙fcw-init ⊙fin-skel) (inr ltS) (inl idp)))
      frcc-comm-fccc-nth-zero ⊙fin-skel (inr (ltSR (ltSR ()))) (inr ltS)
      frcc-comm-fccc-nth-zero ⊙fin-skel (inr (ltSR (ltSR 0<n))) (inr (ltSR 1<Sn)) =
        (coe!
          (ap2 (λ p₁ p₂ → frcc-comm-fccc-Type ⊙fin-skel (inl (inr (ltSR (ltSR 0<n)))) (inl (inr (ltSR 1<Sn))) p₁ p₂)
            (RCC.coboundary-first-template-descend-from-far ⊙⦉ ⊙fin-skel ⦊ (ltSR 0<n) 1<Sn)
            (CCC.boundary-template-descend-from-far ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
              (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
              (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))
              (ltSR 0<n) 1<Sn))
          (frcc-comm-fccc-nth-zero (⊙fcw-init ⊙fin-skel) (inr (ltSR 0<n)) (inr 1<Sn)))

      frcc-comm-fccc-nth-higher : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n) {m} (Sm≤n : S m ≤ n) (SSm≤n : S (S m) ≤ n)
        → frcc-comm-fccc-Type ⊙fin-skel (inl Sm≤n) (inl SSm≤n)
            (RCC-coboundary-template' ⊙fin-skel (inl Sm≤n) (inl SSm≤n))
            (CCC-boundary-template' ⊙fin-skel (inl Sm≤n) (inl SSm≤n))
      frcc-comm-fccc-nth-higher ⊙fin-skel (inl idp) (inl SSm=Sm) = ⊥-rec (<-to-≠ ltS (! SSm=Sm))
      frcc-comm-fccc-nth-higher ⊙fin-skel (inl idp) (inr SSm<Sm) = ⊥-rec (<-to-≠ (<-trans SSm<Sm ltS) idp)
      frcc-comm-fccc-nth-higher ⊙fin-skel {m} (inr ltS) (inl SSm=SSm) =
        transport!
          (λ SSm=SSm → frcc-comm-fccc-Type ⊙fin-skel (inl lteS) (inl (inl SSm=SSm))
            (RCC-coboundary-template' ⊙fin-skel (inl lteS) (inl (inl SSm=SSm)))
            (CCC-boundary-template' ⊙fin-skel (inl lteS) (inl (inl SSm=SSm))))
          (prop-has-all-paths SSm=SSm idp)
          (coe!
            (ap2 (λ p₁ p₂ → frcc-comm-fccc-Type ⊙fin-skel {m = S m} (inl (inr ltS)) (inl (inl idp)) p₁ p₂)
              (RCC.coboundary-higher-template-β ⊙⦉ ⊙fin-skel ⦊)
              (CCC.boundary-template-β ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
                (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
                (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))))
            (fst (higher-coboundary-comm-sqrᴳ ⊙fin-skel)))
      frcc-comm-fccc-nth-higher ⊙fin-skel (inr ltS) (inr SSm<SSm) = ⊥-rec (<-to-≠ SSm<SSm idp)
      frcc-comm-fccc-nth-higher ⊙fin-skel (inr (ltSR Sm<n)) (inl SSm=Sn) = ⊥-rec (<-to-≠ (<-ap-S Sm<n) SSm=Sn)
      frcc-comm-fccc-nth-higher ⊙fin-skel (inr (ltSR ltS)) (inr SSm<SSSm) =
        transport!
          (λ SSm<SSSm → frcc-comm-fccc-Type ⊙fin-skel (inl (inr (ltSR ltS))) (inl (inr SSm<SSSm))
            (RCC-coboundary-template' ⊙fin-skel (inl (inr (ltSR ltS))) (inl (inr SSm<SSSm)))
            (CCC-boundary-template' ⊙fin-skel (inl (inr (ltSR ltS))) (inl (inr SSm<SSSm))))
          (prop-has-all-paths SSm<SSSm ltS)
          (coe!
            (ap2 (λ p₁ p₂ → frcc-comm-fccc-Type ⊙fin-skel (inl (inr (ltSR ltS))) (inl (inr ltS)) p₁ p₂)
              (RCC.coboundary-higher-template-descend-from-one-above ⊙⦉ ⊙fin-skel ⦊)
              (CCC.boundary-template-descend-from-two-above ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
                (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
                (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))))
            (frcc-comm-fccc-nth-higher (⊙fcw-init ⊙fin-skel) (inr ltS) (inl idp)))
      frcc-comm-fccc-nth-higher ⊙fin-skel (inr (ltSR (ltSR Sm<Sm))) (inr ltS) = ⊥-rec (<-to-≠ Sm<Sm idp)
      frcc-comm-fccc-nth-higher ⊙fin-skel (inr (ltSR (ltSR Sm<n))) (inr (ltSR SSm<Sn)) =
        (coe!
          (ap2 (λ p₁ p₂ → frcc-comm-fccc-Type ⊙fin-skel (inl (inr (ltSR (ltSR Sm<n)))) (inl (inr (ltSR SSm<Sn))) p₁ p₂)
            (RCC.coboundary-higher-template-descend-from-far ⊙⦉ ⊙fin-skel ⦊ (ltSR Sm<n) SSm<Sn)
            (CCC.boundary-template-descend-from-far ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
              (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
              (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))
              (ltSR Sm<n) SSm<Sn))
          (frcc-comm-fccc-nth-higher (⊙fcw-init ⊙fin-skel) (inr (ltSR Sm<n)) (inr SSm<Sn)))

      frcc-comm-fccc-template : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n)
          {m} (m≤n? : Dec (m ≤ n)) (Sm≤n? : Dec (S m ≤ n))
        → frcc-comm-fccc-Type ⊙fin-skel m≤n? Sm≤n?
            (RCC-coboundary-template' ⊙fin-skel m≤n? Sm≤n?)
            (CCC-boundary-template' ⊙fin-skel m≤n? Sm≤n?)
      frcc-comm-fccc-template ⊙fin-skel m≤n? (inr Sm≰n) = frcc-comm-fccc-above ⊙fin-skel m≤n? Sm≰n
      frcc-comm-fccc-template ⊙fin-skel (inr m≰n) (inl Sm≤n) = ⊥-rec $ m≰n (≤-trans lteS Sm≤n)
      frcc-comm-fccc-template ⊙fin-skel {m = O} (inl m≤n) (inl Sm≤n) = frcc-comm-fccc-nth-zero ⊙fin-skel m≤n Sm≤n
      frcc-comm-fccc-template ⊙fin-skel {m = S m} (inl Sm≤n) (inl SSm≤n) = frcc-comm-fccc-nth-higher ⊙fin-skel Sm≤n SSm≤n

      frcc-comm-fccc : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n) m
        → frcc-comm-fccc-Type ⊙fin-skel (≤-dec m n) (≤-dec (S m) n)
            (RCC-coboundary-template' ⊙fin-skel (≤-dec m n) (≤-dec (S m) n))
            (CCC-boundary-template' ⊙fin-skel (≤-dec m n) (≤-dec (S m) n))
      frcc-comm-fccc {n} ⊙fin-skel m =
        frcc-comm-fccc-template ⊙fin-skel {m} (≤-dec m n) (≤-dec (S m) n)

      frcc-comm-fccc-augment : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n)
        → CommSquareᴳ
            (CochainComplex.augment (RCC.cochain-complex ⊙⦉ ⊙fin-skel ⦊))
            (pre∘ᴳ-hom (C2-abgroup 0) (FreeAbGroup-extend (Lift-abgroup {j = lzero} ℤ-abgroup) λ _ → lift 1))
            (GroupIso.f-hom rhead-iso-chead)
            (GroupIso.f-hom (rcc-iso-ccc-template ⊙⦉ ⊙fin-skel ⦊ (inl (O≤ n))
              (⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero)))
      frcc-comm-fccc-augment {n = O} ⊙fin-skel =
        fst (augment-comm-sqrᴳ ⊙fin-skel)
      frcc-comm-fccc-augment {n = S O} ⊙fin-skel =
        frcc-comm-fccc-augment (⊙fcw-init ⊙fin-skel)
      frcc-comm-fccc-augment {n = S (S n)} ⊙fin-skel =
        frcc-comm-fccc-augment (⊙fcw-init ⊙fin-skel)

  frcc-equiv-fccc : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n) →
    CochainComplexEquiv
      (RCC.cochain-complex ⊙⦉ ⊙fin-skel ⦊)
      (CCC.cochain-complex ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
         (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
         (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))
         (C2-abgroup 0))
  frcc-equiv-fccc {n} ⊙fin-skel = record
    { head = rhead-iso-chead
    ; cochain = λ m → rcc-iso-ccc ⊙⦉ ⊙fin-skel ⦊ m (⊙FinSkeleton-has-cells-with-choice 0 ⊙fin-skel lzero)
    ; augment = frcc-comm-fccc-augment ⊙fin-skel
    ; coboundary = frcc-comm-fccc ⊙fin-skel}

  frc-iso-fcc : ∀ {n} (⊙fin-skel : ⊙FinSkeleton n) (m : ℤ)
    →  cohomology-group (RCC.cochain-complex ⊙⦉ ⊙fin-skel ⦊) m
    ≃ᴳ cohomology-group
        (CCC.cochain-complex ⦉ ⊙FinSkeleton.skel ⊙fin-skel ⦊
          (FinSkeleton-has-cells-with-dec-eq (⊙FinSkeleton.skel ⊙fin-skel))
          (FinSkeleton-has-degrees-with-finite-support (⊙FinSkeleton.skel ⊙fin-skel))
          (C2-abgroup 0))
        m
  frc-iso-fcc ⊙fin-skel = cohomology-group-emap (frcc-equiv-fccc ⊙fin-skel)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{- This file describes properties of computable relations. -}

open import bool
open import level
open import eq
open import product
open import product-thms
open import negation

module relations where

  -- Decidable relations.
  -- This was taken from the Agda STDLIB.
  data Dec {p} (P : Set p) : Set p where
    yes : ( p :   P) → Dec P
    no  : (¬p : ¬ P) → Dec P

  module relationsOld {ℓ ℓ' : level}{A : Set ℓ} (_≥A_ : A → A → Set ℓ') where

    reflexive : Set (ℓ ⊔ ℓ')
    reflexive = ∀ {a : A} → a ≥A a

    transitive : Set (ℓ ⊔ ℓ')
    transitive = ∀ {a b c : A} → a ≥A b → b ≥A c → a ≥A c

    preorder : Set (ℓ ⊔ ℓ')
    preorder = reflexive ∧ transitive

    _iso_ : A → A → Set ℓ'
    d iso d' = d ≥A d' ∧ d' ≥A d

    iso-intro : ∀{x y : A} → x ≥A y → y ≥A x → x iso y
    iso-intro p1 p2 = p1 , p2

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- Andreas, 2016-09-20 test whether --no-eta-equality is respected

{-# OPTIONS --no-eta-equality #-}

record ⊤ : Set where

test : ⊤
test = _ -- should remain unsolved

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module BasicIPC.Metatheory.ClosedHilbert-BasicTarski where

open import BasicIPC.Syntax.ClosedHilbert public
open import BasicIPC.Semantics.BasicTarski public

-- Soundness with respect to all models, or evaluation, for closed terms only.

eval₀ : ∀ {A} → ⊢ A → ⊨ A
eval₀ (app t u) = eval₀ t $ eval₀ u
eval₀ ci        = I
eval₀ ck        = K
eval₀ cs        = S
eval₀ cpair     = _,_
eval₀ cfst      = π₁
eval₀ csnd      = π₂
eval₀ unit      = ∙

-- Correctness of evaluation with respect to conversion.

eval₀✓ : ∀ {{_ : Model}} {A} {t t′ : ⊢ A} → t ⋙ t′ → eval₀ t ≡ eval₀ t′
eval₀✓ refl⋙           = refl
eval₀✓ (trans⋙ p q)    = trans (eval₀✓ p) (eval₀✓ q)
eval₀✓ (sym⋙ p)        = sym (eval₀✓ p)
eval₀✓ (congapp⋙ p q)  = cong² _$_ (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congi⋙ p)      = cong I (eval₀✓ p)
eval₀✓ (congk⋙ p q)    = cong² K (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congs⋙ p q r)  = cong³ S (eval₀✓ p) (eval₀✓ q) (eval₀✓ r)
eval₀✓ (congpair⋙ p q) = cong² _,_ (eval₀✓ p) (eval₀✓ q)
eval₀✓ (congfst⋙ p)    = cong π₁ (eval₀✓ p)
eval₀✓ (congsnd⋙ p)    = cong π₂ (eval₀✓ p)
eval₀✓ beta▻ₖ⋙         = refl
eval₀✓ beta▻ₛ⋙         = refl
eval₀✓ beta∧₁⋙         = refl
eval₀✓ beta∧₂⋙         = refl
eval₀✓ eta∧⋙           = refl
eval₀✓ eta⊤⋙          = refl

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


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

open import Base
open import Homotopy.PushoutDef
open import Homotopy.PushoutUP as PushoutUP
open import Homotopy.Truncation
open import Homotopy.PullbackDef
open import Homotopy.PullbackInvariantEquiv

module Homotopy.TruncationRightExact {i} (n : ℕ₋₂) (d : pushout-diag i) where

open pushout-diag d
open import Homotopy.PushoutIsPushout d

τd : pushout-diag i
τd = diag (τ n A), (τ n B), (τ n C), (τ-fmap f), (τ-fmap g)

module H  = PushoutUP d  (cst unit)
module τH = PushoutUP τd (is-truncated n)

-- I want to prove that [τ n d.pushout] is a pushout in [is-truncated n]. It
-- first needs to be equipped with a cocone

cocone-τpushout : τH.cocone (τ n (pushout d))
cocone-τpushout = (τ-fmap left , τ-fmap right ,
                     τ-extend ⦃ λ _ → ≡-is-truncated _ (τ-is-truncated _ _) ⦄
                       (ap proj ◯ glue))

-- We have a map [(τ n (pushout d) → E) → τH.cocone E] with [E] in [P] given by
-- [τH.compose-cocone-map] and we want to prove that it’s an equivalence

-- The idea is that it’s the composite of five equivalences:

-- [equiv1 : τ n (pushout d) → E ≃ (pushout d) → E]
--    by the universal property of truncations
-- [equiv2 : (pushout d) → E ≃ H.cocone E]
--    by the universal property of pushout in Type
-- [equiv3 : H.cocone E ≃ pullback … (without truncations)]
--    via [cocone-is-pullback]
-- [equiv4 : pullback … (without truncations) ≃ pullback … (with truncations)]
--    by the universal property of truncations and invariance of pullback wrt
--    equivalence of diagrams
-- [equiv5 : pullback … (with truncations) ≃ τH.cocone E]
--    via [cocone-is-pullback]

module _ (E : Set i) ⦃ P-E : is-truncated n E ⦄ where

  private
    ≡E-is-truncated#instance : {x y : E} → is-truncated n (x ≡ y)
    ≡E-is-truncated#instance = ≡-is-truncated n P-E

    λ-≡E-is-truncated#instance : {A : Set i} {u v : A → E}
      → ((x : A) → is-truncated n (u x ≡ v x))
    λ-≡E-is-truncated#instance = λ _ → ≡E-is-truncated#instance

    ≡≡E-is-truncated#instance : {x y : E} {p q : x ≡ y} → is-truncated n (p ≡ q)
    ≡≡E-is-truncated#instance = ≡-is-truncated n (≡-is-truncated n P-E)

    λ-≡≡E-is-truncated#instance : {A : Set i} {x y : A → E}
      {p q : (a : A) → x a ≡ y a} → ((a : A) → is-truncated n (p a ≡ q a))
    λ-≡≡E-is-truncated#instance = λ _ → ≡≡E-is-truncated#instance

    equiv1 : (τ n (pushout d) → E) ≃ (pushout d → E)
    equiv1 = ((λ u → u ◯ proj) , τ-up n _ _)

    equiv2 : (pushout d → E) ≃ H.cocone E
    equiv2 = ((λ f → ((f ◯ left) , (f ◯ right) , (ap f ◯ glue)))
             , pushout-is-pushout E)

    -- (could be defined more generally somewhere else)
    diag-hom : pullback-diag i
    diag-hom = diag (A → E), (B → E), (C → E), (λ u → u ◯ f), (λ u → u ◯ g)

    τdiag-hom : pullback-diag i
    τdiag-hom = diag (τ n A → E), (τ n B → E), (τ n C → E),
                     (λ u → u ◯ τ-fmap f) , (λ u → u ◯ τ-fmap g)

    equiv3 : H.cocone E ≃ pullback diag-hom
    equiv3 = H.cocone-equiv-pullback E

    p₀ : (a : A → E) (x : τ n C)
      → τ-extend-nondep a (τ-fmap f x) ≡ τ-extend-nondep (a ◯ f) x
    p₀ a = τ-extend (λ x → refl)

    p : (a : A → E) → (τ-extend-nondep a) ◯ τ-fmap f ≡ τ-extend-nondep (a ◯ f)
    p a = funext (p₀ a)

    q₀ : (b : B → E) (x : τ n C)
      → τ-extend-nondep (b ◯ g) x ≡ τ-extend-nondep b (τ-fmap g x)
    q₀ b = τ-extend (λ x → refl)

    q : (b : B → E) → τ-extend-nondep (b ◯ g) ≡ (τ-extend-nondep b) ◯ τ-fmap g
    q b = funext (q₀ b)

    equiv4 : pullback diag-hom ≃ pullback τdiag-hom
    equiv4 = pullback-invariant-equiv diag-hom τdiag-hom
               (τ-extend-equiv n A E) (τ-extend-equiv n B E)
               (τ-extend-equiv n C E) p q

    equiv5 : pullback τdiag-hom ≃ τH.cocone E
    equiv5 = τH.pullback-equiv-cocone E

    -- We have defined the five equivalences, now we want to prove that the
    -- composite is what we want. We start by computing the composite of the
    -- equivalences 3, 4 and 5.

    map-543 : H.cocone E → τH.cocone E
    map-543 (a , b , e) = (τ-extend-nondep a , τ-extend-nondep b , τ-extend e)

    map-543-correct : (x : H.cocone E)
      → equiv5 ☆ (equiv4 ☆ (equiv3 ☆ x)) ≡ map-543 x
    map-543-correct (a , b , h) =
      ap (λ u → _ , _ , u)
        (funext (τ-extend
          (λ x →
            ap-concat (λ u → u (proj x)) (p a)
              (ap τ-extend-nondep (funext h) ∘ q b)
            ∘ (whisker-right _ (happly (happly-funext (p₀ a)) (proj x))
            ∘ (ap-concat (λ u → u (proj x))
                (ap τ-extend-nondep (funext h)) (q b)
            ∘ (whisker-right _
                (compose-ap (λ u → u (proj x)) τ-extend-nondep (funext h))
            ∘ (whisker-right _ (happly (happly-funext h) x)
            ∘ (whisker-left (h x)
                (happly (happly-funext (q₀ b)) (proj x))
            ∘ refl-right-unit (h x)))))))))

    -- We now study the full composite

    map-54321 : (τ n (pushout d) → E) → τH.cocone E
    map-54321 = τH.compose-cocone-map _ _ cocone-τpushout

    map-21-A₀ : (f : τ n (pushout d) → E) (u : τ n A)
      → τH.A→top (map-543 (equiv2 ☆ (equiv1 ☆ f))) u ≡ τH.A→top (map-54321 f) u
    map-21-A₀ f = τ-extend (λ x → refl)

    map-21-A : (f : τ n (pushout d) → E)
      → τH.A→top (map-543 (equiv2 ☆ (equiv1 ☆ f))) ≡ τH.A→top (map-54321 f)
    map-21-A f = funext (map-21-A₀ f)

    map-21-B₀ : (f : τ n (pushout d) → E) (u : τ n B)
      → τH.B→top (map-543 (equiv2 ☆ (equiv1 ☆ f))) u ≡ τH.B→top (map-54321 f) u
    map-21-B₀ f = τ-extend (λ x → refl)

    map-21-B : (f : τ n (pushout d) → E)
      → τH.B→top (map-543 (equiv2 ☆ (equiv1 ☆ f))) ≡ τH.B→top (map-54321 f)
    map-21-B f = funext (map-21-B₀ f)

    map-21-correct : (h : τ n (pushout d) → E)
      → map-543 (equiv2 ☆ (equiv1 ☆ h)) ≡ map-54321 h
    map-21-correct h = τH.cocone-eq _ (map-21-A h) (map-21-B h)
      (τ-extend
        (λ x →
          whisker-right _ (happly (happly-funext (map-21-A₀ h)) (proj (f x)))
          ∘ (compose-ap h proj _
          ∘ (! (refl-right-unit (ap (h ◯ proj) (glue x)))
          ∘ whisker-left (ap (h ◯ proj) (glue x))
          (! (happly (happly-funext (map-21-B₀ h)) (proj (g x))))))))

    map-54321-correct : (f : τ n (pushout d) → E)
      → equiv5 ☆ (equiv4 ☆ (equiv3 ☆ (equiv2 ☆ (equiv1 ☆ f)))) ≡ map-54321 f
    map-54321-correct f = map-543-correct (equiv2 ☆ (equiv1 ☆ f))
                          ∘ map-21-correct f

  map-54321-is-equiv : is-equiv map-54321
  map-54321-is-equiv =
    transport is-equiv (funext map-54321-correct)
      (compose-is-equiv
        ((λ f₁ → equiv4 ☆ (equiv3 ☆ (equiv2 ☆ (equiv1 ☆ f₁))))
        , compose-is-equiv
          ((λ f₁ → equiv3 ☆ (equiv2 ☆ (equiv1 ☆ f₁)))
            , compose-is-equiv
              ((λ f₁ → equiv2 ☆ (equiv1 ☆ f₁))
                , compose-is-equiv equiv1 equiv2)
              equiv3)
          equiv4)
      equiv5)

abstract
  τpushout-is-pushout : τH.is-pushout (τ n (pushout d)) cocone-τpushout
  τpushout-is-pushout E = map-54321-is-equiv E

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

module Container.Stream where

open import Prelude
open import Data.Fin
open import Container

Stream : Type a → Type a
Stream = ⟦ ⊤ , const ℕ ⟧

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import LogicalFormulae
open import Setoids.Setoids
open import Functions
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Naturals
open import Sets.FinSet
open import Groups.Groups
open import Groups.Definition
open import Sets.EquivalenceRelations
open import Setoids.Functions.Extension

module Groups.SymmetricGroups.CycleType where


text:
module Structure.Setoid.Proofs where

import Lvl
open import Functional
open import Logic
open import Logic.Propositional
open import Structure.Setoid
open import Structure.Function
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties

{-

module _ where
  private variable ℓ ℓ₁ ℓ₂ ℓ₃ : Level
  private variable A B : Type{ℓ}
  private variable P : Stmt{ℓ}

  Choice : (A → B → Stmt{ℓ}) → Stmt
  Choice{A = A}{B = B}(_▫_) = (∀{x} → ∃(y ↦ x ▫ y)) → (∃{Obj = A → B}(f ↦ ∀{x} → (x ▫ f(x))))

  module _ ⦃ choice : ∀{ℓ₁ ℓ₂ ℓ₃}{A : Type{ℓ₁}}{B : Type{ℓ₂}}{_▫_ : A → B → Stmt{ℓ₃}} → Choice(_▫_) ⦄ where
    open import Data.Boolean
    open import Structure.Relator.Properties
    open import Structure.Relator.Properties.Proofs
    open import Relator.Equals.Proofs.Equiv

    thing : Stmt{ℓ} → Bool → Bool → Stmt
    thing P a b = (a ≡ b) ∨ P

    thing-functionallyTotal : ∀{x} → ∃(y ↦ thing P x y)
    thing-functionallyTotal {x = x} = [∃]-intro x ⦃ [∨]-introₗ (reflexivity(_≡_)) ⦄

    thing-choice : ∃(f ↦ ∀{x} → thing(P) x (f(x)))
    thing-choice {P = P} = choice{_▫_ = thing P} thing-functionallyTotal

    instance
      thing-reflexivity : Reflexivity(thing(P))
      Reflexivity.proof thing-reflexivity = [∨]-introₗ(reflexivity(_≡_))

    instance
      thing-symmetry : Symmetry(thing(P))
      Symmetry.proof thing-symmetry = [∨]-elim2 (symmetry(_≡_)) id

    instance
      thing-transitivity : Transitivity(thing(P))
      Transitivity.proof thing-transitivity ([∨]-introₗ xy) ([∨]-introₗ yz) = [∨]-introₗ (transitivity(_) xy yz)
      Transitivity.proof thing-transitivity ([∨]-introₗ xy) ([∨]-introᵣ p)  = [∨]-introᵣ p
      Transitivity.proof thing-transitivity ([∨]-introᵣ p)  _               = [∨]-introᵣ p

    thing-ext : let ([∃]-intro f) = thing-choice{P = P} in ∀{a b} → thing(P) a b → (f(a) ≡ f(b))
    thing-ext ([∨]-introₗ ab) = congruence₁([∃]-witness thing-choice) ab
    thing-ext {a = a} {b = b} ([∨]-introᵣ p) = {!!}

    thing-eq : let ([∃]-intro f) = thing-choice{P = P} in (P ↔ (f(𝐹) ≡ f(𝑇)))
    _⨯_.left  (thing-eq {P = P}) ft with [∃]-proof (thing-choice{P = P}){𝐹}
    _⨯_.left (thing-eq {P = P}) ft | [∨]-introₗ ff = [∨]-syllogismₗ ([∃]-proof (thing-choice{P = P}){𝑇}) ((symmetry(_≢_) ⦃ negated-symmetry ⦄ ∘ [↔]-to-[←] [≢][𝑇]-is-[𝐹] ∘ symmetry(_≡_)) (transitivity(_≡_) ff ft))
    _⨯_.left (thing-eq {P = P}) ft | [∨]-introᵣ p = p
    _⨯_.right (thing-eq {P = P}) p = thing-ext ([∨]-introᵣ p)

    bool-eq-classical : Classical₂ {X = Bool} (_≡_)

    choice-to-classical : Classical(P)
    excluded-middle ⦃ choice-to-classical {P = P} ⦄ with excluded-middle ⦃ bool-eq-classical {[∃]-witness (thing-choice{P = P}) 𝐹} {[∃]-witness (thing-choice{P = P}) 𝑇} ⦄
    excluded-middle ⦃ choice-to-classical {P = P} ⦄ | [∨]-introₗ ft  = [∨]-introₗ ([↔]-to-[←] thing-eq ft)
    excluded-middle ⦃ choice-to-classical {P = P} ⦄ | [∨]-introᵣ nft = [∨]-introᵣ (nft ∘ [↔]-to-[→] thing-eq)

  module _ ⦃ classical : ∀{ℓ}{P : Stmt{ℓ}} → Classical(P) ⦄ where
    proof-irrelevance : ∀{p₁ p₂ : P} → (p₁ ≡ p₂)
    proof-irrelevance with excluded-middle
    proof-irrelevance {P = P}{p₁}{p₂} | [∨]-introₗ p  = {!!}
    proof-irrelevance {P = P}{p₁}{p₂} | [∨]-introᵣ np = [⊥]-elim(np p₁)

-}

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Data.NDTrie where

open import Class.Map
open import Data.Char
open import Data.Char.Instance
open import Data.List
open import Data.List.Instance
open import Data.AVL.Value
open import Data.Product

import Data.Char.Properties as Char
import Data.Trie Char.<-strictTotalOrder-≈ as T

NDTrie : Set -> Set
NDTrie A = T.Trie (const _ A) _

instance
  NDTrie-Map : MapClass (List Char) NDTrie
  NDTrie-Map = record
           { insert = T.insert
           ; remove = T.deleteValue
           ; lookup = T.lookupValue
           ; mapSnd = λ f -> T.map f
           ; emptyMap = T.empty
           }

trieKeys : ∀ {A} -> NDTrie A -> List (List Char)
trieKeys t = Data.List.map proj₁ (T.toList t)

lookupNDTrie : ∀ {A} -> List Char -> NDTrie A -> NDTrie A
lookupNDTrie [] t = t
lookupNDTrie (c ∷ cs) t = lookupNDTrie cs (T.lookupTrie c t)

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
-- New feature by Jesper Cockx in commit be89d4a8b264dd2719cb8c601a2c7f45a95ba220 :
-- disabling the universe check for a data or record type.

-- Andreas, 2018-10-27, re issue #3327: restructured test cases.

-- Andreas, 2019-07-16, issue #3916:
-- {-# NO_UNIVERSE_CHECK #-} should also disable the index sort check
-- for --cubical-compatible.

{-# OPTIONS --cubical-compatible #-}

module _ where

-- Switch off the index sort check

module BigHetEq where

  {-# NO_UNIVERSE_CHECK #-}
  data _≅_ {a}{A : Set a} (x : A) : {B : Set a} → B → Set where
     refl : x ≅ x

module PittsHetEq where

  {-# NO_UNIVERSE_CHECK #-}
  data _≅_ {a}{A : Set a} (x : A) : {B : Set a} → B → Set a where
     refl : x ≅ x

-- Pragma is naturally attached to definition.

module DataDef where

  data U : Set
  T : U → Set

  {-# NO_UNIVERSE_CHECK #-}
  data U where
    pi : (A : Set)(b : A → U) → U

  T (pi A b) = (x : A) → T (b x)

-- Pragma can also be attached to signature.

module DataSig where

  {-# NO_UNIVERSE_CHECK #-}
  data U : Set
  T : U → Set

  data U where
    pi : (A : Set)(b : A → U) → U

  T (pi A b) = (x : A) → T (b x)

-- Works also for explicit mutual blocks.

module Mutual where

  {-# NO_UNIVERSE_CHECK #-}
  data U : Set where
    pi : (A : Set)(b : A → U) → U

  T : U → Set
  T (pi A b) = (x : A) → T (b x)

-- Records:

module Records where

  {-# NO_UNIVERSE_CHECK #-}
  record R : Set where
    field out : Set

  {-# NO_UNIVERSE_CHECK #-}
  record S : Set

  record S where
    field out : Set


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

module CombiningProofs.CommDisjunction where

open import Common.FOL.FOL

postulate
  A B : Set
  ∨-comm : A ∨ B → B ∨ A
{-# ATP prove ∨-comm #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2016-08-04, issue #964
-- Allow open metas and interaction points in imported files

-- {-# OPTIONS -v import:100 #-}
-- {-# OPTIONS -v meta.postulate:20 #-}
-- {-# OPTIONS -v tc.conv.level:50 #-}

open import Common.Level
open import Common.Equality

postulate something : Set₁

open import Common.Issue964.UnsolvedMetas something

test =  M.N.meta3

shouldFail : _≡_ {A = Level} meta (lsuc (lsuc lzero))
shouldFail = refl

-- WAS: WEIRD ERROR:
-- Set (Set .Issue964.UnsolvedMetas.1) != Set₂
-- when checking that the expression refl has type
-- meta ≡ lsuc (lsuc lzero)

-- NOW:
-- Set (.Issue964.UnsolvedMetas.unsolved#meta.1 something) != Set₂
-- when checking that the expression refl has type
-- meta ≡ lsuc (lsuc lzero)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical #-}
module Agda.Primitive.Cubical where
{-# BUILTIN INTERVAL I    #-} -- I : Setω

{-# BUILTIN IZERO    i0   #-}
{-# BUILTIN IONE     i1   #-}

infix 30 primINeg
infixr 20 primIMin primIMax

primitive
    primIMin : I → I → I
    primIMax : I → I → I
    primINeg : I → I

{-# BUILTIN ISONE        IsOne #-} -- IsOne : I → Setω

postulate
  itIsOne : IsOne i1
  IsOne1  : ∀ i j → IsOne i → IsOne (primIMax i j)
  IsOne2  : ∀ i j → IsOne j → IsOne (primIMax i j)

{-# BUILTIN ITISONE      itIsOne  #-}
{-# BUILTIN ISONE1       IsOne1   #-}
{-# BUILTIN ISONE2       IsOne2   #-}
{-# BUILTIN PARTIAL      Partial  #-}
{-# BUILTIN PARTIALP     PartialP #-}

postulate
  isOneEmpty : ∀ {a} {A : Partial i0 (Set a)} → PartialP i0 A
{-# BUILTIN ISONEEMPTY isOneEmpty #-}

primitive
  primPFrom1 : ∀ {a} {A : I → Set a} → A i1 → ∀ i j → Partial i (A (primIMax i j))
  primPOr : ∀ {a} (i j : I) {A : Partial (primIMax i j) (Set a)}
            → PartialP i (λ z → A (IsOne1 i j z)) → PartialP j (λ z → A (IsOne2 i j z))
            → PartialP (primIMax i j) A
  primComp : ∀ {a} (A : (i : I) → Set (a i)) (φ : I) → (∀ i → Partial φ (A i)) → (a : A i0) → A i1

syntax primPOr p q u t = [ p ↦ u , q ↦ t ]

primitive
  primTransp : ∀ {a} (A : (i : I) → Set (a i)) (φ : I) → (a : A i0) → A i1
  primHComp : ∀ {a} {A : Set a} {φ : I} → (∀ i → Partial φ A) → A → A

max_stars_repo_name: bennn/agda

max_issues_repo_name: bennn/agda

max_forks_repo_name: bennn/agda


text:
module Sessions.Semantics.Expr where

open import Prelude
open import Data.Fin

open import Relation.Unary.PredicateTransformer hiding (_⊔_)
open import Relation.Ternary.Separation.Morphisms
open import Relation.Ternary.Separation.Monad
open import Relation.Ternary.Separation.Monad.Reader

open import Sessions.Syntax.Types
open import Sessions.Syntax.Values
open import Sessions.Syntax.Expr
-- open import Sessions.Semantics.Commands
open import Sessions.Semantics.Runtime

open import Relation.Ternary.Separation.Construct.List Type
-- open import Relation.Ternary.Separation.Monad.Free Cmd δ
open import Relation.Ternary.Separation.Monad.Delay

module _ where

  mutual
    data Cmd : Pred RCtx 0ℓ where
      fork    :             ∀[ Thread unit ⇒ Cmd ]
      mkchan  : ∀ α       → ε[ Cmd ]
      send    : ∀ {a α}   → ∀[ (Endptr (a ! α) ✴ Val a) ⇒ Cmd ]
      receive : ∀ {a α}   → ∀[ Endptr (a ¿ α) ⇒ Cmd ]
      close   :             ∀[ Endptr end ⇒ Cmd ]
      yield   :             ε[ Cmd ]

    Cont : ∀ i {Δ} → Cmd Δ → Pt RCtx 0ℓ
    Cont i c P = δ c ─✴ Free i P

    data Free i : Pt RCtx 0ℓ where
      pure   : ∀ {P}   → ∀[ P ⇒ Free i P ]
      impure : ∀ {P Φ} → Thunk (λ j → (∃[ Cmd ]✴ (λ c → Cont j c P)) Φ) i → Free i P Φ

    δ : ∀ {Δ} → Cmd Δ → Pred RCtx 0ℓ
    δ (fork {α} _)        = Emp
    δ (mkchan α)          = Endptr α ✴ Endptr (α ⁻¹)
    δ (send {α = α} _)    = Endptr α
    δ (receive {a} {α} _) = Val a ✴ Endptr α
    δ (close _)           = Emp
    δ yield               = Emp

    Thread : Type → Pred RCtx _
    Thread a = Free ∞ (Val a)

  open Monads using (Monad; str; _&_) public

  m-monad : ∀ {i} → Monad ⊤ _ (λ _ _ → Free i)
  Monad.return m-monad px = pure px
  app (Monad.bind m-monad f) (pure px) σ = app f px σ
  app (Monad.bind m-monad f) (impure tx) σ =
    impure λ where
      .force →
        let
          cmd ×⟨ σ₁ ⟩ κ = tx .force
          _ , σ₂ , σ₃   = ⊎-assoc σ₁ (⊎-comm σ)
        in cmd ×⟨ σ₂ ⟩ wand λ r σ₄ →
          let _ , τ₁ , τ₂ = ⊎-assoc (⊎-comm σ₃) σ₄ in
          app (Monad.bind m-monad f) (app κ r τ₂) τ₁

  module _ {i} where
    open ReaderTransformer id-morph Val (Free i) {{m-monad}} renaming (Reader to T) public

  M : Size → LCtx → LCtx → Pt RCtx 0ℓ
  M i Γ₁ Γ₂ P = T {i} Γ₁ Γ₂ P

  -- open import Relation.Ternary.Separation.Monad.Free Cmd δ renaming (Cont to Cont')

  ⟪_⟫ : ∀ {i Φ} → (c : Cmd Φ) → Free i (δ c) Φ
  ⟪_⟫ c =
    impure (λ where .force → c ×⟨ ⊎-idʳ ⟩ wand λ r σ → case ⊎-id⁻ˡ σ of λ where refl → pure r )

open Monad reader-monad public
mutual
  eval : ∀ {i} → Exp a Γ → ε[ M i Γ [] (Val a) ]

  eval unit = do
    return tt

  eval (var refl) = do
    (v :⟨ σ ⟩: nil) ← ask
    case ⊎-id⁻ʳ σ of λ where
      refl → return v

  eval (lam a e) = do
    env ← ask
    return (clos e env)

  eval (ap (f ×⟨ Γ≺ ⟩ e)) = do
    v ← frame (⊎-comm Γ≺) (►eval e)
    {!!} -- eval⊸ f v

  eval (pairs (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    v₁ ← frame Γ≺ (►eval e₁)
    v₂⋆v₂ ← ►eval e₂ & v₁
    return (pairs (✴-swap v₂⋆v₂))

  eval (letpair (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    pairs (v₁ ×⟨ σ ⟩ v₂) ← frame Γ≺ (►eval e₁)
    empty ← prepend (cons (v₁ ×⟨ σ ⟩ singleton v₂))
    ►eval e₂

  eval (send (e₁ ×⟨ Γ≺ ⟩ e₂)) = do
    v₁ ← frame Γ≺ (►eval e₁)
    cref φ ×⟨ σ ⟩ v₁ ← ►eval e₂ & v₁
    φ' ← liftM  ⟪ send (φ ×⟨ σ ⟩ v₁) ⟫
    return (cref φ')

  eval (recv e) = do
    cref φ ← ►eval e
    v ×⟨ σ ⟩ φ' ← liftM  ⟪ receive φ ⟫
    return (pairs (cref φ' ×⟨ ⊎-comm σ ⟩ v))

  eval (fork e) = do
    clos body env ← ►eval e
    empty ← liftM ⟪ fork (app (runReader (cons (tt ×⟨ ⊎-idˡ ⟩ env))) (►eval body) ⊎-idʳ) ⟫ -- (app (runReader (cons (tt ×⟨ ⊎-idˡ ⟩ env))) (►eval body) ⊎-idʳ)
    return tt

  eval (terminate e) = do
    cref φ ← ►eval e
    empty ← liftM ⟪ close φ ⟫
    return tt

  -- eval⊸ : ∀ {i Γ} → Exp (a ⊸ b) Γ → ∀[ Val a ⇒ⱼ M i Γ [] (Val b) ]
  -- eval⊸ e v = do
  --   (clos e env) ×⟨ σ₂ ⟩ v ← ►eval e & v
  --   empty                  ← append (cons (v ×⟨ ⊎-comm σ₂ ⟩ env))
  --   ►eval e

  -- ►eval⊸ : ∀ {i Γ} → Exp (a ⊸ b) Γ → ∀[ Val a ⇒ⱼ M i Γ [] (Val b) ]
  -- app (►eval⊸ e v) E σ = impure λ where
  --   .force →
  --     yield
  --       ×⟨ ⊎-idˡ ⟩
  --     wand (λ where empty σ' → case ⊎-id⁻ʳ σ' of λ where refl → app (eval⊸ e v) E σ )

  ►eval : ∀ {i} → Exp a Γ → ε[ M i Γ [] (Val a) ]
  app (►eval e) E σ = impure λ where
    .force →
      yield
        ×⟨ ⊎-idˡ ⟩
      wand (λ where empty σ' → case ⊎-id⁻ʳ σ' of λ where refl → app (eval e) E σ )


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

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

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

module LibraBFT.Impl.Util.Util where
  open import LibraBFT.Impl.Util.RWST public
  ----------------
  -- LBFT Monad --
  ----------------

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

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

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

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

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

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

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

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

max_stars_repo_name: haroldcarr/bft-consensus-agda

max_issues_repo_name: haroldcarr/bft-consensus-agda

max_forks_repo_name: haroldcarr/bft-consensus-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers
------------------------------------------------------------------------

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

module Data.Nat where

------------------------------------------------------------------------
-- Publicly re-export the contents of the base module

open import Data.Nat.Base public

------------------------------------------------------------------------
-- Publicly re-export queries

open import Data.Nat.Properties public
  using
  ( _≟_
  ; _≤?_ ; _≥?_ ; _<?_ ; _>?_
  ; _≤′?_; _≥′?_; _<′?_; _>′?_
  ; _≤″?_; _<″?_; _≥″?_; _>″?_
  )

------------------------------------------------------------------------
-- Deprecated

-- Version 0.17

open import Data.Nat.Properties public
  using (≤-pred)


text:
-- https://personal.cis.strath.ac.uk/conor.mcbride/PolyTest.pdf

module Sandbox.PolyTest where

open import Data.Nat
open import Data.Nat.Properties.Extra
open import Relation.Binary.PropositionalEquality

_^_ : ℕ → ℕ → ℕ
x ^ zero  = suc zero
x ^ suc y = x * (x ^ y)

-- data Poly : ℕ → Set where
--    κ : ℕ → Poly 0
--    ι : Poly 1
--    _⊕_ : ∀ {l m} → Poly l → Poly m → Poly (l ⊓ m)
--    _⊗_ : ∀ {l m} → Poly l → Poly m → Poly (l * m)
--
-- ⟦_⟧_ : ∀ {n} → Poly n → ℕ → ℕ
-- ⟦ κ c ⟧ x = c
-- ⟦ ι ⟧ x = x
-- ⟦ p ⊕ q ⟧ x = ⟦ p ⟧ x + ⟦ q ⟧ x
-- ⟦ p ⊗ q ⟧ x = ⟦ p ⟧ x * ⟦ q ⟧ x
--
-- Δ : ∀ {n} → Poly (suc n) → Poly n
-- Δ p = {! p  !}
-- -- I'm not sure if there should be a case for the constructor _⊕_,
-- -- because I get stuck when trying to solve the following unification
-- -- problems (inferred index ≟ expected index):
-- --   l ⊓ m ≟ suc n
-- -- when checking that the expression ? has type Poly .n

-- data Poly : ℕ → Set where
--    κ : ℕ → Poly 0
--    ι : Poly 1
--    plus : ∀ {l m n} → Poly l → Poly m → (l ⊓ m) ≡ n → Poly n
--    times : ∀ {l m n} → Poly l → Poly m → (l * m) ≡ n → Poly n
--
-- ⟦_⟧_ : ∀ {n} → Poly n → ℕ → ℕ
-- ⟦ κ c ⟧ x = c
-- ⟦ ι ⟧ x = x
-- ⟦ plus p q eq ⟧ x = ⟦ p ⟧ x + ⟦ q ⟧ x
-- ⟦ times p q eq ⟧ x = ⟦ p ⟧ x * ⟦ q ⟧ x

-- Δ : ∀ {n} → Poly (suc n) → Poly n
-- Δ ι = κ 1
-- Δ (plus (κ x) q ())
-- Δ (plus ι (κ x) ())
-- Δ (plus ι ι eq) = plus (Δ ι) (Δ ι) (cancel-suc eq)
-- Δ (plus ι (plus p₂ q₂ eq₂) eq) = plus (Δ ι) (Δ {! (plus p₂ q₂ eq₂)  !}) {!   !}
-- Δ (plus ι (times p₂ q₂ eq₂) eq) = {!   !}
-- -- Δ (plus ι q eq) = plus (Δ ι) (Δ {!   !}) {!   !}
-- Δ (plus (plus p q' eq') q eq) = {!   !}
-- Δ (plus (times p q' eq') q eq) = {!   !}
-- Δ (times p q eq) = {!   !}

-- data Poly : ℕ → Set where
--    κ     : ∀ {n}                                 → ℕ → Poly n
--    ι     : ∀ {n}                                      → Poly (suc n)
--    plus  : ∀ {n}     → Poly n → Poly n               → Poly n
--    times : ∀ {l m n} → Poly l → Poly m → (l * m) ≡ n → Poly n
--
-- -- ∆(p ⊗ r) = ∆p ⊗ (r · (1+)) ⊕ p ⊗ ∆r
-- Δ : ∀ {n} → Poly (suc n) → Poly n
-- Δ (κ x)          = κ 0
-- Δ ι              = κ 1
-- Δ (plus p q)     = plus (Δ p) (Δ q)
-- Δ (times p q eq) = times (Δ {! p  !}) {!   !} {!   !}

data Add : ℕ → ℕ → ℕ → Set where
    0+n : ∀ {n} → Add 0 n n
    n+0 : ∀ {n} → Add n 0 n
    m+n : ∀ {l m n} → Add l m n → Add (suc l) (suc m) (suc (suc n))

data Poly : ℕ → Set where
   κ     : ∀ {n}                                 → ℕ → Poly n
   ι     : ∀ {n}                                      → Poly (suc n)
   ↑     : ∀ {n}     → Poly n                        → Poly n
   _⊕_  : ∀ {n}     → Poly n → Poly n               → Poly n
   times : ∀ {l m n} → Poly l → Poly m → Add l m n → Poly n
infixl 5 _⊕_

⟦_⟧_ : ∀ {n} → Poly n → ℕ → ℕ
⟦ κ c ⟧ x = c
⟦ ι ⟧ x = x
⟦ ↑ p ⟧ x = ⟦ p ⟧ suc x
⟦ p ⊕ q ⟧ x = ⟦ p ⟧ x + ⟦ q ⟧ x
⟦ times p q add ⟧ x = ⟦ p ⟧ x * ⟦ q ⟧ x

sucl : ∀ {l m n} → Add l m n → Add (suc l) m (suc n)
sucl (0+n {zero})  = n+0
sucl (0+n {suc n}) = m+n 0+n
sucl (n+0 {zero})  = n+0
sucl (n+0 {suc n}) = n+0
sucl (m+n add)     = m+n (sucl add)

sucr : ∀ {l m n} → Add l m n → Add l (suc m) (suc n)
sucr 0+n           = 0+n
sucr (n+0 {zero})  = 0+n
sucr (n+0 {suc n}) = m+n n+0
sucr (m+n add)     = m+n (sucr add)

-- -- ∆(p ⊗ q) = (∆p ⊗ (q · (1+))) ⊕ (p ⊗ ∆q)
Δ : ∀ {n} → Poly (suc n) → Poly n
Δ (κ c) = κ 0
Δ ι = κ 1
Δ (↑ p) = ↑ (Δ p)
Δ (p ⊕ q) = Δ p ⊕ Δ q
Δ (times p q 0+n) = times (κ (⟦ p ⟧ 0)) (Δ q) 0+n
Δ (times p q n+0) = times (Δ p) (κ (⟦ q ⟧ 0)) n+0
Δ (times p q (m+n add)) = times (Δ p) (↑ q) (sucr add) ⊕ times p (Δ q) (sucl add)

add : ∀ l m → Add l m (l + m)
add zero m = 0+n
add (suc l) m = sucl (add l m)

_⊗_ : ∀ {l m} → Poly l → Poly m → Poly (l + m)
_⊗_ {l} {m} p q = times p q (add l m)
infixr 6 _⊗_

ι₁ : Poly 1
ι₁ = ι

κ₀ : ℕ → Poly 0
κ₀ c = κ c

_⊛_ : ∀ {m} → Poly m → (n : ℕ) → Poly (n * m)
p ⊛ zero = κ 1
p ⊛ suc n = {!   !}

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Experiments.NatMinusTwo.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Nat
open import Cubical.Data.NatMinusOne using (ℕ₋₁)
open import Cubical.Experiments.NatMinusTwo.Base

-2+Path : ℕ ≡ ℕ₋₂
-2+Path = isoToPath (iso -2+_ 2+_ (λ _ → refl) (λ _ → refl))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Generics.Prelude hiding (lookup; pi; curry)
open import Generics.Telescope
open import Generics.Desc
open import Generics.All
open import Generics.HasDesc
import Generics.Helpers as Helpers

module Generics.Constructions.Fold
  {P I ℓ} {A : Indexed P I ℓ} (H : HasDesc {P} {I} {ℓ} A)
  {p c} {X : Pred′ I λ i → Set c}
  where

open HasDesc H

private
  variable
    V : ExTele P
    i : ⟦ I ⟧tel p
    v : ⟦ V ⟧tel p

X′ : ⟦ I ⟧tel p → Set c
X′ i = unpred′ I _ X i

------------------------
-- Types of the algebra

levelAlg : ConDesc P V I → Level
levelAlg (var _) = c
levelAlg (π {ℓ} _ _ C) = ℓ ⊔ levelAlg C
levelAlg (A ⊗ B) = levelAlg A ⊔ levelAlg B

AlgIndArg : (C : ConDesc P V I) → ⟦ V ⟧tel p → Set (levelAlg C)
AlgIndArg (var f) v = X′ (f (p , v))
AlgIndArg (π ia S C) v = Π< ia > (S (p , v)) λ s → AlgIndArg C (v , s)
AlgIndArg (A ⊗ B) v = AlgIndArg A v × AlgIndArg B v

AlgCon : (C : ConDesc P V I) → ⟦ V ⟧tel p → Set (levelAlg C)
AlgCon (var f) v = X′ (f (p , v))
AlgCon (π ia S C) v = Π< ia > (S (p , v)) λ s → AlgCon C (v , s)
AlgCon (A ⊗ B) v = AlgIndArg A v → AlgCon B v

Algebra : ∀ k → Set (levelAlg (lookupCon D k))
Algebra k = AlgCon (lookupCon D k) tt

----------------
-- Generic fold

module _ (algs : Els Algebra) where

  fold-wf : (x : A′ (p , i)) → Acc x → X′ i

  foldData-wf : (x : ⟦ D ⟧Data A′ (p , i)) → AllDataω Acc D x → X′ i
  foldData-wf {i} (k , x) = foldCon (lookupCon D k) (algs k) x
    where
      foldIndArg : (C : ConDesc P V I)
                   (x : ⟦ C ⟧IndArg A′ (p , v))
                 → AllIndArgω Acc C x
                 → AlgIndArg C v
      foldIndArg (var f) x a = fold-wf x a
      foldIndArg (π ia S C) x a = fun< ia > λ s → foldIndArg C (app< ia > x s) (a s)
      foldIndArg (A ⊗ B) (xa , xb) (aa , ab)
        = foldIndArg A xa aa
        , foldIndArg B xb ab

      foldCon : (C   : ConDesc P V I)
                (alg : AlgCon C v)
                (x   : ⟦ C ⟧Con A′ (p , v , i))
              → AllConω Acc C x
              → X′ i
      foldCon (var _) alg refl _ = alg
      foldCon (π ia S C) alg (s , x) a = foldCon C (app< ia > alg s) x a
      foldCon (A ⊗ B) alg (xa , xb) (aa , ab)
        = foldCon B (alg (foldIndArg A xa aa)) xb ab

  fold-wf x (acc a) = foldData-wf (split x) a

  fold : A′ (p , i) → X′ i
  fold x = fold-wf x (wf x)

deriveFold : Arrows Algebra (Pred′ I λ i → A′ (p , i) → X′ i)
deriveFold = curryₙ λ m → pred′ I _ λ i → fold m

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
module Either where

  data Either (A : Set) (B : Set) : Set where
    left : A → Either A B
    right : B → Either A B

  [_,_] : ∀ {A B} {C : Set} → (A → C) → (B → C) → Either A B → C
  [ f , g ] (left x)  = f x
  [ f , g ] (right x) = g x

max_stars_repo_name: cantsin/agda-experiments

max_issues_repo_name: cantsin/agda-experiments

max_forks_repo_name: cantsin/agda-experiments


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

module Categories.Category.Instance.Properties.Cats where

open import Data.Product using (_,_)

open import Categories.Category
open import Categories.Category.Construction.Functors
  using (Functors; eval; module curry)
open import Categories.Category.Cartesian using (Cartesian)
import Categories.Category.CartesianClosed as CCC
import Categories.Category.CartesianClosed.Canonical as Canonical
open import Categories.Category.Instance.Cats using (Cats)
open import Categories.Category.Monoidal.Instance.Cats
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Bifunctor using (Bifunctor)
open import Categories.Functor.Construction.Constant using (constNat)
import Categories.Morphism.Reasoning as MR
open import Categories.NaturalTransformation
  using (NaturalTransformation; _∘ˡ_) renaming (id to idNT)
open import Categories.NaturalTransformation.NaturalIsomorphism
  using (NaturalIsomorphism; _≃_; module LeftRightId)

-- It's easier to define exponentials with respect to the *canonical*
-- product.  The more generic version can then be given by appealing
-- to uniqueness (up to iso) of products.

module CanonicallyCartesianClosed {l} where
  private
    module Cats = Category (Cats l l l)
    module Cart = Cartesian (Product.Cats-is {l} {l} {l})
  open Cats using (_⇒_) renaming (Obj to Cat)
  open Cart hiding (η)

  infixr 9 _^_

  _^_ : Cat → Cat → Cat
  B ^ A = Functors A B

  -- The β law (aka computation principle) for exponential objects

  eval-comp : ∀ {A B C} {G : C × A ⇒ B} → eval ∘F (curry.F₀ G ⁂ idF) ≃ G
  eval-comp {A} {B} {C} {G} = record
    { F⇒G = record
      { η           = λ _ → id B
      ; commute     = λ _ → ∘-resp-≈ʳ B commute ○ MR.id-comm-sym B
      ; sym-commute = λ _ → ⟺ (∘-resp-≈ʳ B commute ○ MR.id-comm-sym B)
      }
    ; F⇐G = record
      { η           = λ _ → id B
      ; commute     = λ _ → ⟺ (MR.id-comm B ○ ∘-resp-≈ʳ B commute)
      ; sym-commute = λ _ → MR.id-comm B ○ ∘-resp-≈ʳ B commute
      }
    ; iso = iso-id-id
    }
    where
      open Functor G renaming (F₀ to G₀; F₁ to G₁)
      open Category hiding (_∘_)
      open Category B using (_∘_)
      open HomReasoning B
      open LeftRightId G

      commute : ∀ {a₁ a₂ b₁ b₂} {f₁ : C [ a₁ , b₁ ]} {f₂ : A [ a₂ , b₂ ]} →
                B [ (G₁ (f₁ , id A) ∘ G₁ (id C , f₂)) ≈ G₁ (f₁ , f₂) ]
      commute {_} {_} {_} {_} {f₁} {f₂} = begin
          G₁ (f₁ , id A) ∘ G₁ (id C , f₂)
        ≈˘⟨ homomorphism ⟩
          G₁ (C [ f₁ ∘ id C ] , A [ id A ∘ f₂ ])
        ≈⟨ F-resp-≈ (identityʳ C , identityˡ A) ⟩
          G₁ (f₁ , f₂)
        ∎

  -- The η law (aka uniqueness principle) for exponential objects

  η-exp : ∀ {A B C} {H : C ⇒ B ^ A} → H ≃ curry.F₀ (eval ∘F (H ⁂ idF))
  η-exp {A} {B} {C} {H} = record
    { F⇒G = record
      { η = λ _ → record
        { η           = λ _ → id B
        ; commute     = λ f → ⟺ (MR.id-comm B ○ ∘-resp-≈ʳ B (commute₁ f))
        ; sym-commute = λ f → MR.id-comm B ○ ∘-resp-≈ʳ B (commute₁ f)
        }
      ; commute       = λ f → ⟺ (MR.id-comm B ○ ∘-resp-≈ʳ B (commute₂ f))
      ; sym-commute   = λ f → MR.id-comm B ○ ∘-resp-≈ʳ B (commute₂ f)
      }
    ; F⇐G = record
      { η = λ _ → record
        { η           = λ _ → id B
        ; commute     = λ f → ∘-resp-≈ʳ B (commute₁ f) ○ MR.id-comm-sym B
        ; sym-commute = λ f → ⟺ (∘-resp-≈ʳ B (commute₁ f) ○ MR.id-comm-sym B)
        }
      ; commute       = λ f → ∘-resp-≈ʳ B (commute₂ f) ○ MR.id-comm-sym B
      ; sym-commute   = λ f → ⟺ (∘-resp-≈ʳ B (commute₂ f) ○ MR.id-comm-sym B)
      }
    ; iso = λ _ → record { isoˡ = identity² B; isoʳ = identity² B }
    }
    where
      open Functor using (identity) renaming (F₁ to _$₁_)
      open Functor H hiding (identity) renaming (F₀ to H₀; F₁ to H₁)
      open Category hiding (_∘_)
      open Category B using (_∘_)
      open HomReasoning B
      open NaturalTransformation
      open LeftRightId H

      commute₁ : ∀ {a b c} (f : A [ a , b ]) →
                 B [ (η (H₁ (id C)) b ∘ (H₀ c $₁ f)) ≈ H₀ c $₁ f ]
      commute₁ {_} {b} {c} f = begin
        η (H₁ (id C)) b ∘ (H₀ c $₁ f)  ≈⟨ ∘-resp-≈ˡ B (identity H) ⟩
        id B ∘ (H₀ c $₁ f)             ≈⟨ identityˡ B ⟩
        H₀ c $₁ f                      ∎

      commute₂ : ∀ {c₁ c₂} (f : C [ c₁ , c₂ ]) {a} →
                 B [ (η (H₁ f) a ∘ (H₀ c₁ $₁ id A)) ≈ η (H₁ f) a ]
      commute₂ {c} {_} f {a} = begin
        η (H₁ f) a ∘ (H₀ c $₁ id A)    ≈⟨ ∘-resp-≈ʳ B (identity (H₀ c)) ⟩
        η (H₁ f) a ∘ id B              ≈⟨ identityʳ B ⟩
        η (H₁ f) a                     ∎

  curry-unique : ∀ {A B C} {G : C ⇒ B ^ A} {H : C × A ⇒ B} →
                 eval ∘F (G ⁂ idF) ≃ H → G ≃ curry.F₀ H
  curry-unique {A} {B} {C} {G} {H} hyp =
    begin
      G
    ≈⟨ η-exp {A} {B} {C} {G} ⟩
      curry.F₀ (eval ∘F (G ⁂ idF))
    ≈⟨ curry.resp-NI {F = eval ∘F (G ⁂ idF)} {H} hyp ⟩
      curry.F₀ H
    ∎
    where
      open Functor
      open Cats.HomReasoning

  Cats-CCC : Canonical.CartesianClosed (Cats l l l)
  Cats-CCC = record
    { !            = !
    ; π₁           = π₁
    ; π₂           = π₂
    ; ⟨_,_⟩        = ⟨_,_⟩
    ; !-unique     = !-unique
    ; π₁-comp      = λ {_} {_} {F} {_} {G} → project₁ {h = F} {i = G}
    ; π₂-comp      = λ {_} {_} {F} {_} {G} → project₂ {h = F} {i = G}
    ; ⟨,⟩-unique   = unique
    ; eval         = eval
    ; curry        = curry.F₀
    ; eval-comp    = λ {_} {_} {_} {G} → eval-comp {G = G}
    ; curry-resp-≈ = λ {_} {_} {_} {G} {H} → curry.resp-NI {F = G} {H}
    ; curry-unique = λ {_} {_} {_} {G} {H} → curry-unique {G = G} {H}
    }

  open Canonical.CartesianClosed Cats-CCC

Cats-CCC : ∀ {l} → CCC.CartesianClosed (Cats l l l)
Cats-CCC =
  Canonical.Equivalence.fromCanonical _ CanonicallyCartesianClosed.Cats-CCC

module CartesianClosed {l} = CCC.CartesianClosed (Cats-CCC {l})

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module Data.QuadTree.LensProofs.Valid-LensLeaf where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Agda.Primitive
open import Data.Lens.Proofs.LensLaws
open import Data.Lens.Proofs.LensPostulates
open import Data.Lens.Proofs.LensComposition
open import Data.QuadTree.InternalAgda
open import Data.QuadTree.Implementation.QuadrantLenses
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes

--- Lens laws for lensLeaf

ValidLens-Leaf-ViewSet : {t : Set} {{eqT : Eq t}} -> ViewSet (lensLeaf {t})
ValidLens-Leaf-ViewSet v (CVQuadrant (Leaf x)) = refl

ValidLens-Leaf-SetView :
    {t : Set} {{eqT : Eq t}}
    -> SetView (lensLeaf {t})
ValidLens-Leaf-SetView (CVQuadrant (Leaf x)) = refl

ValidLens-Leaf-SetSet :
    {t : Set} {{eqT : Eq t}}
    -> SetSet (lensLeaf {t})
ValidLens-Leaf-SetSet v1 v2 (CVQuadrant (Leaf x)) = refl

ValidLens-Leaf :
    {t : Set} {{eqT : Eq t}}
    -> ValidLens (VQuadrant t {0}) t
ValidLens-Leaf = CValidLens lensLeaf ValidLens-Leaf-ViewSet ValidLens-Leaf-SetView ValidLens-Leaf-SetSet

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


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

-- Borrowed from OldUnivalence/Equivalences.agda, without HoTT
-- and then upgraded to work on Setoid rather than just on ≡

module SetoidEquiv where

open import Level using (Level; zero; _⊔_)

open import Data.Empty using (⊥)
open import Data.Sum using (_⊎_; inj₁; inj₂)

import Function as Fun using (id)
open import Function.Equality using (id; _∘_; _⟶_; _⟨$⟩_; _⇨_; cong)
open import Relation.Binary using (Setoid; module Setoid)
open import Relation.Binary.PropositionalEquality as P using (setoid; →-to-⟶)

open Setoid

-- Equivalence of setoids

infix 4 _≃S_

------------------------------------------------------------------------------
-- A setoid gives us a set and an equivalence relation on that set.
-- The setoids constructed in PropositionalEquality (P) use ≡ as the
-- equivalence relation

-- the empty set with ≡

{--
0S : Setoid zero zero
0S = P.setoid ⊥
--}

-- sum of setoids
-- we take the disjoint union of the carriers and construct a new
-- equivalence relation that uses the underlying relations on each
-- summand (and is undefined on elements that come from different
-- summands)

{--
_⊎S_ : (AS : Setoid zero zero) (BS : Setoid zero zero) → Setoid zero zero
_⊎S_ AS BS = record
  { Carrier = A ⊎ B
  ; _≈_ = _∼₁_
  ; isEquivalence = record
    { refl = λ { {inj₁ _} → refl AS ; {inj₂ _} → refl BS}
    ; sym = λ {x} {y} → sym∼₁ {x} {y}
    ; trans = λ {x} {y} {z} → trans∼₁ {x} {y} {z} }
  }
  where
    A = Carrier AS
    B = Carrier BS

    _∼₁_ : A ⊎ B → A ⊎ B → Set
    inj₁ x ∼₁ inj₁ x₁ = _≈_ AS x x₁
    inj₁ x ∼₁ inj₂ y = ⊥
    inj₂ y ∼₁ inj₁ x = ⊥
    inj₂ y ∼₁ inj₂ y₁ = _≈_ BS y y₁

    sym∼₁ : {x y : A ⊎ B} → x ∼₁ y → y ∼₁ x
    sym∼₁ {inj₁ _} {inj₁ _} x~y = sym AS x~y
    sym∼₁ {inj₁ _} {inj₂ _} ()
    sym∼₁ {inj₂ _} {inj₁ _} ()
    sym∼₁ {inj₂ _} {inj₂ _} x~y = sym BS x~y

    trans∼₁ : Relation.Binary.Transitive _∼₁_
    trans∼₁ {inj₁ x} {inj₁ x₁} {inj₁ x₂} i~j j~k = trans AS i~j j~k
    trans∼₁ {inj₁ x} {inj₁ x₁} {inj₂ y} i~j ()
    trans∼₁ {inj₁ x} {inj₂ y} {inj₁ x₁} i~j ()
    trans∼₁ {inj₁ x} {inj₂ y}  () j~k
    trans∼₁ {inj₂ y} {inj₁ x} () j~k
    trans∼₁ {inj₂ y} {inj₂ y₁} {inj₁ x} i~j ()
    trans∼₁ {inj₂ y} {inj₂ y₁} {inj₂ y₂} i~j j~k = trans BS i~j j~k
--}

------------------------------------------------------------------------------
-- Equivalence of setoids

-- Two setoids are equivalent if

record _≃S_ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} (A : Setoid ℓ₁ ℓ₂) (B : Setoid ℓ₃ ℓ₄) :
  Set (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where
  constructor equiv

  field
    f : A ⟶ B
    g : B ⟶ A
    α : ∀ {x y} → _≈_ B x y → _≈_ B ((f ∘ g) ⟨$⟩ x) y
    β : ∀ {x y} → _≈_ A x y → _≈_ A ((g ∘ f) ⟨$⟩ x) y

{--
id≃S : ∀ {ℓ₁ ℓ₂} {A : Setoid ℓ₁ ℓ₂} → A ≃S A
id≃S {A = A} = equiv id id Fun.id Fun.id

sym≃S : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Setoid ℓ₁ ℓ₂} {B : Setoid ℓ₃ ℓ₄} →
        (A ≃S B) → B ≃S A
sym≃S eq = equiv e.g e.f e.β e.α
  where module e = _≃S_ eq

trans≃S : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄ ℓ₅ ℓ₆}
          {A : Setoid ℓ₁ ℓ₂} {B : Setoid ℓ₃ ℓ₄} {C : Setoid ℓ₅ ℓ₆} →
          A ≃S B → B ≃S C → A ≃S C
trans≃S {A = A} {B} {C} A≃B B≃C = equiv f g α' β'
  where
    module fm = _≃S_ A≃B
    module gm = _≃S_ B≃C
    f : A ⟶ C
    f = gm.f ∘ fm.f
    g : C ⟶ A
    g = fm.g ∘ gm.g
    α' : _≈_ (C ⇨ C) (f ∘ g)  id
    α' = λ z → trans C (cong gm.f (fm.α (cong gm.g (refl C)))) (gm.α z)
    β' : _≈_ (A ⇨ A) (g ∘ f) id
    β' = λ z → trans A (cong fm.g (gm.β (cong fm.f (refl A)))) (fm.β z)

_✴_ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Setoid ℓ₁ ℓ₂} {B : Setoid ℓ₃ ℓ₄} →
      (A ≃S B) → (x : Carrier A) → Carrier B
(equiv f _ _ _) ✴ x = f ⟨$⟩ x
--}

-- can't use id because it is not sufficiently dependently typed!

{--
0≃S : 0S ≃S 0S
0≃S = equiv id id (λ x → x) (λ x → x)
--}

-- just to make things prettier

_≃S≡_ : ∀ {ℓ₁} → (A B : Set ℓ₁) → Set ℓ₁
A ≃S≡ B = (P.setoid A) ≃S (P.setoid B)

-- Need to be able to take ⊎ of ≃S-Setoids
{--
_⊎≃S_ : {A B C D : Set} → A ≃S≡ B → C ≃S≡ D → (A ⊎ C) ≃S≡ (B ⊎ D)
_⊎≃S_ {A} {B} {C} {D} (equiv f g α β) (equiv f₁ g₁ α₁ β₁) =
  equiv (→-to-⟶ ff) (→-to-⟶ gg) αα ββ
  where
    ff : A ⊎ C → B ⊎ D
    ff (inj₁ x) = inj₁ (f ⟨$⟩ x)
    ff (inj₂ y) = inj₂ (f₁ ⟨$⟩ y)
    gg : B ⊎ D → A ⊎ C
    gg (inj₁ x) = inj₁ (g ⟨$⟩ x)
    gg (inj₂ y) = inj₂ (g₁ ⟨$⟩ y)
    αα : {x y : B ⊎ D} → x P.≡ y → ff (gg x) P.≡ y
    αα {inj₁ x} P.refl = P.cong inj₁ (α P.refl)
    αα {inj₂ y} P.refl = P.cong inj₂ (α₁ P.refl)
    ββ : {x y : A ⊎ C} → x P.≡ y → gg (ff x) P.≡ y
    ββ {inj₁ x} P.refl = P.cong inj₁ (β P.refl)
    ββ {inj₂ y} P.refl = P.cong inj₂ (β₁ P.refl)
--}
-- note that this appears to be redundant (especially when looking at
-- the proofs), but having both f and g is needed for inference of
-- other aspects to succeed.

record _≋_ {ℓ₁} {A B : Set ℓ₁} (eq₁ eq₂ : A ≃S≡ B) : Set ℓ₁ where
  constructor equivS
  field
    f≡ : ∀ (x : A) → P._≡_ (_≃S_.f eq₁ ⟨$⟩ x) (_≃S_.f eq₂ ⟨$⟩ x)
    g≡ : ∀ (x : B) → P._≡_ (_≃S_.g eq₁ ⟨$⟩ x) (_≃S_.g eq₂ ⟨$⟩ x)

id≋ : ∀ {ℓ} {A B : Set ℓ} {x : A ≃S≡ B} → x ≋ x
id≋ = record { f≡ = λ x → P.refl ; g≡ = λ x → P.refl }

sym≋ : ∀ {ℓ} {A B : Set ℓ} {x y : A ≃S≡ B} → x ≋ y → y ≋ x
sym≋ (equivS f≡ g≡) = equivS (λ a → P.sym (f≡ a)) (λ b → P.sym (g≡ b))

trans≋ : ∀ {ℓ} {A B : Set ℓ} {x y z : A ≃S≡ B} → x ≋ y → y ≋ z → x ≋ z
trans≋ (equivS f≡ g≡) (equivS h≡ i≡) =
   equivS (λ a → P.trans (f≡ a) (h≡ a)) (λ b → P.trans (g≡ b) (i≡ b))

-- WARNING: this is not generic, but specific to ≡-Setoids of functions.

≃S-Setoid : ∀ {ℓ₁} → (A B : Set ℓ₁) → Setoid ℓ₁ ℓ₁
≃S-Setoid {ℓ₁} A B = record
  { Carrier = AS ≃S BS
  ; _≈_ = _≋_
  ; isEquivalence = record
    { refl = id≋
    ; sym = sym≋
    ; trans = trans≋
    }
  }
  where
    open _≃S_
    AS = P.setoid A
    BS = P.setoid B

-- equivalences are injective

{--
inj≃ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Setoid ℓ₁ ℓ₂} {B : Setoid ℓ₃ ℓ₄} →
       (eq : A ≃S B) → {x y : Carrier A} →
       _≈_ B (eq ✴ x)  (eq ✴ y) → _≈_ A x y
inj≃ {A = A'} (equiv f g _ β) p =
  A.trans (A.sym (β A.refl)) (A.trans (cong g p) (β A.refl))
  where
    module A = Setoid A'
--}

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------------
-- Well-founded induction on the natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.Induction.Acc.WF-I where

open import FOTC.Base
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Inequalities.EliminationPropertiesI
open import FOTC.Data.Nat.Inequalities.PropertiesI
open import FOTC.Data.Nat.Type
open import FOTC.Induction.WF

------------------------------------------------------------------------------
-- The relation _<_ is well-founded.
module <-WF where
  <-wf : WellFounded _<_
  <-wf Nn = acc (helper Nn)
    where
    -- N.B. The helper function is the same that the function used by
    -- FOTC.Data.Nat.Induction.NonAcc.WellFoundedInductionATP.
    helper : ∀ {n m} → N n → N m → m < n → Acc N _<_ m
    helper nzero Nm m<0  = ⊥-elim (x<0→⊥ Nm m<0)
    helper (nsucc _) nzero 0<Sn = acc (λ Nm' m'<0 → ⊥-elim (x<0→⊥ Nm' m'<0))
    helper (nsucc {n} Nn) (nsucc {m} Nm) Sm<Sn =
      acc (λ {m'} Nm' m'<Sm →
             let m<n : m < n
                 m<n = Sx<Sy→x<y Sm<Sn

                 m'<n : m' < n
                 m'<n = case (λ m'<m → <-trans Nm' Nm Nn m'<m m<n)
                             (λ m'≡m → x≡y→y<z→x<z m'≡m m<n)
                             (x<Sy→x<y∨x≡y Nm' Nm m'<Sm)

             in  helper Nn Nm' m'<n
          )

  -- Well-founded induction on the natural numbers.
  <-wfind : (A : D → Set) →
             (∀ {n} → N n → (∀ {m} → N m → m < n → A m) → A n) →
             ∀ {n} → N n → A n
  <-wfind A = WellFoundedInduction <-wf

------------------------------------------------------------------------------
-- The relation _<_ is well-founded (a different proof).
module <-WF' where

  <-wf : WellFounded {N} _<_
  <-wf nzero      = acc (λ Nm m<0 → ⊥-elim (x<0→⊥ Nm m<0))
  <-wf (nsucc Nn) = acc (λ Nm m<Sn → helper Nm Nn (<-wf Nn)
                                          (x<Sy→x≤y Nm Nn m<Sn))
    where
    helper : ∀ {n m} → N n → N m → Acc N _<_ m → n ≤ m → Acc N _<_ n
    helper {n} {m} Nn Nm (acc h) n≤m = case (λ n<m → h Nn n<m)
                                            (λ n≡m → helper₁ (sym n≡m) (acc h))
                                            (x≤y→x<y∨x≡y Nn Nm n≤m)
      where
      helper₁ : ∀ {a b} → a ≡ b → Acc N _<_ a → Acc N _<_ b
      helper₁ refl h = h


text:
module Prelude.Ord.Properties where

open import Prelude.Ord
open import Prelude.Empty
open import Prelude.Equality
open import Prelude.Equality.Inspect

open import Prelude.Function
open import Prelude.Decidable
open import Prelude.Bool
open import Prelude.Bool.Properties

-- Ord/Laws extra lemmas
module _  {ℓ} {A : Set ℓ} {{_ : Ord/Laws A}} where

  <⇒≤ : {a b : A} → a < b → a ≤ b
  <⇒≤ = lt-to-leq

  ≡⇒≮ : {a b : A} → a ≡ b → a ≮ b
  ≡⇒≮ refl a<b = less-antisym a<b a<b

  <⇒≱ : {a b : A} → a < b → a ≱ b
  <⇒≱ = flip leq-less-antisym

  ≮⇒≥ : {a b : A} → a ≮ b → a ≥ b
  ≮⇒≥ {a = a} {b = b} ¬a<b
    with compare a b
  ...| less a<b = ⊥-elim (¬a<b a<b)
  ...| equal a≡b = eq-to-leq (sym a≡b)
  ...| greater a>b = lt-to-leq a>b

  ≰⇒> : {a b : A} → a ≰ b → a > b
  ≰⇒> {a = a} {b = b} a≰b
    with compare a b
  ...| less a<b = ⊥-elim (a≰b (lt-to-leq a<b))
  ...| equal a≡b = ⊥-elim (a≰b (eq-to-leq a≡b))
  ...| greater b>a = b>a

  ≰⇒≥ : {a b : A} → a ≰ b → a ≥ b
  ≰⇒≥ = <⇒≤ ∘ ≰⇒>

  <?⇒< :  {a b : A} → (a <? b) ≡ true → a < b
  <?⇒< {a = a} {b = b} a<?b
    with compare a b
  ...| less a<b = a<b
  ...| equal a≡b rewrite a≡b = case a<?b of λ ()
  ...| greater _ = case a<?b of λ ()

  ≮?⇒≮ : {a b : A} → (a <? b) ≡ false → a ≮ b
  ≮?⇒≮ {a = a} {b = b} a≮?b
    with compare a b
  ...| less _ = case a≮?b of λ ()
  ...| equal a≡b rewrite a≡b = λ a<b → ⊥-elim (less-antirefl a<b)
  ...| greater a>b = λ a<b → ⊥-elim (less-antisym a>b a<b)

  ≤?⇒≤ :  {a b : A} → (a ≤? b) ≡ true → a ≤ b
  ≤?⇒≤ {a = a} {b = b} a≤?b
    with inspect (compare b a)
  ...| less a<b with≡ compare≡ rewrite compare≡ =
       case a≤?b of λ ()
  ...| equal a≡b with≡ _ = eq-to-leq (sym a≡b)
  ...| greater a>b with≡ _ = lt-to-leq a>b

  ≰?⇒≰ :  {a b : A} → (a ≤? b) ≡ false → a ≰ b
  ≰?⇒≰ {a = a} {b = b} a≰?b
    with (compare b a)
  ...| less b<a = <⇒≱ b<a
  ...| equal a≡b rewrite a≡b = case a≰?b of λ ()
  ...| greater _ = case a≰?b of λ ()

  ≰?⇒≥ : {a b : A} → (a ≤? b) ≡ false → a ≥ b
  ≰?⇒≥ = ≰⇒≥ ∘ ≰?⇒≰

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.ZariskiLattice.BasicOpens 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.Foundations.Structure
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.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.Relation.Binary.Poset

open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Localisation.Base
open import Cubical.Algebra.CommRing.Localisation.UniversalProperty
open import Cubical.Algebra.CommRing.Localisation.InvertingElements
open import Cubical.Algebra.CommAlgebra.Base
open import Cubical.Algebra.CommAlgebra.Properties
open import Cubical.Algebra.CommAlgebra.Localisation
open import Cubical.Algebra.RingSolver.ReflectionSolving
open import Cubical.Algebra.Semilattice

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

open Iso
open BinaryRelation
open isEquivRel

private
  variable
    ℓ ℓ' : Level

module Presheaf (A' : CommRing ℓ) where
 open CommRingStr (snd A') renaming (_·_ to _·r_ ; ·-comm to ·r-comm ; ·Assoc to ·rAssoc
                                                 ; ·Lid to ·rLid ; ·Rid to ·rRid)
 open Exponentiation A'
 open CommRingTheory A'
 open isMultClosedSubset
 open CommAlgebraStr ⦃...⦄
 private
  A = fst A'

  A[1/_] : A → CommAlgebra A' ℓ
  A[1/ x ] = AlgLoc.S⁻¹RAsCommAlg A' ([_ⁿ|n≥0] A' x) (powersFormMultClosedSubset _ _)

  A[1/_]ˣ : (x : A) → ℙ (fst A[1/ x ])
  A[1/ x ]ˣ = (CommAlgebra→CommRing A[1/ x ]) ˣ

 _≼_ : A → A → Type ℓ
 x ≼ y = ∃[ n ∈ ℕ ] Σ[ z ∈ A ] x ^ n ≡ z ·r y -- rad(x) ⊆ rad(y)

-- ≼ is a pre-order:
 Refl≼ : isRefl _≼_
 Refl≼ x = PT.∣ 1 , 1r , ·r-comm _ _ ∣

 Trans≼ : isTrans _≼_
 Trans≼ x y z = map2 Trans≼Σ
  where
  Trans≼Σ : Σ[ n ∈ ℕ ] Σ[ a ∈ A ] x ^ n ≡ a ·r y
          → Σ[ n ∈ ℕ ] Σ[ a ∈ A ] y ^ n ≡ a ·r z
          → Σ[ n ∈ ℕ ] Σ[ a ∈ A ] x ^ n ≡ a ·r z
  Trans≼Σ (n , a , p) (m , b , q) = n ·ℕ m , (a ^ m ·r b) , path
   where
   path : x ^ (n ·ℕ m) ≡ a ^ m ·r b ·r z
   path = x ^ (n ·ℕ m)    ≡⟨ ^-rdist-·ℕ x n m ⟩
          (x ^ n) ^ m     ≡⟨ cong (_^ m) p ⟩
          (a ·r y) ^ m     ≡⟨ ^-ldist-· a y m ⟩
          a ^ m ·r y ^ m   ≡⟨ cong (a ^ m ·r_) q ⟩
          a ^ m ·r (b ·r z) ≡⟨ ·rAssoc _ _ _ ⟩
          a ^ m ·r b ·r z   ∎

 R : A → A → Type ℓ
 R x y = x ≼ y × y ≼ x -- rad(x) ≡ rad(y)

 RequivRel : isEquivRel R
 RequivRel .reflexive x = Refl≼ x , Refl≼ x
 RequivRel .symmetric _ _ Rxy = (Rxy .snd) , (Rxy .fst)
 RequivRel .transitive _ _ _ Rxy Ryz = Trans≼ _ _ _ (Rxy .fst) (Ryz .fst)
                                     , Trans≼ _ _ _  (Ryz .snd) (Rxy .snd)

 RpropValued : isPropValued R
 RpropValued x y = isProp× isPropPropTrunc isPropPropTrunc

 powerIs≽ : (x a : A) → x ∈ ([_ⁿ|n≥0] A' a) → a ≼ x
 powerIs≽ x a = map powerIs≽Σ
  where
  powerIs≽Σ : Σ[ n ∈ ℕ ] (x ≡ a ^ n) → Σ[ n ∈ ℕ ] Σ[ z ∈ A ] (a ^ n ≡ z ·r x)
  powerIs≽Σ (n , p) = n , 1r , sym p ∙ sym (·rLid _)

 module ≼ToLoc (x y : A) where
  private
   instance
    _ = snd A[1/ x ]

  lemma : x ≼ y → y ⋆ 1a ∈ A[1/ x ]ˣ -- y/1 ∈ A[1/x]ˣ
  lemma = PT.rec (A[1/ x ]ˣ (y ⋆ 1a) .snd) lemmaΣ
   where
   path1 : (y z : A) → 1r ·r (y ·r 1r ·r z) ·r 1r ≡ z ·r y
   path1 = solve A'
   path2 : (xn : A) → xn ≡ 1r ·r 1r ·r (1r ·r 1r ·r xn)
   path2 = solve A'

   lemmaΣ : Σ[ n ∈ ℕ ] Σ[ a ∈ A ] x ^ n ≡ a ·r y → y ⋆ 1a ∈ A[1/ x ]ˣ
   lemmaΣ (n , z , p) = [ z , (x ^ n) ,  PT.∣ n , refl ∣ ] -- xⁿ≡zy → y⁻¹ ≡ z/xⁿ
                      , eq/ _ _ ((1r , powersFormMultClosedSubset _ _ .containsOne)
                      , (path1 _ _ ∙∙ sym p ∙∙ path2 _))

 module ≼PowerToLoc (x y : A) (x≼y : x ≼ y) where
  private
   [yⁿ|n≥0] = [_ⁿ|n≥0] A' y
   instance
    _ = snd A[1/ x ]
  lemma : ∀ (s : A) → s ∈ [yⁿ|n≥0] → s ⋆ 1a ∈ A[1/ x ]ˣ
  lemma _ s∈[yⁿ|n≥0] = ≼ToLoc.lemma _ _ (Trans≼ _ y _ x≼y (powerIs≽ _ _ s∈[yⁿ|n≥0]))

 𝓞ᴰ : A / R → CommAlgebra A' ℓ
 𝓞ᴰ = rec→Gpd.fun isGroupoidCommAlgebra (λ a → A[1/ a ]) RCoh LocPathProp
    where
    RCoh : ∀ a b → R a b → A[1/ a ] ≡ A[1/ b ]
    RCoh a b (a≼b , b≼a) = fst (isContrS₁⁻¹R≡S₂⁻¹R (≼PowerToLoc.lemma _ _ b≼a)
                                                   (≼PowerToLoc.lemma _ _ a≼b))
     where
     open AlgLocTwoSubsets A' ([_ⁿ|n≥0] A' a) (powersFormMultClosedSubset _ _)
                              ([_ⁿ|n≥0] A' b) (powersFormMultClosedSubset _ _)

    LocPathProp : ∀ a b → isProp (A[1/ a ] ≡ A[1/ b ])
    LocPathProp a b = isPropS₁⁻¹R≡S₂⁻¹R
     where
     open AlgLocTwoSubsets A' ([_ⁿ|n≥0] A' a) (powersFormMultClosedSubset _ _)
                              ([_ⁿ|n≥0] A' b) (powersFormMultClosedSubset _ _)

 -- The quotient A/R corresponds to the basic opens of the Zariski topology.
 -- Multiplication lifts to the quotient and corresponds to intersection
 -- of basic opens, i.e. we get a meet-semilattice with:
 _∧/_ : A / R → A / R → A / R
 _∧/_ = setQuotSymmBinOp (RequivRel .reflexive) (RequivRel .transitive) _·r_
          (λ a b → subst (λ x → R (a ·r b) x) (·r-comm a b) (RequivRel .reflexive (a ·r b))) ·r-lcoh
  where
  ·r-lcoh-≼ : (x y z : A) → x ≼ y → (x ·r z) ≼ (y ·r z)
  ·r-lcoh-≼ x y z = map ·r-lcoh-≼Σ
   where
   path : (x z a y zn : A) →  x ·r z ·r (a ·r y ·r zn) ≡ x ·r zn ·r a ·r (y ·r z)
   path = solve A'

   ·r-lcoh-≼Σ : Σ[ n ∈ ℕ ] Σ[ a ∈ A ] x ^ n ≡ a ·r y
              → Σ[ n ∈ ℕ ] Σ[ a ∈ A ] (x ·r z) ^ n ≡ a ·r (y ·r z)
   ·r-lcoh-≼Σ  (n , a , p) = suc n , (x ·r z ^ n ·r a) , (cong (x ·r z ·r_) (^-ldist-· _ _ _)
                                                       ∙∙ cong (λ v → x ·r z ·r (v ·r z ^ n)) p
                                                       ∙∙ path _ _ _ _ _)

  ·r-lcoh : (x y z : A) → R x y → R (x ·r z) (y ·r z)
  ·r-lcoh x y z Rxy = ·r-lcoh-≼ x y z (Rxy .fst) , ·r-lcoh-≼ y x z (Rxy .snd)

 BasicOpens : Semilattice ℓ
 BasicOpens = makeSemilattice [ 1r ] _∧/_ squash/
   (elimProp3 (λ _ _ _ → squash/ _ _) λ _ _ _ → cong [_] (·rAssoc _ _ _))
     (elimProp (λ _ → squash/ _ _) λ _ → cong [_] (·rRid _))
       (elimProp (λ _ → squash/ _ _) λ _ → cong [_] (·rLid _))
         (elimProp2 (λ _ _ → squash/ _ _) λ _ _ → cong [_] (·r-comm _ _))
           (elimProp (λ _ → squash/ _ _) λ a → eq/ _ _ -- R a a²
              (∣ 1 , a , ·rRid _ ∣ , ∣ 2 , 1r , cong (a ·r_) (·rRid a) ∙ sym (·rLid _) ∣))

 -- The induced partial order
 open MeetSemilattice BasicOpens renaming (_≤_ to _≼/_ ; IndPoset to BasicOpensAsPoset)

 -- coincides with our ≼
 ≼/CoincidesWith≼ : ∀ (x y : A) → ([ x ] ≼/ [ y ]) ≡ (x ≼ y)
 ≼/CoincidesWith≼ x y = [ x ] ≼/ [ y ] -- ≡⟨ refl ⟩ [ x ·r y ] ≡ [ x ]
                      ≡⟨ isoToPath (isEquivRel→effectiveIso RpropValued RequivRel _ _) ⟩
                        R (x ·r y) x
                      ≡⟨ isoToPath Σ-swap-Iso ⟩
                        R x (x ·r y)
                      ≡⟨ hPropExt (RpropValued _ _) isPropPropTrunc ·To≼ ≼To· ⟩
                        x ≼ y ∎
  where
  x≼xy→x≼yΣ : Σ[ n ∈ ℕ ] Σ[ z ∈ A ] x ^ n ≡ z ·r (x ·r y)
            → Σ[ n ∈ ℕ ] Σ[ z ∈ A ] x ^ n ≡ z ·r y
  x≼xy→x≼yΣ (n , z , p) =  n , (z ·r x) , p ∙ ·rAssoc _ _ _

  ·To≼ : R x (x ·r y) → x ≼ y
  ·To≼ (x≼xy , _) = PT.map x≼xy→x≼yΣ x≼xy

  x≼y→x≼xyΣ : Σ[ n ∈ ℕ ] Σ[ z ∈ A ] x ^ n ≡ z ·r y
            → Σ[ n ∈ ℕ ] Σ[ z ∈ A ] x ^ n ≡ z ·r (x ·r y)
  x≼y→x≼xyΣ (n , z , p) = suc n , z , cong (x ·r_) p ∙ ·-commAssocl _ _ _

  ≼To· : x ≼ y → R x ( x ·r y)
  ≼To· x≼y = PT.map x≼y→x≼xyΣ x≼y , PT.∣ 1 , y , ·rRid _ ∙ ·r-comm _ _ ∣

 open IsPoset
 open PosetStr
 Refl≼/ : isRefl _≼/_
 Refl≼/ = BasicOpensAsPoset .snd .isPoset .is-refl

 Trans≼/ : isTrans _≼/_
 Trans≼/ = BasicOpensAsPoset .snd .isPoset .is-trans

 -- The restrictions:
 ρᴰᴬ : (a b : A) → a ≼ b → isContr (CommAlgebraHom A[1/ b ] A[1/ a ])
 ρᴰᴬ _ b a≼b = A[1/b]HasUniversalProp _ (≼PowerToLoc.lemma _ _ a≼b)
  where
  open AlgLoc A' ([_ⁿ|n≥0] A' b) (powersFormMultClosedSubset _ _)
       renaming (S⁻¹RHasAlgUniversalProp to A[1/b]HasUniversalProp)

 ρᴰᴬId : ∀ (a : A) (r : a ≼ a) → ρᴰᴬ a a r .fst ≡ idAlgHom
 ρᴰᴬId a r = ρᴰᴬ a a r .snd _

 ρᴰᴬComp : ∀ (a b c : A) (l : a ≼ b) (m : b ≼ c)
         → ρᴰᴬ a c (Trans≼ _ _ _ l m) .fst ≡ ρᴰᴬ a b l .fst ∘a ρᴰᴬ b c m .fst
 ρᴰᴬComp a _ c l m = ρᴰᴬ a c (Trans≼ _ _ _ l m) .snd _

 ρᴰ : (x y : A / R) → x ≼/ y → CommAlgebraHom (𝓞ᴰ y) (𝓞ᴰ x)
 ρᴰ = elimContr2 λ _ _ → isContrΠ
                 λ [a]≼/[b] → ρᴰᴬ _ _ (transport (≼/CoincidesWith≼ _ _) [a]≼/[b])

 ρᴰId : ∀ (x : A / R) (r : x ≼/ x) → ρᴰ x x r ≡ idAlgHom
 ρᴰId = SQ.elimProp (λ _ → isPropΠ (λ _ → isSetAlgebraHom _ _ _ _))
                     λ a r → ρᴰᴬId  a (transport (≼/CoincidesWith≼ _ _) r)

 ρᴰComp : ∀ (x y z : A / R) (l : x ≼/ y) (m : y ≼/ z)
        → ρᴰ x z (Trans≼/ _ _ _ l m) ≡ ρᴰ x y l ∘a ρᴰ y z m
 ρᴰComp = SQ.elimProp3 (λ _ _ _ → isPropΠ2 (λ _ _ → isSetAlgebraHom _ _ _ _))
                        λ a b c _ _ → sym (ρᴰᴬ a c _ .snd _) ∙ ρᴰᴬComp a b c _ _

max_stars_repo_name: dolio/cubical

max_issues_repo_name: dolio/cubical

max_forks_repo_name: dolio/cubical


text:
-- NB. This test fail if Agda is called with the --no-sharing option.

module Issue1351 where

open import Common.Equality
open import Common.Prelude

f1 : Nat → Nat
f1 x = x + x

f2 : Nat → Nat
f2 x = f1 (f1 x)

f4 : Nat → Nat
f4 x = f2 (f2 x)

f8 : Nat → Nat
f8 x = f4 (f4 x)

f16 : Nat → Nat
f16 x = f8 (f8 x)

f32 : Nat → Nat
f32 x = f16 (f16 x)

thm : f32 1 ≡ 4294967296
thm = refl