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

open import lib.Basics
open import lib.NType2
open import lib.types.Empty
open import lib.types.Group
open import lib.types.LoopSpace
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.types.TLevel
open import lib.types.Truncation
open import lib.groups.GroupProduct
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism
open import lib.groups.LoopSpace
open import lib.groups.TruncationGroup
open import lib.groups.Unit

module lib.groups.HomotopyGroup where

{- Higher homotopy groups -}
module _ {i} where

  πS : (n : ℕ) (X : Ptd i) → Group i
  πS n X = Trunc-group (Ω^S-group-structure n X)

  π'S : (n : ℕ) (X : Ptd i) → Group i
  π'S n X = Trunc-group (Ω^'S-group-structure n X)

  fundamental-group : (X : Ptd i) → Group i
  fundamental-group X = πS 0 X

module _ {i j} (n : ℕ) {X : Ptd i} {Y : Ptd j} where

  πS-fmap : X ⊙→ Y → (πS n X →ᴳ πS n Y)
  πS-fmap F = Trunc-group-fmap (Ω^S-group-structure-fmap n F)

  π'S-fmap : X ⊙→ Y → (π'S n X →ᴳ π'S n Y)
  π'S-fmap F = Trunc-group-fmap (Ω^'S-group-structure-fmap n F)

  πS-emap : (X ⊙≃ Y) → (πS n X ≃ᴳ πS n Y)
  πS-emap e = Trunc-group-emap (Ω^S-group-structure-emap n e)

  π'S-emap : (X ⊙≃ Y) → (π'S n X ≃ᴳ π'S n Y)
  π'S-emap e = Trunc-group-emap (Ω^'S-group-structure-emap n e)

{- π_(n+1) of a space is π_n of its loop space -}
abstract
  πS-Ω-split-iso : ∀ {i} (n : ℕ) (X : Ptd i)
    → πS (S n) X ≃ᴳ πS n (⊙Ω X)
  πS-Ω-split-iso n X =
    group-hom
      (Trunc-fmap (Ω^-Ω-split (S n) X))
      (Trunc-elim
        (λ p → Trunc-elim
          (λ q → ap [_] (Ω^S-Ω-split-∙ n X p q)))) ,
    Trunc-isemap {n = 0} (Ω^-Ω-split-is-equiv (S n) X)

