text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Subset.Setoid.Properties directly.
------------------------------------------------------------------------

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

module Data.List.Relation.Subset.Setoid.Properties where

open import Data.List.Relation.Binary.Subset.Setoid.Properties public


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

open import lib.Basics
open import lib.types.TLevel
open import lib.types.Group
open import lib.types.LoopSpace
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism

module lib.groups.LoopSpace where

{- A loop space is a pregroup, and a group if it has the right level -}
module _ {i} (n : ℕ) (X : Ptd i) where

  Ω^S-group-structure : GroupStructure (Ω^ (S n) X)
  Ω^S-group-structure = record {
    ident = idp^ (S n);
    inv = Ω^S-! n;
    comp = Ω^S-∙ n;
    unit-l = Ω^S-∙-unit-l n;
    assoc = Ω^S-∙-assoc n;
    inv-l = Ω^S-!-inv-l n
    }

  Ω^S-group : has-level ⟨ S n ⟩ (de⊙ X) → Group i
  Ω^S-group pX = group
    (Ω^ (S n) X)
    (Ω^-level 0 (S n) X $
       transport (λ t → has-level t (de⊙ X)) (! (+2+0 ⟨ S n ⟩₋₂)) pX)
    Ω^S-group-structure

module _ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j} where
  Ω^S-group-structure-fmap : X ⊙→ Y
    → GroupStructureHom (Ω^S-group-structure n X) (Ω^S-group-structure n Y)
  Ω^S-group-structure-fmap F = group-structure-hom (Ω^-fmap (S n) F) (Ω^S-fmap-∙ n F)

  Ω^S-group-structure-isemap : {F : X ⊙→ Y}
    → is-equiv (fst F) → is-equiv (GroupStructureHom.f (Ω^S-group-structure-fmap F))
  Ω^S-group-structure-isemap {F} F-is-equiv = Ω^-isemap (S n) F F-is-equiv

  Ω^S-group-structure-emap : X ⊙≃ Y
    → Ω^S-group-structure n X ≃ᴳˢ Ω^S-group-structure n Y
  Ω^S-group-structure-emap (F , F-is-equiv) =
    Ω^S-group-structure-fmap F , Ω^S-group-structure-isemap F-is-equiv

module _ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j}
  (X-level : has-level ⟨ S n ⟩ (de⊙ X))
  (Y-level : has-level ⟨ S n ⟩ (de⊙ Y))
  where

  Ω^S-group-fmap : X ⊙→ Y → Ω^S-group n X X-level →ᴳ Ω^S-group n Y Y-level
  Ω^S-group-fmap = →ᴳˢ-to-→ᴳ ∘ Ω^S-group-structure-fmap n

  Ω^S-group-emap : X ⊙≃ Y → Ω^S-group n X X-level ≃ᴳ Ω^S-group n Y Y-level
  Ω^S-group-emap = ≃ᴳˢ-to-≃ᴳ ∘ Ω^S-group-structure-emap n

ext: agda

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

open import lemmas-general
open import preservation

