text:
open import Relation.Binary.Core

module PLRTree.DropLast.Permutation {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_) where

open import Data.List
open import Data.Sum
open import List.Permutation.Base A
open import List.Permutation.Base.Concatenation A
open import List.Permutation.Base.Equivalence A
open import PLRTree {A}
open import PLRTree.Complete {A}
open import PLRTree.Compound {A}
open import PLRTree.Drop _≤_ tot≤
open import PLRTree.DropLast.Complete _≤_ tot≤
open import PLRTree.Equality {A}

lemma-last-dropLast : {t : Tag}{x : A}{l r : PLRTree} → Complete (node t x l r) → (last (node t x l r) compound ∷ flatten (dropLast (node t x l r))) ∼ flatten (node t x l r)
lemma-last-dropLast (perfect {l} {r} x cl cr l≃r)
    with l | r | l≃r
... | leaf | leaf | ≃lf = ∼x /head /head ∼[]
... | node perfect x' l' r' | node perfect x'' l'' r'' | ≃nd .x' .x'' l'≃r' l''≃r'' l'≃l'' =
                 let _l = node perfect x' l' r' ;
                      _r = node perfect x'' l'' r'' ;
                      zxflfrd∼xflzfrd = ∼x /head (lemma++/ {last _r compound} {x ∷ flatten _l}) refl∼ ;
                      xflzfrd∼xflfr = lemma++∼l {x ∷ flatten _l} (lemma-last-dropLast cr)
                 in trans∼ zxflfrd∼xflzfrd xflzfrd∼xflfr
lemma-last-dropLast (left {l} {r} x cl cr l⋘r)
    with l | r | l⋘r | lemma-dropLast-⋘ l⋘r
... | leaf | _ | () | _
... | node perfect x' l' r' | _ | () | _
... | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₁ ld⋘r
    with dropLast (node left x' l' r') | ld⋘r | lemma-last-dropLast cl
... | leaf | () | _
... | node perfect _ _ _ | () | _
... | node left x''' l''' r''' | ld⋘r' | zfldfr∼flfr = ∼x (/tail /head) /head (lemma++∼r zfldfr∼flfr)
... | node right x''' l''' r''' | ld⋘r' | zfldfr∼flfr  = ∼x (/tail /head) /head (lemma++∼r zfldfr∼flfr)
lemma-last-dropLast (left x cl cr l⋘r) | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₂ ld≃r
    with dropLast (node left x' l' r') | ld≃r | lemma-last-dropLast cl
... | leaf | () | _
... | node perfect x''' l''' r''' | ld≃r' | zfldfr∼flfr = ∼x (/tail /head) /head (lemma++∼r zfldfr∼flfr)
... | node left _ _ _ | () | _
... | node right _ _ _ | () | _
lemma-last-dropLast (left x cl cr l⋘r) | node right x' l' r' | leaf | () | _
lemma-last-dropLast (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₁ ()
lemma-last-dropLast (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₂ x'≃x''' =
                 ∼x (/tail /head) /head (lemma++∼r (lemma-last-dropLast cl))
lemma-last-dropLast (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₁ ld⋘r
    with dropLast (node right x' l' r') | ld⋘r | lemma-last-dropLast cl
... | leaf | () | _
... | node perfect _ _ _ | () | _
... | node left x''' l''' r''' | ld⋘r' | zfldfr∼flfr = ∼x (/tail /head) /head (lemma++∼r zfldfr∼flfr)
... | node right x''' l''' r''' | ld⋘r' | zfldfr∼flfr = ∼x (/tail /head) /head (lemma++∼r zfldfr∼flfr)
lemma-last-dropLast (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₂ ld≃r
    with dropLast (node right x' l' r') | ld≃r | lemma-last-dropLast cl
... | leaf | () | _
... | node perfect x''' l''' r''' | ld≃r' | zfldfr∼flfr = ∼x (/tail /head) /head (lemma++∼r zfldfr∼flfr)
... | node left _ _ _ | () | _
... | node right _ _ _ | () | _
lemma-last-dropLast (left x cl cr l⋘r) | node right x' l' r' | node left x'' l'' r'' | () | _
lemma-last-dropLast (left x cl cr l⋘r) | node right x' l' r' | node right x'' l'' r'' | () | _
lemma-last-dropLast (right {l} {r} x cl cr l⋙r)
    with l | r | l⋙r
... | leaf | _ | ⋙p ()
... | node perfect x' leaf leaf | leaf | ⋙p (⋗lf .x') = ∼x (/tail /head) /head (∼x /head /head ∼[])
... | node perfect x' leaf leaf | node left _ _ _ | ⋙p ()
... | node perfect x' leaf leaf | node right _ _ _ | ⋙p ()
... | node perfect x' l' r' | node perfect x'' l'' r'' | ⋙p (⋗nd .x' .x'' l'≃r' l''≃r'' l'⋗l'') =
                 ∼x (/tail /head) /head (lemma++∼r (lemma-last-dropLast cl))
... | node perfect x' l' r' | node left x'' l'' r'' | ⋙l .x' .x'' l'≃r' l''⋘r'' l'⋗r''
    with lemma-dropLast-⋙ (⋙l x' x'' l'≃r' l''⋘r'' l'⋗r'')
... | inj₁ l⋙rd =
                 let _l = node perfect x' l' r' ;
                      _r = node left x'' l'' r'' ;
                      zxflfrd∼xflzfrd = ∼x /head (lemma++/ {last _r compound} {x ∷ flatten _l}) refl∼ ;
                      xflzfrd∼xflfr = lemma++∼l {x ∷ flatten _l} (lemma-last-dropLast cr)
                 in trans∼ zxflfrd∼xflzfrd xflzfrd∼xflfr
... | inj₂ ()
lemma-last-dropLast (right x cl cr l⋙r) | node perfect x' l' r' | node right x'' l'' r'' | ⋙r .x' .x'' l'≃r' l''⋙r'' l'≃l''
    with lemma-dropLast-⋙ (⋙r x' x'' l'≃r' l''⋙r'' l'≃l'')
... | inj₁ l⋙rd =
                 let _l = node perfect x' l' r' ;
                      _r = node right x'' l'' r'' ;
                      zxflfrd∼xflzfrd = ∼x /head (lemma++/ {last _r compound} {x ∷ flatten _l}) refl∼ ;
                      xflzfrd∼xflfr = lemma++∼l {x ∷ flatten _l} (lemma-last-dropLast cr)
                 in trans∼ zxflfrd∼xflzfrd xflzfrd∼xflfr
... | inj₂ ()
lemma-last-dropLast (right x cl cr l⋙r) | node left _ _ _ | _ | ⋙p ()
lemma-last-dropLast (right x cl cr l⋙r) | node right _ _ _ | _ | ⋙p ()

lemma-dropLast-∼ : {t : Tag}{x : A}{l r : PLRTree} → Complete (node t x l r) → flatten (setRoot (last (node t x l r) compound) (dropLast (node t x l r))) ∼ (flatten l ++ flatten r)
lemma-dropLast-∼ (perfect {l} {r} x cl cr l≃r)
    with l | r | l≃r
... | leaf | leaf | ≃lf = ∼[]
... | node perfect x' l' r' | node perfect x'' l'' r'' | ≃nd .x' .x'' l'≃r' l''≃r'' l'≃l'' =
                 let _l = node perfect x' l' r' ;
                      _r = node perfect x'' l'' r'' ;
                      zflfrd∼flzfrd = ∼x /head (lemma++/ {last _r compound} {flatten _l}) refl∼ ;
                      flzfrd∼flfr = lemma++∼l {flatten _l} (lemma-last-dropLast cr)
                 in trans∼ zflfrd∼flzfrd flzfrd∼flfr
lemma-dropLast-∼ (left {l} {r} x cl cr l⋘r)
    with l | r | l⋘r | lemma-dropLast-⋘ l⋘r
... | leaf | _ | () | _
... | node perfect x' l' r' | _ | () | _
... | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₁ ld⋘r
    with dropLast (node left x' l' r') | ld⋘r | lemma-last-dropLast cl
... | leaf | () | _
... | node perfect _ _ _ | () | _
... | node left x''' l''' r''' | ld⋘r' | zfld∼fl = lemma++∼r zfld∼fl
... | node right x''' l''' r''' | ld⋘r' | zfld∼fl  = lemma++∼r zfld∼fl
lemma-dropLast-∼ (left x cl cr l⋘r) | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₂ ld≃r
    with dropLast (node left x' l' r') | ld≃r | lemma-last-dropLast cl
... | leaf | () | _
... | node perfect x''' l''' r''' | ld≃r' | zfld∼fl = lemma++∼r zfld∼fl
... | node left _ _ _ | () | _
... | node right _ _ _ | () | _
lemma-dropLast-∼ (left x cl cr l⋘r) | node right x' l' r' | leaf | () | _
lemma-dropLast-∼ (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₁ ()
lemma-dropLast-∼ (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₂ x'≃x''' =
                 lemma++∼r (lemma-last-dropLast cl)
lemma-dropLast-∼ (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₁ ld⋘r
    with dropLast (node right x' l' r') | ld⋘r | lemma-last-dropLast cl
... | leaf | () | _
... | node perfect _ _ _ | () | _
... | node left x''' l''' r''' | ld⋘r' | zfld∼fl = lemma++∼r zfld∼fl
... | node right x''' l''' r''' | ld⋘r' | zfld∼fl = lemma++∼r zfld∼fl
lemma-dropLast-∼ (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₂ ld≃r
    with dropLast (node right x' l' r') | ld≃r | lemma-last-dropLast cl
... | leaf | () | _
... | node perfect x''' l''' r''' | ld≃r' | zfld∼fl = lemma++∼r zfld∼fl
... | node left _ _ _ | () | _
... | node right _ _ _ | () | _
lemma-dropLast-∼ (left x cl cr l⋘r) | node right x' l' r' | node left x'' l'' r'' | () | _
lemma-dropLast-∼ (left x cl cr l⋘r) | node right x' l' r' | node right x'' l'' r'' | () | _
lemma-dropLast-∼ (right {l} {r} x cl cr l⋙r)
    with l | r | l⋙r
... | leaf | _ | ⋙p ()
... | node perfect x' leaf leaf | leaf | ⋙p (⋗lf .x') = ∼x /head /head ∼[]
... | node perfect x' leaf leaf | node left _ _ _ | ⋙p ()
... | node perfect x' leaf leaf | node right _ _ _ | ⋙p ()
... | node perfect x' l' r' | node perfect x'' l'' r'' | ⋙p (⋗nd .x' .x'' l'≃r' l''≃r'' l'⋗l'') = lemma++∼r (lemma-last-dropLast cl)
... | node perfect x' l' r' | node left x'' l'' r'' | ⋙l .x' .x'' l'≃r' l''⋘r'' l'⋗r''
    with lemma-dropLast-⋙ (⋙l x' x'' l'≃r' l''⋘r'' l'⋗r'')
... | inj₁ l⋙rd =
                 let _l = node perfect x' l' r' ;
                      _r = node left x'' l'' r'' ;
                      zflfrd∼flzfrd = ∼x /head (lemma++/ {last _r compound} {flatten _l}) refl∼ ;
                      flzfrd∼flfr = lemma++∼l {flatten _l} (lemma-last-dropLast cr)
                 in trans∼ zflfrd∼flzfrd flzfrd∼flfr
... | inj₂ ()
lemma-dropLast-∼ (right x cl cr l⋙r) | node perfect x' l' r' | node right x'' l'' r'' | ⋙r .x' .x'' l'≃r' l''⋙r'' l'≃l''
    with lemma-dropLast-⋙ (⋙r x' x'' l'≃r' l''⋙r'' l'≃l'')
... | inj₁ l⋙rd =
                 let _l = node perfect x' l' r' ;
                      _r = node right x'' l'' r'' ;
                      zflfrd∼flzfrd = ∼x /head (lemma++/ {last _r compound} {flatten _l}) refl∼ ;
                      flzfrd∼flfr = lemma++∼l {flatten _l} (lemma-last-dropLast cr)
                 in trans∼ zflfrd∼flzfrd flzfrd∼flfr
... | inj₂ ()
lemma-dropLast-∼ (right x cl cr l⋙r) | node left _ _ _ | _ | ⋙p ()
lemma-dropLast-∼ (right x cl cr l⋙r) | node right _ _ _ | _ | ⋙p ()

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Structs where

open import Data.List
open import Data.String
open import Data.Product hiding (map)
open import Relation.Binary.PropositionalEquality as PE hiding ([_])
open import Data.List.Any hiding (map)
open module M {ℓ}{X : Set ℓ} = Membership (PE.setoid X )
import Level

data StructEnd {ℓ} : Set ℓ where
  end : StructEnd

data StructField {ℓ}(s : String)(t : Set ℓ) : Set ℓ where
  _∹_ : (x : String) → {_ : x ≡ s} → t → StructField s t

FieldTypes = λ ℓ → List (String × Set ℓ)

Struct : ∀{ℓ} → FieldTypes ℓ → Set ℓ
Struct [] = StructEnd
Struct {ℓ} ( (n , t) ∷ l) = StructField {ℓ} n t × Struct l

infixr 6 _∶_∷_
data StructLit {ℓ} : FieldTypes ℓ → Set (Level.suc ℓ) where
  [] : StructLit []
  _∶_∷_ : ∀{t : Set ℓ}{ls} → (s : String) → t → StructLit ls → StructLit ((s , t) ∷ ls)

⟨_⟩ : ∀{ℓ}{ls} → StructLit {ℓ} ls → Struct ls
⟨ [] ⟩ = end
⟨ s ∶ x ∷ xs ⟩ = _∹_ s {refl} x , ⟨ xs ⟩

instance
  found-it : ∀{ℓ}{X : Set ℓ}{x : X}{xs : List X}
           → x ∈ (x ∷ xs)
  found-it = here refl
  keep-looking : ∀{ℓ}{X : Set ℓ}{x y : X}{xs : List X}
               → ⦃ t : y ∈ xs ⦄
               → y ∈ (x ∷ xs)
  keep-looking ⦃ t ⦄ = there t

lookup : ∀{ℓ ℓ′}{K : Set ℓ}{V : Set ℓ′}{s}
       → (l : List (K × V)) → s ∈ (map proj₁ l) → V
lookup [] ()
lookup (x ∷ l) (here refl) = proj₂ x
lookup (x ∷ l) (there p)   = lookup l p

update : ∀{ℓ ℓ′}{K : Set ℓ}{V : Set ℓ′}{s}
       → (l : List (K × V)) → s ∈ (map proj₁ l) → V → List (K × V)
update [] () _
update (x ∷ l) (here refl) n = (proj₁ x , n) ∷ l
update (x ∷ l) (there p) n = x ∷ update l p n

field-names = λ{ℓ}(ls : FieldTypes ℓ) → map proj₁ ls

infixl 6 _∙_

_∙_ : ∀{ℓ}{ls : FieldTypes ℓ}
    → Struct ls
    → (s : String) ⦃ prf : s ∈ field-names ls ⦄
    → lookup ls prf
_∙_ {ls = []} _ x ⦃ () ⦄
_∙_ {ls = x ∷ ls} (tg ∹ v , r) ._ ⦃ here refl ⦄ = v
_∙_ {ls = x ∷ ls} (k , r) x₁ ⦃ there prf ⦄ = _∙_ {ls = ls} r x₁ ⦃ prf ⦄

infixl 6 _∙_≔_

module TypeChangingAssignment where

  infixl 6 _∙_≔′_

  _∙_≔′_ : ∀{ℓ}{ls : FieldTypes ℓ}{X : Set ℓ}
        → Struct ls
        → (s : String) ⦃ prf : s ∈ field-names ls ⦄
        → X
        → Struct (update ls prf X)
  _∙_≔′_ {ls = []} s t ⦃ () ⦄ n
  _∙_≔′_ {ls = (q , _) ∷ ls} (_∹_ .q {refl} v , r) ._ ⦃ here refl ⦄ n = _∹_ q {refl} n , r
  _∙_≔′_ {ls = x ∷ ls} (t , r) k  ⦃ there prf ⦄ n = t , (r ∙ k ≔′ n)

  memb-update : ∀{ℓ ℓ′}{K : Set ℓ}{V : Set ℓ′}{ls : List (K × V)}{k}{x : V} → ⦃ prf : k ∈ map proj₁ ls ⦄ → k ∈ map proj₁ (update ls prf x)
  memb-update {ls = []} ⦃ () ⦄
  memb-update {ls = x ∷ ls} {{prf = here refl}} = here refl
  memb-update {ls = x ∷ ls} {{prf = there prf}} = there (memb-update {ls = ls} ⦃ prf ⦄)

  lookup-update : ∀{ℓ ℓ′}{K : Set ℓ}{V : Set ℓ′}{ls : List (K × V)}{k}{x : V}
        → ⦃ prf : k ∈ map proj₁ ls ⦄
        → lookup (update ls prf x) (memb-update ⦃ prf ⦄) ≡ x
  lookup-update {ls = []} ⦃ prf = () ⦄
  lookup-update {ls = x ∷ ls} ⦃ prf = here refl ⦄ = refl
  lookup-update {ls = x ∷ ls} ⦃ prf = there prf ⦄ = lookup-update {ls = ls} ⦃ prf ⦄

  update-lookup : ∀{ℓ ℓ′}{K : Set ℓ}{V : Set ℓ′}{ls : List (K × V)}{k}
                → ⦃ prf : k ∈ map proj₁ ls ⦄
                → update ls prf (lookup ls prf) ≡ ls
  update-lookup {ls = []} ⦃ () ⦄
  update-lookup {ls = x ∷ ls} ⦃ here refl ⦄ = refl
  update-lookup {ls = x ∷ ls} ⦃ there prf ⦄ rewrite update-lookup {ls = ls} ⦃ prf ⦄ = refl

_∙_≔_ : ∀{ℓ}{ls : FieldTypes ℓ}
      → Struct ls
      → (s : String) ⦃ prf : s ∈ field-names ls ⦄
      → lookup ls prf
      → Struct ls
_∙_≔_ {ls = []} s f ⦃ () ⦄ v
_∙_≔_ {ls = x ∷ ls} (_∹_ ._ {refl} _ , r) ._ ⦃ here refl ⦄ v = _∹_ (proj₁ x) {refl} v , r
_∙_≔_ {ls = x ∷ ls} (k , r) f ⦃ there prf ⦄ v = k , r ∙ f ≔ v

spurious-update : ∀{ℓ}{ls : FieldTypes ℓ}{s : Struct ls}{f}
                → ⦃ prf : f ∈ field-names ls ⦄
                → (s ∙ f ≔ (s ∙ f)) ≡ s
spurious-update {ls = []}                         ⦃ () ⦄
spurious-update {ls = _ ∷ _}{_∹_ ._ {refl} _ , _} ⦃ here refl ⦄ = refl
spurious-update {ls = _ ∷ _}{_∹_ ._ {refl} _ , _} ⦃ there prf ⦄ = cong (_,_ _) spurious-update

read-after-update : ∀{ℓ}{ls : FieldTypes ℓ}{s : Struct ls}{f}
                  → ⦃ prf : f ∈ field-names ls ⦄
                  → {v : lookup ls prf}
                  → (s ∙ f ≔ v) ∙ f ≡ v
read-after-update {ls = []}                           ⦃ () ⦄
read-after-update {ls = _ ∷ _}{ _∹_ ._ {refl} _ , _ } ⦃ here refl ⦄ = refl
read-after-update {ls = _ ∷ _}{ _∹_ ._ {refl} _ , _ } ⦃ there prf ⦄ = read-after-update ⦃ prf ⦄

frame-inertia : ∀{ℓ}{ls : FieldTypes ℓ}{s : Struct ls}{f f′}
              → f ≢ f′
              → ⦃ prf : f  ∈ field-names ls ⦄
              → ⦃ prf′ : f′ ∈ field-names ls ⦄
              → {v : lookup ls prf′}
              → (s ∙ f′ ≔ v) ∙ f ≡ (s ∙ f)
frame-inertia {ls = []}                            _ ⦃ () ⦄
frame-inertia {ls = _ ∷ ls}{ _∹_ ._ {refl} _ , _ } _ ⦃ here refl ⦄ ⦃ there prf′ ⦄ = refl
frame-inertia {ls = _ ∷ ls}{ _∹_ ._ {refl} _ , _ } _ ⦃ there prf ⦄ ⦃ here refl  ⦄ = refl
frame-inertia {ls = _ ∷ ls}{ _∹_ ._ {refl} _ , _ } p ⦃ there prf ⦄ ⦃ there prf′ ⦄ = frame-inertia {ls = ls} p
frame-inertia {ls = _ ∷ ls}{ _∹_ ._ {refl} _ , _ } p ⦃ here refl ⦄ ⦃ here refl  ⦄ with p refl
... | ()

append : ∀{ℓ}{ls : FieldTypes ℓ}{ms : FieldTypes ℓ} → Struct ls → Struct ms → Struct (Data.List._++_ ls ms)
append {ls = [] } s₁ s₂ = s₂
append {ls = x ∷ xs} (f , rest) s₂ = f , append rest s₂

drop-append : ∀{ℓ}{ls : FieldTypes ℓ}{ms : FieldTypes ℓ} → Struct (Data.List._++_ ls ms) → Struct ms
drop-append {ls = []} m = m
drop-append {ls = x ∷ xs} (f , rest) = drop-append {ls = xs} rest

ext: agda

max_stars_repo_name: liamoc/structs

max_issues_repo_name: liamoc/structs

max_forks_repo_name: liamoc/structs


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.ZCohomology.Groups.Sn where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.MayerVietorisUnreduced
open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Connected
open import Cubical.ZCohomology.KcompPrelims
open import Cubical.ZCohomology.Groups.Prelims

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

open import Cubical.HITs.Pushout
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Susp
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim ; elim2 to sElim2)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim ; elim2 to pElim2 ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁)
open import Cubical.HITs.Nullification

open import Cubical.Data.Sigma
open import Cubical.Data.Int renaming (_+_ to _+ℤ_; +-comm to +ℤ-comm ; +-assoc to +ℤ-assoc)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec)
open import Cubical.Data.Unit

open import Cubical.Algebra.Group

infixr 31 _□_
_□_ : _
_□_ = compGroupEquiv

open GroupEquiv
open vSES

Sn-connected : (n : ℕ) (x : S₊ (suc n)) → ∥ north ≡ x ∥₁
Sn-connected n = suspToPropRec north (λ _ → propTruncIsProp) ∣ refl ∣₁

H⁰-Sⁿ≅ℤ : (n : ℕ) → GroupEquiv (coHomGr 0 (S₊ (suc n))) intGroup
H⁰-Sⁿ≅ℤ n = H⁰-connected north (Sn-connected n)

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

--- We will need to switch between Sⁿ defined using suspensions and using pushouts
--- in order to apply Mayer Vietoris.

coHomPushout≅coHomSn : (n m : ℕ) → GroupEquiv (coHomGr m (S₊ (suc n))) (coHomGr m (Pushout {A = S₊ n} (λ _ → tt) λ _ → tt))
coHomPushout≅coHomSn n m = transport (λ i → GroupEquiv (coHomGr m (PushoutSusp≡Susp {A = S₊ n} i))
                                       (coHomGr m (Pushout {A = S₊ n} (λ _ → tt) λ _ → tt))) (idGroupEquiv _)

-------------------------- H⁰(S⁰) -----------------------------
S0→Int : (a : Int × Int) → S₊ 0 → Int
S0→Int a north = fst a
S0→Int a south = snd a

H⁰-S⁰≅ℤ×ℤ : GroupEquiv (coHomGr 0 (S₊ 0)) (dirProd intGroup intGroup)
eq H⁰-S⁰≅ℤ×ℤ =
  isoToEquiv (iso (sRec (isOfHLevelΣ 2 isSetInt λ _ → isSetInt) λ f → (f north) , (f south))
                  (λ a → ∣ S0→Int a ∣₂)
                  (λ _ → refl)
                  (sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                         λ f → cong ∣_∣₂ (funExt (λ {north → refl ; south → refl}))))
isHom H⁰-S⁰≅ℤ×ℤ =
  sElim2 (λ _ _ → isOfHLevelPath 2 (isOfHLevelΣ 2 isSetInt (λ _ → isSetInt)) _ _)
         λ a b i → addLemma (a north) (b north) i , addLemma (a south) (b south) i

-- --------------------------H¹(S¹) -----------------------------------
{-
In order to apply Mayer-Vietoris, we need the following lemma.
Given the following diagram
  a ↦ (a , 0)   ψ         ϕ
 A -->  A × A -------> B --->  C
If ψ is an isomorphism and ϕ is surjective with ker ϕ ≡ {ψ (a , a) ∣ a ∈ A}, then C ≅ B
-}

diagonalIso : ∀ {ℓ ℓ' ℓ''} {A : Group {ℓ}} (B : Group {ℓ'}) {C : Group {ℓ''}}
               (ψ : GroupEquiv (dirProd A A) B) (ϕ : GroupHom B C)
             → isSurjective _ _ ϕ
             → ((x : ⟨ B ⟩) → isInKer B C ϕ x
                                    → ∃[ y ∈ ⟨ A ⟩ ] x ≡ fst (eq ψ) (y , y))
             → ((x : ⟨ B ⟩) → (∃[ y ∈ ⟨ A ⟩ ] x ≡ fst (eq ψ) (y , y))
                                    → isInKer B C ϕ x)
             → GroupEquiv A C
diagonalIso {A = A} B {C = C} ψ ϕ issurj ker→diag diag→ker =
  BijectionIsoToGroupEquiv
    (bij-iso (compGroupHom fstProj (compGroupHom (grouphom (fst (eq ψ)) (isHom ψ)) ϕ))
          (λ a inker
           → pRec (isSetCarrier A _ _)
                   (λ {(a' , id) → cong fst (sym (secEq (eq ψ) (a , 0g A)) ∙∙ cong (invEq (eq ψ)) id ∙∙ secEq (eq ψ) (a' , a'))
                                  ∙ cong snd (sym (secEq (eq ψ) (a' , a')) ∙∙ cong (invEq (eq ψ)) (sym id) ∙∙ secEq (eq ψ) (a , 0g A))})
                   (ker→diag _ inker))
          λ c → pRec propTruncIsProp
                     (λ { (b , id) → ∣ (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b))) -- (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)))
                                     , (sym (Group.rid C _)
                                     ∙∙ cong ((fun ϕ) (equivFun (eq ψ) (fst (ψ⁻ b) A.+ (A.- snd (ψ⁻ b)) , 0g A)) C.+_)
                                            (sym (diag→ker (equivFun (eq ψ) ((snd (ψ⁻ b)) , (snd (ψ⁻ b))))
                                                            ∣ (snd (ψ⁻ b)) , refl ∣₁))
                                     ∙∙ sym ((isHom ϕ) _ _))
                                     ∙∙ cong (fun ϕ) (sym ((isHom ψ) _ _)
                                                  ∙∙ cong (equivFun (eq ψ)) (ΣPathP (sym (Group.assoc A _ _ _)
                                                                                ∙∙ cong (fst (ψ⁻ b) A.+_) (Group.invl A _)
                                                                                ∙∙ Group.rid A _
                                                                                , (Group.lid A _)))
                                                  ∙∙ retEq (eq ψ) b)
                                     ∙∙ id ∣₁ })
                     (issurj c))
  where
  open Group
  open IsGroup
  open GroupHom
  module A = Group A
  module B = Group B
  module C = Group C
  module A×A = Group (dirProd A A)
  module ψ = GroupEquiv ψ
  module ϕ = GroupHom ϕ
  ψ⁻ = fst (invEquiv (eq ψ))

  fstProj : GroupHom A (dirProd A A)
  fun fstProj a = a , 0g A
  isHom fstProj g0 g1 i = (g0 A.+ g1) , Group.lid A (0g A) (~ i)

H¹-S¹≅ℤ : GroupEquiv intGroup (coHomGr 1 (S₊ 1))
H¹-S¹≅ℤ =
    diagonalIso (coHomGr 0 (S₊ 0))
                (invGroupEquiv H⁰-S⁰≅ℤ×ℤ)
                (I.d 0)
                (λ x → I.Ker-i⊂Im-d 0 x
                                     (ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _
                                            , isOfHLevelSuc 0 (isContrHⁿ-Unit 0) _ _)))
                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
                        (λ x inker
                            → pRec propTruncIsProp
                                    (λ {((f , g) , id') → helper x f g id' inker})
                                    ((I.Ker-d⊂Im-Δ 0 ∣ x ∣₂ inker)))))
                ((sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                         λ F surj
                           → pRec (setTruncIsSet _ _)
                                   (λ { (x , id) → I.Im-Δ⊂Ker-d 0 ∣ F ∣₂
                                                      ∣ (∣ (λ _ → x) ∣₂ , ∣ (λ _ → 0) ∣₂) ,
                                                       (cong ∣_∣₂ (funExt (surjHelper x))) ∙ sym id ∣₁ })
                                   surj) )
  □ invGroupEquiv (coHomPushout≅coHomSn 0 1)
  where
  module I = MV Unit Unit (S₊ 0) (λ _ → tt) (λ _ → tt)

  surjHelper :  (x : Int) (x₁ : S₊ 0) → x +ₖ (-ₖ pos 0) ≡ S0→Int (x , x) x₁
  surjHelper x north = cong (x +ₖ_) (-0ₖ) ∙ rUnitₖ x
  surjHelper x south = cong (x +ₖ_) (-0ₖ) ∙ rUnitₖ x

  helper : (F : S₊ 0 → Int) (f g : ∥ (Unit → Int) ∥₂)
           (id : GroupHom.fun (I.Δ 0) (f , g) ≡ ∣ F ∣₂)
         → isInKer (coHomGr 0 (S₊ 0))
                    (coHomGr 1 (Pushout (λ _ → tt) (λ _ → tt)))
                    (I.d 0)
                    ∣ F ∣₂
         → ∃[ x ∈ Int ] ∣ F ∣₂ ≡ equivFun (invEquiv (eq H⁰-S⁰≅ℤ×ℤ)) (x , x)
  helper F =
    sElim2 (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
           λ f g id inker
             → pRec propTruncIsProp
                     (λ ((a , b) , id2)
                        → sElim2 {B = λ f g → GroupHom.fun (I.Δ 0) (f , g) ≡ ∣ F ∣₂ → _ }
                                  (λ _ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp)
                                  (λ f g id → ∣ (helper2 f g .fst) , (sym id ∙ sym (helper2 f g .snd)) ∣₁)
                                  a b id2)
                     (MV.Ker-d⊂Im-Δ _ _ (S₊ 0) (λ _ → tt) (λ _ → tt) 0 ∣ F ∣₂ inker)
    where
    helper2 : (f g : Unit → Int)
            → Σ[ x ∈ Int ] (equivFun (invEquiv (eq H⁰-S⁰≅ℤ×ℤ))) (x , x)
             ≡ GroupHom.fun (I.Δ 0) (∣ f ∣₂ , ∣ g ∣₂)
    helper2 f g = (f _ +ₖ (-ₖ g _) ) , cong ∣_∣₂ (funExt (λ {north → refl ; south → refl}))

------------------------- H¹(S⁰) ≅ 0 -------------------------------

private
  Hⁿ-S0≃Kₙ×Kₙ : (n : ℕ) → Iso (S₊ 0 → coHomK (suc n)) (coHomK (suc n) × coHomK (suc n))
  Iso.fun (Hⁿ-S0≃Kₙ×Kₙ n) f = (f north) , (f south)
  Iso.inv (Hⁿ-S0≃Kₙ×Kₙ n) (a , b) north = a
  Iso.inv (Hⁿ-S0≃Kₙ×Kₙ n) (a , b) south = b
  Iso.rightInv (Hⁿ-S0≃Kₙ×Kₙ n) a = refl
  Iso.leftInv (Hⁿ-S0≃Kₙ×Kₙ n) b = funExt λ {north → refl ; south → refl}

  isContrHⁿ-S0 : (n : ℕ) → isContr (coHom (suc n) (S₊ 0))
  isContrHⁿ-S0 n =
    transport (λ i → isContr ∥ isoToPath (Hⁿ-S0≃Kₙ×Kₙ n) (~ i) ∥₂)
      (transport (λ i → isContr (isoToPath (setTruncOfProdIso {A = coHomK (suc n)} {B = coHomK (suc n)} ) (~ i)))
         ((∣ 0ₖ ∣₂ , ∣ 0ₖ ∣₂)
         , prodElim (λ _ → isOfHLevelSuc 1 (isOfHLevelΣ 2 setTruncIsSet (λ _ → setTruncIsSet) _ _))
            (elim2 (λ _ _ → isProp→isOfHLevelSuc (2 + n) (isOfHLevelΣ 2 setTruncIsSet (λ _ → setTruncIsSet) _ _))
              (suspToPropRec2 north (λ _ _ → isOfHLevelΣ 2 setTruncIsSet (λ _ → setTruncIsSet) _ _) refl))))

H¹-S⁰≅0 : (n : ℕ) → GroupEquiv (coHomGr (suc n) (S₊ 0)) trivialGroup
H¹-S⁰≅0 n = contrGroup≅trivialGroup (isContrHⁿ-S0 n)

------------------------- H²(S¹) ≅ 0 -------------------------------

H²-S¹≅0 : GroupEquiv (coHomGr 2 (S₊ 1)) trivialGroup
H²-S¹≅0 =
    coHomPushout≅coHomSn 0 2
  □ (invGroupEquiv (vSES→GroupEquiv _ _ vSES-helper))
  □ (H¹-S⁰≅0 0)
  where
  module I = MV Unit Unit (S₊ 0) (λ _ → tt) (λ _ → tt)
  vSES-helper : vSES (coHomGr 1 (S₊ 0)) (coHomGr 2 (Pushout (λ _ → tt) (λ _ → tt)))
                     _ _
  isTrivialLeft vSES-helper = isOfHLevelSuc 0 (isOfHLevelΣ 0 (isContrHⁿ-Unit 0) (λ _ → isContrHⁿ-Unit 0))
  isTrivialRight vSES-helper = isOfHLevelSuc 0 (isOfHLevelΣ 0 (isContrHⁿ-Unit 1) (λ _ → isContrHⁿ-Unit 1))
  left vSES-helper = I.Δ 1
  right vSES-helper = I.i 2
  vSES.ϕ vSES-helper = I.d 1
  Ker-ϕ⊂Im-left vSES-helper = I.Ker-d⊂Im-Δ 1
  Ker-right⊂Im-ϕ vSES-helper = sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 propTruncIsProp) -- doesn't terminate without elimination
                                          λ a → I.Ker-i⊂Im-d 1 ∣ a ∣₂

--------------- H¹(Sⁿ), n ≥ 1 --------------------------------------------

H¹-Sⁿ≅0 : (n : ℕ) → GroupEquiv (coHomGr 1 (S₊ (2 + n))) trivialGroup
H¹-Sⁿ≅0 n = coHomPushout≅coHomSn (1 + n) 1
         □ BijectionIsoToGroupEquiv
            (bij-iso (I.i 1)
                     helper
                     λ x → ∣ 0ₕ , isOfHLevelSuc 0 (isOfHLevelΣ 0 (isContrHⁿ-Unit zero) (λ _ → isContrHⁿ-Unit zero)) _ x ∣₁)
         □ dirProdEquiv (Hⁿ-Unit≅0 zero) (Hⁿ-Unit≅0 zero)
         □ lUnitGroupIso
  where
    module I = MV Unit Unit (S₊ (1 + n)) (λ _ → tt) (λ _ → tt)
    surj-helper : (x : ⟨ coHomGr 0 (S₊ _) ⟩) → isInIm _ _ (I.Δ 0) x
    surj-helper =
      sElim (λ _ → isOfHLevelSuc 1 propTruncIsProp)
             λ f → ∣ (∣ (λ _ → f north) ∣₂ , 0ₕ)
                   , (cong ∣_∣₂ (funExt (suspToPropRec north
                                         (λ _ → isSetInt _ _)
                                         (cong (f north +ₖ_) -0ₖ  ∙ rUnitₖ (f north))))) ∣₁
    helper : isInjective _ _ (I.i 1)
    helper =
      sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 (setTruncIsSet _ _))  -- useless elimination speeds things up significantly
             λ x inker → pRec (setTruncIsSet _ _)
                              (sigmaElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                          λ a id → sym id ∙ I.Im-Δ⊂Ker-d 0 ∣ a ∣₂ (surj-helper _))
                              (I.Ker-i⊂Im-d 0 ∣ x ∣₂ inker)

--------- Direct proof of H¹(S¹) ≅ ℤ without Mayer-Vietoris -------

-- The strategy is to use the proof that ΩS¹ ≃ ℤ. Since we only have this for S¹ with the base/loop definition
-- we begin with some functions translating between H¹(S₊ 1) and ∥ S¹ → S¹ ∥₀.  The latter type is easy to characterise,
-- by (S¹ → S¹) ≃ S¹ × ℤ (see Cubical.ZCohomology.Groups.Prelims). Truncating this leaves only ℤ, since S¹ is connected.

-- The translation mentioned above uses the basechange function. We use basechange-lemma (Cubical.ZCohomology.Groups.Prelims) to prove the basechange2⁻ preserves
-- path composition (in a more general sense than what is proved in basechange2⁻-morph)

-- We can now give the group equivalence. The first bit is just a big composition of our previously defined translations and is pretty uninteresting.
-- The harder step is proving that the equivalence is a morphism. This relies heavily on the fact that addition the cohomology groups essentially is defined using an
-- application of cong₂, which allows us to use basechange-lemma.

coHom1S1≃ℤ : GroupEquiv (coHomGr 1 (S₊ 1)) intGroup
eq coHom1S1≃ℤ = isoToEquiv theIso
  where
  F = Iso.fun S¹→S¹≡S¹×Int
  F⁻ = Iso.inv S¹→S¹≡S¹×Int
  G = Iso.fun S1→S1≡S¹→S¹
  G⁻ = Iso.inv S1→S1≡S¹→S¹

  theIso : Iso ⟨ coHomGr 1 (S₊ 1) ⟩ ⟨ intGroup ⟩
  Iso.fun theIso = sRec isSetInt (λ f → snd (F (G f)))
  Iso.inv theIso a = ∣ G⁻ (F⁻ (base , a)) ∣₂
  Iso.rightInv theIso a =
      (cong (snd ∘ F) (Iso.rightInv S1→S1≡S¹→S¹ (F⁻ (base , a)))
     ∙ cong snd (Iso.rightInv S¹→S¹≡S¹×Int (base , a)))
  Iso.leftInv theIso =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
          λ f → cong ((sRec setTruncIsSet (λ x → ∣ G⁻ x ∣₂))
                        ∘ sRec setTruncIsSet λ x → ∣ F⁻ (x , (snd (F (G f)))) ∣₂)
                      (Iso.inv PathIdTrunc₀Iso (isConnectedS¹ (fst (F (G f)))))
               ∙∙ cong (∣_∣₂ ∘ G⁻) (Iso.leftInv S¹→S¹≡S¹×Int (G f))
               ∙∙ cong ∣_∣₂ (Iso.leftInv S1→S1≡S¹→S¹ f)
isHom coHom1S1≃ℤ =
  sElim2 (λ _ _ → isOfHLevelPath 2 isSetInt _ _)
           λ f g → (λ i → winding (guy (ΩKn+1→Kn (Kn→ΩKn+1 1 (f (S¹→S1 base)) ∙ Kn→ΩKn+1 1 (g (S¹→S1 base))))
                                    (λ i → pre-guy (ΩKn+1→Kn (Kn→ΩKn+1 1 (f (S¹→S1 (loop i))) ∙ Kn→ΩKn+1 1 (g (S¹→S1 (loop i))))))))
                 ∙∙ cong winding (helper (f (S¹→S1 base)) (g (S¹→S1 base)) f g refl refl)
                 ∙∙ winding-hom (guy (f north)
                                     (λ i → pre-guy (f (S¹→S1 (loop i)))))
                                (guy (g north)
                                     (λ i → pre-guy (g (S¹→S1 (loop i)))))
  where
  pre-guy = S¹map ∘ trMap S1→S¹
  guy = basechange2⁻ ∘ pre-guy

  helper : (x y : coHomK 1) (f g : S₊ 1 → coHomK 1)
        → (f (S¹→S1 base)) ≡ x
        → (g (S¹→S1 base)) ≡ y
        → (guy (ΩKn+1→Kn (Kn→ΩKn+1 1 (f (S¹→S1 base)) ∙ Kn→ΩKn+1 1 (g (S¹→S1 base))))
                (λ i → S¹map (trMap S1→S¹ (ΩKn+1→Kn (Kn→ΩKn+1 1 (f (S¹→S1 (loop i))) ∙ Kn→ΩKn+1 1 (g (S¹→S1 (loop i))))))))
          ≡ (guy (f (S¹→S1 base))
                 (λ i → pre-guy (f (S¹→S1 (loop i)))))
          ∙ (guy (g (S¹→S1 base))
                 (λ i → pre-guy ((g (S¹→S1 (loop i))))))
  helper = elim2 (λ _ _ → isGroupoidΠ4 λ _ _ _ _ → isOfHLevelPath 3 (isOfHLevelSuc 3 (isGroupoidS¹) base base) _ _)
                 (suspToPropRec2 {A = S₊ 0} north
                      (λ _ _ → isPropΠ4 λ _ _ _ _ → isGroupoidS¹ _ _ _ _)
                      λ f g reflf reflg →
                     (basechange-lemma
                        base
                        base
                        (λ x → S¹map (trMap S1→S¹ (ΩKn+1→Kn x)))
                        (λ x → Kn→ΩKn+1 1 (f (S¹→S1 x)))
                        ((λ x → Kn→ΩKn+1 1 (g (S¹→S1 x))))
                        (cong (Kn→ΩKn+1 1) reflf ∙ Kn→ΩKn+10ₖ 1)
                        (cong (Kn→ΩKn+1 1) reflg ∙ Kn→ΩKn+10ₖ 1))
                   ∙ λ j → guy (Iso.leftInv (Iso3-Kn-ΩKn+1 1) (f (S¹→S1 base)) j)
                                (λ i → pre-guy (Iso.leftInv (Iso3-Kn-ΩKn+1 1) (f (S¹→S1 (loop i))) j))
                         ∙ guy (Iso.leftInv (Iso3-Kn-ΩKn+1 1) (g (S¹→S1 base)) j)
                               (λ i → pre-guy (Iso.leftInv (Iso3-Kn-ΩKn+1 1) (g (S¹→S1 (loop i))) j)))

---------------------------- Hⁿ(Sⁿ) ≅ ℤ , n ≥ 1 -------------------

Hⁿ-Sⁿ≅ℤ : (n : ℕ) → GroupEquiv intGroup (coHomGr (suc n) (S₊ (suc n)))
Hⁿ-Sⁿ≅ℤ zero = invGroupEquiv coHom1S1≃ℤ
Hⁿ-Sⁿ≅ℤ (suc n) =
    Hⁿ-Sⁿ≅ℤ n
  □ vSES→GroupEquiv _ _ theIso
  □ invGroupEquiv (coHomPushout≅coHomSn (suc n) (suc (suc n)))
  where
  module I = MV Unit Unit (S₊ (suc n)) (λ _ → tt) (λ _ → tt)
  theIso : vSES (coHomGr (suc n) (S₊ (suc n))) (coHomGr (suc (suc n))
                (Pushout {A = S₊ (suc n)} (λ _ → tt) (λ _ → tt)))
                _
                _
  isTrivialLeft theIso p q = ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit n) (fst p) (fst q)
                                        , isOfHLevelSuc 0 (isContrHⁿ-Unit n) (snd p) (snd q))
  isTrivialRight theIso p q = ΣPathP (isOfHLevelSuc 0 (isContrHⁿ-Unit (suc n)) (fst p) (fst q)
                                         , isOfHLevelSuc 0 (isContrHⁿ-Unit (suc n)) (snd p) (snd q))
  left theIso = I.Δ (suc n)
  right theIso = I.i (2 + n)
  vSES.ϕ theIso = I.d (suc n)
  Ker-ϕ⊂Im-left theIso = I.Ker-d⊂Im-Δ  (suc n)
  Ker-right⊂Im-ϕ theIso = I.Ker-i⊂Im-d (suc n)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
open import Agda.Builtin.Nat

foo : Nat → Nat → Nat
foo 0 m = {!m!}
foo (suc n) m = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import lib.Base
open import lib.NType
open import lib.Relation
open import lib.types.Bool
open import lib.types.Int

module lib.types.List where

infixr 80 _::_

data List {i} (A : Type i) : Type i where
  nil : List A
  _::_ : A → List A → List A

data HList {i} : List (Type i) → Type (lsucc i) where
  nil : HList nil
  _::_ : {A : Type i} {L : List (Type i)} → A → HList L → HList (A :: L)

hlist-curry-type : ∀ {i j} (L : List (Type i))
  (B : HList L → Type (lmax i j)) → Type (lmax i j)
hlist-curry-type nil B = B nil
hlist-curry-type {j = j} (A :: L) B =
  (x : A) → hlist-curry-type {j = j} L (λ xs → B (x :: xs))

hlist-curry : ∀ {i j} {L : List (Type i)} {B : HList L → Type (lmax i j)}
  (f : Π (HList L) B) → hlist-curry-type {j = j} L B
hlist-curry {L = nil} f = f nil
hlist-curry {L = A :: _} f = λ x → hlist-curry (λ xs → f (x :: xs))

infixr 80 _++_
_++_ : ∀ {i} {A : Type i} → List A → List A → List A
nil ++ l = l
(x :: l₁) ++ l₂ = x :: (l₁ ++ l₂)

++-nil-r : ∀ {i} {A : Type i} (l : List A) → l ++ nil == l
++-nil-r nil      = idp
++-nil-r (a :: l) = ap (a ::_) $ ++-nil-r l

-- [any] in Haskell
data Any {i j} {A : Type i} (P : A → Type j) : List A → Type (lmax i j) where
  here : ∀ {a} {l} → P a → Any P (a :: l)
  there : ∀ {a} {l} → Any P l → Any P (a :: l)

infix 80 _∈_
_∈_ : ∀ {i} {A : Type i} → A → List A → Type i
a ∈ l = Any (_== a) l

Any-dec : ∀ {i j} {A : Type i} (P : A → Type j) → (∀ a → Dec (P a)) → (∀ l → Dec (Any P l))
Any-dec P _   nil       = inr λ{()}
Any-dec P dec (a :: l) with dec a
... | inl p = inl $ here p
... | inr p⊥ with Any-dec P dec l
...   | inl ∃p = inl $ there ∃p
...   | inr ∃p⊥ = inr λ{(here p) → p⊥ p; (there ∃p) → ∃p⊥ ∃p}

∈-dec : ∀ {i} {A : Type i} → has-dec-eq A → ∀ a l → Dec (a ∈ l)
∈-dec dec a l = Any-dec (_== a) (λ a' → dec a' a) l

Any-++-l : ∀ {i j} {A : Type i} (P : A → Type j)
  → ∀ l₁ l₂ → Any P l₁ → Any P (l₁ ++ l₂)
Any-++-l P _ _ (here p)   = here p
Any-++-l P _ _ (there ∃p) = there (Any-++-l P _ _ ∃p)

∈-++-l : ∀ {i} {A : Type i} (a : A) → ∀ l₁ l₂ → a ∈ l₁ → a ∈ (l₁ ++ l₂)
∈-++-l a = Any-++-l (_== a)

Any-++-r : ∀ {i j} {A : Type i} (P : A → Type j)
  → ∀ l₁ l₂ → Any P l₂ → Any P (l₁ ++ l₂)
Any-++-r P nil      _ ∃p = ∃p
Any-++-r P (a :: l) _ ∃p = there (Any-++-r P l _ ∃p)

∈-++-r : ∀ {i} {A : Type i} (a : A) → ∀ l₁ l₂ → a ∈ l₂ → a ∈ (l₁ ++ l₂)
∈-++-r a = Any-++-r (_== a)

Any-++ : ∀ {i j} {A : Type i} (P : A → Type j)
  → ∀ l₁ l₂ → Any P (l₁ ++ l₂) → (Any P l₁) ⊔ (Any P l₂)
Any-++ P nil       l₂ ∃p         = inr ∃p
Any-++ P (a :: l₁) l₂ (here p)   = inl (here p)
Any-++ P (a :: l₁) l₂ (there ∃p) with Any-++ P l₁ l₂ ∃p
... | inl ∃p₁ = inl (there ∃p₁)
... | inr ∃p₂ = inr ∃p₂

∈-++ : ∀ {i} {A : Type i} (a : A) → ∀ l₁ l₂ → a ∈ (l₁ ++ l₂) → (a ∈ l₁) ⊔ (a ∈ l₂)
∈-++ a = Any-++ (_== a)

-- [map] in Haskell
map : ∀ {i j} {A : Type i} {B : Type j} → (A → B) → (List A → List B)
map f nil = nil
map f (a :: l) = f a :: map f l

-- [foldr] in Haskell
foldr : ∀ {i j} {A : Type i} {B : Type j} → (A → B → B) → B → List A → B
foldr f b nil = b
foldr f b (a :: l) = f a (foldr f b l)

-- [concat] in Haskell
concat : ∀ {i} {A : Type i} → List (List A) → List A
concat l = foldr _++_ nil l

ℤsum = foldr _ℤ+_ 0

-- [filter] in Haskell
-- Note that [Bool] is currently defined as a coproduct.
filter : ∀ {i j k} {A : Type i} {Keep : A → Type j} {Drop : A → Type k}
  → ((a : A) → Keep a ⊔ Drop a) → List A → List A
filter p nil = nil
filter p (a :: l) with p a
... | inl _ = a :: filter p l
... | inr _ = filter p l

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

open import Setoids.Setoids
open import Rings.Definition
open import Rings.Orders.Partial.Definition
open import Sets.EquivalenceRelations
open import Sequences
open import Setoids.Orders.Partial.Definition
open import Functions.Definition
open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Groups.Definition

module Rings.Orders.Partial.Bounded {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} (pRing : PartiallyOrderedRing R pOrder) where

open Group (Ring.additiveGroup R)
open import Groups.Lemmas (Ring.additiveGroup R)
open Setoid S
open Equivalence eq
open SetoidPartialOrder pOrder

BoundedAbove : Sequence A → Set (m ⊔ o)
BoundedAbove x = Sg A (λ K → (n : ℕ) → index x n < K)

BoundedBelow : Sequence A → Set (m ⊔ o)
BoundedBelow x = Sg A (λ K → (n : ℕ) → K < index x n)

Bounded : Sequence A → Set (m ⊔ o)
Bounded x = Sg A (λ K → (n : ℕ) → ((Group.inverse (Ring.additiveGroup R) K) < index x n) && (index x n < K))

boundNonzero : {s : Sequence A} → (b : Bounded s) → underlying b ∼ 0G → False
boundNonzero {s} (a , b) isEq with b 0
... | bad1 ,, bad2 = irreflexive (<Transitive bad1 (<WellDefined reflexive (transitive isEq (symmetric (transitive (inverseWellDefined isEq) invIdent))) bad2))


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Transitive closures
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Construct.Closure.Transitive module directly.
------------------------------------------------------------------------

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

module Data.Plus where

open import Relation.Binary.Construct.Closure.Transitive public


text:
module LiftGet where

open import Data.Unit using (⊤ ; tt)
open import Data.Nat using (ℕ ; suc)
open import Data.Vec using (Vec ; toList ; fromList) renaming ([] to []V ; _∷_ to _∷V_ ; map to mapV)
open import Data.List using (List ; [] ; _∷_ ; length ; replicate ; map)
open import Data.List.Properties using (length-map)
open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
open import Function using (_∘_ ; flip ; const)
open import Relation.Binary.Core using (_≡_)
open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance ; module ≡-Reasoning)
open import Relation.Binary.HeterogeneousEquality as H using (module ≅-Reasoning ; _≅_ ; ≅-to-≡ ; ≡-to-≅ ; ≡-subst-removable) renaming (refl to het-refl ; sym to het-sym ; cong to het-cong ; reflexive to het-reflexive)

import FreeTheorems
open import Generic using (length-replicate ; toList-fromList ; toList-subst)
open FreeTheorems.ListList using (get-type) renaming (free-theorem to free-theoremL ; Get to GetL ; module Get to GetL)
open FreeTheorems.VecVec using () renaming (get-type to getV-type ; Get to GetV ; module Get to GetV)

getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type
getVec-to-getList get = toList ∘ get ∘ fromList

fromList∘map : {α β : Set} → (f : α → β) → (l : List α) → fromList (map f l) ≅ mapV f (fromList l)
fromList∘map f []       = het-refl
fromList∘map f (x ∷ xs) = H.cong₂ (λ n → _∷V_ {n = n} (f x)) (H.reflexive (length-map f xs)) (fromList∘map f xs)

toList∘map : {α β : Set} {n : ℕ} → (f : α → β) → (v : Vec α n) → toList (mapV f v) ≡ map f (toList v)
toList∘map f []V       = refl
toList∘map f (x ∷V xs) = cong (_∷_ (f x)) (toList∘map f xs)

GetV-to-GetL : GetV → GetL
GetV-to-GetL getrecord = record { get = toList ∘ get ∘ fromList; free-theorem = ft }
  where open GetV getrecord
        open ≡-Reasoning
        ft : {α β : Set} → (f : α → β) → (xs : List α) → toList (get (fromList (map f xs))) ≡ map f (toList (get (fromList xs)))
        ft f xs = begin
          toList (get (fromList (map f xs)))
            ≅⟨ H.cong₂ {B = Vec _} (λ n → toList ∘ get) (het-reflexive (length-map f xs)) (fromList∘map f xs) ⟩
          toList (get (mapV f (fromList xs)))
            ≡⟨ cong toList (free-theorem f (fromList xs)) ⟩
          toList (mapV f (get (fromList xs)))
            ≡⟨ toList∘map f (get (fromList xs)) ⟩
          map f (toList (get (fromList xs))) ∎

getList-to-getlen : get-type → ℕ → ℕ
getList-to-getlen get = length ∘ get ∘ flip replicate tt

replicate-length : {A : Set} → (l : List A) → map (const tt) l ≡ replicate (length l) tt
replicate-length [] = refl
replicate-length (_ ∷ l) = cong (_∷_ tt) (replicate-length l)

getList-length : (get : get-type) → {B : Set} → (l : List B) → length (get l) ≡ getList-to-getlen get (length l)
getList-length get l = begin
  length (get l)
    ≡⟨ sym (length-map (const tt) (get l)) ⟩
  length (map (const tt) (get l))
    ≡⟨ cong length (sym (free-theoremL get (const tt) l)) ⟩
  length (get (map (const tt) l))
    ≡⟨ cong (length ∘ get) (replicate-length l) ⟩
  length (get (replicate (length l) tt)) ∎
  where open ≡-Reasoning

length-toList : {A : Set} {n : ℕ} → (v : Vec A n) → length (toList v) ≡ n
length-toList []V = refl
length-toList (x ∷V xs) = cong suc (length-toList xs)

getList-to-getVec-length-property : (get : get-type) → {C : Set} → {m : ℕ} → (v : Vec C m) → length (get (toList v)) ≡ length (get (replicate m tt))
getList-to-getVec-length-property get {_} {m} v = begin
    length (get (toList v))
      ≡⟨ getList-length get (toList v) ⟩
    length (get (replicate (length (toList v)) tt))
      ≡⟨ cong (length ∘ get ∘ flip replicate tt) (length-toList v) ⟩
    length (get (replicate m tt)) ∎
    where open ≡-Reasoning

getList-to-getVec : get-type → ∃ λ (getlen : ℕ → ℕ) → (getV-type getlen)
getList-to-getVec get = getlen , get'
  where getlen : ℕ → ℕ
        getlen = getList-to-getlen get
        get' : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
        get' {C} v = subst (Vec C) (getList-to-getVec-length-property get v) (fromList (get (toList v)))

private
  module GetV-Implementation (getrecord : GetL) where

    open GetL getrecord

    getlen = length ∘ get ∘ flip replicate tt

    length-property : {C : Set} {m : ℕ} → (s : Vec C m) → length (get (toList s)) ≡ getlen m
    length-property = getList-to-getVec-length-property get

    getV : {C : Set} {m : ℕ} → Vec C m → Vec C (getlen m)
    getV s = subst (Vec _) (length-property s) (fromList (get (toList s)))

    ft : {α β : Set} (f : α → β) {n : ℕ} (v : Vec α n) → getV (mapV f v) ≡ mapV f (getV v)
    ft f v = ≅-to-≡ (begin
      subst (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v))))
        ≅⟨ ≡-subst-removable (Vec _) (length-property (mapV f v)) (fromList (get (toList (mapV f v)))) ⟩
      fromList (get (toList (mapV f v)))
        ≅⟨ het-cong (fromList ∘ get) (het-reflexive (toList∘map f v)) ⟩
      fromList (get (map f (toList v)))
        ≅⟨ het-cong fromList (het-reflexive (free-theorem f (toList v))) ⟩
      fromList (map f (get (toList v)))
        ≅⟨ fromList∘map f (get (toList v)) ⟩
      mapV f (fromList (get (toList v)))
        ≅⟨ H.cong₂ (λ n → mapV {n = n} f) (H.reflexive (length-property v)) (H.sym (≡-subst-removable (Vec _) (length-property v) (fromList (get (toList v))))) ⟩
      mapV f (subst (Vec _) (length-property v) (fromList (get (toList v)))) ∎)
      where open ≅-Reasoning

GetL-to-GetV : GetL → GetV
GetL-to-GetV getrecord = record { getlen = getlen; get = getV; free-theorem = ft }
  where open GetV-Implementation getrecord

get-commut-1-≅ : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≅ proj₂ (getList-to-getVec get) (fromList l)
get-commut-1-≅ get l = begin
  fromList (get l)
    ≅⟨ het-cong (fromList ∘ get) (≡-to-≅ (sym (toList-fromList l))) ⟩
  fromList (get (toList (fromList l)))
    ≅⟨ het-sym (≡-subst-removable (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l))))) ⟩
  subst (Vec _) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))) ∎
  where open ≅-Reasoning

get-commut-1 : (get : get-type) {A : Set} → (l : List A) → fromList (get l) ≡ subst (Vec A) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))
get-commut-1 get {A} l = ≅-to-≡ (begin
  fromList (get l)
    ≅⟨ get-commut-1-≅ get l ⟩
  proj₂ (getList-to-getVec get) (fromList l)
    ≅⟨ het-sym (≡-subst-removable (Vec _) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l))) ⟩
  subst (Vec _) (sym (getList-length get l)) (proj₂ (getList-to-getVec get) (fromList l)) ∎)
  where open ≅-Reasoning

get-trafo-1 : (get : get-type) → {B : Set} → getVec-to-getList (proj₂ (getList-to-getVec get)) {B} ≗ get {B}
get-trafo-1 get {B} l = begin
  getVec-to-getList (proj₂ (getList-to-getVec get)) l
    ≡⟨ refl ⟩
  toList (proj₂ (getList-to-getVec get) (fromList l))
    ≡⟨ refl ⟩
  toList (subst (Vec B) (getList-to-getVec-length-property get (fromList l)) (fromList (get (toList (fromList l)))))
    ≡⟨ toList-subst (fromList (get (toList (fromList l)))) (getList-to-getVec-length-property get (fromList l)) ⟩
  toList (fromList (get (toList (fromList l))))
    ≡⟨ toList-fromList (get (toList (fromList l))) ⟩
  get (toList (fromList l))
    ≡⟨ cong get (toList-fromList l) ⟩
  get l ∎
  where open ≡-Reasoning

GetLVL-identity : (G : GetL) → {A : Set} → GetL.get (GetV-to-GetL (GetL-to-GetV G)) ≗ GetL.get G {A}
GetLVL-identity G = get-trafo-1 (GetL.get G)

vec-len : {A : Set} {n : ℕ} → Vec A n → ℕ
vec-len {_} {n} _ = n

fromList-toList : {A : Set} {n : ℕ} → (v : Vec A n) → fromList (toList v) ≅ v
fromList-toList []V       = het-refl
fromList-toList (x ∷V xs) = H.cong₂ (λ n → _∷V_ {n = n} x) (het-reflexive (length-toList xs)) (fromList-toList xs)

get-commut-2 : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → (toList ∘ get {B} {n}) ≗ (getVec-to-getList get) ∘ toList
get-commut-2 get {B} v = sym (≅-to-≡ (H.cong₂ (λ n → toList ∘ get {n = n}) (H.reflexive (length-toList v)) (fromList-toList v)))

get-trafo-2-getlen : {getlen : ℕ → ℕ} → (get : getV-type getlen) → proj₁ (getList-to-getVec (getVec-to-getList get)) ≗ getlen
get-trafo-2-getlen {getlen} get n = begin
  proj₁ (getList-to-getVec (getVec-to-getList get)) n
    ≡⟨ refl ⟩
  length (toList (get (fromList (replicate n tt))))
    ≡⟨ length-toList (get (fromList (replicate n tt))) ⟩
  vec-len (get (fromList (replicate n tt)))
    ≡⟨ cong getlen (length-replicate n) ⟩
  getlen n ∎
  where open ≡-Reasoning

get-trafo-2-get-≅ : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → (v : Vec B n) → proj₂ (getList-to-getVec (getVec-to-getList get)) v ≅ get v
get-trafo-2-get-≅ {getlen} get v = begin
  subst (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v)))))
    ≅⟨ ≡-subst-removable (Vec _) (getList-to-getVec-length-property (getVec-to-getList get) v) (fromList (toList (get (fromList (toList v))))) ⟩
  fromList (toList (get (fromList (toList v))))
    ≅⟨ fromList-toList (get (fromList (toList v))) ⟩
  get (fromList (toList v))
    ≅⟨ H.cong₂ (λ n → get {n = n}) (H.reflexive (length-toList v)) (fromList-toList v) ⟩
  get v ∎
  where open ≅-Reasoning

get-trafo-2-get : {getlen : ℕ → ℕ} → (get : getV-type getlen) → {B : Set} {n : ℕ} → proj₂ (getList-to-getVec (getVec-to-getList get)) ≗ subst (Vec B) (sym (get-trafo-2-getlen get n)) ∘ get
get-trafo-2-get get v = ≅-to-≡ (begin
  proj₂ (getList-to-getVec (getVec-to-getList get)) v
    ≅⟨ get-trafo-2-get-≅ get v ⟩
  get v
    ≅⟨ het-sym (≡-subst-removable (Vec _) (sym (get-trafo-2-getlen get (vec-len v))) (get v)) ⟩
  subst (Vec _) (sym (get-trafo-2-getlen get (vec-len v))) (get v) ∎)
  where open ≅-Reasoning

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
module TestQuote where

{- test of reflection, implementing a trivial prover. -}

open import Common.Reflection
open import Common.Prelude
open import Common.Level

_==_ : Term → Term → Bool
def x [] == def y [] = primQNameEquality x y
_        == _        = false

data Thm : Set where
  triv : Thm

`Thm = def (quote Thm) []

⟦_⟧ : Term → Set
⟦ goal ⟧ with goal == `Thm
...     | true  = Thm
...     | false = ⊥

Hyp : Term → Set → Set
Hyp goal A with goal == `Thm
...        | true  = ⊤
...        | false = A

solve : (goal : Term) → Hyp goal ⟦ goal ⟧ → ⟦ goal ⟧
solve goal h  with goal == `Thm
...      | true = triv
...      | false = h

test₁ : Thm
test₁ = quoteGoal t in solve t _

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


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

module Cham.Context where

open import Cham.Name
open import Cham.Label
open import Data.Product

infix 5 _⊢_
data Context : Set where
  ∅  : Context
  _⊢_ : Context → Label → Context
  _,_ : Context → Context → Context

rename : (Name → Label) → Context → Context
rename ϕ ∅           = ∅
rename ϕ (Γ ⊢ (N ⁺)) = rename ϕ Γ ⊢ ϕ N
rename ϕ (Γ ⊢ (N ⁻)) = rename ϕ Γ ⊢ ϕ N
rename ϕ (Γ₁ , Γ₂)   = rename ϕ Γ₁ , rename ϕ Γ₂

permeate : Context → Context → Context
permeate ∅ Γ₂        = Γ₂
permeate (Γ₁ ⊢ N) Γ₂ = permeate Γ₁ (Γ₂ ⊢ N)
permeate (Γ₁ , Γ₂) Γ₃ = Γ₁ , Γ₂ , Γ₃


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

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

open import Cubical.Data.Unit

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.GroupPath
open import Cubical.Algebra.Group.Instances.Unit

open import Cubical.HITs.PropositionalTruncation as PT

-- TODO : Define exact sequences
-- (perhaps short, finite, ℕ-indexed and ℤ-indexed)

SES→isEquiv : ∀ {ℓ ℓ'} {L R : Group ℓ-zero}
  → {G : Group ℓ} {H : Group ℓ'}
  → UnitGroup₀ ≡ L
  → UnitGroup₀ ≡ R
  → (lhom : GroupHom L G) (midhom : GroupHom G H) (rhom : GroupHom H R)
  → ((x : _) → isInKer midhom x → isInIm lhom x)
  → ((x : _) → isInKer rhom x → isInIm midhom x)
  → isEquiv (fst midhom)
SES→isEquiv {R = R} {G = G} {H = H} =
  J (λ L _ → UnitGroup₀ ≡ R →
      (lhom : GroupHom L G) (midhom : GroupHom G H)
      (rhom : GroupHom H R) →
      ((x : fst G) → isInKer midhom x → isInIm lhom x) →
      ((x : fst H) → isInKer rhom x → isInIm midhom x) →
      isEquiv (fst midhom))
      ((J (λ R _ → (lhom : GroupHom UnitGroup₀ G) (midhom : GroupHom G H)
                   (rhom : GroupHom H R) →
                   ((x : fst G) → isInKer midhom x → isInIm lhom x) →
                   ((x : _) → isInKer rhom x → isInIm midhom x) →
                   isEquiv (fst midhom))
         main))
  where
  main : (lhom : GroupHom UnitGroup₀ G) (midhom : GroupHom G H)
         (rhom : GroupHom H UnitGroup₀) →
         ((x : fst G) → isInKer midhom x → isInIm lhom x) →
         ((x : fst H) → isInKer rhom x → isInIm midhom x) →
         isEquiv (fst midhom)
  main lhom midhom rhom lexact rexact =
    BijectionIsoToGroupEquiv {G = G} {H = H}
      bijIso' .fst .snd
    where
    bijIso' : BijectionIso G H
    BijectionIso.fun bijIso' = midhom
    BijectionIso.inj bijIso' x inker =
      PT.rec (GroupStr.is-set (snd G) _ _)
           (λ s → sym (snd s) ∙ IsGroupHom.pres1 (snd lhom))
           (lexact _ inker)
    BijectionIso.surj bijIso' x = rexact x refl

-- exact sequence of 4 groups. Useful for the proof of π₄S³
record Exact4 {ℓ ℓ' ℓ'' ℓ''' : Level} (G : Group ℓ)
  (H : Group ℓ') (L : Group ℓ'') (R : Group ℓ''')
  (G→H : GroupHom G H) (H→L : GroupHom H L) (L→R : GroupHom L R)
  : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ'' ℓ'''))) where
  field
    ImG→H⊂KerH→L : (x : fst H) → isInIm G→H x → isInKer H→L x
    KerH→L⊂ImG→H : (x : fst H) → isInKer H→L x → isInIm G→H x

    ImH→L⊂KerL→R : (x : fst L) → isInIm H→L x → isInKer L→R x
    KerL→R⊂ImH→L : (x : fst L) → isInKer L→R x → isInIm H→L x

open Exact4

extendExact4Surjective : {ℓ ℓ' ℓ'' ℓ''' ℓ'''' : Level}
  (G : Group ℓ) (H : Group ℓ') (L : Group ℓ'') (R : Group ℓ''') (S : Group ℓ'''')
  (G→H : GroupHom G H) (H→L : GroupHom H L) (L→R : GroupHom L R) (R→S : GroupHom R S)
  → isSurjective G→H
  → Exact4 H L R S H→L L→R R→S
  → Exact4 G L R S (compGroupHom G→H H→L) L→R R→S
ImG→H⊂KerH→L (extendExact4Surjective G H L R S G→H H→L L→R R→S surj ex) x =
  PT.rec (GroupStr.is-set (snd R) _ _)
    (uncurry λ g → J (λ x _ → isInKer L→R x)
      (ImG→H⊂KerH→L ex (fst H→L (fst G→H g))
        ∣ (fst G→H g) , refl ∣₁))
KerH→L⊂ImG→H (extendExact4Surjective G H L R S G→H H→L L→R R→S surj ex) x ker =
  PT.rec squash₁
    (uncurry λ y → J (λ x _ → isInIm (compGroupHom G→H H→L) x)
      (PT.map (uncurry
        (λ y → J (λ y _ → Σ[ g ∈ fst G ] fst H→L (fst G→H g) ≡ H→L .fst y)
        (y , refl))) (surj y)))
    (KerH→L⊂ImG→H ex x ker)
ImH→L⊂KerL→R (extendExact4Surjective G H L R S G→H H→L L→R R→S surj ex) =
  ImH→L⊂KerL→R ex
KerL→R⊂ImH→L (extendExact4Surjective G H L R S G→H H→L L→R R→S surj ex) =
  KerL→R⊂ImH→L ex

-- Useful lemma in the proof of π₄S³≅ℤ
transportExact4 : {ℓ ℓ' ℓ'' : Level}
                   {G G₂ : Group ℓ} {H H₂ : Group ℓ'} {L L₂ : Group ℓ''} {R : Group₀}
                   (G≡G₂ : G ≡ G₂) (H≡H₂ : H ≡ H₂) (L≡L₂ : L ≡ L₂)
                → UnitGroup₀ ≡ R
                → (G→H : GroupHom G H) (G₂→H₂ : GroupHom G₂ H₂)
                   (H→L : GroupHom H L) (H₂→L₂ : GroupHom H₂ L₂)
                   (L→R : GroupHom L R)
                → Exact4 G H L R G→H H→L L→R
                → PathP (λ i → GroupHom (G≡G₂ i) (H≡H₂ i)) G→H G₂→H₂
                → PathP (λ i → GroupHom (H≡H₂ i) (L≡L₂ i)) H→L H₂→L₂
                → Exact4 G₂ H₂ L₂ UnitGroup₀ G₂→H₂ H₂→L₂ (→UnitHom L₂)
transportExact4 {G = G} {G₂ = G₂} {H = H} {H₂ = H₂} {L = L} {L₂ = L₂} {R = R} =
  J4 (λ G₂ H₂ L₂ R G≡G₂ H≡H₂ L≡L₂ Unit≡R
                → (G→H : GroupHom G H) (G₂→H₂ : GroupHom G₂ H₂)
                   (H→L : GroupHom H L) (H₂→L₂ : GroupHom H₂ L₂)
                   (L→R : GroupHom L R)
                → Exact4 G H L R G→H H→L L→R
                → PathP (λ i → GroupHom (G≡G₂ i) (H≡H₂ i)) G→H G₂→H₂
                → PathP (λ i → GroupHom (H≡H₂ i) (L≡L₂ i)) H→L H₂→L₂
                → Exact4 G₂ H₂ L₂ UnitGroup₀ G₂→H₂ H₂→L₂ (→UnitHom L₂))
      (λ G→H G₂→H₂ H→L H₂→L₂ L→R ex pp1 pp2
        → J4 (λ G₂→H₂ H₂→L₂ (x : Unit) (y : Unit)
                 pp1 pp2 (_ : tt ≡ x) (_ : tt ≡ x)
             → Exact4 G H L UnitGroup₀ G₂→H₂ H₂→L₂ (→UnitHom L))
               ex G₂→H₂ H₂→L₂ tt tt pp1 pp2 refl refl )
      G₂ H₂ L₂ R
  where
  J4 : ∀ {ℓ ℓ₂ ℓ₃ ℓ₄ ℓ'} {A : Type ℓ}
       {A₂ : Type ℓ₂} {A₃ : Type ℓ₃} {A₄ : Type ℓ₄}
       {x : A} {x₂ : A₂} {x₃ : A₃} {x₄ : A₄}
       (B : (y : A) (z : A₂) (w : A₃) (u : A₄)
       → x ≡ y → x₂ ≡ z → x₃ ≡ w → x₄ ≡ u → Type ℓ')
    → B x x₂ x₃ x₄ refl refl refl refl
    → (y : A) (z : A₂) (w : A₃) (u : A₄)
       (p : x ≡ y) (q : x₂ ≡ z) (r : x₃ ≡ w) (s : x₄ ≡ u)
    → B y z w u p q r s
  J4 {x = x} {x₂ = x₂} {x₃ = x₃} {x₄ = x₄} B b y z w u =
    J (λ y p → (q : x₂ ≡ z) (r : x₃ ≡ w) (s : x₄ ≡ u) →
      B y z w u p q r s)
      (J (λ z q → (r : x₃ ≡ w) (s : x₄ ≡ u) → B x z w u refl q r s)
        (J (λ w r → (s : x₄ ≡ u) → B x x₂ w u refl refl r s)
          (J (λ u s → B x x₂ x₃ u refl refl refl s) b)))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
module _ where

open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.Nat

variable
  ℓ : Level
  A B C : Set ℓ

infixr 1 _×_ _,_
record _×_ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  constructor _,_
  field
    fst : A
    snd : B

module _ (x : A) (y : B) where
  f : C → A × B × C
  f z = x , y , z

check : (x : B) (y : C) (z : A) → f x y z ≡ (x , y , z)
check x y z = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

-- This file contains everything that can be compiled in --safe mode.

open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Division
open import Numbers.BinaryNaturals.Definition
open import Numbers.BinaryNaturals.Multiplication
open import Numbers.BinaryNaturals.Order
open import Numbers.BinaryNaturals.Subtraction
open import Numbers.Primes.PrimeNumbers
open import Numbers.Primes.IntegerFactorisation
open import Numbers.Rationals.Lemmas

open import Numbers.Modulo.Group

open import Numbers.Integers.Integers
open import Numbers.Integers.RingStructure.EuclideanDomain
open import Numbers.Integers.RingStructure.Archimedean

open import Numbers.ClassicalReals.Examples
open import Numbers.ClassicalReals.RealField.Lemmas

open import Lists.Lists
open import Lists.Filter.AllTrue

open import Groups.Groups
open import Groups.Abelian.Lemmas
open import Groups.DirectSum.Definition
open import Groups.QuotientGroup.Definition
open import Groups.QuotientGroup.Lemmas
open import Groups.FiniteGroups.Definition
open import Groups.Homomorphisms.Lemmas
open import Groups.Homomorphisms.Lemmas2
open import Groups.Homomorphisms.Examples
open import Groups.Isomorphisms.Lemmas
open import Groups.FinitePermutations
open import Groups.Lemmas
open import Groups.FirstIsomorphismTheorem
open import Groups.SymmetricGroups.Definition
open import Groups.Actions.Stabiliser
open import Groups.Actions.Orbit
open import Groups.SymmetricGroups.Lemmas
open import Groups.ActionIsSymmetry
open import Groups.Cyclic.Definition
open import Groups.Cyclic.DefinitionLemmas
open import Groups.Polynomials.Examples
open import Groups.Cosets
open import Groups.Subgroups.Normal.Examples
open import Groups.Examples.ExampleSheet1
open import Groups.LectureNotes.Lecture1

open import Fields.Fields
open import Fields.Orders.Partial.Definition
open import Fields.Orders.Total.Definition
open import Fields.Orders.Partial.Archimedean
open import Fields.Orders.LeastUpperBounds.Examples
open import Fields.Orders.Lemmas
open import Fields.FieldOfFractions.Field
open import Fields.FieldOfFractions.Lemmas
open import Fields.FieldOfFractions.Order
--open import Fields.FieldOfFractions.Archimedean

open import Rings.Definition
open import Rings.Lemmas
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Lemmas
open import Rings.Orders.Partial.Lemmas
open import Rings.IntegralDomains.Definition
open import Rings.DirectSum
open import Rings.Polynomial.Ring
open import Rings.Polynomial.Evaluation
open import Rings.Ideals.Definition
open import Rings.Isomorphisms.Definition
open import Rings.Quotients.Definition
open import Rings.Cosets
open import Rings.EuclideanDomains.Definition
open import Rings.EuclideanDomains.Examples
open import Rings.Homomorphisms.Image
open import Rings.Homomorphisms.Kernel
open import Rings.Ideals.FirstIsomorphismTheorem
open import Rings.Ideals.Lemmas
open import Rings.Ideals.Prime.Definition
open import Rings.Ideals.Prime.Lemmas
open import Rings.Ideals.Principal.Definition
open import Rings.IntegralDomains.Examples
open import Rings.PrincipalIdealDomains.Lemmas
open import Rings.Subrings.Definition
open import Rings.Ideals.Maximal.Lemmas
open import Rings.Primes.Lemmas
open import Rings.Irreducibles.Definition
open import Rings.Divisible.Lemmas
open import Rings.Associates.Lemmas
open import Rings.InitialRing
open import Rings.Homomorphisms.Lemmas
open import Rings.UniqueFactorisationDomains.Definition
open import Rings.Examples.Examples

open import Setoids.Setoids
open import Setoids.DirectSum
open import Setoids.Lists
open import Setoids.Orders.Total.Lemmas
open import Setoids.Functions.Definition
open import Setoids.Functions.Extension
open import Setoids.Algebra.Lemmas
open import Setoids.Intersection.Lemmas
open import Setoids.Union.Lemmas
open import Setoids.Cardinality.Infinite.Lemmas
open import Setoids.Cardinality.Finite.Definition

open import Sets.Cardinality.Infinite.Lemmas
open import Sets.Cardinality.Countable.Lemmas
open import Sets.Cardinality.Finite.Lemmas
open import Sets.Cardinality
open import Sets.FinSet.Lemmas

open import Decidable.Sets
open import Decidable.Reduction
open import Decidable.Relations

open import Vectors
open import Vectors.VectorSpace

open import KeyValue.KeyValue
open import KeyValue.LinearStore.Definition

open import Maybe
open import Orders.Total.Lemmas
open import Orders.WellFounded.Induction

open import ClassicalLogic.ClassicalFive

open import Monoids.Definition

open import Semirings.Definition
open import Semirings.Solver

open import Categories.Definition
open import Categories.Functor.Definition
open import Categories.Functor.Lemmas
open import Categories.Dual.Definition

open import Graphs.PathGraph
open import Graphs.CycleGraph
open import Graphs.UnionGraph
open import Graphs.CompleteGraph
open import Graphs.Colouring
open import Graphs.Bipartite
open import Graphs.Complement
open import Graphs.InducedSubgraph

open import LectureNotes.MetAndTop.Chapter1
open import LectureNotes.NumbersAndSets.Lecture1

open import Modules.Examples
open import Modules.PolynomialModule
open import Modules.Lemmas
open import Modules.DirectSum

open import Computability.LambdaCalculus.ChurchNumeral

open import ProjectEuler.Problem1

module Everything.Safe where


text:
module Issue2756 where

module M where

  postulate A : Set

module M′ = M

B : Set
B = M′.A


text:
------------------------------------------------------------------------
-- A variant of Nat.Wrapper.Cubical, defined using --erased-cubical
------------------------------------------------------------------------

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

open import Equality.Path as P
open import Prelude hiding (zero; suc; _+_)

open import Bijection equality-with-J using (_↔_)

module Nat.Wrapper.Cubical.Erased
  -- The underlying representation of natural numbers.
  (Nat′ : Type)
  -- A bijection between this representation and the unary natural
  -- numbers.
  (Nat′↔ℕ : Nat′ ↔ ℕ)
  where

open import Equality.Path.Univalence
open import Logical-equivalence using (_⇔_)

import Equivalence equality-with-J as Eq
open import Equivalence.Erased.Cubical equality-with-paths as EEq
  using (_≃ᴱ_)
import Equivalence.Erased.Contractible-preimages.Cubical
         equality-with-paths
  as ECP
open import Erased.Cubical equality-with-paths
open import Function-universe equality-with-J as F hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional.Erased equality-with-paths
  as Trunc
import Nat equality-with-J as Nat
import Univalence-axiom equality-with-J as U

open import Nat.Wrapper equality-with-J Nat′ Nat′↔ℕ as NW
open NW.[]-cong instance-of-[]-cong-axiomatisation

private
  variable
    A   : Type
    m n : A

------------------------------------------------------------------------
-- Could Nat have been defined using the propositional truncation
-- operator (with an erased higher constructor) instead of Erased?

-- Could Nat have been defined using ∥_∥ᴱ instead of Erased? Let us
-- try.

-- Given a truncated natural number we can kind of apply Nat-[_] to
-- it, because Nat-[_] is a family of contractible types. (The code
-- uses erased univalence.)

Nat-[]′ : ∥ ℕ ∥ᴱ → ∃ λ (A : Type) → Contractible A
Nat-[]′ = Trunc.rec λ where
  .truncation-is-propositionʳ →
    U.∃-H-level-H-level-1+ ext univ 0
  .∣∣ʳ n →
      Nat-[ n ]
    , propositional⇒inhabited⇒contractible
        Nat-[]-propositional
        ( _↔_.from Nat′↔ℕ n
        , [ _↔_.right-inverse-of Nat′↔ℕ n ]
        )

Nat-[_]′ : ∥ ℕ ∥ᴱ → Type
Nat-[ n ]′ = proj₁ (Nat-[]′ n)

-- Thus we can form a variant of Nat.

Nat-with-∥∥ᴱ : Type
Nat-with-∥∥ᴱ = Σ ∥ ℕ ∥ᴱ Nat-[_]′

-- However, this variant is equivalent (with erased proofs) to the
-- unit type.

Nat-with-∥∥ᴱ≃ᴱ⊤ : Nat-with-∥∥ᴱ ≃ᴱ ⊤
Nat-with-∥∥ᴱ≃ᴱ⊤ =
  _⇔_.to EEq.Contractibleᴱ⇔≃ᴱ⊤ $
  ECP.Contractibleᴱ-Σ
    (ECP.inhabited→Is-proposition→Contractibleᴱ
       ∣ 0 ∣ truncation-is-proposition)
    (ECP.Contractible→Contractibleᴱ ∘ proj₂ ∘ Nat-[]′)

-- And thus it is not isomorphic to the natural numbers.

¬-Nat-with-∥∥ᴱ↔ℕ : ¬ (Nat-with-∥∥ᴱ ↔ ℕ)
¬-Nat-with-∥∥ᴱ↔ℕ =
  Stable-¬
    [ Nat-with-∥∥ᴱ ↔ ℕ  ↝⟨ F._∘ inverse (from-equivalence (EEq.≃ᴱ→≃ Nat-with-∥∥ᴱ≃ᴱ⊤)) ⟩
      ⊤ ↔ ℕ             ↝⟨ (λ hyp → _↔_.injective (inverse hyp) refl) ⟩
      0 ≡ 1             ↝⟨ Nat.0≢+ ⟩□
      ⊥                 □
    ]

------------------------------------------------------------------------
-- Addition of "wrapped" numbers is commutative and associative

module _ (o : Operations) where

  open Operations-for-Nat o
  open Operations-for-Nat-correct o

  private

    -- A lemma used several times below.

    from[to+to]≡+ :
      ∀ m →
      _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n) ≡ m + n
    from[to+to]≡+ {n = n} m =
      _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)  ≡⟨ cong (_↔_.from Nat↔ℕ) $ sym $ to-ℕ-+ m n ⟩
      _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ (m + n))                     ≡⟨ _↔_.left-inverse-of Nat↔ℕ _ ⟩∎
      m + n                                                     ∎

  -- First two "traditional" proofs.

  -- Addition is commutative.

  +-comm-traditional : ∀ m {n} → m + n ≡ n + m
  +-comm-traditional m {n = n} =
    m + n                                                     ≡⟨ sym $ from[to+to]≡+ m ⟩
    _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)  ≡⟨ cong (_↔_.from Nat↔ℕ) $ Nat.+-comm (_↔_.to Nat↔ℕ m) ⟩
    _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ n Prelude.+ _↔_.to Nat↔ℕ m)  ≡⟨ from[to+to]≡+ n ⟩∎
    n + m                                                     ∎

  -- Addition is associative.

  +-assoc-traditional : ∀ m {n o} → m + (n + o) ≡ (m + n) + o
  +-assoc-traditional m {n = n} {o = o} =
    m + (n + o)                                                     ≡⟨ cong (m +_) $ sym $ from[to+to]≡+ n ⟩

    m + (_↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ n Prelude.+ _↔_.to Nat↔ℕ o))  ≡⟨ sym $ from[to+to]≡+ m ⟩

    _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m
                      Prelude.+
                    _↔_.to Nat↔ℕ (_↔_.from Nat↔ℕ
                      (_↔_.to Nat↔ℕ n Prelude.+ _↔_.to Nat↔ℕ o)))   ≡⟨ cong (λ n → _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ n)) $
                                                                       _↔_.right-inverse-of Nat↔ℕ _ ⟩
    _↔_.from Nat↔ℕ
      (_↔_.to Nat↔ℕ m
         Prelude.+
       (_↔_.to Nat↔ℕ n Prelude.+ _↔_.to Nat↔ℕ o))                   ≡⟨ cong (_↔_.from Nat↔ℕ) $ Nat.+-assoc (_↔_.to Nat↔ℕ m) ⟩

    _↔_.from Nat↔ℕ
      ((_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)
         Prelude.+
       _↔_.to Nat↔ℕ o)                                              ≡⟨ cong (λ n → _↔_.from Nat↔ℕ (n Prelude.+ _↔_.to Nat↔ℕ o)) $ sym $
                                                                       _↔_.right-inverse-of Nat↔ℕ _ ⟩
    _↔_.from Nat↔ℕ
      (_↔_.to Nat↔ℕ (_↔_.from Nat↔ℕ
         (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n))
         Prelude.+
       _↔_.to Nat↔ℕ o)                                              ≡⟨ from[to+to]≡+ (_↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)) ⟩

    (_↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n)) + o  ≡⟨ cong (_+ o) $ from[to+to]≡+ {n = n} m ⟩∎

    (m + n) + o                                                     ∎

  -- The following proofs are instead based on a technique used by
  -- Vezzosi, Mörtberg and Abel in "Cubical Agda: A Dependently Typed
  -- Programming Language with Univalence and Higher Inductive Types".

  -- The type of unary natural numbers is equal to the type of wrapped
  -- natural numbers (in erased contexts).

  @0 ℕ≡Nat : ℕ ≡ Nat
  ℕ≡Nat = sym (≃⇒≡ (Eq.↔⇒≃ Nat↔ℕ))

  -- Addition of unary natural numbers is, in a certain sense, equal
  -- to addition of wrapped natural numbers (in erased contexts).

  @0 +≡+ : P.[ (λ i → ℕ≡Nat i → ℕ≡Nat i → ℕ≡Nat i) ] Prelude._+_ ≡ _+_
  +≡+ =
    Prelude._+_                                                         ≡⟨ (λ i → transport
                                                                                (λ j → ℕ≡Nat (min i j) → ℕ≡Nat (min i j) → ℕ≡Nat (min i j))
                                                                                (- i) Prelude._+_) ⟩h
    transport (λ i → ℕ≡Nat i → ℕ≡Nat i → ℕ≡Nat i) 0̲ Prelude._+_         ≡⟨⟩
    (λ m n → _↔_.from Nat↔ℕ (_↔_.to Nat↔ℕ m Prelude.+ _↔_.to Nat↔ℕ n))  ≡⟨ (⟨ext⟩ λ m → ⟨ext⟩ λ _ → from[to+to]≡+ m) ⟩∎
    _+_                                                                 ∎

  -- Addition is commutative (in erased contexts).

  @0 +-comm-cubical : ∀ m {n} → m + n ≡ n + m
  +-comm-cubical =
    transport
      (λ i → (m {n} : ℕ≡Nat i) → +≡+ i m n ≡ +≡+ i n m)
      0̲
      Nat.+-comm

  -- Addition is associative (in erased contexts).

  @0 +-assoc-cubical : ∀ m {n o} → m + (n + o) ≡ (m + n) + o
  +-assoc-cubical =
    transport
      (λ i → (m {n o} : ℕ≡Nat i) →
             +≡+ i m (+≡+ i n o) ≡ +≡+ i (+≡+ i m n) o)
      0̲
      Nat.+-assoc

  -- This proof technique seems to scale better than the one used
  -- above, at least for examples of the kind used here. However, when
  -- --erased-cubical is used it only works in erased contexts.

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module reverse-++-distrib where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open Eq.≡-Reasoning
open import lists using (List; []; _∷_; [_]; _++_; ++-assoc; ++-identityʳ; reverse)

-- 結合したリストの逆順は、逆順にしたリストの逆順の結合と等しいことの証明
reverse-++-distrib : ∀ {A : Set} → (xs ys : List A)
  → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++-distrib [] ys =
  begin
    reverse ([] ++ ys)
  ≡⟨⟩
    reverse ys
  ≡⟨ sym (++-identityʳ (reverse ys)) ⟩
    reverse ys ++ []
  ≡⟨⟩
    reverse ys ++ reverse []
  ∎
reverse-++-distrib (x ∷ xs) ys =
  begin
    reverse (x ∷ xs ++ ys)
  ≡⟨⟩
    reverse (xs ++ ys) ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩
    (reverse ys ++ reverse xs) ++ [ x ]
  ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩
    reverse ys ++ (reverse xs ++ [ x ])
  ≡⟨⟩
    reverse ys ++ reverse (x ∷ xs)
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.ProofIrrelevance {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties using (wkSingleSubstId)
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution

open import Tools.Product
open import Tools.Unit
open import Tools.Empty
open import Tools.Nat

import Tools.PropositionalEquality as PE
import Data.Nat as Nat

~-quasirefl : ∀ {Γ n n′ A r} → Γ ⊢ n ~ n′ ∷ A ^ r → Γ ⊢ n ~ n ∷ A ^ r
~-quasirefl p = ~-trans p (~-sym p)

≅-quasirefl : ∀ {Γ n n′ A r} → Γ ⊢ n ≅ n′ ∷ A ^ r → Γ ⊢ n ≅ n ∷ A ^ r
≅-quasirefl p = ≅ₜ-trans p (≅ₜ-sym p)

proof-irrelevanceRel : ∀ {Γ A t u l l′} ([A] : Γ ⊩⟨ l ⟩ A ^ [ % , l′ ])
                   → Γ ⊩⟨ l ⟩ t ∷ A ^ [ % , l′ ] / [A]
                   → Γ ⊩⟨ l ⟩ u ∷ A ^ [ % , l′ ] / [A]
                   → Γ ⊩⟨ l ⟩ t ≡ u ∷ A ^ [ % , l′ ] / [A]
proof-irrelevanceRel (Emptyᵣ x)
                   (Emptyₜ (ne ⊢t))
                   (Emptyₜ (ne ⊢t₁)) = Emptyₜ₌ (ne ⊢t ⊢t₁)

proof-irrelevanceRel (ne x)
                   (neₜ ⊢t)
                   (neₜ ⊢t₁) =
                   neₜ₌ ⊢t  ⊢t₁
proof-irrelevanceRel {Γ} {l = l} (Πᵣ′ rF lF lG _ _ F G D ⊢F ⊢G A≡A [F] [G] G-ext) [f] [f₁] =
  [f] , [f₁]
proof-irrelevanceRel {Γ} {l = l} (∃ᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) [f] [f₁] =
  [f] , [f₁]

proof-irrelevanceRel (emb emb< [A]) [t] [u] = proof-irrelevanceRel [A] [t] [u]
proof-irrelevanceRel (emb ∞< [A]) [t] [u] = proof-irrelevanceRel [A] [t] [u]

proof-irrelevanceᵛ : ∀ {Γ A t u l l′} ([Γ] : ⊩ᵛ Γ) ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ [ % , l′ ] / [Γ])
                   → Γ ⊩ᵛ⟨ l ⟩ t ∷ A ^ [ % , l′ ] / [Γ] / [A]
                   → Γ ⊩ᵛ⟨ l ⟩ u ∷ A ^ [ % , l′ ] / [Γ] / [A]
                   → Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A ^ [ % , l′ ] / [Γ] / [A]
proof-irrelevanceᵛ [Γ] [A] [t] [u] {σ = σ} ⊢Δ [σ] =
  proof-irrelevanceRel (proj₁ ([A] ⊢Δ [σ])) (proj₁ ([t] ⊢Δ [σ])) (proj₁ ([u] ⊢Δ [σ]))

validityIrr : ∀ {l A t Γ l'} ([Γ] : ⊩ᵛ Γ) ([A] : Γ ⊩ᵛ⟨ l ⟩ A ^ [ % , l' ] / [Γ])
                (⊢t : ∀ {Δ σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ) → Δ ⊢ subst σ t ∷ subst σ A ^ [ % , l' ]) → Γ ⊩ᵛ⟨ l ⟩ t ∷ A ^ [ % , l' ] / [Γ] / [A]
validityIrr [Γ] [A] ⊢t {Δ} {σ} ⊢Δ [σ] =
  let [Aσ] = proj₁ ([A] ⊢Δ [σ])
      [tσ] = logRelIrr [Aσ] (⊢t ⊢Δ [σ])
      -- [tσ] = proj₁ ([t] ⊢Δ [σ])
  in  logRelIrr [Aσ] (⊢t ⊢Δ [σ]) ,
      λ [σ′] [σ≡σ′] → let [Aσ′] = proj₁ ([A] ⊢Δ [σ′])
                          [tσ′] = logRelIrr [Aσ′] (⊢t ⊢Δ [σ′])
                          [Aσ≡σ′] = proj₂ ([A] ⊢Δ [σ]) [σ′] [σ≡σ′]
                      in logRelIrrEq [Aσ] (⊢t ⊢Δ [σ]) (escapeTerm [Aσ] (convTerm₂ [Aσ] [Aσ′] [Aσ≡σ′] [tσ′]))

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

module Tools.List where

infixr 30 _∷_

data List (A : Set) : Set where
  [] : List A
  _∷_ : A → List A → List A

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
-- Andreas, 2014-07-02 wondering about the ETA pragma (legacy?)

open import Common.Equality

data Prod (A B : Set) : Set where
  pair : A → B → Prod A B

{-# ETA Prod #-}

-- The ETA pragma does not exist anymore.

fst : {A B : Set} → Prod A B → A
fst (pair a b) = a

snd : {A B : Set} → Prod A B → B
snd (pair a b) = b

-- Just an illusion...
test : {A B : Set} (x : Prod A B) → x ≡ pair (fst x) (snd x)
test x = refl


text:
{-# POLARITY F #-}
{-# POLARITY G #-}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
----------------------------------------------------------------------
-- Copyright: 2013, Jan Stolarek, Lodz University of Technology     --
--                                                                  --
-- License: See LICENSE file in root of the repo                    --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps   --
--                                                                  --
-- Definition of datatypes that represent ordering and functions    --
-- that operate on them. These datatypes are based on ideas         --
-- introduced in "Why Dependent Types Matter".                      --
----------------------------------------------------------------------

module Basics.Ordering where

open import Basics.Nat hiding (_≥_)

-- The ≥ type is a proof of greater-equal relation between two natural
-- numbers. It proves that: a) any number natural is greater or equal
-- to zero and b) any two natural numbers are in ≥ relation if their
-- predecessors are also in that relation.
data _≥_ : Nat → Nat → Set where
  ge0 : {  y : Nat}         → y     ≥ zero
  geS : {x y : Nat} → x ≥ y → suc x ≥ suc y

infixl 4 _≥_

-- Order datatype tells whether two numbers are in ≥ relation or
-- not. In that sense it is an equivalent of Bool datatype. Unlike
-- Bool however, Order supplies a proof of WHY the numbers are (or are
-- not) in the ≥ relation.
data Order : Nat → Nat → Set where
  ge : {x : Nat} {y : Nat} → x ≥ y → Order x y
  le : {x : Nat} {y : Nat} → y ≥ x → Order x y

-- order function takes two natural numbers and compares them,
-- returning the result of comparison together with a proof of the
-- result (result and its proof are encoded by Order datatype).
order : (a : Nat) → (b : Nat) → Order a b
order a       zero    = ge ge0
order zero    (suc b) = le ge0
order (suc a) (suc b) with order a b
order (suc a) (suc b) | ge a≥b = ge (geS a≥b)
order (suc a) (suc b) | le b≥a = le (geS b≥a)

max_stars_repo_name: jstolarek/dep-typed-wbl-heaps

max_issues_repo_name: jstolarek/dep-typed-wbl-heaps

max_forks_repo_name: jstolarek/dep-typed-wbl-heaps


text:
module Numeral.Natural.Oper.Comparisons where

import      Lvl
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Numeral.Natural
open import Numeral.Sign

ℕbool : Bool → ℕ
ℕbool = if_then 1 else 0

-- Compare
_⋚?_ : ℕ → ℕ → (−|0|+)
𝟎    ⋚? 𝟎    = 𝟎
𝟎    ⋚? 𝐒(b) = ➖
𝐒(a) ⋚? 𝟎    = ➕
𝐒(a) ⋚? 𝐒(b) = a ⋚? b

-- Equality check
_≡?_ : ℕ → ℕ → Bool
a ≡? b = elim₃ 𝐹 𝑇 𝐹 (a ⋚? b)
{-# BUILTIN NATEQUALS _≡?_ #-}

-- Non-equality check
_≢?_ : ℕ → ℕ → Bool
x ≢? y = !(x ≡? y)

-- Positivity check
positive? : ℕ → Bool
positive? (𝟎)    = 𝐹
positive? (𝐒(_)) = 𝑇

-- Zero check
zero? : ℕ → Bool
zero? n = !(positive? n)

-- Lesser-than check
_<?_ : ℕ → ℕ → Bool
_    <? 𝟎    = 𝐹
𝟎    <? 𝐒(_) = 𝑇
𝐒(x) <? 𝐒(y) = (x <? y)
{-# BUILTIN NATLESS _<?_ #-}

-- Lesser-than or equals check
_≤?_ : ℕ → ℕ → Bool
x ≤? y = x <? 𝐒(y)

-- Greater-than check
_>?_ : ℕ → ℕ → Bool
x >? y = y <? x

-- Greater-than or equals check
_≥?_ : ℕ → ℕ → Bool
x ≥? y = y ≤? x

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by preorders
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Properties.Preorder
         {p₁ p₂ p₃} (P : Preorder p₁ p₂ p₃) where

open import Function
open import Data.Product as Prod

open Relation.Binary.Preorder P

-- The inverse relation is also a preorder.

invIsPreorder : IsPreorder _≈_ (flip _∼_)
invIsPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = reflexive ∘ Eq.sym
  ; trans         = flip trans
  }

invPreorder : Preorder p₁ p₂ p₃
invPreorder = record { isPreorder = invIsPreorder }

------------------------------------------------------------------------
-- For every preorder there is an induced equivalence

InducedEquivalence : Setoid _ _
InducedEquivalence = record
  { _≈_           = λ x y → x ∼ y × y ∼ x
  ; isEquivalence = record
    { refl  = (refl , refl)
    ; sym   = swap
    ; trans = Prod.zip trans (flip trans)
    }
  }


text:
module Data.List.Functions.Multi where

import      Lvl
open import Data
open import Data.List
open import Data.List.Functions hiding (separate)
open import Data.Option
open import Data.Tuple
open import Data.Tuple.Raise
import      Data.Tuple.Raiseᵣ.Functions as Raise
open import Numeral.Finite
open import Numeral.Natural
open import Numeral.Natural.Oper.Modulo
open import Type

private variable ℓ : Lvl.Level
private variable T : Type{ℓ}

-- TODO: Also called zip in other languages
-- module _ where
--   open import Data.Tuple.Raise as Tuple using (_^_)
--   open import Function.Multi as Multi using (_⇉_)

  --map₊ : ∀{n}{As : Type{ℓ} ^ n}{B} → (As ⇉ B) → (Tuple.map List(As) ⇉ List(B))
  -- map₊ {n = 𝟎}                 = const ∅
  -- map₊ {n = 𝐒(𝟎)}              = map
  -- map₊ {n = 𝐒(𝐒(n))} _ ∅       = Multi.const ∅
  -- map₊ {n = 𝐒(𝐒(n))} f (x ⊰ l) = {!!}

{-
separate : (n : ℕ) → List(T) → (List(T) ^ n)
separate(0)       _ = <>
separate(1)       l = l
separate(𝐒(𝐒(n))) l = {!!}
-- Raise.repeat (𝐒(𝐒(n))) ∅
-- (x ⊰ l) = Raise.map₂ {!skip!} {!!} (∅ , separate(𝐒(n)) l)
-}

-- Separates a list by a function assigning which list index it should lie in.
-- Example:
--   separateBy(_mod 3) [0,1,2,3,4,5,6,7,8,9] = [[0,3,6,9] , [1,4,7] , [2,5,8]]
separateBy : ∀{n} → (T → 𝕟(n)) → List(T) → (List(T) ^ n)
separateBy f ∅       = Raise.repeat _ ∅
separateBy f (x ⊰ l) = Raise.updateAt (f(x)) (x ⊰_) (separateBy f l)