{- We can shift the truncation inside the loop in the definition of π -}
module _ {i} where

  private
    record Ω^STruncPreIso (n : ℕ) (m : ℕ₋₂) (k : ℕ₋₂) (X : Ptd i)
      : Type i where
      field
        F : ⊙Ω^ (S n) (⊙Trunc k X) ⊙→ ⊙Trunc m (⊙Ω^ (S n) X)
        pres-comp : ∀ (p q : Ω^ (S n) (⊙Trunc k X))
          → fst F (Ω^S-∙ n p q) == Trunc-fmap2 (Ω^S-∙ n) (fst F p) (fst F q)
        e : is-equiv (fst F)

    Ω^S-Trunc-preiso : (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
      → Ω^STruncPreIso n m (⟨ S n ⟩₋₂ +2+ m) X
    Ω^S-Trunc-preiso O m X =
      record { F = (–> (Trunc=-equiv [ pt X ] [ pt X ]) , idp);
               pres-comp = Trunc=-∙-comm;
               e = snd (Trunc=-equiv [ pt X ] [ pt X ]) }
    Ω^S-Trunc-preiso (S n) m X =
      let
        r : Ω^STruncPreIso n (S m) (⟨ S n ⟩₋₂ +2+ S m) X
        r = Ω^S-Trunc-preiso n (S m) X

        H = (–> (Trunc=-equiv [ idp^ (S n) ] [ idp^ (S n) ]) , idp)
        G = ⊙Ω-fmap (Ω^STruncPreIso.F r)
      in
      transport (λ k → Ω^STruncPreIso (S n) m k X)
        (+2+-βr ⟨ S n ⟩₋₂ m)
        (record {
           F = H ⊙∘ G;
           pres-comp = λ p q →
             ap (fst H) (Ω^S-fmap-∙ 0 (Ω^STruncPreIso.F r) p q)
             ∙ (Trunc=-∙-comm (fst G p) (fst G q));
           e = snd (Trunc=-equiv [ idp^ (S n) ] [ idp^ (S n) ]
                    ∘e Ω^-emap 1 (Ω^STruncPreIso.F r , Ω^STruncPreIso.e r))})

  Ω^S-group-Trunc-fuse-diag-iso : (n : ℕ) (X : Ptd i)
    → Ω^S-group n (⊙Trunc ⟨ S n ⟩ X) ≃ᴳ πS n X
  Ω^S-group-Trunc-fuse-diag-iso n X = group-hom (fst F) pres-comp , e
    where
    r = transport (λ k → Ω^STruncPreIso n 0 k X)
                  (+2+0 ⟨ S n ⟩₋₂) (Ω^S-Trunc-preiso n 0 X)
    open Ω^STruncPreIso r

{- favonia: the same lemma for the alternative homotopy groups is trivial. -}

  Ω^'S-group-Trunc-fuse-diag-iso : (n : ℕ) (X : Ptd i)
    → Ω^'S-group n (⊙Trunc ⟨ S n ⟩ X) ≃ᴳ π'S n X
  Ω^'S-group-Trunc-fuse-diag-iso O X =
    ≃-to-≃ᴳ (Trunc=-equiv [ pt X ] [ pt X ]) Trunc=-∙-comm
  Ω^'S-group-Trunc-fuse-diag-iso (S n) X =
        Ω^'S-group-Trunc-fuse-diag-iso n (⊙Ω X)
    ∘eᴳ Ω^'S-group-emap n {X = ⊙Ω (⊙Trunc ⟨ S (S n) ⟩ X)} (≃-to-⊙≃ (Trunc=-equiv [ pt X ] [ pt X ]) idp)

abstract
  πS-Trunc-fuse-≤-iso : ∀ {i} (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
    → (⟨ S n ⟩ ≤T m) → πS n (⊙Trunc m X) ≃ᴳ πS n X
  πS-Trunc-fuse-≤-iso n m X Sn≤m =
    πS n (⊙Trunc m X)
      ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso n (⊙Trunc m X) ⁻¹ᴳ ⟩
    Ω^S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X))
      ≃ᴳ⟨ Ω^S-group-emap n (≃-to-⊙≃ (Trunc-fuse-≤ (de⊙ X) Sn≤m) idp) ⟩
    Ω^S-group n (⊙Trunc ⟨ S n ⟩ X)
      ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso n X ⟩
    πS n X
      ≃ᴳ∎

  π'S-Trunc-fuse-≤-iso : ∀ {i} (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
    → (⟨ S n ⟩ ≤T m) → π'S n (⊙Trunc m X) ≃ᴳ π'S n X
  π'S-Trunc-fuse-≤-iso n m X Sn≤m =
    π'S n (⊙Trunc m X)
      ≃ᴳ⟨ Ω^'S-group-Trunc-fuse-diag-iso n (⊙Trunc m X) ⁻¹ᴳ ⟩
    Ω^'S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X))
      ≃ᴳ⟨ Ω^'S-group-emap n (≃-to-⊙≃ (Trunc-fuse-≤ (de⊙ X) Sn≤m) idp) ⟩
    Ω^'S-group n (⊙Trunc ⟨ S n ⟩ X)
      ≃ᴳ⟨ Ω^'S-group-Trunc-fuse-diag-iso n X ⟩
    π'S n X
      ≃ᴳ∎

  πS-Trunc-fuse->-iso : ∀ {i} (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
    → (m <T ⟨ S n ⟩) → πS n (⊙Trunc m X) ≃ᴳ 0ᴳ
  πS-Trunc-fuse->-iso n m X m<n =
    πS n (⊙Trunc m X)
      ≃ᴳ⟨ Ω^S-group-Trunc-fuse-diag-iso n (⊙Trunc m X) ⁻¹ᴳ ⟩
    Ω^S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X))
      ≃ᴳ⟨ contr-iso-0ᴳ _ $ inhab-prop-is-contr
           (Group.ident (Ω^S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X))))
           {{Ω^-level -1 (S n) _ $ Trunc-preserves-level ⟨ S n ⟩ $
             raise-level-≤T
               (transport (λ k → m ≤T k) (+2+-comm -1 ⟨ S n ⟩₋₂) (<T-to-≤T m<n))
               (Trunc-level {n = m})}} ⟩
    0ᴳ ≃ᴳ∎

  π'S-Trunc-fuse->-iso : ∀ {i} (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
    → (m <T ⟨ S n ⟩) → π'S n (⊙Trunc m X) ≃ᴳ 0ᴳ
  π'S-Trunc-fuse->-iso n m X m<n =
    π'S n (⊙Trunc m X)
      ≃ᴳ⟨ Ω^'S-group-Trunc-fuse-diag-iso n (⊙Trunc m X) ⁻¹ᴳ ⟩
    Ω^'S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X))
      ≃ᴳ⟨ contr-iso-0ᴳ _ $ inhab-prop-is-contr
           (Group.ident (Ω^'S-group n (⊙Trunc ⟨ S n ⟩ (⊙Trunc m X))))
           {{Ω^'-is-prop (S n) _ $ Trunc-preserves-level ⟨ S n ⟩ $
             raise-level-≤T (<T-to-≤T m<n) (Trunc-level {n = m})}} ⟩
    0ᴳ ≃ᴳ∎

  -- XXX Naming conventions?
  πS->level-econv : ∀ {i} (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
    → (m <T ⟨ S n ⟩) → {{_ : has-level m (de⊙ X)}}
    → πS n X ≃ᴳ 0ᴳ
  πS->level-econv n m X lt =
    πS n X
      ≃ᴳ⟨ πS-emap n (⊙unTrunc-equiv X ⊙⁻¹) ⟩
    πS n (⊙Trunc m X)
      ≃ᴳ⟨ πS-Trunc-fuse->-iso n m X lt ⟩
    0ᴳ
      ≃ᴳ∎

  π'S->level-econv : ∀ {i} (n : ℕ) (m : ℕ₋₂) (X : Ptd i)
    → (m <T ⟨ S n ⟩) → {{_ : has-level m (de⊙ X)}}
    → π'S n X ≃ᴳ 0ᴳ
  π'S->level-econv n m X lt =
    π'S n X
      ≃ᴳ⟨ π'S-emap n (⊙unTrunc-equiv X ⊙⁻¹) ⟩
    π'S n (⊙Trunc m X)
      ≃ᴳ⟨ π'S-Trunc-fuse->-iso n m X lt ⟩
    0ᴳ
      ≃ᴳ∎

{- πₙ(X × Y) == πₙ(X) × πₙ(Y) -}
module _ {i j} (n : ℕ) (X : Ptd i) (Y : Ptd  j) where

  πS-× : πS n (X ⊙× Y) ≃ᴳ πS n X ×ᴳ πS n Y
  πS-× = Trunc-group-× _ _ ∘eᴳ Trunc-group-emap (Ω^S-group-structure-× n X Y)

  π'S-× : π'S n (X ⊙× Y) ≃ᴳ π'S n X ×ᴳ π'S n Y
  π'S-× = Trunc-group-× _ _ ∘eᴳ Trunc-group-emap (Ω^'S-group-structure-× n X Y)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
module _ where

module A where

  infixl 0 _+_

  data D : Set where
    •   : D
    _+_ : D → D → D

module B where

  infixr 0 _+_

  data D : Set where
    •   : D
    _+_ : D → D → D

open A
open B

Foo : A.D
Foo = • + • + •

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Oscar.Class.Substitute where

open import Oscar.Class.Substitution
open import Oscar.Data.Equality
open import Oscar.Function
open import Oscar.Relation
open import Oscar.Level

record Substitute {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) {d} (D : A → Set d) : Set (a ⊔ b ⊔ c ⊔ d) where
  field
    ⦃ substitution ⦄ : Substitution B C
    _◃_ : ∀ {m n} → (B m → C n) → m ⟨ D ⟩→ n
    ◃-identity : ∀ {m} → (x : D m) → ε ◃ x ≡ x
    ◃-associativity : ∀ {l m n} (f : B l → C m) (g : B m → C n) (t : D l) → (g ◇ f) ◃ t ≡ g ◃ (f ◃ t)
    ◃-extensionality : ∀ {m n} {f g : B m → C n} → f ≡̇ g → f ◃_ ≡̇ g ◃_

open Substitute ⦃ … ⦄ public

{-# DISPLAY Substitute._◃_ _ = _◃_ #-}

instance Substitute-id : ∀ {a} {A : Set a} {bcd} {BCD : A → Set bcd} → Substitute BCD BCD BCD
Substitute.substitution Substitute-id = Substitution-id
Substitute._◃_ Substitute-id = id
Substitute.◃-identity Substitute-id _ = refl
Substitute.◃-associativity Substitute-id _ _ _ = refl
Substitute.◃-extensionality Substitute-id f≡̇g = f≡̇g

-- record Substitution {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) {d} (D : A → Set d) : Set (a ⊔ b ⊔ c ⊔ d) where
--   field
--     _◃_ : ∀ {m n} → (B m → C n) → m ⟨ D ⟩→ n
--     ε : ∀ {m} → B m → C m
--     ◃-identity : ∀ {m} → (x : D m) → ε ◃ x ≡ x
--     _◇_ : ∀ {l m n} → (g : B m → C n) (f : B l → C m) → B l → C n
--     ◃-associativity : ∀ {l m n} → {f : B m → C n} {g : B l → C m} (t : D l) → (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)
--     ◃-extensionality : ∀ {m n} {f g : B m → C n} → f ≡̇ g → f ◃_ ≡̇ g ◃_

-- {-
--   Unifies : ∀ {m} (s t : A m) → Property m
--   Unifies s t f = f ◃ s ≡ f ◃ t
-- -}

-- open Substitution ⦃ … ⦄ public

-- -- record Substitution {a} {A : Set a} {b} (S : A → A → Set b) {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
-- --   field
-- --     _◃_ : ∀ {m n} → S m n → m ⟨ C ⟩→ n
-- --     ε : ∀ {m} → S m m
-- --     ◃-identity : ∀ {m} → (x : C m) → ε ◃ x ≡ x
-- --     _◇_ : ∀ {l m n} → S m n → S l m → S l n

-- --   field
-- --     ◃-associativity : ∀ {l m n} → {f : S m n} {g : S l m} (t : C l) → (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)
-- --     ◃-extensionality : ∀ {m n} {f g : S m n} → f ≡ g → f ◃_ ≡̇ g ◃_

-- -- open Substitution ⦃ … ⦄ public

-- -- -- record Substitution {a} {A : Set a} {b} (B : A → Set b) {c} (C : A → Set c) : Set (a ⊔ b ⊔ c) where
-- -- --   field
-- -- --     _◃_ : ∀ {m n} → (B m → C n) → m ⟨ C ⟩→ n
-- -- --     ε : ∀ {m} → B m → C m
-- -- --     ◃-identity : ∀ {m} → (x : C m) → ε ◃ x ≡ x

-- -- --   _◇_ : ∀ {l m n} → (f : B m → C n) (g : B l → C m) → B l → C n
-- -- --   _◇_ f g = (f ◃_) ∘ g

-- -- --   field
-- -- --     ◃-associativity : ∀ {l m n} → {f : B m → C n} {g : B l → C m} (t : C l) → (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)
-- -- --     ◃-extensionality : ∀ {m n} {f g : B m → C n} → f ≡̇ g → f ◃_ ≡̇ g ◃_

-- -- -- {-
-- -- --   Unifies : ∀ {m} (s t : A m) → Property m
-- -- --   Unifies s t f = f ◃ s ≡ f ◃ t
-- -- -- -}

-- -- -- open Substitution ⦃ … ⦄ public

-- -- -- instance Substitution⋆ : ∀ {a} {A : Set a} {bc} {BC : A → Set bc} → Substitution BC BC
-- -- -- Substitution._◃_ Substitution⋆ = id
-- -- -- Substitution.ε Substitution⋆ = id
-- -- -- Substitution.◃-identity Substitution⋆ _ = refl
-- -- -- Substitution.◃-associativity Substitution⋆ _ = refl
-- -- -- Substitution.◃-extensionality Substitution⋆ f≡̇g x = f≡̇g x


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists where all elements satisfy a given property
------------------------------------------------------------------------

module Data.List.All where

open import Data.List as List hiding (map; all)
open import Data.List.Any as Any using (here; there)
open Any.Membership-≡ using (_∈_; _⊆_)
open import Function
open import Level
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary using (Decidable) renaming (_⊆_ to _⋐_)
open import Relation.Binary.PropositionalEquality

-- All P xs means that all elements in xs satisfy P.

infixr 5 _∷_

data All {a p} {A : Set a}
         (P : A → Set p) : List A → Set (p ⊔ a) where
  []  : All P []
  _∷_ : ∀ {x xs} (px : P x) (pxs : All P xs) → All P (x ∷ xs)

head : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} →
       All P (x ∷ xs) → P x
head (px ∷ pxs) = px

tail : ∀ {a p} {A : Set a} {P : A → Set p} {x xs} →
       All P (x ∷ xs) → All P xs
tail (px ∷ pxs) = pxs

lookup : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A} →
         All P xs → (∀ {x : A} → x ∈ xs → P x)
lookup []         ()
lookup (px ∷ pxs) (here refl)  = px
lookup (px ∷ pxs) (there x∈xs) = lookup pxs x∈xs

tabulate : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
           (∀ {x} → x ∈ xs → P x) → All P xs
tabulate {xs = []}     hyp = []
tabulate {xs = x ∷ xs} hyp = hyp (here refl) ∷ tabulate (hyp ∘ there)

map : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} →
      P ⋐ Q → All P ⋐ All Q
map g []         = []
map g (px ∷ pxs) = g px ∷ map g pxs

all : ∀ {a p} {A : Set a} {P : A → Set p} →
      Decidable P → Decidable (All P)
all p []       = yes []
all p (x ∷ xs) with p x
all p (x ∷ xs) | yes px = Dec.map′ (_∷_ px) tail (all p xs)
all p (x ∷ xs) | no ¬px = no (¬px ∘ head)


text:
{-# OPTIONS --universe-polymorphism #-}
module Literals where

open import Common.Nat
open import Common.Float
open import Common.Char
open import Common.String
open import Common.Unit
open import Common.IO

afloat : Float
afloat = 1.23

astring : String
astring = "abc"

achar : Char
achar = 'd'

anat : Nat
anat = 123

main : IO Unit
main =
  printFloat  afloat  ,,
  putStr      astring ,,
  printChar   achar   ,,
  printNat    anat    ,,
  putStrLn ""

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import HoTT

module homotopy.HSpace where

-- This is just an approximation because
-- not all higher cells are killed.
record HSpaceStructure {i} (X : Ptd i) : Type i where
  constructor hSpaceStructure
  field
    ⊙μ : (X ⊙× X) ⊙→ X

  μ : de⊙ X → de⊙ X → de⊙ X
  μ = curry (fst ⊙μ)

  field
    ⊙unit-l : ⊙μ ⊙∘ ⊙×-inr X X ⊙∼ ⊙idf X
    ⊙unit-r : ⊙μ ⊙∘ ⊙×-inl X X ⊙∼ ⊙idf X

  unit-l : ∀ x → μ (pt X) x == x
  unit-l = fst ⊙unit-l

  unit-r : ∀ x → μ x (pt X) == x
  unit-r = fst ⊙unit-r

  coh : unit-l (pt X) == unit-r (pt X)
  coh = ! (↓-idf=cst-out (snd ⊙unit-l) ∙ ∙-unit-r _)
      ∙ (↓-idf=cst-out (snd ⊙unit-r) ∙ ∙-unit-r _)

record AlternativeHSpaceStructure {i} (X : Ptd i) : Type i where
  constructor hSpaceStructure
  field
    μ : de⊙ X → de⊙ X → de⊙ X
    unit-l : ∀ x → μ (pt X) x == x
    unit-r : ∀ x → μ x (pt X) == x
    coh : unit-l (pt X) == unit-r (pt X)

  ⊙μ : (X ⊙× X) ⊙→ X
  ⊙μ = uncurry μ , unit-l (pt X)

  ⊙unit-l : ⊙μ ⊙∘ ⊙×-inr X X ⊙∼ ⊙idf X
  ⊙unit-l = unit-l , ↓-idf=cst-in' idp

  ⊙unit-r : ⊙μ ⊙∘ ⊙×-inl X X ⊙∼ ⊙idf X
  ⊙unit-r = unit-r , ↓-idf=cst-in' coh

from-alt-h-space : ∀ {i} {X : Ptd i} → AlternativeHSpaceStructure X → HSpaceStructure X
from-alt-h-space hss = record {AlternativeHSpaceStructure hss}

to-alt-h-space : ∀ {i} {X : Ptd i} → HSpaceStructure X → AlternativeHSpaceStructure X
to-alt-h-space hss = record {HSpaceStructure hss}

module ConnectedHSpace {i} {X : Ptd i} {{_ : is-connected 0 (de⊙ X)}}
  (hX : HSpaceStructure X) where

  open HSpaceStructure hX public

  {-
  Given that [X] is 0-connected, to prove that each [μ x] is an equivalence we
  only need to prove that one of them is. But for [x] = [pt X], [μ x] is the
  identity so we’re done.
  -}

  l-is-equiv : ∀ x → is-equiv (λ y → μ y x)
  l-is-equiv = prop-over-connected {a = pt X}
    (λ x → (is-equiv (λ y → μ y x) , is-equiv-is-prop))
    (transport! is-equiv (λ= unit-r) (idf-is-equiv _))

  r-is-equiv : ∀ x → is-equiv (λ y → μ x y)
  r-is-equiv = prop-over-connected {a = pt X}
    (λ x → (is-equiv (λ y → μ x y) , is-equiv-is-prop))
    (transport! is-equiv (λ= unit-l) (idf-is-equiv _))

  l-equiv : de⊙ X → de⊙ X ≃ de⊙ X
  l-equiv x = _ , l-is-equiv x

  r-equiv : de⊙ X → de⊙ X ≃ de⊙ X
  r-equiv x = _ , r-is-equiv x


text:
module Examples where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Bool : Set where
  true  : Bool
  false : Bool

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

not : Bool -> Bool
not x = if x then false else true

isZero : Nat -> Bool
isZero zero    = true
isZero (suc _) = false

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

f : (x : Bool) -> F x -> F (not x)
f true n  = isZero n
f false b = if b then zero else suc zero

test : Bool
test = f ? zero


text:
module Foundation.Level0 where
{-
it : ∀ {a} {A : Set a} {{x : A}} → A
it {{x}} = x
{-# INLINE it #-}
-}
private

  module Data where

    data ⊥ : Set where

module _ where

  open import Foundation.Bottom

  open import Foundation.Primitive

  instance isBottom-Data : ∀ {a} → IsBottom Data.⊥ a
  IsBottom.⊥-elim isBottom-Data ()

  instance Bottom-Data : ∀ {a} → Bottom 𝟘 a
  Bottom.⊥ Bottom-Data = Data.⊥
  Bottom.isBottom Bottom-Data = isBottom-Data

open import Agda.Builtin.Equality

module _ where

  open import Foundation.Equivalence

  isEquivalence-Builtin : ∀ {a} {A : Set a} → IsEquivalence {A = A} _≡_
  IsEquivalence.reflexivity isEquivalence-Builtin x = refl
  IsEquivalence.symmetry isEquivalence-Builtin x .x refl = refl
  IsEquivalence.transitivity isEquivalence-Builtin x .x z refl x₂ = x₂

  instance _ = isEquivalence-Builtin

  equivalence-Builtin : ∀ {a} {A : Set a} → Equivalence A a
  Equivalence._≈_ equivalence-Builtin = _≡_

  instance _ = equivalence-Builtin


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

open import Cubical.Algebra.AbGroup.Base public
open import Cubical.Algebra.AbGroup.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Agda.Builtin.Equality

module _ (F : Set₁ → Set₁) where

  f : (B : Set₁) → B ≡ F Set → Set
  f B eq = {!eq!}

-- WAS: splitting on eq produces
--   f .(_ Set) refl = {!!}
-- with unsolved metavariables

-- SHOULD: instead produce
--   f .(F Set) refl = {!!}


text:
{-# OPTIONS --safe #-}
module CF.Syntax.DeBruijn where

open import Level

open import Data.Bool
open import Data.Product
open import Data.Integer
open import Data.List hiding (null)
open import Data.List.Relation.Unary.All
open import Relation.Unary.PredicateTransformer using (Pt)
open import Relation.Unary hiding (_⊢_)
open import Relation.Binary.Structures using (IsPreorder)
open import Relation.Binary.PropositionalEquality using (isEquivalence)

open import CF.Types
open import CF.Contexts.Lexical using (Ctx; module DeBruijn; Closed) public
open import CF.Syntax using (BinOp; module BinOp) public

open DeBruijn public
open BinOp    public

mutual
  data Exp : Ty → Pred Ctx 0ℓ where
    unit       : ∀[ Exp void ]
    num        : ℤ    → ∀[ Exp int ]
    bool       : Bool → ∀[ Exp bool ]
    ifthenelse : ∀[ Exp bool ⇒ Exp a ⇒ Exp a ⇒ Exp a ]
    var'       : ∀[ Var a ⇒ Exp a ]
    bop        : BinOp a b c → ∀[ Exp a ⇒ Exp b ⇒ Exp c ]

  Exps = λ as Γ → All (λ a → Exp a Γ) as

mutual
  data Stmt (r : Ty) : Pred Ctx 0ℓ where
    asgn          : ∀[ Var a ⇒ Exp a ⇒ Stmt r ]

    run           : ∀[ Exp a ⇒ Stmt r ]

    ifthenelse    : ∀[ Exp bool ⇒ Stmt r ⇒ Stmt r ⇒ Stmt r ]
    while         : ∀[ Exp bool ⇒ Stmt r ⇒ Stmt r ]
    block         : ∀[ Block r  ⇒ Stmt r ]

  data Block (r : Ty) : Pred Ctx 0ℓ where
    _⍮⍮_  : ∀[ Stmt r ⇒ Block r ⇒ Block r ]
    nil   : ∀[ Block r ]


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors
------------------------------------------------------------------------

-- This implementation is designed for reasoning about dynamic
-- vectors which may increase or decrease in size.

-- See `Data.Vec.Functional` for an alternative implementation as
-- functions from finite sets, which is more suitable for reasoning
-- about fixed sized vectors and for when ease of retrevial is
-- important.

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

module Data.Vec where

open import Level
open import Data.Bool.Base
import Data.Nat.Properties as ℕₚ
open import Data.Vec.Bounded.Base as Vec≤
  using (Vec≤; ≤-cast; fromVec)
open import Relation.Nullary
open import Relation.Unary

private
  variable
    a p : Level
    A : Set a

------------------------------------------------------------------------
-- Publicly re-export the contents of the base module

open import Data.Vec.Base public

------------------------------------------------------------------------
-- Additional operations

module _ {P : A → Set p} (P? : Decidable P) where

  filter : ∀ {n} → Vec A n → Vec≤ A n
  filter []       = Vec≤.[]
  filter (a ∷ as) with does (P? a)
  ... | true  = a Vec≤.∷ filter as
  ... | false = ≤-cast (ℕₚ.n≤1+n _) (filter as)

  takeWhile : ∀ {n} → Vec A n → Vec≤ A n
  takeWhile []       = Vec≤.[]
  takeWhile (a ∷ as) with does (P? a)
  ... | true  = a Vec≤.∷ takeWhile as
  ... | false = Vec≤.[]

  dropWhile : ∀ {n} → Vec A n → Vec≤ A n
  dropWhile Vec.[]       = Vec≤.[]
  dropWhile (a Vec.∷ as) with does (P? a)
  ... | true  = ≤-cast (ℕₚ.n≤1+n _) (dropWhile as)
  ... | false = fromVec (a Vec.∷ as)


text:
open import parse-tree
open import string

module run (ptr : ParseTreeRec)  where

open import lib
open import datatypes

open ParseTreeRec ptr

module deriv where
  data RunElement : 𝕃 char → Set where
    Id : string → RunElement []
    InputChar : (c : char) → RunElement (c :: [])
    ParseTree : {l : 𝕃 char}{s : string}{pt : ParseTreeT} → isParseTree pt l s → RunElement l

  infixr 6 _::'_

  data Run : (ls : 𝕃 char) → Set where
    []' : Run []
    _::'_ : {lc elc : 𝕃 char} → RunElement elc → Run lc → Run (elc ++ lc)

  length-run : {lc : 𝕃 char} → Run lc → ℕ
  length-run []' = 0
  length-run (x ::' xs) = suc (length-run xs)

  RunElement-to-string : {lc : 𝕃 char} → RunElement lc → string
  RunElement-to-string (Id s) = ("id:" ^ s)
  RunElement-to-string (InputChar c) = "#" ^ (char-to-string c)
  RunElement-to-string (ParseTree{pt = pt} ipt) = (ParseTreeToString pt)

  Run-to-string : {lc : 𝕃 char} → Run lc → string
  Run-to-string []' = "\n"
  Run-to-string (e ::' r) =  (RunElement-to-string e) ^ " " ^ (Run-to-string r)

  assocRun : (ls : 𝕃 (𝕃 char))(lc : 𝕃 char) → Run ((concat ls) ++ lc) × ℕ → Run (foldr _++_ lc ls) × ℕ
  assocRun ls lc (r , n) rewrite concat-foldr ls lc = r , n

  record rewriteRules : Set where
    field
      len-dec-rewrite : {lc : 𝕃 char} → (r : Run lc) → maybe (Run lc × ℕ) --(λ r' → length-run r' < length-run r ≡ tt))

module noderiv where

  data RunElement : Set where
    Id : string → RunElement
    InputChar : (c : char) → RunElement
    ParseTree : ParseTreeT → RunElement
    Posinfo : ℕ → RunElement

  Run : Set
  Run = 𝕃 RunElement

  _::'_ : RunElement → Run → Run
  _::'_ = _::_

  []' : Run
  []' = []

  length-run : Run → ℕ
  length-run = length

  RunElement-to-string : RunElement → string
  RunElement-to-string (Id s) = ("id:" ^ s)
  RunElement-to-string (InputChar c) = "#" ^ (char-to-string c)
  RunElement-to-string (ParseTree pt) = (ParseTreeToString pt)
  RunElement-to-string (Posinfo n) = "pos:" ^ ℕ-to-string n

  Run-to-string : Run → string
  Run-to-string [] = "\n"
  Run-to-string (e :: r) =  (RunElement-to-string e) ^ " " ^ (Run-to-string r)

  record rewriteRules : Set where
    field
      len-dec-rewrite : Run → maybe (Run × ℕ)

empty-string : string
empty-string = ""

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
------------------------------------------------------------------------------
-- Miscellaneous properties
------------------------------------------------------------------------------

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

module FOTC.Program.SortList.Properties.MiscellaneousATP where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Bool
open import FOTC.Data.Bool.PropertiesATP
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.List.PropertiesATP
open import FOTC.Data.Nat.List.Type
open import FOTC.Data.Nat.Type
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesATP
open import FOTC.Program.SortList.Properties.Totality.BoolATP
open import FOTC.Program.SortList.SortList

------------------------------------------------------------------------------
-- This is a weird result but recall that "the relation ≤ between
-- lists is only an ordering if nil is excluded" (Burstall 1969,
-- p. 46).
-- xs≤[] : ∀ {is} → ListN is → OrdList is → ≤-Lists is []
-- xs≤[] nilLN                     _       = ≤-Lists-[] []
-- xs≤[] (lncons {i} {is} Ni LNis) LOconsL =
--   prf $ xs≤[] LNis (subList-OrdList Ni LNis LOconsL)
--   where
--     postulate prf : ≤-Lists is [] →  --IH.
--                     ≤-Lists (i ∷ is) []
--     {-# ATP prove prf ≤-ItemList-Bool ordList-Bool x&&y≡true→x≡true #-}

x≤ys→x≤zs→x≤ys++zs : ∀ {i js ks} → N i → ListN js → ListN ks →
                     ≤-ItemList i js →
                     ≤-ItemList i ks →
                     ≤-ItemList i (js ++ ks)
x≤ys→x≤zs→x≤ys++zs {i} {ks = ks} Ni lnnil LNks _ i≤k =
  subst (≤-ItemList i) (sym (++-leftIdentity ks)) i≤k
x≤ys→x≤zs→x≤ys++zs {i} {ks = ks} Ni (lncons {j} {js} Nj LNjs) LNks i≤j∷js i≤k =
  prf (x≤ys→x≤zs→x≤ys++zs Ni LNjs LNks (&&-list₂-t₂ helper₁ helper₂ helper₃) i≤k)
  where
  helper₁ : Bool (le i j)
  helper₁ = le-Bool Ni Nj

  helper₂ : Bool (le-ItemList i js)
  helper₂ = le-ItemList-Bool Ni LNjs

  helper₃ : le i j && le-ItemList i js ≡ true
  helper₃ = trans (sym (le-ItemList-∷ i j js)) i≤j∷js

  postulate prf : ≤-ItemList i (js ++ ks) → ≤-ItemList i ((j ∷ js) ++ ks)
  {-# ATP prove prf &&-list₂-t helper₁ helper₂ helper₃ #-}

xs≤ys→xs≤zs→xs≤ys++zs : ∀ {is js ks} → ListN is → ListN js → ListN ks →
                        ≤-Lists is js →
                        ≤-Lists is ks →
                        ≤-Lists is (js ++ ks)
xs≤ys→xs≤zs→xs≤ys++zs lnnil LNjs LNks _ _ = le-Lists-[] _
xs≤ys→xs≤zs→xs≤ys++zs {js = js} {ks} (lncons {i} {is} Ni LNis)
                      LNjs LNks i∷is≤js i∷is≤ks =
  prf ((xs≤ys→xs≤zs→xs≤ys++zs LNis LNjs LNks
                              (&&-list₂-t₂ helper₁ helper₂ helper₃)
                              (&&-list₂-t₂ helper₄ helper₅ helper₆)))
  where
  helper₁ = le-ItemList-Bool Ni LNjs
  helper₂ = le-Lists-Bool LNis LNjs
  helper₃ = trans (sym (le-Lists-∷ i is js)) i∷is≤js

  helper₄ = le-ItemList-Bool Ni LNks
  helper₅ = le-Lists-Bool LNis LNks
  helper₆ = trans (sym (le-Lists-∷ i is ks)) i∷is≤ks

  postulate prf : ≤-Lists is (js ++ ks) → ≤-Lists (i ∷ is) (js ++ ks)
  {-# ATP prove prf x≤ys→x≤zs→x≤ys++zs &&-list₂-t helper₁ helper₂ helper₃ helper₄ helper₅ helper₆ #-}

xs≤zs→ys≤zs→xs++ys≤zs : ∀ {is js ks} → ListN is → ListN js → ListN ks →
                        ≤-Lists is ks →
                        ≤-Lists js ks →
                        ≤-Lists (is ++ js) ks
xs≤zs→ys≤zs→xs++ys≤zs {js = js} {ks} lnnil LNjs LNks is≤ks js≤ks =
  subst (λ t → ≤-Lists t ks)
        (sym (++-leftIdentity js))
        js≤ks
xs≤zs→ys≤zs→xs++ys≤zs {js = js} {ks}
                      (lncons {i} {is} Ni LNis) LNjs LNks i∷is≤ks js≤ks =
  prf (xs≤zs→ys≤zs→xs++ys≤zs LNis LNjs LNks
                             (&&-list₂-t₂ helper₁ helper₂ helper₃)
                             js≤ks)
  where
  helper₁ = le-ItemList-Bool Ni LNks
  helper₂ = le-Lists-Bool LNis LNks
  helper₃ = trans (sym (le-Lists-∷ i is ks)) i∷is≤ks

  postulate prf : ≤-Lists (is ++ js) ks → ≤-Lists ((i ∷ is) ++ js) ks
  {-# ATP prove prf &&-list₂-t helper₁ helper₂ helper₃ #-}

------------------------------------------------------------------------------
-- References
--
-- Burstall, R. M. (1969). Proving properties of programs by
-- structural induction. The Computer Journal 12.1, pp. 41–48.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- Examples/exercises related to CCS from "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi
--
-- Implemented using coinductive definitions of strong and weak
-- bisimilarity and expansion.
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude hiding (module W; step-→)

module Bisimilarity.Weak.CCS.Examples {ℓ} {Name : Type ℓ} where

open import Equality.Propositional

open import Function-universe equality-with-J hiding (id; _∘_)

open import Bisimilarity.CCS
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.Weak.CCS as WL
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
import Expansion.CCS as EL
import Expansion.Equational-reasoning-instances
open import Labelled-transition-system.CCS Name

open import Bisimilarity CCS using (_∼_; ∼:_)
open import Bisimilarity.Weak CCS as W
open import Expansion CCS as E
import Labelled-transition-system.Equational-reasoning-instances CCS
  as Dummy

mutual

  -- Example 6.5.4.

  6-5-4 :
    ∀ {i a b} →
    [ i ] ! name a ∙ (b ∙) ∣ ! co a ∙ ≈ (! a ∙ ∣ ! b ∙) ∣ ! co a ∙
  6-5-4 {i} {a} {b} = W.⟨ lr , rl ⟩
    where
    lemma =
      (! a ∙ ∣ ! b ∙) ∣ b ∙  ∼⟨ symmetric ∣-assoc ⟩
      ! a ∙ ∣ (! b ∙ ∣ b ∙)  ∼⟨ symmetric ∣-right-identity ∣-cong 6-1-2 ⟩■
      (! a ∙ ∣ ∅) ∣ ! b ∙

    lr :
      ∀ {P μ} →
      ! name a ∙ (b ∙) ∣ ! co a ∙ [ μ ]⟶ P →
      ∃ λ Q → (! a ∙ ∣ ! b ∙) ∣ ! co a ∙ [ μ ]⇒̂ Q × [ i ] P ≈′ Q
    lr (par-left {P′ = P} tr) = case 6-1-3-2 tr of λ where
      (inj₁ (.(b ∙) , action , P∼!ab∣b)) →
        P ∣ ! co a ∙                         ∼⟨ P∼!ab∣b ∣-cong reflexive ⟩
        (! name a ∙ (b ∙) ∣ b ∙) ∣ ! co a ∙  ∼⟨ swap-rightmost ⟩
        (! name a ∙ (b ∙) ∣ ! co a ∙) ∣ b ∙  ∼′⟨ 6-5-4′ WL.∣-cong′ reflexive ⟩
        ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙) ∣ b ∙   ∼⟨ swap-rightmost ⟩ ∼:
        ((! a ∙ ∣ ! b ∙) ∣ b ∙) ∣ ! co a ∙   ∼⟨ lemma ∣-cong reflexive ⟩■
        ((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ ! co a ∙
          W.⇐̂[ name a ]                      ←⟨ ⟶: par-left (par-left (replication (par-right action))) ⟩■
        (! a ∙ ∣ ! b ∙) ∣ ! co a ∙

      (inj₂ (_ , .(b ∙) , _ , .a , action , ab[a̅]⟶ , _)) →
        ⊥-elim (names-are-not-inverted ab[a̅]⟶)

    lr (par-right {Q′ = Q} tr) = case 6-1-3-2 tr of λ where
      (inj₁ (.∅ , action , Q∼!a̅∣∅)) →
        ! name a ∙ (b ∙) ∣ Q               ∼⟨ reflexive ∣-cong Q∼!a̅∣∅ ⟩
        ! name a ∙ (b ∙) ∣ (! co a ∙ ∣ ∅)  ∼⟨ ∣-assoc ⟩
        (! name a ∙ (b ∙) ∣ ! co a ∙) ∣ ∅  ∼′⟨ 6-5-4′ WL.∣-cong′ reflexive ⟩ ∼:
        ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙) ∣ ∅   ∼⟨ symmetric ∣-assoc ⟩■
        (! a ∙ ∣ ! b ∙) ∣ (! co a ∙ ∣ ∅)
          W.⇐̂[ name (co a) ]               ←⟨ ⟶: par-right (replication (par-right action)) ⟩■
        (! a ∙ ∣ ! b ∙) ∣ ! co a ∙

      (inj₂ (_ , .∅ , _ , .(co a) , action , a̅[a̅̅]⟶ , _)) →
        ⊥-elim (names-are-not-inverted a̅[a̅̅]⟶)

    lr (par-τ {P′ = P} {Q′ = Q} tr₁ tr₂) =
      case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
        (inj₁ (.(b ∙) , action , P∼!ab∣b) ,
         inj₁ (R      , tr     , Q∼!a̅∣R)) →
          P ∣ Q                                      ∼⟨ P∼!ab∣b ∣-cong Q∼!a̅∣R ⟩
          (! name a ∙ (b ∙) ∣ b ∙) ∣ (! co a ∙ ∣ R)  ∼≡⟨ cong (λ R → _ ∣ (_ ∣ R)) (·-only⟶ tr) ⟩
          (! name a ∙ (b ∙) ∣ b ∙) ∣ (! co a ∙ ∣ ∅)  ∼⟨ swap-in-the-middle ⟩
          (! name a ∙ (b ∙) ∣ ! co a ∙) ∣ (b ∙ ∣ ∅)  ∼′⟨ 6-5-4′ WL.∣-cong′ reflexive ⟩
          ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙) ∣ (b ∙ ∣ ∅)   ∼⟨ swap-in-the-middle ⟩ ∼:
          ((! a ∙ ∣ ! b ∙) ∣ b ∙) ∣ (! co a ∙ ∣ ∅)   ∼⟨ lemma ∣-cong reflexive ⟩■
          ((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ (! co a ∙ ∣ ∅)
            W.⇐̂[ τ ]                                 ←⟨ par-τ (par-left (replication (par-right action)))
                                                              (replication (par-right action)) ⟩■
          (! a ∙ ∣ ! b ∙) ∣ ! co a ∙

        (_ , inj₂ (() , _))
        (inj₂ (() , _) , _)

    rl-lemma :
      ∀ {Q μ} →
      (! a ∙ ∣ ! b ∙) ∣ ! co a ∙ [ μ ]⟶ Q →
      (! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼ Q
        ×
      (μ ≡ name a ⊎ μ ≡ name b ⊎ μ ≡ name (co a) ⊎ μ ≡ τ)
    rl-lemma (par-left (par-left {P′ = P} tr)) =
      case 6-1-3-2 tr of λ where
        (inj₁ (.∅ , action , P∼!a∣∅)) →
            ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙        ∼⟨ (symmetric ∣-right-identity ∣-cong reflexive) ∣-cong reflexive ⟩
             ((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ ! co a ∙  ∼⟨ (symmetric P∼!a∣∅ ∣-cong reflexive) ∣-cong reflexive ⟩■
             (P ∣ ! b ∙) ∣ ! co a ∙)
          , inj₁ refl

        (inj₂ (refl , .∅ , _ , .a , action , a[a̅]⟶ , _)) →
          ⊥-elim (names-are-not-inverted a[a̅]⟶)

    rl-lemma (par-left (par-right {Q′ = P} tr)) =
      case 6-1-3-2 tr of λ where
        (inj₁ (.∅ , action , P∼!b∣∅)) →
            ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙        ∼⟨ (reflexive ∣-cong symmetric ∣-right-identity) ∣-cong reflexive ⟩
             (! a ∙ ∣ (! b ∙ ∣ ∅)) ∣ ! co a ∙  ∼⟨ (reflexive ∣-cong symmetric P∼!b∣∅) ∣-cong reflexive ⟩■
             (! a ∙ ∣ P) ∣ ! co a ∙)
          , inj₂ (inj₁ refl)

        (inj₂ (_ , .∅ , _ , .b , action , b[b̅]⟶ , _)) →
          ⊥-elim (names-are-not-inverted b[b̅]⟶)

    rl-lemma (par-left (par-τ {P′ = P} {Q′ = Q} tr₁ tr₂)) =
      case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
        (inj₁ (.∅ , action , P∼!a∣∅) ,
         inj₁ (.∅ , action , Q∼!b∣∅)) →
            ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙              ∼⟨ symmetric (∣-right-identity ∣-cong ∣-right-identity) ∣-cong reflexive ⟩
             ((! a ∙ ∣ ∅) ∣ (! b ∙ ∣ ∅)) ∣ ! co a ∙  ∼⟨ symmetric (P∼!a∣∅ ∣-cong Q∼!b∣∅) ∣-cong reflexive ⟩■
             (P ∣ Q) ∣ ! co a ∙)
          , inj₂ (inj₂ (inj₂ refl))

        (inj₂ (() , _) , _)
        (_ , inj₂ (() , _))

    rl-lemma (par-right {Q′ = Q} tr) =
      case 6-1-3-2 tr of λ where
        (inj₁ (.∅ , action , Q∼!a̅∣∅)) →
            ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙        ∼⟨ reflexive ∣-cong symmetric ∣-right-identity ⟩
             (! a ∙ ∣ ! b ∙) ∣ (! co a ∙ ∣ ∅)  ∼⟨ reflexive ∣-cong symmetric Q∼!a̅∣∅ ⟩■
             (! a ∙ ∣ ! b ∙) ∣ Q)
          , inj₂ (inj₂ (inj₁ refl))

        (inj₂ (_ , .∅ , _ , .(co a) , action , a̅[a̅̅]⟶ , _)) →
          ⊥-elim (names-are-not-inverted a̅[a̅̅]⟶)

    rl-lemma (par-τ {Q′ = Q} (par-left {P′ = P} tr₁) tr₂) =
      case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
        (inj₁ (.∅ , action , P∼!a∣∅) ,
         inj₁ (R  , tr     , Q∼!a̅∣R)) →
            ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙              ∼⟨ symmetric ((∣-right-identity ∣-cong reflexive) ∣-cong ∣-right-identity) ⟩
             ((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ (! co a ∙ ∣ ∅)  ∼≡⟨ cong (λ R → _ ∣ (_ ∣ R)) (sym $ ·-only⟶ tr) ⟩
             ((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ (! co a ∙ ∣ R)  ∼⟨ symmetric ((P∼!a∣∅ ∣-cong reflexive) ∣-cong Q∼!a̅∣R) ⟩■
             (P ∣ ! b ∙) ∣ Q)
          , inj₂ (inj₂ (inj₂ refl))

        (inj₂ (() , _) , _)
        (_ , inj₂ (() , _))

    rl-lemma (par-τ {Q′ = Q} (par-right {Q′ = P} tr₁) tr₂) =
      case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
        (inj₁ (.∅ , action , P∼!b∣∅) ,
         inj₁ (R  , tr     , Q∼!a̅∣R)) →
            ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙              ∼⟨ symmetric ((reflexive ∣-cong ∣-right-identity) ∣-cong ∣-right-identity) ⟩
             (! a ∙ ∣ (! b ∙ ∣ ∅)) ∣ (! co a ∙ ∣ ∅)  ∼≡⟨ cong (λ R → _ ∣ (_ ∣ R)) (sym $ ·-only⟶ tr) ⟩
             (! a ∙ ∣ (! b ∙ ∣ ∅)) ∣ (! co a ∙ ∣ R)  ∼⟨ symmetric ((reflexive ∣-cong P∼!b∣∅) ∣-cong Q∼!a̅∣R) ⟩■
             (! a ∙ ∣ P) ∣ Q)
          , inj₂ (inj₂ (inj₂ refl))

        (inj₂ (() , _) , _)
        (_ , inj₂ (() , _))

    rl :
      ∀ {Q μ} →
      (! a ∙ ∣ ! b ∙) ∣ ! co a ∙ [ μ ]⟶ Q →
      ∃ λ P → ! name a ∙ (b ∙) ∣ ! co a ∙ [ μ ]⇒̂ P × [ i ] P ≈′ Q
    rl {Q} tr = case rl-lemma tr of λ where
      (!a∣!b∣!a̅∼Q , inj₁ refl) →
        ! name a ∙ (b ∙) ∣ ! co a ∙          →⟨ ⟶: par-left (replication (par-right action)) ⟩■
          W.⇒̂[ name a ]
        (! name a ∙ (b ∙) ∣ b ∙) ∣ ! co a ∙  ∼⟨ swap-rightmost ⟩
        (! name a ∙ (b ∙) ∣ ! co a ∙) ∣ b ∙  ∼′⟨ 6-5-4′ WL.∣-cong′ reflexive ⟩
        ((! a ∙ ∣ ! b ∙) ∣ ! co a ∙) ∣ b ∙   ∼⟨ swap-rightmost ⟩
        ((! a ∙ ∣ ! b ∙) ∣ b ∙) ∣ ! co a ∙   ∼⟨ symmetric ∣-assoc ∣-cong reflexive ⟩
        (! a ∙ ∣ (! b ∙ ∣ b ∙)) ∣ ! co a ∙   ∼⟨ (reflexive ∣-cong 6-1-2) ∣-cong reflexive ⟩ ∼:
        (! a ∙ ∣ ! b ∙) ∣ ! co a ∙           ∼⟨ !a∣!b∣!a̅∼Q ⟩■
        Q

      (!a∣!b∣!a̅∼Q , inj₂ (inj₁ refl)) →
        ! name a ∙ (b ∙) ∣ ! co a ∙                  →⟨ par-τ (replication (par-right action))
                                                              (replication (par-right action)) ⟩
        (! name a ∙ (b ∙) ∣ (b ∙)) ∣ (! co a ∙ ∣ ∅)  →⟨ ⟶: par-left (par-right action) ⟩■
          W.⇒̂[ name b ]
        (! name a ∙ (b ∙) ∣ ∅) ∣ (! co a ∙ ∣ ∅)      ∼⟨ ∣-right-identity ∣-cong ∣-right-identity ⟩
        (! name a ∙ (b ∙)) ∣ ! co a ∙                ∼′⟨ 6-5-4′ ⟩ ∼:
        (! a ∙ ∣ ! b ∙) ∣ ! co a ∙                   ∼⟨ !a∣!b∣!a̅∼Q ⟩■
        Q

      (!a∣!b∣!a̅∼Q , inj₂ (inj₂ (inj₁ refl))) →
        ! name a ∙ (b ∙) ∣ ! co a ∙        →⟨ ⟶: par-right (replication (par-right action)) ⟩■
          W.⇒̂[ name (co a) ]
        ! name a ∙ (b ∙) ∣ (! co a ∙ ∣ ∅)  ∼⟨ reflexive ∣-cong ∣-right-identity ⟩
        ! name a ∙ (b ∙) ∣ ! co a ∙        ∼′⟨ 6-5-4′ ⟩ ∼:
        (! a ∙ ∣ ! b ∙) ∣ ! co a ∙         ∼⟨ !a∣!b∣!a̅∼Q ⟩■
        Q

      (!a∣!b∣!a̅∼Q , inj₂ (inj₂ (inj₂ refl))) →
        ! name a ∙ (b ∙) ∣ ! co a ∙  ■
          W.⇒̂[ τ ]
        ! name a ∙ (b ∙) ∣ ! co a ∙  ∼′⟨ 6-5-4′ ⟩ ∼:
        (! a ∙ ∣ ! b ∙) ∣ ! co a ∙   ∼⟨ !a∣!b∣!a̅∼Q ⟩■
        Q

  6-5-4′ :
    ∀ {i a b} →
    [ i ] ! name a ∙ (b ∙) ∣ ! co a ∙ ≈′ (! a ∙ ∣ ! b ∙) ∣ ! co a ∙
  force 6-5-4′ = 6-5-4

-- The first part of Exercise 6.5.8.

6-5-8-1 :
  ∀ a {P Q} →
  ⟨ν proj₁ a ⟩ (name a ∙ P ∣ name (co a) ∙ Q) ≳ ⟨ν proj₁ a ⟩ (P ∣ Q)
6-5-8-1 a {P} {Q} = E.⟨ lr , rl ⟩
  where
  lr :
    ∀ {μ R} →
    ⟨ν proj₁ a ⟩ (name a ∙ P ∣ name (co a) ∙ Q) [ μ ]⟶ R →
    ∃ λ R′ → ⟨ν proj₁ a ⟩ (P ∣ Q) [ μ ]⟶̂ R′ × R ≳′ R′
  lr (restriction a∉μ (par-left action))          = ⊥-elim (a∉μ refl)
  lr (restriction a∉μ (par-right action))         = ⊥-elim (a∉μ refl)
  lr (restriction a∉μ (par-τ {Q′ = R} action tr)) =
    ⟨ν proj₁ a ⟩ (P ∣ R)  ∼≡⟨ cong (λ R → ⟨ν _ ⟩ (_ ∣ R)) (·-only⟶ tr) ⟩■
    ⟨ν proj₁ a ⟩ (P ∣ Q)
      ⟵̂[ τ ]
    ⟨ν proj₁ a ⟩ (P ∣ Q)  ■

  rl :
    ∀ {μ R′} →
    ⟨ν proj₁ a ⟩ (P ∣ Q) [ μ ]⟶ R′ →
    ∃ λ R → ⟨ν proj₁ a ⟩ (name a ∙ P ∣ name (co a) ∙ Q) [ μ ]⇒ R ×
            R ≳′ R′
  rl {μ} (restriction {P′ = R} a∉μ P∣Q⟶R) =
    ⟨ν proj₁ a ⟩ (name a ∙ P ∣ name (co a) ∙ Q)  →⟨ ⟶: restriction _ (par-τ action action) ⟩
    ⟨ν proj₁ a ⟩ (P ∣ Q)                         →⟨ ⟶: restriction a∉μ P∣Q⟶R ⟩■
      E.⇒[ μ ]
    ⟨ν proj₁ a ⟩ R                               ■

-- One interpretation of the second part of Exercise 6.5.8 is
-- contradictory, assuming that Name is inhabited.

¬-6-5-8-2 :
  Name →
  ¬ (∀ {a b P} →
     ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ≈
     ! name b ∙ ⟨ν proj₁ a ⟩ P)
¬-6-5-8-2 x =
  (∀ {a b P} →
   ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ≈
   ! name b ∙ ⟨ν proj₁ a ⟩ P)                                          ↝⟨ (λ hyp → hyp {a = a} {b = co a}) ⟩

  (! ⟨ν proj₁ a ⟩ (name (co a) ∙ (a ∙) ∣ co a ∙) ≈
   ! name (co a) ∙ ⟨ν proj₁ a ⟩ ∅)                                     ↝⟨ (λ hyp → Σ-map id proj₁ $ W.right-to-left hyp
                                                                                (replication (par-right action))) ⟩
  ∃ (! ⟨ν proj₁ a ⟩ (name (co a) ∙ (a ∙) ∣ co a ∙) [ name (co a) ]⇒̂_)  ↝⟨ !P⇒̂ ∘ proj₂ ⟩□

  ⊥                                                                    □
  where
  a = x , true

  P = ⟨ν proj₁ a ⟩ (name (co a) ∙ (a ∙) ∣ co a ∙)

  P⟶ : ∀ {μ Q} → ¬ P [ μ ]⟶ Q
  P⟶ (restriction x≢x (par-left action))  = ⊥-elim (x≢x refl)
  P⟶ (restriction x≢x (par-right action)) = ⊥-elim (x≢x refl)
  P⟶ (restriction _   (par-τ action tr))  = names-are-not-inverted tr

  !P⟶ : ∀ {μ Q} → ¬ ! P [ μ ]⟶ Q
  !P⟶ (replication (par-left tr))  = !P⟶ tr
  !P⟶ (replication (par-right tr)) = P⟶ tr
  !P⟶ (replication (par-τ _ tr))   = P⟶ tr

  !P⇒ : ∀ {Q} → ! P ⇒ Q → Q ≡ ! P
  !P⇒ done          = refl
  !P⇒ (step _ tr _) = ⊥-elim (!P⟶ tr)

  !P[]⇒ : ∀ {μ Q} → ¬ ! P [ μ ]⇒ Q
  !P[]⇒ (steps trs tr _) rewrite !P⇒ trs = !P⟶ tr

  !P⇒̂ : ∀ {b Q} → ¬ ! P [ name b ]⇒̂ Q
  !P⇒̂ (silent () _)
  !P⇒̂ (non-silent _ tr) = !P[]⇒ tr

-- Another interpretation of the second part of Exercise 6.5.8 can be
-- proved.

6-5-8-2 :
  ∀ {i a b P} →
  proj₁ a ≢ proj₁ b →
  [ i ] ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ≈
        ! name b ∙ ⟨ν proj₁ a ⟩ P
6-5-8-2 {i} {a} {b} {P} a≢b = W.⟨ lr , rl ⟩
  where
  6-5-8-2′ :
    [ i ] ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ≈′
          ! name b ∙ ⟨ν proj₁ a ⟩ P
  force 6-5-8-2′ = 6-5-8-2 a≢b

  lr :
    ∀ {Q μ} →
    ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) [ μ ]⟶ Q →
    ∃ λ Q′ → ! name b ∙ ⟨ν proj₁ a ⟩ P [ μ ]⇒̂ Q′ × [ i ] Q ≈′ Q′
  lr {Q} tr = case 6-1-3-2 tr of λ where
    (inj₁ (_ , restriction a≢b (par-left action)
             , Q∼!νa[ba∣a̅P]∣νa[a∣a̅P])) →
      Q                                                    ∼⟨ Q∼!νa[ba∣a̅P]∣νa[a∣a̅P] ⟩

      ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ∣
      ⟨ν proj₁ a ⟩ (a ∙ ∣ name (co a) ∙ P)                 ∼⟨ (_ ■) EL.∣-cong 6-5-8-1 _ ⟩

      ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ∣
      ⟨ν proj₁ a ⟩ (∅ ∣ P)                                 ∼⟨ 6-5-8-2′ WL.∣-cong′ convert {a = ℓ} (⟨ν refl ⟩-cong ∣-left-identity) ⟩■

      ! name b ∙ ⟨ν proj₁ a ⟩ P ∣ ⟨ν proj₁ a ⟩ P

        W.⇐̂[ name b ]                                      ←⟨ ⟶: replication (par-right action) ⟩■

      ! name b ∙ ⟨ν proj₁ a ⟩ P

    (inj₁ (_ , restriction _ (par-τ action tr) , _)) →
      ⊥-elim (                              $⟨ tr ⟩
        name (co a) · _ [ name (co b) ]⟶ _  ↝⟨ ·-only ⟩
        name (co a) ≡ name (co b)           ↝⟨ cancel-name ⟩
        co a ≡ co b                         ↝⟨ cong proj₁ ⟩
        proj₁ a ≡ proj₁ b                   ↝⟨ a≢b ⟩□
        ⊥                                   □)

    (inj₁ (_ , restriction a≢a (par-right action) , _)) →
      ⊥-elim (a≢a refl)

    (inj₂ (refl , _ , _ , _
                , restriction _ (par-left action)
                , restriction _ (par-left tr)
                , _)) →
      ⊥-elim (names-are-not-inverted tr)

    (inj₂ (refl , _ , _ , _
                , restriction _ (par-right action)
                , restriction _ (par-right tr)
                , _)) →
      ⊥-elim (names-are-not-inverted tr)

    (inj₂ (refl , _ , _ , _
                , restriction a≢b (par-left action)
                , restriction _   (par-right tr)
                , _)) →
                                          $⟨ tr ⟩
      name (co a) ∙ P [ name (co b) ]⟶ _  ↝⟨ cong proj₁ ∘ cancel-name ∘ ·-only ⟩
      proj₁ a ≡ proj₁ b                   ↝⟨ a≢b ⟩
      ⊥                                   ↝⟨ ⊥-elim ⟩□
      _                                   □

    (inj₂ (refl , _ , _ , c
                , restriction a≢c (par-right tr)
                , restriction _   (par-left action)
                , _)) →
                                     $⟨ tr ⟩
      name (co a) ∙ P [ name c ]⟶ _  ↝⟨ cong proj₁ ∘ cancel-name ∘ ·-only ⟩
      proj₁ a ≡ proj₁ c              ↝⟨ a≢c ⟩
      ⊥                              ↝⟨ ⊥-elim ⟩□
      _                              □

  rl :
    ∀ {Q′ μ} →
    ! name b ∙ ⟨ν proj₁ a ⟩ P [ μ ]⟶ Q′ →
    ∃ λ Q → ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) [ μ ]⇒̂ Q ×
            [ i ] Q ≈′ Q′
  rl {Q′} tr = case 6-1-3-2 tr of λ where
    (inj₁ (_ , action , Q′∼!bνaP∣νaP)) →
      ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P)    →⟨ ⟶: replication (par-right (restriction a≢b (par-left action))) ⟩■

        W.⇒̂[ name b ]

      ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ∣
      ⟨ν proj₁ a ⟩ (a ∙ ∣ name (co a) ∙ P)                 ∼′⟨ 6-5-8-2′ WL.∣-cong′ convert {a = ℓ} (6-5-8-1 a) ⟩

      ! name b ∙ ⟨ν proj₁ a ⟩ P ∣ ⟨ν proj₁ a ⟩ (∅ ∣ P)     ∼⟨ (_ ■) ∣-cong ⟨ν refl ⟩-cong ∣-left-identity ⟩ ∼:

      ! name b ∙ ⟨ν proj₁ a ⟩ P ∣ ⟨ν proj₁ a ⟩ P           ∼⟨ symmetric Q′∼!bνaP∣νaP ⟩■

      Q′

    (inj₂ (refl , _ , _ , _ , action , tr , _)) →
      ⊥-elim (names-are-not-inverted tr)

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


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

open import HoTT
open import homotopy.elims.CofPushoutSection

module cohomology.MayerVietoris {i} where

{- Mayer-Vietoris Sequence: Given a span X ←f– Z –g→ Y, the cofiber space
   of the natural map [reglue : X ∨ Y → X ⊔_Z Y] (defined below) is equivalent
   to the suspension of Z. -}

{- Relevant functions -}
module MayerVietorisFunctions (ps : ⊙Span {i} {i} {i}) where

  open ⊙Span ps

  module Reglue = ⊙WedgeRec (⊙left ps) (⊙right ps)

  reglue : X ∨ Y → de⊙ (⊙Pushout ps)
  reglue = Reglue.f

  ⊙reglue : X ⊙∨ Y ⊙→ ⊙Pushout ps
  ⊙reglue = Reglue.⊙f

  module MVDiff = SuspRec {C = Susp (X ∨ Y)}
    north
    north
    (λ z → merid (winl (fst f z)) ∙ ! (merid (winr (fst g z))))

  mv-diff : Susp (de⊙ Z) → Susp (X ∨ Y)
  mv-diff = MVDiff.f

  ⊙mv-diff : ⊙Susp Z ⊙→ ⊙Susp (X ⊙∨ Y)
  ⊙mv-diff = (mv-diff , idp)

{- We use path induction (via [⊙pushout-J]) to assume that the
   basepoint preservation paths of the span maps are [idp]. The module
   [MayerVietorisBase] contains the proof of the theorem for this case. -}
module MayerVietorisBase
  {A B : Type i} (Z : Ptd i) (f : de⊙ Z → A) (g : de⊙ Z → B) where

  X = ⊙[ A , f (pt Z) ]
  Y = ⊙[ B , g (pt Z) ]
  ps = ⊙span X Y Z (f , idp) (g , idp)
  F : Z ⊙→ X
  F = (f , idp)
  G : Z ⊙→ Y
  G = (g , idp)

  open MayerVietorisFunctions ps

  {- Definition of the maps
       into : Cofiber reglue → ΣZ
       out  : ΣZ → Cofiber reglue
   -}

  private
    into-glue-square :
      Square idp idp (ap (extract-glue ∘ reglue) wglue) (merid (pt Z))
    into-glue-square =
      connection ⊡v∙
      ! (ap-∘ extract-glue reglue wglue
         ∙ ap (ap extract-glue) (Reglue.glue-β ∙ !-! (glue (pt Z)))
         ∙ ExtractGlue.glue-β (pt Z))

    module IntoGlue = WedgeElim {P = λ xy → north == extract-glue (reglue xy)}
      (λ _ → idp)
      (λ _ → merid (pt Z))
      (↓-cst=app-from-square into-glue-square)

    into-glue = IntoGlue.f

  module Into = CofiberRec {f = reglue} north extract-glue into-glue

  private
    out-glue-and-square : (z : de⊙ Z)
      → Σ (cfbase' reglue == cfbase' reglue)
          (λ p → Square (cfglue (winl (f z))) p
                   (ap cfcod (glue z)) (cfglue (winr (g z))))
    out-glue-and-square z = fill-square-top _ _ _

    out-glue = fst ∘ out-glue-and-square
    out-square = snd ∘ out-glue-and-square

  module Out = SuspRec {C = Cofiber reglue}
    cfbase
    cfbase
    out-glue

  into = Into.f
  out = Out.f

  abstract
    {- [out] is a right inverse for [into] -}

    private
      into-out-sq : (z : de⊙ Z) →
        Square idp (ap into (ap out (merid z))) (merid z) (merid (pt Z))
      into-out-sq z =
        (ap (ap into) (Out.merid-β z) ∙v⊡
          (! (Into.glue-β (winl (f z)))) ∙h⊡
            ap-square into (out-square z)
          ⊡h∙ (Into.glue-β (winr (g z))))
        ⊡v∙ (∘-ap into cfcod (glue z) ∙ ExtractGlue.glue-β z)

    into-out : ∀ σ → into (out σ) == σ
    into-out = Susp-elim
      idp
      (merid (pt Z))
      (λ z → ↓-∘=idf-from-square into out (into-out-sq z))

    {- [out] is a left inverse for [into] -}

    {- [out] is left inverse on codomain part of cofiber space,
     - i.e. [out (into (cfcod γ)) == cfcod γ] -}

    private
      out-into-cod-square : (z : de⊙ Z) →
        Square (cfglue' reglue (winl (f z)))
               (ap (out ∘ extract-glue {s = ⊙Span-to-Span ps}) (glue z))
               (ap cfcod (glue z)) (cfglue (winr (g z)))
      out-into-cod-square z =
        (ap-∘ out extract-glue (glue z)
          ∙ ap (ap out) (ExtractGlue.glue-β z) ∙ Out.merid-β z)
        ∙v⊡ out-square z

      module OutIntoCod = PushoutElim
        {d = ⊙Span-to-Span ps} {P = λ γ → out (into (cfcod γ)) == cfcod γ}
        (λ x → cfglue (winl x))
        (λ y → cfglue (winr y))
        (λ z → ↓-='-from-square (out-into-cod-square z))

      out-into-cod = OutIntoCod.f

    out-into : ∀ κ → out (into κ) == κ
    out-into = CofPushoutSection.elim
      (λ _ → unit) (λ _ → idp)
      idp
      out-into-cod
      (↓-='-from-square ∘ λ x →
        (ap-∘ out into (cfglue (winl x))
         ∙ ap (ap out) (Into.glue-β (winl x)))
        ∙v⊡ connection
        ⊡v∙ ! (ap-idf (glue (winl x))))
      (↓-='-from-square ∘ λ y →
        (ap-∘ out into (cfglue (winr y))
         ∙ ap (ap out) (Into.glue-β (winr y))
         ∙ Out.merid-β (pt Z)
         ∙ square-top-unique (out-square (pt Z))
             (! (ap-cst cfbase wglue) ∙v⊡
              natural-square cfglue wglue
              ⊡v∙ (ap-∘ cfcod reglue wglue
                   ∙ ap (ap cfcod) (Reglue.glue-β ∙ !-! (glue (pt Z))))))
        ∙v⊡ connection
        ⊡v∙ ! (ap-idf (glue (winr y))))

  {- equivalence and path -}

  eq : Cofiber reglue ≃ Susp (de⊙ Z)
  eq = equiv into out into-out out-into

  ⊙eq : ⊙Cofiber ⊙reglue ⊙≃ ⊙Susp Z
  ⊙eq = ≃-to-⊙≃ eq idp

  {- Transporting [cfcod reglue] over the equivalence -}

  cfcod-comm-sqr : CommSquare (cfcod' reglue) extract-glue (idf _) into
  cfcod-comm-sqr = comm-sqr λ _ → idp

  {- Transporting [extract-glue] over the equivalence. -}

  ext-comm-sqr : CommSquare extract-glue mv-diff into (idf _)
  ext-comm-sqr = comm-sqr $ ! ∘ fn-lemma
    where
    fn-lemma : ∀ κ → mv-diff (into κ) == extract-glue κ
    fn-lemma = CofPushoutSection.elim
      (λ _ → unit) (λ _ → idp)
      idp
      (Pushout-elim
        (λ x → merid (winl x))
        (λ y → merid (winr y))
        (↓-='-from-square ∘ λ z →
          (ap-∘ mv-diff extract-glue (glue z)
           ∙ ap (ap mv-diff) (ExtractGlue.glue-β z)
           ∙ MVDiff.merid-β z)
          ∙v⊡ (lt-square (merid (winl (f z)))
               ⊡h rt-square (merid (winr (g z))))
          ⊡v∙ ! (ap-cst south (glue z))))
      (↓-='-from-square ∘ λ x →
        (ap-∘ mv-diff into (cfglue (winl x))
         ∙ ap (ap mv-diff) (Into.glue-β (winl x)))
        ∙v⊡ connection
        ⊡v∙ ! (ExtractGlue.glue-β (winl x)))
      (↓-='-from-square ∘ λ y →
        (ap-∘ mv-diff into (cfglue (winr y))
         ∙ ap (ap mv-diff) (Into.glue-β (winr y))
         ∙ MVDiff.merid-β (pt Z)
         ∙ ap (λ w → merid w ∙ ! (merid (winr (g (pt Z))))) wglue
         ∙ !-inv-r (merid (winr (g (pt Z)))))
        ∙v⊡ connection
        ⊡v∙ ! (ExtractGlue.glue-β (winr y)))

{- Main results -}
module MayerVietoris (ps : ⊙Span {i} {i} {i}) where

  private
    record Results (ps : ⊙Span {i} {i} {i}) : Type (lsucc i) where
      open ⊙Span ps
      open MayerVietorisFunctions ps public
      field
        ⊙eq : ⊙Cofiber ⊙reglue ⊙≃ ⊙Susp Z
        cfcod-comm-sqr : CommSquare
          (cfcod' reglue) extract-glue
          (idf _) (fst (⊙–> ⊙eq))
        ext-comm-sqr : CommSquare
          extract-glue mv-diff (fst (⊙–> ⊙eq)) (idf _)

    results : Results ps
    results = ⊙pushout-J Results base-results ps
      where
      base-results : ∀ {A} {B} Z (f : de⊙ Z → A) (g : de⊙ Z → B) →
        Results (⊙span _ _ Z (f , idp) (g , idp))
      base-results Z f g = record {
        ⊙eq = ⊙eq;
        cfcod-comm-sqr = cfcod-comm-sqr;
        ext-comm-sqr = ext-comm-sqr}
        where open MayerVietorisBase Z f g

  open Results results public


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

open import LogicalFormulae
open import Lists.Lists
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Numbers.Naturals.Semiring
open import Numbers.BinaryNaturals.Definition
open import Orders.Partial.Definition
open import Orders.Total.Definition
open import Semirings.Definition

module Numbers.BinaryNaturals.Order where

data Compare : Set where
  Equal : Compare
  FirstLess : Compare
  FirstGreater : Compare

private
  badCompare : Equal ≡ FirstLess → False
  badCompare ()

  badCompare' : Equal ≡ FirstGreater → False
  badCompare' ()

  badCompare'' : FirstLess ≡ FirstGreater → False
  badCompare'' ()

_<BInherited_ : BinNat → BinNat → Compare
a <BInherited b with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
(a <BInherited b) | inl (inl x) = FirstLess
(a <BInherited b) | inl (inr x) = FirstGreater
(a <BInherited b) | inr x = Equal

private
  go<Bcomp : Compare → BinNat → BinNat → Compare
  go<Bcomp Equal [] [] = Equal
  go<Bcomp Equal [] (zero :: b) = go<Bcomp Equal [] b
  go<Bcomp Equal [] (one :: b) = FirstLess
  go<Bcomp Equal (zero :: a) [] = go<Bcomp Equal a []
  go<Bcomp Equal (zero :: a) (zero :: b) = go<Bcomp Equal a b
  go<Bcomp Equal (zero :: a) (one :: b) = go<Bcomp FirstLess a b
  go<Bcomp Equal (one :: a) [] = FirstGreater
  go<Bcomp Equal (one :: a) (zero :: b) = go<Bcomp FirstGreater a b
  go<Bcomp Equal (one :: a) (one :: b) = go<Bcomp Equal a b
  go<Bcomp FirstGreater [] [] = FirstGreater
  go<Bcomp FirstGreater [] (zero :: b) = go<Bcomp FirstGreater [] b
  go<Bcomp FirstGreater [] (one :: b) = FirstLess
  go<Bcomp FirstGreater (zero :: a) [] = FirstGreater
  go<Bcomp FirstGreater (zero :: a) (zero :: b) = go<Bcomp FirstGreater a b
  go<Bcomp FirstGreater (zero :: a) (one :: b) = go<Bcomp FirstLess a b
  go<Bcomp FirstGreater (one :: a) [] = FirstGreater
  go<Bcomp FirstGreater (one :: a) (zero :: b) = go<Bcomp FirstGreater a b
  go<Bcomp FirstGreater (one :: a) (one :: b) = go<Bcomp FirstGreater a b
  go<Bcomp FirstLess [] b = FirstLess
  go<Bcomp FirstLess (zero :: a) [] = go<Bcomp FirstLess a []
  go<Bcomp FirstLess (one :: a) [] = FirstGreater
  go<Bcomp FirstLess (zero :: a) (zero :: b) = go<Bcomp FirstLess a b
  go<Bcomp FirstLess (zero :: a) (one :: b) = go<Bcomp FirstLess a b
  go<Bcomp FirstLess (one :: a) (zero :: b) = go<Bcomp FirstGreater a b
  go<Bcomp FirstLess (one :: a) (one :: b) = go<Bcomp FirstLess a b

_<Bcomp_ : BinNat → BinNat → Compare
a <Bcomp b = go<Bcomp Equal a b

private
  lemma1 : {s : Compare} → (n : BinNat) → go<Bcomp s n n ≡ s
  lemma1 {Equal} [] = refl
  lemma1 {Equal} (zero :: n) = lemma1 n
  lemma1 {Equal} (one :: n) = lemma1 n
  lemma1 {FirstLess} [] = refl
  lemma1 {FirstLess} (zero :: n) = lemma1 n
  lemma1 {FirstLess} (one :: n) = lemma1 n
  lemma1 {FirstGreater} [] = refl
  lemma1 {FirstGreater} (zero :: n) = lemma1 n
  lemma1 {FirstGreater} (one :: n) = lemma1 n

  lemma : {s : Compare} → (n : BinNat) → go<Bcomp s (incr n) n ≡ FirstGreater
  lemma {Equal} [] = refl
  lemma {Equal} (zero :: n) = lemma1 n
  lemma {Equal} (one :: n) = lemma {FirstLess} n
  lemma {FirstLess} [] = refl
  lemma {FirstLess} (zero :: n) = lemma1 n
  lemma {FirstLess} (one :: n) = lemma {FirstLess} n
  lemma {FirstGreater} [] = refl
  lemma {FirstGreater} (zero :: n) = lemma1 {FirstGreater} n
  lemma {FirstGreater} (one :: n) = lemma {FirstLess} n

  succLess : (n : ℕ) → (NToBinNat (succ n)) <Bcomp (NToBinNat n) ≡ FirstGreater
  succLess zero = refl
  succLess (succ n) with NToBinNat n
  succLess (succ n) | [] = refl
  succLess (succ n) | zero :: bl = lemma {FirstLess} bl
  succLess (succ n) | one :: bl = lemma1 {FirstGreater} (incr bl)

  compareRefl : (n : BinNat) → n <Bcomp n ≡ Equal
  compareRefl [] = refl
  compareRefl (zero :: n) = compareRefl n
  compareRefl (one :: n) = compareRefl n

  zeroLess : (n : BinNat) → ((canonical n ≡ []) → False) → [] <Bcomp n ≡ FirstLess
  zeroLess [] pr = exFalso (pr refl)
  zeroLess (zero :: n) pr with inspect (canonical n)
  zeroLess (zero :: n) pr | [] with≡ x rewrite x = exFalso (pr refl)
  zeroLess (zero :: n) pr | (x₁ :: y) with≡ x = zeroLess n λ i → nonEmptyNotEmpty (transitivity (equalityCommutative x) i)
  zeroLess (one :: n) pr = refl

  zeroLess' : (n : BinNat) → ((canonical n ≡ []) → False) → n <Bcomp [] ≡ FirstGreater
  zeroLess' [] pr = exFalso (pr refl)
  zeroLess' (zero :: n) pr with inspect (canonical n)
  zeroLess' (zero :: n) pr | [] with≡ x rewrite x = exFalso (pr refl)
  zeroLess' (zero :: n) pr | (x₁ :: y) with≡ x = zeroLess' n (λ i → nonEmptyNotEmpty (transitivity (equalityCommutative x) i))
  zeroLess' (one :: n) pr = refl

abstract
  canonicalFirst : (n m : BinNat) (state : Compare) → go<Bcomp state n m ≡ go<Bcomp state (canonical n) m
  canonicalFirst [] m Equal = refl
  canonicalFirst (zero :: n) m Equal with inspect (canonical n)
  canonicalFirst (zero :: n) [] Equal | [] with≡ x rewrite x = transitivity (canonicalFirst n [] Equal) (applyEquality (λ i → go<Bcomp Equal i []) {canonical n} x)
  canonicalFirst (zero :: n) (zero :: ms) Equal | [] with≡ x rewrite x | canonicalFirst n ms Equal | x = refl
  canonicalFirst (zero :: n) (one :: ms) Equal | [] with≡ x rewrite x | canonicalFirst n ms FirstLess | x = refl
  canonicalFirst (zero :: n) [] Equal | (x₁ :: y) with≡ x rewrite x | canonicalFirst n [] Equal | x = refl
  canonicalFirst (zero :: n) (zero :: ms) Equal | (x₁ :: y) with≡ x rewrite x | canonicalFirst n ms Equal | x = refl
  canonicalFirst (zero :: n) (one :: ms) Equal | (x₁ :: y) with≡ x rewrite x | canonicalFirst n ms FirstLess | x = refl
  canonicalFirst (one :: n) [] Equal = refl
  canonicalFirst (one :: n) (zero :: m) Equal = canonicalFirst n m FirstGreater
  canonicalFirst (one :: n) (one :: m) Equal = canonicalFirst n m Equal
  canonicalFirst [] m FirstLess = refl
  canonicalFirst (zero :: n) [] FirstLess with inspect (canonical n)
  canonicalFirst (zero :: n) [] FirstLess | [] with≡ x rewrite x | canonicalFirst n [] FirstLess | x = refl
  canonicalFirst (zero :: n) [] FirstLess | (x₁ :: y) with≡ x rewrite x | canonicalFirst n [] FirstLess | x = refl
  canonicalFirst (zero :: n) (zero :: m) FirstLess with inspect (canonical n)
  canonicalFirst (zero :: n) (zero :: m) FirstLess | [] with≡ x rewrite x | canonicalFirst n m FirstLess | x = refl
  canonicalFirst (zero :: n) (zero :: m) FirstLess | (x₁ :: y) with≡ x rewrite x | canonicalFirst n m FirstLess | x = refl
  canonicalFirst (zero :: n) (one :: m) FirstLess with inspect (canonical n)
  canonicalFirst (zero :: n) (one :: m) FirstLess | [] with≡ x rewrite x | canonicalFirst n m FirstLess | x = refl
  canonicalFirst (zero :: n) (one :: m) FirstLess | (x₁ :: y) with≡ x rewrite x | canonicalFirst n m FirstLess | x = refl
  canonicalFirst (one :: n) [] FirstLess = refl
  canonicalFirst (one :: n) (zero :: m) FirstLess = canonicalFirst n m FirstGreater
  canonicalFirst (one :: n) (one :: m) FirstLess = canonicalFirst n m FirstLess
  canonicalFirst [] m FirstGreater = refl
  canonicalFirst (zero :: n) m FirstGreater with inspect (canonical n)
  canonicalFirst (zero :: n) [] FirstGreater | [] with≡ x rewrite x = refl
  canonicalFirst (zero :: n) (zero :: ms) FirstGreater | [] with≡ x rewrite x | canonicalFirst n ms FirstGreater | x = refl
  canonicalFirst (zero :: n) (one :: ms) FirstGreater | [] with≡ x rewrite x | canonicalFirst n ms FirstLess | x = refl
  canonicalFirst (zero :: n) [] FirstGreater | (x₁ :: y) with≡ x rewrite x = refl
  canonicalFirst (zero :: n) (zero :: ms) FirstGreater | (x₁ :: y) with≡ x rewrite x | canonicalFirst n ms FirstGreater | x = refl
  canonicalFirst (zero :: n) (one :: ms) FirstGreater | (x₁ :: y) with≡ x rewrite x | canonicalFirst n ms FirstLess | x = refl
  canonicalFirst (one :: n) [] FirstGreater = refl
  canonicalFirst (one :: n) (zero :: m) FirstGreater = canonicalFirst n m FirstGreater
  canonicalFirst (one :: n) (one :: m) FirstGreater = canonicalFirst n m FirstGreater

private
  greater0Lemma : (n : BinNat) → go<Bcomp FirstGreater n [] ≡ FirstGreater
  greater0Lemma [] = refl
  greater0Lemma (zero :: n) = refl
  greater0Lemma (one :: n) = refl

  canonicalSecond : (n m : BinNat) (state : Compare) → go<Bcomp state n m ≡ go<Bcomp state n (canonical m)
  canonicalSecond n [] Equal = refl
  canonicalSecond [] (zero :: m) Equal with inspect (canonical m)
  canonicalSecond [] (zero :: m) Equal | [] with≡ x rewrite x | canonicalSecond [] m Equal | x = refl
  canonicalSecond [] (zero :: m) Equal | (x₁ :: y) with≡ x rewrite x | canonicalSecond [] m Equal | x = refl
  canonicalSecond (zero :: n) (zero :: m) Equal with inspect (canonical m)
  canonicalSecond (zero :: n) (zero :: m) Equal | [] with≡ x rewrite x | canonicalSecond n m Equal | x = refl
  canonicalSecond (zero :: n) (zero :: m) Equal | (x₁ :: y) with≡ x rewrite x | canonicalSecond n m Equal | x = refl
  canonicalSecond (one :: n) (zero :: m) Equal with inspect (canonical m)
  canonicalSecond (one :: n) (zero :: m) Equal | [] with≡ x rewrite x | canonicalSecond n m FirstGreater | x = greater0Lemma n
  canonicalSecond (one :: n) (zero :: m) Equal | (x₁ :: y) with≡ x rewrite x | canonicalSecond n m FirstGreater | x = refl
  canonicalSecond [] (one :: m) Equal = refl
  canonicalSecond (zero :: n) (one :: m) Equal = canonicalSecond n m FirstLess
  canonicalSecond (one :: n) (one :: m) Equal = canonicalSecond n m Equal
  canonicalSecond n [] FirstLess = refl
  canonicalSecond [] (zero :: m) FirstLess = refl
  canonicalSecond (x :: n) (zero :: m) FirstLess with inspect (canonical m)
  canonicalSecond (zero :: n) (zero :: m) FirstLess | [] with≡ x rewrite x | canonicalSecond n m FirstLess | x = refl
  canonicalSecond (one :: n) (zero :: m) FirstLess | [] with≡ x rewrite x | canonicalSecond n m FirstGreater | x = greater0Lemma n
  canonicalSecond (zero :: n) (zero :: m) FirstLess | (x₁ :: bl) with≡ pr rewrite pr | canonicalSecond n m FirstLess | pr = refl
  canonicalSecond (one :: n) (zero :: m) FirstLess | (x₁ :: bl) with≡ pr rewrite pr | canonicalSecond n m FirstGreater | pr = refl
  canonicalSecond [] (one :: m) FirstLess = refl
  canonicalSecond (zero :: n) (one :: m) FirstLess = canonicalSecond n m FirstLess
  canonicalSecond (one :: n) (one :: m) FirstLess = canonicalSecond n m FirstLess
  canonicalSecond n [] FirstGreater = refl
  canonicalSecond [] (zero :: m) FirstGreater with inspect (canonical m)
  canonicalSecond [] (zero :: m) FirstGreater | [] with≡ x rewrite x | canonicalSecond [] m FirstGreater | x = refl
  canonicalSecond [] (zero :: m) FirstGreater | (x₁ :: y) with≡ x rewrite x | canonicalSecond [] m FirstGreater | x = refl
  canonicalSecond (zero :: n) (zero :: m) FirstGreater with inspect (canonical m)
  canonicalSecond (zero :: n) (zero :: m) FirstGreater | [] with≡ x rewrite x | canonicalSecond n m FirstGreater | x = greater0Lemma n
  canonicalSecond (zero :: n) (zero :: m) FirstGreater | (x₁ :: y) with≡ x rewrite x | canonicalSecond n m FirstGreater | x = refl
  canonicalSecond (one :: n) (zero :: m) FirstGreater with inspect (canonical m)
  canonicalSecond (one :: n) (zero :: m) FirstGreater | [] with≡ x rewrite x | canonicalSecond n m FirstGreater | x = greater0Lemma n
  canonicalSecond (one :: n) (zero :: m) FirstGreater | (x₁ :: y) with≡ x rewrite x | canonicalSecond n m FirstGreater | x = refl
  canonicalSecond [] (one :: m) FirstGreater = refl
  canonicalSecond (zero :: n) (one :: m) FirstGreater = canonicalSecond n m FirstLess
  canonicalSecond (one :: n) (one :: m) FirstGreater = canonicalSecond n m FirstGreater

  equalContaminated : (n m : BinNat) → go<Bcomp FirstLess n m ≡ Equal → False
  equalContaminated' : (n m : BinNat) → go<Bcomp FirstGreater n m ≡ Equal → False

  equalContaminated (zero :: n) [] pr = equalContaminated n [] pr
  equalContaminated (zero :: n) (zero :: m) pr = equalContaminated n m pr
  equalContaminated (zero :: n) (one :: m) pr = equalContaminated n m pr
  equalContaminated (one :: n) (zero :: m) pr = equalContaminated' n m pr
  equalContaminated (one :: n) (one :: m) pr = equalContaminated n m pr

  equalContaminated' [] (zero :: m) pr = equalContaminated' [] m pr
  equalContaminated' (zero :: n) (zero :: m) pr = equalContaminated' n m pr
  equalContaminated' (zero :: n) (one :: m) pr = equalContaminated n m pr
  equalContaminated' (one :: n) (zero :: m) pr = equalContaminated' n m pr
  equalContaminated' (one :: n) (one :: m) pr = equalContaminated' n m pr

  comparisonEqual : (a b : BinNat) → (a <Bcomp b ≡ Equal) → canonical a ≡ canonical b
  comparisonEqual [] [] pr = refl
  comparisonEqual [] (zero :: b) pr with inspect (canonical b)
  comparisonEqual [] (zero :: b) pr | [] with≡ p rewrite p = refl
  comparisonEqual [] (zero :: b) pr | (x :: r) with≡ p rewrite zeroLess b (λ i → nonEmptyNotEmpty (transitivity (equalityCommutative p) i)) = exFalso (badCompare (equalityCommutative pr))
  comparisonEqual (zero :: a) [] pr with inspect (canonical a)
  comparisonEqual (zero :: a) [] pr | [] with≡ x rewrite x = refl
  comparisonEqual (zero :: a) [] pr | (x₁ :: y) with≡ x rewrite zeroLess' a (λ i → nonEmptyNotEmpty (transitivity (equalityCommutative x) i)) = exFalso (badCompare' (equalityCommutative pr))
  comparisonEqual (zero :: a) (zero :: b) pr with inspect (canonical a)
  comparisonEqual (zero :: a) (zero :: b) pr | [] with≡ x with inspect (canonical b)
  comparisonEqual (zero :: a) (zero :: b) pr | [] with≡ pr2 | [] with≡ pr3 rewrite pr2 | pr3 = refl
  comparisonEqual (zero :: a) (zero :: b) pr | [] with≡ pr2 | (x₂ :: y) with≡ pr3 rewrite pr2 | pr3 | comparisonEqual a b pr = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr3) pr2))
  comparisonEqual (zero :: a) (zero :: b) pr | (c :: cs) with≡ pr2 with inspect (canonical b)
  comparisonEqual (zero :: a) (zero :: b) pr | (c :: cs) with≡ pr2 | [] with≡ pr3 rewrite pr2 | pr3 | comparisonEqual a b pr = exFalso (nonEmptyNotEmpty (transitivity (equalityCommutative pr2) pr3))
  comparisonEqual (zero :: a) (zero :: b) pr | (c :: cs) with≡ pr2 | (x₁ :: y) with≡ pr3 rewrite pr2 | pr3 | comparisonEqual a b pr = applyEquality (zero ::_) (transitivity (equalityCommutative pr2) pr3)
  comparisonEqual (zero :: a) (one :: b) pr = exFalso (equalContaminated a b pr)
  comparisonEqual (one :: a) (zero :: b) pr = exFalso (equalContaminated' a b pr)
  comparisonEqual (one :: a) (one :: b) pr = applyEquality (one ::_) (comparisonEqual a b pr)

  equalSymmetric : (n m : BinNat) → n <Bcomp m ≡ Equal → m <Bcomp n ≡ Equal
  equalSymmetric [] [] n=m = refl
  equalSymmetric [] (zero :: m) n=m rewrite equalSymmetric [] m n=m = refl
  equalSymmetric (zero :: n) [] n=m rewrite equalSymmetric n [] n=m = refl
  equalSymmetric (zero :: n) (zero :: m) n=m = equalSymmetric n m n=m
  equalSymmetric (zero :: n) (one :: m) n=m = exFalso (equalContaminated n m n=m)
  equalSymmetric (one :: n) (zero :: m) n=m = exFalso (equalContaminated' n m n=m)
  equalSymmetric (one :: n) (one :: m) n=m = equalSymmetric n m n=m

  equalToFirstGreater : (state : Compare) → (a b : BinNat) → go<Bcomp Equal a b ≡ FirstGreater → go<Bcomp state a b ≡ FirstGreater
  equalToFirstGreater FirstGreater [] (zero :: b) pr = equalToFirstGreater FirstGreater [] b pr
  equalToFirstGreater FirstGreater (zero :: a) [] pr = refl
  equalToFirstGreater FirstGreater (zero :: a) (zero :: b) pr = equalToFirstGreater FirstGreater a b pr
  equalToFirstGreater FirstGreater (zero :: a) (one :: b) pr = pr
  equalToFirstGreater FirstGreater (one :: a) [] pr = refl
  equalToFirstGreater FirstGreater (one :: a) (zero :: b) pr = pr
  equalToFirstGreater FirstGreater (one :: a) (one :: b) pr = equalToFirstGreater FirstGreater a b pr
  equalToFirstGreater Equal a b pr = pr
  equalToFirstGreater FirstLess [] (zero :: b) pr = equalToFirstGreater FirstLess [] b pr
  equalToFirstGreater FirstLess (zero :: a) [] pr = equalToFirstGreater FirstLess a [] pr
  equalToFirstGreater FirstLess (zero :: a) (zero :: b) pr = equalToFirstGreater FirstLess a b pr
  equalToFirstGreater FirstLess (zero :: a) (one :: b) pr = pr
  equalToFirstGreater FirstLess (one :: a) [] pr = refl
  equalToFirstGreater FirstLess (one :: a) (zero :: b) pr = pr
  equalToFirstGreater FirstLess (one :: a) (one :: b) pr = equalToFirstGreater FirstLess a b pr

  equalToFirstLess : (state : Compare) → (a b : BinNat) → go<Bcomp Equal a b ≡ FirstLess → go<Bcomp state a b ≡ FirstLess
  equalToFirstLess FirstLess [] b pr = refl
  equalToFirstLess FirstLess (zero :: a) [] pr = equalToFirstLess FirstLess a [] pr
  equalToFirstLess FirstLess (zero :: a) (zero :: b) pr = equalToFirstLess FirstLess a b pr
  equalToFirstLess FirstLess (zero :: a) (one :: b) pr = pr
  equalToFirstLess FirstLess (one :: a) (zero :: b) pr = pr
  equalToFirstLess FirstLess (one :: a) (one :: b) pr = equalToFirstLess FirstLess a b pr
  equalToFirstLess Equal a b pr = pr
  equalToFirstLess FirstGreater [] (zero :: b) pr = equalToFirstLess FirstGreater [] b pr
  equalToFirstLess FirstGreater [] (one :: b) pr = refl
  equalToFirstLess FirstGreater (zero :: a) [] pr = transitivity (t a) (equalToFirstLess FirstGreater a [] pr)
    where
      t : (a : BinNat) → FirstGreater ≡ go<Bcomp FirstGreater a []
      t [] = refl
      t (zero :: a) = refl
      t (one :: a) = refl
  equalToFirstLess FirstGreater (zero :: a) (zero :: b) pr = equalToFirstLess FirstGreater a b pr
  equalToFirstLess FirstGreater (zero :: a) (one :: b) pr = pr
  equalToFirstLess FirstGreater (one :: a) (zero :: b) pr = pr
  equalToFirstLess FirstGreater (one :: a) (one :: b) pr = equalToFirstLess FirstGreater a b pr

  zeroNotSucc : (n : ℕ) (b : BinNat) → (canonical b ≡ []) → (binNatToN b ≡ succ n) → False
  zeroNotSucc n b b=0 b>0 rewrite binNatToNZero' b b=0 = naughtE b>0

  chopFirstBit : (m n : BinNat) {b : Bit} (s : Compare) → go<Bcomp s (b :: m) (b :: n) ≡ go<Bcomp s m n
  chopFirstBit m n {zero} Equal = refl
  chopFirstBit m n {one} Equal = refl
  chopFirstBit m n {zero} FirstLess = refl
  chopFirstBit m n {one} FirstLess = refl
  chopFirstBit m n {zero} FirstGreater = refl
  chopFirstBit m n {one} FirstGreater = refl

  chopDouble : (a b : BinNat) (i : Bit) → (i :: a) <BInherited (i :: b) ≡ a <BInherited b
  chopDouble a b i with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
  chopDouble a b zero | inl (inl a<b) with TotalOrder.totality ℕTotalOrder (2 *N binNatToN a) (2 *N binNatToN b)
  chopDouble a b zero | inl (inl a<b) | inl (inl x) = refl
  chopDouble a b zero | inl (inl a<b) | inl (inr b<a) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive ℕTotalOrder b<a (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl))))
  chopDouble a b zero | inl (inl a<b) | inr a=b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) a=b = exFalso (TotalOrder.irreflexive ℕTotalOrder a<b)
  chopDouble a b one | inl (inl a<b) with TotalOrder.totality ℕTotalOrder (2 *N binNatToN a) (2 *N binNatToN b)
  chopDouble a b one | inl (inl a<b) | inl (inl 2a<2b) = refl
  chopDouble a b one | inl (inl a<b) | inl (inr 2b<2a) = exFalso (TotalOrder.irreflexive ℕTotalOrder (TotalOrder.<Transitive (ℕTotalOrder) a<b (cancelInequalityLeft {2} 2b<2a)))
  chopDouble a b one | inl (inl a<b) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
  chopDouble a b zero | inl (inr b<a) with TotalOrder.totality ℕTotalOrder (2 *N binNatToN a) (2 *N binNatToN b)
  chopDouble a b zero | inl (inr b<a) | inl (inl 2a<2b) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) b<a (cancelInequalityLeft {2} {binNatToN a} {binNatToN b} 2a<2b)))
  chopDouble a b zero | inl (inr b<a) | inl (inr 2b<2a) = refl
  chopDouble a b zero | inl (inr b<a) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
  chopDouble a b one | inl (inr b<a) with TotalOrder.totality ℕTotalOrder (2 *N binNatToN a) (2 *N binNatToN b)
  chopDouble a b one | inl (inr b<a) | inl (inl 2a<2b) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) b<a (cancelInequalityLeft {2} 2a<2b)))
  chopDouble a b one | inl (inr b<a) | inl (inr x) = refl
  chopDouble a b one | inl (inr b<a) | inr 2a=2b rewrite productCancelsLeft 2 (binNatToN a) (binNatToN b) (le 1 refl) 2a=2b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
  chopDouble a b i | inr x with TotalOrder.totality ℕTotalOrder (binNatToN (i :: a)) (binNatToN (i :: b))
  chopDouble a b zero | inr a=b | inl (inl a<b) rewrite a=b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
  chopDouble a b one | inr a=b | inl (inl a<b) rewrite a=b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
  chopDouble a b zero | inr a=b | inl (inr b<a) rewrite a=b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
  chopDouble a b one | inr a=b | inl (inr b<a) rewrite a=b = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
  chopDouble a b _ | inr a=b | inr x = refl

  succNotLess : {n : ℕ} → succ n <N n → False
  succNotLess {succ n} (le x proof) = succNotLess {n} (le x (succInjective (transitivity (applyEquality succ (transitivity (Semiring.commutative ℕSemiring (succ x) (succ n)) (transitivity (applyEquality succ (transitivity (Semiring.commutative ℕSemiring n (succ x)) (applyEquality succ (Semiring.commutative ℕSemiring x n)))) (Semiring.commutative ℕSemiring (succ (succ n)) x)))) proof)))

<BIsInherited : (a b : BinNat) → a <BInherited b ≡ a <Bcomp b
<BIsInherited [] b with TotalOrder.totality ℕTotalOrder 0 (binNatToN b)
<BIsInherited [] b | inl (inl x) with inspect (binNatToN b)
<BIsInherited [] b | inl (inl x) | 0 with≡ pr rewrite binNatToNZero b pr | pr = exFalso (TotalOrder.irreflexive (ℕTotalOrder) x)
<BIsInherited [] b | inl (inl x) | (succ bl) with≡ pr rewrite pr = equalityCommutative (zeroLess b λ p → zeroNotSucc bl b p pr)
<BIsInherited [] b | inr 0=b rewrite canonicalSecond [] b Equal | binNatToNZero b (equalityCommutative 0=b) = refl
<BIsInherited (a :: as) [] with TotalOrder.totality ℕTotalOrder (binNatToN (a :: as)) 0
<BIsInherited (a :: as) [] | inl (inr x) with inspect (binNatToN (a :: as))
<BIsInherited (a :: as) [] | inl (inr x) | zero with≡ pr rewrite binNatToNZero (a :: as) pr | pr = exFalso (TotalOrder.irreflexive (ℕTotalOrder) x)
<BIsInherited (a :: as) [] | inl (inr x) | succ y with≡ pr rewrite pr = equalityCommutative (zeroLess' (a :: as) λ i → zeroNotSucc y (a :: as) i pr)
<BIsInherited (a :: as) [] | inr x rewrite canonicalFirst (a :: as) [] Equal | binNatToNZero (a :: as) x = refl
<BIsInherited (zero :: a) (zero :: b) = transitivity (chopDouble a b zero) (<BIsInherited a b)
<BIsInherited (zero :: a) (one :: b) with TotalOrder.totality ℕTotalOrder (binNatToN (zero :: a)) (binNatToN (one :: b))
<BIsInherited (zero :: a) (one :: b) | inl (inl 2a<2b+1) with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
<BIsInherited (zero :: a) (one :: b) | inl (inl 2a<2b+1) | inl (inl a<b) = equalityCommutative (equalToFirstLess FirstLess a b (equalityCommutative indHyp))
    where
      t : a <BInherited b ≡ FirstLess
      t with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
      t | inl (inl x) = refl
      t | inl (inr x) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) x a<b))
      t | inr x rewrite x = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
      indHyp : FirstLess ≡ go<Bcomp Equal a b
      indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
<BIsInherited (zero :: a) (one :: b) | inl (inl 2a<2b+1) | inl (inr b<a) = exFalso (noIntegersBetweenXAndSuccX {2 *N binNatToN a} (2 *N binNatToN b) (lessRespectsMultiplicationLeft (binNatToN b) (binNatToN a) 2 b<a (le 1 refl)) 2a<2b+1)
<BIsInherited (zero :: a) (one :: b) | inl (inl 2a<2b+1) | inr a=b rewrite a=b | canonicalFirst a b FirstLess | canonicalSecond (canonical a) b FirstLess | transitivity (equalityCommutative (binToBin a)) (transitivity (applyEquality NToBinNat a=b) (binToBin b)) = equalityCommutative (lemma1 (canonical b))
<BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
<BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inl (inl a<b) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) 2b+1<2a (TotalOrder.<Transitive (ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl)) (le zero refl))))
<BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inl (inr b<a) = equalityCommutative (equalToFirstGreater FirstLess a b (equalityCommutative indHyp))
  where
    t : a <BInherited b ≡ FirstGreater
    t with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
    t | inl (inl x) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) x b<a))
    t | inl (inr x) = refl
    t | inr x rewrite x = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
    indHyp : FirstGreater ≡ go<Bcomp Equal a b
    indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
<BIsInherited (zero :: a) (one :: b) | inl (inr 2b+1<2a) | inr a=b rewrite a=b = exFalso (succNotLess 2b+1<2a)
<BIsInherited (zero :: a) (one :: b) | inr 2a=2b+1 = exFalso (parity (binNatToN b) (binNatToN a) (equalityCommutative 2a=2b+1))
<BIsInherited (one :: a) (zero :: b) with TotalOrder.totality ℕTotalOrder (binNatToN (one :: a)) (binNatToN (zero :: b))
<BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
<BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) | inl (inl a<b) = equalityCommutative (equalToFirstLess FirstGreater a b (equalityCommutative indHyp))
  where
    t : a <BInherited b ≡ FirstLess
    t with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
    t | inl (inr x) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) x a<b))
    t | inl (inl x) = refl
    t | inr x rewrite x = exFalso (TotalOrder.irreflexive (ℕTotalOrder) a<b)
    indHyp : FirstLess ≡ go<Bcomp Equal a b
    indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
<BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) | inl (inr b<a) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) 2a+1<2b (TotalOrder.<Transitive (ℕTotalOrder) (lessRespectsMultiplicationLeft (binNatToN b) (binNatToN a) 2 b<a (le 1 refl)) (le zero refl))))
<BIsInherited (one :: a) (zero :: b) | inl (inl 2a+1<2b) | inr a=b rewrite a=b = exFalso (succNotLess 2a+1<2b)
<BIsInherited (one :: a) (zero :: b) | inl (inr 2b<2a+1) with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
<BIsInherited (one :: a) (zero :: b) | inl (inr 2b<2a+1) | inl (inl a<b) = exFalso (noIntegersBetweenXAndSuccX {2 *N binNatToN b} (2 *N binNatToN a) (lessRespectsMultiplicationLeft (binNatToN a) (binNatToN b) 2 a<b (le 1 refl)) 2b<2a+1)
<BIsInherited (one :: a) (zero :: b) | inl (inr 2b<2a+1) | inl (inr b<a) = equalityCommutative (equalToFirstGreater FirstGreater a b (equalityCommutative indHyp))
  where
    t : a <BInherited b ≡ FirstGreater
    t with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
    t | inl (inl x) = exFalso (TotalOrder.irreflexive (ℕTotalOrder) (TotalOrder.<Transitive (ℕTotalOrder) x b<a))
    t | inl (inr x) = refl
    t | inr x rewrite x = exFalso (TotalOrder.irreflexive (ℕTotalOrder) b<a)
    indHyp : FirstGreater ≡ go<Bcomp Equal a b
    indHyp = transitivity (equalityCommutative t) (<BIsInherited a b)
<BIsInherited (one :: a) (zero :: b) | inl (inr 2b<2a+1) | inr a=b rewrite a=b | canonicalFirst a b FirstGreater | canonicalSecond (canonical a) b FirstGreater | transitivity (equalityCommutative (binToBin a)) (transitivity (applyEquality NToBinNat a=b) (binToBin b)) = equalityCommutative (lemma1 (canonical b))
<BIsInherited (one :: a) (zero :: b) | inr x = exFalso (parity (binNatToN a) (binNatToN b) x)
<BIsInherited (one :: a) (one :: b) = transitivity (chopDouble a b one) (<BIsInherited a b)

_<B_ : BinNat → BinNat → Set
a <B b = (a <Bcomp b) ≡ FirstLess

translate : (a b : BinNat) → (a <B b) → (binNatToN a) <N (binNatToN b)
translate a b a<b with <BIsInherited a b
... | r with TotalOrder.totality ℕTotalOrder (binNatToN a) (binNatToN b)
... | inl (inl x) = x
... | inl (inr x) = exFalso (badCompare'' (transitivity (equalityCommutative a<b) (equalityCommutative r)))
... | inr x = exFalso (badCompare (transitivity r a<b))

private
  totality : (a b : BinNat) → ((a <B b) || (b <B a)) || (canonical a ≡ canonical b)
  totality [] [] = inr refl
  totality [] (zero :: b) with totality [] b
  ... | inl (inl x) = inl (inl x)
  ... | inl (inr x) = inl (inr x)
  ... | inr x with canonical b
  ... | [] = inr refl
  totality [] (one :: b) = inl (inl refl)
  totality (zero :: a) [] with totality a []
  ... | inl (inl x) = inl (inl x)
  ... | inl (inr x) = inl (inr x)
  ... | inr x with canonical a
  ... | [] = inr refl
  totality (zero :: a) (zero :: b) with totality a b
  ... | inl (inl x) = inl (inl x)
  ... | inl (inr x) = inl (inr x)
  ... | inr x rewrite x = inr refl
  totality (zero :: a) (one :: b) with totality a b
  ... | inl (inl x) = inl (inl (equalToFirstLess FirstLess a b x))
  ... | inr x rewrite canonicalSecond a b FirstLess | canonicalFirst a (canonical b) FirstLess | x = inl (inl (lemma1 (canonical b)))
  ... | inl (inr x) with equalToFirstLess FirstGreater b a x
  ... | r = inl (inr r)
  totality (one :: a) [] = inl (inr refl)
  totality (one :: a) (zero :: b) with totality a b
  ... | inr x rewrite canonicalSecond b a FirstLess | canonicalFirst b (canonical a) FirstLess | x = inl (inr (lemma1 (canonical b)))
  ... | inl (inr x) = inl (inr (equalToFirstLess FirstLess b a x))
  ... | inl (inl x) with equalToFirstLess FirstGreater a b x
  ... | r = inl (inl r)
  totality (one :: a) (one :: b) with totality a b
  ... | inl (inl x) = inl (inl x)
  ... | inl (inr x) = inl (inr x)
  ... | inr x rewrite x = inr refl

translate' : (a b : ℕ) → (a <N b) → (NToBinNat a) <B (NToBinNat b)
translate' a b a<b with totality (NToBinNat a) (NToBinNat b)
... | inl (inl x) = x
... | inl (inr x) with translate (NToBinNat b) (NToBinNat a) x
... | m = exFalso (lessIrreflexive (lessTransitive a<b (identityOfIndiscernablesLeft _<N_ (identityOfIndiscernablesRight _<N_ m (nToN a)) (nToN b))))
translate' a b a<b | inr x rewrite NToBinNatInj a b x = exFalso (lessIrreflexive a<b)

private
  <BTransitive : (a b c : BinNat) → (a <B b) → (b <B c) → a <B c
  <BTransitive a b c a<b b<c with translate' (binNatToN a) (binNatToN c) (PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) (translate a b a<b) (translate b c b<c))
  ... | r rewrite binToBin a | binToBin c = transitivity (canonicalFirst a c Equal) (transitivity (canonicalSecond (canonical a) c Equal) r)

-- This order fails to be total because [] is not literally equal to 0::[] .
BinNatOrder : PartialOrder BinNat
PartialOrder._<_ (BinNatOrder) = _<B_
PartialOrder.irreflexive (BinNatOrder) {x} bad = badCompare (transitivity (equalityCommutative (compareRefl x)) bad)
PartialOrder.<Transitive (BinNatOrder) {a} {b} {c} a<b b<c = <BTransitive a b c a<b b<c


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

module Categories.Adjoint.Instance.Discrete where

-- The Discrete/Forgetful/Codiscrete adjoint triple between Sets and
-- StrictCats.
--
-- We need 'strict' functor equality to prove functionality of the
-- forgetful functor (we cannot extract a propositional equality proof
-- on objects from a natural isomorphism).

open import Level using (Lift; lift)
open import Data.Unit using (⊤; tt)
import Function as Fun
open import Relation.Binary.PropositionalEquality

open import Categories.Adjoint
open import Categories.Category using (Category)
open import Categories.Category.Instance.StrictCats
open import Categories.Category.Instance.Sets
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Equivalence
import Categories.Category.Discrete as D
open import Categories.Morphism.HeterogeneousIdentity
open import Categories.Morphism.HeterogeneousIdentity.Properties
open import Categories.NaturalTransformation as NT using (NaturalTransformation; ntHelper)

-- The forgetful functor from StrictCats to Sets.

Forgetful : ∀ {o ℓ e} → Functor (Cats o ℓ e) (Sets o)
Forgetful {o} {ℓ} {e} = record
  { F₀ = Obj
  ; F₁ = F₀
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = λ F≡G {X} → eq₀ F≡G X
  }
  where
    open Category
    open Functor
    open _≡F_

-- The discrete functor (strict version)

Discrete : ∀ {o} → Functor (Sets o) (Cats o o o)
Discrete {o} = record
  { F₀ = D.Discrete
  ; F₁ = λ f → record
    { F₀ = f
    ; F₁ = cong f
    ; identity     = refl
    ; homomorphism = λ {_ _ _ p q} → cong-trans f p q
    ; F-resp-≈     = cong (cong f)
    }
  ; identity = record
    { eq₀ = λ _ → refl
    ; eq₁ = λ p → let open ≡-Reasoning in begin
        trans (cong Fun.id p) refl   ≡⟨ trans-reflʳ _ ⟩
               cong Fun.id p         ≡⟨ cong-id p ⟩
                           p         ∎
    }
  ; homomorphism = λ {_ _ _ f g} → record
    { eq₀ = λ _ → refl
    ; eq₁ = λ p → let open ≡-Reasoning in begin
        trans (cong (g Fun.∘ f) p) refl ≡⟨ trans-reflʳ _ ⟩
               cong (g Fun.∘ f) p       ≡⟨ cong-∘ p ⟩
               cong g (cong f p)        ∎
    }
  ; F-resp-≈ = λ {_ _ f g} f≗g → record
    { eq₀ = λ x → f≗g {x}
    ; eq₁ = λ {x} {y} p → naturality (λ x → subst (f x ≡_) (f≗g {x}) refl)
    }
  }
  where

    -- A helper lemma.
    -- FIXME: Should probably go into Relation.Binary.PropositionalEquality

    cong-trans : ∀ {A B : Set o} (f : A → B) {x y z} (p : x ≡ y) (q : y ≡ z) →
                 cong f (trans p q) ≡ trans (cong f p) (cong f q)
    cong-trans f refl refl = refl

-- The codiscrete functor (strict version)

Codiscrete : ∀ {o} ℓ e → Functor (Sets o) (Cats o ℓ e)
Codiscrete {o} ℓ e = record
  { F₀ = λ A → record
    { Obj = A
    ; _⇒_ = λ _ _ → Lift ℓ ⊤
    ; _≈_ = λ _ _ → Lift e ⊤
    ; id  = lift tt
    ; _∘_ = λ _ _ → lift tt
    ; assoc     = lift tt
    ; identityˡ = lift tt
    ; identityʳ = lift tt
    ; equiv     = record
      { refl  = lift tt
      ; sym   = λ _ → lift tt
      ; trans = λ _ _ → lift tt
      }
    ; ∘-resp-≈ = λ _ _ → lift tt
    }
  ; F₁ = λ f → record
    { F₀ = f
    ; F₁ = λ _ → lift tt
    ; identity     = lift tt
    ; homomorphism = lift tt
    ; F-resp-≈     = λ _ → lift tt
    }
  ; identity     = Equiv.refl
  ; homomorphism = Equiv.refl
  ; F-resp-≈     = λ {_ _ f g} f≗g → record
    { eq₀ = λ x → f≗g {x}
    ; eq₁ = λ _ → lift tt
    }
  }
  where open Category (Cats o ℓ e)

-- Discrete is left-adjoint to the forgetful functor from StrictCats to Sets

DiscreteLeftAdj : ∀ {o} → Discrete ⊣ Forgetful {o} {o} {o}
DiscreteLeftAdj {o} = record
  { unit   = unit
  ; counit = counit
  ; zig    = zig
  ; zag    = refl
  }
  where
    module U = Functor Forgetful
    module Δ = Functor Discrete

    unit : NaturalTransformation idF (Forgetful ∘F Discrete)
    unit = NT.id

    counitFun : ∀ C → Functor (Δ.F₀ (U.F₀ C)) C
    counitFun C = let open Category C in record
      { F₀ = Fun.id
      ; F₁ = hid C
      ; identity     = Equiv.refl
      ; homomorphism = λ {_ _ _ p q} → Equiv.sym (hid-trans C q p)
      ; F-resp-≈     = hid-cong C
      }

    counitComm : ∀ {C D} → (F : Functor C D) →
                 counitFun D ∘F (Δ.F₁ (U.F₁ F)) ≡F F ∘F counitFun C
    counitComm {C} {D} F =
      let open Functor F
          open Category D
          open HomReasoning hiding (refl)
      in record
      { eq₀ = λ _ → refl
      ; eq₁ = λ {X Y} p → begin
        id ∘ hid D (cong F₀ p)   ≈⟨ identityˡ ⟩
             hid D (cong F₀ p)   ≈˘⟨ F-hid F p ⟩
        F₁ (hid C p)             ≈˘⟨ identityʳ ⟩
        F₁ (hid C p) ∘ id        ∎
      }

    counit : NaturalTransformation (Discrete ∘F Forgetful) idF
    counit = ntHelper record { η = counitFun ; commute = counitComm }

    zig : {A : Set o} → counitFun (Δ.F₀ A) ∘F (Δ.F₁ Fun.id) ≡F idF
    zig {A} = record { eq₀ = λ _ → refl ; eq₁ = λ{ refl → refl } }

-- Codiscrete is right-adjoint to the forgetful functor from StrictCats to Sets

CodiscreteRightAdj : ∀ {o ℓ e} → Forgetful ⊣ Codiscrete {o} ℓ e
CodiscreteRightAdj {o} {ℓ} {e} = record
  { unit   = unit
  ; counit = counit
  ; zig    = refl
  ; zag    = zag
  }
  where
    module U = Functor Forgetful
    module ∇ = Functor (Codiscrete ℓ e)

    unitFun : ∀ C → Functor C (∇.F₀ (U.F₀ C))
    unitFun C = let open Category C in record
      { F₀ = Fun.id
      ; F₁ = λ _ → lift tt
      ; identity     = lift tt
      ; homomorphism = lift tt
      ; F-resp-≈     = λ _ → lift tt
      }

    unitComm : ∀ {C D} → (F : Functor C D) →
               unitFun D ∘F F ≡F (∇.F₁ (U.F₁ F)) ∘F unitFun C
    unitComm {C} {D} F = record { eq₀ = λ _ → refl ; eq₁ = λ _ → lift tt }

    unit : NaturalTransformation idF (Codiscrete ℓ e ∘F Forgetful)
    unit = ntHelper record { η = unitFun ; commute = unitComm }

    counit : NaturalTransformation (Forgetful ∘F Codiscrete ℓ e) idF
    counit = NT.id

    zag : {B : Set o} → ∇.F₁ Fun.id ∘F unitFun (∇.F₀ B) ≡F idF
    zag {B} = record { eq₀ = λ _ → refl ; eq₁ = λ _ → lift tt }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module list-simplifier where

open import level
open import bool
open import functions
open import eq
open import empty
open import level
open import list
open import list-thms
open import nat
open import neq
open import product
open import product-thms

data 𝕃ʳ : Set → Set lone where
  _ʳ : {A : Set} → 𝕃 A → 𝕃ʳ A
  _++ʳ_ : {A : Set} → 𝕃ʳ A → 𝕃ʳ A → 𝕃ʳ A
  mapʳ : {A B : Set} → (A → B) → 𝕃ʳ A → 𝕃ʳ B
  _::ʳ_ : {A : Set} → A → 𝕃ʳ A → 𝕃ʳ A
  []ʳ : {A : Set} → 𝕃ʳ A

𝕃⟦_⟧ : {A : Set} → 𝕃ʳ A → 𝕃 A
𝕃⟦ l ʳ ⟧ = l
𝕃⟦ t1 ++ʳ t2 ⟧ = 𝕃⟦ t1 ⟧ ++ 𝕃⟦ t2 ⟧
𝕃⟦ mapʳ f t ⟧ = map f 𝕃⟦ t ⟧
𝕃⟦ x ::ʳ t ⟧ = x :: 𝕃⟦ t ⟧
𝕃⟦ []ʳ ⟧ = []

is-emptyʳ : {A : Set} → 𝕃ʳ A → 𝔹
is-emptyʳ []ʳ = tt
is-emptyʳ _ = ff

is-emptyʳ-≡ : {A : Set}(t : 𝕃ʳ A) → is-emptyʳ t ≡ tt → t ≡ []ʳ
is-emptyʳ-≡ []ʳ p = refl
is-emptyʳ-≡ (_ ++ʳ _) ()
is-emptyʳ-≡ (mapʳ _ _) ()
is-emptyʳ-≡ (_ ::ʳ _) ()
is-emptyʳ-≡ (_ ʳ) ()

𝕃ʳ-simp-step : {A : Set}(t : 𝕃ʳ A) → 𝕃ʳ A
𝕃ʳ-simp-step ((t1a ++ʳ t1b) ++ʳ t2) = t1a ++ʳ (t1b ++ʳ t2)
𝕃ʳ-simp-step ((x ::ʳ t1) ++ʳ t2) = x ::ʳ (t1 ++ʳ t2)
𝕃ʳ-simp-step ([]ʳ ++ʳ t2) = t2
𝕃ʳ-simp-step ((l ʳ) ++ʳ t2) =
  if is-emptyʳ t2 then l ʳ else ((l ʳ) ++ʳ t2)
𝕃ʳ-simp-step ((mapʳ f t1) ++ʳ t2) =
  if is-emptyʳ t2 then mapʳ f t1 else ((mapʳ f t1) ++ʳ t2)
𝕃ʳ-simp-step (mapʳ f (t1 ++ʳ t2)) = (mapʳ f t1) ++ʳ (mapʳ f t2)
𝕃ʳ-simp-step (mapʳ f (l ʳ)) = (map f l) ʳ
𝕃ʳ-simp-step (mapʳ f (mapʳ g t)) = mapʳ (f ∘ g) t
𝕃ʳ-simp-step (mapʳ f (x ::ʳ t)) = (f x) ::ʳ (mapʳ f t)
𝕃ʳ-simp-step (mapʳ f []ʳ) = []ʳ
𝕃ʳ-simp-step (l ʳ) = l ʳ
𝕃ʳ-simp-step (x ::ʳ t) = (x ::ʳ t)
𝕃ʳ-simp-step []ʳ = []ʳ

𝕃ʳ-simp-sdev : {A : Set}(t : 𝕃ʳ A) → 𝕃ʳ A
𝕃ʳ-simp-sdev (l ʳ) = (l ʳ)
𝕃ʳ-simp-sdev (t1 ++ʳ t2) = 𝕃ʳ-simp-step ((𝕃ʳ-simp-sdev t1) ++ʳ (𝕃ʳ-simp-sdev t2))
𝕃ʳ-simp-sdev (mapʳ f t1) = 𝕃ʳ-simp-step (mapʳ f (𝕃ʳ-simp-sdev t1))
𝕃ʳ-simp-sdev (x ::ʳ t1) = 𝕃ʳ-simp-step (x ::ʳ (𝕃ʳ-simp-sdev t1))
𝕃ʳ-simp-sdev []ʳ = []ʳ

𝕃ʳ-simp : {A : Set}(t : 𝕃ʳ A) → ℕ → 𝕃ʳ A
𝕃ʳ-simp t 0 = t
𝕃ʳ-simp t (suc n) = 𝕃ʳ-simp-sdev (𝕃ʳ-simp t n)

𝕃ʳ-simp-step-sound : {A : Set}(t : 𝕃ʳ A) → 𝕃⟦ t ⟧ ≡ 𝕃⟦ 𝕃ʳ-simp-step t ⟧
𝕃ʳ-simp-step-sound ((t1a ++ʳ t1b) ++ʳ t2) = ++-assoc 𝕃⟦ t1a ⟧ 𝕃⟦ t1b ⟧ 𝕃⟦ t2 ⟧
𝕃ʳ-simp-step-sound ((x ::ʳ t1) ++ʳ t2) = refl
𝕃ʳ-simp-step-sound ([]ʳ ++ʳ t2) = refl
𝕃ʳ-simp-step-sound ((l ʳ) ++ʳ t2) with keep (is-emptyʳ t2)
𝕃ʳ-simp-step-sound ((l ʳ) ++ʳ t2) | tt , p rewrite p | is-emptyʳ-≡ t2 p | ++[] l = refl
𝕃ʳ-simp-step-sound ((l ʳ) ++ʳ t2) | ff , p rewrite p = refl
𝕃ʳ-simp-step-sound ((mapʳ f t1) ++ʳ t2) with keep (is-emptyʳ t2)
𝕃ʳ-simp-step-sound ((mapʳ f t1) ++ʳ t2) | tt , p rewrite p | is-emptyʳ-≡ t2 p | ++[] (map f 𝕃⟦ t1 ⟧) = refl
𝕃ʳ-simp-step-sound ((mapʳ f t1) ++ʳ t2) | ff , p rewrite p = refl
𝕃ʳ-simp-step-sound (l ʳ) = refl
𝕃ʳ-simp-step-sound (mapʳ f (t1 ++ʳ t2)) = map-append f 𝕃⟦ t1 ⟧ 𝕃⟦ t2 ⟧
𝕃ʳ-simp-step-sound (mapʳ f (l ʳ)) = refl
𝕃ʳ-simp-step-sound (mapʳ f (mapʳ g t)) = map-compose f g 𝕃⟦ t ⟧
𝕃ʳ-simp-step-sound (mapʳ f (x ::ʳ t)) = refl
𝕃ʳ-simp-step-sound (mapʳ f []ʳ) = refl
𝕃ʳ-simp-step-sound (x ::ʳ t) = refl
𝕃ʳ-simp-step-sound []ʳ = refl

𝕃ʳ-simp-sdev-sound : {A : Set}(t : 𝕃ʳ A) → 𝕃⟦ t ⟧ ≡ 𝕃⟦ 𝕃ʳ-simp-sdev t ⟧
𝕃ʳ-simp-sdev-sound (l ʳ) = refl
𝕃ʳ-simp-sdev-sound (t1 ++ʳ t2)
  rewrite sym (𝕃ʳ-simp-step-sound ((𝕃ʳ-simp-sdev t1) ++ʳ (𝕃ʳ-simp-sdev t2))) | 𝕃ʳ-simp-sdev-sound t1 | 𝕃ʳ-simp-sdev-sound t2 = refl
𝕃ʳ-simp-sdev-sound (mapʳ f t1)
  rewrite sym (𝕃ʳ-simp-step-sound (mapʳ f (𝕃ʳ-simp-sdev t1))) | 𝕃ʳ-simp-sdev-sound t1 = refl
𝕃ʳ-simp-sdev-sound (x ::ʳ t1) rewrite 𝕃ʳ-simp-sdev-sound t1 = refl
𝕃ʳ-simp-sdev-sound []ʳ = refl

𝕃ʳ-simp-sound : {A : Set}(t : 𝕃ʳ A)(n : ℕ) → 𝕃⟦ t ⟧ ≡ 𝕃⟦ 𝕃ʳ-simp t n ⟧
𝕃ʳ-simp-sound t 0 = refl
𝕃ʳ-simp-sound t (suc n) rewrite sym (𝕃ʳ-simp-sdev-sound (𝕃ʳ-simp t n)) = 𝕃ʳ-simp-sound t n

module test1 {A B : Set}(f : A → B)(l1 l2 : 𝕃 A) where

  lhs = (mapʳ f (l1 ʳ)) ++ʳ (mapʳ f (l2 ʳ))

  rhs = mapʳ f ((l1 ʳ) ++ʳ (l2 ʳ))

  test-tp : Set
  test-tp = 𝕃⟦ lhs ⟧ ≡ 𝕃⟦ rhs ⟧

  test : test-tp
  test rewrite (𝕃ʳ-simp-sdev-sound rhs) = refl

module test2 {A B : Set}(f : A → B)(l1 l2 l3 : 𝕃 A) where

  lhs = mapʳ f (((l1 ʳ) ++ʳ (l2 ʳ)) ++ʳ (l3 ʳ))

  rhs = 𝕃ʳ-simp lhs 3

  test-tp : Set
  test-tp = 𝕃⟦ lhs ⟧ ≡ 𝕃⟦ rhs ⟧

  test : test-tp
  test = 𝕃ʳ-simp-sound lhs 3

  one-step : 𝕃ʳ B
  one-step = 𝕃ʳ-simp-step lhs

  sdev : 𝕃ʳ B
  sdev = 𝕃ʳ-simp-sdev lhs

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module Sized.SelfRef where

open import Data.Product
open import Data.String.Base

open import Size

open import SizedIO.Object
open import SizedIO.IOObject
open import SizedIO.ConsoleObject

open import SizedIO.Base
open import SizedIO.Console hiding (main)

open import NativeIO

data AMethod : Set where
    print :  AMethod
    m1    :  AMethod
    m2    :  AMethod

AResult : (c : AMethod) → Set
AResult _  =  Unit

aI : Interface
Method  aI  =  AMethod
Result  aI  =  AResult

aC : (i : Size) → Set
aC i = ConsoleObject i aI

--
--  Self Referential: method 'm1' calls method 'm2'
--
{-# NON_TERMINATING #-}
aP :  ∀{i} (s : String) → aC i
method (aP s) print =
  exec1 (putStrLn s) >>
  return (_ , aP s)

method (aP s) m1 =
  exec1 (putStrLn s) >>
  method (aP s) m2  >>= λ{ (_ , c₀) →
  return (_ , c₀) }
method (aP s) m2 =
  return (_ , aP (s ++ "->m2"))

program : String → IOConsole ∞ Unit
program arg =
  let c₀ = aP ("start̄") in
  method c₀ m1  >>= λ{ (_ , c₁) →   --- ===> m1 called, then m2 prints out text
  method c₁ print  >>= λ{ (_ , c₂) →
  exec1 (putStrLn "end")        }}

main : NativeIO Unit
main = translateIOConsole (program "")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Formalization.ImperativePL where

open import Data.Boolean
open import Data.List
import      Lvl
open import Numeral.Natural
open import String
open import Type

Ident : TYPE
data Lit : TYPE
data Stmt : TYPE
data Expr : TYPE
Ty : TYPE
record Context : TYPE₁

Ident = String

data Lit where
  unit : Lit
  bool : Bool → Lit
  nat  : ℕ → Lit

data Expr where
  lit    : Lit → Expr
  ident  : Ident → Expr
  apply  : Expr → Expr → Expr
  func   : Ident → Ty → Expr → Expr
  ifelse : Expr → Expr → Expr → Expr
  stmts  : List(Stmt) → Expr

Ty = Expr

data Stmt where
  expr       : Expr → Stmt
  decl       : Ident → Ty → Stmt
  def        : Ident → Expr → Stmt
  loop       : Stmt → Stmt
  return     : ℕ → Expr → Stmt

record Context where
  inductive
  field
    typing : Ident → Ty → TYPE

open import Logic.Propositional
open import Relator.Equals

add : Ident → Ty → Context → Context
Context.typing (add name ty ctx) a b = (Context.typing ctx a b) ∨ (a ≡ name)

pattern UnitTy   = ident "Unit"
pattern BoolTy   = ident "Bool"
pattern NatTy    = ident "Nat"
pattern FnTy A B = apply (apply (ident "→") A) B

data _⊢ₛ_,_ : Context → Context → Stmt → TYPE₁
data _⊢ₑ_,_=:_ : Context → Context → Expr → Ty → TYPE₁

data _⊢ₛ_,_ where
  expr : ∀{Γ₁ Γ₂}{e}{T} → (Γ₁ ⊢ₑ Γ₂ , e =: T) → (Γ₁ ⊢ₛ Γ₂ , expr e)
  decl : ∀{Γ}{name}{T} → (Γ ⊢ₛ (add name T Γ) , decl name T)
  def  : ∀{Γ₁ Γ₂}{name}{e}{T} → Context.typing Γ₁ name T → (Γ₁ ⊢ₑ Γ₂ , e =: T) → (Γ₁ ⊢ₛ Γ₂ , def name e)
  loop : ∀{Γ₁ Γ₂}{s} → (Γ₁ ⊢ₛ Γ₂ , s) → (Γ₁ ⊢ₛ Γ₁ , loop s)

data _⊢ₑ_,_=:_ where
  unit   : ∀{Γ} → (Γ ⊢ₑ Γ , (lit unit) =: UnitTy)
  bool   : ∀{Γ}{b} → (Γ ⊢ₑ Γ , (lit(bool b)) =: BoolTy)
  nat    : ∀{Γ}{n} → (Γ ⊢ₑ Γ , (lit(nat n)) =: NatTy)
  ident  : ∀{Γ}{i}{ty} → Context.typing Γ i ty → (Γ ⊢ₑ Γ , (ident i) =: ty)
  apply  : ∀{Γ₁ Γ₂ Γ₃}{f x}{A B} → (Γ₁ ⊢ₑ Γ₂ , x =: A) → (Γ₂ ⊢ₑ Γ₃ , f =: FnTy A B) → (Γ₁ ⊢ₑ Γ₃ , (apply f x) =: B)
  func   : ∀{Γ₁ Γ₂}{A B}{var}{body} → ((add var A Γ₁) ⊢ₑ Γ₂ , body =: B) → (Γ₁ ⊢ₑ Γ₁ , (func var A body) =: FnTy A B)
  ifelse : ∀{Γ₁ Γ₂ Γ₃ Γ₄}{b t f}{T} → (Γ₁ ⊢ₑ Γ₂ , b =: BoolTy) → (Γ₂ ⊢ₑ Γ₃ , t =: T) → (Γ₂ ⊢ₑ Γ₄ , f =: T) → (Γ₁ ⊢ₑ Γ₂ , (ifelse b t f) =: T)
  -- stmts∅ : ∀{Γ}{n} → (Γ ⊢ₑ Γ , (stmts ) =: NatTy)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- Tactic for proving coprimality.
-- Finds Coprime hypotheses in the context.
module Tactic.Nat.Coprime where

import Agda.Builtin.Nat as Builtin

open import Prelude
open import Control.Monad.Zero
open import Control.Monad.State
open import Container.List
open import Container.Traversable
open import Numeric.Nat
open import Tactic.Reflection
open import Tactic.Reflection.Parse
open import Tactic.Reflection.Quote

open import Tactic.Nat.Coprime.Problem
open import Tactic.Nat.Coprime.Decide
open import Tactic.Nat.Coprime.Reflect

private
  Proof : Problem → Env → Set
  Proof Q ρ with canProve Q
  ... | true  = ⟦ Q ⟧p ρ
  ... | false = ⊤

  erasePrf : ∀ Q {ρ} → ⟦ Q ⟧p ρ → ⟦ Q ⟧p ρ
  erasePrf ([] ⊨ a ⋈ b) Ξ = eraseEquality Ξ
  erasePrf (ψ ∷ Γ ⊨ φ) Ξ = λ H → erasePrf (Γ ⊨ φ) (Ξ H)

  proof : ∀ Q ρ → Proof Q ρ
  proof Q ρ with canProve Q | sound Q
  ... | true  | prf = erasePrf Q (prf refl ρ)
  ... | false | _   = _

  -- For the error message

  unquoteE : List Term → Exp → Term
  unquoteE ρ (atom x) = fromMaybe (lit (nat 0)) (index ρ x)
  unquoteE ρ (e ⊗ e₁) = def₂ (quote _*_) (unquoteE ρ e) (unquoteE ρ e₁)

  unquoteF : List Term → Formula → Term
  unquoteF ρ (a ⋈ b) = def₂ (quote Coprime) (unquoteE ρ a) (unquoteE ρ b)

macro
  auto-coprime : Tactic
  auto-coprime ?hole = withNormalisation true $ do
    goal ← inferType ?hole
    ensureNoMetas goal
    cxt  ← reverse <$> getContext
    (_ , Hyps , Q) , ρ ← runParse (parseProblem (map unArg cxt) goal)
    unify ?hole (def (quote proof) $ map vArg (` Q ∷ quotedEnv ρ ∷ Hyps))
      <|> do
        case Q of λ where
          (Γ ⊨ φ) → typeError (strErr "Cannot prove" ∷
                               termErr (unquoteF ρ φ) ∷
                               strErr "from" ∷
                               punctuate (strErr "and") (map (termErr ∘ unquoteF ρ) Γ))

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude