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

open import lib.Basics
open import lib.types.Paths
open import lib.types.TwoSemiCategory

module lib.two-semi-categories.Functor where

record TwoSemiFunctor {i₁ j₁ i₂ j₂} (C : TwoSemiCategory i₁ j₁) (D : TwoSemiCategory i₂ j₂)
  : Type (lmax (lmax i₁ j₁) (lmax i₂ j₂)) where
  private
    module C = TwoSemiCategory C
    module D = TwoSemiCategory D
  field
    F₀ : C.El → D.El
    F₁ : {x y : C.El} → C.Arr x y → D.Arr (F₀ x) (F₀ y)
    pres-comp : {x y z : C.El} (f : C.Arr x y) (g : C.Arr y z)
      → F₁ (C.comp f g) == D.comp (F₁ f) (F₁ g)

  pres-comp-coh-seq₁ : {w x y z : C.El} (f : C.Arr w x) (g : C.Arr x y) (h : C.Arr y z)
    → F₁ (C.comp (C.comp f g) h) =-= D.comp (F₁ f) (D.comp (F₁ g) (F₁ h))
  pres-comp-coh-seq₁ f g h =
    F₁ (C.comp (C.comp f g) h)
      =⟪ pres-comp (C.comp f g) h ⟫
    D.comp (F₁ (C.comp f g)) (F₁ h)
      =⟪ ap (λ s → D.comp s (F₁ h)) (pres-comp f g) ⟫
    D.comp (D.comp (F₁ f) (F₁ g)) (F₁ h)
      =⟪ D.assoc (F₁ f) (F₁ g) (F₁ h) ⟫
    D.comp (F₁ f) (D.comp (F₁ g) (F₁ h)) ∎∎

  pres-comp-coh-seq₂ : {w x y z : C.El} (f : C.Arr w x) (g : C.Arr x y) (h : C.Arr y z)
    → F₁ (C.comp (C.comp f g) h) =-= D.comp (F₁ f) (D.comp (F₁ g) (F₁ h))
  pres-comp-coh-seq₂ f g h =
    F₁ (C.comp (C.comp f g) h)
      =⟪ ap F₁ (C.assoc f g h) ⟫
    F₁ (C.comp f (C.comp g h))
      =⟪ pres-comp f (C.comp g h) ⟫
    D.comp (F₁ f) (F₁ (C.comp g h))
      =⟪ ap (D.comp (F₁ f)) (pres-comp g h) ⟫
    D.comp (F₁ f) (D.comp (F₁ g) (F₁ h)) ∎∎

  field
    pres-comp-coh : {w x y z : C.El} (f : C.Arr w x) (g : C.Arr x y) (h : C.Arr y z)
      → pres-comp-coh-seq₁ f g h =ₛ pres-comp-coh-seq₂ f g h

module FunctorComposition
  {i₁ j₁ i₂ j₂ i₃ j₃} {C : TwoSemiCategory i₁ j₁} {D : TwoSemiCategory i₂ j₂} {E : TwoSemiCategory i₃ j₃}
  (F : TwoSemiFunctor C D) (G : TwoSemiFunctor D E) where

  private
    module C = TwoSemiCategory C
    module D = TwoSemiCategory D
    module E = TwoSemiCategory E
    module F = TwoSemiFunctor F
    module G = TwoSemiFunctor G

    F₀ : C.El → E.El
    F₀ = G.F₀ ∘ F.F₀

    F₁ : {x y : C.El} → C.Arr x y → E.Arr (F₀ x) (F₀ y)
    F₁ f = G.F₁ (F.F₁ f)

  pres-comp-seq : {x y z : C.El} (f : C.Arr x y) (g : C.Arr y z)
    → G.F₁ (F.F₁ (C.comp f g)) =-= E.comp (G.F₁ (F.F₁ f)) (G.F₁ (F.F₁ g))
  pres-comp-seq f g =
    G.F₁ (F.F₁ (C.comp f g))
      =⟪ ap G.F₁ (F.pres-comp f g) ⟫
    G.F₁ (D.comp (F.F₁ f) (F.F₁ g))
      =⟪ G.pres-comp (F.F₁ f) (F.F₁ g) ⟫
    E.comp (G.F₁ (F.F₁ f)) (G.F₁ (F.F₁ g)) ∎∎

  abstract
    pres-comp : {x y z : C.El} (f : C.Arr x y) (g : C.Arr y z)
      → G.F₁ (F.F₁ (C.comp f g)) == E.comp (G.F₁ (F.F₁ f)) (G.F₁ (F.F₁ g))
    pres-comp f g = ↯ (pres-comp-seq f g)

    pres-comp-β : {x y z : C.El} (f : C.Arr x y) (g : C.Arr y z)
      → pres-comp f g ◃∎ =ₛ pres-comp-seq f g
    pres-comp-β f g = =ₛ-in idp

  private
    abstract
      pres-comp-coh : {w x y z : C.El} (f : C.Arr w x) (g : C.Arr x y) (h : C.Arr y z)
        → pres-comp (C.comp f g) h ◃∙ ap (λ s → E.comp s (F₁ h)) (pres-comp f g) ◃∙ E.assoc (F₁ f) (F₁ g) (F₁ h) ◃∎
          =ₛ
          ap F₁ (C.assoc f g h) ◃∙ pres-comp f (C.comp g h) ◃∙ ap (E.comp (F₁ f)) (pres-comp g h) ◃∎
      pres-comp-coh f g h =
        pres-comp (C.comp f g) h ◃∙
        ap (λ s → E.comp s (F₁ h)) (pres-comp f g) ◃∙
        E.assoc (F₁ f) (F₁ g) (F₁ h) ◃∎
          =ₛ⟨ 0 & 1 & expand (pres-comp-seq (C.comp f g) h) ⟩
        ap G.F₁ (F.pres-comp (C.comp f g) h) ◃∙
        G.pres-comp (F.F₁ (C.comp f g)) (F.F₁ h) ◃∙
        ap (λ s → E.comp s (F₁ h)) (pres-comp f g) ◃∙
        E.assoc (F₁ f) (F₁ g) (F₁ h) ◃∎
          =ₛ⟨ 2 & 1 & ap-seq-∙ (λ s → E.comp s (F₁ h)) (pres-comp-seq f g) ⟩
        ap G.F₁ (F.pres-comp (C.comp f g) h) ◃∙
        G.pres-comp (F.F₁ (C.comp f g)) (F.F₁ h) ◃∙
        ap (λ s → E.comp s (F₁ h)) (ap G.F₁ (F.pres-comp f g)) ◃∙
        ap (λ s → E.comp s (F₁ h)) (G.pres-comp (F.F₁ f) (F.F₁ g)) ◃∙
        E.assoc (F₁ f) (F₁ g) (F₁ h) ◃∎
          =ₛ₁⟨ 2 & 1 & ∘-ap (λ s → E.comp s (F₁ h)) G.F₁ (F.pres-comp f g) ⟩
        ap G.F₁ (F.pres-comp (C.comp f g) h) ◃∙
        G.pres-comp (F.F₁ (C.comp f g)) (F.F₁ h) ◃∙
        ap (λ s → E.comp (G.F₁ s) (F₁ h)) (F.pres-comp f g) ◃∙
        ap (λ s → E.comp s (F₁ h)) (G.pres-comp (F.F₁ f) (F.F₁ g)) ◃∙
        E.assoc (F₁ f) (F₁ g) (F₁ h) ◃∎
          =ₛ⟨ 1 & 2 & !ₛ $
              homotopy-naturality (λ s → G.F₁ (D.comp s (F.F₁ h)))
                                  (λ s → E.comp (G.F₁ s) (F₁ h))
                                  (λ s → G.pres-comp s (F.F₁ h))
                                  (F.pres-comp f g) ⟩
        ap G.F₁ (F.pres-comp (C.comp f g) h) ◃∙
        ap (λ s → G.F₁ (D.comp s (F.F₁ h))) (F.pres-comp f g) ◃∙
        G.pres-comp (D.comp (F.F₁ f) (F.F₁ g)) (F.F₁ h) ◃∙
        ap (λ s → E.comp s (F₁ h)) (G.pres-comp (F.F₁ f) (F.F₁ g)) ◃∙
        E.assoc (F₁ f) (F₁ g) (F₁ h) ◃∎
          =ₛ⟨ 2 & 3 & G.pres-comp-coh (F.F₁ f) (F.F₁ g) (F.F₁ h) ⟩
        ap G.F₁ (F.pres-comp (C.comp f g) h) ◃∙
        ap (λ s → G.F₁ (D.comp s (F.F₁ h))) (F.pres-comp f g) ◃∙
        ap G.F₁ (D.assoc (F.F₁ f) (F.F₁ g) (F.F₁ h)) ◃∙
        G.pres-comp (F.F₁ f) (D.comp (F.F₁ g) (F.F₁ h)) ◃∙
        ap (E.comp (F₁ f)) (G.pres-comp (F.F₁ g) (F.F₁ h)) ◃∎
          =ₛ₁⟨ 1 & 1 & ap-∘ G.F₁ (λ s → D.comp s (F.F₁ h)) (F.pres-comp f g) ⟩
        ap G.F₁ (F.pres-comp (C.comp f g) h) ◃∙
        ap G.F₁ (ap (λ s → D.comp s (F.F₁ h)) (F.pres-comp f g)) ◃∙
        ap G.F₁ (D.assoc (F.F₁ f) (F.F₁ g) (F.F₁ h)) ◃∙
        G.pres-comp (F.F₁ f) (D.comp (F.F₁ g) (F.F₁ h)) ◃∙
        ap (E.comp (F₁ f)) (G.pres-comp (F.F₁ g) (F.F₁ h)) ◃∎
          =ₛ⟨ 0 & 3 & ap-seq-=ₛ G.F₁ (F.pres-comp-coh f g h) ⟩
        ap G.F₁ (ap F.F₁ (C.assoc f g h)) ◃∙
        ap G.F₁ (F.pres-comp f (C.comp g h)) ◃∙
        ap G.F₁ (ap (D.comp (F.F₁ f)) (F.pres-comp g h)) ◃∙
        G.pres-comp (F.F₁ f) (D.comp (F.F₁ g) (F.F₁ h)) ◃∙
        ap (E.comp (F₁ f)) (G.pres-comp (F.F₁ g) (F.F₁ h)) ◃∎
          =ₛ₁⟨ 2 & 1 & ∘-ap G.F₁ (D.comp (F.F₁ f)) (F.pres-comp g h) ⟩
        ap G.F₁ (ap F.F₁ (C.assoc f g h)) ◃∙
        ap G.F₁ (F.pres-comp f (C.comp g h)) ◃∙
        ap (G.F₁ ∘ D.comp (F.F₁ f)) (F.pres-comp g h) ◃∙
        G.pres-comp (F.F₁ f) (D.comp (F.F₁ g) (F.F₁ h)) ◃∙
        ap (E.comp (F₁ f)) (G.pres-comp (F.F₁ g) (F.F₁ h)) ◃∎
          =ₛ⟨ 2 & 2 &
              homotopy-naturality (G.F₁ ∘ D.comp (F.F₁ f))
                                  (E.comp (F₁ f) ∘ G.F₁)
                                  (G.pres-comp (F.F₁ f))
                                  (F.pres-comp g h) ⟩
        ap G.F₁ (ap F.F₁ (C.assoc f g h)) ◃∙
        ap G.F₁ (F.pres-comp f (C.comp g h)) ◃∙
        G.pres-comp (F.F₁ f) (F.F₁ (C.comp g h)) ◃∙
        ap (λ s → E.comp (F₁ f) (G.F₁ s)) (F.pres-comp g h) ◃∙
        ap (E.comp (F₁ f)) (G.pres-comp (F.F₁ g) (F.F₁ h)) ◃∎
          =ₛ⟨ 1 & 2 & contract ⟩
        ap G.F₁ (ap F.F₁ (C.assoc f g h)) ◃∙
        pres-comp f (C.comp g h) ◃∙
        ap (λ s → E.comp (F₁ f) (G.F₁ s)) (F.pres-comp g h) ◃∙
        ap (E.comp (F₁ f)) (G.pres-comp (F.F₁ g) (F.F₁ h)) ◃∎
          =ₛ₁⟨ 2 & 1 & ap-∘ (E.comp (F₁ f)) G.F₁ (F.pres-comp g h) ⟩
        ap G.F₁ (ap F.F₁ (C.assoc f g h)) ◃∙
        pres-comp f (C.comp g h) ◃∙
        ap (E.comp (F₁ f)) (ap G.F₁ (F.pres-comp g h)) ◃∙
        ap (E.comp (F₁ f)) (G.pres-comp (F.F₁ g) (F.F₁ h)) ◃∎
          =ₛ⟨ 2 & 2 & ∙-ap-seq (E.comp (F₁ f)) (pres-comp-seq g h) ⟩
        ap G.F₁ (ap F.F₁ (C.assoc f g h)) ◃∙
        pres-comp f (C.comp g h) ◃∙
        ap (E.comp (F₁ f)) (pres-comp g h) ◃∎
          =ₛ₁⟨ 0 & 1 & ∘-ap G.F₁ F.F₁ (C.assoc f g h) ⟩
        ap F₁ (C.assoc f g h) ◃∙
        pres-comp f (C.comp g h) ◃∙
        ap (E.comp (F₁ f)) (pres-comp g h) ◃∎ ∎ₛ

  composition : TwoSemiFunctor C E
  composition =
    record
    { F₀ = F₀
    ; F₁ = F₁
    ; pres-comp = pres-comp
    ; pres-comp-coh = pres-comp-coh
    }

open FunctorComposition
  renaming ( composition to comp-functors
           ; pres-comp-seq to comp-functors-pres-comp-seq
           ; pres-comp to comp-functors-pres-comp
           ; pres-comp-β to comp-functors-pres-comp-β
           ) public

infixr 80 _–F→_
_–F→_ = comp-functors

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

open import LogicalFormulae
open import Groups.Definition
open import Numbers.Naturals.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.EuclideanDomains.Definition
open import Fields.Fields
open import Fields.Lemmas

module Rings.EuclideanDomains.Examples where

polynomialField : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (F : Field R) → (Setoid._∼_ S (Ring.1R R) (Ring.0R R) → False) → EuclideanDomain R
EuclideanDomain.isIntegralDomain (polynomialField F 1!=0) = fieldIsIntDom F
EuclideanDomain.norm (polynomialField F _) a!=0 = zero
EuclideanDomain.normSize (polynomialField F _) a!=0 b!=0 c b=ac = inr refl
DivisionAlgorithmResult.quotient (EuclideanDomain.divisionAlg (polynomialField {_*_ = _*_} F _) {a = a} {b} a!=0 b!=0) with Field.allInvertible F b b!=0
... | bInv , prB = a * bInv
DivisionAlgorithmResult.rem (EuclideanDomain.divisionAlg (polynomialField F _) a!=0 b!=0) = Field.0F F
DivisionAlgorithmResult.remSmall (EuclideanDomain.divisionAlg (polynomialField {S = S} F _) a!=0 b!=0) = inl (Equivalence.reflexive (Setoid.eq S))
DivisionAlgorithmResult.divAlg (EuclideanDomain.divisionAlg (polynomialField {S = S} {R = R} F _) {a = a} {b = b} a!=0 b!=0) with Field.allInvertible F b b!=0
... | bInv , prB = transitive (transitive (transitive (symmetric identIsIdent) (transitive *Commutative (*WellDefined reflexive (symmetric prB)))) *Associative) (symmetric identRight)
  where
    open Setoid S
    open Equivalence eq
    open Ring R
    open Group additiveGroup

ext: agda


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

open import Setoids.Setoids
open import Rings.Definition
open import Groups.Definition
open import Fields.Fields
open import Sets.EquivalenceRelations
open import LogicalFormulae
open import Rings.IntegralDomains.Definition
open import Rings.IntegralDomains.Lemmas
open import Setoids.Subset

module Fields.Lemmas {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (F : Field R) where

open Setoid S
open Field F
open Ring R
open Group additiveGroup
open Equivalence eq
open import Rings.Lemmas R

halve : (charNot2 : ((1R + 1R) ∼ 0R) → False) → (a : A) → Sg A (λ i → i + i ∼ a)
halve charNot2 a with allInvertible (1R + 1R) charNot2
... | 1/2 , pr1/2 = (a * 1/2) , transitive (+WellDefined *Commutative *Commutative) (transitive (symmetric (*DistributesOver+ {1/2} {a} {a})) (transitive (*WellDefined (reflexive) r) (transitive (*Associative) (transitive (*WellDefined pr1/2 (reflexive)) identIsIdent))))
  where
    r : a + a ∼ (1R + 1R) * a
    r = symmetric (transitive *Commutative (transitive *DistributesOver+ (+WellDefined (transitive *Commutative identIsIdent) (transitive *Commutative identIsIdent))))

abstract

  halfHalves : {x : A} (1/2 : A) (pr : 1/2 + 1/2 ∼ 1R) → (x + x) * 1/2 ∼ x
  halfHalves {x} 1/2 pr = transitive (transitive (transitive *Commutative (transitive (transitive *DistributesOver+ (transitive (+WellDefined *Commutative *Commutative) (symmetric *DistributesOver+))) *Commutative)) (*WellDefined pr (reflexive))) identIsIdent

fieldIsIntDom : IntegralDomain R
IntegralDomain.intDom fieldIsIntDom {a} {b} ab=0 a!=0 with Field.allInvertible F a a!=0
IntegralDomain.intDom fieldIsIntDom {a} {b} ab=0 a!=0 | 1/a , prA = transitive (symmetric identIsIdent) (transitive (*WellDefined (symmetric prA) reflexive) (transitive (symmetric *Associative) (transitive (*WellDefined reflexive ab=0) (Ring.timesZero R))))
IntegralDomain.nontrivial fieldIsIntDom 1=0 = Field.nontrivial F (symmetric 1=0)

allInvertibleWellDefined : {a b : A} {a!=0 : (a ∼ 0F) → False} {b!=0 : (b ∼ 0F) → False} → (a ∼ b) → underlying (allInvertible a a!=0) ∼ underlying (allInvertible b b!=0)
allInvertibleWellDefined {a} {b} {a!=0} {b!=0} a=b with allInvertible a a!=0
... | x , prX with allInvertible b b!=0
... | y , prY with transitive (transitive prX (symmetric prY)) (*WellDefined reflexive (symmetric a=b))
... | xa=ya = cancelIntDom fieldIsIntDom (transitive *Commutative (transitive xa=ya *Commutative)) a!=0

private
  mulNonzeros : Sg A (λ m → (Setoid._∼_ S m (Ring.0R R)) → False) → Sg A (λ m → (Setoid._∼_ S m (Ring.0R R)) → False) → Sg A (λ m → (Setoid._∼_ S m (Ring.0R R)) → False)
  mulNonzeros (a , a!=0) (b , b!=0) = (a * b) , λ ab=0 → b!=0 (IntegralDomain.intDom (fieldIsIntDom) ab=0 a!=0)

fieldMultiplicativeGroup : Group (subsetSetoid S {pred = λ m → ((Setoid._∼_ S m (Ring.0R R)) → False)}(λ {x} {y} x=y x!=0 → λ y=0 → x!=0 (Equivalence.transitive (Setoid.eq S) x=y y=0))) (mulNonzeros)
Group.+WellDefined (fieldMultiplicativeGroup) {x , prX} {y , prY} {z , prZ} {w , prW} = Ring.*WellDefined R
Group.0G (fieldMultiplicativeGroup) = Ring.1R R , λ 1=0 → Field.nontrivial F (Equivalence.symmetric (Setoid.eq S) 1=0)
Group.inverse (fieldMultiplicativeGroup) (x , pr) with Field.allInvertible F x pr
... | 1/x , pr1/x = 1/x , λ 1/x=0 → Field.nontrivial F (Equivalence.transitive (Setoid.eq S) (Equivalence.symmetric (Setoid.eq S) (Equivalence.transitive (Setoid.eq S) (Ring.*WellDefined R 1/x=0 (Equivalence.reflexive (Setoid.eq S))) (Ring.timesZero' R))) pr1/x)
Group.+Associative (fieldMultiplicativeGroup) {x , prX} {y , prY} {z , prZ} = Ring.*Associative R
Group.identRight (fieldMultiplicativeGroup) {x , prX} = Ring.identIsIdent' R
Group.identLeft (fieldMultiplicativeGroup) {x , prX} = Ring.identIsIdent R
Group.invLeft (fieldMultiplicativeGroup) {x , prX} with Field.allInvertible F x prX
... | 1/x , pr1/x = pr1/x
Group.invRight (fieldMultiplicativeGroup) {x , prX} with Field.allInvertible F x prX
... | 1/x , pr1/x = Equivalence.transitive (Setoid.eq S) (Ring.*Commutative R) pr1/x


text:
{-

Product of structures S and T: X ↦ S X × T X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Product where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Foundations.SIP
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ₁ ℓ₁' ℓ₂ ℓ₂' : Level

ProductStructure : (S₁ : Type ℓ → Type ℓ₁) (S₂ : Type ℓ → Type ℓ₂)
               → Type ℓ → Type (ℓ-max ℓ₁ ℓ₂)
ProductStructure S₁ S₂ X = S₁ X × S₂ X

ProductEquivStr : {S₁ : Type ℓ → Type ℓ₁} (ι₁ : StrEquiv S₁ ℓ₁')
           {S₂ : Type ℓ → Type ℓ₂} (ι₂ : StrEquiv S₂ ℓ₂')
         → StrEquiv (ProductStructure S₁ S₂) (ℓ-max ℓ₁' ℓ₂')
ProductEquivStr ι₁ ι₂ (X , s₁ , s₂) (Y , t₁ , t₂) f = (ι₁ (X , s₁) (Y , t₁) f) × (ι₂ (X , s₂) (Y , t₂) f)

ProductUnivalentStr : {S₁ : Type ℓ → Type ℓ₁} (ι₁ : StrEquiv S₁ ℓ₁') (θ₁ : UnivalentStr S₁ ι₁)
           {S₂ : Type ℓ → Type ℓ₂} (ι₂ : StrEquiv S₂ ℓ₂') (θ₂ : UnivalentStr S₂ ι₂)
         → UnivalentStr (ProductStructure S₁ S₂) (ProductEquivStr ι₁ ι₂)
ProductUnivalentStr {S₁ = S₁} ι₁ θ₁ {S₂} ι₂ θ₂ {X , s₁ , s₂} {Y , t₁ , t₂} e =
  isoToEquiv (iso φ ψ η ε)
    where
    φ : ProductEquivStr ι₁ ι₂ (X , s₁ , s₂) (Y , t₁ , t₂) e
      → PathP (λ i → ProductStructure S₁ S₂ (ua e i)) (s₁ , s₂) (t₁ , t₂)
    φ (p , q) i = (θ₁ e .fst p i) , (θ₂ e .fst q i)

    ψ : PathP (λ i → ProductStructure S₁ S₂ (ua e i)) (s₁ , s₂) (t₁ , t₂)
      → ProductEquivStr ι₁ ι₂ (X , s₁ , s₂) (Y , t₁ , t₂) e
    ψ p = invEq (θ₁ e) (λ i → p i .fst) , invEq (θ₂ e) (λ i → p i .snd)

    η : section φ ψ
    η p i j = retEq (θ₁ e) (λ k → p k .fst) i j , retEq (θ₂ e) (λ k → p k .snd) i j

    ε : retract φ ψ
    ε (p , q) i = secEq (θ₁ e) p i , secEq (θ₂ e) q i

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
-- Andreas, 2017-01-12, issue #2386
-- Relaxing the constraints of BUILTIN EQUALITY

open import Agda.Primitive

postulate
  ℓ : Level
  A : Set ℓ
  a b : A
  P : A → Set

-- Level-polymorphic equality, living in the first universe

data _≡_ {a} {A : Set a} (x : A) : A → Set where
  instance refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

-- The type of primTrustMe has to match the flavor of EQUALITY

primitive primTrustMe : ∀ {a}{A : Set a} {x y : A} → x ≡ y

testTM : primTrustMe {x = a} {y = a} ≡ refl
testTM = refl

-- Testing rewrite

subst : a ≡ b → P a → P b
subst eq p rewrite eq = p

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --enable-prop #-}

open import Agda.Builtin.Nat

-- You can define datatypes in Prop, even with multiple constructors.
-- However, all constructors are considered (definitionally) equal.
data TestProp : Prop where
  p₁ p₂ : TestProp

-- Pattern matching on a datatype in Prop is disallowed unless the
-- target type is a Prop:
test-case : {P : Prop} (x₁ x₂ : P) → TestProp → P
test-case x₁ x₂ p₁ = x₁
test-case x₁ x₂ p₂ = x₂

-- All elements of a Prop are definitionally equal:
data _≡Prop_ {A : Prop} (x : A) : A → Set where
  refl : x ≡Prop x

p₁≡p₂ : p₁ ≡Prop p₂
p₁≡p₂ = refl

-- A special case are empty types in Prop: these can be eliminated to
-- any other type.
data ⊥ : Prop where

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

-- We can also define record types in Prop, such as the unit:
record ⊤ : Prop  where
  constructor tt

-- We have Prop : Set₀, so we can store predicates in a small datatype:
data NatProp : Set₁ where
  c : (Nat → Prop) → NatProp

-- To define more interesting predicates, we need to define them by pattern matching:
_≤_ : Nat → Nat → Prop
zero  ≤ y     = ⊤
suc x ≤ suc y = x ≤ y
_     ≤ _     = ⊥

-- We can also define the induction principle for predicates defined in this way,
-- using the fact that we can eliminate absurd propositions with a () pattern.
≤-ind : (P : (m n : Nat) → Set)
      → (pzy : (y : Nat) → P zero y)
      → (pss : (x y : Nat) → P x y → P (suc x) (suc y))
      → (m n : Nat) → m ≤ n → P m n
≤-ind P pzy pss zero y pf = pzy y
≤-ind P pzy pss (suc x) (suc y) pf = pss x y (≤-ind P pzy pss x y pf)
≤-ind P pzy pss (suc _) zero ()

-- We can define equality as a Prop, but (currently) we cannot define
-- the corresponding eliminator, so the equality is only useful for
-- refuting impossible equations.
data _≡P_ {A : Set} (x : A) : A → Prop where
  refl : x ≡P x

0≢1 : 0 ≡P 1 → ⊥
0≢1 ()

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
module bool where

------------------------
-- Datatypes
------------------------
data 𝔹 : Set where
  true  : 𝔹
  false : 𝔹

----------------------
-- AND
----------------------
infixr 6 _∧_
_∧_ : 𝔹 → 𝔹 → 𝔹
true  ∧ b  = b
false ∧ b = false

---------------------
-- OR
---------------------
infixr 5 _∨_
_∨_ : 𝔹 → 𝔹 → 𝔹
true  ∨ b = true
false ∨ b = b

--------------------
-- NEFATION
--------------------
infixr 7 ¬_
¬_ : 𝔹 → 𝔹
¬ true  = false
¬ false = true

max_stars_repo_name: mrLSD/agda-emacs

max_issues_repo_name: mrLSD/agda-emacs

max_forks_repo_name: mrLSD/agda-emacs


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

open import HoTT

module homotopy.EilenbergMacLane1 {i} (G : Group i) where
  private
    module G = Group G

    comp-equiv : ∀ g → G.El ≃ G.El
    comp-equiv g = equiv
      (λ x → G.comp x g)
      (λ x → G.comp x (G.inv g))
      (λ x → G.assoc x (G.inv g) g ∙ ap (G.comp x) (G.inv-l g) ∙ G.unit-r x)
      (λ x → G.assoc x g (G.inv g) ∙ ap (G.comp x) (G.inv-r g) ∙ G.unit-r x)

    comp-equiv-id : comp-equiv G.ident == ide G.El
    comp-equiv-id =
      pair= (λ= G.unit-r)
            (prop-has-all-paths-↓ {B = is-equiv})

    comp-equiv-comp : (g₁ g₂ : G.El) → comp-equiv (G.comp g₁ g₂)
                      == (comp-equiv g₂ ∘e comp-equiv g₁)
    comp-equiv-comp g₁ g₂ =
      pair= (λ= (λ x → ! (G.assoc x g₁ g₂)))
            (prop-has-all-paths-↓ {B = is-equiv})

    Ω-group : Group (lsucc i)
    Ω-group = Ω^S-group 0
      ⊙[ (0 -Type i) , (G.El , G.El-level) ]

    Codes-hom : G →ᴳ Ω-group
    Codes-hom = group-hom (nType=-out ∘ ua ∘ comp-equiv) pres-comp where
      abstract
        pres-comp : ∀ g₁ g₂
          → nType=-out {A = G.El , G.El-level} {B = G.El , G.El-level} (ua (comp-equiv (G.comp g₁ g₂)))
          == nType=-out {A = G.El , G.El-level} {B = G.El , G.El-level} (ua (comp-equiv g₁))
          ∙ nType=-out {A = G.El , G.El-level} {B = G.El , G.El-level} (ua (comp-equiv g₂))
        pres-comp g₁ g₂ =
          nType=-out {A = G.El , G.El-level} {B = G.El , G.El-level} (ua (comp-equiv (G.comp g₁ g₂)))
            =⟨ comp-equiv-comp g₁ g₂ |in-ctx nType=-out ∘ ua ⟩
          nType=-out {A = G.El , G.El-level} {B = G.El , G.El-level} (ua (comp-equiv g₂ ∘e comp-equiv g₁))
            =⟨ ua-∘e (comp-equiv g₁) (comp-equiv g₂) |in-ctx nType=-out ⟩
          nType=-out {A = G.El , G.El-level} {B = G.El , G.El-level} (ua (comp-equiv g₁) ∙ ua (comp-equiv g₂))
            =⟨ ! $ nType-∙ {A = G.El , G.El-level} {B = G.El , G.El-level} {C = G.El , G.El-level}
                  (ua (comp-equiv g₁)) (ua (comp-equiv g₂)) ⟩
          nType=-out {A = G.El , G.El-level} {B = G.El , G.El-level} (ua (comp-equiv g₁))
          ∙ nType=-out {A = G.El , G.El-level} {B = G.El , G.El-level} (ua (comp-equiv g₂))
            =∎

    Codes : EM₁ G → 0 -Type i
    Codes = EM₁-rec {G = G} {C = 0 -Type i}
                    (G.El , G.El-level)
                    Codes-hom

    abstract
      ↓-Codes-loop : ∀ g g' → g' == G.comp g' g [ fst ∘ Codes ↓ emloop g ]
      ↓-Codes-loop g g' =
        ↓-ap-out fst Codes (emloop g) $
        ↓-ap-out (idf _) fst (ap Codes (emloop g)) $
        transport (λ w → g' == G.comp g' g [ idf _ ↓ ap fst w ])
                  (! (EM₁Rec.emloop-β (G.El , G.El-level) Codes-hom g)) $
        transport (λ w → g' == G.comp g' g [ idf _ ↓ w ])
                  (! (fst=-β (ua $ comp-equiv g) _)) $
        ↓-idf-ua-in (comp-equiv g) idp

    encode : {x : EM₁ G} → embase == x → fst (Codes x)
    encode α = transport (fst ∘ Codes) α G.ident

    encode-emloop : ∀ g → encode (emloop g) == g
    encode-emloop g = to-transp $
      transport (λ x → G.ident == x [ fst ∘ Codes ↓ emloop g ])
                 (G.unit-l g) (↓-Codes-loop g G.ident)

    decode : {x : EM₁ G} → fst (Codes x) → embase == x
    decode {x} =
      EM₁-elim {P = λ x' → fst (Codes x') → embase == x'}
        emloop
        loop'
        (λ _ _ → prop-has-all-paths-↓ {{↓-level ⟨⟩}})
        x
      where
      loop' : (g : G.El)
        → emloop == emloop [ (λ x' → fst (Codes x') → embase == x') ↓ emloop g ]
      loop' g = ↓-→-from-transp $ λ= $ λ y →
        transport (λ z → embase == z) (emloop g) (emloop y)
          =⟨ transp-cst=idf (emloop g) (emloop y) ⟩
        emloop y ∙ emloop g
          =⟨ ! (emloop-comp y g) ⟩
        emloop (G.comp y g)
          =⟨ ap emloop (! (to-transp (↓-Codes-loop g y))) ⟩
        emloop (transport (λ z → fst (Codes z)) (emloop g) y) =∎

    decode-encode : ∀ {x} (α : embase' G == x) → decode (encode α) == α
    decode-encode idp = emloop-ident {G = G}

    emloop-equiv : G.El ≃ (embase' G == embase)
    emloop-equiv = equiv emloop encode decode-encode encode-emloop

  Ω¹-EM₁ : Ω^S-group 0 (⊙EM₁ G) ≃ᴳ G
  Ω¹-EM₁ = ≃-to-≃ᴳ (emloop-equiv ⁻¹)
    (λ l₁ l₂ → <– (ap-equiv emloop-equiv _ _) $
      emloop (encode (l₁ ∙ l₂))
        =⟨ decode-encode (l₁ ∙ l₂) ⟩
      l₁ ∙ l₂
        =⟨ ! $ ap2 _∙_ (decode-encode l₁) (decode-encode l₂) ⟩
      emloop (encode l₁) ∙ emloop (encode l₂)
        =⟨ ! $ emloop-comp (encode l₁) (encode l₂) ⟩
      emloop (G.comp (encode l₁) (encode l₂))
        =∎)

  π₁-EM₁ : πS 0 (⊙EM₁ G) ≃ᴳ G
  π₁-EM₁ = Ω¹-EM₁ ∘eᴳ unTrunc-iso (Ω^S-group-structure 0 (⊙EM₁ G))

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
import Level as L
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import RevMachine

module RevNoRepeat {ℓ} (M : RevMachine {ℓ}) where
  infix  99 _ᵣₑᵥ
  infixr 10 _∷_
  infixr 10 _++↦_
  open RevMachine.RevMachine M

  is-stuck : State → Set _
  is-stuck st = ∄[ st' ] (st ↦ st')

  is-initial : State → Set _
  is-initial st = ∄[ st' ] (st' ↦ st)

  data _↦ᵣₑᵥ_ : State → State → Set (L.suc ℓ) where
    _ᵣₑᵥ : ∀ {st₁ st₂} → st₁ ↦ st₂ → st₂ ↦ᵣₑᵥ st₁

  data _↦*_ : State → State → Set (L.suc ℓ) where
    ◾ : {st : State} → st ↦* st
    _∷_ : {st₁ st₂ st₃ : State} → st₁ ↦ st₂ → st₂ ↦* st₃ → st₁ ↦* st₃

  _++↦_ : {st₁ st₂ st₃ : State} → st₁ ↦* st₂ → st₂ ↦* st₃ → st₁ ↦* st₃
  ◾ ++↦ st₁↦*st₂ = st₁↦*st₂
  (st₁↦st₁' ∷ st₁'↦*st₂) ++↦ st₂'↦*st₃ = st₁↦st₁' ∷ (st₁'↦*st₂ ++↦ st₂'↦*st₃)

  len↦ : ∀ {st st'} → st ↦* st' → ℕ
  len↦ ◾ = 0
  len↦ (_ ∷ r) = 1 + len↦ r

  data _↦ᵣₑᵥ*_ : State → State → Set (L.suc ℓ) where
    ◾ : ∀ {st} → st ↦ᵣₑᵥ* st
    _∷_ : ∀ {st₁ st₂ st₃} → st₁ ↦ᵣₑᵥ st₂ → st₂ ↦ᵣₑᵥ* st₃ → st₁ ↦ᵣₑᵥ* st₃

  _++↦ᵣₑᵥ_ : ∀ {st₁ st₂ st₃} → st₁ ↦ᵣₑᵥ* st₂ → st₂ ↦ᵣₑᵥ* st₃ → st₁ ↦ᵣₑᵥ* st₃
  ◾ ++↦ᵣₑᵥ st₁↦ᵣₑᵥ*st₂ = st₁↦ᵣₑᵥ*st₂
  (st₁↦ᵣₑᵥst₁' ∷ st₁'↦ᵣₑᵥ*st₂) ++↦ᵣₑᵥ st₂'↦ᵣₑᵥ*st₃ = st₁↦ᵣₑᵥst₁' ∷ (st₁'↦ᵣₑᵥ*st₂ ++↦ᵣₑᵥ st₂'↦ᵣₑᵥ*st₃)

  Rev↦ : ∀ {st₁ st₂} → st₁ ↦* st₂ → st₂ ↦ᵣₑᵥ* st₁
  Rev↦ ◾ = ◾
  Rev↦ (r ∷ rs) = Rev↦ rs ++↦ᵣₑᵥ ((r ᵣₑᵥ) ∷ ◾)

  Rev↦ᵣₑᵥ : ∀ {st₁ st₂} → st₁ ↦ᵣₑᵥ* st₂ → st₂ ↦* st₁
  Rev↦ᵣₑᵥ ◾ = ◾
  Rev↦ᵣₑᵥ ((r ᵣₑᵥ) ∷ rs) = Rev↦ᵣₑᵥ rs ++↦ (r ∷ ◾)

  deterministic* : ∀ {st st₁ st₂} → st ↦* st₁ → st ↦* st₂
                 → is-stuck st₁ → is-stuck st₂
                 → st₁ ≡ st₂
  deterministic* ◾ ◾ stuck₁ stuck₂ = refl
  deterministic* ◾ (r ∷ ↦*₂) stuck₁ stuck₂ = ⊥-elim (stuck₁ (_ , r))
  deterministic* (r ∷ ↦*₁) ◾ stuck₁ stuck₂ = ⊥-elim (stuck₂ (_ , r))
  deterministic* (r₁ ∷ ↦*₁) (r₂ ∷ ↦*₂) stuck₁ stuck₂ with deterministic r₁ r₂
  ... | refl = deterministic* ↦*₁ ↦*₂ stuck₁ stuck₂

  deterministic*' : ∀ {st st₁ st'} → (rs₁ : st ↦* st₁) → (rs : st ↦* st')
                  → is-stuck st'
                  → Σ[ rs' ∈ st₁ ↦* st' ] (len↦ rs ≡ len↦ rs₁ + len↦ rs')
  deterministic*' ◾ rs stuck = rs , refl
  deterministic*' (r ∷ rs₁) ◾ stuck = ⊥-elim (stuck (_ , r))
  deterministic*' (r ∷ rs₁) (r' ∷ rs) stuck with deterministic r r'
  ... | refl with deterministic*' rs₁ rs stuck
  ... | (rs' , eq) = rs' , cong suc eq

  deterministicᵣₑᵥ* : ∀ {st st₁ st₂} → st ↦ᵣₑᵥ* st₁ → st ↦ᵣₑᵥ* st₂
                    → is-initial st₁ → is-initial st₂
                    → st₁ ≡ st₂
  deterministicᵣₑᵥ* ◾ ◾ initial₁ initial₂ = refl
  deterministicᵣₑᵥ* ◾ (r ᵣₑᵥ ∷ ↦ᵣₑᵥ*₂) initial₁ initial₂ = ⊥-elim (initial₁ (_ , r))
  deterministicᵣₑᵥ* (r ᵣₑᵥ ∷ ↦ᵣₑᵥ*₁) ◾ initial₁ initial₂ = ⊥-elim (initial₂ (_ , r))
  deterministicᵣₑᵥ* (r₁ ᵣₑᵥ ∷ ↦ᵣₑᵥ*₁) (r₂ ᵣₑᵥ ∷ ↦ᵣₑᵥ*₂) initial₁ initial₂ with deterministicᵣₑᵥ r₁ r₂
  ... | refl = deterministicᵣₑᵥ* ↦ᵣₑᵥ*₁ ↦ᵣₑᵥ*₂ initial₁ initial₂

  data _↦[_]_ : State → ℕ → State → Set (L.suc ℓ) where
    ◾ : ∀ {st} → st ↦[ 0 ] st
    _∷_ : ∀ {st₁ st₂ st₃ n} → st₁ ↦ st₂ → st₂ ↦[ n ] st₃ → st₁ ↦[ suc n ] st₃

  _++↦ⁿ_ : ∀ {st₁ st₂ st₃ n m} → st₁ ↦[ n ] st₂ → st₂ ↦[ m ] st₃ → st₁ ↦[ n + m ] st₃
  ◾ ++↦ⁿ st₁↦*st₂ = st₁↦*st₂
  (st₁↦st₁' ∷ st₁'↦*st₂) ++↦ⁿ st₂'↦*st₃ = st₁↦st₁' ∷ (st₁'↦*st₂ ++↦ⁿ st₂'↦*st₃)

  data _↦ᵣₑᵥ[_]_ : State → ℕ → State → Set (L.suc ℓ) where
    ◾ : ∀ {st} → st ↦ᵣₑᵥ[ 0 ] st
    _∷_ : ∀ {st₁ st₂ st₃ n} → st₁ ↦ᵣₑᵥ st₂ → st₂ ↦ᵣₑᵥ[ n ] st₃ → st₁ ↦ᵣₑᵥ[ suc n ] st₃

  _++↦ᵣₑᵥⁿ_ : ∀ {st₁ st₂ st₃ n m} → st₁ ↦ᵣₑᵥ[ n ] st₂ → st₂ ↦ᵣₑᵥ[ m ] st₃ → st₁ ↦ᵣₑᵥ[ n + m ] st₃
  ◾ ++↦ᵣₑᵥⁿ st₁↦*st₂ = st₁↦*st₂
  (st₁↦st₁' ∷ st₁'↦*st₂) ++↦ᵣₑᵥⁿ st₂'↦*st₃ = st₁↦st₁' ∷ (st₁'↦*st₂ ++↦ᵣₑᵥⁿ st₂'↦*st₃)

  deterministicⁿ : ∀ {st st₁ st₂ n} → st ↦[ n ] st₁ → st ↦[ n ] st₂
                 → st₁ ≡ st₂
  deterministicⁿ ◾ ◾ = refl
  deterministicⁿ (r₁ ∷ rs₁) (r₂ ∷ rs₂) with deterministic r₁ r₂
  ... | refl = deterministicⁿ rs₁ rs₂

  deterministicᵣₑᵥⁿ : ∀ {st st₁ st₂ n} → st ↦ᵣₑᵥ[ n ] st₁ → st ↦ᵣₑᵥ[ n ] st₂
                 → st₁ ≡ st₂
  deterministicᵣₑᵥⁿ ◾ ◾ = refl
  deterministicᵣₑᵥⁿ (r₁ ᵣₑᵥ ∷ rs₁) (r₂ ᵣₑᵥ ∷ rs₂) with deterministicᵣₑᵥ r₁ r₂
  ... | refl = deterministicᵣₑᵥⁿ rs₁ rs₂

  private
    split↦ⁿ : ∀ {st st'' n m} → st ↦ᵣₑᵥ[ n + m ] st''
            → ∃[ st' ] (st ↦ᵣₑᵥ[ n ] st' × st' ↦ᵣₑᵥ[ m ] st'')
    split↦ⁿ {n = 0} {m} rs = _ , ◾ , rs
    split↦ⁿ {n = suc n} {m} (r ∷ rs) with split↦ⁿ {n = n} {m} rs
    ... | st' , st↦ⁿst' , st'↦ᵐst'' = st' , (r ∷ st↦ⁿst') , st'↦ᵐst''

    diff : ∀ {n m} → n < m → ∃[ k ] (0 < k × n + k ≡ m)
    diff {0} {(suc m)} (s≤s z≤n) = suc m , s≤s z≤n , refl
    diff {(suc n)} {(suc (suc m))} (s≤s (s≤s n≤m)) with diff {n} {suc m} (s≤s n≤m)
    ... | k , 0<k , eq = k , 0<k , cong suc eq

  Revⁿ : ∀ {st st' n} → st ↦[ n ] st' → st' ↦ᵣₑᵥ[ n ] st
  Revⁿ {n = 0} ◾ = ◾
  Revⁿ {n = suc n} (r ∷ rs) rewrite +-comm 1 n = Revⁿ rs ++↦ᵣₑᵥⁿ (r ᵣₑᵥ ∷ ◾)

  NoRepeat : ∀ {st₀ stₙ stₘ n m}
           → is-initial st₀
           → n < m
           → st₀ ↦[ n ] stₙ
           → st₀ ↦[ m ] stₘ
           → stₙ ≢ stₘ
  NoRepeat {stₙ = st} {_} {m} st₀-is-init n<m st₀↦ᵐst st₀↦ᵐ⁺ᵏ⁺¹st refl with diff n<m
  ... | suc k , 0<k , refl with (Revⁿ st₀↦ᵐst , Revⁿ st₀↦ᵐ⁺ᵏ⁺¹st)
  ... | st'↦ᵐst₀' , st'↦ᵐ⁺ᵏ⁺¹st₀' with split↦ⁿ {n = m} {suc k} st'↦ᵐ⁺ᵏ⁺¹st₀'
  ... | st′ , st'↦ᵐst′ , st′↦ᵏ⁺¹st₀' with deterministicᵣₑᵥⁿ st'↦ᵐst₀' st'↦ᵐst′
  ... | refl with st′↦ᵏ⁺¹st₀'
  ... | r ᵣₑᵥ ∷ rs = ⊥-elim (st₀-is-init (_ , r))


text:
------------------------------------------------------------------------------
-- Distributive laws on a binary operation: Lemma 6
------------------------------------------------------------------------------

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

module DistributiveLaws.Lemma6-ATP where

open import DistributiveLaws.Base

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

postulate
  lemma₆ : ∀ u x y z →
           (((x · y) · (z · u)) · ((x · y) · (z · u))) ≡ (x · y) · (z · u)
{-# ATP prove lemma₆ #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Categories.Category.Instance.Properties.Setoids.LCCC where

open import Level
open import Data.Product using (Σ; _,_)
open import Function.Equality as Func using (Π; _⟶_)
open import Relation.Binary using (Setoid)
import Relation.Binary.PropositionalEquality as ≡

open import Categories.Category
open import Categories.Category.Slice
open import Categories.Category.Slice.Properties
open import Categories.Category.CartesianClosed
open import Categories.Category.CartesianClosed.Canonical
  using (module Equivalence)
  renaming (CartesianClosed to Canonical)
open import Categories.Category.CartesianClosed.Locally using (Locally)
open import Categories.Category.Cartesian
open import Categories.Category.Instance.Span
open import Categories.Category.Instance.Setoids
open import Categories.Category.Instance.Properties.Setoids.Complete
open import Categories.Category.Monoidal.Instance.Setoids
open import Categories.Functor

open import Categories.Object.Terminal
open import Categories.Diagram.Pullback
open import Categories.Diagram.Pullback.Limit
import Categories.Object.Product as Prod

open Π using (_⟨$⟩_)

module _ {o ℓ} where

  module _ {A X : Setoid o ℓ} where
    private
      module A = Setoid A
      module X = Setoid X

    record InverseImage (a : Setoid.Carrier A) (f : X ⟶ A) : Set (o ⊔ ℓ) where
      constructor pack

      field
        x    : X.Carrier
        fx≈a : f ⟨$⟩ x A.≈ a

    inverseImage-transport : ∀ {a a′} {f : X ⟶ A} → a A.≈ a′ → InverseImage a f → InverseImage a′ f
    inverseImage-transport eq img = pack x (A.trans fx≈a eq)
      where open InverseImage img

  module _ {A X Y : Setoid o ℓ} where
    private
      module A = Setoid A
      module X = Setoid X
      module Y = Setoid Y

    -- the inverse image part of an exponential object the slice category of Setoids
    -- it's a morphism from f to g, which in set theory is
    --   f⁻¹(a) ⟶ g⁻¹(a)
    -- here, we need to take care of some coherence condition.
    record InverseImageMap (a : Setoid.Carrier A)
                           (f : X ⟶ A)
                           (g : Y ⟶ A) : Set (o ⊔ ℓ) where
      field
        f⇒g  : InverseImage a f → InverseImage a g
        cong : ∀ (x x′ : InverseImage a f) →
                 InverseImage.x x X.≈ InverseImage.x x′ →
                 InverseImage.x (f⇒g x) Y.≈ InverseImage.x (f⇒g x′)

    inverseImageMap-transport : ∀ {a a′} {f : X ⟶ A} {g : Y ⟶ A} → a A.≈ a′ →
                                  InverseImageMap a f g → InverseImageMap a′ f g
    inverseImageMap-transport eq h = record
      { f⇒g  = λ img → inverseImage-transport eq (f⇒g (inverseImage-transport (A.sym eq) img))
      ; cong = λ x x′ eq′ → cong (inverseImage-transport (A.sym eq) x) (inverseImage-transport (A.sym eq) x′) eq′
      }
      where open InverseImageMap h

    record SlExp (f : X ⟶ A)
                 (g : Y ⟶ A) : Set (o ⊔ ℓ) where

      field
        idx : A.Carrier
        map : InverseImageMap idx f g

      open InverseImageMap map public

    record SlExp≈ {f : X ⟶ A}
                  {g : Y ⟶ A}
                  (h i : SlExp f g) : Set (o ⊔ ℓ) where
      private
        module h = SlExp h
        module i = SlExp i

      field
        idx≈  : h.idx A.≈ i.idx
        map≈  : ∀ (img : InverseImage h.idx f) → InverseImage.x (h.f⇒g img) Y.≈ InverseImage.x (i.f⇒g (inverseImage-transport idx≈ img))
        -- map≈′ : ∀ (img : InverseImage i.idx f) → InverseImage.x (i.f⇒g img) Y.≈ InverseImage.x (h.f⇒g (inverseImage-transport idx≈ img))

  SlExp-Setoid : ∀ {A X Y : Setoid o ℓ}
                   (f : X ⟶ A) (g : Y ⟶ A) → Setoid (o ⊔ ℓ) (o ⊔ ℓ)
  SlExp-Setoid {A} {X} {Y} f g = record
    { Carrier       = SlExp f g
    ; _≈_           = SlExp≈
    ; isEquivalence = record
      { refl  = λ {h} → record
        { idx≈ = A.refl
        ; map≈ = λ img → SlExp.cong h img (inverseImage-transport A.refl img) X.refl
        }
      ; sym   = λ {h i} eq →
        let open SlExp≈ eq
        in record
        { idx≈ = A.sym idx≈
        ; map≈ = λ img → Y.trans (SlExp.cong i img (inverseImage-transport idx≈ (inverseImage-transport (A.sym idx≈) img)) X.refl)
                                 (Y.sym (map≈ (inverseImage-transport (A.sym idx≈) img)))
        }
      ; trans = λ {h i j} eq eq′ →
        let module eq = SlExp≈ eq
            module eq′ = SlExp≈ eq′
        in record
        { idx≈ = A.trans eq.idx≈ eq′.idx≈
        ; map≈ = λ img → Y.trans  (eq.map≈ img)
                         (Y.trans (eq′.map≈ (inverseImage-transport eq.idx≈ img))
                                  (SlExp.cong j (inverseImage-transport eq′.idx≈ (inverseImage-transport eq.idx≈ img))
                                                (inverseImage-transport (A.trans eq.idx≈ eq′.idx≈) img)
                                                X.refl))
        }
      }
    }
    where module A = Setoid A
          module X = Setoid X
          module Y = Setoid Y

module _ {o} where
  private
    S : Category (suc o) o o
    S = Setoids o o

    module S = Category S

    module _ (A : S.Obj) where
      private
        Sl = Slice S A
        module Sl = Category Sl

      open Setoid A
      open Prod (Slice S A)

      slice-terminal : Terminal Sl
      slice-terminal = record
        { ⊤             = sliceobj {Y = A} record
          { _⟨$⟩_ = λ x → x
          ; cong  = λ eq → eq
          }
        ; ⊤-is-terminal = record
          { !        = λ { {sliceobj f} → slicearr {h = f} (Π.cong f) }
          ; !-unique = λ { {X} (slicearr △) eq →
                         let module X = SliceObj X
                         in sym (△ (Setoid.sym X.Y eq)) }
          }
        }

      F₀ : Sl.Obj → Sl.Obj → SpanObj → Setoid o o
      F₀ X Y center = A
      F₀ X Y left   = SliceObj.Y X
      F₀ X Y right  = SliceObj.Y Y

      slice-product : (X Y : Sl.Obj) → Product X Y
      slice-product X Y = pullback⇒product S XY-pullback
        where module X = SliceObj X
              module Y = SliceObj Y

              F : Functor (Category.op Span) (Setoids o o)
              F = record
                { F₀           = F₀ X Y
                ; F₁           = λ { span-id   → Func.id
                                   ; span-arrˡ → X.arr
                                   ; span-arrʳ → Y.arr
                                   }
                ; identity     = λ {Z} → S.Equiv.refl {F₀ X Y Z} {F₀ X Y Z} {Func.id}
                ; homomorphism = λ { {_} {_} {_} {span-id}   {span-id}   eq → eq
                                   ; {_} {_} {_} {span-id}   {span-arrˡ}    → Π.cong X.arr
                                   ; {_} {_} {_} {span-id}   {span-arrʳ}    → Π.cong Y.arr
                                   ; {_} {_} {_} {span-arrˡ} {span-id}      → Π.cong X.arr
                                   ; {_} {_} {_} {span-arrʳ} {span-id}      → Π.cong Y.arr
                                   }
                ; F-resp-≈     = λ { {_} {_} {span-id}   ≡.refl eq → eq
                                   ; {_} {_} {span-arrˡ} ≡.refl    → Π.cong X.arr
                                   ; {_} {_} {span-arrʳ} ≡.refl    → Π.cong Y.arr
                                   }
                }

              XY-pullback : Pullback S X.arr Y.arr
              XY-pullback = limit⇒pullback S {F = F} (Setoids-Complete 0ℓ 0ℓ 0ℓ o o F)

      module slice-terminal = Terminal slice-terminal
      module slice-product X Y = Product (slice-product X Y)

      cartesian : Cartesian Sl
      cartesian = record
        { terminal = slice-terminal
        ; products = record
          { product = slice-product _ _
          }
        }

      module cartesian = Cartesian cartesian

      _^_ : Sl.Obj → Sl.Obj → Sl.Obj
      f ^ g = sliceobj {Y = SlExp-Setoid g.arr f.arr} record
        { _⟨$⟩_ = SlExp.idx
        ; cong  = SlExp≈.idx≈
        }
        where module f = SliceObj f
              module g = SliceObj g

      prod = slice-product.A×B

      eval : {f g : Sl.Obj} → prod (f ^ g) g Sl.⇒ f
      eval {f} {g} = slicearr {h = h} λ { {J₁ , arr₁} {J₂ , arr₂} eq →
        let open SlExp (J₁ left)
        in trans (InverseImage.fx≈a (f⇒g (pack (J₁ right) _)))
          (trans (arr₁ span-arrˡ)
          (trans (eq center)
                 (sym (arr₂ span-arrʳ)))) }
        where module f  = SliceObj f
              module g  = SliceObj g
              module fY = Setoid f.Y

              h : SliceObj.Y (prod (f ^ g) g) S.⇒ f.Y
              h = record
                { _⟨$⟩_ = λ { (J , arr) →
                  let module exp = SlExp (J left)
                  in InverseImage.x (exp.f⇒g (pack (J right) (trans (arr span-arrʳ) (sym (arr span-arrˡ))))) }
                ; cong  = λ { {J₁ , arr₁} {J₂ , arr₂} eq →
                  let open SlExp≈ (eq left)
                      open SlExp (J₂ left)
                  in fY.trans (map≈ _) (cong _ _ (eq right)) }
                }

      module _ {f g : Sl.Obj} where
        private
          module f  = SliceObj f
          module g  = SliceObj g
          module fY = Setoid f.Y
          module gY = Setoid g.Y

        Jpb : ∀ x → InverseImage (f.arr ⟨$⟩ x) g.arr → ∀ j → Setoid.Carrier (F₀ f g j)
        Jpb x img center = f.arr ⟨$⟩ x
        Jpb x img left   = x
        Jpb x img right  = InverseImage.x img

        xypb : ∀ x → InverseImage (f.arr ⟨$⟩ x) g.arr → Setoid.Carrier (SliceObj.Y (prod f g))
        xypb x img = Jpb x img
                   , λ { {center} span-id → refl
                       ; {left} span-id   → fY.refl
                       ; {right} span-id  → gY.refl
                       ; span-arrˡ        → refl
                       ; span-arrʳ        → fx≈a }
          where open InverseImage img renaming (x to y)

        module _ {h : Sl.Obj} (α : prod f g Sl.⇒ h) where
          private
            module α  = Slice⇒ α
            module h  = SliceObj h
            module hY = Setoid h.Y

            βmap : fY.Carrier → SlExp g.arr h.arr
            βmap x = record
              { idx = f.arr ⟨$⟩ x
              ; map = record
                { f⇒g  = λ img →
                  let open InverseImage img renaming (x to y)
                  in pack (α.h ⟨$⟩ xypb x img)
                          (trans (α.△ {xypb x img} {xypb x img} (Setoid.refl (SliceObj.Y (prod f g)) {xypb x img}))
                                 fx≈a)
                ; cong = λ img img′ eq →
                  let module img  = InverseImage img
                      module img′ = InverseImage img′
                  in Π.cong α.h λ { center → refl
                                  ; left   → fY.refl
                                  ; right  → eq }
                }
              }

            βcong : {i j : fY.Carrier} → i fY.≈ j → SlExp≈ (βmap i) (βmap j)
            βcong {i} {j} eq = record
              { idx≈ = Π.cong f.arr eq
              ; map≈ = λ img →
                let open InverseImage img
                in Π.cong α.h λ { center → Π.cong f.arr eq
                                ; left   → eq
                                ; right  → gY.refl }
              }

            β : f.Y S.⇒ SliceObj.Y (h ^ g)
            β = record
              { _⟨$⟩_ = βmap
              ; cong  = βcong
              }

          curry : f Sl.⇒ (h ^ g)
          curry = slicearr {h = β} (Π.cong f.arr)

      module _ {f g h : Sl.Obj} {α β : prod f g Sl.⇒ h} where
        private
          module f  = SliceObj f
          module g  = SliceObj g
          module gY = Setoid g.Y

        curry-resp-≈ : α Sl.≈ β → curry α Sl.≈ curry β
        curry-resp-≈ eq eq′ = record
          { idx≈ = Π.cong f.arr eq′
          ; map≈ = λ img →
            let open InverseImage img
            in eq λ { center → Π.cong f.arr eq′
                    ; left   → eq′
                    ; right  → gY.refl }
          }

      module _ {f g h : Sl.Obj} {α : f Sl.⇒ (g ^ h)} {β : prod f h Sl.⇒ g} where
        private
          module f  = SliceObj f
          module g  = SliceObj g
          module h  = SliceObj h
          module α  = Slice⇒ α
          module β  = Slice⇒ β
          module fY = Setoid f.Y
          module gY = Setoid g.Y
          module hY = Setoid h.Y

        curry-unique : eval Sl.∘ (α cartesian.⁂ Sl.id) Sl.≈ β → α Sl.≈ curry β
        curry-unique eq {z} {w} eq′ = record
          { idx≈ = α.△ eq′
          ; map≈ = λ img →
            let open InverseImage img
            in gY.trans (InverseImageMap.cong (SlExp.map (α.h ⟨$⟩ z)) img _ hY.refl)
                        (eq {xypb z (inverseImage-transport (trans (α.△ eq′) (Π.cong f.arr (fY.sym eq′))) img)}
                            {xypb w (inverseImage-transport (α.△ eq′) img)}
                            λ { center → Π.cong f.arr eq′
                              ; left   → eq′
                              ; right  → hY.refl })
          }

      slice-canonical : Canonical Sl
      slice-canonical = record
        { ⊤            = slice-terminal.⊤
        ; _×_          = slice-product.A×B
        ; !            = slice-terminal.!
        ; π₁           = slice-product.π₁ _ _
        ; π₂           = slice-product.π₂ _ _
        ; ⟨_,_⟩        = slice-product.⟨_,_⟩ _ _
        ; !-unique     = slice-terminal.!-unique
        ; π₁-comp      = λ {_ _ f _ g} → slice-product.project₁ _ _ {_} {f} {g}
        ; π₂-comp      = λ {_ _ f _ g} → slice-product.project₂ _ _ {_} {f} {g}
        ; ⟨,⟩-unique   = λ {_ _ _ f g h} → slice-product.unique _ _ {_} {h} {f} {g}
        ; _^_          = _^_
        ; eval         = eval
        ; curry        = curry
        ; eval-comp    = λ { {_} {_} {_} {α} {J , arr₁} eq →
          let module α = Slice⇒ α
          in Π.cong α.h λ { center → trans (arr₁ span-arrˡ) (eq center)
                          ; left   → eq left
                          ; right  → eq right } }
        ; curry-resp-≈ = λ {_ _ _} {α β} → curry-resp-≈ {_} {_} {_} {α} {β}
        ; curry-unique = λ {_ _ _} {α β} → curry-unique {_} {_} {_} {α} {β}
        }

      Setoids-sliceCCC : CartesianClosed (Slice S A)
      Setoids-sliceCCC = Equivalence.fromCanonical (Slice S A) slice-canonical

  Setoids-LCCC : Locally S
  Setoids-LCCC = record
    { sliceCCC = Setoids-sliceCCC
    }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

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

-- This module defines and abstract view if a system, encompassing only a predicate for Records,
-- another for Votes and a proof that, if a Vote is included in a QC in the system, then and
-- equivalent Vote is also in the system.  It further defines a notion "Complete", which states that
-- if an honest vote is included in a QC in the system, then there is a RecordChain up to the block
-- that the QC extends, such that all Records in the RecordChain are also in the system.  The latter
-- property is used to extend correctness conditions on RecordChains to correctness conditions that
-- require only a short suffix of a RecordChain.

module LibraBFT.Abstract.System
    (UID    : Set)
    (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁))
    (NodeId : Set)
    (𝓔 : EpochConfig UID NodeId)
    (𝓥 : VoteEvidence UID NodeId 𝓔)
  where

  open import LibraBFT.Abstract.Types           UID        NodeId 𝓔
  open import LibraBFT.Abstract.Records         UID _≟UID_ NodeId 𝓔 𝓥
  open import LibraBFT.Abstract.Records.Extends UID _≟UID_ NodeId 𝓔 𝓥
  open import LibraBFT.Abstract.RecordChain     UID _≟UID_ NodeId 𝓔 𝓥

  module All-InSys-props {ℓ}(InSys : Record → Set ℓ) where

    All-InSys : ∀ {o r} → RecordChainFrom o r → Set ℓ
    All-InSys rc = {r' : Record} → r' ∈RC-simple rc → InSys r'

    All-InSys⇒last-InSys : ∀ {r} → {rc : RecordChain r} → All-InSys rc → InSys r
    All-InSys⇒last-InSys {rc = empty} a∈s = a∈s here
    All-InSys⇒last-InSys {r = r'} {step {r' = .r'} rc ext} a∈s = a∈s here

    All-InSys-unstep : ∀ {o r r' rc ext } → All-InSys (step {o} {r} {r'} rc ext) → All-InSys rc
    All-InSys-unstep {ext = ext} a∈s r'∈RC = a∈s (there ext r'∈RC)

    All-InSys-step : ∀ {r r' }{rc : RecordChain r}
                   → All-InSys rc → (ext : r ← r') → InSys r'
                   → All-InSys (step rc ext)
    All-InSys-step hyp ext r here = r
    All-InSys-step hyp ext r (there .ext r∈rc) = hyp r∈rc

  -- We say an InSys predicate is /Complete/ when we can construct a record chain
  -- from any vote by an honest participant. This essentially says that whenever
  -- an honest participant casts a vote, they have checked that the voted-for
  -- block is in a RecordChain whose records are all in the system.  This notion
  -- is used to extend correctness conditions on RecordChains to correctness conditions that
  -- require only a short suffix of a RecordChain.
  Complete : ∀{ℓ} → (Record → Set ℓ) → Set ℓ
  Complete ∈sys = ∀{α q}
                → Meta-Honest-Member α
                → α ∈QC q
                → ∈sys (Q q)
                → ∃[ b ] ( Σ (RecordChain (B b)) All-InSys
                         × B b ← Q q)
    where open All-InSys-props ∈sys

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
-- {-# OPTIONS --verbose tc.constr.findInScope:15 #-}

module 01-arguments where

data T : Set where
  tt : T

data A : Set where
  mkA : A
  mkA2 : T → A

giveA : ⦃ a : A ⦄ → A
giveA {{a}} = a

test : A → T
test a = tt

test2 : T
test2 = test giveA

id : {A : Set} → A → A
id v = v

test5 : T → T
test5 = id

⋯ : {A : Set} → {{a : A}} → A
⋯ {{a}} = a

--giveA' : {{a : A}} → A
--giveA' = ⋯

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Generics.Desc where

open import Data.String using (String)
open import Generics.Prelude hiding (lookup)
open import Generics.Telescope

private
  variable
    P   : Telescope ⊤
    V I : ExTele P
    p   : ⟦ P ⟧tel tt
    ℓ   : Level
    n   : ℕ

data ConDesc (P : Telescope ⊤) (V I : ExTele P) : Setω where
  var : (((p , v) : ⟦ P , V ⟧xtel) → ⟦ I ⟧tel p) → ConDesc P V I
  π   : (ai : String × ArgInfo)
        (S : ⟦ P , V ⟧xtel → Set ℓ)
        (C : ConDesc P (V ⊢< ai > S) I)
      → ConDesc P V I
  _⊗_ : (A B : ConDesc P V I) → ConDesc P V I

data DataDesc P (I : ExTele P) : ℕ → Setω where
  []  : DataDesc P I 0
  _∷_ : ∀ {n} (C : ConDesc P ε I) (D : DataDesc P I n) → DataDesc P I (suc n)

lookupCon : DataDesc P I n → Fin n → ConDesc P ε I
lookupCon (C ∷ D) (zero ) = C
lookupCon (C ∷ D) (suc k) = lookupCon D k

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

⟦_⟧IndArg : (C : ConDesc P V I)
          → (⟦ P , I ⟧xtel → Set ℓ)
          → (⟦ P , V ⟧xtel → Set (levelIndArg C ℓ))
⟦ var f    ⟧IndArg X (p , v) = X (p , f (p , v))
⟦ π ai S C ⟧IndArg X (p , v) = Π< ai > (S (p , v)) (λ s → ⟦ C ⟧IndArg X (p , v , s))
⟦ A ⊗ B    ⟧IndArg X pv      = ⟦ A ⟧IndArg X pv × ⟦ B ⟧IndArg X pv

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

⟦_⟧Con : (C : ConDesc P V I)
       → (⟦ P , I     ⟧xtel → Set ℓ)
       → (⟦ P , V & I ⟧xtel → Set (levelCon C ℓ))
⟦ var f    ⟧Con X (p , v , i) = i ≡ f (p , v)
⟦ π (n , ai) S C ⟧Con X (p , v , i) = Σ[ s ∈ < relevance ai > S (p , v) ] ⟦ C ⟧Con X (p , ((v , s) , i))
⟦ A ⊗ B    ⟧Con X pvi@(p , v , i) = ⟦ A ⟧IndArg X (p , v) × ⟦ B ⟧Con X pvi

record Σℓω {a} (A : Set a) {ℓB : A → Level} (B : ∀ x → Set (ℓB x)) : Setω where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

⟦_⟧Data : DataDesc P I n → (⟦ P , I ⟧xtel → Set ℓ) → ⟦ P , I ⟧xtel → Setω
⟦_⟧Data {n = n} D X (p , i) = Σℓω (Fin n) (λ k → ⟦ lookupCon D k ⟧Con X (p , tt , i))

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Floats: basic types and operations
------------------------------------------------------------------------

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

module Data.Float.Base where

open import Relation.Binary.Core using (Rel)
import Data.Word.Base as Word
open import Function using (_on_)
open import Agda.Builtin.Equality

------------------------------------------------------------------------
-- Re-export built-ins publically

open import Agda.Builtin.Float public
  using (Float)
  renaming
  -- Relations
  ( primFloatEquality          to _≡ᵇ_
  ; primFloatLess              to _≤ᵇ_
  ; primFloatNumericalEquality to _≈ᵇ_
  ; primFloatNumericalLess     to _≲ᵇ_
  -- Conversions
  ; primShowFloat     to show
  ; primFloatToWord64 to toWord
  ; primNatToFloat    to fromℕ
  -- Operations
  ; primFloatPlus   to _+_
  ; primFloatMinus  to _-_
  ; primFloatTimes  to _*_
  ; primFloatNegate to -_
  ; primFloatDiv    to _÷_
  ; primFloatSqrt   to sqrt
  ; primRound       to round
  ; primFloor       to ⌊_⌋
  ; primCeiling     to ⌈_⌉
  ; primExp         to e^_
  ; primLog         to log
  ; primSin         to sin
  ; primCos         to cos
  ; primTan         to tan
  ; primASin        to asin
  ; primACos        to acos
  ; primATan        to atan
  )

_≈_ : Rel Float _
_≈_ = Word._≈_ on toWord

_<_ : Rel Float _
_<_ = Word._<_ on toWord


text:
-- Andreas, 2016-02-04
-- Printing of overapplied operator patterns

-- Expected results see comments.

_fun : (A : Set) → Set
_fun = {!!}
-- C-c C-c RET gives
--
-- A fun = ?

_nofun : (A : Set₁) (B : Set₁) → Set₁
_nofun = {!!}
-- C-c C-c RET gives
--
-- (A nofun) B = ?

module Works where

  record Safe : Set₁ where
    field <_>safe : Set
  open Safe

  mixfix : Safe
  mixfix = {!!}
  -- C-c C-c RET gives
  --
  --   < mixfix >safe

record Safe : Set₁ where
  field <_>safe : Set → Set
open Safe

mixfix : Safe
mixfix = {! !}
-- C-c C-c RET gives
--
--   < mixfix >safe x

_+_ : (A B C : Set) → Set
_+_ = {!!}
-- C-c C-c RET gives
--
--   (A + B) C = ?

-_ : (A B : Set) →  Set
-_ = {!!}
-- C-c C-c RET gives
--
--   (- A) B = ?

data D : Set where
  _*_ : (x y z : D) → D

splitP : D → D
splitP d = {! d!}
-- C-c C-c [d RET] gives
--
--   splitP ((d * d₁) d₂) = ?


text:
module bohm-out where
open import lib
open import general-util
open import cedille-types
open import syntax-util

{- Implementation of the Böhm-Out Algorithm -}

private

  nfoldr : ℕ → ∀ {ℓ} {X : Set ℓ} → X → (ℕ → X → X) → X
  nfoldr zero    z s = z
  nfoldr (suc n) z s = s n (nfoldr n z s)

  nfoldl : ℕ → ∀ {ℓ} {X : Set ℓ} → X → (ℕ → X → X) → X
  nfoldl zero    z s = z
  nfoldl (suc n) z s = nfoldl n (s n z) s

  set-nth : ∀ {ℓ} {X : Set ℓ} → ℕ → X → 𝕃 X → 𝕃 X
  set-nth n x [] = []
  set-nth zero x (x' :: xs) = x :: xs
  set-nth (suc n) x (x' :: xs) = x' :: set-nth n x xs

  -- Böhm Tree
  data BT : Set where
    Node : (n i : ℕ) → 𝕃 BT → BT
  -- n: number of lambdas currently bound
  -- i: head variable
  -- 𝕃 BT: list of arguments

  -- Path to difference
  data path : Set where
    hd : path                  -- Difference in heads
    as : path                  -- Difference in number of arguments
    ps : (n : ℕ) → path → path -- Difference in nth subtrees (recursive)

  -- η functions
  η-expand'' : ℕ → 𝕃 BT → 𝕃 BT
  η-expand'' g [] = []
  η-expand'' g (Node n i b :: bs) =
    Node (suc n) (if i ≥ g then suc i else i) (η-expand'' g b) :: η-expand'' g bs

  η-expand' : ℕ → BT → BT
  η-expand' g (Node n i b) = Node (suc n) (if i ≥ g then suc i else i) (η-expand'' g b)

  η-expand : BT → BT
  η-expand t @ (Node n _ _) with η-expand' (suc n) t
  ...| Node n' i' b' = Node n' i' (b' ++ [ Node n' n' [] ])

  bt-n : BT → ℕ
  bt-n (Node n i b) = n

  η-equate : BT → BT → BT × BT
  η-equate t₁ t₂ =
    nfoldr (bt-n t₂ ∸ bt-n t₁) t₁ (λ _ → η-expand) ,
    nfoldr (bt-n t₁ ∸ bt-n t₂) t₂ (λ _ → η-expand)

  -- η-equates all nodes along path to difference
  η-equate-path : BT → BT → path → BT × BT
  η-equate-path (Node n₁ i₁ b₁) (Node n₂ i₂ b₂) (ps d p) =
    let b-b = h d b₁ b₂ in
    η-equate (Node n₁ i₁ (fst b-b)) (Node n₂ i₂ (snd b-b))
    where
    h : ℕ → 𝕃 BT → 𝕃 BT → 𝕃 BT × 𝕃 BT
    h zero (b₁ :: bs₁) (b₂ :: bs₂) with η-equate-path b₁ b₂ p
    ...| b₁' , b₂' = b₁' :: bs₁ , b₂' :: bs₂
    h (suc d) (b₁ :: bs₁) (b₂ :: bs₂) with h d bs₁ bs₂
    ...| bs₁' , bs₂' = b₁ :: bs₁' , b₂ :: bs₂'
    h d b₁ b₂ = b₁ , b₂
  η-equate-path t₁ t₂ p = η-equate t₁ t₂

  -- Rotation functions
  rotate : (k : ℕ) → BT
  rotate k =
    Node (suc k) (suc k) (nfoldl k [] (λ k' → Node (suc k) (suc k') [] ::_))

  rotate-BT' : ℕ → 𝕃 BT → 𝕃 BT
  rotate-BT' k [] = []
  rotate-BT' k (Node n i b :: bs) with i =ℕ k
  ...| ff = Node n i (rotate-BT' k b) :: rotate-BT' k bs
  ...| tt = Node (suc n) (suc n) (η-expand'' (suc n) (rotate-BT' k b)) :: rotate-BT' k bs
  rotate-BT : ℕ → BT → BT
  rotate-BT k (Node n i b) with i =ℕ k
  ...| ff = Node n i (rotate-BT' k b)
  ...| tt = Node (suc n) (suc n) (η-expand'' (suc n) (rotate-BT' k b))

  -- Returns the greatest number of arguments k ever has at each node it where it is the head
  greatest-apps' : ℕ → 𝕃 BT → ℕ
  greatest-apps' k [] = zero
  greatest-apps' k (Node n k' bs' :: bs) with k =ℕ k'
  ...| ff = max (greatest-apps' k bs') (greatest-apps' k bs)
  ...| tt = max (length bs') (max (greatest-apps' k bs') (greatest-apps' k bs))
  greatest-apps : ℕ → BT → ℕ
  greatest-apps k (Node n i b) with k =ℕ i
  ...| ff = greatest-apps' k b
  ...| tt = max (length b) (greatest-apps' k b)
  greatest-η' : ℕ → ℕ → 𝕃 BT → 𝕃 BT
  greatest-η' k m [] = []
  greatest-η' k m (Node n i bs :: bs') with k =ℕ i
  ...| ff = Node n i (greatest-η' k m bs) :: greatest-η' k m bs'
  ...| tt = nfoldr (m ∸ length bs) (Node n i (greatest-η' k m bs)) (λ _ → η-expand) :: greatest-η' k m bs'
  greatest-η : ℕ → ℕ → BT → BT
  greatest-η k m (Node n i b) with k =ℕ i
  ...| ff = Node n i (greatest-η' k m b)
  ...| tt = nfoldr (m ∸ length b) (Node n i (greatest-η' k m b)) (λ _ → η-expand)

  -- Returns tt if k ever is at the head of a node along the path to the difference
  occurs-in-path : ℕ → BT → path → 𝔹
  occurs-in-path k (Node n i b) (ps d p) =
    k =ℕ i || maybe-else ff (λ t → occurs-in-path k t p) (nth d b)
  occurs-in-path k (Node n i b) p = k =ℕ i

  adjust-path : ℕ → BT → path → path
  adjust-path k (Node n i b) (ps d p) = maybe-else' (nth d b) (ps d p) λ n → ps d (adjust-path k n p)
  adjust-path k (Node n i b) as with k =ℕ i
  ...| tt = hd
  ...| ff = as
  adjust-path k (Node n i b) hd = hd

  -- Δ functions
  construct-BT : term → maybe BT
  construct-BT = h zero empty-trie Node where
    h : ℕ → trie ℕ → ((n i : ℕ) → 𝕃 BT → BT) → term → maybe BT
    h n vm f (Var _ x) = just (f n (trie-lookup-else zero vm x) [])
    h n vm f (App t NotErased t') =
      h n vm Node t' ≫=maybe λ t' →
      h n vm (λ n i b → f n i (b ++ [ t' ])) t
    h n vm f (Lam _ NotErased _ x NoClass t) = h (suc n) (trie-insert vm x (suc n)) f t
    h n vm f t = nothing

  {-# TERMINATING #-}
  construct-path' : BT → BT → maybe (path × BT × BT)
  construct-path : BT → BT → maybe (path × BT × BT)
  construct-path (Node _ zero _) _ = nothing
  construct-path _ (Node _ zero _) = nothing
  construct-path t₁ t₂ = uncurry construct-path' (η-equate t₁ t₂)
  construct-path' t₁ @ (Node n₁ i₁ b₁) t₂ @ (Node n₂ i₂ b₂) =
    if ~ i₁ =ℕ i₂
      then just (hd , t₁ , t₂)
      else if length b₁ =ℕ length b₂
        then maybe-map (λ {(p , b₁ , b₂) → p , Node n₁ i₁ b₁ , Node n₂ i₂ b₂}) (h zero b₁ b₂)
        else just (as , t₁ , t₂)
    where
    h : ℕ → 𝕃 BT → 𝕃 BT → maybe (path × 𝕃 BT × 𝕃 BT)
    h n (b₁ :: bs₁) (b₂ :: bs₂) =
      maybe-else
        (maybe-map (λ {(p , bs₁ , bs₂) → p , b₁ :: bs₁ , b₂ :: bs₂}) (h (suc n) bs₁ bs₂))
        (λ {(p , b₁ , b₂) → just (ps n p , b₁ :: bs₁ , b₂ :: bs₂)})
        (construct-path b₁ b₂)
    h _ _ _ = nothing

  {-# TERMINATING #-}
  construct-Δ : BT → BT → path → 𝕃 BT
  construct-Δ (Node n₁ i₁ b₁) (Node n₂ i₂ b₂) hd =
    nfoldl n₁ [] λ m → _::_
      (if suc m =ℕ i₁
        then Node (2 + length b₁) (1 + length b₁) []
        else if suc m =ℕ i₂
          then Node (2 + length b₂) (2 + length b₂) []
          else Node 1 1 [])
  construct-Δ (Node n₁ i₁ b₁) (Node n₂ i₂ b₂) as =
    let l₁ = length b₁
        l₂ = length b₂
        d = l₁ > l₂
        lM = if d then l₁ else l₂
        lm = if d then l₂ else l₁
        l = lM ∸ lm in
    nfoldl n₁
      (nfoldr l [ Node (2 + l) ((if d then 1 else 2) + l) [] ]
         λ l' → _++
           [ if suc l' =ℕ l
               then Node 2 (if d then 2 else 1) []
               else Node 1 1 [] ])
     (λ n' → _::_
       (if suc n' =ℕ i₁
         then Node (suc lM) (suc lM) []
         else Node 1 1 []))
  construct-Δ t₁ @ (Node n₁ i₁ b₁) t₂ @ (Node n₂ i₂ b₂) (ps d p)
    with nth d b₁ ≫=maybe λ b₁ → nth d b₂ ≫=maybe λ b₂ → just (b₁ , b₂)
  ...| nothing = [] -- Shouldn't happen
  ...| just (t₁' @ (Node n₁' i₁' b₁') , t₂' @ (Node n₂' i₂' b₂'))
    with occurs-in-path i₁ t₁' p || occurs-in-path i₂ t₂' p
  ...| ff = set-nth (pred i₁) (Node (length b₁) (suc d) []) (construct-Δ t₁' t₂' p)
  ...| tt with max (greatest-apps i₁ t₁) (greatest-apps i₂ t₂)
  ...| kₘ with η-equate-path (rotate-BT i₁ (greatest-η i₁ kₘ t₁))
                             (rotate-BT i₂ (greatest-η i₂ kₘ t₂)) (ps d p)
  ...| t₁'' , t₂'' = set-nth (pred i₁) (rotate kₘ) (construct-Δ t₁'' t₂'' (ps d $ adjust-path i₁ t₁' p))

  reconstruct : BT → term
  reconstruct = h zero where
    mkvar : ℕ → var
    mkvar n = "x" ^ ℕ-to-string n
    h : ℕ → BT → term
    a : ℕ → term → 𝕃 BT → term
    a n t [] = t
    a n t (b :: bs) = a n (mapp t (h n b)) bs
    h m (Node n i b) = nfoldl (n ∸ m) (a n (mvar (mkvar i)) b) (λ nm → mlam (mkvar (suc (m + nm))))

-- Returns a term f such that f t₁ ≃ λ t. λ f. t and f t₂ ≃ λ t. λ f. f, assuming two things:
-- 1. t₁ ≄ t₂
-- 2. The head of each node along the path to the difference between t₁ and t₂ is bound
--    withing the terms (so λ x. λ y. y y (x y) and λ x. λ y. y y (x x) works, but not
--    λ x. λ y. y y (f y), where f is already declared/defined)
make-contradiction : (t₁ t₂ : term) → maybe term
make-contradiction t₁ t₂ =
  construct-BT t₁ ≫=maybe λ t₁ →
  construct-BT t₂ ≫=maybe λ t₂ →
  construct-path t₁ t₂ ≫=maybe λ {(p , t₁ , t₂) →
  just (reconstruct (Node (suc zero) (suc zero)
    (map (η-expand' zero) (construct-Δ t₁ t₂ p))))}

-- Returns tt if the two terms are provably not equal
is-contradiction : term → term → 𝔹
is-contradiction t₁ t₂ = isJust (make-contradiction t₁ t₂)

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Data.Fin.Core where

open import Core
open import Data.Nat
import Data.Nat.Core as Nat

data Fin : ℕ → Set where
  fzero : {n : ℕ} → Fin (suc n)
  fsuc  : {n : ℕ} → Fin n → Fin (suc n)

instance
  Fin-Number : {n : ℕ} → Number (Fin (suc n))
  Fin-Number {n} =
    record {
      Constraint = λ x → x ℕ,≤.≤ n;
      fromNat = f n
    }

    where
    f : ∀ n x {{_ : x ℕ,≤.≤ n}} → Fin (suc n)
    f n .0 {{Nat.0≤s}} = fzero
    f (suc n) (suc x) {{Nat.s≤s p}} = fsuc (f n x {{p}})

  Fin,≡ : ∀ {n} → Equiv (Fin n)
  Fin,≡ = PropEq _

fsuc-inj : ∀ {n} {x y : Fin (suc n)} → fsuc x ≡ fsuc y → x ≡ y
fsuc-inj ≡-refl = ≡-refl

fromℕ : ∀ {n} (x : ℕ) → x Nat.≤ n → Fin (suc n)
fromℕ zero p = fzero
fromℕ (suc x) (Nat.s≤s p) = fsuc (fromℕ x p)

toℕ : ∀ {n} → Fin (suc n) → ∃ (λ x → x Nat.≤ n)
toℕ fzero = zero , Nat.0≤s
toℕ {zero} (fsuc ())
toℕ {suc n} (fsuc x) with toℕ x
toℕ {suc n} (fsuc x) | x' , p = suc x' , Nat.s≤s p

embed : ∀ {n} → Fin n → Fin (suc n)
embed fzero = fzero
embed (fsuc x) = fsuc (embed x)

_≤_ : ∀ {n} (x y : Fin (suc n)) → Set _
x ≤ y = fst (toℕ x) Nat.≤ fst (toℕ y)

infix 1 _≤_

_≤?_ : ∀ {n} (x y : Fin (suc n)) → Decision (x ≤ y)
x ≤? y = fst (toℕ x) Nat.≤? fst (toℕ y)

-- Fin,≤ : ∀ {n} → TotalOrder (Fin (suc n))
-- Fin,≤ {n} =
--   record {
--     partialOrder = record {
--       Eq = Fin,≡;
--       _≤_ = _≤_;
--       antisym = antisym;
--       refl' = refl';
--       trans = λ {x} {y} {z} → trans {x} {y} {z}
--     };
--     total = total
--   }

--   where
--   not-s≤0 : ∀ {n} {x : Fin (suc n)} → not (fsuc x ≤ fzero)
--   not-s≤0 ()

--   antisym : ∀ {x y} → x ≤ y → y ≤ x → x ≡ y
--   antisym {fzero} {fzero} p q = ≡-refl
--   antisym {fzero} {fsuc y} p q with not-s≤0 {!!}
--   antisym {fzero} {fsuc y} p q | ()
--   antisym {fsuc x} p q = {!!}

--   refl' : ∀ {x y} → x ≡ y → x ≤ y
--   refl' = {!!}

--   trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
--   trans = {!!}

--   total : ∀ x y → Either (x ≤ y) (y ≤ x)
--   total = {!!}

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.FiniteMultiset.CountExtensionality where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sum
open import Cubical.Relation.Nullary
open import Cubical.HITs.FiniteMultiset.Base
open import Cubical.HITs.FiniteMultiset.Properties as FMS
open import Cubical.Structures.MultiSet
open import Cubical.Relation.Nullary.DecidableEq

private
 variable
  ℓ : Level

-- We define a partial order on FMSet A and use it to proof
-- a strong induction principle for finite multi-sets.
-- Finally, we use this stronger elimination principle to show
-- that any two FMSets can be identified, if they have the same count for every a : A
module _{A : Type ℓ} (discA : Discrete A) where
 _≼_ : FMSet A → FMSet A → Type ℓ
 xs ≼ ys = ∀ a → FMScount discA a xs ≤ FMScount discA a ys

 ≼-refl : ∀ xs → xs ≼ xs
 ≼-refl xs a  = ≤-refl

 ≼-trans : ∀ xs ys zs → xs ≼ ys → ys ≼ zs → xs ≼ zs
 ≼-trans xs ys zs xs≼ys ys≼zs a = ≤-trans (xs≼ys a) (ys≼zs a)

 ≼[]→≡[] : ∀ xs → xs ≼ [] → xs ≡ []
 ≼[]→≡[] xs xs≼[] = FMScount-0-lemma discA xs λ a → ≤0→≡0 (xs≼[] a)

 ≼-remove1 : ∀ a xs → remove1 discA a xs ≼ xs
 ≼-remove1 a xs b with discA a b
 ...              | yes a≡b = subst (λ n → n ≤ FMScount discA b xs) (sym path) (≤-predℕ)
  where
  path : FMScount discA b (remove1 discA a xs) ≡ predℕ (FMScount discA b xs)
  path = cong (λ c → FMScount discA b (remove1 discA c xs)) a≡b ∙ remove1-predℕ-lemma discA b xs
 ...              | no  a≢b = subst (λ n → n ≤ FMScount discA b xs)
                                    (sym (FMScount-remove1-≢-lemma discA xs λ b≡a → a≢b (sym b≡a))) ≤-refl

 ≼-remove1-lemma : ∀ x xs ys → ys ≼ (x ∷ xs) → (remove1 discA x ys) ≼ xs
 ≼-remove1-lemma x xs ys ys≼x∷xs a with discA a x
 ...                               | yes a≡x = ≤-trans (≤-trans (0 , p₁) (predℕ-≤-predℕ (ys≼x∷xs a)))
                                                                (0 , cong predℕ (FMScount-≡-lemma discA xs a≡x))
  where
  p₁ : FMScount discA a (remove1 discA x ys) ≡ predℕ (FMScount discA a ys)
  p₁ = subst (λ b →  FMScount discA a (remove1 discA b ys) ≡ predℕ (FMScount discA a ys)) a≡x (remove1-predℕ-lemma discA a ys)
 ...                               | no  a≢x = ≤-trans (≤-trans (0 ,  FMScount-remove1-≢-lemma discA ys a≢x) (ys≼x∷xs a))
                                                                (0 , FMScount-≢-lemma discA  xs a≢x)

 ≼-Dichotomy : ∀ x xs ys → ys ≼ (x ∷ xs) → (ys ≼ xs) ⊎ (ys ≡ x ∷ (remove1 discA x ys))
 ≼-Dichotomy x xs ys ys≼x∷xs with (FMScount discA x ys) ≟ suc (FMScount discA x xs)
 ...                         | lt <suc = inl ys≼xs
  where
  ys≼xs : ys ≼ xs
  ys≼xs a with discA a x
  ...     | yes a≡x = pred-≤-pred (subst (λ b → (FMScount discA b ys) < suc (FMScount discA b xs)) (sym a≡x) <suc)
  ...     | no  a≢x = ≤-trans (ys≼x∷xs a) (subst (λ n → FMScount discA a (x ∷ xs) ≤ n) (FMScount-≢-lemma discA xs a≢x) ≤-refl)
 ...                         | eq ≡suc = inr (remove1-suc-lemma discA x (FMScount discA x xs) ys ≡suc)
 ...                         | gt >suc = ⊥.rec (¬m<m strict-ineq)
  where
  strict-ineq : suc (FMScount discA x xs) < suc (FMScount discA x xs)
  strict-ineq =  <≤-trans (<≤-trans >suc (ys≼x∷xs x)) (0 , FMScount-≡-lemma-refl discA xs)

 -- proving a strong elimination principle for finite multisets
 module ≼-ElimProp {ℓ'} {B : FMSet A → Type ℓ'}
                       (BisProp : ∀ {xs} → isProp (B xs)) (b₀ : B [])
                       (B-≼-hyp : ∀ x xs → (∀ ys → ys ≼ xs → B ys) → B (x ∷ xs)) where

  C : FMSet A → Type (ℓ-max ℓ ℓ')
  C xs = ∀ ys → ys ≼ xs → B ys

  g : ∀ xs → C xs
  g = ElimProp.f (isPropΠ2 (λ _ _ → BisProp)) c₀ θ
   where
   c₀ : C []
   c₀ ys ys≼[] = subst B (sym (≼[]→≡[] ys ys≼[])) b₀

   θ : ∀ x {xs} → C xs → C (x ∷ xs)
   θ x {xs} hyp ys ys≼x∷xs with ≼-Dichotomy x xs ys ys≼x∷xs
   ...                     | inl ys≼xs   = hyp ys ys≼xs
   ...                     | inr ys≡x∷zs = subst B (sym ys≡x∷zs) (B-≼-hyp x zs χ)
    where
    zs = remove1 discA x ys
    χ : ∀ vs → vs ≼ zs → B vs
    χ vs vs≼zs = hyp vs (≼-trans vs zs xs vs≼zs (≼-remove1-lemma x xs ys ys≼x∷xs))

  f : ∀ xs → B xs
  f = C→B g
   where
   C→B : (∀ xs → C xs) → (∀ xs → B xs)
   C→B C-hyp xs = C-hyp xs xs (≼-refl xs)

 ≼-ElimPropBin :  ∀ {ℓ'} {B : FMSet A → FMSet A → Type ℓ'}
                   → (∀ {xs} {ys} → isProp (B xs ys))
                   → (B [] [])
                   → (∀ x xs ys → (∀ vs ws → vs ≼ xs → ws ≼ ys → B vs ws) → B (x ∷ xs) ys)
                   → (∀ x xs ys → (∀ vs ws → vs ≼ xs → ws ≼ ys → B vs ws) → B xs (x ∷ ys))
                   -------------------------------------------------------------------------------
                   → (∀ xs ys → B xs ys)
 ≼-ElimPropBin {B = B} BisProp b₀₀ left-hyp right-hyp = ≼-ElimProp.f (isPropΠ (λ _ → BisProp)) θ χ
  where
  θ : ∀ ys → B [] ys
  θ = ≼-ElimProp.f BisProp b₀₀ h₁
   where
   h₁ : ∀ x ys → (∀ ws → ws ≼ ys → B [] ws) → B [] (x ∷ ys)
   h₁ x ys mini-h = right-hyp x [] ys h₂
    where
    h₂ : ∀ vs ws → vs ≼ [] → ws ≼ ys → B vs ws
    h₂ vs ws vs≼[] ws≼ys = subst (λ zs → B zs ws) (sym (≼[]→≡[] vs vs≼[])) (mini-h ws ws≼ys)

  χ : ∀ x xs → (∀ zs → zs ≼ xs → (∀ ys → B zs ys)) → ∀ ys → B (x ∷ xs) ys
  χ x xs h ys = left-hyp x xs ys λ vs ws vs≼xs _ → h vs vs≼xs ws

 ≼-ElimPropBinSym :  ∀ {ℓ'} {B : FMSet A → FMSet A → Type ℓ'}
                      → (∀ {xs} {ys} → isProp (B xs ys))
                      → (∀ {xs} {ys} → B xs ys → B ys xs)
                      → (B [] [])
                      → (∀ x xs ys → (∀ vs ws → vs ≼ xs → ws ≼ ys → B vs ws) → B (x ∷ xs) ys)
                      ----------------------------------------------------------------------------
                      → (∀ xs ys → B xs ys)
 ≼-ElimPropBinSym {B = B} BisProp BisSym b₀₀ left-hyp = ≼-ElimPropBin BisProp b₀₀ left-hyp right-hyp
  where
  right-hyp : ∀ x xs ys → (∀ vs ws → vs ≼ xs → ws ≼ ys → B vs ws) → B xs (x ∷ ys)
  right-hyp x xs ys h₁ = BisSym (left-hyp x ys xs (λ vs ws vs≼ys ws≼xs → BisSym (h₁ ws vs ws≼xs vs≼ys)))

 -- The main result
 module FMScountExt where
  B : FMSet A → FMSet A → Type ℓ
  B xs ys = (∀ a → FMScount discA a xs ≡ FMScount discA a ys) → xs ≡ ys

  BisProp : ∀ {xs} {ys} → isProp (B xs ys)
  BisProp = isPropΠ λ _ → trunc _ _

  BisSym : ∀ {xs} {ys} → B xs ys → B ys xs
  BisSym {xs} {ys} b h = sym (b (λ a → sym (h a)))

  b₀₀ : B [] []
  b₀₀ _ = refl

  left-hyp : ∀ x xs ys → (∀ vs ws → vs ≼ xs → ws ≼ ys → B vs ws) → B (x ∷ xs) ys
  left-hyp x xs ys hyp h₁ = (λ i → x ∷ (hyp-path i)) ∙ sym path
   where
   eq₁ : FMScount discA x ys ≡ suc (FMScount discA x xs)
   eq₁ = sym (h₁ x) ∙ FMScount-≡-lemma-refl discA xs

   path : ys ≡ x ∷ (remove1 discA x ys)
   path = remove1-suc-lemma discA x (FMScount discA x xs) ys eq₁

   hyp-path : xs ≡ remove1 discA x ys
   hyp-path = hyp xs (remove1 discA x ys) (≼-refl xs) (≼-remove1 x ys) θ
    where
    θ : ∀ a → FMScount discA a xs ≡ FMScount discA a (remove1 discA x ys)
    θ a with discA a x
    ... | yes a≡x = subst (λ b → FMScount discA b xs ≡ FMScount discA b (remove1 discA x ys)) (sym a≡x) eq₂
     where
     eq₂ : FMScount discA x xs ≡ FMScount discA x (remove1 discA x ys)
     eq₂ = FMScount discA x xs                     ≡⟨ cong predℕ (sym (FMScount-≡-lemma-refl discA xs)) ⟩
           predℕ (FMScount discA x (x ∷ xs))       ≡⟨ cong predℕ (h₁ x) ⟩
           predℕ (FMScount discA x ys)             ≡⟨ sym (remove1-predℕ-lemma discA x ys) ⟩
           FMScount discA x (remove1 discA x ys)   ∎
    ... | no  a≢x =
           FMScount discA a xs                         ≡⟨ sym (FMScount-≢-lemma discA  xs a≢x) ⟩
           FMScount discA a (x ∷ xs)                   ≡⟨ h₁ a ⟩
           FMScount discA a ys                         ≡⟨ cong (FMScount discA a) path ⟩
           FMScount discA a (x ∷ (remove1 discA x ys)) ≡⟨ FMScount-≢-lemma discA (remove1 discA x ys) a≢x ⟩
           FMScount discA a (remove1 discA x ys)       ∎

  Thm : ∀ xs ys → (∀ a → FMScount discA a xs ≡ FMScount discA a ys) → xs ≡ ys
  Thm = ≼-ElimPropBinSym BisProp BisSym b₀₀ left-hyp

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:
module SameName where

data Stuff : Set where
  mkStuff : Stuff

stuffFunc : Stuff -> (Stuff : Set) -> Stuff
stuffFunc = {!   !}


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

module FunExt where

open import Base

module _ {i j} {A : Type i} {B : A → Type j} where

  happly : (f g : (x : A) → B x) → (f == g) → ((x : A) → f x == g x)
  happly f g = ind== D d where
    D : (f g : (x : A) → B x) → f == g → Type _
    D f g _ = (x : A) → f x == g x

    d : (f : (x : A) → B x) → D f f idp
    d f = λ x → idp

  postulate
    fun-ext : (f g : (x : A) → B x) → is-equiv (happly f g)

max_stars_repo_name: aerskine/hott-ex

max_issues_repo_name: aerskine/hott-ex

max_forks_repo_name: aerskine/hott-ex


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

--
-- Prelude.agda - Some base definitions
--

module Prelude where

  open import Agda.Primitive public

  record ⊤ : Set where
    constructor tt

  {-# BUILTIN UNIT ⊤ #-}

  record Σ {i j} (A : Set i) (B : A → Set j) : Set (i ⊔ j) where
    constructor _,_
    field
      fst : A
      snd : B fst

  open Σ public

  _×_ : ∀ {i j} (A : Set i) (B : Set j) → Set (i ⊔ j)
  A × B = Σ A (λ a → B)

  id : ∀ {i} {A : Set i} → A → A
  id x = x

  uncurry : ∀ {i j k} {A : Set i} {B : A → Set j} {C : Set k} →
            (φ : (a : A) → (b : B a) → C) →
            Σ A B → C
  uncurry φ (a , b) = φ a b

  curry : ∀ {i j k} {A : Set i} {B : A → Set j} {C : Set k} →
          (ψ : Σ A B → C) →
          (a : A) → (b : B a) → C
  curry ψ a b = ψ (a , b)

  {- Equality -}

  infix 30 _==_

  data _==_ {i} {A : Set i} (a : A) : A → Set i where
    idp : a == a
  {-# BUILTIN EQUALITY _==_ #-}
  {-# BUILTIN REWRITE _==_ #-}

  infixl 20 _>>_

  _>>_ : ∀ {i} {A : Set i} {a b c : A} → a == b → b == c → a == c
  idp >> idp = idp

  _^ : ∀ {i} {A : Set i} {a b : A} → a == b → b == a
  _^ idp = idp

  coe : ∀ {a} {A B : Set a} → A == B → A → B
  coe idp x = x

  coe^ : ∀ {a} {A B : Set a} (p : A == B) {a : A} {b : B} → a == (coe (p ^) b) → (coe p a) == b
  coe^ idp q = q

  coe= : ∀ {a} {A B : Set a} (p : A == B) {a b : A} → a == b → coe p a == coe p b
  coe= p idp = idp

  ap : ∀ {i j} {A : Set i} {C : Set j} {M N : A} (f : A → C) → M == N → (f M) == (f N)
  ap f idp = idp

  ap² : ∀ {i j k} {A : Set i} {B : Set k} {C : Set j} {a a' : A} {b b' : B} (f : A → B → C) → a == a' →  b == b' → (f a b) == (f a' b')
  ap² f idp idp = idp

  ap³ : ∀ {i j k l} {A : Set i} {B : Set k} {C : Set j} {D : Set l} {a a' : A} {b b' : B} {c c' : C} (f : A → B → C → D) → a == a' →  b == b' → c == c' → (f a b c) == (f a' b' c')
  ap³ f idp idp idp = idp

  ap⁴ : ∀ {i j k l m} {A : Set i} {B : Set k} {C : Set j} {D : Set l} {E : Set m} {a a' : A} {b b' : B} {c c' : C} {d d' : D} (f : A → B → C → D → E) → a == a' →  b == b' → c == c' → d == d' → (f a b c d) == (f a' b' c' d')
  ap⁴ f idp idp idp idp = idp

  ap⁵ : ∀ {i j k l m n} {A : Set i} {B : Set k} {C : Set j} {D : Set l} {E : Set m} {F : Set n} {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} (f : A → B → C → D → E → F) → a == a' →  b == b' → c == c' → d == d' → e == e' → (f a b c d e) == (f a' b' c' d' e')
  ap⁵ f idp idp idp idp idp = idp

  ap⁶ : ∀ {i j k l m n o} {A : Set i} {B : Set k} {C : Set j} {D : Set l} {E : Set m} {F : Set n} {G : Set o} {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} {f f' : F} (α : A → B → C → D → E → F → G) → a == a' →  b == b' → c == c' → d == d' → e == e' → f == f' → (α a b c d e f) == (α a' b' c' d' e' f')
  ap⁶ f idp idp idp idp idp idp = idp

  ap⁷ : ∀ {i j k l m n o p} {A : Set i} {B : Set k} {C : Set j} {D : Set l} {E : Set m} {F : Set n} {G : Set o} {H : Set p} {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} {f f' : F} {g g' : G} (α : A → B → C → D → E → F → G → H) → a == a' →  b == b' → c == c' → d == d' → e == e' → f == f' → g == g' → (α a b c d e f g) == (α a' b' c' d' e' f' g')
  ap⁷ f idp idp idp idp idp idp idp = idp

  transport : ∀ {i j} {A : Set i} {B : A → Set j} {a a' : A} (pₐ : a == a') → B a → B a'
  transport pₐ b = coe (ap _ pₐ) b

  transport₂ : ∀ {i j k} {A : Set i} {B : Set j} {C : A → B → Set k} {a a' : A} {b b' : B} (pₐ : a == a') (q : b == b') → C a b → C a' b'
  transport₂ pₐ q c = coe (ap² _ pₐ q) c

  hfiber : ∀ {i} {A B : Set i} (f : A → B) (b : B) → Set i
  hfiber {A = A} f b = Σ A (λ a → f a == b)

  PathOver : ∀ {i j} {A : Set i} (B : A → Set j) {a₀ a₁ : A} (p : a₀ == a₁) (b₉ : B a₀) (b₁ : B a₁) → Set j
  PathOver B idp b₀ b₁ = b₀ == b₁

  infix 30 PathOver
  syntax PathOver B p u v =
    u == v [ B ↓ p ]

  ×= : ∀{i j} {A : Set i} {B : Set j}  {a a' : A} {b b' : B} → a == a' → b == b' → (a , b) == (a' , b')
  ×= idp idp = idp

  Σ= : ∀ {i j} {A : Set i} {B : A → Set j}  {a a' : A} {b : B a} {b' : B a'} → (pₐ : a == a') → transport pₐ b == b' → (a , b) == (a' , b')
  Σ= idp idp = idp

  ,= : ∀ {i j} {A : Set i} {B : Set j}  {a a' : A} {b b' : B} → a == a' → b == b' → (a , b) == (a' , b')
  ,= idp idp = idp

  Σ-r : ∀ {i j k} {A : Set i} {B : A → Set j} (C : Σ A B → Set k) → A → Set (j ⊔ k)
  Σ-r {A = A} {B = B} C a = Σ (B a) (λ b → C (a , b))

  Σ-in : ∀ {i j k} {A : Set i} {B : A → Set j} (C : (a : A) → B a → Set k) → A → Set (j ⊔ k)
  Σ-in {A = A} {B = B} C a = Σ (B a) (λ b → C a b)

  =, : ∀ {i j} {A : Set i} {B : Set j} {a a' : A} {b b' : B} → (a , b) == (a' , b') → (a == a') × (b == b')
  =, idp = idp , idp

  fst-is-inj : ∀ {i j} {A : Set i} {B : A → Set j} {x y : Σ A B} → x == y → fst x == fst y
  fst-is-inj idp = idp

  {- False and negation -}

  data ⊥ {i} : Set i where

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

  ¬_ : ∀ {i} → Set i → Set i
  ¬ A = A → ⊥ {lzero}

  _≠_ : ∀{i} {A : Set i} (a b : A) → Set i
  a ≠ b = ¬ (a == b)

  data _+_  {i j} (A : Set i) (B : Set j) : Set (i ⊔ j) where
    inl : A → A + B
    inr : B → A + B

  inl= : ∀ {i j} {A : Set i} {B : Set j} {a b : A} → a == b → _==_ {i ⊔ j} {A + B} (inl a) (inl b)
  inl= idp = idp

  inr= : ∀ {i j} {A : Set i} {B : Set j} {a b : B} → a == b → _==_ {i ⊔ j} {A + B} (inr a) (inr b)
  inr= idp = idp

  {- Booleans -}
  data Bool : Set where
    true : Bool
    false : Bool

  {- Decidability -}
  dec : ∀ {i} → Set i → Set i
  dec A = A + (¬ A)

  eqdec : ∀ {i} → Set i → Set i
  eqdec A = ∀ (a b : A) → dec (a == b)

  {- Natural numbers -}
  data ℕ : Set where
    O : ℕ
    S : ℕ → ℕ

  {-# BUILTIN NATURAL ℕ #-}

  S= : ∀{n m} → n == m → S n == S m
  S= idp = idp

  pred : ℕ → ℕ
  pred O = O
  pred (S n) = n

  S-is-inj : ∀ n m → (S n == S m) → n == m
  S-is-inj n m p = ap pred p

  S-≠ : ∀ {n m : ℕ} (p : n ≠ m) → S n ≠ S m
  S-≠ {n} {m} n≠m  p = n≠m (S-is-inj n m p)

  private
    S≠O-type : ℕ → Set
    S≠O-type O = ⊥
    S≠O-type (S n) = ⊤

  S≠O : (n : ℕ) → S n ≠ O
  S≠O n p = coe (ap S≠O-type p) tt

  O≠S : (n : ℕ) → (O ≠ S n)
  O≠S n p = S≠O n (p ^)

  n≠Sn : (n : ℕ) → (n ≠ S n)
  n≠Sn O ()
  n≠Sn (S n) n=Sn = n≠Sn n (S-is-inj _ _ n=Sn)

  Sn≠n : (n : ℕ) → (S n ≠ n)
  Sn≠n O ()
  Sn≠n (S n) Sn=n = Sn≠n n (S-is-inj _ _ Sn=n)

  eqdecℕ : eqdec ℕ
  eqdecℕ O O = inl idp
  eqdecℕ O (S b) = inr (O≠S b)
  eqdecℕ (S a) O = inr (S≠O a)
  eqdecℕ (S a) (S b) with (eqdecℕ a b)
  ...                 | inl idp = inl idp
  ...                 | inr a≠b = inr (S-≠ a≠b)

  {- Order on ℕ -}
  data _≤_ : ℕ → ℕ → Set where
    0≤ : ∀ n → O ≤ n
    S≤ : ∀ {n m} → n ≤ m → S n ≤ S m

  n≤n : ∀ (n : ℕ) → n ≤ n
  n≤n O = 0≤ O
  n≤n (S n) = S≤ (n≤n n)

  ≤-antisymetry : ∀ {n m} → n ≤ m → m ≤ n → n == m
  ≤-antisymetry (0≤ _) (0≤ _) = idp
  ≤-antisymetry (S≤ n≤m) (S≤ m≤n) = ap S (≤-antisymetry n≤m m≤n)

  n≤Sn : ∀ (n : ℕ) → n ≤ S n
  n≤Sn O = 0≤ _
  n≤Sn (S n) = S≤ (n≤Sn _)

  S≤S : ∀ {n m} → S n ≤ S m → n ≤ m
  S≤S (S≤ n≤m) = n≤m

  Sn≰n : ∀ (n : ℕ) → ¬ (S n ≤ n)
  Sn≰n .(S _) (S≤ Sn≤n) = Sn≰n _ Sn≤n

  Sn≰n-t : ∀ {n m} → n == m → ¬ (S n ≤ m)
  Sn≰n-t idp Sn≤n = Sn≰n _ Sn≤n

  Sn≰0 : ∀ (n : ℕ) → ¬ (S n ≤ O)
  Sn≰0 n ()

  n≤m→n≤Sm : ∀ {n m : ℕ} → n ≤ m → n ≤ S m
  n≤m→n≤Sm (0≤ n) = 0≤ (S n)
  n≤m→n≤Sm (S≤ n≤m) = S≤ (n≤m→n≤Sm n≤m)

  Sn≤m→n≤m : ∀ {n m : ℕ} → S n ≤ m → n ≤ m
  Sn≤m→n≤m (S≤ n≤m) = n≤m→n≤Sm n≤m

  dec-≤ : ∀ n m → dec (n ≤ m)
  dec-≤ O m = inl (0≤ m)
  dec-≤ (S n) O = inr λ ()
  dec-≤ (S n) (S m) with (dec-≤ n m)
  ...               | inl n≤m = inl (S≤ n≤m)
  ...               | inr n≰m = inr λ {(S≤ n≤m) → n≰m n≤m}

  ≤S : ∀ (n m : ℕ) → n ≤ S m → (n ≤ m) + (n == S m)
  ≤S .0 m (0≤ .(S m)) = inl (0≤ _)
  ≤S .1 O (S≤ (0≤ .0)) = inr idp
  ≤S .(S _) (S m) (S≤ n≤Sm) with ≤S _ _ n≤Sm
  ... | inl n≤m = inl (S≤ n≤m)
  ... | inr n=Sm = inr (ap S n=Sm)

  ≤-= : ∀ {n m k} → n ≤ m → m == k → n ≤ k
  ≤-= n≤m idp = n≤m

  =-≤ : ∀ {n m k} → n == m → m ≤ k → n ≤ k
  =-≤ idp m≤k = m≤k

  =-≤-= : ∀ {n m k l} → n == m → m ≤ k → k == l → n ≤ l
  =-≤-= idp m≤k idp = m≤k

  ≤T : ∀ {n m k} → n ≤ m → m ≤ k → n ≤ k
  ≤T (0≤ _) _ = 0≤ _
  ≤T (S≤ n≤m) (S≤ m≤k) = S≤ (≤T n≤m m≤k)

  {- Strict order on ℕ -}
  _<_ : ℕ → ℕ → Set
  n < m = S n ≤ m

  ≤×≠→< : ∀ {n m} → n ≤ m → n ≠ m → n < m
  ≤×≠→< {.0} {.0} (0≤ O) n≠m = ⊥-elim (n≠m idp)
  ≤×≠→< {.0} {.(S m)} (0≤ (S m)) n≠m = S≤ (0≤ _)
  ≤×≠→< (S≤ n≤m) Sn≠Sm = S≤ (≤×≠→< n≤m λ n=m → Sn≠Sm (ap S n=m))

  ≰ : ∀ {n m } → ¬ (n ≤ m) → m < n
  ≰ {O} {m} n≰m = ⊥-elim (n≰m (0≤ _))
  ≰ {S n} {O} n≰m = S≤ (0≤ _)
  ≰ {S n} {S m} n≰m = S≤ (≰ λ n≤m → n≰m (S≤ n≤m))

  ℕ-trichotomy : ∀ n m → ((n < m) + (m < n)) + (n == m)
  ℕ-trichotomy n m with dec-≤ n m
  ... | inr n≰m = inl (inr (≰ n≰m))
  ... | inl n≤m with eqdecℕ n m
  ... | inl n=m = inr n=m
  ... | inr n≠m = inl (inl (≤×≠→< n≤m n≠m))

  {- Minimum and maximum -}
  max : ℕ → ℕ → ℕ
  max n m with dec-≤ n m
  ...     | inl _ = m
  ...     | inr _ = n

  n≤max : ∀ n m → n ≤ max n m
  n≤max n m with dec-≤ n m
  ... | inl n≤m = n≤m
  ... | inr m≤n = n≤n _

  m≤max : ∀ n m → m ≤ max n m
  m≤max n m with dec-≤ n m
  ... | inl n≤m = n≤n _
  ... | inr n≰m = Sn≤m→n≤m (≰ n≰m)

  up-max : ∀ {n m k} → n ≤ k → m ≤ k → max n m ≤ k
  up-max {n} {m} {k} n≤k m≤k with dec-≤ n m
  ... | inl n≤m = m≤k
  ... | inr n≰m = n≤k

  up-maxS : ∀ {n m k} → S n ≤ k → S m ≤ k → S (max n m) ≤ k
  up-maxS {n} {m} {k} n≤k m≤k with dec-≤ n m
  ... | inl n≤m = m≤k
  ... | inr n≰m = n≤k

  simplify-max-l : ∀ {n m} → m ≤ n → max n m == n
  simplify-max-l {n} {m} m≤n with dec-≤ n m
  ... | inl n≤m = ≤-antisymetry m≤n n≤m
  ... | inr _ = idp

  simplify-max-r : ∀ {n m} → n ≤ m → max n m == m
  simplify-max-r {n} {m} n≤m with dec-≤ n m
  ... | inl _ = idp
  ... | inr n≰m = ⊥-elim (n≰m n≤m)

  min : ℕ → ℕ → ℕ
  min n m with dec-≤ n m
  ...     | inl _ = n
  ...     | inr _ = m

  min≤m : ∀ n m → min n m ≤ m
  min≤m n m with dec-≤ n m
  ... | inl n≤m = n≤m
  ... | inr n≰m = n≤n _

  simplify-min-l : ∀ {n m} → n ≤ m → min n m == n
  simplify-min-l {n} {m} n≤m with dec-≤ n m
  ... | inl _ = idp
  ... | inr n≰m = ⊥-elim (n≰m n≤m)

  simplify-min-r : ∀ {n m} → m ≤ n → min n m == m
  simplify-min-r {n} {m} n≤m with dec-≤ n m
  ... | inl m≤n = ≤-antisymetry m≤n n≤m
  ... | inr _ = idp

  min<l : ∀ {n m} → min n m < n → m ≤ n
  min<l {n} {m} min<n with dec-≤ n m
  ... | inl _ = ⊥-elim (Sn≰n _ min<n)
  ... | inr _ = Sn≤m→n≤m min<n

  greater-than-min-r : ∀ {n m k} → k < n → min n m ≤ k → m ≤ k
  greater-than-min-r {n} {m} {k} k<n min≤k with dec-≤ n m
  ... | inl _ = ⊥-elim (Sn≰n _ (≤T (S≤ min≤k) k<n))
  ... | inr _ = min≤k

  {- Conditional branchings -}
  ifdec_>_then_else_ : ∀ {i j} {A : Set i} (B : Set j) → (dec B) → A → A → A
  ifdec b > inl x then A else B = A
  ifdec b > inr x then A else B = B

  iftrue : ∀ {i j}{A : Set i} {B : Set j} → (H : dec B) → (a : A) {a' : A} → B → (ifdec B > H then a else a') == a
  iftrue (inl _) a b = idp
  iftrue (inr ¬B) a b = ⊥-elim (¬B b)

  iffalse : ∀ {i j}{A : Set i} {B : Set j} → (H : dec B) → {a : A} (a' : A) → ¬ B → (ifdec B > H then a else a') == a'
  iffalse (inl b) a' ¬B = ⊥-elim (¬B b)
  iffalse (inr ¬B) a' b = idp

  if_≡_then_else_ : ∀ {i} {A : Set i} → ℕ → ℕ → A → A → A
  if v ≡ w then A else B = ifdec (v == w) > (eqdecℕ v w) then A else B

  if= : ∀ {i} {A : Set i} {n m : ℕ} (p : n == m) (a : A) {a' : A} → (if n ≡ m then a else a') == a
  if= p a = iftrue (eqdecℕ _ _) a p

  if≠ : ∀ {i} {A : Set i} {n m : ℕ} (p : n ≠ m) {a : A} (a' : A) → (if n ≡ m then a else a') == a'
  if≠ p a' = iffalse (eqdecℕ _ _) a' p

  simplify-if : ∀ {i} {A : Set i} {n} {a b : A} → 0 < n → (if n ≡ 0 then a else b) == b
  simplify-if {n = n} {b = b} 0<n with eqdecℕ n 0
  ... | inl idp = ⊥-elim (Sn≰0 _ 0<n)
  ... | inr _ = idp

  -- logical equivalence
  _↔_ : ∀{i j} (A : Set i) (B : Set j) → Set (i ⊔ j)
  A ↔ B = (A → B) × (B → A)

  {- Lists -}
  data list {i} : Set i → Set (lsuc i) where
    nil : ∀{A} → list A
    _::_ : ∀ {A} → list A → (a : A) → list A

  ::= : ∀ {i} {A : Set i} {l l' : list A} {a a' : A} → l == l' → a == a' → (l :: a) == (l' :: a')
  ::= idp idp = idp

  =:: : ∀ {i} {A : Set i} {a b : A} {l k} → (l :: a) == (k :: b) → (l == k) × (a == b)
  =:: idp = idp , idp

  cons≠nil : ∀ {i} {A : Set i} {l : list A} {a : A} → (l :: a) ≠ nil
  cons≠nil ()

  length : ∀ {i} {A : Set i} → list A → ℕ
  length nil = 0
  length (l :: _) = S (length l)

  _++_ : ∀ {i} {A : Set i} → list A → list A → list A
  l ++ nil = l
  l ++ (l' :: a) = (l ++ l') :: a

  _∈-list_ : ∀ {i} {A : Set i} → A → list A → Set i
  x ∈-list nil = ⊥
  x ∈-list (l :: a) = (x ∈-list l) + (x == a)

  dec-∈-list : ∀ {i} {A : Set i} → eqdec A →  ∀ (a : A) (l : list A) → dec (a ∈-list l)
  dec-∈-list eqdecA a nil = inr λ{()}
  dec-∈-list eqdecA a (l :: b) with eqdecA a b
  ...                    | inl idp = inl (inr idp)
  ...                    | inr a≠b with dec-∈-list eqdecA a l
  ...                             | inl a∈l = inl (inl a∈l)
  ...                             | inr a∉l = inr λ{(inl a∈l) → a∉l a∈l; (inr a=b) → a≠b a=b}

{- Univalence and known consequences -}

  record is-equiv {i j} {A : Set i} {B : Set j} (f : A → B) : Set (i ⊔ j)
    where
    field
      g : B → A
      f-g : (b : B) → f (g b) == b
      g-f : (a : A) → g (f a) == a
      adj : (a : A) → ap f (g-f a) == f-g (f a)

  _≃_ : ∀ {i j} → (A : Set i) (B : Set j) → Set (i ⊔ j)
  A ≃ B = Σ (A → B) λ f → is-equiv f

  postulate
    univalence : ∀ {i} {A B : Set i} → (A == B) ≃ (A ≃ B)
    funext : ∀ {i} {A B : Set i} (f g : A → B) → (∀ x → f x == g x) → f == g
    funext-dep : ∀ {i} {A : Set i} {B : A → Set i} (f g : ∀ a → B a) → (∀ a → f a == g a) → f == g

{- Definition of the first H-levels -}

  is-contr : ∀ {i} → Set i → Set i
  is-contr A = Σ A (λ x → ((y : A) → x == y))

  is-prop : ∀ {i} → Set i → Set i
  is-prop A = ∀ (x y : A) → is-contr (x == y)

  is-set : ∀{i} → Set i → Set i
  is-set A = ∀ (x y : A) → is-prop (x == y)

  has-all-paths : ∀ {i} → Set i → Set i
  has-all-paths A = ∀ (a b : A) → a == b

  {- Known properties of H-levels -}
  postulate
    has-all-paths-idp : ∀ {i} (A : Set i) (pathsA : has-all-paths A) (a : A) → pathsA a a == idp
    has-all-paths-is-prop : ∀ {i} → {A : Set i} → has-all-paths A → is-prop A
    is-prop-has-all-paths : ∀ {i} → {A : Set i} → is-prop A → has-all-paths A
    eqdec-is-set : ∀ {i} {A : Set i} → eqdec A → is-set A

  is-setℕ : is-set ℕ
  is-setℕ = eqdec-is-set eqdecℕ

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
------------------------------------------------------------------------
-- Pullbacks
------------------------------------------------------------------------

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

-- This module is partly based on code written by Guillame Brunerie in
-- a fork of the Coq HoTT library
-- (https://github.com/guillaumebrunerie/HoTT/), and partly based on
-- the Wikipedia page about pullbacks
-- (https://en.wikipedia.org/wiki/Pullback_(category_theory)).

open import Equality

module Pullback {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

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

open import Bijection eq as Bijection using (_↔_)
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
open import Function-universe eq as F hiding (_∘_)
open import H-level.Closure eq

private
  variable
    a a₁ a₂ b b₁ b₂ l m r : Level
    A A₁ A₂ B             : Type a
    C                     : A
    k                     : Kind

-- Cospans.

record Cospan l r m : Type (lsuc (l ⊔ r ⊔ m)) where
  field
    {Left}   : Type l
    {Right}  : Type r
    {Middle} : Type m
    left     : Left  → Middle
    right    : Right → Middle

-- Cones over cospans. The "corner opposite to" the Middle type is a
-- parameter, not a field, so a more accurate name might be something
-- like Cone-over-cospan-with-given-opposite-corner.

record Cone (A : Type a) (C : Cospan l r m) :
            Type (a ⊔ l ⊔ r ⊔ m) where
  field
    left     : A → Cospan.Left C
    right    : A → Cospan.Right C
    commutes : ∀ x → Cospan.left C (left x) ≡ Cospan.right C (right x)

-- The type of cones can also be written using Σ-types.

Cone↔Σ :
  Cone A C
    ↔
  ∃ λ ((f , g) : (A → Cospan.Left C) × (A → Cospan.Right C)) →
    ∀ x → Cospan.left C (f x) ≡ Cospan.right C (g x)
Cone↔Σ = record
  { surjection = record
    { logical-equivalence = record
      { to   = λ f → (Cone.left f , Cone.right f) , Cone.commutes f
      ; from = λ ((l , r) , c) →
                 record { left = l; right = r; commutes = c }
      }
    ; right-inverse-of = refl
    }
  ; left-inverse-of = refl
  }

-- Equality between cones is isomorphic to certain kinds of triples.

Cone-≡-↔-Σ :
  {C : Cospan l m r} {c d : Cone A C} →
  c ≡ d
    ↔
  (∃ λ (p : Cone.left  c ≡ Cone.left  d) →
   ∃ λ (q : Cone.right c ≡ Cone.right d) →
     subst
       (λ (f , g) →
          ∀ x → Cospan.left C (f x) ≡ Cospan.right C (g x))
       (cong₂ _,_ p q)
       (Cone.commutes c) ≡
     Cone.commutes d)
Cone-≡-↔-Σ {C = C} {c = c} {d = d} =
  c ≡ d                                                      ↔⟨ inverse $ Eq.≃-≡ (Eq.↔⇒≃ Cone↔Σ) ⟩

  ((Cone.left c , Cone.right c) , Cone.commutes c) ≡
  ((Cone.left d , Cone.right d) , Cone.commutes d)           ↝⟨ inverse $ Bijection.Σ-≡,≡↔≡ ⟩

  (∃ λ (p : (Cone.left c , Cone.right c) ≡
            (Cone.left d , Cone.right d)) →
     subst
       (λ (f , g) →
          ∀ x → Cospan.left C (f x) ≡ Cospan.right C (g x))
       p
       (Cone.commutes c) ≡
     Cone.commutes d)                                        ↝⟨ (Σ-cong-contra ≡×≡↔≡ λ _ → F.id) ⟩

  (∃ λ (p : Cone.left  c ≡ Cone.left  d ×
            Cone.right c ≡ Cone.right d) →
     subst
       (λ (f , g) →
          ∀ x → Cospan.left C (f x) ≡ Cospan.right C (g x))
       (uncurry (cong₂ _,_) p)
       (Cone.commutes c) ≡
     Cone.commutes d)                                        ↝⟨ inverse Σ-assoc ⟩□

  (∃ λ (p : Cone.left  c ≡ Cone.left  d) →
   ∃ λ (q : Cone.right c ≡ Cone.right d) →
     subst
       (λ (f , g) →
          ∀ x → Cospan.left C (f x) ≡ Cospan.right C (g x))
       (cong₂ _,_ p q)
       (Cone.commutes c) ≡
     Cone.commutes d)                                        □

-- A composition operation for cones.

composition : Cone B C → (A → B) → Cone A C
composition c f .Cone.left     = c .Cone.left     ∘ f
composition c f .Cone.right    = c .Cone.right    ∘ f
composition c f .Cone.commutes = c .Cone.commutes ∘ f

-- The pullback for a given cospan.

Pullback : Cospan l r m → Type (l ⊔ r ⊔ m)
Pullback C = ∃ λ x → ∃ λ y → Cospan.left C x ≡ Cospan.right C y

-- The cone with the pullback as the "opposite corner".

pullback-cone : Cone (Pullback C) C
pullback-cone .Cone.left     = proj₁
pullback-cone .Cone.right    = proj₁ ∘ proj₂
pullback-cone .Cone.commutes = proj₂ ∘ proj₂

-- The property of being a homotopy pullback.

Is-homotopy-pullback :
  {A : Type a} {C : Cospan l r m} →
  Cone A C → ∀ b → Type (a ⊔ lsuc b ⊔ l ⊔ r ⊔ m)
Is-homotopy-pullback c b =
  (B : Type b) → Is-equivalence (composition {A = B} c)

-- The pullback is a homotopy pullback for pullback-cone.

is-homotopy-pullback : Is-homotopy-pullback (pullback-cone {C = C}) b
is-homotopy-pullback {C = C} B =
  _≃_.is-equivalence (
    (B → Pullback C)                                                    ↔⟨⟩
    (B → ∃ λ x → ∃ λ y → Cospan.left C x ≡ Cospan.right C y)            ↔⟨ ΠΣ-comm ⟩
    (∃ λ f → ∀ x → ∃ λ y → Cospan.left C (f x) ≡ Cospan.right C y)      ↔⟨ (∃-cong λ _ → ΠΣ-comm) ⟩
    (∃ λ f → ∃ λ g → ∀ x → Cospan.left C (f x) ≡ Cospan.right C (g x))  ↔⟨ Σ-assoc ⟩
    (∃ λ (f , g) → ∀ x → Cospan.left C (f x) ≡ Cospan.right C (g x))    ↔⟨ inverse Cone↔Σ ⟩□
    Cone B C                                                            □)

-- A universal property for pullbacks.

universal-property : (A → Pullback C) ≃ Cone A C
universal-property = Eq.⟨ _ , is-homotopy-pullback _ ⟩

-- A variant of the universal property.

universal-property′ :
  {C : Cospan l r m}
  (c : Cone A C) →
  Contractible
    (∃ λ (f : A → Pullback C) → composition pullback-cone f ≡ c)
universal-property′ {A = A} {C = C} c = _⇔_.from contractible⇔↔⊤ (
  (∃ λ (f : A → Pullback C) → composition pullback-cone f ≡ c)  ↝⟨ (Σ-cong universal-property λ _ → F.id) ⟩
  (∃ λ (d : Cone A C) → d ≡ c)                                  ↝⟨ _⇔_.to contractible⇔↔⊤ (singleton-contractible _) ⟩□
  ⊤                                                             □)

-- A preservation lemma for Cone.

Cone-cong :
  {A₁ : Type a₁} {A₂ : Type a₂} {C : Cospan l r m} →
  Extensionality? k (a₁ ⊔ a₂) (l ⊔ r ⊔ m) →
  A₁ ≃ A₂ →
  Cone A₁ C ↝[ k ] Cone A₂ C
Cone-cong {A₁ = A₁} {A₂ = A₂} {C = C} ext A₁≃A₂ =
  Cone A₁ C          ↔⟨ inverse universal-property ⟩
  (A₁ → Pullback C)  ↝⟨ →-cong₁ ext A₁≃A₂ ⟩
  (A₂ → Pullback C)  ↔⟨ universal-property ⟩□
  Cone A₂ C          □

private

  -- A special case of Cone-cong that does not require extensionality.

  Cone-↑⊤↔Cone-↑⊤ : Cone (↑ a₁ ⊤) C ↔ Cone (↑ a₂ ⊤) C
  Cone-↑⊤↔Cone-↑⊤ {C = C} =
    Cone (↑ _ ⊤) C        ↔⟨ inverse universal-property ⟩
    (↑ _ ⊤ → Pullback C)  ↝⟨ Π-left-identity-↑ ⟩
    Pullback C            ↝⟨ inverse Π-left-identity-↑ ⟩
    (↑ _ ⊤ → Pullback C)  ↔⟨ universal-property ⟩□
    Cone (↑ _ ⊤) C        □

-- The "opposite corners" of homotopy pullbacks for a fixed cospan are
-- equivalent.

homotopy-pullbacks-equivalent :
  (c₁ : Cone A₁ C) (c₂ : Cone A₂ C) →
  Is-homotopy-pullback c₁ b₁ →
  Is-homotopy-pullback c₂ b₂ →
  A₁ ≃ A₂
homotopy-pullbacks-equivalent {A₁ = A₁} {C = C} {A₂ = A₂} _ _ p₁ p₂ =
  A₁              ↔⟨ inverse Π-left-identity-↑ ⟩
  (↑ _ ⊤ → A₁)    ↝⟨ Eq.⟨ _ , p₁ (↑ _ ⊤) ⟩ ⟩
  Cone (↑ _ ⊤) C  ↔⟨ Cone-↑⊤↔Cone-↑⊤ ⟩
  Cone (↑ _ ⊤) C  ↝⟨ inverse Eq.⟨ _ , p₂ (↑ _ ⊤) ⟩ ⟩
  (↑ _ ⊤ → A₂)    ↔⟨ Π-left-identity-↑ ⟩□
  A₂              □

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
open import Oscar.Class.Congruity
open import Oscar.Data.Proposequality

module Oscar.Class.Congruity.Proposextensequality where

instance

  𝓒̇ongruityProposextensequality : ∀ {a b} → 𝓒̇ongruity a b Proposextensequality
  𝓒̇ongruity.ċongruity 𝓒̇ongruityProposextensequality _ f≡̇g x rewrite f≡̇g x = ∅


text:
-- Andreas, 2017-01-01, issue #2377
-- Warn about useless `public` in `open` statements.

-- {-# OPTIONS -v scope.decl:70 #-}

-- Warning #1
open import Agda.Builtin.Nat public

import Agda.Builtin.Bool as B

-- Warning #2
open B public

module _ where

open import Agda.Builtin.Equality public -- no warning

-- Warning #3
test-let : Set₁
test-let = let open B public in Set

-- Warning #4
test-letm : Set₁
test-letm = let open module C = B public in Set

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Minimal implicational logic, de Bruijn approach, final encoding

module Bf.ArrMp where

open import Lib using (List; _,_; LMem; lzero; lsuc)

-- Types

infixr 0 _=>_
data Ty : Set where
  UNIT :             Ty
  _=>_ : Ty -> Ty -> Ty

-- Context and truth judgement

Cx : Set
Cx = List Ty

isTrue : Ty -> Cx -> Set
isTrue a tc = LMem a tc

-- Terms

TmRepr : Set1
TmRepr = Cx -> Ty -> Set

module ArrMp where
  record Tm (tr : TmRepr) : Set1 where
    infixl 1 _$_
    infixr 0 lam=>_
    field
      var    : forall {tc a}   -> isTrue a tc    -> tr tc a
      lam=>_ : forall {tc a b} -> tr (tc , a) b  -> tr tc (a => b)
      _$_    : forall {tc a b} -> tr tc (a => b) -> tr tc a -> tr tc b

    v0 : forall {tc a} -> tr (tc , a) a
    v0 = var lzero

    v1 : forall {tc a b} -> tr (tc , a , b) a
    v1 = var (lsuc lzero)

    v2 : forall {tc a b c} -> tr (tc , a , b , c) a
    v2 = var (lsuc (lsuc lzero))
  open Tm {{...}} public

  Thm : Ty -> Set1
  Thm a = forall {tr tc} {{_ : Tm tr}} -> tr tc a
open ArrMp public

-- Example theorems

aI : forall {a} -> Thm (a => a)
aI =
  lam=> v0

aK : forall {a b} -> Thm (a => b => a)
aK =
  lam=>
    lam=> v1

aS : forall {a b c} -> Thm ((a => b => c) => (a => b) => a => c)
aS =
  lam=>
    lam=>
      lam=> v2 $ v0 $ (v1 $ v0)

tSKK : forall {a} -> Thm (a => a)
tSKK {a = a} =
  aS {b = a => a} $ aK $ aK

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
{-# OPTIONS --universe-polymorphism --allow-unsolved-metas #-}

module Issue209 where

postulate
  Level : Set
  zero : Level
  suc  : Level → Level
  _⊔_ : Level -> Level -> Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}
{-# BUILTIN LEVELMAX _⊔_ #-}

data _≡_ {a} {A : Set a} (x : A) : A → Set where
  refl : x ≡ x

data _≅_ {a} {A : Set a} (x : A) : ∀ {b} {B : Set b} → B → Set where
  refl : x ≅ x

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

lemma : ∀ {A} (P : A → Set) {x y} (eq : x ≡ y) z →
        subst P eq z ≅ z
lemma P refl z = refl

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Telescope.hs:51

-- The problematic call to reorderTel is
--   reorderTel tel3
-- in Agda.TypeChecking.Rules.LHS.Instantiate.

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- Andreas, 2016-02-11, bug reported by sanzhiyan

module Issue610-module where

import Common.Level
open import Common.Equality

data ⊥ : Set where
record ⊤ : Set where

data A : Set₁ where
  set : .Set → A

module M .(x : Set) where

  .out : Set
  out = x

.ack : A → Set
ack (set x) = M.out x

hah : set ⊤ ≡ set ⊥
hah = refl

-- SHOULD FAIL
.moo' : ⊥
moo' = subst (λ x → x) (cong ack hah) _

-- SHOULD FAIL
.moo : ⊥
moo with cong ack hah
moo | q = subst (λ x → x) q _

baa : .⊥ → ⊥
baa ()

yoink : ⊥
yoink = baa moo


text:
module _ where

open import Agda.Builtin.String

_&_ = primStringAppend

record Show (A : Set) : Set where
  field
    show : A → String

open Show {{...}} public

data Bin : Set where
  []  : Bin
  0:_ : Bin → Bin
  1:_ : Bin → Bin

five : Bin
five = 1: 0: 1: []

instance
  ShowBin : Show Bin
  show {{ShowBin}} [] = ""
  show {{ShowBin}} (0: b) = "0" & show b
  show {{ShowBin}} (1: b) = "1" & show b

hole : Bin → Bin
hole x = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Data.List.Sort where

open import Data.List.Sort.InsertionSort using (insert-sort; sort-sorts; sort-perm; perm-invar)
open import Data.List.Sort.MergeSort using (merge-sort; merge≡insert-sort)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground