text:
------------------------------------------------------------------------
-- Definitions of functions that generate list
------------------------------------------------------------------------

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

module Math.Combinatorics.ListFunction where

open import Data.List
open import Data.List.NonEmpty as NE using (List⁺)
open import Data.Nat
open import Data.Product as Prod using (_×_; _,_)
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])

module _ {a} {A : Set a} where
  -- applyEach (_+ 10) (upTo 3)
  -- >>> (10 ∷ 1 ∷ 2 ∷ []) ∷ (0 ∷ 11 ∷ 2 ∷ []) ∷ (0 ∷ 1 ∷ 12 ∷ []) ∷ []
  applyEach : (A → A) → List A → List (List A)
  applyEach f []       = []
  applyEach f (x ∷ xs) = (f x ∷ xs) ∷ map (x ∷_) (applyEach f xs)

module _ {a} {A : Set a} where
  -- Combinations
  -- combinations 2 (upTo 3)
  -- >>> (0 ∷ 1 ∷ []) ∷ (0 ∷ 2 ∷ []) ∷
  -- >>> (0 ∷ 3 ∷ []) ∷ (1 ∷ 2 ∷ []) ∷ (1 ∷ 3 ∷ []) ∷ (2 ∷ 3 ∷ []) ∷ []
  combinations : ℕ → List A → List (List A)
  combinations 0       xs       = [ [] ]
  combinations (suc k) []       = []
  combinations (suc k) (x ∷ xs) =
    map (x ∷_) (combinations k xs) ++ combinations (suc k) xs

  -- combinationsWithComplement 2 (upTo 2)
  -- >>> (0 ∷ 1 ∷ [] , 2 ∷ []) ∷
  -- >>> (0 ∷ 2 ∷ [] , 1 ∷ []) ∷ (1 ∷ 2 ∷ [] , 0 ∷ []) ∷ []
  combinationsWithComplement : ℕ → List A → List (List A × List A)
  combinationsWithComplement 0       xs       = [ [] , xs ]
  combinationsWithComplement (suc k) []       = []
  combinationsWithComplement (suc k) (x ∷ xs) =
    map (Prod.map₁ (x ∷_)) (combinationsWithComplement k xs) ++
    map (Prod.map₂ (x ∷_)) (combinationsWithComplement (suc k) xs)

  -- split list into two list (include empty list and order is preserved)
  -- splits₂ (upTo 3)
  -- >>> ([] , 0 ∷ 1 ∷ 2 ∷ []) ∷
  -- >>> (0 ∷ [] , 1 ∷ 2 ∷ []) ∷
  -- >>> (0 ∷ 1 ∷ [] , 2 ∷ []) ∷ (0 ∷ 1 ∷ 2 ∷ [] , []) ∷ []
  splits₂ : List A → List (List A × List A)
  splits₂ []       = ([] , []) ∷ []
  splits₂ (x ∷ xs) = ([] , x ∷ xs) ∷ map (Prod.map₁ (x ∷_)) (splits₂ xs)

  splits : ℕ → List A → List (List (List A))
  splits 0             xs = []
  splits 1             xs = [ xs ∷ [] ]
  splits (suc (suc k)) xs = concatMap f (splits (suc k) xs)
    where
    f : List (List A) → List (List (List A))
    f []         = []
    f (ys ∷ yss) = map (λ { (as , bs) → as ∷ bs ∷ yss }) (splits₂ ys)

  splits⁺₂Acc : A → List A → List (List⁺ A × List⁺ A)
  splits⁺₂Acc x []       = []
  splits⁺₂Acc x (y ∷ xs) = (x NE.∷ [] , y NE.∷ xs) ∷
                           map (Prod.map₁ (x NE.∷⁺_)) (splits⁺₂Acc y xs)

  -- split list into two list (exclude empty list and order is preserved)
  splits⁺₂ : List⁺ A → List (List⁺ A × List⁺ A)
  splits⁺₂ (x NE.∷ xs) = splits⁺₂Acc x xs

  splits⁺ : ℕ → List⁺ A → List (List (List⁺ A))
  splits⁺ 0             xs = []
  splits⁺ 1             xs = [ xs ∷ [] ]
  splits⁺ (suc (suc k)) xs = concatMap f (splits⁺ (suc k) xs)
    where
    f : List (List⁺ A) → List (List (List⁺ A))
    f []         = []
    f (ys ∷ yss) =
      map (λ { (as , bs) → as ∷ bs ∷ yss }) (splits⁺₂ ys)

  splits⁺AllAcc : A → List A → List⁺ (List⁺ (List⁺ A))
  splits⁺AllAcc x []       = ((x NE.∷ []) NE.∷ []) NE.∷ []
  splits⁺AllAcc x (y ∷ xs) =
    NE.map (λ zs → (x NE.∷ []) NE.∷⁺ zs) yss NE.⁺++⁺
    NE.map (λ { (z NE.∷ zs) → (x NE.∷⁺ z) NE.∷ zs} ) yss
    where yss = splits⁺AllAcc y xs

  splits⁺All : List⁺ A → List⁺ (List⁺ (List⁺ A))
  splits⁺All (x NE.∷ xs) = splits⁺AllAcc x xs

  -- Partition of set
  -- Generalization of `combinationsWithComplement`
  -- partitions 2 (upTo 3)
  -- >>> ((0 ∷ []) ∷ (1 ∷ 2 ∷ []) ∷ []) ∷
  -- >>> ((0 ∷ 1 ∷ []) ∷ (2 ∷ []) ∷ []) ∷
  -- >>> ((1 ∷ []) ∷ (0 ∷ 2 ∷ []) ∷ []) ∷ []
  partitions : ℕ → List A → List (List (List A))
  partitions 0       []       = [ [] ]
  partitions 0       (x ∷ xs) = []
  partitions (suc k) []       = []
  partitions (suc k) (x ∷ xs) =
    map ([ x ] ∷_) (partitions k xs) ++
    concatMap (applyEach (x ∷_)) (partitions (suc k) xs)

  partitionsAll : List A → List (List (List A))
  partitionsAll []       = [ [] ]
  partitionsAll (x ∷ xs) =
    map ([ x ] ∷_) yss ++ concatMap (applyEach (x ∷_)) yss
    where yss = partitionsAll xs

module _ {a} {A : Set a} where
  -- insertEverywhere 100 (upTo 2)
  -- >>> (100 ∷ 0 ∷ 1 ∷ []) ∷ (0 ∷ 100 ∷ 1 ∷ []) ∷ (0 ∷ 1 ∷ 100 ∷ []) ∷ []
  insertEverywhere : A → List A → List (List A)
  insertEverywhere x []       = [ [ x ] ]
  insertEverywhere x (y ∷ ys) = (x ∷ y ∷ ys) ∷ map (y ∷_) (insertEverywhere x ys)

module _ {a} {A : Set a} where
  -- permutations (upTo 2)
  -- >>> (0 ∷ 1 ∷ []) ∷ (1 ∷ 0 ∷ []) ∷ []
  permutations : List A → List (List A)
  permutations []       = [ [] ]
  permutations (x ∷ xs) = concatMap (insertEverywhere x) (permutations xs)


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

module Cubical.ZCohomology.EilenbergSteenrodZ where

open import Cubical.Homotopy.EilenbergSteenrod

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.Properties
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Groups.Wedge
open import Cubical.ZCohomology.Groups.Sn

open import Cubical.Relation.Nullary

open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Int
open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws renaming (assoc to assoc∙)
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.SetTruncation
  renaming (map to sMap ; rec to sRec ; elim2 to sElim2; elim to sElim ; rec2 to sRec2)
open import Cubical.HITs.PropositionalTruncation
  renaming (map to pMap ; rec to pRec ; elim to pElim ; elim2 to pElim2)
open import Cubical.HITs.Truncation
  renaming (rec to trRec ; map to trMap ; elim to trEilim ; elim2 to trElim2)
open import Cubical.HITs.Susp
open import Cubical.HITs.Pushout
open import Cubical.HITs.Wedge
open import Cubical.HITs.Sn
open import Cubical.HITs.S1

open import Cubical.Algebra.Group
open import Cubical.Algebra.AbGroup

open coHomTheory
open Iso
open IsGroup
open GroupStr
open GroupIso
open GroupHom

private
  suspΩFun' : ∀ {ℓ} {A : Type ℓ} (n : ℕ) (f : A → Path _ (0ₖ _) (0ₖ _))
           → Susp A → coHomK (suc n)
  suspΩFun' n f north = 0ₖ _
  suspΩFun' n f south = 0ₖ _
  suspΩFun' n f (merid a i) = f a i

  suspΩFun : ∀ {ℓ} {A : Type ℓ} (n : ℕ) (f : A → coHomK n) → Susp A → coHomK (suc n)
  suspΩFun n f = suspΩFun' n λ a → Kn→ΩKn+1 n (f a)

  ≡suspΩFun : ∀ {ℓ} (n : ℕ) (A : Pointed ℓ) (f : Susp (typ A) → coHomK (suc n)) (p : f north ≡ 0ₖ _)
            → f ≡ suspΩFun' n λ a → sym p ∙∙ (cong f (merid a)) ∙∙ (cong f (sym (merid (pt A))) ∙ p)
  ≡suspΩFun n s f p i north = p i
  ≡suspΩFun n s f p i south = (cong f (sym (merid (pt s))) ∙ p) i
  ≡suspΩFun n s f p i (merid a j) =
    doubleCompPath-filler (sym p) (cong f (merid a)) (cong f (sym (merid (pt s))) ∙ p) i j

-- induction principle for Hⁿ(Susp A)
SuspCohomElim : ∀ {ℓ ℓ'} {A : Pointed ℓ} (n : ℕ) {B : coHom (suc n) (Susp (typ A)) → Type ℓ'}
             → ((x : coHom (suc n) (Susp (typ A))) → isProp (B x))
             → ((f : typ A → Path _ (0ₖ _) (0ₖ _)) → f (pt A) ≡ refl → B ∣ suspΩFun' n f ∣₂)
             → (x : _) → B x
SuspCohomElim {A = A} n {B = B} isprop f =
  coHomPointedElim _ north isprop λ g gid
    → subst (B ∘ ∣_∣₂) (sym (≡suspΩFun n A g gid))
                       (f _ ((λ i → (sym gid ∙∙ (λ j → g (merid (pt A) (~ i ∧ j))) ∙∙ ((λ j → g (merid (pt A) (~ i ∧ ~ j))) ∙ gid)))
                                  ∙∙ (λ i → (λ j → gid (i ∨ ~ j)) ∙∙ refl ∙∙ lUnit (λ j → gid (i ∨ j)) (~ i))
                                  ∙∙ sym (rUnit refl)))

-- (Reduced) cohomology functor
coHomFunctor : {ℓ : Level}  (n : Int) → Pointed ℓ → AbGroup {ℓ}
coHomFunctor (pos n) = coHomRedGroup n
coHomFunctor (negsuc n) _ = trivialAbGroup

-- Alternative definition with reduced groups replaced by unrecued one for n ≥ 1
coHomFunctor' : {ℓ : Level} (n : Int) → Pointed ℓ → AbGroup {ℓ}
coHomFunctor' (pos zero) = coHomFunctor 0
coHomFunctor' (pos (suc n)) A = coHomGroup (suc n) (typ A)
coHomFunctor' (negsuc n) = coHomFunctor (negsuc n)

coHomFunctor≡coHomFunctor' : ∀ {ℓ} → coHomFunctor {ℓ} ≡ coHomFunctor'
coHomFunctor≡coHomFunctor' = funExt λ {(pos zero) → refl
                                     ; (pos (suc n)) → funExt λ A → sym (coHomGroup≡coHomRedGroup n A)
                                     ; (negsuc n) → refl}

-- Ĥ⁰(Susp A) is contractible
H0-susp : ∀ {ℓ} {A : Pointed ℓ} → isContr (coHomRed 0 (Susp (typ A) , north))
fst H0-susp = 0ₕ∙ _
snd (H0-susp {A = A}) =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        λ {(f , p)
          → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _)
                        (funExt λ {north → sym p
                                 ; south → sym p ∙ cong f (merid (pt A))
                                 ; (merid a i) j → isSet→isSet' (isSetInt)
                                                                  (sym p)
                                                                  (sym p ∙ cong f (merid (pt A)))
                                                                  refl (cong f (merid a)) i j}))}
-- We need that Hⁿ⁺¹(Susp A) ≃ Hⁿ(A)

private
  suspFunCharacFun : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ)
                     → ((Susp (typ A)) → coHomK (suc n))
                     → (typ A → (coHomK n))
  suspFunCharacFun {A = A} n f x = ΩKn+1→Kn n (sym (rCancelₖ (suc n) (f north))
                                                     ∙∙ cong (λ x → f x -[ (suc n) ]ₖ f north) ((merid x) ∙ sym (merid (pt A)))
                                                     ∙∙ rCancelₖ (suc n) (f north))

  linvLem : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) (f : typ A → Path (coHomK (suc n)) (0ₖ _) (0ₖ _))
                        (fId : f (pt A) ≡ refl)
                     → (x : _) → suspΩFun n (suspFunCharacFun {A = A} n (suspΩFun' n f)) x
                                 ≡ suspΩFun' n f x
  linvLem n f fId north = refl
  linvLem n f fId south = refl
  linvLem {A = A} n f fId (merid x i) j = helper n x f fId j i
    where
    helper : (n : ℕ) (a : typ A) (f : typ A → Path (coHomK (suc n)) (0ₖ _) (0ₖ _))
                       (fId : f (pt A) ≡ refl)
                     → Kn→ΩKn+1 n (suspFunCharacFun {A = A} n (suspΩFun' n f) a) ≡ f a
    helper zero a f fId =
        Iso.rightInv (Iso-Kn-ΩKn+1 0) (sym (rCancelₖ _ (0ₖ 1))
                                    ∙∙ cong (λ x → suspΩFun' 0 f x +ₖ 0ₖ 1) (merid a ∙ (sym (merid (pt A))))
                                    ∙∙ rCancelₖ _ (0ₖ 1))
     ∙∙ (λ i → sym (transportRefl (λ _ → 0ₖ 1) i)
             ∙∙ cong (λ x → rUnitₖ 1 (suspΩFun' 0 f x) i) (merid a ∙ (sym (merid (pt A))))
             ∙∙ transportRefl (λ _ → 0ₖ 1) i)
     ∙∙ (λ i → rUnit (congFunct (suspΩFun' 0 f) (merid a) (sym (merid (pt A))) i) (~ i))
     ∙∙ cong (λ p → f a ∙ sym p) fId
     ∙∙ sym (rUnit (f a))
    helper (suc n) a f fId =
         Iso.rightInv (Iso-Kn-ΩKn+1 (suc n))
                           (sym (rCancelₖ _ (0ₖ (suc (suc n))))
                        ∙∙ cong (λ x → suspΩFun' (suc n) f x +ₖ 0ₖ (suc (suc n))) (merid a ∙ (sym (merid (pt A))))
                        ∙∙ rCancelₖ _ (0ₖ (suc (suc n))))
      ∙∙ ((λ i → sym (transportRefl (λ _ → 0ₖ (suc (suc n))) i)
                   ∙∙ cong (λ x → rUnitₖ (suc (suc n)) (suspΩFun' (suc n) f x) i) (merid a ∙ (sym (merid (pt A))))
                   ∙∙ transportRefl (λ _ → 0ₖ (suc (suc n))) i))
      ∙∙ (λ i → rUnit (congFunct (suspΩFun' (suc n) f) (merid a) (sym (merid (pt A))) i) (~ i))
      ∙∙ cong (λ p → f a ∙ sym p) fId
      ∙∙ sym (rUnit (f a))

suspFunCharac : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → Iso (coHom (suc (suc n)) (Susp (typ A))) (coHom (suc n) (typ A))
fun (suspFunCharac {A = A} n) =
  sMap λ f → suspFunCharacFun {A = A} (suc n) f
inv (suspFunCharac {A = A} n) = sMap (suspΩFun (suc n))
rightInv (suspFunCharac {A = A} n) =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
    (λ f → trRec (isProp→isOfHLevelSuc n (setTruncIsSet _ _))
                  (λ fId → cong ∣_∣₂ (funExt λ x → (cong (ΩKn+1→Kn (suc n))
                                                            ((λ i → (sym (transportRefl (λ _ → 0ₖ _) i)
                                                                ∙∙ cong (λ x → suspΩFun (suc n) f x +ₖ 0ₖ _)
                                                                        (merid x ∙ sym (merid (pt A)))
                                                                ∙∙ transportRefl (λ _ → 0ₖ _) i))
                                                         ∙∙ (sym (rUnit (cong (λ x → suspΩFun (suc n) f x +ₖ 0ₖ _)
                                                                                ((merid x) ∙ sym (merid (pt A))))))
                                                         ∙∙ (λ i → congFunct (λ x → rUnitₖ _ (suspΩFun (suc n) f x) i)
                                                                              (merid x) (sym (merid (pt A))) i)))
                                                 ∙∙ ΩKn+1→Kn-hom (suc n) (Kn→ΩKn+1 (suc n) (f x))
                                                                  (sym (Kn→ΩKn+1 (suc n) (f (pt A))))
                                                 ∙∙ cong₂ _+ₖ_ (Iso.leftInv (Iso-Kn-ΩKn+1 (suc n)) (f x))
                                                               (cong (λ x → ΩKn+1→Kn (suc n) (sym (Kn→ΩKn+1 (suc n) x))) fId)
                                                 ∙∙ cong (λ y → f x +ₖ ΩKn+1→Kn (suc n) (sym y)) (Kn→ΩKn+10ₖ (suc n))
                                                 ∙∙ cong (f x +ₖ_) (ΩKn+1→Kn-refl (suc n))
                                                  ∙ rUnitₖ _ (f x)))
                  (fst (isConnectedPathKn n (f (pt A)) (0ₖ _))))
leftInv (suspFunCharac {A = A} n) =
  SuspCohomElim {A = A} _ (λ _ → setTruncIsSet _ _)
    λ f fId → cong ∣_∣₂ (funExt (linvLem (suc n) f fId))

-- We also need that H¹(Susp A) ≃ Ĥ⁰(A)
suspFunCharac0 : ∀ {ℓ} {A : Pointed ℓ} → Iso (∥ ((Susp (typ A)) → coHomK 1) ∥₂) ∥ A →∙ (Int , 0) ∥₂
fun (suspFunCharac0 {A = A}) =
    sMap λ f → suspFunCharacFun {A = A} 0 f
  ,  (cong (ΩKn+1→Kn 0) ((λ i → sym (rCancelₖ _ (f north))
                                   ∙∙ cong (λ x → f x -ₖ f north) (rCancel (merid (pt A)) i)
                                   ∙∙ rCancelₖ _ (f north))
                      ∙∙ (doubleCompPath-elim (sym (rCancelₖ _ (f north))) refl (rCancelₖ _ (f north)))
                      ∙∙ (cong (_∙ (rCancelₖ _ (f north))) (sym (rUnit (sym (rCancelₖ _ (f north))))))
                       ∙ (lCancel (rCancelₖ _ (f north)))))
inv suspFunCharac0 = sMap λ f → suspΩFun 0 (fst f)
rightInv (suspFunCharac0 {A = A}) =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
    λ {(f , p)
      → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _)
                   (funExt (λ x → (λ j → transp (λ i → helix (wedgeMapS¹ (intLoop (p j) (~ i)) base)) j
                                             ((transport (λ i → helix (trRec isGroupoidS¹ (λ x → x)
                                                                              (rUnitₖ 1 ∣ intLoop (f x) i ∣ j)))
                                                         (pos 0))))
                                 ∙ windingIntLoop (f x))))}
leftInv (suspFunCharac0 {A = A}) =
  SuspCohomElim {A = A} _ (λ _ → setTruncIsSet _ _)
    λ f fId → cong ∣_∣₂ (funExt (linvLem 0 f fId))

-- We now prove that the alternative definition of cohomology is a cohomology theory.
private
  -- First, we need to that coHomFunctor' is contravariant
  theMorph : ∀ {ℓ} (n : Int) {A B : Pointed ℓ} (f : A →∙ B)
          → AbGroupHom (coHomFunctor' n B) (coHomFunctor' n A)
  fun (theMorph (pos zero) f) = sMap λ g → (λ x → fst g (fst f x)) , cong (fst g) (snd f) ∙ snd g
  isHom (theMorph (pos zero) f) =
    sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
           λ f g → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) refl)
  theMorph (pos (suc n)) f = coHomMorph _ (fst f)
  fun (theMorph (negsuc n) f) = idfun _
  isHom (theMorph (negsuc n) f) _ _ = refl

  open coHomTheory
  isCohomTheoryZ' : ∀ {ℓ} → coHomTheory {ℓ} coHomFunctor'
  Hmap isCohomTheoryZ' = theMorph

  -------------------------- Suspension --------------------------
  -- existence of suspension isomorphism
  fst (Suspension isCohomTheoryZ') (pos zero) {A = A} =
      invGroupEquiv
      (GrIsoToGrEquiv
        (Iso+Hom→GrIso (invIso suspFunCharac0)
                        (sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                λ f g → cong ∣_∣₂ (funExt λ { north → refl
                                                           ; south → refl
                                                           ; (merid a i) j → helper a (fst f) (fst g) j i}))))
    where
    helper : (a : typ A) (f g : typ A → coHomK 0)
          → Kn→ΩKn+1 0 (f a +[ 0 ]ₖ g a)
           ≡ cong₂ _+ₖ_ (Kn→ΩKn+1 0 (f a)) (Kn→ΩKn+1 0 (g a))
    helper a f g = Kn→ΩKn+1-hom 0 (f a) (g a)
                ∙ ∙≡+₁ (Kn→ΩKn+1 _ (f a)) (Kn→ΩKn+1 _ (g a))
  fst (Suspension isCohomTheoryZ') (pos (suc n)) {A = A} =
      invGroupEquiv
      (GrIsoToGrEquiv
        (Iso+Hom→GrIso (invIso (suspFunCharac {A = A} n))
                        (sElim2 (λ _ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                                λ f g → cong ∣_∣₂ (funExt λ { north → refl
                                                           ; south → refl
                                                           ; (merid a i) j → helper a f g j i}))))
    where
    helper : (a : typ A) (f g : typ A → coHomK (suc n))
          → Kn→ΩKn+1 (suc n) (f a +ₖ g a)
           ≡ cong₂ _+ₖ_ (Kn→ΩKn+1 (suc n) (f a)) (Kn→ΩKn+1 (suc n) (g a))
    helper a f g = Kn→ΩKn+1-hom (suc n) (f a) (g a)
                ∙ ∙≡+₂ n (Kn→ΩKn+1 _ (f a)) (Kn→ΩKn+1 _ (g a))
  fst (Suspension isCohomTheoryZ') (negsuc zero) {A = A} =
      GrIsoToGrEquiv (Iso+Hom→GrIso (isContr→Iso (H0-susp {A = _ , pt A}) isContrUnit*)
                      λ _ _ → refl)
  fst (Suspension isCohomTheoryZ') (negsuc (suc n)) = idGroupEquiv _

  -- naturality of the suspension isomorphism
  snd (Suspension (isCohomTheoryZ' {ℓ})) (f , p) (pos zero) =
    funExt (sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
           λ {(f , _) → cong ∣_∣₂ (funExt λ {north → refl
                                          ; south → refl
                                          ; (merid a i) → refl})})
  snd (Suspension (isCohomTheoryZ' {ℓ})) (f , p) (pos (suc n)) =
    funExt (sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
           λ f → cong ∣_∣₂ (funExt λ {north → refl
                                    ; south → refl
                                    ; (merid a i) → refl}))
  snd (Suspension (isCohomTheoryZ' {ℓ})) (f , p) (negsuc zero) = refl
  snd (Suspension (isCohomTheoryZ' {ℓ})) (f , p) (negsuc (suc n)) = refl

  -------------------------- Exactness ---------------------------
  Exactness isCohomTheoryZ' {A = A} {B = B} f n = isoToPath (exactnessIso n f)
    where
    exactnessIso : (n : Int) (f : A →∙ B)
                → Iso (Ker (theMorph n f)) (Im (theMorph n (cfcod (fst f) , refl)))
    fun (exactnessIso (pos zero) (f , p)) =
      uncurry (sElim (λ _ → isSetΠ λ _ → isSetΣ setTruncIsSet λ _ → isProp→isSet propTruncIsProp)
                     λ {(g , q) inker → ∣ g , q ∣₂
                                       , pRec propTruncIsProp
                                              (λ gId → ∣ ∣ (λ { (inl tt) → 0
                                                              ; (inr b) → g b
                                                              ; (push a i) → funExt⁻ (cong fst gId) a (~ i)}) , q ∣₂
                                                       , cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) refl) ∣)
                                              (Iso.fun PathIdTrunc₀Iso inker)})
    inv (exactnessIso (pos zero) (f , p)) =
      uncurry (sElim (λ _ → isSetΠ λ _ → isSetΣ setTruncIsSet λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                λ {(g , q) inim'
                  → ∣ g , q ∣₂
                   , pRec (setTruncIsSet _ _)
                          (uncurry
                            (sElim (λ _ → isSetΠ (λ _ → isOfHLevelPath 2 setTruncIsSet _ _))
                                   (λ pushmap pushId'
                                     → pRec (setTruncIsSet _ _)
                                             (λ pushId
                                               → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _)
                                                             (funExt λ x → sym (funExt⁻ (cong fst pushId) (f x))
                                                                         ∙∙ cong (fst pushmap) (sym (push x) ∙ push (pt A))
                                                                         ∙∙ (cong (fst pushmap ∘ inr) p
                                                                           ∙ snd pushmap))))
                                             (Iso.fun PathIdTrunc₀Iso pushId'))))
                          inim'})
    rightInv (exactnessIso (pos zero) (f , p)) =
      uncurry (sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2
                                              (isSetΣ setTruncIsSet
                                                      (λ _ → isProp→isSet propTruncIsProp)) _ _)
                     λ {(p , q) _ → Σ≡Prop (λ _ → propTruncIsProp) refl})
    leftInv (exactnessIso (pos zero) (f , p)) =
      uncurry (sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2
                                              (isSetΣ setTruncIsSet
                                                      (λ _ → isProp→isSet (setTruncIsSet _ _))) _ _)
                     λ {(p , q) _ → Σ≡Prop (λ _ → setTruncIsSet _ _) refl})
    fun (exactnessIso (pos (suc n)) f) ker = (fst ker) , inIm-helper (fst ker) (snd ker)
      where
      inIm-helper : (x : coHom (suc n) (typ B))
                  → isInKer _ _ (theMorph (pos (suc n)) {A = A} {B = B} f) x
                  → isInIm _ _ (theMorph (pos (suc n)) {A = B} {B = _ , inr (pt B)} (cfcod (fst f) , refl)) x
      inIm-helper =
        coHomPointedElim _ (pt B) (λ _ → isPropΠ λ _ → propTruncIsProp)
          λ g gId inker → pRec propTruncIsProp
                               (λ gIdTot → ∣ ∣ (λ { (inl tt) → 0ₖ _
                                                  ; (inr b) → g b
                                                  ; (push a i) → funExt⁻ gIdTot a (~ i)}) ∣₂
                                             , cong ∣_∣₂ (funExt λ b → refl) ∣)
                               (Iso.fun PathIdTrunc₀Iso inker)
    inv (exactnessIso (pos (suc n)) f) im = fst im , inKer-helper (fst im) (snd im)
      where
      inKer-helper : (x : coHom (suc n) (typ B))
                  → isInIm _ _ (theMorph (pos (suc n)) {A = B} {B = _ , inr (pt B)} (cfcod (fst f) , refl)) x
                  → isInKer _ _ (theMorph (pos (suc n)) {A = A} {B = B} f) x
      inKer-helper =
        coHomPointedElim _ (pt B) (λ _ → isPropΠ λ _ → setTruncIsSet _ _)
          λ g gId → pRec (setTruncIsSet _ _)
                          (uncurry λ cg p
                            → subst (isInKer (coHomGr (suc n) (typ B)) (coHomGr (suc n) (typ A))
                                                                        (coHomMorph (suc n) (fst f)))
                                     p
                                     (helper cg))
         where
         helper : (cg : _) → coHomFun (suc n) (fst f) (coHomFun (suc n) (cfcod (fst f)) cg) ≡ 0ₕ _
         helper = sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
                        λ cg → trRec (isProp→isOfHLevelSuc n (setTruncIsSet _ _))
                                      (λ p → (cong ∣_∣₂ (funExt λ x → cong cg (sym (push x))
                                                                    ∙ p)))
                                      (isConnectedPathKn _ (cg (inl tt)) (0ₖ (suc n)) .fst)
    rightInv (exactnessIso (pos (suc n)) f) _ = Σ≡Prop (λ _ → propTruncIsProp) refl
    leftInv (exactnessIso (pos (suc n)) f) _ = Σ≡Prop (λ _ → setTruncIsSet _ _) refl
    exactnessIso (negsuc n) (f , p) =
      isContr→Iso ((tt* , refl)
                   , λ {(tt* , p) → Σ≡Prop (λ _ → isOfHLevelPath 1 isPropUnit* _ _)
                                            refl})
                   ((tt* , ∣ tt* , refl ∣)
                   , λ {(tt* , p) → Σ≡Prop (λ _ → propTruncIsProp)
                                            refl})

  -------------------------- Dimension ---------------------------
  Dimension isCohomTheoryZ' (pos zero) p = ⊥-rec (p refl)
  fst (Dimension isCohomTheoryZ' (pos (suc n)) _) = 0ₕ _
  snd (Dimension isCohomTheoryZ' (pos (suc n)) _) =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
          (λ f → trRec (isProp→isOfHLevelSuc n (setTruncIsSet _ _))
                        (λ f-true → trRec (isProp→isOfHLevelSuc n (setTruncIsSet _ _))
                                          (λ f-false → cong ∣_∣₂ (funExt (λ {(lift true) → f-true
                                                                          ; (lift false) → f-false})))
                                          (isConnectedPathKn n (0ₖ _) (f (lift false)) .fst))
                        (isConnectedPathKn n (0ₖ _) (f (lift true)) .fst))
  Dimension isCohomTheoryZ' (negsuc n) _ = isContrUnit*

  ------------------------ Binary wedges -------------------------
  BinaryWedge isCohomTheoryZ' (pos zero) = GrIsoToGrEquiv (H⁰Red-⋁ _ _)
  BinaryWedge isCohomTheoryZ' (pos (suc n)) = GrIsoToGrEquiv (Hⁿ-⋁ _ _ n)
  BinaryWedge isCohomTheoryZ' (negsuc n) =
    GrIsoToGrEquiv
      (compGroupIso (IsoContrGroupTrivialGroup isContrUnit*)
                    (invGroupIso (IsoContrGroupTrivialGroup (isOfHLevel× 0 isContrUnit* isContrUnit*))))

-- Substituting back for our original theory, we are done
isCohomTheoryZ : ∀ {ℓ} → coHomTheory {ℓ} coHomFunctor
isCohomTheoryZ = subst coHomTheory (sym coHomFunctor≡coHomFunctor')
                       isCohomTheoryZ'

ext: agda

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Modal where

open import Prelude
open import Star

data Progress (A : Set) : Set where
  cont : A -> Progress A
  stop : Progress A

record Some {A : Set}(R : Rel A) : Set where
  field
    a    : A
    b    : A
    edge : R a b

some : {A : Set}{R : Rel A}{a b : A} -> R a b -> Some R
some x = record {a = _; b = _; edge = x}

EdgePred : {A : Set} -> Rel A -> Set1
EdgePred R = forall {a b} -> R a b -> Set

data PStep {A : Set}{R : Rel A}(P : EdgePred R) :
           Rel (Progress (Some (Star R))) where
  step : {a b c : A}{x : R a b}{xs : Star R b c} ->
         PStep P (cont (some (x • xs))) (cont (some xs))
  done : {a b c : A}{x : R a b}{xs : Star R b c} ->
         P x -> PStep P (cont (some (x • xs))) stop

Any : {A : Set}{R : Rel A}(P : EdgePred R) -> EdgePred (Star R)
Any P xs = Star (PStep P) (cont (some xs)) stop

mapAny : {A₁ A₂ : Set}{R₁ : Rel A₁}{R₂ : Rel A₂}
         {P₁ : EdgePred R₁}{P₂ : EdgePred R₂}{a b : A₁}{xs : Star R₁ a b}
         {i : A₁ -> A₂}{f : R₁ =[ i ]=> R₂} ->
         ({a b : A₁}{x : R₁ a b} -> P₁ x -> P₂ (f x)) ->
         Any P₁ xs -> Any (\{a b} -> P₂{a}{b}) (map i f xs)
mapAny h (step   • i) = step • mapAny h i
mapAny h (done p • ε) = done (h p) • ε
mapAny h (done p • (() • _))

data Check {A : Set}{R : Rel A}(P : EdgePred R) :
           Rel (Some (Star R)) where
  check : {a b c : A}{x : R a b}{xs : Star R b c} ->
          P x -> Check P (some (x • xs)) (some xs)

checkedEdge : {A : Set}{R : Rel A}{P : EdgePred R}{xs ys : Some (Star R)} ->
              Check P xs ys -> Some R
checkedEdge (check {x = x} _) = some x

uncheck : {X : Set}{R : Rel X}{P : EdgePred R}{xs ys : Some (Star R)}
          (chk : Check P xs ys) -> P (Some.edge (checkedEdge chk))
uncheck (check p) = p

All : {A : Set}{R : Rel A}(P : EdgePred R) -> EdgePred (Star R)
All P {a}{b} xs = Star (Check P) (some xs) (some {a = b} ε)

data Lookup {A : Set}{R : Rel A}(P Q : EdgePred R) : Set where
  result : {a b : A} -> (x : R a b) -> P x -> Q x -> Lookup P Q

lookup : {A : Set}{R : Rel A}{P Q : EdgePred R}{a b : A}{xs : Star R a b} ->
         Any P xs -> All Q xs -> Lookup (\{a b} -> P{a}{b}) Q
lookup (step   • i) (check _ • xs) = lookup i xs
lookup (done p • ε) (check q • _ ) = result _ p q
lookup (done p • (() • _)) (check q • _ )

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Utils.Product where

open import Level
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality

-- "very dependent" versions of map and zipWith
map⁎ : ∀ {a b p q} {A : Set a} {B : A → Set b} {P : A → Set p} {Q : {x : A} → P x → B x → Set q} →
      (f : (x : A) → B x) → (∀ {x} → (y : P x) → Q y (f x)) → (v : Σ A P) → Σ (B (proj₁ v)) (Q (proj₂ v))
map⁎ f g (x , y) = (f x , g y)

map⁎′ : ∀ {a b p q} {A : Set a} {B : A → Set b} {P : Set p} {Q : P → Set q} → (f : (x : A) → B x) → ((x : P) → Q x) → (v : A × P) → B (proj₁ v) × Q (proj₂ v)
map⁎′ f g (x , y) = (f x , g y)

zipWith : ∀ {a b c p q r s} {A : Set a} {B : Set b} {C : Set c} {P : A → Set p} {Q : B → Set q} {R : C → Set r} {S : (x : C) → R x → Set s} (_∙_ : A → B → C) → (_∘_ : ∀ {x y} → P x → Q y → R (x ∙ y)) → (_*_ : (x : C) → (y : R x) → S x y) → (x : Σ A P) → (y : Σ B Q) → S (proj₁ x ∙ proj₁ y) (proj₂ x ∘ proj₂ y)
zipWith _∙_ _∘_ _*_ (a , p) (b , q) = (a ∙ b) * (p ∘ q)
syntax zipWith f g h = f -< h >- g

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.SetoidDiscrete where

open import Categories.Category

open import Level
open import Relation.Binary using (Setoid)
open import Function
open import Data.Unit

{-
 This is a better version of Discrete, which is more in line with
 the rest of this library, and makes a Category out of a Setoid.
 But here we have no choice, and we need to truncate the equivalence.
-}

Discrete : ∀ {o ℓ e} (A : Setoid o ℓ) → Category o ℓ e
Discrete {_} {_} {e} A = record
  { Obj       = Carrier
  ; _⇒_       = _≈_
  ; _≈_       = λ _ _ → Lift e ⊤
  ; id        = refl
  ; _∘_       = flip trans
  }
  where
  open Setoid A

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Setoids.Setoids
open import Rings.Definition
open import Rings.PrincipalIdealDomains.Definition
open import Rings.IntegralDomains.Definition
open import Rings.Ideals.Maximal.Definition

module Rings.PrincipalIdealDomains.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) (pid : {c : _} → PrincipalIdealDomain intDom {c}) where

open import Rings.Ideals.Definition R
open import Rings.Irreducibles.Definition intDom
open import Rings.Ideals.Principal.Definition R
open import Rings.Divisible.Definition R
open import Rings.Associates.Lemmas intDom
open import Rings.Ideals.Lemmas R
open import Rings.Units.Definition R
open import Rings.Irreducibles.Lemmas intDom
open import Rings.Units.Lemmas R
open import Rings.Ideals.Prime.Definition {R = R}
open import Rings.Ideals.Prime.Lemmas {R = R}
open import Rings.Primes.Definition intDom
open import Rings.Primes.Lemmas intDom
open import Rings.Ideals.Principal.Lemmas R
open import Rings.Ideals.Maximal.Lemmas {R = R}

open Ring R
open Setoid S
open Equivalence eq

irreducibleImpliesMaximalIdeal : {r : A} → Irreducible r → {d : _} → MaximalIdeal (generatedIdeal r) {d}
MaximalIdeal.notContained (irreducibleImpliesMaximalIdeal {r} irred {d}) = 1R
MaximalIdeal.notContainedIsNotContained (irreducibleImpliesMaximalIdeal {r} irred {d}) = Irreducible.nonunit irred
MaximalIdeal.isMaximal (irreducibleImpliesMaximalIdeal {r} irred {d}) {biggerPred} bigger biggerContains (outsideR , (biggerContainsOutside ,, notInR)) {x} = biggerPrincipal' (unitImpliesGeneratedIdealEverything w {x})
  where
    biggerGen : A
    biggerGen = PrincipalIdeal.generator (pid bigger)
    biggerPrincipal : {x : A} → biggerPred x → biggerGen ∣ x
    biggerPrincipal = PrincipalIdeal.genGenerates (pid bigger)
    bp : biggerPred biggerGen
    bp = PrincipalIdeal.genIsInIdeal (pid bigger)
    biggerPrincipal' : {x : A} → biggerGen ∣ x → biggerPred x
    biggerPrincipal' {y} bg|y = memberDividesImpliesMember bigger bp bg|y
    u : biggerGen ∣ r
    u = biggerPrincipal (biggerContains (1R , transitive *Commutative identIsIdent))
    biggerGenNonzero : biggerGen ∼ 0R → False
    biggerGenNonzero bg=0 = notInR (Ideal.isSubset (generatedIdeal r) (symmetric t) (Ideal.containsIdentity (generatedIdeal r)))
      where
        t : outsideR ∼ 0R
        t with biggerPrincipal {outsideR} biggerContainsOutside
        ... | mult , pr = transitive (symmetric pr) (transitive (*WellDefined bg=0 reflexive) (transitive *Commutative timesZero))
    v : (r ∣ biggerGen) → False
    v r|bg with mutualDivisionImpliesAssociate r|bg u (Irreducible.nonzero irred)
    v r|bg | assoc = notInR (associateImpliesGeneratedIdealsEqual' assoc (PrincipalIdeal.genGenerates (pid bigger) biggerContainsOutside))
    w : Unit biggerGen
    w = dividesIrreducibleImpliesUnit irred u v

primeIdealIsMaximal : {c : _} {pred : A → Set c} → {i : Ideal pred} → (nonzero : Sg A (λ a → ((a ∼ 0R) → False) && pred a)) → PrimeIdeal i → {d : _} → MaximalIdeal i {d}
primeIdealIsMaximal {pred = pred} {i} (m , (m!=0 ,, predM)) prime {d = d} = maximalIdealWellDefined (generatedIdeal (PrincipalIdeal.generator princ)) i (memberDividesImpliesMember i (PrincipalIdeal.genIsInIdeal princ)) (PrincipalIdeal.genGenerates princ) isMaximal
  where
    princ : PrincipalIdeal i
    princ = pid i
    isPrime : Prime (PrincipalIdeal.generator princ)
    isPrime = primeIdealImpliesPrime (λ gen=0 → PrimeIdeal.notContainedIsNotContained prime (exFalso (m!=0 (generatorZeroImpliesAllZero princ gen=0 predM)))) (primeIdealWellDefined i (generatedIdeal (PrincipalIdeal.generator princ)) (PrincipalIdeal.genGenerates princ) (memberDividesImpliesMember i (PrincipalIdeal.genIsInIdeal princ)) prime)
    isIrreducible : Irreducible (PrincipalIdeal.generator princ)
    isIrreducible = primeIsIrreducible isPrime
    isMaximal : MaximalIdeal (generatedIdeal (PrincipalIdeal.generator princ)) {d}
    isMaximal = irreducibleImpliesMaximalIdeal isIrreducible {d}

irreducibleImpliesPrime : {x : A} → Irreducible x → Prime x
irreducibleImpliesPrime {x} irred = primeIdealImpliesPrime (Irreducible.nonzero irred) (idealMaximalImpliesIdealPrime (generatedIdeal x) (irreducibleImpliesMaximalIdeal irred))


text:
module x02-842Induction where

-- Library

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

-- PLFA coverage of identity, associativity, commutativity, distributivity.

-- An example of the associative law for addition.

_ : (3 + 4) + 5 ≡ 3 + (4 + 5)
_ =
  begin
    (3 + 4) + 5
  ≡⟨⟩
    7 + 5
  ≡⟨⟩
    12
  ≡⟨⟩
    3 + 9
  ≡⟨⟩
    3 + (4 + 5)
  ∎

-- A theorem easy to prove.

+-identityᴸ : ∀ (m : ℕ) → zero + m ≡ m
+-identityᴸ m = {!!}

-- A first nontrivial theorem.
-- An equational proof is shown in PLFA.
-- It uses helpers cong and sym imported from the standard library,
-- and a form of equational reasoning that allows more elaborate justification.
-- Instead we will use 'rewrite'.

+-identityʳ : ∀ (m : ℕ) → m + zero ≡ m
+-identityʳ m = {!!}

-- Associativity of addition.
-- (Done first in PLFA.)

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc m n p = {!!}

-- A useful lemma about addition.
-- Equational proof shown in PLFA.

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc m n = {!!}

-- Commutativity of addition.
-- Equational proof shown in PLFA.

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m n = {!!}

-- 842 exercise: AddSwap (1 point)
-- Please do this without using induction/recursion.

+-swap : ∀ (m n p : ℕ) → (m + n) + p ≡ n + (m + p)
+-swap m n p = {!!}

-- 842 exercise: AddDistMult (2 points)
-- Show that addition distributes over multiplication.

*-+-rdistrib : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-+-rdistrib m n p = {!!}

-- 842 exercise: MultAssoc (2 points)
-- Show that multiplication is associative.

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc m n p = {!!}

-- 842 exercise: MultComm (3 points)
-- Show that multiplication is commutative.
-- As with the addition proof above, helper lemmas will be needed.

*-comm : ∀ (m n : ℕ) → m * n ≡ n * m
*-comm m n = {!!}

-- 842 exercise: LeftMonusZero (1 point)
-- PLFA asks "Did your proof require induction?"
-- (which should give you an indication of the expected answer).

0∸n≡0 : ∀ (m : ℕ) → zero ∸ m ≡ zero
0∸n≡0 m = {!!}

-- 842 exercise: MonusAssocish (2 points)
-- Show a form of associativity for monus.

∸-+-assoc : ∀ (m n p : ℕ) → m ∸ n ∸ p ≡ m ∸ (n + p)
∸-+-assoc m n p = {!!}

-- 842 extended exercise: properties of binary representation.
-- This is based on the PLFA Bin-laws exercise.

-- Copied from 842Naturals.

data Bin-ℕ : Set where
  bits : Bin-ℕ
  _x0 : Bin-ℕ → Bin-ℕ
  _x1 : Bin-ℕ → Bin-ℕ

dbl : ℕ → ℕ
dbl zero = zero
dbl (suc n) = suc (suc (dbl n))

-- Copy your versions of 'inc', 'to', 'from', 'bin-+' over from 842Naturals.
-- You may choose to change them here to make proofs easier.
-- But make sure to test them if you do!

inc : Bin-ℕ → Bin-ℕ
inc m = {!!}

tob : ℕ → Bin-ℕ
tob m = {!!}

fromb : Bin-ℕ → ℕ
fromb m = {!!}

_bin-+_ : Bin-ℕ → Bin-ℕ → Bin-ℕ
m bin-+ n = {!!}

-- 842 exercise: DoubleB (1 point)
-- Write the Bin-ℕ version of dbl, here called dblb.
-- As with the other Bin-ℕ operations, don't use tob/fromb.

dblb : Bin-ℕ → Bin-ℕ
dblb m = {!!}

-- Here are some properties of tob/fromb/inc suggested by PLFA Induction.
-- Please complete the proofs.

-- 842 exercise: FromInc (1 point)

from∘inc : ∀ (m : Bin-ℕ) → fromb (inc m) ≡ suc (fromb m)
from∘inc m = {!!}

-- 842 exercise: FromToB (1 point)

from∘tob : ∀ (m : ℕ) → fromb (tob m) ≡ m
from∘tob m = {!!}

-- 842 exercise: ToFromB (2 points)
-- The property ∀ (m : Bin-ℕ) → tob (fromb m) ≡ m cannot be proved.
-- Can you see why?
-- However, this restriction of it can be proved.

to/from-corr : ∀ (m : Bin-ℕ) (n : ℕ) → m ≡ tob n → fromb m ≡ n
to/from-corr m n m≡tn = {!!}

-- Here are a few more properties for you to prove.

-- 842 exercise: DblBInc (1 point)

dblb∘inc : ∀ (m : Bin-ℕ) → dblb (inc m) ≡ inc (inc (dblb m))
dblb∘inc m = {!!}

-- 842 exercise: ToDbl (1 point)

to∘dbl : ∀ (m : ℕ) → tob (dbl m) ≡ dblb (tob m)
to∘dbl m = {!!}

-- 842 exercise: FromDblB (1 point)

from∘dblb : ∀ (m : Bin-ℕ) → fromb (dblb m) ≡ dbl (fromb m)
from∘dblb m = {!!}

-- 842 exercise: BinPlusLInc (2 points)
-- This helper function translates the second case for unary addition
--  suc m + n = suc (m + n)
-- into the binary setting. It's useful in the next proof.
-- Hint: induction on both m and n is needed.

bin-+-linc : ∀ (m n : Bin-ℕ) → (inc m) bin-+ n ≡ inc (m bin-+ n)
bin-+-linc m n = {!!}

-- 842 exercise: PlusUnaryBinary (2 points)
-- This theorem relates unary and binary addition.

to∘+ : ∀ (m n : ℕ) → tob (m + n) ≡ tob m bin-+ tob n
to∘+ m n = {!!}

-- This ends the extended exercise.

-- The following theorems proved in PLFA can be found in the standard library.

-- import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm)

-- Unicode used in this chapter:

{-

    ∀  U+2200  FOR ALL (\forall, \all)
    ʳ  U+02B3  MODIFIER LETTER SMALL R (\^r)
    ′  U+2032  PRIME (\')
    ″  U+2033  DOUBLE PRIME (\')
    ‴  U+2034  TRIPLE PRIME (\')
    ⁗  U+2057  QUADRUPLE PRIME (\')

-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
{-# OPTIONS --cubical #-}
module _ where
open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

data Interval : Set where
  left right : Interval
  sq      : left ≡ right

-- Agda should not loop when typechecking the following definition.
--
-- Termination checking should catch that `id left` is not
-- normalizing, given our definition of reduction.
--
-- Hence conversion checking shouldn't reduce applications of `id`.
id : Interval → Interval
id (sq i) = sq i
id left = id (sq i0)
id right = id (sq i1)


text:
import cedille-options
open import general-util

module process-cmd
  (options : cedille-options.options)
  {mF : Set → Set}
  {{mFm : monad mF}}
  (progress-update : string → mF ⊤)
  (write-to-log : string → mF ⊤) where

--open import cedille-find
open import cedille-types
open import classify options {mF} ⦃ mFm ⦄ write-to-log
open import constants
open import conversion
open import ctxt
open import free-vars
open import rename
open import spans options { mF } ⦃ mFm ⦄
open import subst
open import syntax-util
open import type-util
open import toplevel-state options { mF } ⦃ mFm ⦄
open import to-string options

open import datatype-util
open import rewriting
open import elab-util options
import cws-types
import cws

-- generate spans from the given comments-and-whitespace syntax tree
process-cwst-etys : cws-types.entities → spanM ⊤
process-cwst-ety : cws-types.entity → spanM ⊤
process-cwst-etys (cws-types.Entity ety etys) = process-cwst-ety ety >> process-cwst-etys etys
process-cwst-etys cws-types.EndEntity = return triv
process-cwst-ety cws-types.EntityNonws = return triv
process-cwst-ety (cws-types.EntityWs pi pi') = return triv
process-cwst-ety (cws-types.EntityComment pi pi') = [- comment-span pi pi' -] return triv

process-cwst : toplevel-state → filepath → spanM toplevel-state
process-cwst s filename with include-elt.cwst (get-include-elt s filename)
process-cwst s filename | nothing = return s
process-cwst s filename | just (cws-types.File etys) = process-cwst-etys etys >> return s

check-and-add-params : ctxt → posinfo → ex-params → spanM (ctxt × params)
check-and-add-params Γ pi' (p@(ExParam pi1 me pi1' x atk pi2) :: ps') =
  Γ ⊢ atk ↝ atk~ /
  let Γ' = Γ , pi1' - x :` atk~
      qx = pi1' % x in
  [- punctuation-span "Parens (parameter)" pi1 pi2 -]
  [- Decl-span Γ' decl-param pi1 pi1' x atk~ me pi2 pi' -]
  [- var-span me Γ' pi1' x checking atk~ nothing -]
  check-and-add-params Γ' pi' ps' >>=c λ Γ'' ps~ →
  return2 Γ'' (Param me qx atk~ :: ps~)
check-and-add-params Γ pi' [] = return2 Γ []

optAs-posinfo-var : ctxt → maybe import-as → posinfo × var → spanM (posinfo × var)
optAs-posinfo-var Γ nothing = return
optAs-posinfo-var Γ (just (ImportAs pi x)) orig =
  [- Import-module-span Γ orig [] [ not-for-navigation ] nothing -]
  return2 pi x

{-# TERMINATING #-}
{- notice that these are elaborating functions: they take an ex-QQQ and return a QQQ (along with other activity) -}
process-cmd : toplevel-state → ex-cmd → spanM (toplevel-state × cmd)
process-cmds : toplevel-state → ex-cmds → spanM (toplevel-state × cmds)
process-ctrs : (uqv lqv mqv : var) → params → posinfo → toplevel-state → ex-ctrs → spanM ((ctxt → ctxt) × ctrs)
process-params : toplevel-state → posinfo → ex-params → spanM (toplevel-state × params)
process-start : toplevel-state → filepath → (progress-name : string) → ex-file → spanM (toplevel-state × file)
process-file : toplevel-state → filepath → (progress-name : string) → mF (toplevel-state × file × string × string × params × qualif)

maybe-add-opaque-span : optopaque → (end : posinfo) → spanM ⊤
maybe-add-opaque-span nothing pi = return triv
maybe-add-opaque-span (just piₒ) pi =
  spanM-add $ Opaque-span piₒ pi

process-cmd s (ExCmdDef op (ExDefTerm pi x (just tp) t) pi') =
  let Γ = toplevel-state.Γ s in
  Γ ⊢ tp ⇐ KdStar ↝ tp' /
  Γ ⊢ t ⇐ tp' ↝ t' /
  check-erased-margs Γ (term-start-pos t) (term-end-pos t) t' (just tp') >>
  let Γ' = ctxt-term-def pi globalScope (isNothing op) x (just t') tp' Γ in
  maybe-add-opaque-span op pi' >>
  [- DefTerm-span Γ' pi x checking (just tp') t' pi' [] -]
  check-redefined pi x s
    (CmdDefTerm x t')
    ([- uncurry (Var-span Γ' pi x checking) (compileFail-in Γ t') -]
     return (record s { Γ = Γ' }))

process-cmd s (ExCmdDef op (ExDefTerm pi x nothing t) pi') =
  let Γ = toplevel-state.Γ s in
  Γ ⊢ t ↝ t~ ⇒ T~ /
  check-erased-margs Γ (term-start-pos t) (term-end-pos t) t~ nothing >>
  let Γ' = ctxt-term-def pi globalScope (isNothing op) x (just t~) T~ Γ in
  maybe-add-opaque-span op pi' >>
  [- DefTerm-span Γ' pi x synthesizing (just T~) t~ pi' [] -]
  check-redefined pi x s
    (CmdDefTerm x t~)
    ([- uncurry (Var-span Γ' pi x synthesizing) (compileFail-in Γ t~) -]
     return (record s { Γ = Γ' }))

process-cmd s (ExCmdDef op (ExDefType pi x k tp) pi') =
  let Γ = toplevel-state.Γ s in
  Γ ⊢ k ↝ k~ /
  Γ ⊢ tp ⇐ k~ ↝ tp~ /
  let Γ' = ctxt-type-def pi globalScope (isNothing op) x (just tp~) k~ Γ in
  maybe-add-opaque-span op pi' >>
  spanM-add (DefType-span Γ' pi x checking (just k~) tp~ pi' []) >>
  check-redefined pi x s
    (CmdDefType x k~ tp~)
    ([- TpVar-span Γ' pi x checking [] nothing -]
     return (record s { Γ = Γ' }))

process-cmd s (ExCmdKind pi x ps k pi') =
  let Γ = toplevel-state.Γ s in
  check-and-add-params Γ pi' ps >>=c λ Γₚₛ ps~ →
  Γₚₛ ⊢ k ↝ k~ /
  let Γ' = ctxt-kind-def pi x ps~ k~ Γ in
  [- DefKind-span Γ' pi x k~ pi' -]
  check-redefined pi x s (CmdDefKind x ps~ k~)
    ([- KdVar-span Γ' (pi , x) (posinfo-plus-str pi x) ps~ checking [] nothing -]
     return (record s { Γ = Γ' }))

process-cmd s (ExCmdData (DefDatatype pi pi' x ps k cs) pi'') =
  let Γ = toplevel-state.Γ s
      old-Γ = Γ in
  [- DefDatatype-header-span pi -]
  check-and-add-params Γ pi'' ps >>=c λ Γₚₛ ps' →
  Γₚₛ ⊢ k ↝ k' /
  let mn = ctxt.mn Γ
      qx = mn # x
      mps = ctxt.ps Γ ++ ps'
      Γ-decl = λ Γ → ctxt-type-decl pi' x k' $ data-highlight Γ (pi' % x)
      cmd-fail = CmdDefType x (params-to-kind ps' k') (TpHole pi')
      fail = λ e → [- TpVar-span Γ pi' x checking [] (just e) -] return2 s cmd-fail in
  process-ctrs x (pi' % x) qx mps pi' (record s {Γ = Γ-decl Γₚₛ}) cs >>=c λ Γ-cs cs~ →
  maybe-else' (cedille-options.options.datatype-encoding options >>=c λ fp f → f)
    (fail "Missing directive for datatype encoding.  Please add a datatype-encoding directive to your .cedille/options file. See cedille/.cedille/options for the current location") λ de →
  let is = kind-to-indices Γₚₛ k'
      kᵢ = indices-to-kind is $ KdAbs ignored-var
             (Tkt $ indices-to-tpapps is $ params-to-tpapps mps $ TpVar qx) KdStar in
  either-else' (init-encoding Γₚₛ de (Data x ps' is cs~)) fail λ ecs →
  check-redefined pi' x (record s {Γ = Γ-cs Γ}) (CmdDefData ecs x ps' k' cs~)
  let fₓ = fresh-var (add-indices-to-ctxt is Γ) "X"
      cs~ = map-fst (mn #_) <$> cs~
      Γ' = Γ-cs Γ
      kₘᵤ = abs-expand-kind ps' $ KdAbs ignored-var (Tkk k') KdStar
      Γ' = ctxt-type-def pi' globalScope opacity-open (data-Is/ x) nothing kₘᵤ Γ'
      Tₘᵤ = params-to-alls ps' $ TpApp (params-to-tpapps mps (TpVar (mn # data-Is/ x))) (Ttp (params-to-tpapps mps $ TpVar qx))
      Γ' = ctxt-term-def pi' globalScope opacity-open (data-is/ x) nothing Tₘᵤ Γ'
      Tₜₒ =
        abs-expand-type ps' $
        mall fₓ (Tkk $ indices-to-kind is KdStar) $
        TpAbs Erased ignored-var (Tkt (TpApp (params-to-tpapps mps $ TpVar $ mn # data-Is/ x) $ Ttp $ TpVar fₓ)) $
        indices-to-alls is $
        TpAbs NotErased ignored-var (Tkt (indices-to-tpapps is $ TpVar fₓ)) $
        indices-to-tpapps is $ params-to-tpapps mps $ TpVar qx
      Γ' = ctxt-term-def pi' globalScope opacity-open (data-to/ x) (just id-term) Tₜₒ Γ'
      Γ' = ctxt-datatype-def pi' x ps' kᵢ k' cs~ ecs Γ' in
  [- DefDatatype-span Γ' pi pi' x ps' (abs-expand-kind ps' k') kₘᵤ k' Tₘᵤ Tₜₒ cs~ k pi'' -]
  [- TpVar-span Γ' pi' x checking (kind-data old-Γ k' :: params-data old-Γ ps') nothing -]
  return (record s {Γ = Γ'})

-- TODO ignore checking but still gen spans if need-to-check false?
process-cmd s (ExCmdImport (ExImport pi op pi' x oa as pi'')) =
  let fnₒ = ctxt.fn (toplevel-state.Γ s)
      ie = get-include-elt s fnₒ
      oa' = maybe-map (λ {(ImportAs pi x) → x}) oa in
  case trie-lookup (include-elt.import-to-dep ie) x of λ where
    nothing → [- Import-span pi "missing" pi'' [] (just ("File not found: " ^ x)) -]
              return2 (set-include-elt s fnₒ (record ie {err = tt}))
                      (CmdImport (Import op x x oa' []))
    (just fnᵢ) →
      spanM-push (process-file s fnᵢ x) >>= uncurry₂ λ s f _ →
        process-import (toplevel-state.Γ s) op oa fnₒ fnᵢ
          (lookup-mod-params (toplevel-state.Γ s) fnᵢ)
          (maybe-else' (lookup-mod-params (toplevel-state.Γ s) fnₒ) [] id) >>=c λ e as~ →
         let s-e = scope-file s fnₒ fnᵢ oa' as~
             Γ = toplevel-state.Γ s in
         [- Import-span pi fnᵢ pi'' [] (snd s-e ||-maybe e) -]
         return2 (fst s-e) (CmdImport (Import op fnᵢ x oa' as~))
  where
  -- When importing a file publicly, you may use any number of arguments as long as the
  -- parameters of the current module are not free in them.
  -- You may then use any number of single-variable parameters from the current module
  -- as arguments as long as they retain the same order as before and have no non-parameter
  -- arguments between them
  -- (so parameters A, B, C, ..., Z can be used as arguments ·C ·X, but not ·X ·C)
  public-import-params-ok : params → args → err-m
  public-import-params-ok ps = h nothing where
    err = just "You can only use parameters for arguments to public imports if the are in order at the end"
    params-order : params → trie ℕ
    params-order = h 0 where
      h : ℕ → params → trie ℕ
      h n [] = empty-trie
      h n (Param me x atk :: ps) = trie-insert (h (suc n) ps) x n
    pso = params-order ps
    ps-free : arg → err-m → err-m
    ps-free a e = if ~ are-free-in-h pso (free-vars-arg a) then e else err
    h : maybe ℕ → args → err-m
    h c (a :: as) =
      maybe-else' (arg-var a >>= trie-lookup pso)
        (maybe-else' c (ps-free a $ h nothing as) λ _ → err) λ aₙ →
      maybe-else' c (h (just aₙ) as) λ cₙ →
      if cₙ ≥ aₙ then err else h (just aₙ) as
    h n [] = nothing

  process-import : ctxt → opt-public → maybe import-as → (cur imp : filepath) → maybe params → params → spanM (err-m × args)
  process-import Γ op oa fnₒ fnᵢ nothing _ = return2 (just "Undefined module import (this probably shouldn't happen?)") []
  process-import Γ Public (just _) fnₒ fnᵢ (just psᵢ) psₒ = return2 (just "Public imports aren't allowed to be qualified") []
  process-import Γ op oa fnₒ fnᵢ (just psᵢ) psₒ =
    optAs-posinfo-var Γ oa (pi' , x) >>= λ pi-v →
    check-args Γ as psᵢ >>= λ as~ →
    [- Import-module-span Γ (pi' , x) psᵢ [ location-data (fnᵢ , "1") ] nothing -]
    return2 (ifMaybe op $ public-import-params-ok psₒ as~) as~

process-cmds s (c :: cs) =
  process-cmd s c >>=c λ s c →
  process-cmds s cs >>=c λ s cs →
  return2 s (c :: cs)
process-cmds s [] = return2 s []

process-ctrs uX lX mX ps piₓ s csₒ c? = h s csₒ c? where
  h : toplevel-state → ex-ctrs → spanM ((ctxt → ctxt) × ctrs)
  h s [] = return2 id []
  h s (ExCtr pi x T :: cs) =
    let Γ = toplevel-state.Γ s in
    Γ ⊢ T ⇐ KdStar ↝ T~ /
    let T = hnf-ctr Γ lX T~
        𝕃tpkd-to-string = foldr (λ tk s → rope-to-string (tpkd-to-string Γ tk) ^ " ; " ^ s) ""
        neg-ret-err : maybe string
        neg-ret-err =
          let err-msg = λ s s' → just (uX ^ s ^ " type of the constructor: " ^ s') in
            case run-posM (positivity.ctr-positive lX Γ T) of
              λ where
                (ctorOk , l) → nothing
                (ctorNegative , l) → err-msg " occurs negatively in the"
                                       ("Searching types: " ^ 𝕃tpkd-to-string l)
                (ctorNotInReturnType , l) → err-msg " is not the return" "" in
    let T = [ Γ - TpVar mX / lX ] T
        Tₚₛ = [ Γ - params-to-tpapps ps (TpVar mX) / lX ] T~ in
    h s cs >>=c λ Γ-f cs →
    let Γ = toplevel-state.Γ s
        Γ-f' = ctxt-ctr-def pi x Tₚₛ ps (length csₒ) (length csₒ ∸ suc (length cs)) in
    check-redefined pi x s (Ctr x T :: cs)
      (let Γ = Γ-f' Γ in
         [- Var-span Γ pi x checking
             [ summary-data x (ctxt-type-def piₓ globalScope opacity-open uX nothing KdStar Γ)
                 (abs-expand-type ps T) ] neg-ret-err -]
       return (record s {Γ = Γ})) >>=c λ s →
    return2 (Γ-f ∘ Γ-f')

process-params s pi ps =
  let Γ = toplevel-state.Γ s in
  check-and-add-params Γ pi ps >>=c λ Γₚₛ ps →
  return2
    (record s {Γ = ctxt-add-current-params (record Γₚₛ { ps = ps })})
    ps

process-start s filename pn (ExModule is pi1 pi2 mn ps cs pi3) =
  spanM-push (progress-update pn) >>
  process-cmds s (map ExCmdImport is) >>=c λ s is' →
  process-params s (params-end-pos first-position ps) ps >>=c λ s ps →
  process-cmds s cs >>=c λ s cs →
  process-cwst s filename >>= λ s →
  let pi2' = posinfo-plus-str pi2 mn in
  [- File-span (toplevel-state.Γ s) first-position (posinfo-plus pi3 1) filename -]
  [- Module-span pi2 pi2' -]
  [- Module-header-span pi1 pi2' -]
  return2 s (Module mn ps (is' ++ cs))
--  where
--  unqual-cmd : ctxt → renamectxt → cmd → cmd
--  unqual-cmd Γ ρ (CmdDefTerm x t) = CmdDefTerm x (subst-renamectxt Γ ρ t)
--  unqual-cmd Γ ρ (CmdDefType x k T) = CmdDefType x (subst-renamectxt Γ ρ k) (subst-renamectxt Γ ρ T)
--  unqual-cmd Γ ρ (CmdDefKind x ps k) = CmdDefKind x (substh-params Γ ρ empty-trie ps) (subst-renamectxt (add-params-to-ctxt ps Γ) ρ k)
--  unqual-cmd Γ ρ (CmdDefData eds x ps k cs) = CmdDefData eds x (substh-params Γ ρ empty-trie ps) (subst-renamectxt (add-params-to-ctxt ps Γ) ρ k) (map-snd (subst-renamectxt (add-params-to-ctxt ps Γ) ρ) <$> cs)
--  unqual-cmd Γ ρ (CmdImport (Import op fnᵢ x oa as)) = CmdImport (Import op fnᵢ x oa (subst-renamectxt Γ ρ -arg_ <$> as))

{- process (type-check if necessary) the given file.
   We assume the given top-level state has a syntax tree associated with the file. -}
process-file s filename pn with get-include-elt s filename
process-file s filename pn | ie =
  proceed s (include-elt.ast ie) (include-elt.ast~ ie)
      (set-need-to-add-symbols-to-context-include-elt ie ff) >>= λ where
    (s , ie , ret-mod , f) → return ({-set-include-elt s filename ie-} s , f , ret-mod)
  where
  proceed : toplevel-state → maybe ex-file → maybe file → include-elt →
            mF (toplevel-state × include-elt × (string × string × params × qualif) × file)
  proceed s nothing f~ ie' =
    progress-update filename >>
--    write-to-log "should not happen" >>
    return (s , ie' , ctxt-get-current-mod (toplevel-state.Γ s) ,
             maybe-else' f~ (Module ignored-var [] []) id) {- should not happen -}
  proceed s (just x) f~ ie' with include-elt.need-to-add-symbols-to-context ie
  proceed s (just x) (just f~) ie' | ff =
    let Γ = toplevel-state.Γ s
        mod = ctxt.fn Γ , ctxt.mn Γ , ctxt.ps Γ , ctxt.qual Γ in
    return (s , ie' , mod , f~)
  proceed (mk-toplevel-state ip fns is Γ logFilePath) (just x) f~ ie' | _
    with include-elt.do-type-check ie | ctxt-get-current-mod Γ
  proceed (mk-toplevel-state ip fns is Γ logFilePath) (just x) f~ ie' | _ | do-check | prev-mod =
   let Γ = ctxt-initiate-file Γ filename (start-modname x) in
     process-start (mk-toplevel-state ip fns (trie-insert is filename ie') Γ logFilePath)
             filename pn x empty-spans >>= λ where
       ((mk-toplevel-state ip fns is Γ logFilePath , f) , ss) →
         let ret-mod = ctxt.fn Γ , ctxt.mn Γ , ctxt.ps Γ , ctxt.qual Γ
             ie'' = if do-check then set-spans-include-elt ie' ss f else record ie' { ast~ = include-elt.ast~ ie' ||-maybe just f } in
         progress-update pn >> return
           (mk-toplevel-state ip (if do-check then (filename :: fns) else fns) (trie-insert is filename ie'')
             (ctxt-set-current-mod Γ prev-mod) logFilePath ,
            ie'' ,
            ret-mod ,
            f)
--  proceed s (just x) f~ ie' | ff =
--    return (s , ie' , ctxt-get-current-mod (toplevel-state.Γ s) ,
--             maybe-else' f~ (Module ignored-var [] []) id)


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax Naturals | Nat

type
  N : 0-ary

term
  ze   : N
  su   : N  ->  N
  nrec : N  α  (α,N).α  ->  α

theory
  (zeβ) z : α   s : (α,N).α        |> nrec (ze,       z, r m. s[r,m]) = z
  (suβ) z : α   s : (α,N).α  n : N |> nrec (su (n), z, r m. s[r,m]) = s[nrec (n, z, r m. s[r,m]), n]
-}

module Naturals.Signature where

open import SOAS.Context

-- Type declaration
data NatT : Set where
  N : NatT

open import SOAS.Syntax.Signature NatT public
open import SOAS.Syntax.Build NatT public

-- Operator symbols
data Natₒ : Set where
  zeₒ suₒ : Natₒ
  nrecₒ : {α : NatT} → Natₒ

-- Term signature
Nat:Sig : Signature Natₒ
Nat:Sig = sig λ
  {  zeₒ        → ⟼₀ N
  ;  suₒ        → (⊢₀ N) ⟼₁ N
  ; (nrecₒ {α}) → (⊢₀ N) , (⊢₀ α) , (α , N ⊢₂ α) ⟼₃ α
  }

open Signature Nat:Sig public

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-# OPTIONS --instance-search-depth=10 #-}
data ⊥ : Set where

it : {A : Set} {{_ : A}} → A
it {{x}} = x

postulate Eq : Set → Set

instance
  postulate weaken : Eq ⊥ → Eq _

loop : Eq ⊥
loop = it

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --universe-polymorphism #-}

module Issue228 where

postulate
  Level : Set
  zero : Level
  suc  : Level → Level
  ∞    : Level
  _⊔_  : Level → Level → Level

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

infixl 6 _⊔_

data _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  _,_ : A → B → A × B

data Large : Set ∞ where
  large : Large

data Small : Set₁ where
  small : Set → Small

P : Set
P = Large × Small

[_] : Set → P
[ A ] = (large , small A)

potentially-bad : P
potentially-bad = [ P ]

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- {-# OPTIONS -v tc.polarity:10 -v tc.conv.elim:25 #-}

module Issue755 where

open import Common.Prelude renaming (Nat to ℕ)
open import Common.Equality

abstract
  foo : Bool → ℕ → ℕ
  foo true  x = 0
  foo false x = 0

  -- should work
  works : ∀{b} → foo b 0 ≡ foo b 1 → foo b 0 ≡ foo b 1
  works refl = refl

-- should fail
test : ∀{b} → foo b 0 ≡ foo b 1 → foo b 0 ≡ foo b 1
test refl = refl
-- 0 != 1 of type ℕ
-- when checking that the pattern refl has type foo 0 ≡ foo 1

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.CohomologyRings.Coproduct where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_ ; snotz to nsnotz)
open import Cubical.Data.Sigma
open import Cubical.Data.Sum

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.DirProd
open import Cubical.Algebra.AbGroup
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.DirectProd
open import Cubical.Algebra.DirectSum.DirectSumHIT.Base

open import Cubical.HITs.SetTruncation as ST

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Groups.Coproduct
open import Cubical.ZCohomology.RingStructure.CupProduct
open import Cubical.ZCohomology.RingStructure.CohomologyRing

private variable
  ℓ ℓ' : Level

module Equiv-Coproduct-Properties
  {X : Type ℓ}
  {Y : Type ℓ'}
  where

  open Iso
  open IsGroupHom
  open GroupStr
  open PlusBis

  open RingStr (snd (H*R X)) using ()
    renaming
    ( 0r        to 0H*X
    ; 1r        to 1H*X
    ; _+_       to _+H*X_
    ; -_        to -H*X_
    ; _·_       to _cupX_
    ; +Assoc    to +H*XAssoc
    ; +IdL      to +H*XIdL
    ; +IdR      to +H*XIdR
    ; +Comm     to +H*XComm
    ; ·Assoc    to ·H*XAssoc
    ; ·IdL      to ·H*XIdL
    ; ·IdR      to ·H*XIdR
    ; is-set    to isSetH*X     )

  open RingStr (snd (H*R Y)) using ()
    renaming
    ( 0r        to 0H*Y
    ; 1r        to 1H*Y
    ; _+_       to _+H*Y_
    ; -_        to -H*Y_
    ; _·_       to _cupY_
    ; +Assoc    to +H*YAssoc
    ; +IdL      to +H*YIdL
    ; +IdR      to +H*YIdR
    ; +Comm     to +H*YComm
    ; ·Assoc    to ·H*YAssoc
    ; ·IdL      to ·H*YIdL
    ; ·IdR      to ·H*YIdR
    ; is-set    to isSetH*Y     )

  -- warning this does not open H*(X×Y) !
  -- This just a notation shorter and pratical
  open RingStr (snd (DirectProd-Ring (H*R X) (H*R Y))) using ()
    renaming
    ( 0r        to 0H*X×Y
    ; 1r        to 1H*X×Y
    ; _+_       to _+H*X×Y_
    ; -_        to -H*X×Y_
    ; _·_       to _cupX×Y_
    ; +Assoc    to +H*X×YAssoc
    ; +IdL      to +H*X×YIdL
    ; +IdR      to +H*X×YIdR
    ; +Comm     to +H*X×YComm
    ; ·Assoc    to ·H*X×YAssoc
    ; ·IdL      to ·H*X×YIdL
    ; ·IdR      to ·H*X×YIdR
    ; is-set    to isSetH*X×Y     )

  open RingStr (snd (H*R (X ⊎ Y))) using ()
    renaming
    ( 0r        to 0H*X⊎Y
    ; 1r        to 1H*X⊎Y
    ; _+_       to _+H*X⊎Y_
    ; -_        to -H*X⊎Y_
    ; _·_       to _cupX⊎Y_
    ; +Assoc    to +H*X⊎YAssoc
    ; +IdL      to +H*X⊎YIdL
    ; +IdR      to +H*X⊎YIdR
    ; +Comm     to +H*X⊎YComm
    ; ·Assoc    to ·H*X⊎YAssoc
    ; ·IdL      to ·H*X⊎YIdL
    ; ·IdR      to ·H*X⊎YIdR
    ; is-set    to isSetH*X⊎Y     )

-----------------------------------------------------------------------------
-- Notation needed for type checking
-- indeed several base coexists and two cannot be inferef without implicit argument
-- it is clearer to add a notation

  baseX : (n : ℕ) → (x : coHom n X) → H* X
  baseX n x = base n x

  baseY : (n : ℕ) → (x : coHom n Y) → H* Y
  baseY n x = base n x

-----------------------------------------------------------------------------
-- Direct Sens

  H*-X⊎Y→H*-X×H*-Y : H* (X ⊎ Y) → (H* X) × (H* Y)
  H*-X⊎Y→H*-X×H*-Y =
    DS-Rec-Set.f _ _ _ _
    isSetH*X×Y
    (0H*X , 0H*Y)
    (λ n a → (base n (fst (fun (fst Equiv-Coproduct-CoHom) a))) , (base n (snd (fun (fst Equiv-Coproduct-CoHom) a))))
    _+H*X×Y_
    +H*X×YAssoc
    +H*X×YIdR
    +H*X×YComm
    (λ n → ≡-× ((cong (λ A → baseX n (fst A)) (pres1 (snd Equiv-Coproduct-CoHom))) ∙ base-neutral n)
               (((cong (λ B → baseY n (snd B)) (pres1 (snd Equiv-Coproduct-CoHom))) ∙ base-neutral n)))
    λ n a b → sym (≡-× (cong (λ A → baseX n (fst A)) (pres· (snd Equiv-Coproduct-CoHom) a b)
                        ∙ cong (base n) (helper1 _ _ _)
                        ∙ sym (base-add n _ _))
                   (cong (λ B → baseY n (snd B)) (pres· (snd Equiv-Coproduct-CoHom) a b)
                        ∙ cong (base n) (helper2 _ _ _)
                        ∙ sym (base-add n _ _)))
      where
      helper1 : (n : ℕ) → (x y : coHom n X × coHom n Y)
                → fst ((DirProd (coHomGr n X) (coHomGr n Y) .snd GroupStr.· x) y) ≡ ((fst x) +ₕ (fst y))
      helper1 n (fst₁ , snd₁) (fst₂ , snd₂) = refl

      helper2 : (n : ℕ) → (x y : coHom n X × coHom n Y)
                → snd ((DirProd (coHomGr n X) (coHomGr n Y) .snd GroupStr.· x) y) ≡ ((snd x) +ₕ (snd y))
      helper2 n (fst₁ , snd₁) (fst₂ , snd₂) = refl

-----------------------------------------------------------------------------
-- Converse Sens

-- One need to convert seperatly the X an Y
-- Otherwise the traduction fails in the case base n a , 0
-- because one need then to lift x + 0 ≡ 0
-- which doesn't work because the + being lifted is on H*(Y) and not H*(X)×H*(Y)

  H*-X→H*-X⊎Y : H*(X) → H*(X ⊎ Y)
  H*-X→H*-X⊎Y = DS-Rec-Set.f _ _ _ _ isSetH*X⊎Y
       0H*X⊎Y
       (λ n a → base n (inv (fst Equiv-Coproduct-CoHom) (a , (0ₕ n))))
       _+H*X⊎Y_
       +H*X⊎YAssoc
       +H*X⊎YIdR
       +H*X⊎YComm
       (λ n → cong (base n) (pres1 (snd (invGroupIso Equiv-Coproduct-CoHom))) ∙ base-neutral n)
       λ n a a' → base-add _ _ _
                   ∙ cong (base n) (sym (pres· (snd (invGroupIso Equiv-Coproduct-CoHom)) _ _))
                   ∙ cong (base n) (cong (inv (fst Equiv-Coproduct-CoHom))
                                         (≡-× refl (AbGroupStr.+IdL (snd (coHomGroup n Y)) (0ₕ n))))

  H*-Y→H*-X⊎Y : H*(Y) → H*(X ⊎ Y)
  H*-Y→H*-X⊎Y = DS-Rec-Set.f _ _ _ _ isSetH*X⊎Y
       0H*X⊎Y
       (λ m b → base m (inv (fst Equiv-Coproduct-CoHom) (0ₕ m , b)))
       _+H*X⊎Y_
       +H*X⊎YAssoc
       +H*X⊎YIdR
       +H*X⊎YComm
       (λ m → cong (base m) (pres1 (snd (invGroupIso Equiv-Coproduct-CoHom))) ∙ base-neutral m)
       λ m b b' → base-add _ _ _
                   ∙ cong (base m) (sym (pres· (snd (invGroupIso Equiv-Coproduct-CoHom)) (0ₕ m , b) (0ₕ m , b')))
                   ∙ cong (base m) (cong (inv (fst Equiv-Coproduct-CoHom)) (≡-× (AbGroupStr.+IdL (snd (coHomGroup m X)) (0ₕ m)) refl))

  H*-X×H*-Y→H*-X⊎Y : H*(X) × H*(Y) → H*(X ⊎ Y)
  H*-X×H*-Y→H*-X⊎Y (x , y) = (H*-X→H*-X⊎Y x) +H*X⊎Y (H*-Y→H*-X⊎Y y)

  H*-X×H*-Y→H*-X⊎Y-pres+ : (x y : H*(X) × H*(Y)) → H*-X×H*-Y→H*-X⊎Y (x +H*X×Y y) ≡ ((H*-X×H*-Y→H*-X⊎Y x) +H*X⊎Y (H*-X×H*-Y→H*-X⊎Y y))
  H*-X×H*-Y→H*-X⊎Y-pres+ (x , y) (x' , y') = RingTheory.+ShufflePairs (H*R (X ⊎ Y)) _ _ _ _

-----------------------------------------------------------------------------
-- Section Sens

  e-sectX : (x : H* X) → H*-X⊎Y→H*-X×H*-Y (H*-X→H*-X⊎Y x) ≡ (x , 0H*Y)
  e-sectX = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*X×Y _ _)
            refl
            (λ n a → ≡-× (cong (base n) (cong fst (rightInv (fst Equiv-Coproduct-CoHom) (a , 0ₕ n))))
                          (cong (base n) (cong snd (rightInv (fst Equiv-Coproduct-CoHom) (a , 0ₕ n))))
                     ∙ ≡-× refl (base-neutral n))
            λ {U V} ind-U ind-V → cong₂ _+H*X×Y_ ind-U ind-V ∙ ≡-× refl (+H*YIdR _)

  e-sectY : (y : H* Y) → (H*-X⊎Y→H*-X×H*-Y (H*-Y→H*-X⊎Y y)) ≡ (0H*X , y)
  e-sectY = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*X×Y _ _)
            refl
            (λ m b → ≡-× (cong (base m) (cong fst (rightInv (fst Equiv-Coproduct-CoHom) (0ₕ m , b))))
                          (cong (base m) (cong snd (rightInv (fst Equiv-Coproduct-CoHom) (0ₕ m , b))))
                     ∙ ≡-× (base-neutral m) refl)
            λ {U V} ind-U ind-V → cong₂ _+H*X×Y_ ind-U ind-V ∙ ≡-× (+H*XIdR _) refl

  e-sect : (z : H*(X) × H*(Y)) → H*-X⊎Y→H*-X×H*-Y (H*-X×H*-Y→H*-X⊎Y z) ≡ z
  e-sect (x , y) = cong₂ _+H*X×Y_ (e-sectX x) (e-sectY y) ∙ ≡-× (+H*XIdR x) (+H*YIdL y)

-----------------------------------------------------------------------------
-- Retraction Sens

  e-retr : (x : H*(X ⊎ Y)) → H*-X×H*-Y→H*-X⊎Y (H*-X⊎Y→H*-X×H*-Y x) ≡ x
  e-retr = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*X⊎Y _ _)
           (+H*X⊎YIdR _)
           (λ n a → ((base n (T⁻ ((fst (T a)) , 0ₕ n))) +H*X⊎Y (base n (T⁻ (0ₕ n , snd (T a)))))
                           ≡⟨ base-add n _ _ ⟩
                     base n ((T⁻ ((fst (T a)) , 0ₕ n)) +ₕ (T⁻ (0ₕ n , snd (T a))))
                           ≡⟨ cong (base n) (sym (pres· (snd (invGroupIso Equiv-Coproduct-CoHom)) ((fst (T a)) , 0ₕ n) (0ₕ n , snd (T a)))) ⟩
                     base n (T⁻ ( fst (T a) +ₕ 0ₕ n , 0ₕ n +ₕ snd (T a)))
                           ≡⟨ cong (base n) (cong T⁻ (≡-× (rUnitₕ n (fst (T a))) (lUnitₕ n (snd (T a))))) ⟩
                     base n (T⁻ ( fst (T a) , snd (T a)))
                           ≡⟨ cong (base n) (cong T⁻ (helper1 _ _ (T a))) ⟩
                     base n (T⁻ (T a))
                           ≡⟨ cong (base n) (leftInv (fst Equiv-Coproduct-CoHom) a) ⟩
                     base n a ∎)
           λ {U V} ind-U ind-V → (H*-X×H*-Y→H*-X⊎Y-pres+ _ _) ∙ (cong₂ _+H*X⊎Y_ ind-U ind-V)

           where
           T : {n : ℕ} → coHom n (X ⊎ Y) → coHom n X × coHom n Y
           T {n} = fun (fst (Equiv-Coproduct-CoHom))

           T⁻ : {n : ℕ} → coHom n X × coHom n Y → coHom n (X ⊎ Y)
           T⁻ {n} = inv (fst (Equiv-Coproduct-CoHom))

           helper1 : (A : Type ℓ) → (B : Type ℓ') → (x : A × B) → (fst x , snd x) ≡ x
           helper1 A B (fst₁ , snd₁) = refl

-----------------------------------------------------------------------------
-- Ring Equiv-Coproduct-CoHomphism

  H*-X⊎Y→H*-X×H*-Y-pres1 : H*-X⊎Y→H*-X×H*-Y 1H*X⊎Y ≡ (1H*X , 1H*Y)
  H*-X⊎Y→H*-X×H*-Y-pres1 = refl

  H*-X⊎Y→H*-X×H*-Y-pres+ : (x y : H* (X ⊎ Y)) →
                              H*-X⊎Y→H*-X×H*-Y ( x +H*X⊎Y y)
                            ≡ H*-X⊎Y→H*-X×H*-Y x +H*X×Y H*-X⊎Y→H*-X×H*-Y y
  H*-X⊎Y→H*-X×H*-Y-pres+ x y = refl

  H*-X⊎Y→H*-X×H*-Y-pres· : (x y : H* (X ⊎ Y)) →
                              H*-X⊎Y→H*-X×H*-Y ( x cupX⊎Y y)
                            ≡ H*-X⊎Y→H*-X×H*-Y x cupX×Y H*-X⊎Y→H*-X×H*-Y y
  H*-X⊎Y→H*-X×H*-Y-pres· = DS-Ind-Prop.f _ _ _ _ (λ x p q i y → isSetH*X×Y _ _ (p y) (q y) i)
         (λ y → refl)
         (λ n a → DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*X×Y _ _)
                   refl
                   (λ m b → (base (n +' m) (fst (T (a ⌣ b)))) , base (n +' m) (snd (T (a ⌣ b)))
                                  ≡⟨ ≡-× (cong (base (n +' m)) (helperX a b))
                                         (cong (base (n +' m)) (helperY a b)) ⟩
                             (base (n +' m) ((fst (T a)) ⌣ (fst (T b)))) , base (n +' m) ((snd (T a)) ⌣ (snd (T b))) ∎ )
                   λ {U V} ind-U ind-V → cong₂ _+H*X×Y_ ind-U ind-V)
         (λ {U V} ind-U ind-V y → cong₂ _+H*X×Y_ (ind-U y) (ind-V y))

         where
         T : {n : ℕ} → coHom n (X ⊎ Y) → coHom n X × coHom n Y
         T {n} = fun (fst (Equiv-Coproduct-CoHom))

         helperX : {n : ℕ} → {m : ℕ} → (a : coHom n (X ⊎ Y)) → (b : coHom m (X ⊎ Y))
                    → fst (T (a ⌣ b)) ≡ (fst (T a)) ⌣ (fst (T b))
         helperX = ST.elim (λ x → isProp→isSet λ u v i y → squash₂ _ _ (u y) (v y) i )
                   λ g → ST.elim (λ _ → isProp→isSet (squash₂ _ _))
                   (λ h → refl)

         helperY : {n : ℕ} → {m : ℕ} → (a : coHom n (X ⊎ Y)) → (b : coHom m (X ⊎ Y))
                   → snd (T (a ⌣ b)) ≡ (snd (T a)) ⌣ (snd (T b))
         helperY = ST.elim (λ x → isProp→isSet λ u v i y → squash₂ _ _ (u y) (v y) i )
                   λ g → ST.elim (λ _ → isProp→isSet (squash₂ _ _))
                   (λ h → refl)

-----------------------------------------------------------------------------
-- Computation of the Cohomology Ring

module _
  (X : Type ℓ)
  (Y : Type ℓ')
  where

  open Equiv-Coproduct-Properties
  open Iso
  open RingEquivs

  CohomologyRing-Coproduct : RingEquiv (H*R(X ⊎ Y)) (DirectProd-Ring (H*R X) (H*R Y))
  fst (CohomologyRing-Coproduct) = isoToEquiv is
    where
    is : Iso (H* (X ⊎ Y)) (H* X × H* Y)
    fun is = H*-X⊎Y→H*-X×H*-Y
    inv is = H*-X×H*-Y→H*-X⊎Y
    rightInv is = e-sect
    leftInv is = e-retr
  snd (CohomologyRing-Coproduct) = makeIsRingHom
                                   H*-X⊎Y→H*-X×H*-Y-pres1
                                   H*-X⊎Y→H*-X×H*-Y-pres+
                                   H*-X⊎Y→H*-X×H*-Y-pres·

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- {-# OPTIONS -v tc.lhs:40 #-} {-# OPTIONS -v scope.pat:40 #-}
module Issue822 where

module M₁ where

  postulate [_] : Set

module M₂ where

  data D : Set₁ where
    [_] : Set → D

module M₃ where

  data D : Set₁ where
    [_] : Set → D

open M₁
open M₂
open M₃

Foo : _ → Set
Foo [ A ] = A

-- Strange error message:

-- Bug.agda:16,1-14
-- Left hand side gives too many arguments to a function of type
-- D → Set
-- when checking that the clause Foo [ A ] = A has type D → Set

-- If the two open statements are swapped, then we get a more
-- reasonable error message:

-- Bug.agda:16,1-10
-- Ambiguous name [_]. It could refer to any one of
--   M₂.[_] bound at /home/nad/research/dtp/pretty/Bug.agda:10,5-8
--   M₁.[_] bound at /home/nad/research/dtp/pretty/Bug.agda:5,13-16
-- when scope checking the left-hand side Foo [ A ] in the definition
-- of Foo

-- One could perhaps also argue that the code above should be
-- syntactically correct, because M₁.[_] can't be used in the pattern
-- (except for under a dot).

-- Andreas, 2013-03-21
-- To reproduce an error, one now needs ambiguous constructors.

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --no-auto-inline #-}

open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Equality

_>>_ : {A B : Set} → TC A → TC B → TC B
m >> m' = m >>= λ _ → m'

-- Normally auto-inlined
id : {A : Set} → A → A
id x = x

id-inline : {A : Set} → A → A
id-inline x = x
{-# INLINE id-inline #-}

f₁ : Nat → Nat
f₁ n = id n

f₂ : Nat → Nat
f₂ n = id-inline n

macro
  rhs : Name → Term → TC ⊤
  rhs f hole = do
    function (clause _ _ rhs ∷ _) ← getDefinition f
      where _ → typeError (strErr "fail" ∷ [])
    `rhs ← quoteTC rhs
    unify hole `rhs

pattern vArg x = arg (arg-info visible relevant) x
pattern hArg x = arg (arg-info hidden relevant) x

-- Should not be inlined
check₁ : rhs f₁ ≡ def (quote id) (hArg (def (quote Nat) []) ∷ vArg (var 0 []) ∷ [])
check₁ = refl

-- Should be inlined
check₂ : rhs f₂ ≡ var 0 []
check₂ = refl

max_forks_repo_name: shlevy/agda


text:
-- Andreas, 2017-08-23, issue #2714

-- This file should compile from within the interaction mode
-- without warning about missing main function.

{-# OPTIONS --no-main #-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Order morphisms
------------------------------------------------------------------------

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

open import Relation.Binary.Core

module Relation.Binary.Morphism.Structures
  {a b} {A : Set a} {B : Set b}
  where

open import Data.Product using (_,_)
open import Function.Definitions
open import Level
open import Relation.Binary.Morphism.Definitions A B

private
  variable
    ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

------------------------------------------------------------------------
-- Raw relations
------------------------------------------------------------------------

record IsRelHomomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
                         (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    cong : Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧

record IsRelMonomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
                         (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isHomomorphism : IsRelHomomorphism _∼₁_ _∼₂_ ⟦_⟧
    injective      : Injective _∼₁_ _∼₂_ ⟦_⟧

  open IsRelHomomorphism isHomomorphism public

record IsRelIsomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
                        (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isMonomorphism : IsRelMonomorphism _∼₁_ _∼₂_ ⟦_⟧
    surjective     : Surjective _∼₁_ _∼₂_ ⟦_⟧

  open IsRelMonomorphism isMonomorphism

  bijective : Bijective _∼₁_ _∼₂_ ⟦_⟧
  bijective = injective , surjective

------------------------------------------------------------------------
-- Raw orders
------------------------------------------------------------------------

record IsOrderHomomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
                           (_∼₁_ : Rel A ℓ₃) (_∼₂_ : Rel B ℓ₄)
                           (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                           where
  field
    cong  : Homomorphic₂ _≈₁_ _≈₂_ ⟦_⟧
    mono  : Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧

  module Eq where
    isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
    isRelHomomorphism = record { cong = cong }

  isRelHomomorphism : IsRelHomomorphism _∼₁_ _∼₂_ ⟦_⟧
  isRelHomomorphism = record { cong = mono }

record IsOrderMonomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
                           (_∼₁_ : Rel A ℓ₃) (_∼₂_ : Rel B ℓ₄)
                           (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                           where
  field
    isOrderHomomorphism : IsOrderHomomorphism _≈₁_ _≈₂_ _∼₁_ _∼₂_ ⟦_⟧
    injective           : Injective _≈₁_ _≈₂_ ⟦_⟧
    cancel              : Injective _∼₁_ _∼₂_ ⟦_⟧

  open IsOrderHomomorphism isOrderHomomorphism public
    hiding (module Eq)

  module Eq where
    isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧
    isRelMonomorphism = record
      { isHomomorphism = IsOrderHomomorphism.Eq.isRelHomomorphism isOrderHomomorphism
      ; injective      = injective
      }

  isRelMonomorphism : IsRelMonomorphism _∼₁_ _∼₂_ ⟦_⟧
  isRelMonomorphism = record
    { isHomomorphism = isRelHomomorphism
    ; injective      = cancel
    }

record IsOrderIsomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
                          (_∼₁_ : Rel A ℓ₃) (_∼₂_ : Rel B ℓ₄)
                          (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                          where
  field
    isOrderMonomorphism : IsOrderMonomorphism _≈₁_ _≈₂_ _∼₁_ _∼₂_ ⟦_⟧
    surjective          : Surjective _≈₁_ _≈₂_ ⟦_⟧

  open IsOrderMonomorphism isOrderMonomorphism public
    hiding (module Eq)

  module Eq where
    isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧
    isRelIsomorphism = record
      { isMonomorphism = IsOrderMonomorphism.Eq.isRelMonomorphism isOrderMonomorphism
      ; surjective     = surjective
      }


text:
module CoInf where

open import Codata.Musical.Notation

-- Check that ∞ can be used as an "expression".
test : Set → Set
test = ∞


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

open import Groups.Definition
open import Groups.Groups
open import Groups.Homomorphisms.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Groups.Lemmas
open import Groups.Homomorphisms.Lemmas

module Groups.QuotientGroup.Definition {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_·A_ : A → A → A} {_·B_ : B → B → B} (G : Group S _·A_) {H : Group T _·B_} {f : A → B} (fHom : GroupHom G H f) where

quotientGroupSetoid : (Setoid {a} {d} A)
quotientGroupSetoid = ansSetoid
  where
    open Setoid T
    open Group H
    open Equivalence eq
    ansSetoid : Setoid A
    Setoid._∼_ ansSetoid r s = (f (r ·A (Group.inverse G s))) ∼ 0G
    Equivalence.reflexive (Setoid.eq ansSetoid) {b} = transitive (GroupHom.wellDefined fHom (Group.invRight G)) (imageOfIdentityIsIdentity fHom)
    Equivalence.symmetric (Setoid.eq ansSetoid) {m} {n} pr = i
      where
        g : f (Group.inverse G (m ·A Group.inverse G n)) ∼ 0G
        g = transitive (homRespectsInverse fHom {m ·A Group.inverse G n}) (transitive (inverseWellDefined H pr) (invIdent H))
        h : f (Group.inverse G (Group.inverse G n) ·A Group.inverse G m) ∼ 0G
        h = transitive (GroupHom.wellDefined fHom (Equivalence.symmetric (Setoid.eq S) (invContravariant G))) g
        i : f (n ·A Group.inverse G m) ∼ 0G
        i = transitive (GroupHom.wellDefined fHom (Group.+WellDefined G (Equivalence.symmetric (Setoid.eq S) (invTwice G n)) (Equivalence.reflexive (Setoid.eq S)))) h
    Equivalence.transitive (Setoid.eq ansSetoid) {m} {n} {o} prmn prno = transitive (GroupHom.wellDefined fHom (Group.+WellDefined G (Equivalence.reflexive (Setoid.eq S)) (Equivalence.symmetric (Setoid.eq S) (Group.identLeft G)))) k
      where
        g : f (m ·A Group.inverse G n) ·B f (n ·A Group.inverse G o) ∼ 0G ·B 0G
        g = replaceGroupOp H reflexive reflexive prmn prno reflexive
        h : f (m ·A Group.inverse G n) ·B f (n ·A Group.inverse G o) ∼ 0G
        h = transitive g identLeft
        i : f ((m ·A Group.inverse G n) ·A (n ·A Group.inverse G o)) ∼ 0G
        i = transitive (GroupHom.groupHom fHom) h
        j : f (m ·A (((Group.inverse G n) ·A n) ·A Group.inverse G o)) ∼ 0G
        j = transitive (GroupHom.wellDefined fHom (fourWay+Associative G)) i
        k : f (m ·A ((Group.0G G) ·A Group.inverse G o)) ∼ 0G
        k = transitive (GroupHom.wellDefined fHom (Group.+WellDefined G (Equivalence.reflexive (Setoid.eq S)) (Group.+WellDefined G (Equivalence.symmetric (Setoid.eq S) (Group.invLeft G)) (Equivalence.reflexive (Setoid.eq S))))) j

quotientGroupByHom : Group (quotientGroupSetoid) _·A_
Group.+WellDefined (quotientGroupByHom) {x} {y} {m} {n} x~m y~n = ans
  where
    open Setoid T
    open Equivalence (Setoid.eq T)
    p1 : f ((x ·A y) ·A (Group.inverse G (m ·A n))) ∼ f ((x ·A y) ·A ((Group.inverse G n) ·A (Group.inverse G m)))
    p2 : f ((x ·A y) ·A ((Group.inverse G n) ·A (Group.inverse G m))) ∼ f (x ·A ((y ·A (Group.inverse G n)) ·A (Group.inverse G m)))
    p3 : f (x ·A ((y ·A (Group.inverse G n)) ·A (Group.inverse G m))) ∼ (f x) ·B f ((y ·A (Group.inverse G n)) ·A (Group.inverse G m))
    p4 : (f x) ·B f ((y ·A (Group.inverse G n)) ·A (Group.inverse G m)) ∼ (f x) ·B (f (y ·A (Group.inverse G n)) ·B f (Group.inverse G m))
    p5 : (f x) ·B (f (y ·A (Group.inverse G n)) ·B f (Group.inverse G m)) ∼ (f x) ·B (Group.0G H ·B f (Group.inverse G m))
    p6 : (f x) ·B (Group.0G H ·B f (Group.inverse G m)) ∼ (f x) ·B f (Group.inverse G m)
    p7 : (f x) ·B f (Group.inverse G m) ∼ f (x ·A (Group.inverse G m))
    p8 : f (x ·A (Group.inverse G m)) ∼ Group.0G H
    p1 = GroupHom.wellDefined fHom (Group.+WellDefined G (Equivalence.reflexive (Setoid.eq S)) (invContravariant G))
    p2 = GroupHom.wellDefined fHom (Equivalence.symmetric (Setoid.eq S) (fourWay+Associative G))
    p3 = GroupHom.groupHom fHom
    p4 = Group.+WellDefined H reflexive (GroupHom.groupHom fHom)
    p5 = Group.+WellDefined H reflexive (replaceGroupOp H (symmetric y~n) reflexive reflexive reflexive reflexive)
    p6 = Group.+WellDefined H reflexive (Group.identLeft H)
    p7 = symmetric (GroupHom.groupHom fHom)
    p8 = x~m
    ans : f ((x ·A y) ·A (Group.inverse G (m ·A n))) ∼ Group.0G H
    ans = transitive p1 (transitive p2 (transitive p3 (transitive p4 (transitive p5 (transitive p6 (transitive p7 p8))))))
Group.0G (quotientGroupByHom) = Group.0G G
Group.inverse (quotientGroupByHom) = Group.inverse G
Group.+Associative (quotientGroupByHom) {a} {b} {c} = ans
  where
    open Setoid T
    open Equivalence (Setoid.eq T)
    ans : f ((a ·A (b ·A c)) ·A (Group.inverse G ((a ·A b) ·A c))) ∼ Group.0G H
    ans = transitive (GroupHom.wellDefined fHom (transferToRight'' G (Group.+Associative G))) (imageOfIdentityIsIdentity fHom)
Group.identRight (quotientGroupByHom) {a} = ans
  where
    open Group G
    open Setoid T
    open Equivalence eq
    transitiveG = Equivalence.transitive (Setoid.eq S)
    ans : f ((a ·A 0G) ·A inverse a) ∼ Group.0G H
    ans = transitive (GroupHom.wellDefined fHom (transitiveG (Group.+WellDefined G (Group.identRight G) (Equivalence.reflexive (Setoid.eq S))) (Group.invRight G))) (imageOfIdentityIsIdentity fHom)
Group.identLeft (quotientGroupByHom) {a} = ans
  where
    open Group G
    open Setoid T
    open Equivalence eq
    transitiveG = Equivalence.transitive (Setoid.eq S)
    ans : f ((0G ·A a) ·A (inverse a)) ∼ Group.0G H
    ans = transitive (GroupHom.wellDefined fHom (transitiveG (Group.+WellDefined G (Group.identLeft G) (Equivalence.reflexive (Setoid.eq S))) (Group.invRight G))) (imageOfIdentityIsIdentity fHom)
Group.invLeft (quotientGroupByHom) {x} = ans
  where
    open Group G
    open Setoid T
    open Equivalence eq
    ans : f ((inverse x ·A x) ·A (inverse 0G)) ∼ (Group.0G H)
    ans = transitive (GroupHom.wellDefined fHom (Equivalence.transitive (Setoid.eq S) (replaceGroupOp G (Equivalence.symmetric (Setoid.eq S) (Group.invLeft G)) (Equivalence.symmetric (Setoid.eq S) (invIdent G)) (Equivalence.reflexive (Setoid.eq S)) ((Equivalence.reflexive (Setoid.eq S))) ((Equivalence.reflexive (Setoid.eq S)))) (identRight {0G}))) (imageOfIdentityIsIdentity fHom)
Group.invRight (quotientGroupByHom) {x} = ans
  where
    open Group G
    open Setoid T
    open Equivalence eq
    ans : f ((x ·A inverse x) ·A (inverse 0G)) ∼ (Group.0G H)
    ans = transitive (GroupHom.wellDefined fHom (Equivalence.transitive (Setoid.eq S) (replaceGroupOp G (Equivalence.symmetric (Setoid.eq S) (Group.invRight G)) (Equivalence.symmetric (Setoid.eq S) (invIdent G)) (Equivalence.reflexive (Setoid.eq S)) (Equivalence.reflexive (Setoid.eq S)) (Equivalence.reflexive (Setoid.eq S))) (identRight {0G}))) (imageOfIdentityIsIdentity fHom)


text:
module Prolegomenon where

open import Agda.Primitive
open import Relation.Binary
open import Algebra
open import Category.Applicative.Predicate

open import Algebra
open import Algebra.Structures
open import Category.Monad.Indexed
open import Algebra.FunctionProperties.Core
open import Function

PowerRightIdentity : ∀ {a ℓ} {A : Set a} → Rel A ℓ → ∀ {b} {B : Set b} → B → (B → A → A) → Set _
PowerRightIdentity _≈_ e _◃_ = ∀ x → (e ◃ x) ≈ x

PowerAssociative : ∀ {a b ℓ} {A : Set a} {B : Set b} → (A → A → Set ℓ) → (B → A → A) → (B → B → B) → Set _
PowerAssociative _≈_ _◃_ _∙_ = ∀ x a b → ((b ∙ a) ◃ x) ≈ (b ◃ (a ◃ x))

_over_ : ∀ {f} {F : Set f} {g} → (F → F → Set g) → ∀ {i} {I : Set i} {a} {A : Set a} → (A → I → F) → A → A → Set (i ⊔ g)
_*_ over f = λ x y → ∀ i → f x i * f y i

record IsMonoidTransformer {s ℓˢ} {S : Set s} (≈ˢ : Rel S ℓˢ) {m ℓᵐ} {M : Set m} (≈ᵐ : Rel M ℓᵐ) (∙ : Op₂ M) (ε : M) (◃ : M → S → S) : Set (s ⊔ ℓˢ ⊔ m ⊔ ℓᵐ) where
  field
    ◃-identity : PowerRightIdentity ≈ˢ ε ◃
    ≈ˢ-over-◃-⟶-≈ᵐ : ≈ˢ over ◃ ⇒ ≈ᵐ
    ≈ᵐ-to-≈ˢ-over-◃ : ≈ᵐ ⇒ ≈ˢ over ◃
    ◃-extracts-∙ : PowerAssociative ≈ˢ ◃ ∙

record MonoidTransformer ℓˢ ℓ⁼ˢ ℓᵐ ℓ⁼ᵐ
  : Set (lsuc (ℓˢ ⊔ ℓ⁼ˢ ⊔ ℓᵐ ⊔ ℓ⁼ᵐ)) where
  field
    base : Setoid ℓˢ ℓ⁼ˢ
    exponent : Monoid ℓᵐ ℓ⁼ᵐ

  module B = Setoid base
  module E = Monoid exponent
{-
  open Setoid base public renaming
    (Carrier to Carrierˢ
    ;_≈_ to _≈ˢ_
    ;reflexive to reflexiveˢ
    ;refl to reflˢ
    ;trans to transˢ
    ;sym to symˢ
    )

  open Monoid exponent public renaming
    (Carrier to Carrierᵐ
    ;_≈_ to _≈ᵐ_
    ;reflexive to reflexiveᵐ
    ;_∙_ to _∙_
    ;ε to ε
    ;refl to reflᵐ
    ;trans to transᵐ
    ;sym to symᵐ)
-}
  infixl 6 _◃_
  field
    _◃_ : E.Carrier → B.Carrier → B.Carrier
    isMonoidTransformer : IsMonoidTransformer B._≈_ E._≈_ E._∙_ E.ε _◃_

  open IsMonoidTransformer isMonoidTransformer public


text:
module Int where

open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg
open import Data.Char hiding (fromNat)
open import Data.Integer hiding (_≤_; suc)
open import Data.Integer.Literals
open import Data.List
open import Data.Nat hiding (_≤_)
open import Data.String
open import Data.Unit hiding (_≤_)
open import Function
open import Show

postulate
  Int : Set
  primShow : Int → List Char
  primFromInteger : ℤ → Int
  primToInteger : Int → ℤ
  primMinBound : Int
  primMaxBound : Int

{-# COMPILE GHC Int = type Int #-}
{-# COMPILE GHC primShow = show #-}
{-# COMPILE GHC primFromInteger = fromInteger #-}
{-# COMPILE GHC primToInteger = toInteger #-}
{-# COMPILE GHC primMinBound = minBound #-}
{-# COMPILE GHC primMaxBound = maxBound #-}

instance ShowInt : Show Int
ShowInt = fromHaskell primShow

instance Numberℤ : Number ℤ
Numberℤ = number

-- Its values can be automatically derived as instance arguments, but
-- is otherwise identical to the standard library version
data _ℕ≤_ : ℕ → ℕ → Set where
  instance z≤n : ∀ {n}                 → zero  ℕ≤ n
  instance s≤s : ∀ {m n} {{m≤n : m ℕ≤ n}} → suc m ℕ≤ suc n

-- Its values can be automatically derived as instance arguments, but
-- is otherwise identical to the standard library version
data _≤_ : ℤ → ℤ → Set where
  instance -≤- : {m n : ℕ} → {{n≤m : n ℕ≤ m}} → -[1+ m ] ≤ -[1+ n ]
  instance -≤+ : {m n : ℕ} → (-[1+ m ]) ≤ (+ n)
  instance +≤+ : {m n : ℕ} → {{m≤n : m ℕ≤ n}} → (+ m) ≤ (+ n)

-- Use a literal for the bound so that Agda can automatically check
-- the constraints for fromNat and fromNeg. Value taken from
-- https://hackage.haskell.org/package/base-4.12.0.0/docs/Prelude.html#t:Int
maxBound : ℤ
maxBound = 536870911

-- Use the actual bound in compiled code
{-# COMPILE GHC maxBound = toInteger (maxBound :: Int) #-}

instance NumberInt : Number Int
NumberInt = record { Constraint = Constraint ; fromNat = fromNatInt }
  where
    Constraint : ℕ → Set
    Constraint n = (+ n) ≤ maxBound

    fromNatInt : ∀ n → {{_ : Constraint n}} → Int
    fromNatInt n = primFromInteger (+ n)

max_stars_repo_name: cruhland/agda-editor

max_issues_repo_name: cruhland/agda-editor

max_forks_repo_name: cruhland/agda-editor


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

open import lib.Basics
open import lib.types.Sigma
open import lib.NType2

open import Preliminaries
open import Truncation_Level_Criteria

module Anonymous_Existence_CollSplit where

-- CHAPTER 4
-- SECTION 4.1

-- Lemma 4.1.2, part 1
constant-implies-path-constant : ∀ {i j} {X : Type i} {Y : Type j} → (f : X → Y) → (const f)
  → (x₁ x₂ : X) → const (ap f {x = x₁} {y = x₂})
constant-implies-path-constant {X = X} f c x₁ x₂ p₁ p₂ = claim-cor where
  claim : {x₃ x₄ : X} → {p : x₃ == x₄} → (ap f p) == ! (c x₃ x₃) ∙ (c x₃ x₄)
  claim {x₃} {p = idp} = ! (!-inv-l (c x₃ x₃))
  claim-cor : ap f p₁ == ap f p₂
  claim-cor =
    ap f p₁                 =⟨ claim ⟩
    ! (c x₁ x₁) ∙ (c x₁ x₂) =⟨ ! claim ⟩
    ap f p₂                 ∎

-- Lemma 4.1.2, part 2
constant-refl :  ∀ {i j} {X : Type i} {Y : Type j} → (f : X → Y) → (const f)
  → (x : X) → (p : x == x) → ap f p == idp
constant-refl f c x p = constant-implies-path-constant f c x x p idp

-- todo: this is not in the library?
-- We also need the following very simple lemma:
ap-id-trivial : ∀ {i} {X : Type i} → {x₁ x₂ : X} → (p : x₁ == x₂) → ap (idf X) p == p
ap-id-trivial idp = idp

-- Main Lemma 4.1.1 needs a bit of preparation.
fix : ∀ {i} {X : Type i} → (f : X → X) → Type i
fix {X = X} f = Σ X λ x → x == f x

-- let us give a name to the map X → fix f:
to-fix : ∀ {i} {X : Type i} → (f : X → X) → (const f) → X → fix f
to-fix f c x₀ = f x₀ , c _ _

-- the other direction is just projection:
from-fix : ∀ {i} {X : Type i} → (f : X → X) → fix f → X
from-fix f (x₀ , p₀) = x₀

-- let us structure the proof of the fixed point lemma a bit:
module fixedpoint {i : ULevel} {X : Type i}  (f : X → X) (c : const f) where

  -- let us show that (x , p) == (x , q) first
  module _ (x : X) (p q : x == f x) where
    t : x == x
    t = p ∙ ! q

    r : f x == f x
    r = ap f t

    r-is-triv : r == idp
    r-is-triv = constant-refl f c x t

    t' : x == x
    t' = ap (idf X) t

    t'-is-t : t' == t
    t'-is-t = ap-id-trivial t

    trans-t-p-is-q : transport (λ y → y == f y) t p == q
    trans-t-p-is-q =
      transport (λ y → y == f y) t p   =⟨  transport-is-comp (idf X) f t p  ⟩
      ! t' ∙ p ∙ r                     =⟨ ap (λ s → ! s ∙ p ∙ r) t'-is-t ⟩
      ! t ∙ p ∙ r                      =⟨ ! (∙-assoc (! t) _ _) ⟩
      (! t ∙ p) ∙ r                    =⟨ ap (λ s → (! t ∙ p) ∙ s) r-is-triv ⟩
      (! t ∙ p) ∙ idp                  =⟨ ∙-unit-r _ ⟩
      ! t ∙ p                          =⟨ ap (λ s → s ∙ p) (!-∙ p (! q)) ⟩
      (! (! q) ∙ ! p) ∙ p              =⟨ ∙-assoc (! (! q)) _ _ ⟩
      ! (! q) ∙ ! p ∙ p                =⟨ ap (λ s → ! (! q) ∙ s) (!-inv-l p) ⟩
      ! (! q) ∙ idp                    =⟨ ∙-unit-r _ ⟩
      ! (! q)                          =⟨ !-! _ ⟩
      q                                ∎

    single-x-claim : (x , p) == (x , q)
    single-x-claim = pair= t (from-transp _ _ trans-t-p-is-q)

  -- Now, we can prove that (x₁ , p₁) and (x₂ , p₂) are always equal:
  fix-paths : has-all-paths (fix f)
  fix-paths (x₁ , p₁) (x₂ , p₂) =
    (x₁ , p₁) =⟨ pair= (p₁ ∙ c x₁ x₂ ∙ ! p₂) (from-transp _ (p₁ ∙ c x₁ x₂ ∙ ! p₂) idp) ⟩
    (x₂ , _)  =⟨ single-x-claim x₂ _ _ ⟩
    (x₂ , p₂) ∎

-- finally, the proof of the fixed point lemma
fixed-point : ∀ {i} {X : Type i} → (f : X → X) → (const f) → is-prop (fix f)
fixed-point {X = X} f c = all-paths-is-prop (fixedpoint.fix-paths f c)

-- Sattler's argument
fixed-point-alt :  ∀ {i} {X : Type i} → (f : X → X) → (const f) → is-prop (fix f)
fixed-point-alt {X = X} f c = inhab-to-contr-is-prop inh→contr where
  inh→contr : fix f → is-contr (fix f)
  inh→contr (x₀ , p₀) = equiv-preserves-level {A = Σ X λ x → x == f x₀} {B = fix f} claim-Σ (pathto-is-contr _) where
    claim : (x : X) → (x == f x₀) ≃ (x == f x)
    claim x = (λ p → p ∙ c x₀ x) , post∙-is-equiv _
    claim-Σ : (Σ X λ x → x == f x₀) ≃ fix f
    claim-Σ = equiv-Σ-snd claim

--from here, we need truncation
module with-weak-trunc where
  open wtrunc

  -- Corollary 4.1.3
  -- let us define the following map:
  trunc-to-fix : ∀ {i} {X : Type i} → (fc : coll X) → ∣∣ X ∣∣ → fix (fst fc)
  trunc-to-fix (f , c) z = tr-rec (fixed-point f c) (to-fix f c) z

  coll→splitSup : ∀ {i} {X : Type i} → coll X → splitSup X
  coll→splitSup (f , c) = (from-fix f) ∘ trunc-to-fix (f , c)

  -- Theorem 4.1.4
  coll↔splitSup : ∀ {i} {X : Type i} → coll X ↔ splitSup X
  coll↔splitSup {X = X} = coll→splitSup , splitSup→coll where
    splitSup→coll : splitSup X → coll X
    splitSup→coll hst = f , c where
      f = hst ∘ ∣_∣
      c : const f
      c x₁ x₂ =
        f x₁      =⟨ idp ⟩
        hst ∣ x₁ ∣ =⟨ ap hst (prop-has-all-paths tr-is-prop _ _) ⟩
        hst ∣ x₂ ∣ =⟨ idp ⟩
        f x₂      ∎

  -- preparation for Statement 4.1.5 - we need to prove that
  -- f : X → X with an inhabitant of ∣∣ const f ∣∣ is enough
  -- to show that fix f is propositional.
  fixed-point-strong : ∀ {i} {X : Type i} → (f : X → X) → ∣∣ const f ∣∣ → is-prop (fix f)
  fixed-point-strong {X = X} f = tr-rec {X = const f} {P = is-prop(fix f)} is-prop-is-prop (fixed-point f)

  -- Statement 4.1.5 (we exclude the part which is already included in Theorem 4.1.4)
  -- to get an easy proof of the addendum, we structure it in the following way:
  module thm46 {i : ULevel} {X : Type i}  where
    module _ (fhc : Σ (X → X) (λ f → ∣∣ const f ∣∣))  where
      f = fst fhc
      hc = snd fhc
      trunc-const-fix : ∣∣ X ∣∣ → ∣∣ const f ∣∣ → fix f
      trunc-const-fix z = tr-rec {X = const f} {P = fix f} (fixed-point-strong f hc) (λ c → trunc-to-fix (f , c) z)
      trunc-fix : ∣∣ X ∣∣ → fix f
      trunc-fix z = trunc-const-fix z hc
      g : X → X
      g = fst ∘ trunc-fix ∘ ∣_∣
      g-const : const g
      g-const x₁ x₂ = ap (fst ∘ trunc-fix) (prop-has-all-paths tr-is-prop _ _)

  coll↔hideProof : ∀ {i} {X : Type i} → coll X ↔ Σ (X → X) (λ f → ∣∣ const f ∣∣)
  coll↔hideProof {X = X} = one , two where
    one : coll X → Σ (X → X) (λ f → ∣∣ const f ∣∣)
    one (f , c) = f , ∣ c ∣
    two : (Σ (X → X) (λ f → ∣∣ const f ∣∣)) → coll X
    two fhc = thm46.g fhc , thm46.g-const fhc

  -- Statement 4.1.5 addendum
  merely-equal : ∀ {i} {X : Type i} → (fhc : Σ (X → X) (λ f → ∣∣ const f ∣∣)) → ∣∣ ((x : X) → fst fhc x == thm46.g fhc x) ∣∣
  merely-equal {X = X} (f , hc) = tr-rec tr-is-prop (∣_∣ ∘ const-equal) hc where
    open thm46
    const-equal : const f → (x : X) → f x == thm46.g (f , hc) x
    const-equal c x =
      f x                                     =⟨ idp ⟩
      fst (to-fix f c x)                      =⟨ ap fst (! (trunc-β _ _ x)) ⟩
      fst (trunc-to-fix (f , c) ∣ x ∣)          =⟨ ap fst (! (trunc-β _ _ c)) ⟩
      fst (trunc-const-fix (f , hc) ∣ x ∣ ∣ c ∣) =⟨ ap (λ hc' → fst (trunc-const-fix (f , hc) ∣ x ∣ hc')) (prop-has-all-paths tr-is-prop _ _) ⟩
      fst (trunc-const-fix (f , hc) ∣ x ∣ hc)   =⟨ idp ⟩
      fst (trunc-fix (f , hc) ∣ x ∣)            =⟨ idp ⟩
      g (f , hc) x                             ∎

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 #-}
module PathStructure.Unit where

open import Equivalence
open import Types

split-path : {x y : ⊤} → x ≡ y → ⊤
split-path _ = _

merge-path : {x y : ⊤} → ⊤ → x ≡ y
merge-path _ = refl

split-merge-eq : {x y : ⊤} → (x ≡ y) ≃ ⊤
split-merge-eq
  = split-path
  , (merge-path , λ _ → refl)
  , (merge-path , J {A = ⊤}
      (λ _ _ p → refl ≡ p)
      (λ _ → refl) _ _)

max_stars_repo_name: vituscze/HoTT-lectures

max_issues_repo_name: vituscze/HoTT-lectures

max_forks_repo_name: vituscze/HoTT-lectures


text:
-- Andreas, 2017-11-01, issue #2824
-- Allow built-ins that define a new name to be in parametrized module.

module Issue2824SizeU (A : Set) where  -- This is the top-level module header.

{-# BUILTIN SIZEUNIV SizeU #-}

-- Should succeed.


text:
open import Agda.Builtin.Nat

data Vec (A : Set) : Nat → Set where

variable
  A  : Set
  x  : A
  n  : Nat
  xs : Vec A n

postulate
  IsNil : Vec A 0 → Set

foo : (xs : Vec A n) → IsNil xs
foo = {!!}


text:
module prelude.Stream where
open import prelude
open import Data.List as L using (List)

record Stream (a : Set) : Set where
    constructor _∷_
    coinductive
    field
        hd : a
        tl : Stream a
open Stream

take : ∀ {a} → ℕ → Stream a → List a
take ℕz xs = L.[]
take (ℕs n) xs = hd xs L.∷ take n (tl xs)

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Product
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℚ using (ℚ)
open import Data.List
open import Relation.Binary.PropositionalEquality

module reachability-output where

private
  VEHICLE_PROJECT_FILE = "TODO_projectFile"

f : Tensor ℚ (2 ∷ []) → ℚ
f = evaluate record
  { projectFile = VEHICLE_PROJECT_FILE
  ; networkUUID = "TODO_networkUUID"
  }

abstract
  reachable : ∃ λ (x : Tensor ℚ (2 ∷ [])) → f x ≡ ℤ.+ 0 ℚ./ 1
  reachable = checkProperty record
    { projectFile  = VEHICLE_PROJECT_FILE
    ; propertyUUID = "TODO_propertyUUID"
    }

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: wenkokke/vehicle