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

module Cubical.Data.Fin.Recursive.Properties where

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

open import Cubical.Functions.Embedding

import Cubical.Data.Empty as Empty
open Empty hiding (rec; elim)
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.Nat.Order.Recursive
open import Cubical.Data.Sigma
import Cubical.Data.Sum as Sum
open Sum using (_⊎_; _⊎?_; inl; inr)

open import Cubical.Data.Fin.Recursive.Base

open import Cubical.Relation.Nullary

private
  variable
    ℓ : Level
    m n : ℕ
    A : Type ℓ
    x y : A

isPropFin0 : isProp (Fin 0)
isPropFin0 = isProp⊥

isContrFin1 : isContr (Fin 1)
isContrFin1 .fst = zero
isContrFin1 .snd zero = refl

Unit≡Fin1 : Unit ≡ Fin 1
Unit≡Fin1 = ua (const zero , ctr)
  where
  fibr : fiber (const zero) zero
  fibr = tt , refl

  fibr! : ∀ f → fibr ≡ f
  fibr! (tt , p) i .fst = tt
  fibr! (tt , p) i .snd = J (λ{ zero q → refl ≡ q }) refl p i

  ctr : isEquiv (const zero)
  ctr .equiv-proof zero .fst = fibr
  ctr .equiv-proof zero .snd = fibr!

module Cover where
  Cover : FinF A → FinF A → Type _
  Cover zero zero = Unit
  Cover (suc x) (suc y) = x ≡ y
  Cover _ _ = ⊥

  crefl : Cover x x
  crefl {x = zero} = _
  crefl {x = suc x} = refl

  cover : x ≡ y → Cover x y
  cover p = transport (λ i → Cover (p i0) (p i)) crefl

  predp : Path (FinF A) (suc x) (suc y) → x ≡ y
  predp {x = x} p = transport (λ i → Cover (suc x) (p i)) refl

  suc-predp-refl
    : Path (Path (FinF A) (suc x) (suc x))
        (λ i → suc (predp (λ _ → suc x) i)) refl
  suc-predp-refl {x = x} i j
    = suc (transportRefl (refl {x = x}) i j)

  suc-retract : (p : Path (FinF A) (suc x) (suc y)) → (λ i → suc (predp p i)) ≡ p
  suc-retract
    = J (λ{ (suc m) q → (λ i → suc (predp q i)) ≡ q ; zero _ → ⊥}) suc-predp-refl

  isEmbedding-suc : isEmbedding {B = FinF A} suc
  isEmbedding-suc w x = isoToIsEquiv theIso
    where
    open Iso
    theIso : Iso (w ≡ x) (suc w ≡ suc x)
    theIso .fun = cong suc
    theIso .inv p = predp p
    theIso .rightInv = suc-retract
    theIso .leftInv
      = J (λ _ q → transport (λ i → w ≡ q i) refl ≡ q) (transportRefl refl)

private
  zK : (p : Path (FinF A) zero zero) → p ≡ refl
  zK = J (λ{ zero q → q ≡ refl ; one _ → ⊥ }) refl

  isSetFinF : isSet A → isSet (FinF A)
  isSetFinF Aset zero zero p
    = J (λ{ zero q → p ≡ q ; _ _ → ⊥ }) (zK p)
  isSetFinF Aset (suc x) (suc y)
    = isOfHLevelRetract 1 Cover.predp (cong suc) Cover.suc-retract (Aset x y)
  isSetFinF Aset zero (suc _) p = Empty.rec (Cover.cover p)
  isSetFinF Aset (suc _) zero p = Empty.rec (Cover.cover p)

isSetFin : isSet (Fin m)
isSetFin {zero} = isProp→isSet isPropFin0
isSetFin {suc m} = isSetFinF isSetFin

discreteFin : Discrete (Fin m)
discreteFin {suc m} zero zero = yes refl
discreteFin {suc m} (suc i) (suc j) with discreteFin i j
... | yes p = yes (cong suc p)
... | no ¬p = no (¬p ∘ Cover.predp)
discreteFin {suc m} zero (suc _) = no Cover.cover
discreteFin {suc m} (suc _) zero = no Cover.cover

inject< : m < n → Fin m → Fin n
inject< {suc m} {suc n} _ zero = zero
inject< {suc m} {suc n} m<n (suc i) = suc (inject< m<n i)

inject≤ : m ≤ n → Fin m → Fin n
inject≤ {suc m} {suc n} _ zero = zero
inject≤ {suc m} {suc n} m≤n (suc i) = suc (inject≤ m≤n i)

any? : {P : Fin m → Type ℓ} → (∀ i → Dec (P i)) → Dec (Σ _ P)
any? {zero} P? = no fst
any? {suc m} P? with P? zero ⊎? any? (P? ∘ suc)
... | yes (inl p) = yes (zero , p)
... | yes (inr (i , p)) = yes (suc i , p)
... | no k = no λ where
  (zero , p) → k (inl p)
  (suc x , p) → k (inr (x , p))

_#_ : Fin m → Fin m → Type₀
_#_ {m = suc m} zero zero = ⊥
_#_ {m = suc m} (suc i) zero = Unit
_#_ {m = suc m} zero (suc j) = Unit
_#_ {m = suc m} (suc i) (suc j) = i # j

#→≢ : ∀{i j : Fin m} → i # j → ¬ i ≡ j
#→≢ {suc _} {zero} {suc j} _ = Cover.cover
#→≢ {suc _} {suc i} {zero} _ = Cover.cover
#→≢ {suc m} {suc i} {suc j} ap p = #→≢ ap (Cover.predp p)

≢→# : ∀{i j : Fin m} → ¬ i ≡ j → i # j
≢→# {suc m} {zero}  {zero}  ¬p = ¬p refl
≢→# {suc m} {zero}  {suc j}  _ = _
≢→# {suc m} {suc i} {zero}   _ = _
≢→# {suc m} {suc i} {suc j} ¬p = ≢→# {m} {i} {j} (¬p ∘ cong suc)

#-inject< : ∀{l : m < n} (i j : Fin m) → i # j → inject< {m} {n} l i # inject< l j
#-inject< {suc m} {suc n} zero    (suc _) _ = _
#-inject< {suc m} {suc n} (suc _) zero    _ = _
#-inject< {suc m} {suc n} (suc i) (suc j) a = #-inject< {m} {n} i j a

punchOut : (i j : Fin (suc m)) → i # j → Fin m
punchOut {suc m} zero (suc j) _ = j
punchOut {suc m} (suc i) zero _ = zero
punchOut {suc m} (suc i) (suc j) ap = suc (punchOut i j ap)

punchOut-inj
  : ∀{i j k : Fin (suc m)}
  → (i#j : i # j) (i#k : i # k)
  → punchOut i j i#j ≡ punchOut i k i#k
  → j ≡ k
punchOut-inj {suc m} {suc i} {zero} {zero} i#j i#k p = refl
punchOut-inj {suc m} {zero} {suc j} {suc k} i#j i#k p = cong suc p
punchOut-inj {suc m} {suc i} {suc j} {suc k} i#j i#k p
  = cong suc (punchOut-inj {m} {i} {j} {k} i#j i#k (Cover.predp p))
punchOut-inj {suc m} {suc i} {zero} {suc x} i#j i#k p
  = Empty.rec (Cover.cover p)
punchOut-inj {suc m} {suc i} {suc j} {zero} i#j i#k p
  = Empty.rec (Cover.cover p)

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

toFin : (n : ℕ) → Fin (suc n)
toFin zero = zero
toFin (suc n) = suc (toFin n)

inject<#toFin : ∀(i : Fin n) → inject< (≤-refl (suc n)) i # toFin n
inject<#toFin {suc n} zero = _
inject<#toFin {suc n} (suc i) = inject<#toFin {n} i

inject≤#⊕ : ∀(i : Fin m) (j : Fin n) → inject≤ (k≤k+n m) i # (m ⊕ j)
inject≤#⊕ {suc m} {suc n} zero    j = _
inject≤#⊕ {suc m} {suc n} (suc i) j = inject≤#⊕ i j

split : (m : ℕ) → Fin (m + n) → Fin m ⊎ Fin n
split zero    j = inr j
split (suc m) zero = inl zero
split (suc m) (suc i) with split m i
... | inl k = inl (suc k)
... | inr j = inr j

pigeonhole
  : m < n
  → (f : Fin n → Fin m)
  → Σ[ i ∈ Fin n ] Σ[ j ∈ Fin n ] (i # j) × (f i ≡ f j)
pigeonhole {zero} {suc n} m<n f = Empty.rec (f zero)
pigeonhole {suc m} {suc n} m<n f with any? (λ i → discreteFin (f zero) (f (suc i)))
... | yes (j , p) = zero , suc j , _ , p
... | no ¬p = let i , j , ap , p = pigeonhole {m} {n} m<n g
               in suc i , suc j , ap
                , punchOut-inj {i = f zero} (apart i) (apart j) p
  where
  apart : (i : Fin n) → f zero # f (suc i)
  apart i = ≢→# {suc m} {f zero} (¬p ∘ _,_ i)

  g : Fin n → Fin m
  g i = punchOut (f zero) (f (suc i)) (apart i)

Fin-inj₀ : m < n → ¬ Fin n ≡ Fin m
Fin-inj₀ m<n P with pigeonhole m<n (transport P)
... | i , j , i#j , p = #→≢ i#j i≡j
  where
  i≡j : i ≡ j
  i≡j = transport (λ k → transport⁻Transport P i k ≡ transport⁻Transport P j k)
          (cong (transport⁻ P) p)

Fin-inj : (m n : ℕ) → Fin m ≡ Fin n → m ≡ n
Fin-inj m n P with m ≟ n
... | eq p   = p
... | lt m<n = Empty.rec (Fin-inj₀ m<n (sym P))
... | gt n<m = Empty.rec (Fin-inj₀ n<m P)

module Isos where
  open Iso

  up : Fin m → Fin (m + n)
  up {m} = inject≤ (k≤k+n m)

  resplit-identᵣ₀ : ∀ m (i : Fin n) → Sum.⊎Path.Cover (split m (m ⊕ i)) (inr i)
  resplit-identᵣ₀ zero    i = lift refl
  resplit-identᵣ₀ (suc m) i with split m (m ⊕ i) | resplit-identᵣ₀ m i
  ... | inr j | p = p

  resplit-identᵣ : ∀ m (i : Fin n) → split m (m ⊕ i) ≡ inr i
  resplit-identᵣ m i = Sum.⊎Path.decode _ _ (resplit-identᵣ₀ m i)

  resplit-identₗ₀ : ∀ m (i : Fin m) → Sum.⊎Path.Cover (split {n} m (up i)) (inl i)
  resplit-identₗ₀ (suc m) zero = lift refl
  resplit-identₗ₀ {n} (suc m) (suc i)
    with split {n} m (up i) | resplit-identₗ₀ {n} m i
  ... | inl j | lift p = lift (cong suc p)

  resplit-identₗ : ∀ m (i : Fin m) → split {n} m (up i) ≡ inl i
  resplit-identₗ m i = Sum.⊎Path.decode _ _ (resplit-identₗ₀ m i)

  desplit-ident : ∀ m → (i : Fin (m + n)) → Sum.rec up (m ⊕_) (split m i) ≡ i
  desplit-ident zero i = refl
  desplit-ident (suc m) zero = refl
  desplit-ident (suc m) (suc i) with split m i | desplit-ident m i
  ... | inl j | p = cong suc p
  ... | inr j | p = cong suc p

  sumIso : Iso (Fin m ⊎ Fin n) (Fin (m + n))
  sumIso {m} .fun = Sum.rec up (m ⊕_)
  sumIso {m} .inv i = split m i
  sumIso {m} .rightInv i = desplit-ident m i
  sumIso {m} .leftInv (inr j) = resplit-identᵣ m j
  sumIso {m} .leftInv (inl i) = resplit-identₗ m i

sum≡ : Fin m ⊎ Fin n ≡ Fin (m + n)
sum≡ = isoToPath Isos.sumIso

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


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-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₂))
            =∎

    module CodesRec = EM₁Level₁Rec {G = G} {C = 0 -Type i} (G.El , G.El-level) Codes-hom

    Codes : EM₁ G → 0 -Type i
    Codes = CodesRec.f

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

    abstract
      transp-Codes-β : ∀ g g' → transport (fst ∘ Codes) (emloop g) g' == G.comp g' g
      transp-Codes-β g g' =
        coe (ap (fst ∘ Codes) (emloop g)) g'
          =⟨ ap (λ v → coe v g') (ap-∘ fst Codes (emloop g)) ⟩
        coe (ap fst (ap Codes (emloop g))) g'
          =⟨ ap (λ v → coe (ap fst v) g') (CodesRec.emloop-β g) ⟩
        coe (ap fst (nType=-out (ua (comp-equiv g)))) g'
          =⟨ ap (λ v → coe v g') (fst=-β (ua (comp-equiv g)) _) ⟩
        coe (ua (comp-equiv g)) g'
          =⟨ coe-β (comp-equiv g) g' ⟩
        –> (comp-equiv g) g' =∎

      encode-emloop : ∀ g → encode (emloop g) == g
      encode-emloop g =
        transport (fst ∘ Codes) (emloop g) G.ident
          =⟨ transp-Codes-β g G.ident ⟩
        G.comp G.ident g
          =⟨ G.unit-l g ⟩
        g =∎

    module Decode where

      private
        {- transport in path fibration of EM₁ -}
        transp-PF : embase' G == embase → embase' G == embase → embase' G == embase
        transp-PF = transport (embase' G ==_)

        {- transport in Codes -}
        transp-C : embase' G == embase → G.El → G.El
        transp-C = transport (fst ∘ Codes)

        transp-emloop : embase' G == embase → G.El → embase' G == embase
        transp-emloop p = transp-PF p ∘ emloop

        emloop-transp : embase' G == embase → G.El → embase' G == embase
        emloop-transp p = emloop ∘ transp-C p

        swap-transp-emloop-seq : ∀ g h → transp-emloop (emloop g) h =-= emloop-transp (emloop g) h
        swap-transp-emloop-seq g h =
          transp-emloop (emloop g) h
            =⟪ transp-cst=idf (emloop g) (emloop h) ⟫
          emloop h ∙ emloop g
            =⟪ ! (emloop-comp h g) ⟫
          emloop (G.comp h g)
            =⟪ ap emloop (! (transp-Codes-β g h)) ⟫
          emloop-transp (emloop g) h ∎∎

        swap-transp-emloop : ∀ g h → transp-emloop (emloop g) h == emloop-transp (emloop g) h
        swap-transp-emloop g h = ↯ (swap-transp-emloop-seq g h)

      private

        decode-emloop-comp : ∀ g₁ g₂ h →
          swap-transp-emloop (G.comp g₁ g₂) h ◃∙
          ap (λ p → emloop (transp-C p h)) (emloop-comp g₁ g₂) ◃∙
          ap emloop (transp-∙ (emloop g₁) (emloop g₂) h) ◃∎
          =ₛ
          ap (λ p → transp-PF p (emloop h)) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (swap-transp-emloop g₁ h) ◃∙
          swap-transp-emloop g₂ (transp-C (emloop g₁) h) ◃∎
        decode-emloop-comp g₁ g₂ h =
          swap-transp-emloop g₁g₂ h ◃∙
          ap (λ p → emloop-transp p h) (emloop-comp g₁ g₂) ◃∙
          ap emloop (transp-∙ (emloop g₁) (emloop g₂) h) ◃∎
            =ₛ₁⟨ 1 & 1 & ap-∘ emloop (λ p → transp-C p h) (emloop-comp g₁ g₂) ⟩
          swap-transp-emloop g₁g₂ h ◃∙
          ap emloop (ap (λ p → transp-C p h) (emloop-comp g₁ g₂)) ◃∙
          ap emloop (transp-∙ (emloop g₁) (emloop g₂) h) ◃∎
            =ₛ⟨ 0 & 1 & expand (swap-transp-emloop-seq g₁g₂ h) ⟩
          transp-cst=idf (emloop g₁g₂) (emloop h) ◃∙
          ! (emloop-comp h g₁g₂) ◃∙
          ap emloop (! (transp-Codes-β g₁g₂ h)) ◃∙
          ap emloop (ap (λ p → transp-C p h) (emloop-comp g₁ g₂)) ◃∙
          ap emloop (transp-∙ (emloop g₁) (emloop g₂) h) ◃∎
            =ₛ⟨ 2 & 3 &
                ap-seq-=ₛ emloop $
                =ₛ-in {s = ! (transp-Codes-β g₁g₂ h) ◃∙
                           ap (λ p → transp-C p h) (emloop-comp g₁ g₂) ◃∙
                           transp-∙ (emloop g₁) (emloop g₂) h ◃∎}
                      {t = ! (G.assoc h g₁ g₂) ◃∙
                           ap (λ k → G.comp k g₂) (! (transp-Codes-β g₁ h)) ◃∙
                           ! (transp-Codes-β g₂ (transp-C (emloop g₁) h)) ◃∎} $
                prop-path (has-level-apply G.El-level _ _) _ _
              ⟩
          transp-cst=idf (emloop g₁g₂) (emloop h) ◃∙
          ! (emloop-comp h g₁g₂) ◃∙
          ap emloop (! (G.assoc h g₁ g₂)) ◃∙
          ap emloop (ap (λ k → G.comp k g₂) (! (transp-Codes-β g₁ h))) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ⟨ 0 & 1 &
                post-rotate-in {p = _ ◃∎} $ !ₛ $
                homotopy-naturality (λ p → transp-PF p (emloop h))
                                    (emloop h ∙_)
                                    (λ p → transp-cst=idf p (emloop h))
                                    (emloop-comp g₁ g₂)
              ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-cst=idf (emloop g₁ ∙ emloop g₂) (emloop h) ◃∙
          ! (ap (emloop h ∙_) (emloop-comp g₁ g₂)) ◃∙
          ! (emloop-comp h g₁g₂) ◃∙
          ap emloop (! (G.assoc h g₁ g₂)) ◃∙
          ap emloop (ap (λ k → G.comp k g₂) (! (transp-Codes-β g₁ h))) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ₁⟨ 4 & 1 & ap-! emloop (G.assoc h g₁ g₂) ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-cst=idf (emloop g₁ ∙ emloop g₂) (emloop h) ◃∙
          ! (ap (emloop h ∙_) (emloop-comp g₁ g₂)) ◃∙
          ! (emloop-comp h g₁g₂) ◃∙
          ! (ap emloop (G.assoc h g₁ g₂)) ◃∙
          ap emloop (ap (λ k → G.comp k g₂) (! (transp-Codes-β g₁ h))) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ⟨ 2 & 3 & !ₛ (!-=ₛ (emloop-coh' G h g₁ g₂)) ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-cst=idf (emloop g₁ ∙ emloop g₂) (emloop h) ◃∙
          ! (∙-assoc (emloop h) (emloop g₁) (emloop g₂)) ◃∙
          ! (ap (_∙ emloop g₂) (emloop-comp h g₁)) ◃∙
          ! (emloop-comp (G.comp h g₁) g₂) ◃∙
          ap emloop (ap (λ k → G.comp k g₂) (! (transp-Codes-β g₁ h))) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ⟨ 1 & 2 &
                post-rotate'-in {p = _ ◃∙ _ ◃∙ _ ◃∎} $
                transp-cst=idf-pentagon (emloop g₁) (emloop g₂) (emloop h)
              ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (transp-cst=idf (emloop g₁) (emloop h)) ◃∙
          transp-cst=idf (emloop g₂) (emloop h ∙ emloop g₁) ◃∙
          ! (ap (_∙ emloop g₂) (emloop-comp h g₁)) ◃∙
          ! (emloop-comp (G.comp h g₁) g₂) ◃∙
          ap emloop (ap (λ k → G.comp k g₂) (! (transp-Codes-β g₁ h))) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ₁⟨ 6 & 1 & ∘-ap emloop (λ k → G.comp k g₂) (! (transp-Codes-β g₁ h)) ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (transp-cst=idf (emloop g₁) (emloop h)) ◃∙
          transp-cst=idf (emloop g₂) (emloop h ∙ emloop g₁) ◃∙
          ! (ap (_∙ emloop g₂) (emloop-comp h g₁)) ◃∙
          ! (emloop-comp (G.comp h g₁) g₂) ◃∙
          ap (λ k → emloop (G.comp k g₂)) (! (transp-Codes-β g₁ h)) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ⟨ 5 & 2 & !ₛ $
                homotopy-naturality (λ k → emloop k ∙ emloop g₂)
                                    (λ k → emloop (G.comp k g₂))
                                    (λ k → ! (emloop-comp k g₂))
                                    (! (transp-Codes-β g₁ h))
              ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (transp-cst=idf (emloop g₁) (emloop h)) ◃∙
          transp-cst=idf (emloop g₂) (emloop h ∙ emloop g₁) ◃∙
          ! (ap (_∙ emloop g₂) (emloop-comp h g₁)) ◃∙
          ap (λ k → emloop k ∙ emloop g₂) (! (transp-Codes-β g₁ h)) ◃∙
          ! (emloop-comp (transp-C (emloop g₁) h) g₂) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ₁⟨ 4 & 1 & !-ap (_∙ emloop g₂) (emloop-comp h g₁) ⟩
          ap (λ p → transp-PF p (emloop h)) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (transp-cst=idf (emloop g₁) (emloop h)) ◃∙
          transp-cst=idf (emloop g₂) (emloop h ∙ emloop g₁) ◃∙
          ap (_∙ emloop g₂) (! (emloop-comp h g₁)) ◃∙
          ap (λ k → emloop k ∙ emloop g₂) (! (transp-Codes-β g₁ h)) ◃∙
          ! (emloop-comp (transp-C (emloop g₁) h) g₂) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ⟨ 3 & 2 & !ₛ $
                homotopy-naturality (transp-PF (emloop g₂))
                                    (_∙ emloop g₂)
                                    (transp-cst=idf (emloop g₂))
                                    (! (emloop-comp h g₁))
              ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (transp-cst=idf (emloop g₁) (emloop h)) ◃∙
          ap (transp-PF (emloop g₂)) (! (emloop-comp h g₁)) ◃∙
          transp-cst=idf (emloop g₂) (emloop (G.comp h g₁)) ◃∙
          ap (λ k → emloop k ∙ emloop g₂) (! (transp-Codes-β g₁ h)) ◃∙
          ! (emloop-comp (transp-C (emloop g₁) h) g₂) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ₁⟨ 5 & 1 & ap-∘ (_∙ emloop g₂) emloop (! (transp-Codes-β g₁ h)) ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (transp-cst=idf (emloop g₁) (emloop h)) ◃∙
          ap (transp-PF (emloop g₂)) (! (emloop-comp h g₁)) ◃∙
          transp-cst=idf (emloop g₂) (emloop (G.comp h g₁)) ◃∙
          ap (_∙ emloop g₂) (ap emloop (! (transp-Codes-β g₁ h))) ◃∙
          ! (emloop-comp (transp-C (emloop g₁) h) g₂) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ⟨ 4 & 2 & !ₛ $
                homotopy-naturality (transp-PF (emloop g₂))
                                    (_∙ emloop g₂)
                                    (transp-cst=idf (emloop g₂))
                                    (ap emloop (! (transp-Codes-β g₁ h)))
              ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (transp-cst=idf (emloop g₁) (emloop h)) ◃∙
          ap (transp-PF (emloop g₂)) (! (emloop-comp h g₁)) ◃∙
          ap (transp-PF (emloop g₂)) (ap emloop (! (transp-Codes-β g₁ h))) ◃∙
          transp-cst=idf (emloop g₂) (emloop (transp-C (emloop g₁) h)) ◃∙
          ! (emloop-comp (transp-C (emloop g₁) h) g₂) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ⟨ 2 & 3 & ∙-ap-seq (transp-PF (emloop g₂)) (swap-transp-emloop-seq g₁ h) ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (swap-transp-emloop g₁ h) ◃∙
          transp-cst=idf (emloop g₂) (emloop (transp-C (emloop g₁) h)) ◃∙
          ! (emloop-comp (transp-C (emloop g₁) h) g₂) ◃∙
          ap emloop (! (transp-Codes-β g₂ (transp-C (emloop g₁) h))) ◃∎
            =ₛ⟨ 3 & 3 & contract ⟩
          ap (λ p → transp-emloop p h) (emloop-comp g₁ g₂) ◃∙
          transp-∙ (emloop g₁) (emloop g₂) (emloop h) ◃∙
          ap (transp-PF (emloop g₂)) (swap-transp-emloop g₁ h) ◃∙
          swap-transp-emloop g₂ (transp-C (emloop g₁) h) ◃∎ ∎ₛ
          where g₁g₂ = G.comp g₁ g₂

      decode : {x : EM₁ G} → fst (Codes x) → embase == x
      decode {x} = Decode.f x
        where
        module Decode =
          EM₁Level₁FunElim {B = fst ∘ Codes} {C = embase' G ==_}
            emloop
            swap-transp-emloop
            decode-emloop-comp

    open Decode using (decode)

    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

  ⊙emloop-equiv : G.⊙El ⊙≃ ⊙Ω (⊙EM₁ G)
  ⊙emloop-equiv = ≃-to-⊙≃ emloop-equiv emloop-ident

  abstract
    instance
      EM₁-level₁ : {n : ℕ₋₂} → has-level (S (S (S n))) (EM₁ G)
      EM₁-level₁ {⟨-2⟩} = has-level-in pathspace-is-set
        where
        embase-loopspace-is-set : is-set (embase' G == embase)
        embase-loopspace-is-set = transport is-set (ua emloop-equiv) ⟨⟩
        pathspace-is-set : ∀ (x y : EM₁ G) → is-set (x == y)
        pathspace-is-set = EM₁-prop-elim (EM₁-prop-elim embase-loopspace-is-set)
      EM₁-level₁ {S n} = raise-level _ EM₁-level₁

  Ω¹-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))

ext: agda

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Functor.Algebras where

open import Level hiding (lift)

open import Categories.Category
open import Categories.Functor hiding (_≡_; id; _∘_; equiv; assoc; identityˡ; identityʳ; ∘-resp-≡)
open import Categories.Functor.Algebra

record F-Algebra-Morphism {o ℓ e} {C : Category o ℓ e} {F : Endofunctor C} (X Y : F-Algebra F) : Set (ℓ ⊔ e) where
  constructor _,_
  open Category C
  module X = F-Algebra X
  module Y = F-Algebra Y
  open Functor F
  field
    f : X.A ⇒ Y.A
    .commutes : f ∘ X.α ≡ Y.α ∘ F₁ f

F-Algebras : ∀ {o ℓ e} {C : Category o ℓ e} → Endofunctor C → Category (ℓ ⊔ o) (e ⊔ ℓ) e
F-Algebras {C = C} F = record
  { Obj = Obj′
  ; _⇒_ = Hom′
  ; _≡_ = _≡′_
  ; _∘_ = _∘′_
  ; id = id′
  ; assoc = assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; equiv = record
    { refl = refl
    ; sym = sym
    ; trans = trans
    }
  ; ∘-resp-≡ = ∘-resp-≡
  }
  where
  open Category C
  open Equiv
  open Functor F

  Obj′ = F-Algebra F

  Hom′ : (A B : Obj′) → Set _
  Hom′ = F-Algebra-Morphism

  _≡′_ : ∀ {A B} (f g : Hom′ A B) → Set _
  (f , _) ≡′ (g , _) = f ≡ g

  _∘′_ : ∀ {A B C} → Hom′ B C → Hom′ A B → Hom′ A C
  _∘′_ {A} {B} {C} (f , pf₁) (g , pf₂) = _,_ {X = A} {C} (f ∘ g) pf -- TODO: find out why the hell I need to provide these implicits
    where
    module A = F-Algebra A
    module B = F-Algebra B
    module C = F-Algebra C

    .pf : (f ∘ g) ∘ A.α ≡ C.α ∘ (F₁ (f ∘ g))
    pf = begin
           (f ∘ g) ∘ A.α
         ↓⟨ assoc ⟩
           f ∘ (g ∘ A.α)
         ↓⟨ ∘-resp-≡ʳ pf₂ ⟩
           f ∘ (B.α ∘ F₁ g)
         ↑⟨ assoc ⟩
           (f ∘ B.α) ∘ F₁ g
         ↓⟨ ∘-resp-≡ˡ pf₁ ⟩
           (C.α ∘ F₁ f) ∘ F₁ g
         ↓⟨ assoc ⟩
           C.α ∘ (F₁ f ∘ F₁ g)
         ↑⟨ ∘-resp-≡ʳ homomorphism ⟩
           C.α ∘ (F₁ (f ∘ g))
         ∎
      where
      open HomReasoning

  id′ : ∀ {A} → Hom′ A A
  id′ {A} = _,_ {X = A} {A} id pf
    where
    module A = F-Algebra A

    .pf : id ∘ A.α ≡ A.α ∘ F₁ id
    pf = begin
           id ∘ A.α
         ↓⟨ identityˡ ⟩
           A.α
         ↑⟨ identityʳ ⟩
           A.α ∘ id
         ↑⟨ ∘-resp-≡ʳ identity ⟩
           A.α ∘ F₁ id
         ∎
      where
      open HomReasoning

open import Categories.Object.Initial

module Lambek {o ℓ e} {C : Category o ℓ e} {F : Endofunctor C} (I : Initial (F-Algebras F)) where
  open Category C
  open Equiv
  module FA = Category (F-Algebras F) renaming (_∘_ to _∘FA_; _≡_ to _≡FA_)
  open Functor F
  import Categories.Morphisms as Morphisms
  open Morphisms C
  open Initial I
  open F-Algebra ⊥

  lambek : A ≅ F₀ A
  lambek = record
    { f = f′
    ; g = g′
    ; iso = iso′
    }
    where
    f′ : A ⇒ F₀ A
    f′ = F-Algebra-Morphism.f (! {lift ⊥})

    g′ : F₀ A ⇒ A
    g′ = α

    .iso′ : Iso f′ g′
    iso′ = record
      { isoˡ = isoˡ′
      ; isoʳ = begin
                 f′ ∘ g′
               ↓⟨ F-Algebra-Morphism.commutes (! {lift ⊥}) ⟩
                 F₁ g′ ∘ F₁ f′
               ↑⟨ homomorphism ⟩
                 F₁ (g′ ∘ f′)
               ↓⟨ F-resp-≡ isoˡ′ ⟩
                 F₁ id
               ↓⟨ identity ⟩
                 id
               ∎
      }
      where
      open FA hiding (id; module HomReasoning)
      open HomReasoning

      isoˡ′ = ⊥-id ((_,_ {C = C} {F} g′ refl) ∘FA !)

open Lambek public

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Agda.Builtin.TrustMe where

open import Agda.Builtin.Equality

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


text:
module Issue2649-1 where

module MyModule (A : Set) (a : A) where

  foo : A
  foo = a

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Prelude.Semigroup where

open import Prelude.Function
open import Prelude.Maybe

open import Prelude.List

open import Prelude.Semiring
open import Prelude.Applicative
open import Prelude.Functor
open import Prelude.Equality

record Semigroup {a} (A : Set a) : Set a where
  infixr 6 _<>_
  field
    _<>_ : A → A → A
open Semigroup {{...}} public

{-# DISPLAY Semigroup._<>_ _ a b = a <> b #-}
{-# DISPLAY Semigroup._<>_ _ = _<>_ #-}

record Semigroup/Laws {a} (A : Set a) : Set a where
  field
    {{super}} : Semigroup A
    semigroup-assoc : (a b c : A) → (a <> b) <> c ≡ a <> (b <> c)
open Semigroup/Laws {{...}} public hiding (super)

instance
  SemigroupList : ∀ {a} {A : Set a} → Semigroup (List A)
  _<>_   {{SemigroupList}} = _++_

  SemigroupFun : ∀ {a b} {A : Set a} {B : A → Set b} {{_ : ∀ {x} → Semigroup (B x)}} → Semigroup (∀ x → B x)
  _<>_   {{SemigroupFun}} f g x = f x <> g x

  SemigroupMaybe : ∀ {a} {A : Set a} → Semigroup (Maybe A)
  _<>_   {{SemigroupMaybe}} nothing  y = y
  _<>_   {{SemigroupMaybe}} (just x) _ = just x

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
------------------------------------------------------------------------
-- Comparisons of different kinds of lenses, focusing on the
-- definition of composable record setters and getters
------------------------------------------------------------------------

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

-- This module uses both dependent and non-dependent lenses, in order
-- to illustrate a problem with the non-dependent ones. It also uses
-- two kinds of dependent lenses, in order to illustrate a minor
-- problem with one of them.

module README.Record-getters-and-setters where

open import Equality.Propositional.Cubical
open import Prelude hiding (_∘_)

open import Bijection equality-with-J as Bij using (_↔_; module _↔_)
open import Equality.Decision-procedures equality-with-J
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J as F hiding (_∘_)

import Lens.Dependent
import Lens.Non-dependent.Higher equality-with-paths as Higher

------------------------------------------------------------------------
-- Dependent lenses with "remainder types" visible in the type

module Dependent₃ where

  open Lens.Dependent

  -- Nested records.

  record R₁ (A : Set) : Set where
    field
      f     : A → A
      x     : A
      lemma : ∀ y → f y ≡ y

  record R₂ : Set₁ where
    field
      A  : Set
      r₁ : R₁ A

  -- Lenses for each of the three fields of R₁.

  -- The x field is easiest, because it is independent of the others.
  --
  -- (Note that the from function is inferred automatically.)

  x : {A : Set} →
      Lens₃ (R₁ A) (∃ λ (f : A → A) → ∀ y → f y ≡ y) (λ _ → A)
  x = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ r → (R₁.f r , R₁.lemma r) , R₁.x r
        ; from = _
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    })

  -- The lemma field depends on the f field, so whenever the f field
  -- is set the lemma field needs to be updated as well.

  f : {A : Set} →
      Lens₃ (R₁ A) A (λ _ → ∃ λ (f : A → A) → ∀ y → f y ≡ y)
  f = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ r → R₁.x r , (R₁.f r , R₁.lemma r)
        ; from = _
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    })

  -- The lemma field can be updated independently.

  lemma : {A : Set} →
          Lens₃ (R₁ A) (A × (A → A)) (λ r → ∀ y → proj₂ r y ≡ y)
  lemma = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ r → (R₁.x r , R₁.f r) , R₁.lemma r
        ; from = _
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    })

  -- Note that the type of the last lens may not be quite
  -- satisfactory: the type of the lens does not guarantee that the
  -- lemma applies to the input's f field. The following lemma may
  -- provide some form of consolation:

  consolation : {A : Set} (r : R₁ A) → ∀ y → R₁.f r y ≡ y
  consolation = Lens₃.get lemma

  -- Let us now construct lenses for the same fields, but accessed
  -- through an R₂ record.

  -- First we define lenses for the fields of R₂ (note that the A lens
  -- does not seem to be very useful):

  A : Lens₃ R₂ ⊤ (λ _ → R₂)
  A = id₃

  r₁ : Lens₃ R₂ Set R₁
  r₁ = Eq.↔⇒≃ (record
    { surjection = record
      { logical-equivalence = record
        { to   = λ r → R₂.A r , R₂.r₁ r
        ; from = _
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ _ → refl
    })

  -- The lenses for the three R₁ fields can now be defined by
  -- composition:

  x₂ : Lens₃ R₂ _ (λ r → proj₁ r)
  x₂ = x ₃∘₃ r₁

  f₂ : Lens₃ R₂ _ (λ r → ∃ λ (f : proj₁ r → proj₁ r) → ∀ y → f y ≡ y)
  f₂ = f ₃∘₃ r₁

  lemma₂ : Lens₃ R₂ _ (λ r → ∀ y → proj₂ (proj₂ r) y ≡ y)
  lemma₂ = lemma ₃∘₃ r₁

  consolation₂ : (r : R₂) → ∀ y → proj₁ (Lens₃.get f₂ r) y ≡ y
  consolation₂ = Lens₃.get lemma₂

------------------------------------------------------------------------
-- Dependent lenses without "remainder types" visible in the type

module Dependent where

  open Lens.Dependent
  open Dependent₃ using (R₁; module R₁; R₂; module R₂)

  -- Lenses for each of the three fields of R₁.

  x : {A : Set} → Lens (R₁ A) (λ _ → A)
  x = Lens₃-to-Lens Dependent₃.x

  f : {A : Set} → Lens (R₁ A) (λ _ → ∃ λ (f : A → A) → ∀ y → f y ≡ y)
  f = Lens₃-to-Lens Dependent₃.f

  lemma : {A : Set} → Lens (R₁ A) (λ r → ∀ y → R₁.f r y ≡ y)
  lemma = Lens₃-to-Lens Dependent₃.lemma

  -- Note that the type of lemma is now more satisfactory: the type of
  -- the lens /does/ guarantee that the lemma applies to the input's f
  -- field.

  -- A lens for the r₁ field of R₂.

  r₁ : Lens R₂ (λ r → R₁ (R₂.A r))
  r₁ = Lens₃-to-Lens {-a = # 0-} Dependent₃.r₁

  -- Lenses for the fields of R₁, accessed through an R₂ record. Note
  -- the use of /forward/ composition.

  x₂ : Lens R₂ (λ r → R₂.A r)
  x₂ = r₁ ⨾ x

  f₂ : Lens R₂ (λ r → ∃ λ (f : R₂.A r → R₂.A r) → ∀ y → f y ≡ y)
  f₂ = r₁ ⨾ f

  lemma₂ : Lens R₂ (λ r → ∀ y → R₁.f (R₂.r₁ r) y ≡ y)
  lemma₂ = r₁ ⨾ lemma

------------------------------------------------------------------------
-- Non-dependent lenses

module Non-dependent where

  open Higher
  open Lens-combinators

  -- Labels.

  data Label : Set where
    ″f″ ″x″ ″lemma″ ″A″ ″r₁″ : Label

  -- Labels come with decidable equality.

  Label↔Fin : Label ↔ Fin 5
  Label↔Fin = record
    { surjection = record
      { logical-equivalence = record
        { to   = to
        ; from = from
        }
      ; right-inverse-of = to∘from
      }
    ; left-inverse-of = from∘to
    }
    where

    to : Label → Fin 5
    to ″f″     = fzero
    to ″x″     = fsuc fzero
    to ″lemma″ = fsuc (fsuc fzero)
    to ″A″     = fsuc (fsuc (fsuc fzero))
    to ″r₁″    = fsuc (fsuc (fsuc (fsuc fzero)))

    from : Fin 5 → Label
    from fzero                                 = ″f″
    from (fsuc fzero)                          = ″x″
    from (fsuc (fsuc fzero))                   = ″lemma″
    from (fsuc (fsuc (fsuc fzero)))            = ″A″
    from (fsuc (fsuc (fsuc (fsuc fzero))))     = ″r₁″
    from (fsuc (fsuc (fsuc (fsuc (fsuc ())))))

    to∘from : ∀ i → to (from i) ≡ i
    to∘from fzero                                 = refl
    to∘from (fsuc fzero)                          = refl
    to∘from (fsuc (fsuc fzero))                   = refl
    to∘from (fsuc (fsuc (fsuc fzero)))            = refl
    to∘from (fsuc (fsuc (fsuc (fsuc fzero))))     = refl
    to∘from (fsuc (fsuc (fsuc (fsuc (fsuc ())))))

    from∘to : ∀ ℓ → from (to ℓ) ≡ ℓ
    from∘to ″f″     = refl
    from∘to ″x″     = refl
    from∘to ″lemma″ = refl
    from∘to ″A″     = refl
    from∘to ″r₁″    = refl

  _≟_ : Decidable-equality Label
  _≟_ = Bij.decidable-equality-respects (inverse Label↔Fin) Fin._≟_

  -- Records.

  open import Records-with-with equality-with-J Label _≟_

  -- Nested records (defined using the record language from Record, so
  -- that we can use manifest fields).

  R₁ : Set → Signature _
  R₁ A = ∅ , ″f″     ∶ (λ _ → A → A)
           , ″x″     ∶ (λ _ → A)
           , ″lemma″ ∶ (λ r → ∀ y → (r · ″f″) y ≡ y)

  R₂ : Signature _
  R₂ = ∅ , ″A″  ∶ (λ _ → Set)
         , ″r₁″ ∶ (λ r → ↑ _ (Record (R₁ (r · ″A″))))

  -- Lenses for each of the three fields of R₁.

  -- The x field is easiest, because it is independent of the others.

  x : {A : Set} → Lens (Record (R₁ A)) A
  x {A} = isomorphism-to-lens

    (Record (R₁ A)                                    ↝⟨ Record↔Recʳ ⟩
     (∃ λ (f : A → A) → ∃ λ (x : A) → ∀ y → f y ≡ y)  ↝⟨ ∃-comm ⟩
     (A × ∃ λ (f : A → A) → ∀ y → f y ≡ y)            ↝⟨ ×-comm ⟩□
     (∃ λ (f : A → A) → ∀ y → f y ≡ y) × A            □)

  -- The lemma field depends on the f field, so whenever the f field
  -- is set the lemma field needs to be updated as well.

  f : {A : Set} →
      Lens (Record (R₁ A))
           (Record (∅ , ″f″     ∶ (λ _ → A → A)
                      , ″lemma″ ∶ (λ r → ∀ x → (r · ″f″) x ≡ x)))
  f {A} = isomorphism-to-lens

    (Record (R₁ A)                                    ↝⟨ Record↔Recʳ ⟩
     (∃ λ (f : A → A) → ∃ λ (x : A) → ∀ y → f y ≡ y)  ↝⟨ ∃-comm ⟩
     A × (∃ λ (f : A → A) → ∀ y → f y ≡ y)            ↝⟨ F.id ×-cong inverse Record↔Recʳ ⟩□
     A × Record _                                     □)

  -- The lemma field can be updated independently. Note the use of a
  -- manifest field in the type of the lens to capture the dependency
  -- between the two lens parameters.

  lemma : {A : Set} {f : A → A} →
          Lens (Record (R₁ A With ″f″ ≔ (λ _ → f)))
               (∀ x → f x ≡ x)
  lemma {A} {f} = isomorphism-to-lens

    (Record (R₁ A With ″f″ ≔ (λ _ → f))  ↝⟨ Record↔Recʳ ⟩□
     A × (∀ x → f x ≡ x)                 □)

  -- The use of a manifest field is problematic, because the domain of
  -- the lens is no longer Record (R₁ A). It is easy to convert
  -- records into the required form, but this conversion is not a
  -- non-dependent lens (due to the dependency).

  convert : {A : Set} (r : Record (R₁ A)) →
            Record (R₁ A With ″f″ ≔ (λ _ → r · ″f″))
  convert (rec (rec (rec (_ , f) , x) , lemma)) =
    rec (rec (_ , x) , lemma)

  -- Let us now try to construct lenses for the same fields, but
  -- accessed through an R₂ record.

  -- First we define a lens for the r₁ field.

  r₁ : {A : Set} →
       Lens (Record (R₂ With ″A″ ≔ λ _ → A)) (Record (R₁ A))
  r₁ {A} = isomorphism-to-lens

    (Record (R₂ With ″A″ ≔ λ _ → A)  ↝⟨ Record↔Recʳ ⟩
     ↑ _ (Record (R₁ A))             ↝⟨ Bij.↑↔ ⟩
     Record (R₁ A)                   ↝⟨ inverse ×-left-identity ⟩
     ⊤ × Record (R₁ A)               ↝⟨ inverse Bij.↑↔ ×-cong F.id ⟩□
     ↑ _ ⊤ × Record (R₁ A)           □)

  -- It is now easy to construct lenses for the embedded x and f
  -- fields using composition of lenses.

  x₂ : {A : Set} →
       Lens (Record (R₂ With ″A″ ≔ λ _ → A)) A
  x₂ = ⟨ _ , _ ⟩ x ∘ r₁

  f₂ : {A : Set} →
       Lens (Record (R₂ With ″A″ ≔ λ _ → A))
            (Record (∅ , ″f″     ∶ (λ _ → A → A)
                       , ″lemma″ ∶ (λ r → ∀ x → (r · ″f″) x ≡ x)))
  f₂ = ⟨ _ , _ ⟩ f ∘ r₁

  -- It is less obvious how to construct the corresponding lens for
  -- the embedded lemma field.

  module Lemma-lens
    (r₁₂ : {A : Set} {r : Record (R₁ A)} →
           Lens (Record (R₂ With ″A″  ≔ (λ _ → A)
                            With ″r₁″ ≔ (λ _ → lift r)))
                (Record (R₁ A With ″f″ ≔ (λ _ → r · ″f″)))) where

    -- To start with, what should the type of the lemma lens be? The
    -- type used below is an obvious choice.

    lemma₂ : {A : Set} {r : Record (R₁ A)} →
             Lens (Record (R₂ With ″A″  ≔ (λ _ → A)
                              With ″r₁″ ≔ (λ _ → lift r)))
                  (∀ x → (r · ″f″) x ≡ x)

    -- If we can construct a suitable lens r₁₂, with the type
    -- signature given above, then we can define the lemma lens using
    -- composition.

    lemma₂ = ⟨ _ , _ ⟩ lemma ∘ r₁₂

    -- However, we cannot define r₁₂.

    not-r₁₂ : ⊥
    not-r₁₂ = no-isomorphism isomorphism
      where
      open Lens

      isomorphisms : ∀ _ _ → _
      isomorphisms = λ A r →
        ⊤                                                 ↝⟨ inverse Bij.↑↔ ⟩
        ↑ _ ⊤                                             ↝⟨ inverse Record↔Recʳ ⟩
        Record (R₂ With ″A″  ≔ (λ _ → A)
                   With ″r₁″ ≔ (λ _ → lift r))            ↔⟨ equiv r₁₂ ⟩
        R r₁₂ × Record (R₁ A With ″f″ ≔ (λ _ → r · ″f″))  ↝⟨ F.id ×-cong Record↔Recʳ ⟩□
        R r₁₂ × A × (∀ y → (r · ″f″) y ≡ y)               □

      isomorphism : ∃ λ (A : Set₁) → ⊤ ↔ A × Bool
      isomorphism =
        _ ,
        (⊤                               ↝⟨ isomorphisms Bool r ⟩
         R r₁₂ × Bool × (∀ b → b ≡ b)    ↝⟨ F.id ×-cong ×-comm ⟩
         R r₁₂ × (∀ b → b ≡ b) × Bool    ↝⟨ ×-assoc ⟩□
         (R r₁₂ × (∀ b → b ≡ b)) × Bool  □)
        where
        r : Record (R₁ Bool)
        r = rec (rec (rec (_ , F.id) , true) , λ _ → refl)

      no-isomorphism : ¬ ∃ λ (A : Set₁) → ⊤ ↔ A × Bool
      no-isomorphism (A , iso) = Bool.true≢false (
        true                           ≡⟨⟩
        proj₂ (a , true)               ≡⟨ cong proj₂ $ sym $ right-inverse-of (a , true) ⟩
        proj₂ (to (from (a , true)))   ≡⟨⟩
        proj₂ (to (from (a , false)))  ≡⟨ cong proj₂ $ right-inverse-of (a , false) ⟩
        proj₂ (a , false)              ≡⟨ refl ⟩∎
        false                          ∎)
        where
        open _↔_ iso

        a : A
        a = proj₁ (to _)

  -- Conclusion: The use of manifest fields limits the usefulness of
  -- these lenses, because they do not compose as well as they do for
  -- non-dependent records. Dependent lenses seem to be more useful.

max_stars_repo_name: Saizan/dependent-lenses

max_issues_repo_name: Saizan/dependent-lenses

max_forks_repo_name: Saizan/dependent-lenses


text:
module Type.Category.ExtensionalFunctionsCategory{ℓ} where

open import Data
open import Functional
open import Function.Equals
open import Function.Equals.Proofs
open import Logic.Propositional
import      Relator.Equals as Eq
open import Relator.Equals.Proofs.Equiv
open import Structure.Category
open import Structure.Categorical.Properties
open import Type
open import Type.Properties.Singleton

-- The set category but the equality on the morphisms/functions is pointwise/extensional.
typeExtensionalFnCategory : Category{Obj = Type{ℓ}}(_→ᶠ_) ⦃ [⊜]-equiv ⦃ [≡]-equiv ⦄ ⦄
Category._∘_ typeExtensionalFnCategory = _∘_
Category.id  typeExtensionalFnCategory = id
Category.binaryOperator typeExtensionalFnCategory = [⊜][∘]-binaryOperator
Morphism.Associativity.proof (Category.associativity typeExtensionalFnCategory) {x = _} {_} {_} {x = f} {g} {h} = [⊜]-associativity {x = f}{y = g}{z = h}
Category.identity typeExtensionalFnCategory = [∧]-intro (Morphism.intro (Dependent.intro Eq.[≡]-intro)) (Morphism.intro (Dependent.intro Eq.[≡]-intro))

typeExtensionalFnCategoryObject : CategoryObject
typeExtensionalFnCategoryObject = intro typeExtensionalFnCategory

Empty-initialObject : Object.Initial{Obj = Type{ℓ}}(_→ᶠ_) ⦃ [⊜]-equiv ⦃ [≡]-equiv ⦄ ⦄ (Empty)
IsUnit.unit Empty-initialObject = empty
_⊜_.proof (IsUnit.uniqueness Empty-initialObject {f}) {}

Unit-terminalObject : Object.Terminal{Obj = Type{ℓ}}(_→ᶠ_) ⦃ [⊜]-equiv ⦃ [≡]-equiv ⦄ ⦄ (Unit)
IsUnit.unit Unit-terminalObject = const <>
_⊜_.proof (IsUnit.uniqueness Unit-terminalObject {f}) {_} = Eq.[≡]-intro

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Oscar.Data.Vec where

open import Data.Vec public
open import Oscar.Data.Nat
open import Oscar.Data.Equality

open import Data.Nat

map₂ : ∀ {a b} {A : Set a} {B : Set b} {m n}
           → ∀ {c} {C : Set c} (f : A → B → C)
           → Vec A m → Vec B n → Vec C (m * n)
map₂ f xs ys = map f xs ⊛* ys

open import Data.Fin

delete : ∀ {a n} {A : Set a} → Fin (suc n) → Vec A (suc n) → Vec A n
delete zero (x ∷ xs) = xs
delete {n = zero} (suc ()) _
delete {n = suc n} (suc i) (x ∷ xs) = x ∷ delete i xs

open import Function
open import Data.Product

tabulate⋆ : ∀ {n a} {A : Set a} → (F : Fin n → A) → ∃ λ (v : Vec A n) → ∀ (i : Fin n) → F i ∈ v
tabulate⋆ {zero} F = [] , (λ ())
tabulate⋆ {suc n} F = let v , t = tabulate⋆ (F ∘ suc) in F zero ∷ v , (λ { zero → here ; (suc i) → there (t i)})


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

module PiG where

import Level as L
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Data.Nat
open import Function
open import Relation.Binary.PropositionalEquality
open import Relation.Binary

------------------------------------------------------------------------------
-- Reasoning about paths

pathInd : ∀ {u u'} → {A : Set u} →
  (C : (x y : A) → (x ≡ y) → Set u') →
  (c : (x : A) → C x x refl) →
  ((x y : A) (p : x ≡ y) → C x y p)
pathInd C c x .x refl = c x

trans' : {A : Set} → {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
trans' {A} {x} {y} {z} p q =
  pathInd
    (λ x y p → ((z : A) → (q : y ≡ z) → (x ≡ z)))
    (pathInd (λ x z q → x ≡ z) (λ _ → refl))
    x y p z q

ap : {A B : Set} {x y : A} → (f : A → B) → (x ≡ y) → (f x ≡ f y)
ap {A} {B} {x} {y} f p =
  pathInd
    (λ x y p → f x ≡ f y)
    (λ x → refl)
    x y p

ap× : {A B : Set} {x y : A} {z w : B} → (x ≡ y) → (z ≡ w) →
      ((x , z) ≡ (y , w))
ap× {A} {B} {x} {y} {z} {w} p₁ p₂ =
  pathInd
    (λ x y p₁ → ((z : B) (w : B) (p₂ : z ≡ w) → ((x , z) ≡ (y , w))))
    (λ x → pathInd
             (λ z w p₂ → ((x , z) ≡ (x , w)))
             (λ z → refl))
    x y p₁ z w p₂

transport : {A : Set} {x y : A} {P : A → Set} → (p : x ≡ y) → P x → P y
transport {A} {x} {y} {P} p =
  pathInd
    (λ x y p → (P x → P y))
    (λ x → id)
    x y p

------------------------------------------------------------------------------
-- Codes for our types

data B : Set where
  -- no zero because we map types to POINTED SETS
  ONE   : B
  PLUS  : B → B → B
  TIMES : B → B → B
  HALF  : B -- used to explore fractionals

{--

Now let's define groups/groupoids

The type 1/2 is modeled by the group { refl , loop }
where loop is self-inverse, i.e., loop . loop = refl

We always get refl, inverses, and associativity for free. We need to
explicitly add the new element 'loop' and the new equation
'loop . loop = refl'

--}

cut-path : {A : Set} → {x : A} → (f g : ( x ≡ x) → (x ≡ x)) → x ≡ x → Set
cut-path f g a = f a ≡ g a

record GroupoidVal : Set₁ where
  constructor •[_,_,_,_,_,_]
  field
    ∣_∣       : Set
    •        : ∣_∣
    path     : • ≡ •        -- the additional path (loop)
    -- truncate : trans' path path ≡ refl  -- the equivalence used to truncate
    -- truncate : (f : • ≡ • → • ≡ •) → (b : • ≡ •) → f b ≡ refl
    path-rel₁ : • ≡ • → • ≡ •
    path-rel₂ : • ≡ • → • ≡ •
    truncate : cut-path path-rel₁ path-rel₂ path

open GroupoidVal public

-- Example:

const-loop : {A : Set} {x : A} → (y : x ≡ x) → x ≡ x
const-loop _ = refl

postulate iloop     : tt ≡ tt
          itruncate : (f : tt ≡ tt → tt ≡ tt) → cut-path f const-loop iloop
              -- (trans' iloop iloop) ≡ refl

2loop : {A : Set} → {x : A} → x ≡ x → x ≡ x
2loop x = trans' x x

half : GroupoidVal
half = •[ ⊤ , tt , iloop , 2loop , const-loop , itruncate 2loop ]

-- Interpretations of types

⟦_⟧ : B → GroupoidVal
⟦ ONE ⟧ = •[ ⊤ , tt , refl , id , id , refl ]
⟦ PLUS b₁ b₂ ⟧ with ⟦ b₁ ⟧ | ⟦ b₂ ⟧
... | •[ B₁ , x₁ , p₁ , f₁ , g₁ , t₁ ] | •[ B₂ , x₂ , p₂ , f₂ , g₂ , t₂ ] =
  •[ B₁ ⊎ B₂ , inj₁ x₁ , ap inj₁ p₁ , id , id ,  refl ]
⟦ TIMES b₁ b₂ ⟧ with ⟦ b₁ ⟧ | ⟦ b₂ ⟧
... | •[ B₁ , x₁ , p₁ , f₁ , g₁ , t₁ ] | •[ B₂ , x₂ , p₂ , f₂ , g₂ , t₂ ] =
  •[ B₁ × B₂ , (x₁ , x₂) , ap× p₁ p₂ , id , id , refl ]
⟦ HALF ⟧ = half

-- Combinators

data _⟷_ : B → B → Set₁ where
  swap× : {b₁ b₂ : B} → TIMES b₁ b₂ ⟷ TIMES b₂ b₁

record GFunctor (G₁ G₂ : GroupoidVal) : Set where
  field
    fun : ∣ G₁ ∣ → ∣ G₂ ∣
    baseP : fun (• G₁) ≡ (• G₂)
    -- dependent paths??
    isoP : {x y : ∣ G₁ ∣} (p : x ≡ y) → (fun x ≡ fun y)

eval : {b₁ b₂ : B} → (b₁ ⟷ b₂) → GFunctor ⟦ b₁ ⟧ ⟦ b₂ ⟧
eval swap× =
  record {
    fun = swap;
    baseP = refl;
    isoP = λ p → ap swap p
  }

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

{-
   Some old scribblings
A-2 : Set
A-2 = ⊤

postulate
  S⁰ : Set
  S¹ : Set

record Trunc-1 (A : Set) : Set where
  field
    embed : A → Trunc-1 A
    hub : (r : S⁰ → Trunc-1 A) → Trunc-1 A
    spoke : (r : S⁰ → Trunc-1 A) → (x : S⁰) → r x ≡ hub r

-}

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

record 2Groupoid : Set₁ where
  constructor ²[_,_,_]
  field
    obj      : Set
    hom     : Rel obj L.zero        -- paths (loop)
    2path    : ∀ {a b} → hom a b → hom a b → Set  -- 2paths, i.e. path eqns

open 2Groupoid public

hom⊤ : Rel ⊤ L.zero
hom⊤ = _≡_

2path⊤ : Rel (hom⊤ tt tt) L.zero
2path⊤ = _≡_

half' : 2Groupoid
half' = ²[ ⊤ , hom⊤ , 2path⊤ ]

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module free-vars where
open import cedille-types
open import syntax-util
open import general-util
open import type-util

infixr 7 _++ₛ_
_++ₛ_ : stringset → stringset → stringset
s₁ ++ₛ s₂ = stringset-insert* s₂ (stringset-strings s₁)

stringset-single : string → stringset
stringset-single = flip trie-single triv

{-# TERMINATING #-}
free-vars : ∀ {ed} → ⟦ ed ⟧ → stringset
free-vars? : ∀ {ed} → maybe ⟦ ed ⟧ → stringset
free-vars-args : args → stringset
free-vars-arg : arg → stringset
free-vars-cases : cases → stringset
free-vars-case : case → stringset
free-vars-tk : tpkd → stringset
free-vars-tT : tmtp → stringset

free-vars-tk = free-vars -tk'_
free-vars-tT = free-vars -tT'_

free-vars? = maybe-else empty-stringset free-vars

free-vars {TERM} (App t t') = free-vars t ++ₛ free-vars t'
free-vars {TERM} (AppE t tT) = free-vars t ++ₛ free-vars -tT' tT
free-vars {TERM} (Beta t t') = free-vars t ++ₛ free-vars t'
free-vars {TERM} (Delta b? T t) = free-vars? (fst <$> b?) ++ₛ free-vars? (snd <$> b?) ++ₛ free-vars T ++ₛ free-vars t
free-vars {TERM} (Hole pi) = empty-stringset
free-vars {TERM} (IotaPair t t' x T) = free-vars t ++ₛ free-vars t' ++ₛ stringset-remove (free-vars T) x
free-vars {TERM} (IotaProj t n) = free-vars t
free-vars {TERM} (Lam me x tk t) = maybe-else empty-stringset (free-vars-tk) tk ++ₛ stringset-remove (free-vars t) x
free-vars {TERM} (LetTm me x T? t t') = free-vars? T? ++ₛ free-vars t ++ₛ stringset-remove (free-vars t') x
free-vars {TERM} (LetTp x k T t) = free-vars k ++ₛ free-vars T ++ₛ stringset-remove (free-vars t) x
free-vars {TERM} (Phi tₑ t₁ t₂) = free-vars tₑ ++ₛ free-vars t₁ ++ₛ free-vars t₂
free-vars {TERM} (Rho t x T t') = free-vars t ++ₛ stringset-remove (free-vars T) x ++ₛ free-vars t'
free-vars {TERM} (Sigma t) = free-vars t
free-vars {TERM} (Mu μ t T t~ cs) = free-vars t ++ₛ free-vars? T ++ₛ free-vars-cases cs
free-vars {TERM} (Var x) = stringset-single x
free-vars {TYPE} (TpAbs me x tk T) = free-vars-tk tk ++ₛ stringset-remove (free-vars T) x
free-vars {TYPE} (TpIota x T₁ T₂) = free-vars T₁ ++ₛ stringset-remove (free-vars T₂) x
free-vars {TYPE} (TpApp T tT) = free-vars T ++ₛ free-vars -tT' tT
free-vars {TYPE} (TpEq t₁ t₂) = free-vars t₁ ++ₛ free-vars t₂
free-vars {TYPE} (TpHole pi) = empty-stringset
free-vars {TYPE} (TpLam x tk T) = free-vars-tk tk ++ₛ stringset-remove (free-vars T) x
free-vars {TYPE} (TpVar x) = stringset-single x
free-vars {KIND} KdStar = empty-stringset
free-vars {KIND} (KdHole pi) = empty-stringset
free-vars {KIND} (KdAbs x tk k) = free-vars-tk tk ++ₛ stringset-remove (free-vars k) x

free-vars-arg (Arg t) = free-vars t
free-vars-arg (ArgE tT) = free-vars -tT' tT
free-vars-args = foldr (_++ₛ_ ∘ free-vars-arg) empty-stringset
free-vars-case (Case x cas t T) = foldr (λ {(CaseArg e x tk) → flip trie-remove x}) (free-vars t) cas
free-vars-cases = foldr (_++ₛ_ ∘ free-vars-case) empty-stringset

{-# TERMINATING #-}
erase : ∀ {ed} → ⟦ ed ⟧ → ⟦ ed ⟧
erase-cases : cases → cases
erase-case : case → case
erase-args : args → 𝕃 term
erase-params : params → 𝕃 var
erase-tk : tpkd → tpkd
erase-tT : tmtp → tmtp
erase-is-mu : is-mu → is-mu

erase-is-mu = either-else (λ _ → inj₁ nothing) inj₂

erase-tk = erase -tk_
erase-tT = erase -tT_

erase {TERM} (App t t') = App (erase t) (erase t')
erase {TERM} (AppE t T) = erase t
erase {TERM} (Beta t t') = erase t'
erase {TERM} (Delta b? T t) = id-term
erase {TERM} (Hole pi) = Hole pi
erase {TERM} (IotaPair t t' x T) = erase t
erase {TERM} (IotaProj t n) = erase t
erase {TERM} (Lam me x tk t) = if me then erase t else Lam ff x nothing (erase t)
erase {TERM} (LetTm me x T? t t') =
  let t'' = erase t' in
  if ~ me && stringset-contains (free-vars t'') x
    then LetTm ff x nothing (erase t) t''
    else t''
erase {TERM} (LetTp x k T t) = erase t
erase {TERM} (Phi tₑ t₁ t₂) = erase t₂
erase {TERM} (Rho t x T t') = erase t'
erase {TERM} (Sigma t) = erase t
erase {TERM} (Mu μ t T t~ ms) = Mu (erase-is-mu μ) (erase t) nothing t~ (erase-cases ms)
erase {TERM} (Var x) = Var x
erase {TYPE} (TpAbs me x tk T) = TpAbs me x (erase-tk tk) (erase T)
erase {TYPE} (TpIota x T₁ T₂) = TpIota x (erase T₁) (erase T₂)
erase {TYPE} (TpApp T tT) = TpApp (erase T) (erase -tT tT)
erase {TYPE} (TpEq t₁ t₂) = TpEq (erase t₁) (erase t₂)
erase {TYPE} (TpHole pi) = TpHole pi
erase {TYPE} (TpLam x tk T) = TpLam x (erase-tk tk) (erase T)
erase {TYPE} (TpVar x) = TpVar x
erase {KIND} KdStar = KdStar
erase {KIND} (KdHole pi) = KdHole pi
erase {KIND} (KdAbs x tk k) = KdAbs x (erase-tk tk) (erase k)

erase-case-args : case-args → case-args
erase-case-args (CaseArg ff x _ :: cas) = CaseArg ff x nothing :: erase-case-args cas
erase-case-args (_ :: cas) = erase-case-args cas
erase-case-args [] = []

erase-cases = map erase-case
erase-case (Case x cas t T) = Case x (erase-case-args cas) (erase t) T

erase-args (Arg t :: as) = erase t :: erase-args as
erase-args (_ :: as) = erase-args as
erase-args [] = []

erase-arg-keep : arg → arg
erase-args-keep : args → args
erase-args-keep = map erase-arg-keep
erase-arg-keep (Arg t) = Arg (erase t)
erase-arg-keep (ArgE tT) = ArgE (erase -tT tT)

erase-params (Param ff x (Tkt T) :: ps) = x :: erase-params ps
erase-params (_ :: ps) = erase-params ps
erase-params [] = []

free-vars-erased : ∀ {ed} → ⟦ ed ⟧ → stringset
free-vars-erased = free-vars ∘ erase

is-free-in : ∀ {ed} → var → ⟦ ed ⟧ → 𝔹
is-free-in x t = stringset-contains (free-vars t) x

are-free-in-h : ∀ {X} → trie X → stringset → 𝔹
are-free-in-h xs fxs = list-any (trie-contains fxs) (map fst (trie-mappings xs))

are-free-in : ∀ {X} {ed} → trie X → ⟦ ed ⟧ → 𝔹
are-free-in xs t = are-free-in-h xs (free-vars t)

erase-if : ∀ {ed} → 𝔹 → ⟦ ed ⟧ → ⟦ ed ⟧
erase-if tt = erase
erase-if ff = id

infix 5 `|_|`
`|_|` = erase

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille


text:
-- Reported and fixed by Andrea Vezzosi.

module Issue902 where

module M (A : Set) where

postulate
  A : Set
  F : Set -> Set

test : A
test = {! let module m = M (F A) in ? !}
-- C-c C-r gives  let module m = M F A in ?
--    instead of  let module m = M (F A) in ?


text:
-- Andreas, 2013-06-15 reported by Guillaume Brunerie
-- {-# OPTIONS -v malonzo.definition:100 #-}
module Issue867 where

{- The program below gives the following error when trying to compile it (using MAlonzo)

$ agda -c Test.agda
Checking Test (/tmp/Test.agda).
Finished Test.
Compiling Test in /tmp/Test.agdai to /tmp/MAlonzo/Code/Test.hs
Calling: ghc -O -o /tmp/Test -Werror -i/tmp -main-is MAlonzo.Code.Test /tmp/MAlonzo/Code/Test.hs --make -fwarn-incomplete-patterns -fno-warn-overlapping-patterns
[1 of 2] Compiling MAlonzo.RTE      ( MAlonzo/RTE.hs, MAlonzo/RTE.o )
[2 of 2] Compiling MAlonzo.Code.Test ( /tmp/MAlonzo/Code/Test.hs, /tmp/MAlonzo/Code/Test.o )

Compilation error:

/tmp/MAlonzo/Code/Test.hs:21:35:
    Not in scope: `d5'
    Perhaps you meant one of these:
      `d1' (line 11), `d4' (line 26), `d9' (line 29)
-}

-- Here is the program

module Test where

data ℕ : Set where
  O : ℕ
  S : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

postulate
  IO : ∀ {i} → Set i → Set i
  return : ∀ {i} {A : Set i} → A → IO A

{-# BUILTIN IO IO #-}

main : IO ℕ
main = return (S 1)

{- It’s the first time I try to compile an Agda program, so presumably I’m doing something wrong. But even if I’m doing something wrong, Agda should be the one giving the error, not ghc. -}

-- Should work now.


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Limits.Pullback where

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

open import Cubical.Data.Sigma

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Instances.Cospan

private
  variable
    ℓ ℓ' : Level

module _ (C : Category ℓ ℓ') where

  open Category C
  open Functor

  record Cospan : Type (ℓ-max ℓ ℓ') where
    constructor cospan
    field
      l m r : ob
      s₁ : C [ l , m ]
      s₂ : C [ r , m ]

  open Cospan

  isPullback : (cspn : Cospan) →
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → Type (ℓ-max ℓ ℓ')
  isPullback cspn {c} p₁ p₂ H =
    ∀ {d} (h : C [ d , cspn .l ]) (k : C [ d , cspn .r ])
          (H' : h ⋆ cspn .s₁ ≡ k ⋆ cspn .s₂)
    → ∃![ hk ∈ C [ d , c ] ] (h ≡ hk ⋆ p₁) × (k ≡ hk ⋆ p₂)

  isPropIsPullback : (cspn : Cospan) →
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → isProp (isPullback cspn p₁ p₂ H)
  isPropIsPullback cspn p₁ p₂ H =
    isPropImplicitΠ (λ x → isPropΠ3 λ h k H' → isPropIsContr)

  record Pullback (cspn : Cospan) : Type (ℓ-max ℓ ℓ') where
    field
      pbOb  : ob
      pbPr₁ : C [ pbOb , cspn .l ]
      pbPr₂ : C [ pbOb , cspn .r ]
      pbCommutes : pbPr₁ ⋆ cspn .s₁ ≡ pbPr₂ ⋆ cspn .s₂
      univProp : isPullback cspn pbPr₁ pbPr₂ pbCommutes

  open Pullback

  pullbackArrow :
    {cspn : Cospan} (pb : Pullback cspn)
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) → C [ c , pb . pbOb ]
  pullbackArrow pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .fst

  pullbackArrowPr₁ :
    {cspn : Cospan} (pb : Pullback cspn)
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) →
    p₁ ≡ pullbackArrow pb p₁ p₂ H ⋆ pbPr₁ pb
  pullbackArrowPr₁ pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .snd .fst

  pullbackArrowPr₂ :
    {cspn : Cospan} (pb : Pullback cspn)
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂) →
    p₂ ≡ pullbackArrow pb p₁ p₂ H ⋆ pbPr₂ pb
  pullbackArrowPr₂ pb p₁ p₂ H = pb .univProp p₁ p₂ H .fst .snd .snd

  pullbackArrowUnique :
    {cspn : Cospan} (pb : Pullback cspn)
    {c : ob} (p₁ : C [ c , cspn .l ]) (p₂ : C [ c , cspn .r ])
    (H : p₁ ⋆ cspn .s₁ ≡ p₂ ⋆ cspn .s₂)
    (pbArrow' : C [ c , pb .pbOb ])
    (H₁ : p₁ ≡ pbArrow' ⋆ pbPr₁ pb) (H₂ : p₂ ≡ pbArrow' ⋆ pbPr₂ pb)
    → pullbackArrow pb p₁ p₂ H ≡ pbArrow'
  pullbackArrowUnique pb p₁ p₂ H pbArrow' H₁ H₂ =
    cong fst (pb .univProp p₁ p₂ H .snd (pbArrow' , (H₁ , H₂)))

  Pullbacks : Type (ℓ-max ℓ ℓ')
  Pullbacks = (cspn : Cospan) → Pullback cspn

  hasPullbacks : Type (ℓ-max ℓ ℓ')
  hasPullbacks = ∥ Pullbacks ∥

-- TODO: finish the following show that this definition of Pullback
-- is equivalent to the Cospan limit
module _ {C : Category ℓ ℓ'} where
  open Category C
  open Functor

  Cospan→Func : Cospan C → Functor CospanCat C
  Cospan→Func (cospan l m r f g) .F-ob ⓪ = l
  Cospan→Func (cospan l m r f g) .F-ob ① = m
  Cospan→Func (cospan l m r f g) .F-ob ② = r
  Cospan→Func (cospan l m r f g) .F-hom {⓪} {①} k = f
  Cospan→Func (cospan l m r f g) .F-hom {②} {①} k = g
  Cospan→Func (cospan l m r f g) .F-hom {⓪} {⓪} k = id
  Cospan→Func (cospan l m r f g) .F-hom {①} {①} k = id
  Cospan→Func (cospan l m r f g) .F-hom {②} {②} k = id
  Cospan→Func (cospan l m r f g) .F-id {⓪} = refl
  Cospan→Func (cospan l m r f g) .F-id {①} = refl
  Cospan→Func (cospan l m r f g) .F-id {②} = refl
  Cospan→Func (cospan l m r f g) .F-seq {⓪} {⓪} {⓪} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {⓪} {⓪} {①} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {⓪} {①} {①} φ ψ = sym (⋆IdR _)
  Cospan→Func (cospan l m r f g) .F-seq {①} {①} {①} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {②} {②} {②} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {②} {②} {①} φ ψ = sym (⋆IdL _)
  Cospan→Func (cospan l m r f g) .F-seq {②} {①} {①} φ ψ = sym (⋆IdR _)


text:
module Issue1839.B where

open import Issue1839.A

postulate
  DontPrintThis : Set

{-# DISPLAY DontPrintThis = PrintThis #-}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2019-04-12, issue #3684
-- Report also available record fields in case user gives spurious fields.

-- {-# OPTIONS -v tc.record:30 #-}

record R : Set₁ where
  field
    foo {boo} moo : Set

test : (A : Set) → R
test A = record
  { moo = A
  ; bar = A
  ; far = A
  }

-- The record type R does not have the fields bar, far but it would
-- have the fields foo, boo
-- when checking that the expression
-- record { moo = A ; bar = A ; far = A } has type R

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

module Data.List.Relation.Unary where

open import Prelude
open import Data.List.Base
open import Data.Fin
open import Relation.Nullary
open import Data.Sum

private
  variable p : Level

module Inductive◇ where
 data ◇ {A : Type a} (P : A → Type p) : List A → Type (a ℓ⊔ p) where
   here   : ∀ {x xs} → P x      → ◇ P (x ∷ xs)
   there  : ∀ {x xs} → ◇ P xs   → ◇ P (x ∷ xs)

◇ : (P : A → Type p) → List A → Type _
◇ P xs = ∃[ i ] P (xs ! i)

◇! : (P : A → Type p) → List A → Type _
◇! P xs = isContr (◇ P xs)

module Exists {a} {A : Type a} {p} (P : A → Type p) where
  push : ∀ {x xs} → ◇ P xs → ◇ P (x ∷ xs)
  push (n , p) = fs n , p

  pull : ∀ {x xs} → ¬ P x → ◇ P (x ∷ xs) → ◇ P xs
  pull ¬Px (f0   , p) = ⊥-elim (¬Px p)
  pull ¬Px (fs n , p) = n , p

  uncons : ∀ {x xs} → ◇ P (x ∷ xs) → P x ⊎ ◇ P xs
  uncons (f0 , p) = inl p
  uncons (fs x , p) = inr (x , p)

  infixr 5 _++◇_ _◇++_
  _++◇_ : ∀ {xs} ys → ◇ P xs → ◇ P (ys ++ xs)
  [] ++◇ ys = ys
  (x ∷ xs) ++◇ ys = push (xs ++◇ ys)

  _◇++_ : ∀ xs → ◇ P xs → ∀ {ys} → ◇ P (xs ++ ys)
  _◇++_ (x ∷ xs) (f0  , ∃Pxs) = f0 , ∃Pxs
  _◇++_ (x ∷ xs) (fs n , ∃Pxs) = push (xs ◇++ (n , ∃Pxs))

  push! : ∀ {x xs} → ¬ P x → ◇! P xs → ◇! P (x ∷ xs)
  push! ¬Px x∈!xs .fst = push (x∈!xs .fst)
  push! ¬Px x∈!xs .snd (f0   , px) = ⊥-elim (¬Px px)
  push! ¬Px x∈!xs .snd (fs n  , y∈xs) i = push (x∈!xs .snd (n , y∈xs) i)

  pull! : ∀ {x xs} → ¬ P x → ◇! P (x ∷ xs) → ◇! P xs
  pull! ¬Px ((f0   , px    ) , uniq) = ⊥-elim (¬Px px)
  pull! ¬Px ((fs n  , x∈xs  ) , uniq) .fst = (n , x∈xs)
  pull! ¬Px ((fs n  , x∈xs  ) , uniq) .snd (m , x∈xs′) i =
    pull ¬Px (uniq (fs m , x∈xs′ ) i)

  here! : ∀ {x xs} → isContr (P x) → ¬ ◇ P xs → ◇! P (x ∷ xs)
  here! Px p∉xs .fst = f0 , Px .fst
  here! Px p∉xs .snd (f0  , p∈xs) i .fst = f0
  here! Px p∉xs .snd (f0  , p∈xs) i .snd = Px .snd p∈xs i
  here! Px p∉xs .snd (fs n , p∈xs) = ⊥-elim (p∉xs (n , p∈xs))

  module _ (P? : ∀ x → Dec (P x)) where
    open import Relation.Nullary.Decidable.Logic

    ◇? : ∀ xs → Dec (◇ P xs)
    ◇? [] = no λ ()
    ◇? (x ∷ xs) =  ⟦yes ⟦l f0 ,_ ,r push ⟧ ,no uncons ⟧ (P? x || ◇? xs)

◻ : (P : A → Type p) → List A → Type _
◻ P xs = ∀ i → P (xs ! i)

module Forall {a} {A : Type a} {p} (P : A → Type p) where
  push : ∀ {x xs} → P x → ◻ P xs → ◻ P (x ∷ xs)
  push Px Pxs f0 = Px
  push Px Pxs (fs n) = Pxs n

  uncons : ∀ {x xs} → ◻ P (x ∷ xs) → P x × ◻ P xs
  uncons Pxs = Pxs f0 , Pxs ∘ fs

  pull : ∀ {x xs} → ◻ P (x ∷ xs) → ◻ P xs
  pull = snd ∘ uncons

  _++◇_ : ∀ xs {ys} → ◻ P (xs ++ ys) → ◻ P ys
  [] ++◇ xs⊆P = xs⊆P
  (x ∷ xs) ++◇ xs⊆P = xs ++◇ (xs⊆P ∘ fs)

  _◇++_ : ∀ xs {ys} → ◻ P (xs ++ ys) → ◻ P xs
  ([] ◇++ xs⊆P) ()
  ((x ∷ xs) ◇++ xs⊆P) f0 = xs⊆P f0
  ((x ∷ xs) ◇++ xs⊆P) (fs n) = (xs ◇++ pull xs⊆P) n

  both : ∀ xs {ys} → ◻ P xs → ◻ P ys → ◻ P (xs ++ ys)
  both [] xs⊆P ys⊆P = ys⊆P
  both (x ∷ xs) xs⊆P ys⊆P f0 = xs⊆P f0
  both (x ∷ xs) xs⊆P ys⊆P (fs i) = both xs (pull xs⊆P) ys⊆P i

  empty : ◻ P []
  empty ()

  module _ where
    open import Relation.Nullary.Decidable.Logic
    ◻? : (∀ x → Dec (P x)) → ∀ xs → Dec (◻ P xs)
    ◻? P? [] = yes λ ()
    ◻? P? (x ∷ xs) =  ⟦yes uncurry push
                      ,no uncons
                      ⟧ (P? x && ◻? P? xs)

module Forall-NotExists {a} {A : Type a} {p} (P : A → Type p) where
  open import Relation.Nullary.Stable
  open import Data.Empty.Properties

  open Forall P
  ¬P = ¬_ ∘ P
  module ∃¬ = Exists ¬P

  ∀⇒¬∃¬ : ∀ xs → ◻ P xs → ¬ (◇ ¬P xs)
  ∀⇒¬∃¬ (x ∷ xs) xs⊆P (f0 , ∃¬P∈xs) = ∃¬P∈xs(xs⊆P f0)
  ∀⇒¬∃¬ (x ∷ xs) xs⊆P (fs n , ∃¬P∈xs) = ∀⇒¬∃¬ xs (xs⊆P ∘ fs) (n , ∃¬P∈xs)

  module _ (stable : ∀ {x} → Stable (P x)) where
    ¬∃¬⇒∀ : ∀ xs → ¬ (◇ ¬P xs) → ◻ P xs
    ¬∃¬⇒∀ (x ∷ xs) ¬∃¬P∈xs f0 = stable (¬∃¬P∈xs ∘ (f0 ,_))
    ¬∃¬⇒∀ (x ∷ xs) ¬∃¬P∈xs (fs n) = ¬∃¬⇒∀ xs (¬∃¬P∈xs ∘ ∃¬.push) n

    leftInv′ : ∀ (prop : ∀ {x} → isProp (P x)) xs → (x : ◻ P xs) → ¬∃¬⇒∀ xs (∀⇒¬∃¬ xs x) ≡ x
    leftInv′ prop [] x i ()
    leftInv′ prop (x ∷ xs) xs⊆P i f0 = prop (stable λ ¬p → ¬p (xs⊆P f0)) (xs⊆P f0) i
    leftInv′ prop (x ∷ xs) xs⊆P i (fs n) = leftInv′ prop xs (pull xs⊆P) i n

    ∀⇔¬∃¬ : ∀ (prop : ∀ {x} → isProp (P x)) xs → ◻ P xs ⇔ (¬ ◇ ¬P xs)
    ∀⇔¬∃¬ _ xs .fun = ∀⇒¬∃¬ xs
    ∀⇔¬∃¬ _ xs .inv = ¬∃¬⇒∀ xs
    ∀⇔¬∃¬ p xs .leftInv  = leftInv′ p xs
    ∀⇔¬∃¬ _ xs .rightInv x = isProp¬ _ _ x

module Exists-NotForall {a} {A : Type a} {p} (P : A → Type p) where
  open Exists P
  ¬P = ¬_ ∘ P
  module ∀¬ = Forall ¬P

  ∃⇒¬∀¬ : ∀ xs → ◇ P xs → ¬ ◻ ¬P xs
  ∃⇒¬∀¬ (x ∷ xs) (f0  , P∈xs) xs⊆P = xs⊆P f0 P∈xs
  ∃⇒¬∀¬ (x ∷ xs) (fs n , P∈xs) xs⊆P = ∃⇒¬∀¬ xs (n , P∈xs) (xs⊆P ∘ fs)

  module _ (P? : ∀ x → Dec (P x)) where
    ¬∀¬⇒∃ : ∀ xs → ¬ ◻ ¬P xs → ◇ P xs
    ¬∀¬⇒∃ [] ¬xs⊆¬P = ⊥-elim (¬xs⊆¬P λ ())
    ¬∀¬⇒∃ (x ∷ xs) ¬xs⊆¬P with P? x
    ¬∀¬⇒∃ (x ∷ xs) ¬xs⊆¬P | yes p = f0 , p
    ¬∀¬⇒∃ (x ∷ xs) ¬xs⊆¬P | no ¬p = push (¬∀¬⇒∃ xs (¬xs⊆¬P ∘ ∀¬.push ¬p))

module Congruence {p q} (P : A → Type p) (Q : B → Type q)
                  {f : A → B} (f↑ : ∀ {x} → P x → Q (f x)) where
  cong-◇ : ∀ xs → ◇ P xs → ◇ Q (map f xs)
  cong-◇ (x ∷ xs) (f0 , P∈xs) = f0 , f↑ P∈xs
  cong-◇ (x ∷ xs) (fs n , P∈xs) = Exists.push Q (cong-◇ xs (n , P∈xs))

◇-concat : ∀ (P : A → Type p) xs → ◇ (◇ P) xs → ◇ P (concat xs)
◇-concat P (x ∷ xs) (f0 , ps) = Exists._◇++_ P x ps
◇-concat P (x ∷ xs) (fs n , ps) = Exists._++◇_ P x (◇-concat P xs (n , ps))

◻-concat : ∀ (P : A → Type p) xs → ◻ (◻ P) xs → ◻ P (concat xs)
◻-concat P [] xs⊆P ()
◻-concat P (x ∷ xs) xs⊆P = Forall.both P x (xs⊆P f0) (◻-concat P xs (xs⊆P ∘ fs))

module Search {A : Type a} where
  data Result {p} (P : A → Type p) (xs : List A) : Bool → Type (a ℓ⊔ p) where
    all′ : ◻ P xs → Result P xs true
    except′ : ◇ (¬_ ∘ P) xs → Result P xs false

  record Found {p} (P : A → Type p) (xs : List A) : Type (a ℓ⊔ p) where
    field
      found? : Bool
      result : Result P xs found?
  open Found public

  pattern all    ps = record { found? = true ; result = all′ ps }
  pattern except ¬p = record { found? = false ; result = except′ ¬p }

  module _ {p} {P : A → Type p} (P? : ∀ x → Dec (P x)) where
    search : ∀ xs → Found P xs
    search [] = all λ ()
    search (x ∷ xs) = search′ x xs (P? x) (search xs)
      where
      search′ : ∀ x xs → Dec (P x) → Found P xs → Found P (x ∷ xs)
      search′ x xs Px Pxs .found? = Px .does and Pxs .found?
      search′ x xs (no ¬p) Pxs .result = except′ (f0 , ¬p)
      search′ x xs (yes p) (except ¬p) .result = except′ (Exists.push (¬_ ∘ P) ¬p)
      search′ x xs (yes p) (all ps) .result = all′ (Forall.push P p ps)

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Issue332 where

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

syntax id x = id x -- This makes parsing id x ambiguous

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import LogicalFormulae
open import Lists.Lists
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Naturals
open import Numbers.BinaryNaturals.Definition
open import Numbers.BinaryNaturals.Addition
open import Semirings.Definition

module Numbers.BinaryNaturals.Multiplication where

_*Binherit_ : BinNat → BinNat → BinNat
a *Binherit b = NToBinNat (binNatToN a *N binNatToN b)

_*B_ : BinNat → BinNat → BinNat
[] *B b = []
(zero :: a) *B b = zero :: (a *B b)
(one :: a) *B b = (zero :: (a *B b)) +B b

private
  contr : {a : _} {A : Set a} {l1 l2 : List A} → {x : A} → l1 ≡ [] → l1 ≡ x :: l2 → False
  contr {l1 = []} p1 ()
  contr {l1 = x :: l1} () p2

  *BEmpty : (a : BinNat) → canonical (a *B []) ≡ []
  *BEmpty [] = refl
  *BEmpty (zero :: a) rewrite *BEmpty a = refl
  *BEmpty (one :: a) rewrite *BEmpty a = refl

canonicalDistributesPlus : (a b : BinNat) → canonical (a +B b) ≡ canonical a +B canonical b
canonicalDistributesPlus a b = transitivity ans (+BIsInherited (canonical a) (canonical b) (canonicalIdempotent a) (canonicalIdempotent b))
  where
    ans : canonical (a +B b) ≡ NToBinNat (binNatToN (canonical a) +N binNatToN (canonical b))
    ans rewrite binNatToNIsCanonical a | binNatToNIsCanonical b = equalityCommutative (+BIsInherited' a b)

incrPullsOut : (a b : BinNat) → incr (a +B b) ≡ (incr a) +B b
incrPullsOut [] [] = refl
incrPullsOut [] (zero :: b) = refl
incrPullsOut [] (one :: b) = refl
incrPullsOut (zero :: a) [] = refl
incrPullsOut (zero :: a) (zero :: b) = refl
incrPullsOut (zero :: a) (one :: b) = refl
incrPullsOut (one :: a) [] = refl
incrPullsOut (one :: a) (zero :: b) = applyEquality (zero ::_) (incrPullsOut a b)
incrPullsOut (one :: a) (one :: b) = applyEquality (one ::_) (incrPullsOut a b)

timesZero : (a b : BinNat) → canonical a ≡ [] → canonical (a *B b) ≡ []
timesZero [] b pr = refl
timesZero (zero :: a) b pr with inspect (canonical a)
timesZero (zero :: a) b pr | [] with≡ prA rewrite prA | timesZero a b prA = refl
timesZero (zero :: a) b pr | (a1 :: as) with≡ prA rewrite prA = exFalso (nonEmptyNotEmpty pr)

timesZero'' : (a b : BinNat) → canonical (a *B b) ≡ [] → (canonical a ≡ []) || (canonical b ≡ [])
timesZero'' [] b pr = inl refl
timesZero'' (x :: a) [] pr = inr refl
timesZero'' (zero :: as) (zero :: bs) pr with inspect (canonical as)
timesZero'' (zero :: as) (zero :: bs) pr | y with≡ x with inspect (canonical bs)
timesZero'' (zero :: as) (zero :: bs) pr | [] with≡ prAs | y₁ with≡ prBs rewrite prAs = inl refl
timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | [] with≡ prBs rewrite prBs = inr refl
timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (x :: y) with≡ prBs with inspect (canonical (as *B (zero :: bs)))
timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | [] with≡ pr' with timesZero'' as (zero :: bs) pr'
timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | [] with≡ pr' | inl x rewrite prAs | prBs | pr' | x = exFalso (nonEmptyNotEmpty x)
timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | [] with≡ pr' | inr x rewrite prBs | pr' | x = exFalso (nonEmptyNotEmpty x)
timesZero'' (zero :: as) (zero :: bs) pr | (a1 :: a's) with≡ prAs | (b1 :: b's) with≡ prBs | (x :: y) with≡ pr' rewrite prAs | prBs | pr' = exFalso (nonEmptyNotEmpty pr)
timesZero'' (zero :: as) (one :: bs) pr with inspect (canonical as)
timesZero'' (zero :: as) (one :: bs) pr | [] with≡ x rewrite x = inl refl
timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x with inspect (canonical (as *B (one :: bs)))
timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x | [] with≡ pr' with timesZero'' as (one :: bs) pr'
timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x | [] with≡ pr' | inl pr'' rewrite x | pr' | pr'' = exFalso (nonEmptyNotEmpty pr'')
timesZero'' (zero :: as) (one :: bs) pr | (a1 :: a's) with≡ x | (x₁ :: y) with≡ pr' rewrite x | pr' = exFalso (nonEmptyNotEmpty pr)
timesZero'' (one :: as) (zero :: bs) pr with inspect (canonical bs)
timesZero'' (one :: as) (zero :: bs) pr | [] with≡ x rewrite x = inr refl
timesZero'' (one :: as) (zero :: bs) pr | (b1 :: b's) with≡ prB with inspect (canonical ((as *B (zero :: bs)) +B bs))
timesZero'' (one :: as) (zero :: bs) pr | (b1 :: b's) with≡ prB | [] with≡ x rewrite equalityCommutative (+BIsInherited' (as *B (zero :: bs)) bs) = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prB) v))
  where
    t : binNatToN (as *B (zero :: bs)) +N binNatToN bs ≡ 0
    t = transitivity (equalityCommutative (nToN _)) (applyEquality binNatToN x)
    u : (binNatToN (as *B (zero :: bs)) ≡ 0) && (binNatToN bs ≡ 0)
    u = sumZeroImpliesSummandsZero t
    v : canonical bs ≡ []
    v with u
    ... | fst ,, snd = binNatToNZero bs snd
timesZero'' (one :: as) (zero :: bs) pr | (b1 :: b's) with≡ prB | (x₁ :: y) with≡ x rewrite prB | x = exFalso (nonEmptyNotEmpty pr)

lemma : {i : Bit} → (a b : BinNat) → canonical a ≡ canonical b → canonical (i :: a) ≡ canonical (i :: b)
lemma {zero} a b pr with inspect (canonical a)
lemma {zero} a b pr | [] with≡ x rewrite x | equalityCommutative pr = refl
lemma {zero} a b pr | (a1 :: as) with≡ x rewrite x | equalityCommutative pr = refl
lemma {one} a b pr = applyEquality (one ::_) pr

binNatToNDistributesPlus : (a b : BinNat) → binNatToN (a +B b) ≡ binNatToN a +N binNatToN b
binNatToNDistributesPlus a b = transitivity (equalityCommutative (binNatToNIsCanonical (a +B b))) (transitivity (applyEquality binNatToN (equalityCommutative (+BIsInherited' a b))) (nToN (binNatToN a +N binNatToN b)))

+BAssociative : (a b c : BinNat) → canonical (a +B (b +B c)) ≡ canonical ((a +B b) +B c)
+BAssociative a b c rewrite equalityCommutative (+BIsInherited' a (b +B c)) | equalityCommutative (+BIsInherited' (a +B b) c) | binNatToNDistributesPlus a b | binNatToNDistributesPlus b c | equalityCommutative (Semiring.+Associative ℕSemiring (binNatToN a) (binNatToN b) (binNatToN c)) = refl

timesOne : (a b : BinNat) → (canonical b) ≡ (one :: []) → canonical (a *B b) ≡ canonical a
timesOne [] b pr = refl
timesOne (zero :: a) b pr with inspect (canonical (a *B b))
timesOne (zero :: a) b pr | [] with≡ prAB with timesZero'' a b prAB
timesOne (zero :: a) b pr | [] with≡ prAB | inl a=0 rewrite a=0 | prAB = refl
timesOne (zero :: a) b pr | [] with≡ prAB | inr b=0 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr) b=0))
timesOne (zero :: a) b pr | (ab1 :: abs) with≡ prAB with inspect (canonical a)
timesOne (zero :: a) b pr | (ab1 :: abs) with≡ prAB | [] with≡ x = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prAB) (timesZero a b x)))
timesOne (zero :: a) b pr | (ab1 :: abs) with≡ prAB | (x₁ :: y) with≡ x rewrite prAB | x | timesOne a b pr = applyEquality (zero ::_) (transitivity (equalityCommutative prAB) x)
timesOne (one :: a) (zero :: b) pr with canonical b
timesOne (one :: a) (zero :: b) () | []
timesOne (one :: a) (zero :: b) () | x :: bl
timesOne (one :: a) (one :: b) pr rewrite canonicalDistributesPlus (a *B (one :: b)) b | ::Inj pr | +BCommutative (canonical (a *B (one :: b))) [] | timesOne a (one :: b) pr = refl

timesZero' : (a b : BinNat) → canonical b ≡ [] → canonical (a *B b) ≡ []
timesZero' [] b pr = refl
timesZero' (zero :: a) b pr with inspect (canonical (a *B b))
timesZero' (zero :: a) b pr | [] with≡ x rewrite x = refl
timesZero' (zero :: a) b pr | (ab1 :: abs) with≡ prAB rewrite prAB = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prAB) (timesZero' a b pr)))
timesZero' (one :: a) b pr rewrite canonicalDistributesPlus (zero :: (a *B b)) b | pr | +BCommutative (canonical (zero :: (a *B b))) [] = ans
  where
    ans : canonical (zero :: (a *B b)) ≡ []
    ans with inspect (canonical (a *B b))
    ans | [] with≡ x rewrite x = refl
    ans | (x₁ :: y) with≡ x rewrite x = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative x) (timesZero' a b pr)))

canonicalDistributesTimes : (a b : BinNat) → canonical (a *B b) ≡ canonical ((canonical a) *B (canonical b))
canonicalDistributesTimes [] b = refl
canonicalDistributesTimes (zero :: a) b with inspect (canonical a)
canonicalDistributesTimes (zero :: a) b | [] with≡ x rewrite timesZero a b x | x = refl
canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA with inspect (canonical b)
canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | [] with≡ prB rewrite prA | prB = ans
  where
    ans : canonical (zero :: (a *B b)) ≡ canonical (zero :: ((a1 :: as) *B []))
    ans with inspect (canonical ((a1 :: as) *B []))
    ans | [] with≡ x rewrite x | timesZero' a b prB = refl
    ans | (x₁ :: y) with≡ x = exFalso (nonEmptyNotEmpty (equalityCommutative (transitivity (equalityCommutative (timesZero' (a1 :: as) [] refl)) x)))
canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB with inspect (canonical (a *B b))
canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | [] with≡ x with timesZero'' a b x
canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | [] with≡ x | inl a=0 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prA) a=0))
canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | [] with≡ x | inr b=0 = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative prB) b=0))
canonicalDistributesTimes (zero :: a) b | (a1 :: as) with≡ prA | (b1 :: bs) with≡ prB | (ab1 :: abs) with≡ x rewrite prA | prB | x = ans
  where
    ans : zero :: ab1 :: abs ≡ canonical (zero :: ((a1 :: as) *B (b1 :: bs)))
    ans rewrite equalityCommutative prA | equalityCommutative prB | equalityCommutative (canonicalDistributesTimes a b) | x = refl
canonicalDistributesTimes (one :: a) b = transitivity (canonicalDistributesPlus (zero :: (a *B b)) b) (transitivity (transitivity (applyEquality (_+B canonical b) (transitivity (equalityCommutative (canonicalAscends'' (a *B b))) (transitivity (applyEquality (λ i → canonical (zero :: i)) (canonicalDistributesTimes a b)) (canonicalAscends'' (canonical a *B canonical b))))) (applyEquality (λ i → canonical (zero :: (canonical a *B canonical b)) +B i) (canonicalIdempotent b))) (equalityCommutative (canonicalDistributesPlus (zero :: (canonical a *B canonical b)) (canonical b))))

NToBinNatDistributesPlus : (a b : ℕ) → NToBinNat (a +N b) ≡ NToBinNat a +B NToBinNat b
NToBinNatDistributesPlus zero b = refl
NToBinNatDistributesPlus (succ a) b with inspect (NToBinNat a)
... | bl with≡ prA with inspect (NToBinNat (a +N b))
... | q with≡ prAB = transitivity (applyEquality incr (NToBinNatDistributesPlus a b)) (incrPullsOut (NToBinNat a) (NToBinNat b))

timesCommutative : (a b : BinNat) → canonical (a *B b) ≡ canonical (b *B a)
timesCommLemma : (a b : BinNat) → canonical (zero :: (b *B a)) ≡ canonical (b *B (zero :: a))
timesCommLemma a b rewrite timesCommutative b (zero :: a) | equalityCommutative (canonicalAscends'' {zero} (b *B a)) | equalityCommutative (canonicalAscends'' {zero} (a *B b)) | timesCommutative b a = refl

timesCommutative [] b rewrite timesZero' b [] refl = refl
timesCommutative (x :: a) [] rewrite timesZero' (x :: a) [] refl = refl
timesCommutative (zero :: as) (zero :: b) rewrite equalityCommutative (canonicalAscends'' {zero} (as *B (zero :: b))) | timesCommutative as (zero :: b) | canonicalAscends'' {zero} (zero :: b *B as) | equalityCommutative (canonicalAscends'' {zero} (b *B (zero :: as))) | timesCommutative b (zero :: as) | canonicalAscends'' {zero} (zero :: (as *B b)) = ans
  where
    ans : canonical (zero :: zero :: (b *B as)) ≡ canonical (zero :: zero :: (as *B b))
    ans rewrite equalityCommutative (canonicalAscends'' {zero} (zero :: (b *B as))) | equalityCommutative (canonicalAscends'' {zero} (b *B as)) | timesCommutative b as | canonicalAscends'' {zero} (as *B b) | canonicalAscends'' {zero} (zero :: (as *B b)) = refl
timesCommutative (zero :: as) (one :: b) = transitivity (equalityCommutative (canonicalAscends'' (as *B (one :: b)))) (transitivity (applyEquality (λ i → canonical (zero :: i)) (timesCommutative as (one :: b))) (transitivity (applyEquality (λ i → canonical (zero :: i)) ans) (canonicalAscends'' ((b *B (zero :: as)) +B as))))
  where
    ans : canonical ((zero :: (b *B as)) +B as) ≡ canonical ((b *B (zero :: as)) +B as)
    ans rewrite canonicalDistributesPlus (zero :: (b *B as)) as | canonicalDistributesPlus (b *B (zero :: as)) as = applyEquality (_+B canonical as) (timesCommLemma as b)
timesCommutative (one :: as) (zero :: bs) = transitivity (equalityCommutative (canonicalAscends'' ((as *B (zero :: bs)) +B bs))) (transitivity (applyEquality (λ i → canonical (zero :: i)) ans) (canonicalAscends'' (bs *B (one :: as))))
  where
    ans : canonical ((as *B (zero :: bs)) +B bs) ≡ canonical (bs *B (one :: as))
    ans rewrite timesCommutative bs (one :: as) | canonicalDistributesPlus (as *B (zero :: bs)) bs | canonicalDistributesPlus (zero :: (as *B bs)) bs = applyEquality (_+B canonical bs) (equalityCommutative (timesCommLemma bs as))
timesCommutative (one :: as) (one :: bs) = applyEquality (one ::_) (transitivity (canonicalDistributesPlus (as *B (one :: bs)) bs) (transitivity (transitivity (applyEquality (_+B canonical bs) (timesCommutative as (one :: bs))) (transitivity ans (equalityCommutative (applyEquality (_+B canonical as) (timesCommutative bs (one :: as)))))) (equalityCommutative (canonicalDistributesPlus (bs *B (one :: as)) as))))
  where
    ans : canonical ((zero :: (bs *B as)) +B as) +B canonical bs ≡ canonical ((zero :: (as *B bs)) +B bs) +B canonical as
    ans rewrite equalityCommutative (canonicalDistributesPlus ((zero :: (bs *B as)) +B as) bs) | equalityCommutative (canonicalDistributesPlus ((zero :: (as *B bs)) +B bs) as) | equalityCommutative (+BAssociative (zero :: (bs *B as)) as bs) | equalityCommutative (+BAssociative (zero :: (as *B bs)) bs as) | canonicalDistributesPlus (zero :: (bs *B as)) (as +B bs) | canonicalDistributesPlus (zero :: (as *B bs)) (bs +B as) | equalityCommutative (canonicalAscends'' {zero} (bs *B as)) | timesCommutative bs as | canonicalAscends'' {zero} (as *B bs) | +BCommutative as bs = refl

*BIsInherited : (a b : BinNat) → a *Binherit b ≡ canonical (a *B b)
*BIsInherited a b = transitivity (applyEquality NToBinNat t) (transitivity (binToBin (canonical (a *B b))) (equalityCommutative (canonicalIdempotent (a *B b))))
  where
    ans : (a b : BinNat) → binNatToN a *N binNatToN b ≡ binNatToN (a *B b)
    ans [] b = refl
    ans (zero :: a) b rewrite equalityCommutative (ans a b) = equalityCommutative (Semiring.*Associative ℕSemiring 2 (binNatToN a) (binNatToN b))
    ans (one :: a) b rewrite binNatToNDistributesPlus (zero :: (a *B b)) b | Semiring.commutative ℕSemiring (binNatToN b) ((2 *N (binNatToN a)) *N (binNatToN b)) | equalityCommutative (ans a b) = applyEquality (_+N binNatToN b) (equalityCommutative (Semiring.*Associative ℕSemiring 2 (binNatToN a) (binNatToN b)))
    t : (binNatToN a *N binNatToN b) ≡ binNatToN (canonical (a *B b))
    t = transitivity (ans a b) (equalityCommutative (binNatToNIsCanonical (a *B b)))


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

open import LogicalFormulae
open import Lists.Lists
open import Numbers.BinaryNaturals.Definition
open import Maybe

module Numbers.BinaryNaturals.SubtractionGo where

go : Bit → BinNat → BinNat → Maybe BinNat
go zero [] [] = yes []
go one [] [] = no
go zero [] (zero :: b) = go zero [] b
go zero [] (one :: b) = no
go one [] (x :: b) = no
go zero (zero :: a) [] = yes (zero :: a)
go one (zero :: a) [] = mapMaybe (one ::_) (go one a [])
go zero (zero :: a) (zero :: b) = mapMaybe (zero ::_) (go zero a b)
go one (zero :: a) (zero :: b) = mapMaybe (one ::_) (go one a b)
go zero (zero :: a) (one :: b) = mapMaybe (one ::_) (go one a b)
go one (zero :: a) (one :: b) = mapMaybe (zero ::_) (go one a b)
go zero (one :: a) [] = yes (one :: a)
go zero (one :: a) (zero :: b) = mapMaybe (one ::_) (go zero a b)
go zero (one :: a) (one :: b) = mapMaybe (zero ::_) (go zero a b)
go one (one :: a) [] = yes (zero :: a)
go one (one :: a) (zero :: b) = mapMaybe (zero ::_) (go zero a b)
go one (one :: a) (one :: b) = mapMaybe (one ::_) (go one a b)

_-B_ : BinNat → BinNat → Maybe BinNat
a -B b = go zero a b

goEmpty : (a : BinNat) → go zero a [] ≡ yes a
goEmpty [] = refl
goEmpty (zero :: a) = refl
goEmpty (one :: a) = refl

goOneSelf : (a : BinNat) → go one a a ≡ no
goOneSelf [] = refl
goOneSelf (zero :: a) rewrite goOneSelf a = refl
goOneSelf (one :: a) rewrite goOneSelf a = refl

goOneEmpty : (b : BinNat) {t : BinNat} → go one [] b ≡ yes t → False
goOneEmpty [] {t} ()
goOneEmpty (x :: b) {t} ()

goOneEmpty' : (b : BinNat) → go one [] b ≡ no
goOneEmpty' b with inspect (go one [] b)
goOneEmpty' b | no with≡ x = x
goOneEmpty' b | yes x₁ with≡ x = exFalso (goOneEmpty b x)

goZeroEmpty : (b : BinNat) {t : BinNat} → go zero [] b ≡ yes t → canonical b ≡ []
goZeroEmpty [] {t} = λ _ → refl
goZeroEmpty (zero :: b) {t} pr with inspect (canonical b)
goZeroEmpty (zero :: b) {t} pr | [] with≡ pr2 rewrite pr2 = refl
goZeroEmpty (zero :: b) {t} pr | (x :: r) with≡ pr2 with goZeroEmpty b pr
... | u = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr2) u))

goZeroEmpty' : (b : BinNat) {t : BinNat} → go zero [] b ≡ yes t → canonical t ≡ []
goZeroEmpty' [] {[]} pr = refl
goZeroEmpty' (x :: b) {[]} pr = refl
goZeroEmpty' (zero :: b) {x₁ :: t} pr = goZeroEmpty' b pr

goZeroIncr : (b : BinNat) → go zero [] (incr b) ≡ no
goZeroIncr [] = refl
goZeroIncr (zero :: b) = refl
goZeroIncr (one :: b) = goZeroIncr b

goPreservesCanonicalRightEmpty : (b : BinNat) → go zero [] (canonical b) ≡ go zero [] b
goPreservesCanonicalRightEmpty [] = refl
goPreservesCanonicalRightEmpty (zero :: b) with inspect (canonical b)
goPreservesCanonicalRightEmpty (zero :: b) | [] with≡ x with goPreservesCanonicalRightEmpty b
... | pr2 rewrite x = pr2
goPreservesCanonicalRightEmpty (zero :: b) | (x₁ :: y) with≡ x with goPreservesCanonicalRightEmpty b
... | pr2 rewrite x = pr2
goPreservesCanonicalRightEmpty (one :: b) = refl

goZero : (b : BinNat) {t : BinNat} → mapMaybe canonical (go zero [] b) ≡ yes t → t ≡ []
goZero b {[]} pr = refl
goZero b {x :: t} pr with inspect (go zero [] b)
goZero b {x :: t} pr | no with≡ pr2 rewrite pr2 = exFalso (noNotYes pr)
goZero b {x :: t} pr | yes x₁ with≡ pr2 with goZeroEmpty b pr2
... | u with applyEquality (mapMaybe canonical) (goPreservesCanonicalRightEmpty b)
... | bl rewrite u | pr = exFalso (nonEmptyNotEmpty (equalityCommutative (yesInjective bl)))


text:
-- Agda program using the Iowa Agda library

open import bool

module PROOF-sortPreservesLength
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
  where

open import eq
open import nat
open import list
open import maybe

---------------------------------------------------------------------------
-- Translated Curry operations:

insert : ℕ → 𝕃 ℕ → 𝕃 ℕ
insert x [] = x :: []
insert y (z :: u) = if y ≤ z then y :: (z :: u) else z :: (insert y u)

sort : 𝕃 ℕ → 𝕃 ℕ
sort [] = []
sort (x :: y) = insert x (sort y)

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

insertIncLength : (x : ℕ) → (xs : 𝕃 ℕ)
                → length (insert x xs) ≡ suc (length xs)
insertIncLength x [] = refl
insertIncLength x (y :: ys) with (x ≤ y)
... | tt = refl
... | ff rewrite insertIncLength x ys = refl

sortPreservesLength : (xs : 𝕃 ℕ) → length (sort xs) ≡ length xs
sortPreservesLength [] = refl
sortPreservesLength (x :: xs)
 rewrite insertIncLength x (sort xs) | sortPreservesLength xs = refl

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

max_stars_repo_name: phlummox/curry-tools

max_issues_repo_name: phlummox/curry-tools

max_forks_repo_name: phlummox/curry-tools


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

module Cubical.Algebra.Group.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Group.Base

private
  variable
    ℓ ℓ' ℓ'' : Level

module GroupLemmas (G : Group {ℓ}) where
  open Group G public
  abstract
    simplL : (a : Carrier) {b c : Carrier} → a + b ≡ a + c → b ≡ c
    simplL a {b} {c} p =
      b
        ≡⟨ sym (lid b) ∙ cong (_+ b) (sym (invl a)) ∙ sym (assoc _ _ _) ⟩
      - a + (a + b)
        ≡⟨ cong (- a +_) p ⟩
      - a + (a + c)
        ≡⟨ assoc _ _ _ ∙ cong (_+ c) (invl a) ∙ lid c ⟩
      c ∎

    simplR : {a b : Carrier} (c : Carrier) → a + c ≡ b + c → a ≡ b
    simplR {a} {b} c p =
      a
        ≡⟨ sym (rid a) ∙ cong (a +_) (sym (invr c)) ∙ assoc _ _ _ ⟩
      (a + c) - c
        ≡⟨ cong (_- c) p ⟩
      (b + c) - c
        ≡⟨ sym (assoc _ _ _) ∙ cong (b +_) (invr c) ∙ rid b ⟩
      b ∎

    invInvo : (a : Carrier) → - (- a) ≡ a
    invInvo a = simplL (- a) (invr (- a) ∙ sym (invl a))

    invId : - 0g ≡ 0g
    invId = simplL 0g (invr 0g ∙ sym (lid 0g))

    idUniqueL : {e : Carrier} (x : Carrier) → e + x ≡ x → e ≡ 0g
    idUniqueL {e} x p = simplR x (p ∙ sym (lid _))

    idUniqueR : (x : Carrier) {e : Carrier} → x + e ≡ x → e ≡ 0g
    idUniqueR x {e} p = simplL x (p ∙ sym (rid _))

    invUniqueL : {g h : Carrier} → g + h ≡ 0g → g ≡ - h
    invUniqueL {g} {h} p = simplR h (p ∙ sym (invl h))

    invUniqueR : {g h : Carrier} → g + h ≡ 0g → h ≡ - g
    invUniqueR {g} {h} p = simplL g (p ∙ sym (invr g))

    invDistr : (a b : Carrier) → - (a + b) ≡ - b - a
    invDistr a b = sym (invUniqueR γ) where
      γ : (a + b) + (- b - a) ≡ 0g
      γ = (a + b) + (- b - a)
            ≡⟨ sym (assoc _ _ _) ⟩
          a + b + (- b) + (- a)
            ≡⟨ cong (a +_) (assoc _ _ _ ∙ cong (_+ (- a)) (invr b)) ⟩
          a + (0g - a)
            ≡⟨ cong (a +_) (lid (- a)) ∙ invr a ⟩
          0g ∎

isPropIsGroup : {G : Type ℓ} (0g : G) (_+_ : G → G → G) (-_ : G → G)
             → isProp (IsGroup 0g _+_ -_)
IsGroup.isMonoid (isPropIsGroup 0g _+_ -_ g1 g2 i) = isPropIsMonoid _ _ (IsGroup.isMonoid g1) (IsGroup.isMonoid g2) i
IsGroup.inverse (isPropIsGroup 0g _+_ -_ g1 g2 i) = isPropInv (IsGroup.inverse g1) (IsGroup.inverse g2) i
  where
  isSetG : isSet _
  isSetG = IsSemigroup.is-set (IsMonoid.isSemigroup (IsGroup.isMonoid g1))

  isPropInv : isProp ((x : _) → ((x + (- x)) ≡ 0g) × (((- x) + x) ≡ 0g))
  isPropInv = isPropΠ λ _ → isProp× (isSetG _ _) (isSetG _ _)

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
open import Data.Nat.Base
open import Relation.Binary.PropositionalEquality

open ≡-Reasoning

test : 0 ≡ 0
test = begin
  0 ≡⟨ {!!} ⟩
  0
  ∎

-- WAS: Goal is garbled:
--
-- ?0 : (.Relation.Binary.Setoid.preorder (setoid ℕ)
--  .Relation.Binary.Preorder.∼ 0)
-- 0

-- EXPECTED: Nice goal:
--
-- ?0 : 0 ≡ 0


text:
{-# OPTIONS --type-in-type #-}
-- {-# OPTIONS --guardedness-preserving-type-constructors #-}

module PatternSynonymsErrorLocation where

data _≡_ {A : Set}(a : A) : A -> Set where
  refl : a ≡ a

infixr 2 _,_

record Unit : Set where

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

-- Prod does not communicate guardedness
Prod : (A B : Set) -> Set
Prod A B = Sigma A \ _ -> B

data Empty : Set where

data ListTag : Set where nil cons : ListTag

{-# TERMINATING #-}
List : (A : Set) -> Set
List A = Sigma ListTag T where
  T : ListTag -> Set
  T nil  = Unit
  T cons = Sigma A \ _ -> List A

infix 5 _∷_

pattern []       = nil , _
pattern _∷_ x xs = cons , x , xs
-- FAILS: pattern x ∷ xs = cons , x , xs

data TyTag : Set where base arr : TyTag

{-# TERMINATING #-}
Ty : Set
Ty = Sigma TyTag T where
  T : TyTag -> Set
  T base = Unit
  T arr  = Sigma Ty \ _ -> Ty  -- Prod Ty Ty

infix 10 _⇒_

pattern ★       = base , _
pattern _⇒_ A B = arr , A , B

Context = List Ty

data NatTag : Set where zero succ : NatTag

Var : (Gamma : Context)(C : Ty) -> Set
Var []           C = Empty
Var (cons , A , Gamma) C =  Sigma NatTag T
  where T : NatTag -> Set
        T zero = A ≡ C
        T succ = Var Gamma C

pattern vz   = zero , refl
pattern vs x = succ , x

idVar : (Gamma : Context)(C : Ty)(x : Var Gamma C) -> Var Gamma C
idVar [] _ ()
-- CORRECT: idVar (A ∷ Gamma) C (zero , proof) = zero , proof
idVar (A ∷ Gamma) C vz         = vz
idVar (A ∷ Gamma) C (vs x)     = vs (idVar Gamma C x)


text:
record Unit : Set where
data Bool : Set where true false : Bool

F : Bool -> Set
F true  = Bool
F false = Unit

f : (b : Bool) -> F b
f true  = true
f false = record {}

-- this should give an error, but only gives yellow
test : Bool
test = f _ false


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

module Cubical.Algebra.Group.Morphism where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Algebra.Group.Base
open import Cubical.HITs.PropositionalTruncation hiding (map)
open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' : Level

-- The following definition of GroupHom and GroupEquiv are level-wise heterogeneous.
-- This allows for example to deduce that G ≡ F from a chain of isomorphisms
-- G ≃ H ≃ F, even if H does not lie in the same level as G and F.

isGroupHom : (G : Group {ℓ}) (H : Group {ℓ'}) (f : ⟨ G ⟩ → ⟨ H ⟩) → Type _
isGroupHom G H f = (x y : ⟨ G ⟩) → f (x G.+ y) ≡ (f x H.+ f y) where
  module G = Group G
  module H = Group H

record GroupHom (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  constructor grouphom
  no-eta-equality
  field
    fun : ⟨ G ⟩ → ⟨ H ⟩
    isHom : isGroupHom G H fun

record GroupEquiv (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  constructor groupequiv
  no-eta-equality
  field
    eq : ⟨ G ⟩ ≃ ⟨ H ⟩
    isHom : isGroupHom G H (equivFun eq)

  hom : GroupHom G H
  hom = grouphom (equivFun eq) isHom

open GroupHom
open GroupEquiv

η-hom : {G : Group {ℓ}} {H : Group {ℓ'}} → (a  : GroupHom G H)
      → grouphom (fun a) (isHom a) ≡ a
fun (η-hom a i) = fun a
isHom (η-hom a i) = isHom a

η-equiv : {G : Group {ℓ}} {H : Group {ℓ'}} → (a  : GroupEquiv G H)
       → groupequiv (eq a) (isHom a) ≡ a
eq (η-equiv a i) = eq a
isHom (η-equiv a i) = isHom a

×hom : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Group {ℓ}} {B : Group {ℓ'}} {C : Group {ℓ''}} {D : Group {ℓ'''}}
    → GroupHom A C → GroupHom B D → GroupHom (dirProd A B) (dirProd C D)
fun (×hom mf1 mf2) = map-× (fun mf1) (fun mf2)
isHom (×hom mf1 mf2) a b = ≡-× (isHom mf1 _ _) (isHom mf2 _ _)

open Group

isInIm : ∀ {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) → (GroupHom G H)
       → ⟨ H ⟩ → Type (ℓ-max ℓ ℓ')
isInIm G H ϕ h = ∃[ g ∈ ⟨ G ⟩ ] (fun ϕ) g ≡ h

isInKer : ∀ {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) → (GroupHom G H)
       → ⟨ G ⟩ → Type ℓ'
isInKer G H ϕ g = (fun ϕ) g ≡ 0g H

isSurjective : ∀ {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) → GroupHom G H → Type (ℓ-max ℓ ℓ')
isSurjective G H ϕ = (x : ⟨ H ⟩) → isInIm G H ϕ x

isInjective : ∀ {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) → GroupHom G H → Type (ℓ-max ℓ ℓ')
isInjective G H ϕ = (x : ⟨ G ⟩) → isInKer G H ϕ x → x ≡ 0g G


text:
-- Andreas, 2019-03-28, issue #3248, reported by guillaumebrunerie

{-# OPTIONS --sized-types --show-implicit #-}

-- {-# OPTIONS -v tc:10 #-}
-- {-# OPTIONS -v tc.term:20 #-}
-- {-# OPTIONS -v tc.conv.size:45 #-}
-- {-# OPTIONS -v tc.conv.coerce:45 #-}
-- {-# OPTIONS -v tc.term.args.target:45 #-}

{-# BUILTIN SIZEUNIV SizeUniv #-}  --  SizeUniv : SizeUniv
{-# BUILTIN SIZE     Size     #-}  --  Size     : SizeUniv
{-# BUILTIN SIZELT   Size<_   #-}  --  Size<_   : ..Size → SizeUniv
{-# BUILTIN SIZESUC  ↑_       #-}  --  ↑_       : Size → Size
{-# BUILTIN SIZEINF  ∞        #-}  --  ∞        : Size
{-# BUILTIN SIZEMAX  _⊔ˢ_     #-}  --  _⊔ˢ_     : Size → Size → Size

data D (i : Size) : Set where
  c : {j : Size< i} → D j → D i

f : {i : Size} → D i → D i → D i
f  (c {j₁} l1)
   (c {j₂} l2) = c {j = j₁ ⊔ˢ j₂} (f {j₁ ⊔ˢ j₂} l1 l2)

-- The problem was that the new "check target first" logic
-- e49d1ca276e5adbf2eb9f6cd33926b786cef78f7
-- for checking applications does not work for Size<.
--
--   Checking target types first
--     inferred = Size
--     expected = Size< i
--
-- It is not the case that Size <= Size< i, however, coerce succeeds,
-- since e.g. j : Size <= Size< i  if  j : Size< i.
--
-- The solution is to switch off the check target first logic
-- if the target type of a (possibly empty) application is Size< _.


text:
open import Formalization.PredicateLogic.Signature

module Formalization.PredicateLogic.Classical.Semantics (𝔏 : Signature) {ℓₘ} where
open Signature(𝔏)

import      Lvl
open import Data.Boolean
open import Data.ListSized
open import Numeral.Natural
open import Type

private variable args : ℕ

-- Model.
-- A model decides which propositional constants that are true or false.
-- A model in a signature `s` consists of a domain and interpretations of the function/relation symbols in `s`.
-- Also called: Structure.
-- Note: A model satisfying `∀{args} → Empty(Prop args)` is called an "Algebraic structure".
record Model : Type{ℓₚ Lvl.⊔ ℓₒ Lvl.⊔ Lvl.𝐒(ℓₘ)} where
  field
    Domain : Type{ℓₘ}                                  -- The type of objects that quantifications quantifies over and functions/relations maps from.
    function : Obj(args) → List(Domain)(args) → Domain -- Maps Obj to a n-ary function (n=0 is interpreted as a constant).
    relation : Prop(args) → List(Domain)(args) → Bool  -- Maps Prop to a boolean n-ary relation (n=0 is interpreted as a proposition).

open Model public using() renaming (Domain to dom ; function to fn ; relation to rel)