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

module Generics.Mu.All where

open import Generics.Prelude hiding (lookup)
open import Generics.Telescope
open import Generics.Desc
open import Generics.Mu

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

AllIndArgωω
  : {X : ⟦ P , I ⟧xtel → Setω}
    (Pr : ∀ {i} → X (p , i) → Setω)
    (C : ConDesc P V I)
  → ∀ {v} → ⟦ C ⟧IndArgω X (p , v) → Setω
AllIndArgωω Pr (var _) x = Pr x
AllIndArgωω Pr (π (n , ai) S C) x = (s : < relevance ai > S _) → AllIndArgωω Pr C (x s)
AllIndArgωω Pr (A ⊗ B) (xa , xb) = AllIndArgωω Pr A xa ×ω AllIndArgωω Pr B xb

AllConωω
  : {X : ⟦ P , I ⟧xtel → Setω}
    (Pr : ∀ {i} → X (p , i) → Setω)
    (C : ConDesc P V I)
  → ∀ {v i} → ⟦ C ⟧Conω X (p , v , i) → Setω
AllConωω Pr (var f) x = ⊤ω
AllConωω Pr (π ia S C) (_ , x) = AllConωω Pr C x
AllConωω Pr (A ⊗ B) (xa , xb) = AllIndArgωω Pr A xa ×ω AllConωω Pr B xb

AllDataωω : {X  : ⟦ P , I ⟧xtel → Setω}
           (Pr : ∀ {i} → X (p , i) → Setω)
           (D : DataDesc P I n)
         → ∀ {i} (x : ⟦ D ⟧Dataω X (p , i))
         → Setω
AllDataωω Pr D (k , x) = AllConωω Pr (lookupCon D k) x

All : ∀ (D : DataDesc P I n) {c}
      (Pr : ∀ {i} → μ D (p , i) → Set c)
    → ∀ {i} → μ D (p , i) → Setω
All D Pr ⟨ x ⟩ = AllDataωω (λ x → Liftω (Pr x)) D x

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of All predicate transformer for fresh lists
------------------------------------------------------------------------

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

module Data.List.Fresh.Relation.Unary.All.Properties where

open import Level using (Level; _⊔_; Lift)
open import Data.Empty
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Product using (_,_)
open import Function using (_∘′_)
open import Relation.Nullary
open import Relation.Unary  as U
open import Relation.Binary as B using (Rel)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
open import Data.List.Fresh.Relation.Unary.All

private
  variable
    a p r : Level
    A : Set a

module _ {R : Rel A r} where

  fromAll : ∀ {x} {xs : List# A R} → All (R x) xs → x # xs
  fromAll []       = _
  fromAll (p ∷ ps) = p , fromAll ps

  toAll : ∀ {x} {xs : List# A R} → x # xs → All (R x) xs
  toAll {xs = []}      _        = []
  toAll {xs = a ∷# as} (p , ps) = p ∷ toAll ps

module _ {R : Rel A r} {P : Pred A p} where

  append⁺ : {xs ys : List# A R} {ps : All (_# ys) xs} →
            All P xs → All P ys → All P (append xs ys ps)
  append⁺ []         pys = pys
  append⁺ (px ∷ pxs) pys = px ∷ append⁺ pxs pys

ext: agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on machine words
------------------------------------------------------------------------

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

module Data.Word.Properties where

import Data.Nat.Base as ℕ
open import Data.Bool.Base using (Bool)
open import Data.Word.Base
import Data.Nat.Properties as ℕₚ
open import Function
open import Relation.Nullary.Decidable using (map′; ⌊_⌋)
open import Relation.Binary
  using ( _⇒_; Reflexive; Symmetric; Transitive; Substitutive
        ; Decidable; DecidableEquality; IsEquivalence; IsDecEquivalence
        ; Setoid; DecSetoid; StrictTotalOrder)
import Relation.Binary.Construct.On as On
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Primitive properties

open import Agda.Builtin.Word.Properties
  renaming (primWord64ToNatInjective to toℕ-injective)
  public

------------------------------------------------------------------------
-- Properties of _≈_

≈⇒≡ : _≈_ ⇒ _≡_
≈⇒≡ = toℕ-injective _ _

≈-reflexive : _≡_ ⇒ _≈_
≈-reflexive = cong toℕ

≈-refl : Reflexive _≈_
≈-refl = refl

≈-sym : Symmetric _≈_
≈-sym = sym

≈-trans : Transitive _≈_
≈-trans = trans

≈-subst : ∀ {ℓ} → Substitutive _≈_ ℓ
≈-subst P x≈y p = subst P (≈⇒≡ x≈y) p

infix 4 _≈?_
_≈?_ : Decidable _≈_
x ≈? y = toℕ x ℕₚ.≟ toℕ y

≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
  { refl  = λ {i} → ≈-refl {i}
  ; sym   = λ {i j} → ≈-sym {i} {j}
  ; trans = λ {i j k} → ≈-trans {i} {j} {k}
  }

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

≈-isDecEquivalence : IsDecEquivalence _≈_
≈-isDecEquivalence = record
  { isEquivalence = ≈-isEquivalence
  ; _≟_           = _≈?_
  }

≈-decSetoid : DecSetoid _ _
≈-decSetoid = record
  { isDecEquivalence = ≈-isDecEquivalence
  }
------------------------------------------------------------------------
-- Properties of _≡_

infix 4 _≟_
_≟_ : DecidableEquality Word64
x ≟ y = map′ ≈⇒≡ ≈-reflexive (x ≈? y)

≡-setoid : Setoid _ _
≡-setoid = setoid Word64

≡-decSetoid : DecSetoid _ _
≡-decSetoid = decSetoid _≟_

------------------------------------------------------------------------
-- Boolean equality test.

infix 4 _==_
_==_ : Word64 → Word64 → Bool
w₁ == w₂ = ⌊ w₁ ≟ w₂ ⌋

------------------------------------------------------------------------
-- Properties of _<_

infix 4 _<?_
_<?_ : Decidable _<_
_<?_ = On.decidable toℕ ℕ._<_ ℕₚ._<?_

<-strictTotalOrder-≈ : StrictTotalOrder _ _ _
<-strictTotalOrder-≈ = On.strictTotalOrder ℕₚ.<-strictTotalOrder toℕ


text:
{-# OPTIONS --without-K #-}
module function.extensionality.proof where

open import level
open import sum
open import equality
open import function.extensionality.core
open import hott.univalence
open import hott.level.core
open import hott.level.closure.core
open import hott.equivalence.core
open import sets.unit

top : ∀ {i} → Set i
top = ↑ _ ⊤

⊤-contr' : ∀ {i} → contr (↑ i ⊤)
⊤-contr' {i} = lift tt , λ { (lift tt) → refl }

-- this uses definitional η for ⊤
contr-exp-⊤ : ∀ {i j}{A : Set i} → contr (A → top {j})
contr-exp-⊤ = (λ _ → lift tt) , (λ f → refl)

module Weak where
  →-contr : ∀ {i j}{A : Set i}{B : Set j}
          → contr B
          → contr (A → B)
  →-contr {A = A}{B = B} hB = subst contr p contr-exp-⊤
    where
      p : (A → top) ≡ (A → B)
      p = ap (λ X → A → X) (unique-contr ⊤-contr' hB)

  funext : ∀ {i j}{A : Set i}{B : Set j}
      → (f : A → B)(b : B)(h : (x : A) → b ≡ f x)
      → (λ _ → b) ≡ f
  funext f b h =
    ap (λ u x → proj₁ (u x))
         (contr⇒prop (→-contr (singl-contr b))
                      (λ _ → (b , refl))
                      (λ x → f x , h x))

abstract
  Π-contr : ∀ {i j}{A : Set i}{B : A → Set j}
          → ((x : A) → contr (B x))
          → contr ((x : A) → B x)
  Π-contr {i}{j}{A}{B} hB = subst contr p contr-exp-⊤
    where
      p₀ : (λ _ → top) ≡ B
      p₀ = Weak.funext B top (λ x → unique-contr ⊤-contr' (hB x))

      p : (A → top {j}) ≡ ((x : A) → B x)
      p = ap (λ Z → (x : A) → Z x) p₀

  private
    funext₀ : ∀ {i j} → Extensionality' i j
    funext₀ {i}{j}{X = X}{Y = Y}{f = f}{g = g} h = ap (λ u x → proj₁ (u x)) lem
      where
        C : X → Set j
        C x = Σ (Y x) λ y → f x ≡ y

        f' g' : (x : X) → C x
        f' x = (f x , refl)
        g' x = (g x , h x)

        lem : f' ≡ g'
        lem = contr⇒prop (Π-contr (λ x → singl-contr (f x))) f' g'

abstract
  funext : ∀ {i j} → Extensionality' i j
  funext h = funext₀ h · sym (funext₀ (λ _ → refl))

  funext-id : ∀ {i j}{X : Set i}{Y : X → Set j}
         → (f : (x : X) → Y x)
         → funext (λ x → refl {x = f x}) ≡ refl
  funext-id _ = left-inverse (funext₀ (λ _ → refl))

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module Oscar.AgdaPatternSyntaxTrick where

record ⊤ : Set where
  constructor tt

data List (A : Set) : Set where
  ∅ : List A
  _∷_ : A → List A → List A

Nat = List ⊤
pattern ‼ xs = tt ∷ xs
syntax ‼ xs = ! xs

data Fin : Nat → Set where
  ∅ : ∀ {n} → Fin (! n)
  ! : ∀ {n} → Fin n → Fin (! n)

test : Fin (! (! ∅)) -- OOPS
test = ! ∅

-- record ⊤ : Set where
--   constructor tt

-- data List (A : Set) : Set where
--   ∅ : List A
--   _∷_ : A → List A → List A

-- Nat = List ⊤
-- pattern ‼ xs = tt ∷ xs

-- data Fin : Nat → Set where
--   ∅ : ∀ {n} → Fin (‼ n) -- BOO!
--   ! : ∀ {n} → Fin n → Fin (‼ n)


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

open import HoTT

module groups.CoefficientExtensionality where

module _ {i} {A : Type i} (dec : has-dec-eq A) where

  Word-coef : Word A → (A → ℤ)
  Word-coef nil a = 0
  Word-coef (inl a' :: w) a with dec a' a
  Word-coef (inl a' :: w) a | inl a'=a = succ $ Word-coef w a
  Word-coef (inl a' :: w) a | inr a'≠a = Word-coef w a
  Word-coef (inr a' :: w) a with dec a' a
  Word-coef (inr a' :: w) a | inl a'=a = pred $ Word-coef w a
  Word-coef (inr a' :: w) a | inr a'≠a = Word-coef w a

  abstract
    Word-coef-++ : ∀ w₁ w₂ a → Word-coef (w₁ ++ w₂) a
      == Word-coef w₁ a ℤ+ Word-coef w₂ a
    Word-coef-++ nil w₂ a = idp
    Word-coef-++ (inl a' :: w₁) w₂ a with dec a' a
    Word-coef-++ (inl a' :: w₁) w₂ a | inl a'=a =
        ap succ (Word-coef-++ w₁ w₂ a)
      ∙ ! (succ-+ (Word-coef w₁ a) (Word-coef w₂ a))
    Word-coef-++ (inl a' :: w₁) w₂ a | inr a'≠a = Word-coef-++ w₁ w₂ a
    Word-coef-++ (inr a' :: w₁) w₂ a with dec a' a
    Word-coef-++ (inr a' :: w₁) w₂ a | inl a'=a =
        ap pred (Word-coef-++ w₁ w₂ a)
      ∙ ! (pred-+ (Word-coef w₁ a) (Word-coef w₂ a))
    Word-coef-++ (inr a' :: w₁) w₂ a | inr a'≠a = Word-coef-++ w₁ w₂ a

    Word-coef-flip : ∀ w a → Word-coef (Word-flip w) a == ℤ~ (Word-coef w a)
    Word-coef-flip nil a = idp
    Word-coef-flip (inl a' :: w) a with dec a' a
    Word-coef-flip (inl a' :: w) a | inl a'=a =
        ap pred (Word-coef-flip w a) ∙ ! (ℤ~-succ (Word-coef w a))
    Word-coef-flip (inl a' :: w) a | inr a'≠a = Word-coef-flip w a
    Word-coef-flip (inr a' :: w) a with dec a' a
    Word-coef-flip (inr a' :: w) a | inl a'=a =
        ap succ (Word-coef-flip w a) ∙ ! (ℤ~-pred (Word-coef w a))
    Word-coef-flip (inr a' :: w) a | inr a'≠a = Word-coef-flip w a

  private
    abstract
      FormalSum-coef-rel : {w₁ w₂ : Word A} → FormalSumRel w₁ w₂
        → ∀ a → Word-coef w₁ a == Word-coef w₂ a
      FormalSum-coef-rel (fsr-refl p) a = ap (λ w → Word-coef w a) p
      FormalSum-coef-rel (fsr-trans fwr₁ fwr₂) a = (FormalSum-coef-rel fwr₁ a) ∙ (FormalSum-coef-rel fwr₂ a)
      FormalSum-coef-rel (fsr-sym fsr) a = ! $ FormalSum-coef-rel fsr a
      FormalSum-coef-rel (fsr-cons x fwr) a =
          Word-coef-++ (x :: nil) _ a
        ∙ ap (Word-coef (x :: nil) a ℤ+_) (FormalSum-coef-rel fwr a)
        ∙ ! (Word-coef-++ (x :: nil) _ a)
      FormalSum-coef-rel (fsr-swap x y w) a =
          Word-coef-++ (x :: y :: nil) _ a
        ∙ ap (_ℤ+ Word-coef w a)
            ( Word-coef-++ (x :: nil) (y :: nil) a
            ∙ ℤ+-comm (Word-coef (x :: nil) a) (Word-coef (y :: nil) a)
            ∙ ! (Word-coef-++ (y :: nil) (x :: nil) a))
        ∙ ! (Word-coef-++ (y :: x :: nil) _ a)
      FormalSum-coef-rel (fsr-flip x w) a =
          Word-coef-++ (x :: flip x :: nil) w a
        ∙ ap (_ℤ+ Word-coef w a)
            ( Word-coef-++ (x :: nil) (flip x :: nil) a
            ∙ ap (Word-coef (x :: nil) a ℤ+_) (Word-coef-flip (x :: nil) a)
            ∙ ℤ~-inv-r (Word-coef (x :: nil) a) )
        ∙ ℤ+-unit-l (Word-coef w a)

  FormalSum-coef : FormalSum A → (A → ℤ)
  FormalSum-coef = FormalSum-rec Word-coef (λ r → λ= $ FormalSum-coef-rel r)

  -- Theorem : if coef w a == 0 then FormalSumRel w nil

  private
    abstract
      Word-exp-succ : ∀ (a : A) z → FormalSumRel (inl a :: Word-exp a z) (Word-exp a (succ z))
      Word-exp-succ a (pos _) = fsr-refl idp
      Word-exp-succ a (negsucc 0) = fsr-flip (inl a) nil
      Word-exp-succ a (negsucc (S n)) = fsr-flip (inl a) (Word-exp a (negsucc n))

      Word-exp-pred : ∀ (a : A) z → FormalSumRel (inr a :: Word-exp a z) (Word-exp a (pred z))
      Word-exp-pred a (pos 0) = fsr-refl idp
      Word-exp-pred a (pos (S n)) = fsr-flip (inr a) (Word-exp a (pos n))
      Word-exp-pred a (negsucc _) = fsr-refl idp

      Word-coef-inl-eq : ∀ {a b} (p : b == a) w
        → Word-coef (inl b :: w) a == succ (Word-coef w a)
      Word-coef-inl-eq {a} {b} p w with dec b a
      Word-coef-inl-eq {a} {b} p w | inl _ = idp
      Word-coef-inl-eq {a} {b} p w | inr ¬p = ⊥-rec (¬p p)

      Word-coef-inr-eq : ∀ {a b} (p : b == a) w
        → Word-coef (inr b :: w) a == pred (Word-coef w a)
      Word-coef-inr-eq {a} {b} p w with dec b a
      Word-coef-inr-eq {a} {b} p w | inl _ = idp
      Word-coef-inr-eq {a} {b} p w | inr ¬p = ⊥-rec (¬p p)

      Word-coef-inl-neq : ∀ {a b} (p : b ≠ a) w
        → Word-coef (inl b :: w) a == Word-coef w a
      Word-coef-inl-neq {a} {b} ¬p w with dec b a
      Word-coef-inl-neq {a} {b} ¬p w | inl p = ⊥-rec (¬p p)
      Word-coef-inl-neq {a} {b} ¬p w | inr _ = idp

      Word-coef-inr-neq : ∀ {a b} (p : b ≠ a) w
        → Word-coef (inr b :: w) a == Word-coef w a
      Word-coef-inr-neq {a} {b} ¬p w with dec b a
      Word-coef-inr-neq {a} {b} ¬p w | inl p = ⊥-rec (¬p p)
      Word-coef-inr-neq {a} {b} ¬p w | inr _ = idp

    -- TODO maybe there is a better way to prove the final theorem?
    -- Here we are collecting all elements [inl a] and [inr a], and recurse on the rest.
    -- The [right-shorter] field makes sure that it is terminating.
    record CollectSplitIH (a : A) {n : ℕ} (w : Word A) (len : length w == n) : Type i where
      field
        left-exponent : ℤ
        left-captures-all : Word-coef w a == left-exponent
        right-list : Word A
        right-shorter : length right-list ≤ n
        fsr : FormalSumRel w (Word-exp a left-exponent ++ right-list)

    abstract
      collect-split : ∀ a {n} w (len=n : length w == n) → CollectSplitIH a w len=n
      collect-split a nil idp = record {
        left-exponent = 0;
        left-captures-all = idp;
        right-list = nil;
        right-shorter = inl idp;
        fsr = fsr-refl idp}
      collect-split a (inl b :: w) idp with dec b a
      ... | inl b=a = record {
        left-exponent = succ left-exponent;
        left-captures-all = Word-coef-inl-eq b=a w ∙ ap succ left-captures-all;
        right-list = right-list;
        right-shorter = ≤-trans right-shorter (inr ltS);
        fsr = fsr-trans (fsr-refl (ap (λ a → inl a :: w) b=a)) $
              fsr-trans (fsr-cons (inl a) fsr) $
                        (FormalSumRel-cong-++-l (Word-exp-succ a left-exponent) right-list)}
        where open CollectSplitIH (collect-split a w idp)
      ... | inr b≠a = record {
        left-exponent = left-exponent;
        left-captures-all = Word-coef-inl-neq b≠a w ∙ left-captures-all;
        right-list = inl b :: right-list;
        right-shorter = ≤-ap-S right-shorter;
        fsr = fsr-trans (fsr-cons (inl b) fsr) $
          fsr-sym (FormalSumRel-swap1 (inl b) (Word-exp a left-exponent) right-list)}
        where open CollectSplitIH (collect-split a w idp)
      collect-split a (inr b :: w) idp with dec b a
      ... | inl b=a = record {
        left-exponent = pred left-exponent;
        left-captures-all = Word-coef-inr-eq b=a w ∙ ap pred left-captures-all;
        right-list = right-list;
        right-shorter = ≤-trans right-shorter (inr ltS);
        fsr = fsr-trans (fsr-refl (ap (λ a → inr a :: w) b=a)) $
              fsr-trans (fsr-cons (inr a) fsr) $
                        (FormalSumRel-cong-++-l (Word-exp-pred a left-exponent) right-list)}
        where open CollectSplitIH (collect-split a w idp)
      ... | inr b≠a = record {
        left-exponent = left-exponent;
        left-captures-all = Word-coef-inr-neq b≠a w ∙ left-captures-all;
        right-list = inr b :: right-list;
        right-shorter = ≤-ap-S right-shorter;
        fsr = fsr-trans (fsr-cons (inr b) fsr) $
          fsr-sym (FormalSumRel-swap1 (inr b) (Word-exp a left-exponent) right-list)}
        where open CollectSplitIH (collect-split a w idp)

      -- We simulate strong induction by recursing on both [m] and [n≤m].
      -- We could develop a general framework for strong induction but I am lazy. -Favonia
      zero-coef-is-ident' : ∀ {m n} (n≤m : n ≤ m) (w : Word A) (len : length w == n)
        → (∀ a → Word-coef w a == 0) → FormalSumRel w nil
      zero-coef-is-ident' (inr ltS) w len zero-coef
        = zero-coef-is-ident' (inl idp) w len zero-coef
      zero-coef-is-ident' (inr (ltSR lt)) w len zero-coef
        = zero-coef-is-ident' (inr lt) w len zero-coef
      zero-coef-is-ident' {m = O} (inl idp) nil _ _ = fsr-refl idp
      zero-coef-is-ident' {m = O} (inl idp) (_ :: _) len _ = ⊥-rec $ ℕ-S≠O _ len
      zero-coef-is-ident' {m = S m} (inl idp) nil len _ = ⊥-rec $ ℕ-S≠O _ (! len)
      zero-coef-is-ident' {m = S m} (inl idp) (inl a :: w) len zero-coef =
        fsr-trans whole-is-right (zero-coef-is-ident' right-shorter right-list idp right-zero-coef)
        where
          open CollectSplitIH (collect-split a w (ℕ-S-is-inj _ _ len))
          left-exponent-is-minus-one : left-exponent == -1
          left-exponent-is-minus-one = succ-is-inj left-exponent -1 $
            ap succ (! left-captures-all) ∙ ! (Word-coef-inl-eq idp w) ∙ zero-coef a

          whole-is-right : FormalSumRel (inl a :: w) right-list
          whole-is-right =
            fsr-trans (fsr-cons (inl a) fsr) $
            fsr-trans (fsr-refl (ap (λ e → inl a :: Word-exp a e ++ right-list) left-exponent-is-minus-one)) $
                      fsr-flip (inl a) right-list

          right-zero-coef : ∀ a' → Word-coef right-list a' == 0
          right-zero-coef a' = ! (FormalSum-coef-rel whole-is-right a') ∙ zero-coef a'
      zero-coef-is-ident' {m = S m} (inl idp) (inr a :: w) len zero-coef =
        fsr-trans whole-is-right (zero-coef-is-ident' right-shorter right-list idp right-zero-coef)
        where
          open CollectSplitIH (collect-split a w (ℕ-S-is-inj _ _ len))
          left-exponent-is-one : left-exponent == 1
          left-exponent-is-one = pred-is-inj left-exponent 1 $
            ap pred (! left-captures-all) ∙ ! (Word-coef-inr-eq idp w) ∙ zero-coef a

          whole-is-right : FormalSumRel (inr a :: w) right-list
          whole-is-right =
            fsr-trans (fsr-cons (inr a) fsr) $
            fsr-trans (fsr-refl (ap (λ e → inr a :: Word-exp a e ++ right-list) left-exponent-is-one)) $
                      fsr-flip (inr a) right-list

          right-zero-coef : ∀ a' → Word-coef right-list a' == 0
          right-zero-coef a' = ! (FormalSum-coef-rel whole-is-right a') ∙ zero-coef a'

      zero-coef-is-ident : ∀ (w : Word A)
        → (∀ a → Word-coef w a == 0)
        → FormalSumRel w nil
      zero-coef-is-ident w = zero-coef-is-ident' (inl idp) w idp

  abstract
    FormalSum-coef-ext' : ∀ w₁ w₂
      → (∀ a → Word-coef w₁ a == Word-coef w₂ a)
      → fs[ w₁ ] == fs[ w₂ ]
    FormalSum-coef-ext' w₁ w₂ same-coef = G.inv-is-inj fs[ w₁ ] fs[ w₂ ] $
      G.inv-unique-l (G.inv fs[ w₂ ]) fs[ w₁ ] $ quot-rel $
      zero-coef-is-ident (Word-flip w₂ ++ w₁)
        (λ a → Word-coef-++ (Word-flip w₂) w₁ a
             ∙ ap2 _ℤ+_ (Word-coef-flip w₂ a) (same-coef a)
             ∙ ℤ~-inv-l (Word-coef w₂ a))
      where module G = FreeAbGroup A

    FormalSum-coef-ext : ∀ fs₁ fs₂
      → (∀ a → FormalSum-coef fs₁ a == FormalSum-coef fs₂ a)
      → fs₁ == fs₂
    FormalSum-coef-ext = FormalSum-elim
      (λ w₁ → FormalSum-elim
        (λ w₂ → FormalSum-coef-ext' w₁ w₂)
        (λ _ → prop-has-all-paths-↓))
      (λ _ → prop-has-all-paths-↓)

  has-finite-support : (A → ℤ) → Type i
  has-finite-support f = Σ (FormalSum A) λ fs → ∀ a → f a == FormalSum-coef fs a

module _ {i} {A : Type i} {dec : has-dec-eq A} where

  abstract
    has-finite-support-is-prop : ∀ f → is-prop (has-finite-support dec f)
    has-finite-support-is-prop f = all-paths-is-prop
      λ{(fs₁ , match₁) (fs₂ , match₂) → pair=
        (FormalSum-coef-ext dec fs₁ fs₂ λ a → ! (match₁ a) ∙ match₂ a)
        prop-has-all-paths-↓}

module _ where

  private
    abstract
      Word-coef-exp-diag-pos : ∀ {I} (<I : Fin I) n →
        Word-coef Fin-has-dec-eq (Word-exp <I (pos n)) <I == pos n
      Word-coef-exp-diag-pos <I O = idp
      Word-coef-exp-diag-pos <I (S n) with Fin-has-dec-eq <I <I
      ... | inl _ = ap succ (Word-coef-exp-diag-pos <I n)
      ... | inr ¬p = ⊥-rec (¬p idp)

      Word-coef-exp-diag-negsucc : ∀ {I} (<I : Fin I) n →
        Word-coef Fin-has-dec-eq (Word-exp <I (negsucc n)) <I == negsucc n
      Word-coef-exp-diag-negsucc <I O with Fin-has-dec-eq <I <I
      ... | inl _ = idp
      ... | inr ¬p = ⊥-rec (¬p idp)
      Word-coef-exp-diag-negsucc <I (S n) with Fin-has-dec-eq <I <I
      ... | inl _ = ap pred (Word-coef-exp-diag-negsucc <I n)
      ... | inr ¬p = ⊥-rec (¬p idp)

      Word-coef-exp-diag : ∀ {I} (<I : Fin I) z →
        Word-coef Fin-has-dec-eq (Word-exp <I z) <I == z
      Word-coef-exp-diag <I (pos n) = Word-coef-exp-diag-pos <I n
      Word-coef-exp-diag <I (negsucc n) = Word-coef-exp-diag-negsucc <I n

      Word-coef-exp-≠-pos : ∀ {I} {<I <I' : Fin I} (_ : <I ≠ <I') n →
        Word-coef Fin-has-dec-eq (Word-exp <I (pos n)) <I' == 0
      Word-coef-exp-≠-pos _ O = idp
      Word-coef-exp-≠-pos {<I = <I} {<I'} neq (S n) with Fin-has-dec-eq <I <I'
      ... | inl p = ⊥-rec (neq p)
      ... | inr ¬p = Word-coef-exp-≠-pos neq n

      Word-coef-exp-≠-negsucc : ∀ {I} {<I <I' : Fin I} (_ : <I ≠ <I') n →
        Word-coef Fin-has-dec-eq (Word-exp <I (negsucc n)) <I' == 0
      Word-coef-exp-≠-negsucc {<I = <I} {<I'} neq O with Fin-has-dec-eq <I <I'
      ... | inl p = ⊥-rec (neq p)
      ... | inr ¬p = idp
      Word-coef-exp-≠-negsucc {<I = <I} {<I'} neq (S n) with Fin-has-dec-eq <I <I'
      ... | inl p = ⊥-rec (neq p)
      ... | inr ¬p = Word-coef-exp-≠-negsucc neq n

      Word-coef-exp-≠ : ∀ {I} {<I <I' : Fin I} (_ : <I ≠ <I') z →
        Word-coef Fin-has-dec-eq (Word-exp <I z) <I' == 0
      Word-coef-exp-≠ neq (pos n) = Word-coef-exp-≠-pos neq n
      Word-coef-exp-≠ neq (negsucc n) = Word-coef-exp-≠-negsucc neq n

    Word-sum' : ∀ (I : ℕ) {A : Type₀} (F : Fin I → A) (f : Fin I → ℤ) → Word A
    Word-sum' 0 F f = nil
    Word-sum' (S I) F f = Word-sum' I (F ∘ Fin-S) (f ∘ Fin-S) ++ Word-exp (F (I , ltS)) (f (I , ltS))

    Word-sum : ∀ {I : ℕ} (f : Fin I → ℤ) → Word (Fin I)
    Word-sum {I} f = Word-sum' I (idf (Fin I)) f

    abstract
      Word-coef-sum'-late : ∀ n m (I : ℕ) (f : Fin I → ℤ)
        → Word-coef Fin-has-dec-eq (Word-sum' I (Fin-S^' (S n) ∘ Fin-S^' m) f) (Fin-S^' n (ℕ-S^' m I , ltS)) == 0
      Word-coef-sum'-late n m 0 f = idp
      Word-coef-sum'-late n m (S I) f =
        Word-coef Fin-has-dec-eq
          (Word-sum' I (Fin-S^' (S n) ∘ Fin-S^' (S m)) (f ∘ Fin-S) ++ Word-exp (Fin-S^' (S n) (Fin-S^' m (I , ltS))) (f (I , ltS)))
          (Fin-S^' n (ℕ-S^' (S m) I , ltS))
          =⟨ Word-coef-++ Fin-has-dec-eq
              (Word-sum' I (Fin-S^' (S n) ∘ Fin-S^' (S m)) (f ∘ Fin-S))
              (Word-exp (Fin-S^' (S n) (Fin-S^' m (I , ltS))) (f (I , ltS)))
              (Fin-S^' n (ℕ-S^' (S m) I , ltS)) ⟩
        Word-coef Fin-has-dec-eq (Word-sum' I (Fin-S^' (S n) ∘ Fin-S^' (S m)) (f ∘ Fin-S)) (Fin-S^' n (ℕ-S^' (S m) I , ltS))
        ℤ+
        Word-coef Fin-has-dec-eq (Word-exp (Fin-S^' (S n) (Fin-S^' m (I , ltS))) (f (I , ltS))) (Fin-S^' n (ℕ-S^' (S m) I , ltS))
          =⟨ ap2 _ℤ+_
              (Word-coef-sum'-late n (S m) I (f ∘ Fin-S))
              (Word-coef-exp-≠ (Fin-S^'-≠ n (ltSR≠ltS _)) (f (I , ltS))) ⟩
        0
          =∎

      Word-coef-sum' : ∀ n {I} (f : Fin I → ℤ) <I
        → Word-coef Fin-has-dec-eq (Word-sum' I (Fin-S^' n) f) (Fin-S^' n <I) == f <I
      Word-coef-sum' n f (I , ltS) =
        Word-coef Fin-has-dec-eq
          (Word-sum' I (Fin-S^' (S n)) (f ∘ Fin-S) ++ Word-exp (Fin-S^' n (I , ltS)) (f (I , ltS)))
          (Fin-S^' n (I , ltS))
          =⟨ Word-coef-++ Fin-has-dec-eq
              (Word-sum' I (Fin-S^' (S n)) (f ∘ Fin-S))
              (Word-exp (Fin-S^' n (I , ltS)) (f (I , ltS)))
              (Fin-S^' n (I , ltS)) ⟩
        Word-coef Fin-has-dec-eq (Word-sum' I (Fin-S^' (S n)) (f ∘ Fin-S)) (Fin-S^' n (I , ltS))
        ℤ+
        Word-coef Fin-has-dec-eq (Word-exp (Fin-S^' n (I , ltS)) (f (I , ltS))) (Fin-S^' n (I , ltS))
          =⟨ ap2 _ℤ+_
              (Word-coef-sum'-late n 0 I (f ∘ Fin-S))
              (Word-coef-exp-diag (Fin-S^' n (I , ltS)) (f (I , ltS))) ⟩
        f (I , ltS)
          =∎
      Word-coef-sum' n {I = S I} f (m , ltSR m<I) =
        Word-coef Fin-has-dec-eq
          (Word-sum' I (Fin-S^' (S n)) (f ∘ Fin-S) ++ Word-exp (Fin-S^' n (I , ltS)) (f (I , ltS)))
          (Fin-S^' (S n) (m , m<I))
          =⟨ Word-coef-++ Fin-has-dec-eq
              (Word-sum' I (Fin-S^' (S n)) (f ∘ Fin-S))
              (Word-exp (Fin-S^' n (I , ltS)) (f (I , ltS)))
              (Fin-S^' (S n) (m , m<I)) ⟩
        Word-coef Fin-has-dec-eq (Word-sum' I (Fin-S^' (S n)) (f ∘ Fin-S)) (Fin-S^' (S n) (m , m<I))
        ℤ+
        Word-coef Fin-has-dec-eq (Word-exp (Fin-S^' n (I , ltS)) (f (I , ltS))) (Fin-S^' (S n) (m , m<I))
          =⟨ ap2 _ℤ+_
              (Word-coef-sum' (S n) {I} (f ∘ Fin-S) (m , m<I))
              (Word-coef-exp-≠ (Fin-S^'-≠ n (ltS≠ltSR (m , m<I))) (f (I , ltS))) ⟩
        f (m , ltSR m<I) ℤ+ 0
          =⟨ ℤ+-unit-r _ ⟩
        f (m , ltSR m<I)
          =∎

  FormalSum-sum' : ∀ n (I : ℕ) (f : Fin I → ℤ) → FormalSum (Fin (ℕ-S^' n I))
  FormalSum-sum' n I f =
    Group.sum (FreeAbGroup.grp (Fin (ℕ-S^' n I)))
      (λ <I → Group.exp (FreeAbGroup.grp (Fin (ℕ-S^' n I))) fs[ inl (Fin-S^' n <I) :: nil ] (f <I))

  FormalSum-sum : ∀ {I : ℕ} (f : Fin I → ℤ) → FormalSum (Fin I)
  FormalSum-sum {I} = FormalSum-sum' 0 I

  private
    abstract
      FormalSum-sum'-β : ∀ n (I : ℕ) (f : Fin I → ℤ)
        → FormalSum-sum' n I f == fs[ Word-sum' I (Fin-S^' n) f ]
      FormalSum-sum'-β n O f = idp
      FormalSum-sum'-β n (S I) f =
        ap2 (Group.comp (FreeAbGroup.grp (Fin (ℕ-S^' (S n) I))))
          (FormalSum-sum'-β (S n) I (f ∘ Fin-S))
          (! (FormalSumRel-pres-exp (Fin-S^' n (I , ltS)) (f (I , ltS))))

  Fin→-has-finite-support : ∀ {I} (f : Fin I → ℤ) → has-finite-support Fin-has-dec-eq f
  Fin→-has-finite-support {I} f = FormalSum-sum f , lemma
    where abstract lemma = λ <I → ! (ap (λ fs → FormalSum-coef Fin-has-dec-eq fs <I) (FormalSum-sum'-β 0 I f) ∙ Word-coef-sum' 0 f <I)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
open import Agda.Primitive

_∘_ : ∀ {a b c}
        {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

data D {a} (A : Set a) : Set a where
  d : D A → D A

data E {a} (A : Set a) : Set a where
  e : A → E A

F : ∀ {a} {A : Set a} → A → D A → Set a
F x (d ys) = E (F x ys)

G : ∀ {a} {A : Set a} → D A → D A → Set a
G xs ys = ∀ x → F x xs → F x ys

postulate
  H : ∀ {a} {A : Set a} {xs ys : D A} → G xs ys → Set

variable
  a  : Level
  A  : Set a
  P  : A → Set a
  x  : A
  xs : D A

postulate
  h : {f : G xs xs} (_ : P x) → F x xs → H (λ _ → e ∘ f _)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Char where

postulate Char : Set

{-# BUILTIN CHAR Char #-}


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

open import HoTT
open import groups.Cokernel
open import cohomology.Theory

open import cw.CW

module cw.cohomology.ZerothCohomologyGroup {i} (OT : OrdinaryTheory i)
  (⊙skel : ⊙Skeleton {i} 1) (ac : ⊙has-cells-with-choice 0 ⊙skel i) where

open OrdinaryTheory OT
open import cw.cohomology.TipCoboundary OT ⊙skel
open import cw.cohomology.TipAndAugment OT (⊙cw-init ⊙skel)
open import cw.cohomology.TipGrid OT ⊙skel ac

{-

    C(X₀)<------C(X₁) = C(X)
                  ^
                  |
                  |
               C(X₁/X₀)
                 WoC

    WoC := Wedges of Cells
-}

open import groups.KernelSndImageInl (C2 0) {H = CX₀ 0}
  {K = C 1 (⊙Cofiber (⊙cw-incl-last ⊙skel))}
  cw-co∂-head' cw-co∂-head (λ _ → idp)
  (C2×CX₀-is-abelian 0)

module CokerCoε = Coker cw-coε (C2×CX₀-is-abelian 0)

open import groups.KernelImage cw-co∂-head cw-coε (C2×CX₀-is-abelian 0)

C-cw-iso-ker/im : C 0 ⊙⟦ ⊙skel ⟧ ≃ᴳ Ker/Im
C-cw-iso-ker/im = Ker-φ-snd-quot-Im-inl ∘eᴳ Ker-cw-co∂-head'

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-
  Definitions for functions
-}
{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.Function where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude

-- The identity function
idfun : ∀ {ℓ} → (A : Type ℓ) → A → A
idfun _ x = x

infixr 9 _∘_

_∘_ : ∀ {ℓ ℓ′ ℓ″} {A : Type ℓ} {B : A → Type ℓ′} {C : (a : A) → B a → Type ℓ″}
        (g : {a : A} → (b : B a) → C a b) → (f : (a : A) → B a) → (a : A) → C a (f a)
g ∘ f = λ x → g (f x)

∘-assoc : ∀ {ℓ ℓ′ ℓ″ ℓ‴} {A : Type ℓ} {B : A → Type ℓ′} {C : (a : A) → B a → Type ℓ″} {D : (a : A) (b : B a) → C a b → Type ℓ‴}
            (h : {a : A} {b : B a} → (c : C a b) → D a b c) (g : {a : A} → (b : B a) → C a b) (f : (a : A) → B a)
          → (h ∘ g) ∘ f ≡ h ∘ (g ∘ f)
∘-assoc h g f i x = h (g (f x))

∘-idˡ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : A → Type ℓ′} (f : (a : A) → B a) → f ∘ idfun A ≡ f
∘-idˡ f i x = f x

∘-idʳ : ∀ {ℓ ℓ′} {A : Type ℓ} {B : A → Type ℓ′} (f : (a : A) → B a) → (λ {a} → idfun (B a)) ∘ f ≡ f
∘-idʳ f i x = f x

const : ∀ {ℓ ℓ′} {A : Type ℓ} {B : Type ℓ′} → A → B → A
const x = λ _ → x

case_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → (x : A) → (∀ x → B x) → B x
case x of f = f x

case_return_of_ : ∀ {ℓ ℓ'} {A : Type ℓ} (x : A) (B : A → Type ℓ') → (∀ x → B x) → B x
case x return P of f = f x

uncurry
  : ∀{ℓ ℓ′ ℓ″} {A : Type ℓ} {B : A → Type ℓ′} {C : (a : A) → B a → Type ℓ″}
  → ((x : A) → (y : B x) → C x y)
  → (p : Σ A B) → C (fst p) (snd p)
uncurry f (x , y) = f x y

module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
  -- Notions of 'coherently constant' functions for low dimensions.
  -- These are the properties of functions necessary to e.g. eliminate
  -- from the propositional truncation.

  -- 2-Constant functions are coherently constant if B is a set.
  2-Constant : (A → B) → Type _
  2-Constant f = ∀ x y → f x ≡ f y

  2-Constant-isProp : isSet B → (f : A → B) → isProp (2-Constant f)
  2-Constant-isProp Bset f link1 link2 i x y j
    = Bset (f x) (f y) (link1 x y) (link2 x y) i j

  -- 3-Constant functions are coherently constant if B is a groupoid.
  record 3-Constant (f : A → B) : Type (ℓ-max ℓ ℓ') where
    field
      link : 2-Constant f
      coh₁ : ∀ x y z → Square refl (link x y) (link x z) (link y z)

    coh₂ : ∀ x y z → Square (link x y) (link x z) (link y z) refl
    coh₂ x y z i j
      = hcomp (λ k → λ
              { (j = i0) → link x y i
              ; (i = i0) → link x z (j ∧ k)
              ; (j = i1) → link x z (i ∨ k)
              ; (i = i1) → link y z j
              })
          (coh₁ x y z j i)

    link≡refl : ∀ x → refl ≡ link x x
    link≡refl x i j
      = hcomp (λ k → λ
              { (i = i0) → link x x (j ∧ ~ k)
              ; (i = i1) → link x x j
              ; (j = i0) → f x
              ; (j = i1) → link x x (~ i ∧ ~ k)
              })
          (coh₁ x x x (~ i) j)

    downleft : ∀ x y → Square refl (link x y) refl (link y x)
    downleft x y i j
      = hcomp (λ k → λ
              { (i = i0) → link x y j
              ; (i = i1) → link≡refl x (~ k) j
              ; (j = i0) → f x
              ; (j = i1) → link y x i
              })
          (coh₁ x y x i j)

    link≡symlink : ∀ x y → link x y ≡ sym (link y x)
    link≡symlink x y i j
      = hcomp (λ k → λ
              { (i = i0) → link x y j
              ; (i = i1) → link y x (~ j ∨ ~ k)
              ; (j = i0) → f x
              ; (j = i1) → link y x (i ∧ ~ k)
              })
          (downleft x y i j)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


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

open import PathInduction
open import Pushout

module JamesFirstComposite {i} (A : Type i) (⋆A : A) where

open import JamesTwoMaps A ⋆A

ap-from-αJ-δJ : (a : A) (x : JA) → ap from (ap (αJ a) (δJ x)) == ap (α∞ a) (δ∞ (from x))
ap-from-αJ-δJ a x = ap-from-αJ a (δJ x) ∙ ap (ap (α∞ a)) (δJ-β x)

ap-from-γ : (a : A) (x : JA) → ap from (γJ a x) == γ∞ a (from x)
ap-from-γ = λ a x → ap-!∙ from (ap (αJ a) (δJ x)) (δJ (αJ a x)) ∙ & coh (ap-from-αJ-δJ a x) (δJ-β (αJ a x))  module ApFromγ where

  coh : Coh ({A : Type i} {a b : A} {p p' : b == a} (p= : p == p') {c : A} {q q' : b == c} (q= : q == q') → ! p ∙ q == ! p' ∙ q')
  coh = path-induction

ap-from-η : (x : JA) → Square (ap (ap from) (ηJ x)) (ap-from-γ ⋆A x) idp (η∞ (from x))
ap-from-η x = & (η-ify-coh from) (ap-δJ (δJ x)) ∙□ & η-coh-homotopy from-δJ-δJ  where

  -- [ap] commutes with [ηIfy.coh]
  -- This lemma would also be true for arbitrary [αJ], [δJ], [α∞] and [δ∞], but for simplicity
  -- we do not abstract over them. We do abstract over [from] because otherwise Agda uses a
  -- crazy amount of memory.
  η-ify-coh : (from : JA → J∞A) → Coh ({a b : JA} {p : a == b} {c : JA} {q r : b == c} (sq : Square p p q r)
              → Square (ap (ap from) (& (ηIfy.coh αJ δJ) sq)) (ap-!∙ from q r) idp (& (ηIfy.coh α∞ δ∞) (ap-square from sq)))
  η-ify-coh = path-induction

  from-δJ-δJ : FlatCube (ap-square from (natural-square δJ (δJ x) (ap-idf (δJ x)) idp))
              (natural-square δ∞ (δ∞ (from x)) (ap-idf (δ∞ (from x))) idp)
              (δJ-β x)
              (δJ-β x)
              (ap-from-αJ-δJ ⋆A x)
              (δJ-β (αJ ⋆A x))
  from-δJ-δJ = adapt-flatcube ∙idp idp∙ idp∙ ∙idp
           (& (ap-square-natural-square from) (δJ x) δJ (& coh) ∙idp
           /∙³ & natural-square-homotopy (δJ-β) (δJ x)
           ∙fc & (natural-square-∘ (δJ x) from) δ∞ (& coh') idp
           /∙³ & natural-square= δ∞ (δJ-β x) (& ap2-idf) (& coh''))  where

    coh : {A B : Type i} {f : A → B} → Coh ({x y : A} {p : x == y} → ap-∘ f (λ z → z) p ∙ ap (ap f) (ap-idf p) == idp)
    coh = path-induction

    coh' : {A B : Type i} {f : A → B} → Coh ({x y : A} {p : x == y} → ∘-ap (λ z → z) f p ∙ idp == ap-idf _)
    coh' = path-induction

    coh'' : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q : c == a} {d : A} {r : c == d}
                 → Square p (! q ∙ r) idp ((! r ∙ q) ∙ p))
    coh'' = path-induction

  -- If [sq] and [sq'] are equal (via a FlatCube), then applying [ηIfy.coh] to them give equal terms
  -- (via a Square).
  η-coh-homotopy : Coh ({a b : J∞A} {p : a == b} {c : J∞A} {q : b == c} {r : b == c} {sq : Square p p q r}
              {p' : a == b} {p= : p == p'} {q' : b == c} {q= : q == q'} {r' : b == c} {r= : r == r'}
              {sq' : Square p' p' q' r'} (cube : FlatCube sq sq' p= p= q= r=)
              → Square (& (ηIfy.coh α∞ δ∞) sq) (& ApFromγ.coh q= r=) idp (& (ηIfy.coh α∞ δ∞) sq'))
  η-coh-homotopy = path-induction

comp-square2 : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q : b == c} → Square p idp q (p ∙ q))
comp-square2 = path-induction

ap-square-comp-square2 : {A B : Type i} (f : A → B) → Coh ({a b : A} {p : a == b} {c : A} {q : b == c}
                       → FlatCube (ap-square f (& comp-square2 {p = p} {q = q})) (& comp-square2) idp idp idp (ap-∙ f p q))
ap-square-comp-square2 f = path-induction

{- First composite -}

-- As for [inJ], we need both [from-inJ] and [from-inJS] for the termination checker
from-inJ : (n : ℕ) (x : J n) → from (inJ n x) == in∞ n x
from-inJS : (n : ℕ) (x : J (S n)) → from (inJS n x) == in∞ (S n) x

-- Those three describe [from ∘ inJS] applied to [ι], [α] and [β], in the case [S n] as it is
-- the only one we need.

from-inJSS-ι : (n : ℕ) (x : J (S n)) → from (inJS (S n) (ι (S n) x)) == in∞ (S (S n)) (ι (S n) x)
from-inJSS-ι n x = ap (α∞ ⋆A) (from-inJS n x) ∙ ap (in∞ (S (S n))) (β (S n) x)

from-inJSS-α : (n : ℕ) (a : A) (x : J (S n)) → from (inJS (S n) (α (S n) a x)) == in∞ (S (S n)) (α (S n) a x)
from-inJSS-α n a x = ap (α∞ a) (from-inJS n x)

from-inJSS-β : (n : ℕ) (x : J (S n)) → Square (ap from (ap (inJS (S n)) (β (S n) x))) (from-inJSS-α n ⋆A x) (from-inJSS-ι n x) (ap (in∞ (S (S n))) (β (S n) x))
from-inJSS-β n x = ap (ap from) (inJS-βS n x) |∙ comp-square

-- Those three terms describe what happens when we apply [from-inJS] to [ι], [α] or [β].
-- Note that the naming scheme is slightly ambiguous, they do *not* describe [from (inJS (ι _ _))] as above.
-- They are defined later, as we need to know the definition of [from-inJS].

from-inJS-ι : (n : ℕ) (x : J n) → Square (from-inJS n (ι n x)) (ap from (inJS-ι n x)) idp (ap (α∞ ⋆A) (from-inJ n x) ∙ ap (in∞ (S n)) (β n x))
from-inJS-α : (n : ℕ) (a : A) (x : J n) → Square (from-inJS n (α n a x)) (ap from (inJS-α n a x)) idp (ap (α∞ a) (from-inJ n x))
from-inJS-β : (n : ℕ) (x : J n) → Cube (natural-square (from-inJS n) (β n x) (ap-∘ from (inJS n) (β n x)) idp) (& comp-square2) (from-inJS-α n ⋆A x) (ap-square from (inJS-β n x)) hid-square (from-inJS-ι n x)

-- The following three terms show that the two ways of reducing [from ∘ inJS (S n) ∘ (ι (S n) | α (S n) a) ∘ (ι n | α n a)]
-- are equal. For some reason, we don’t need it with α twice

side1 : (n : ℕ) (a : A) (x : J n) → ap (α∞ a) (ap from (inJS-ι n x)) ∙
                                    ap (α∞ a) (ap (α∞ ⋆A) (from-inJ n x)) ∙
                                    ap (in∞ (S (S n))) (ap (α (S n) a) (β n x))
                                    == from-inJSS-α n a (ι n x)
side1 n = λ a x → & coh (ap-∙ _ _ _) (ap-square (α∞ a) (from-inJS-ι n x)) (ap-α∞-in∞ (S n) a (β n x))  module Side1 where

  coh : Coh ({A : Type i} {a c : A} {q : a == c} {d : A} {s1 : c == d} {b : A} {s2 : d == b} {s : c == b} (s= : s == s1 ∙ s2)
             {p : a == b} (sq : Square p q idp s) {s2' : d == b} (s2= : s2 == s2')
            → q ∙ s1 ∙ s2' == p)
  coh = path-induction

side2 : (n : ℕ) (a : A) (x : J n) → ap (α∞ ⋆A) (ap from (inJS-α n a x)) ∙
                                    ap (α∞ ⋆A) (ap (α∞ a) (from-inJ n x)) ∙
                                    ap (in∞ (S (S n))) (β (S n) (α n a x))
                                    == from-inJSS-ι n (α n a x)
side2 n = λ a x → & coh (ap-square (α∞ ⋆A) (from-inJS-α n a x))  module Side2 where

  coh : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q : a == c} {s : c == b} (sq : Square p q idp s) {e : A} {t : b == e}
            → q ∙ s ∙ t == p ∙ t)
  coh = path-induction

side3 : (n : ℕ) (x : J n) → ap (α∞ ⋆A) (ap from (inJS-ι n x)) ∙
                            ap (α∞ ⋆A) (ap (α∞ ⋆A) (from-inJ n x)) ∙
                            ap (in∞ (S (S n))) (β (S n) (α n ⋆A x)) ∙
                            ap (in∞ (S (S n))) (ap (ι (S n)) (β n x))
                            == from-inJSS-ι n (ι n x)
side3 n = λ x → & coh (ap-∙ _ _ _) (ap-α∞-in∞ (S n) ⋆A (β n x)) (ap-square (α∞ ⋆A) (from-inJS-ι n x))
                      (ap-square (in∞ (S (S n))) (natural-square (β (S n)) (β n x) idp idp))  module Side3 where

  coh : Coh ({A : Type i} {a c : A} {q : a == c} {d : A} {s : c == d} {b : A} {r : d == b} {rs : c == b} (rs= : rs == s ∙ r)
             {r' : d == b} (r= : r == r') {p : a == b} (sq : Square p q idp rs)
             {e : A} {t : d == e} {f : A} {u : e == f} {v : b == f} (sq2 : Square t r' u v)
            → q ∙ s ∙ t ∙ u == p ∙ v)
  coh = path-induction

piece1 : (n : ℕ) (a : A) (x : J n) → Square (ap from (ap (inJS (S n)) (γ n a x)))
                                            (ap (α∞ a) (ap from (inJS-ι n x)))
                                            (ap (α∞ ⋆A) (ap from (inJS-α n a x)))
                                            (ap from (γJ a (inJ n x)))
piece1 n a x = adapt-square (ap-square from (inJSS-γ n a x)) (ap-from-αJ a (inJS-ι n x)) (ap-from-αJ ⋆A (inJS-α n a x))

from-inJSS-γ : (n : ℕ) (a : A) (x : J n) → Square (ap from (ap (inJS (S n)) (γ n a x))) (from-inJSS-α n a (ι n x)) (from-inJSS-ι n (α n a x)) (ap (in∞ (S (S n))) (γ n a x))
from-inJSS-γ n a x = adapt-square (piece1 n a x
                                  ∙□ ap-from-γ a (inJ n x)
                                  |∙ natural-square (γ∞ a) (from-inJ n x) (ap-∘ (α∞ a) (α∞ ⋆A) (from-inJ n x)) (ap-∘ (α∞ ⋆A) (α∞ a) (from-inJ n x))
                                  ∙□ γ∞-in a n x)
                                  (side1 n a x) (side2 n a x)

adapt-eq : Coh ({A : Type i} {a b : A} {q : a == b} {sq : Square idp q q idp} (sq= : sq == vid-square) {q' : a == b} {p : q == q'} → adapt-square sq p p == vid-square)
adapt-eq = path-induction

natural-square-idp : {A B : Type i} {f : A → B} {x y : A} {p : x == y} {fp : f x == f y} {fp= : ap f p == fp} → natural-square (λ a → idp {a = f a}) p fp= fp= == vid-square
natural-square-idp {p = idp} {fp= = idp} = idp

vid-square∙□vid-square∙□vid-square : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q : b == c} {d : A} {r : c == d} → vid-square {p = p} ∙□ vid-square {p = q} ∙□ vid-square {p = r} == vid-square {p = p ∙ q ∙ r})
vid-square∙□vid-square∙□vid-square = path-induction

adapt-square-natural-square : ∀ {i j} {A : Type i} {B : Type j} → Coh ({f g : A → B} {h : (a : A) → f a == g a}
                                {x y : A} {p : x == y} {pf' : f x == f y} {q : ap f p == pf'} {pg' : g x == g y} {r : ap g p == pg'}
                              → adapt-square (natural-square h p idp idp) q r == natural-square h p q r)
adapt-square-natural-square = path-induction

piece1-η : (n : ℕ) (x : J n) → Cube (ap-square from (ap-square (inJS (S n)) (η n x)))
                                    (horiz-degen-square (ap (ap from) (ηJ (inJ n x))))
                                    (piece1 n ⋆A x) vid-square _ _
piece1-η n x = & (ap-shapeInJSη from) {to = ηJ (inJ n x)} (inJSS-η n x) (ap-from-αJ ⋆A (inJS-α n ⋆A x)) (ap-from-αJ ⋆A (inJS-ι n x))

coh-blip : {A B : Type i} {a b : A} (p : a == b)
       → Coh ({f g : A → B} {k : (a : A) → f a == g a} {h : A → B} {l : (a : A) → g a == h a}
              {fp : _} {fp= : ap f p == fp}
              {gp : _} (gp= : ap g p == gp)
              {hp : _} {hp= : ap h p == hp}
             → square-symmetry (natural-square (λ x → k x ∙ l x) p fp= hp=) == square-symmetry (natural-square k p fp= gp=) ∙□ square-symmetry (natural-square l p gp= hp=))
coh-blip {a = a} idp = path-induction

ap-square-hid : {A B : Type i} {f : A → B} {x y : A} {p : x == y} → ap-square f (hid-square {p = p}) == hid-square
ap-square-hid {p = idp} = idp

from-inJSS-η : (n : ℕ) (x : J n) → Cube (ap-square from (ap-square (inJS (S n)) (η n x)))
                                        (ap-square (in∞ (S (S n))) (η n x))
                                        (from-inJSS-γ n ⋆A x)
                                        vid-square
                                        (square-symmetry (natural-square (from-inJSS-ι n) (β n x) (ap-∘ _ _ _ ∙ ap-∘ _ _ _) (ap-∘ _ _ _)))
                                        (from-inJSS-β n (ι n x))
from-inJSS-η n x =
  adapt-cube (piece1-η n x
             ∙³x  ap-from-η (inJ n x)
             -|∙³ natural-cube-η∞ η∞ (from-inJ n x)
             ∙³x  η∞-in n x)
    (side1 n ⋆A x) (side2 n ⋆A x) (side1 n ⋆A x) (side3 n x)
    idp
    (& adapt-eq (& vid-square∙□vid-square∙□vid-square))
    (& coh4 (ap-square-from-αJ ⋆A (inJS-β n x)) (& (ap-square-comp-square2 (α∞ ⋆A))) ap-square-hid (ap-cube (α∞ ⋆A) (from-inJS-β n x))
            eq1
            eq2
      ∙ ! (& (coh-blip (β n x)) (ap-∘ (in∞ (S (S n))) (α (S n) ⋆A) (β n x))))
    (& coh (ap (ap from) (inJS-βS n (ι n x))))  where

  coh : {A : Type i} {a : A} → Coh ({p : a == a} (sq : p == idp) {b : A} {s : a == b}
        {c : A} {q : b == c} {d : A} {u u'' : c == d} {u= : u'' == u} {u' : b == d} {u'= : u' == q ∙ u''}
        {e : A} {t : c == e} {f : A} {v : e == f} {w : d == f} {ββ : Square t u v w} {k : a == d} {X : Square k s idp u'}
      → adapt-square ((sq |∙ vid-square {p = s}) ∙□ idp |∙ vid-square {p = q} ∙□ skew ββ) (& (Side1.coh n) u'= X u=) (& (Side3.coh n) u'= u= X ββ)
        == sq |∙ comp-square)
  coh = path-induction

  eq1 : natural-square (λ a₁ → ap (α∞ ⋆A) (from-inJS n a₁)) (β n x)
           (ap-∘ (from ∘ inJS (S n)) inr (β n x) ∙
            ap-∘ from (inJS (S n)) (ap inr (β n x)))
           (ap-∘ (in∞ (S (S n))) (α (S n) ⋆A) (β n x))
         == adapt-square (ap-square (α∞ ⋆A) (natural-square (from-inJS n) (β n x) (ap-∘ from (inJS n) (β n x)) idp)) (! (ap-from-αJ ⋆A (ap (inJS n) (β n x))) ∙ ! (ap (ap from) (ap-inJSS-ι n (β n x)))) (ap-α∞-in∞ (S n) ⋆A (β n x))
  eq1 = & (natural-square-ap (α∞ ⋆A)) (β n x) (from-inJS n) (coh' (β n x)) (coh'' (β n x))  where

    coh' : {x y : _} (p : x == y)
         → Square (∘-ap (α∞ ⋆A) (λ z → from (inJS n z)) p)
                  (ap (ap (α∞ ⋆A)) (ap-∘ from (inJS n) p))
                  (ap-∘ (from ∘ inJS (S n)) inr p
                    ∙ ap-∘ from (inJS (S n)) (ap inr p))
                  (! (ap-from-αJ ⋆A (ap (inJS n) p))
                    ∙ ! (ap (ap from) (ap-inJSS-ι n p)))
    coh' idp = ids

    coh'' : {x y : _} (p : x == y)
          → Square (∘-ap (α∞ ⋆A) (λ z → in∞ (S n) z) p)
                   idp
                   (ap-∘ (in∞ (S (S n))) (α (S n) ⋆A) p)
                   (ap-α∞-in∞ (S n) ⋆A p)
    coh'' idp = ids

  eq2 : ap-square (in∞ (S (S n))) (natural-square (β (S n)) (β n x) idp idp)
         == natural-square (λ a₁ → ap (in∞ (S (S n))) (β (S n) a₁)) (β n x)
                           (ap-∘ (in∞ (S (S n))) (α (S n) ⋆A) (β n x))
                           (ap-∘ (in∞ (S (S n))) inr (β n x))
  eq2 = & (ap-square-natural-square (in∞ (S (S n)))) (β n x) (β (S n)) ∙idp ∙idp

  coh4 : Coh ({A : Type i} {a b : A} {p : a == b} {c : A} {q q'' : a == c} {q''= : q'' == q} {q' : a == c}
         {q'= : q' == q''} {d : A} {r r' : b == d} {r= : r == r'}
         {s : c == d} {sq1 : Square p q r s} {e : A} {t : b == e} {f : A} {u : e == f} {v : d == f}
         {sqββ : Square t r' u v} {g : A} {k k' : a == g} {k= : k == k'} {l : c == g}
         {sq2 : Square q'' k l idp} {l' : c == g} {l= : l == l'} {u : g == b} {sqα : Square p k' idp u}
         {ur : g == d} {ur= : ur == u ∙ r} {sq3 : Square q k' l' idp}
         (cube-right : FlatCube sq2 sq3 q''= k= l= idp)
         {comp-square2' : _} (comp-square2'= : FlatCube comp-square2' (& comp-square2) idp idp idp ur=)
         {hid' : _} (hid'= : hid' == hid-square)
         {sqι : Square s l' idp ur} (cube-left : Cube sq1 comp-square2' sqα sq3 hid' sqι)
         {sqx : _} (eq1 : sqx == adapt-square sq1 (! q''= ∙ ! q'=) r=)
         {sqy : _} (eq2 : sqββ == sqy)
       → adapt-square (adapt-square (q'= |∙ sq2) k= l= ∙□ vid-square {p = u} ∙□ comp-square) (& (Side2.coh n) sqα) (& (Side3.coh n) ur= r= sqι sqββ)
         == square-symmetry sqx ∙□ square-symmetry sqy)
  coh4 = path-induction

from-inJ O ε = idp
from-inJ (S n) x = from-inJS n x

hdpssvs : Coh ({A : Type i} {x y : A} {p : x == y} → idp == horiz-degen-path (square-symmetry (vid-square {p = p})))
hdpssvs = path-induction

from-inJS O a = idp
from-inJS (S n) =
  JSS-elim n (from-inJSS-ι n)
             (from-inJSS-α n)
             (λ x   → ↓-='-from-square (ap-∘ from (inJS (S n)) (β (S n) x)) idp (square-symmetry (from-inJSS-β n x)))
             (λ a x → ↓-='-from-square (ap-∘ from (inJS (S n)) (γ n a x))   idp (square-symmetry (from-inJSS-γ n a x)))
             (λ x → cube-to-↓-square (from-inJSS-γ n ⋆A x)
                                     (& hdpssvs)
                                     (↓-ap-in-=' (ι (S n)) (from-inJSS-ι n))
                                     (from-inJSS-β n (ι n x))
                                     (ap-square-∘ from (inJS (S n)) (η n x) |∙³ from-inJSS-η n x))

from-inJS-ι O ε = ids
from-inJS-ι (S n) x = hid-square

from-inJS-α O a ε = ids
from-inJS-α (S n) a x = hid-square

from-inJS-β O ε = idc
from-inJS-β (S n) x = & coh (ap-square-horiz-degen-square (inJS-βS n x))
                            (natural-square-β (from-inJS (S n)) (β (S n) x) (push-βd _)) where

  coh : Coh ({A : Type i} {a b : A} {p : a == b} {q : a == a} {k : q == idp}
             {k' : Square q idp idp idp} (k= : k' == horiz-degen-square k)
             {c : A} {r : b == c} {sq : Square p q r (p ∙ r)} → sq == square-symmetry (k |∙ comp-square)
        → Cube sq (& comp-square2) hid-square k' hid-square hid-square)
  coh = path-induction

from-pushJ : (n : ℕ) (x : J n) → Square (ap from (pushJ n x)) (from-inJ n x) (from-inJ (S n) (ι n x)) (push∞ n x)
from-pushJ n x = & coh (δJ-β (inJ n x)) (ap from (inJS-ι n x)) (ap-∙! from _ _)
                       (natural-square δ∞ (from-inJ n x) (ap-idf (from-inJ n x)) idp) (from-inJS-ι n x)  where

  coh : Coh ({A : Type i} {a d : A} {p p' : a == d} (p= : p == p')
             {b : A} (q : b == d) {pq : a == b} (pq= : pq == p ∙ ! q)
             {c : A} {r : a == c} {f : A} {u : c == f} {e : A} {v : e == f}
             {s : d == e} (sq : Square p' r s (u ∙ ! v)) {t : b == f} (sq2 : Square t q idp (s ∙ v))
            → Square pq r t u)
  coh = path-induction

from-to : (x : J∞A) → from (to x) == x
from-to = J∞A-elim from-inJ (λ n x → ↓-='-from-square (ap-∘ from to (push∞ n x) ∙ ap (ap from) (push∞-β n x)) (ap-idf (push∞ n x)) (square-symmetry (from-pushJ n x)))

max_stars_repo_name: guillaumebrunerie/JamesConstruction

max_issues_repo_name: guillaumebrunerie/JamesConstruction

max_forks_repo_name: guillaumebrunerie/JamesConstruction


text:
-- A binding to a Haskell natural numbers type

open import Data.Nat using ( ℕ ) renaming ( zero to zero' ; suc to suc' )

module Data.Natural where

open import Data.Natural.Primitive public
  using ( Natural ; zero ; suc ; _+_ ; toString ; foldl ; foldl' ; foldr )
  renaming ( fromℕ to # )

% : Natural → ℕ
% = foldr suc' zero'

max_stars_repo_name: agda/agda-data-bindings

max_issues_repo_name: agda/agda-data-bindings

max_forks_repo_name: agda/agda-data-bindings


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

open import HoTT
open import cohomology.Theory

module cw.cohomology.InnerGrid {i} (OT : OrdinaryTheory i)
  (n : ℤ) {X Y Z W : Ptd i} (f : X ⊙→ Y) (g : Y ⊙→ Z) (h : Z ⊙→ W) where

  open OrdinaryTheory OT
  open import cohomology.PtdMapSequence cohomology-theory

{-

  X --> Y ---> Z ---> W
  |     |      |      |
  v     |      v      v
  1 ----+---> Z/X -> W/X
        |      | this |
        v      v  one v
        1 --> Z/Y -> W/Y

-}

  import cw.cohomology.GridPtdMap

  open cw.cohomology.GridPtdMap (g ⊙∘ f) h using ()
    renaming (Y/X-to-Z/X to Z/X-to-W/X; B/A-to-C/A to C/A-to-D/A;
      module B/AToC/A to C/AToD/A)

  open cw.cohomology.GridPtdMap f g
    using (Z/X-to-Z/Y; C/A-to-C/B; module C/AToC/B)

  open cw.cohomology.GridPtdMap f (h ⊙∘ g) using ()
    renaming (Z/X-to-Z/Y to W/X-to-W/Y; C/A-to-C/B to D/A-to-D/B;
      module C/AToC/B to D/AToD/B)

  open cw.cohomology.GridPtdMap g h using ()
    renaming (Y/X-to-Z/X to Z/Y-to-W/Y; B/A-to-C/A to C/B-to-D/B;
      module B/AToC/A to C/BToD/B)

  inner-grid-comm-sqr : CommSquare C/A-to-D/A C/B-to-D/B C/A-to-C/B D/A-to-D/B
  inner-grid-comm-sqr = comm-sqr $ Cofiber-elim idp (λ _ → idp)
    (λ a → ↓-='-in' $ ap-∘ C/B-to-D/B C/A-to-C/B (glue a)
                    ∙ ap (ap C/B-to-D/B) (C/AToC/B.glue-β a)
                    ∙ C/BToD/B.glue-β ((fst f) a)
                    ∙ ! (D/AToD/B.glue-β a)
                    ∙ ap (ap D/A-to-D/B) (! (C/AToD/A.glue-β a))
                    ∙ ∘-ap D/A-to-D/B C/A-to-D/A (glue a))

  C-inner-grid-commutes : CommSquareᴳ
    (C-fmap n Z/Y-to-W/Y) (C-fmap n Z/X-to-W/X) (C-fmap n W/X-to-W/Y) (C-fmap n Z/X-to-Z/Y)
  C-inner-grid-commutes = C-comm-square n inner-grid-comm-sqr


text:
-- {-# OPTIONS -v tc.meta:50 #-}
-- Andreas 2012-03-27, record pattern unification
{-# OPTIONS --irrelevant-projections #-}

module Issue376-irrelevant-projections where

open import Common.Equality
open import Common.Irrelevance

bla4 : (A : Set) ->
  let A' = Squash (Squash A) in
  let X : .(z : A') -> (C : .A' -> Set) -> (.(z : A') -> C z) -> C z
      X = _
  in  (a : A)(C : .A' -> Set)(k : .(z : A') -> C z) ->
      X (squash (squash a)) C k ≡ k (squash (squash a))
bla4 A a C k = refl


text:
{- 1. Booleans -}

data Bool : Set where
  true : Bool
  false : Bool

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

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

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

{- 2. Equality -}
data _≡_ {A : Set} (x : A) : (y : A) → Set where
  refl : x ≡ x

infix 4 _≡_

not-inv : (b : Bool) → not (not b) ≡ b
not-inv true = refl
not-inv false = refl

f : (b : Bool) → (not b) ∧ b ≡ false
f true = refl
f false = refl

max_stars_repo_name: erwinkn/program-eq-proof

max_issues_repo_name: erwinkn/program-eq-proof

max_forks_repo_name: erwinkn/program-eq-proof


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of left-scaling
------------------------------------------------------------------------

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

open import Relation.Binary

-- The properties are parameterised by the two carriers and
-- the result equality.

module Algebra.Module.Definitions.Left
  {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
  where

open import Data.Sum
open import Data.Product

------------------------------------------------------------------------
-- Binary operations

open import Algebra.Core

------------------------------------------------------------------------
-- Properties of operations

LeftIdentity : A → Opₗ A B → Set _
LeftIdentity a _∙ᴮ_ = ∀ m → (a ∙ᴮ m) ≈ m

Associative : Op₂ A → Opₗ A B → Set _
Associative _∙ᴬ_ _∙ᴮ_ = ∀ x y m → ((x ∙ᴬ y) ∙ᴮ m) ≈ (x ∙ᴮ (y ∙ᴮ m))

_DistributesOverˡ_ : Opₗ A B → Op₂ B → Set _
_*_ DistributesOverˡ _+_ =
  ∀ x m n → (x * (m + n)) ≈ ((x * m) + (x * n))

_DistributesOverʳ_⟶_ : Opₗ A B → Op₂ A → Op₂ B → Set _
_*_ DistributesOverʳ _+ᴬ_ ⟶ _+ᴮ_ =
  ∀ x m n → ((m +ᴬ n) * x) ≈ ((m * x) +ᴮ (n * x))

LeftZero : A → B → Opₗ A B → Set _
LeftZero zᴬ zᴮ _∙_ = ∀ x → (zᴬ ∙ x) ≈ zᴮ

RightZero : B → Opₗ A B → Set _
RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z

Commutative : Opₗ A B → Set _
Commutative _∙_ = ∀ x y m → (x ∙ (y ∙ m)) ≈ (y ∙ (x ∙ m))

LeftCongruent : Opₗ A B → Set _
LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_

RightCongruent : ∀ {ℓa} → Rel A ℓa → Opₗ A B → Set _
RightCongruent ≈ᴬ _∙_ = ∀ {m} → (_∙ m) Preserves ≈ᴬ ⟶ _≈_

Congruent : ∀ {ℓa} → Rel A ℓa → Opₗ A B → Set _
Congruent ≈ᴬ ∙ = ∙ Preserves₂ ≈ᴬ ⟶ _≈_ ⟶ _≈_


text:
------------------------------------------------------------------------------
-- Discussion about the inductive approach
------------------------------------------------------------------------------

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

-- Andrés: From our discussion about the inductive approach, can I
-- conclude that it is possible to rewrite the proofs using pattern
-- matching on _≡_, by proofs using only subst, because the types
-- associated with these proofs haven't proof terms?

-- Peter: Yes, provided the RHS of the definition does not refer to the
-- function defined, i e, there is no recursion.

module FOT.FOTC.InductiveApproach.Recursion where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Data.Nat
open import FOTC.Data.Nat.PropertiesI

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

-- foo is recursive and we pattern matching on _≡_.
foo : ∀ {m n} → N m → m ≡ n → N (m + n)
foo nzero refl = subst N (sym (+-leftIdentity zero)) nzero
foo (nsucc {m} Nm) refl = subst N helper (nsucc (nsucc (foo Nm refl)))
  where
  helper : succ₁ (succ₁ (m + m)) ≡ succ₁ m + succ₁ m
  helper =
    succ₁ (succ₁ (m + m)) ≡⟨ succCong (sym (+-Sx m m))  ⟩
    succ₁ (succ₁ m + m)   ≡⟨ succCong (+-comm (nsucc Nm) Nm) ⟩
    succ₁ (m + succ₁ m)   ≡⟨ sym (+-Sx m (succ₁ m)) ⟩
    succ₁ m + succ₁ m     ∎

-- foo' is recursive and we only use subst.
foo' : ∀ {m n} → N m → m ≡ n → N (m + n)
foo' {n = n} nzero h = subst N (sym (+-leftIdentity n)) (subst N h nzero)
foo' {n = n} (nsucc {m} Nm) h = subst N helper (nsucc (nsucc (foo' Nm refl)))
  where
  helper : succ₁ (succ₁ (m + m)) ≡ succ₁ m + n
  helper =
    succ₁ (succ₁ (m + m)) ≡⟨ succCong (sym (+-Sx m m))  ⟩
    succ₁ (succ₁ m + m)   ≡⟨ succCong (+-comm (nsucc Nm) Nm) ⟩
    succ₁ (m + succ₁ m)   ≡⟨ sym (+-Sx m (succ₁ m)) ⟩
    succ₁ m + succ₁ m     ≡⟨ +-rightCong h ⟩
    succ₁ m + n           ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Generics.Telescope where

open import Data.String using (String)
open import Generics.Prelude hiding (curry)

private variable
  l     : Level
  A B   : Set l
  a x y : A

data Telescope (A : Set l) : Setω

private variable T : Telescope A

levelOfTel : Telescope A → Level
⟦_⟧tel     : (T : Telescope A) → A → Set (levelOfTel T)

infixl 7 _⊢<_>_ _⊢_

data Telescope A where
  ε      : Telescope A
  _⊢<_>_ : ∀ (T : Telescope A) (ai : String × ArgInfo) {ℓ} (f : Σ A ⟦ T ⟧tel → Set ℓ) → Telescope A

_⊢_ : ∀ (T : Telescope A) {ℓ} (f : Σ A ⟦ T ⟧tel → Set ℓ) → Telescope A
T ⊢ f = T ⊢< "_" , arg-info visible (modality relevant quantity-ω) > f

extendTel : (T : Telescope A) (f : ∀ {x} → ⟦ T ⟧tel x → Set l) → Telescope A
extendTel T f = T ⊢ f ∘ proj₂

infixr 3 extendTel
syntax extendTel A (λ x → B) = x ∶ A , B

levelOfTel ε = lzero
levelOfTel (_⊢<_>_ T _ {ℓ} f) = levelOfTel T ⊔ ℓ

⟦ ε ⟧tel x = ⊤
⟦ T ⊢< n , i > f ⟧tel x = Σ[ t ∈ ⟦ T ⟧tel x ] < relevance i > f (x , t)

hideInfo : ArgInfo → ArgInfo
hideInfo i = arg-info hidden (getModality i)

ExTele : Telescope ⊤ → Setω
ExTele T = Telescope (⟦ T ⟧tel tt)

⟦_,_⟧xtel : (P : Telescope ⊤) (I : ExTele P) → Set (levelOfTel P ⊔ levelOfTel I)
⟦ P , V ⟧xtel = Σ (⟦ P ⟧tel tt) ⟦ V ⟧tel

⟦_,_&_⟧xtel : (P : Telescope ⊤) (V I : ExTele P) → Set (levelOfTel P ⊔ levelOfTel V ⊔ levelOfTel I)
⟦ P , V & I ⟧xtel = Σ[ p ∈ ⟦ P ⟧tel tt ] ⟦ V ⟧tel p × ⟦ I ⟧tel p

----------------------
-- Telescope currying

Curried′ : (T : Telescope A) → (⟦ T ⟧tel x → Set l) → Set (l ⊔ levelOfTel T)
Curried′ ε P = P tt
Curried′ (T ⊢< ai > g) P = Curried′ T λ t → Π< ai > (g (_ , t)) λ y → P (t , y)

Pred′ : (T : Telescope A) → (⟦ T ⟧tel x → Set l) → Set (l ⊔ levelOfTel T)
Pred′ ε P = P tt
Pred′ (T ⊢< n , i > g) P = Pred′ T λ t → Π< n , hideInfo i > (g (_ , t)) λ y → P (t , y)

uncurry′ : (T : Telescope A) (P : ⟦ T ⟧tel x → Set l) (B : Curried′ T P) → (y : ⟦ T ⟧tel x) → P y
uncurry′ ε P B tt = B
uncurry′ (T ⊢< i > f) P B (tx , gx) =
  app< i > (uncurry′ T (λ p → Π< i > (f (_ , p)) (λ y → P (p , y))) B tx) _

curry′ : (T : Telescope A) (P : ⟦ T ⟧tel x → Set l) → ((y : ⟦ T ⟧tel x) → P y) → Curried′ T P
curry′ ε P f = f tt
curry′ (T ⊢< i > S) P f =
  curry′ T _ λ t → fun< i > λ s → f (t , s)

unpred′ : (T : Telescope A) (P : ⟦ T ⟧tel x → Set l) (B : Pred′ T P) → (y : ⟦ T ⟧tel x) → P y
unpred′ ε P B tt = B
unpred′ (T ⊢< n , i > f) P B (tx , gx) =
  app< n , hideInfo i > (unpred′ T (λ p → Π< n , hideInfo i > (f (_ , p)) λ y → P (p , y)) B tx) _

pred′ : (T : Telescope A) (P : ⟦ T ⟧tel x → Set l) → ((y : ⟦ T ⟧tel x) → P y) → Pred′ T P
pred′ ε P f = f tt
pred′ (T ⊢< n , i > S) P f =
  pred′ T _ λ t → fun< n , hideInfo i > λ s → f (t , s)

Curried : ∀ P (I : ExTele P) {ℓ} (Pr : ⟦ P , I ⟧xtel → Set ℓ) → Set (levelOfTel P ⊔ levelOfTel I ⊔ ℓ)
Curried P I {ℓ} Pr = Curried′ P λ p → Curried′ I λ i → Pr (p , i)

curry : ∀ {P} {I : ExTele P} {ℓ} {Pr : ⟦ P , I ⟧xtel → Set ℓ}
      → ((pi : ⟦ P , I ⟧xtel) →  Pr pi) → Curried P I Pr
curry f = curry′ _ _ λ p → curry′ _ _ λ i → f (p , i)

uncurry : ∀ P (I : ExTele P) {ℓ} {Pr : ⟦ P , I ⟧xtel → Set ℓ} → Curried P I Pr → (pi : ⟦ P , I ⟧xtel) → Pr pi
uncurry P I C (p , i) = uncurry′ I _ (uncurry′ P _ C p) i

-- Type of parametrized, indexed sets: (p₁ : A₁) ... (pₙ : Aₙ) (i₁ : B₁) ... (iₚ : Bₚ) → Set ℓ
Indexed : ∀ P (I : ExTele P) ℓ → Set (levelOfTel P ⊔ levelOfTel I ⊔ lsuc ℓ)
Indexed P I ℓ = Curried P I (const (Set ℓ))

unindexed : ∀ P (I : ExTele P) ℓ → Indexed P I ℓ → ⟦ P , I ⟧xtel → Set ℓ
unindexed P I ℓ = uncurry P I

-- Type of predicates on parametrized & indexed families:
--   {p₁ : A₁} ... {pₙ : Aₙ} {i₁ : B₁} ... {iₚ : Bₚ} → X (p₁ ... iₚ) → Set ℓ
Pred : ∀ P (I : ExTele P) {a} (X : ⟦ P , I ⟧xtel → Set a) ℓ
     → Set (levelOfTel P ⊔ levelOfTel I ⊔ a ⊔ lsuc ℓ)
Pred P I X ℓ = Pred′ P λ p → Pred′ I λ i → X (p , i) → Set ℓ

unpred : ∀ P (I : ExTele P) {a} {X : ⟦ P , I ⟧xtel → Set a} ℓ → Pred P I X ℓ
       → (pi : ⟦ P , I ⟧xtel) → X pi → Set ℓ
unpred P I ℓ C (p , i) = unpred′ I _ (unpred′ P _ C p) i