module eval-checks where
  eval-unicity : ∀{⛽ Δ Σ' Γ E e τ r r' K K'} →
                   Δ , Σ' , Γ ⊢ E →
                   Δ , Σ' , Γ ⊢ e :: τ →
                   E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ K →
                   E ⊢ e ⌊ ⛽ ⌋⇒ r' ⊣ K' →
                   r == r' ∧ K == K'

  xc-unicity : ∀{Δ Σ' r1 r2 τ K K'} →
                 Δ , Σ' ⊢ r1 ·: τ →
                 Δ , Σ' ⊢ r2 ·: τ →
                 Constraints⦃ r1 , r2 ⦄:= K →
                 Constraints⦃ r1 , r2 ⦄:= K' →
                 K == K'

  eval-unicity Γ⊢E (TAFix _) EFix EFix = refl , refl
  eval-unicity Γ⊢E (TAVar _) (EVar h) (EVar h') = ctxunicity h h' , refl
  eval-unicity Γ⊢E (TAApp _ ta-f ta-arg) (EAppFix f1 form eval-f eval-arg eval) (EAppFix f2 form' eval-f' eval-arg' eval')
    rewrite form | form'
    with eval-unicity Γ⊢E ta-f eval-f eval-f' | eval-unicity Γ⊢E ta-arg eval-arg eval-arg'
  ... | refl , refl | refl , refl
    with preservation Γ⊢E ta-f eval-f
  ... | TAFix Γ'⊢Ef (TAFix ta-ef)
    rewrite Fuel-depletion-unicity f1 f2
    with eval-unicity (EnvInd (EnvInd Γ'⊢Ef (preservation Γ⊢E ta-f eval-f)) (preservation Γ⊢E ta-arg eval-arg)) ta-ef eval eval'
  ... | refl , refl = refl , refl
  eval-unicity Γ⊢E TAUnit EUnit EUnit = refl , refl
  eval-unicity Γ⊢E (TAApp x ta-e ta-e₁) (EAppFix x₁ form eval eval₁ eval₂) (EAppUnfinished eval' nf eval'')
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl
    rewrite form
      = abort (nf refl)
  eval-unicity Γ⊢E (TAApp x ta-e ta-e₁) (EAppUnfinished eval nf eval₁) (EAppFix x₂ form eval' eval'' eval''')
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl
    rewrite form
      = abort (nf refl)
  eval-unicity Γ⊢E (TAApp x ta-f ta-arg) (EAppUnfinished eval-f x₁ eval-arg) (EAppUnfinished eval-f' x₂ eval-arg')
    with eval-unicity Γ⊢E ta-f eval-f eval-f' | eval-unicity Γ⊢E ta-arg eval-arg eval-arg'
  ... | refl , refl | refl , refl = refl , refl
  eval-unicity Γ⊢E (TAPair x ta-e1 ta-e2) (EPair eval1 eval2) (EPair eval1' eval2')
    with eval-unicity Γ⊢E ta-e1 eval1 eval1' | eval-unicity Γ⊢E ta-e2 eval2 eval2'
  ... | refl , refl | refl , refl = refl , refl
  eval-unicity Γ⊢E (TAFst ta-e) (EFst eval) (EFst eval')
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = refl , refl
  eval-unicity Γ⊢E (TAFst ta-e) (EFst eval) (EFstUnfinished eval' np)
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = abort (np refl)
  eval-unicity Γ⊢E (TAFst ta-e) (EFstUnfinished eval np) (EFst eval')
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = abort (np refl)
  eval-unicity Γ⊢E (TAFst ta-e) (EFstUnfinished eval x) (EFstUnfinished eval' x₁)
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = refl , refl
  eval-unicity Γ⊢E (TASnd ta-e) (ESnd eval) (ESnd eval')
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = refl , refl
  eval-unicity Γ⊢E (TASnd ta-e) (ESnd eval) (ESndUnfinished eval' np)
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = abort (np refl)
  eval-unicity Γ⊢E (TASnd ta-e) (ESndUnfinished eval np) (ESnd eval')
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = abort (np refl)
  eval-unicity Γ⊢E (TASnd ta-e) (ESndUnfinished eval x) (ESndUnfinished eval' x₁)
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = refl , refl
  eval-unicity Γ⊢E (TACtor x x₁ ta-e) (ECtor eval) (ECtor eval')
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = refl , refl
  eval-unicity Γ⊢E (TACase d∈σ' ta-e x₁ ta-rules) (EMatch f1 form eval-e eval-ec) (EMatch f2 form' eval'-e eval'-ec)
    with eval-unicity Γ⊢E ta-e eval-e eval'-e
  ... | refl , refl
    with ctxunicity form form'
  ... | refl
    with ta-rules form
  ... | _ , _ , _ , c∈cctx , ta-ec
    with preservation Γ⊢E ta-e eval-e
  ... | TACtor d∈'σ' c∈'cctx ta-r'
    rewrite ctxunicity d∈σ' d∈'σ' | ctxunicity c∈cctx c∈'cctx | Fuel-depletion-unicity f1 f2
    with eval-unicity (EnvInd Γ⊢E ta-r') ta-ec eval-ec eval'-ec
  ... | refl , refl = refl , refl
  eval-unicity Γ⊢E (TACase x ta-e x₁ x₂) (EMatch x₃ x₄ eval eval₁) (EMatchUnfinished eval' nc)
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = abort (nc refl)
  eval-unicity Γ⊢E (TACase x ta-e x₁ x₂) (EMatchUnfinished eval nc) (EMatch x₄ x₅ eval' eval'')
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = abort (nc refl)
  eval-unicity Γ⊢E (TACase x ta-e x₁ x₂) (EMatchUnfinished eval x₃) (EMatchUnfinished eval' x₄)
    with eval-unicity Γ⊢E ta-e eval eval'
  ... | refl , refl = refl , refl
  eval-unicity Γ⊢E (TAHole x) EHole EHole = refl , refl
  eval-unicity Γ⊢E (TAAsrt x ta-e1 ta-e2) (EAsrt eval1 eval2 xc) (EAsrt eval1' eval2' xc')
    with eval-unicity Γ⊢E ta-e1 eval1 eval1' | eval-unicity Γ⊢E ta-e2 eval2 eval2'
  ... | refl , refl | refl , refl
    rewrite xc-unicity (preservation Γ⊢E ta-e1 eval1) (preservation Γ⊢E ta-e2 eval2) xc xc'
      = refl , refl

  xc-unicity ta1 ta2 RCRefl RCRefl = refl
  xc-unicity ta1 ta2 RCRefl (RCPair x rc2 rc3) = abort (x refl)
  xc-unicity ta1 ta2 RCRefl (RCCtor x rc2) = abort (x refl)
  xc-unicity ta1 ta2 RCRefl (RCVal1 x x₁ x₂ x₃) = abort (x refl)
  xc-unicity ta1 ta2 RCRefl (RCVal2 x x₁ x₂ x₃) = abort (x refl)
  xc-unicity ta1 ta2 (RCPair x rc1 rc2) RCRefl = abort (x refl)
  xc-unicity (TAPair ta1 ta2) (TAPair ta3 ta4) (RCPair x rc1 rc2) (RCPair x₁ rc3 rc4)
    rewrite xc-unicity ta1 ta3 rc1 rc3 | xc-unicity ta2 ta4 rc2 rc4
      = refl
  xc-unicity ta1 ta2 (RCPair x rc1 rc2) (RCVal1 x₁ (Inl x₂) x₃ x₄) = abort (x₂ refl)
  xc-unicity ta1 ta2 (RCPair x rc1 rc2) (RCVal1 x₁ (Inr x₂) x₃ x₄) = abort (x₂ refl)
  xc-unicity ta1 ta2 (RCPair x rc1 rc2) (RCVal2 x₁ (Inl x₂) x₃ x₄) = abort (x₂ refl)
  xc-unicity ta1 ta2 (RCPair x rc1 rc2) (RCVal2 x₁ (Inr x₂) x₃ x₄) = abort (x₂ refl)
  xc-unicity ta1 ta2 (RCCtor x rc1) RCRefl = abort (x refl)
  xc-unicity (TACtor d∈σ' c∈cctx ta1) (TACtor d∈'σ' c∈'cctx ta2) (RCCtor x rc1) (RCCtor x₁ rc2)
    rewrite ctxunicity d∈σ' d∈'σ' | ctxunicity c∈cctx c∈'cctx
      = xc-unicity ta1 ta2 rc1 rc2
  xc-unicity ta1 ta2 (RCCtor x rc1) (RCVal1 x₁ x₂ (Inl x₃) x₄) = abort (x₃ refl)
  xc-unicity ta1 ta2 (RCCtor x rc1) (RCVal1 x₁ x₂ (Inr x₃) x₄) = abort (x₃ refl)
  xc-unicity ta1 ta2 (RCCtor x rc1) (RCVal2 x₁ x₂ (Inl x₃) x₄) = abort (x₃ refl)
  xc-unicity ta1 ta2 (RCCtor x rc1) (RCVal2 x₁ x₂ (Inr x₃) x₄) = abort (x₃ refl)
  xc-unicity ta1 ta2 (RCVal1 x x₁ x₂ x₃) RCRefl = abort (x refl)
  xc-unicity ta1 ta2 (RCVal1 x (Inl x₁) x₂ x₃) (RCPair x₄ rc2 rc3) = abort (x₁ refl)
  xc-unicity ta1 ta2 (RCVal1 x (Inr x₁) x₂ x₃) (RCPair x₄ rc2 rc3) = abort (x₁ refl)
  xc-unicity ta1 ta2 (RCVal1 x _ (Inl x₁) x₃) (RCCtor x₄ rc2) = abort (x₁ refl)
  xc-unicity ta1 ta2 (RCVal1 x _ (Inr x₁) x₃) (RCCtor x₄ rc2) = abort (x₁ refl)
  xc-unicity ta1 ta2 (RCVal1 x x₁ x₂ x₃) (RCVal1 x₄ x₅ x₆ x₇)
    rewrite Coerce-unicity x₃ x₇
      = refl
  xc-unicity TAUnit TAUnit (RCVal1 x x₁ x₂ x₃) (RCVal2 x₄ x₅ x₆ x₇) = abort (x₄ refl)
  xc-unicity (TAPair ta1 ta2) (TAPair ta3 ta4) (RCVal1 x (Inl x₂) _ x₃) (RCVal2 x₄ x₅ x₆ x₇) = abort (x₂ refl)
  xc-unicity (TAPair ta1 ta2) (TAPair ta3 ta4) (RCVal1 x (Inr x₂) _ x₃) (RCVal2 x₄ x₅ x₆ x₇) = abort (x₂ refl)
  xc-unicity (TACtor x₈ x₉ ta1) (TACtor x₁₀ x₁₁ ta2) (RCVal1 x x₁ (Inl h) x₃) (RCVal2 x₄ x₅ x₆ x₇) = abort (h refl)
  xc-unicity (TACtor x₈ x₉ ta1) (TACtor x₁₀ x₁₁ ta2) (RCVal1 x x₁ (Inr h) x₃) (RCVal2 x₄ x₅ x₆ x₇) = abort (h refl)
  xc-unicity ta1 ta2 (RCVal2 x x₁ x₂ x₃) RCRefl = abort (x refl)
  xc-unicity ta1 ta2 (RCVal2 x (Inl x₁) x₂ x₃) (RCPair x₄ rc2 rc3) = abort (x₁ refl)
  xc-unicity ta1 ta2 (RCVal2 x (Inr x₁) x₂ x₃) (RCPair x₄ rc2 rc3) = abort (x₁ refl)
  xc-unicity ta1 ta2 (RCVal2 x x₁ (Inl x₂) x₃) (RCCtor x₄ rc2) = abort (x₂ refl)
  xc-unicity ta1 ta2 (RCVal2 x x₁ (Inr x₂) x₃) (RCCtor x₄ rc2) = abort (x₂ refl)
  xc-unicity TAUnit TAUnit (RCVal2 x x₁ x₂ x₃) (RCVal1 x₄ x₅ x₆ x₇) = abort (x refl)
  xc-unicity (TAPair ta1 ta2) (TAPair ta3 ta4) (RCVal2 x (Inl h) x₂ x₃) (RCVal1 x₄ x₅ x₆ x₇) = abort (h refl)
  xc-unicity (TAPair ta1 ta2) (TAPair ta3 ta4) (RCVal2 x (Inr h) x₂ x₃) (RCVal1 x₄ x₅ x₆ x₇) = abort (h refl)
  xc-unicity (TACtor x₈ x₉ ta1) (TACtor x₁₀ x₁₁ ta2) (RCVal2 x x₁ (Inl h) x₃) (RCVal1 x₄ x₅ x₆ x₇) = abort (h refl)
  xc-unicity (TACtor x₈ x₉ ta1) (TACtor x₁₀ x₁₁ ta2) (RCVal2 x x₁ (Inr h) x₃) (RCVal1 x₄ x₅ x₆ x₇) = abort (h refl)
  xc-unicity ta1 ta2 (RCVal2 x x₁ x₂ x₃) (RCVal2 x₄ x₅ x₆ x₇)
    rewrite Coerce-unicity x₃ x₇
      = refl

  -- useful in practice, since threading type-checks around everywhere can be a pain
  -- note that this does not prove unicity of constraints, which isn't true for poorly-typed terms
  untyped-eval-unicity : ∀{⛽ E e r r' K K'} →
                           E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ K →
                           E ⊢ e ⌊ ⛽ ⌋⇒ r' ⊣ K' →
                           r == r'
  untyped-eval-unicity EFix EFix = refl
  untyped-eval-unicity (EVar h) (EVar h') = ctxunicity h h'
  untyped-eval-unicity (EAppFix f1 form eval-f eval-arg eval) (EAppFix f2 form' eval-f' eval-arg' eval')
    rewrite form | form'
    with untyped-eval-unicity eval-f eval-f' | untyped-eval-unicity eval-arg eval-arg'
  ... | refl | refl
    rewrite Fuel-depletion-unicity f1 f2 | untyped-eval-unicity eval eval'
      = refl
  untyped-eval-unicity EUnit EUnit = refl
  untyped-eval-unicity (EAppFix x₁ form eval eval₁ eval₂) (EAppUnfinished eval' nf eval'')
    rewrite untyped-eval-unicity eval eval' | form
      = abort (nf refl)
  untyped-eval-unicity (EAppUnfinished eval nf eval₁) (EAppFix x₂ form eval' eval'' eval''')
    rewrite untyped-eval-unicity eval eval' | form
      = abort (nf refl)
  untyped-eval-unicity (EAppUnfinished eval-f x₁ eval-arg) (EAppUnfinished eval-f' x₂ eval-arg')
    rewrite untyped-eval-unicity eval-f eval-f' | untyped-eval-unicity eval-arg eval-arg'
      = refl
  untyped-eval-unicity (EPair eval1 eval2) (EPair eval1' eval2')
    rewrite untyped-eval-unicity eval1 eval1' | untyped-eval-unicity eval2 eval2'
      = refl
  untyped-eval-unicity (EFst eval) (EFst eval')
    with untyped-eval-unicity eval eval'
  ... | refl = refl
  untyped-eval-unicity (EFst eval) (EFstUnfinished eval' np)
    with untyped-eval-unicity eval eval'
  ... | refl = abort (np refl)
  untyped-eval-unicity (EFstUnfinished eval np) (EFst eval')
    with untyped-eval-unicity eval eval'
  ... | refl = abort (np refl)
  untyped-eval-unicity (EFstUnfinished eval x) (EFstUnfinished eval' x₁)
    with untyped-eval-unicity eval eval'
  ... | refl = refl
  untyped-eval-unicity (ESnd eval) (ESnd eval')
    with untyped-eval-unicity eval eval'
  ... | refl = refl
  untyped-eval-unicity (ESnd eval) (ESndUnfinished eval' np)
    with untyped-eval-unicity eval eval'
  ... | refl = abort (np refl)
  untyped-eval-unicity (ESndUnfinished eval np) (ESnd eval')
    with untyped-eval-unicity eval eval'
  ... | refl = abort (np refl)
  untyped-eval-unicity (ESndUnfinished eval x) (ESndUnfinished eval' x₁)
    with untyped-eval-unicity eval eval'
  ... | refl = refl
  untyped-eval-unicity (ECtor eval) (ECtor eval')
    with untyped-eval-unicity eval eval'
  ... | refl = refl
  untyped-eval-unicity (EMatch f1 form eval-e eval-ec) (EMatch f2 form' eval'-e eval'-ec)
    with untyped-eval-unicity eval-e eval'-e
  ... | refl
    with ctxunicity form form'
  ... | refl
    rewrite Fuel-depletion-unicity f1 f2
    with untyped-eval-unicity eval-ec eval'-ec
  ... | refl = refl
  untyped-eval-unicity (EMatch x₃ x₄ eval eval₁) (EMatchUnfinished eval' nc)
    with untyped-eval-unicity eval eval'
  ... | refl = abort (nc refl)
  untyped-eval-unicity (EMatchUnfinished eval nc) (EMatch x₄ x₅ eval' eval'')
    with untyped-eval-unicity eval eval'
  ... | refl = abort (nc refl)
  untyped-eval-unicity (EMatchUnfinished eval x₃) (EMatchUnfinished eval' x₄)
    with untyped-eval-unicity eval eval'
  ... | refl = refl
  untyped-eval-unicity EHole EHole = refl
  untyped-eval-unicity (EAsrt eval1 eval2 xc) (EAsrt eval1' eval2' xc')
    with untyped-eval-unicity eval1 eval1' | untyped-eval-unicity eval2 eval2'
  ... | refl | refl = refl

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Powerset

open import Cubical.Data.Sigma

open import Cubical.Reflection.StrictEquiv

open import Cubical.Structures.Axioms
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommRing.Base
open import Cubical.Algebra.CommRing.Properties
open import Cubical.Algebra.CommRing.Localisation.Base
open import Cubical.Algebra.CommRing.Localisation.UniversalProperty
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Algebra
open import Cubical.Algebra.CommAlgebra.Base
open import Cubical.Algebra.CommAlgebra.Properties

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

private
  variable
    ℓ ℓ′ : Level

module AlgLoc (R' : CommRing ℓ)
              (S' : ℙ (fst R')) (SMultClosedSubset : isMultClosedSubset R' S') where
 open isMultClosedSubset
 private R = fst R'
 open CommAlgebraStr
 open IsAlgebraHom
 open CommRingStr (snd R') renaming (_+_ to _+r_ ; _·_ to _·r_ ; ·Rid to ·rRid)
 open RingTheory (CommRing→Ring R')
 open CommRingTheory R'
 open Loc R' S' SMultClosedSubset
 open S⁻¹RUniversalProp R' S' SMultClosedSubset
 open CommAlgChar R'

 S⁻¹RAsCommAlg : CommAlgebra R' ℓ
 S⁻¹RAsCommAlg = toCommAlg (S⁻¹RAsCommRing , /1AsCommRingHom)

 hasLocAlgUniversalProp : (A : CommAlgebra R' ℓ)
                        → (∀ s → s ∈ S' → _⋆_ (snd A) s (1a (snd A)) ∈ (CommAlgebra→CommRing A) ˣ)
                        → Type (ℓ-suc ℓ)
 hasLocAlgUniversalProp A _ = (B : CommAlgebra R' ℓ)
                      → (∀ s → s ∈ S' →  _⋆_ (snd B) s (1a (snd B)) ∈ (CommAlgebra→CommRing B) ˣ)
                      → isContr (CommAlgebraHom A B)

 S⋆1⊆S⁻¹Rˣ : ∀ s → s ∈ S' → _⋆_ (snd S⁻¹RAsCommAlg) s (1a (snd S⁻¹RAsCommAlg)) ∈ S⁻¹Rˣ
 S⋆1⊆S⁻¹Rˣ s s∈S' = subst-∈ S⁻¹Rˣ
                    (cong [_] (≡-× (sym (·rRid s)) (Σ≡Prop (λ x → S' x .snd) (sym (·rRid _)))))
                    (S/1⊆S⁻¹Rˣ s s∈S')

 S⁻¹RHasAlgUniversalProp : hasLocAlgUniversalProp S⁻¹RAsCommAlg S⋆1⊆S⁻¹Rˣ
 S⁻¹RHasAlgUniversalProp B' S⋆1⊆Bˣ = χᴬ , χᴬuniqueness
  where
  B = fromCommAlg B' .fst
  φ = fromCommAlg B' .snd
  open CommRingStr (snd B) renaming (_·_ to _·b_ ; 1r to 1b ; ·Lid to ·bLid)

  χ : CommRingHom S⁻¹RAsCommRing B
  χ = S⁻¹RHasUniversalProp B φ S⋆1⊆Bˣ .fst .fst

  χcomp : ∀ r → fst χ (r /1) ≡ fst φ r
  χcomp = funExt⁻ (S⁻¹RHasUniversalProp B φ S⋆1⊆Bˣ .fst .snd)

  χᴬ : CommAlgebraHom S⁻¹RAsCommAlg B'
  fst χᴬ = fst χ
  pres0 (snd χᴬ) = IsRingHom.pres0 (snd χ)
  pres1 (snd χᴬ) = IsRingHom.pres1 (snd χ)
  pres+ (snd χᴬ) = IsRingHom.pres+ (snd χ)
  pres· (snd χᴬ) = IsRingHom.pres· (snd χ)
  pres- (snd χᴬ) = IsRingHom.pres- (snd χ)
  pres⋆ (snd χᴬ) r x = path
   where
   path : fst χ ((r /1) ·ₗ x) ≡ _⋆_  (snd B') r (fst χ x)
   path = fst χ ((r /1) ·ₗ x)             ≡⟨ IsRingHom.pres· (snd χ) _ _ ⟩
          fst χ (r /1) ·b fst χ x         ≡⟨ cong (_·b fst χ x) (χcomp r) ⟩
          fst φ r ·b fst χ x              ≡⟨ refl ⟩
          _⋆_  (snd B') r 1b ·b fst χ x   ≡⟨ ⋆-lassoc (snd B') _ _ _ ⟩
          _⋆_  (snd B') r (1b ·b fst χ x) ≡⟨ cong (_⋆_ (snd B') r) (·bLid _) ⟩
          _⋆_  (snd B') r (fst χ x)       ∎

  χᴬuniqueness : (ψ : CommAlgebraHom S⁻¹RAsCommAlg B') → χᴬ ≡ ψ
  χᴬuniqueness ψ = Σ≡Prop (λ _ → isPropIsAlgebraHom _ _ _ _)
                          (cong (fst ∘ fst) (χuniqueness (ψ' , funExt ψ'r/1≡φr)))
   where
   χuniqueness = S⁻¹RHasUniversalProp B φ S⋆1⊆Bˣ .snd

   ψ' : CommRingHom S⁻¹RAsCommRing B
   fst ψ' = fst ψ
   IsRingHom.pres0 (snd ψ') = pres0 (snd ψ)
   IsRingHom.pres1 (snd ψ') = pres1 (snd ψ)
   IsRingHom.pres+ (snd ψ') = pres+ (snd ψ)
   IsRingHom.pres· (snd ψ') = pres· (snd ψ)
   IsRingHom.pres- (snd ψ') = pres- (snd ψ)

   ψ'r/1≡φr : ∀ r → fst ψ (r /1) ≡ fst φ r
   ψ'r/1≡φr r =
    fst ψ (r /1) ≡⟨ cong (fst ψ) (sym (·ₗ-rid _)) ⟩
    fst ψ (_⋆_ (snd S⁻¹RAsCommAlg) r (1a (snd S⁻¹RAsCommAlg))) ≡⟨ pres⋆ (snd ψ) _ _ ⟩
    _⋆_  (snd B') r (fst ψ (1a (snd S⁻¹RAsCommAlg))) ≡⟨ cong (_⋆_ (snd B') r) (pres1 (snd ψ)) ⟩
    _⋆_  (snd B') r 1b ∎

 -- an immediate corollary:
 isContrHomS⁻¹RS⁻¹R : isContr (CommAlgebraHom S⁻¹RAsCommAlg S⁻¹RAsCommAlg)
 isContrHomS⁻¹RS⁻¹R = S⁻¹RHasAlgUniversalProp S⁻¹RAsCommAlg S⋆1⊆S⁻¹Rˣ

module AlgLocTwoSubsets (R' : CommRing ℓ)
                        (S₁ : ℙ (fst R')) (S₁MultClosedSubset : isMultClosedSubset R' S₁)
                        (S₂ : ℙ (fst R')) (S₂MultClosedSubset : isMultClosedSubset R' S₂) where
 open isMultClosedSubset
 open CommRingStr (snd R') hiding (is-set)
 open RingTheory (CommRing→Ring R')
 open Loc R' S₁ S₁MultClosedSubset renaming (S⁻¹R to S₁⁻¹R ;
                                             S⁻¹RAsCommRing to S₁⁻¹RAsCommRing)
 open Loc R' S₂ S₂MultClosedSubset renaming (S⁻¹R to S₂⁻¹R ;
                                             S⁻¹RAsCommRing to S₂⁻¹RAsCommRing)
 open AlgLoc R' S₁ S₁MultClosedSubset renaming ( S⁻¹RAsCommAlg to S₁⁻¹RAsCommAlg
                                               ; S⋆1⊆S⁻¹Rˣ to S₁⋆1⊆S₁⁻¹Rˣ
                                               ; S⁻¹RHasAlgUniversalProp to S₁⁻¹RHasAlgUniversalProp
                                               ; isContrHomS⁻¹RS⁻¹R to isContrHomS₁⁻¹RS₁⁻¹R)
 open AlgLoc R' S₂ S₂MultClosedSubset renaming ( S⁻¹RAsCommAlg to S₂⁻¹RAsCommAlg
                                               ; S⋆1⊆S⁻¹Rˣ to S₂⋆1⊆S₂⁻¹Rˣ
                                               ; S⁻¹RHasAlgUniversalProp to S₂⁻¹RHasAlgUniversalProp
                                               ; isContrHomS⁻¹RS⁻¹R to isContrHomS₂⁻¹RS₂⁻¹R)

 open IsAlgebraHom
 open CommAlgebraStr ⦃...⦄

 private
  R = fst R'
  S₁⁻¹Rˣ = S₁⁻¹RAsCommRing ˣ
  S₂⁻¹Rˣ = S₂⁻¹RAsCommRing ˣ
  instance
   _ = snd S₁⁻¹RAsCommAlg
   _ = snd S₂⁻¹RAsCommAlg

 isContrS₁⁻¹R≡S₂⁻¹R : (∀ s₁ → s₁ ∈ S₁ → s₁ ⋆ 1a ∈ S₂⁻¹Rˣ)
                    → (∀ s₂ → s₂ ∈ S₂ → s₂ ⋆ 1a ∈ S₁⁻¹Rˣ)
                    → isContr (S₁⁻¹RAsCommAlg ≡ S₂⁻¹RAsCommAlg)
 isContrS₁⁻¹R≡S₂⁻¹R S₁⊆S₂⁻¹Rˣ S₂⊆S₁⁻¹Rˣ = isOfHLevelRetractFromIso 0
                                            (equivToIso (invEquiv (CommAlgebraPath _ _ _)))
                                              isContrS₁⁻¹R≅S₂⁻¹R
  where
  χ₁ : CommAlgebraHom S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg
  χ₁ = S₁⁻¹RHasAlgUniversalProp S₂⁻¹RAsCommAlg S₁⊆S₂⁻¹Rˣ .fst

  χ₂ : CommAlgebraHom S₂⁻¹RAsCommAlg S₁⁻¹RAsCommAlg
  χ₂ = S₂⁻¹RHasAlgUniversalProp S₁⁻¹RAsCommAlg S₂⊆S₁⁻¹Rˣ .fst

  χ₁∘χ₂≡id : χ₁ ∘a χ₂ ≡ idAlgHom
  χ₁∘χ₂≡id = isContr→isProp isContrHomS₂⁻¹RS₂⁻¹R _ _

  χ₂∘χ₁≡id : χ₂ ∘a χ₁ ≡ idAlgHom
  χ₂∘χ₁≡id = isContr→isProp isContrHomS₁⁻¹RS₁⁻¹R _ _

  IsoS₁⁻¹RS₂⁻¹R : Iso S₁⁻¹R S₂⁻¹R
  Iso.fun IsoS₁⁻¹RS₂⁻¹R = fst χ₁
  Iso.inv IsoS₁⁻¹RS₂⁻¹R = fst χ₂
  Iso.rightInv IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong fst χ₁∘χ₂≡id)
  Iso.leftInv IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong fst χ₂∘χ₁≡id)

  isContrS₁⁻¹R≅S₂⁻¹R : isContr (CommAlgebraEquiv S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg)
  isContrS₁⁻¹R≅S₂⁻¹R = center , uniqueness
   where
   center : CommAlgebraEquiv S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg
   fst center = isoToEquiv IsoS₁⁻¹RS₂⁻¹R
   pres0 (snd center) = pres0 (snd χ₁)
   pres1 (snd center) = pres1 (snd χ₁)
   pres+ (snd center) = pres+ (snd χ₁)
   pres· (snd center) = pres· (snd χ₁)
   pres- (snd center) = pres- (snd χ₁)
   pres⋆ (snd center) = pres⋆ (snd χ₁)

   uniqueness : (φ : CommAlgebraEquiv S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg) → center ≡ φ
   uniqueness φ = Σ≡Prop (λ _ → isPropIsAlgebraHom _ _ _ _)
                         (equivEq (cong fst
                           (S₁⁻¹RHasAlgUniversalProp S₂⁻¹RAsCommAlg S₁⊆S₂⁻¹Rˣ .snd
                             (AlgebraEquiv→AlgebraHom φ))))

 isPropS₁⁻¹R≡S₂⁻¹R  : isProp (S₁⁻¹RAsCommAlg ≡ S₂⁻¹RAsCommAlg)
 isPropS₁⁻¹R≡S₂⁻¹R S₁⁻¹R≡S₂⁻¹R  =
   isContr→isProp (isContrS₁⁻¹R≡S₂⁻¹R  S₁⊆S₂⁻¹Rˣ S₂⊆S₁⁻¹Rˣ) S₁⁻¹R≡S₂⁻¹R
    where
    S₁⊆S₂⁻¹Rˣ : ∀ s₁ → s₁ ∈ S₁ → s₁ ⋆ 1a ∈ S₂⁻¹Rˣ
    S₁⊆S₂⁻¹Rˣ s₁ s₁∈S₁ =
      transport (λ i → _⋆_ ⦃ S₁⁻¹R≡S₂⁻¹R i .snd ⦄ s₁ (1a ⦃ S₁⁻¹R≡S₂⁻¹R i .snd ⦄)
                     ∈ (CommAlgebra→CommRing (S₁⁻¹R≡S₂⁻¹R i)) ˣ) (S₁⋆1⊆S₁⁻¹Rˣ s₁ s₁∈S₁)

    S₂⊆S₁⁻¹Rˣ : ∀ s₂ → s₂ ∈ S₂ → s₂ ⋆ 1a ∈ S₁⁻¹Rˣ
    S₂⊆S₁⁻¹Rˣ s₂ s₂∈S₂ =
      transport (λ i → _⋆_ ⦃ (sym S₁⁻¹R≡S₂⁻¹R) i .snd ⦄ s₂ (1a ⦃ (sym S₁⁻¹R≡S₂⁻¹R) i .snd ⦄)
                     ∈ (CommAlgebra→CommRing ((sym S₁⁻¹R≡S₂⁻¹R) i)) ˣ) (S₂⋆1⊆S₂⁻¹Rˣ s₂ s₂∈S₂)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The identity function
------------------------------------------------------------------------

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

module Function.Construct.Composition where

open import Data.Product using (_,_)
open import Function
open import Level
open import Relation.Binary

private
  variable
    a b c ℓ₁ ℓ₂ ℓ₃ : Level
    A : Set a
    B : Set b
    C : Set c

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

module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
         {f : A → B} {g : B → C}
         where

  congruent : Congruent ≈₁ ≈₂ f → Congruent ≈₂ ≈₃ g →
              Congruent ≈₁ ≈₃ (g ∘ f)
  congruent f-cong g-cong = g-cong ∘ f-cong

  injective : Injective ≈₁ ≈₂ f → Injective ≈₂ ≈₃ g →
              Injective ≈₁ ≈₃ (g ∘ f)
  injective f-inj g-inj = f-inj ∘ g-inj

  surjective : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
               Surjective ≈₁ ≈₂ f → Surjective ≈₂ ≈₃ g →
               Surjective ≈₁ ≈₃ (g ∘ f)
  surjective trans g-cong f-sur g-sur x with g-sur x
  ... | y , fy≈x  with f-sur y
  ...   | z , fz≈y = z , trans (g-cong fz≈y) fy≈x

  bijective : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
              Bijective ≈₁ ≈₂ f → Bijective ≈₂ ≈₃ g →
              Bijective ≈₁ ≈₃ (g ∘ f)
  bijective trans g-cong (f-inj , f-sur) (g-inj , g-sur) =
    injective f-inj g-inj , surjective trans g-cong f-sur g-sur

module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) (≈₃ : Rel C ℓ₃)
         (f : A → B) {f⁻¹ : B → A} {g : B → C} (g⁻¹ : C → B)
         where

  inverseˡ : Transitive ≈₃ → Congruent ≈₂ ≈₃ g →
             Inverseˡ ≈₁ ≈₂ f f⁻¹ → Inverseˡ ≈₂ ≈₃ g g⁻¹ →
             Inverseˡ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
  inverseˡ trn g-cong f-inv g-inv x = trn (g-cong (f-inv _)) (g-inv x)

  inverseʳ : Transitive ≈₁ → Congruent ≈₂ ≈₁ f⁻¹ →
             Inverseʳ ≈₁ ≈₂ f f⁻¹ → Inverseʳ ≈₂ ≈₃ g g⁻¹ →
             Inverseʳ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
  inverseʳ trn f⁻¹-cong f-inv g-inv x = trn (f⁻¹-cong (g-inv _)) (f-inv x)

  inverseᵇ : Transitive ≈₁ → Transitive ≈₃ →
             Congruent ≈₂ ≈₃ g → Congruent ≈₂ ≈₁ f⁻¹ →
             Inverseᵇ ≈₁ ≈₂ f f⁻¹ → Inverseᵇ ≈₂ ≈₃ g g⁻¹ →
             Inverseᵇ ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
  inverseᵇ trn₁ trn₃ g-cong f⁻¹-cong (f-invˡ , f-invʳ) (g-invˡ , g-invʳ) =
    inverseˡ trn₃ g-cong f-invˡ g-invˡ , inverseʳ trn₁ f⁻¹-cong f-invʳ g-invʳ

------------------------------------------------------------------------
-- Structures

module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
         {f : A → B} {g : B → C}
         where

  isCongruent : IsCongruent ≈₁ ≈₂ f → IsCongruent ≈₂ ≈₃ g →
                IsCongruent ≈₁ ≈₃ (g ∘ f)
  isCongruent f-cong g-cong = record
    { cong           = G.cong ∘ F.cong
    ; isEquivalence₁ = F.isEquivalence₁
    ; isEquivalence₂ = G.isEquivalence₂
    } where module F = IsCongruent f-cong; module G = IsCongruent g-cong

  isInjection : IsInjection ≈₁ ≈₂ f → IsInjection ≈₂ ≈₃ g →
                IsInjection ≈₁ ≈₃ (g ∘ f)
  isInjection f-inj g-inj = record
    { isCongruent = isCongruent F.isCongruent G.isCongruent
    ; injective   = injective ≈₁ ≈₂ ≈₃ F.injective G.injective
    } where module F = IsInjection f-inj; module G = IsInjection g-inj

  isSurjection : IsSurjection ≈₁ ≈₂ f → IsSurjection ≈₂ ≈₃ g →
                 IsSurjection ≈₁ ≈₃ (g ∘ f)
  isSurjection f-surj g-surj = record
    { isCongruent = isCongruent F.isCongruent G.isCongruent
    ; surjective   = surjective ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong F.surjective G.surjective
    } where module F = IsSurjection f-surj; module G = IsSurjection g-surj

  isBijection : IsBijection ≈₁ ≈₂ f → IsBijection ≈₂ ≈₃ g →
                IsBijection ≈₁ ≈₃ (g ∘ f)
  isBijection f-bij g-bij = record
    { isInjection = isInjection F.isInjection G.isInjection
    ; surjective  = surjective ≈₁ ≈₂ ≈₃ G.Eq₂.trans G.cong F.surjective G.surjective
    } where module F = IsBijection f-bij; module G = IsBijection g-bij

module _ {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂} {≈₃ : Rel C ℓ₃}
         {f : A → B} {g : B → C} {f⁻¹ : B → A} {g⁻¹ : C → B}
         where

  isLeftInverse : IsLeftInverse ≈₁ ≈₂ f f⁻¹ → IsLeftInverse ≈₂ ≈₃ g g⁻¹ →
                  IsLeftInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
  isLeftInverse f-invˡ g-invˡ = record
    { isCongruent = isCongruent F.isCongruent G.isCongruent
    ; cong₂       = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂
    ; inverseˡ    = inverseˡ ≈₁ ≈₂ ≈₃ f _ G.Eq₂.trans G.cong₁ F.inverseˡ G.inverseˡ
    } where module F = IsLeftInverse f-invˡ; module G = IsLeftInverse g-invˡ

  isRightInverse : IsRightInverse ≈₁ ≈₂ f f⁻¹ → IsRightInverse ≈₂ ≈₃ g g⁻¹ →
                   IsRightInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
  isRightInverse f-invʳ g-invʳ = record
    { isCongruent = isCongruent F.isCongruent G.isCongruent
    ; cong₂       = congruent ≈₃ ≈₂ ≈₁ G.cong₂ F.cong₂
    ; inverseʳ    = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ F.inverseʳ G.inverseʳ
    } where module F = IsRightInverse f-invʳ; module G = IsRightInverse g-invʳ

  isInverse : IsInverse ≈₁ ≈₂ f f⁻¹ → IsInverse ≈₂ ≈₃ g g⁻¹ →
              IsInverse ≈₁ ≈₃ (g ∘ f) (f⁻¹ ∘ g⁻¹)
  isInverse f-inv g-inv = record
    { isLeftInverse = isLeftInverse F.isLeftInverse G.isLeftInverse
    ; inverseʳ      = inverseʳ ≈₁ ≈₂ ≈₃ _ g⁻¹ F.Eq₁.trans F.cong₂ F.inverseʳ G.inverseʳ
    } where module F = IsInverse f-inv; module G = IsInverse g-inv

------------------------------------------------------------------------
-- Setoid bundles

module _ {R : Setoid a ℓ₁} {S : Setoid b ℓ₂} {T : Setoid c ℓ₃} where

  open Setoid renaming (_≈_ to ≈)

  injection : Injection R S → Injection S T → Injection R T
  injection inj₁ inj₂ = record
    { f         = G.f ∘ F.f
    ; cong      = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
    ; injective = injective (≈ R) (≈ S) (≈ T) F.injective G.injective
    } where module F = Injection inj₁; module G = Injection inj₂

  surjection : Surjection R S → Surjection S T → Surjection R T
  surjection surj₁ surj₂ = record
    { f          = G.f ∘ F.f
    ; cong       = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
    ; surjective = surjective (≈ R) (≈ S) (≈ T) G.Eq₂.trans G.cong F.surjective G.surjective
    } where module F = Surjection surj₁; module G = Surjection surj₂

  bijection : Bijection R S → Bijection S T → Bijection R T
  bijection bij₁ bij₂ = record
    { f         = G.f ∘ F.f
    ; cong      = congruent (≈ R) (≈ S) (≈ T) F.cong G.cong
    ; bijective = bijective (≈ R) (≈ S) (≈ T) (trans T) G.cong F.bijective G.bijective
    } where module F = Bijection bij₁; module G = Bijection bij₂

  equivalence : Equivalence R S → Equivalence S T → Equivalence R T
  equivalence equiv₁ equiv₂ = record
    { f        = G.f ∘ F.f
    ; g        = F.g ∘ G.g
    ; cong₁    = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
    ; cong₂    = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
    } where module F = Equivalence equiv₁; module G = Equivalence equiv₂

  leftInverse : LeftInverse R S → LeftInverse S T → LeftInverse R T
  leftInverse invˡ₁ invˡ₂ = record
    { f        = G.f ∘ F.f
    ; g        = F.g ∘ G.g
    ; cong₁    = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
    ; cong₂    = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
    ; inverseˡ = inverseˡ (≈ R) (≈ S) (≈ T) F.f _ (trans T) G.cong₁ F.inverseˡ G.inverseˡ
    } where module F = LeftInverse invˡ₁; module G = LeftInverse invˡ₂

  rightInverse : RightInverse R S → RightInverse S T → RightInverse R T
  rightInverse invʳ₁ invʳ₂ = record
    { f        = G.f ∘ F.f
    ; g        = F.g ∘ G.g
    ; cong₁    = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
    ; cong₂    = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
    ; inverseʳ = inverseʳ (≈ R) (≈ S) (≈ T) _ G.g (trans R) F.cong₂ F.inverseʳ G.inverseʳ
    } where module F = RightInverse invʳ₁; module G = RightInverse invʳ₂

  inverse : Inverse R S → Inverse S T → Inverse R T
  inverse inv₁ inv₂ = record
    { f       = G.f ∘ F.f
    ; f⁻¹     = F.f⁻¹ ∘ G.f⁻¹
    ; cong₁   = congruent (≈ R) (≈ S) (≈ T) F.cong₁ G.cong₁
    ; cong₂   = congruent (≈ T) (≈ S) (≈ R) G.cong₂ F.cong₂
    ; inverse = inverseᵇ (≈ R) (≈ S) (≈ T) _ G.f⁻¹ (trans R) (trans T) G.cong₁ F.cong₂ F.inverse G.inverse
    } where module F = Inverse inv₁; module G = Inverse inv₂

------------------------------------------------------------------------
-- Propositional bundles

infix 8 _∘-↣_ _∘-↠_ _∘-⤖_ _∘-⇔_ _∘-↩_ _∘-↪_ _∘-↔_

_∘-↣_ : A ↣ B → B ↣ C → A ↣ C
_∘-↣_ = injection

_∘-↠_ : A ↠ B → B ↠ C → A ↠ C
_∘-↠_ = surjection

_∘-⤖_ : A ⤖ B → B ⤖ C → A ⤖ C
_∘-⤖_ = bijection

_∘-⇔_ : A ⇔ B → B ⇔ C → A ⇔ C
_∘-⇔_ = equivalence

_∘-↩_ : A ↩ B → B ↩ C → A ↩ C
_∘-↩_ = leftInverse

_∘-↪_ : A ↪ B → B ↪ C → A ↪ C
_∘-↪_ = rightInverse

_∘-↔_ : A ↔ B → B ↔ C → A ↔ C
_∘-↔_ = inverse


text:
{-# OPTIONS --cubical --no-import-sorts  #-}

module MorePropAlgebra.Bundles where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)-- ¬ᵗ_
open import Cubical.Foundations.Logic
open import MoreLogic.Definitions
open import Utils
open import MorePropAlgebra.Structures

-- taken from the cubical standard library and adapted to hProps:
-- Semigroup
-- Monoid
-- Group
-- AbGroup
-- Ring
-- CommRing

record Semigroup : Type (ℓ-suc ℓ) where
  constructor semigroup
  field
    Carrier      : Type ℓ
    _·_          : Carrier → Carrier → Carrier
    is-Semigroup : IsSemigroup _·_

  infixl 7 _·_

  open IsSemigroup is-Semigroup public

record Monoid : Type (ℓ-suc ℓ) where
  constructor monoid
  field
    Carrier   : Type ℓ
    ε         : Carrier
    _·_       : Carrier → Carrier → Carrier
    is-Monoid : IsMonoid ε _·_

  infixl 7 _·_

  open IsMonoid is-Monoid public

record Group : Type (ℓ-suc ℓ) where
  constructor group
  field
    Carrier  : Type ℓ
    0g       : Carrier
    _+_      : Carrier → Carrier → Carrier
    -_       : Carrier → Carrier
    is-Group : IsGroup 0g _+_ -_

  infix  8 -_
  infixr 7 _+_

  open IsGroup is-Group public

record AbGroup : Type (ℓ-suc ℓ) where
  constructor abgroup
  field
    Carrier    : Type ℓ
    0g         : Carrier
    _+_        : Carrier → Carrier → Carrier
    -_         : Carrier → Carrier
    is-AbGroup : IsAbGroup 0g _+_ -_

  infix  8 -_
  infixl 7 _+_

  open IsAbGroup is-AbGroup public

record Ring : Type (ℓ-suc ℓ) where
  constructor ring
  field
    Carrier : Type ℓ
    0r      : Carrier
    1r      : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    is-Ring : IsRing 0r 1r _+_ _·_ -_

  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_

  open IsRing is-Ring public

record CommRing : Type (ℓ-suc ℓ) where
  constructor commring
  field
    Carrier     : Type ℓ
    0r          : Carrier
    1r          : Carrier
    _+_         : Carrier → Carrier → Carrier
    _·_         : Carrier → Carrier → Carrier
    -_          : Carrier → Carrier
    is-CommRing : IsCommRing 0r 1r _+_ _·_ -_

  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_

  open IsCommRing is-CommRing public

record ClassicalField : Type (ℓ-suc ℓ) where
  field
    Carrier : Type ℓ
    0f      : Carrier
    1f      : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    _⁻¹     : (x : Carrier) → {{ ! ¬ᵗ(x ≡ 0f) }} → Carrier -- WARNING: we do not have `_⁻¹` as an assuption
    is-ClassicalField : [ isClassicalField 0f 1f _+_ _·_ -_ _⁻¹ ]

  infix  9 _⁻¹
  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_

  open IsClassicalField is-ClassicalField public

record ConstructiveField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor constructivefield
  field
    Carrier : Type ℓ
    0f      : Carrier
    1f      : Carrier
    _+_     : Carrier → Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    _#_     : hPropRel Carrier Carrier ℓ'
    is-ConstructiveField : [ isConstructiveField 0f 1f _+_ _·_ -_ _#_ ]

  infixl 7 _·_
  infix  6 -_
  infixl 5 _+_
  infixl 4 _#_

  open IsConstructiveField is-ConstructiveField public

record Lattice : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor lattice
  field
    Carrier : Type ℓ
    _≤_ : hPropRel Carrier Carrier ℓ'
    min max : Carrier → Carrier → Carrier
    is-Lattice : [ isLattice _≤_ min max ]

  infixl 4 _≤_

  open IsLattice is-Lattice public

record AlmostPartiallyOrderedField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor almostpartiallyorderedfield
  field
    Carrier : Type ℓ
    0f 1f   : Carrier
    _+_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    min max : Carrier → Carrier → Carrier
    _<_     : hPropRel Carrier Carrier ℓ'
  field
    is-AlmostPartiallyOrderedField : [ isAlmostPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max {- _⁻¹ -} ] -- defines `_≤_` and `_#_`

  infixl 7 _·_
  infix  6 -_
  infixl 5 _+_
  infixl 4 _<_

  open IsAlmostPartiallyOrderedField is-AlmostPartiallyOrderedField public

record PartiallyOrderedField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  constructor partiallyorderedfield
  field
    Carrier : Type ℓ
    0f 1f   : Carrier
    _+_     : Carrier → Carrier → Carrier
    -_      : Carrier → Carrier
    _·_     : Carrier → Carrier → Carrier
    min max : Carrier → Carrier → Carrier
    _<_     : hPropRel Carrier Carrier ℓ'

  field
    is-PartiallyOrderedField : [ isPartiallyOrderedField 0f 1f _+_ _·_ -_ _<_ min max ] -- defines `_≤_` and `_#_`

  infixl 7 _·_
  infix  6 -_
  infixl 5 _+_
  infixl 4 _<_

  open IsPartiallyOrderedField is-PartiallyOrderedField public

  -- abstract
  --   -- NOTE: there might be some reason not to "do" (or "open") all the theory of a record within that record
  --   +-preserves-< : ∀ a b x → a < b → a + x < b + x
  --   +-preserves-< a b x a<b = (
  --      a            <  b            ⇒⟨ transport (λ i → sym (fst (+-identity a)) i < sym (fst (+-identity b)) i) ⟩
  --      a +    0f    <  b +    0f    ⇒⟨ transport (λ i → a + sym (+-rinv x) i < b + sym (+-rinv x) i) ⟩
  --      a + (x  - x) <  b + (x  - x) ⇒⟨ transport (λ i → +-assoc a x (- x) i < +-assoc b x (- x) i) ⟩
  --     (a +  x) - x  < (b +  x) - x  ⇒⟨ +-<-extensional (- x) (a + x) (- x) (b + x) ⟩
  --     (a + x < b + x) ⊎ (- x < - x) ⇒⟨ (λ{ (inl a+x<b+x) → a+x<b+x -- somehow ⊥-elim needs a hint in the next line
  --                                        ; (inr  -x<-x ) → ⊥-elim {A = λ _ → (a + x < b + x)} (<-irrefl (- x) -x<-x) }) ⟩
  --      a + x < b + x ◼) a<b
  --
  --   ≤-isPreorder : IsPreorder _≤_
  --   ≤-isPreorder = ≤-isPreorder' {_<_ = _<_} {<-isStrictPartialOrder}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
-- Andreas, 2018-11-23, 2019-07-22, issue #3353
--
-- Preserved names of named arguments under case splitting.

-- {-# OPTIONS -v tc.lhs:40 #-}
-- {-# OPTIONS -v interaction.case:60 -v reify:30 #-}

open import Agda.Builtin.Nat

test : {m n : Nat} → Nat
test {m} {n = n} = {!n!}  -- C-c C-c

-- Splitting on n gives:
-- test {m} {zero} = {!!}
-- test {m} {suc n} = {!!}

-- Expected:
-- test {m} {n = zero} = {!!}
-- test {m} {n = suc n} = {!!}

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

foo : ∀{A n} → Vec A n → Vec A n
foo (_∷_ {n = n} x xs) = {!n!}  -- C-c C-c

-- Expected:
-- foo (_∷_ {n = suc n} x xs) = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- mathematical integers; see int.agda for imported machine integers from Haskell.
module integer where

open import bool
open import bool-thms2
open import eq
open import nat
open import nat-thms
open import product
open import product-thms
open import sum
open import unit

ℤ-pos-t : ℕ → Set
ℤ-pos-t 0 = ⊤
ℤ-pos-t (suc _) = 𝔹

{- In mkℤ n a, the argument a tells whether the integer is positive or negative, if n is nonzero.
   If n is zero, then a is just triv : ⊤, so there is a unique integer value for 0. -}
data ℤ : Set where
  mkℤ : (n : ℕ) → ℤ-pos-t n → ℤ

0ℤ : ℤ
0ℤ = mkℤ 0 triv

1ℤ : ℤ
1ℤ = mkℤ 1 tt

-1ℤ : ℤ
-1ℤ = mkℤ 1 ff

abs-val : ℤ → ℕ
abs-val (mkℤ n _) = n

is-evenℤ : ℤ → 𝔹
is-evenℤ (mkℤ n _) = is-even n

is-oddℤ : ℤ → 𝔹
is-oddℤ (mkℤ n _) = is-odd n

{- subtract the second natural number from the first, returning an integer.
   This is mostly a helper for _+ℤ_ -}
diffℤ : ℕ → ℕ → ℤ
diffℤ n m with ℕ-trichotomy n m
diffℤ n m | inj₁ p with <∸suc{m}{n} p               -- n < m
diffℤ n m | inj₁ p | x , _ = mkℤ (suc x) ff
diffℤ n m | inj₂ (inj₁ p) = mkℤ 0 triv              -- n = m
diffℤ n m | inj₂ (inj₂ p) with <∸suc{n}{m} p
diffℤ n m | inj₂ (inj₂ p) | x , _ = mkℤ (suc x) tt  -- m < n

_+ℤ_ : ℤ → ℤ → ℤ
(mkℤ 0 _) +ℤ x = x
x +ℤ (mkℤ 0 _) = x
(mkℤ (suc n) p1) +ℤ (mkℤ (suc m) p2) with p1 xor p2
(mkℤ (suc n) p1) +ℤ (mkℤ (suc m) p2) | ff = mkℤ (suc n + suc m) p1
(mkℤ (suc n) p1) +ℤ (mkℤ (suc m) p2) | tt = if p1 imp p2 then diffℤ m n else diffℤ n m

test-+ℤ1 : (mkℤ 2 ff) +ℤ (mkℤ 4 tt) ≡ (mkℤ 2 tt)
test-+ℤ1 = refl

test-+ℤ2 : (mkℤ 2 tt) +ℤ (mkℤ 4 ff) ≡ (mkℤ 2 ff)
test-+ℤ2 = refl

_≤ℤ_ : ℤ → ℤ → 𝔹
(mkℤ 0 triv) ≤ℤ (mkℤ 0 triv) = tt
(mkℤ 0 triv) ≤ℤ (mkℤ (suc _) pos) = pos
(mkℤ (suc _) pos) ≤ℤ (mkℤ 0 triv) = ~ pos
(mkℤ (suc x) pos1) ≤ℤ (mkℤ (suc y) pos2) with pos1 xor pos2
(mkℤ (suc x) pos1) ≤ℤ (mkℤ (suc y) pos2) | tt = pos1 imp pos2
(mkℤ (suc x) pos1) ≤ℤ (mkℤ (suc y) pos2) | ff = if pos1 then x ≤ y else y ≤ x

≤ℤ-antisymm : ∀(x y : ℤ) → x ≤ℤ y ≡ tt → y ≤ℤ x ≡ tt → x ≡ y
≤ℤ-antisymm (mkℤ zero triv) (mkℤ zero triv) p q = refl
≤ℤ-antisymm (mkℤ zero triv) (mkℤ (suc y) pos2) p q rewrite p with q
≤ℤ-antisymm (mkℤ zero triv) (mkℤ (suc y) pos2) p q | ()
≤ℤ-antisymm (mkℤ (suc x) pos1) (mkℤ zero triv) p q rewrite q with p
≤ℤ-antisymm (mkℤ (suc x) pos1) (mkℤ zero triv) p q | ()
≤ℤ-antisymm (mkℤ (suc x) pos1) (mkℤ (suc y) pos2) p q with keep (pos1 xor pos2)
≤ℤ-antisymm (mkℤ (suc x) pos1) (mkℤ (suc y) pos2) p q | tt , rp rewrite rp | xor-comm pos1 pos2 | rp with imp-antisymm{pos1} p q
≤ℤ-antisymm (mkℤ (suc x) pos1) (mkℤ (suc y) pos2) p q | tt , rp | pp rewrite pp | xor-anti-idem pos2 with rp
≤ℤ-antisymm (mkℤ (suc x) pos1) (mkℤ (suc y) pos2) p q | tt , rp | pp | ()
≤ℤ-antisymm (mkℤ (suc x) pos1) (mkℤ (suc y) pos2) p q | ff , rp
 rewrite rp | xor-comm pos1 pos2 | rp | xor-≡{pos2}rp with pos1
≤ℤ-antisymm (mkℤ (suc x) pos1) (mkℤ (suc y) pos2) p q | ff , rp | tt rewrite ≤-antisym{x} p q = refl
≤ℤ-antisymm (mkℤ (suc x) pos1) (mkℤ (suc y) pos2) p q | ff , rp | ff rewrite ≤-antisym{y} p q = refl

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --rewriting --prop --confluence-check #-}

open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Data.Vec.Base
open import Data.Bool
open import Data.Sum

variable ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

{-
 Axiomatisation of ExTT
-}

postulate raise : (A : Set ℓ) → A

-- we now state rewrite rules for raise

postulate raise-Pi : (A : Set ℓ) (B : A → Set ℓ₁) →
                     raise ((a : A) → B a) ≡ λ a → raise (B a)

{-# REWRITE raise-Pi #-}

postulate raise-Sigma : (A : Set ℓ) (B : A → Set ℓ₁) →
                     raise (Σ A B) ≡ (raise A , raise (B (raise A)))

{-# REWRITE raise-Sigma #-}

nat-rec : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) → (n : Nat) → P n
nat-rec P P0 PS zero = P0
nat-rec P P0 PS (suc n) = PS n (nat-rec P P0 PS n)

postulate raise-nat-rec : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                          nat-rec P P0 PS (raise Nat) ≡ raise (P (raise Nat))

{-# REWRITE raise-nat-rec #-}

postulate catch-nat : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                      (Praise : P (raise Nat)) → (n : Nat) → P n

postulate catch-nat-zero : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                           (Praise : P (raise Nat)) → catch-nat P P0 PS Praise 0 ≡ P0

postulate catch-nat-suc : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                          (Praise : P (raise Nat)) → (n : Nat) →
                          catch-nat P P0 PS Praise (suc n) ≡ PS n (catch-nat P P0 PS Praise n)

postulate catch-nat-raise : (P : Nat → Set ℓ) (P0 : P 0) (PS : (n : Nat) → P n → P (suc n)) →
                            (Praise : P (raise Nat)) → catch-nat P P0 PS Praise (raise Nat) ≡ Praise

{-# REWRITE catch-nat-zero #-}
{-# REWRITE catch-nat-suc #-}
{-# REWRITE catch-nat-raise #-}

record Unk ℓ : Set (lsuc ℓ) where
  constructor box
  field
    type : Set ℓ
    elem : type

postulate raise-Unk :  ∀ ℓ → raise (Unk ℓ) ≡ box (raise (Set ℓ)) (raise _)

{-# REWRITE raise-Unk #-}

max_stars_repo_name: kyoDralliam/exceptional-tt

max_issues_repo_name: kyoDralliam/exceptional-tt

max_forks_repo_name: kyoDralliam/exceptional-tt


text:
module m-types where

-- Basic definitions
import container.core

-- Construction of M-types as limits
import container.m.from-nat

-- M-types via Agda coinduction
import container.m.core

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module Data.Vec.Any.Membership.Propositional.Properties where

open import Algebra
open import Data.Vec as Vec
open import Data.Vec.Any
open import Data.Vec.Any.Membership.Propositional
open import Data.Vec.Any.Properties
import Data.Vec.Any.Membership.Properties as Membershipᵖ
open import Function
open import Function.Inverse as Inv using (_↔_)
import Function.Related as Related
open import Function.Related.TypeIsomorphisms
open import Relation.Binary.PropositionalEquality as P
import Relation.Binary.Sigma.Pointwise as Σ
open import Relation.Unary using (_⟨×⟩_)
open import Data.Product

private
  module ×⊎ {k ℓ} = CommutativeSemiring (×⊎-CommutativeSemiring k ℓ)

-- map

module _ {a b} {A : Set a} {B : Set b} {f : A → B} where
  ∈′-map⁺ : ∀ {n x}{xs : Vec A n} → x ∈′ xs → f x ∈′ Vec.map f xs
  ∈′-map⁺ = Membershipᵖ.∈′-map⁺ (P.setoid _) (P.setoid _) (P.cong f)

  ∈′-map⁻ : ∀ {n y}{xs : Vec A n} → y ∈′ Vec.map f xs → ∃ λ x → x ∈′ xs × y ≡ f x
  ∈′-map⁻ = Membershipᵖ.∈′-map⁻ (P.setoid _) (P.setoid _)

  map-∈′↔ : ∀ {n y}{xs : Vec A n} →
    (∃ λ x → x ∈′ xs × y ≡ f x) ↔ y ∈′ Vec.map f xs
  map-∈′↔ {n}{y}{xs} =
    (∃ λ x → x ∈′ xs × y ≡ f x) ↔⟨ Any↔ ⟩
    Any (λ x → y ≡ f x)   xs    ↔⟨ map↔ ⟩
    y ∈′ Vec.map f xs       ∎
    where open Related.EquationalReasoning

max_stars_repo_name: tizmd/agda-vector-any

max_issues_repo_name: tizmd/agda-vector-any

max_forks_repo_name: tizmd/agda-vector-any


text:
{-# OPTIONS --cubical #-}
module _ where

module _ where
  open import Agda.Primitive.Cubical public

  postulate
    Path' : ∀ {ℓ} {A :     Set ℓ} → A    → A    → Set ℓ
    PathP : ∀ {ℓ} (A : I → Set ℓ) → A i0 → A i1 → Set ℓ

  {-# BUILTIN PATH         Path'     #-}
  {-# BUILTIN PATHP        PathP     #-}

  infix 4 _≡_
  _≡_ : ∀ {ℓ} {A : Set ℓ} → A → A → Set ℓ
  _≡_ {A = A} = PathP (λ _ → A)

  Path = _≡_

  refl : ∀ {a} {A : Set a} {x : A} → x ≡ x
  refl {x = x} = \ _ → x

-- Here there's no solution for H, pattern unification will try
-- H := \ i -> b, but the equality constraints from
-- H : Path b a should rule out that assignment.
testPath : ∀ {A : Set} {b a : A} (let H : Path b a; H = _) → ∀ i → H i ≡ b
testPath i = refl

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
module Generic.Test.ReadData where

open import Generic.Main

data D {α β} (A : Set α) (B : ℕ -> Set β) : ∀ {n} -> B n -> List ℕ -> Set (α ⊔ β) where
  c₁ : ∀ {n} (y : B n) xs -> A -> D A B y xs
  c₂ : ∀ {y : B 0} -> (∀ {n} (y : B n) {{xs}} -> D A B y xs) -> .(List A) -> D A B y []

-- No longer works: Failed to solve the following constraints: Has bigger sort: Setω
-- D′ : TypeOf D
D′ : ∀ {α β} -> (A : Set α) -> (B : ℕ -> Set β) -> ∀ {n} -> B n -> List ℕ -> Set (α ⊔ β)
D′ = readData D

unquoteDecl foldD = deriveFoldTo foldD (quote D)

inj : ∀ {α β} {A : Set α} {B : ℕ -> Set β} {n xs} {y : B n} -> D A B y xs -> D′ A B y xs
inj = gcoerce foldD

outj : ∀ {α β} {A : Set α} {B : ℕ -> Set β} {n xs} {y : B n} -> D′ A B y xs -> D A B y xs
outj d = guncoerce d

pattern c₁′ {n} y xs x = #₀  (relv n , relv y , relv xs , relv x , lrefl)
pattern c₂′ {y} r ys   = !#₁ (relv y , r , irrv ys , lrefl)

inj′ : ∀ {α β} {A : Set α} {B : ℕ -> Set β} {n xs} {y : B n} -> D A B y xs -> D′ A B y xs
inj′ (c₁ y xs x) = c₁′ y xs x
inj′ (c₂ r ys)   = c₂′ (λ y -> inj′ (r y)) ys

outj′ : ∀ {α β} {A : Set α} {B : ℕ -> Set β} {n xs} {y : B n} -> D′ A B y xs -> D A B y xs
outj′ (c₁′ y xs x) = c₁ y xs x
outj′ (c₂′ r ys)   = c₂ (λ y -> outj′ (r y)) ys

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  A : Set
  a b : A

  f : (X : Set) → X → A
  g : (X : Set) → X

  rewf₁ : f (A → A) (λ _ → a) ≡ a
  rewf₂ : (X : Set) → f X (g X) ≡ b

  rewg : (x : A) → g (A → A) x ≡ a

test = f (A → A) (λ x → g (A → A) x)

{-# REWRITE rewf₁ rewg #-}

foo : test ≡ a
foo = refl

{-# REWRITE rewf₂ #-}

bar : test ≡ b
bar = refl

fails : a ≡ b
fails = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Data.Nat
open import Data.List as List hiding (null)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All
open import Data.List.Prefix
open import Data.Integer
open import Data.Product

-- This file contains the definition of values for the definitional
-- interpreter for MJ using scopes and frames, described in Section 5
-- of the paper.

module MJSF.Values (k : ℕ) where

open import MJSF.Syntax k
open import ScopesFrames.ScopesFrames k Ty

module ValuesG (g : Graph) where

  open SyntaxG g
  open UsesGraph g public
  open import Common.Weakening

  ------------
  -- VALUES --
  ------------

  -- The values used in our interpreter at run time are either:
  --
  -- * object references `ref`, represented in terms of a frame scoped
  --   by a class scope;
  --
  -- * null values (`ref` typed);
  --
  -- * an integer number literal (`int` typed); or
  --
  -- * `void` (`void typed -- note that there is no expression syntax
  --   for producing a `void` value directly, but method bodies still
  --   return `void`; we regard `void` as a unit type)

  data Val : VTy → List Scope → Set where
    ref    :  ∀ {s s' Σ} → s <: s' → Frame s Σ → Val (ref s') Σ
    null   :  ∀ {s Σ} → Val (ref s) Σ
    num    :  ∀ {Σ} → ℤ → Val int Σ
    void   :  ∀ {Σ} → Val void Σ

  -- There are three kinds of values stored in frame slots at run
  -- time, corresponding to each of the three kinds of declarations
  -- defined in `MJSF.Syntax`:
  --
  -- * values, as defined above;
  --
  -- * methods, where a method records a "self" frame `Frame s Σ` and
  --   a well-typed method definition `Meth s ts rt`, such that the
  --   scope of the method corresponds to the "self"; and
  --
  -- * classes which record a well-typed class definition and a
  --   witness that the class has a finite inheritance chain, both
  --   used for initializing new object instances, as well as a frame
  --   pointer to the root frame (class table).

  data Valᵗ : Ty → List Scope → Set where
    vᵗ : ∀ {t Σ} → Val t Σ → Valᵗ (vᵗ t) Σ
    mᵗ : ∀ {s ts rt Σ} → (self : Frame s Σ) → (body : Meth s ts rt) → Valᵗ (mᵗ ts rt) Σ
    cᵗ : ∀ {sʳ s s' Σ} → (class-def : Class sʳ s) → (ic : Inherits s s') → (root : Frame sʳ Σ) → Valᵗ (cᵗ sʳ s) Σ

  ---------------
  -- WEAKENING --
  ---------------

  -- We define notions of weakening for each of the values summarized above:

  val-weaken    :  ∀ {t Σ Σ'} → Σ ⊑ Σ' → Val t Σ → Val t Σ'
  val-weaken ext (num i)  =  num i
  val-weaken ext (ref i f)  =  ref i (wk ext f)
  val-weaken ext null     =  null
  val-weaken ext void     =  void

  instance
    val-weakenable : ∀ {t} → Weakenable (Val t)
    val-weakenable = record { wk = val-weaken }

  valᵗ-weaken : ∀ {t Σ Σ'} → Σ ⊑ Σ' → Valᵗ t Σ → Valᵗ t Σ'
  valᵗ-weaken ext (vᵗ v)      = vᵗ (val-weaken ext v)
  valᵗ-weaken ext (mᵗ f m)    = mᵗ (wk ext f) m
  valᵗ-weaken ext (cᵗ c ic f) = cᵗ c ic (wk ext f)

  -- And pass these to the scope graph definition:

  open UsesVal Valᵗ valᵗ-weaken renaming (getFrame to getFrame')

  --------------
  -- COERCION --
  --------------

  -- Our definition of sub-typing gives rise to a notion of sub-type
  -- coercion, defined below.  Coercions essentially traverse the
  -- inheritance links of the frame hierarchy for an object instance,
  -- as described in the paper.

  upcastRef : ∀ {t t' Σ} → t <: t' → Val (ref t) Σ → Val (ref t') Σ
  upcastRef i (ref i' f) = ref (concatₚ i' i) f
  upcastRef i null = null


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

------------------------------------------------------------------------------
import      LibraBFT.Impl.Consensus.SafetyRules.PersistentSafetyStorage as PersistentSafetyStorage
import      LibraBFT.Impl.Consensus.SafetyRules.SafetyRules             as SafetyRules
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------

module LibraBFT.Impl.Consensus.SafetyRules.SafetyRulesManager where

storage
  : SafetyRulesConfig -> Author -> SK
  → Either ErrLog PersistentSafetyStorage
storage config obmMe obmSK = do
  pure $ PersistentSafetyStorage.new  -- internalStorage
           obmMe
           (config ^∙ srcObmGenesisWaypoint)
           obmSK

newLocal : PersistentSafetyStorage → Bool → Either ErrLog SafetyRulesManager

new
  : SafetyRulesConfig → Author → SK
  → Either ErrLog SafetyRulesManager
new config obmMe obmSK = do
  storage0               ← storage config obmMe obmSK
  let exportConsensusKey = config ^∙ srcExportConsensusKey
  case config ^∙ srcService of λ where
    SRSLocal → newLocal storage0 exportConsensusKey

newLocal storage0 exportConsensusKey = do
  safetyRules ← SafetyRules.new storage0 exportConsensusKey
  pure (mkSafetyRulesManager (SRWLocal safetyRules))

client : SafetyRulesManager → SafetyRules
client self = case self ^∙ srmInternalSafetyRules of λ where
  (SRWLocal safetyRules) → safetyRules


text:
open import Type

module Graph.Walk.Functions {ℓ₁ ℓ₂} {V : Type{ℓ₁}} where

import      Lvl
open import Graph{ℓ₁}{ℓ₂}(V)
open import Graph.Properties
open import Graph.Walk{ℓ₁}{ℓ₂}{V}
open import Numeral.Natural
open import Syntax.Function
open import Type.Dependent
open import Type.Dependent.Functions

module _ {_⟶_ : Graph} where
  edge : ∀{a b} → (a ⟶ b) → (Walk(_⟶_) a b)
  edge e = prepend e at

  join : ∀{a b c} → (a ⟶ b) → (b ⟶ c) → (Walk(_⟶_) a c)
  join e₁ e₂ = prepend e₁ (edge e₂)

  _++_ : ∀{a b c} → Walk(_⟶_) a b → Walk(_⟶_) b c → Walk(_⟶_) a c
  at            ++ w₂ = w₂
  prepend e₁ w₁ ++ w₂ = prepend e₁ (w₁ ++ w₂)

  postpend : ∀{a b c} → (Walk(_⟶_) a b) → (b ⟶ c) → (Walk(_⟶_) a c)
  postpend at             e₂ = edge e₂
  postpend (prepend e₁ w) e₂ = prepend e₁ (postpend w e₂)

  reverse : ⦃ Undirected(_⟶_) ⦄ → ∀{a b} → Walk(_⟶_) a b → Walk(_⟶_) b a
  reverse at            = at
  reverse (prepend e w) = postpend (reverse w) (undirected-reverse(_⟶_) e)

  prelop : ∀{a c} → (Walk(_⟶_) a c) → Σ(_)(b ↦ Walk(_⟶_) b c)
  prelop at            = intro _ at
  prelop (prepend e w) = intro _ w

  postlop : ∀{a c} → (Walk(_⟶_) a c) → Σ(_)(b ↦ Walk(_⟶_) a b)
  postlop at                          = intro _ at
  postlop (prepend e  at)             = intro _ at
  postlop (prepend e₁ (prepend e₂ w)) = [Σ]-applyᵣ (postlop(prepend e₂ w)) (prepend e₁)

  length : ∀{a b} → (Walk(_⟶_) a b) → ℕ
  length at            = 𝟎
  length (prepend _ w) = 𝐒(length w)

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:
{-# OPTIONS --without-K --rewriting #-}

open import HoTT
open import homotopy.HSpace renaming (HSpaceStructure to HSS)
import homotopy.WedgeExtension as WedgeExt

module homotopy.Pi2HSusp where

module Pi2HSusp {i} {X : Ptd i} (gA : has-level 1 (de⊙ X))
  (cA : is-connected 0 (de⊙ X)) (H-X : HSS X)
  where

  {- TODO this belongs somewhere else, but where? -}
  private
    Type=-ext : ∀ {i} {A B : Type i} (p q : A == B)
      → ((x : A) → coe p x == coe q x) → p == q
    Type=-ext p q α =
      ! (ua-η p)
      ∙ ap ua (Subtype=-out is-equiv-prop (λ= α))
      ∙ ua-η q

  open HSS H-X
  open ConnectedHSpace cA H-X
  private
    A = de⊙ X
    e = pt X

  P : Susp A → Type i
  P x = Trunc 1 (north == x)

  module Codes = SuspRec A A (λ a → ua (μ-e-r-equiv a))

  Codes : Susp A → Type i
  Codes = Codes.f

  Codes-level : (x : Susp A) → has-level 1 (Codes x)
  Codes-level = Susp-elim gA gA
    (λ _ → prop-has-all-paths-↓ has-level-is-prop)

  encode₀ : {x : Susp A} → (north == x) → Codes x
  encode₀ α = transport Codes α e

  encode : {x : Susp A} → P x → Codes x
  encode {x} = Trunc-rec (Codes-level x) encode₀

  decode' : A → P north
  decode' a = [ (merid a ∙ ! (merid e)) ]

  abstract
    transport-Codes-mer : (a a' : A)
      → transport Codes (merid a) a' == μ a a'
    transport-Codes-mer a a' =
      coe (ap Codes (merid a)) a'
        =⟨ Codes.merid-β a |in-ctx (λ w → coe w a') ⟩
      coe (ua (μ-e-r-equiv a)) a'
        =⟨ coe-β (μ-e-r-equiv a) a' ⟩
      μ a a' ∎

    transport-Codes-mer-e-! : (a : A)
      → transport Codes (! (merid e)) a == a
    transport-Codes-mer-e-! a =
      coe (ap Codes (! (merid e))) a
        =⟨ ap-! Codes (merid e) |in-ctx (λ w → coe w a) ⟩
      coe (! (ap Codes (merid e))) a
        =⟨ Codes.merid-β e |in-ctx (λ w → coe (! w) a) ⟩
      coe (! (ua (μ-e-r-equiv e))) a
        =⟨ Type=-ext (ua (μ-e-r-equiv e)) idp (λ x → coe-β _ x ∙ μ-e-l x)
          |in-ctx (λ w → coe (! w) a) ⟩
      coe (! idp) a ∎

  abstract
    encode-decode' : (a : A) → encode (decode' a) == a
    encode-decode' a =
      transport Codes (merid a ∙ ! (merid e)) e
        =⟨ transp-∙ {B = Codes} (merid a) (! (merid e)) e ⟩
      transport Codes (! (merid e)) (transport Codes (merid a) e)
        =⟨ transport-Codes-mer a e ∙ μ-e-r a
          |in-ctx (λ w → transport Codes (! (merid e)) w) ⟩
      transport Codes (! (merid e)) a
        =⟨ transport-Codes-mer-e-! a ⟩
      a ∎

  abstract
    homomorphism : (a a' : A)
      → Path {A = Trunc 1 (north == south)}
        [ merid (μ a a' ) ] [ merid a' ∙ ! (merid e) ∙ merid a ]
    homomorphism = WedgeExt.ext args
      where
      args : WedgeExt.args {a₀ = e} {b₀ = e}
      args = record {m = -1; n = -1; cA = cA; cB = cA;
        P = λ a a' → (_ , Trunc-level {n = 1} _ _);
        f = λ a →  ap [_] $
              merid (μ a e)
                =⟨ ap merid (μ-e-r a) ⟩
              merid a
                =⟨ ap (λ w → w ∙ merid a) (! (!-inv-r (merid e)))
                   ∙ ∙-assoc (merid e) (! (merid e)) (merid a)  ⟩
              merid e ∙ ! (merid e) ∙ merid a ∎;
        g = λ a' → ap [_] $
              merid (μ e a')
                =⟨ ap merid (μ-e-l a') ⟩
              merid a'
                =⟨ ! (∙-unit-r (merid a'))
                   ∙ ap (λ w → merid a' ∙ w) (! (!-inv-l (merid e))) ⟩
              merid a' ∙ ! (merid e) ∙ merid e ∎ ;
        p = ap (λ {(p₁ , p₂) → ap [_] $
              merid (μ e e) =⟨ p₁ ⟩
              merid e       =⟨ p₂ ⟩
              merid e ∙ ! (merid e) ∙ merid e ∎})
             (pair×= (ap (λ x → ap merid x) (! μ-coh)) (coh (merid e)))}
        where coh : {B : Type i} {b b' : B} (p : b == b')
                → ap (λ w → w ∙ p) (! (!-inv-r p)) ∙ ∙-assoc p (! p) p
                  == ! (∙-unit-r p) ∙ ap (λ w → p ∙ w) (! (!-inv-l p))
              coh idp = idp

  decode : {x : Susp A} → Codes x → P x
  decode {x} = Susp-elim {P = λ x → Codes x → P x}
                 decode'
                 (λ a → [ merid a ])
                 (λ a → ↓-→-from-transp (λ= $ STS a))
                 x
    where
    abstract
      STS : (a a' : A) → transport P (merid a) (decode' a')
                         == [ merid (transport Codes (merid a) a') ]
      STS a a' =
        transport P (merid a) [ merid a' ∙ ! (merid e) ]
          =⟨ transport-Trunc (north ==_) (merid a) _ ⟩
        [ transport (north ==_) (merid a) (merid a' ∙ ! (merid e)) ]
          =⟨ ap [_] (transp-cst=idf {A = Susp A} (merid a) _) ⟩
        [ (merid a' ∙ ! (merid e)) ∙ merid a ]
          =⟨ ap [_] (∙-assoc (merid a') (! (merid e)) (merid a)) ⟩
        [ merid a' ∙ ! (merid e) ∙ merid a ]
          =⟨ ! (homomorphism a a') ⟩
        [ merid (μ a a') ]
          =⟨ ap ([_] ∘ merid) (! (transport-Codes-mer a a')) ⟩
        [ merid (transport Codes (merid a) a') ] ∎

  abstract
    decode-encode : {x : Susp A} (tα : P x)
      → decode {x} (encode {x} tα) == tα
    decode-encode {x} = Trunc-elim
      {P = λ tα → decode {x} (encode {x} tα) == tα}
      (λ _ → =-preserves-level Trunc-level)
      (J (λ y p → decode {y} (encode {y} [ p ]) == [ p ])
         (ap [_] (!-inv-r (merid e))))

  main-lemma-eq : Trunc 1 (north' A == north) ≃ A
  main-lemma-eq = equiv encode decode' encode-decode' decode-encode

  ⊙main-lemma : ⊙Trunc 1 (⊙Ω (⊙Susp X)) ⊙≃ X
  ⊙main-lemma = ≃-to-⊙≃ main-lemma-eq idp

  abstract
    main-lemma-iso : Ω^S-group 0 (⊙Trunc 1 (⊙Ω (⊙Susp X))) Trunc-level
                  ≃ᴳ Ω^S-group 0 (⊙Trunc 1 X) Trunc-level
    main-lemma-iso = (record {f = f; pres-comp = pres-comp} , ie)
      where
      h : ⊙Trunc 1 (⊙Ω (⊙Susp X)) ⊙→ ⊙Trunc 1 X
      h = (λ x → [ encode x ]) , idp

      f : Ω (⊙Trunc 1 (⊙Ω (⊙Susp X))) → Ω (⊙Trunc 1 X)
      f = Ω-fmap h

      pres-comp : (p q : Ω^ 1 (⊙Trunc 1 (⊙Ω (⊙Susp X))))
        → f (Ω^S-∙ 0 p q) == Ω^S-∙ 0 (f p) (f q)
      pres-comp = Ω^S-fmap-∙ 0 h

      ie : is-equiv f
      ie = Ω^-isemap 1 h (snd $ ((unTrunc-equiv A gA)⁻¹ ∘e main-lemma-eq))

  abstract
    π₂-Susp : πS 1 (⊙Susp X) ≃ᴳ πS 0 X
    π₂-Susp =
      πS 1 (⊙Susp X)
        ≃ᴳ⟨ πS-Ω-split-iso 0 (⊙Susp X) ⟩
      πS 0 (⊙Ω (⊙Susp X))
        ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso 0 (⊙Ω (⊙Susp X)) ⁻¹ᴳ ⟩
      Ω^S-group 0 (⊙Trunc 1 (⊙Ω (⊙Susp X))) Trunc-level
        ≃ᴳ⟨ main-lemma-iso ⟩
      Ω^S-group 0 (⊙Trunc 1 X) Trunc-level
        ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso 0 X ⟩
      πS 0 X ≃ᴳ∎


text:
module Issue1076 where

{-# OPTIONS --no-coverage-check #-}

-- WAS: Parse error

-- NOW:
-- OPTIONS pragma only allowed at beginning of file, before top module
-- declaration
-- when checking the pragma OPTIONS --no-coverage-check

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2012-07-31, issue reported by Nicolas Pouillard
-- {-# OPTIONS -v tc:100 -v term:100 #-}
-- {-# OPTIONS -v tc.def.alias:20 #-}
-- {-# OPTIONS -v tc:0 -v term:0  #-}
module Issue655 where

-- import Common.Level -- this should not be necessary

module TypeAliases where

  postulate A : Set

  B = A → A

module Ex0 where
 postulate
  f : ∀ {A : Set} → A → A

 yellow = f

 boring : ∀ {A : Set} → A → A
 boring = f

 boring' = λ {A} → f {A}

module Ex1 where
 postulate
  A : Set
  f : ∀ {x : A} → A

 yellow = f

 boring : ∀ {x : A} → A
 boring {x} = f {x}

 boring' = λ {x} → f {x}

module Ex2 where
 postulate
  A : Set
  f : ∀ {B : Set} (x : B) {y : A} → A
  a : A

 yellow = f a

 boring : ∀ {y : A} → A
 boring {y} = f a {y}

 boring' = λ {y} → f a {y}

-- no longer yellow...

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Human.Nat where

open import Human.Bool

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

{-# BUILTIN NATURAL Nat #-}

infix  4 _==_ _<_
infixl 6 _+_ _-_
infixl 7 _*_
-- add theses guys on infixl 7: _div_ _%_

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

{-# BUILTIN NATPLUS _+_ #-}

_-_ : Nat → Nat → Nat
n     - zero = n
zero  - suc m = zero
suc n - suc m = n - m

{-# BUILTIN NATMINUS _-_ #-}

_*_ : Nat → Nat → Nat
zero  * m = zero
suc n * m = m + n * m

{-# BUILTIN NATTIMES _*_ #-}

_==_ : Nat → Nat → Bool
zero  == zero  = true
suc n == suc m = n == m
_     == _     = false

{-# BUILTIN NATEQUALS _==_ #-}

_<_ : Nat → Nat → Bool
_     < zero  = false
zero  < suc _ = true
suc n < suc m = n < m

{-# BUILTIN NATLESS _<_ #-}

div-helper : (k m n j : Nat) → Nat
div-helper k m  zero    j      = k
div-helper k m (suc n)  zero   = div-helper (suc k) m n m
div-helper k m (suc n) (suc j) = div-helper k       m n j

{-# BUILTIN NATDIVSUCAUX div-helper #-}

mod-helper : (k m n j : Nat) → Nat
mod-helper k m  zero    j      = k
mod-helper k m (suc n)  zero   = mod-helper 0       m n m
mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j

{-# BUILTIN NATMODSUCAUX mod-helper #-}

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
module Univalence where

------------------------------------------------------------------------------
-- Basic utilities

open import LeqLemmas
open import FinNatLemmas
open import FiniteFunctions
open import VectorLemmas     -- only _!!_ and lookupassoc are needed
open import Proofs

-- Proofs is a wrapper over all the basic utilities
-- The only thing imported from now on is Proofs

------------------------------------------------------------------------------
-- Structures (Definitions)

-- We use (and extend) the package Categories.

open import Categories.Category
open import Categories.Groupoid
open import Categories.Monoidal
open import Categories.Monoidal.Helpers
open import Categories.Functor
open import Categories.Bifunctor
open import Categories.NaturalIsomorphism
open import Categories.Monoidal.Braided
open import Categories.Monoidal.Symmetric
open import Categories.RigCategory
open import Categories.Bicategory

------------------------------------------------------------------------------
-- General
--
-- We have three representations of types: Agda types, Pi types, and
-- Fin types. We have three equivalence relations between types:
-- extensional equivalences, Pi combinators, and Vec
-- permutations. Each type representation suggests a natural choice
-- for the equivalence relation:
--
-- Agda_Type <===== extensional equivalence =====> Agda_Type
-- Pi_Type   <=====      Pi combinator      =====> Pi_Type
-- Fin_Type  <=====     Vec permutation     =====> Fin_Type
--
--
------------------------------------------------------------------------------
-- Equivalences

open import Equiv
-- Defines extensional equality of functions ∼; quasi-inverses; and
-- then equivalences ≃ between spaces

open import EquivEquiv
-- Defines an extensional equivalence relation to be used to equate
-- equivalences so we can talk about equivalences up to equivalence

------------------------------------------------------------------------------
-- Equivalences between Agda types (extensional type isomorphisms)

open import TypeEquiv
-- Proves that types and type equivalences form a commutative semiring
-- in the Algebra sense

open import TypeEquivEquiv
-- All the equivalences between (type) equivalences

open import Data.Sum.Properties
-- Proves simple properties about type equivalences such as:
-- uniti₊ (unite₊ x) ≡ x

open import Data.SumProd.Properties
-- Proves simple properties about type equivalences such as:
-- distzr x ≡ distz (swap⋆ x)

open import TypeEquivCat
-- Proves that types and type equivalences form a symmetric rig
-- groupoid up to extensional equality of equivalences

------------------------------------------------------------------------------
-- Equivalences between Pi types (combinators)
--
-- Because Pi does not rely on extensionality it is easy to iterate
-- equivalences up and down. The following shows levels -2, -1, 0, and
-- 1.

open import PiU

-- First we introduce a univere U of finite types

open import PiLevelm2
open import Pim2Cat

-- A trivial relation on finite types is to identify all the types;
-- this makes U a contractible (-2)-type, i.e., a singleton.
--
-- The Pi types with the trivial relation that identifies all the
-- types form a trivial symmetric rig groupoid up to propositional
-- equality.
--
-- A (-1)-type is either empty or a singleton. The previous setup at
-- level -2 collapsed U to a singleton and hence also makes U a
-- (-1)-type

open import PiLevel0
open import Pi0Cat

-- If the relation on finite types is modeled after type isomorphisms
-- and all isomorphisms of the same type are equated, we collapse U to
-- the set of natural numbers which makes it a 0-type. (We do not
-- distinguish 'id' and 'not'.)

open import Pi0Examples

-- Pi0 is interesting as a programming language for reversible
-- circuits. This module has a few examples.

open import PiLevel1
open import Pi1Cat

-- If the relation on finite types is modeled after type isomorphisms
-- and only the isomorphisms corresponding to the coherence conditions
-- of rig categories are equated, we make U a 1-type. (We do
-- distinguish 'id' and 'not'.) The higher-level equality on the
-- 2-morphisms is trivial, i.e., all two level morphisms are
-- equated. This should yield a weak 2-category (i.e., a bicategory).

open import Pi1Examples

-- Pi1 is interesting as a programming language for reversible
-- circuits that has its own optimizer. This module has a few
-- examples.

open import PiEquiv

-- Each pi combinator is an equivalence

-- How to make U a 2-type, 3-type, etc. ???

------------------------------------------------------------------------------
-- Equivalences between Fin types (permutations)
--
-- A finite type is a set Fin n for some n. It is possible to directly
-- write permutations between finite types but this is extremely
-- tedious especially if we want to prove that we have enough
-- structure to model a symmetric rig groupoid. What we will do
-- instead is to derive these permutations from equivalences as
-- illustrated by the digram below:
--
-- Fin m <—-Equivalence-—> Fin n
--            ||
--            || Univalence
--            ||
-- Fin m <—-Permutation-—> Fin n
--
-- The vertical line is evocative of the univalence postulate: it is
-- an equivalence between equivalences and concrete identifications
-- expressed as permutations. It is relatively easy to establish the
-- symmetric rig groupoid structure in the top line and then
-- automatically transport it to the bottom line.

open import ConcretePermutation

-- Defines a permutation of a finite set 'Fin m' using two vectors of
-- the form Vec (Fin m) m. The first occurrence of m bounds the values
-- in the vector and the second bounds the length of the vector. In
-- general, a permutation 'Vec (Fin m) n' can be viewed as a function
-- that maps indices in 'Fin n' to values in 'Fin m'. To guarantee
-- that each value in Fin m occurs exactly once in the vector, the
-- representation of permutations includes two proofs that the
-- composition of the two vectors is the identity permutation (in both
-- directions). A crucial property of such permutations is that they
-- can be compared for equality using just ≡ which is elaborated on in
-- the module.
--
-- Ultimately we want to prove that finite sets and permutations form
-- a symmetric rig groupoid. Although it is possible to prove this
-- directly, it is extremely tedious. We will instead develop all the
-- infrastructure using equivalences on finite sets and transport it
-- using a specialized instance of 'univalence'.

open import FinEquivPlusTimes
open import FinEquivTypeEquiv

-- Defines the top line. We prove various equivalences between
-- Fin types like:
--   Fin (m + n) ≃ Fin m ⊎ Fin n
-- and
--   Fin (m * n) ≃ Fin m × Fin n
-- We make sure we have enough equivalences to model a commutative
-- semiring.

-- open import FinEquivEquivPlus
-- open import FinEquivEquivTimes
-- open import FinEquivEquivPlusTimes
-- open import FinEquivCat

-- Establishes that finite types and equivalences for a symmetric rig
-- groupoid. This is the structure we want to transport to permutations.

open import SEquivSCPermEquiv

-- An instance of univalence that allows us to transport all the
-- structure from FinEquivCat to permutations

-- open import CPermCat

-- Establishes that CPerm m n is a symmetric rig category by
-- transporting the structure from FinEquivCat using univalence

-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Wavefront ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-- Composes previously defined equivalences to establish things like:
-- FiniteType (A ⊎ B) (m + n) ≃ FiniteType (B ⊎ A) (n + m)

-- FiniteTpyeEquivCat
-- show that Finite types and equivalences for a symmetric rig groupoid

-- define Permutation
-- should be simple definition

-- define EquivPerm
-- big thm

-- define EquivPermTransport
-- might be just an application of thm to derive the symmetric rig
-- structure on permutations

-- Finding a good representation of permutations is tricky.

-- We can compose equivalences from FinEquiv and TypeEquiv to get
-- equivalences that correspond to permutations on finite sets, e.g.,
--   Fin (m + n) ≃ Fin m ⊎ Fin n ≃ Fin n ⊎ Fin m ≃ Fin (n + m)
-- At this point these permutations are represented as extensional
-- functions. In FinVec, we represent these extensional functions
-- using the one-line notation of permutations represented in Agda as
-- the type 'Vec (Fin m) n' (which we abbreviate as 'FinVec m n').
-- The setup allows us to directly extract one-line permutations from
-- the equivalences. For example, the one-line notation for:
--   FinVec ((m + n) + o) (m + (n + o))
-- is extracted using 'tabulate' of the equivalence between:
--   Fin ((m + n) + o) and Fin (m + (n + o))
-- The fact that we have equivalences for the entire commutative
-- semiring axioms means that we also easily define the one-line
-- notation for composing permutations:
--   FinVec m₁ m₂ → FinVec n₁ n₂ → FinVec (m₁ + n₁) (m₂ + n₂)
--   FinVec m₁ m₂ → FinVec n₁ n₂ → FinVec (m₁ * n₁) (m₂ * n₂)

-- What remains now is to explicitly include proofs that the one-line
-- notation has an inverse and that the two compositions yield the
-- identity permutation. This is one in ConcretePermutation and
-- consists mostly of making explicit the proofs that are implicit in
-- FinEquiv and FinVec.

-- open import FinEquiv
-- Establishes that Fin m ≃ Fin n is a commutative semiring

-- open import ConcretePermutation
-- Establishes that CPerm m n is a commutative semiring (including
-- symmetry now)

-- open import ConcretePermutationProperties
-- Establishes properties of concrete permutations that are necessary
-- to show that it is symmetric rig category

-- open import CPermCat
-- Establishes that CPerm m n is a symmetric rig category

-- FiniteType ???
-- SCEquivSCPermEquiv ???

-- We have so far presented each instance separately. Now we focus on
-- relating the different type representations.
--

-- Now we want to relate Pi-types and type equivalences. The punchline
-- would be that TypeEquivCat is isomorphic to Pi1Cat. But the setup
-- for Pi1Cat allows us to keep going up and down the levels unlike
-- the setup for TypeEquivCat which has extensional equivalence
-- hardwired and can't be generalized to level 2.

-- Are they really really necessary as a stepping stone to prove the
-- correspondence between TypeEquivCat and Pi1Cat ???

-- Equivalences between finite sets (enumerations and permutations);
-- Equivalences between setoids; Equivalences between equivalences;
-- Unfinished files; Unused files

-- open import EnumEquiv
-- equivalence between A and Fin m is an enumeration of A

-- open import SetoidEquiv
-- do a version of EquivSetoid specialized for finite sets that
-- include an enumeration just like quasi-inverses include one
-- particular function to specify the equivalence; must really be done
-- in conjection with SEquivSCPermEquiv so let's wait until
-- dependencies satisfied...

-- open import SEquivSCPermEquiv
-- open import PiPerm
-- open import PiEquiv

-- open import SkFinSetCategory
-- open import Pim1Cat

-- open import LeftCancellation
-- Proves that ((⊤ ⊎ A) ≃ (⊤ ⊎ B)) → A ≃ B
-- open import RepresPerm
-- open import Groupoid
-- should be subsumed by Categories.Groupoid

-- Old proofs
-- open import SubstLemmas
-- open import PathLemmas

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Numeral.Finite where

import Lvl
open import Syntax.Number
open import Data.Boolean.Stmt
open import Functional
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural hiding (𝐏)
open import Type

-- A structure corresponding to a finite set of natural numbers (0,..,n−1).
-- Specifically an upper bounded set of natural numbers, and the boundary is strictly lesser than the parameter.
-- Positive integers including zero less than a specified integer (0≤_<n).
-- Or represented using a set: {(i∊ℕ). 0≤i<n}.
-- The structure works in the following way:
--   • 𝟎 can be constructed for any non-zero upper bound (n).
--   • 𝐒 can be constructed from only a smaller upper bounded 𝕟.
--       Example: A 𝕟 constructed through 𝐒{3} can only be the following:
--         0 ≡ 𝟎{3}
--         1 ≡ 𝐒{3} (𝟎{2})
--         2 ≡ 𝐒{3} (𝐒{2} (𝟎{1}))
--         3 ≡ 𝐒{3} (𝐒{2} (𝐒{1} (𝟎{0})))
--         because there is nothing that could fill the blank in (𝐒{3} (𝐒{2} (𝐒{1} (𝐒{0} (_))))).
--       The smallest upper bound that can be is 0 (from using ℕ and its definition).
--       This limits how many successors (𝐒) that can "fit".
data 𝕟 : ℕ → Type{Lvl.𝟎} where
  𝟎 : ∀{n} → 𝕟(ℕ.𝐒(n))        -- Zero
  𝐒 : ∀{n} → 𝕟(n) → 𝕟(ℕ.𝐒(n)) -- Successor function
{-# INJECTIVE 𝕟 #-}

𝕟₌ = 𝕟 ∘ 𝐒

bound : ∀{n} → 𝕟(n) → ℕ
bound{n} _ = n

minimum : ∀{n} → 𝕟(ℕ.𝐒(n))
minimum{_} = 𝟎

maximum : ∀{n} → 𝕟(ℕ.𝐒(n))
maximum{𝟎}    = 𝟎
maximum{𝐒(n)} = 𝐒(maximum{n})

𝕟-to-ℕ : ∀{n} → 𝕟(n) → ℕ
𝕟-to-ℕ {ℕ.𝟎}    ()
𝕟-to-ℕ {ℕ.𝐒(_)} (𝟎)    = ℕ.𝟎
𝕟-to-ℕ {ℕ.𝐒(_)} (𝐒(n)) = ℕ.𝐒(𝕟-to-ℕ (n))

ℕ-to-𝕟 : (x : ℕ) → ∀{n} → . ⦃ _ : IsTrue(x <? n) ⦄ → 𝕟(n)
ℕ-to-𝕟 (ℕ.𝟎)    {ℕ.𝟎}    ⦃ ⦄
ℕ-to-𝕟 (ℕ.𝐒(x)) {ℕ.𝟎}    ⦃ ⦄
ℕ-to-𝕟 (ℕ.𝟎)    {ℕ.𝐒(_)} ⦃ _ ⦄ = 𝟎
ℕ-to-𝕟 (ℕ.𝐒(x)) {ℕ.𝐒(n)} ⦃ p ⦄ = 𝐒(ℕ-to-𝕟 (x) {n} ⦃ p ⦄)

instance
  𝕟-from-ℕ : ∀{N} → Numeral(𝕟(N))
  Numeral.restriction-ℓ ( 𝕟-from-ℕ {N} ) = Lvl.𝟎
  Numeral.restriction ( 𝕟-from-ℕ {N} ) (n) = IsTrue(n <? N)
  num ⦃ 𝕟-from-ℕ {N} ⦄ (n) ⦃ proof ⦄ = ℕ-to-𝕟 (n) {N} ⦃ proof ⦄


text:
module Monads.StateT where

open import Class.Monad
open import Class.Functor
open import Class.MonadTrans
open import Class.Monad.State
open import Class.Monad.Writer
open import Data.Product
open import Data.Unit.Polymorphic
open import Function
open import Level

private
  variable
    a : Level
    S : Set a

StateT : (Set a → Set a) → Set a → Set a → Set (a)
StateT M S A = S → M (A × S)

module _ {M : Set a → Set a} {{_ : Monad M}} {S} where

  instance
    StateT-Monad : Monad (StateT M S)
    StateT-Monad = record { _>>=_ = helper ; return = λ a → λ s → return (a , s) }
      where
        helper : ∀ {A B} → StateT M S A → (A → StateT M S B) → StateT M S B
        helper x f = λ s → do
          (a' , s') ← x s
          f a' s'

    StateT-MonadState : MonadState (StateT M S) S
    MonadState.get StateT-MonadState s = return (s , s)
    MonadState.put StateT-MonadState s = λ s' → return (tt , s)

instance
  StateT-MonadTrans : MonadTrans (λ M → StateT M S)
  StateT-MonadTrans = record { embed = λ x s → (_, s) <$> x }

  StateT-MonadWriter : ∀ {M W} {{_ : Monad M}} {{_ : MonadWriter M W}}
    → MonadWriter (StateT M S) W
  StateT-MonadWriter = record
    { tell = λ w s → tell w >>= λ _ → return (tt , s)
    ; listen = λ x s → listen (x s) >>= λ { ((a , s') , w) → return ((a , w) , s') }
    ; pass = λ x s → x s >>= λ { (x' , s') → pass (return x') >>= λ a → return (a , s') } }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
------------------------------------------------------------------------------
-- Test the consistency of GroupTheory.Base
------------------------------------------------------------------------------

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

-- In the module GroupTheory.Base we declare Agda postulates as FOL
-- axioms. We test if it is possible to prove an unprovable theorem
-- from these axioms.

module GroupTheory.Base.Consistency.Axioms where

open import GroupTheory.Base

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

postulate impossible : (d e : G) → d ≡ e
{-# ATP prove impossible #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-

This file contains:

- Properties of groupoid truncations

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.GroupoidTruncation.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.GroupoidTruncation.Base

rec : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (gB : isGroupoid B) → (A → B) → (∥ A ∥₁ → B)
rec gB f ∣ x ∣₁ = f x
rec gB f (squash₁ x y p q r s i j k) =
  gB _ _ _ _
    (λ m n → rec gB f (r m n))
    (λ m n → rec gB f (s m n))
    i j k

elim : ∀ {ℓ ℓ'} {A : Type ℓ} {B : ∥ A ∥₁ → Type ℓ'}
  (bG : (x : ∥ A ∥₁) → isGroupoid (B x))
  (f : (x : A) → B ∣ x ∣₁) (x : ∥ A ∥₁) → B x
elim bG f (∣ x ∣₁) = f x
elim bG f (squash₁ x y p q r s i j k) =
  isOfHLevel→isOfHLevelDep 3 bG _ _ _ _
    (λ j k → elim bG f (r j k)) (λ j k → elim bG f (s j k))
    (squash₁ x y p q r s)
    i j k

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Nat.Divisibility where

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

open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥

open import Cubical.HITs.PropositionalTruncation as PropTrunc

open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties
open import Cubical.Data.Nat.Order

open import Cubical.Relation.Nullary

private
  variable
    l m n : ℕ

_∣_ : ℕ → ℕ → Type₀
m ∣ n = ∃[ c ∈ ℕ ] c · m ≡ n

isProp∣ : isProp (m ∣ n)
isProp∣ = squash

prediv : ℕ → ℕ → Type₀
prediv m n = Σ[ c ∈ ℕ ] c · m ≡ n

-- an alternate definition of m ∣ n that doesn't use truncation

_∣'_ : ℕ → ℕ → Type₀
zero  ∣' n = zero ≡ n
suc m ∣' n = Σ[ c ∈ ℕ ] c · suc m ≡ n

isProp∣' : isProp (m ∣' n)
isProp∣' {zero} {n} = isSetℕ _ _
isProp∣' {suc m} {n} (c₁ , p₁) (c₂ , p₂) =
  Σ≡Prop (λ _ → isSetℕ _ _) (inj-·sm {c₁} {m} {c₂} (p₁ ∙ sym p₂))

∣≃∣' : (m ∣ n) ≃ (m ∣' n)
∣≃∣' {zero} = propBiimpl→Equiv isProp∣ isProp∣'
                              (PropTrunc.rec (isSetℕ _ _) λ { (c , p) → 0≡m·0 c ∙ p })
                              (λ p → ∣ zero , p ∣)
∣≃∣' {suc m} = propTruncIdempotent≃ isProp∣'

∣-untrunc : m ∣ n → Σ[ c ∈ ℕ ] c · m ≡ n
∣-untrunc {zero} p = zero , equivFun ∣≃∣' p
∣-untrunc {suc m} = equivFun ∣≃∣'

-- basic properties of ∣

∣-refl : m ≡ n → m ∣ n
∣-refl p = ∣ 1 , +-zero _ ∙ p ∣

∣-trans : l ∣ m → m ∣ n → l ∣ n
∣-trans = PropTrunc.map2 λ {
  (c₁ , p) (c₂ , q) → (c₂ · c₁ , sym (·-assoc c₂ c₁ _) ∙ cong (c₂ ·_) p ∙ q) }

∣-left : ∀ k → m ∣ (m · k)
∣-left k = ∣ k , ·-comm k _ ∣

∣-right : ∀ k → m ∣ (k · m)
∣-right k = ∣ k , refl ∣

∣-cancelʳ : ∀ k → (m · suc k) ∣ (n · suc k) → m ∣ n
∣-cancelʳ k = PropTrunc.map λ {
  (c , p) → (c , inj-·sm (sym (·-assoc c _ (suc k)) ∙ p)) }

∣-multʳ : ∀ k → m ∣ n → (m · k) ∣ (n · k)
∣-multʳ k = PropTrunc.map λ {
  (c , p) → (c , ·-assoc c _ k ∙ cong (_· k) p) }

∣-zeroˡ : zero ∣ m → zero ≡ m
∣-zeroˡ = equivFun ∣≃∣'

∣-zeroʳ : ∀ m → m ∣ zero
∣-zeroʳ m = ∣ zero , refl ∣

∣-oneˡ : ∀ m → 1 ∣ m
∣-oneˡ m = ∣ m , ·-identityʳ m ∣

-- if n > 0, then the constant c (s.t. c · m ≡ n) is also > 0
∣s-untrunc : m ∣ suc n → Σ[ c ∈ ℕ ] (suc c) · m ≡ suc n
∣s-untrunc ∣p∣ with ∣-untrunc ∣p∣
... | (zero  , p) = ⊥.rec (znots p)
... | (suc c , p) = (c , p)

m∣sn→m≤sn : m ∣ suc n → m ≤ suc n
m∣sn→m≤sn {m} {n} = f ∘ ∣s-untrunc
  where f : Σ[ c ∈ ℕ ] (suc c) · m ≡ suc n → Σ[ c ∈ ℕ ] c + m ≡ suc n
        f (c , p) = (c · m) , (+-comm (c · m) m ∙ p)

m∣n→m≤n : {m n : ℕ} → ¬ n ≡ 0 → m ∣ n → m ≤ n
m∣n→m≤n {m = m} {n = n} p q =
  let n≡sd = suc-predℕ _ p
      m≤sd = m∣sn→m≤sn (subst (λ a → m ∣ a) n≡sd q)
  in  subst (λ a → m ≤ a) (sym n≡sd) m≤sd

m∣sn→z<m : m ∣ suc n → zero < m
m∣sn→z<m {zero} p = ⊥.rec (znots (∣-zeroˡ p))
m∣sn→z<m {suc m} p = suc-≤-suc zero-≤

antisym∣ : ∀ {m n} → m ∣ n → n ∣ m → m ≡ n
antisym∣ {zero} {n} z∣n _ = ∣-zeroˡ z∣n
antisym∣ {m} {zero} _ z∣m = sym (∣-zeroˡ z∣m)
antisym∣ {suc m} {suc n} p q = ≤-antisym (m∣sn→m≤sn p) (m∣sn→m≤sn q)

-- Inequality for strict divisibility

stDivIneq : ¬ m ≡ 0 → ¬ m ∣ n → l ∣ m → l ∣ n → l < m
stDivIneq {m = 0} p = ⊥.rec (p refl)
stDivIneq {n = 0} _ q = ⊥.rec (q (∣-zeroʳ _))
stDivIneq {m = suc m} {n = n} {l = l} _ q h h' =
  case (≤-split (m∣sn→m≤sn h))
  return (λ _ → l < suc m) of
    λ { (inl r) → r
      ; (inr r) → ⊥.rec (q (subst (λ a → a ∣ n) r h')) }

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Meta.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Data.Sigma

open import Cubical.Relation.Binary

open import Cubical.DStructures.Base

private
  variable
    ℓ ℓ' ℓ'' ℓ₁ ℓ₁' ℓ₁'' ℓ₂ ℓA ℓA' ℓ≅A ℓ≅A' ℓB ℓB' ℓ≅B ℓC ℓ≅C ℓ≅ᴰ ℓ≅ᴰ' ℓX ℓ≅X ℓD ℓ≅D : Level

-- the total space of a DURGS is a URGS
𝒮ᴰ→𝒮 : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
        {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
        → URGStr (Σ A B) (ℓ-max ℓ≅A ℓ≅B)
𝒮ᴰ→𝒮 {A = A} 𝒮-A {B = B} 𝒮ᴰ-B
  = make-𝒮 {_≅_ = _≅Σ_} ρΣ contrTotalΣ
  where
   open URGStr 𝒮-A
   open URGStrᴰ 𝒮ᴰ-B

   -- in the context of a fixed point (a , b)
   module _ ((a , b) : Σ A B) where
     -- the graph relation on the total space
     _≅Σ_ = λ ((a' , b') : Σ A B)
              → Σ[ e ∈ a ≅ a' ] (b ≅ᴰ⟨ e ⟩ b')
     -- reflexivity for that relation
     ρΣ = ρ a , ρᴰ b
     -- contractability of the corresponding total space
     contrTotalA : isContr (Σ[ a' ∈ A ] (a ≅ a'))
     contrTotalA = isUnivalent→contrRelSingl _≅_ ρ uni a
     contrTotalB : isContr (Σ[ b' ∈ B a ] (b ≅ᴰ⟨ ρ a ⟩ b'))
     contrTotalB = isUnivalent→contrRelSingl (_≅ᴰ⟨ ρ a ⟩_) ρᴰ uniᴰ b

     contrTotalΣ
       = isContrRespectEquiv (relSinglAt (_≅ᴰ⟨ ρ a ⟩_) b
                                  ≃⟨ idEquiv (relSinglAt (_≅ᴰ⟨ ρ a ⟩_) b) ⟩
                                Σ[ b' ∈ B a ] (b ≅ᴰ⟨ ρ a ⟩ b')
                                  -- ≃⟨ invEquiv (Σ-contractFst contrTotalA') ⟩
                                  ≃⟨ invEquiv (Σ-contractFst-recenter contrTotalA (a , ρ a)) ⟩
                                Σ[ (a' , e) ∈ (Σ[ a' ∈ A ] (a ≅ a')) ] Σ[ b' ∈ B a' ] (b ≅ᴰ⟨ e ⟩ b')
                                  ≃⟨ Σ-assoc-≃ ⟩
                                Σ[ a' ∈ A ] Σ[ e ∈ (a ≅ a') ] Σ[ b' ∈ B a' ] (b ≅ᴰ⟨ e ⟩ b')
                                  ≃⟨ Σ-cong-equiv-snd (λ a' → invEquiv Σ-assoc-≃) ⟩
                                Σ[ a' ∈ A ] Σ[ (e , b') ∈ (a ≅ a') × B a' ] (b ≅ᴰ⟨ e ⟩ b')
                                  ≃⟨ Σ-cong-equiv-snd (λ a' → Σ-cong-equiv-fst Σ-swap-≃) ⟩
                                Σ[ a' ∈ A ] Σ[ (b' , e) ∈ (B a' × (a ≅ a')) ] (b ≅ᴰ⟨ e ⟩ b')
                                  ≃⟨ Σ-cong-equiv-snd (λ a' → Σ-assoc-≃) ⟩
                                Σ[ a' ∈ A ] Σ[ b' ∈ B a' ] Σ[ e ∈ (a ≅ a') ] (b ≅ᴰ⟨ e ⟩ b')
                                  ≃⟨ invEquiv Σ-assoc-≃ ⟩
                                Σ[ (a' , b') ∈ Σ A B ] Σ[ e ∈ (a ≅ a') ] (b ≅ᴰ⟨ e ⟩ b') ■)
                                contrTotalB

-- integral notation like in the disp cats paper
∫⟨_⟩_ : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
       {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
       → URGStr (Σ A B) (ℓ-max ℓ≅A ℓ≅B)
∫⟨_⟩_ 𝒮-A {B} DispStrB .URGStr._≅_ = 𝒮ᴰ→𝒮 𝒮-A DispStrB .URGStr._≅_
∫⟨_⟩_ 𝒮-A {B} DispStrB .URGStr.ρ = 𝒮ᴰ→𝒮 𝒮-A DispStrB .URGStr.ρ
∫⟨_⟩_ 𝒮-A {B} DispStrB .URGStr.uni = 𝒮ᴰ→𝒮 𝒮-A DispStrB .URGStr.uni

-- transport URG structures along an equivalence
𝒮-transport : {A : Type ℓA} {A' : Type ℓA'}
               (e : A ≃ A') (StrA : URGStr A ℓ≅A)
               → URGStr A' ℓ≅A
𝒮-transport {A = A} {A' = A'} e StrA =
  make-𝒮 {_≅_ = λ a a' → e- a ≅ e- a'}
             (λ a → ρ (e- a))
             λ a → isContrRespectEquiv (Σ[ x ∈ A ] e- a ≅ x
                                           ≃⟨ Σ-cong-equiv-snd (λ x → pathToEquiv (cong (e- a ≅_)
                                                                                (sym (Iso.leftInv (equivToIso e)
                                                                                x)))) ⟩
                                       Σ[ x ∈ A ] e- a ≅ e- (e* x)
                                          ≃⟨ Σ-cong-equiv-fst e ⟩
                                       Σ[ a' ∈ A' ] e- a ≅ e- a' ■)
                                         (𝒮→cTS StrA (e- a))
                                       where
                                         open URGStr StrA
                                         e⁻¹ = invEquiv e
                                         e- = equivFun e⁻¹
                                         e* = equivFun e

-- obtain a path from a relation
𝒮-≅→≡ : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
          {a a' : A} (p : URGStr._≅_ 𝒮-A a a')
          → a ≡ a'
𝒮-≅→≡ 𝒮-A {a} {a'} p = equivFun (invEquiv (isUnivalent→isUnivalent' _≅_ ρ uni a a')) p
  where
    open URGStr 𝒮-A

-- context: structure on A, B and C displayed over A
-- then B can be lifted to be displayed over ∫⟨ 𝒮-A ⟩ 𝒮ᴰ-C
VerticalLift-𝒮ᴰ : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
        {B : A → Type ℓB}
        (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
        {C : A → Type ℓC}
        (𝒮ᴰ-C : URGStrᴰ 𝒮-A C ℓ≅C)
        → URGStrᴰ (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-C) (λ (a , _) → B a) ℓ≅B
VerticalLift-𝒮ᴰ {ℓ≅B = ℓ≅B} 𝒮-A {B = B} 𝒮ᴰ-B 𝒮ᴰ-C =
  urgstrᴰ (λ b (pA , _) b' → b ≅ᴰ⟨ pA ⟩ b')
          ρᴰ
          uniᴰ
  where open URGStrᴰ 𝒮ᴰ-B

VerticalLift2-𝒮ᴰ : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
                   {X : A → Type ℓX} (𝒮ᴰ-X : URGStrᴰ 𝒮-A X ℓ≅X)
                   {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
                   {C : Σ A B → Type ℓC} (𝒮ᴰ-C : URGStrᴰ (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-B) C ℓ≅C)
                   → URGStrᴰ (∫⟨ ∫⟨ 𝒮-A ⟩ 𝒮ᴰ-B ⟩ 𝒮ᴰ-C)
                             (λ ((a , b) , c) → X a)
                             ℓ≅X
VerticalLift2-𝒮ᴰ 𝒮-A 𝒮ᴰ-X 𝒮ᴰ-B 𝒮ᴰ-C =
  VerticalLift-𝒮ᴰ (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-B)
                  (VerticalLift-𝒮ᴰ 𝒮-A 𝒮ᴰ-X 𝒮ᴰ-B)
                  𝒮ᴰ-C

-- context: 𝒮-A on A, 𝒮ᴰ-B / A, 𝒮ᴰ-C / ∫⟨𝒮-A⟩ 𝒮ᴰ-B
-- then 𝒮ᴰ-C can be rebased to 𝒮-A
splitTotal-𝒮ᴰ : {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
                {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
                {C : Σ A B → Type ℓC} (𝒮ᴰ-C : URGStrᴰ (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-B) C ℓ≅C)
                → URGStrᴰ 𝒮-A
                          (λ a → Σ[ b ∈ B a ] C (a , b))
                          (ℓ-max ℓ≅B ℓ≅C)
splitTotal-𝒮ᴰ {A = A} 𝒮-A {B} 𝒮ᴰ-B {C} 𝒮ᴰ-C
  = make-𝒮ᴰ (λ (b , c) eA (b' , c') → Σ[ eB ∈ b B≅ᴰ⟨ eA ⟩ b' ] c ≅ᴰ⟨ eA , eB ⟩ c')
            (λ (b , c) → Bρᴰ b , ρᴰ c)
            q

  where
    open URGStrᴰ 𝒮ᴰ-C
    open URGStr 𝒮-A
    _B≅ᴰ⟨_⟩_ = URGStrᴰ._≅ᴰ⟨_⟩_ 𝒮ᴰ-B
    Bρᴰ = URGStrᴰ.ρᴰ 𝒮ᴰ-B
    Buniᴰ = URGStrᴰ.uniᴰ 𝒮ᴰ-B

    module _ (a : A) (b : B a) where
      abstract
        contrTotalB : isContr (Σ[ b' ∈ B a ] b B≅ᴰ⟨ ρ a ⟩ b')
        contrTotalB = isUnivalent→contrRelSingl (_B≅ᴰ⟨ ρ a ⟩_) Bρᴰ Buniᴰ b

        contrTotalC : (c : C (a , b)) → isContr (Σ[ c' ∈ C (a , b) ] c ≅ᴰ⟨ ρ a , Bρᴰ b ⟩ c')
        contrTotalC = isUnivalent→contrRelSingl (λ c₁ c₂ → c₁ ≅ᴰ⟨ ρ a , Bρᴰ b ⟩ c₂) ρᴰ uniᴰ

    abstract
      q = λ a (b , c) → isContrRespectEquiv (Σ[ c' ∈ C (a , b) ] c ≅ᴰ⟨ ρ a , Bρᴰ b ⟩ c'
                                                ≃⟨ invEquiv (Σ-contractFst-recenter (contrTotalB a b) (b , Bρᴰ b)) ⟩
                                            Σ[ (b' , eB) ∈ Σ[ b' ∈ B a ] b B≅ᴰ⟨ ρ a ⟩ b' ] (Σ[ c' ∈ C (a , b') ] (c ≅ᴰ⟨ ρ a , eB ⟩ c'))
                                                       ≃⟨ compEquiv Σ-assoc-≃
                                                                    (compEquiv (Σ-cong-equiv-snd (λ b' → compEquiv (invEquiv Σ-assoc-≃)
                                                                                (compEquiv (Σ-cong-equiv-fst Σ-swap-≃)
                                                                                Σ-assoc-≃)))
                                                                               (invEquiv Σ-assoc-≃)) ⟩
                                                     Σ[ (b' , c') ∈ Σ[ b' ∈ B a ] C (a , b') ] (Σ[ eB ∈ b B≅ᴰ⟨ ρ a ⟩ b' ] (c ≅ᴰ⟨ ρ a , eB ⟩ c')) ■)
                                                     (contrTotalC a b c)

-- pullback in the (∞,1)-topos of DURGs,
-- combine two DURGs over the same URG to one
combine-𝒮ᴰ : {A : Type ℓA} {𝒮-A : URGStr A ℓ≅A}
             {B : A → Type ℓB} {C : A → Type ℓC}
             (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
             (𝒮ᴰ-C : URGStrᴰ 𝒮-A C ℓ≅C)
             → URGStrᴰ 𝒮-A (λ a → B a × C a) (ℓ-max ℓ≅B ℓ≅C)
combine-𝒮ᴰ {𝒮-A = 𝒮-A} 𝒮ᴰ-B 𝒮ᴰ-C = splitTotal-𝒮ᴰ 𝒮-A 𝒮ᴰ-B (VerticalLift-𝒮ᴰ 𝒮-A 𝒮ᴰ-C 𝒮ᴰ-B)

-- old stuff, not sure if relevant

-- extract the relational family from a DURG
SplitTotal-𝒮ᴰ→RelFamily : {ℓ≅A ℓ≅B ℓ≅C : Level}
                          {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
                          {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
                          {C : Σ A B → Type ℓC} (𝒮ᴰ-C : URGStrᴰ (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-B) C ℓ≅C)
                          → Σ[ _≅_ ∈ Rel A A ℓ≅A ]
                               ({a a' : A} ((b , c) : Σ[ b ∈ B a ] C (a , b)) (e : a ≅ a') ((b' , c') : (Σ[ b' ∈ B a' ] C (a' , b'))) → Type (ℓ-max ℓ≅B ℓ≅C))
SplitTotal-𝒮ᴰ→RelFamily 𝒮-A {B = B} 𝒮ᴰ-B {C = C} 𝒮ᴰ-C .fst = _≅_
  where
    open URGStr 𝒮-A
SplitTotal-𝒮ᴰ→RelFamily 𝒮-A {B = B} 𝒮ᴰ-B {C = C} 𝒮ᴰ-C .snd (b , c) e (b' , c') = Σ[ eB ∈ b B≅ᴰ⟨ e ⟩ b' ] (c ≅ᴰ⟨ e , eB ⟩ c')
  where
    open URGStr 𝒮-A
    _B≅ᴰ⟨_⟩_ = URGStrᴰ._≅ᴰ⟨_⟩_ 𝒮ᴰ-B
    open URGStrᴰ 𝒮ᴰ-C

SplitTotal-𝒮ᴰ→RelFamily' : {ℓ≅A ℓ≅B ℓ≅C : Level}
                          {A : Type ℓA} (𝒮-A : URGStr A ℓ≅A)
                          {B : A → Type ℓB} (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
                          {C : Σ A B → Type ℓC} (𝒮ᴰ-C : URGStrᴰ (∫⟨ 𝒮-A ⟩ 𝒮ᴰ-B) C ℓ≅C)
                          → RelFamily A (ℓ-max ℓB ℓC) (ℓ-max ℓ≅B ℓ≅C)
SplitTotal-𝒮ᴰ→RelFamily' 𝒮-A {B = B} 𝒮ᴰ-B {C = C} 𝒮ᴰ-C .fst a = Σ[ b ∈ B a ] C (a , b)
SplitTotal-𝒮ᴰ→RelFamily' 𝒮-A {B = B} 𝒮ᴰ-B {C = C} 𝒮ᴰ-C .snd {a = a} (b , c) (b' , c') = Σ[ p ∈ b B≅ᴰ⟨ ρ a ⟩ b' ] (c C≅ᴰ⟨ ρ a , p ⟩ c')
  where
    open URGStr 𝒮-A
    _B≅ᴰ⟨_⟩_ = URGStrᴰ._≅ᴰ⟨_⟩_ 𝒮ᴰ-B
    _C≅ᴰ⟨_⟩_ = URGStrᴰ._≅ᴰ⟨_⟩_ 𝒮ᴰ-C

-- combine two structures 𝒮-B and 𝒮-C over 𝒮-A to a structure 𝒮-B × 𝒮-C over A, direct proof
combine'-𝒮ᴰ : {A : Type ℓA} {𝒮-A : URGStr A ℓ≅A}
                 {B : A → Type ℓB} {C : A → Type ℓC}
                 (𝒮ᴰ-B : URGStrᴰ 𝒮-A B ℓ≅B)
                 (𝒮ᴰ-C : URGStrᴰ 𝒮-A C ℓ≅C)
                 → URGStrᴰ 𝒮-A (λ a → B a × C a) (ℓ-max ℓ≅B ℓ≅C)
combine'-𝒮ᴰ {ℓ≅B = ℓ≅B} {ℓ≅C = ℓ≅C} {A = A} {𝒮-A = 𝒮-A} {B = B} {C = C} 𝒮ᴰ-B 𝒮ᴰ-C =
  make-𝒮ᴰ -- equality in the combined structure is defined componentwise
              (λ (b , c) p (b' , c') → b B≅ᴰ⟨ p ⟩ b' × c C≅ᴰ⟨ p ⟩ c')
              -- reflexivity follows from B and C reflexivity
              (λ (b , c) → Bρᴰ b , Cρᴰ c)
              -- so does univalence
              contrTot
  where
    ρ = URGStr.ρ 𝒮-A
    _B≅ᴰ⟨_⟩_ = URGStrᴰ._≅ᴰ⟨_⟩_ 𝒮ᴰ-B
    _C≅ᴰ⟨_⟩_ = URGStrᴰ._≅ᴰ⟨_⟩_ 𝒮ᴰ-C
    Bρᴰ = URGStrᴰ.ρᴰ 𝒮ᴰ-B
    Cρᴰ = URGStrᴰ.ρᴰ 𝒮ᴰ-C
    Buniᴰ = URGStrᴰ.uniᴰ 𝒮ᴰ-B
    Cuniᴰ = URGStrᴰ.uniᴰ 𝒮ᴰ-C
    contrTot : (a : A) ((b , c) : B a × C a) → isContr (Σ[ (b' , c') ∈ B a × C a ] (b B≅ᴰ⟨ ρ a ⟩ b' × c C≅ᴰ⟨ ρ a ⟩ c') )
    contrTot = λ (a : A) ((b , c) : B a × C a)
      → isContrRespectEquiv (Σ[ b' ∈ B a ] (b B≅ᴰ⟨ ρ a ⟩ b')
                                 ≃⟨ invEquiv (Σ-contractSnd (λ _ → isUnivalent→contrRelSingl (_C≅ᴰ⟨ ρ a ⟩_) Cρᴰ Cuniᴰ c)) ⟩
                               (Σ[ b' ∈ B a ] (b B≅ᴰ⟨ ρ a ⟩ b')) × (Σ[ c' ∈ C a ] (c C≅ᴰ⟨ ρ a ⟩ c'))
                                 ≃⟨ Σ-assoc-≃ ⟩
                               (Σ[ b' ∈ B a ] Σ[ _ ∈ b B≅ᴰ⟨ ρ a ⟩ b' ] Σ[ c' ∈ C a ] (c C≅ᴰ⟨ ρ a ⟩ c'))
                                 ≃⟨ Σ-cong-equiv-snd (λ b' → compEquiv (invEquiv Σ-assoc-≃) (compEquiv (Σ-cong-equiv-fst Σ-swap-≃) Σ-assoc-≃)) ⟩
                               (Σ[ b' ∈ B a ] Σ[ c' ∈ C a ] Σ[ _ ∈ b B≅ᴰ⟨ ρ a ⟩ b' ] (c C≅ᴰ⟨ ρ a ⟩ c'))
                                 ≃⟨ invEquiv Σ-assoc-≃ ⟩
                               (Σ[ (b' , c') ∈ B a × C a ] (b B≅ᴰ⟨ ρ a ⟩ b' × c C≅ᴰ⟨ ρ a ⟩ c') ) ■)
                               (isUnivalent→contrRelSingl (_B≅ᴰ⟨ ρ a ⟩_) Bρᴰ Buniᴰ b)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Structures.Pointed where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path

open import Cubical.Foundations.Pointed.Base

open import Cubical.Foundations.SIP renaming (SNS-PathP to SNS)

private
  variable
    ℓ : Level

-- Pointed types with SNS

pointed-structure : Type ℓ → Type ℓ
pointed-structure X = X

pointed-iso : StrIso pointed-structure ℓ
pointed-iso A B f = equivFun f (pt A) ≡ pt B

pointed-is-SNS : SNS {ℓ} pointed-structure pointed-iso
pointed-is-SNS f = invEquiv (ua-ungluePath-Equiv f)

pointed-SIP : (A B : Pointed ℓ) → A ≃[ pointed-iso ] B ≃ (A ≡ B)
pointed-SIP = SIP pointed-structure pointed-iso pointed-is-SNS

pointed-sip : (A B : Pointed ℓ) → A ≃[ pointed-iso ] B → (A ≡ B)
pointed-sip A B = equivFun (pointed-SIP A B) -- ≡ λ (e , p) i → ua e i , ua-gluePath e p i