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

open import Categories.Category using (Category)
open import Categories.Category.Monoidal using (Monoidal)

module Categories.Category.Monoidal.Reasoning {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open import Data.Product using (_,_)

open import Categories.Functor using (Functor)

open Category C

private
  variable
    X Y : Obj
    f g h i : X ⇒ Y

open Monoidal M using (_⊗₀_; _⊗₁_; ⊗)
open Functor ⊗ using (F-resp-≈; homomorphism)
open HomReasoning public

infixr 6 _⟩⊗⟨_ refl⟩⊗⟨_
infixl 7 _⟩⊗⟨refl

⊗-resp-≈ : f ≈ h → g ≈ i → (f ⊗₁ g) ≈ (h ⊗₁ i)
⊗-resp-≈ p q = F-resp-≈ (p , q)

⊗-resp-≈ˡ : f ≈ h → (f ⊗₁ g) ≈ (h ⊗₁ g)
⊗-resp-≈ˡ p = ⊗-resp-≈ p Equiv.refl

⊗-resp-≈ʳ : g ≈ i → (f ⊗₁ g) ≈ (f ⊗₁ i)
⊗-resp-≈ʳ p = ⊗-resp-≈ Equiv.refl p

_⟩⊗⟨_ : f ≈ h → g ≈ i → (f ⊗₁ g) ≈ (h ⊗₁ i)
_⟩⊗⟨_ = ⊗-resp-≈

refl⟩⊗⟨_ : g ≈ i → (f ⊗₁ g) ≈ (f ⊗₁ i)
refl⟩⊗⟨_ = ⊗-resp-≈ʳ

_⟩⊗⟨refl : f ≈ h → (f ⊗₁ g) ≈ (h ⊗₁ g)
_⟩⊗⟨refl = ⊗-resp-≈ˡ

-- This corresponds to the graphical coherence property of diagrams
-- modelling monoidal categories:
--
--   |        |         |   |
--  [h]      [i]       [h] [i]
--   |        |    ≈    |   |
--  [f]      [g]        |   |
--   |        |         |   |
--                     [f] [g]
--                      |   |

⊗-distrib-over-∘ : ((f ∘ h) ⊗₁ (g ∘ i)) ≈ ((f ⊗₁ g) ∘ (h ⊗₁ i))
⊗-distrib-over-∘ = homomorphism

-- Parallel commutation

parallel : ∀ {X₁ X₂ Y₁ Y₂ Z₁ Z₂ W₁ W₂}
           {f₁ : Y₁ ⇒ W₁} {f₂ : Z₁ ⇒ W₁} {g₁ : Y₂ ⇒ W₂} {g₂ : Z₂ ⇒ W₂}
           {h₁ : X₁ ⇒ Y₁} {h₂ : X₁ ⇒ Z₁} {i₁ : X₂ ⇒ Y₂} {i₂ : X₂ ⇒ Z₂} →
           f₁ ∘ h₁ ≈ f₂ ∘ h₂ → g₁ ∘ i₁ ≈ g₂ ∘ i₂ →
           f₁ ⊗₁ g₁ ∘ h₁ ⊗₁ i₁ ≈ f₂ ⊗₁ g₂ ∘ h₂ ⊗₁ i₂
parallel {f₁ = f₁} {f₂} {g₁} {g₂} {h₁} {h₂} {i₁} {i₂} hyp₁ hyp₂ = begin
  f₁ ⊗₁ g₁ ∘ h₁ ⊗₁ i₁      ≈˘⟨ ⊗-distrib-over-∘ ⟩
  (f₁ ∘ h₁) ⊗₁ (g₁ ∘ i₁)   ≈⟨ hyp₁ ⟩⊗⟨ hyp₂ ⟩
  (f₂ ∘ h₂) ⊗₁ (g₂ ∘ i₂)   ≈⟨ ⊗-distrib-over-∘ ⟩
  f₂ ⊗₁ g₂ ∘ h₂ ⊗₁ i₂      ∎

-- Parallel-to-serial conversions
--
--   |   |        |   |       |   |
--   |   |        |  [g]     [f]  |
--  [f] [g]   =   |   |   =   |   |
--   |   |       [f]  |       |  [g]
--   |   |        |   |       |   |

serialize₁₂ : ∀ {X₁ Y₁ X₂ Y₂} {f : X₁ ⇒ Y₁} {g : X₂ ⇒ Y₂} →
              f ⊗₁ g ≈ f ⊗₁ id ∘ id ⊗₁ g
serialize₁₂ {f = f} {g} = begin
  f ⊗₁ g                 ≈˘⟨ identityʳ ⟩⊗⟨ identityˡ ⟩
  (f ∘ id) ⊗₁ (id ∘ g)   ≈⟨ ⊗-distrib-over-∘ ⟩
  f ⊗₁ id ∘ id ⊗₁ g      ∎

serialize₂₁ : ∀ {X₁ Y₁ X₂ Y₂} {f : X₁ ⇒ Y₁} {g : X₂ ⇒ Y₂} →
              f ⊗₁ g ≈ id ⊗₁ g ∘ f ⊗₁ id
serialize₂₁ {f = f} {g} = begin
  f ⊗₁ g                 ≈˘⟨ identityˡ ⟩⊗⟨ identityʳ ⟩
  (id ∘ f) ⊗₁ (g ∘ id)   ≈⟨ ⊗-distrib-over-∘ ⟩
  id ⊗₁ g ∘ f ⊗₁ id      ∎

-- Split a composite in the first component
--
--   |   |        |   |       |   |
--  [g]  |       [g]  |      [g] [h]
--   |  [h]   =   |   |   =   |   |
--  [f]  |       [f] [h]     [f]  |
--   |   |        |   |       |   |

split₁ʳ : ∀ {X₁ Y₁ Z₁ X₂ Y₂} {f : Y₁ ⇒ Z₁} {g : X₁ ⇒ Y₁} {h : X₂ ⇒ Y₂} →
          (f ∘ g) ⊗₁ h ≈ f ⊗₁ h ∘ g ⊗₁ id
split₁ʳ {f = f} {g} {h} = begin
  (f ∘ g) ⊗₁ h          ≈˘⟨ refl⟩⊗⟨ identityʳ ⟩
  (f ∘ g) ⊗₁ (h ∘ id)   ≈⟨ ⊗-distrib-over-∘ ⟩
  f ⊗₁ h ∘ g ⊗₁ id      ∎

split₁ˡ : ∀ {X₁ Y₁ Z₁ X₂ Y₂} {f : Y₁ ⇒ Z₁} {g : X₁ ⇒ Y₁} {h : X₂ ⇒ Y₂} →
          (f ∘ g) ⊗₁ h ≈ f ⊗₁ id ∘ g ⊗₁ h
split₁ˡ {f = f} {g} {h} = begin
  (f ∘ g) ⊗₁ h          ≈˘⟨ refl⟩⊗⟨ identityˡ ⟩
  (f ∘ g) ⊗₁ (id ∘ h)   ≈⟨ ⊗-distrib-over-∘ ⟩
  f ⊗₁ id ∘ g ⊗₁ h      ∎

-- Split a composite in the second component
--
--   |   |        |   |       |   |
--   |  [h]       |  [h]     [f] [h]
--  [f]  |    =   |   |   =   |   |
--   |  [g]      [f] [g]      |  [g]
--   |   |        |   |       |   |

split₂ʳ : ∀ {X₁ Y₁ X₂ Y₂ Z₂} {f : X₁ ⇒ Y₁} {g : Y₂ ⇒ Z₂} {h : X₂ ⇒ Y₂} →
          f ⊗₁ (g ∘ h) ≈ f ⊗₁ g ∘ id ⊗₁ h
split₂ʳ {f = f} {g} {h} = begin
  f ⊗₁ (g ∘ h)          ≈˘⟨ identityʳ ⟩⊗⟨refl ⟩
  (f ∘ id) ⊗₁ (g ∘ h)   ≈⟨ ⊗-distrib-over-∘ ⟩
  f ⊗₁ g ∘ id ⊗₁ h      ∎

split₂ˡ : ∀ {X₁ Y₁ X₂ Y₂ Z₂} {f : X₁ ⇒ Y₁} {g : Y₂ ⇒ Z₂} {h : X₂ ⇒ Y₂} →
          f ⊗₁ (g ∘ h) ≈ id ⊗₁ g ∘ f ⊗₁ h
split₂ˡ {f = f} {g} {h} = begin
  f ⊗₁ (g ∘ h)          ≈˘⟨ identityˡ ⟩⊗⟨refl ⟩
  (id ∘ f) ⊗₁ (g ∘ h)   ≈⟨ ⊗-distrib-over-∘ ⟩
  id ⊗₁ g ∘ f ⊗₁ h      ∎

-- Combined splitting and re-association.

module _ {X Y Z} {f : X ⇒ Z} {g : Y ⇒ Z} {h : X ⇒ Y} (f≈gh : f ≈ g ∘ h) where

  infixr 4 split₁_⟩∘⟨_ split₂_⟩∘⟨_
  infixl 5 _⟩∘⟨split₁_ _⟩∘⟨split₂_

  split₁_⟩∘⟨_ : ∀ {V W} {i j : V ⇒ X ⊗₀ W} → i ≈ j →
                f ⊗₁ id ∘ i ≈ g ⊗₁ id ∘ h ⊗₁ id ∘ j
  split₁_⟩∘⟨_ {_} {_} {i} {j} i≈j = begin
    f ⊗₁ id ∘ i                ≈⟨ f≈gh ⟩⊗⟨refl ⟩∘⟨ i≈j ⟩
    (g ∘ h) ⊗₁ id ∘ j          ≈⟨ split₁ˡ ⟩∘⟨refl ⟩
    (g ⊗₁ id ∘ h ⊗₁ id) ∘ j    ≈⟨ assoc ⟩
    g ⊗₁ id ∘ (h ⊗₁ id ∘ j)    ∎

  split₂_⟩∘⟨_ : ∀ {V W} {i j : V ⇒ W ⊗₀ X} → i ≈ j →
                id ⊗₁ f ∘ i ≈ id ⊗₁ g ∘ id ⊗₁ h ∘ j
  split₂_⟩∘⟨_ {_} {_} {i} {j} i≈j = begin
    id ⊗₁ f ∘ i                ≈⟨ refl⟩⊗⟨ f≈gh ⟩∘⟨ i≈j ⟩
    id ⊗₁ (g ∘ h) ∘ j          ≈⟨ split₂ˡ ⟩∘⟨refl ⟩
    (id ⊗₁ g ∘ id ⊗₁ h) ∘ j    ≈⟨ assoc ⟩
    id ⊗₁ g ∘ (id ⊗₁ h ∘ j)    ∎

  _⟩∘⟨split₁_ : ∀ {V W} {i j : Z ⊗₀ W ⇒ V} → i ≈ j →
                i ∘ f ⊗₁ id ≈ (j ∘ g ⊗₁ id) ∘ h ⊗₁ id
  _⟩∘⟨split₁_ {_} {_} {i} {j} i≈j = begin
    i ∘ f ⊗₁ id                ≈⟨ i≈j ⟩∘⟨ f≈gh ⟩⊗⟨refl ⟩
    j ∘ (g ∘ h) ⊗₁ id          ≈⟨ refl⟩∘⟨ split₁ˡ ⟩
    j ∘ (g ⊗₁ id ∘ h ⊗₁ id)    ≈⟨ sym-assoc ⟩
    (j ∘ g ⊗₁ id) ∘ h ⊗₁ id    ∎

  _⟩∘⟨split₂_ : ∀ {V W} {i j : W ⊗₀ Z ⇒ V} → i ≈ j →
                i ∘ id ⊗₁ f ≈ (j ∘ id ⊗₁ g) ∘ id ⊗₁ h
  _⟩∘⟨split₂_ {_} {_} {i} {j} i≈j = begin
    i ∘ id ⊗₁ f                ≈⟨ i≈j ⟩∘⟨ refl⟩⊗⟨ f≈gh ⟩
    j ∘ id ⊗₁ (g ∘ h)          ≈⟨ refl⟩∘⟨ split₂ˡ ⟩
    j ∘ (id ⊗₁ g ∘ id ⊗₁ h)    ≈⟨ sym-assoc ⟩
    (j ∘ id ⊗₁ g) ∘ id ⊗₁ h    ∎

-- Combined merging and re-association.

module _ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} {h : X ⇒ Z} (fg≈h : f ∘ g ≈ h) where

  infixr 4 merge₁_⟩∘⟨_ merge₂_⟩∘⟨_
  infixl 5 _⟩∘⟨merge₁_ _⟩∘⟨merge₂_

  merge₁_⟩∘⟨_ : ∀ {V W} {i j : V ⇒ X ⊗₀ W} → i ≈ j →
                f ⊗₁ id ∘ g ⊗₁ id ∘ i ≈ h ⊗₁ id ∘ j
  merge₁_⟩∘⟨_ i≈j = ⟺ (split₁ ⟺ fg≈h ⟩∘⟨ ⟺ i≈j)

  merge₂_⟩∘⟨_ : ∀ {V W} {i j : V ⇒ W ⊗₀ X} → i ≈ j →
                id ⊗₁ f ∘ id ⊗₁ g ∘ i ≈ id ⊗₁ h ∘ j
  merge₂_⟩∘⟨_ i≈j = ⟺ (split₂ ⟺ fg≈h ⟩∘⟨ ⟺ i≈j)

  _⟩∘⟨merge₁_ : ∀ {V W} {i j : Z ⊗₀ W ⇒ V} → i ≈ j →
                (i ∘ f ⊗₁ id) ∘ g ⊗₁ id ≈ j ∘ h ⊗₁ id
  _⟩∘⟨merge₁_ i≈j = ⟺ (⟺ fg≈h ⟩∘⟨split₁ ⟺ i≈j)

  _⟩∘⟨merge₂_ : ∀ {V W} {i j : W ⊗₀ Z ⇒ V} → i ≈ j →
                (i ∘ id ⊗₁ f) ∘ id ⊗₁ g ≈ j ∘ id ⊗₁ h
  _⟩∘⟨merge₂_ i≈j = ⟺ (⟺ fg≈h ⟩∘⟨split₂ ⟺ i≈j)

ext: agda

max_stars_repo_name: TOTBWF/agda-categories

max_issues_repo_name: TOTBWF/agda-categories

max_forks_repo_name: TOTBWF/agda-categories


text:
module Issue254 where

data Unit : Set where
  * : Unit

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

data Vec : Nat → Set where
  cons : ∀ n → Vec (suc n)

remove : ∀ n → Nat → Vec (suc n) → Unit
remove n x (cons .n) with *
remove n x (cons .n) | * = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-

This file contains:

- Definition of functions of the equivalence between FreeGroup and the FundamentalGroup
- Definition of encode decode functions
- Proof that for all x : Bouquet A → p : base ≡ x → decode x (encode x p) ≡ p (no truncations)
- Proof of the truncated versions of encodeDecode and of right-homotopy
- Definition of truncated encode decode functions
- Proof of the truncated versions of decodeEncode and encodeDecode
- Proof that π₁Bouquet ≡ FreeGroup A

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

module Cubical.HITs.Bouquet.FundamentalGroupProof where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws renaming (assoc to pathAssoc)
open import Cubical.HITs.SetTruncation hiding (rec2)
open import Cubical.HITs.PropositionalTruncation hiding (map ; elim) renaming (rec to propRec)
open import Cubical.Algebra.Group
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.Loopspace

open import Cubical.HITs.Bouquet.Base
open import Cubical.HITs.FreeGroup.Base
open import Cubical.HITs.FreeGroupoid

private
  variable
    ℓ : Level
    A : Type ℓ

-- Pointed versions of the non truncated types

ΩBouquet : {A : Type ℓ} → Pointed ℓ
ΩBouquet {A = A} = Ω (Bouquet∙ A)

FreeGroupoid∙ : {A : Type ℓ} → Pointed ℓ
FreeGroupoid∙ {A = A} = FreeGroupoid A , ε

-- Functions without using the truncated forms of types

looping : FreeGroupoid A → typ ΩBouquet
looping (η a)              = loop a
looping (g1 · g2)          = looping g1 ∙ looping g2
looping ε                  = refl
looping (inv g)            = sym (looping g)
looping (assoc g1 g2 g3 i) = pathAssoc (looping g1) (looping g2) (looping g3) i
looping (idr g i)          = rUnit (looping g) i
looping (idl g i)          = lUnit (looping g) i
looping (invr g i)         = rCancel (looping g) i
looping (invl g i)         = lCancel (looping g) i

looping∙ : FreeGroupoid∙ →∙ ΩBouquet {A = A}
looping∙ = looping , refl

code : {A : Type ℓ} → (Bouquet A) → Type ℓ
code {A = A} base = (FreeGroupoid A)
code (loop a i)   = pathsInU (η a) i

winding : typ ΩBouquet → FreeGroupoid A
winding l = subst code l ε

winding∙ : ΩBouquet →∙ FreeGroupoid∙ {A = A}
winding∙ = winding , refl

-- Functions using the truncated forms of types

π₁Bouquet : {A : Type ℓ} → Type ℓ
π₁Bouquet {A = A} = π 1 (Bouquet∙ A)

loopingT : ∥ FreeGroupoid A ∥₂ → π₁Bouquet
loopingT = map looping

windingT : π₁Bouquet → ∥ FreeGroupoid A ∥₂
windingT = map winding

-- Utility proofs

substPathsR : {C : Type ℓ}{y z : C} → (x : C) → (p : y ≡ z) → subst (λ y → x ≡ y) p ≡ λ q → q ∙ p
substPathsR {y = y} x p = funExt homotopy where
  homotopy : ∀ q → subst (λ y → x ≡ y) p q ≡ q ∙ p
  homotopy q = J P d p where
    P : ∀ z' → y ≡ z' → Type _
    P z' p' = subst (λ y → x ≡ y) p' q ≡ q ∙ p'
    d : P y refl
    d =
      subst (λ y → x ≡ y) refl q
      ≡⟨ substRefl {B = λ y → x ≡ y} q ⟩
      q
      ≡⟨ rUnit q ⟩
      q ∙ refl ∎

substFunctions : {B C : A → Type ℓ}{x y : A}
                  → (p : x ≡ y)
                  → (f : B x → C x)
                  → subst (λ z → (B z → C z)) p f ≡ subst C p ∘ f ∘ subst B (sym p)
substFunctions {B = B} {C = C} {x = x} p f =  J P d p where
  auxC : idfun (C x) ≡ subst C refl
  auxC = funExt (λ c → sym (substRefl {B = C} c))
  auxB : idfun (B x) ≡ subst B refl
  auxB = funExt (λ b → sym (substRefl {B = B} b))
  P : ∀ y' → x ≡ y' → Type _
  P y' p' = subst (λ z → (B z → C z)) p' f ≡ subst C p' ∘ f ∘ subst B (sym p')
  d : P x refl
  d =
    subst (λ z → (B z → C z)) refl f
    ≡⟨ substRefl {B = λ z → (B z → C z)} f ⟩
    f
    ≡⟨ cong (λ h → h ∘ f ∘ idfun (B x)) auxC ⟩
    subst C refl ∘ f ∘ idfun (B x)
    ≡⟨ cong (λ h → subst C refl ∘ f ∘ h) auxB ⟩
    subst C refl ∘ f ∘ subst B (sym refl) ∎

-- Definition of the encode - decode functions over the family of types Π(x : W A) → code x

encode : (x : Bouquet A) → base ≡ x → code x
encode x l = subst code l ε

decode : {A : Type ℓ}(x : Bouquet A) → code x → base ≡ x
decode {A = A} base       = looping
decode {A = A} (loop a i) = path i where
  pathover : PathP (λ i → (code (loop a i) → base ≡ (loop a i))) looping (subst (λ z → (code z → base ≡ z)) (loop a) looping)
  pathover = subst-filler (λ z → (code z → base ≡ z)) (loop a) looping
  aux : (a : A) → subst code (sym (loop a)) ≡ action (inv (η a))
  aux a = funExt homotopy where
    homotopy : ∀ (g : FreeGroupoid A) → subst code (sym (loop a)) g ≡ action (inv (η a)) g
    homotopy g =
      subst code (sym (loop a)) g
      ≡⟨ cong (λ x → transport x g) (sym (invPathsInUNaturality (η a))) ⟩
      transport (pathsInU (inv (η a))) g
      ≡⟨ uaβ  (equivs (inv (η a))) g ⟩
      action (inv (η a)) g ∎
  calculations : ∀ (a : A) → ∀ g → looping (g · (inv (η a))) ∙ loop a ≡ looping g
  calculations a g =
    looping (g · (inv (η a))) ∙ loop a
    ≡⟨ sym (pathAssoc (looping g) (sym (loop a)) (loop a)) ⟩
    looping g ∙ (sym (loop a) ∙ loop a)
    ≡⟨ cong (λ x → looping g ∙ x) (lCancel (loop a)) ⟩
    looping g ∙ refl
    ≡⟨ sym (rUnit (looping g)) ⟩
    looping g ∎
  path' : subst (λ z → (code z → base ≡ z)) (loop a) looping ≡ looping
  path' =
    subst (λ z → (code z → base ≡ z)) (loop a) looping
    ≡⟨ substFunctions {B = code} {C = λ z → base ≡ z} (loop a) looping ⟩
    subst (λ z → base ≡ z) (loop a) ∘ looping ∘ subst code (sym (loop a))
    ≡⟨ cong (λ x → x ∘ looping ∘ subst code (sym (loop a))) (substPathsR base (loop a)) ⟩
    (λ p → p ∙ loop a) ∘ looping ∘ subst code (sym (loop a))
    ≡⟨ cong (λ x → (λ p → p ∙ loop a) ∘ looping ∘ x) (aux a) ⟩
    (λ p → p ∙ loop a) ∘ looping ∘ action (inv (η a))
    ≡⟨ funExt (calculations a) ⟩
    looping ∎
  path'' : PathP (λ i → code ((loop a ∙ refl) i) → base ≡ ((loop a ∙ refl) i)) looping looping
  path'' = compPathP' {A = Bouquet A} {B = λ z → code z → base ≡ z} pathover path'
  p''≡p : PathP (λ i → code ((loop a ∙ refl) i) → base ≡ ((loop a ∙ refl) i)) looping looping ≡
          PathP (λ i → code (loop a i) → base ≡ (loop a i)) looping looping
  p''≡p = cong (λ x → PathP (λ i → code (x i) → base ≡ (x i)) looping looping) (sym (rUnit (loop a)))
  path : PathP (λ i → code (loop a i) → base ≡ (loop a i)) looping looping
  path = transport p''≡p path''

-- Non truncated Left Homotopy

decodeEncode : (x : Bouquet A) → (p : base ≡ x) → decode x (encode x p) ≡ p
decodeEncode x p = J P d p where
  P : (x' : Bouquet A) → base ≡ x' → Type _
  P x' p' = decode x' (encode x' p') ≡ p'
  d : P base refl
  d =
    decode base (encode base refl)
    ≡⟨ cong (λ e' → looping e') (transportRefl ε) ⟩
    refl ∎

left-homotopy : ∀ (l : typ (ΩBouquet {A = A})) → looping (winding l) ≡ l
left-homotopy l = decodeEncode base l

-- Truncated proofs of right homotopy of winding/looping functions

truncatedPathEquality : (g : FreeGroupoid A) → ∥ cong code (looping g) ≡ ua (equivs g) ∥₁
truncatedPathEquality = elimProp
            Bprop
            (λ a → ∣ η-ind a ∣₁)
            (λ g1 g2 → λ ∣ind1∣₁ ∣ind2∣₁ → rec2 squash₁ (λ ind1 ind2 → ∣ ·-ind g1 g2 ind1 ind2 ∣₁) ∣ind1∣₁ ∣ind2∣₁)
            ∣ ε-ind ∣₁
            (λ g → λ ∣ind∣₁ → propRec squash₁ (λ ind → ∣ inv-ind g ind ∣₁) ∣ind∣₁) where
  B : ∀ g → Type _
  B g = cong code (looping g) ≡ ua (equivs g)
  Bprop : ∀ g → isProp ∥ B g ∥₁
  Bprop g = squash₁
  η-ind : ∀ a → B (η a)
  η-ind a = refl
  ·-ind : ∀ g1 g2 → B g1 → B g2 → B (g1 · g2)
  ·-ind g1 g2 ind1 ind2 =
    cong code (looping (g1 · g2))
    ≡⟨ cong (λ x → x ∙ cong code (looping g2)) ind1 ⟩
    pathsInU g1 ∙ cong code (looping g2)
    ≡⟨ cong (λ x → pathsInU g1 ∙ x) ind2 ⟩
    pathsInU g1 ∙ pathsInU g2
    ≡⟨ sym (multPathsInUNaturality g1 g2) ⟩
    pathsInU (g1 · g2) ∎
  ε-ind : B ε
  ε-ind =
    cong code (looping ε)
    ≡⟨ sym idPathsInUNaturality ⟩
    pathsInU ε ∎
  inv-ind : ∀ g → B g → B (inv g)
  inv-ind g ind =
    cong code (looping (inv g))
    ≡⟨ cong sym ind ⟩
    sym (pathsInU g)
    ≡⟨ sym (invPathsInUNaturality g) ⟩
    ua (equivs (inv g)) ∎

truncatedRight-homotopy : (g : FreeGroupoid A) → ∥ winding (looping g) ≡ g ∥₁
truncatedRight-homotopy g = propRec squash₁ recursion (truncatedPathEquality g) where
  recursion : cong code (looping g) ≡ ua (equivs g) → ∥ winding (looping g) ≡ g ∥₁
  recursion hyp = ∣ aux ∣₁ where
    aux : winding (looping g) ≡ g
    aux =
      winding (looping g)
      ≡⟨ cong (λ x → transport x ε) hyp ⟩
      transport (ua (equivs g)) ε
      ≡⟨ uaβ  (equivs g) ε ⟩
      ε · g
      ≡⟨ sym (idl g) ⟩
      g ∎

right-homotopyInTruncatedGroupoid : (g : FreeGroupoid A) → ∣ winding (looping g) ∣₂ ≡ ∣ g ∣₂
right-homotopyInTruncatedGroupoid g = Iso.inv PathIdTrunc₀Iso (truncatedRight-homotopy g)

-- Truncated encodeDecode over all fibrations

truncatedEncodeDecode : (x : Bouquet A) → (g : code x) → ∥ encode x (decode x g) ≡ g ∥₁
truncatedEncodeDecode base = truncatedRight-homotopy
truncatedEncodeDecode (loop a i) = isProp→PathP prop truncatedRight-homotopy truncatedRight-homotopy i where
  prop : ∀ i → isProp (∀ (g : code (loop a i)) → ∥ encode (loop a i) (decode (loop a i) g) ≡ g ∥₁)
  prop i f g = funExt pointwise where
    pointwise : (x : code (loop a i)) → PathP (λ _ → ∥ encode (loop a i) (decode (loop a i) x) ≡ x ∥₁) (f x) (g x)
    pointwise x = isProp→PathP (λ i → squash₁) (f x) (g x)

encodeDecodeInTruncatedGroupoid : (x : Bouquet A) → (g : code x) → ∣ encode x (decode x g) ∣₂ ≡ ∣ g ∣₂
encodeDecodeInTruncatedGroupoid x g = Iso.inv PathIdTrunc₀Iso (truncatedEncodeDecode x g)

-- Encode Decode over the truncated versions of the types

encodeT : (x : Bouquet A) → ∥ base ≡ x ∥₂ → ∥ code x ∥₂
encodeT x = map (encode x)

decodeT : (x : Bouquet A) → ∥ code x ∥₂ → ∥ base ≡ x ∥₂
decodeT x = map (decode x)

decodeEncodeT : (x : Bouquet A) → (p : ∥ base ≡ x ∥₂) → decodeT x (encodeT x p) ≡ p
decodeEncodeT x g = elim sethood induction g where
  sethood : (q : ∥ base ≡ x ∥₂) → isSet (decodeT x (encodeT x q) ≡ q)
  sethood q = isProp→isSet (squash₂ (decodeT x (encodeT x q)) q)
  induction : (l : base ≡ x) → ∣ decode x (encode x l) ∣₂ ≡ ∣ l ∣₂
  induction l = cong (λ l' → ∣ l' ∣₂) (decodeEncode x l)

encodeDecodeT : (x : Bouquet A) → (g : ∥ code x ∥₂) → encodeT x (decodeT x g) ≡ g
encodeDecodeT x g = elim sethood induction g where
  sethood : (z : ∥ code x ∥₂) → isSet (encodeT x (decodeT x z) ≡ z)
  sethood z = isProp→isSet (squash₂ (encodeT x (decodeT x z)) z)
  induction : (a : code x) → ∣ encode x (decode x a) ∣₂ ≡ ∣ a ∣₂
  induction a = encodeDecodeInTruncatedGroupoid x a

-- Final equivalences

TruncatedFamiliesIso : (x : Bouquet A) → Iso ∥ base ≡ x ∥₂ ∥ code x ∥₂
Iso.fun (TruncatedFamiliesIso x)      = encodeT x
Iso.inv (TruncatedFamiliesIso x)      = decodeT x
Iso.rightInv (TruncatedFamiliesIso x) = encodeDecodeT x
Iso.leftInv (TruncatedFamiliesIso x)  = decodeEncodeT x

TruncatedFamiliesEquiv : (x : Bouquet A) → ∥ base ≡ x ∥₂ ≃ ∥ code x ∥₂
TruncatedFamiliesEquiv x = isoToEquiv (TruncatedFamiliesIso x)

TruncatedFamilies≡ : (x : Bouquet A) → ∥ base ≡ x ∥₂ ≡ ∥ code x ∥₂
TruncatedFamilies≡ x = ua (TruncatedFamiliesEquiv x)

π₁Bouquet≡∥FreeGroupoid∥₂ : π₁Bouquet ≡ ∥ FreeGroupoid A ∥₂
π₁Bouquet≡∥FreeGroupoid∥₂ = TruncatedFamilies≡ base

π₁Bouquet≡FreeGroup : {A : Type ℓ} → π₁Bouquet ≡ FreeGroup A
π₁Bouquet≡FreeGroup {A = A} =
  π₁Bouquet
  ≡⟨ π₁Bouquet≡∥FreeGroupoid∥₂ ⟩
  ∥ FreeGroupoid A ∥₂
  ≡⟨ sym freeGroupTruncIdempotent ⟩
  FreeGroup A ∎

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Equality

infixl 4 _>>=_
_>>=_ = bindTC

data Tm : Set where
  [_] : Term → Tm

macro
  qType : Term → Term → TC ⊤
  qType t hole = inferType t >>= quoteTC >>= unify hole

  qTerm : Term → Term → TC ⊤
  qTerm t hole = quoteTC t >>= unify hole

  unQ : Tm → Term → TC ⊤
  unQ [ t ] hole = unify hole t

postulate
  X : Set
  x y z : X

id : (A : Set) → A → A
id _ x = x

record R (A B : Set) : Set₁ where
  field
    F : X → X → X → Set

  bar : F x y z → Term
  bar fx = qType fx  -- result: F z   (x y are dropped)

  check-bar : F x y z → F x y z
  check-bar fx = id (unQ [ bar fx ]) fx

baz : ∀ {A B} (r : R A B) → R.F r x y z → Term
baz r fx = qType fx

check-baz : ∀ {A B} (r : R A B) → R.F r x y z → R.F r x y z
check-baz r fx = id (unQ [ baz r fx ]) fx

module M (A B : Set) where

  data D : Set where
    d : D

  `d = qTerm d
  d′ = unquote (unify `d)

`Md = qTerm (M.d {X} {X})

Md : M.D X X
Md = unquote (unify `Md)


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

open import HoTT renaming (pt to pt⊙)
open import homotopy.DisjointlyPointedSet
open import lib.types.Nat
open import lib.types.Vec

module simplicial.SCequivCW where

open import cw.CW public
open import cw.examples.Sphere public
open import simplicial.Base

SC-to-CW : {dim : ℕ} → SC (S dim) → Skeleton {lzero} dim
SC-to-CW {dim} sc = SC-to-CW' dim dim ltS sc
  where
  SC-to-CW' : (n : ℕ) → (predim : ℕ) → (p : n < (S predim)) → SC (S predim) → Skeleton {lzero} n
  SC-to-CW' 0 predim _ (complex ss _) = (Fin (length (lookup ss (0 , O<S predim)))) , Fin-is-set
  SC-to-CW' (S n) predim p (complex ss c) =
      attached-skeleton
          (SC-to-CW' n predim (<-cancel-S-left p) (complex ss c))
          ((Fin (length (lookup ss (n , <-cancel-S-left p)))) , Fin-is-set)
          λ cells sph → {!!}

max_stars_repo_name: maxdore/hott-morse

max_issues_repo_name: maxdore/hott-morse

max_forks_repo_name: maxdore/hott-morse


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

open import Cubical.ZCohomology.Base
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Hopf
open import Cubical.Homotopy.Freudenthal hiding (encode)
open import Cubical.HITs.Sn
open import Cubical.HITs.S1
open import Cubical.HITs.Truncation renaming (elim to trElim ; rec to trRec ; map to trMap)

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Equiv.HalfAdjoint

open import Cubical.Data.Int renaming (_+_ to +Int)
open import Cubical.Data.Nat hiding (_·_)
open import Cubical.Data.Unit

open import Cubical.HITs.Susp
open import Cubical.HITs.Nullification
open import Cubical.Data.Prod.Base
open import Cubical.Homotopy.Loopspace
open import Cubical.Data.Bool
open import Cubical.Data.Sum.Base
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.Foundations.Function
open import Cubical.Foundations.Pointed
open import Cubical.HITs.S3

private
  variable
    ℓ : Level
    A : Type ℓ

{- We want to prove that Kn≃ΩKn+1. For this we use the map ϕ-}

ϕ : (pt a : A) → typ (Ω (Susp A , north))
ϕ pt a = (merid a) ∙ sym (merid pt)

private
  Kn→ΩKn+1 : (n : ℕ) → coHomK n → typ (Ω (coHomK-ptd (suc n)))
  Kn→ΩKn+1 zero x i = ∣ intLoop x i ∣
  Kn→ΩKn+1 (suc zero) = trRec (isOfHLevelTrunc 4 ∣ north ∣ ∣ north ∣)
                               λ a i → ∣ ϕ base a i ∣
  Kn→ΩKn+1 (suc (suc n)) = trRec (isOfHLevelTrunc (2 + (3 + n)) ∣ north ∣ ∣ north ∣)
                                  λ a i → ∣ ϕ north a i ∣

  d-map : typ (Ω ((Susp S¹) , north)) → S¹
  d-map p = subst HopfSuspS¹ p base

  d-mapId : (r : S¹) → d-map (ϕ base r) ≡ r
  d-mapId r = substComposite HopfSuspS¹ (merid r) (sym (merid base)) base ∙
              rotLemma r
    where
    rotLemma : (r : S¹) → r · base ≡ r
    rotLemma base = refl
    rotLemma (loop i) = refl

sphereConnectedSpecCase : isConnected 4 (Susp (Susp S¹))
sphereConnectedSpecCase = sphereConnected 3

d-mapComp : Iso (fiber d-map base) (Path (S₊ 3) north north)
d-mapComp = compIso (IsoΣPathTransportPathΣ {B = HopfSuspS¹} _ _)
                     (congIso (invIso IsoS³TotalHopf))

is1Connected-dmap : isConnectedFun 3 d-map
is1Connected-dmap = toPropElim (λ _ → isPropIsOfHLevel 0)
                               (isConnectedRetractFromIso 3 d-mapComp
                                 (isOfHLevelRetractFromIso 0 (invIso (PathIdTruncIso 3))
                                              contrHelper))
  where
  contrHelper : isContr (Path (∥ Susp (Susp S¹) ∥ 4) ∣ north ∣ ∣ north ∣)
  fst contrHelper = refl
  snd contrHelper = isOfHLevelPlus {n = 0} 2 (sphereConnected 3) ∣ north ∣ ∣ north ∣ refl

d-Iso : Iso (∥ Path (S₊ 2) north north ∥ 3) (coHomK 1)
d-Iso = connectedTruncIso _ d-map is1Connected-dmap

d-mapId2 : Iso.fun d-Iso ∘ trMap (ϕ base) ≡ idfun (coHomK 1)
d-mapId2 = funExt (trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _) λ a i → ∣ d-mapId a i ∣)

Iso∥ϕ₁∥ : Iso (coHomK 1) (∥ Path (S₊ 2) north north ∥ 3)
Iso∥ϕ₁∥ = composesToId→Iso d-Iso (trMap (ϕ base)) d-mapId2

Iso-Kn-ΩKn+1 : (n : HLevel) → Iso (coHomK n) (typ (Ω (coHomK-ptd (suc n))))
Iso-Kn-ΩKn+1 zero = invIso (compIso (congIso (truncIdempotentIso _ isGroupoidS¹)) ΩS¹IsoInt)
Iso-Kn-ΩKn+1 (suc zero) = compIso Iso∥ϕ₁∥ (invIso (PathIdTruncIso 3))
Iso-Kn-ΩKn+1 (suc (suc n)) = compIso (stabSpheres-n≥2 n)
                                     (invIso (PathIdTruncIso (4 + n)))
 where
  helper : n + (4 + n) ≡ 2 + (n + (2 + n))
  helper = +-suc n (3 + n) ∙ (λ i → suc (+-suc n (2 + n) i))

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
module Simple where

open import Data.Nat renaming (_≟_ to _≟ℕ_)
open import Data.Fin hiding (_+_; inject)
open import Data.String hiding (_++_) renaming (_≟_ to _≟S_)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Binary.PropositionalEquality using (refl; _≡_)

open import Data.List

open import Data.Sum using (_⊎_; inj₁; inj₂)

FName : Set
FName = String

FNames : Set
FNames = List FName

data Expr : ℕ → Set where
   num : ∀ {n} → ℕ → Expr n
   bv  : ∀ {n} → (i : Fin n) → Expr n
   fv  : ∀ {n} → (x : FName) → Expr n
   ƛ   : ∀ {n} → (e : Expr (suc n)) → Expr n
   _·_ : ∀ {n} → (f : Expr n) → (e : Expr n) → Expr n

-- This idx indicates the amount of existence of lambda
-- out of current express

Expr0 : Set
Expr0 = Expr zero

↓ℕ≠ℕ : ∀ {n m} {i : Fin m}
     → ¬ (suc n ≡ toℕ (suc i))
     → ¬ (n ≡ toℕ i)
↓ℕ≠ℕ {n} {m} {i} sn≠si n≡i rewrite n≡i = sn≠si refl
-- ↓ℕ≠ℕ {n} {m} {i} sn≠si n≡i with n≡i
-- ↓ℕ≠ℕ sn≠si n≡i | refl = sn≠si refl

↓fin : ∀ {n} → (i : Fin (suc n)) → ¬ (n ≡ toℕ i) → Fin n
↓fin {zero} zero 0≠0 with 0≠0 refl
↓fin {zero} zero 0≠0 | ()
↓fin {zero} (suc ()) 0≠n
↓fin {suc n} zero i≠0 = zero
↓fin {suc n} (suc i) sn≠si = suc (↓fin i (↓ℕ≠ℕ sn≠si))

↑expr : ∀ {n} → Expr n → Expr (suc n)
↑expr (num i) = num i
↑expr (bv i)   = bv (inject₁ i)
-- inject₁ : ∀ {m} → Fin m → Fin (suc m)
↑expr (fv x)   = fv x
↑expr (ƛ e)    = ƛ (↑expr e)
↑expr (e · e₁) = ↑expr e · ↑expr e₁

{- substitution for bounded and free variable-}

[_↦_] : ∀ n → Expr n → Expr (suc n) → Expr n
[ m ↦ t ] (num i) = num i
[ m ↦ t ] (bv i) with m ≟ℕ toℕ i
... | yes m=i = t
... | no  m≠i = bv (↓fin i m≠i)
[ m ↦ t ] (fv x) = fv x
[ m ↦ t ] (ƛ e) = ƛ ([ suc m ↦ ↑expr t ] e)
[ m ↦ t ] (e · e₁) = [ m ↦ t ] e · [ m ↦ t ] e₁

[_↤_] : ∀ n → FName → Expr n → Expr (suc n)
[ m ↤ name ] (num x)  = num x
[ m ↤ name ] (bv i)   = ↑expr (bv i)
[ m ↤ name ] (fv x)   with x ≟S name
[ m ↤ name ] (fv x) | yes p = bv (fromℕ m)
[ m ↤ name ] (fv x) | no ¬p = fv x
[ m ↤ name ] (ƛ t)    = ƛ ([ suc m ↤ name ] t)
[ m ↤ name ] (t · t₁) = [ m ↤ name ] t · [ m ↤ name ] t₁

[_↝_] : ∀ {n} → FName → Expr n → Expr n → Expr n
[ n ↝ t ] (num i) = num i
[ n ↝ t ] (bv i) = bv i
[ n ↝ t ] (fv x) with n ≟S x
[ n ↝ t ] (fv x) | yes p = t
[ n ↝ t ] (fv x) | no ¬p = fv x
[ n ↝ t ] (ƛ x) = ƛ ([ n ↝ ↑expr t ] x)
[ n ↝ t ] (x · y) = [ n ↝ t ] x · [ n ↝ t ] y

_₀↦_ : Expr 1 → Expr 0 → Expr 0
m ₀↦ t = [ 0 ↦ t ] m

_↦₀_ : FName → Expr 0 → Expr 1
name ↦₀ t = [ 0 ↤ name ] t

_₀↤_ : Expr 0 → FName → Expr 1
t ₀↤ x = [ 0 ↤ x ] t

_₀↝_ : Expr 1 → FName → Expr 0
x ₀↝ s = x ₀↦ (fv s)

fvars : ∀ {n} → Expr n → FNames
fvars (num x) = []
fvars (bv i)  = []
fvars (fv x)  = x ∷ []
fvars (ƛ f)   = fvars f
fvars (f · x) = fvars f ++ fvars x

-- ############################## --
{-         locally closed         -}
-- ############################## --

open import Data.List.Any as Any
open Any.Membership-≡ using (_∈_; _∉_)
open import Data.Product

data LC : ∀ {n} → Expr n → Set where
   numᶜ : ∀ {n} → (i : ℕ) → LC {n} (num i)
   fvᶜ  : ∀ {n}
       → (x : FName)
       → LC {n} (fv x)
   _·ᶜ_ : ∀ {n} {f x}
       → LC {n} f
       → LC {n} x
       → LC {n} (f · x)
   ƛᶜ   : ∀ {e}
       → (ns : FNames)
       → ( ∀ {x} → x ∉ ns → LC {0} (e ₀↦ fv x) )
       → LC {0} (ƛ e)

postulate fresh-gen      : FNames → FName
postulate fresh-gen-spec : ∀ ns → fresh-gen ns ∉ ns

genName : (ns : FNames) → ∃ (λ x → x ∉ ns)
genName ns = fresh-gen ns , fresh-gen-spec ns

orz : ∀ {e} {nn} → nn ↦₀ (e ₀↦ fv nn) ≡ e
orz = {!   !}

foo : ∀ {nn} → (e : Expr 1) → LC {0} (e ₀↦ fv nn) → LC {1} e
foo (num i) lcp = {!   !}
foo (bv i)  lcp = {!   !}
foo (fv y)  lcp = {!   !}
foo (ƛ e)   lcp = {!   !}
foo (f · x) lcp = {!   !}

absᶜ  : ∀ {e} → LC {0} (ƛ e) → LC {1} e
absᶜ (ƛᶜ ns lcex) = {!   !}
   where nn    = proj₁ (genName ns)
         nn∉ns = proj₂ (genName ns)
         x     = lcex {nn} nn∉ns

appᶜ₁ : ∀ {n} {f x} → LC {n} (f · x) → LC {n} f
appᶜ₁ (lcf ·ᶜ lcx) = lcf

appᶜ₂ : ∀ {n} {f x} → LC {n} (f · x) → LC {n} x
appᶜ₂ (lcf ·ᶜ lcx) = lcx

lc? : ∀ {n} → (e : Expr n) → (LC {n} e ⊎ ¬ LC {n} e)
lc? (num x) = inj₁ (numᶜ x)
lc? (bv i)  = inj₂ (λ ())
lc? (fv x)  = inj₁ (fvᶜ x)
lc? (ƛ e)   with lc? e
lc? (ƛ e) | inj₁ x = inj₁ {!   !}
lc? (ƛ e) | inj₂ y = inj₂ {!   !}
lc? (f · x) with lc? f | lc? x
lc? (f · x) | inj₁ f' | inj₁ x' = inj₁ (f' ·ᶜ x')
lc? (f · x) | inj₁ f' | inj₂ x' = inj₂ (λ p → x' (appᶜ₂ p))
lc? (f · x) | inj₂ f' | _       = inj₂ (λ p → f' (appᶜ₁ p))

-- ############################## --
{-       value and semantics      -}
-- ############################## --

data Val : Expr0 → Set where
   num⁰ : ∀ n → Val (num n)
   ƛ⁰   : ∀ e → Val (ƛ e)

var? : (e : Expr0) → (Val e ⊎ ¬ (Val e))
var? (num i) = inj₁ (num⁰ i)
var? (bv i) = inj₂ (λ ())
var? (fv x) = inj₂ (λ ())
var? (ƛ x) = inj₁ (ƛ⁰ x)
var? (x · y) = inj₂ (λ ())

-- don't know what the hell this shit is
data _⟼_ : Expr 0 → Expr 0 → Set where
   app : ∀ {body para}
       → ((ƛ body) · para) ⟼ (body ₀↦ para)

max_stars_repo_name: jaiyalas/ParametricLambda

max_issues_repo_name: jaiyalas/haha

max_forks_repo_name: jaiyalas/haha


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

module Data.Fin.Properties where

open import Prelude
open import Data.Fin.Base
import Data.Nat.Properties as ℕ
open import Data.Nat.Properties using (+-comm)
open import Data.Nat
open import Function.Injective
open import Agda.Builtin.Nat renaming (_<_ to _<ᵇ_)

private
  variable
    n m : ℕ

suc-natfin : Σ[ m ⦂ ℕ ] (m ℕ.< n) → Σ[ m ⦂ ℕ ] (m ℕ.< suc n)
suc-natfin (m , p) = suc m , p

Fin-to-Nat-lt : Fin n → Σ[ m ⦂ ℕ ] (m ℕ.< n)
Fin-to-Nat-lt {n = suc n} f0 = zero , tt
Fin-to-Nat-lt {n = suc n} (fs x) = suc-natfin (Fin-to-Nat-lt x)

Fin-from-Nat-lt : ∀ m → m ℕ.< n → Fin n
Fin-from-Nat-lt {n = suc n} zero p = f0
Fin-from-Nat-lt {n = suc n} (suc m) p = fs (Fin-from-Nat-lt m p)

Fin-Nat-lt-rightInv : ∀ m → (p : m ℕ.< n) → Fin-to-Nat-lt {n = n} (Fin-from-Nat-lt m p) ≡ (m , p)
Fin-Nat-lt-rightInv {n = suc n} zero p = refl
Fin-Nat-lt-rightInv {n = suc n} (suc m) p = cong (suc-natfin {n = n}) (Fin-Nat-lt-rightInv {n = n} m p)

Fin-Nat-lt-leftInv : (x : Fin n) → uncurry Fin-from-Nat-lt (Fin-to-Nat-lt x) ≡ x
Fin-Nat-lt-leftInv {n = suc n} f0 = refl
Fin-Nat-lt-leftInv {n = suc n} (fs x) = cong fs (Fin-Nat-lt-leftInv x)

Fin-Nat-lt : Fin n ⇔ Σ[ m ⦂ ℕ ] (m ℕ.< n)
Fin-Nat-lt .fun = Fin-to-Nat-lt
Fin-Nat-lt .inv = uncurry Fin-from-Nat-lt
Fin-Nat-lt .rightInv = uncurry Fin-Nat-lt-rightInv
Fin-Nat-lt .leftInv = Fin-Nat-lt-leftInv

FinToℕ : Fin n → ℕ
FinToℕ {n = suc n} f0     = zero
FinToℕ {n = suc n} (fs x)  = suc (FinToℕ x)

FinToℕ-injective : ∀ {k} {m n : Fin k} → FinToℕ m ≡ FinToℕ n → m ≡ n
FinToℕ-injective {suc k} {f0}  {f0}  _ = refl
FinToℕ-injective {suc k} {f0}  {fs x} p = ⊥-elim (ℕ.znots p)
FinToℕ-injective {suc k} {fs m} {f0}  p = ⊥-elim (ℕ.snotz p)
FinToℕ-injective {suc k} {fs m} {fs x} p = cong fs (FinToℕ-injective (ℕ.injSuc p))

pred : Fin (suc n) → Fin (suc (ℕ.pred n))
pred f0 = f0
pred {n = suc n} (fs m) = m

discreteFin : ∀ {k} → Discrete (Fin k)
discreteFin {k = suc _} f0 f0 = yes refl
discreteFin {k = suc _} f0 (fs fk) = no (ℕ.znots ∘ cong FinToℕ)
discreteFin {k = suc _} (fs fj) f0 = no (ℕ.snotz ∘ cong FinToℕ)
discreteFin {k = suc _} (fs fj) (fs fk) =
  ⟦yes cong fs ,no cong (λ { f0 → fk ; (fs x) → x}) ⟧ (discreteFin fj fk)

isSetFin : isSet (Fin n)
isSetFin = Discrete→isSet discreteFin

FinFromℕ : (n m : ℕ) → T (n <ᵇ m) → Fin m
FinFromℕ zero (suc m) p = f0
FinFromℕ (suc n) (suc m) p = fs (FinFromℕ n m p)

infix 4 _≢ᶠ_ _≡ᶠ_
_≢ᶠ_ _≡ᶠ_ : Fin n → Fin n → Type _
n ≢ᶠ m = T (not (discreteFin n m .does))
n ≡ᶠ m = T (discreteFin n m .does)

_F↣_ : ℕ → ℕ → Type₀
n F↣ m = Σ[ f ⦂ (Fin n → Fin m) ] ∀ {x y} → x ≢ᶠ y → f x ≢ᶠ f y

shift : (x y : Fin (suc n)) → x ≢ᶠ y → Fin n
shift          f0     (fs y)  x≢y = y
shift {suc _}  (fs x)  f0     x≢y = f0
shift {suc _}  (fs x)  (fs y)  x≢y = fs (shift x y x≢y)

shift-inj : ∀ (x y z : Fin (suc n)) x≢y x≢z → y ≢ᶠ z → shift x y x≢y ≢ᶠ shift x z x≢z
shift-inj          f0     (fs y)  (fs z)  x≢y x≢z x+y≢x+z = x+y≢x+z
shift-inj {suc _}  (fs x)  f0     (fs z)  x≢y x≢z x+y≢x+z = tt
shift-inj {suc _}  (fs x)  (fs y)  f0     x≢y x≢z x+y≢x+z = tt
shift-inj {suc _}  (fs x)  (fs y)  (fs z)  x≢y x≢z x+y≢x+z = shift-inj x y z x≢y x≢z x+y≢x+z

shrink : suc n F↣ suc m → n F↣ m
shrink (f , inj) .fst  x  = shift (f f0) (f (fs x)) (inj tt)
shrink (f , inj) .snd  p  = shift-inj (f f0) (f (fs _)) (f (fs _)) (inj tt) (inj tt) (inj p)

¬plus-inj : ∀ n m → ¬ (suc (n + m) F↣ m)
¬plus-inj zero     zero     (f , _)  = f f0
¬plus-inj zero     (suc m)  inj      = ¬plus-inj zero m (shrink inj)
¬plus-inj (suc n)  m        (f , p)  = ¬plus-inj n m (f ∘ fs , p)

toFin-inj : (Fin n ↣ Fin m) → n F↣ m
toFin-inj f .fst = f .fst
toFin-inj (f , inj) .snd {x} {y} x≢ᶠy with discreteFin x y | discreteFin (f x) (f y)
... | no ¬p  | yes p  = ¬p (inj _ _ p)
... | no _   | no _   = tt

n≢sn+m : ∀ n m → Fin n ≢ Fin (suc (n + m))
n≢sn+m n m n≡m =
  ¬plus-inj m n
    (toFin-inj
      (subst
        (_↣ Fin n)
        (n≡m ; cong (Fin ∘ suc) (+-comm n m))
        refl-↣))

Fin-inj : Injective Fin
Fin-inj n m eq with compare n m
... | equal _        = refl
... | less     n  k  = ⊥-elim (n≢sn+m n k eq)
... | greater  m  k  = ⊥-elim (n≢sn+m m k (sym eq))

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
module Data.MoreNatProp where

open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong)
open import Data.Nat as Nat
  using (ℕ ; suc ; zero ; _≤′_ ; _≤_ ; _+_ ; s≤s ; z≤n ; ≤′-refl ;
         ≤′-step ; _⊔_)
open import Data.Nat.Properties as NatP
  using (≤⇒≤′ ; ≤′⇒≤ ;  m≤m+n ; s≤′s ; ≤-stepsˡ ; ≤⇒pred≤)
open import Data.Nat.Properties.Simple as NatPS
  using (+-comm ; +-suc)

≤-trans : ∀ {x y z} -> x ≤ y -> y ≤ z -> x ≤ z
≤-trans z≤n       _         = z≤n
≤-trans (s≤s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)

≤′-trans : ∀ {x y z} -> x ≤′ y -> y ≤′ z -> x ≤′ z
≤′-trans xy yz = ≤⇒≤′ (≤-trans (≤′⇒≤ xy) (≤′⇒≤ yz))

≤′+r : ∀ {x y z} -> x ≤′ y -> z + x  ≤′ z + y
≤′+r {x} {y} {zero} x≤′y = x≤′y
≤′+r {x} {y} {suc z} x≤′y = s≤′s (≤′+r {x} {y} {z} x≤′y)

≤′+l : ∀ {x y z} -> x ≤′ y -> x + z ≤′ y + z
≤′+l {x} {y} {z} x≤′y rewrite +-comm x z | +-comm y z = ≤′+r{x}{y}{z} x≤′y

≡is≤′ : ∀ {p q} -> p ≡ q -> p ≤′ q
≡is≤′ p≡q rewrite p≡q = ≤′-refl

≤+b : ∀ x y z w -> x ≤ z -> y ≤ w -> x + y ≤ z + w
≤+b .0 y z w Nat.z≤n y≤w = ≤-stepsˡ z y≤w
≤+b .(suc x) y .(suc z) w (Nat.s≤s{x}{z} x≤z) y≤w = s≤s (≤+b x y z w x≤z y≤w)

≤′+b : ∀ x y z w -> x ≤′ z -> y ≤′ w -> x + y ≤′ z + w
≤′+b x y z w x≤′z y≤′w = ≤⇒≤′ (≤+b x y z w (≤′⇒≤ x≤′z) (≤′⇒≤ y≤′w))

suc≤′⇒≤′ : ∀ x y -> suc x ≤′ y -> x ≤′ y
suc≤′⇒≤′ x .(suc x) ≤′-refl = ≤′-step ≤′-refl
suc≤′⇒≤′ x (suc n) (≤′-step sucx≤′y) = ≤′-step (suc≤′⇒≤′ x n sucx≤′y)

⊔-sym : ∀ n m -> n ⊔ m ≡ m ⊔ n
⊔-sym zero zero = refl
⊔-sym zero (suc m) = refl
⊔-sym (suc n) zero = refl
⊔-sym (suc n) (suc m) = cong suc (⊔-sym n m)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
-- {-# OPTIONS -v extendedlambda:100 -v int2abs.reifyterm.def:100 #-}
module Issue435 where

data Bool : Set where
  true false : Bool

record Unit : Set where

postulate
  Dh : ({ x : Bool } → Bool) → Set
  Di : ({{x : Bool}} → Bool) → Set

noth : Set
noth = Dh (\ { {true}  → false ; {false} → true})

noti : Set
noti = Di (\ { {{true}}  → false ; {{false}} → true})

-- Testing absurd patterns

data ⊥ : Set where

data T : Set where
  expl : (⊥ → ⊥) → T
  impl : ({_ : ⊥} → ⊥) → T
  inst : ({{_ : ⊥}} → ⊥) → T

explicit : T
explicit = expl (λ ())

implicit : T
implicit = impl (λ {})

instance : T
instance = inst (λ {{ }})

explicit-match : T
explicit-match = expl (λ { () })

implicit-match : T
implicit-match = impl (λ { {} })

implicit-match′ : T
implicit-match′ = impl (λ { { () } })

instance-match : T
instance-match = inst (λ { {{}} })

instance-match′ : T
instance-match′ = inst (λ { {{ () }} })

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Agda.Builtin.Equality

postulate
  cong₂ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} {x y : A} {u v : B}
        → (f : A → B → C) → x ≡ y → u ≡ v → f x u ≡ f y v

test = cong₂ (λ A B → A → B)


text:
module Ex6App where  -- git indicates that only commenting out of imports has happened 0/15 + 0/5 gives 0/20

open import CS410-Prelude
open import CS410-Nat
open import CS410-Vec
open import CS410-Indexed
open import CS410-Monoid
open import Ex6AgdaSetup
-- open import Ex5Sol
-- open import Ex5

--open MonadIx TilingMonadIx
--open FunctorIx (monadFunctorIx TilingMonadIx)

---------------------------------------------------------------------------
-- CURSES DISPLAY FOR APPLICATIONS (5 marks)                             --
---------------------------------------------------------------------------

-- You may need to look at the Ex6AgdaSetup file to find some of the relevant
-- kit for this episode, and it's worth looking there for goodies, anyway.
-- We start from the idea of a main loop.

{- This is the bit of code I wrote in Haskell to animate your code. -}
postulate
  mainAppLoop : {S : Set} ->             -- program state
    -- INITIALIZER
    S ->                              -- initial state
    -- EVENT HANDLER
    (Event -> S ->                    -- event and state in
     S ** List Action) ->             -- new state and screen actions out
    -- PUT 'EM TOGETHER AND YOU'VE GOT AN APPLICATION!
    IO One
{-# COMPILED mainAppLoop (\ _ -> HaskellSetup.mainAppLoop) #-}

-- The type S ** T is a type of pairs that the compiler can share with
-- Haskell. Its constructor is _,_ just as for S * T.

-- To make a thing you can run, you need to
--   (i)    choose a type to represent the program's internal state S
--   (ii)   give the initial state
--   (iii)  explain how, given an event and the current state, to
--            produce a new state and a list of actions to update the
--            display.

-- Let me show you an example...

-- To run this program, start a terminal, then
--
--    make app
--
-- You should be able to press keys and resize the thing and see sensible
-- stuff happen. Ctrl-C quits.

-- When you're bored of green rectangles, comment out the above main
-- function, so you can move on to the actual work. There are other
-- main functions further down the file which you can comment in as you
-- need them. Of course, you can have at most one main at a time.

-- Now your turn. Making use of the equipment you developed in exercise 5,
-- get us from a Painting to a List Action in two hops. Note that you will
-- have to decide how to render a Hole: some bland background stuff, please.
-- (1 mark)

layerMatrix : [ Layer -:> Matrix Cell ]
layerMatrix p = paste matrixPaste (mapIx fill p) where
  fill : [ HoleOr (Matrix Cell) -:> Matrix Cell ]
  fill h = {!!}

vecFoldR : {X Y : Set} -> (X -> Y -> Y) -> Y -> {n : Nat} -> Vec X n -> Y
vecFoldR c n [] = n
vecFoldR c n (x :: xs) = c x (vecFoldR c n xs)

matrixAction : forall {wh} -> Matrix Cell wh -> List Action
matrixAction = vecFoldR (vecFoldR {!!} id) []

---------------------------------------------------------------------------
-- APPLICATIONS                                                          --
---------------------------------------------------------------------------

-- Here's a general idea of what it means to be an "application".
-- You need to choose some sort of size-dependent state, then provide these
-- bits and pieces. We need to know how the state is updated according to
-- events, with resizing potentially affecting the state's type. We must
-- be able to paint the state. The state should propose a cursor position.
-- (Keen students may modify this definition to ensure the cursor must be
-- within the bounds of the application.)

record Application (S : Nat * Nat -> Set) : Set where
  field
    handleKey     : Key -> [ S -:> S ]
    handleResize  : {w h : Nat}(w' h' : Nat) -> S (w , h) -> S (w' , h')
    paintMe       : [ S -:> Layer ]
    cursorMe      : {w h : Nat} -> S (w , h) -> Nat * Nat  -- x,y coords
open Application public

-- Now your turn. Build the appropriate handler to connect these
-- applications with mainLoop. Again, work in two stages, first
-- figuring out how to do the right actions, then managing the
-- state properly. (1 mark)

AppState : (S : Nat * Nat -> Set) -> Set
AppState S = Sg Nat \ w -> Sg Nat \ h -> S (w , h)

appPaint : {S : Nat * Nat -> Set}{w h : Nat} ->
           Application S -> S (w , h) -> List Action
appPaint app s =
  goRowCol 0 0 :: matrixAction (layerMatrix p)
  ++ (goRowCol (snd xy) (fst xy) :: [])
  where
    p  = paintMe app s
    xy = cursorMe app s

appHandler : {S : Nat * Nat -> Set} ->
           Application S ->
           Event -> AppState S -> AppState S ** List Action
appHandler app (key k) (w , h , s) = (w , h , s') , appPaint app s'
  where s' = handleKey app k s
appHandler app (resize w' h') (w , h , s) = (w' , h' , s') , appPaint app s'
  where s' = handleResize app w' h' s

-- Your code turns into a main function, as follows.

appMain : {S : Nat * Nat -> Set} -> Application S -> S (0 , 0) -> IO One
appMain app s = mainAppLoop (0 , 0 , s) (appHandler app)

---------------------------------------------------------------------------
-- A DEMO APPLICATION                                                    --
---------------------------------------------------------------------------

sillyChar : Char -> {w h : Nat} -> Layer (w , h)
sillyChar c = ! (block (vec (vec (green - c / black))))

sillyApp : Application \ _ -> Char
sillyApp = record
  {  handleKey     = \ { (char c) _ -> c ; _ c -> c }
  ;  handleResize  = \ _ _ c -> c
  ;  paintMe       = \
       { {suc (suc w) , suc (suc h)} c ->
          joinV 1 (suc h) refl
            (sillyChar c)
            (joinV h 1 (sym (plusCommFact 1 h))
              (joinH 1 (suc w) refl (sillyChar c)
               (joinH w 1 (sym (plusCommFact 1 w)) (sillyChar ' ') (sillyChar c))
               )
              (sillyChar c) )
       ; c -> sillyChar c
       }
  ;  cursorMe      = \ _ -> 0 , 0
  }

{- -}
main : IO One
main = appMain sillyApp '*'
{- -}

---------------------------------------------------------------------------
-- COMPARING TWO NUMBERS                                                 --
---------------------------------------------------------------------------

-- You've done the tricky part in exercise 5, comparing two splittings of
-- the same number. Here's an easy way to reuse that code just to compare
-- two numbers. It may help in what is to come.

Compare : Nat -> Nat -> Set
Compare x y = CutComparable x y y x (x +N y)

compare : (x y : Nat) -> Compare x y
compare x y = cutCompare x y y x (x +N y) refl (sym (plusCommFact x y))

-- To make sure you've got the message, try writing these things
-- "with compare" to resize paintings. If you need to make a painting
-- bigger, pad its right or bottom with a hole. If you need to make it
-- smaller, trim off the right or bottom excess. You have all the gadgets
-- you need! I'm not giving marks for these, but they'll be useful in
-- the next bit.

cropPadLR : (w h w' : Nat) -> Layer (w , h) -> Layer (w' , h)
cropPadLR w h w' p = {!!}

cropPadTB : (w h h' : Nat) -> Layer (w , h) -> Layer (w , h')
cropPadTB w h h' p = {!!}

---------------------------------------------------------------------------
-- THE MOVING RECTANGLE                                                  --
---------------------------------------------------------------------------

-- This is the crux of this episode. Please build me an application which
-- displays a movable resizeable rectangle drawn with ascii art as follows
--
--           +--------------+
--           |              |
--           |              |
--           +--------------+
--
-- The "size" of the application is the terminal size: the rectangle should
-- be freely resizable *within* the terminal, so you should pad out the
-- rectangle to the size of the screen using Hole.
-- That is, only the rectangle is opaque; the rest is transparent.
-- The background colour of the rectangle should be given as an argument.
-- The foreground colour of the rectangle should be white.
-- The rectangle should have an interior consisting of opaque space with
-- the given background colour.
--
-- The arrow keys should move the rectangle around inside the terminal
-- window, preserving its size (like when you drag a window around).
-- Shifted arrow keys should resize the rectangle by moving its bottom
-- right corner (again, like you might do with a mouse).
-- You do not need to ensure that the rectangle fits inside the terminal.
-- The cursor should sit at the bottom right corner of the rectangle.
--
-- Mac users: the Terminal application which ships with OS X does NOT
-- give the correct treatment to shift-up and shift-down. You can get a
-- suitable alternative from http://iterm2.com/ (Thank @sigfpe for the tip!)
--
-- (2 marks, one for key handling, one for painting)

record RectState : Set where
  constructor rect
  field
    gapL rectW : Nat
    gapT rectH : Nat

rectKey : Key -> RectState -> RectState
rectKey k s = {!!}

rectApp : Colour -> Application \ _ -> RectState
rectApp c = record
  {  handleKey     = \ k -> rectKey k
  ;  handleResize  = \ _ _ -> id
  ;  paintMe = {!!}
  ;  cursorMe = {!!}
  } where
  -- helper functions can go here

{- -
main : IO One
main = appMain (rectApp blue) (rect 10 40 3 15)
- -}

---------------------------------------------------------------------------
-- TWO BECOME ONE                                                        --
---------------------------------------------------------------------------

-- Write a function which turns two sub-applications into one main
-- application by layering them.
--
-- For some S and T, you get an Application S and an Application T
-- You should choose a suitable state representation so that you know
--   (i)   which of the two applications is at the front, and which behind
--   (ii)  the states of both.
--
-- The Tab key should swap which sub-application is at the front, as if you had
-- clicked on the one at the back. All other keys should be handled by
-- whichever action is in front at the time. Also, the cursor position
-- should be chosen by the sub-application at the front.
--
-- The overall application size will be used as the size for both
-- sub-application sizes, which means you should be able to compute the
-- Layer, using equipment from exercise 5. Crucially, we should be
-- able to see through the holes in the front sub-application to stuff from
-- the back sub-application.
--
-- (1 mark)

frontBack : {S T : Nat * Nat -> Set} ->
  Application S ->
  Application T ->
  Application \ wh -> {!!}
frontBack appS appT = record
  { handleKey = {!!}
  ; handleResize = {!!}
  ; paintMe = {!!}
  ; cursorMe = {!!}
  }

-- By way of example, let's have a blue rectangle and a red rectangle.

{- -
main : IO One
main = appMain (frontBack (rectApp blue) (rectApp red))
  (inl (rect 10 40 3 15 , rect 20 40 8 15))
- -}

---------------------------------------------------------------------------
-- IF YOU WANT MORE...                                                   --
---------------------------------------------------------------------------

-- Figure out how to reduce flicker.
-- Put editors in the rectangles.


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

open import lib.Basics

module lib.types.Empty where

Empty-rec : ∀ {i} {A : Type i} → (Empty → A)
Empty-rec = Empty-elim

⊥-rec : ∀ {i} {A : Type i} → (⊥ → A)
⊥-rec = Empty-rec

abstract
  Empty-is-prop : is-prop Empty
  Empty-is-prop = Empty-elim

  Empty-is-set : is-set Empty
  Empty-is-set = raise-level -1 Empty-is-prop

  Empty-level = Empty-is-prop
  ⊥-is-prop = Empty-is-prop
  ⊥-is-set = Empty-is-set
  ⊥-level = Empty-level

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
open import library.NType2

open import Sec2preliminaries
open import Sec3hedberg
open import Sec4hasConstToSplit

module Sec5factorConst where

-- Definition 5.1
factors-through : {X Y : Type} → Type → (X → Y) → Type
factors-through {X} {Y} Z f = Σ (X → Z) λ f₁ → Σ (Z → Y) λ f₂ → (x : X) → f₂ (f₁ x) == f x

-- Definition 5.1 addendum: "factors through the truncation"
factors : {X Y : Type} → (X → Y) → Type
factors {X} = factors-through (Trunc X)

-- Principle 5.2
factor-helper : {X Y : Type} → (f : X → Y) → (P : Type) → (X → is-prop P) → (factors-through P f) → factors f
factor-helper {X} {Y} f P xpp (f₁ , f₂ , q) = f₁' , f₂' , q' where
  f₁' : X → Trunc X
  f₁' = ∣_∣

  f₂' : Trunc X → Y
  f₂' z = f₂ (rec {X} (rec is-prop-is-prop xpp z) f₁ z)

  q' : (x : X) → f₂' (f₁' x) == f x
  q' x =
    f₂' (f₁' x)         =⟨ idp ⟩
    f₂' ∣ x ∣            =⟨ idp ⟩
    f₂ (rec _ f₁ ∣ x ∣ ) =⟨ ap f₂ (trunc-β _ f₁ x) ⟩
    f₂ (f₁ x)           =⟨ q x ⟩
    f x                 ∎

-- Theorem 5.3
module thm53 {X Y : Type} (f : X → Y) (c : const f) where
  One = ¬ X
  Two = X
  Three = Trunc X → X
  Four = hasConst X
  Five = Y → X

  One→Three : One → Three
  One→Three nx z = Empty-elim {A = λ _ → X} (rec Empty-elim nx z)

  Two→Three : Two → Three
  Two→Three x = λ _ → x

  Five→Four : Five → Four
  Five→Four g = g ∘ f , (λ x₁ x₂ → ap g (c x₁ x₂))

  Three↔Four : Three ↔ Four
  Three↔Four = snd hasConst↔splitSup , fst hasConst↔splitSup

  Three→factors : Three → factors f
  Three→factors s = ∣_∣ , f ∘ s , (λ x → c _ _)

-- Theorem 5.4
-- as a small preparation, let us define a function that applies the truncation recursor twice:
double-rec : {X₁ X₂ P : Type} → (is-prop P) → (X₁ → X₂ → P) → Trunc X₁ → Trunc X₂ → P
double-rec {X₁} {X₂} {P} pp f z₁ z₂ = next-step z₂ z₁ where
  step : X₁ → Trunc X₂ → P
  step x₁ = rec {X = X₂} {P = P} pp (f x₁)
  step-switch : Trunc X₂ → X₁ → P
  step-switch z₂ x₁ = step x₁ z₂
  next-step : Trunc X₂ → Trunc X₁ → P
  next-step z₂ = rec pp (step-switch z₂)

-- now, the actual Theorem 5.4
factor-codomain-set : {X Y : Type} → (f : X → Y) → const f → is-set Y → factors f
factor-codomain-set {X} {Y} f c h = factor-helper f P (λ _ → pp) fact-through-p where
  P : Type
  P = Σ Y λ y → Trunc(Σ X λ x → f x == y)

  pp : is-prop P
  pp = all-paths-is-prop all-paths where
    all-paths : has-all-paths P
    all-paths (y₁ , t₁) (y₂ , t₂) = pair= ys ts where
      ys = double-rec {P = y₁ == y₂} (h _ _) (λ {(x₁ , p₁) (x₂ , p₂) → ! p₁ ∙ c _ _ ∙ p₂}) t₁ t₂
      ts = from-transp _ ys (prop-has-all-paths (h-tr _) _ _)

  fact-through-p : factors-through P f
  fact-through-p = f₁ , f₂ , q where
    f₁ : X → P
    f₁ x = f x , ∣ x , idp ∣
    f₂ : P → Y
    f₂ = fst
    q : (x : X) → f₂ (f₁ x) == f x
    q x = idp

-- Theorem 5.5
-- Note that this lemma requires function extensionality (hidden in the use of the library.types.Pi library:
-- at one point, we use that Π X Y is propositional as soon as Y x is (for all x)).

open import library.types.Pi

-- a general auxiliary function which switches the second and third component of a Σ-type with four components
-- (provided that it is possible)
-- we formulate this explicitly as we will need it several times
switch23 : {X : Type} → {Y Z : X → Type} → {W : (x : X) → (Y x) → (Z x) → Type} →
  (Σ X λ x → Σ (Y x) λ y → Σ (Z x) λ z → (W x y z)) ≃
  (Σ X λ x → Σ (Z x) λ z → Σ (Y x) λ y → (W x y z))
switch23 = equiv (λ {(y , s , t , coh) → (y , t , s , coh)}) (λ {(y , t , s , coh) → (y , s , t , coh)}) (λ _ → idp) (λ _ → idp)

module thm55aux {P : Type} {Y : P → Type} (pp : is-prop P) (x₀ : P) where
  neutral-contr-base-space : Σ P Y ≃ Y x₀
  neutral-contr-base-space =
    Σ P Y               ≃⟨ (equiv-Σ-fst {A = Unit} {B = P} Y
                             {λ _ → x₀}
                             (is-eq _ (λ _ → unit) (λ _ → prop-has-all-paths pp _ _) (λ _ → idp))) ⁻¹  ⟩
    Σ Unit (λ _ → Y x₀) ≃⟨ Σ₁-Unit ⟩
    Y x₀                ≃∎

  neutral-contr-exp : Π P Y ≃ Y x₀
  neutral-contr-exp =
    Π P Y               ≃⟨ (equiv-Π-l {A = Unit} {B = P} Y
                             {λ _ → x₀}
                             (is-eq _ (λ _ → unit) (λ _ → prop-has-all-paths pp _ _) (λ _ → idp))) ⁻¹ ⟩
    Π Unit (λ _ → Y x₀) ≃⟨ Π₁-Unit ⟩
    Y x₀                ≃∎

module thm55 {Q R Y : Type} (qq : is-prop Q) (rr : is-prop R) (f : Q + R → Y) (c : const f) where

  P : Type
  P = Σ Y λ y →
        Σ ((q : Q) → y == f(inl q)) λ s →
        Σ ((r : R) → y == f(inr r)) λ t →
          (q : Q) → (r : R) → ! (s q) ∙ (t r) == c (inl q) (inr r)

  -- This is going to be tedious: if q₀ : Q is given, we can show that P is equivalent to the Unit type.
  given-q-reduce-P : Q → P ≃ Unit
  given-q-reduce-P q₀ =

    P

                         ≃⟨ switch23 ⟩

    (Σ Y λ y →
        Σ ((r : R) → y == f(inr r)) λ t →
        Σ ((q : Q) → y == f(inl q)) λ s →
          (q : Q) → (r : R) → ! (s q) ∙ (t r) == c (inl q) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → choice ⁻¹)) ⟩

    (Σ Y λ y →
        Σ ((r : R) → y == f(inr r)) λ t →
          (q : Q) → Σ (y == f(inl q)) λ s-reduced →
                      (r : R) → ! s-reduced ∙ (t r) == c (inl q) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → thm55aux.neutral-contr-exp qq q₀)) ⟩

    (Σ Y λ y →
        Σ ((r : R) → y == f(inr r)) λ t →
          Σ (y == f(inl q₀)) λ s-reduced →
            (r : R) → ! s-reduced ∙ (t r) == c (inl q₀) (inr r))

                         ≃⟨ switch23 ⟩

    (Σ Y λ y →
        Σ (y == f(inl q₀)) λ s-reduced →
          Σ ((r : R) → y == f(inr r)) λ t →
            (r : R) → ! s-reduced ∙ (t r) == c (inl q₀) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → choice ⁻¹)) ⟩

    (Σ Y λ y →
        Σ (y == f(inl q₀)) λ s-reduced →
          (r : R) → Σ (y == f(inr r)) λ t-reduced →
                       ! s-reduced ∙ t-reduced == c (inl q₀) (inr r))

                         ≃⟨ Σ-assoc ⁻¹ ⟩

    (Σ (Σ Y λ y → (y == f(inl q₀))) λ {(y , s-reduced) →
       (r : R) → Σ (y == f(inr r)) λ t-reduced →
                   ! s-reduced ∙ t-reduced == c (inl q₀) (inr r)})

                         ≃⟨ thm55aux.neutral-contr-base-space (contr-is-prop (pathto-is-contr _)) (f(inl q₀) , idp) ⟩

    ((r : R) → Σ (f(inl q₀) == f(inr r)) λ t-reduced →
                 idp ∙ t-reduced == c (inl q₀) (inr r))

                         ≃⟨ neutral-codomain (λ r → pathto-is-contr _) ⟩

    Unit                 ≃∎

  given-r-reduce-P : R → P ≃ Unit
  given-r-reduce-P r₀ =

    P

                         ≃⟨ equiv-Σ-snd (λ _ → equiv-Σ-snd (λ _ → equiv-Σ-snd (λ _ → switch-args))) ⟩

    (Σ Y λ y →
        Σ ((q : Q) → y == f(inl q)) λ s →
        Σ ((r : R) → y == f(inr r)) λ t →
          (r : R) → (q : Q) → ! (s q) ∙ (t r) == c (inl q) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ s → choice ⁻¹)) ⟩

    (Σ Y λ y →
        Σ ((q : Q) → y == f(inl q)) λ s →
          (r : R) → Σ (y == f(inr r)) λ t-reduced →
                      (q : Q) → ! (s q) ∙ t-reduced == c (inl q) (inr r))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ t → thm55aux.neutral-contr-exp rr r₀)) ⟩

    (Σ Y λ y →
        Σ ((q : Q) → y == f(inl q)) λ s →
          Σ (y == f(inr r₀)) λ t-reduced →
            (q : Q) → ! (s q) ∙ t-reduced == c (inl q) (inr r₀))

                         ≃⟨ switch23 ⟩

    (Σ Y λ y →
        Σ (y == f(inr r₀)) λ t-reduced →
          Σ ((q : Q) → y == f(inl q)) λ s →
            (q : Q) → ! (s q) ∙ t-reduced == c (inl q) (inr r₀))

                         ≃⟨ equiv-Σ-snd (λ y → equiv-Σ-snd (λ s → choice ⁻¹)) ⟩

    (Σ Y λ y →
        Σ (y == f(inr r₀)) λ t-reduced →
          (q : Q) → Σ (y == f(inl q)) λ s-reduced →
                       ! s-reduced ∙ t-reduced == c (inl q) (inr r₀))

                         ≃⟨ Σ-assoc ⁻¹ ⟩

    (Σ (Σ Y λ y → (y == f(inr r₀))) λ {(y , t-reduced) →
       (q : Q) → Σ (y == f(inl q)) λ s-reduced →
                   ! s-reduced ∙ t-reduced == c (inl q) (inr r₀)})

                         ≃⟨ thm55aux.neutral-contr-base-space (contr-is-prop (pathto-is-contr _)) (f(inr r₀) , idp) ⟩

    ((q : Q) → Σ (f(inr r₀) == f(inl q)) λ s-reduced →
                  ! s-reduced ∙ idp == c (inl q) (inr r₀))

                         ≃⟨ equiv-Π-r (λ q → equiv-Σ-snd (λ proof →
                              ! proof ∙ idp == c (inl q) (inr r₀) ≃⟨ delete-idp _ _ ⟩
                              ! proof == c (inl q) (inr r₀) ≃⟨ reverse-paths _ _ ⟩
                              proof == ! (c (inl q) (inr r₀))   ≃∎
                         )) ⟩

    ((q : Q) → Σ (f(inr r₀) == f(inl q)) λ s-reduced →
                  s-reduced == ! (c (inl q) (inr r₀)))

                         ≃⟨  neutral-codomain (λ q → pathto-is-contr _) ⟩

    Unit                 ≃∎

  given-q+r-reduce-P : Q + R → P ≃ Unit
  given-q+r-reduce-P (inl q) = given-q-reduce-P q
  given-q+r-reduce-P (inr r) = given-r-reduce-P r

  Q+R→P : Q + R → P
  Q+R→P x = <– (given-q+r-reduce-P x) _

  P→Y : P → Y
  P→Y = fst

  open import library.types.Unit

  -- Finally : the statement of Theorem 5.5
  factor-f : factors f
  factor-f = factor-helper f P (λ x → equiv-preserves-level ((given-q+r-reduce-P x) ⁻¹) Unit-is-prop) (Q+R→P , P→Y , proof) where
    proof : (x : Q + R) → P→Y (Q+R→P x) == f x
    proof (inl q) = idp
    proof (inr r) = idp

-- and Theorem 5.5 again (outside of a specialized module)
Theorem55 : {Q R Y : Type} → (is-prop Q) → (is-prop R) → (f : Q + R → Y) → (const f) → factors f
Theorem55 = thm55.factor-f

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Relation.Binary using (Rel; Setoid; IsEquivalence)
module Magma.Structures
  {a ℓ} {A : Set a}  -- The underlying set
  (_≈_ : Rel A ℓ)    -- The underlying equality relation
  where

open import Algebra.Core
open import Level using (_⊔_)
open import Data.Product using (_,_; proj₁; proj₂)
open import Algebra.Definitions _≈_
open import Algebra.Structures _≈_
open import Magma.Definitions  _≈_

record IsIdempotentMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma ∙
    idem    : Idempotent ∙

  open IsMagma isMagma public

record IsAlternateMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma  : IsMagma ∙
    alter    : Alternative ∙

  open IsMagma isMagma public

record IsFlexibleMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma  : IsMagma ∙
    flex     : Flexible ∙

  open IsMagma isMagma public

record IsMedialMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma ∙
    medial  : Medial ∙

  open IsMagma isMagma public

record IsSemimedialMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
  field
    isMagma : IsMagma ∙
    semiMedial  : Semimedial ∙

  open IsMagma isMagma public

record IsLeftUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isMagma  : IsMagma ∙
    identity : LeftIdentity ε ∙

  open IsMagma isMagma public

record IsRightUnitalMagma (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
  field
    isMagma  : IsMagma ∙
    identity : RightIdentity ε ∙

  open IsMagma isMagma public


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

open import HoTT
open import homotopy.RibbonCover

module homotopy.CoverClassification {i} (A∙ : Ptd i)
  (A-conn : is-connected 0 (fst A∙)) where

  open Cover

  private
    A : Type i
    A = fst A∙
    a₁ : A
    a₁ = snd A∙
    π1A = fundamental-group A∙

  -- A covering space constructed from a G-set.
  gset-to-cover : ∀ {j} → Gset π1A j → Cover A (lmax i j)
  gset-to-cover gs = Ribbon-cover A∙ gs

  -- Covering spaces to G-sets.
  cover-to-gset-struct : ∀ {j} (cov : Cover A j)
    → GsetStructure π1A (Fiber cov a₁) (Fiber-is-set cov a₁)
  cover-to-gset-struct cov = record
    { act = cover-trace cov
    ; unit-r = cover-trace-idp₀ cov
    ; assoc = cover-paste cov
    }

  cover-to-gset : ∀ {j} → Cover A j → Gset π1A j
  cover-to-gset cov = record
    { El = Fiber cov a₁
    ; El-level = Fiber-level cov a₁
    ; gset-struct = cover-to-gset-struct cov
    }

  -- This is derivable from connectedness condition.
  module _ where
    abstract
      [base-path] : ∀ {a₂ : A} → Trunc -1 (a₁ == a₂)
      [base-path] {a₂} =
        –> (Trunc=-equiv [ a₁ ] [ a₂ ]) (contr-has-all-paths A-conn [ a₁ ] [ a₂ ])

  -- Part 1: Show that the synthesized cover (ribbon) is fiberwisely
  --         equivalent to the original fiber.
  private
    module _ {j} (cov : Cover A j) where

      -- Suppose that we get the path, we can compute the ribbon easily.
      fiber+path-to-ribbon : ∀ {a₂} (a↑ : Fiber cov a₂) (p : a₁ == a₂)
        → Ribbon A∙ (cover-to-gset cov) a₂
      fiber+path-to-ribbon {a₂} a↑ p =
        trace (cover-trace cov a↑ [ ! p ]) [ p ]

      abstract
        -- Our construction is "constant" with respect to paths.
        fiber+path-to-ribbon-is-path-irrelevant :
          ∀ {a₂} (a↑ : Fiber cov a₂) (p₁ p₂ : a₁ == a₂)
          → fiber+path-to-ribbon a↑ p₁ == fiber+path-to-ribbon a↑ p₂
        fiber+path-to-ribbon-is-path-irrelevant a↑ p idp =
          trace (cover-trace cov a↑ [ ! p ]) [ p ]
            =⟨ paste a↑ [ ! p ] [ p ] ⟩
          trace a↑ [ ! p ∙ p ]
            =⟨ ap (trace a↑) $ !₀-inv-l [ p ] ⟩
          trace a↑ idp₀
            ∎

      open import homotopy.ConstantToSetFactorization

      fiber+path₋₁-to-ribbon : ∀ {a₂} (a↑ : Cover.Fiber cov a₂)
        → Trunc -1 (a₁ == a₂) → Ribbon A∙ (cover-to-gset cov) a₂
      fiber+path₋₁-to-ribbon a↑ = cst-extend
        Ribbon-is-set
        (fiber+path-to-ribbon a↑)
        (fiber+path-to-ribbon-is-path-irrelevant a↑)

  -- So the conversion from fiber to ribbon is done.
  fiber-to-ribbon : ∀ {j} (cov : Cover A j)
    → {a₂ : A} (a↑ : Cover.Fiber cov a₂)
    → Ribbon A∙ (cover-to-gset cov) a₂
  fiber-to-ribbon cov a↑ = fiber+path₋₁-to-ribbon cov a↑ [base-path]

  -- The other direction is easy.
  ribbon-to-fiber : ∀ {j} (cov : Cover A j) {a₂}
    → Ribbon A∙ (cover-to-gset cov) a₂ → Cover.Fiber cov a₂
  ribbon-to-fiber cov {a₂} r =
    Ribbon-rec (Fiber-is-set cov a₂) (cover-trace cov) (cover-paste cov) r

  private
    -- Some routine computations.
    abstract
      ribbon-to-fiber-to-ribbon : ∀ {j} (cov : Cover A j) {a₂}
        → (r : Ribbon A∙ (cover-to-gset cov) a₂)
        → fiber-to-ribbon cov (ribbon-to-fiber cov r) == r
      ribbon-to-fiber-to-ribbon cov {a₂} = Ribbon-elim
        {P = λ r → fiber-to-ribbon cov (ribbon-to-fiber cov r) == r}
        (λ _ → =-preserves-set Ribbon-is-set)
        (λ a↑ p → Trunc-elim
          -- All ugly things will go away when bp = proj bp′
          (λ bp → Ribbon-is-set
                    (fiber+path₋₁-to-ribbon cov (cover-trace cov a↑ p) bp)
                    (trace a↑ p))
          (lemma a↑ p)
          [base-path])
        (λ _ _ _ → prop-has-all-paths-↓ (Ribbon-is-set _ _))
        where
          abstract
            lemma : ∀ {a₂} (a↑ : Cover.Fiber cov a₁) (p : a₁ =₀ a₂) (bp : a₁ == a₂)
              → trace {A∙ = A∙} {gs = cover-to-gset cov}
                  (cover-trace cov (cover-trace cov a↑ p) [ ! bp ]) [ bp ]
              == trace {A∙ = A∙} {gs = cover-to-gset cov} a↑ p
            lemma a↑ p idp =
              trace (cover-trace cov a↑ p) idp₀
                =⟨ paste a↑ p idp₀ ⟩
              trace a↑ (p ∙₀ idp₀)
                =⟨ ap (trace a↑) $ ∙₀-unit-r p ⟩
              trace a↑ p
                ∎

      fiber-to-ribbon-to-fiber : ∀ {j} (cov : Cover A j) {a₂}
        → (a↑ : Cover.Fiber cov a₂)
        → ribbon-to-fiber cov (fiber-to-ribbon cov {a₂} a↑) == a↑
      fiber-to-ribbon-to-fiber cov {a₂} a↑ = Trunc-elim
        -- All ugly things will go away when bp = proj bp′
        (λ bp → Cover.Fiber-is-set cov a₂
                  (ribbon-to-fiber cov
                    (fiber+path₋₁-to-ribbon cov a↑ bp))
                  a↑)
        (lemma a↑)
        [base-path]
        where
          abstract
            lemma : ∀ {a₂} (a↑ : Cover.Fiber cov a₂) (bp : a₁ == a₂)
              → cover-trace cov (cover-trace cov a↑ [ ! bp ]) [ bp ]
              == a↑
            lemma a↑ idp = idp

  cover-to-gset-to-cover : ∀ {j} (cov : Cover A (lmax i j))
    → gset-to-cover (cover-to-gset cov) == cov
  cover-to-gset-to-cover cov = cover= λ _ →
    ribbon-to-fiber cov , is-eq
      (ribbon-to-fiber cov)
      (fiber-to-ribbon cov)
      (fiber-to-ribbon-to-fiber cov)
      (ribbon-to-fiber-to-ribbon cov)

  -- The second direction : gset -> covering -> gset

  -- Part 2.1: The fiber over the point a is the carrier.
  ribbon-a₁-to-El : ∀ {j} {gs : Gset π1A j}
    → Ribbon A∙ gs a₁ → Gset.El gs
  ribbon-a₁-to-El {j} {gs} = let open Gset gs in
    Ribbon-rec El-level act assoc

  ribbon-a₁-to-El-equiv : ∀ {j} {gs : Gset π1A j}
    → Ribbon A∙ gs a₁ ≃ Gset.El gs
  ribbon-a₁-to-El-equiv {j} {gs} = let open Gset gs in
    ribbon-a₁-to-El , is-eq _
      (λ r → trace r idp₀)
      (λ a↑ → unit-r a↑)
      (Ribbon-elim
        {P = λ r → trace (ribbon-a₁-to-El r) idp₀ == r}
        (λ _ → =-preserves-set Ribbon-is-set)
        (λ y p →
          trace (act y p) idp₀
            =⟨ paste y p idp₀ ⟩
          trace y (p ∙₀ idp₀)
            =⟨ ap (trace y) $ ∙₀-unit-r p ⟩
          trace y p
            ∎)
        (λ _ _ _ → prop-has-all-paths-↓ (Ribbon-is-set _ _)))

  gset-to-cover-to-gset : ∀ {j} (gs : Gset π1A (lmax i j))
    → cover-to-gset (gset-to-cover gs) == gs
  gset-to-cover-to-gset gs =
    gset=
      ribbon-a₁-to-El-equiv
      (λ {x₁}{x₂} x= → Trunc-elim (λ _ → =-preserves-set $ Gset.El-is-set gs) λ g →
        ribbon-a₁-to-El (transport (Ribbon A∙ gs) g x₁)
          =⟨ ap (λ x → ribbon-a₁-to-El (transport (Ribbon A∙ gs) g x))
                $ ! $ <–-inv-l ribbon-a₁-to-El-equiv x₁ ⟩
        ribbon-a₁-to-El (transport (Ribbon A∙ gs) g (trace (ribbon-a₁-to-El x₁) idp₀))
          =⟨ ap (λ x → ribbon-a₁-to-El (transport (Ribbon A∙ gs) g (trace x idp₀))) x= ⟩
        ribbon-a₁-to-El (transport (Ribbon A∙ gs) g (trace x₂ idp₀))
          =⟨ ap ribbon-a₁-to-El $ trans-trace g x₂ idp₀ ⟩
        Gset.act gs x₂ [ g ]
          ∎)

  -- Finally...
  gset-to-cover-equiv : ∀ {j}
    → Gset π1A (lmax i j) ≃ Cover A (lmax i j)
  gset-to-cover-equiv {j} =
    gset-to-cover , is-eq
      _
      (λ c → cover-to-gset c)
      (λ c → cover-to-gset-to-cover {lmax i j} c)
      (gset-to-cover-to-gset {lmax i j})

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Agda.Builtin.Coinduction where

infix 1000 ♯_

postulate
  ∞  : ∀ {a} (A : Set a) → Set a
  ♯_ : ∀ {a} {A : Set a} → A → ∞ A
  ♭  : ∀ {a} {A : Set a} → ∞ A → A

{-# BUILTIN INFINITY ∞  #-}
{-# BUILTIN SHARP    ♯_ #-}
{-# BUILTIN FLAT     ♭  #-}


text:
-- Andreas, 2013-02-27
module Issue653 where

postulate
  P : {A : Set} → (A → Set) → Set

mutual

  A : Set
  A = P B -- note A = P {A} B is non-terminating

  data B : A → Set where
    c : (a : A) → B a
-- This caused a stack overflow due to infinite reduction
-- in the positivity checker.
-- Now functions that do not pass the termination checker are not unfolded
-- any more.
-- So, it should report positivity violation now.


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.QuoInt.Properties where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Relation.Nullary

open import Cubical.Data.Nat as ℕ using (ℕ; zero; suc)
open import Cubical.Data.Bool as Bool using (Bool; not; notnot)
open import Cubical.Data.Empty
open import Cubical.Data.Unit renaming (Unit to ⊤)

open import Cubical.HITs.Ints.QuoInt.Base

·S-comm : ∀ x y → x ·S y ≡ y ·S x
·S-comm = Bool.⊕-comm

·S-assoc : ∀ x y z → x ·S (y ·S z) ≡ (x ·S y) ·S z
·S-assoc = Bool.⊕-assoc

not-·Sˡ : ∀ x y → not (x ·S y) ≡ not x ·S y
not-·Sˡ = Bool.not-⊕ˡ

snotz : ∀ s n s' → ¬ (signed s (suc n) ≡ signed s' zero)
snotz s n s' eq = subst (λ { (signed s (suc n)) → ⊤
                           ; _                  → ⊥ }) eq tt

+-zeroʳ : ∀ s m → m + signed s zero ≡ m
+-zeroʳ s (signed s' zero) = signed-zero s s'
+-zeroʳ s (pos (suc n)) = cong sucℤ  (+-zeroʳ s (pos n))
+-zeroʳ s (neg (suc n)) = cong predℤ (+-zeroʳ s (neg n))
+-zeroʳ spos (posneg i) j = posneg (i ∧ j)
+-zeroʳ sneg (posneg i) j = posneg (i ∨ ~ j)

+-identityʳ : ∀ m → m + pos zero ≡ m
+-identityʳ = +-zeroʳ spos

sucℤ-+ʳ : ∀ m n → sucℤ (m + n) ≡ m + sucℤ n
sucℤ-+ʳ (signed _ zero) _ = refl
sucℤ-+ʳ (posneg _) _ = refl
sucℤ-+ʳ (pos (suc m)) n = cong sucℤ (sucℤ-+ʳ (pos m) n)
sucℤ-+ʳ (neg (suc m)) n =
  sucPredℤ (neg m + n) ∙∙
  sym (predSucℤ (neg m + n)) ∙∙
  cong predℤ (sucℤ-+ʳ (neg m) n)

-- I wonder if we could somehow use negEq to get this for free from the above...
predℤ-+ʳ : ∀ m n → predℤ (m + n) ≡ m + predℤ n
predℤ-+ʳ (signed _ zero) _ = refl
predℤ-+ʳ (posneg _) _ = refl
predℤ-+ʳ (neg (suc m)) n = cong predℤ (predℤ-+ʳ (neg m) n)
predℤ-+ʳ (pos (suc m)) n =
  predSucℤ (pos m + n) ∙∙
  sym (sucPredℤ (pos m + n)) ∙∙
  cong sucℤ (predℤ-+ʳ (pos m) n)

+-comm : ∀ m n → m + n ≡ n + m
+-comm (signed s zero) n = sym (+-zeroʳ s n)
+-comm (pos (suc m)) n = cong sucℤ  (+-comm (pos m) n) ∙ sucℤ-+ʳ  n (pos m)
+-comm (neg (suc m)) n = cong predℤ (+-comm (neg m) n) ∙ predℤ-+ʳ n (neg m)
+-comm (posneg i) n = lemma n i
  where
  -- get some help from:
  -- https://www.codewars.com/kata/reviews/5c878e3ef1abb10001e32eb1/groups/5cca3f9e840f4b0001d8ac98
  lemma : ∀ n → (λ i → (posneg i + n) ≡ (n + posneg i))
          [ sym (+-zeroʳ spos n) ≡ sym (+-zeroʳ sneg n) ]
  lemma (pos zero) i j = posneg (i ∧ j)
  lemma (pos (suc n)) i = cong sucℤ (lemma (pos n) i)
  lemma (neg zero) i j = posneg (i ∨ ~ j)
  lemma (neg (suc n)) i = cong predℤ (lemma (neg n) i)
  lemma (posneg i) j k = posneg ((i ∧ ~ k) ∨ (i ∧ j) ∨ (j ∧ k))

sucℤ-+ˡ : ∀ m n → sucℤ (m + n) ≡ sucℤ m + n
sucℤ-+ˡ (pos _) n = refl
sucℤ-+ˡ (neg zero) n = refl
sucℤ-+ˡ (neg (suc m)) n = sucPredℤ _
sucℤ-+ˡ (posneg _) n = refl

-- I wonder if we could somehow use negEq to get this for free from the above...
predℤ-+ˡ : ∀ m n → predℤ (m + n) ≡ predℤ m + n
predℤ-+ˡ (pos zero) n = refl
predℤ-+ˡ (pos (suc m)) n = predSucℤ _
predℤ-+ˡ (neg _) n = refl
predℤ-+ˡ (posneg _) n = refl

+-assoc : ∀ m n o → m + (n + o) ≡ m + n + o
+-assoc (signed s zero) n o = refl
+-assoc (posneg i) n o = refl
+-assoc (pos (suc m)) n o = cong sucℤ  (+-assoc (pos m) n o) ∙ sucℤ-+ˡ  (pos m + n) o
+-assoc (neg (suc m)) n o = cong predℤ (+-assoc (neg m) n o) ∙ predℤ-+ˡ (neg m + n) o

sucℤ-inj : ∀ m n → sucℤ m ≡ sucℤ n → m ≡ n
sucℤ-inj m n p = sym (predSucℤ m) ∙ cong predℤ p ∙ predSucℤ n

predℤ-inj : ∀ m n → predℤ m ≡ predℤ n → m ≡ n
predℤ-inj m n p = sym (sucPredℤ m) ∙ cong sucℤ p ∙ sucPredℤ n

+-injˡ : ∀ o m n → o + m ≡ o + n → m ≡ n
+-injˡ (signed _ zero) _ _ p = p
+-injˡ (posneg _)      _ _ p = p
+-injˡ (pos (suc o)) m n p = +-injˡ (pos o) m n (sucℤ-inj  _ _ p)
+-injˡ (neg (suc o)) m n p = +-injˡ (neg o) m n (predℤ-inj _ _ p)

+-injʳ : ∀ m n o → m + o ≡ n + o → m ≡ n
+-injʳ m n o p = +-injˡ o m n (+-comm o m ∙ p ∙ +-comm n o)

·-comm : ∀ m n → m · n ≡ n · m
·-comm m n i = signed (·S-comm (sign m) (sign n) i) (ℕ.·-comm (abs m) (abs n) i)

·-identityˡ : ∀ n → pos 1 · n ≡ n
·-identityˡ n = cong (signed (sign n)) (ℕ.+-zero (abs n)) ∙ signed-inv n

·-identityʳ : ∀ n → n · pos 1 ≡ n
·-identityʳ n = ·-comm n (pos 1) ∙ ·-identityˡ n

·-zeroˡ : ∀ {s} n → signed s zero · n ≡ signed s zero
·-zeroˡ _ = signed-zero _ _

·-zeroʳ : ∀ {s} n → n · signed s zero ≡ signed s zero
·-zeroʳ n = cong (signed _) (sym (ℕ.0≡m·0 (abs n))) ∙ signed-zero _ _

·-signed-pos : ∀ {s} m n → signed s m · pos n ≡ signed s (m ℕ.· n)
·-signed-pos {s} zero n = ·-zeroˡ {s} (pos n)
·-signed-pos {s} (suc m) n i = signed (·S-comm s (sign-pos n i) i) (suc m ℕ.· n)

-- this proof is why we defined ℤ using `signed` instead of `pos` and `neg`
-- based on that in: https://github.com/danr/Agda-Numerics
·-assoc : ∀ m n o → m · (n · o) ≡ m · n · o

·-assoc (signed s zero) n o =
  ·-zeroˡ (n · o)
·-assoc m@(signed _ (suc _)) (signed s zero) o =
  ·-zeroʳ {sign o} m ∙ signed-zero _ _ ∙ cong (_· o) (sym (·-zeroʳ {s} m))
·-assoc m@(signed _ (suc _)) n@(signed _ (suc _)) (signed s zero) =
  cong (m ·_) (·-zeroʳ {s} n) ∙ ·-zeroʳ {s} m ∙ sym (·-zeroʳ {s} (m · n))

·-assoc (signed sm (suc m)) (signed sn (suc n)) (signed so (suc o)) i =
  signed (·S-assoc sm sn so i) (ℕ.·-assoc (suc m) (suc n) (suc o) i)

·-assoc (posneg i) n o j =
  isSet→isSet' isSetℤ (·-assoc (pos zero) n o) (·-assoc (neg zero) n o)
                      (λ i → posneg i · (n · o)) (λ i → posneg i · n · o) i j
·-assoc m@(signed _ (suc _)) (posneg i) o j =
  isSet→isSet' isSetℤ (·-assoc m (pos zero) o) (·-assoc m (neg zero) o)
                      (λ i → m · (posneg i · o)) (λ i → m · posneg i · o) i j
·-assoc m@(signed _ (suc _)) n@(signed _ (suc _)) (posneg i) j =
  isSet→isSet' isSetℤ (·-assoc m n (pos zero)) (·-assoc m n (neg zero))
                      (λ i → m · (n · posneg i)) (λ i → m · n · posneg i) i j

negateSuc : ∀ n → - sucℤ n ≡ predℤ (- n)
negateSuc n i = - sucℤ (negate-invol n (~ i))

negatePred : ∀ n → - predℤ n ≡ sucℤ (- n)
negatePred n i = negate-invol (sucℤ (- n)) i

negate-+ : ∀ m n → - (m + n) ≡  (- m) + (- n)
negate-+ (signed _ zero) n = refl
negate-+ (posneg _)      n = refl
negate-+ (pos (suc m))   n = negateSuc  (pos m + n) ∙ cong predℤ (negate-+ (pos m) n)
negate-+ (neg (suc m))   n = negatePred (neg m + n) ∙ cong sucℤ  (negate-+ (neg m) n)

negate-·ˡ : ∀ m n → - (m · n) ≡ (- m) · n
negate-·ˡ (signed _ zero) n = signed-zero (not (sign n)) (sign n)
negate-·ˡ (signed ss (suc m)) n i = signed (not-·Sˡ ss (sign n) i) (suc m ℕ.· abs n)
negate-·ˡ (posneg i) n j =
  isSet→isSet' isSetℤ (signed-zero (not (sign n)) _) (signed-zero _ _)
                      refl (λ i → posneg (~ i) · n) i j

signed-distrib : ∀ s m n → signed s (m ℕ.+ n) ≡ signed s m + signed s n
signed-distrib s zero n = refl
signed-distrib spos (suc m) n = cong sucℤ  (signed-distrib spos m n)
signed-distrib sneg (suc m) n = cong predℤ (signed-distrib sneg m n)

·-pos-suc : ∀ m n → pos (suc m) · n ≡ n + pos m · n
·-pos-suc m n = signed-distrib (sign n) (abs n) (m ℕ.· abs n)
                ∙ (λ i → signed-inv n i + signed (sign-pos m (~ i) ·S sign n) (m ℕ.· abs n))

-- the below is based on that in: https://github.com/danr/Agda-Numerics

·-distribˡ-pos : ∀ o m n → (pos o · m) + (pos o · n) ≡ pos o · (m + n)
·-distribˡ-pos zero m n = signed-zero (sign n) (sign (m + n))
·-distribˡ-pos (suc o) m n =
  pos (suc o) · m + pos (suc o) · n ≡[ i ]⟨ ·-pos-suc o m i + ·-pos-suc o n i ⟩
  m + pos o · m + (n + pos o · n)   ≡⟨ +-assoc (m + pos o · m) n (pos o · n) ⟩
  m + pos o · m + n + pos o · n     ≡[ i ]⟨ +-assoc m (pos o · m) n (~ i) + pos o · n ⟩
  m + (pos o · m + n) + pos o · n   ≡[ i ]⟨ m + +-comm (pos o · m) n i + pos o · n ⟩
  m + (n + pos o · m) + pos o · n   ≡[ i ]⟨ +-assoc m n (pos o · m) i + pos o · n ⟩
  m + n + pos o · m + pos o · n     ≡⟨ sym (+-assoc (m + n) (pos o · m) (pos o · n)) ⟩
  m + n + (pos o · m + pos o · n)   ≡⟨ cong ((m + n) +_) (·-distribˡ-pos o m n) ⟩
  m + n + pos o · (m + n)           ≡⟨ sym (·-pos-suc o (m + n)) ⟩
  pos (suc o) · (m + n) ∎

·-distribˡ-neg : ∀ o m n → (neg o · m) + (neg o · n) ≡ neg o · (m + n)
·-distribˡ-neg o m n =
     neg o · m  +    neg o · n  ≡[ i ]⟨ negate-·ˡ (pos o) m (~ i) + negate-·ˡ (pos o) n (~ i) ⟩
  - (pos o · m) + - (pos o · n) ≡⟨ sym (negate-+ (pos o · m) (pos o · n)) ⟩
  - (pos o · m + pos o · n)     ≡⟨ cong -_ (·-distribˡ-pos o m n) ⟩
  - (pos o · (m + n))           ≡⟨ negate-·ˡ (pos o) (m + n) ⟩
     neg o · (m + n)            ∎

·-distribˡ : ∀ o m n → (o · m) + (o · n) ≡ o · (m + n)
·-distribˡ (pos o) m n = ·-distribˡ-pos o m n
·-distribˡ (neg o) m n = ·-distribˡ-neg o m n
·-distribˡ (posneg i) m n j =
  isSet→isSet' isSetℤ (·-distribˡ-pos zero m n) (·-distribˡ-neg zero m n)
                      (λ i → posneg i · n) (λ i → posneg i · (m + n)) i j

·-distribʳ : ∀ m n o → (m · o) + (n · o) ≡ (m + n) · o
·-distribʳ m n o = (λ i → ·-comm m o i + ·-comm n o i) ∙ ·-distribˡ o m n ∙ ·-comm o (m + n)

sign-pos-suc-· : ∀ m n → sign (pos (suc m) · n) ≡ sign n
sign-pos-suc-· m (signed s zero) = sign-pos (suc m ℕ.· zero)
sign-pos-suc-· m (posneg i)      = sign-pos (suc m ℕ.· zero)
sign-pos-suc-· m (signed s (suc n)) = refl

·-injˡ : ∀ o m n → pos (suc o) · m ≡ pos (suc o) · n → m ≡ n
·-injˡ o m n p = sym (signed-inv m) ∙ (λ i → signed (sign-eq i) (abs-eq i)) ∙ signed-inv n
  where sign-eq = sym (sign-pos-suc-· o m) ∙ cong sign p ∙ sign-pos-suc-· o n
        abs-eq = ℕ.inj-sm· {o} (cong abs p)

·-injʳ : ∀ m n o → m · pos (suc o) ≡ n · pos (suc o) → m ≡ n
·-injʳ m n o p = ·-injˡ o m n (·-comm (pos (suc o)) m ∙ p ∙ ·-comm n (pos (suc o)))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
{-# OPTIONS --without-K #-}
module Model.Type where

open import Model.Exponential public
open import Model.Nat public
open import Model.Product public
open import Model.Terminal public
open import Model.Type.Core public
open import Model.Stream public
open import Model.Quantification public

open import Model.Size as MS using
  ( ≤-IsProp ; ⟦_⟧Δ ; ⟦_⟧n ; ⟦_⟧σ )
open import Source.Size.Substitution.Theory
open import Source.Size.Substitution.Universe as SS using (Sub⊢ᵤ ; ⟨_⟩)
open import Util.Prelude hiding (id ; _∘_ ; _×_ ; ⊤)

import Source.Size as SS
import Source.Type as ST

open MS._≤_

⟦_⟧T : ∀ {Δ} (T : ST.Type Δ) → ⟦Type⟧ ⟦ Δ ⟧Δ
⟦ ST.Nat n ⟧T = subT ⟦ n ⟧n Nat
⟦ ST.Stream n ⟧T = subT ⟦ n ⟧n Stream
⟦ T ST.⇒ U ⟧T = ⟦ T ⟧T ↝ ⟦ U ⟧T
⟦ ST.Π n , T ⟧T = ⟦∀⟧ n ⟦ T ⟧T

⟦_⟧Γ : ∀ {Δ} (Γ : ST.Ctx Δ) → ⟦Type⟧ ⟦ Δ ⟧Δ
⟦ ST.[] ⟧Γ = ⊤
⟦ Γ ST.∙ T ⟧Γ = ⟦ Γ ⟧Γ × ⟦ T ⟧T

⇒-resp-≈⟦Type⟧ : ∀ {Γ} {T T′ U U′ : ⟦Type⟧ Γ}
  → T ≈⟦Type⟧ T′
  → U ≈⟦Type⟧ U′
  → T ⇒ U
  → T′ ⇒ U′
⇒-resp-≈⟦Type⟧ T≈T′ U≈U′ f = U≈U′ .forth ∘ f ∘ T≈T′ .back

⟦subT⟧ : ∀ {Δ Ω σ} (⊢σ : σ ∶ Δ ⇒ᵤ Ω) T
  → ⟦ T [ σ ]ᵤ ⟧T ≈⟦Type⟧ subT ⟦ ⊢σ ⟧σ ⟦ T ⟧T
⟦subT⟧ ⊢σ (ST.Nat n) = record
  { forth = record
    { fobj = castℕ≤ (reflexive (MS.⟦sub⟧ ⊢σ n))
    ; feq = λ γ≈γ′ m≡m → m≡m
    }
  ; back = record
    { fobj = castℕ≤ (reflexive (sym (MS.⟦sub⟧ ⊢σ n)))
    ; feq = λ γ≈γ′ m≡m → m≡m
    }
  ; back-forth = ≈⁺ λ γ x → ℕ≤-≡⁺ _ _ refl
  ; forth-back = ≈⁺ λ γ x → ℕ≤-≡⁺ _ _ refl
  }
⟦subT⟧ ⊢σ (ST.Stream n) = record
  { forth = record
    { fobj = castColist (reflexive (sym (MS.⟦sub⟧ ⊢σ n)))
    ; feq = λ γ≈γ′ xs≈ys a a₁ a₂ → xs≈ys _ _ _
    }
  ; back = record
    { fobj = castColist (reflexive (MS.⟦sub⟧ ⊢σ n))
    ; feq = λ γ≈γ′ xs≈ys a a₁ a₂ → xs≈ys _ _ _
    }
  ; back-forth = ≈⁺ λ γ xs → Colist-≡⁺ λ m m≤n → cong (xs m) (≤-IsProp _ _)
  ; forth-back = ≈⁺ λ γ xs → Colist-≡⁺ λ m m≤n → cong (xs m) (≤-IsProp _ _)
  }
⟦subT⟧ {Δ} {Ω} {σ} ⊢σ (T ST.⇒ U)
  = ≈⟦Type⟧-trans (↝-resp-≈⟦Type⟧ _ _ _ _ (⟦subT⟧ ⊢σ T) (⟦subT⟧ ⊢σ U))
      (subT-↝ ⟦ ⊢σ ⟧σ ⟦ T ⟧T ⟦ U ⟧T)
⟦subT⟧ {Δ} {Ω} {σ} ⊢σ (ST.Π n , T)
  = ≈⟦Type⟧-trans (⟦∀⟧-resp-≈⟦Type⟧ (n [ σ ]ᵤ) (⟦subT⟧ (SS.Lift ⊢σ refl) T))
      (subT-⟦∀⟧ ⊢σ ⟦ T ⟧T)

⟦subΓ⟧ : ∀ {Δ Ω σ} (⊢σ : σ ∶ Δ ⇒ᵤ Ω) Γ
  → ⟦ Γ [ σ ]ᵤ ⟧Γ ≈⟦Type⟧ subT ⟦ ⊢σ ⟧σ ⟦ Γ ⟧Γ
⟦subΓ⟧ σ ST.[] = record
  { forth = record { fobj = λ x → x ; feq = λ γ≈γ′ x → x }
  ; back = record { fobj = λ x → x ; feq = λ γ≈γ′ x → x }
  ; back-forth = ≈⁺ λ γ x → refl
  ; forth-back = ≈⁺ λ γ x → refl
  }
⟦subΓ⟧ σ (Γ ST.∙ T) = ×-resp-≈⟦Type⟧ (⟦subΓ⟧ σ Γ) (⟦subT⟧ σ T)

subₛ
  : ∀ {Δ Ω σ Γ T}
  → (⊢σ : σ ∶ Δ ⇒ᵤ Ω)
  → ⟦ Γ ⟧Γ ⇒ ⟦ T ⟧T
  → ⟦ Γ [ σ ]ᵤ ⟧Γ ⇒ ⟦ T [ σ ]ᵤ ⟧T
subₛ {Γ = Γ} {T} ⊢σ f
  = ⟦subT⟧ ⊢σ T .back ∘ subt ⟦ ⊢σ ⟧σ f ∘ ⟦subΓ⟧ ⊢σ Γ .forth

≡→≈⟦Type⟧Γ : ∀ {Δ} {Γ Ψ : ST.Ctx Δ}
  → Γ ≡ Ψ
  → ⟦ Γ ⟧Γ ≈⟦Type⟧ ⟦ Ψ ⟧Γ
≡→≈⟦Type⟧Γ p = ≡→≈⟦Type⟧ (cong ⟦_⟧Γ p)

≡→≈⟦Type⟧T : ∀ {Δ} {T U : ST.Type Δ}
  → T ≡ U
  → ⟦ T ⟧T ≈⟦Type⟧ ⟦ U ⟧T
≡→≈⟦Type⟧T p = ≡→≈⟦Type⟧ (cong ⟦_⟧T p)

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
open import Function using ( _∘_ )
open import Data.Product using ( ∃ ; _×_ ; _,_ )
open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ )
open import Data.Empty using ( ⊥ ; ⊥-elim )
open import Data.Nat using ( ℕ ; zero ; suc ) renaming ( _+_ to _+ℕ_ ; _≤_ to _≤ℕ_ )
open import Relation.Binary.PropositionalEquality using
  ( _≡_ ; _≢_ ; refl ; sym ; cong ; cong₂ ; subst₂ ; inspect ; [_] )
open import Relation.Nullary using ( ¬_ ; Dec ; yes ; no )
open import FRP.LTL.Util using ( _trans_ ; _∋_ ; m+n≡0-impl-m≡0 ; ≤0-impl-≡0 ; 1+n≰n )
  renaming ( +-comm to +ℕ-comm ; +-assoc to +ℕ-assoc )

open Relation.Binary.PropositionalEquality.≡-Reasoning using ( begin_ ; _≡⟨_⟩_ ; _∎ )

module FRP.LTL.Time where

infix 2 _≤_ _≥_ _≰_ _≱_ _<_ _>_
infixr 4 _,_
infixr 5 _≤-trans_ _<-transˡ_ _<-transʳ_ _≤-asym_ _≤-total_
infixl 6 _+_ _∸_

-- Time has a cancellative action _+_ which respects the monoid structure of ℕ

postulate

  Time : Set
  _+_ : Time → ℕ → Time

  +-unit : ∀ t → (t + 0 ≡ t)
  +-assoc : ∀ t m n → ((t + m) + n ≡ t + (m +ℕ n))
  +-cancelˡ : ∀ t {m n} → (t + m ≡ t + n) → (m ≡ n)
  +-cancelʳ : ∀ {s t} n → (s + n ≡ t + n) → (s ≡ t)

-- The order on time is derived from +

data _≤_ (t u : Time) : Set where
  _,_ : ∀ n → (t + n ≡ u) → (t ≤ u)

-- Floored subtraction t ∸ u is the smallest n such that t ≤ u + n

postulate

  _∸_ : Time → Time → ℕ
  t≤u+t∸u : ∀ {t u} → (t ≤ u + (t ∸ u))
  ∸-min : ∀ {t u n} → (t ≤ u + n) → (t ∸ u ≤ℕ n)

-- End of postulates.

suc-cancelʳ : ∀ {t u m n} → (t + suc m ≡ u + suc n) → (t + m ≡ u + n)
suc-cancelʳ {t} {u} {m} {n} t+1+m≡u+1+n =
  +-cancelʳ 1
    (+-assoc t m 1 trans
      cong₂ _+_ refl (+ℕ-comm m 1) trans
        t+1+m≡u+1+n trans
          cong₂ _+_ refl (+ℕ-comm 1 n) trans
            sym (+-assoc u n 1))

-- Syntax sugar for ≤

_≥_ : Time → Time → Set
t ≥ u = u ≤ t

_≰_ :  Time → Time → Set
t ≰ u = ¬(t ≤ u)

_≱_ :  Time → Time → Set
t ≱ u = u ≰ t

_<_ : Time → Time → Set
t < u = (t ≤ u) × (u ≰ t)

_>_ : Time → Time → Set
t > u = u < t

-- ≤ is a decidable total order

≤-refl : ∀ {t} → (t ≤ t)
≤-refl {t} = (0 , +-unit t)

_≤-trans_ : ∀ {t u v} → (t ≤ u) → (u ≤ v) → (t ≤ v)
_≤-trans_ {t} {u} {v} (m , t+m≡u) (n , u+n≡v) =
  (m +ℕ n , (sym (+-assoc t m n)) trans (cong₂ _+_ t+m≡u refl) trans u+n≡v)

≡-impl-≤ : ∀ {t u} → (t ≡ u) → (t ≤ u)
≡-impl-≤ refl = ≤-refl

≡-impl-≥ : ∀ {t u} → (t ≡ u) → (t ≥ u)
≡-impl-≥ refl = ≤-refl

_≤-asym_ : ∀ {t u} → (t ≤ u) → (u ≤ t) → (t ≡ u)
(m , t+m≡u) ≤-asym (n , u+n≡t) =
  sym (+-unit _) trans cong₂ _+_ refl (sym m≡0) trans t+m≡u where

  m≡0 : m ≡ 0
  m≡0 = m+n≡0-impl-m≡0 m n (+-cancelˡ _
    (sym (+-assoc _ m n) trans
      cong₂ _+_ t+m≡u refl trans
        u+n≡t trans sym (+-unit _)))

≤-impl-∸≡0 : ∀ {t u} → (t ≤ u) → (t ∸ u ≡ 0)
≤-impl-∸≡0 t≤u with (∸-min (t≤u ≤-trans ≡-impl-≤ (sym (+-unit _))))
≤-impl-∸≡0 t≤u | t∸u≤0 = ≤0-impl-≡0 t∸u≤0

∸≡0-impl-≤ : ∀ {t u} → (t ∸ u ≡ 0) → (t ≤ u)
∸≡0-impl-≤ t∸u≡0 = t≤u+t∸u ≤-trans ≡-impl-≤ (cong₂ _+_ refl t∸u≡0 trans +-unit _)

∸≢0-impl-≰ : ∀ {t u n} → (t ∸ u ≡ suc n) → (t ≰ u)
∸≢0-impl-≰ t∸u≡1+n t≤u
  with sym t∸u≡1+n trans ≤0-impl-≡0 (∸-min (t≤u ≤-trans ≡-impl-≤ (sym (+-unit _))))
∸≢0-impl-≰ t∸u≡1+n t≤u
  | ()

t∸u≢0-impl-u∸t≡0 : ∀ t u {n} → (t ∸ u ≡ suc n) → (u ∸ t ≡ 0)
t∸u≢0-impl-u∸t≡0 t u {n} t∸u≡1+n with t≤u+t∸u {t} {u}
t∸u≢0-impl-u∸t≡0 t u {n} t∸u≡1+n | (zero , t+0≡u+t∸u) =
  ≤-impl-∸≡0 (t ∸ u , sym t+0≡u+t∸u trans +-unit t)
t∸u≢0-impl-u∸t≡0 t u {n} t∸u≡1+n | (suc m , t+1+m≡u+t∸u) =
  ⊥-elim (1+n≰n n (subst₂ _≤ℕ_ t∸u≡1+n refl
    (∸-min (m , suc-cancelʳ (t+1+m≡u+t∸u trans cong₂ _+_ refl t∸u≡1+n)))))

_≤-total_ : ∀ t u → (t ≤ u) ⊎ (u < t)
t ≤-total u with t ∸ u | inspect (_∸_ t) u
t ≤-total u | zero  | [ t∸u≡0 ] = inj₁ (∸≡0-impl-≤ t∸u≡0)
t ≤-total u | suc n | [ t∸u≡1+n ] with t∸u≢0-impl-u∸t≡0 t u t∸u≡1+n
t ≤-total u | suc n | [ t∸u≡1+n ] | u∸t≡0 = inj₂ (∸≡0-impl-≤ u∸t≡0 , ∸≢0-impl-≰ t∸u≡1+n)

-- Case analysis on ≤

data _≤-Case_ (t u : Time) : Set where
  lt : .(t < u) → (t ≤-Case u)
  eq : .(t ≡ u) → (t ≤-Case u)
  gt : .(u < t) → (t ≤-Case u)

_≤-case_ : ∀ t u → (t ≤-Case u)
t ≤-case u with (t ∸ u) | inspect (_∸_ t) u | u ∸ t | inspect (_∸_ u) t
t ≤-case u | zero  | [ t∸u≡0 ]   | zero   | [ u∸t≡0 ] = eq (∸≡0-impl-≤ t∸u≡0 ≤-asym ∸≡0-impl-≤ u∸t≡0)
t ≤-case u | suc n | [ t∸u≡1+n ] | zero   | [ u∸t≡0 ] = gt (∸≡0-impl-≤ u∸t≡0 , ∸≢0-impl-≰ t∸u≡1+n)
t ≤-case u | zero  | [ t∸u≡0 ]   | suc w₁ | [ u∸t≡1+n ] = lt (∸≡0-impl-≤ t∸u≡0 , ∸≢0-impl-≰ u∸t≡1+n)
t ≤-case u | suc m | [ t∸u≡1+m ] | suc n  | [ u∸t≡1+n ] with sym u∸t≡1+n trans t∸u≢0-impl-u∸t≡0 t u t∸u≡1+m
t ≤-case u | suc m | [ t∸u≡1+m ] | suc n  | [ u∸t≡1+n ] | ()

-- + is monotone

+-resp-≤ : ∀ {t u} → (t ≤ u) → ∀ n → (t + n ≤ u + n)
+-resp-≤ (m , t+m≡u) n =
  ( m
  , +-assoc _ n m trans
      cong₂ _+_ refl (+ℕ-comm n m) trans
        sym (+-assoc _ m n) trans
          cong₂ _+_ t+m≡u refl )

+-refl-≤ : ∀ {t u} n → (t + n ≤ u + n) → (t ≤ u)
+-refl-≤ n (m , t+n+m≡u+n) =
  ( m
  , +-cancelʳ n
    (+-assoc _ m n trans
      cong₂ _+_ refl (+ℕ-comm m n) trans
        sym (+-assoc _ n m) trans
          t+n+m≡u+n) )

-- Lemmas about <

<-impl-≤ : ∀ {t u} → (t < u) → (t ≤ u)
<-impl-≤ (t≤u , u≰t) = t≤u

<-impl-≱ : ∀ {t u} → (t < u) → (u ≰ t)
<-impl-≱ (t≤u , u≰t) = u≰t

_<-transˡ_ : ∀ {t u v} → (t < u) → (u ≤ v) → (t < v)
_<-transˡ_ (t≤u , u≰t) u≤v = (t≤u ≤-trans u≤v , λ v≤t → u≰t (u≤v ≤-trans v≤t))

_<-transʳ_ : ∀ {t u v} → (t ≤ u) → (u < v) → (t < v)
_<-transʳ_ t≤u (u≤v , v≰u) = (t≤u ≤-trans u≤v , λ v≤t → v≰u (v≤t ≤-trans t≤u))

≤-proof-irrel′ : ∀ {t u m n} → (m ≡ n) → (t+m≡u : t + m ≡ u) → (t+n≡u : t + n ≡ u) →
  (t ≤ u) ∋ (m , t+m≡u) ≡ (n , t+n≡u)
≤-proof-irrel′ refl refl refl = refl

t≤t+1 : ∀ {t} → (t ≤ t + 1)
t≤t+1 = (1 , refl)

t≱t+1 : ∀ {t} → (t ≱ t + 1)
t≱t+1 {t} (m , t+1+m≡t) with +-cancelˡ t (sym (+-assoc t 1 m) trans t+1+m≡t trans sym (+-unit t))
t≱t+1 (m , t+1+m≡t) | ()

t<t+1 : ∀ {t} → (t < t + 1)
t<t+1 = (t≤t+1 , t≱t+1)

<-impl-+1≤ : ∀ {t u} → (t < u) → (t + 1 ≤ u)
<-impl-+1≤ {t} ((zero  , t+0≡u)   , u≰t) = ⊥-elim (u≰t (≡-impl-≥ (sym (+-unit t) trans t+0≡u)))
<-impl-+1≤ {t} ((suc n , t+1+n≡u) , u≰t) = (n , +-assoc t 1 n trans t+1+n≡u)

+-resp-< : ∀ {t u} → (t < u) → ∀ n → (t + n < u + n)
+-resp-< (t≤u , t≱u) n = (+-resp-≤ t≤u n , λ u+n≤t+n → t≱u (+-refl-≤ n u+n≤t+n))

-- Proof irrelevance for ≤

≤-proof-irrel : ∀ {t u} → (p q : t ≤ u) → (p ≡ q)
≤-proof-irrel {t} (m , t+m≡u) (n , t+n≡u) =
  ≤-proof-irrel′ (+-cancelˡ t (t+m≡u trans (sym t+n≡u))) t+m≡u t+n≡u

-- Well ordering of < on an interval

_≮[_]_ : Time → ℕ → Time → Set
s ≮[ zero  ] u = ⊥
s ≮[ suc n ] u = ∀ {t} → (s ≤ t) → (t < u) → (s ≮[ n ] t)

<-wo′ : ∀ n {s u} → (s ≤ u) → (u ≤ s + n) → (s ≮[ suc n ] u)
<-wo′ zero {s} s≤u u≤s+0 s≤t t<u =
  <-impl-≱ t<u (u≤s+0 ≤-trans ≡-impl-≤ (+-unit s) ≤-trans s≤t)
<-wo′ (suc n) s≤u u≤s+1+n {t} s≤t ((zero , t+0≡u) , t≱u) =
  ⊥-elim (t≱u (≡-impl-≤ ((sym t+0≡u) trans (+-unit t))))
<-wo′ (suc n) {s} {u} s≤u (l , u+l≡s+1+n) {t} s≤t ((suc m , t+1+m≡u) , t≱u) =
  <-wo′ n s≤t (l +ℕ m , suc-cancelʳ t+1+l+m≡s+1+n) where
    t+1+l+m≡s+1+n : t + suc (l +ℕ m) ≡ s + suc n
    t+1+l+m≡s+1+n =
      cong₂ _+_ refl (cong suc (+ℕ-comm l m)) trans
        sym (+-assoc t (1 +ℕ m) l) trans
          cong₂ _+_ t+1+m≡u refl trans
            u+l≡s+1+n

<-wo : ∀ {s u} → (s ≤ u) → ∃ λ n → (s ≮[ n ] u)
<-wo (n , s+n≡u) = (suc n , λ {t} → <-wo′ n (n , s+n≡u) (≡-impl-≤ (sym s+n≡u)) {t})

max_stars_repo_name: agda/agda-frp-ltl

max_issues_repo_name: agda/agda-frp-ltl

max_forks_repo_name: agda/agda-frp-ltl


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.Equality {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open import MLib.Matrix.Core

import Relation.Binary.Indexed as I

module S = Struct struct renaming (Carrier to S; _≈_ to _≈′_)
open S hiding (isEquivalence; setoid; refl; sym; trans) public

module _ {m n} where

  -- Pointwise equality --

  infix 4 _≈_

  _≈_ : Rel (Matrix S m n) _
  A ≈ B = ∀ i j → A i j ≈′ B i j

  isEquivalence : IsEquivalence _≈_
  isEquivalence = record { Proofs } where
    module Proofs where
      refl : Reflexive _≈_
      refl _ _ = S.refl

      sym : Symmetric _≈_
      sym p = λ i j → S.sym (p i j)

      trans : Transitive _≈_
      trans p q = λ i j → S.trans (p i j) (q i j)

  setoid : Setoid _ _
  setoid = record { isEquivalence = isEquivalence }

  open Setoid setoid public using (refl; sym; trans)

  module FunctionProperties = Algebra.FunctionProperties _≈_

-- Size-heterogeneous pointwise equality

infix 4 _≃_

record _≃_ {m n p q} (A : Matrix S m n) (B : Matrix S p q) : Set (c ⊔ˡ ℓ) where
  field
    m≡p : m ≡ p
    n≡q : n ≡ q
    equal : ∀ {i i′ j j′} → i ≅ i′ → j ≅ j′ → A i j ≈′ B i′ j′

open _≃_

≃-refl : ∀ {m n} {A : Matrix S m n} → A ≃ A
≃-refl .m≡p = ≡.refl
≃-refl .n≡q = ≡.refl
≃-refl .equal ≅.refl ≅.refl = S.refl

≃-trans :
  ∀ {m n p q r s} {A : Matrix S m n} {B : Matrix S p q} {C : Matrix S r s} →
  A ≃ B → B ≃ C → A ≃ C
≃-trans x y .m≡p = ≡.trans (x .m≡p) (y .m≡p)
≃-trans x y .n≡q = ≡.trans (x .n≡q) (y .n≡q)
≃-trans {m} {n} {p} {q} {r} {s} x y .equal i≅i′′ j≅j′′ =
  let i≅i′ = ≅.sym (≅.≡-subst-removable Fin (x .m≡p) _)
      i′≅i′′ = ≅.trans (≅.sym i≅i′) i≅i′′
      j≅j′ = ≅.sym (≅.≡-subst-removable Fin (x .n≡q) _)
      j′≅j′′ = ≅.trans (≅.sym j≅j′) j≅j′′
  in S.trans (x .equal i≅i′ j≅j′) (y .equal i′≅i′′ j′≅j′′)

≃-sym :
  ∀ {m n p q} {A : Matrix S m n} {B : Matrix S p q} →
  A ≃ B → B ≃ A
≃-sym A≃B .m≡p = ≡.sym (A≃B .m≡p)
≃-sym A≃B .n≡q = ≡.sym (A≃B .n≡q)
≃-sym A≃B .equal i≅i′ j≅j′ = S.sym (A≃B .equal (≅.sym i≅i′) (≅.sym j≅j′))

≃-setoid : I.Setoid (ℕ × ℕ) _ _
≃-setoid = record
  { Carrier = uncurry (Matrix S)
  ; _≈_ = _≃_
  ; isEquivalence = record
    { refl = ≃-refl
    ; sym = ≃-sym
    ; trans = ≃-trans
    }
  }

≡-subst-≃₁ : ∀ {m n p} {A : Matrix S m n} (m≡p : m ≡ p) → ≡.subst (λ h → Matrix S h n) m≡p A ≃ A
≡-subst-≃₁ ≡.refl = ≃-refl

≡-subst-≃₂ : ∀ {m n q} {A : Matrix S m n} (n≡q : n ≡ q) → ≡.subst (Matrix S m) n≡q A ≃ A
≡-subst-≃₂ ≡.refl = ≃-refl


text:
module Type.Identity.Heterogenous where

import      Lvl
open import Type

data HId {ℓ} : ∀{A : Type{ℓ}}{B : Type{ℓ}} → A → B → Type{Lvl.𝐒(ℓ)} where
  instance intro : ∀{T : Type{ℓ}}{x : T} → HId x x

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Data.Sigma.Properties where

open import Prelude hiding (B; C)
open import Cubical.Foundations.HLevels using (isOfHLevelΣ) public
open import Cubical.Data.Sigma.Properties using (Σ≡Prop) public

private
  variable
    B : A → Type b
    C : Σ A B → Type c

reassoc : Σ (Σ A B) C ⇔ Σ[ x ⦂ A ] × Σ[ y ⦂ B x ] × C (x , y)
reassoc .fun       ((x , y) , z)    = x , (y , z)
reassoc .inv       (x , (y , z))    = (x , y) , z
reassoc .leftInv   ((x , y) , z) i  = ((x , y) , z)
reassoc .rightInv  (x , (y , z)) i  = (x , (y , z))

≃ΣProp≡ : ∀ {A : Type a} {u} {U : A → Type u} → ((x : A) → isProp (U x)) → {p q : Σ A U} → (p ≡ q) ≃ (fst p ≡ fst q)
≃ΣProp≡ {A = A} {U = U} pA {p} {q} = isoToEquiv (iso to fro (λ _ → refl) (J Jt Jp))
  where
  to : {p q : Σ A U} → p ≡ q → fst p ≡ fst q
  to = cong fst

  fro : ∀ {p q} → fst p ≡ fst q → p ≡ q
  fro = Σ≡Prop pA

  Jt : (q : Σ A U) → p ≡ q → Type _
  Jt q q≡ = fro (to q≡) ≡ q≡

  Jp : Jt p refl
  Jp i j .fst = p .fst
  Jp i j .snd = isProp→isSet (pA (p .fst)) (p .snd) (p .snd) (λ k → fro {p} {p} (to (refl {x = p})) k .snd) refl i j

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import lib.Basics
open import lib.types.Pi

module lib.types.Group where

record GroupStructure {i} (El : Type i) --(El-level : has-level 0 El)
  : Type i where
  constructor group-structure
  field
    ident : El
    inv : El → El
    comp : El → El → El
    unitl : ∀ a → comp ident a == a
    unitr : ∀ a → comp a ident == a
    assoc   : ∀ a b c → comp (comp a b) c == comp a (comp b c)
    invl    : ∀ a → (comp (inv a) a) == ident
    invr    : ∀ a → (comp a (inv a)) == ident

record Group i : Type (lsucc i) where
  constructor group
  field
    El : Type i
    El-level : has-level 0 El
    group-struct : GroupStructure El
  open GroupStructure group-struct public

  ⊙El : Σ (Type i) (λ A → A)
  ⊙El = (El , ident)

Group₀ : Type (lsucc lzero)
Group₀ = Group lzero

is-abelian : ∀ {i} → Group i → Type i
is-abelian G = (a b : Group.El G) → Group.comp G a b == Group.comp G b a

module _ where
  open GroupStructure

  abstract
    group-structure= : ∀ {i} {A : Type i} (pA : has-level 0 A)
      {id₁ id₂ : A} {inv₁ inv₂ : A → A} {comp₁ comp₂ : A → A → A}
      → ∀ {unitl₁ unitl₂} → ∀ {unitr₁ unitr₂} → ∀ {assoc₁ assoc₂}
      → ∀ {invr₁ invr₂} → ∀ {invl₁ invl₂}
      → (id₁ == id₂) → (inv₁ == inv₂) → (comp₁ == comp₂)
      → Path {A = GroupStructure A}
          (group-structure id₁ inv₁ comp₁ unitl₁ unitr₁ assoc₁ invl₁ invr₁)
          (group-structure id₂ inv₂ comp₂ unitl₂ unitr₂ assoc₂ invl₂ invr₂)
    group-structure= pA {id₁ = id₁} {inv₁ = inv₁} {comp₁ = comp₁} idp idp idp =
      ap5 (group-structure id₁ inv₁ comp₁)
        (prop-has-all-paths (Π-level (λ _ → pA _ _)) _ _)
        (prop-has-all-paths (Π-level (λ _ → pA _ _)) _ _)
        (prop-has-all-paths
          (Π-level (λ _ → Π-level (λ _ → Π-level (λ _ → pA _ _)))) _ _)
        (prop-has-all-paths (Π-level (λ _ → pA _ _)) _ _)
        (prop-has-all-paths (Π-level (λ _ → pA _ _)) _ _)
      where
      ap5 : ∀ {j} {C D E F G H : Type j}
        {c₁ c₂ : C} {d₁ d₂ : D} {e₁ e₂ : E} {f₁ f₂ : F} {g₁ g₂ : G}
        (f : C → D → E → F → G → H)
        → (c₁ == c₂) → (d₁ == d₂) → (e₁ == e₂) → (f₁ == f₂) → (g₁ == g₂)
        → f c₁ d₁ e₁ f₁ g₁ == f c₂ d₂ e₂ f₂ g₂
      ap5 f idp idp idp idp idp = idp

    ↓-group-structure= : ∀ {i} {A B : Type i}
      (A-level : has-level 0 A)
      {GS : GroupStructure A} {HS : GroupStructure B} (p : A == B)
      → (ident GS == ident HS [ (λ C → C) ↓ p ])
      → (inv GS == inv HS [ (λ C → C → C) ↓ p ])
      → (comp GS == comp HS [ (λ C → C → C → C) ↓ p ])
      → GS == HS [ GroupStructure ↓ p ]
    ↓-group-structure= A-level idp = group-structure= A-level

module _ {i} (G : Group i) where
  private
    open Group G
    infix 80 _⊙_
    _⊙_ = comp

  group-inv-unique-l : (g h : El) → (g ⊙ h == ident) → inv h == g
  group-inv-unique-l g h p =
    inv h              =⟨ ! (unitl (inv h)) ⟩
    ident ⊙ inv h      =⟨ ! p |in-ctx (λ w → w ⊙ inv h) ⟩
    (g ⊙ h) ⊙ inv h    =⟨ assoc g h (inv h) ⟩
    g ⊙ (h ⊙ inv h)    =⟨ invr h |in-ctx (λ w → g ⊙ w) ⟩
    g ⊙ ident          =⟨ unitr g ⟩
    g                     ∎

  group-inv-unique-r : (g h : El) → (g ⊙ h == ident) → inv g == h
  group-inv-unique-r g h p =
    inv g              =⟨ ! (unitr (inv g)) ⟩
    inv g ⊙ ident      =⟨ ! p |in-ctx (λ w → inv g ⊙ w) ⟩
    inv g ⊙ (g ⊙ h)    =⟨ ! (assoc (inv g) g h) ⟩
    (inv g ⊙ g) ⊙ h    =⟨ invl g |in-ctx (λ w → w ⊙ h) ⟩
    ident ⊙ h          =⟨ unitl h ⟩
    h                     ∎

  group-inv-ident : inv ident == ident
  group-inv-ident =
    group-inv-unique-l ident ident (unitl ident)

  group-inv-comp : (g₁ g₂ : El) → inv (g₁ ⊙ g₂) == inv g₂ ⊙ inv g₁
  group-inv-comp g₁ g₂ =
    group-inv-unique-r (g₁ ⊙ g₂) (inv g₂ ⊙ inv g₁) $
      (g₁ ⊙ g₂) ⊙ (inv g₂ ⊙ inv g₁)
        =⟨ assoc g₁ g₂ (inv g₂ ⊙ inv g₁) ⟩
      g₁ ⊙ (g₂ ⊙ (inv g₂ ⊙ inv g₁))
        =⟨ ! (assoc g₂ (inv g₂) (inv g₁)) |in-ctx (λ w → g₁ ⊙ w) ⟩
      g₁ ⊙ ((g₂ ⊙ inv g₂) ⊙ inv g₁)
        =⟨ invr g₂ |in-ctx (λ w → g₁ ⊙ (w ⊙ inv g₁)) ⟩
      g₁ ⊙ (ident ⊙ inv g₁)
        =⟨ unitl (inv g₁) |in-ctx (λ w → g₁ ⊙ w) ⟩
      g₁ ⊙ inv g₁
        =⟨ invr g₁ ⟩
      ident ∎

  group-inv-inv : (g : El) → inv (inv g) == g
  group-inv-inv g = group-inv-unique-r (inv g) g (invl g)

  group-cancel-l : (g : El) {h k : El} → g ⊙ h == g ⊙ k → h == k
  group-cancel-l g {h} {k} p =
    h                  =⟨ ! (unitl h) ⟩
    ident ⊙ h          =⟨ ap (λ w → w ⊙ h) (! (invl g)) ⟩
    (inv g ⊙ g) ⊙ h    =⟨ assoc (inv g) g h ⟩
    inv g ⊙ (g ⊙ h)    =⟨ ap (λ w → inv g ⊙ w) p ⟩
    inv g ⊙ (g ⊙ k)    =⟨ ! (assoc (inv g) g k) ⟩
    (inv g ⊙ g) ⊙ k    =⟨ ap (λ w → w ⊙ k) (invl g) ⟩
    ident ⊙ k          =⟨ unitl k ⟩
    k ∎

  group-cancel-r : (g : El) {h k : El} → h ⊙ g == k ⊙ g → h == k
  group-cancel-r g {h} {k} p =
    h                  =⟨ ! (unitr h) ⟩
    h ⊙ ident          =⟨ ap (λ w → h ⊙ w) (! (invr g)) ⟩
    h ⊙ (g ⊙ inv g)    =⟨ ! (assoc h g (inv g)) ⟩
    (h ⊙ g) ⊙ inv g    =⟨ ap (λ w → w ⊙ inv g) p ⟩
    (k ⊙ g) ⊙ inv g    =⟨ assoc k g (inv g) ⟩
    k ⊙ (g ⊙ inv g)    =⟨ ap (λ w → k ⊙ w) (invr g) ⟩
    k ⊙ ident          =⟨ unitr k ⟩
    k ∎