text:
open import Relation.Binary using (Rel; Reflexive; Trans)
open import Level using (Level; _⊔_; suc)
open import Data.Product using (Σ; _×_; _,_; Σ-syntax;  ∃-syntax; proj₁; proj₂)

data Star {t r} {T : Set t} (R : Rel T r) : Rel T (t ⊔ r) where
  ε   : Reflexive (Star R)
  _▻_ : Trans (Star R) R (Star R)

_▻▻_ : ∀ {t r} {T : Set t} {R : Rel T r} {M L N : T}
  → Star R M L
  → Star R L N
  → Star R M N
ML ▻▻ ε = ML
ML ▻▻ (LL′ ▻ L′N) = (ML ▻▻ LL′) ▻ L′N

Semi-Confluence : ∀ {t r} {T : Set t} (R : Rel T r) → Set (t ⊔ r)
Semi-Confluence R = ∀ {M A B}
  →              R M A → Star R M B
    --------------------------------
  → ∃[ N ] (Star R A N × Star R B N)

Confluence : ∀ {t r} {T : Set t} (R : Rel T r) → Set (t ⊔ r)
Confluence R = ∀ {M A B}
  →         Star R M A → Star R M B
    --------------------------------
  → ∃[ N ] (Star R A N × Star R B N)

semi-to-confluence : ∀ {t r} {T : Set t} {R : Rel T r} →
  Semi-Confluence R → Confluence R
semi-to-confluence sc {B = B} ε M*B = B , M*B , ε
semi-to-confluence sc (M*M′ ▻ M′A) M*B
    with semi-to-confluence sc M*M′ M*B
... | N , M′*N , B*N
    with sc M′A M′*N
... | N′ , A*N′ , N*N′
    = N′ , A*N′ , B*N ▻▻ N*N′

Z : ∀ {t r} {T : Set t} (R : Rel T r) → Set (t ⊔ r)
Z {t}{r}{T} R =
  Σ[ _* ∈ (T → T) ]
      (∀ {A B : T} → R A B → Star {t}{r} R B     (A *))
    × (∀ {A B : T} → R A B → Star {t}{r} R (A *) (B *))

z-monotonic : ∀ {t r} {T : Set t} {R : Rel T r}
  → (z : Z R)
    ------------------------------------------
  → (∀ {A B} → Star R A B
             → Star R (proj₁ z A) (proj₁ z B))
z-monotonic z ε = ε
z-monotonic z@(_* , Z₁ , Z₂) (A*A′ ▻ A′B) = z-monotonic z A*A′ ▻▻ Z₂ A′B

z-semi-confluence : ∀ {t r} {T : Set t} {R : Rel T r} →
  Z R → Semi-Confluence R
z-semi-confluence   (_* , Z₁ , Z₂) {A = A} MA ε = A , ε , (ε ▻ MA)
z-semi-confluence z@(_* , Z₁ , Z₂) MA (_▻_ {j = M′} M*M′ M′B) =
   M′ * , Z₁ MA ▻▻ z-monotonic z M*M′ , Z₁ M′B

z-confluence : ∀ {t r} {T : Set t} {R : Rel T r} →
  Z R → Confluence R
z-confluence z = semi-to-confluence (z-semi-confluence z)

max_stars_repo_name: iwilare/church-rosser

max_issues_repo_name: iwilare/church-rosser

max_forks_repo_name: iwilare/church-rosser


text:
module Basic.EqvSemantics where

open import Data.Vec
open import Function
open import Data.Product
open import Data.Maybe

open import Utils.Decidable
open import Basic.AST
open import Basic.BigStep
open import Basic.SmallStep

{-

Equivalence of big step and small step semantics (Theorem 2.26 in the book).

The main difference from the book is the proof for the

  ⟨ S , s ⟩ k ⟶ s' → ⟨ S , s ⟩⟱ s'

direction. The book does case analysis directly on the transition the
"cons" case of the computation sequence, and then uses Lemma 2.19 (which
I named "seq-split" in the SmallStep module) to split the sequence into
two parts corresponding to the two parts of a composite statement.

The problem with this is that it relies on the usual well-ordering of natural
numbers, and it's not immediately structurally recursive. In other words, it relies
on the fact that the resulting parts of a split sequence are both shorter than the
original sequence.

However, the book omits the proof that no splitting ever produces computation
sequences of length zero. This is required for the recursion to be well-founded,
and in Agda we would indeed have to prove this too.

It's simpler to use "prepend". It essentially digs down to the leftmost "edge" of
a small-step transition, and composes it with a big-step derivation. It's evidently
structurally recursive and I find it a bit neater than the proof in the book.

-}

Small≡Big : ∀ {n}{S : St n}{s s'} → ⟨ S , s ⟩⟱ s' ⇔ ⟨ S , s ⟩⟶* s'
Small≡Big {n} = to , from ∘ proj₂
  where
  to : ∀ {S s s'} → ⟨ S , s ⟩⟱ s' → ⟨ S , s ⟩⟶* s'
  to ass                 = , ass stop
  to skip                = , skip stop
  to (A , B)             = , append (proj₂ $ to A) (proj₂ $ to B)
  to (if-true x p)       = , if-true x ∷ proj₂ (to p)
  to (if-false x p)      = , if-false x ∷ proj₂ (to p)
  to (while-true x p p₁) = , while ∷ if-true x ∷ append (proj₂ $ to p) (proj₂ $ to p₁)
  to (while-false x)     = , while ∷ if-false x ∷ skip stop

  mutual
    prepend :
      ∀ {s₁ s₂ s₃}{S₁ S₂ : St n}
      → ⟨ S₁ , s₁ ⟩⟶⟨ S₂ , s₂ ⟩
      → ⟨ S₂ , s₂ ⟩⟱ s₃
      → ⟨ S₁ , s₁ ⟩⟱ s₃
    prepend (p1 ◄) (p2 , p3)            = prepend p1 p2 , p3
    prepend (x ∙) p2                    = from (x stop) , p2
    prepend (if-true x) p2              = if-true x p2
    prepend (if-false x) p2             = if-false x p2
    prepend while (if-true x (p2 , p3)) = while-true x p2 p3
    prepend while (if-false x skip)     = while-false x

    from : ∀ {k S s s'} → ⟨ S , s ⟩ k ⟶ s' → ⟨ S , s ⟩⟱ s'
    from (ass stop)  = ass
    from (skip stop) = skip
    from (x ∷ p)     = prepend x (from p)

ext: agda

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


text:
module Categories.Comonad where

open import Level using (_⊔_)

open import Categories.Category using (Category)
open import Categories.Functor hiding (_≡_; assoc; identityˡ; identityʳ)
open import Categories.NaturalTransformation renaming (id to idN)

record Comonad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  field
    F : Endofunctor C
    ε : NaturalTransformation F id
    δ : NaturalTransformation F (F ∘ F)

  open Functor F

  field
    .assoc     : (δ ∘ʳ F) ∘₁ δ ≡ (F ∘ˡ δ) ∘₁ δ
    .identityˡ : (F ∘ˡ ε) ∘₁ δ ≡ idN
    .identityʳ : (ε ∘ʳ F) ∘₁ δ ≡ idN

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: copumpkin/categories

max_forks_repo_name: copumpkin/categories


text:
-- A module which imports every Web.Semantic module.

module Web.Semantic.Everything where

import Web.Semantic.DL.ABox
import Web.Semantic.DL.ABox.Interp
import Web.Semantic.DL.ABox.Interp.Meet
import Web.Semantic.DL.ABox.Interp.Morphism
import Web.Semantic.DL.ABox.Model
import Web.Semantic.DL.ABox.Skolemization
import Web.Semantic.DL.Category
import Web.Semantic.DL.Category.Composition
import Web.Semantic.DL.Category.Morphism
import Web.Semantic.DL.Category.Object
import Web.Semantic.DL.Category.Properties
import Web.Semantic.DL.Category.Properties.Composition
import Web.Semantic.DL.Category.Properties.Composition.Assoc
import Web.Semantic.DL.Category.Properties.Composition.LeftUnit
import Web.Semantic.DL.Category.Properties.Composition.Lemmas
import Web.Semantic.DL.Category.Properties.Composition.RespectsEquiv
import Web.Semantic.DL.Category.Properties.Composition.RespectsWiring
import Web.Semantic.DL.Category.Properties.Composition.RightUnit
import Web.Semantic.DL.Category.Properties.Equivalence
import Web.Semantic.DL.Category.Properties.Tensor
import Web.Semantic.DL.Category.Properties.Tensor.AssocNatural
import Web.Semantic.DL.Category.Properties.Tensor.Coherence
import Web.Semantic.DL.Category.Properties.Tensor.Functor
import Web.Semantic.DL.Category.Properties.Tensor.Isomorphisms
import Web.Semantic.DL.Category.Properties.Tensor.Lemmas
import Web.Semantic.DL.Category.Properties.Tensor.RespectsEquiv
import Web.Semantic.DL.Category.Properties.Tensor.RespectsWiring
import Web.Semantic.DL.Category.Properties.Tensor.SymmNatural
import Web.Semantic.DL.Category.Properties.Tensor.UnitNatural
import Web.Semantic.DL.Category.Tensor
import Web.Semantic.DL.Category.Unit
import Web.Semantic.DL.Category.Wiring
import Web.Semantic.DL.Concept
import Web.Semantic.DL.Concept.Model
import Web.Semantic.DL.Concept.Skolemization
import Web.Semantic.DL.FOL
import Web.Semantic.DL.FOL.Model
import Web.Semantic.DL.Integrity
import Web.Semantic.DL.Integrity.Closed
import Web.Semantic.DL.Integrity.Closed.Alternate
import Web.Semantic.DL.Integrity.Closed.Properties
import Web.Semantic.DL.KB
import Web.Semantic.DL.KB.Model
import Web.Semantic.DL.KB.Skolemization
import Web.Semantic.DL.Role
import Web.Semantic.DL.Role.Model
import Web.Semantic.DL.Role.Skolemization
import Web.Semantic.DL.Sequent
import Web.Semantic.DL.Sequent.Model
import Web.Semantic.DL.Signature
import Web.Semantic.DL.TBox
import Web.Semantic.DL.TBox.Interp
import Web.Semantic.DL.TBox.Interp.Morphism
import Web.Semantic.DL.TBox.Minimizable
import Web.Semantic.DL.TBox.Model
import Web.Semantic.DL.TBox.Skolemization

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


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

module Generics.Mu where

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

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

⟦_⟧IndArgω : ConDesc P V I → (⟦ P , I ⟧xtel → Setω) → ⟦ P , V ⟧xtel → Setω
⟦ var f    ⟧IndArgω X (p , v) = X (p , f (p , v))
⟦ π (n , ai) S C ⟧IndArgω X (p , v) = (s : < relevance ai > S (p , v)) → ⟦ C ⟧IndArgω X (p , v , s)
⟦ A ⊗ B    ⟧IndArgω X pv      = ⟦ A ⟧IndArgω X pv ×ω ⟦ B ⟧IndArgω X pv

⟦_⟧Conω : ConDesc P V I → (⟦ P , I ⟧xtel → Setω) → ⟦ P , V & I ⟧xtel → Setω
⟦ var f ⟧Conω X (p , v , i) = Liftω (i ≡ f (p , v))
⟦ π (n , ai) S C ⟧Conω X (p , v , i) = Σω (< relevance ai > S _) λ s → ⟦ C ⟧Conω X (p , (v , s) , i)
⟦ A ⊗ B ⟧Conω X (p , v , i) = ⟦ A ⟧IndArgω X (p , v) ×ω ⟦ B ⟧Conω X (p , v , i)

⟦_⟧Dataω : DataDesc P I n → (⟦ P , I ⟧xtel → Setω) → ⟦ P , I ⟧xtel → Setω
⟦_⟧Dataω {n = n} D X (p , i) = Σω (Fin n) λ k → ⟦ lookupCon D k ⟧Conω X (p , tt , i)

data μ (D : DataDesc P I n) (pi : ⟦ P , I ⟧xtel) : Setω where
  ⟨_⟩ : ⟦ D ⟧Dataω (μ D) pi → μ D pi

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


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

module Cubical.Data.FinSet.Binary.Small.Properties where

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

open import Cubical.Functions.Embedding
open import Cubical.Functions.Involution

open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Data.FinSet.Binary.Small.Base

open import Cubical.Data.Bool
import Cubical.Data.FinSet.Binary.Large as FS
open FS using (isBinary)

open import Cubical.Foundations.Univalence.Universe Binary El un (λ _ → refl)

private
  variable
    ℓ : Level
    B : Type ℓ

isBinaryEl : ∀ b → isBinary (El b)
isBinaryEl ℕ₂ = ∣ idEquiv Bool ∣
isBinaryEl (un b c e i)
  = squash
      (transp (λ j → ∥ Bool ≃ ua e (i ∧ j) ∥) (~ i) (isBinaryEl b))
      (transp (λ j → ∥ Bool ≃ ua e (i ∨ ~ j) ∥) i (isBinaryEl c))
      i

isBinaryEl' : ∀ ℓ b → isBinary (Lift {j = ℓ} (El b))
isBinaryEl' ℓ ℕ₂ = ∣ LiftEquiv ∣
isBinaryEl' ℓ (un b c e i)
  = squash
      (transp (λ j → ∥ Bool ≃ Lift {j = ℓ} (ua e (i ∧ j)) ∥) (~ i) (isBinaryEl' ℓ b))
      (transp (λ j → ∥ Bool ≃ Lift {j = ℓ} (ua e (i ∨ ~ j)) ∥) i (isBinaryEl' ℓ c))
      i

isPropIsSetEl : isOfHLevelDep 1 (λ b → isSet (El b))
isPropIsSetEl = isOfHLevel→isOfHLevelDep 1 (λ b → isPropIsSet)

isSetEl : ∀ b → isSet (El b)
isSetEl ℕ₂ = isSetBool
isSetEl (un b c e i)
  = isPropIsSetEl (isSetEl b) (isSetEl c) (un b c e) i

isGroupoidBinary : isGroupoid Binary
isGroupoidBinary b c = isOfHLevelRetract 2 fun inv leftInv sub
  where
  open Iso (pathIso b c)
  sub : isSet (El b ≡ El c)
  sub = isOfHLevel≡ 2 (isSetEl b) (isSetEl c)

module Reflection where
  bigger : Binary → FS.Binary _
  bigger b = El b , isBinaryEl b

  open Iso

  lemma : ∀(B : Type₀) → ∥ Bool ≃ B ∥ → Σ[ b ∈ Binary ] El b ≃ B
  lemma B = rec Sprp (_,_ ℕ₂)
    where
    Fprp : isProp (fiber El B)
    Fprp = isEmbedding→hasPropFibers isEmbeddingEl B

    Sprp : isProp (Σ[ b ∈ Binary ] El b ≃ B)
    Sprp = isOfHLevelRetract 1 (map-snd ua) (map-snd pathToEquiv)
             (λ{ (A , e) → ΣPathP (refl , pathToEquiv-ua e) }) Fprp

  smaller : FS.Binary ℓ-zero → Binary
  smaller (B , tp) = lemma B tp .fst

  bigger-smaller : ∀ p → bigger (smaller p) ≡ p
  bigger-smaller (B , tp)
    = ΣPathP (b≡B , ∥∥-isPropDep (λ B → Bool ≃ B) (isBinaryEl b) tp b≡B)
    where
    b = smaller (B , tp)
    b≡B = ua (lemma B tp .snd)

  smaller-bigger : ∀ b → smaller (bigger b) ≡ b
  smaller-bigger b = equivIso _ _ .inv (lemma (El b) (isBinaryEl b) .snd)

  reflectIso : Iso Binary (FS.Binary ℓ-zero)
  reflectIso .fun = bigger
  reflectIso .inv = smaller
  reflectIso .rightInv = bigger-smaller
  reflectIso .leftInv = smaller-bigger

reflect : Binary ≃ FS.Binary ℓ-zero
reflect = isoToEquiv Reflection.reflectIso

structureᵤ : FS.BinStructure Binary
structureᵤ = λ where
    .base → bs .base .lower
    .loop i → bs .loop i .lower
    .loop² i j → bs .loop² i j .lower
    .trunc → isGroupoidBinary
  where
  open FS.BinStructure

  path : Lift Binary ≡ FS.Binary _
  path = ua (compEquiv (invEquiv LiftEquiv) reflect)

  bs : FS.BinStructure (Lift Binary)
  bs = subst⁻ FS.BinStructure path FS.structure₀

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


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

module FinEquivEquivTimes where

open import Data.Product using (_×_; proj₁; proj₂)

open import Equiv using (refl∼; sym∼; sym≃; _⊎≃_; id≃; _≃_; _●_; _×≃_; qinv)

open import FinEquivPlusTimes using (F0≃⊥; Fin1≃⊤; module Plus; module Times)
open Plus using (⊎≃+; +≃⊎)
open Times using (×≃*; *≃×)

open import FinEquivTypeEquiv
  using (_fin≃_; module PlusE; module TimesE; module PlusTimesE)
open PlusE using (_+F_; unite+; uniti+; unite+r; uniti+r; assocr+; assocl+;
                 swap+; sswap+)
open TimesE using (_*F_; unite*; uniti*; unite*r; uniti*r; assocr*; assocl*;
                  swap*; sswap*)
open PlusTimesE using (distz; factorz; distzr; factorzr;
                       dist; factor; distl; factorl)
open import EquivEquiv
open import TypeEquiv
  using (unite⋆equiv; unite⋆′equiv; assocl⋆equiv)

open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Fin using (Fin)
open import Data.Sum using (_⊎_)
open import Data.Product using (_,_)
import Relation.Binary.PropositionalEquality as P using (refl)

import TypeEquivEquiv as T
  using (id×id≋id; ×●≋●×; _×≋_; sym≃-distrib×;
      unite⋆-nat; assocl⋆-nat;
      [g*1]●[1*f]≋[1*f]●[g*1]; unite⋆′-nat)

------------------------------------------------------------------------------
-- Equivalences for the multiplicative structure

id1≃ : Fin 1 ≃ Fin 1
id1≃ = id≃ {A = Fin 1}

id*id≋id : ∀ {m n : ℕ} →
    id≃ {A = Fin m} *F id≃ {A = Fin n} ≋ id≃
id*id≋id {m} {n} =
  let em = id≃ {A = Fin m} in
  let en = id≃ {A = Fin n} in
  let em×en = id≃ {A = Fin m × Fin n} in
  let em*n = id≃ {A = Fin (m * n)} in
  let f≋ = id≋ {x = ×≃* {m} {n}} in
  let g≋ = id≋ {x = *≃× {m} {n}} in
  begin (
  em *F en
    ≋⟨ id≋ ⟩
  ×≃* ● (em ×≃ en) ● *≃×
    ≋⟨ f≋ ◎ (T.id×id≋id ◎ g≋) ⟩
  ×≃* ● id≃ {A = Fin m × Fin n} ● *≃×
    ≋⟨ f≋ ◎ lid≋ {f = *≃×} ⟩
  ×≃* {m} ● *≃×
    ≋⟨ rinv≋ (×≃* {m}) ⟩
  em*n ∎)
  where open ≋-Reasoning

intro-inv-r* : {m n : ℕ} {B : Set} (f : (Fin m × Fin n) ≃ B) → f ≋ (f ● *≃×) ● ×≃*
intro-inv-r* f =
  begin (
    f
      ≋⟨ sym≋ rid≋ ⟩
    f ● id≃
      ≋⟨ id≋ {x = f} ◎ sym≋ (linv≋ ×≃*) ⟩
    f ● (*≃× ● ×≃*)
      ≋⟨ ●-assocl  ⟩
    (f ● *≃×) ● ×≃* ∎)
  where open ≋-Reasoning

*●≋●* : {A B C D E F : ℕ} →
  {f : A fin≃ C} {g : B fin≃ D} {h : C fin≃ E} {i : D fin≃ F} →
  (h ● f) *F (i ● g) ≋ (h *F i) ● (f *F g)
*●≋●* {f = f} {g} {h} {i} =
  let f≋ = id≋ {x = ×≃*} in
  let g≋ = id≋ {x = *≃×} in
  let id≋fg = id≋ {x = f ×≃ g} in
  begin (
    (h ● f) *F (i ● g)
      ≋⟨ id≋ ⟩
    ×≃* ● ((h ● f) ×≃ (i ● g)) ● *≃×
      ≋⟨ f≋ ◎ (T.×●≋●× ◎ g≋) ⟩ -- the real work, rest is shuffling
    ×≃* ● ((h ×≃ i) ● (f ×≃ g)) ● *≃×
      ≋⟨ ●-assocl ⟩
    (×≃* ● ((h ×≃ i) ● (f ×≃ g))) ● *≃×
      ≋⟨ ●-assocl ◎ g≋ ⟩
    ((×≃* ● h ×≃ i) ● f ×≃ g) ● *≃×
      ≋⟨ ((f≋ ◎ intro-inv-r* (h ×≃ i)) ◎ id≋fg) ◎ g≋ ⟩
    ((×≃* ● (h ×≃ i ● *≃×) ● ×≃*) ● f ×≃ g) ● *≃×
      ≋⟨ (●-assocl ◎ id≋fg) ◎ g≋ ⟩
    (((×≃* ● (h ×≃ i ● *≃×)) ● ×≃*) ● f ×≃ g) ● *≃×
      ≋⟨ id≋ ⟩ -- the left part is done, show it
    ((h *F i ● ×≃*) ● f ×≃ g) ● *≃×
      ≋⟨ ●-assoc {f = f ×≃ g} {×≃*} {h *F i} ◎ g≋ ⟩
    (h *F i ● (×≃* ● f ×≃ g)) ● *≃×
      ≋⟨ ●-assoc {f = *≃×} {×≃* ● f ×≃ g} {h *F i}⟩
    (h *F i) ● ((×≃* ● f ×≃ g) ● *≃×)
      ≋⟨ id≋ {x = h *F i} ◎ ●-assoc {f = *≃×} {f ×≃ g} {×≃*}⟩
    (h *F i) ● (f *F g) ∎)
  where open ≋-Reasoning

_*≋_ : {A B C D : ℕ} {f₁ g₁ : A fin≃ B} {f₂ g₂ : C fin≃ D} →
  (f₁ ≋ g₁) → (f₂ ≋ g₂) → (f₁ *F f₂ ≋ g₁ *F g₂)
_*≋_ {A} {B} {C} {D} {f₁} {g₁} {f₂} {g₂} f₁≋g₁ f₂≋g₂ =
  let f≋ = id≋ {x = ×≃*} in
  let g≋ = id≋ {x = *≃×} in
  begin (
    f₁ *F f₂
      ≋⟨ id≋ ⟩
    ×≃* ● (f₁ ×≃ f₂) ● *≃×
      ≋⟨ f≋ ◎ (T._×≋_ f₁≋g₁ f₂≋g₂ ◎ g≋) ⟩
    ×≃* ● (g₁ ×≃ g₂) ● *≃×
      ≋⟨ id≋ ⟩
    g₁ *F g₂ ∎)
  where open ≋-Reasoning

unite⋆-nat : {m n : ℕ} {f : m fin≃ n} →
  unite* ● (id1≃ *F f) ≋ f ● unite*
unite⋆-nat {m} {n} {f} =
  begin (
    unite* ● (id1≃ *F f)
      ≋⟨ id≋ ⟩
    (unite⋆equiv ● (Fin1≃⊤ ×≃ id≃) ● *≃×) ● ×≃* ● ((id≃ ×≃ f) ● *≃×)
      ≋⟨ ●-assocl {f = (id≃ ×≃ f) ● *≃×} {×≃*} {unite⋆equiv ● (Fin1≃⊤ ×≃ id≃) ● *≃×} ⟩
    ((unite⋆equiv ● ((Fin1≃⊤ ×≃ id≃) ● *≃×)) ● ×≃*) ● ((id≃ ×≃ f) ● *≃×)
      ≋⟨ (●-assocl ◎ id≋) ◎ id≋ ⟩
    (((unite⋆equiv ● (Fin1≃⊤ ×≃ id≃)) ● *≃×) ● ×≃*) ● (id≃ ×≃ f) ● *≃×
      ≋⟨ sym≋ (intro-inv-r* (unite⋆equiv ● (Fin1≃⊤ ×≃ id≃))) ◎ id≋ ⟩
    (unite⋆equiv ● (Fin1≃⊤ ×≃ id≃)) ● (id≃ ×≃ f) ● *≃×
      ≋⟨ ●-assocl ⟩
    ((unite⋆equiv ● (Fin1≃⊤ ×≃ id≃)) ● (id≃ ×≃ f)) ● *≃×
      ≋⟨ ●-assoc ◎ id≋ ⟩
    (unite⋆equiv ● (Fin1≃⊤ ×≃ id≃) ● (id≃ ×≃ f)) ● *≃×
      ≋⟨ (id≋ ◎ (T.[g*1]●[1*f]≋[1*f]●[g*1] {f = f} {Fin1≃⊤})) ◎ id≋ ⟩
    (unite⋆equiv ● ((id≃ ×≃ f) ● (Fin1≃⊤ ×≃ id≃))) ● *≃×
      ≋⟨ ●-assocl ◎ id≋ ⟩
    ((unite⋆equiv ● (id≃ ×≃ f)) ● (Fin1≃⊤ ×≃ id≃)) ● *≃×
      ≋⟨ ●-assoc ⟩
    (unite⋆equiv ● (id≃ ×≃ f)) ● (Fin1≃⊤ ×≃ id≃) ● *≃×
      ≋⟨ T.unite⋆-nat ◎ id≋ ⟩
    (f ● unite⋆equiv) ● (Fin1≃⊤ ×≃ id≃) ● *≃×
      ≋⟨ ●-assoc ⟩
    f ● unite⋆equiv ● (Fin1≃⊤ ×≃ id≃) ● *≃×
      ≋⟨ id≋ ⟩
    f ● unite* ∎)
  where open ≋-Reasoning

-- sym≃ distributes over *F
sym*F : ∀ {A B C D} {f : A fin≃ B} {g : C fin≃ D} →
  sym≃ (f *F g) ≋ sym≃ f *F sym≃ g
sym*F {f = f} {g = g} =
  begin (
    sym≃ (f *F g)
      ≋⟨ id≋ ⟩
    sym≃ (×≃* ● (f ×≃ g ● *≃×))
      ≋⟨ sym≃● ⟩
    sym≃ (f ×≃ g ● *≃×) ● sym≃ ×≃*
      ≋⟨ sym≃● ◎ id≋ ⟩
    (sym≃ *≃× ● sym≃ (f ×≃ g)) ● sym≃ ×≃*
      ≋⟨ (id≋ ◎ T.sym≃-distrib×) ◎ id≋ ⟩
    (sym≃ *≃× ● (sym≃ f ×≃ sym≃ g)) ● sym≃ ×≃*
      ≋⟨ ●-assoc ⟩
    sym≃ *≃× ● ((sym≃ f ×≃ sym≃ g) ● sym≃ ×≃*)
      ≋⟨ id≋ ⟩
    sym≃ f *F sym≃ g ∎)
  where open ≋-Reasoning

uniti⋆-nat : ∀ {A B} {f : A fin≃ B} →
  uniti* ● f ≋ (id1≃ *F f) ● uniti*
uniti⋆-nat {f = f} =
  begin (
    uniti* ● f
      ≋⟨ id≋ ⟩
    sym≃ unite* ● sym≃ (sym≃ f)
      ≋⟨ sym≋ sym≃● ⟩
    sym≃ (sym≃ f ● unite*)
      ≋⟨ flip-sym≋ unite⋆-nat ⟩
    sym≃ (unite* ● (id1≃ *F sym≃ f))
      ≋⟨ sym≃● ⟩
    sym≃ (id1≃ *F sym≃ f) ● uniti*
      ≋⟨  sym*F ◎ id≋ {x = uniti*} ⟩
    (id1≃ *F sym≃ (sym≃ f)) ● uniti*
      ≋⟨ id≋ ⟩
    (id1≃ *F f) ● uniti* ∎)
  where open ≋-Reasoning

unite⋆r-nat : {m n : ℕ} {f : m fin≃ n} →
  unite*r ● (f *F id1≃) ≋ f ● unite*r
unite⋆r-nat {m} {n} {f} =
  let 1*⊥ = id≃ ×≃ Fin1≃⊤ in
  let f*1 = f ×≃ id≃ in
  let g≋ = id≋ {x = *≃×} in
  let rhs≋ = id≋ {x = f*1 ● *≃×} in
  begin (
    unite*r ● (f *F id1≃)
      ≋⟨ id≋ ⟩
    (unite⋆′equiv ● 1*⊥ ● *≃×) ● ×≃* ● (f*1 ● *≃×)
      ≋⟨ ●-assocl ⟩
    ((unite⋆′equiv ● 1*⊥ ● *≃×) ● ×≃*) ● (f*1 ● *≃×)
      ≋⟨ (●-assocl ◎ id≋) ◎ id≋ ⟩
    (((unite⋆′equiv ● 1*⊥) ● *≃×) ● ×≃*) ● (f*1 ● *≃×)
      ≋⟨ sym≋ (intro-inv-r* (unite⋆′equiv ● 1*⊥)) ◎ rhs≋ ⟩
    (unite⋆′equiv ● 1*⊥) ● (f*1 ● *≃×)
      ≋⟨ trans≋ ●-assocl (●-assoc ◎ id≋) ⟩
    (unite⋆′equiv ● (1*⊥ ● f*1)) ● *≃×
      ≋⟨ (id≋ {x = unite⋆′equiv} ◎ sym≋ (T.[g*1]●[1*f]≋[1*f]●[g*1] {f = Fin1≃⊤} {f})) ◎ g≋ ⟩
    (unite⋆′equiv ● (f ×≃ id≃) ● (id≃ ×≃ Fin1≃⊤)) ● *≃× -- the id≃ are at different types!
      ≋⟨ ●-assocl ◎ id≋ ⟩
    ((unite⋆′equiv ● (f ×≃ id≃)) ● (id≃ ×≃ Fin1≃⊤)) ● *≃×
      ≋⟨ ●-assoc ⟩
    (unite⋆′equiv ● (f ×≃ id≃)) ● (id≃ ×≃ Fin1≃⊤) ● *≃×
      ≋⟨ T.unite⋆′-nat ◎ id≋ {x = (id≃ ×≃ Fin1≃⊤) ● *≃×} ⟩
    (f ● unite⋆′equiv) ● (id≃ ×≃ Fin1≃⊤) ● *≃×
      ≋⟨ ●-assoc ⟩ -- assoc * defn
    f ● unite*r ∎)
  where open ≋-Reasoning

uniti₊r-nat : {m n : ℕ} {f : m fin≃ n} →
    uniti*r ● f ≋ (f *F id1≃) ● uniti*r
uniti₊r-nat {f = f} =
  begin (
    uniti*r ● f
      ≋⟨ id≋ ⟩
     sym≃ unite*r ● sym≃ (sym≃ f)
      ≋⟨ sym≋ sym≃● ⟩
     sym≃ (sym≃ f ● unite*r)
      ≋⟨ flip-sym≋ unite⋆r-nat ⟩
     sym≃ (unite*r ● (sym≃ f *F id1≃))
      ≋⟨ sym≃● ⟩
     sym≃ (sym≃ f *F id1≃) ● uniti*r
      ≋⟨ sym*F ◎ id≋ {x = uniti*r} ⟩
     (sym≃ (sym≃ f) *F id1≃) ● uniti*r
      ≋⟨ id≋ ⟩
    (f *F id1≃) ● uniti*r ∎)
  where open ≋-Reasoning

-- assocl* is the one which is defined directly (?)
assocl⋆-nat : {m n o m' n' o' : ℕ}
    {f : m fin≃ m'} {g : n fin≃ n'} {h : o fin≃ o'} →
    assocl* {m'} {n'} {o'} ● (f *F (g *F h)) ≋
    ((f *F g) *F h) ● assocl* {m} {n} {o}
-- expand the definitions right away, the pattern is clear
assocl⋆-nat {m} {n} {o} {m'} {n'} {o'} {f} {g} {h} =
  let αmno' = assocl⋆equiv {Fin m'} {Fin n'} {Fin o'} in
  let αmno = assocl⋆equiv {Fin m} {Fin n} {Fin o} in
  begin (
  (×≃* ● ×≃* ×≃ id≃ ● αmno' ● id≃ ×≃ *≃× ● *≃×) ●
            ×≃* ● ((f ×≃ (×≃* ● g ×≃ h ● *≃×)) ● *≃×)
    ≋⟨ ●-assocl ⟩
  ((×≃* ● ×≃* ×≃ id≃ ● assocl⋆equiv ● id≃ ×≃ *≃× ● *≃×) ● ×≃*) ●
            (f ×≃ (×≃* ● g ×≃ h ● *≃×) ● *≃×)
    ≋⟨ ((id≋ ◎ (id≋ ◎ ●-assocl)) ◎ id≋) ◎ id≋ ⟩
  ((×≃* ● ×≃* ×≃ id≃ ● (assocl⋆equiv ● id≃ ×≃ *≃×) ● *≃×) ● ×≃*) ●
            (f ×≃ (×≃* ● g ×≃ h ● *≃×) ● *≃×)
    ≋⟨ ((id≋ ◎ ●-assocl) ◎ id≋) ◎ id≋ ⟩
  ((×≃* ● (×≃* ×≃ id≃ ● (assocl⋆equiv ● id≃ ×≃ *≃×)) ● *≃×) ● ×≃*) ●
            (f ×≃ (×≃* ● g ×≃ h ● *≃×) ● *≃×)
    ≋⟨ (●-assocl ◎ id≋) ◎ id≋ ⟩
  (((×≃* ● (×≃* ×≃ id≃ ● (assocl⋆equiv ● id≃ ×≃ *≃×))) ● *≃×) ● ×≃*) ●
            (f ×≃ (×≃* ● g ×≃ h ● *≃×) ● *≃×)
    ≋⟨ sym≋ (intro-inv-r* (×≃* ● (×≃* ×≃ id≃ ● (assocl⋆equiv ● id≃ ×≃ *≃×)))) ◎ id≋ ⟩
   (×≃* ● (×≃* ×≃ id≃ ● (assocl⋆equiv ● id≃ ×≃ *≃×))) ●
          (f ×≃ (×≃* ● g ×≃ h ● *≃×) ● *≃×)
    ≋⟨ ●-assoc ⟩
  ×≃* ● (×≃* ×≃ id≃ ● (assocl⋆equiv ● id≃ ×≃ *≃×)) ●
          (f ×≃ (×≃* ● g ×≃ h ● *≃×) ● *≃×)
    ≋⟨ id≋ ◎ (●-assocl ◎ id≋) ⟩
  ×≃* ● ((×≃* ×≃ id≃ ● assocl⋆equiv) ● id≃ ×≃ *≃×) ●
          (f ×≃ (×≃* ● g ×≃ h ● *≃×) ● *≃×)
    ≋⟨ id≋ ◎ ●-assoc ⟩
  ×≃* ● (×≃* ×≃ id≃ ● assocl⋆equiv) ● (id≃ ×≃ *≃× ●
          (f ×≃ (×≃* ● g ×≃ h ● *≃×) ● *≃×))
    ≋⟨ id≋ ◎ (id≋ ◎ ●-assocl) ⟩
  ×≃* ● (×≃* ×≃ id≃ ● assocl⋆equiv) ● ((id≃ ×≃ *≃× ●
          f ×≃ (×≃* ● g ×≃ h ● *≃×)) ● *≃×)
    ≋⟨ id≋ ◎ (id≋ ◎ (sym≋ T.×●≋●× ◎ id≋)) ⟩
  ×≃* ● (×≃* ×≃ id≃ ● assocl⋆equiv) ● ((id≃ ● f) ×≃ (*≃× ● (×≃* ● g ×≃ h ● *≃×))) ● *≃×
    ≋⟨ id≋ ◎ (id≋ ◎ (T._×≋_
                     (trans≋ lid≋ (sym≋ rid≋))
                     (trans≋ ●-assocl  (trans≋ (linv≋ ×≃* ◎ id≋) lid≋)) ◎ id≋)) ⟩
  ×≃* ● (×≃* ×≃ id≃ ● assocl⋆equiv) ● ((f ● id≃) ×≃ (g ×≃ h ● *≃×)) ● *≃×
    ≋⟨ id≋ ◎ (id≋ ◎ (T.×●≋●× ◎ id≋)) ⟩
  ×≃* ● (×≃* ×≃ id≃ ● assocl⋆equiv) ● (f ×≃ (g ×≃ h) ● id≃ ×≃ *≃×) ● *≃×
    ≋⟨ id≋ ◎ ●-assocl ⟩
  ×≃* ● ((×≃* ×≃ id≃ ● assocl⋆equiv) ● (f ×≃ (g ×≃ h) ● id≃ ×≃ *≃×)) ● *≃×
    ≋⟨ id≋ ◎ (●-assocl ◎ id≋) ⟩
  ×≃* ● (((×≃* ×≃ id≃ ● assocl⋆equiv) ● f ×≃ (g ×≃ h)) ● id≃ ×≃ *≃×) ● *≃×
    ≋⟨ id≋ ◎ ((●-assoc ◎ id≋) ◎ id≋) ⟩
  ×≃* ● ((×≃* ×≃ id≃ ● (assocl⋆equiv ● f ×≃ (g ×≃ h))) ● id≃ ×≃ *≃×) ● *≃×
    ≋⟨ id≋ ◎ ( ((id≋ ◎ T.assocl⋆-nat) ◎ id≋) ◎ id≋) ⟩
  ×≃* ● ((×≃* ×≃ id≃ ● ((f ×≃ g) ×≃ h) ● assocl⋆equiv) ● id≃ ×≃ *≃×) ● *≃×
    ≋⟨ id≋ ◎ ((●-assocl ◎ id≋)  ◎ id≋) ⟩
  ×≃* ● (((×≃* ×≃ id≃ ● (f ×≃ g) ×≃ h) ● assocl⋆equiv) ● id≃ ×≃ *≃×) ● *≃×
    ≋⟨ id≋ ◎ (((T*1-nat ◎ id≋) ◎ id≋) ◎ id≋) ⟩
  ×≃* ● ((((×≃* ● f ×≃ g ● *≃×) ● ×≃*) ×≃ (h ● id≃) ● assocl⋆equiv) ● id≃ ×≃ *≃×) ● *≃×
    ≋⟨ id≋ ◎ ●-assoc ⟩
  ×≃* ● (((×≃* ● f ×≃ g ● *≃×) ● ×≃*) ×≃ (h ● id≃) ● assocl⋆equiv) ● (id≃ ×≃ *≃× ● *≃×)
    ≋⟨ id≋ ◎ ●-assoc ⟩
  ×≃* ● ((×≃* ● f ×≃ g ● *≃×) ● ×≃*) ×≃ (h ● id≃) ● (assocl⋆equiv ● id≃ ×≃ *≃× ● *≃×)
    ≋⟨ ●-assocl ⟩
  (×≃* ● ((×≃* ● (f ×≃ g) ● *≃×) ● ×≃*) ×≃ (h ● id≃)) ● (αmno ● id≃ ×≃ *≃× ● *≃×)
    ≋⟨ (id≋ ◎ T.×●≋●× ) ◎ id≋ ⟩
  (×≃* ●  (((×≃* ● (f ×≃ g) ● *≃×) ×≃ h) ● (×≃* ×≃ id≃))) ●
           (αmno ● id≃ ×≃ *≃× ● *≃×)
    ≋⟨ ●-assocl ◎ id≋ ⟩
  ((×≃* ●  ((×≃* ● (f ×≃ g) ● *≃×) ×≃ h)) ● (×≃* ×≃ id≃)) ●
           (αmno ● id≃ ×≃ *≃× ● *≃×)
    ≋⟨ ●-assoc ⟩
  (×≃* ●  ((×≃* ● (f ×≃ g) ● *≃×) ×≃ h)) ●
            (×≃* ×≃ id≃ ● αmno ● id≃ ×≃ *≃× ● *≃×)
    ≋⟨ id≋ ◎ sym≋ lid≋ ⟩
  (×≃* ●  ((×≃* ● (f ×≃ g) ● *≃×) ×≃ h)) ●
            id≃ ● (×≃* ×≃ id≃ ● αmno ● id≃ ×≃ *≃× ● *≃×)
    ≋⟨ id≋ ◎ (sym≋ (rinv≋ *≃×) ◎ id≋) ⟩
  (×≃* ●  ((×≃* ● (f ×≃ g) ● *≃×) ×≃ h)) ●
            (*≃× ● ×≃*) ● (×≃* ×≃ id≃ ● αmno ● id≃ ×≃ *≃× ● *≃×)
    ≋⟨ id≋ ◎ ●-assoc ⟩
  ((×≃* ●  ((×≃* ● (f ×≃ g) ● *≃×) ×≃ h))) ●
            (*≃× ● ×≃* ● ×≃* ×≃ id≃ ● αmno ● id≃ ×≃ *≃× ● *≃×)
    ≋⟨ ●-assocl ⟩
  ((×≃* ●  ((×≃* ● (f ×≃ g) ● *≃×) ×≃ h)) ● *≃×) ●
            (×≃* ● ×≃* ×≃ id≃ ● αmno ● id≃ ×≃ *≃× ● *≃×)
    ≋⟨ ●-assoc ◎ id≋ ⟩
  (×≃* ● ((×≃* ● (f ×≃ g) ● *≃×) ×≃ h) ● *≃×) ●
            (×≃* ● ×≃* ×≃ id≃ ● αmno ● id≃ ×≃ *≃× ● *≃×) ∎)
  where
    open ≋-Reasoning
    T*1-nat : ×≃* ×≃ id≃ ● (f ×≃ g) ×≃ h ≋  ((×≃* ● f ×≃ g ● *≃×) ● ×≃*) ×≃ (h ● id≃)
    T*1-nat = begin (
      ×≃* ×≃ id≃ ● (f ×≃ g) ×≃ h
        ≋⟨ sym≋ (T.×●≋●×) ⟩
      (×≃* ● f ×≃ g) ×≃ (id≃ ● h)
        ≋⟨ id≋ T.×≋ (trans≋ lid≋ (sym≋ rid≋))⟩
      (×≃* ● f ×≃ g) ×≃ (h ● id≃)
        ≋⟨ trans≋ (intro-inv-r* ((×≃* ● f ×≃ g))) ●-assoc T.×≋ id≋ ⟩
        ((×≃* ● f ×≃ g) ● *≃× ● ×≃*) ×≃ (h ● id≃)
         ≋⟨ trans≋ ●-assocl (●-assoc ◎ id≋) T.×≋ id≋ ⟩
       ((×≃* ● f ×≃ g ● *≃×) ● ×≃*) ×≃ (h ● id≃) ∎)

assocr₊-nat : {m n o m' n' o' : ℕ}
    {f : m fin≃ m'} {g : n fin≃ n'} {h : o fin≃ o'} →
    assocr* {m'} {n'} {o'} ● ((f *F g) *F h) ≋
    (f *F (g *F h)) ● assocr* {m} {n} {o}
assocr₊-nat {m} {n} {o} {m'} {n'} {o'} {f} {g} {h} = begin (
  assocr* {m'} {n'} {o'} ● ((f *F g) *F h)
    ≋⟨ id≋ ⟩
  sym≃ assocl* ● sym≃ (sym≃ ((f *F g) *F h))
    ≋⟨ sym≋ (sym≃● {f = assocl*}) ⟩
  sym≃ (sym≃ ((f *F g) *F h) ● assocl* {m'} {n'} {o'})
    ≋⟨ flip≋ ((trans≋ sym*F (sym*F *≋ id≋ )) ◎ id≋) ⟩
  sym≃ (((sym≃ f *F sym≃ g) *F sym≃ h) ● assocl* {m'})
    ≋⟨ flip-sym≋ assocl⋆-nat ⟩
  sym≃ (assocl* {m} {n} {o} ● (sym≃ f *F (sym≃ g *F sym≃ h)))
    ≋⟨ flip≋ (id≋ ◎ (trans≋ (id≋ *≋ (sym≋ sym*F)) (sym≋ sym*F))) ⟩
  sym≃ ( assocl* ● sym≃ (f *F (g *F h)))
    ≋⟨ sym≃● ⟩
  sym≃ (sym≃ (f *F (g *F h))) ● sym≃ (assocl* {m} {n} {o})
    ≋⟨ id≋ ⟩
  (f *F (g *F h)) ● (assocr* {m} {n} {o}) ∎)
  where open ≋-Reasoning

unite-assocr*-coh : {m n : ℕ} →
    unite*r {m = m} *F id≃ {A = Fin n} ≋
    (id≃ {A = Fin m} *F unite* {m = n}) ● assocr* {m} {1} {n}
unite-assocr*-coh = {!!}

assocr*-coh : {m n o p : ℕ} →
    assocr* {m} {n} {o * p} ● assocr* {m * n} {o} {p} ≋
    (id≃ {A = Fin m} *F assocr* {n} {o} {p}) ●
      assocr* {m} {n * o} {p} ● (assocr* {m} {n} {o} *F id≃ {A = Fin p})
assocr*-coh = {!!}

swap*-nat : {m n o p : ℕ} {f : m fin≃ o} {g : n fin≃ p} →
    swap* {o} {p} ● (f *F g) ≋ (g *F f) ● swap* {m} {n}
swap*-nat = {!!}

sswap*-nat : {m n o p : ℕ} {f : m fin≃ o} {g : n fin≃ p} →
    sswap* {o} {p} ● (g *F f) ≋ (f *F g) ● sswap* {m} {n}
sswap*-nat = {!!}

assocr*-swap*-coh : {m n o : ℕ} →
    assocr* {n} {o} {m} ● swap* {m} {n * o} ● assocr* {m} {n} {o} ≋
    (id≃ {A = Fin n} *F swap* {m} {o}) ●
      assocr* {n} {m} {o} ● (swap* {m} {n} *F id≃ {A = Fin o})
assocr*-swap*-coh = {!!}

assocl*-swap*-coh : {m n o : ℕ} →
    assocl* {o} {m} {n} ● swap* {m * n} {o} ● assocl* {m} {n} {o} ≋
    (swap* {m} {o} *F id≃ {A = Fin n}) ●
      assocl* {m} {o} {n} ● (id≃ {A = Fin m} *F swap* {n} {o})
assocl*-swap*-coh = {!!}

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- Now you don't need a mutual keyword anymore!
module Issue162 where

data Odd : Set
data Even : Set where
  zero : Even
  suc  : Odd → Even

data Odd where
  suc : Even → Odd

-- This means you can have all kinds of things in
-- mutual blocks.

-- Like postulates
_o+e_ : Odd → Even → Odd

_e+e_ : Even → Even → Even
zero e+e m = m
suc n e+e m = suc (n o+e m)

postulate todo : Even

suc n o+e m = suc todo

-- Or modules
_e+o_ : Even → Odd → Odd
_o+o_ : Odd → Odd → Even
suc n o+o m = suc (n e+o m)

module Helper where
  f : Even → Odd → Odd
  f zero    m = m
  f (suc n) m = suc (n o+o m)

n e+o m = Helper.f n m

-- Multiplication just for the sake of it
_o*o_ : Odd → Odd → Odd
_e*o_ : Even → Odd → Even
zero  e*o m = zero
suc n e*o m = m o+o (n o*o m)

suc n o*o m = m o+e (n e*o m)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Data.Tuple.Proofs where

import      Lvl
open import Data using (Unit ; <>)
open import Data.Tuple as Tuple using (_⨯_ ; _,_)
open import Data.Tuple.Equiv
open import Function.Equals
open import Logic.Predicate
open import Logic.Propositional
open import Structure.Function.Domain
open import Structure.Function.Domain.Proofs
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ ℓₑ₃ ℓₑ₄ ℓₑ₅ ℓₑ₆ : Lvl.Level
private variable A B A₁ B₁ A₂ B₂ : Type{ℓ}
private variable f g : A → B
private variable p : A ⨯ B

module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄
  ⦃ equiv-AB : Equiv{ℓₑ}(A ⨯ B) ⦄ ⦃ ext-AB : Extensionality(equiv-AB) ⦄
  where
  open Extensionality(ext-AB)

  [,]-left-right-inverses : ∀{x : A ⨯ B} → ((Tuple.left x , Tuple.right x) ≡ x)
  [,]-left-right-inverses {_ , _} = reflexivity(_≡_)

  left-right-[,]-inverses : ∀{a : A}{b : B} → ((Tuple.left(a , b) ≡ a) ∧ (Tuple.right(a , b) ≡ b))
  left-right-[,]-inverses = [∧]-intro (reflexivity(_≡_)) (reflexivity(_≡_))

  instance
    [,]ₗ-injective : ∀{r : B} → Injective(_, r)
    Injective.proof [,]ₗ-injective = congruence₁(Tuple.left)

  instance
    [,]ᵣ-injective : ∀{l : A} → Injective(l ,_)
    Injective.proof [,]ᵣ-injective = congruence₁(Tuple.right)

module _
  ⦃ equiv-A₁ : Equiv{ℓₑ₁}(A₁) ⦄
  ⦃ equiv-B₁ : Equiv{ℓₑ₂}(B₁) ⦄
  ⦃ equiv-A₂ : Equiv{ℓₑ₃}(A₂) ⦄
  ⦃ equiv-B₂ : Equiv{ℓₑ₄}(B₂) ⦄
  ⦃ equiv-AB₁ : Equiv{ℓₑ₅}(A₁ ⨯ B₁) ⦄ ⦃ equiv-AB₁ : Extensionality(equiv-AB₁) ⦄
  ⦃ equiv-AB₂ : Equiv{ℓₑ₆}(A₂ ⨯ B₂) ⦄ ⦃ equiv-AB₂ : Extensionality(equiv-AB₂) ⦄
  {f : A₁ → A₂}
  {g : B₁ → B₂}
  where

  instance
    map-function : BinaryOperator(Tuple.map {A₁ = A₁}{A₂ = A₂}{B₁ = B₁}{B₂ = B₂})
    _⊜_.proof (BinaryOperator.congruence map-function (intro eq₁) (intro eq₂)) {_ , _} = congruence₂(_,_) eq₁ eq₂

  instance
    map-injective : ⦃ inj-f : Injective(f) ⦄ → ⦃ inj-g : Injective(g) ⦄ → Injective(Tuple.map f g)
    Injective.proof map-injective {_ , _} {_ , _} p = congruence₂(_,_) (injective(f) (congruence₁(Tuple.left) p)) (injective(g) (congruence₁(Tuple.right) p))

  instance
    map-surjective : ⦃ surj-f : Surjective(f) ⦄ → ⦃ surj-g : Surjective(g) ⦄ → Surjective(Tuple.map f g)
    ∃.witness (Surjective.proof map-surjective {l , r}) = ([∃]-witness(surjective(f) {l}) , [∃]-witness(surjective(g) {r}))
    ∃.proof   (Surjective.proof map-surjective {l , r}) = congruence₂(_,_) ([∃]-proof(surjective(f) {l})) ([∃]-proof(surjective(g) {r}))

  instance
    map-bijective : ⦃ bij-f : Bijective(f) ⦄ → ⦃ bij-g : Bijective(g) ⦄ → Bijective(Tuple.map f g)
    map-bijective = injective-surjective-to-bijective(Tuple.map f g) where
      instance
        inj-f : Injective(f)
        inj-f = bijective-to-injective(f)
      instance
        inj-g : Injective(g)
        inj-g = bijective-to-injective(g)
      instance
        surj-f : Surjective(f)
        surj-f = bijective-to-surjective(f)
      instance
        surj-g : Surjective(g)
        surj-g = bijective-to-surjective(g)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import HoTT

module homotopy.JoinComm where

module _ {i j} {A : Type i} {B : Type j} where

  swap : A * B → B * A
  swap = Swap.f  module _ where

    swap-glue : (a : A) (b : B) → right a == left b
    swap-glue a b = ! (glue (b , a))

    module Swap = PushoutRec right left (uncurry swap-glue)

{- ∞TT:

  swap : A * B → B * A
  swap (left a) = right a
  swap (right b) = left b
  ap swap (glue (a , b)) = ! (glue (b , a))
-}

module _ {i j} {A : Type i} {B : Type j} where

  swap-swap : (x : A * B) → swap (swap x) == x
  swap-swap = Pushout-elim (λ a → idp) (λ b → idp) (λ c → ↓-∘=idf-in swap swap
    (swap-swap-glue c)) where

    swap-swap-glue : (c : A × B) → ap swap (ap swap (glue c)) == glue c
    swap-swap-glue (a , b) =
      ap swap (ap swap (glue (a , b)))   =⟨ Swap.glue-β (a , b) |in-ctx ap swap ⟩
      ap swap (! (glue (b , a)))         =⟨ ap-! swap (glue (b , a)) ⟩
      ! (ap swap (glue (b , a)))         =⟨ Swap.glue-β (b , a) |in-ctx ! ⟩
      ! (! (glue (a , b)))               =⟨ !-! (glue (a , b)) ⟩
      glue (a , b) ∎

{- ∞TT:

  swap-swap : (x : A * B) → swap (swap x) == x
  swap-swap (left a) = idp
  swap-swap (right b) = idp
  apd swap-swap (glue (a , b)) = !-! (glue (a , b))
-}

module _ {i j} {A : Type i} {B : Type j} where

  swap-equiv : (A * B) ≃ (B * A)
  swap-equiv = equiv swap swap swap-swap swap-swap

  swap-path : (A * B) == (B * A)
  swap-path = ua swap-equiv

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by bounded lattice
------------------------------------------------------------------------

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

open import Relation.Binary.Lattice

module Relation.Binary.Properties.BoundedLattice
  {c ℓ₁ ℓ₂} (L : BoundedLattice c ℓ₁ ℓ₂) where

open BoundedLattice L

open import Algebra.FunctionProperties _≈_
open import Data.Product using (_,_)
open import Relation.Binary using (Setoid)
open import Relation.Binary.Properties.MeetSemilattice meetSemilattice
open import Relation.Binary.Properties.JoinSemilattice joinSemilattice

open Setoid setoid renaming (trans to ≈-trans)

∧-zeroʳ : RightZero ⊥ _∧_
∧-zeroʳ x = y≤x⇒x∧y≈y (minimum x)

∧-zeroˡ : LeftZero ⊥ _∧_
∧-zeroˡ x = ≈-trans (∧-comm ⊥ x) (∧-zeroʳ x)

∧-zero : Zero ⊥ _∧_
∧-zero = ∧-zeroˡ , ∧-zeroʳ

∨-zeroʳ : RightZero ⊤ _∨_
∨-zeroʳ x = x≤y⇒x∨y≈y (maximum x)

∨-zeroˡ : LeftZero ⊤ _∨_
∨-zeroˡ x = ≈-trans (∨-comm ⊤ x) (∨-zeroʳ x)

∨-zero : Zero ⊤ _∨_
∨-zero = ∨-zeroˡ , ∨-zeroʳ


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Boolean.Definition where

data Bool : Set where
  BoolTrue : Bool
  BoolFalse : Bool
{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  BoolTrue  #-}
{-# BUILTIN FALSE BoolFalse #-}

if_then_else_ : {a : _} → {A : Set a} → Bool → A → A → A
if BoolTrue then tr else fls = tr
if BoolFalse then tr else fls = fls

not : Bool → Bool
not BoolTrue = BoolFalse
not BoolFalse = BoolTrue

boolAnd : Bool → Bool → Bool
boolAnd BoolTrue y = y
boolAnd BoolFalse y = BoolFalse

boolOr : Bool → Bool → Bool
boolOr BoolTrue y = BoolTrue
boolOr BoolFalse y = y

xor : Bool → Bool → Bool
xor BoolTrue BoolTrue = BoolFalse
xor BoolTrue BoolFalse = BoolTrue
xor BoolFalse b = b


text:
module root2 where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Data.Unit using (⊤ ; tt)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions

import gcd as GCD
open import even
open import nat
open import logic

record Rational : Set where
  field
    i j : ℕ
    coprime : GCD.gcd i j ≡ 1

-- record Dividable (n m : ℕ ) : Set where
--    field
--       factor : ℕ
--       is-factor : factor * n + 0 ≡ m

gcd : (i j : ℕ) → ℕ
gcd = GCD.gcd

gcd-euclid : ( p a b : ℕ )  → 1 < p  → 0 < a → 0 < b → ((i : ℕ ) → i < p → 0 < i   → gcd p i ≡ 1)
   →  Dividable p (a * b)  → Dividable p a ∨ Dividable p b
gcd-euclid = GCD.gcd-euclid

gcd-div1 : ( i j k : ℕ ) → k > 1 → (if : Dividable k i) (jf : Dividable k j )
   → Dividable k ( gcd i  j )
gcd-div1 = GCD.gcd-div

open _∧_

open import prime

divdable^2 : ( n k : ℕ ) → 1 < k → 1 < n → Prime k → Dividable k ( n * n ) → Dividable k n
divdable^2 zero zero () 1<n pk dn2
divdable^2 (suc n) (suc k) 1<k 1<n pk dn2 with decD {suc k} {suc n} 1<k
... | yes y = y
... | no non with gcd-euclid (suc k) (suc n) (suc n) 1<k (<-trans a<sa 1<n) (<-trans a<sa 1<n) (Prime.isPrime pk) dn2
... | case1 dn = dn
... | case2 dm = dm

-- p * n * n ≡ m * m means (m/n)^2 = p
-- rational m/n requires m and n is comprime each other which contradicts the condition

root-prime-irrational : ( n m p : ℕ ) → n > 1 → Prime p → m > 1  →  p * n * n ≡ m * m  → ¬ (gcd n m ≡ 1)
root-prime-irrational n m 0 n>1 pn m>1 pnm = ⊥-elim ( nat-≡< refl (<-trans a<sa (Prime.p>1 pn)))
root-prime-irrational n m (suc p0) n>1 pn m>1 pnm = rot13 ( gcd-div1 n m (suc p0) 1<sp dn dm ) where
    p = suc p0
    1<sp : 1 < p
    1<sp = Prime.p>1 pn
    rot13 : {m : ℕ } → Dividable (suc p0) m →  m ≡ 1 → ⊥
    rot13 d refl with Dividable.factor d | Dividable.is-factor d
    ... | zero | ()   -- gcd 0 m ≡ 1
    ... | suc n | x = ⊥-elim ( nat-≡< (sym x) rot17 ) where -- x : (suc n * p + 0) ≡ 1
        rot17 : suc n * (suc p0) + 0 > 1
        rot17 = begin
           2 ≡⟨ refl ⟩
           suc (1 * 1 ) ≤⟨ 1<sp  ⟩
           suc p0  ≡⟨ cong suc (+-comm 0 _) ⟩
           suc (p0 + 0) ≤⟨ s≤s (+-monoʳ-≤ p0 z≤n) ⟩
           suc (p0 + n * p )  ≡⟨ +-comm 0 _ ⟩
           suc n * p + 0 ∎   where open ≤-Reasoning
    dm : Dividable p m
    dm = divdable^2 m p 1<sp m>1 pn record { factor = n * n ; is-factor = begin
       (n * n) * p + 0 ≡⟨  +-comm _ 0 ⟩
       (n * n) * p  ≡⟨ *-comm (n * n) p ⟩
       p * (n * n)  ≡⟨ sym (*-assoc p n n)  ⟩
       (p * n) * n ≡⟨ pnm ⟩
       m * m ∎ }  where open ≡-Reasoning
     -- p * n * n = 2m' 2m'
     --  n * n = m' 2m'
    df = Dividable.factor dm
    dn : Dividable p n
    dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df  ; is-factor = begin
        df * df * p + 0  ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin
          (df * df * p + 0) * p ≡⟨  cong (λ k → k * p)  (+-comm (df * df * p) 0)  ⟩
          ((df * df) * p  ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩
            (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p)  ⟩
            (df * (p * df)) * p ≡⟨ sym ( cong (λ k → k * p) (*-assoc df p df ) ) ⟩
            ((df * p) * df) * p ≡⟨ *-assoc (df * p) df p  ⟩
            (df * p) * (df * p) ≡⟨ cong₂ (λ j k → j * k ) (+-comm 0 (df * p)) (+-comm 0 _) ⟩
          (df * p + 0) * (df * p + 0)   ≡⟨ cong₂ (λ j k → j * k) (Dividable.is-factor dm ) (Dividable.is-factor dm )⟩
          m * m   ≡⟨ sym pnm ⟩
          p * n * n     ≡⟨ cong (λ k → k * n) (*-comm p n) ⟩
          n * p * n     ≡⟨ *-assoc n p n ⟩
          n * (p * n)   ≡⟨ cong (λ k → n * k) (*-comm p n) ⟩
          n * (n * p)   ≡⟨ sym (*-assoc n n p) ⟩
          n * n * p ∎  ) ⟩
       n * n ∎ }  where open ≡-Reasoning

Rational* : (r s : Rational) → Rational
Rational* r s = record  { i = {!!} ; j = {!!} ; coprime = {!!} }

_r=_ : Rational → ℕ → Set
r r= n  = (Rational.i r ≡ n) ∧ (Rational.j r ≡ 1)

root-prime-irrational1 : ( p : ℕ ) → Prime p → ¬ ( ( r  : Rational ) → Rational* r r r= p )
root-prime-irrational1 = {!!}

max_stars_repo_name: shinji-kono/automaton-in-agda

max_issues_repo_name: shinji-kono/automaton-in-agda

max_forks_repo_name: shinji-kono/automaton-in-agda


text:
module Data.List.Proofs where

import Lvl
open import Functional
open import Data.Option using (Option ; Some ; None)
open import Data.List
open import Data.List.Equiv
open import Data.List.Functions
open import Logic
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Proofs
open import Relator.Equals renaming (_≡_ to _≡ₑ_ ; _≢_ to _≢ₑ_)
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Multi
import      Structure.Function.Names as Names
import      Structure.Operator.Names as Names
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ ℓₑₗ ℓₑₒ ℓₑ₁ ℓₑ₂ ℓₑₗ₁ ℓₑₗ₂ : Lvl.Level
private variable T A B : Type{ℓ}
private variable n : ℕ

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ ⦃ equiv-List : Equiv{ℓₑₗ}(List(T)) ⦄ ⦃ extensionality : Extensionality(equiv-List) ⦄ where
  private variable l l₁ l₂ : List(T)
  private variable a b x : T
  private variable P : List(T) → Stmt{ℓ}

  open Equiv(equiv-List) using () renaming (_≡_ to _≡ₗ_)

  instance
    tail-function : Function(tail)
    Function.congruence tail-function {∅}      {∅}      p = p
    Function.congruence tail-function {∅}      {x ⊰ y}  p with () ← [∅][⊰]-unequal p
    Function.congruence tail-function {x ⊰ xl} {∅}      p with () ← [∅][⊰]-unequal (symmetry(_≡_) p)
    Function.congruence tail-function {x ⊰ xl} {y ⊰ yl} p = [⊰]-generalized-cancellationₗ p

  instance
    first-function : ⦃ equiv-Option : Equiv{ℓₑₒ}(Option(T)) ⦄ ⦃ Some-function : Function(Some) ⦄ → Function(first)
    Function.congruence first-function {∅}      {∅}      p = reflexivity(_≡_)
    Function.congruence first-function {∅}      {y ⊰ yl} p with () ← [∅][⊰]-unequal p
    Function.congruence first-function {x ⊰ xl} {∅}      p with () ← [∅][⊰]-unequal (symmetry(_≡_) p)
    Function.congruence first-function {x ⊰ xl} {y ⊰ yl} p = congruence₁(Some) ([⊰]-generalized-cancellationᵣ p)

  instance
    [⊰]-cancellationₗ : Cancellationₗ(_⊰_)
    Cancellationₗ.proof([⊰]-cancellationₗ) = [⊰]-generalized-cancellationₗ

  instance
    [⊰]-cancellationᵣ : Cancellationᵣ(_⊰_)
    Cancellationᵣ.proof([⊰]-cancellationᵣ) = [⊰]-generalized-cancellationᵣ

  [⊰]-unequal : (x ⊰ l ≢ l)
  [⊰]-unequal {l = ∅} = [∅][⊰]-unequal ∘ symmetry(_≡_)
  [⊰]-unequal {l = x ⊰ l} = [⊰]-unequal {l = l} ∘ [⊰]-generalized-cancellationₗ

  postpend-of-prepend : (postpend a (b ⊰ l) ≡ b ⊰ postpend a l)
  postpend-of-prepend = reflexivity(_≡_)

  instance
    postpend-function : BinaryOperator(postpend)
    postpend-function = intro p where
      p : Names.Congruence₂(postpend)
      p {x₂ = ∅}        {y₂ = ∅}        px pl = congruence₂(_⊰_) px pl
      p {x₂ = ∅}        {y₂ = y₂ ⊰ yl₂} px pl with () ← [∅][⊰]-unequal pl
      p {x₂ = x₂ ⊰ xl₂} {y₂ = ∅}        px pl with () ← [∅][⊰]-unequal (symmetry(_≡_) pl)
      p {x₂ = x₂ ⊰ xl₂} {y₂ = y₂ ⊰ yl₂} px pl = congruence₂(_⊰_) ([⊰]-generalized-cancellationᵣ pl) (p{x₂ = xl₂} {y₂ = yl₂} px ([⊰]-generalized-cancellationₗ pl))

  instance
    reverse-function : Function(reverse)
    reverse-function = intro p where
      p : Names.Congruence₁(reverse)
      p {∅}      {∅}      pl = reflexivity(_≡_)
      p {∅}      {y ⊰ yl} pl with () ← [∅][⊰]-unequal pl
      p {x ⊰ xl} {∅}      pl with () ← [∅][⊰]-unequal (symmetry(_≡_) pl)
      p {x ⊰ xl} {y ⊰ yl} pl = congruence₂(postpend) ([⊰]-generalized-cancellationᵣ pl) (p([⊰]-generalized-cancellationₗ pl))

  instance
    [++]-identityₗ : Identityₗ(_++_) ∅
    Identityₗ.proof([++]-identityₗ) = reflexivity(_≡_)

  instance
    [++]-identityᵣ : Identityᵣ(_++_) ∅
    Identityᵣ.proof([++]-identityᵣ) {x = l} = elim (reflexivity(_≡_)) (\x l → congruence₂ᵣ(_⊰_)(x) {l ++ ∅}{l}) l

  instance
    [++]-associativity : Associativity(_++_)
    Associativity.proof([++]-associativity) {l₁}{l₂}{l₃} = elim (reflexivity(_≡_)) (\x l → congruence₂ᵣ(_⊰_)(x) {(l ++ l₂) ++ l₃}{l ++ (l₂ ++ l₃)}) l₁

  reverse-postpend : (reverse(postpend a l) ≡ a ⊰ reverse l)
  reverse-postpend {a = a}{l = l} = elim (reflexivity(_≡ₗ_)) (\x l p → congruence₂ᵣ(postpend) ⦃ postpend-function ⦄ (x) {reverse(postpend a l)}{a ⊰ reverse l} p) l

  prepend-[++] : (a ⊰ l ≡ singleton{T = T}(a) ++ l)
  prepend-[++] = reflexivity(_≡_)

  postpend-[++] : (postpend{T = T} a l ≡ l ++ singleton(a))
  postpend-[++] {a = a}{l = l} = elim (reflexivity(_≡_)) (\x l → congruence₂ᵣ(_⊰_)(x) {postpend a l}{l ++ (singleton a)}) l

  postpend-of-[++] : (postpend{T = T} a (l₁ ++ l₂) ≡ l₁ ++ postpend a l₂)
  postpend-of-[++] {a = a} {l₁}{l₂} = elim (reflexivity(_≡_)) (\x l → congruence₂ᵣ(_⊰_)(x) {postpend a (l ++ l₂)}{l ++ (postpend a l₂)}) l₁

  reverse-[++] : (reverse(l₁ ++ l₂) ≡ reverse(l₂) ++ reverse(l₁))
  reverse-[++] {l₁ = l₁} {l₂ = l₂} = elim
    (congruence₁(reverse) (identityₗ(_++_)(∅) {l₂}) 🝖 symmetry(_≡_) (identityᵣ(_++_)(∅) {reverse l₂}))
    (\x l₁ p → congruence₂ᵣ(postpend) ⦃ postpend-function ⦄ (x) {reverse (l₁ ++ l₂)}{reverse l₂ ++ reverse l₁} p 🝖 postpend-of-[++] {l₁ = reverse l₂} {l₂ = reverse l₁})
    l₁

  [∅]-postpend-unequal : (postpend x l ≢ ∅)
  [∅]-postpend-unequal {l = ∅}     = [∅][⊰]-unequal ∘ symmetry(_≡_)
  [∅]-postpend-unequal {l = _ ⊰ l} = [∅][⊰]-unequal ∘ symmetry(_≡_)

  postpend-unequal : (postpend x l ≢ l)
  postpend-unequal {l = ∅}     = [∅][⊰]-unequal ∘ symmetry(_≡_)
  postpend-unequal {l = y ⊰ l} = postpend-unequal {l = l} ∘ cancellationₗ(_⊰_)

  [++]-middle-prepend-postpend : postpend x l₁ ++ l₂ ≡ l₁ ++ (x ⊰ l₂)
  [++]-middle-prepend-postpend {l₁ = ∅}      {l₂ = ∅} = reflexivity(_≡_)
  [++]-middle-prepend-postpend {l₁ = ∅}      {l₂ = x ⊰ l₂} = reflexivity(_≡_)
  [++]-middle-prepend-postpend {l₁ = x ⊰ l₁} {l₂ = l₂} = congruence₂ᵣ(_⊰_)(x) ([++]-middle-prepend-postpend {l₁ = l₁} {l₂ = l₂})

  instance
    [++]-cancellationₗ : Cancellationₗ(_++_)
    Cancellationₗ.proof [++]-cancellationₗ {x}{y}{z} = proof {x}{y}{z} where
      proof : Names.Cancellationₗ (_++_)
      proof {∅}     p = p
      proof {x ⊰ l} p = proof {l} (cancellationₗ(_⊰_) p)

  instance
    [++]-cancellationᵣ : Cancellationᵣ(_++_)
    Cancellationᵣ.proof([++]-cancellationᵣ) {a}{b} = proof {a}{b} where
      proof : Names.Cancellationᵣ(_++_)
      proof {z}      {∅}      {∅}      p = reflexivity(_≡_)
      proof {z}      {x ⊰ xl} {y ⊰ yl} p = congruence₂(_⊰_) ([⊰]-generalized-cancellationᵣ p) (proof {z}{xl}{yl} ([⊰]-generalized-cancellationₗ p))
      proof {∅}      {∅}      {y ⊰ yl} p with () ← [∅][⊰]-unequal {l = yl} (p 🝖 identityᵣ(_++_)(∅))
      proof {z ⊰ zl} {∅}      {y ⊰ yl} p with () ← [∅]-postpend-unequal(symmetry(_≡_) (proof{zl}{∅}{postpend z yl} ([⊰]-generalized-cancellationₗ p 🝖 symmetry(_≡_) ([++]-middle-prepend-postpend {x = z}{l₁ = yl}{l₂ = zl}))))
      proof {∅}      {x ⊰ xl} {∅}      p with () ← [∅][⊰]-unequal {l = xl} (symmetry(_≡_) p 🝖 identityᵣ(_++_)(∅))
      proof {z ⊰ zl} {x ⊰ xl} {∅}      p with () ← [∅]-postpend-unequal(proof{zl}{postpend z xl}{∅} ([++]-middle-prepend-postpend {x = z}{l₁ = xl}{l₂ = zl} 🝖 [⊰]-generalized-cancellationₗ p))

  reverse-involution-raw : Names.Involution(reverse{T = T})
  reverse-involution-raw {x = ∅}     = reflexivity(_≡_)
  reverse-involution-raw {x = x ⊰ l} = reverse-postpend {a = x}{l = reverse l} 🝖 congruence₂ᵣ(_⊰_)(x) (reverse-involution-raw {x = l})

  instance
    reverse-involution : Involution(reverse{T = T})
    Involution.proof reverse-involution = reverse-involution-raw

  initial-of-∅ : (initial(n)(∅ {T = T}) ≡ ∅)
  initial-of-∅ {n = 𝟎}    = reflexivity(_≡_)
  initial-of-∅ {n = 𝐒(n)} = reflexivity(_≡_)

  module _ where
    open import Relator.Equals.Proofs.Equiv {T = ℕ}
    foldᵣ-constant-[+]ᵣ : ∀{init step} → (foldᵣ (const(_+ step)) init l ≡ₑ (step ⋅ length(l)) + init)
    foldᵣ-constant-[+]ᵣ {l = ∅} = reflexivity(_≡ₑ_)
    foldᵣ-constant-[+]ᵣ {l = x ⊰ l} {init}{step} =
      const(_+ step) x (foldᵣ (const(_+ step)) init l) 🝖[ _≡_ ]-[]
      (foldᵣ (const(_+ step)) init l) + step           🝖[ _≡_ ]-[ congruence₁(_+ step) (foldᵣ-constant-[+]ᵣ {l = l} {init}{step}) ]
      ((step ⋅ length(l)) + init) + step               🝖[ _≡_ ]-[ One.commuteᵣ-assocₗ {a = step ⋅ length(l)}{init}{step} ]
      ((step ⋅ length(l)) + step) + init               🝖[ _≡_ ]-[ congruence₁(_+ init) (commutativity(_+_) {step ⋅ length(l)}{step}) ]
      (step + (step ⋅ length(l))) + init               🝖-end

    foldᵣ-constant-[+]ₗ : ∀{init step} → (foldᵣ (const(step +_)) init l ≡ (length(l) ⋅ step) + init)
    foldᵣ-constant-[+]ₗ {l = ∅}                  = reflexivity(_≡_)
    foldᵣ-constant-[+]ₗ {l = x ⊰ l} {init}{step} =
      foldᵣ(const(step +_)) init (x ⊰ l)  🝖[ _≡_ ]-[]
      step + foldᵣ(const(step +_)) init l 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(step) (foldᵣ-constant-[+]ₗ {l = l} {init}{step}) ]
      step + ((length(l) ⋅ step) + init)  🝖[ _≡_ ]-[ associativity(_+_) {step}{length(l) ⋅ step}{init} ]-sym
      (step + (length(l) ⋅ step)) + init  🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(init) (commutativity(_+_) {step}{length(l) ⋅ step}) ]
      ((length(l) ⋅ step) + step) + init  🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(init) ([⋅]-with-[𝐒]ₗ {length(l)}{step}) ]-sym
      (𝐒(length(l)) ⋅ step) + init        🝖[ _≡_ ]-[]
      (length(x ⊰ l) ⋅ step) + init       🝖-end

open import Structure.Setoid
module _
  ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-List₁ : Equiv{ℓₑₗ₁}(List(A)) ⦄ ⦃ extensionality-A : Extensionality(equiv-List₁) ⦄
  ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ ⦃ equiv-List₂ : Equiv{ℓₑₗ₂}(List(B)) ⦄ ⦃ extensionality-B : Extensionality(equiv-List₂) ⦄
  where

  private variable l l₁ l₂ : List(T)
  private variable a b x : T
  private variable P : List(T) → Stmt{ℓ}

  private variable f : A → B

  map-postpend : (map f(postpend a l) ≡ postpend (f(a)) (map f(l)))
  map-postpend {f = f} {a = a}{l = l} = elim (reflexivity(_≡_)) (\x l → congruence₂ᵣ(_⊰_)(f(x)) {map f (postpend a l)}{postpend (f(a)) (map f l)}) l

  instance
    map-preserves-[++] : Preserving₂(map f)(_++_)(_++_)
    Preserving.proof (map-preserves-[++] {f = f}) {l₁} {l₂} = elim (reflexivity(_≡_)) (\x l₁ → congruence₂ᵣ(_⊰_)(f(x)) {map f(l₁ ++ l₂)}{(map f l₁) ++ (map f l₂)}) l₁


text:
{-# OPTIONS --safe #-}
{-# OPTIONS --sized-types #-}
module ++-Identity where

open import Size

-- +-identityʳ : ∀ (n : ℕ) → n + 0 ≅ n
-- +-identityʳ zero = refl
-- +-identityʳ (suc n) = cong suc (+-identityʳ n)

-- ∷-≅ : ∀ {m n : ℕ} {A : Set} (x : A) (xs : Vec A m) (ys : Vec A n) → m ≅ n → xs ≅ ys → (x ∷ xs) ≅ (x ∷ ys)
-- ∷-≅ x xs .xs refl refl = refl

-- ++-identityʳ : ∀ {n} {A : Set} (xs : Vec A n) → xs ++ [] ≅ xs
-- ++-identityʳ {.0} {A} [] = refl
-- ++-identityʳ {suc n} {A} (x ∷ xs)  = ∷-≅ x (xs ++ []) xs (+-identityʳ n) (++-identityʳ xs)

data Nat : {i : Size} -> Set where
  zero : {i : Size} -> Nat {↑ i}
  suc : {i : Size} -> Nat {i} -> Nat {↑ i}

sub : {i : Size} -> Nat {i} -> Nat {∞} -> Nat {i}
sub zero n = zero
sub (suc m) zero = suc m
sub (suc m) (suc n) = sub m n

div : {i : Size} -> Nat {i} -> Nat -> Nat {i}
div zero n = zero
div (suc m) n = suc (div (sub m n) n)

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


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

open import Boolean.Definition
open import LogicalFormulae
open import Decidable.Lemmas

module Numbers.Naturals.Definition where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

infix 100 succ

{-# BUILTIN NATURAL ℕ #-}

succInjective : {a b : ℕ} → (succ a ≡ succ b) → a ≡ b
succInjective {a} {.a} refl = refl

naughtE : {a : ℕ} → zero ≡ succ a → False
naughtE ()

aIsNotSuccA : (a : ℕ) → (a ≡ succ a) → False
aIsNotSuccA zero pr = naughtE pr
aIsNotSuccA (succ a) pr = aIsNotSuccA a (succInjective pr)

ℕDecideEquality : (a b : ℕ) → ((a ≡ b) || ((a ≡ b) → False))
ℕDecideEquality zero zero = inl refl
ℕDecideEquality zero (succ b) = inr (λ ())
ℕDecideEquality (succ a) zero = inr (λ ())
ℕDecideEquality (succ a) (succ b) with ℕDecideEquality a b
ℕDecideEquality (succ a) (succ b) | inl x = inl (applyEquality succ x)
ℕDecideEquality (succ a) (succ b) | inr x = inr λ pr → x (succInjective pr)

ℕDecideEquality' : (a b : ℕ) → Bool
ℕDecideEquality' a b with ℕDecideEquality a b
ℕDecideEquality' a b | inl x = BoolTrue
ℕDecideEquality' a b | inr x = BoolFalse

record _=N'_ (a b : ℕ) : Set where
  field
    .eq : a ≡ b

squashN : {a b : ℕ} → a =N' b → a ≡ b
squashN record { eq = eq } = squash ℕDecideEquality eq

collapseN : {a b : ℕ} → a ≡ b → a =N' b
collapseN refl = record { eq = refl }

=N'Refl : {a b : ℕ} → (p1 p2 : a =N' b) → p1 ≡ p2
=N'Refl p1 p2 = refl


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
open import LibraBFT.Impl.OBM.Rust.Duration     as Duration
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.Liveness.ExponentialTimeInterval where

new : Duration → F64 → Usize → ExponentialTimeInterval
new base exponentBase maxExponent =
{- TODO-1
  if | maxExponent >= 32
       -> errorExit [ "ExponentialTimeInterval", "new"
                    , "maxExponent for PacemakerTimeInterval should be < 32", show maxExponent ]
     | ceiling (exponentBase ** fromIntegral maxExponent) >= {-F64-} (maxBound::Int)
       -> errorExit [ "ExponentialTimeInterval", "new"
                    , "maximum interval multiplier should be less then u32::Max"]
     | otherwise
       ->
-}        mkExponentialTimeInterval
            (Duration.asMillis base)
            exponentBase
            maxExponent


text:
module AllTests where

import Issue14
import LanguageConstructs
import Numbers
import Pragmas
import Sections
import Test
import Tuples
import Where

{-# FOREIGN AGDA2HS
import Issue14
import LanguageConstructs
import Numbers
import Pragmas
import Sections
import Test
import Tuples
import Where
#-}


text:
-- Task:
-- Try to compile a function that requires a proof as input.
-- It should be similar to what exportSqrt does in the ℝ but
-- for Nats (ℕ)


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

open import Categories.Category
open import Categories.Functor hiding (equiv) renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_)
open import Categories.NaturalTransformation.Core public

infixr 9 _∘ˡ_ _∘ʳ_

_∘ˡ_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
     → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
     → {F G : Functor C D}
     → (H : Functor D E) → (η : NaturalTransformation F G) → NaturalTransformation (H ∘F F) (H ∘F G)
_∘ˡ_ {C = C} {D} {E} {F} {G} H η′ = record
  { η       = λ X → Functor.F₁ H (NaturalTransformation.η η′ X)
  ; commute = commute′
  }
  where
  module C = Category C
  module D = Category D renaming (_∘_ to _∘D_; _≡_ to _≡D_)
  module E = Category E renaming (_∘_ to _∘E_; _≡_ to _≡E_)
  module H = Functor H
  open D
  open E

  .commute′ : ∀ {X Y} (f : C [ X , Y ]) →
      Functor.F₁ H (NaturalTransformation.η η′ Y) ∘E Functor.F₁ H (Functor.F₁ F f) ≡E
      Functor.F₁ H (Functor.F₁ G f) ∘E Functor.F₁ H (NaturalTransformation.η η′ X)
  commute′ {X} {Y} f =
      begin
        Functor.F₁ H (NaturalTransformation.η η′ Y) ∘E Functor.F₁ H (Functor.F₁ F f)
      ↑⟨ H.homomorphism ⟩
        Functor.F₁ H (NaturalTransformation.η η′ Y ∘D Functor.F₁ F f)
      ↓⟨ H.F-resp-≡ (NaturalTransformation.commute η′ f) ⟩
        Functor.F₁ H (Functor.F₁ G f ∘D NaturalTransformation.η η′ X)
      ↓⟨ H.homomorphism ⟩
        Functor.F₁ H (Functor.F₁ G f) ∘E Functor.F₁ H (NaturalTransformation.η η′ X)
      ∎
    where
    open E.HomReasoning

_∘ʳ_ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂}
     → {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁} {E : Category o₂ ℓ₂ e₂}
     → {F G : Functor C D}
     → (η : NaturalTransformation F G) → (K : Functor E C) → NaturalTransformation (F ∘F K) (G ∘F K)
_∘ʳ_ η K = record
  { η       = λ X → NaturalTransformation.η η (Functor.F₀ K X)
  ; commute = λ f → NaturalTransformation.commute η (Functor.F₁ K f)
  }

-- The vertical versions
.identity₁ˡ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D} {X : NaturalTransformation F G}
           → id ∘₁ X ≡ X
identity₁ˡ {D = D} = Category.identityˡ D

.identity₁ʳ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D} {X : NaturalTransformation F G}
           → X ∘₁ id ≡ X
identity₁ʳ {D = D} = Category.identityʳ D

.assoc₁ : ∀ {o ℓ e o′ ℓ′ e′}
           {P : Category o ℓ e} {Q : Category o′ ℓ′ e′} {A B C D : Functor P Q}
           {X : NaturalTransformation A B} {Y : NaturalTransformation B C} {Z : NaturalTransformation C D}
       → (Z ∘₁ Y) ∘₁ X ≡ Z ∘₁ (Y ∘₁ X)
assoc₁ {Q = Q} = Category.assoc Q

-- The horizontal ones
.identity₀ˡ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D} {X : NaturalTransformation F G}
           → id {F = idF} ∘₀ X ≡ X
identity₀ˡ {D = D} = Category.identityʳ D

.identity₀ʳ : ∀ {o ℓ e o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {F G : Functor C D} {X : NaturalTransformation F G}
           → X ∘₀ id {F = idF} ≡ X
identity₀ʳ {C = C} {D} {F} {G} {X} =
    begin
      G₁ C.id ∘ (η _)
    ↓⟨ ∘-resp-≡ˡ G.identity ⟩
      D.id ∘ (η _)
    ↓⟨ D.identityˡ ⟩
      η _
    ∎
  where
  module C = Category C
  module D = Category D
  module F = Functor F
  module G = Functor G renaming (F₀ to G₀; F₁ to G₁; F-resp-≡ to G-resp-≡)
  open NaturalTransformation X
  open D.HomReasoning
  open F
  open G
  open D

open import Categories.Functor.Core using () renaming ( _∘_ to _∘F_)
.assoc₀ : ∀ {o₀ ℓ₀ e₀ o₁ ℓ₁ e₁ o₂ ℓ₂ e₂ o₃ ℓ₃ e₃}
            {C₀ : Category o₀ ℓ₀ e₀} {C₁ : Category o₁ ℓ₁ e₁} {C₂ : Category o₂ ℓ₂ e₂} {C₃ : Category o₃ ℓ₃ e₃}
            {F G : Functor C₀ C₁} {H I : Functor C₁ C₂} {J K : Functor C₂ C₃}
        → {X : NaturalTransformation F G} → {Y : NaturalTransformation H I} → {Z : NaturalTransformation J K}
        → (Z ∘₀ Y) ∘₀ X ≡ (_∘₀_   {F = H ∘F F} {I ∘F G} Z  (_∘₀_ {C = C₀} {C₁} {C₂} Y  X))
assoc₀ {C₀ = C₀} {C₁} {C₂} {C₃} {F} {G} {H} {I} {J} {K} {X} {Y} {Z} =
    begin
      K₁ (I₁ (X.η _)) ∘C₃ (K₁ (Y.η (F₀ _)) ∘C₃ Z.η (H₀ (F₀ _)))
    ↑⟨ C₃.assoc ⟩
      (K₁ (I₁ (X.η _)) ∘C₃ K₁ (Y.η (F₀ _))) ∘C₃ Z.η (H₀ (F₀ _))
    ↑⟨ C₃.∘-resp-≡ˡ K.homomorphism ⟩
      (K₁ ((I₁ (X.η _)) ∘C₂ Y.η (F₀ _))) ∘C₃ Z.η (H₀ (F₀ _))
    ∎
  where
  module C₂ = Category C₂ renaming (_∘_ to _∘C₂_; _≡_ to _≡C₂_)
  module C₃ = Category C₃ renaming (_∘_ to _∘C₃_; _≡_ to _≡C₃_)
  module F = Functor F
  module G = Functor G renaming (F₀ to G₀; F₁ to G₁; F-resp-≡ to G-resp-≡)
  module H = Functor H renaming (F₀ to H₀; F₁ to H₁; F-resp-≡ to H-resp-≡)
  module I = Functor I renaming (F₀ to I₀; F₁ to I₁; F-resp-≡ to I-resp-≡)
  module J = Functor J renaming (F₀ to J₀; F₁ to J₁; F-resp-≡ to J-resp-≡)
  module K = Functor K renaming (F₀ to K₀; F₁ to K₁; F-resp-≡ to K-resp-≡)
  module X = NaturalTransformation X
  module Y = NaturalTransformation Y
  module Z = NaturalTransformation Z
  open C₃.HomReasoning
  open C₂
  open C₃
  open F
  open H
  open I
  open K

.interchange : ∀ {o₀ ℓ₀ e₀} {o₁ ℓ₁ e₁} {o₂ ℓ₂ e₂}
                 {C₀ : Category o₀ ℓ₀ e₀} {C₁ : Category o₁ ℓ₁ e₁} {C₂ : Category o₂ ℓ₂ e₂}
                 {F₀ F₁ F₅ : Functor C₀ C₁} {F₂ F₃ F₄ : Functor C₁ C₂}
                 {α : NaturalTransformation F₃ F₄}
                 {β : NaturalTransformation F₁ F₅}
                 {γ : NaturalTransformation F₂ F₃}
                 {δ : NaturalTransformation F₀ F₁}
             → (α ∘₀ β) ∘₁ (γ ∘₀ δ) ≡ (α ∘₁ γ) ∘₀ (β ∘₁ δ)
interchange {C₀ = C₀} {C₁} {C₂} {F₀} {F₁} {F₅} {F₂} {F₃} {F₄} {α} {β} {γ} {δ} =
    begin
      (F₄.F₁ (β.η _) ∘ α.η (F₁.F₀ _)) ∘ (F₃.F₁ (δ.η _) ∘ γ.η (F₀.F₀ _))
    ↓⟨ C₂.assoc ⟩
      F₄.F₁ (β.η _) ∘ (α.η (F₁.F₀ _) ∘ (F₃.F₁ (δ.η _) ∘ γ.η (F₀.F₀ _)))
    ↑⟨ C₂.∘-resp-≡ʳ C₂.assoc ⟩
      F₄.F₁ (β.η _) ∘ ((α.η (F₁.F₀ _) ∘ (F₃.F₁ (δ.η _))) ∘ γ.η (F₀.F₀ _))
    ↓⟨ C₂.∘-resp-≡ʳ (C₂.∘-resp-≡ˡ (α.commute (δ.η _))) ⟩
      F₄.F₁ (β.η _) ∘ ((F₄.F₁ (δ.η _) ∘ α.η (F₀.F₀ _)) ∘ γ.η (F₀.F₀ _))
    ↓⟨ C₂.∘-resp-≡ʳ C₂.assoc ⟩
      F₄.F₁ (β.η _) ∘ (F₄.F₁ (δ.η _) ∘ (α.η (F₀.F₀ _) ∘ γ.η (F₀.F₀ _)))
    ↑⟨ C₂.assoc ⟩
      (F₄.F₁ (β.η _) ∘ F₄.F₁ (δ.η _)) ∘ (α.η (F₀.F₀ _) ∘ γ.η (F₀.F₀ _))
    ↑⟨ C₂.∘-resp-≡ˡ F₄.homomorphism ⟩
      F₄.F₁ (β.η _ ∘C₁ δ.η _) ∘ (α.η (F₀.F₀ _) ∘ γ.η (F₀.F₀ _))
    ∎
  where
  module C₁ = Category C₁ renaming (_∘_ to _∘C₁_; _≡_ to _≡C₁_)
  module C₂ = Category C₂
  module F₀ = Functor F₀
  module F₁ = Functor F₁
  module F₂ = Functor F₂
  module F₃ = Functor F₃
  module F₄ = Functor F₄
  module F₅ = Functor F₅
  module α = NaturalTransformation α
  module β = NaturalTransformation β
  module γ = NaturalTransformation γ
  module δ = NaturalTransformation δ
  open C₁
  open C₂
  open C₂.HomReasoning

.∘₁-resp-≡ : ∀ {o ℓ e} {o′ ℓ′ e′}
               {D : Category o ℓ e} {E : Category o′ ℓ′ e′}
               {A B C : Functor D E}
               {f h : NaturalTransformation B C} {g i : NaturalTransformation A B}
          → f ≡ h → g ≡ i → f ∘₁ g ≡ h ∘₁ i
∘₁-resp-≡ {E = E} f≡h g≡i = Category.∘-resp-≡ E f≡h g≡i

.∘₀-resp-≡ : ∀ {o ℓ e} {o′ ℓ′ e′} {o″ ℓ″ e″}
               {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o″ ℓ″ e″}
               {F F′ : Functor C D} {G G′ : Functor D E}
               {f h : NaturalTransformation G G′} {g i : NaturalTransformation F F′}
           → f ≡ h → g ≡ i → f ∘₀ g ≡ h ∘₀ i
∘₀-resp-≡ {E = E} {G′ = G′} f≡h g≡i = Category.∘-resp-≡ E (Functor.F-resp-≡ G′ g≡i) f≡h

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

open import HoTT
open import cohomology.CofiberSequence
open import cohomology.Exactness
open import cohomology.ExactPairIso
open import cohomology.FunctionOver
open import cohomology.MayerVietoris
open import cohomology.SplitExactRight
open import cohomology.Theory

module cohomology.Coproduct {i} (OT : OrdinaryTheory i) where

open OrdinaryTheory OT
open import cohomology.ConstantFunction cohomology-theory
open import cohomology.Functor cohomology-theory
open import cohomology.Sn OT

{- Cⁿ(X ⊔ Y) == Cⁿ(X ∨ Y) × Cⁿ(S⁰). The proof is by constructing a
 - splitting exact sequence

         0 → Cⁿ(X ∨ Y) → Cⁿ(X ⊔ Y) → C(S⁰)

 - by defining a map [select : S⁰ → X ⊔ Y] such that
   [Cofiber select == X ∨ Y] and [select] has a left inverse. -}

module CofSelect (X Y : Ptd i) where

  select : Sphere {i} 0 → fst (X ⊙⊔ Y)
  select (lift true) = inl (snd X)
  select (lift false) = inr (snd Y)

  ⊙select : fst (⊙Sphere {i} 0 ⊙→ X ⊙⊔ Y)
  ⊙select = (select , idp)

  module Into = CofiberRec select {C = X ∨ Y}
    (winl (snd X))
    add-wglue
    (λ {(lift true) → idp; (lift false) → wglue})

  module Out = WedgeRec {X = X} {Y = Y} {C = Cofiber select}
    (λ x → cfcod _ (inl x))
    (λ y → cfcod _ (inr y))
    (! (cfglue _ (lift true)) ∙ cfglue _ (lift false))

  into = Into.f
  out = Out.f

  into-out : ∀ w → into (out w) == w
  into-out = Wedge-elim
    (λ x → idp)
    (λ y → idp)
    (↓-∘=idf-in into out $
      ap into (ap out wglue)
        =⟨ ap (ap into) Out.glue-β ⟩
      ap into (! (cfglue _ (lift true)) ∙ cfglue _ (lift false))
        =⟨ ap-∙ into (! (cfglue _ (lift true))) (cfglue _ (lift false)) ⟩
      ap into (! (cfglue _ (lift true))) ∙ ap into (cfglue _ (lift false))
        =⟨ ap-! into (cfglue _ (lift true)) ∙ ap ! (Into.glue-β (lift true))
           |in-ctx (λ w → w ∙ ap into (cfglue _ (lift false))) ⟩
      ap into (cfglue _ (lift false))
        =⟨ Into.glue-β (lift false) ⟩
      wglue ∎)

  out-into : ∀ κ → out (into κ) == κ
  out-into = Cofiber-elim _
    (! (cfglue _ (lift true)))
    (λ {(inl x) → idp; (inr y) → idp})
    (λ {(lift true) → ↓-∘=idf-from-square out into $
          ap (ap out) (Into.glue-β (lift true)) ∙v⊡ bl-square _;
        (lift false) → ↓-∘=idf-from-square out into $
          (ap (ap out) (Into.glue-β (lift false)) ∙ Out.glue-β)
          ∙v⊡ lt-square (! (cfglue _ (lift true))) ⊡h vid-square})

  eq : Cofiber select ≃ X ∨ Y
  eq = equiv into out into-out out-into

  ⊙path : ⊙Cof ⊙select == X ⊙∨ Y
  ⊙path = ⊙ua eq idp

  cfcod-over : ⊙cfcod ⊙select == ⊙add-wglue
               [ (λ U → fst (X ⊙⊔ Y ⊙→ U)) ↓ ⊙path ]
  cfcod-over = codomain-over-⊙equiv _ _ _ ▹ pair= idp lemma
    where
    lemma : ap into (! (cfglue _ (lift true))) ∙ idp == idp
    lemma = ∙-unit-r _ ∙ ap-! into (cfglue _ (lift true))
            ∙ ap ! (Into.glue-β (lift true))

  ext-glue-cst :
    ⊙ext-glue == ⊙cst {X = ⊙Cof ⊙select} {Y = ⊙Sphere 1}
  ext-glue-cst = ⊙λ=
    (Cofiber-elim _
      idp
      (λ {(inl _) → ! (merid _ (lift true));
          (inr _) → ! (merid _ (lift false))})
      (λ {(lift true) → ↓-='-from-square $
            ExtGlue.glue-β (lift true)
            ∙v⊡ tr-square (merid _ (lift true))
            ⊡v∙ ! (ap-cst (north _) (glue (lift true)));
          (lift false) → ↓-='-from-square $
            ExtGlue.glue-β (lift false)
            ∙v⊡ tr-square (merid _ (lift false))
            ⊡v∙ ! (ap-cst (north _) (glue (lift false)))}))
    idp

  ext-over : ⊙ext-glue == ⊙cst
             [ (λ U → fst (U ⊙→ ⊙Sphere 1)) ↓ ⊙path ]
  ext-over = ext-glue-cst ◃ domain-over-⊙equiv _ _ _

module C⊔ (n : ℤ) (m : ℕ) (X Y : Ptd i) where

  open CofSelect X Y

  ed : {G : Group i} (φ : GroupHom (C n (⊙Susp^ m (X ⊙⊔ Y))) G)
    → ExactDiag _ _
  ed {G} φ =
    C n (⊙Susp^ m (⊙Sphere 1))
      ⟨ cst-hom ⟩→
    C n (⊙Susp^ m (X ⊙∨ Y))
      ⟨ CF-hom n (⊙susp^-fmap m ⊙add-wglue) ⟩→
    C n (⊙Susp^ m (X ⊙⊔ Y))
      ⟨ φ ⟩→ -- CF-hom n (⊙susp^-fmap m ⊙select)
    G ⊣| -- C n (⊙Susp^ m (⊙Sphere 0))

  es : ExactSeq (ed (CF-hom n (⊙susp^-fmap m ⊙select)))
  es = exact-build (ed (CF-hom n (⊙susp^-fmap m ⊙select)))
    (transport
      (λ g → is-exact g (CF n (⊙susp^-fmap m ⊙add-wglue)))
      (ap (CF n) (⊙susp^-fmap-cst m) ∙ ap GroupHom.⊙f (CF-cst n))
      (transport
        (λ {(_ , g , h) → is-exact (CF n (⊙susp^-fmap m h))
                                   (CF n (⊙susp^-fmap m g))})
        (pair= ⊙path (↓-×-in cfcod-over ext-over))
        (transport
          (λ {(_ , g , h) → is-exact (CF n h) (CF n g)})
          (suspend^-cof= m (⊙cfcod ⊙select) (⊙ext-glue)
            (pair= (Cof².space-path ⊙select) (Cof².cfcod²-over ⊙select)))
          (C-exact n (⊙susp^-fmap m (⊙cfcod ⊙select))))))
    (transport
      (λ {(_ , g) → is-exact (CF n (⊙susp^-fmap m g))
                             (CF n (⊙susp^-fmap m ⊙select))})
      (pair= ⊙path cfcod-over)
      (transport
        (λ {(_ , g , h) → is-exact (CF n h) (CF n g)})
        (suspend^-cof= m ⊙select _ idp)
        (C-exact n (⊙susp^-fmap m ⊙select))))

  module Nonzero (neq : n ≠ ℕ-to-ℤ m) where

    iso : C n (⊙Susp^ m (X ⊙∨ Y)) == C n (⊙Susp^ m (X ⊙⊔ Y))
    iso = exact-pair-iso $
      transport (λ {(G , φ) → ExactSeq (ed {G} φ)})
        (pair= (ap (C n) (⊙Susp^-+ m O
                          ∙ ap (λ k → ⊙Susp^ k (⊙Sphere 0)) (+-unit-r m))
                ∙ C-Sphere-≠ n m neq)
               (prop-has-all-paths-↓
                  {B = λ G → GroupHom (C n (⊙Susp^ m (X ⊙⊔ Y))) G}
                  (contr-is-prop 0ᴳ-hom-in-level)))
        es

    add-wglue-over :
      idhom _ == CF-hom n (⊙susp^-fmap m ⊙add-wglue)
      [ (λ G → GroupHom (C n (⊙Susp^ m (X ⊙∨ Y))) G) ↓ iso ]
    add-wglue-over = codomain-over-iso _ _ _ _ $ codomain-over-equiv _ _

  module Any where

    deselect : fst (X ⊙⊔ Y) → Sphere {i} 0
    deselect (inl _) = lift true
    deselect (inr _) = lift false

    ⊙deselect : fst (X ⊙⊔ Y ⊙→ ⊙Sphere {i} 0)
    ⊙deselect = (deselect , idp)

    deselect-select : ⊙deselect ⊙∘ ⊙select == ⊙idf _
    deselect-select = ⊙λ= (λ {(lift true) → idp; (lift false) → idp}) idp

    module SER = SplitExactRight (C-abelian n _)
      (CF-hom n (⊙susp^-fmap m ⊙add-wglue))
      (CF-hom n (⊙susp^-fmap m ⊙select))
      es
      (CF-hom n (⊙susp^-fmap m ⊙deselect))
      (app= $ ap GroupHom.f $ CF-inverse n
        (⊙susp^-fmap m ⊙select)
        (⊙susp^-fmap m ⊙deselect)
        (! (⊙susp^-fmap-∘ m ⊙deselect ⊙select)
         ∙ ap (⊙susp^-fmap m) deselect-select
         ∙ ⊙susp^-fmap-idf m _))

    iso : C n (⊙Susp^ m (X ⊙⊔ Y))
       == C n (⊙Susp^ m (X ⊙∨ Y)) ×ᴳ C n (⊙Susp^ m (⊙Sphere 0))
    iso = SER.iso

    add-wglue-over :
      CF-hom n (⊙susp^-fmap m ⊙add-wglue) == ×ᴳ-inl
      [ (λ G → GroupHom (C n (⊙Susp^ m (X ⊙∨ Y))) G) ↓ iso ]
    add-wglue-over = SER.φ-over-iso

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels


text:
------------------------------------------------------------------------
-- Indexed containers
------------------------------------------------------------------------

-- Partly based on "Indexed containers" by Altenkirch, Ghani, Hancock,
-- McBride and Morris, and partly based on "Non-wellfounded trees in
-- Homotopy Type Theory" by Ahrens, Capriotti and Spadotti.

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

open import Equality

module Container.Indexed
  {e⁺} (eq : ∀ {a p} → Equality-with-J a p e⁺) where

open Derived-definitions-and-properties eq

open import Prelude

import Bijection eq as B
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq as F hiding (id; _∘_)
open import H-level.Closure eq
open import Univalence-axiom eq

private
  variable
    a ℓ p p₁ p₂ q s : Level
    A I O           : Type a
    P Q R           : A → Type p
    ext f i k o     : A

------------------------------------------------------------------------
-- _⇾_

-- A kind of function space for indexed types.

infix 4 _⇾_

_⇾_ :
  {A : Type a} →
  (A → Type p) → (A → Type q) → Type (a ⊔ p ⊔ q)
P ⇾ Q = ∀ x → P x → Q x

-- An identity function.

id⇾ : P ⇾ P
id⇾ _ = id

-- Composition for _⇾_.

infixr 9 _∘⇾_

_∘⇾_ : Q ⇾ R → P ⇾ Q → P ⇾ R
f ∘⇾ g = λ i → f i ∘ g i

------------------------------------------------------------------------
-- Containers

-- Doubly indexed containers.

record Container₂ (I : Type i) (O : Type o) s p :
                  Type (i ⊔ o ⊔ lsuc (s ⊔ p)) where
  field
    Shape    : O → Type s
    Position : ∀ {o} → Shape o → Type p
    index    : ∀ {o} {s : Shape o} → Position s → I

open Container₂ public

-- Singly indexed containers.

Container : Type i → ∀ s p → Type (i ⊔ lsuc (s ⊔ p))
Container I = Container₂ I I

private
  variable
    C : Container₂ I O s p

-- Container₂ can be expressed as a nested Σ-type.

Container≃Σ :
  Container₂ I O s p ≃
  (∃ λ (S : O → Type s) →
   ∃ λ (P : ∀ {o} → S o → Type p) →
     ∀ {o} {s : S o} → P s → I)
Container≃Σ = Eq.↔→≃
  (λ C → C .Shape , C .Position , C .index)
  (λ (S , P , i) → record { Shape = S; Position = P; index = i })
  refl
  refl

------------------------------------------------------------------------
-- Polynomial functors

-- The polynomial functor associated to a container.

⟦_⟧ :
  {I : Type i} {O : Type o} →
  Container₂ I O s p → (I → Type ℓ) → O → Type (ℓ ⊔ s ⊔ p)
⟦ C ⟧ P i = ∃ λ (s : Shape C i) → (p : Position C s) → P (index C p)

-- A map function.

map : (C : Container₂ I O s p) → P ⇾ Q → ⟦ C ⟧ P ⇾ ⟦ C ⟧ Q
map C f _ (s , g) = s , f _ ∘ g

-- Functor laws.

map-id : map C (id⇾ {P = P}) ≡ id⇾
map-id = refl _

map-∘ :
  (f : Q ⇾ R) (g : P ⇾ Q) →
  map C (f ∘⇾ g) ≡ map C f ∘⇾ map C g
map-∘ _ _ = refl _

-- A preservation lemma.

⟦⟧-cong :
  {I : Type i} {P₁ : I → Type p₁} {P₂ : I → Type p₂} →
  Extensionality? k p (p₁ ⊔ p₂) →
  (C : Container₂ I O s p) →
  (∀ i → P₁ i ↝[ k ] P₂ i) →
  (∀ o → ⟦ C ⟧ P₁ o ↝[ k ] ⟦ C ⟧ P₂ o)
⟦⟧-cong {P₁ = P₁} {P₂ = P₂} ext C P₁↝P₂ o =
  (∃ λ (s : Shape C o) → (p : Position C s) → P₁ (index C p))  ↝⟨ (∃-cong λ _ → ∀-cong ext λ _ → P₁↝P₂ _) ⟩□
  (∃ λ (s : Shape C o) → (p : Position C s) → P₂ (index C p))  □

-- The forward direction of ⟦⟧-cong is an instance of map (at least
-- when k is equivalence).

_ : _≃_.to (⟦⟧-cong ext C f o) ≡ map C (_≃_.to ∘ f) o
_ = refl _

-- The shapes of a container are pointwise equivalent to the
-- polynomial functor of the container applied to the constant
-- function yielding the unit type.
--
-- (This lemma was suggested to me by an anonymous reviewer of a
-- paper.)

Shape≃⟦⟧⊤ :
  (C : Container₂ I O s p) →
  Shape C o ≃ ⟦ C ⟧ (λ _ → ⊤) o
Shape≃⟦⟧⊤ {o = o} C =
  Shape C o                                 ↔⟨ inverse $ drop-⊤-right (λ _ → →-right-zero) ⟩□
  (∃ λ (s : Shape C o) → Position C s → ⊤)  □

------------------------------------------------------------------------
-- Coalgebras

-- The type of coalgebras for a (singly indexed) container.

Coalgebra : {I : Type i} → Container I s p → Type (lsuc (i ⊔ s ⊔ p))
Coalgebra {i = i} {s = s} {p = p} {I = I} C =
  ∃ λ (P : I → Type (i ⊔ s ⊔ p)) → P ⇾ ⟦ C ⟧ P

-- Coalgebra morphisms.

infix 4 _⇨_

_⇨_ :
  {I : Type i} {C : Container I s p} →
  Coalgebra C → Coalgebra C → Type (i ⊔ s ⊔ p)
(P , f) ⇨ (Q , g) = ∃ λ (h : P ⇾ Q) → g ∘⇾ h ≡ map _ h ∘⇾ f

private
  variable
    X Y Z : Coalgebra C

-- An identity morphism.

id⇨ : X ⇨ X
id⇨ = id⇾ , refl _

-- Composition for _⇨_.

infix 9 [_]_∘⇨_

[_]_∘⇨_ : ∀ Z → Y ⇨ Z → X ⇨ Y → X ⇨ Z
[_]_∘⇨_ {Y = _ , g} {X = _ , f} (_ , h) (f₁ , eq₁) (f₂ , eq₂) =
    f₁ ∘⇾ f₂
  , (h ∘⇾ (f₁ ∘⇾ f₂)              ≡⟨⟩
     (h ∘⇾ f₁) ∘⇾ f₂              ≡⟨ cong (_∘⇾ f₂) eq₁ ⟩
     (map _ f₁ ∘⇾ g) ∘⇾ f₂        ≡⟨⟩
     map _ f₁ ∘⇾ (g ∘⇾ f₂)        ≡⟨ cong (map _ f₁ ∘⇾_) eq₂ ⟩
     map _ f₁ ∘⇾ (map _ f₂ ∘⇾ f)  ≡⟨⟩
     map _ (f₁ ∘⇾ f₂) ∘⇾ f        ∎)

-- The property of being a final coalgebra.

Final :
  {I : Type i} {C : Container I s p} →
  Coalgebra C → Type (lsuc (i ⊔ s ⊔ p))
Final X = ∀ Y → Contractible (Y ⇨ X)

-- A perhaps more traditional definition of what it means to be final.

Final′ :
  {I : Type i} {C : Container I s p} →
  Coalgebra C → Type (lsuc (i ⊔ s ⊔ p))
Final′ X =
  ∀ Y → ∃ λ (m : Y ⇨ X) → (m′ : Y ⇨ X) → proj₁ m ≡ proj₁ m′

-- Final X implies Final′ X.

Final→Final′ : (X : Coalgebra C) → Final X → Final′ X
Final→Final′ _ =
  ∀-cong _ λ _ → ∃-cong λ _ → ∀-cong _ λ _ → cong proj₁

-- Final is pointwise propositional (assumption extensionality).

Final-propositional :
  {I : Type i} {C : Container I s p} →
  Extensionality (lsuc (i ⊔ s ⊔ p)) (i ⊔ s ⊔ p) →
  (X : Coalgebra C) →
  Is-proposition (Final X)
Final-propositional ext _ =
  Π-closure ext 1 λ _ →
  Contractible-propositional (lower-extensionality _ lzero ext)

-- Final coalgebras.

Final-coalgebra :
  {I : Type i} →
  Container I s p → Type (lsuc (i ⊔ s ⊔ p))
Final-coalgebra C = ∃ λ (X : Coalgebra C) → Final X

-- Final coalgebras, defined using Final′.

Final-coalgebra′ :
  {I : Type i} →
  Container I s p → Type (lsuc (i ⊔ s ⊔ p))
Final-coalgebra′ C = ∃ λ (X : Coalgebra C) → Final′ X

-- Final-coalgebra C implies Final-coalgebra′ C.

Final-coalgebra→Final-coalgebra′ :
  Final-coalgebra C → Final-coalgebra′ C
Final-coalgebra→Final-coalgebra′ =
  ∃-cong Final→Final′

-- Carriers of final coalgebras (defined using Final′) for a given
-- container are pointwise equivalent.

carriers-of-final-coalgebras-equivalent′ :
  (((P₁ , _) , _) ((P₂ , _) , _) : Final-coalgebra′ C) →
  ∀ i → P₁ i ≃ P₂ i
carriers-of-final-coalgebras-equivalent′ (X₁ , final₁) (X₂ , final₂) i =
  Eq.↔→≃ (proj₁ to i) (proj₁ from i) to∘from from∘to
  where
  to : X₁ ⇨ X₂
  to = proj₁ (final₂ X₁)

  from : X₂ ⇨ X₁
  from = proj₁ (final₁ X₂)

  to∘from : ∀ x → proj₁ ([ X₂ ] to ∘⇨ from) i x ≡ x
  to∘from x =
    proj₁ ([ X₂ ] to ∘⇨ from) i x  ≡⟨ cong (λ f → f i x) $ sym $ proj₂ (final₂ X₂) $ [ X₂ ] to ∘⇨ from ⟩
    proj₁ (proj₁ (final₂ X₂)) i x  ≡⟨ cong (λ f → f i x) $ proj₂ (final₂ X₂) id⇨ ⟩
    proj₁ (id⇨ {X = X₂}) i x       ≡⟨⟩
    x                              ∎

  from∘to : ∀ x → proj₁ ([ X₁ ] from ∘⇨ to) i x ≡ x
  from∘to x =
    proj₁ ([ X₁ ] from ∘⇨ to) i x  ≡⟨ cong (λ f → f i x) $ sym $ proj₂ (final₁ X₁) $ [ X₁ ] from ∘⇨ to ⟩
    proj₁ (proj₁ (final₁ X₁)) i x  ≡⟨ cong (λ f → f i x) $ proj₂ (final₁ X₁) id⇨ ⟩
    proj₁ (id⇨ {X = X₁}) i x       ≡⟨⟩
    x                              ∎

-- The previous lemma relates the "out" functions of the two final
-- coalgebras in a certain way.

out-related′ :
  {C : Container I s p}
  (F₁@((_ , out₁) , _) F₂@((_ , out₂) , _) : Final-coalgebra′ C) →
  map C (_≃_.to ∘ carriers-of-final-coalgebras-equivalent′ F₁ F₂) ∘⇾
    out₁
    ≡
  out₂ ∘⇾ (_≃_.to ∘ carriers-of-final-coalgebras-equivalent′ F₁ F₂)
out-related′ (X₁ , _) (_ , final₂) =
  sym $ proj₂ (proj₁ (final₂ X₁))

-- Carriers of final coalgebras for a given container are pointwise
-- equivalent.

carriers-of-final-coalgebras-equivalent :
  (((P₁ , _) , _) ((P₂ , _) , _) : Final-coalgebra C) →
  ∀ i → P₁ i ≃ P₂ i
carriers-of-final-coalgebras-equivalent =
  carriers-of-final-coalgebras-equivalent′ on
    Final-coalgebra→Final-coalgebra′

-- The previous lemma relates the "out" functions of the two final
-- coalgebras in a certain way.

out-related :
  {C : Container I s p}
  (F₁@((_ , out₁) , _) F₂@((_ , out₂) , _) : Final-coalgebra C) →
  map C (_≃_.to ∘ carriers-of-final-coalgebras-equivalent F₁ F₂) ∘⇾ out₁
    ≡
  out₂ ∘⇾ (_≃_.to ∘ carriers-of-final-coalgebras-equivalent F₁ F₂)
out-related = out-related′ on Final-coalgebra→Final-coalgebra′

-- If X and Y are final coalgebras (with finality defined using
-- Final′), then—assuming extensionality—finality of X (defined using
-- Final) is equivalent to finality of Y.

Final′→Final≃Final :
  {I : Type i} {C : Container I s p}
  ((X , _) (Y , _) : Final-coalgebra′ C) →
  Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p) →
  Final X ↝[ lsuc (i ⊔ s ⊔ p) ∣ i ⊔ s ⊔ p ] Final Y
Final′→Final≃Final {i = i} {s = s} {p = p} {C = C}
  ((X₁ , out₁) , final₁) ((X₂ , out₂) , final₂) ext {k = k} ext′ =
  ∀-cong ext′ λ Y@(_ , f) →
  H-level-cong
    (lower-extensionality? k _ lzero ext′)
    0
    (Σ-cong (lemma₂ Y) λ g →

       out₁ ∘⇾ g ≡ map C g ∘⇾ f                 ↝⟨ inverse $ Eq.≃-≡ (lemma₃ Y) ⟩

       _≃_.to (lemma₃ Y) (out₁ ∘⇾ g) ≡
       _≃_.to (lemma₃ Y) (map C g ∘⇾ f)         ↔⟨⟩

       map C (_≃_.to ∘ lemma₁) ∘⇾ out₁ ∘⇾ g ≡
       map C (_≃_.to ∘ lemma₁) ∘⇾ map C g ∘⇾ f  ↝⟨ ≡⇒↝ _ $ cong (λ h → h ∘⇾ g ≡ map C (_≃_.to ∘ lemma₁) ∘⇾ map C g ∘⇾ f) $
                                                   out-related′ ((X₁ , out₁) , final₁) ((X₂ , out₂) , final₂) ⟩
       out₂ ∘⇾ (_≃_.to ∘ lemma₁) ∘⇾ g ≡
       map C (_≃_.to ∘ lemma₁) ∘⇾ map C g ∘⇾ f  ↔⟨⟩

       out₂ ∘⇾ _≃_.to (lemma₂ Y) g ≡
       map C (_≃_.to (lemma₂ Y) g) ∘⇾ f         □)
  where
  ext₁ = lower-extensionality (s ⊔ p) lzero ext
  ext₂ = lower-extensionality (i ⊔ s) lzero ext

  lemma₁ : ∀ i → X₁ i ≃ X₂ i
  lemma₁ =
    carriers-of-final-coalgebras-equivalent′
      ((X₁ , out₁) , final₁)
      ((X₂ , out₂) , final₂)

  lemma₂ : ((Y , _) : Coalgebra C) → (Y ⇾ X₁) ≃ (Y ⇾ X₂)
  lemma₂ _ =
    ∀-cong ext₁ λ _ →
    ∀-cong ext  λ _ →
    lemma₁ _

  lemma₃ : ((Y , _) : Coalgebra C) → (Y ⇾ ⟦ C ⟧ X₁) ≃ (Y ⇾ ⟦ C ⟧ X₂)
  lemma₃ _ =
    ∀-cong ext₁ λ _ →
    ∀-cong ext  λ _ →
    ⟦⟧-cong ext₂ C lemma₁ _

-- If there is a final C-coalgebra, and we have Final′ X for some
-- C-coalgebra X, then we also have Final X (assuming extensionality).

Final′→Final :
  {I : Type i} {C : Container I s p} →
  Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p) →
  Final-coalgebra C →
  ((X , _) : Final-coalgebra′ C) →
  Final X
Final′→Final ext F₁@(_ , final₁) F₂ =
  Final′→Final≃Final
    (Final-coalgebra→Final-coalgebra′ F₁) F₂
    ext _ final₁

-- Final-coalgebra is pointwise propositional, assuming extensionality
-- and univalence.
--
-- This is a variant of Lemma 5 from "Non-wellfounded trees in
-- Homotopy Type Theory".

Final-coalgebra-propositional :
  {I : Type i} {C : Container I s p} →
  Extensionality (lsuc (i ⊔ s ⊔ p)) (lsuc (i ⊔ s ⊔ p)) →
  Univalence (i ⊔ s ⊔ p) →
  Is-proposition (Final-coalgebra C)
Final-coalgebra-propositional {I = I} {C = C}
  ext univ F₁@((P₁ , out₁) , _) F₂@(X₂@(P₂ , out₂) , _) =
  block λ b →
  Σ-≡,≡→≡ (Σ-≡,≡→≡ (lemma₁ b) (lemma₂ b))
    (Final-propositional (lower-extensionality lzero _ ext) X₂ _ _)
  where
  ext₁′ = lower-extensionality _ lzero ext
  ext₁  = Eq.good-ext ext₁′

  lemma₀ : Block "lemma₀" → ∀ i → P₁ i ≃ P₂ i
  lemma₀ ⊠ = carriers-of-final-coalgebras-equivalent F₁ F₂

  lemma₀-lemma :
    ∀ b x →
    map C (_≃_.to ∘ lemma₀ b) i (out₁ i (_≃_.from (lemma₀ b i) x)) ≡
    out₂ i x
  lemma₀-lemma {i = i} ⊠ x =
    map C (_≃_.to ∘ lemma₀ ⊠) i (out₁ i (_≃_.from (lemma₀ ⊠ i) x))  ≡⟨ cong (λ f → f _ (_≃_.from (lemma₀ ⊠ i) x)) $
                                                                       out-related F₁ F₂ ⟩
    out₂ i (_≃_.to (lemma₀ ⊠ i) (_≃_.from (lemma₀ ⊠ i) x))          ≡⟨ cong (out₂ _) $
                                                                       _≃_.right-inverse-of (lemma₀ ⊠ i) _ ⟩∎
    out₂ i x                                                        ∎

  lemma₁ : Block "lemma₀" → P₁ ≡ P₂
  lemma₁ b =
    apply-ext ext₁ λ i →
    ≃⇒≡ univ (lemma₀ b i)

  lemma₁-lemma₁ = λ b i →
    sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) (subst-const _)   ≡⟨ cong sym Σ-≡,≡→≡-subst-const-refl ⟩
    sym $ cong₂ _,_ (sym (lemma₁ b)) (refl _)        ≡⟨ sym cong₂-sym ⟩
    cong₂ _,_ (sym (sym (lemma₁ b))) (sym (refl _))  ≡⟨ cong₂ (cong₂ _) (sym-sym _) sym-refl ⟩
    cong₂ _,_ (lemma₁ b) (refl i)                    ≡⟨ cong₂-reflʳ _ ⟩∎
    cong (_, i) (lemma₁ b)                           ∎

  lemma₁-lemma₂ = λ b i x →
    subst (_$ i) (sym (lemma₁ b)) x                                    ≡⟨⟩
    subst (_$ i) (sym (apply-ext ext₁ λ i → ≃⇒≡ univ (lemma₀ b i))) x  ≡⟨ cong (flip (subst (_$ i)) _) $ sym $
                                                                          Eq.good-ext-sym ext₁′ _ ⟩
    subst (_$ i) (apply-ext ext₁ λ i → sym (≃⇒≡ univ (lemma₀ b i))) x  ≡⟨ Eq.subst-good-ext ext₁′ _ _ ⟩
    subst id (sym (≃⇒≡ univ (lemma₀ b i))) x                           ≡⟨ subst-id-in-terms-of-inverse∘≡⇒↝ equivalence ⟩
    _≃_.from (≡⇒≃ (≃⇒≡ univ (lemma₀ b i))) x                           ≡⟨ cong (λ eq → _≃_.from eq _) $
                                                                          _≃_.right-inverse-of (≡≃≃ univ) _ ⟩∎
    _≃_.from (lemma₀ b i) x                                            ∎

  lemma₁-lemma₃ = λ b i _ f p →
    subst (λ P → P (index C p)) (lemma₁ b) (f p)          ≡⟨⟩

    subst (λ P → P (index C p))
      (apply-ext ext₁ λ i → ≃⇒≡ univ (lemma₀ b i)) (f p)  ≡⟨ Eq.subst-good-ext ext₁′ _ _ ⟩

    subst id (≃⇒≡ univ (lemma₀ b (index C p))) (f p)      ≡⟨ subst-id-in-terms-of-≡⇒↝ equivalence ⟩

    ≡⇒→ (≃⇒≡ univ (lemma₀ b (index C p))) (f p)           ≡⟨ cong (λ eq → _≃_.to eq _) $
                                                             _≃_.right-inverse-of (≡≃≃ univ) _ ⟩∎
    _≃_.to (lemma₀ b (index C p)) (f p)                   ∎

  lemma₂ = λ b →
    apply-ext (lower-extensionality _ _ ext) λ i →
    apply-ext (lower-extensionality _ _ ext) λ x →

    subst (λ P → P ⇾ ⟦ C ⟧ P) (lemma₁ b) out₁ i x                        ≡⟨⟩

    subst (λ P → ∀ i → P i → ⟦ C ⟧ P i) (lemma₁ b) out₁ i x              ≡⟨ cong (_$ x) subst-∀ ⟩

    subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
      (sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) (refl _))
      (out₁ (subst (λ _ → I) (sym (lemma₁ b)) i)) x                      ≡⟨ elim¹
                                                                              (λ {i′} eq →
                                                                                subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
                                                                                (sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) (refl _))
                                                                                (out₁ (subst (λ _ → I) (sym (lemma₁ b)) i)) x ≡
                                                                                subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
                                                                                (sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) eq)
                                                                                (out₁ i′) x)
                                                                              (refl _)
                                                                              _ ⟩
    subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
      (sym $ Σ-≡,≡→≡ (sym (lemma₁ b)) (subst-const _))
      (out₁ i) x                                                         ≡⟨ cong (λ eq → subst (uncurry λ P i → P i → ⟦ C ⟧ P i) eq _ _) $
                                                                            lemma₁-lemma₁ b i ⟩
    subst (uncurry λ P i → P i → ⟦ C ⟧ P i)
      (cong (_, _) (lemma₁ b))
      (out₁ i) x                                                         ≡⟨ cong (_$ x) $ sym $ subst-∘ _ _ _ ⟩

    subst (λ P → P i → ⟦ C ⟧ P i) (lemma₁ b) (out₁ i) x                  ≡⟨ subst-→ ⟩

    subst (λ P → ⟦ C ⟧ P i) (lemma₁ b)
      (out₁ i (subst (_$ i) (sym (lemma₁ b)) x))                         ≡⟨ cong (subst (λ P → ⟦ C ⟧ P i) _) $ cong (out₁ _) $
                                                                            lemma₁-lemma₂ b i x ⟩
    subst (λ P → ⟦ C ⟧ P i) (lemma₁ b)
      (out₁ i (_≃_.from (lemma₀ b i) x))                                 ≡⟨⟩

    subst (λ P → ∃ λ (s : Shape C i) → ∀ p → P (index C p))
      (lemma₁ b)
      (out₁ i (_≃_.from (lemma₀ b i) x))                                 ≡⟨ push-subst-pair-× _ _ ⟩

    (let s , f = out₁ i (_≃_.from (lemma₀ b i) x) in
     s , subst (λ P → (p : Position C s) → P (index C p)) (lemma₁ b) f)  ≡⟨ (let s , _ = out₁ i (_≃_.from (lemma₀ b i) x) in
                                                                             cong (s ,_) $ apply-ext (lower-extensionality _ _ ext) λ _ → sym $
                                                                             push-subst-application _ _) ⟩
    (let s , f = out₁ i (_≃_.from (lemma₀ b i) x) in
     s , λ p → subst (λ P → P (index C p)) (lemma₁ b) (f p))             ≡⟨ (let _ , f = out₁ i (_≃_.from (lemma₀ b i) x) in
                                                                             cong (_ ,_) $ apply-ext (lower-extensionality _ _ ext) $
                                                                             lemma₁-lemma₃ b i x f) ⟩
    (let s , f = out₁ i (_≃_.from (lemma₀ b i) x) in
     s , λ p → _≃_.to (lemma₀ b (index C p)) (f p))                      ≡⟨⟩

    map C (_≃_.to ∘ lemma₀ b) i (out₁ i (_≃_.from (lemma₀ b i) x))       ≡⟨ lemma₀-lemma b x ⟩∎

    out₂ i x                                                             ∎

------------------------------------------------------------------------
-- Lifting the position type family

-- One can lift the position type family so that it is in a universe
-- that is at least as large as that containing the input indices.

lift-positions :
  {I : Type i} →
  Container₂ I O s p → Container₂ I O s (i ⊔ p)
lift-positions {i = i} C = λ where
  .Shape          → C .Shape
  .Position s     → ↑ i (C .Position s)
  .index (lift p) → C .index p

-- The result of ⟦_⟧ is not affected by lift-positions (up to
-- pointwise equivalence, assuming extensionality).

⟦⟧≃⟦lift-positions⟧ :
  {I : Type i}
  (C : Container₂ I O s p) (P : I → Type ℓ) →
  ⟦ C ⟧ P o ↝[ i ⊔ p ∣ ℓ ] ⟦ lift-positions C ⟧ P o
⟦⟧≃⟦lift-positions⟧ {o = o} C P ext =
  ∃-cong λ s →

  ((      p  :      Position C s)  → P (index C p))  ↝⟨ inverse-ext? (λ ext → Π-cong ext B.↑↔ λ _ → F.id) ext ⟩□
  (((lift p) : ↑ _ (Position C s)) → P (index C p))  □

-- The definition of coalgebras is not affected by lift-positions (up
-- to pointwise equivalence, assuming extensionality).

Coalgebra≃Coalgebra-lift-positions :
  {I : Type i} {C : Container I s p} →
  Coalgebra C ↝[ i ⊔ s ⊔ p ∣ i ⊔ s ⊔ p ] Coalgebra (lift-positions C)
Coalgebra≃Coalgebra-lift-positions
  {i = i} {s = s} {p = p} {C = C} {k = k} ext =

  (∃ λ P → P ⇾ ⟦                C ⟧ P)  ↝⟨ (∃-cong λ P →
                                            ∀-cong (lower-extensionality? k l lzero ext) λ _ →
                                            ∀-cong (lower-extensionality? k l lzero ext) λ _ →
                                            ⟦⟧≃⟦lift-positions⟧ C P (lower-extensionality? k l lzero ext)) ⟩□
  (∃ λ P → P ⇾ ⟦ lift-positions C ⟧ P)  □
  where
  l = i ⊔ s ⊔ p

-- The definition of coalgebra morphisms is not affected by
-- lift-positions (in a certain sense, assuming extensionality).

⇨≃⇨-lift-positions :
  {I : Type i} {C : Container I s p}
  (ext : Extensionality (i ⊔ s ⊔ p) (i ⊔ s ⊔ p)) →
  (X Y : Coalgebra C) →
  (X ⇨ Y) ≃
  (_≃_.to (Coalgebra≃Coalgebra-lift-positions ext) X ⇨
   _≃_.to (Coalgebra≃Coalgebra-lift-positions ext) Y)
⇨≃⇨-lift-positions {i = i} {s = s} {p = p} {C = C} ext (P , f) (Q , g) =
  (∃ λ (h : P ⇾ Q) → g ∘⇾ h ≡ map _ h ∘⇾ f)      ↝⟨ (∃-cong λ _ → inverse $
                                                     Eq.≃-≡ $
                                                     ∀-cong (lower-extensionality l lzero ext) λ _ →
                                                     ∀-cong (lower-extensionality l lzero ext) λ _ →
                                                     ⟦⟧≃⟦lift-positions⟧ C Q (lower-extensionality l lzero ext)) ⟩□
  (∃ λ (h : P ⇾ Q) →
     (Σ-map id (_∘ lower) ∘_) ∘ (g ∘⇾ h) ≡
     (Σ-map id (_∘ lower) ∘_) ∘ (map _ h ∘⇾ f))  □
  where
  l = i ⊔ s ⊔ p

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
module Data.List.Relation.Membership.Proofs where

import Lvl
open import Functional
open import Data.Boolean
open import Data.Boolean.Stmt
open import Data.List
open import Data.List.Functions hiding (skip)
open import Data.List.Relation.Membership
open import Data.List.Relation.Quantification hiding (use ; skip)
open import Data.List.Relation.Quantification.Proofs
import      Data.Tuple as Tuple
open import Logic
open import Logic.Predicate
open import Logic.Propositional
open import Numeral.Natural
open import Structure.Function
open import Structure.Relator.Properties
open import Structure.Relator
open import Structure.Setoid renaming (_≡_ to _≡ₛ_)
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable T A B C : Type{ℓ}

module _ ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
  private variable l l₁ l₂ : List(T)
  private variable a b c x : T

  instance
    [∈]-relatorₗ : UnaryRelator(_∈ l)
    [∈]-relatorₗ = intro p where
      p : Names.Substitution₁(_∈ l)
      p{x ⊰ _}     xy (• q) = • (symmetry(_≡ₛ_) xy 🝖 q)
      p{x ⊰ y ⊰ l} xy (⊰ q) = ⊰ p{y ⊰ l} xy q

  [∈]-self : AllElements(_∈ l)(l)
  [∈]-self {∅}     = ∅
  [∈]-self {x ⊰ l} = (• reflexivity(_≡ₛ_)) ⊰ AllElements-fn (⊰_) ([∈]-self {l})

  [∉]-empty : (a ∉ ∅)
  [∉]-empty ()

  [∈]-in-singleton : (a ∈ singleton(a))
  [∈]-in-singleton = use(reflexivity(_≡ₛ_))

  [∈]-singleton : (a ∈ singleton(b)) ↔ (a ≡ₛ b)
  [∈]-singleton = [↔]-intro L R where
    L : (a ∈ singleton(b)) ← (a ≡ₛ b)
    L p = substitute₁(_∈ _) (symmetry(_≡ₛ_) p) [∈]-in-singleton

    R : (a ∈ singleton(b)) → (a ≡ₛ b)
    R(use p) = p
    R(skip ())

  [∈][++] : (a ∈ (l₁ ++ l₂)) ↔ ((a ∈ l₁) ∨ (a ∈ l₂))
  [∈][++] = [↔]-intro L R where
    L : (a ∈ (l₁ ++ l₂)) ← ((a ∈ l₁) ∨ (a ∈ l₂))
    L {l₁ = ∅}      ([∨]-introᵣ p)     = p
    L {l₁ = x ⊰ l₁} ([∨]-introₗ (• p)) = • p
    L {l₁ = x ⊰ l₁} ([∨]-introₗ (⊰ p)) = ⊰ L {l₁ = l₁} ([∨]-introₗ p)
    L {l₁ = x ⊰ l₁} ([∨]-introᵣ p)     = ⊰ L {l₁ = l₁} ([∨]-introᵣ p)

    R : (a ∈ (l₁ ++ l₂)) → ((a ∈ l₁) ∨ (a ∈ l₂))
    R {l₁ = ∅}      p     = [∨]-introᵣ p
    R {l₁ = x ⊰ l₁} (• p) = [∨]-introₗ (• p)
    R {l₁ = x ⊰ l₁} (⊰ p) with R {l₁ = l₁} p
    ... | [∨]-introₗ q = [∨]-introₗ (⊰ q)
    ... | [∨]-introᵣ q = [∨]-introᵣ q

  [∈]-postpend : (a ∈ postpend a l)
  [∈]-postpend{l = ∅}     = use (reflexivity(_≡ₛ_))
  [∈]-postpend{l = _ ⊰ l} = skip([∈]-postpend{l = l})

  {-
  open import Data.Boolean.Proofs
  [∈]-filter : ∀{f} ⦃ func : Function(f) ⦄ → (a ∈ filter f(l)) ↔ ((a ∈ l) ∧ IsTrue(f(a)))
  [∈]-filter{l = ll}{f = f} = [↔]-intro (Tuple.uncurry L) (x ↦ [∧]-intro (R₁ x) (R₂{l = ll} x)) where
    postulate L : (a ∈ l) → IsTrue(f(a)) → (a ∈ filter f(l))
    {-L {a = a}{l = x ⊰ ∅}     (• p) t with _ ← substitute₁ ⦃ {![≡]-equiv {T = Bool}!} ⦄ (IsTrue) ⦃ {!!} ⦄ p t | 𝑇 ← f(x) = {!!}
    L {a = a}{l = x ⊰ y ⊰ l} (• p) _ = {!!}
    L {a = a}{l = x ⊰ y ⊰ l} (⊰ p) _ = {!!}-}

    postulate R₁ : (a ∈ filter f(l)) → (a ∈ l)
    -- R₁ {l = x ⊰ ∅} p = {!p!}
    -- R₁ {l = x ⊰ x₁ ⊰ l} p = {!!}

    postulate R₂ : (a ∈ filter f(l)) → IsTrue(f(a))
  -}

module _ ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ where
  private variable f : A → B
  private variable l l₁ l₂ : List(T)
  private variable a b c x : T

  [∈]-map : ⦃ func-f : Function(f) ⦄ → (a ∈ l) → (f(a) ∈ (map f(l)))
  [∈]-map {f = f} (use p)  = use (congruence₁(f) p)
  [∈]-map         (skip p) = skip([∈]-map p)

{- TODO: Stuff below is supposed to be moved to Structure.Sets.Proofs

[∈][++]-expandₗ : (a ∈ l₂) → (a ∈ (l₁ ++ l₂))
[∈][++]-expandₗ {l₂ = l₂}{l₁ = l₁} = [↔]-to-[←] ([∈][++] {l₁ = l₁}{l₂ = l₂}) ∘ [∨]-introᵣ

[∈][++]-expandᵣ : (a ∈ l₁) → (a ∈ (l₁ ++ l₂))
[∈][++]-expandᵣ {l₁ = l₁}{l₂ = l₂} = [↔]-to-[←] ([∈][++] {l₁ = l₁}{l₂ = l₂}) ∘ [∨]-introₗ

[∈][⊰]-reorderₗ : (a ∈ (l₁ ++ (x ⊰ l₂))) → (a ∈ (x ⊰ (l₁ ++ l₂)))
[∈][⊰]-reorderₗ (a∈l₁++xl₂) = [∨]-elim left right ([↔]-to-[→] [∈]-[++] (a∈l₁++xl₂)) where
  left : (a ∈ l₁) → (a ∈ (x ⊰ (l₁ ++ l₂)))
  left (a∈l₁) = [∈][⊰]-expand ([∈][++]-expandᵣ {a}{l₁}{l₂} (a∈l₁))

  right : ∀{a} → (a ∈ (x ⊰ l₂)) → (a ∈ (x ⊰ (l₁ ++ l₂)))
  {-right ([∈]-id)              = use
  right ([∈][⊰]-expand (a∈l₂)) = [∈][⊰]-expand ([∈][++]-expandₗ {_}{l₁}{l₂} (a∈l₂))-}

-- [∈][⊰]-reorderᵣ : ∀{a x}{l₁ l₂} → (a ∈ (x ⊰ (l₁ ++ l₂))) → (a ∈ (l₁ ++ (x ⊰ l₂)))
-- [∈][⊰]-reorderᵣ {a}{x}{l₁}{l₂} ([∈]-id) =
-- [∈][⊰]-reorderᵣ {a}{x}{l₁}{l₂} ([∈][⊰]-expand (a∈l₁++l₂)) =

[∈]-in-middle : (a ∈ (l₁ ++ singleton(a) ++ l₂))
[∈]-in-middle{a}{l₁}{l₂} = [↔]-to-[←] ([∈]-[++] {a}{l₁ ++ singleton(a)}{l₂}) ([∨]-introₗ ([∈]-at-last{l = l₁}))

module _ where
  private variable ℓ₂ : Lvl.Level

  [⊆]-substitution : ∀{l₁ l₂ : List(T)} → (l₁ ⊆ l₂) → ∀{P : T → Stmt{ℓ₂}} → (∀{a} → (a ∈ l₂) → P(a)) → (∀{a} → (a ∈ l₁) → P(a))
  [⊆]-substitution (l₁⊆l₂) proof = proof ∘ (l₁⊆l₂)

  [⊇]-substitution : ∀{l₁ l₂ : List(T)} → (l₁ ⊇ l₂) → ∀{P : T → Stmt{ℓ₂}} → (∀{a} → (a ∈ l₁) → P(a)) → (∀{a} → (a ∈ l₂) → P(a))
  [⊇]-substitution (l₁⊇l₂) proof = proof ∘ (l₁⊇l₂)

  [≡]-substitutionₗ : ∀{l₁ l₂ : List(T)} → (l₁ ≡ l₂) → ∀{P : T → Stmt{ℓ₂}} → (∀{a} → (a ∈ l₁) → P(a)) → (∀{a} → (a ∈ l₂) → P(a))
  [≡]-substitutionₗ (l₁≡l₂) = [⊆]-substitution ([↔]-to-[←] (l₁≡l₂))

  [≡]-substitutionᵣ : ∀{l₁ l₂ : List(T)} → (l₁ ≡ l₂) → ∀{P : T → Stmt{ℓ₂}} → (∀{a} → (a ∈ l₂) → P(a)) → (∀{a} → (a ∈ l₁) → P(a))
  [≡]-substitutionᵣ (l₁≡l₂) = [⊆]-substitution ([↔]-to-[→] (l₁≡l₂))
-}

{-
open import Structure.Relator.Properties

instance
  [⊆]-reflexivity : Reflexivity(_⊆_)
  Reflexivity.proof [⊆]-reflexivity = id

instance
  [⊆]-antisymmetry : Antisymmetry(_⊆_)(_≡_)
  Antisymmetry.proof [⊆]-antisymmetry = swap [↔]-intro

instance
  [⊆]-transitivity : Transitivity(_⊆_)
  Transitivity.proof [⊆]-transitivity xy yz = yz ∘ xy

instance
  [⊆]-reflexivity : Reflexivity(_⊆_)

[≡]-reflexivity : ∀{L} → (L ≡ L)
-- [≡]-reflexivity = [↔]-intro [⊆]-reflexivity [⊆]-reflexivity

[≡]-symmetry : ∀{l₁ l₂} → (l₁ ≡ l₂) → (l₂ ≡ l₁)
[≡]-symmetry (l₁≡l₂) {x} with (l₁≡l₂){x}
... | [↔]-intro l r = [↔]-intro r l

[≡]-transitivity : ∀{l₁ l₂ L₃} → (l₁ ≡ l₂) → (l₂ ≡ L₃) → (l₁ ≡ L₃)
[≡]-transitivity (l₁≡l₂) (l₂≡L₃) {x} with [∧]-intro ((l₁≡l₂){x}) ((l₂≡L₃){x})
... | ([∧]-intro (lr₁) (lr₂)) = [↔]-transitivity  (lr₁) (lr₂)

-- [⊆]-application : ∀{l₁ l₂} → (l₁ ⊆ l₂) → ∀{f} → (map f(l₁))⊆(map f(l₂))
-- [⊆]-application proof fl₁ = [∈]-proof.application ∘ proof
-- (∀{x} → (x ∈ l₂) → (x ∈ l₁)) → ∀{f} → (∀{x} → (x ∈ map f(l₂)) → (x ∈ map f(l₁)))

{-
[≡]-included-in : ∀{L : List(T)}{x} → (x ∈ L) → ((x ⊰ L) ≡ L)
[≡]-included-in xL = [⊆]-antisymmetry (sub xL) (super xL) where
  super : ∀{L : List(T)}{x} → (x ∈ L) → ((x ⊰ L) ⊇ L)
  super [∈]-id  [∈]-id  = [∈]-id
  super [∈]-id  (skip p) = skip ?
  super (skip p) [∈]-id  = skip(use ?)
  super (skip p ) (skip q) = skip(skip ?)

  sub : ∀{L : List(T)}{x} → (x ∈ L) → ((x ⊰ L) ⊆ L)
  sub use  use          = use
  sub use  (skip ⦃ p ⦄) = p
  sub skip use          = skip
  sub skip (skip ⦃ p ⦄) = p
-}

postulate [≡]-included-subset : ∀{l₁ l₂ : List(T)} → (l₁ ⊆ l₂) → ((l₁ ++ l₂) ≡ l₂)

postulate [≡]-subset-[++] : ∀{L l₁ l₂ : List(T)} → (l₁ ⊆ L) → (l₂ ⊆ L) → (l₁ ++ l₂ ⊆ L)

[⊆]-with-[⊰] : ∀{l₁ l₂ : List(T)} → (l₁ ⊆ l₂) → ∀{b} → (l₁ ⊆ (b ⊰ l₂))
[⊆]-with-[⊰] (l₁⊆l₂) (x∈l₁) = [∈][⊰]-expand ((l₁⊆l₂) (x∈l₁))

[⊆]-with-[++]ₗ : ∀{l₁ l₂ : List(T)} → (l₁ ⊆ l₂) → ∀{L₃} → (l₁ ⊆ (L₃ ++ l₂))
-- [⊆]-with-[++]ₗ {l₁}{l₂} (l₁⊆l₂) {L₃} (x∈l₁) = [∈][++]-expandₗ {_}{L₃}{l₂} ((l₁⊆l₂) (x∈l₁))

[⊆]-with-[++]ᵣ : ∀{l₁ l₂ : List(T)} → (l₁ ⊆ l₂) → ∀{L₃} → (l₁ ⊆ (l₂ ++ L₃))
[⊆]-with-[++]ᵣ {l₁}{l₂} (l₁⊆l₂) {L₃} (x∈l₁) = [∈][++]-expandᵣ {_}{l₂}{L₃} ((l₁⊆l₂) (x∈l₁))

-- TODO: Does this work? It would be easier to "port" all (∈)-theorems to (⊆)-theorems then.
-- [∈]-to-[⊆]-property : ∀{l₂}{f : List(T) → List(T)} → (∀{a} → (a ∈ l₂) → (a ∈ f(l₂))) → (∀{l₁} → (l₁ ⊆ l₂) → (l₁ ⊆ f(l₂)))

-}

module _ where
  open import Relator.Equals as Id
  open import Relator.Equals.Proofs.Equiv

  non-empty-inclusion-existence : ∀{l : List(T)} → (l Id.≢ ∅) → ∃(_∈ l)
  non-empty-inclusion-existence {l = ∅}     p with () ← p(reflexivity(Id._≡_))
  non-empty-inclusion-existence {l = x ⊰ l} p = [∃]-intro x ⦃ •(reflexivity(Id._≡_)) ⦄


text:
module Base.Free.Instance.Maybe where

open import Data.Unit    using (⊤; tt)
open import Data.Empty   using (⊥)

open import Base.Free    using (Free; pure; impure)
open import Base.Partial using (Partial)
open        Partial

-- Representation of the `Maybe` monad using Free.
Shape : Set
Shape = ⊤

Position : Shape → Set
Position _ = ⊥

Maybe : Set → Set
Maybe = Free Shape Position

Nothing : ∀ {A} → Maybe A
Nothing = impure tt λ()

Just : ∀ {A} → A → Maybe A
Just x = pure x

instance
  maybePartial : Partial Shape Position
  undefined maybePartial   = Nothing
  error     maybePartial _ = Nothing

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler