text:
module Numeral.Integer.Relation.Divisibility where

open import Functional
open import Logic.Propositional
import      Numeral.Natural.Relation.Divisibility as ℕ
open import Numeral.Integer
open import Type

_∣_ = (ℕ._∣_) on₂ absₙ
_∤_ = (¬_) ∘₂ (_∣_)


text:
module Oscar.Data.Product where

open import Data.Product public using (Σ; _,_; proj₁; proj₂; ∃; ∃₂; _×_)

ext: agda


text:
module BasicIPC.Metatheory.Gentzen-TarskiGluedClosedImplicit where

open import BasicIPC.Syntax.Gentzen public
open import BasicIPC.Semantics.TarskiGluedClosedImplicit public

open ImplicitSyntax (∅ ⊢_) public

-- Completeness with respect to a particular model.

module _ {{_ : Model}} where
  reify : ∀ {A} → ⊩ A → ∅ ⊢ A
  reify {α P}   s = syn s
  reify {A ▻ B} s = syn s
  reify {A ∧ B} s = pair (reify (π₁ s)) (reify (π₂ s))
  reify {⊤}    s = unit

  reify⋆ : ∀ {Ξ} → ⊩⋆ Ξ → ∅ ⊢⋆ Ξ
  reify⋆ {∅}     ∙        = ∙
  reify⋆ {Ξ , A} (ts , t) = reify⋆ ts , reify t

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)    γ = lookup i γ
eval (lam t)    γ = multicut (reify⋆ γ) (lam t) ⅋ λ a →
                      eval t (γ , a)
eval (app t u)  γ = eval t γ ⟪$⟫ eval u γ
eval (pair t u) γ = eval t γ , eval u γ
eval (fst t)    γ = π₁ (eval t γ)
eval (snd t)    γ = π₂ (eval t γ)
eval unit       γ = ∙

-- TODO: Correctness of evaluation with respect to conversion.

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { ⊩ᵅ_ = λ P → ∅ ⊢ α P
      }

-- Completeness with respect to all models, or quotation, for closed terms only.

quot₀ : ∀ {A} → ∅ ⊨ A → ∅ ⊢ A
quot₀ t = reify (t ∙)

-- Normalisation by evaluation, for closed terms only.

norm₀ : ∀ {A} → ∅ ⊢ A → ∅ ⊢ A
norm₀ = quot₀ ∘ eval

-- TODO: Correctness of normalisation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- Operations on and properties of decidable relations
------------------------------------------------------------------------

module Relation.Nullary.Decidable where

open import Data.Empty
open import Data.Function
open import Data.Bool
open import Data.Product hiding (map)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

decToBool : ∀ {P} → Dec P → Bool
decToBool (yes _) = true
decToBool (no  _) = false

True : ∀ {P} → Dec P → Set
True Q = T (decToBool Q)

False : ∀ {P} → Dec P → Set
False Q = T (not (decToBool Q))

witnessToTruth : ∀ {P} {Q : Dec P} → True Q → P
witnessToTruth {Q = yes p} _  = p
witnessToTruth {Q = no  _} ()

map : ∀ {P Q} → P ⇔ Q → Dec P → Dec Q
map eq (yes p) = yes (proj₁ eq p)
map eq (no ¬p) = no (¬p ∘ proj₂ eq)

fromYes : ∀ {P} → P → Dec P → P
fromYes _ (yes p) = p
fromYes p (no ¬p) = ⊥-elim (¬p p)

fromYes-map-commute :
  ∀ {P Q p q} (eq : P ⇔ Q) (d : Dec P) →
  fromYes q (map eq d) ≡ proj₁ eq (fromYes p d)
fromYes-map-commute         _ (yes p) = refl
fromYes-map-commute {p = p} _ (no ¬p) = ⊥-elim (¬p p)

max_issues_repo_name: larrytheliquid/Lemmachine


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

module Cubical.Induction.WellFounded where

open import Cubical.Foundations.Everything

Rel : ∀{ℓ} → Type ℓ → ∀ ℓ' → Type _
Rel A ℓ = A → A → Type ℓ

module _ {ℓ ℓ'} {A : Type ℓ} (_<_ : A → A → Type ℓ') where
  WFRec : ∀{ℓ''} → (A → Type ℓ'') → A → Type _
  WFRec P x = ∀ y → y < x → P y

  data Acc (x : A) : Type (ℓ-max ℓ ℓ') where
    acc : WFRec Acc x → Acc x

  WellFounded : Type _
  WellFounded = ∀ x → Acc x

module _ {ℓ ℓ'} {A : Type ℓ} {_<_ : A → A → Type ℓ'} where
  isPropAcc : ∀ x → isProp (Acc _<_ x)
  isPropAcc x (acc p) (acc q)
    = λ i → acc (λ y y<x → isPropAcc y (p y y<x) (q y y<x) i)

  access : ∀{x} → Acc _<_ x → WFRec _<_ (Acc _<_) x
  access (acc r) = r

  private
    wfi : ∀{ℓ''} {P : A → Type ℓ''}
        → ∀ x → (wf : Acc _<_ x)
        → (∀ x → (∀ y → y < x → P y) → P x)
        → P x
    wfi x (acc p) e = e x λ y y<x → wfi y (p y y<x) e

  module WFI (wf : WellFounded _<_) where
    module _ {ℓ''} {P : A → Type ℓ''} (e : ∀ x → (∀ y → y < x → P y) → P x) where
      private
        wfi-compute : ∀ x ax → wfi x ax e ≡ e x (λ y _ → wfi y (wf y) e)
        wfi-compute x (acc p)
          = λ i → e x (λ y y<x → wfi y (isPropAcc y (p y y<x) (wf y) i) e)

      induction :  ∀ x → P x
      induction x = wfi x (wf x) e

      induction-compute : ∀ x → induction x ≡ (e x λ y _ → induction y)
      induction-compute x = wfi-compute x (wf x)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

open import Cubical.Core.Everything
open import Cubical.Algebra.Monoid

module Cubical.Algebra.Monoid.Construct.Opposite {ℓ} (M : Monoid ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Prod using (_,_)

open Monoid M

import Cubical.Algebra.Semigroup.Construct.Opposite semigroup as OpSemigroup
open OpSemigroup public hiding (Op-isSemigroup; Sᵒᵖ)

•ᵒᵖ-identityˡ : LeftIdentity ε _•ᵒᵖ_
•ᵒᵖ-identityˡ _ = identityʳ _

•ᵒᵖ-identityʳ : RightIdentity ε _•ᵒᵖ_
•ᵒᵖ-identityʳ _ = identityˡ _

•ᵒᵖ-identity : Identity ε _•ᵒᵖ_
•ᵒᵖ-identity = •ᵒᵖ-identityˡ , •ᵒᵖ-identityʳ

Op-isMonoid : IsMonoid Carrier _•ᵒᵖ_ ε
Op-isMonoid = record
  { isSemigroup = OpSemigroup.Op-isSemigroup
  ; identity    = •ᵒᵖ-identity
  }

Mᵒᵖ : Monoid ℓ
Mᵒᵖ = record { isMonoid = Op-isMonoid }


text:
module Structure.Operator.Vector.LinearMap.Equiv where

open import Functional
open import Function.Proofs
open import Logic.Predicate
import      Lvl
open import Structure.Category
open import Structure.Function
open import Structure.Function.Multi
open import Structure.Operator.Properties
open import Structure.Operator.Vector.LinearMap
open import Structure.Operator.Vector.LinearMaps
open import Structure.Operator.Vector.Proofs
open import Structure.Operator.Vector
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓ ℓᵥ ℓᵥₗ ℓᵥᵣ ℓᵥ₁ ℓᵥ₂ ℓᵥ₃ ℓₛ ℓᵥₑ ℓᵥₑₗ ℓᵥₑᵣ ℓᵥₑ₁ ℓᵥₑ₂ ℓᵥₑ₃ ℓₛₑ : Lvl.Level
private variable V Vₗ Vᵣ V₁ V₂ V₃ S : Type{ℓ}
private variable _+ᵥ_ _+ᵥₗ_ _+ᵥᵣ_ _+ᵥ₁_ _+ᵥ₂_ _+ᵥ₃_ : V → V → V
private variable _⋅ₛᵥ_ _⋅ₛᵥₗ_ _⋅ₛᵥᵣ_ _⋅ₛᵥ₁_ _⋅ₛᵥ₂_ _⋅ₛᵥ₃_ : S → V → V
private variable _+ₛ_ _⋅ₛ_ : S → S → S
private variable f g : Vₗ → Vᵣ

open VectorSpace ⦃ … ⦄

module _ ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄ where
  private variable A B : VectorSpaceVObject {ℓᵥ}{_}{ℓᵥₑ}{ℓₛₑ} ⦃ equiv-S ⦄ (_+ₛ_)(_⋅ₛ_)

  [_→ˡⁱⁿᵉᵃʳᵐᵃᵖ_]-equiv : Equiv(A →ˡⁱⁿᵉᵃʳᵐᵃᵖ B)
  Equiv._≡_ [_→ˡⁱⁿᵉᵃʳᵐᵃᵖ_]-equiv ([∃]-intro f) ([∃]-intro g) = {!!}
  Equiv.equivalence [_→ˡⁱⁿᵉᵃʳᵐᵃᵖ_]-equiv = {!!}

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:
data D (X : Set) : Set

data D (X : Set) where

-- Should complain about repeated type signature for X

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Streams
------------------------------------------------------------------------

module Stream where

open import Codata.Musical.Stream public renaming (_∷_ to _≺_)

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
open import Data.Product using ( _×_ ; _,_ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox using ( ABox ; ε ; _,_ ; _∼_ ; _∈₁_ ; _∈₂_ )
open import Web.Semantic.DL.ABox.Interp using ( ⌊_⌋ ; ind )
open import Web.Semantic.DL.ABox.Model using ( _⊨a_ )
open import Web.Semantic.DL.Concept.Model using ( ⟦⟧₁-resp-≈ )
open import Web.Semantic.DL.Concept.Skolemization using ( CSkolems ; cskolem ; cskolem-sound )
open import Web.Semantic.DL.FOL using  ( Formula ; true ; _∧_ ; _∈₁_ ; _∈₂_ ; _∼_ )
open import Web.Semantic.DL.FOL.Model using ( _⊨f_ )
open import Web.Semantic.DL.Role.Skolemization using ( rskolem ; rskolem-sound )
open import Web.Semantic.DL.Role.Model using ( ⟦⟧₂-resp-≈ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.Util using ( True ; tt )

module Web.Semantic.DL.ABox.Skolemization {Σ : Signature} {X : Set} where

askolem : ∀ {Δ} → (X → Δ) → ABox Σ X → Formula Σ Δ
askolem i ε = true
askolem i (A , B) = (askolem i A) ∧ (askolem i B)
askolem i (x ∼ y) = i x ∼ i y
askolem i (x ∈₁ c) = i x ∈₁ c
askolem i ((x , y) ∈₂ r) = (i x , i y) ∈₂ r

askolem-sound : ∀ I A → (⌊ I ⌋ ⊨f askolem (ind I) A) → (I ⊨a A)
askolem-sound I ε _ = tt
askolem-sound I (A , B) (I⊨A , I⊨B) = (askolem-sound I A I⊨A , askolem-sound I B I⊨B)
askolem-sound I (x ∼ y) I⊨x∼y = I⊨x∼y
askolem-sound I (x ∈₁ c) I⊨x∈c = I⊨x∈c
askolem-sound I ((x , y) ∈₂ r) I⊨xy∈r = I⊨xy∈r

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module Control.Monad.Transformer where

open import Prelude

record Transformer {a b} (T : (Set a → Set b) → (Set a → Set b)) : Set (lsuc a ⊔ lsuc b) where
  field
    lift : {M : Set a → Set b} {{_ : Monad M}} {A : Set a} → M A → T M A

open Transformer {{...}} public

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --without-K #-}
module Computability.Enumeration.Base where

open import Computability.Prelude
open import Computability.Function

record Enumerable (A : Set) : Set where
  field
    enum : ℕ → A
    bijective : Bijective enum

open Enumerable

ℕ-Enumerable : Enumerable ℕ
enum ℕ-Enumerable n = n
proj₁ (bijective ℕ-Enumerable) eq = eq
proj₁ (proj₂ (bijective ℕ-Enumerable) y) = y
proj₂ (proj₂ (bijective ℕ-Enumerable) y) = refl

max_stars_repo_name: jesyspa/computability-in-agda

max_issues_repo_name: jesyspa/computability-in-agda

max_forks_repo_name: jesyspa/computability-in-agda


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

open import Common.Prelude
open import Common.Equality

{-# BUILTIN REWRITE _≡_ #-}

postulate
  f g    : Nat → Nat
  f-zero : f zero ≡ g zero
  f-suc  : ∀ n → f n ≡ g n → f (suc n) ≡ g (suc n)

r : (n : Nat) → f n ≡ g n
r zero = f-zero
r (suc n) = f-suc n refl
  where
    rn : f n ≡ g n
    rn = r n
    {-# REWRITE rn #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --cubical-compatible #-}
module Common.Equality where

open import Agda.Builtin.Equality public
open import Common.Level

subst : ∀ {a p}{A : Set a}(P : A → Set p){x y : A} → x ≡ y → P x → P y
subst P refl t = t

cong : ∀ {a b}{A : Set a}{B : Set b}(f : A → B){x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl

sym : ∀ {a}{A : Set a}{x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {a}{A : Set a}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl


text:
module _ {T : Type{ℓₒ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  instance
    PredSet-setLike : SetLike{C = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_)
    SetLike._⊆_ PredSet-setLike = _⊆_
    SetLike._≡_ PredSet-setLike = _≡_
    SetLike.[⊆]-membership PredSet-setLike = [↔]-intro intro _⊆_.proof
    SetLike.[≡]-membership PredSet-setLike = [↔]-intro intro _≡_.proof

  instance
    PredSet-emptySet : SetLike.EmptySet{C = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_)
    SetLike.EmptySet.∅          PredSet-emptySet = ∅
    SetLike.EmptySet.membership PredSet-emptySet ()

  instance
    PredSet-universalSet : SetLike.UniversalSet{C = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_)
    SetLike.UniversalSet.𝐔          PredSet-universalSet = 𝐔
    SetLike.UniversalSet.membership PredSet-universalSet = record {}

  instance
    PredSet-unionOperator : SetLike.UnionOperator{C = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_)
    SetLike.UnionOperator._∪_        PredSet-unionOperator = _∪_
    SetLike.UnionOperator.membership PredSet-unionOperator = [↔]-intro id id

  instance
    PredSet-intersectionOperator : SetLike.IntersectionOperator{C = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_)
    SetLike.IntersectionOperator._∩_        PredSet-intersectionOperator = _∩_
    SetLike.IntersectionOperator.membership PredSet-intersectionOperator = [↔]-intro id id

  instance
    PredSet-complementOperator : SetLike.ComplementOperator{C = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_)
    SetLike.ComplementOperator.∁          PredSet-complementOperator = ∁_
    SetLike.ComplementOperator.membership PredSet-complementOperator = [↔]-intro id id

module _ {T : Type{ℓ}} ⦃ equiv : Equiv{ℓ}(T) ⦄ where -- TODO: Levels in SetLike
  instance
    PredSet-mapFunction : SetLike.MapFunction{C₁ = PredSet{ℓ}(T) ⦃ equiv ⦄}{C₂ = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_)(_∈_)
    SetLike.MapFunction.map        PredSet-mapFunction f = map f
    SetLike.MapFunction.membership PredSet-mapFunction   = [↔]-intro id id

  instance
    PredSet-unmapFunction : SetLike.UnmapFunction{C₁ = PredSet{ℓ}(T) ⦃ equiv ⦄}{C₂ = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_)(_∈_)
    SetLike.UnmapFunction.unmap      PredSet-unmapFunction = unmap
    SetLike.UnmapFunction.membership PredSet-unmapFunction = [↔]-intro id id

  instance
    PredSet-unapplyFunction : SetLike.UnapplyFunction{C = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_) {O = T}
    SetLike.UnapplyFunction.unapply    PredSet-unapplyFunction = unapply
    SetLike.UnapplyFunction.membership PredSet-unapplyFunction = [↔]-intro id id

  instance
    PredSet-filterFunction : SetLike.FilterFunction{C = PredSet{ℓ}(T) ⦃ equiv ⦄} (_∈_) {ℓ}{ℓ}
    SetLike.FilterFunction.filter     PredSet-filterFunction = filter
    SetLike.FilterFunction.membership PredSet-filterFunction = [↔]-intro id id

{- TODO: SetLike is not general enough
module _ {T : Type{ℓ}} ⦃ equiv : Equiv{ℓ}(T) ⦄ where
  instance
    -- PredSet-bigUnionOperator : SetLike.BigUnionOperator{Cₒ = PredSet(PredSet(T) ⦃ {!!} ⦄) ⦃ {!!} ⦄} {Cᵢ = PredSet(T) ⦃ {!!} ⦄} (_∈_)(_∈_)
    SetLike.BigUnionOperator.⋃          PredSet-bigUnionOperator = {!⋃!}
    SetLike.BigUnionOperator.membership PredSet-bigUnionOperator = {!!}
-}


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

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

open import Cubical.Structures.NAryOp
open import Cubical.Structures.Pointed
open import Cubical.Structures.Ring hiding (⟨_⟩)

private
  variable
    ℓ ℓ' : Level

comm-ring-axioms : (X : Type ℓ) (s : raw-ring-structure X) → Type ℓ
comm-ring-axioms X (_+_ , ₁ , _·_) = (ring-axioms X (_+_ , ₁ , _·_)) ×
                                     ((x y : X) → x · y ≡ y · x)

comm-ring-structure : Type ℓ → Type ℓ
comm-ring-structure = add-to-structure raw-ring-structure comm-ring-axioms

CommRing : Type (ℓ-suc ℓ)
CommRing {ℓ} = TypeWithStr ℓ comm-ring-structure

comm-ring-iso : StrIso comm-ring-structure ℓ
comm-ring-iso = add-to-iso (join-iso (nAryFunIso 2) (join-iso pointed-iso (nAryFunIso 2))) comm-ring-axioms

comm-ring-axioms-isProp : (X : Type ℓ) (s : raw-ring-structure X) → isProp (comm-ring-axioms X s)
comm-ring-axioms-isProp X (_·_ , ₀ , _+_) = isPropΣ (ring-axioms-isProp X (_·_ , ₀ , _+_))
                                            λ ((((isSetX , _) , _) , _) , _) → isPropΠ2 λ _ _ → isSetX _ _

comm-ring-is-SNS : SNS {ℓ} comm-ring-structure comm-ring-iso
comm-ring-is-SNS = add-axioms-SNS _ comm-ring-axioms-isProp raw-ring-is-SNS

CommRingPath : (M N : CommRing {ℓ}) → (M ≃[ comm-ring-iso ] N) ≃ (M ≡ N)
CommRingPath = SIP comm-ring-is-SNS

-- CommRing is Ring

CommRing→Ring : CommRing {ℓ} → Ring
CommRing→Ring (R , str , isRing , ·comm) = R , str , isRing

-- CommRing Extractors

⟨_⟩ : CommRing {ℓ} → Type ℓ
⟨ R , _ ⟩ = R

module _ (R : CommRing {ℓ}) where

  commring+-operation = ring+-operation (CommRing→Ring R)

  commring-is-set = ring-is-set (CommRing→Ring R)

  commring+-assoc = ring+-assoc (CommRing→Ring R)

  commring+-id = ring+-id (CommRing→Ring R)

  commring+-rid = ring+-rid (CommRing→Ring R)

  commring+-lid = ring+-lid (CommRing→Ring R)

  commring+-inv = ring+-inv (CommRing→Ring R)

  commring+-rinv = ring+-rinv (CommRing→Ring R)

  commring+-linv = ring+-linv (CommRing→Ring R)

  commring+-comm = ring+-comm (CommRing→Ring R)

  commring·-operation = ring·-operation (CommRing→Ring R)

  commring·-assoc = ring·-assoc (CommRing→Ring R)

  commring·-id = ring·-id (CommRing→Ring R)

  commring·-rid = ring·-rid (CommRing→Ring R)

  commring·-lid = ring·-lid (CommRing→Ring R)

  commring-ldist = ring-ldist (CommRing→Ring R)

  commring-rdist = ring-rdist (CommRing→Ring R)

module commring-operation-syntax where

  commring+-operation-syntax : (R : CommRing {ℓ}) → ⟨ R ⟩ → ⟨ R ⟩ → ⟨ R ⟩
  commring+-operation-syntax R = commring+-operation R
  infixr 14 commring+-operation-syntax
  syntax commring+-operation-syntax G x y = x +⟨ G ⟩ y

  commring·-operation-syntax : (R : CommRing {ℓ}) → ⟨ R ⟩ → ⟨ R ⟩ → ⟨ R ⟩
  commring·-operation-syntax R = commring·-operation R
  infixr 18 commring·-operation-syntax
  syntax commring·-operation-syntax G x y = x ·⟨ G ⟩ y

open commring-operation-syntax

commring-comm : (R : CommRing {ℓ}) (x y : ⟨ R ⟩) → x ·⟨ R ⟩ y ≡ y ·⟨ R ⟩ x
commring-comm (_ , _ , _ , P) = P

-- CommRing ·syntax

module commring-·syntax (R : CommRing {ℓ}) where
  open ring-·syntax (CommRing→Ring R) public


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

open import Cubical.Core.Glue
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Nat
open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Data.Prod
open import Cubical.Data.BinNat
open import Cubical.Data.Bool
open import Cubical.Relation.Nullary
open import Direction

module NNat where
-- much of this is based directly on the
-- BinNat module in the Cubical Agda library

data BNat : Type₀ where
  b0 : BNat
  b1 : BNat
  x0 : BNat → BNat
  x1 : BNat → BNat

sucBNat : BNat → BNat
sucBNat b0 = b1
sucBNat b1 = x0 b1
sucBNat (x0 bs) = x1 bs
sucBNat (x1 bs) = x0 (sucBNat bs)

BNat→ℕ : BNat → ℕ
BNat→ℕ b0 = 0
BNat→ℕ b1 = 1
BNat→ℕ (x0 x) = doubleℕ (BNat→ℕ x)
BNat→ℕ (x1 x) = suc (doubleℕ (BNat→ℕ x))

-- BNat→Binℕ : BNat → Binℕ
-- BNat→Binℕ pos0 = binℕ0
-- BNat→Binℕ pos1 = binℕpos pos1
-- BNat→Binℕ (x0 x) = {!binℕpos (x0 binℕpos (BNat→Binℕ x))!}
-- BNat→Binℕ (x1 x) = {!!}

BNat→ℕsucBNat : (b : BNat) → BNat→ℕ (sucBNat b) ≡ suc (BNat→ℕ b)
BNat→ℕsucBNat b0 = refl
BNat→ℕsucBNat b1 = refl
BNat→ℕsucBNat (x0 b) = refl
BNat→ℕsucBNat (x1 b) = λ i → doubleℕ (BNat→ℕsucBNat b i)

ℕ→BNat : ℕ → BNat
ℕ→BNat zero = b0
ℕ→BNat (suc zero) = b1
ℕ→BNat (suc (suc n)) = sucBNat (ℕ→BNat (suc n))

ℕ→BNatSuc : ∀ n → ℕ→BNat (suc n) ≡ sucBNat (ℕ→BNat n)
ℕ→BNatSuc zero = refl
ℕ→BNatSuc (suc n) = refl

bNatInd : {P : BNat → Type₀} → P b0 → ((b : BNat) → P b → P (sucBNat b)) → (b : BNat) → P b
-- prove later...

BNat→ℕ→BNat : (b : BNat) → ℕ→BNat (BNat→ℕ b) ≡ b
BNat→ℕ→BNat b = bNatInd refl hs b
  where
  hs : (b : BNat) → ℕ→BNat (BNat→ℕ b) ≡ b → ℕ→BNat (BNat→ℕ (sucBNat b)) ≡ sucBNat b
  hs b hb =
      ℕ→BNat (BNat→ℕ (sucBNat b))
    ≡⟨ cong ℕ→BNat (BNat→ℕsucBNat b) ⟩
      ℕ→BNat (suc (BNat→ℕ b))
    ≡⟨ ℕ→BNatSuc (BNat→ℕ b) ⟩
      sucBNat (ℕ→BNat (BNat→ℕ b))
    ≡⟨ cong sucBNat hb ⟩
      sucBNat b
    ∎

ℕ→BNat→ℕ : (n : ℕ) → BNat→ℕ (ℕ→BNat n) ≡ n
ℕ→BNat→ℕ zero = refl
ℕ→BNat→ℕ (suc n) =
    BNat→ℕ (ℕ→BNat (suc n))
  ≡⟨ cong BNat→ℕ (ℕ→BNatSuc n) ⟩
    BNat→ℕ (sucBNat (ℕ→BNat n))
  ≡⟨ BNat→ℕsucBNat (ℕ→BNat n) ⟩
    suc (BNat→ℕ (ℕ→BNat n))
  ≡⟨ cong suc (ℕ→BNat→ℕ n) ⟩
    suc n
  ∎

BNat≃ℕ : BNat ≃ ℕ
BNat≃ℕ = isoToEquiv (iso BNat→ℕ ℕ→BNat ℕ→BNat→ℕ BNat→ℕ→BNat)

BNat≡ℕ : BNat ≡ ℕ
BNat≡ℕ = ua BNat≃ℕ

open NatImpl

NatImplBNat : NatImpl BNat
z NatImplBNat = b0
s NatImplBNat = sucBNat

--

data np (r : ℕ) : Type₀ where
  bp : DirNum r → np r
  zp : ∀ (d d′ : DirNum r) → bp d ≡ bp d′
  xp : DirNum r → np r → np r

sucnp : ∀ {r} → np r → np r
sucnp {zero} (bp tt) = xp tt (bp tt)
sucnp {zero} (zp tt tt i) = xp tt (bp tt)
sucnp {zero} (xp tt n) = xp tt (sucnp n)
sucnp {suc r} (bp d) = xp (one-n (suc r)) (bp d)
sucnp {suc r} (zp d d′ i) = xp (one-n (suc r)) (zp d d′ i)
sucnp {suc r} (xp d n) with max? d
... | no _ = xp (next d) n
... | yes _ = xp (zero-n (suc r)) (sucnp n)

np→ℕ : (r : ℕ) (x : np r) → ℕ
np→ℕ r (bp x) = 0
np→ℕ r (zp d d′ i) = 0
np→ℕ zero (xp x x₁) = suc (np→ℕ zero x₁)
np→ℕ (suc r) (xp x x₁) = sucn (DirNum→ℕ x) (doublesℕ (suc r) (np→ℕ (suc r) x₁))

ℕ→np : (r : ℕ) → (n : ℕ) → np r
ℕ→np r zero = bp (zero-n r)
ℕ→np zero (suc n) = xp tt (ℕ→np zero n)
ℕ→np (suc r) (suc n) = sucnp (ℕ→np (suc r) n)

---- generalize bnat:

data N (r : ℕ) : Type₀ where
  bn : DirNum r → N r
  xr : DirNum r → N r → N r

-- should define induction principle for N r

-- we have 2ⁿ "unary" constructors, analogous to BNat with 2¹ (b0 and b1)
-- rename n to r
-- this likely introduces inefficiencies compared
-- to BinNat, with the max? check etc.
sucN : ∀ {n} → N n → N n
sucN {zero} (bn tt) = xr tt (bn tt)
sucN {zero} (xr tt x) = xr tt (sucN x)
sucN {suc n} (bn (↓ , ds)) = (bn (↑ , ds))
sucN {suc n} (bn (↑ , ds)) with max? ds
... | no _ = (bn (↓ , next ds))
... | yes _ = xr (zero-n (suc n)) (bn (one-n (suc n)))
sucN {suc n} (xr d x) with max? d
... | no _ = xr (next d) x
... | yes _ = xr (zero-n (suc n)) (sucN x)

sucnN : {r : ℕ} → (n : ℕ) → (N r → N r)
sucnN n = iter n sucN

doubleN : (r : ℕ) → N r → N r
doubleN zero (bn tt) = bn tt
doubleN zero (xr d x) = sucN (sucN (doubleN zero x))
doubleN (suc r) (bn x) with zero-n? x
... | yes _    = bn x
            -- bad:
... | no _ = caseBool (bn (doubleDirNum (suc r) x)) (xr (zero-n (suc r)) (bn x)) (doubleable-n? x)
-- ... | no _  | doubleable  = {!bn (doubleDirNum x)!}
-- ... | no _  | notdoubleable = xr (zero-n (suc r)) (bn x)
doubleN (suc r) (xr x x₁) = sucN (sucN (doubleN (suc r) x₁))

doublesN : (r : ℕ) → ℕ → N r → N r
doublesN r zero m = m
doublesN r (suc n) m = doublesN r n (doubleN r m)

N→ℕ : (r : ℕ) (x : N r) → ℕ
N→ℕ zero (bn tt) = zero
N→ℕ zero (xr tt x) = suc (N→ℕ zero x)
N→ℕ (suc r) (bn x) = DirNum→ℕ x
N→ℕ (suc r) (xr d x) = sucn (DirNum→ℕ d) (doublesℕ (suc r) (N→ℕ (suc r) x))

N→ℕsucN : (r : ℕ) (x : N r) → N→ℕ r (sucN x) ≡ suc (N→ℕ r x)
N→ℕsucN zero (bn tt) = refl
N→ℕsucN zero (xr tt x) =
    suc (N→ℕ zero (sucN x))
  ≡⟨ cong suc (N→ℕsucN zero x) ⟩
    suc (suc (N→ℕ zero x))
  ∎
N→ℕsucN (suc r) (bn (↓ , d)) = refl
N→ℕsucN (suc r) (bn (↑ , d)) with max? d
... | no d≠max =
          doubleℕ (DirNum→ℕ (next d))
        ≡⟨ cong doubleℕ (next≡suc r d d≠max)  ⟩
          doubleℕ (suc (DirNum→ℕ d))
        ∎
... | yes d≡max = -- this can probably be shortened by not reducing down to zero
          sucn (doubleℕ (DirNum→ℕ (zero-n r)))
            (doublesℕ r (suc (suc (doubleℕ (doubleℕ (DirNum→ℕ (zero-n r)))))))
        ≡⟨ cong (λ x → sucn (doubleℕ x) (doublesℕ r (suc (suc (doubleℕ (doubleℕ x)))))) (zero-n→0 {r}) ⟩
          sucn (doubleℕ zero) (doublesℕ r (suc (suc (doubleℕ (doubleℕ zero)))))
        ≡⟨ refl ⟩
          doublesℕ (suc r) (suc zero) -- 2^(r+1)
        ≡⟨ sym (doubleDoubles r 1) ⟩
          doubleℕ (doublesℕ r (suc zero)) --2*2^r
        ≡⟨ sym (sucPred (doubleℕ (doublesℕ r (suc zero))) (doubleDoublesOne≠0 r)) ⟩
          suc (predℕ (doubleℕ (doublesℕ r (suc zero))))
        ≡⟨ cong suc (sym (sucPred (predℕ (doubleℕ (doublesℕ r (suc zero)))) (predDoubleDoublesOne≠0 r))) ⟩
          suc (suc (predℕ (predℕ (doubleℕ (doublesℕ r (suc zero))))))
        ≡⟨ cong (λ x → suc (suc x)) (sym (doublePred (doublesℕ r (suc zero)))) ⟩
          suc (suc (doubleℕ (predℕ (doublesℕ r (suc zero)))))
        ≡⟨ cong (λ x → suc (suc (doubleℕ x))) (sym (maxr≡pred2ʳ r d d≡max)) ⟩
          suc (suc (doubleℕ (DirNum→ℕ d))) -- 2*(2^r - 1) + 2 = 2^(r+1) - 2 + 2 = 2^(r+1)
        ∎
N→ℕsucN (suc r) (xr (↓ , d) x) = refl
N→ℕsucN (suc r) (xr (↑ , d) x) with max? d
... | no d≠max =
          sucn (doubleℕ (DirNum→ℕ (next d)))
           (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))
        ≡⟨ cong (λ y → sucn (doubleℕ y) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))) (next≡suc r d d≠max) ⟩
          sucn (doubleℕ (suc (DirNum→ℕ d)))
           (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))
        ≡⟨ refl ⟩
          suc
           (suc
            (iter (doubleℕ (DirNum→ℕ d)) suc
            (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
        ∎
... | yes d≡max =
        sucn (doubleℕ (DirNum→ℕ (zero-n r)))
        (doublesℕ r (doubleℕ (N→ℕ (suc r) (sucN x))))
      ≡⟨ cong (λ z → sucn (doubleℕ z) (doublesℕ r (doubleℕ (N→ℕ (suc r) (sucN x))))) (zero-n≡0 {r}) ⟩
        sucn (doubleℕ zero)
        (doublesℕ r (doubleℕ (N→ℕ (suc r) (sucN x))))
      ≡⟨ refl ⟩
        doublesℕ r (doubleℕ (N→ℕ (suc r) (sucN x)))
      ≡⟨ cong (λ x → doublesℕ r (doubleℕ x)) (N→ℕsucN (suc r) x)  ⟩
        doublesℕ r (doubleℕ (suc (N→ℕ (suc r) x)))
      ≡⟨ refl ⟩
        doublesℕ r (suc (suc (doubleℕ (N→ℕ (suc r) x)))) -- 2^r * (2x + 2) = 2^(r+1)x + 2^(r+1)
      ≡⟨ doublesSucSuc r (doubleℕ (N→ℕ (suc r) x)) ⟩
        sucn (doublesℕ (suc r) 1) -- _ + 2^(r+1)
         (doublesℕ (suc r) (N→ℕ (suc r) x)) --  2^(r+1)x + 2^(r+1)
      ≡⟨ H r (doublesℕ (suc r) (N→ℕ (suc r) x)) ⟩
        suc
         (suc
          (sucn (doubleℕ (predℕ (doublesℕ r 1))) -- _ + 2(2^r - 1) + 2
           (doublesℕ (suc r) (N→ℕ (suc r) x))))
      ≡⟨ refl ⟩
        suc
         (suc
          (sucn (doubleℕ (predℕ (doublesℕ r 1)))
           (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
      ≡⟨ cong (λ z → suc (suc (sucn (doubleℕ z) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))) (sym (max→ℕ r))  ⟩
         suc
         (suc
          (sucn (doubleℕ (DirNum→ℕ (max-n r)))
           (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
      ≡⟨ cong (λ z → suc (suc (sucn (doubleℕ (DirNum→ℕ z)) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))) (sym (d≡max)) ⟩
         suc
         (suc
          (sucn (doubleℕ (DirNum→ℕ d))
           (doublesℕ r (doubleℕ (N→ℕ (suc r) x))))) -- (2^r*2x + (2*(2^r - 1))) + 2 = 2^(r+1)x + 2^(r+1)
      ∎
      where
        H : (n m : ℕ) → sucn (doublesℕ (suc n) 1) m ≡ suc (suc (sucn (doubleℕ (predℕ (doublesℕ n 1))) m))
        H zero m = refl
        H (suc n) m =
            sucn (doublesℕ n 4) m
          ≡⟨ cong (λ z → sucn z m) (doublesSucSuc n 2) ⟩
            sucn (sucn (doublesℕ (suc n) 1) (doublesℕ n 2)) m
          ≡⟨ refl ⟩
            sucn (sucn (doublesℕ n 2) (doublesℕ  n 2)) m
          ≡⟨ {!!} ⟩
            sucn (doubleℕ (doublesℕ n 2)) m
          ≡⟨ {!!} ⟩ {!!}

ℕ→N : (r : ℕ) → (n : ℕ) → N r
ℕ→N r zero = bn (zero-n r)
ℕ→N zero (suc n) = xr tt (ℕ→N zero n)
ℕ→N (suc r) (suc n) = sucN (ℕ→N (suc r) n)

ℕ→Nsuc : (r : ℕ) (n : ℕ) → ℕ→N r (suc n) ≡ sucN (ℕ→N r n)
ℕ→Nsuc r n = {!!}

ℕ→Nsucn : (r : ℕ) (n m : ℕ) → ℕ→N r (sucn n m) ≡ sucnN n (ℕ→N r m)
ℕ→Nsucn r n m = {!!}

-- NℕNlemma is actually a pretty important fact;
-- this is what allows the direct isomorphism of N and ℕ to go
-- without the need for an extra datatype, e.g. Pos for BinNat,
-- since each ℕ < 2^r maps to its "numeral" in N r.
-- should rename and move elsewhere.
numeral-next : (r : ℕ) (d : DirNum r) → N (suc r)
numeral-next r d = bn (embed-next r d)

--
NℕNlemma : (r : ℕ) (d : DirNum r) → ℕ→N r (DirNum→ℕ d) ≡ bn d
NℕNlemma zero tt = refl
NℕNlemma (suc r) (↓ , ds) =
    ℕ→N (suc r) (doubleℕ (DirNum→ℕ ds))
  ≡⟨ {!!} ⟩ {!!}
NℕNlemma (suc r) (↑ , ds) = {!!}

N→ℕ→N : (r : ℕ) → (x : N r) → ℕ→N r (N→ℕ r x) ≡ x
N→ℕ→N zero (bn tt) = refl
N→ℕ→N zero (xr tt x) = cong (xr tt) (N→ℕ→N zero x)
N→ℕ→N (suc r) (bn (↓ , ds)) =
    ℕ→N (suc r) (doubleℕ (DirNum→ℕ ds))
  ≡⟨ cong (λ x → ℕ→N (suc r) x) (double-lemma ds) ⟩
    ℕ→N (suc r) (DirNum→ℕ {suc r} (↓ , ds))
  ≡⟨ NℕNlemma (suc r) (↓ , ds) ⟩
    bn (↓ , ds)
  ∎
N→ℕ→N (suc r) (bn (↑ , ds)) =
    sucN (ℕ→N (suc r) (doubleℕ (DirNum→ℕ ds)))
  ≡⟨ cong (λ x → sucN (ℕ→N (suc r) x)) (double-lemma ds) ⟩
    sucN (ℕ→N (suc r) (DirNum→ℕ {suc r} (↓ , ds)))
  ≡⟨ cong sucN (NℕNlemma (suc r) (↓ , ds)) ⟩
    sucN (bn (↓ , ds))
  ≡⟨ refl ⟩
    bn (↑ , ds)
  ∎
N→ℕ→N (suc r) (xr (↓ , ds) x) =
     ℕ→N (suc r)
      (sucn (doubleℕ (DirNum→ℕ ds))
       (doublesℕ r (doubleℕ (N→ℕ (suc r) x))))
   ≡⟨ cong (λ z → ℕ→N (suc r) (sucn z (doublesℕ r (doubleℕ (N→ℕ (suc r) x))))) (double-lemma ds)  ⟩
      ℕ→N (suc r)
      (sucn (DirNum→ℕ {suc r} (↓ , ds))
       (doublesℕ r (doubleℕ (N→ℕ (suc r) x))))
   ≡⟨ refl ⟩
     ℕ→N (suc r)
      (sucn (DirNum→ℕ {suc r} (↓ , ds))
       (doublesℕ (suc r) (N→ℕ (suc r) x)))
   ≡⟨ ℕ→Nsucn (suc r) (DirNum→ℕ {suc r} (↓ , ds)) (doublesℕ (suc r) (N→ℕ (suc r) x)) ⟩
     sucnN (DirNum→ℕ {suc r} (↓ , ds))
      (ℕ→N (suc r) (doublesℕ (suc r) (N→ℕ (suc r) x)))
   ≡⟨ cong (λ z → sucnN (DirNum→ℕ {suc r} (↓ , ds)) z) (H (suc r) (suc r) (N→ℕ (suc r) x)) ⟩
     sucnN (DirNum→ℕ {suc r} (↓ , ds))
      (doublesN (suc r) (suc r) (ℕ→N (suc r) (N→ℕ (suc r) x)))
   ≡⟨ cong (λ z → sucnN (DirNum→ℕ {suc r} (↓ , ds)) (doublesN (suc r) (suc r) z)) (N→ℕ→N (suc r) x) ⟩
     sucnN (DirNum→ℕ {suc r} (↓ , ds))
      (doublesN (suc r) (suc r) x)
   ≡⟨ G (suc r) (↓ , ds) x snotz ⟩
     xr (↓ , ds) x ∎
   where
     H : (r m n : ℕ) → ℕ→N r (doublesℕ m n) ≡ doublesN r m (ℕ→N r n)
     H r m n = {!!}
     G : (r : ℕ) (d : DirNum r) (x : N r) → ¬ (r ≡ 0) → sucnN (DirNum→ℕ {r} d) (doublesN r r x) ≡ xr d x
     G zero d x 0≠0 = ⊥-elim (0≠0 refl)
     G (suc r) d (bn x) r≠0 = {!!}
     G (suc r) d (xr x x₁) r≠0 = {!!}
N→ℕ→N (suc r) (xr (↑ , ds) x) with max? ds
... | no ds≠max =
          sucN
          (ℕ→N (suc r)
           (sucn (doubleℕ (DirNum→ℕ ds))
            (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
        ≡⟨ sym (ℕ→Nsuc (suc r)
                (sucn (doubleℕ (DirNum→ℕ ds)) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
         ⟩
           ℕ→N (suc r)
           (suc (sucn (doubleℕ (DirNum→ℕ ds)) (doublesℕ r (doubleℕ (N→ℕ (suc r) x)))))
        ≡⟨ refl ⟩
           ℕ→N (suc r)
           (suc (sucn (doubleℕ (DirNum→ℕ ds)) (doublesℕ (suc r) (N→ℕ (suc r) x))))
        ≡⟨ cong (λ z → ℕ→N (suc r) z)
                (sym (sucnsuc (doubleℕ (DirNum→ℕ ds)) (doublesℕ (suc r) (N→ℕ (suc r) x))))
         ⟩
           ℕ→N (suc r)
           (sucn (doubleℕ (DirNum→ℕ ds)) (suc (doublesℕ (suc r) (N→ℕ (suc r) x))))
         ≡⟨ ℕ→Nsucn (suc r) (doubleℕ (DirNum→ℕ ds)) (suc (doublesℕ (suc r) (N→ℕ (suc r) x))) ⟩
           sucnN (doubleℕ (DirNum→ℕ ds)) (ℕ→N (suc r) (suc (doublesℕ (suc r) (N→ℕ (suc r) x))))
         ≡⟨ cong (λ z → sucnN (doubleℕ (DirNum→ℕ ds)) z)
                  (ℕ→Nsuc (suc r) (doublesℕ (suc r) (N→ℕ (suc r) x)))
          ⟩
           --   (2^(r+1)*x + 1) + 2*ds
           -- = 2*(2^r*x + ds) + 1
           -- = 2*(
           sucnN (doubleℕ (DirNum→ℕ ds)) (sucN (ℕ→N (suc r) (doublesℕ (suc r) (N→ℕ (suc r) x))))
         ≡⟨ {!!} ⟩ {!!}

... | yes ds≡max = {!!}

ℕ→N→ℕ : (r : ℕ) → (n : ℕ) → N→ℕ r (ℕ→N r n) ≡ n
ℕ→N→ℕ zero zero = refl
ℕ→N→ℕ (suc r) zero =
    doubleℕ (DirNum→ℕ (zero-n r))
  ≡⟨ cong doubleℕ (zero-n≡0 {r}) ⟩
    doubleℕ zero
  ≡⟨ refl ⟩
    zero
  ∎
ℕ→N→ℕ zero (suc n) = cong suc (ℕ→N→ℕ zero n)
ℕ→N→ℕ (suc r) (suc n) =
    N→ℕ (suc r) (sucN (ℕ→N (suc r) n))
  ≡⟨ N→ℕsucN (suc r) (ℕ→N (suc r) n) ⟩
    suc (N→ℕ (suc r) (ℕ→N (suc r) n))
  ≡⟨ cong suc (ℕ→N→ℕ (suc r) n) ⟩
    suc n
  ∎

N≃ℕ : (r : ℕ) → N r ≃ ℕ
N≃ℕ r = isoToEquiv (iso (N→ℕ r) (ℕ→N r) (ℕ→N→ℕ r) (N→ℕ→N r))

N≡ℕ : (r : ℕ) → N r ≡ ℕ
N≡ℕ r = ua (N≃ℕ r)

---- pos approach:

data NPos (n : ℕ) : Type₀ where
  npos1 : NPos n
  x⇀ : DirNum n → NPos n → NPos n

sucNPos : ∀ {n} → NPos n → NPos n
sucNPos {zero} npos1      = x⇀ tt npos1
sucNPos {zero} (x⇀ tt x) = x⇀ tt (sucNPos x)
sucNPos {suc n} npos1     = x⇀ (next (one-n (suc n))) npos1
sucNPos {suc n} (x⇀ d x) with (max? d)
...            | (no _)  = x⇀ (next d) x
...            | (yes _) = x⇀ (zero-n (suc n)) (sucNPos x)

-- some examples for sanity check

2₂ : NPos 1
2₂ = x⇀ (↓ , tt) npos1

3₂ : NPos 1
3₂ = x⇀ (↑ , tt) npos1

4₂ : NPos 1
4₂ = x⇀ (↓ , tt) (x⇀ (↓ , tt) npos1)

2₄ : NPos 2
2₄ = x⇀ (↓ , (↑ , tt)) npos1 -- how does this make sense?

3₄ : NPos 2
3₄ = x⇀ (↑ , (↑ , tt)) npos1 -- how does this make sense?

-- sucnpos1≡x⇀one-n : ∀ {r} → sucNPos npos1 ≡ x⇀ (one-n r) npos1
-- sucnpos1≡x⇀one-n {zero} = refl
-- sucnpos1≡x⇀one-n {suc r} = {!!}

-- sucnposx⇀zero-n≡x⇀one-n : ∀ {r} {p} → sucNPos (x⇀ (zero-n r) p) ≡ x⇀ (one-n r) p
-- sucnposx⇀zero-n≡x⇀one-n {zero} {npos1} = {!!}
-- sucnposx⇀zero-n≡x⇀one-n {zero} {x⇀ x p} = {!!}
-- sucnposx⇀zero-n≡x⇀one-n {suc r} {p} = refl

nPosInd : ∀ {r} {P : NPos r → Type₀} →
            P npos1 →
            ((p : NPos r) → P p → P (sucNPos p)) →
            (p : NPos r) →
            P p
nPosInd {r} {P} h1 hs ps = f ps
  where
     H :  (p : NPos r) → P (x⇀ (zero-n r) p) → P (x⇀ (zero-n r) (sucNPos p))
     --H p hx0p = hs (x⇀ (one-n r) p) (hs (x⇀ (zero-n r) p) hx0p)

     f : (ps : NPos r) → P ps
     f npos1 = h1
     f (x⇀ d ps) with (max? d)
     ... | (no _) = {!nPosInd (hs npos1 h1) H ps!}
     ... | (yes _) = {!hs (x⇀ (zero-n r) ps) (nPosInd (hs npos1 h1) H ps)!}

-- nPosInd {zero} {P} h1 hs ps = f ps
--   where
--   H : (p : NPos zero) → P (x⇀ (zero-n zero) p) → P (x⇀ (zero-n zero) (sucNPos p))
--   H p hx0p = hs (x⇀ tt (x⇀ (zero-n zero) p)) (hs (x⇀ (zero-n zero) p) hx0p)

--   f : (ps : NPos zero) → P ps
--   f npos1 = h1
--   f (x⇀ tt ps) = nPosInd (hs npos1 h1) H ps
-- nPosInd {suc r} {P} h1 hs ps = f ps
--   where
--   H : (p : NPos (suc r)) → P (x⇀ (zero-n (suc r)) p) → P (x⇀ (zero-n (suc r)) (sucNPos p))
--   --H p hx0p = hs (x⇀ (one-n r) p) (hs (x⇀ (zero-n r) p) hx0p)

--   f : (ps : NPos (suc r)) → P ps
--   f npos1 = h1
--   f (x⇀ d ps) = {!!}

NPos→ℕ : ∀ r → NPos r → ℕ
NPos→ℕ zero npos1 = suc zero
NPos→ℕ zero (x⇀ tt x) = suc (NPos→ℕ zero x)
NPos→ℕ (suc r) npos1 = suc zero
NPos→ℕ (suc r) (x⇀ d x) with max? d
... | no _ = sucn (DirNum→ℕ (next d)) (doublesℕ (suc r) (NPos→ℕ (suc r) x))
... | yes _ = sucn (DirNum→ℕ (next d)) (doublesℕ (suc r) (suc (NPos→ℕ (suc r) x)))
-- NPos→ℕ (suc r) (x⇀ d x) =
--   sucn (DirNum→ℕ d) (doublesℕ (suc r) (NPos→ℕ (suc r) x))

NPos→ℕsucNPos : ∀ r → (p : NPos r) → NPos→ℕ r (sucNPos p) ≡ suc (NPos→ℕ r p)
NPos→ℕsucNPos zero npos1 = refl
NPos→ℕsucNPos zero (x⇀ d p) = cong suc (NPos→ℕsucNPos zero p)
NPos→ℕsucNPos (suc r) npos1 = {!!}
    sucn (doubleℕ (DirNum→ℕ (zero-n r))) (doublesℕ r 2)
  ≡⟨ cong (λ y → sucn y (doublesℕ r 2)) (zero-n→0) ⟩
    sucn (doubleℕ zero) (doublesℕ r 2)
  ≡⟨ refl ⟩
    doublesℕ r 2
  ≡⟨ {!!} ⟩ {!!}
NPos→ℕsucNPos (suc r) (x⇀ d p) with max? d
... | no _ = {!!}
... | yes _ = {!!}

-- zero≠NPos→ℕ : ∀ {r} → (p : NPos r) → ¬ (zero ≡ NPos→ℕ r p)
-- zero≠NPos→ℕ {r} p = {!!}

ℕ→NPos : ∀ r → ℕ → NPos r
ℕ→NPos zero zero = npos1
ℕ→NPos zero (suc zero) = npos1
ℕ→NPos zero (suc (suc n)) = sucNPos (ℕ→NPos zero (suc n))
ℕ→NPos (suc r) zero = npos1
ℕ→NPos (suc r) (suc zero) = npos1
ℕ→NPos (suc r) (suc (suc n)) = sucNPos (ℕ→NPos (suc r) (suc n))

lemma : ∀ {r} → (ℕ→NPos r (NPos→ℕ r npos1)) ≡ npos1
lemma {zero} = refl
lemma {suc r} = refl

NPos→ℕ→NPos : ∀ r → (p : NPos r) → ℕ→NPos r (NPos→ℕ r p) ≡ p
NPos→ℕ→NPos r p = nPosInd lemma hs p
  where
  hs : (p : NPos r) → ℕ→NPos r (NPos→ℕ r p) ≡ p → ℕ→NPos r (NPos→ℕ r (sucNPos p)) ≡ (sucNPos p)
  hs p hp =
      ℕ→NPos r (NPos→ℕ r (sucNPos p))
    ≡⟨ {!!} ⟩
      ℕ→NPos r (suc (NPos→ℕ r p))
    ≡⟨ {!!} ⟩
      sucNPos (ℕ→NPos r (NPos→ℕ r p))
    ≡⟨ cong sucNPos hp ⟩
      sucNPos p
    ∎

-- note: the cases for zero and suc r are almost identical
-- (why) does this need to split?
ℕ→NPos→ℕ : ∀ r → (n : ℕ) → NPos→ℕ r (ℕ→NPos r (suc n)) ≡ (suc n)
ℕ→NPos→ℕ zero zero = refl
ℕ→NPos→ℕ zero (suc n) =
      NPos→ℕ zero (sucNPos (ℕ→NPos zero (suc n)))
    ≡⟨ {!!} ⟩
      suc (NPos→ℕ zero (ℕ→NPos zero (suc n)))
    ≡⟨ cong suc (ℕ→NPos→ℕ zero n) ⟩
      suc (suc n)
    ∎
ℕ→NPos→ℕ (suc r) zero = refl
ℕ→NPos→ℕ (suc r) (suc n) =
    NPos→ℕ (suc r) (sucNPos (ℕ→NPos (suc r) (suc n)))
  ≡⟨ {!!} ⟩
    suc (NPos→ℕ (suc r) (ℕ→NPos (suc r) (suc n)))
  ≡⟨ cong suc (ℕ→NPos→ℕ (suc r) n) ⟩
    suc (suc n)
  ∎

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use `Data.Vec.Functional` instead.
------------------------------------------------------------------------

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

-- Disabled to prevent warnings from other Table modules
{-# OPTIONS --warn=noUserWarning #-}

module Data.Table.Properties where

{-# WARNING_ON_IMPORT
"Data.Table.Properties was deprecated in v1.2.
Use Data.Vec.Functional.Properties instead."
#-}

open import Data.Table
open import Data.Table.Relation.Binary.Equality

open import Data.Bool.Base using (true; false; if_then_else_)
open import Data.Nat.Base using (zero; suc)
open import Data.Empty using (⊥-elim)
open import Data.Fin using (Fin; suc; zero; _≟_; punchIn)
import Data.Fin.Properties as FP
open import Data.Fin.Permutation as Perm using (Permutation; _⟨$⟩ʳ_; _⟨$⟩ˡ_)
open import Data.List.Base as L using (List; _∷_; [])
open import Data.List.Relation.Unary.Any using (here; there; index)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.Product as Product using (Σ; ∃; _,_; proj₁; proj₂)
open import Data.Vec.Base as V using (Vec; _∷_; [])
import Data.Vec.Properties as VP
open import Level using (Level)
open import Function.Base using (_∘_; flip)
open import Function.Inverse using (Inverse)
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; _≢_; refl; sym; cong)
open import Relation.Nullary using (does)
open import Relation.Nullary.Decidable using (dec-true; dec-false)
open import Relation.Nullary.Negation using (contradiction)

private
  variable
    a : Level
    A : Set a

------------------------------------------------------------------------
-- select

-- Selecting from any table is the same as selecting from a constant table.

select-const : ∀ {n} (z : A) (i : Fin n) t →
               select z i t ≗ select z i (replicate (lookup t i))
select-const z i t j with does (j ≟ i)
... | true  = refl
... | false = refl

-- Selecting an element from a table then looking it up is the same as looking
-- up the index in the original table

select-lookup : ∀ {n x i} (t : Table A n) →
                lookup (select x i t) i ≡ lookup t i
select-lookup {i = i} t rewrite dec-true (i ≟ i) refl = refl

-- Selecting an element from a table then removing the same element produces a
-- constant table

select-remove : ∀ {n x} i (t : Table A (suc n)) →
                remove i (select x i t) ≗ replicate {n = n} x
select-remove i t j rewrite dec-false (punchIn i j ≟ i) (FP.punchInᵢ≢i _ _)
                          = refl

------------------------------------------------------------------------
-- permute

-- Removing an index 'i' from a table permuted with 'π' is the same as
-- removing the element, then permuting with 'π' minus 'i'.

remove-permute : ∀ {m n} (π : Permutation (suc m) (suc n))
                 i (t : Table A (suc n)) →
                 remove (π ⟨$⟩ˡ i) (permute π t)
                 ≗ permute (Perm.remove (π ⟨$⟩ˡ i) π) (remove i t)
remove-permute π i t j = P.cong (lookup t) (Perm.punchIn-permute′ π i j)

------------------------------------------------------------------------
-- fromList

fromList-∈ : ∀ {xs : List A} (i : Fin (L.length xs)) → lookup (fromList xs) i ∈ xs
fromList-∈ {xs = x ∷ xs} zero    = here refl
fromList-∈ {xs = x ∷ xs} (suc i) = there (fromList-∈ i)

index-fromList-∈ : ∀ {xs : List A} {i} → index (fromList-∈ {xs = xs} i) ≡ i
index-fromList-∈ {xs = x ∷ xs} {zero}  = refl
index-fromList-∈ {xs = x ∷ xs} {suc i} = cong suc index-fromList-∈

fromList-index : ∀ {xs} {x : A} (x∈xs : x ∈ xs) → lookup (fromList xs) (index x∈xs) ≡ x
fromList-index (here px)    = sym px
fromList-index (there x∈xs) = fromList-index x∈xs

------------------------------------------------------------------------
-- There exists an isomorphism between tables and vectors.

↔Vec : ∀ {n} → Inverse (≡-setoid A n) (P.setoid (Vec A n))
↔Vec = record
  { to = record { _⟨$⟩_ = toVec ; cong = VP.tabulate-cong }
  ; from = P.→-to-⟶ fromVec
  ; inverse-of = record
    { left-inverse-of  = VP.lookup∘tabulate ∘ lookup
    ; right-inverse-of = VP.tabulate∘lookup
    }
  }

------------------------------------------------------------------------
-- Other

lookup∈ : ∀ {xs : List A} (i : Fin (L.length xs)) → ∃ λ x → x ∈ xs
lookup∈ i = _ , fromList-∈ i


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.Unit
open import Oscar.Class.Leftunit

module Oscar.Class.Leftunit.ToUnit where

module _
  {𝔞} {𝔄 : Ø 𝔞} {𝔢} {𝔈 : Ø 𝔢} {ℓ}
  {_↦_ : 𝔄 → 𝔄 → Ø ℓ} (let _↦_ = _↦_; infix 4 _↦_)
  {ε : 𝔈}
  {_◃_ : 𝔈 → 𝔄 → 𝔄} (let _◃_ = _◃_; infix 16 _◃_)
  {x : 𝔄}
  ⦃ _ : Leftunit.class _↦_ ε _◃_ x ⦄
  where
  instance
    Leftunit--Unit : Unit.class (ε ◃ x ↦ x)
    Leftunit--Unit .⋆ = leftunit


text:
module Lectures.One where

-- Check background color
-- Check fontsize
-- Ask questions at *any* time

data ⊤ : Set where
  tt : ⊤

data ⊥ : Set where

absurd : ⊥ → {P : Set} → P
absurd ()

-- Introduce most common key bindings
-- C-c C-l     load
-- C-c C-,     show context
-- C-c C-.     show context + type
-- C-c C-SPACE input
-- C-c C-A     auto
-- C-c C-r     refine
-- C-c C-d     type inference
-- C-c C-c     pattern match

-- Briefly introduce syntax
-- Introduce Set 0

modus-ponens : {P Q : Set} → P → (P → Q) → Q
modus-ponens p f = f p

-- Introduce misfix operators

¬_ : Set → Set
¬ P = P → ⊥

contra-elim : {P : Set} → P → ¬ P → ⊥
contra-elim = modus-ponens

-- no-dne : {P : Set} → ¬ ¬ P → P
-- no-dne ¬¬P = {!!}

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

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

_isEven : ℕ → Set
zero isEven = ⊤
suc zero isEven = ⊥
suc (suc n) isEven = n isEven

half : (n : ℕ) → n isEven → ℕ
half zero tt = zero
half (suc (suc n)) p = suc (half n p)

_ : ℕ
_ = half 8 tt

-- Comment on termination checking

-- brexit : ⊥
-- brexit = brexit


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 13-propositional-truncation where

import 12-univalence
open 12-univalence public

-- Section 13 Propositional truncations, the image of a map, and the replacement axiom

-- Section 13.1 Propositional truncations

-- Definition 13.1.1

type-hom-Prop :
  { l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) → UU (l1 ⊔ l2)
type-hom-Prop P Q = type-Prop P → type-Prop Q

hom-Prop :
  { l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU-Prop (l1 ⊔ l2)
hom-Prop P Q =
  pair
    ( type-hom-Prop P Q)
    ( is-prop-function-type (type-Prop P) (type-Prop Q) (is-prop-type-Prop Q))

is-prop-type-hom-Prop :
  { l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) → is-prop (type-hom-Prop P Q)
is-prop-type-hom-Prop P Q =
  is-prop-function-type
    ( type-Prop P)
    ( type-Prop Q)
    ( is-prop-type-Prop Q)

equiv-Prop :
  { l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) → UU (l1 ⊔ l2)
equiv-Prop P Q = (type-Prop P) ≃ (type-Prop Q)

precomp-Prop :
  { l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) →
  (A → type-Prop P) → (Q : UU-Prop l3) →
  (type-hom-Prop P Q) → (A → type-Prop Q)
precomp-Prop P f Q g = g ∘ f

is-propositional-truncation :
  ( l : Level) {l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) →
  ( A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
is-propositional-truncation l P f =
  (Q : UU-Prop l) → is-equiv (precomp-Prop P f Q)

universal-property-propositional-truncation :
  ( l : Level) {l1 l2 : Level} {A : UU l1}
  (P : UU-Prop l2) (f : A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-propositional-truncation l {A = A} P f =
  (Q : UU-Prop l) (g : A → type-Prop Q) →
  is-contr (Σ (type-hom-Prop P Q) (λ h → (h ∘ f) ~  g))

-- Some unnumbered remarks after Definition 13.1.3

universal-property-is-propositional-truncation :
  (l : Level) {l1 l2 : Level} {A : UU l1}
  (P : UU-Prop l2) (f : A → type-Prop P) →
  is-propositional-truncation l P f →
  universal-property-propositional-truncation l P f
universal-property-is-propositional-truncation l P f is-ptr-f Q g =
  is-contr-equiv'
    ( Σ (type-hom-Prop P Q) (λ h → Id (h ∘ f) g))
    ( equiv-tot (λ h → equiv-funext))
    ( is-contr-map-is-equiv (is-ptr-f Q) g)

map-is-propositional-truncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
  ({l : Level} → is-propositional-truncation l P f) →
  (Q : UU-Prop l3) (g : A → type-Prop Q) → type-hom-Prop P Q
map-is-propositional-truncation P f is-ptr-f Q g =
  pr1
    ( center
      ( universal-property-is-propositional-truncation _ P f is-ptr-f Q g))

htpy-is-propositional-truncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
  (is-ptr-f : {l : Level} → is-propositional-truncation l P f) →
  (Q : UU-Prop l3) (g : A → type-Prop Q) →
  ((map-is-propositional-truncation P f is-ptr-f Q g) ∘ f) ~ g
htpy-is-propositional-truncation P f is-ptr-f Q g =
  pr2
    ( center
      ( universal-property-is-propositional-truncation _ P f is-ptr-f Q g))

is-propositional-truncation-universal-property :
  (l : Level) {l1 l2 : Level} {A : UU l1}
  (P : UU-Prop l2) (f : A → type-Prop P) →
  universal-property-propositional-truncation l P f →
  is-propositional-truncation l P f
is-propositional-truncation-universal-property l P f up-f Q =
  is-equiv-is-contr-map
    ( λ g → is-contr-equiv
      ( Σ (type-hom-Prop P Q) (λ h → (h ∘ f) ~ g))
      ( equiv-tot (λ h → equiv-funext))
      ( up-f Q g))

-- Remark 13.1.2

is-propositional-truncation' :
  ( l : Level) {l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) →
  ( A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
is-propositional-truncation' l {A = A} P f =
  (Q : UU-Prop l) → (A → type-Prop Q) → (type-hom-Prop P Q)

is-propositional-truncation-simpl :
  { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2)
  ( f : A → type-Prop P) →
  ( (l : Level) → is-propositional-truncation' l P f) →
  ( (l : Level) → is-propositional-truncation l P f)
is-propositional-truncation-simpl P f up-P l Q =
  is-equiv-is-prop
    ( is-prop-Π (λ x → is-prop-type-Prop Q))
    ( is-prop-Π (λ x → is-prop-type-Prop Q))
    ( up-P l Q)

-- Example 13.1.3

is-propositional-truncation-const-star :
  { l1 : Level} (A : UU-pt l1)
  ( l : Level) → is-propositional-truncation l unit-Prop (const (type-UU-pt A) unit star)
is-propositional-truncation-const-star A =
  is-propositional-truncation-simpl
    ( unit-Prop)
    ( const (type-UU-pt A) unit star)
    ( λ l P f → const unit (type-Prop P) (f (pt-UU-pt A)))

-- Example 13.1.4

is-propositional-truncation-id :
  { l1 : Level} (P : UU-Prop l1) →
  ( l : Level) → is-propositional-truncation l P id
is-propositional-truncation-id P l Q =
  is-equiv-id (type-hom-Prop P Q)

-- Proposition 13.1.5

abstract
  is-equiv-is-equiv-precomp-Prop :
    {l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (f : type-hom-Prop P Q) →
    ((l : Level) (R : UU-Prop l) →
    is-equiv (precomp-Prop Q f R)) → is-equiv f
  is-equiv-is-equiv-precomp-Prop P Q f is-equiv-precomp-f =
    is-equiv-is-equiv-precomp-subuniverse id (λ l → is-prop) P Q f
      is-equiv-precomp-f

triangle-3-for-2-is-ptruncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P')
  (h : type-hom-Prop P P') (H : (h ∘ f) ~ f') →
  {l : Level} (Q : UU-Prop l) →
  ( precomp-Prop P' f' Q) ~
  ( (precomp-Prop P f Q) ∘ (precomp h (type-Prop Q)))
triangle-3-for-2-is-ptruncation P P' f f' h H Q g =
  eq-htpy (λ p → inv (ap g (H p)))

is-equiv-is-ptruncation-is-ptruncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P')
  (h : type-hom-Prop P P') (H : (h ∘ f) ~ f') →
  ((l : Level) → is-propositional-truncation l P f) →
  ((l : Level) → is-propositional-truncation l P' f') →
  is-equiv h
is-equiv-is-ptruncation-is-ptruncation P P' f f' h H is-ptr-P is-ptr-P' =
  is-equiv-is-equiv-precomp-Prop P P' h
    ( λ l Q →
      is-equiv-right-factor
        ( precomp-Prop P' f' Q)
        ( precomp-Prop P f Q)
        ( precomp h (type-Prop Q))
        ( triangle-3-for-2-is-ptruncation P P' f f' h H Q)
        ( is-ptr-P l Q)
        ( is-ptr-P' l Q))

is-ptruncation-is-ptruncation-is-equiv :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P')
  (h : type-hom-Prop P P') (H : (h ∘ f) ~ f') →
  is-equiv h →
  ((l : Level) → is-propositional-truncation l P f) →
  ((l : Level) → is-propositional-truncation l P' f')
is-ptruncation-is-ptruncation-is-equiv P P' f f' h H is-equiv-h is-ptr-f l Q =
  is-equiv-comp
    ( precomp-Prop P' f' Q)
    ( precomp-Prop P f Q)
    ( precomp h (type-Prop Q))
    ( triangle-3-for-2-is-ptruncation P P' f f' h H Q)
    ( is-equiv-precomp-is-equiv h is-equiv-h (type-Prop Q))
    ( is-ptr-f l Q)

is-ptruncation-is-equiv-is-ptruncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P')
  (h : type-hom-Prop P P') (H : (h ∘ f) ~ f') →
  ((l : Level) → is-propositional-truncation l P' f') →
  is-equiv h →
  ((l : Level) → is-propositional-truncation l P f)
is-ptruncation-is-equiv-is-ptruncation P P' f f' h H is-ptr-f' is-equiv-h l Q =
  is-equiv-left-factor
    ( precomp-Prop P' f' Q)
    ( precomp-Prop P f Q)
    ( precomp h (type-Prop Q))
    ( triangle-3-for-2-is-ptruncation P P' f f' h H Q)
    ( is-ptr-f' l Q)
    ( is-equiv-precomp-is-equiv h is-equiv-h (type-Prop Q))

-- Corollary 13.1.6

is-uniquely-unique-propositional-truncation :
  {l1 l2 l3 : Level} {A : UU l1} (P : UU-Prop l2) (P' : UU-Prop l3)
  (f : A → type-Prop P) (f' : A → type-Prop P') →
  ({l : Level} → is-propositional-truncation l P f) →
  ({l : Level} → is-propositional-truncation l P' f') →
  is-contr (Σ (equiv-Prop P P') (λ e → (map-equiv e ∘ f) ~ f'))
is-uniquely-unique-propositional-truncation P P' f f' is-ptr-f is-ptr-f' =
  is-contr-total-Eq-substructure
    ( universal-property-is-propositional-truncation _ P f is-ptr-f P' f')
    ( is-subtype-is-equiv)
    ( map-is-propositional-truncation P f is-ptr-f P' f')
    ( htpy-is-propositional-truncation P f is-ptr-f P' f')
    ( is-equiv-is-ptruncation-is-ptruncation  P P' f f'
      ( map-is-propositional-truncation P f is-ptr-f P' f')
      ( htpy-is-propositional-truncation P f is-ptr-f P' f')
      ( λ l → is-ptr-f)
      ( λ l → is-ptr-f'))

-- Axiom 13.1.8

postulate trunc-Prop : {l : Level} → UU l → UU-Prop l

type-trunc-Prop : {l : Level} → UU l → UU l
type-trunc-Prop A = pr1 (trunc-Prop A)

is-prop-type-trunc-Prop : {l : Level} (A : UU l) → is-prop (type-trunc-Prop A)
is-prop-type-trunc-Prop A = pr2 (trunc-Prop A)

postulate unit-trunc-Prop : {l : Level} (A : UU l) → A → type-Prop (trunc-Prop A)

postulate is-propositional-truncation-trunc-Prop : {l1 l2 : Level} (A : UU l1) → is-propositional-truncation l2 (trunc-Prop A) (unit-trunc-Prop A)

universal-property-trunc-Prop : {l1 l2 : Level} (A : UU l1) →
  universal-property-propositional-truncation l2
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
universal-property-trunc-Prop A =
  universal-property-is-propositional-truncation _
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
    ( is-propositional-truncation-trunc-Prop A)

map-universal-property-trunc-Prop :
  {l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) →
  (A → type-Prop P) → type-hom-Prop (trunc-Prop A) P
map-universal-property-trunc-Prop {A = A} P f =
  map-is-propositional-truncation
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
    ( is-propositional-truncation-trunc-Prop A)
    ( P)
    ( f)

-- Proposition 13.1.9

unique-functor-trunc-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  is-contr
    ( Σ ( type-hom-Prop (trunc-Prop A) (trunc-Prop B))
        ( λ h → (h ∘ (unit-trunc-Prop A)) ~ ((unit-trunc-Prop B) ∘ f)))
unique-functor-trunc-Prop {l1} {l2} {A} {B} f =
  universal-property-trunc-Prop A (trunc-Prop B) ((unit-trunc-Prop B) ∘ f)

functor-trunc-Prop :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  (A → B) → type-hom-Prop (trunc-Prop A) (trunc-Prop B)
functor-trunc-Prop f =
  pr1 (center (unique-functor-trunc-Prop f))

htpy-functor-trunc-Prop :
  { l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  ( (functor-trunc-Prop f) ∘ (unit-trunc-Prop A)) ~ ((unit-trunc-Prop B) ∘ f)
htpy-functor-trunc-Prop f =
  pr2 (center (unique-functor-trunc-Prop f))

htpy-uniqueness-functor-trunc-Prop :
  { l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) →
  ( h : type-hom-Prop (trunc-Prop A) (trunc-Prop B)) →
  ( ( h ∘ (unit-trunc-Prop A)) ~ ((unit-trunc-Prop B) ∘ f)) →
  (functor-trunc-Prop f) ~ h
htpy-uniqueness-functor-trunc-Prop f h H =
  htpy-eq (ap pr1 (contraction (unique-functor-trunc-Prop f) (pair h H)))

id-functor-trunc-Prop :
  { l1 : Level} {A : UU l1} → functor-trunc-Prop (id {A = A}) ~ id
id-functor-trunc-Prop {l1} {A} =
  htpy-uniqueness-functor-trunc-Prop id id refl-htpy

comp-functor-trunc-Prop :
  { l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  ( g : B → C) (f : A → B) →
  ( functor-trunc-Prop (g ∘ f)) ~
  ( (functor-trunc-Prop g) ∘ (functor-trunc-Prop f))
comp-functor-trunc-Prop g f =
  htpy-uniqueness-functor-trunc-Prop
    ( g ∘ f)
    ( (functor-trunc-Prop g) ∘ (functor-trunc-Prop f))
    ( ( (functor-trunc-Prop g) ·l (htpy-functor-trunc-Prop f)) ∙h
      ( ( htpy-functor-trunc-Prop g) ·r f))

-- Section 13.2 Propositional truncations as higher inductive types

-- Definition 13.2.1

case-paths-induction-principle-propositional-truncation :
  { l : Level} {l1 l2 : Level} {A : UU l1}
  ( P : UU-Prop l2) (α : (p q : type-Prop P) → Id p q) (f : A → type-Prop P) →
  ( B : type-Prop P → UU l) → UU (l ⊔ l2)
case-paths-induction-principle-propositional-truncation P α f B =
  (p q : type-Prop P) (x : B p) (y : B q) → Id (tr B (α p q) x) y

induction-principle-propositional-truncation :
  (l : Level) {l1 l2 : Level} {A : UU l1}
  (P : UU-Prop l2) (α : (p q : type-Prop P) → Id p q) (f : A → type-Prop P) →
  UU (lsuc l ⊔ l1 ⊔ l2)
induction-principle-propositional-truncation l {l1} {l2} {A} P α f =
  ( B : type-Prop P → UU l) →
  ( g : (x : A) → (B (f x))) →
  ( β : case-paths-induction-principle-propositional-truncation P α f B) →
  Σ ((p : type-Prop P) → B p) (λ h → (x : A) → Id (h (f x)) (g x))

-- Lemma 13.2.2

is-prop-case-paths-induction-principle-propositional-truncation :
  { l : Level} {l1 l2 : Level} {A : UU l1}
  ( P : UU-Prop l2) (α : (p q : type-Prop P) → Id p q) (f : A → type-Prop P) →
  ( B : type-Prop P → UU l) →
  case-paths-induction-principle-propositional-truncation P α f B →
  ( p : type-Prop P) → is-prop (B p)
is-prop-case-paths-induction-principle-propositional-truncation P α f B β p =
  is-prop-is-contr-if-inh (λ x → pair (tr B (α p p) x) (β p p x))

case-paths-induction-principle-propositional-truncation-is-prop :
  { l : Level} {l1 l2 : Level} {A : UU l1}
  ( P : UU-Prop l2) (α : (p q : type-Prop P) → Id p q) (f : A → type-Prop P) →
  ( B : type-Prop P → UU l) →
  ( (p : type-Prop P) → is-prop (B p)) →
  case-paths-induction-principle-propositional-truncation P α f B
case-paths-induction-principle-propositional-truncation-is-prop
  P α f B is-prop-B p q x y =
  is-prop'-is-prop (is-prop-B q) (tr B (α p q) x) y

-- Definition 13.2.3

dependent-universal-property-propositional-truncation :
  ( l : Level) {l1 l2 : Level} {A : UU l1}
  ( P : UU-Prop l2) (f : A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2)
dependent-universal-property-propositional-truncation l {l1} {l2} {A} P f =
  ( Q : type-Prop P → UU-Prop l) → is-equiv (precomp-Π f (type-Prop ∘ Q))

-- Theorem 13.2.4

abstract
  dependent-universal-property-is-propositional-truncation :
    { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
    ( {l : Level} → is-propositional-truncation l P f) →
    ( {l : Level} → dependent-universal-property-propositional-truncation l P f)
  dependent-universal-property-is-propositional-truncation
    {l1} {l2} {A} P f is-ptr-f Q =
    is-fiberwise-equiv-is-equiv-toto-is-equiv-base-map
      ( λ (g : A → type-Prop P) → (x : A) → type-Prop (Q (g x)))
      ( precomp f (type-Prop P))
      ( λ h → precomp-Π f (λ p → type-Prop (Q (h p))))
      ( is-ptr-f P)
      ( is-equiv-top-is-equiv-bottom-square
        ( inv-choice-∞
          { C = λ (x : type-Prop P) (p : type-Prop P) → type-Prop (Q p)})
        ( inv-choice-∞
          { C = λ (x : A) (p : type-Prop P) → type-Prop (Q p)})
        ( toto
          ( λ (g : A → type-Prop P) → (x : A) → type-Prop (Q (g x)))
          ( precomp f (type-Prop P))
          ( λ h → precomp-Π f (λ p → type-Prop (Q (h p)))))
        ( precomp f (Σ (type-Prop P) (λ p → type-Prop (Q p))))
        ( ind-Σ (λ h h' → refl))
        ( is-equiv-inv-choice-∞)
        ( is-equiv-inv-choice-∞)
        ( is-ptr-f (Σ-Prop P Q)))
      ( id {A = type-Prop P})

dependent-universal-property-trunc-Prop :
  {l l1 : Level} (A : UU l1) →
  dependent-universal-property-propositional-truncation l
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
dependent-universal-property-trunc-Prop A =
  dependent-universal-property-is-propositional-truncation
    ( trunc-Prop A)
    ( unit-trunc-Prop A)
    ( is-propositional-truncation-trunc-Prop A)

abstract
  is-propositional-truncation-dependent-universal-property :
    { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
    ( {l : Level} →
      dependent-universal-property-propositional-truncation l P f) →
    ( {l : Level} → is-propositional-truncation l P f)
  is-propositional-truncation-dependent-universal-property P f dup-f Q =
    dup-f (λ p → Q)

abstract
  induction-principle-dependent-universal-property-propositional-truncation :
    { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
    ( {l : Level} →
      dependent-universal-property-propositional-truncation l P f) →
    ( {l : Level} → induction-principle-propositional-truncation l P
      ( is-prop'-is-prop (is-prop-type-Prop P)) f)
  induction-principle-dependent-universal-property-propositional-truncation
    P f dup-f B g α =
    tot
      ( λ h → htpy-eq)
      ( center
        ( is-contr-map-is-equiv
          ( dup-f
            ( λ p →
              pair
                ( B p)
                ( is-prop-case-paths-induction-principle-propositional-truncation
                  ( P)
                  ( is-prop'-is-prop (is-prop-type-Prop P))
                  f B α p)))
          ( g)))

abstract
  dependent-universal-property-induction-principle-propositional-truncation :
    { l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P) →
    ( {l : Level} → induction-principle-propositional-truncation l P
      ( is-prop'-is-prop (is-prop-type-Prop P)) f) →
    ( {l : Level} → dependent-universal-property-propositional-truncation l P f)
  dependent-universal-property-induction-principle-propositional-truncation
    P f ind-f Q =
    is-equiv-is-prop
      ( is-prop-Π (λ p → is-prop-type-Prop (Q p)))
      ( is-prop-Π (λ a → is-prop-type-Prop (Q (f a))))
      ( λ g →
        pr1
          ( ind-f
            ( λ p → type-Prop (Q p))
            ( g)
            ( case-paths-induction-principle-propositional-truncation-is-prop
              ( P)
              ( is-prop'-is-prop (is-prop-type-Prop P))
              ( f)
              ( λ p → type-Prop (Q p))
              ( λ p → is-prop-type-Prop (Q p)))))

-- Exercises

-- Exercise 13.1

is-propositional-truncation-retract :
  {l l1 l2 : Level} {A : UU l1} (P : UU-Prop l2) →
  (R : (type-Prop P) retract-of A) →
  is-propositional-truncation l P (retraction-retract-of R)
is-propositional-truncation-retract {A = A} P R Q =
  is-equiv-is-prop
    ( is-prop-function-type
      ( type-Prop P)
      ( type-Prop Q)
      ( is-prop-type-Prop Q))
    ( is-prop-function-type
      ( A)
      ( type-Prop Q)
      ( is-prop-type-Prop Q))
    ( λ g → g ∘ (section-retract-of R))

-- Exercise 13.2

is-propositional-truncation-prod :
  {l1 l2 l3 l4 : Level}
  {A : UU l1} (P : UU-Prop l2) (f : A → type-Prop P)
  {A' : UU l3} (P' : UU-Prop l4) (f' : A' → type-Prop P') →
  ({l : Level} → is-propositional-truncation l P f) →
  ({l : Level} → is-propositional-truncation l P' f') →
  {l : Level} → is-propositional-truncation l (prod-Prop P P') (functor-prod f f')
is-propositional-truncation-prod P f P' f' is-ptr-f is-ptr-f' Q =
  is-equiv-top-is-equiv-bottom-square
    ( ev-pair)
    ( ev-pair)
    ( precomp (functor-prod f f') (type-Prop Q))
    ( λ h a a' → h (f a) (f' a'))
    ( refl-htpy)
    ( is-equiv-ev-pair)
    ( is-equiv-ev-pair)
    ( is-equiv-comp'
      ( λ h a a' → h a (f' a'))
      ( λ h a p' → h (f a) p')
      ( is-ptr-f (pair (type-hom-Prop P' Q) (is-prop-type-hom-Prop P' Q)))
      ( is-equiv-postcomp-Π
        ( λ a g a' → g (f' a'))
        ( λ a → is-ptr-f' Q)))

equiv-prod-trunc-Prop :
  {l1 l2 : Level} (A : UU l1) (A' : UU l2) →
  equiv-Prop (trunc-Prop (A × A')) (prod-Prop (trunc-Prop A) (trunc-Prop A'))
equiv-prod-trunc-Prop A A' =
  pr1
    ( center
      ( is-uniquely-unique-propositional-truncation
        ( trunc-Prop (A × A'))
        ( prod-Prop (trunc-Prop A) (trunc-Prop A'))
        ( unit-trunc-Prop (A × A'))
        ( functor-prod (unit-trunc-Prop A) (unit-trunc-Prop A'))
        ( is-propositional-truncation-trunc-Prop (A × A'))
        ( is-propositional-truncation-prod
          ( trunc-Prop A)
          ( unit-trunc-Prop A)
          ( trunc-Prop A')
          ( unit-trunc-Prop A')
          ( is-propositional-truncation-trunc-Prop A)
          ( is-propositional-truncation-trunc-Prop A'))))

-- Exercise 13.3

-- Exercise 13.3(a)

conj-Prop = prod-Prop

disj-Prop :
  {l1 l2 : Level} → UU-Prop l1 → UU-Prop l2 → UU-Prop (l1 ⊔ l2)
disj-Prop P Q = trunc-Prop (coprod (type-Prop P) (type-Prop Q))

inl-disj-Prop :
  {l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) →
  type-hom-Prop P (disj-Prop P Q)
inl-disj-Prop P Q =
  (unit-trunc-Prop (coprod (type-Prop P) (type-Prop Q))) ∘ inl

inr-disj-Prop :
  {l1 l2 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) →
  type-hom-Prop Q (disj-Prop P Q)
inr-disj-Prop P Q =
  (unit-trunc-Prop (coprod (type-Prop P) (type-Prop Q))) ∘ inr

-- Exercise 13.3(b)

ev-disj-Prop :
  {l1 l2 l3 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (R : UU-Prop l3) →
  type-hom-Prop
    ( hom-Prop (disj-Prop P Q) R)
    ( conj-Prop (hom-Prop P R) (hom-Prop Q R))
ev-disj-Prop P Q R h =
  pair (h ∘ (inl-disj-Prop P Q)) (h ∘ (inr-disj-Prop P Q))

inv-ev-disj-Prop :
  {l1 l2 l3 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (R : UU-Prop l3) →
  type-hom-Prop
    ( conj-Prop (hom-Prop P R) (hom-Prop Q R))
    ( hom-Prop (disj-Prop P Q) R)
inv-ev-disj-Prop P Q R (pair f g) =
  map-universal-property-trunc-Prop R (ind-coprod (λ t → type-Prop R) f g)

is-equiv-ev-disj-Prop :
  {l1 l2 l3 : Level} (P : UU-Prop l1) (Q : UU-Prop l2) (R : UU-Prop l3) →
  is-equiv (ev-disj-Prop P Q R)
is-equiv-ev-disj-Prop P Q R =
  is-equiv-is-prop
    ( is-prop-type-Prop (hom-Prop (disj-Prop P Q) R))
    ( is-prop-type-Prop (conj-Prop (hom-Prop P R) (hom-Prop Q R)))
    ( inv-ev-disj-Prop P Q R)

-- Exercise 13.5

{-
impredicative-trunc-Prop :
  {l : Level} → UU l → UU-Prop (lsuc l)
impredicative-trunc-Prop {l} A =
  (P : UU-Prop l) → (A → type-Prop P) → type-Prop P
-}

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for reasoning with a partial setoid
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Reasoning.PartialSetoid
  {s₁ s₂} (S : PartialSetoid s₁ s₂) where

open PartialSetoid S
import Relation.Binary.Reasoning.Base.Partial _≈_ trans as Base

------------------------------------------------------------------------
-- Re-export the contents of the base module

open Base public
  hiding (step-∼)

------------------------------------------------------------------------
-- Additional reasoning combinators

infixr 2 step-≈ step-≈˘

-- A step using an equality

step-≈ = Base.step-∼
syntax step-≈ x y≈z x≈y = x ≈⟨ x≈y ⟩ y≈z

-- A step using a symmetric equality

step-≈˘ : ∀ x {y z} → y IsRelatedTo z → y ≈ x → x IsRelatedTo z
step-≈˘ x y∼z y≈x = x ≈⟨ sym y≈x ⟩ y∼z
syntax step-≈˘ x y≈z y≈x = x ≈˘⟨ y≈x ⟩ y≈z


text:
module Issue1232.Fin where

data Fin : Set where
  zero : Fin


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.ConsensusTypes.Vote               as Vote
import      LibraBFT.Impl.Consensus.ConsensusTypes.TimeoutCertificate as TimeoutCertificate
open import LibraBFT.Impl.OBM.Rust.RustTypes
import      LibraBFT.Impl.Types.CryptoProxies                         as CryptoProxies
import      LibraBFT.Impl.Types.LedgerInfoWithSignatures              as LedgerInfoWithSignatures
import      LibraBFT.Impl.Types.ValidatorVerifier                     as ValidatorVerifier
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import Optics.All
open import Util.Hash
import      Util.KVMap                                                as Map
open import Util.Prelude

module LibraBFT.Impl.Consensus.PendingVotes where

insertVoteM : Vote → ValidatorVerifier → LBFT VoteReceptionResult
insertVoteM vote vv = do
  let liDigest = hashLI (vote ^∙ vLedgerInfo)
  atv          ← use (lPendingVotes ∙ pvAuthorToVote)
  caseMD Map.lookup (vote ^∙ vAuthor) atv of λ where
    (just previouslySeenVote) →
      ifD liDigest ≟Hash (hashLI (previouslySeenVote ^∙ vLedgerInfo))
      then (do
        let newTimeoutVote = Vote.isTimeout vote ∧ not (Vote.isTimeout previouslySeenVote)
        if not newTimeoutVote
          then pure DuplicateVote
          else continue1 liDigest)
      else
        pure EquivocateVote
    nothing →
      continue1 liDigest

 where

  continue2 : U64 → LBFT VoteReceptionResult

  continue1 : HashValue → LBFT VoteReceptionResult
  continue1 liDigest = do
    pv            ← use lPendingVotes
    lPendingVotes ∙ pvAuthorToVote %= Map.kvm-insert-Haskell (vote ^∙ vAuthor) vote
    let liWithSig = CryptoProxies.addToLi (vote ^∙ vAuthor) (vote ^∙ vSignature)
                      (fromMaybe (LedgerInfoWithSignatures∙new (vote ^∙ vLedgerInfo) Map.empty)
                                 (Map.lookup liDigest (pv ^∙ pvLiDigestToVotes)))
    lPendingVotes ∙ pvLiDigestToVotes %= Map.kvm-insert-Haskell liDigest liWithSig
    case⊎D ValidatorVerifier.checkVotingPower vv (Map.kvm-keys (liWithSig ^∙ liwsSignatures)) of λ where
      (Right unit) →
        pure (NewQuorumCertificate (QuorumCert∙new (vote ^∙ vVoteData) liWithSig))
      (Left (ErrVerify (TooLittleVotingPower votingPower _))) →
        continue2 votingPower
      (Left _) →
        pure VRR_TODO

  continue2 qcVotingPower =
    caseMD vote ^∙ vTimeoutSignature of λ where
      (just timeoutSignature) → do
        pv            ← use lPendingVotes
        let partialTc = TimeoutCertificate.addSignature (vote ^∙ vAuthor) timeoutSignature
                          (fromMaybe (TimeoutCertificate∙new (Vote.timeout vote))
                                     (pv ^∙ pvMaybePartialTC))
        lPendingVotes ∙ pvMaybePartialTC %= const (just partialTc)
        case⊎D ValidatorVerifier.checkVotingPower vv (Map.kvm-keys (partialTc ^∙ tcSignatures)) of λ where
          (Right unit) →
            pure (NewTimeoutCertificate partialTc)
          (Left (ErrVerify (TooLittleVotingPower votingPower _))) →
            pure (TCVoteAdded votingPower)
          (Left _) →
            pure VRR_TODO
      nothing →
        pure (QCVoteAdded qcVotingPower)


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

module Polynomial.Simple.AlmostCommutativeRing where

import Algebra.Solver.Ring.AlmostCommutativeRing as Complex
open import Level
open import Relation.Binary
open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties
import Algebra.Morphism as Morphism
open import Function
open import Level
open import Data.Maybe as Maybe using (Maybe; just; nothing)

record IsAlmostCommutativeRing
         {a ℓ} {A : Set a} (_≈_ : Rel A ℓ)
         (_+_ _*_ : A → A → A) (-_ : A → A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
    -‿cong                : -_ Preserves _≈_ ⟶ _≈_
    -‿*-distribˡ          : ∀ x y → ((- x) * y)     ≈ (- (x * y))
    -‿+-comm              : ∀ x y → ((- x) + (- y)) ≈ (- (x + y))

  open IsCommutativeSemiring isCommutativeSemiring public

import Polynomial.Exponentiation as Exp

record AlmostCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  infixr 8 _^_
  field
    Carrier                 : Set c
    _≈_                     : Rel Carrier ℓ
    _+_                     : Op₂ Carrier
    _*_                     : Op₂ Carrier
    -_                      : Op₁ Carrier
    0#                      : Carrier
    0≟_                     : (x : Carrier) → Maybe (0# ≈ x)
    1#                      : Carrier
    isAlmostCommutativeRing :
      IsAlmostCommutativeRing _≈_ _+_ _*_ -_ 0# 1#

  open IsAlmostCommutativeRing isAlmostCommutativeRing hiding (refl) public
  open import Data.Nat as ℕ using (ℕ)

  commutativeSemiring : CommutativeSemiring _ _
  commutativeSemiring =
    record { isCommutativeSemiring = isCommutativeSemiring }

  open CommutativeSemiring commutativeSemiring public
         using ( +-semigroup; +-monoid; +-commutativeMonoid
               ; *-semigroup; *-monoid; *-commutativeMonoid
               ; semiring
               )

  rawRing : RawRing _ _
  rawRing = record
    { Carrier = Carrier
    ; _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; -_  = -_
    ; 0#  = 0#
    ; 1#  = 1#
    }

  _^_ : Carrier → ℕ → Carrier
  _^_ = Exp._^_ rawRing
  {-# NOINLINE _^_ #-}

  refl : ∀ {x} → x ≈ x
  refl = IsAlmostCommutativeRing.refl isAlmostCommutativeRing

flipped : ∀ {c ℓ} → AlmostCommutativeRing c ℓ → AlmostCommutativeRing c ℓ
flipped rng = record
  { Carrier = Carrier
  ; _≈_ = _≈_
  ; _+_ = flip _+_
  ; _*_ = flip _*_
  ; -_ = -_
  ; 0# = 0#
  ; 0≟_ = 0≟_
  ; 1# = 1#
  ; isAlmostCommutativeRing = record
    { -‿cong = -‿cong
    ; -‿*-distribˡ = λ x y → *-comm y (- x) ⟨ trans ⟩ (-‿*-distribˡ x y ⟨ trans ⟩ -‿cong (*-comm x y))
    ; -‿+-comm = λ x y → -‿+-comm y x
    ; isCommutativeSemiring = record
      { +-isCommutativeMonoid = record
        { isSemigroup = record
          { isMagma = record
            { isEquivalence = isEquivalence
            ; ∙-cong = flip (+-cong )
            }
          ; assoc = λ x y z → sym (+-assoc z y x)
          }
        ; identityˡ = +-identityʳ
        ; comm = λ x y → +-comm y x
        }
      ; *-isCommutativeMonoid = record
        { isSemigroup = record
          { isMagma = record
            { isEquivalence = isEquivalence
            ; ∙-cong = flip (*-cong )
            }
          ; assoc = λ x y z → sym (*-assoc z y x)
          }
          ; identityˡ = *-identityʳ
          ; comm = λ x y → *-comm y x
        }
      ; distribʳ = λ x y z → distribˡ _ _ _
      ; zeroˡ = zeroʳ
      }
    }
  } where open AlmostCommutativeRing rng

record _-Raw-AlmostCommutative⟶_
         {c r₁ r₂ r₃}
         (From : RawRing c r₁)
         (To : AlmostCommutativeRing r₂ r₃) : Set (c ⊔ r₁ ⊔ r₂ ⊔ r₃) where
  private
    module F = RawRing From
    module T = AlmostCommutativeRing To
  open Morphism.Definitions F.Carrier T.Carrier T._≈_
  field
    ⟦_⟧    : Morphism
    +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
    *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
    -‿homo : Homomorphic₁ ⟦_⟧ F.-_  T.-_
    0-homo : Homomorphic₀ ⟦_⟧ F.0#  T.0#
    1-homo : Homomorphic₀ ⟦_⟧ F.1#  T.1#

-raw-almostCommutative⟶
  : ∀ {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂) →
    AlmostCommutativeRing.rawRing R -Raw-AlmostCommutative⟶ R
-raw-almostCommutative⟶ R = record
  { ⟦_⟧    = id
  ; +-homo = λ _ _ → refl
  ; *-homo = λ _ _ → refl
  ; -‿homo = λ _ → refl
  ; 0-homo = refl
  ; 1-homo = refl
  }
  where open AlmostCommutativeRing R

-- A homomorphism induces a notion of equivalence on the raw ring.

Induced-equivalence :
  ∀ {c₁ c₂ ℓ₁ ℓ₂} {Coeff : RawRing c₁ ℓ₁} {R : AlmostCommutativeRing c₂ ℓ₂} →
  Coeff -Raw-AlmostCommutative⟶ R → Rel (RawRing.Carrier Coeff) ℓ₂
Induced-equivalence {R = R} morphism a b = ⟦ a ⟧ ≈ ⟦ b ⟧
  where
  open AlmostCommutativeRing R
  open _-Raw-AlmostCommutative⟶_ morphism

------------------------------------------------------------------------
-- Conversions

-- Commutative rings are almost commutative rings.

fromCommutativeRing : ∀ {r₁ r₂} → (CR : CommutativeRing r₁ r₂) → (∀ x → Maybe ((CommutativeRing._≈_ CR) (CommutativeRing.0# CR) x)) → AlmostCommutativeRing _ _
fromCommutativeRing CR 0≟_ = record
  { isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿cong                = -‿cong
      ; -‿*-distribˡ          = -‿*-distribˡ
      ; -‿+-comm              = ⁻¹-∙-comm
      }
  ; 0≟_ = 0≟_
  }
  where
  open CommutativeRing CR
  import Algebra.Properties.Ring as R; open R ring
  import Algebra.Properties.AbelianGroup as AG; open AG +-abelianGroup

fromCommutativeSemiring : ∀ {r₁ r₂} → (CS : CommutativeSemiring r₁ r₂) → (∀ x → Maybe ((CommutativeSemiring._≈_ CS) (CommutativeSemiring.0# CS) x)) → AlmostCommutativeRing _ _
fromCommutativeSemiring CS 0≟_ = record
  { -_                      = id
  ; isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿cong                = id
      ; -‿*-distribˡ          = λ _ _ → refl
      ; -‿+-comm              = λ _ _ → refl
      }
  ; 0≟_ = 0≟_
  }
  where open CommutativeSemiring CS

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


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

open import lib.Basics
open import lib.NType2
open import lib.types.Bool
open import lib.types.Empty
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Sigma

{-
This file contains various lemmas that rely on lib.types.Paths or
functional extensionality for pointed maps.
-}

module lib.types.Pointed where

{- Sequences of pointed maps and paths between their compositions -}

infixr 80 _◃⊙∘_
data ⊙FunctionSeq {i} : Ptd i → Ptd i → Type (lsucc i) where
  ⊙idf-seq : {X : Ptd i} → ⊙FunctionSeq X X
  _◃⊙∘_ : {X Y Z : Ptd i} (g : Y ⊙→ Z) (fs : ⊙FunctionSeq X Y) → ⊙FunctionSeq X Z

infix 30 _⊙–→_
_⊙–→_ = ⊙FunctionSeq

infix 90 _◃⊙idf
_◃⊙idf : ∀ {i} {X Y : Ptd i} → (X ⊙→ Y) → X ⊙–→ Y
_◃⊙idf fs = fs ◃⊙∘ ⊙idf-seq

⊙compose : ∀ {i} {X Y : Ptd i} → (X ⊙–→ Y) → X ⊙→ Y
⊙compose ⊙idf-seq = ⊙idf _
⊙compose (g ◃⊙∘ fs) = g ⊙∘ ⊙compose fs

record _=⊙∘_ {i} {X Y : Ptd i} (fs gs : X ⊙–→ Y) : Type i where
  constructor =⊙∘-in
  field
    =⊙∘-out : ⊙compose fs == ⊙compose gs
open _=⊙∘_ public

{- Pointed maps -}

⊙→-level : ∀ {i j} (X : Ptd i) (Y : Ptd j)
  {n : ℕ₋₂}
  → has-level n (de⊙ Y)
  → has-level n (X ⊙→ Y)
⊙→-level X Y Y-level =
  Σ-level
    (Π-level (λ _ → Y-level))
    (λ f' → =-preserves-level Y-level)

⊙app= : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : X ⊙→ Y}
  → f == g → f ⊙∼ g
⊙app= {X = X} {Y = Y} p =
  app= (fst= p) , ↓-ap-in (_== pt Y) (λ u → u (pt X)) (snd= p)

-- function extensionality for pointed maps
⊙λ= : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : X ⊙→ Y}
  → f ⊙∼ g → f == g
⊙λ= {g = g} (p , α) = pair= (λ= p)
  (↓-app=cst-in (↓-idf=cst-out α ∙ ap (_∙ snd g) (! (app=-β p _))))

⊙λ=' : ∀ {i j} {X : Ptd i} {Y : Ptd j} {f g : X ⊙→ Y}
  (p : fst f ∼ fst g)
  (α : snd f == snd g [ (λ y → y == pt Y) ↓ p (pt X) ])
  → f == g
⊙λ=' {g = g} = curry ⊙λ=

-- associativity of pointed maps
⊙∘-assoc-pt : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
  {a₁ a₂ : A} (f : A → B) {b : B} (g : B → C) {c : C}
  (p : a₁ == a₂) (q : f a₂ == b) (r : g b == c)
  → ⊙∘-pt (g ∘ f) p (⊙∘-pt g q r) == ⊙∘-pt g (⊙∘-pt f p q) r
⊙∘-assoc-pt _ _ idp _ _ = idp

⊙∘-assoc : ∀ {i j k l} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {W : Ptd l}
  (h : Z ⊙→ W) (g : Y ⊙→ Z) (f : X ⊙→ Y)
  → ((h ⊙∘ g) ⊙∘ f) ⊙∼ (h ⊙∘ (g ⊙∘ f))
⊙∘-assoc (h , hpt) (g , gpt) (f , fpt) = (λ _ → idp) , ⊙∘-assoc-pt g h fpt gpt hpt

⊙∘-cst-l : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → (f : X ⊙→ Y) → (⊙cst :> (Y ⊙→ Z)) ⊙∘ f ⊙∼ ⊙cst
⊙∘-cst-l {Z = Z} f = (λ _ → idp) , ap (_∙ idp) (ap-cst (pt Z) (snd f))

⊙∘-cst-r : ∀ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k}
  → (f : Y ⊙→ Z) → f ⊙∘ (⊙cst :> (X ⊙→ Y)) ⊙∼ ⊙cst
⊙∘-cst-r {X = X} f = (λ _ → snd f) , ↓-idf=cst-in' idp

private
  ⊙coe-pt : ∀ {i} {X Y : Ptd i} (p : X == Y)
    → coe (ap de⊙ p) (pt X) == pt Y
  ⊙coe-pt idp = idp

⊙coe : ∀ {i} {X Y : Ptd i}
  → X == Y → X ⊙→ Y
⊙coe p = coe (ap de⊙ p) , ⊙coe-pt p

⊙coe-equiv : ∀ {i} {X Y : Ptd i}
  → X == Y → X ⊙≃ Y
⊙coe-equiv p = ⊙coe p , snd (coe-equiv (ap de⊙ p))

transport-post⊙∘ : ∀ {i} {j} (X : Ptd i) {Y Z : Ptd j} (p : Y == Z)
  (f : X ⊙→ Y)
  → transport (X ⊙→_) p f == ⊙coe p ⊙∘ f
transport-post⊙∘ X p@idp f = ! (⊙λ= (⊙∘-unit-l f))

⊙coe-∙ : ∀ {i} {X Y Z : Ptd i} (p : X == Y) (q : Y == Z)
  → ⊙coe (p ∙ q) ◃⊙idf =⊙∘ ⊙coe q ◃⊙∘ ⊙coe p ◃⊙idf
⊙coe-∙ p@idp q = =⊙∘-in idp

private
  ⊙coe'-pt : ∀ {i} {X Y : Ptd i} (p : de⊙ X == de⊙ Y) (q : pt X == pt Y [ idf _ ↓ p ])
    → coe p (pt X) == pt Y
  ⊙coe'-pt p@idp q = q

⊙coe' : ∀ {i} {X Y : Ptd i} (p : de⊙ X == de⊙ Y) (q : pt X == pt Y [ idf _ ↓ p ])
  → X ⊙→ Y
⊙coe' p q = coe p , ⊙coe'-pt p q

private
  ⊙transport-pt : ∀ {i j} {A : Type i} (B : A → Ptd j) {x y : A} (p : x == y)
    → transport (de⊙ ∘ B) p (pt (B x)) == pt (B y)
  ⊙transport-pt B idp = idp

⊙transport : ∀ {i j} {A : Type i} (B : A → Ptd j) {x y : A} (p : x == y)
  → (B x ⊙→ B y)
⊙transport B p = transport (de⊙ ∘ B) p , ⊙transport-pt B p

⊙transport-∙ : ∀ {i j} {A : Type i} (B : A → Ptd j)
  {x y z : A} (p : x == y) (q : y == z)
  → ⊙transport B (p ∙ q) ◃⊙idf =⊙∘ ⊙transport B q ◃⊙∘ ⊙transport B p ◃⊙idf
⊙transport-∙ B p@idp q = =⊙∘-in idp

⊙transport-⊙coe : ∀ {i j} {A : Type i} (B : A → Ptd j) {x y : A} (p : x == y)
  → ⊙transport B p == ⊙coe (ap B p)
⊙transport-⊙coe B p@idp = idp

⊙transport-natural : ∀ {i j k} {A : Type i} {B : A → Ptd j} {C : A → Ptd k}
  {x y : A} (p : x == y)
  (h : ∀ a → B a ⊙→ C a)
  → h y ⊙∘ ⊙transport B p == ⊙transport C p ⊙∘ h x
⊙transport-natural p@idp h = ! (⊙λ= (⊙∘-unit-l (h _)))

{- This requires that B and C have the same universe level -}
⊙transport-natural-=⊙∘ : ∀ {i j} {A : Type i} {B C : A → Ptd j}
  {x y : A} (p : x == y)
  (h : ∀ a → B a ⊙→ C a)
  → h y ◃⊙∘ ⊙transport B p ◃⊙idf =⊙∘ ⊙transport C p ◃⊙∘ h x ◃⊙idf
⊙transport-natural-=⊙∘ p h = =⊙∘-in (⊙transport-natural p h)

{- Pointed equivalences -}

-- Extracting data from an pointed equivalence
module _ {i j} {X : Ptd i} {Y : Ptd j} (⊙e : X ⊙≃ Y) where

  ⊙≃-to-≃ : de⊙ X ≃ de⊙ Y
  ⊙≃-to-≃ = fst (fst ⊙e) , snd ⊙e

  ⊙–> : X ⊙→ Y
  ⊙–> = fst ⊙e

  ⊙–>-pt = snd ⊙–>

  ⊙<– : Y ⊙→ X
  ⊙<– = is-equiv.g (snd ⊙e) , lemma ⊙e where
    lemma : {Y : Ptd j} (⊙e : X ⊙≃ Y) → is-equiv.g (snd ⊙e) (pt Y) == pt X
    lemma ((f , idp) , f-ise) = is-equiv.g-f f-ise (pt X)

  ⊙<–-pt = snd ⊙<–

  infix 120 _⊙⁻¹
  _⊙⁻¹ : Y ⊙≃ X
  _⊙⁻¹ = ⊙<– , is-equiv-inverse (snd ⊙e)

module _ {i j} {X : Ptd i} {Y : Ptd j} where

  ⊙<–-inv-l : (⊙e : X ⊙≃ Y) → ⊙<– ⊙e ⊙∘ ⊙–> ⊙e == ⊙idf _
  ⊙<–-inv-l ⊙e = ⊙λ= (<–-inv-l (⊙≃-to-≃ ⊙e) , ↓-idf=cst-in' (lemma ⊙e)) where
    lemma : {Y : Ptd j} (⊙e : X ⊙≃ Y)
      → snd (⊙<– ⊙e ⊙∘ ⊙–> ⊙e) == is-equiv.g-f (snd ⊙e) (pt X)
    lemma ((f , idp) , f-ise) = idp

  ⊙<–-inv-r : (⊙e : X ⊙≃ Y) → ⊙–> ⊙e ⊙∘ ⊙<– ⊙e == ⊙idf _
  ⊙<–-inv-r ⊙e = ⊙λ= (<–-inv-r (⊙≃-to-≃ ⊙e) , ↓-idf=cst-in' (lemma ⊙e)) where
    lemma : {Y : Ptd j} (⊙e : X ⊙≃ Y)
      → snd (⊙–> ⊙e ⊙∘ ⊙<– ⊙e) == is-equiv.f-g (snd ⊙e) (pt Y)
    lemma ((f , idp) , f-ise) = ∙-unit-r _ ∙ is-equiv.adj f-ise (pt X)

module _ {i} {X Y : Ptd i} where

  ⊙<–-inv-l-=⊙∘ : (⊙e : X ⊙≃ Y) → ⊙<– ⊙e ◃⊙∘ ⊙–> ⊙e ◃⊙idf =⊙∘ ⊙idf-seq
  ⊙<–-inv-l-=⊙∘ ⊙e = =⊙∘-in (⊙<–-inv-l ⊙e)

  ⊙<–-inv-r-=⊙∘ : (⊙e : X ⊙≃ Y) → ⊙–> ⊙e ◃⊙∘ ⊙<– ⊙e ◃⊙idf =⊙∘ ⊙idf-seq
  ⊙<–-inv-r-=⊙∘ ⊙e = =⊙∘-in (⊙<–-inv-r ⊙e)

module _ {i j k} {X : Ptd i} {Y : Ptd j} {Z : Ptd k} (⊙e : X ⊙≃ Y) where

  post⊙∘-is-equiv : is-equiv (λ (k : Z ⊙→ X) → ⊙–> ⊙e ⊙∘ k)
  post⊙∘-is-equiv = is-eq (⊙–> ⊙e ⊙∘_) (⊙<– ⊙e ⊙∘_) (to-from ⊙e) (from-to ⊙e) where
    abstract
      to-from : ∀ {Y} (⊙e : X ⊙≃ Y) (k : Z ⊙→ Y) → ⊙–> ⊙e ⊙∘ (⊙<– ⊙e ⊙∘ k) == k
      to-from ((f , idp) , f-ise) (k , k-pt) = ⊙λ=' (f.f-g ∘ k) (↓-idf=cst-in' $ lemma k-pt)
        where
          module f = is-equiv f-ise
          lemma : ∀ {y₀} (k-pt : y₀ == f (pt X))
            → ⊙∘-pt f (⊙∘-pt f.g k-pt (f.g-f _)) idp == f.f-g y₀ ∙' k-pt
          lemma idp = ∙-unit-r _ ∙ f.adj _

      from-to : ∀ {Y} (⊙e : X ⊙≃ Y) (k : Z ⊙→ X) → ⊙<– ⊙e ⊙∘ (⊙–> ⊙e ⊙∘ k) == k
      from-to ((f , idp) , f-ise) (k , idp) = ⊙λ=' (f.g-f ∘ k) $ ↓-idf=cst-in' idp
        where module f = is-equiv f-ise

  post⊙∘-equiv : (Z ⊙→ X) ≃ (Z ⊙→ Y)
  post⊙∘-equiv = _ , post⊙∘-is-equiv

  pre⊙∘-is-equiv : is-equiv (λ (k : Y ⊙→ Z) → k ⊙∘ ⊙–> ⊙e)
  pre⊙∘-is-equiv = is-eq (_⊙∘ ⊙–> ⊙e) (_⊙∘ ⊙<– ⊙e) (to-from ⊙e) (from-to ⊙e) where
    abstract
      to-from : ∀ {Z} (⊙e : X ⊙≃ Y) (k : X ⊙→ Z) → (k ⊙∘ ⊙<– ⊙e) ⊙∘ ⊙–> ⊙e == k
      to-from ((f , idp) , f-ise) (k , idp) = ⊙λ=' (ap k ∘ f.g-f) $ ↓-idf=cst-in' $ ∙-unit-r _
        where module f = is-equiv f-ise

      from-to : ∀ {Z} (⊙e : X ⊙≃ Y) (k : Y ⊙→ Z) → (k ⊙∘ ⊙–> ⊙e) ⊙∘ ⊙<– ⊙e == k
      from-to ((f , idp) , f-ise) (k , idp) = ⊙λ=' (ap k ∘ f.f-g) $ ↓-idf=cst-in' $
        ∙-unit-r _ ∙ ap-∘ k f (f.g-f (pt X)) ∙ ap (ap k) (f.adj (pt X))
        where module f = is-equiv f-ise

  pre⊙∘-equiv : (Y ⊙→ Z) ≃ (X ⊙→ Z)
  pre⊙∘-equiv = _ , pre⊙∘-is-equiv

{- Pointed maps out of bool -}

-- intuition : [f true] is fixed and the only changable part is [f false].

⊙Bool→-to-idf : ∀ {i} {X : Ptd i}
  → ⊙Bool ⊙→ X → de⊙ X
⊙Bool→-to-idf (h , _) = h false

⊙Bool→-equiv-idf : ∀ {i} (X : Ptd i)
  → (⊙Bool ⊙→ X) ≃ de⊙ X
⊙Bool→-equiv-idf {i} X = equiv ⊙Bool→-to-idf g f-g g-f
  where
  g : de⊙ X → ⊙Bool ⊙→ X
  g x = Bool-rec (pt X) x , idp

  abstract
    f-g : ∀ x → ⊙Bool→-to-idf (g x) == x
    f-g x = idp

    g-f : ∀ H → g (⊙Bool→-to-idf H) == H
    g-f (h , hpt) = pair=
      (λ= lemma)
      (↓-app=cst-in $
        idp
          =⟨ ! (!-inv-l hpt) ⟩
        ! hpt ∙ hpt
          =⟨ ! (app=-β lemma true) |in-ctx (λ w → w ∙ hpt) ⟩
        app= (λ= lemma) true ∙ hpt
          =∎)
      where lemma : ∀ b → fst (g (h false)) b == h b
            lemma true = ! hpt
            lemma false = idp

⊙Bool→-equiv-idf-nat : ∀ {i j} {X : Ptd i} {Y : Ptd j} (F : X ⊙→ Y)
  → CommSquareEquiv
      (F ⊙∘_)
      (fst F)
      ⊙Bool→-to-idf
      ⊙Bool→-to-idf
⊙Bool→-equiv-idf-nat F = (comm-sqr λ _ → idp) ,
  snd (⊙Bool→-equiv-idf _) , snd (⊙Bool→-equiv-idf _)

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
open import Signature

-- | One signature for terms and one for predicates.
module Logic (Σ Δ : Sig) (V : Set) where

open import Data.Empty renaming (⊥ to Ø)
open import Data.Unit
open import Data.Sum
open import Data.Product renaming (Σ to ∐)
open import Data.Nat
open import Data.Fin

FinSet : Set → Set
FinSet X = ∃ λ n → (Fin n → X)

dom : ∀{X} → FinSet X → Set
dom (n , _) = Fin n

get : ∀{X} (F : FinSet X) → dom F → X
get (_ , f) k = f k

drop : ∀{X} (F : FinSet

domEmpty : ∀{X} → FinSet X → Set
domEmpty (zero  , _) = ⊤
domEmpty (suc _ , _) = Ø

open import Terms Σ

Term : Set
Term = T V

-- | An atom is either a predicate on terms or bottom.
Atom : Set
Atom = ⟪ Δ ⟫ Term -- ⊎ ⊤

{-
⊥ : Atom
⊥ = inj₂ tt
-}

Formula : Set
Formula = Atom

Sentence : Set
Sentence = FinSet Formula

data Parity : Set where
  ind : Parity
  coind : Parity

record Clause : Set where
  constructor _⊢[_]_
  field
    head : Sentence
    par : Parity
    concl : Formula
open Clause public

Program : Set
Program = FinSet Clause

indClauses : Program → Program
indClauses (zero , P) = zero , λ ()
indClauses (suc n , P) = {!!}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
-- Andreas, 2017-01-24, issue #2429
-- Respect subtyping also for irrelevant lambdas!

-- Subtyping: (.A → B) ≤ (A → B)
-- Where a function is expected, we can put one which does not use its argument.

id : ∀{A B : Set} → (.A → B) → A → B
id f = f

test : ∀{A B : Set} → (.A → B) → A → B
test f = λ .a → f a

-- Should work!
-- The eta-expansion should not change anything!

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

module Data.Empty.Properties where

open import Data.Empty.Base
open import Level
open import HLevels

isProp⊥ : isProp ⊥
isProp⊥ ()

isProp¬ : (A : Type a) → isProp (¬ A)
isProp¬ _ f g i x = isProp⊥ (f x) (g x) i

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The type for booleans and some operations
------------------------------------------------------------------------

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

module Data.Bool.Base where

open import Data.Unit.Base using (⊤)
open import Data.Empty
open import Relation.Nullary

infixr 6 _∧_
infixr 5 _∨_ _xor_
infix  0 if_then_else_

------------------------------------------------------------------------
-- The boolean type

open import Agda.Builtin.Bool public

------------------------------------------------------------------------
-- Some operations

not : Bool → Bool
not true  = false
not false = true

-- A function mapping true to an inhabited type and false to an empty
-- type.

T : Bool → Set
T true  = ⊤
T false = ⊥

if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
if true  then t else f = t
if false then t else f = f

_∧_ : Bool → Bool → Bool
true  ∧ b = b
false ∧ b = false

_∨_ : Bool → Bool → Bool
true  ∨ b = true
false ∨ b = b

_xor_ : Bool → Bool → Bool
true  xor b = not b
false xor b = b


text:
open import prelude
open import ch6 using (Term  ; var ; fun ; _$_ ; two ; four)

-- A stack is a list of values
-- Values are either closures or errors

data Value : Set where
  error : Value
  closure : List(Value) → Term → Value

Stack = List(Value)

lookup : (s : Stack) → (x : Nat) → Value
lookup nil x = error
lookup (v :: s) zero = v
lookup (v :: s) (suc x) = lookup s x

-- Big step sematics

data _▷_⇓_ : Stack → Term → Value → Set where

  E─Var : ∀ {s x} →

    --------------------------
    s ▷ (var x) ⇓ (lookup s x)

  E─Fun : ∀ {s t} →

    ---------------------------
    s ▷ (fun t) ⇓ (closure s t)

  E─App : ∀ {s s′ t t′ u u′ v} →

    s ▷ t ⇓ (closure s′ t′) →
    s ▷ u ⇓ u′ →
    (u′ :: s′) ▷ t′ ⇓ v →
    -------------------
    s ▷ (t $ u) ⇓ v

  E─AppErr : ∀ {s t u} →

    s ▷ t ⇓ error →
    -------------------
    s ▷ (t $ u) ⇓ error

-- An interpreter result

data Result : Stack → Term → Set where

  result : ∀ {s t} →

    (v : Value) →
    (s ▷ t ⇓ v) →
    -------------
    Result s t

{-# NON_TERMINATING #-}
interpret : (s : Stack) → (t : Term) → Result s t
interpret s (var x) = result (lookup s x) E─Var
interpret s (fun t) = result (closure s t) E─Fun
interpret s (t₁ $ t₂) = helper₁ (interpret s t₁) where

  helper₃ : ∀ {s′ t′ u′} → (s ▷ t₁ ⇓ (closure s′ t′)) → (s ▷ t₂ ⇓ u′) → Result (u′ :: s′) t′ → Result s (t₁ $ t₂)
  helper₃ p q (result v r) = result v (E─App p q r)

  helper₂ : ∀ {s′ t′} → (s ▷ t₁ ⇓ (closure s′ t′)) → Result s t₂ → Result s (t₁ $ t₂)
  helper₂ {s′} {t′} p (result u′ q) = helper₃ p q (interpret (u′ :: s′) t′)

  helper₁ : Result s t₁ → Result s (t₁ $ t₂)
  helper₁ (result error           p) = result error (E─AppErr p)
  helper₁ (result (closure s′ t′) p) = helper₂ p (interpret s t₂)

-- Shorthand for starting from the empty stack

i = interpret nil

max_stars_repo_name: asajeffrey/tapl

max_issues_repo_name: asajeffrey/tapl

max_forks_repo_name: asajeffrey/tapl


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Normal Forms.
------------------------------------------------------------------------------

open import Data.Nat using (ℕ)

module Data.PropFormula.NormalForms (n : ℕ) where

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

open import Data.Nat.Base public
open import Data.Fin  using ( Fin; #_ )
open import Data.List using ( List; [_]; [];  _++_; _∷_ ; concatMap; map )

open import Data.PropFormula.Properties n using ( subst )
open import Data.PropFormula.Syntax n
open import Data.PropFormula.Theorems n

open import Relation.Nullary using (yes; no)

open import Function using ( _∘_; _$_ )
open import Relation.Binary.PropositionalEquality using ( _≡_; sym )

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

data Literal : Set where
  Var  : Fin n   → Literal
  ¬l_  : Literal → Literal

Clause : Set
Clause = List Literal

------------------------------------------------------------------------------
-- Conjunctive Normal Form (CNF)
------------------------------------------------------------------------------

Cnf : Set
Cnf = List Clause

varCnf_ : Literal → Cnf
varCnf l = [ [ l ] ]

_∧Cnf_ : (φ ψ : Cnf) → Cnf
φ ∧Cnf ψ = φ ++ ψ

_∨Cnf_ : (φ ψ : Cnf) → Cnf
[]  ∨Cnf ψ       = ψ
φ   ∨Cnf []      = []
cls ∨Cnf (x ∷ ψ) = (cls ∨⋆ x) ∧Cnf (cls ∨Cnf ψ)
  where
    _∨⋆_ : Cnf → Clause → Cnf
    xs ∨⋆ ys = concatMap (λ x → [ x ++ ys ]) xs

¬Cnf₀_ : Literal → Literal
¬Cnf₀ Var x    = ¬l Var x
¬Cnf₀ (¬l lit) = lit

¬Cnf₁ : Clause → Cnf
¬Cnf₁ []  = []  -- ¬ ⊥ → ⊤
¬Cnf₁ cls = map (λ lit → [ ¬Cnf₀ lit ]) cls

¬Cnf : Cnf → Cnf
¬Cnf [] = [ [] ]
¬Cnf fm = concatMap (λ cl → ¬Cnf₁ cl) fm

_⊃Cnf_ : (φ ψ : Cnf) → Cnf
φ ⊃Cnf ψ = (¬Cnf φ) ∨Cnf ψ

_⇔Cnf_ : (φ ψ : Cnf) → Cnf
φ ⇔Cnf ψ = (φ ⊃Cnf ψ) ∧Cnf (ψ ⊃Cnf φ)

toCnf : PropFormula → Cnf
toCnf (Var x) = varCnf Var x
toCnf ⊤       = []
toCnf ⊥       = [ [] ]
toCnf (φ ∧ ψ) = toCnf φ ∧Cnf toCnf ψ
toCnf (φ ∨ ψ) = toCnf φ ∨Cnf toCnf ψ
toCnf (φ ⊃ ψ) = toCnf φ ⊃Cnf toCnf ψ
toCnf (φ ⇔ ψ) = toCnf φ ⇔Cnf toCnf ψ
toCnf (¬ φ)   = ¬Cnf (toCnf φ)

toPropLiteral : Literal → PropFormula
toPropLiteral (Var x)  = Var x
toPropLiteral (¬l lit) = ¬ toPropLiteral lit

toPropClause : Clause → PropFormula
toPropClause []       = ⊥
toPropClause (l ∷ []) = toPropLiteral l
toPropClause (l ∷ ls) = toPropLiteral l ∨ toPropClause ls

toProp : Cnf → PropFormula
toProp []         = ⊤
toProp (fm ∷ [] ) = toPropClause fm
toProp (fm ∷ fms) = toPropClause fm ∧ toProp fms

cnf : PropFormula → PropFormula
cnf = toProp ∘ toCnf

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
module Prelude.Equality.Inspect where

open import Prelude.Function using (id)
open import Prelude.Equality
open import Prelude.Product

module _ {a b} {A : Set a} {B : A → Set b} (f : ∀ x → B x) (x : A) where

  -- The Graph idiom is more powerful than the old Inspect idiom
  -- (defined in terms of Graph below), in that it lets you both
  -- abstract over a term and keep the equation that the old term
  -- equals the abstracted variable.

  -- Use as follows:
  --   example : Γ → T (f e)
  --   example xs with f e | graphAt f e
  --   ... | z | ingraph eq = ?  -- eq : f e ≡ z, goal : T z

  data Graph (y : B x) : Set b where
    ingraph : f x ≡ y → Graph y

  graphAt : Graph (f x)
  graphAt = ingraph refl
  {-# INLINE graphAt #-}

module _ {a} {A : Set a} where

  Inspect : A → Set a
  Inspect x = Σ _ λ y → Graph id x y

  infix 4 _with≡_
  pattern _with≡_ x eq = x , ingraph eq

  inspect : ∀ x → Inspect x
  inspect x = x , ingraph refl
  {-# INLINE inspect #-}


text:
module Issue2492 where

open import Agda.Builtin.Nat

infix 0 _!
data Singleton {A : Set} : A → Set where
  _! : (a : A) → Singleton a

_ : Singleton 10
_ = {!!}


text:
------------------------------------------------------------------------
-- Application of substitutions
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Data.Application.Application
  {i u e} {Uni : IndexedUniverse i u e} where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Basics
open import deBruijn.Substitution.Data.Map
open import Level using (_⊔_)
import Relation.Binary.PropositionalEquality as P

-- Given an operation which applies substitutions to terms one can
-- define composition of substitutions.

record Application
  {t₁} (T₁ : Term-like t₁)
  {t₂} (T₂ : Term-like t₂) :
  Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where

  open Term-like T₂ renaming (_⊢_ to _⊢₂_; _≅-⊢_ to _≅-⊢₂_)

  field
    -- Application of substitutions to terms.
    app : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Sub T₁ ρ̂ → [ T₂ ⟶ T₂ ] ρ̂

  -- Post-application of substitutions to terms.

  infixl 8 _/⊢_

  _/⊢_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Γ ⊢₂ σ → Sub T₁ ρ̂ → Δ ⊢₂ σ /̂ ρ̂
  t /⊢ ρ = app ρ · t

  -- Reverse composition. (Fits well with post-application.)

  infixl 9 _∘_

  _∘_ : ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} →
        Sub T₂ ρ̂₁ → Sub T₁ ρ̂₂ → Sub T₂ (ρ̂₁ ∘̂ ρ̂₂)
  ρ₁ ∘ ρ₂ = map (app ρ₂) ρ₁

  -- Application of multiple substitutions to terms.

  app⋆ : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → Subs T₁ ρ̂ → [ T₂ ⟶ T₂ ] ρ̂
  app⋆ = fold [ T₂ ⟶ T₂ ] [id] (λ f ρ → app ρ [∘] f)

  infixl 8 _/⊢⋆_

  _/⊢⋆_ : ∀ {Γ Δ σ} {ρ̂ : Γ ⇨̂ Δ} → Γ ⊢₂ σ → Subs T₁ ρ̂ → Δ ⊢₂ σ /̂ ρ̂
  t /⊢⋆ ρs = app⋆ ρs · t

  -- Some congruence lemmas.

  app-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T₁ ρ̂₁}
               {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T₁ ρ̂₂} →
             ρ₁ ≅-⇨ ρ₂ → app ρ₁ ≅-⟶ app ρ₂
  app-cong P.refl = [ P.refl ]

  /⊢-cong :
    ∀ {Γ₁ Δ₁ σ₁} {t₁ : Γ₁ ⊢₂ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : Sub T₁ ρ̂₁}
      {Γ₂ Δ₂ σ₂} {t₂ : Γ₂ ⊢₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : Sub T₁ ρ̂₂} →
    t₁ ≅-⊢₂ t₂ → ρ₁ ≅-⇨ ρ₂ → t₁ /⊢ ρ₁ ≅-⊢₂ t₂ /⊢ ρ₂
  /⊢-cong P.refl P.refl = P.refl

  ∘-cong :
    ∀ {Γ₁ Δ₁ Ε₁} {ρ̂₁₁ : Γ₁ ⇨̂ Δ₁} {ρ̂₂₁ : Δ₁ ⇨̂ Ε₁}
      {ρ₁₁ : Sub T₂ ρ̂₁₁} {ρ₂₁ : Sub T₁ ρ̂₂₁}
      {Γ₂ Δ₂ Ε₂} {ρ̂₁₂ : Γ₂ ⇨̂ Δ₂} {ρ̂₂₂ : Δ₂ ⇨̂ Ε₂}
      {ρ₁₂ : Sub T₂ ρ̂₁₂} {ρ₂₂ : Sub T₁ ρ̂₂₂} →
    ρ₁₁ ≅-⇨ ρ₁₂ → ρ₂₁ ≅-⇨ ρ₂₂ → ρ₁₁ ∘ ρ₂₁ ≅-⇨ ρ₁₂ ∘ ρ₂₂
  ∘-cong P.refl P.refl = P.refl

  app⋆-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T₁ ρ̂₁}
                {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T₁ ρ̂₂} →
              ρs₁ ≅-⇨⋆ ρs₂ → app⋆ ρs₁ ≅-⟶ app⋆ ρs₂
  app⋆-cong P.refl = [ P.refl ]

  /⊢⋆-cong :
    ∀ {Γ₁ Δ₁ σ₁} {t₁ : Γ₁ ⊢₂ σ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρs₁ : Subs T₁ ρ̂₁}
      {Γ₂ Δ₂ σ₂} {t₂ : Γ₂ ⊢₂ σ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρs₂ : Subs T₁ ρ̂₂} →
    t₁ ≅-⊢₂ t₂ → ρs₁ ≅-⇨⋆ ρs₂ → t₁ /⊢⋆ ρs₁ ≅-⊢₂ t₂ /⊢⋆ ρs₂
  /⊢⋆-cong P.refl P.refl = P.refl

  abstract

    -- An unfolding lemma.

    ▻-∘ : ∀ {Γ Δ Ε} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε} {σ}
          (ρ₁ : Sub T₂ ρ̂₁) (t : Δ ⊢₂ σ / ρ₁) (ρ₂ : Sub T₁ ρ̂₂) →
          (ρ₁ ▻⇨[ σ ] t) ∘ ρ₂ ≅-⇨ ρ₁ ∘ ρ₂ ▻⇨[ σ ] t /⊢ ρ₂
    ▻-∘ ρ₁ t ρ₂ = map-▻ (app ρ₂) ρ₁ t

    -- Applying a composed substitution to a variable is equivalent to
    -- applying one substitution and then the other.

    /∋-∘ : ∀ {Γ Δ Ε σ} {ρ̂₁ : Γ ⇨̂ Δ} {ρ̂₂ : Δ ⇨̂ Ε}
           (x : Γ ∋ σ) (ρ₁ : Sub T₂ ρ̂₁) (ρ₂ : Sub T₁ ρ̂₂) →
           x /∋ ρ₁ ∘ ρ₂ ≅-⊢₂ x /∋ ρ₁ /⊢ ρ₂
    /∋-∘ x ρ₁ ρ₂ = /∋-map x (app ρ₂) ρ₁

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
-- Andreas, 2021-10-08, first test case for unsupported generalization

variable
  X : Set

Y = X

-- Expected:
-- Generalizable variable GeneralizeRHS.X is not supported here
-- when scope checking X

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module Text.XML.Everything where

-- Imported packages

import Web.URI.Everything

max_stars_repo_name: agda/agda-text-xml

max_issues_repo_name: agda/agda-text-xml

max_forks_repo_name: agda/agda-text-xml


text:
open import bool
open import list
open import nat

_⇒_ : 𝕃 Set → Set → Set
[] ⇒ rettp = rettp
(x :: inputtps) ⇒ rettp = x → inputtps ⇒ rettp

_⇒𝕃_ : 𝕃 Set → Set → Set
inputtps ⇒𝕃 rettp = (map 𝕃 inputtps) ⇒ (𝕃 rettp)

eatInputs : {inputtps : 𝕃 Set}{rettp : Set} → inputtps ⇒𝕃 rettp
eatInputs {[]} {rettp₁} = []
eatInputs {x₁ :: inputtps₁} {rettp₁} _ = eatInputs{inputtps₁}{rettp₁}

zipWith : {inputtps : 𝕃 Set}{rettp : Set} → (inputtps ⇒ rettp) → inputtps ⇒𝕃 rettp
zipWith {[]} {rettp} a = [ a ]
zipWith {tp :: inputtps} {rettp} f [] = eatInputs {inputtps}{rettp}
zipWith {tp :: inputtps} {rettp} f (h :: t) =
  helper{inputtps}{rettp} (f h) (zipWith{tp :: inputtps}{rettp} f t)
  where helper : {inputtps : 𝕃 Set}{rettp : Set} →
                 inputtps ⇒ rettp →
                 inputtps ⇒𝕃 rettp →
                 inputtps ⇒𝕃 rettp
        helper {[]} {rettp₁} f F = f :: F
        helper {tp :: inputtps} {rettp} _ _ [] = eatInputs{inputtps}{rettp}
        helper {tp :: inputtps} {rettp} f F (h :: t) = helper{inputtps}{rettp} (f h) (F t)

testTpList : 𝕃 Set
testTpList = (𝔹 :: ℕ :: ℕ :: [])

test = zipWith{testTpList}{ℕ} (λ b n m → if b then n else m) (tt :: tt :: ff :: []) (1 :: 2 :: 3 :: []) (10 :: 20 :: 30 :: 1000 :: [])

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module Data.Tuple.Equiv where

import      Lvl
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Structure.Function
open import Structure.Operator
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable A B : Type{ℓ}

record Extensionality ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ (equiv : Equiv{ℓₑ}(A ⨯ B)) : Type{Lvl.of(A) Lvl.⊔ Lvl.of(B) Lvl.⊔ ℓₑ₁ Lvl.⊔ ℓₑ₂ Lvl.⊔ ℓₑ} where
  constructor intro
  private instance _ = equiv
  field
    ⦃ [,]-function ⦄   : BinaryOperator(_,_)
    ⦃ left-function ⦄  : Function(Tuple.left)
    ⦃ right-function ⦄ : Function(Tuple.right)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module PosFunction where

data Functor : Set1 where
  |Id|  : Functor
  |K|   : Set -> Functor
  _|+|_ : Functor -> Functor -> Functor
  _|x|_ : Functor -> Functor -> Functor

data _⊕_ (A B : Set) : Set where
  inl : A -> A ⊕ B
  inr : B -> A ⊕ B

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

-- The positivity checker can see that [_] is positive in its second argument.
[_] : Functor -> Set -> Set
[ |Id|    ] X = X
[ |K| A   ] X = A
[ F |+| G ] X = [ F ] X ⊕ [ G ] X
[ F |x| G ] X = [ F ] X × [ G ] X

data μ_ (F : Functor) : Set where
  <_> : [ F ] (μ F) -> μ F

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda