text:
{-

https://github.com/mietek/hilbert-gentzen

An Agda formalisation of IPC, IS4, ICML, and ILP.  Work in progress.

Made by Miëtek Bak.  Published under the MIT X11 license.

-}

module Everything where

import Common
import Common.Context
import Common.ContextPair
import Common.Predicate
import Common.PredicateBasedContext
import Common.Semantics
import Common.UntypedContext

-- Basic intuitionistic propositional calculus, without ∨ or ⊥.

-- Common syntax.
import BasicIPC.Syntax.Common

-- Hilbert-style formalisation of closed syntax.
import BasicIPC.Syntax.ClosedHilbertSequential  -- Sequences of terms.
import BasicIPC.Syntax.ClosedHilbert            -- Nested terms.

-- Hilbert-style formalisation of syntax.
import BasicIPC.Syntax.HilbertSequential        -- Sequences of terms.
import BasicIPC.Syntax.Hilbert                  -- Nested terms.

-- Gentzen-style formalisation of syntax.
import BasicIPC.Syntax.Gentzen                  -- Simple terms.
import BasicIPC.Syntax.GentzenNormalForm        -- Normal forms and neutrals.
import BasicIPC.Syntax.GentzenSpinalNormalForm  -- Normal forms, neutrals, and spines.

-- Translation between different formalisations of syntax.
import BasicIPC.Syntax.Translation

-- Basic Tarski-style semantics, for soundness only.
import BasicIPC.Semantics.BasicTarski

-- Tarski-style semantics with glueing for α and ▻, after Coquand-Dybjer.
import BasicIPC.Semantics.TarskiGluedClosedImplicit    -- Implicit closed syntax.
import BasicIPC.Semantics.TarskiGluedClosedHilbert     -- Hilbert-style closed syntax.

-- Tarski-style semantics with contexts as concrete worlds, and glueing for α and ▻.
import BasicIPC.Semantics.TarskiConcreteGluedImplicit  -- Implicit syntax.
import BasicIPC.Semantics.TarskiConcreteGluedHilbert   -- Hilbert-style syntax.
import BasicIPC.Semantics.TarskiConcreteGluedGentzen   -- Gentzen-style syntax.

-- Kripke-style semantics with contexts as concrete worlds, and glueing for α and ▻.
import BasicIPC.Semantics.KripkeConcreteGluedImplicit  -- Implicit syntax.
import BasicIPC.Semantics.KripkeConcreteGluedHilbert   -- Hilbert-style syntax.
import BasicIPC.Semantics.KripkeConcreteGluedGentzen   -- Gentzen-style syntax.

-- Kripke-style semantics with contexts as concrete worlds.
import BasicIPC.Semantics.KripkeConcrete

-- Kripke-style semantics with abstract worlds.
import BasicIPC.Semantics.KripkeMcKinseyTarski         -- McKinsey-Tarski embedding.
import BasicIPC.Semantics.KripkeGodel                  -- Gödel embedding.

-- Available metatheory for basic IPC.
--
--       ┌─────┬─────┬─────┬─────┬─────┐
--       │ CH  │ H   │ G   │ Gⁿᶠ │ Gˢⁿᶠ│
-- ┌─────┼─────┼─────┼─────┼─────┼─────┤
-- │ BT  │ e₀  │ e   │ e   │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TGCI│ e₀q₀│ eq₀ │ eq₀ │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TGCH│ e₀q₀│ eq₀ │     │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TCGI│     │ eq  │ eq  │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TCGH│     │ eq  │ eq  │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TCGG│     │ eq  │ eq  │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ KCGI│     │ eq  │ eq  │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ KCGH│     │ eq  │ eq  │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ KCGG│     │ eq  │ eq  │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ KC  │     │ eq  │ eq  │ eq  │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ KMT │     │ eq  │ eq  │ eq  │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ KG  │     │ eq  │ eq  │ eq  │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ HS  │     │     │     │     │ n   │
-- └─────┴─────┴─────┴─────┴─────┴─────┘
--
-- e₀   : Soundness only, for closed terms only.
-- e₀q₀ : Soundness and completeness, for closed terms only.
-- e    : Soundness only.
-- eq₀  : Soundness, for all terms; completeness, for closed terms only.
-- eq   : Soundness and completeness, or normalisation by evaluation.
-- n    : Normalisation by other means.

import BasicIPC.Metatheory.ClosedHilbert-BasicTarski
import BasicIPC.Metatheory.ClosedHilbert-TarskiGluedClosedImplicit
import BasicIPC.Metatheory.ClosedHilbert-TarskiGluedClosedHilbert

import BasicIPC.Metatheory.Hilbert-BasicTarski
import BasicIPC.Metatheory.Hilbert-TarskiGluedClosedImplicit
import BasicIPC.Metatheory.Hilbert-TarskiGluedClosedHilbert
import BasicIPC.Metatheory.Hilbert-TarskiConcreteGluedImplicit
import BasicIPC.Metatheory.Hilbert-TarskiConcreteGluedHilbert
import BasicIPC.Metatheory.Hilbert-TarskiConcreteGluedGentzen
import BasicIPC.Metatheory.Hilbert-KripkeConcreteGluedImplicit
import BasicIPC.Metatheory.Hilbert-KripkeConcreteGluedHilbert
import BasicIPC.Metatheory.Hilbert-KripkeConcreteGluedGentzen
import BasicIPC.Metatheory.Hilbert-KripkeConcrete
import BasicIPC.Metatheory.Hilbert-KripkeMcKinseyTarski
import BasicIPC.Metatheory.Hilbert-KripkeGodel

import BasicIPC.Metatheory.Gentzen-BasicTarski
import BasicIPC.Metatheory.Gentzen-TarskiGluedClosedImplicit
import BasicIPC.Metatheory.Gentzen-TarskiConcreteGluedImplicit
import BasicIPC.Metatheory.Gentzen-TarskiConcreteGluedHilbert
import BasicIPC.Metatheory.Gentzen-TarskiConcreteGluedGentzen
import BasicIPC.Metatheory.Gentzen-KripkeConcreteGluedImplicit
import BasicIPC.Metatheory.Gentzen-KripkeConcreteGluedHilbert
import BasicIPC.Metatheory.Gentzen-KripkeConcreteGluedGentzen
import BasicIPC.Metatheory.Gentzen-KripkeConcrete
import BasicIPC.Metatheory.Gentzen-KripkeMcKinseyTarski
import BasicIPC.Metatheory.Gentzen-KripkeGodel

import BasicIPC.Metatheory.GentzenNormalForm-KripkeConcrete
import BasicIPC.Metatheory.GentzenNormalForm-KripkeMcKinseyTarski
import BasicIPC.Metatheory.GentzenNormalForm-KripkeGodel

import BasicIPC.Metatheory.GentzenSpinalNormalForm-HereditarySubstitution

-- TODO

-- Common syntax.
import BasicT.Syntax.Common

-- Gentzen-style formalisation of syntax.
import BasicT.Syntax.Gentzen
import BasicT.Syntax.GentzenNormalForm

-- Basic Tarski-style semantics, for soundness only.
import BasicT.Semantics.BasicTarski

-- Available metatheory.

import BasicT.Metatheory.Gentzen-BasicTarski

import BasicT.Metatheory.GentzenNormalForm-Unknown

-- Intuitionistic propositional calculus.

-- Common syntax.
import IPC.Syntax.Common

-- Hilbert-style formalisation of closed syntax.
import IPC.Syntax.ClosedHilbertSequential  -- Sequences of terms.
import IPC.Syntax.ClosedHilbert            -- Nested terms.

-- Hilbert-style formalisation of syntax.
import IPC.Syntax.HilbertSequential        -- Sequences of terms.
import IPC.Syntax.Hilbert                  -- Nested terms.

-- Gentzen-style formalisation of syntax.
import IPC.Syntax.Gentzen                  -- Simple terms.
import IPC.Syntax.GentzenNormalForm        -- Normal forms and neutrals.
import IPC.Syntax.GentzenSpinalNormalForm  -- Normal forms, neutrals, and spines.

-- Translation between different formalisations of syntax.
import IPC.Syntax.Translation

-- Basic Tarski-style semantics, for soundness only.
import IPC.Semantics.BasicTarski

-- Kripke-style semantics with exploding abstract worlds.
import IPC.Semantics.KripkeExploding

-- Available metatheory for IPC.
--
--       ┌─────┬─────┬─────┬─────┬─────┐
--       │ CH  │ H   │ G   │ Gⁿᶠ │ Gˢⁿᶠ│
-- ┌─────┼─────┼─────┼─────┼─────┼─────┤
-- │ BT  │ e₀  │ e   │ e   │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ KE  │     │     │ eq  │ eq  │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ HS  │     │     │     │     │ n   │
-- └─────┴─────┴─────┴─────┴─────┴─────┘
--
-- e₀   : Soundness only, for closed terms only.
-- e₀q₀ : Soundness and completeness, for closed terms only.
-- e    : Soundness only.
-- eq₀  : Soundness, for all terms; completeness, for closed terms only.
-- eq   : Soundness and completeness, or normalisation by evaluation.
-- n    : Normalisation by other means.

import IPC.Metatheory.ClosedHilbert-BasicTarski

import IPC.Metatheory.Hilbert-BasicTarski

import IPC.Metatheory.Gentzen-BasicTarski
import IPC.Metatheory.Gentzen-KripkeExploding

import IPC.Metatheory.GentzenNormalForm-KripkeExploding

import IPC.Metatheory.GentzenSpinalNormalForm-HereditarySubstitution

-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.

-- Common syntax.
import BasicIS4.Syntax.Common

-- Hilbert-style formalisation of closed syntax.
import BasicIS4.Syntax.ClosedHilbertSequential        -- Sequences of terms.
import BasicIS4.Syntax.ClosedHilbert                  -- Nested terms.

-- Hilbert-style formalisation of syntax.
import BasicIS4.Syntax.HilbertSequential              -- Sequences of terms.
import BasicIS4.Syntax.Hilbert                        -- Nested terms.

-- Gentzen-style formalisation of syntax, after Bierman-de Paiva.
import BasicIS4.Syntax.Gentzen

-- Hilbert-style formalisation of syntax with context pairs.
import BasicIS4.Syntax.DyadicHilbertSequential        -- Sequences of terms.
import BasicIS4.Syntax.DyadicHilbert                  -- Nested terms.

-- Gentzen-style formalisation of syntax with context pairs, after Pfenning-Davies.
import BasicIS4.Syntax.DyadicGentzen                  -- Simple terms.
import BasicIS4.Syntax.DyadicGentzenNormalForm        -- Normal forms and neutrals.
import BasicIS4.Syntax.DyadicGentzenSpinalNormalForm  -- Normal forms, neutrals, and spines.

-- Gentzen-style formalisation of labelled syntax, after Basin-Matthews-Viganò.
import BasicIS4.Syntax.LabelledGentzen

-- Translation between different formalisations of syntax.
import BasicIS4.Syntax.Translation

-- Basic Kripke-style semantics with abstract worlds, for soundness only.
import BasicIS4.Semantics.BasicKripkeOno                 -- Ono-style conditions.
import BasicIS4.Semantics.BasicKripkeBozicDosen          -- Božić-Došen-style conditions.
import BasicIS4.Semantics.BasicKripkeEwald               -- Ewald-style conditions.
import BasicIS4.Semantics.BasicKripkeAlechina            -- Alechina-style conditions.

-- Tarski-style semantics with glueing for α, ▻, and □, after Gabbay-Nanevski.
import BasicIS4.Semantics.TarskiClosedOvergluedImplicit  -- Implicit closed syntax.
import BasicIS4.Semantics.TarskiClosedOvergluedHilbert   -- Hilbert-style closed syntax.

-- Tarski-style semantics with contexts as concrete worlds, and glueing for α, ▻, and □.
import BasicIS4.Semantics.TarskiOvergluedImplicit        -- Implicit syntax.
import BasicIS4.Semantics.TarskiOvergluedHilbert         -- Hilbert-style syntax.
import BasicIS4.Semantics.TarskiOvergluedGentzen         -- Gentzen-style syntax.

-- Tarski-style semantics with contexts as concrete worlds, and glueing for □ only.
import BasicIS4.Semantics.TarskiGluedImplicit            -- Implicit syntax.
import BasicIS4.Semantics.TarskiGluedHilbert             -- Hilbert-style syntax.
import BasicIS4.Semantics.TarskiGluedGentzen             -- Gentzen-style syntax.

-- Tarski-style semantics with context pairs as concrete worlds, and glueing for α, ▻, and □.
import BasicIS4.Semantics.TarskiOvergluedDyadicImplicit  -- Implicit syntax.
import BasicIS4.Semantics.TarskiOvergluedDyadicHilbert   -- Hilbert-style syntax.
import BasicIS4.Semantics.TarskiOvergluedDyadicGentzen   -- Gentzen-style syntax.

-- Tarski-style semantics with context pairs as concrete worlds, and glueing for □ only.
import BasicIS4.Semantics.TarskiGluedDyadicImplicit      -- Implicit syntax.

-- TODO
import BasicIS4.Semantics.TarskiGluedDyadicHilbert       -- Hilbert-style syntax.

import BasicIS4.Semantics.TarskiGluedDyadicGentzen       -- Gentzen-style syntax.

-- Canonical model equipment for Kripke-style semantics with contexts as concrete worlds.
import BasicIS4.Equipment.KripkeCanonical
import BasicIS4.Equipment.KripkeNonCanonical

-- Canonical model equipment for Kripke-style semantics with context pairs as concrete worlds.
import BasicIS4.Equipment.KripkeDyadicCanonical
import BasicIS4.Equipment.KripkeDyadicNonCanonical

-- Available metatheory for basic IS4.
--
--       ┌─────┬─────┬─────┬─────┬─────┐
--       │ CH  │ H   │ G   │ DH  │ DG  │
-- ┌─────┼─────┼─────┼─────┼─────┼─────┤
-- │ BKO │     │ e   │ e   │ e   │ e   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ BKBD│     │ e   │ e   │ e   │ e   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ BKE │     │ e   │ e   │ e   │ e   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ BKA&│     │ e   │ e   │ e   │ e   │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TCOI│ e₀q₀│ eq₀ │ eq₀ │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TCOH│ e₀q₀│ eq₀ │     │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TOI │     │ eq  │ eq  │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TOH │     │ eq  │     │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TOG │     │ eq  │ eq  │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TGI │     │ eq  │ WIP │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TGH │     │ eq  │     │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TGG │     │     │ WIP │     │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TODI│     │     │     │ eq  │ eq  │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TODH│     │     │     │ eq  │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TODG│     │     │     │ eq  │ eq  │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TGDI│     │     │     │ WIP │ WIP │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TGDH│     │     │     │ WIP │     │
-- ├─────┼─────┼─────┼─────┼─────┼─────┤
-- │ TGDG│     │     │     │     │ WIP │
-- └─────┴─────┴─────┴─────┴─────┴─────┘
--
-- e₀   : Soundness only, for closed terms only.
-- e₀q₀ : Soundness and completeness, for closed terms only.
-- e    : Soundness only.
-- eq₀  : Soundness, for all terms; completeness, for closed terms only.
-- eq   : Soundness and completeness, or normalisation by evaluation.
-- WIP  : Work in progress.

import BasicIS4.Metatheory.ClosedHilbert-TarskiClosedOvergluedImplicit
import BasicIS4.Metatheory.ClosedHilbert-TarskiClosedOvergluedHilbert

import BasicIS4.Metatheory.Hilbert-BasicKripkeOno
import BasicIS4.Metatheory.Hilbert-BasicKripkeBozicDosen
import BasicIS4.Metatheory.Hilbert-BasicKripkeEwald
import BasicIS4.Metatheory.Hilbert-BasicKripkeAlechina
import BasicIS4.Metatheory.Hilbert-TarskiClosedOvergluedImplicit
import BasicIS4.Metatheory.Hilbert-TarskiClosedOvergluedHilbert
import BasicIS4.Metatheory.Hilbert-TarskiOvergluedImplicit
import BasicIS4.Metatheory.Hilbert-TarskiOvergluedHilbert
import BasicIS4.Metatheory.Hilbert-TarskiOvergluedGentzen
import BasicIS4.Metatheory.Hilbert-TarskiGluedImplicit
import BasicIS4.Metatheory.Hilbert-TarskiGluedHilbert

import BasicIS4.Metatheory.Gentzen-BasicKripkeOno
import BasicIS4.Metatheory.Gentzen-BasicKripkeBozicDosen
import BasicIS4.Metatheory.Gentzen-BasicKripkeEwald
import BasicIS4.Metatheory.Gentzen-BasicKripkeAlechina
import BasicIS4.Metatheory.Gentzen-TarskiClosedOvergluedImplicit
import BasicIS4.Metatheory.Gentzen-TarskiOvergluedImplicit
import BasicIS4.Metatheory.Gentzen-TarskiOvergluedGentzen
import BasicIS4.Metatheory.Gentzen-TarskiGluedImplicit -- FIXME
import BasicIS4.Metatheory.Gentzen-TarskiGluedGentzen -- FIXME

import BasicIS4.Metatheory.DyadicHilbert-BasicKripkeOno
import BasicIS4.Metatheory.DyadicHilbert-BasicKripkeBozicDosen
import BasicIS4.Metatheory.DyadicHilbert-BasicKripkeEwald
import BasicIS4.Metatheory.DyadicHilbert-BasicKripkeAlechina
import BasicIS4.Metatheory.DyadicHilbert-TarskiOvergluedDyadicImplicit
import BasicIS4.Metatheory.DyadicHilbert-TarskiOvergluedDyadicHilbert
import BasicIS4.Metatheory.DyadicHilbert-TarskiOvergluedDyadicGentzen
import BasicIS4.Metatheory.DyadicHilbert-TarskiGluedDyadicImplicit -- FIXME
import BasicIS4.Metatheory.DyadicHilbert-TarskiGluedDyadicHilbert

import BasicIS4.Metatheory.DyadicGentzen-BasicKripkeOno
import BasicIS4.Metatheory.DyadicGentzen-BasicKripkeBozicDosen
import BasicIS4.Metatheory.DyadicGentzen-BasicKripkeEwald
import BasicIS4.Metatheory.DyadicGentzen-BasicKripkeAlechina
import BasicIS4.Metatheory.DyadicGentzen-TarskiOvergluedDyadicImplicit
import BasicIS4.Metatheory.DyadicGentzen-TarskiOvergluedDyadicGentzen
import BasicIS4.Metatheory.DyadicGentzen-TarskiGluedDyadicImplicit -- FIXME
import BasicIS4.Metatheory.DyadicGentzen-TarskiGluedDyadicGentzen -- FIXME

import BasicIS4.Metatheory.DyadicGentzenSpinalNormalForm-HereditarySubstitution

-- Basic intuitionistic contextual modal logic, without ∨ or ⊥.

-- Common syntax.
import BasicICML.Syntax.Common

-- Gentzen-style formalisation of syntax with context pairs, after Nanevski-Pfenning-Pientka.
import BasicICML.Syntax.DyadicGentzen
import BasicICML.Syntax.DyadicGentzenNormalForm
import BasicICML.Syntax.DyadicGentzenSpinalNormalForm

-- Available metatheory for basic ICML.
import BasicICML.Metatheory.DyadicGentzenSpinalNormalForm-HereditarySubstitution

-- Basic intuitionistic logic of proofs, without ∨, ⊥, or +.

-- Common syntax.
import BasicILP.Syntax.Common

-- Gentzen-style formalisation of syntax with context pairs.
import BasicILP.Syntax.DyadicGentzen
import BasicILP.Syntax.DyadicGentzenNormalForm

-- (To be rewritten.)

-- Common syntax, with types parametrised by a closed, untyped representation of syntax.
import OldBasicILP.UntypedSyntax.Common

-- Hilbert-style formalisation of closed syntax.
import OldBasicILP.UntypedSyntax.ClosedHilbertSequential  -- Sequences of terms.
import OldBasicILP.UntypedSyntax.ClosedHilbert            -- Nested terms.

-- Translation between different formalisations of syntax.
import OldBasicILP.UntypedSyntax.Translation -- FIXME

-- Common syntax, with types parametrised by closed syntax.
import OldBasicILP.Syntax.Common

-- Hilbert-style formalisation of closed syntax.
import OldBasicILP.Syntax.ClosedHilbertSequential  -- Sequences of terms.
import OldBasicILP.Syntax.ClosedHilbert            -- Nested terms.

-- Translation between different formalisations of syntax.
import OldBasicILP.Syntax.Translation -- FIXME
-- import OldBasicILP.Syntax.Projection -- FIXME

-- (To be rewritten.)

import OlderBasicILP.Indirect
import OlderBasicILP.Indirect.Hilbert.Sequential
import OlderBasicILP.Indirect.Hilbert.Nested
import OlderBasicILP.Indirect.Gentzen
-- import OlderBasicILP.Indirect.Translation
import OlderBasicILP.Direct.Hilbert.Nested
import OlderBasicILP.Direct.Gentzen
-- import OlderBasicILP.Direct.Translation

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module IPL where

data _∧_ (P : Set) (Q : Set) : Set where
  ∧-intro : P → Q → (P ∧ Q)

proof₁ : {P Q : Set} → (P ∧ Q) → P
proof₁ (∧-intro p q) = p

proof₂ : {P Q : Set} → (P ∧ Q) → Q
proof₂ (∧-intro p q) = q

_⇔_ : (P : Set) → (Q : Set) → Set
a ⇔ b = (a → b) ∧ (b → a)

∧-comm′ : (P Q : Set) → (P ∧ Q) → (Q ∧ P)
∧-comm′ _ _ (∧-intro p q) = ∧-intro q p

∧-comm : (P Q : Set) → (P ∧ Q) ⇔ (Q ∧ P)
∧-comm P Q = ∧-intro (∧-comm′ P Q) (∧-comm′ Q P)

∧-comm1′ : {P Q : Set} → (P ∧ Q) → (Q ∧ P)
∧-comm1′ (∧-intro p q) = ∧-intro q p

data _∨_ (P Q : Set) : Set where
   ∨-intro₁ : P → P ∨ Q
   ∨-intro₂ : Q → P ∨ Q

∨-elim : {A B C : Set} → (A → C) → (B → C) → (A ∨ B) → C
∨-elim ac bc (∨-intro₁ a) = ac a
∨-elim ac bc (∨-intro₂ b) = bc b

∨-comm′ : {A B : Set} → (A ∨ B) → (B ∨ A)
∨-comm′ (∨-intro₁ a) = ∨-intro₂ a
∨-comm′ (∨-intro₂ b) = ∨-intro₁ b

∨-comm : {A B : Set} → (A ∨ B) ⇔ (B ∨ A)
∨-comm = ∧-intro ∨-comm′ ∨-comm′

data ⊥ : Set where

¬ : Set → Set
¬ A = A → ⊥

ext: agda

max_stars_repo_name: shouya/thinking-dumps

max_issues_repo_name: shouya/thinking-dumps

max_forks_repo_name: shouya/thinking-dumps


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion of ≤ to <, along with a number of properties
------------------------------------------------------------------------

-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a
-- relation equivalent to the original one (and similarly for
-- < → ≤ → <).

open import Relation.Binary

module Relation.Binary.NonStrictToStrict
         {a ℓ₁ ℓ₂} {A : Set a}
         (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂)
         where

open import Relation.Nullary
open import Relation.Binary.Consequences
open import Function
open import Data.Product
open import Data.Sum

------------------------------------------------------------------------
-- Conversion

-- _≤_ can be turned into _<_ as follows:

_<_ : Rel A _
x < y = (x ≤ y) × ¬ (x ≈ y)

------------------------------------------------------------------------
-- The converted relations have certain properties
-- (if the original relations have certain other properties)

irrefl : Irreflexive _≈_ _<_
irrefl x≈y x<y = proj₂ x<y x≈y

trans : IsPartialOrder _≈_ _≤_ → Transitive _<_
trans po = λ x<y y<z →
  ( PO.trans (proj₁ x<y) (proj₁ y<z)
  , λ x≈z → proj₂ x<y $ lemma (proj₁ x<y) (proj₁ y<z) x≈z
  )
  where
  module PO = IsPartialOrder po

  lemma : ∀ {x y z} → x ≤ y → y ≤ z → x ≈ z → x ≈ y
  lemma x≤y y≤z x≈z =
    PO.antisym x≤y $ PO.trans y≤z (PO.reflexive $ PO.Eq.sym x≈z)

antisym⟶asym : Antisymmetric _≈_ _≤_ → Asymmetric _<_
antisym⟶asym antisym (x≤y , ¬x≈y) (y≤x , ¬y≈x) =
  ¬x≈y (antisym x≤y y≤x)

<-resp-≈ : IsEquivalence _≈_ → _≤_ Respects₂ _≈_ → _<_ Respects₂ _≈_
<-resp-≈ eq ≤-resp-≈ =
  (λ {x y' y} y'≈y x<y' →
    ( proj₁ ≤-resp-≈ y'≈y (proj₁ x<y')
    , λ x≈y → proj₂ x<y' (Eq.trans x≈y (Eq.sym y'≈y))
    )
  ) ,
  (λ {y x' x} x'≈x x'<y →
    ( proj₂ ≤-resp-≈ x'≈x (proj₁ x'<y)
    , λ x≈y → proj₂ x'<y (Eq.trans x'≈x x≈y)
    ))
  where module Eq = IsEquivalence eq

trichotomous : Symmetric _≈_ → Decidable _≈_ →
               Antisymmetric _≈_ _≤_ → Total _≤_ →
               Trichotomous _≈_ _<_
trichotomous ≈-sym ≈-dec antisym total x y with ≈-dec x y
... | yes x≈y = tri≈ (irrefl x≈y) x≈y (irrefl (≈-sym x≈y))
... | no  x≉y with total x y
...   | inj₁ x≤y = tri< (x≤y , x≉y) x≉y
                        (x≉y ∘ antisym x≤y ∘ proj₁)
...   | inj₂ x≥y = tri> (x≉y ∘ flip antisym x≥y ∘ proj₁) x≉y
                        (x≥y , x≉y ∘ ≈-sym)

decidable : Decidable _≈_ → Decidable _≤_ → Decidable _<_
decidable ≈-dec ≤-dec x y with ≈-dec x y | ≤-dec x y
... | yes x≈y | _       = no (flip proj₂ x≈y)
... | no  x≉y | yes x≤y = yes (x≤y , x≉y)
... | no  x≉y | no  x≰y = no (x≰y ∘ proj₁)

isPartialOrder⟶isStrictPartialOrder :
  IsPartialOrder _≈_ _≤_ → IsStrictPartialOrder _≈_ _<_
isPartialOrder⟶isStrictPartialOrder po = record
  { isEquivalence = PO.isEquivalence
  ; irrefl        = irrefl
  ; trans         = trans po
  ; <-resp-≈      = <-resp-≈ PO.isEquivalence PO.≤-resp-≈
  } where module PO = IsPartialOrder po

isTotalOrder⟶isStrictTotalOrder :
  Decidable _≈_ → IsTotalOrder _≈_ _≤_ → IsStrictTotalOrder _≈_ _<_
isTotalOrder⟶isStrictTotalOrder dec-≈ tot = record
  { isEquivalence = TO.isEquivalence
  ; trans         = trans TO.isPartialOrder
  ; compare       = trichotomous TO.Eq.sym dec-≈ TO.antisym TO.total
  ; <-resp-≈      = <-resp-≈ TO.isEquivalence TO.≤-resp-≈
  } where module TO = IsTotalOrder tot

isDecTotalOrder⟶isStrictTotalOrder :
  IsDecTotalOrder _≈_ _≤_ → IsStrictTotalOrder _≈_ _<_
isDecTotalOrder⟶isStrictTotalOrder dtot =
  isTotalOrder⟶isStrictTotalOrder DTO._≟_ DTO.isTotalOrder
  where module DTO = IsDecTotalOrder dtot


text:
-- This module is used to illustrate how to import a non-parameterised module.
module examples.syntax.ModuleA where

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

  eval : Nat -> Nat
  eval zero		    = zero
  eval (suc x)		    = suc (eval x)
  eval (plus zero y)	    = eval y
  eval (plus (suc x) y)	    = suc (eval (plus x y))
  eval (plus (plus x y) z)  = eval (plus x (plus y z))

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2012-09-24 Ensure that size successor is monotone
{-# OPTIONS --sized-types #-}
module SizeSucMonotone where

open import Common.Size

data Bool : Set where
  true false : Bool

-- T should be monotone in its second arg
T : Bool → Size → Set
T true  i = Size< i
T false i = Size< (↑ i)

test : {x : Bool}{i : Size}{j : Size< i} → T x j → T x i
test h = h

max_stars_repo_name: larrytheliquid/agda


text:
module Data.String.Exts where

open import Data.Bool hiding (_<?_)
open import Data.Char hiding (_<?_)
open import Data.String hiding (_<?_)
open import Data.Maybe
open import Data.Nat

open import Relation.Nullary.Decidable

{-#
  FOREIGN GHC
  import Data.Text
#-}

postulate
  strHead : String -> Maybe Char
  strNull : String -> Bool
  strTake : ℕ -> String -> String
  strDrop : ℕ -> String -> String
  stripPrefix : String -> String -> Maybe String
  strLength : String -> ℕ

{-# COMPILE GHC strHead = (fmap fst) . uncons #-}
{-# COMPILE GHC strNull = Data.Text.null #-}
{-# COMPILE GHC strTake = Data.Text.take . fromIntegral #-}
{-# COMPILE GHC strDrop = Data.Text.drop . fromIntegral #-}
{-# COMPILE GHC stripPrefix = stripPrefix #-}
{-# COMPILE GHC strLength = toInteger . Data.Text.length #-}

shortenString : ℕ -> String -> String
shortenString l s = if ⌊ length s <? l ⌋ then s else strTake l s ++ "..."

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


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

open import HoTT
import homotopy.RelativelyConstantToSetExtendsViaSurjection as SurjExt

module homotopy.vankampen.Code {i j k l}
  (span : Span {i} {j} {k})
  {D : Type l} (h : D → Span.C span) (h-is-surj : is-surj h) where

  open Span span
  open import homotopy.vankampen.CodeAP span h h-is-surj
  open import homotopy.vankampen.CodeBP span h h-is-surj

  pcAA-to-pcBA : ∀ d₀ {a} → precodeAA (f (h d₀)) a → precodeBA (g (h d₀)) a
  pcAB-to-pcBB : ∀ d₀ {b} → precodeAB (f (h d₀)) b → precodeBB (g (h d₀)) b
  pcAA-to-pcBA d₀ (pc-a pA) = pc-bba d₀ (pc-b idp₀) pA
  pcAA-to-pcBA d₀ (pc-aba d pc pA) = pc-bba d (pcAB-to-pcBB d₀ pc) pA
  pcAB-to-pcBB d₀ (pc-aab d pc pB) = pc-bab d (pcAA-to-pcBA d₀ pc) pB

  abstract
    pcAA-to-pcBA-rel : ∀ d₀ {a} {pcAA₁ pcAA₂ : precodeAA (f (h d₀)) a}
      → precodeAA-rel pcAA₁ pcAA₂
      → precodeBA-rel (pcAA-to-pcBA d₀ pcAA₁) (pcAA-to-pcBA d₀ pcAA₂)
    pcAB-to-pcBB-rel : ∀ d₀ {a} {pcAB₁ pcAB₂ : precodeAB (f (h d₀)) a}
      → precodeAB-rel pcAB₁ pcAB₂
      → precodeBB-rel (pcAB-to-pcBB d₀ pcAB₁) (pcAB-to-pcBB d₀ pcAB₂)
    pcAA-to-pcBA-rel d₀ (pcAAr-idp₀-idp₀ pcAA) = pcBAr-idp₀-idp₀ (pcAA-to-pcBA d₀ pcAA)
    pcAA-to-pcBA-rel d₀ (pcAAr-cong r pA) = pcBAr-cong (pcAB-to-pcBB-rel d₀ r) pA
    pcAB-to-pcBB-rel d₀ (pcABr-idp₀-idp₀ pcAB) = pcBBr-idp₀-idp₀ (pcAB-to-pcBB d₀ pcAB)
    pcAB-to-pcBB-rel d₀ (pcABr-switch pcAB pC) = pcBBr-switch (pcAB-to-pcBB d₀ pcAB) pC
    pcAB-to-pcBB-rel d₀ (pcABr-cong r pB) = pcBBr-cong (pcAA-to-pcBA-rel d₀ r) pB

  cAA-to-cBA : ∀ d₀ {a} → codeAA (f (h d₀)) a → codeBA (g (h d₀)) a
  cAA-to-cBA d₀ = SetQuot-rec SetQuot-level (q[_] ∘ pcAA-to-pcBA d₀) (quot-rel ∘ pcAA-to-pcBA-rel d₀)
  cAB-to-cBB : ∀ d₀ {b} → codeAB (f (h d₀)) b → codeBB (g (h d₀)) b
  cAB-to-cBB d₀ = SetQuot-rec SetQuot-level (q[_] ∘ pcAB-to-pcBB d₀) (quot-rel ∘ pcAB-to-pcBB-rel d₀)

  -- BX to AX
  pcBA-to-pcAA : ∀ d₀ {a} → precodeBA (g (h d₀)) a → precodeAA (f (h d₀)) a
  pcBB-to-pcAB : ∀ d₀ {b} → precodeBB (g (h d₀)) b → precodeAB (f (h d₀)) b
  pcBA-to-pcAA d₀ (pc-bba d pc pA) = pc-aba d (pcBB-to-pcAB d₀ pc) pA
  pcBB-to-pcAB d₀ (pc-b pB) = pc-aab d₀ (pc-a idp₀) pB
  pcBB-to-pcAB d₀ (pc-bab d pc pB) = pc-aab d (pcBA-to-pcAA d₀ pc) pB

  abstract
    pcBA-to-pcAA-rel : ∀ d₀ {a} {pcBA₁ pcBA₂ : precodeBA (g (h d₀)) a}
      → precodeBA-rel pcBA₁ pcBA₂
      → precodeAA-rel (pcBA-to-pcAA d₀ pcBA₁) (pcBA-to-pcAA d₀ pcBA₂)
    pcBB-to-pcAB-rel : ∀ d₀ {a} {pcBB₁ pcBB₂ : precodeBB (g (h d₀)) a}
      → precodeBB-rel pcBB₁ pcBB₂
      → precodeAB-rel (pcBB-to-pcAB d₀ pcBB₁) (pcBB-to-pcAB d₀ pcBB₂)
    pcBA-to-pcAA-rel d₀ (pcBAr-idp₀-idp₀ pcBA) = pcAAr-idp₀-idp₀ (pcBA-to-pcAA d₀ pcBA)
    pcBA-to-pcAA-rel d₀ (pcBAr-cong r pA) = pcAAr-cong (pcBB-to-pcAB-rel d₀ r) pA
    pcBB-to-pcAB-rel d₀ (pcBBr-idp₀-idp₀ pcBB) = pcABr-idp₀-idp₀ (pcBB-to-pcAB d₀ pcBB)
    pcBB-to-pcAB-rel d₀ (pcBBr-switch pcBB pC) = pcABr-switch (pcBB-to-pcAB d₀ pcBB) pC
    pcBB-to-pcAB-rel d₀ (pcBBr-cong r pB) = pcABr-cong (pcBA-to-pcAA-rel d₀ r) pB

  cBA-to-cAA : ∀ d₀ {a} → codeBA (g (h d₀)) a → codeAA (f (h d₀)) a
  cBA-to-cAA d₀ = SetQuot-rec SetQuot-level (q[_] ∘ pcBA-to-pcAA d₀) (quot-rel ∘ pcBA-to-pcAA-rel d₀)
  cBB-to-cAB : ∀ d₀ {b} → codeBB (g (h d₀)) b → codeAB (f (h d₀)) b
  cBB-to-cAB d₀ = SetQuot-rec SetQuot-level (q[_] ∘ pcBB-to-pcAB d₀) (quot-rel ∘ pcBB-to-pcAB-rel d₀)

  -- roundtrips
  abstract
    pcBA-to-pcAA-to-pcBA : ∀ d₀ {a} (pcBA : precodeBA _ a)
      → q[ pcAA-to-pcBA d₀ (pcBA-to-pcAA d₀ pcBA) ] == q[ pcBA ] :> codeBA _ a
    pcBB-to-pcAB-to-pcBB : ∀ d₀ {b} (pcBB : precodeBB _ b)
      → q[ pcAB-to-pcBB d₀ (pcBB-to-pcAB d₀ pcBB) ] == q[ pcBB ] :> codeBB _ b
    pcBA-to-pcAA-to-pcBA d₀ (pc-bba d pc pA) = pcBB-to-pcAB-to-pcBB d₀ pc |in-ctx λ c → c-bba d c pA
    pcBB-to-pcAB-to-pcBB d₀ (pc-b pB) = pcBB-idp₀-idp₀-head pB
    pcBB-to-pcAB-to-pcBB d₀ (pc-bab d pc pB) = pcBA-to-pcAA-to-pcBA d₀ pc |in-ctx λ c → c-bab d c pB

    pcAA-to-pcBA-to-pcAA : ∀ d₀ {a} (pcAA : precodeAA _ a)
      → q[ pcBA-to-pcAA d₀ (pcAA-to-pcBA d₀ pcAA) ] == q[ pcAA ] :> codeAA _ a
    pcAB-to-pcBB-to-pcAB : ∀ d₀ {b} (pcAB : precodeAB _ b)
      → q[ pcBB-to-pcAB d₀ (pcAB-to-pcBB d₀ pcAB) ] == q[ pcAB ] :> codeAB _ b
    pcAA-to-pcBA-to-pcAA d₀ (pc-aba d pc pA) = pcAB-to-pcBB-to-pcAB d₀ pc |in-ctx λ c → c-aba d c pA
    pcAA-to-pcBA-to-pcAA d₀ (pc-a pA) = pcAA-idp₀-idp₀-head pA
    pcAB-to-pcBB-to-pcAB d₀ (pc-aab d pc pB) = pcAA-to-pcBA-to-pcAA d₀ pc |in-ctx λ c → c-aab d c pB

  private
    pcAA-lemma : ∀ d₁ d₂ {a₁} (p : h d₂ == h d₁) (pcAA : precodeAA _ a₁)
      →  q[ pcBA-prepend d₁ [ ap g p ] (pcAA-to-pcBA d₁ pcAA) ]
      == q[ pcAA-to-pcBA d₂ (pcAA-prepend d₁ [ ap f p ] pcAA) ]
    pcAB-lemma : ∀ d₁ d₂ {b₁} (p : h d₂ == h d₁) (pcAB : precodeAB _ b₁)
      →  q[ pcBB-prepend d₁ [ ap g p ] (pcAB-to-pcBB d₁ pcAB) ]
      == q[ pcAB-to-pcBB d₂ (pcAB-prepend d₁ [ ap f p ] pcAB) ]
    pcAA-lemma d₁ d₂ p (pc-a pA) = ap (λ c → c-bba d₁ c pA) $ ! $
      q[ ⟧b idp₀ bb⟦ _ ⟧a [ ap f p ] ba⟦ _ ⟧b idp₀ ]
        =⟨ quot-rel (pcBBr-switch (⟧b idp₀) [ p ]) ⟩
      q[ ⟧b idp₀ bb⟦ _ ⟧a idp₀ ba⟦ _ ⟧b [ ap g p ] ]
        =⟨ pcBB-idp₀-idp₀-head [ ap g p ] ⟩
      q[ ⟧b [ ap g p ] ]
        =⟨ ! (quot-rel (pcBBr-idp₀-idp₀ (pc-b [ ap g p ]))) ⟩
      q[ ⟧b [ ap g p ] bb⟦ _ ⟧a idp₀ ba⟦ _ ⟧b idp₀ ]
        =∎
    pcAA-lemma d₁ d₂ p (pc-aba d pc pA) = pcAB-lemma d₁ d₂ p pc |in-ctx (λ c → c-bba d c pA)
    pcAB-lemma d₁ d₂ p (pc-aab d pc pB) = pcAA-lemma d₁ d₂ p pc |in-ctx (λ c → c-bab d c pB)

  module CodeAAEquivCodeBA (a₁ : A) where

    eqv-on-image : (d₀ : D) → codeAA (f (h d₀)) a₁ ≃ codeBA (g (h d₀)) a₁
    eqv-on-image d₀ = equiv to from to-from from-to where
      to : codeAA (f (h d₀)) a₁ → codeBA (g (h d₀)) a₁
      to = cAA-to-cBA d₀

      from : codeBA (g (h d₀)) a₁ → codeAA (f (h d₀)) a₁
      from = cBA-to-cAA d₀

      abstract
        to-from : ∀ cBA → to (from cBA) == cBA
        to-from = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-is-set)
          (pcBA-to-pcAA-to-pcBA d₀)
          (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

        from-to : ∀ cAA → from (to cAA) == cAA
        from-to = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-is-set)
          (pcAA-to-pcBA-to-pcAA d₀)
          (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

    abstract
      eqv-is-const : ∀ d₁ d₂ (p : h d₁ == h d₂)
        → eqv-on-image d₁ == eqv-on-image d₂
        [ (λ c → codeAA (f c) a₁ ≃ codeBA (g c) a₁) ↓ p ]
      eqv-is-const d₁ d₂ p = ↓-Subtype-in (λ d → is-equiv-prop) $
        ↓-→-from-transp $ λ= $
          SetQuot-elim (λ _ → =-preserves-set SetQuot-is-set)
            (λ pcAA →
              transport (λ c → codeBA (g c) a₁) p q[ pcAA-to-pcBA d₁ pcAA ]
                =⟨ ap-∘ (λ b → codeBA b a₁) g p |in-ctx (λ p → coe p q[ pcAA-to-pcBA d₁ pcAA ]) ⟩
              transport (λ b → codeBA b a₁) (ap g p) q[ pcAA-to-pcBA d₁ pcAA ]
                =⟨ transp-cBA-l d₁ (ap g p) (pcAA-to-pcBA d₁ pcAA) ⟩
              q[ pcBA-prepend d₁ [ ! $ ap g p ] (pcAA-to-pcBA d₁ pcAA) ]
                =⟨ !-ap g p |in-ctx (λ p → q[ pcBA-prepend d₁ [ p ] (pcAA-to-pcBA d₁ pcAA) ]) ⟩
              q[ pcBA-prepend d₁ [ ap g (! p) ] (pcAA-to-pcBA d₁ pcAA) ]
                =⟨ pcAA-lemma d₁ d₂ (! p) pcAA ⟩
              q[ pcAA-to-pcBA d₂ (pcAA-prepend d₁ [ ap f (! p) ] pcAA) ]
                =⟨ ap-! f p |in-ctx (λ p → q[ pcAA-to-pcBA d₂ (pcAA-prepend d₁ [ p ] pcAA) ]) ⟩
              q[ pcAA-to-pcBA d₂ (pcAA-prepend d₁ [ ! $ ap f p ] pcAA) ]
                =⟨ ! $ transp-cAA-l d₁ (ap f p) pcAA |in-ctx cAA-to-cBA d₂ ⟩
              cAA-to-cBA d₂ (transport (λ a → codeAA a a₁) (ap f p) q[ pcAA ])
                =⟨ ∘-ap (λ c → codeAA c a₁) f p |in-ctx (λ p → coe p q[ pcAA ]) |in-ctx cAA-to-cBA d₂ ⟩
              cAA-to-cBA d₂ (transport (λ c → codeAA (f c) a₁) p q[ pcAA ])
                =∎)
            (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

    module SE = SurjExt
      (λ c → ≃-is-set SetQuot-is-set SetQuot-is-set)
      h h-is-surj
      eqv-on-image
      eqv-is-const

    abstract
      eqv : ∀ c → codeAA (f c) a₁ ≃ codeBA (g c) a₁
      eqv = SE.ext

      eqv-β : ∀ d → eqv (h d) == eqv-on-image d
      eqv-β = SE.β

  module CodeABEquivCodeBB (b₁ : B) where

    eqv-on-image : (d₀ : D) → codeAB (f (h d₀)) b₁ ≃ codeBB (g (h d₀)) b₁
    eqv-on-image d₀ = equiv to from to-from from-to where
      to : codeAB (f (h d₀)) b₁ → codeBB (g (h d₀)) b₁
      to = cAB-to-cBB d₀

      from : codeBB (g (h d₀)) b₁ → codeAB (f (h d₀)) b₁
      from = cBB-to-cAB d₀

      abstract
        to-from : ∀ cBB → to (from cBB) == cBB
        to-from = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-is-set)
          (pcBB-to-pcAB-to-pcBB d₀)
          (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

        from-to : ∀ cAB → from (to cAB) == cAB
        from-to = SetQuot-elim
          (λ _ → =-preserves-set SetQuot-is-set)
          (pcAB-to-pcBB-to-pcAB d₀)
          (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

    abstract
      eqv-is-const : ∀ d₁ d₂ (p : h d₁ == h d₂)
        → eqv-on-image d₁ == eqv-on-image d₂
        [ (λ c → codeAB (f c) b₁ ≃ codeBB (g c) b₁) ↓ p ]
      eqv-is-const d₁ d₂ p = ↓-Subtype-in (λ d → is-equiv-prop) $
        ↓-→-from-transp $ λ= $
          SetQuot-elim (λ _ → =-preserves-set SetQuot-is-set)
            (λ pcAB →
              transport (λ c → codeBB (g c) b₁) p q[ pcAB-to-pcBB d₁ pcAB ]
                =⟨ ap-∘ (λ b → codeBB b b₁) g p |in-ctx (λ p → coe p q[ pcAB-to-pcBB d₁ pcAB ]) ⟩
              transport (λ b → codeBB b b₁) (ap g p) q[ pcAB-to-pcBB d₁ pcAB ]
                =⟨ transp-cBB-l d₁ (ap g p) (pcAB-to-pcBB d₁ pcAB) ⟩
              q[ pcBB-prepend d₁ [ ! $ ap g p ] (pcAB-to-pcBB d₁ pcAB) ]
                =⟨ !-ap g p |in-ctx (λ p → q[ pcBB-prepend d₁ [ p ] (pcAB-to-pcBB d₁ pcAB) ]) ⟩
              q[ pcBB-prepend d₁ [ ap g (! p) ] (pcAB-to-pcBB d₁ pcAB) ]
                =⟨ pcAB-lemma d₁ d₂ (! p) pcAB ⟩
              q[ pcAB-to-pcBB d₂ (pcAB-prepend d₁ [ ap f (! p) ] pcAB) ]
                =⟨ ap-! f p |in-ctx (λ p → q[ pcAB-to-pcBB d₂ (pcAB-prepend d₁ [ p ] pcAB) ]) ⟩
              q[ pcAB-to-pcBB d₂ (pcAB-prepend d₁ [ ! $ ap f p ] pcAB) ]
                =⟨ ! $ transp-cAB-l d₁ (ap f p) pcAB |in-ctx cAB-to-cBB d₂ ⟩
              cAB-to-cBB d₂ (transport (λ a → codeAB a b₁) (ap f p) q[ pcAB ])
                =⟨ ∘-ap (λ c → codeAB c b₁) f p |in-ctx (λ p → coe p q[ pcAB ]) |in-ctx cAB-to-cBB d₂ ⟩
              cAB-to-cBB d₂ (transport (λ c → codeAB (f c) b₁) p q[ pcAB ])
                =∎)
            (λ _ → prop-has-all-paths-↓ (SetQuot-is-set _ _))

    module SE = SurjExt
      (λ c → ≃-is-set SetQuot-is-set SetQuot-is-set)
      h h-is-surj
      eqv-on-image
      eqv-is-const

    abstract
      eqv : ∀ c → codeAB (f c) b₁ ≃ codeBB (g c) b₁
      eqv = SE.ext

      eqv-β : ∀ d → eqv (h d) == eqv-on-image d
      eqv-β = SE.β

  module EqvPAIdEqvPB where
    abstract
      path-on-image : ∀ d₀ d₁
        →  CodeAAEquivCodeBA.eqv (f (h d₁)) (h d₀)
        == CodeABEquivCodeBB.eqv (g (h d₁)) (h d₀)
        [ (λ p → codeAP (f (h d₀)) p ≃ codeBP (g (h d₀)) p) ↓ glue (h d₁) ]
      path-on-image d₀ d₁ =
        CodeAAEquivCodeBA.eqv-β (f (h d₁)) d₀
        ∙ᵈ lemma
        ∙'ᵈ ! (CodeABEquivCodeBB.eqv-β (g (h d₁)) d₀) where
        lemma : CodeAAEquivCodeBA.eqv-on-image (f (h d₁)) d₀
             == CodeABEquivCodeBB.eqv-on-image (g (h d₁)) d₀
             [ (λ p → codeAP (f (h d₀)) p ≃ codeBP (g (h d₀)) p) ↓ glue (h d₁) ]
        lemma = ↓-Subtype-in (λ d → is-equiv-prop) $
          ↓-→-from-transp $ λ= $ SetQuot-elim
            (λ _ → =-preserves-set SetQuot-is-set)
            (λ pcAA →
              transport (λ p → codeBP (g (h d₀)) p) (glue (h d₁)) q[ pcAA-to-pcBA d₀ pcAA ]
                =⟨ transp-cBP-glue d₁ (pcAA-to-pcBA d₀ pcAA) ⟩
              q[ pcAA-to-pcBA d₀ pcAA ba⟦ d₁ ⟧b idp₀ ]
                =⟨ ! $ transp-cAP-glue d₁ pcAA |in-ctx cAB-to-cBB d₀ ⟩
              cAB-to-cBB d₀ (transport (λ p → codeAP (f (h d₀)) p) (glue (h d₁)) q[ pcAA ])
                =∎)
            (λ _ → prop-has-all-paths-↓ $ SetQuot-is-set _ _)

    abstract
      path : ∀ c₀ c₁
        →  CodeAAEquivCodeBA.eqv (f c₁) c₀
        == CodeABEquivCodeBB.eqv (g c₁) c₀
        [ (λ p → codeAP (f c₀) p ≃ codeBP (g c₀) p) ↓ glue c₁ ]
      path = SurjExt.ext
        (λ c₀ → Π-is-set λ c₁ → ↓-preserves-level $ ≃-is-set SetQuot-is-set SetQuot-is-set)
        h h-is-surj
        (λ d₀ → SurjExt.ext
          (λ c₁ → ↓-preserves-level $ ≃-is-set SetQuot-is-set SetQuot-is-set)
          h h-is-surj
          (λ d₁ → path-on-image d₀ d₁)
          (λ _ _ _ → prop-has-all-paths-↓ $ ↓-level $ ≃-is-set SetQuot-is-set SetQuot-is-set))
        (λ _ _ _ → prop-has-all-paths-↓ $ Π-is-prop λ _ → ↓-level $ ≃-is-set SetQuot-is-set SetQuot-is-set)

  cAP-equiv-cBP : ∀ c₀ p₁ → codeAP (f c₀) p₁ ≃ codeBP (g c₀) p₁
  cAP-equiv-cBP c₀ = Pushout-elim
    {P = λ p₁ → codeAP (f c₀) p₁ ≃ codeBP (g c₀) p₁}
    (λ a₁ → CodeAAEquivCodeBA.eqv a₁ c₀)
    (λ b₁ → CodeABEquivCodeBB.eqv b₁ c₀)
    (λ c₁ → EqvPAIdEqvPB.path c₀ c₁)

  module Code = PushoutRec
    {D = Pushout span → Type (lmax (lmax (lmax i j) k) l)}
    codeAP codeBP (λ c₀ → λ= $ ua ∘ cAP-equiv-cBP c₀)

  code : Pushout span → Pushout span → Type (lmax (lmax (lmax i j) k) l)
  code = Code.f

  abstract
    code-level : ∀ {p₀ p₁} → is-set (code p₀ p₁)
    code-level {p₀} {p₁} = Pushout-elim
      {P = λ p₀ → ∀ p₁ → is-set (code p₀ p₁)}
      (λ a₀ p₁ → codeAP-level {a₀} {p₁})
      (λ b₀ p₁ → codeBP-level {b₀} {p₁})
      (λ c₀ → prop-has-all-paths-↓ $ Π-is-prop λ p₁ → is-set-is-prop)
      p₀ p₁
  code-is-set = code-level

  abstract
    transp-cPA-glue : ∀ d₀ {a₁} (pcAA : precodeAA (f (h d₀)) a₁)
      → transport (λ p₀ → code p₀ (left a₁)) (glue (h d₀)) q[ pcAA  ] == q[ pcAA-to-pcBA d₀ pcAA ]
    transp-cPA-glue d₀ {a₁} pcAA =
      transport (λ p₀ → code p₀ (left a₁)) (glue (h d₀)) q[ pcAA  ]
        =⟨ ap (λ e → coe e q[ pcAA ])
            ( ap-∘ (_$ left a₁) code (glue (h d₀))
            ∙ ap (ap (_$ left a₁)) (Code.glue-β (h d₀))
            ∙ app=-β (ua ∘ cAP-equiv-cBP (h d₀)) (left a₁)
            ∙ ap ua (CodeAAEquivCodeBA.eqv-β a₁ d₀)) ⟩
      coe (ua (CodeAAEquivCodeBA.eqv-on-image a₁ d₀)) q[ pcAA  ]
        =⟨ coe-β (CodeAAEquivCodeBA.eqv-on-image a₁ d₀) q[ pcAA ] ⟩
      q[ pcAA-to-pcBA d₀ pcAA ]
        =∎

    transp-cPB-glue : ∀ d₀ {b₁} (pcAB : precodeAB (f (h d₀)) b₁)
      → transport (λ p₀ → code p₀ (right b₁)) (glue (h d₀)) q[ pcAB  ] == q[ pcAB-to-pcBB d₀ pcAB ]
    transp-cPB-glue d₀ {b₁} pcAB =
      transport (λ p₀ → code p₀ (right b₁)) (glue (h d₀)) q[ pcAB  ]
        =⟨ ap (λ e → coe e q[ pcAB ])
            ( ap-∘ (_$ right b₁) code (glue (h d₀))
            ∙ ap (ap (_$ right b₁)) (Code.glue-β (h d₀))
            ∙ app=-β (ua ∘ cAP-equiv-cBP (h d₀)) (right b₁)
            ∙ ap ua (CodeABEquivCodeBB.eqv-β b₁ d₀)) ⟩
      coe (ua (CodeABEquivCodeBB.eqv-on-image b₁ d₀)) q[ pcAB  ]
        =⟨ coe-β (CodeABEquivCodeBB.eqv-on-image b₁ d₀) q[ pcAB ] ⟩
      q[ pcAB-to-pcBB d₀ pcAB ]
        =∎

  -- code to path
  abstract
    pcAA-to-pcBA-to-path : ∀ d₀ {a₁} (pcAA : precodeAA _ a₁) →
         pcBA-to-path (pcAA-to-pcBA d₀ pcAA)
      == !₀ [ glue (h d₀) ] ∙₀' pcAA-to-path pcAA
    pcAB-to-pcBB-to-path : ∀ d₀ {b₁} (pcAB : precodeAB _ b₁) →
         pcBB-to-path (pcAB-to-pcBB d₀ pcAB)
      == !₀ [ glue (h d₀) ] ∙₀' pcAB-to-path pcAB
    pcAA-to-pcBA-to-path d₀ (pc-a pA) = ∙₀'-unit-l (!₀ [ glue (h d₀) ] ∙₀' ap₀ left pA)
    pcAA-to-pcBA-to-path d₀ (pc-aba d pc pA) =
        ap (λ p → p ∙₀' !₀ [ glue (h d) ] ∙₀' ap₀ left pA) (pcAB-to-pcBB-to-path d₀ pc)
      ∙ ∙₀'-assoc (!₀ [ glue (h d₀) ]) (pcAB-to-path pc) (!₀ [ glue (h d) ] ∙₀' ap₀ left pA)
    pcAB-to-pcBB-to-path d₀ (pc-aab d pc pB) =
        ap (λ p → p ∙₀' [ glue (h d) ] ∙₀' ap₀ right pB) (pcAA-to-pcBA-to-path d₀ pc)
      ∙ ∙₀'-assoc (!₀ [ glue (h d₀) ]) (pcAA-to-path pc) ([ glue (h d) ] ∙₀' ap₀ right pB)

  abstract
    decodeAA-is-decodeBA : ∀ {a₁} c₀ →
      decodeAA {f c₀} {a₁} == decodeBA {g c₀} {a₁}
      [ (λ p₀ → code p₀ (left a₁) → p₀ =₀ left a₁) ↓ glue c₀ ]
    decodeAA-is-decodeBA {a₁ = a₁} = SurjExt.ext
      (λ _ → ↓-preserves-level $ Π-is-set λ _ → Trunc-level) h h-is-surj
      (λ d₀ → ↓-→-from-transp $ λ= $ SetQuot-elim
        {P = λ cAA → transport (_=₀ left a₁) (glue (h d₀)) (decodeAA cAA)
                  == decodeBA (transport (λ p₀ → code p₀ (left a₁)) (glue (h d₀)) cAA)}
        (λ _ → =-preserves-set Trunc-level)
        (λ pcAA →
          transport (_=₀ left a₁) (glue (h d₀)) (pcAA-to-path pcAA)
            =⟨ transp₀-idf=₀cst [ glue (h d₀) ] (pcAA-to-path pcAA) ⟩
          !₀ [ glue (h d₀) ] ∙₀ pcAA-to-path pcAA
            =⟨ ∙₀=∙₀' [ ! (glue (h d₀)) ] (pcAA-to-path pcAA) ⟩
          !₀ [ glue (h d₀) ] ∙₀' pcAA-to-path pcAA
            =⟨ ! $ pcAA-to-pcBA-to-path d₀ pcAA ⟩
          pcBA-to-path (pcAA-to-pcBA d₀ pcAA)
            =⟨ ! $ ap (λ e → decodeBA (–> e q[ pcAA ])) (CodeAAEquivCodeBA.eqv-β a₁ d₀) ⟩
          decodeBA (–> (CodeAAEquivCodeBA.eqv a₁ (h d₀)) q[ pcAA ])
            =⟨ ! $ ap decodeBA (coe-β (CodeAAEquivCodeBA.eqv a₁ (h d₀)) q[ pcAA ]) ⟩
          decodeBA (coe (ua (CodeAAEquivCodeBA.eqv a₁ (h d₀))) q[ pcAA ])
            =⟨ ! $ ap (λ p → decodeBA (coe p q[ pcAA ])) (app=-β (ua ∘ cAP-equiv-cBP (h d₀)) (left a₁)) ⟩
          decodeBA (coe (app= (λ= λ p₁ → ua (cAP-equiv-cBP (h d₀) p₁)) (left a₁)) q[ pcAA ])
            =⟨ ! $ ap (λ p → decodeBA (coe (app= p (left a₁)) q[ pcAA ])) (Code.glue-β (h d₀)) ⟩
          decodeBA (coe (app= (ap code (glue (h d₀))) (left a₁)) q[ pcAA ])
            =⟨ ap (λ p → decodeBA (coe p q[ pcAA ])) (∘-ap (λ f₁ → f₁ (left a₁)) code (glue (h d₀))) ⟩
          decodeBA (transport (λ p₀ → code p₀ (left a₁)) (glue (h d₀)) q[ pcAA ])
            =∎)
        (λ _ → prop-has-all-paths-↓ $ Trunc-level {n = 0} _ _))
      (λ _ _ _ → prop-has-all-paths-↓ $ ↓-level $ Π-is-set λ _ → Trunc-level)

  abstract
    decodeAB-is-decodeBB : ∀ {b₁} c₀ →
      decodeAB {f c₀} {b₁} == decodeBB {g c₀} {b₁}
      [ (λ p₀ → code p₀ (right b₁) → p₀ =₀ right b₁) ↓ glue c₀ ]
    decodeAB-is-decodeBB {b₁ = b₁} = SurjExt.ext
      (λ _ → ↓-preserves-level $ Π-is-set λ _ → Trunc-level) h h-is-surj
      (λ d₀ → ↓-→-from-transp $ λ= $ SetQuot-elim
        {P = λ cAB → transport (_=₀ right b₁) (glue (h d₀)) (decodeAB cAB)
                  == decodeBB (transport (λ p₀ → code p₀ (right b₁)) (glue (h d₀)) cAB)}
        (λ _ → =-preserves-set Trunc-level)
        (λ pcAB →
          transport (_=₀ right b₁) (glue (h d₀)) (pcAB-to-path pcAB)
            =⟨ transp₀-idf=₀cst [ glue (h d₀) ] (pcAB-to-path pcAB) ⟩
          !₀ [ glue (h d₀) ] ∙₀ pcAB-to-path pcAB
            =⟨ ∙₀=∙₀' [ ! (glue (h d₀)) ] (pcAB-to-path pcAB) ⟩
          !₀ [ glue (h d₀) ] ∙₀' pcAB-to-path pcAB
            =⟨ ! $ pcAB-to-pcBB-to-path d₀ pcAB ⟩
          pcBB-to-path (pcAB-to-pcBB d₀ pcAB)
            =⟨ ! $ ap (λ e → decodeBB (–> e q[ pcAB ])) (CodeABEquivCodeBB.eqv-β b₁ d₀) ⟩
          decodeBB (–> (CodeABEquivCodeBB.eqv b₁ (h d₀)) q[ pcAB ])
            =⟨ ! $ ap decodeBB (coe-β (CodeABEquivCodeBB.eqv b₁ (h d₀)) q[ pcAB ]) ⟩
          decodeBB (coe (ua (CodeABEquivCodeBB.eqv b₁ (h d₀))) q[ pcAB ])
            =⟨ ! $ ap (λ p → decodeBB (coe p q[ pcAB ])) (app=-β (ua ∘ cAP-equiv-cBP (h d₀)) (right b₁)) ⟩
          decodeBB (coe (app= (λ= λ p₁ → ua (cAP-equiv-cBP (h d₀) p₁)) (right b₁)) q[ pcAB ])
            =⟨ ! $ ap (λ p → decodeBB (coe (app= p (right b₁)) q[ pcAB ])) (Code.glue-β (h d₀)) ⟩
          decodeBB (coe (app= (ap code (glue (h d₀))) (right b₁)) q[ pcAB ])
            =⟨ ap (λ p → decodeBB (coe p q[ pcAB ])) (∘-ap (λ f₁ → f₁ (right b₁)) code (glue (h d₀))) ⟩
          decodeBB (transport (λ p₀ → code p₀ (right b₁)) (glue (h d₀)) q[ pcAB ])
            =∎)
        (λ _ → prop-has-all-paths-↓ $ Trunc-level {n = 0} _ _))
      (λ _ _ _ → prop-has-all-paths-↓ $ ↓-level $ Π-is-set λ _ → Trunc-level)

  abstract
    decodeAP-is-decodeBP : ∀ c₀ p₁
      → decodeAP {f c₀} {p₁} == decodeBP {g c₀} {p₁}
        [ (λ p₀ → code p₀ p₁ → p₀ =₀ p₁) ↓ glue c₀ ]
    decodeAP-is-decodeBP c₀ = Pushout-elim
      {P = λ p₁ → decodeAP {f c₀} {p₁} == decodeBP {g c₀} {p₁}
        [ (λ p₀ → code p₀ p₁ → p₀ =₀ p₁) ↓ glue c₀ ]}
      (λ a₁ → decodeAA-is-decodeBA {a₁ = a₁} c₀)
      (λ b₁ → decodeAB-is-decodeBB {b₁ = b₁} c₀)
      (λ _ → prop-has-all-paths-↓ $ ↓-level $ Π-is-set λ _ → Trunc-level)

  decode : ∀ {p₀ p₁} → code p₀ p₁ → p₀ =₀ p₁
  decode {p₀} {p₁} = Pushout-elim
    {P = λ p₀ → code p₀ p₁ → p₀ =₀ p₁}
    (λ a₀ → decodeAP {a₀} {p₁})
    (λ b₀ → decodeBP {b₀} {p₁})
    (λ c₀ → decodeAP-is-decodeBP c₀ p₁)
    p₀

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import Cubical.Core.Everything
open import Cubical.Relation.Binary.Raw

module Cubical.Relation.Binary.Reasoning.Preorder {c ℓ} {A : Type c} (P : Preorder A ℓ) where

open Preorder P

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

open import Cubical.Relation.Binary.Reasoning.Base.Single _∼_ isPreorder public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use the
-- Relation.Binary.Construct.Closure.Reflexive module directly.
------------------------------------------------------------------------

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

module Data.ReflexiveClosure where

open import Relation.Binary.Construct.Closure.Reflexive public

{-# WARNING_ON_IMPORT
"Data.ReflexiveClosure was deprecated in v0.16.
Use Relation.Binary.Construct.Closure.Reflexive instead."
#-}


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Prod.Properties where

open import Cubical.Core.Everything

open import Cubical.Data.Prod.Base
open import Cubical.Data.Sigma

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

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ
    B : Type ℓ'

-- Swapping is an equivalence

swap : A × B → B × A
swap (x , y) = (y , x)

swap-invol : (xy : A × B) → swap (swap xy) ≡ xy
swap-invol (_ , _) = refl

isEquivSwap : (A : Type ℓ) (B : Type ℓ') → isEquiv (λ (xy : A × B) → swap xy)
isEquivSwap A B = isoToIsEquiv (iso swap swap swap-invol swap-invol)

swapEquiv : (A : Type ℓ) (B : Type ℓ') → A × B ≃ B × A
swapEquiv A B = (swap , isEquivSwap A B)

swapEq : (A : Type ℓ) (B : Type ℓ') → A × B ≡ B × A
swapEq A B = ua (swapEquiv A B)

private
  open import Cubical.Data.Nat

  -- As × is defined as a datatype this computes as expected
  -- (i.e. "C-c C-n test1" reduces to (2 , 1)). If × is implemented
  -- using Sigma this would be "transp (λ i → swapEq ℕ ℕ i) i0 (1 , 2)"
  test : ℕ × ℕ
  test = transp (λ i → swapEq ℕ ℕ i) i0 (1 , 2)

  testrefl : test ≡ (2 , 1)
  testrefl = refl

-- equivalence between the sigma-based definition and the inductive one
A×B≃A×ΣB : A × B ≃ A ×Σ B
A×B≃A×ΣB = isoToEquiv (iso (λ { (a , b) → (a , b)})
                          (λ { (a , b) → (a , b)})
                          (λ _ → refl)
                          (λ { (a , b) → refl }))

A×B≡A×ΣB : A × B ≡ A ×Σ B
A×B≡A×ΣB = ua A×B≃A×ΣB

swapΣEquiv : (A : Type ℓ) (B : Type ℓ') → A ×Σ B ≃ B ×Σ A
swapΣEquiv A B = compEquiv (compEquiv (invEquiv A×B≃A×ΣB) (swapEquiv A B)) A×B≃A×ΣB

-- truncation for products
isOfHLevelProd : (n : ℕ) → isOfHLevel n A → isOfHLevel n B → isOfHLevel n (A × B)
isOfHLevelProd {A = A} {B = B} n h1 h2 =
  let h : isOfHLevel n (A ×Σ B)
      h = isOfHLevelΣ n h1 (λ _ → h2)
  in transport (λ i → isOfHLevel n (A×B≡A×ΣB {A = A} {B = B} (~ i))) h

×-≃ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Type ℓ₁} {B : Type ℓ₂} {C : Type ℓ₃} {D : Type ℓ₄}
    → A ≃ C → B ≃ D → A × B ≃ C × D
×-≃ {A = A} {B = B} {C = C} {D = D} f g = isoToEquiv (iso φ ψ η ε)
   where
    φ : A × B → C × D
    φ (a , b) = equivFun f a , equivFun g b

    ψ : C × D → A × B
    ψ (c , d) = equivFun (invEquiv f) c , equivFun (invEquiv g) d

    η : section φ ψ
    η (c , d) i = retEq f c i , retEq g d i

    ε : retract φ ψ
    ε (a , b) i = secEq f a i , secEq g b i

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


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

open import Agda.Primitive.Cubical
open import Agda.Builtin.Cubical.Path

data S1 : Set where
  base : S1
  loop : base ≡ base

postulate
  weird : S1 → I

bad : (x : S1) → I
bad base     = {!!}
bad (loop x) = {!!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Structure.Categorical.Multi where

open import Data
open import Data.Boolean
open import Data.Tuple using (_⨯_ ; _,_)
open import Data.Tuple.Raiseᵣ
import      Data.Tuple.Raiseᵣ.Functions as Raise
open import Data.Tuple.RaiseTypeᵣ
import      Data.Tuple.RaiseTypeᵣ.Functions as RaiseType
open import Function.Multi
open import Function.Multi.Functions
open import Functional using (_→ᶠ_)
import      Functional.Dependent as Fn
open import Lang.Instance
import      Lvl
open import Logic
open import Logic.Predicate
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Oper.Comparisons
open import Structure.Setoid
import      Structure.Categorical.Names as Names
import      Structure.Operator.Names as Names
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Syntax.Function
open import Type
open import Type.Properties.Singleton

private variable ℓ ℓₒ ℓₘ ℓₘ₁ ℓₘ₂ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable Obj Obj₁ Obj₂ : Type{ℓₒ}

module Morphism where
  module _
    (_⟶_ : Obj → Obj → Stmt{ℓₘ})
    ⦃ morphism-equiv : ∀{x y} → Equiv{ℓₑ}(x ⟶ y) ⦄
    where

    {-
    -- Examples:
    --   MorphismChain(3) T x y z
    --   = compose(1) ((x ⟶ y) ,_) (MorphismChain(2) T y) z
    --   = (x ⟶ y) , (MorphismChain(2) T y z)
    --   = (x ⟶ y) , (y ⟶ z) , T(z)
    --
    --   MorphismChain(4) T x y z w
    --   = compose(2) ((x ⟶ y) ,_) (MorphismChain(3) T y) z w
    --   = (x ⟶ y) , (MorphismChain(3) T y z w)
    --   = (x ⟶ y) , (y ⟶ z) , (z ⟶ w) , T(w)
    MorphismChain : (n : ℕ) → (Obj → Type{ℓₘ}) → (RaiseType.repeat (𝐒(n)) Obj) ⇉ Types(Raise.repeat (𝐒(n)) ℓₘ)
    MorphismChain 0         T x   = T(x)
    MorphismChain 1         T x y = (x ⟶ y) , T(y)
    MorphismChain (𝐒(𝐒(n))) T x y = compose(𝐒(n)) ((x ⟶ y) ,_) (MorphismChain(𝐒(n)) T y)

    -- Examples:
    --   MorphismMapping(2) x y
    --   = MorphismChain(2)(x ⟶_) x y
    --   = (x ⟶ y) → (x ⟶ y)
    --
    --   MorphismMapping(3) x y z
    --   = MorphismChain(3)(x ⟶_) x y z
    --   = (x ⟶ y) → (y ⟶ z) → (x ⟶ z)
    --
    --   MorphismMapping(4) x y z w
    --   = MorphismChain(4)(x ⟶_) x y z w
    --   = (x ⟶ y) → (y ⟶ z) → (z ⟶ w) → (x ⟶ w)
    MorphismMapping : (n : ℕ) → (RaiseType.repeat n Obj) ⇉ Type{ℓₘ}
    MorphismMapping(0)   = Unit
    MorphismMapping(1)      = {!!}
    MorphismMapping(𝐒(𝐒 n)) = {!!}
    --MorphismMapping(𝐒 n) = curry(n) {!Fs ↦ (uncurry(n) (MorphismChain(n)) Fs ⇉ (? → ?))!}
    {-
    MorphismMapping(1)       x   = ? -- MorphismChain(1)(x ⟶_) x
    MorphismMapping(𝐒(𝐒(n))) x   = compose(𝐒(n)) (RaiseType.reduceᵣ{𝐒(n)}{\ℓ₁ ℓ₂ → ℓ₁ Lvl.⊔ ℓ₂} _→ᶠ_) (MorphismChain(𝐒(𝐒(n))) (x ⟶_) x)
    -- MorphismChain(𝐒(𝐒(n)))(x ⟶_) x-}
    -}

    MorphismFlippedChain : (n : ℕ) → (RaiseType.repeat (𝐒(n)) Obj) ⇉ Type{ℓₘ}
    MorphismFlippedChain 𝟎      x = x ⟶ x
    MorphismFlippedChain (𝐒(n)) x = Out(𝐒(n)) (x ⟶_) x where
      Out : (n : ℕ) → (Obj → Type{ℓₘ}) → (RaiseType.repeat (𝐒(n)) Obj) ⇉ Type{ℓₘ}
      Out 0         T x   = T(x)
      Out 1         T x y = (x ⟶ y) → T(y)
      Out (𝐒(𝐒(n))) T x y = Out(𝐒(n)) (z ↦ ((x ⟶ y) → T(z))) y

  module _
    (_⟶₁_ : Obj₁ → Obj₁ → Stmt{ℓₘ₁})
    ⦃ morphism-equiv₁ : ∀{x y} → Equiv{ℓₑ₁}(x ⟶₁ y) ⦄
    (_⟶₂_ : Obj₂ → Obj₂ → Stmt{ℓₘ₂})
    ⦃ morphism-equiv₂ : ∀{x y} → Equiv{ℓₑ₂}(x ⟶₂ y) ⦄
    where

    private open module Equiv₂{x}{y} = Equiv(morphism-equiv₂{x}{y}) using () renaming (_≡_ to _≡₂_)

    module _
      {F : Obj₁ → Obj₂}
      where

      -- Definition of the relation between a function and an operation that says:
      -- The function preserves the operation.
      -- Often used when defining homomorphisms.
      -- Examples:
      --   Preserving(0) (map)(G₁)(G₂)
      --   = ∀{x} → (map ∘₀ G₁ ≡ G₂ on₀ map)
      --   = ∀{x} → (map(G₁) ≡ G₂(f))
      --   Preserving(1) (map)(G₁)(G₂)
      --   = ∀{x y}{f : x ⟶ y} → ((map ∘₁ G₁)(f) ≡ (G₂ on₁ map)(f))
      --   = ∀{x y}{f : x ⟶ y} → (map(G₁(f)) ≡ G₂(map(f)))
      --   Preserving(2) (map)(G₁)(G₂)
      --   = ∀{x y z}{f₁ : y ⟶ z}{f₂ : x ⟶ y} → ((map ∘₂ G₁)(f₁)(f₂) ≡ (G₂ on₂ map)(f₁)(f₂))
      --   = ∀{x y z}{f₁ : y ⟶ z}{f₂ : x ⟶ y} → (map(G₁ f₁ f₂) ≡ G₂ (map(f₁)) (map(f₂)))
      --   Preserving(3) (map)(G₁)(G₂)
      --   = ∀{f₁ f₂ f₃} → ((map ∘₃ G₁)(f₁)(f₂)(f₃) ≡ (G₂ on₃ map)(f₁)(f₂)(f₃))
      --   = ∀{f₁ f₂ f₃} → (map(G₁ f₁ f₂ f₃) ≡ G₂ (map(f₁)) (map(f₂)) (map(f₃)))
      Preserving : (n : ℕ) → (map : ∀{x y} → (x ⟶₁ y) → (F(x) ⟶₂ F(y))) → (quantifier₊(𝐒(n))(∀ₗ) (MorphismFlippedChain(_⟶₁_)(n))) → (quantifier₊(𝐒(n))(∀ₗ) (MorphismFlippedChain(_⟶₂_)(n))) → (RaiseType.repeat (𝐒(n)) Obj₁) ⇉ Stmt{if(n ≤? 0) then (ℓₑ₂) else (ℓₘ₁ Lvl.⊔ ℓₑ₂)}
      Preserving 0            map G₁ G₂ x     = (map{x}(G₁) ≡ G₂)
      Preserving 1            map G₁ G₂ x y   = ∀{f : x ⟶₁ y} → map (G₁(f)) ≡ G₂(map f)
      Preserving (𝐒(𝐒(n)))    map G₁ G₂ x y   = {!Preserving(𝐒(n)) map ? ? y!}
      -- ∀{f} → (G₁(f)) (G₂(map f))
      --Preserving 2            map G₁ G₂ x y z = ∀{f₁ : y ⟶₁ z}{f₂ : x ⟶₁ y} → (map(G₁(f₁)(f₂)) ≡ G₂(map f₁)(map f₂))
      -- Preserving (𝐒(𝐒(𝐒(n)))) map G₁ G₂ x y z = {!∀{f} → Preserving(𝐒(𝐒(n))) map !}
      --test (P ↦ (∀{f} → P f)) (f ↦ Preserving (𝐒(𝐒(n))) map {!G₁!} {!G₂!} y z) where
      --  test : ((P : {!!}) → TYPE ({!!} Lvl.⊔ {!!})) → ((f : {!!} ⟶₁ {!!}) → RaiseType.repeat (𝐒 n) Obj₁ ⇉ Type) → (RaiseType.repeat (𝐒 n) Obj₁ ⇉ Type)
        -- compose(𝐒(n)) (P ↦ (∀{f} → P f)) ({!f ↦ Preserving (𝐒(𝐒(n))) map {!G₁!} {!G₂!} {!!} {!!}!})
      -- compose(𝐒(n)) {!!} {!!}
      -- ∀{f : x ⟶₁ y} →
      -- Preserving(𝐒(𝐒(n))) map (\{a b} → {!G₁{a}{x}{b}!}) \{a b} → {!G₂{a}{F x}{b}!}

{-
-- Preserving 3 map G₁ G₂ a x y z
-- = ∀{f : a ⟶₁ x} → Preserving 2 map (G₁(f)) (G₂(map f)) x y z
-- = ∀{f : a ⟶₁ x}{f₁ : x ⟶₁ y}{f₂ : y ⟶₁ z} → (map(G₁(f)(f₁)(f₂)) ≡ G₂(map f)(map f₁)(map f₂))

      -- ∀{x y}{f : x ⟶₁ y} → Preserving(𝐒(𝐒(n))) (map) (G₁(f)) (G₂(map(f)))
{-      Preserving(𝟎)       (f)(g₁)(g₂) = (f(g₁) ≡ g₂)
      Preserving(𝐒(𝟎))    (f)(g₁)(g₂) = (∀{x} → f(g₁(x)) ≡ g₂(f(x)))
      Preserving(𝐒(𝐒(n))) (f)(g₁)(g₂) = (∀{x} → Preserving(𝐒(n)) (f) (g₁(x)) (g₂(f(x))))
  -- ∀{x y z : Objₗ}{f : y ⟶ z}{g : x ⟶ y} → (map(f ∘ g) ≡ map(f) ∘ map(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:
{- 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
-}

import      LibraBFT.Impl.Consensus.LedgerRecoveryData as LedgerRecoveryData
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Prelude
------------------------------------------------------------------------------
open import Data.String                                using (String)

module LibraBFT.Impl.Consensus.RecoveryData where

findBlocksToPrune
  : HashValue → List Block → List QuorumCert
  → (List HashValue × List Block × List QuorumCert)

new
  : Maybe Vote
  → LedgerRecoveryData
  → List Block
  → RootMetadata
  → List QuorumCert
  → Maybe TimeoutCertificate
  → Either ErrLog RecoveryData
new lastVote storageLedger blocks0 rootMetadata quorumCerts0 highestTimeoutCertificate = do
  (root@(RootInfo∙new rb _ _) , blocks1 , quorumCerts1)
            ← withErrCtx' (here' []) (LedgerRecoveryData.findRoot blocks0 quorumCerts0 storageLedger)
  let (blocksToPrune , blocks , quorumCerts)
            = findBlocksToPrune (rb ^∙ bId) blocks1 quorumCerts1
      epoch = rb ^∙ bEpoch
  pure $ mkRecoveryData
      (case lastVote of λ where
        (just v) → if-dec v ^∙ vEpoch ≟ epoch then just v else nothing
        nothing  → nothing)
      root
      rootMetadata
      blocks
      quorumCerts
      (just blocksToPrune)
      (case highestTimeoutCertificate of λ where
        (just tc) → if-dec tc ^∙ tcEpoch ≟ epoch then just tc else nothing
        nothing   → nothing)
 where
  here' : List String → List String
  here' t = "RecoveryData" ∷ "new" ∷ t

-- TODO (the "TODO" is in the Haskell code)
findBlocksToPrune _rootId blocks quorumCerts = ([] , blocks , quorumCerts)


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

module Circle where

open import Agda.Prim
open import Data.Product
open import Function renaming (_∘_ to _○_)

infixr 8  _∘_   -- path composition
infix  4  _≡_   -- propositional equality
infix  4  _∼_   -- homotopy between two functions
infix  4  _≃_   -- type of equivalences
infix  2  _∎      -- equational reasoning
infixr 2  _≡⟨_⟩_  -- equational reasoning

------------------------------------------------------------------------------
-- Identity types

-- Our own version of refl that makes 'a' explicit

data _≡_ {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where
  refl : (a : A) → (a ≡ a)

pathInd : ∀ {u ℓ} → {A : Set u} →
          (C : {x y : A} → x ≡ y → Set ℓ) →
          (c : (x : A) → C (refl x)) →
          ({x y : A} (p : x ≡ y) → C p)
pathInd C c (refl x) = c x

------------------------------------------------------------------------------
-- Ch. 2

-- Lemma 2.1.1

! : ∀ {u} → {A : Set u} {x y : A} → (x ≡ y) → (y ≡ x)
! = pathInd (λ {x} {y} _ → y ≡ x) refl

-- Lemma 2.1.2

_∘_ : ∀ {u} → {A : Set u} → {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_∘_ {u} {A} {x} {y} {z} p q =
  pathInd
    (λ {x} {y} p → ((z : A) → (q : y ≡ z) → (x ≡ z)))
    (λ x z q → pathInd (λ {x} {z} _ → x ≡ z) refl {x} {z} q)
    {x} {y} p z q

-- Lemma 2.1.4

-- p = p . refl

unitTransR : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ p ∘ refl y)
unitTransR {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ p ∘ (refl y))
    (λ x → refl (refl x))
    {x} {y} p

-- p = refl . p

unitTransL : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ refl x ∘ p)
unitTransL {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ≡ (refl x) ∘ p)
    (λ x → refl (refl x))
    {x} {y} p

-- ! p . p = refl

invTransL : {A : Set} {x y : A} → (p : x ≡ y) → (! p ∘ p ≡ refl y)
invTransL {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ! p ∘ p ≡ refl y)
    (λ x → refl (refl x))
    {x} {y} p

-- p . ! p = refl

invTransR : ∀ {ℓ} {A : Set ℓ} {x y : A} → (p : x ≡ y) → (p ∘ ! p ≡ refl x)
invTransR {ℓ} {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → p ∘ ! p ≡ refl x)
    (λ x → refl (refl x))
    {x} {y} p

-- ! (! p) = p

invId : {A : Set} {x y : A} → (p : x ≡ y) → (! (! p) ≡ p)
invId {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ! (! p) ≡ p)
    (λ x → refl (refl x))
    {x} {y} p

-- p . (q . r) = (p . q) . r

assocP : {A : Set} {x y z w : A} → (p : x ≡ y) → (q : y ≡ z) → (r : z ≡ w) →
         (p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r)
assocP {A} {x} {y} {z} {w} p q r =
  pathInd
    (λ {x} {y} p → (z : A) → (w : A) → (q : y ≡ z) → (r : z ≡ w) →
      p ∘ (q ∘ r) ≡ (p ∘ q) ∘ r)
    (λ x z w q r →
      pathInd
        (λ {x} {z} q → (w : A) → (r : z ≡ w) →
          (refl x) ∘ (q ∘ r) ≡ ((refl x) ∘ q) ∘ r)
        (λ x w r →
          pathInd
            (λ {x} {w} r →
              (refl x) ∘ ((refl x) ∘ r) ≡
              ((refl x) ∘ (refl x)) ∘ r)
            (λ x → (refl (refl x)))
            {x} {w} r)
        {x} {z} q w r)
    {x} {y} p z w q r

-- ! (p ∘ q) ≡ ! q ∘ ! p

invComp : {A : Set} {x y z : A} → (p : x ≡ y) → (q : y ≡ z) →
          ! (p ∘ q) ≡ ! q ∘ ! p
invComp {A} {x} {y} {z} p q =
  pathInd
    (λ {x} {y} p → (z : A) → (q : y ≡ z) → ! (p ∘ q) ≡ ! q ∘ ! p)
    (λ x z q →
      pathInd
        (λ {x} {z} q → ! (refl x ∘ q) ≡ ! q ∘ ! (refl x))
        (λ x → refl (refl x))
        {x} {z} q)
    {x} {y} p z q

-- Introduce equational reasoning syntax to simplify proofs

_≡⟨_⟩_ : ∀ {u} → {A : Set u} (x : A) {y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_ ≡⟨ p ⟩ q = p ∘ q

bydef : ∀ {u} → {A : Set u} {x : A} → (x ≡ x)
bydef {u} {A} {x} = refl x

_∎ : ∀ {u} → {A : Set u} (x : A) → x ≡ x
_∎ x = refl x

------------------------------------------------------------------------------
-- Functions are functors

-- Lemma 2.2.1
-- computation rule: ap f (refl x) = refl (f x)

ap : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {x y : A} →
     (f : A → B) → (x ≡ y) → (f x ≡ f y)
ap {ℓ} {ℓ'} {A} {B} {x} {y} f p =
  pathInd
    (λ {x} {y} p → f x ≡ f y)
    (λ x → refl (f x))
    {x} {y} p

-- Lemma 2.2.2

-- f (p ∘ q) ≡ f p ∘ f q

apfTrans : ∀ {u} → {A B : Set u} {x y z : A} →
  (f : A → B) → (p : x ≡ y) → (q : y ≡ z) → ap f (p ∘ q) ≡ (ap f p) ∘ (ap f q)
apfTrans {u} {A} {B} {x} {y} {z} f p q =
  pathInd {u}
    (λ {x} {y} p → (z : A) → (q : y ≡ z) →
      ap f (p ∘ q) ≡ (ap f p) ∘ (ap f q))
    (λ x z q →
      pathInd {u}
        (λ {x} {z} q →
          ap f (refl x ∘ q) ≡ (ap f (refl x)) ∘ (ap f q))
        (λ x → refl (refl (f x)))
        {x} {z} q)
    {x} {y} p z q

-- f (! p) ≡ ! (f p)

apfInv : ∀ {u} → {A B : Set u} {x y : A} → (f : A → B) → (p : x ≡ y) →
         ap f (! p) ≡ ! (ap f p)
apfInv {u} {A} {B} {x} {y} f p =
  pathInd {u}
    (λ {x} {y} p → ap f (! p) ≡ ! (ap f p))
    (λ x → refl (ap f (refl x)))
    {x} {y} p

-- g (f p) ≡ (g ○ f) p

apfComp : {A B C : Set} {x y : A} → (f : A → B) → (g : B → C) → (p : x ≡ y) →
          ap g (ap f p) ≡ ap (g ○ f) p
apfComp {A} {B} {C} {x} {y} f g p =
  pathInd
    (λ {x} {y} p → ap g (ap f p) ≡ ap (g ○ f) p)
    (λ x → refl (ap g (ap f (refl x))))
    {x} {y} p

-- id p ≡ p

apfId : {A : Set} {x y : A} → (p : x ≡ y) → ap id p ≡ p
apfId {A} {x} {y} p =
  pathInd
    (λ {x} {y} p → ap id p ≡ p)
    (λ x → refl (refl x))
    {x} {y} p

-- Transport

-- Lemma 2.3.1

transport : ∀ {ℓ ℓ'} → {A : Set ℓ} {x y : A} →
  (P : A → Set ℓ') → (p : x ≡ y) → P x → P y
transport {ℓ} {ℓ'} {A} {x} {y} P p =
  pathInd
    (λ {x} {y} p → (P x → P y))
    (λ _ → id)
    {x} {y} p

-------------------------------------------------------------------------------
-- Homotopies and equivalences

_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} →
      (f g : (x : A) → P x) → Set (_⊔_ ℓ ℓ')
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x

-- Quasi-inverses

record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (_⊔_ ℓ ℓ') where
  constructor mkqinv
  field
    g : B → A
    α : (f ○ g) ∼ id
    β : (g ○ f) ∼ id

-- Example 2.4.7

idqinv : ∀ {ℓ} → {A : Set ℓ} → qinv {ℓ} {ℓ} {A} {A} id
idqinv = record {
           g = id ;
           α = λ b → refl b ;
           β = λ a → refl a
         }

-- Equivalences

record isequiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) :
  Set (_⊔_ ℓ ℓ') where
  constructor mkisequiv
  field
    g : B → A
    α : (f ○ g) ∼ id
    h : B → A
    β : (h ○ f) ∼ id

equiv₁ : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → qinv f → isequiv f
equiv₁ (mkqinv qg qα qβ) = mkisequiv qg qα qg qβ

_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (_⊔_ ℓ ℓ')
A ≃ B = Σ (A → B) isequiv

-- Lemma 2.4.12

idequiv : ∀ {ℓ} {A : Set ℓ} → A ≃ A
idequiv = (id , equiv₁ idqinv)

------------------------------------------------------------------------------
-- Sec. 2.10: Universes; univalence

idtoeqv : {A B : Set} → (A ≡ B) → (A ≃ B)
idtoeqv {A} {B} p =
  pathInd
    (λ {A} {B} p → A ≃ B)
    (λ A → idequiv)
    {A} {B} p

postulate
  univalence : {A B : Set} → (A ≡ B) ≃ (A ≃ B)

------------------------------------------------------------------------------
-- Sec. 2.11: Identity types

-- Thm 2.11.3

transportId : {A B : Set} {y z : A} → (f g : A → B) →
  (p : y ≡ z) → (q : f y ≡ g y) →
  transport (λ x → f x ≡ g x) p q ≡ ! (ap f p) ∘ q ∘ (ap g p)
transportId {A} {B} {y} {z} f g p q =
  pathInd
    (λ {y} {z} p → (q : f y ≡ g y) →
      transport (λ x → f x ≡ g x) p q ≡ ! (ap f p) ∘ q ∘ (ap g p))
    (λ y q → q
               ≡⟨ unitTransR q ⟩
             q ∘ refl (g y)
               ≡⟨ unitTransL (q ∘ refl (g y)) ⟩
             refl (f y) ∘ q ∘ refl (g y) ∎)
    {y} {z} p q

------------------------------------------------------------------------------
-- Exercise: let's show that the following two definitions of the
-- circle are "the same"

{--

data S¹ where
  base : S¹
  loop : base ≡ base

data S¹' where
  south : S¹'
  north : S¹'
  east  : south ≡ north
  west  : south ≡ north

--}

module Circle1 where
  private
    data S¹* : Set where
      base* : S¹*

  S¹ : Set
  S¹ = S¹*

  base : S¹
  base = base*

  postulate
    loop : base ≡ base

  recS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase) → S¹ → C
  recS¹ cbase cloop base* = cbase

  postulate
    βrecS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase) →
      ap (recS¹ cbase cloop) loop ≡ cloop

  indS¹ : {C : S¹ → Set} →
    (cbase : C base) → (cloop : transport C loop cbase ≡ cbase) →
    (circle : S¹) → C circle
  indS¹ cbase cloop base* = cbase

open Circle1 public

--

module Circle2 where
  private
    data S¹'* : Set where
      south* : S¹'*
      north* : S¹'*

  S¹' : Set
  S¹' = S¹'*

  south : S¹'
  south = south*

  north : S¹'
  north = north*

  postulate
    east : south ≡ north
    west : south ≡ north

  recS¹' : {C : Set} →
    (csouth cnorth : C) → (ceast cwest : csouth ≡ cnorth) → S¹' → C
  recS¹' csouth cnorth ceast cwest south* = csouth
  recS¹' csouth cnorth ceast cwest north* = cnorth

  postulate
    βreceastS¹' : {C : Set} →
      (csouth cnorth : C) → (ceast cwest : csouth ≡ cnorth) →
      ap (recS¹' csouth cnorth ceast cwest) east ≡ ceast
    βrecwestS¹' : {C : Set} →
      (csouth cnorth : C) → (ceast cwest : csouth ≡ cnorth) →
      ap (recS¹' csouth cnorth ceast cwest) west ≡ cwest

  indS¹' : {C : S¹' → Set} →
    (csouth : C south) → (cnorth : C north) →
    (ceast : transport C east csouth ≡ cnorth) →
    (cwest : transport C west csouth ≡ cnorth) →
    (circle : S¹') → C circle
  indS¹' csouth cnorth ceast cwest south* = csouth
  indS¹' csouth cnorth ceast cwest north* = cnorth

open Circle2 public

-- Maps between Circle1 and Circle2 and back

-- fcircle (base) = south
-- fcircle (loop) = east ∘ ! west

fcircle : S¹ → S¹'
fcircle = recS¹ south (east ∘ ! west)

floop : ap fcircle loop ≡ (east ∘ ! west)
floop = βrecS¹ south (east ∘ ! west)

-- gcircle (south) = base
-- gcircle (north) = base
-- gcircle (east)  = loop
-- gcircle (west)  = refl base

gcircle : S¹' → S¹
gcircle = recS¹' base base loop (refl base)

geast : ap gcircle east ≡ loop
geast = βreceastS¹' base base loop (refl base)

gwest : ap gcircle west ≡ (refl base)
gwest = βrecwestS¹' base base loop (refl base)

-- compose both ways

-- gf (base) = base
-- gf (loop) = loop

gf : S¹ → S¹
gf = gcircle ○ fcircle

gfloop : ap gf loop ≡ loop
gfloop = ap gf loop
           ≡⟨ ! (apfComp fcircle gcircle loop) ⟩
         ap gcircle (ap fcircle loop)
           ≡⟨ ap (ap gcircle) floop ⟩
         ap gcircle (east ∘ ! west)
           ≡⟨ apfTrans gcircle east (! west) ⟩
         ap gcircle east ∘ ap gcircle (! west)
           ≡⟨ ap (λ x → ap gcircle east ∘ x) (apfInv gcircle west) ⟩
         ap gcircle east ∘ ! (ap gcircle west)
           ≡⟨ ap (λ x → ap gcircle east ∘ ! x) gwest ⟩
         ap gcircle east ∘ (refl base)
           ≡⟨ ! (unitTransR (ap gcircle east)) ⟩
         ap gcircle east
           ≡⟨ geast ⟩
         loop ∎

αloop : transport (λ x → gf x ≡ x) loop (refl base) ≡ refl base
αloop = transport (λ x → gf x ≡ x) loop (refl base)
          ≡⟨ transportId gf id loop (refl base) ⟩ -- Thm 2.11.3
        ! (ap gf loop) ∘ refl base ∘ ap id loop
          ≡⟨ ap (λ x → ! (ap gf loop) ∘ refl base ∘ x) (apfId loop) ⟩
        ! (ap gf loop) ∘ refl base ∘ loop
          ≡⟨ ap (λ x → ! (ap gf loop) ∘ x) (! (unitTransL loop)) ⟩
        ! (ap gf loop) ∘ loop
          ≡⟨ ap (λ x → ! x ∘ loop) gfloop ⟩
        ! loop ∘ loop
          ≡⟨ invTransL loop ⟩
        refl base ∎

βcircle : gf ∼ id
βcircle =
  indS¹ {λ x → gf x ≡ x}
    (refl base)
    αloop

-- fg (south) = south
-- fg (north) = south
-- fg (east)  = east ∘ ! west
-- fg (west)  = refl south

fg : S¹' → S¹'
fg = fcircle ○ gcircle

fgeast : ap fg east ≡ east ∘ ! west
fgeast = ap fg east
           ≡⟨ ! (apfComp gcircle fcircle east) ⟩
         ap fcircle (ap gcircle east)
           ≡⟨ ap (ap fcircle) geast ⟩
         ap fcircle loop
           ≡⟨ floop ⟩
         (east ∘ ! west) ∎

fgwest : ap fg west ≡ refl south
fgwest = ap fg west
           ≡⟨ ! (apfComp gcircle fcircle west) ⟩
         ap fcircle (ap gcircle west)
           ≡⟨ ap (ap fcircle) gwest ⟩
         ap fcircle (refl base)
           ≡⟨ bydef ⟩
         refl south ∎

αeast : transport (λ x → fg x ≡ x) east (refl south) ≡ west
αeast = transport (λ x → fg x ≡ x) east (refl south)
          ≡⟨ transportId fg id east (refl south) ⟩ -- Thm 2.11.3
        ! (ap fg east) ∘ refl south ∘ ap id east
          ≡⟨ ap (λ x → ! (ap fg east) ∘ refl south ∘ x) (apfId east) ⟩
        ! (ap fg east) ∘ refl south ∘ east
           ≡⟨ ap (λ x → ! (ap fg east) ∘ x) (! (unitTransL east)) ⟩
        ! (ap fg east) ∘ east
           ≡⟨ ap (λ x → ! x ∘ east) fgeast ⟩
        ! (east ∘ ! west) ∘ east
          ≡⟨ ap (λ x → x ∘ east) (invComp east (! west)) ⟩
        (! (! west) ∘ ! east) ∘ east
          ≡⟨ ! (assocP (! (! west)) (! east) east) ⟩
        ! (! west) ∘ ! east ∘ east
          ≡⟨ ap (λ x → ! (! west) ∘ x) (invTransL east) ⟩
        ! (! west) ∘ refl north
          ≡⟨ ! (unitTransR (! (! west)))  ⟩
        ! (! west)
          ≡⟨ invId west ⟩
        west ∎

αwest : transport (λ x → fg x ≡ x) west (refl south) ≡ west
αwest = transport (λ x → fg x ≡ x) west (refl south)
          ≡⟨ transportId fg id west (refl south) ⟩ -- Thm 2.11.3
        ! (ap fg west) ∘ refl south ∘ ap id west
          ≡⟨ ap (λ x → ! (ap fg west) ∘ refl south ∘ x) (apfId west) ⟩
        ! (ap fg west) ∘ refl south ∘ west
           ≡⟨ ap (λ x → ! (ap fg west) ∘ x) (! (unitTransL west)) ⟩
        ! (ap fg west) ∘ west
           ≡⟨ ap (λ x → ! x ∘ west) fgwest ⟩
        ! (refl south) ∘ west
          ≡⟨ ! (unitTransL west) ⟩
        west ∎

αcircle : fg ∼ id
αcircle =
  indS¹' {λ x → fg x ≡ x}
    (refl south) west
    αeast
    αwest

--

sequiv : S¹ ≃ S¹'
sequiv = (fcircle , equiv₁ (mkqinv gcircle αcircle βcircle))

spath : S¹ ≡ S¹'
spath with univalence
... | (_ , eq) = isequiv.g eq sequiv

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
-- Andreas, 2015-03-17
-- Andreas, 2020-10-26 conform to Issue1428a

open import Agda.Builtin.Size

data ⊥ : Set where

data SizeLt (i : Size) : Set where
  wrap : Size< i → SizeLt i

-- This definition of size predecessor should be forbidden...
module _ (i : Size) where
  postulate
    pred : Size< i

-- ...otherwise the injectivity test loops here.
iter : ∀ i → SizeLt i → ⊥
iter i (wrap j) = iter j (wrap (pred j))

loop : Size → ⊥
loop i = iter i (wrap (pred i))

absurd : ⊥
absurd = FIXME loop ∞

-- Testcase temporarily mutilated, original error:
--
-- -Issue1428c.agda:...
-- -We don't like postulated sizes in parametrized modules.
--
-- +Issue1428c.agda:...
-- +Not in scope:
-- +  FIXME at Issue1428c.agda:...
-- +when scope checking FIXME

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------------
-- Note on the equality type class using Kettelhoit's approach
------------------------------------------------------------------------------

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

-- Adapted from Kettelhoit's thesis.

module FOT.FOTC.TypeClasses.EqualityKettelhoit where

open import FOTC.Base
open import FOTC.Data.Bool
open import FOTC.Data.Bool.Type
open import FOTC.Data.Nat.Type

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

record Eq (P : D → Set) : Set₁ where
  field equal : ∀ {t₁ t₂} → P t₁ → P t₂ → Set

open Eq {{...}} public

boolEq : ∀ {b₁ b₂} → Bool b₁ → Bool b₂ → Set
boolEq btrue  btrue  = Bool true
boolEq bfalse bfalse = Bool true
{-# CATCHALL #-}
boolEq _      _      = Bool false

nEq : ∀ {m n} → N m → N n → Set
nEq nzero      nzero      = Bool true
nEq (nsucc Nm) (nsucc Nn) = Bool true
{-# CATCHALL #-}
nEq _          _          = Bool false

instance
  eqInstanceBool : Eq Bool
  eqInstanceBool = record { equal = boolEq }

  eqInstanceN : Eq N
  eqInstanceN = record { equal = nEq }

test₁ : Set
test₁ = equal nzero (nsucc nzero)

test₂ : Set
test₂ = equal bfalse bfalse

eqN-sym : ∀ {m n} → (Nm : N m) → (Nn : N n) → equal Nm Nn → equal Nn Nm
eqN-sym nzero      nzero      h = h
eqN-sym nzero      (nsucc Nn) h = h
eqN-sym (nsucc Nm) nzero      h = h
eqN-sym (nsucc Nm) (nsucc Nn) h = h

postulate eqN-sym' : ∀ {m n} → (Nm : N m) → (Nn : N n) → equal Nm Nn → equal Nn Nm
-- {-# ATP prove eqN-sym' #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- 2014-03-05 Andreas, issue reported by James

-- {-# OPTIONS -v tc.with.strip:60 -v:impossible:10 #-}

data Nat : Set where
  zero : Nat

pattern pzero = zero

f : Nat → Nat
f pzero with pzero
f pzero | pzero = pzero

-- ERROR WAS:
-- With clause pattern pzero is not an instance of its parent pattern
-- when checking that the clause
-- f pzero with pzero
-- f pzero | pzero = pzero
-- has type Nat → Nat

max_forks_repo_name: Agda-zh/agda


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

module Dodo.Binary.Functional where

-- Stdlib imports
open import Level using (Level; _⊔_)
open import Relation.Binary using (Rel; REL)
-- Local imports
open import Dodo.Binary.Equality

-- # Definitions #

Functional : ∀ {a b ℓ₁ ℓ₂ : Level} {A : Set a} {B : Set b}
  → Rel B ℓ₁
  → REL A B ℓ₂
    ---------------------
  → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
Functional _≈_ r = ∀ x y₁ y₂ → r x y₁ → r x y₂ → y₁ ≈ y₂
-- The /explicit/ x, y₁, and y₂ are crucial. If they're implicit, Agda will attempt to
-- instantiate them when absent, which often fails to resolve. Not sure why.

-- # Operations #

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {≈ : Rel A ℓ₁} {P : Rel A ℓ₂} {Q : Rel A ℓ₃} where

  functional-⊆₂ : P ⊆₂ Q → Functional ≈ Q → Functional ≈ P
  functional-⊆₂ P⊆Q funcQ x y₁ y₂ Pxy₁ Pxy₂ = funcQ x y₁ y₂ (⊆₂-apply P⊆Q Pxy₁) (⊆₂-apply P⊆Q Pxy₂)

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


text:
module Data.Environment {a} {A : Set a} where

open import Algebra
open import Data.Nat
open import Data.Empty                                    using (⊥-elim)
open import Data.Pos                                      using (ℕ⁺; suc; replicate⁺)
open import Data.List as L                                using (List; []; _∷_; [_]; _++_; map; concatMap; replicate)
open import Data.List.Any                                 using (here; there)
open import Data.List.Any.BagAndSetEquality as B          using ()
open import Data.List.Any.Membership.Propositional public using (_∈_; _∼[_]_; bag)
open import Data.Product                                  using (Σ-syntax; ∃₂; _×_; proj₁; proj₂; _,_)
open import Data.Sum                                      using (_⊎_; inj₁; inj₂)
open import Function                                      using (_$_; flip)
open import Function.Equality                             using (_⟨$⟩_)
open import Function.Inverse                              using (id; sym; _∘_)
open        Function.Inverse.Inverse                      using (to; from)
open import Relation.Binary.PropositionalEquality as P    using (_≡_)

private module ++ = Monoid (L.monoid A)

bubble : (xs {ys} : List A) {x y z : A} →
         z ∈ xs ++ y ∷ x ∷ ys → z ∈ xs ++ x ∷ y ∷ ys
bubble []       (here px)         = there (here px)
bubble []       (there (here px)) = here px
bubble []       (there (there i)) = there (there i)
bubble (x ∷ xs) (here px)         = here px
bubble (x ∷ xs) (there i)         = there (bubble xs i)

-- There is a bijection between indices into the environment
-- ΓBAΔ and the environment ΓABΔ. This is called a 'bubble',
-- because it swaps two adjacent elements, as in bubble
-- sort.
bbl : (xs {ys} : List A) {x y : A} →
      xs ++ y ∷ x ∷ ys ∼[ bag ] xs ++ x ∷ y ∷ ys
bbl xs {ys} {x} {y} = record
  { to         = P.→-to-⟶ (bubble xs)
  ; from       = P.→-to-⟶ (bubble xs)
  ; inverse-of = record
    { left-inverse-of  = inv xs
    ; right-inverse-of = inv xs } }
  where
    inv : (xs {ys} : List A) {x y z : A} →
          (i : z ∈ xs ++ y ∷ x ∷ ys) →
          bubble xs (bubble xs i) ≡ i
    inv []       (here px)         = P.refl
    inv []       (there (here px)) = P.refl
    inv []       (there (there i)) = P.refl
    inv (x ∷ xs) (here px)         = P.refl
    inv (x ∷ xs) (there i)         = P.cong there (inv xs i)

-- There is a bijection between indices into the environment
-- ΓΔAΘ and the environment ΓAΔΘ.
fwd : (xs ys {zs} : List A) {w : A} →
      xs ++ ys ++ w ∷ zs ∼[ bag ] xs ++ w ∷ ys ++ zs
fwd (x ∷ xs) ys = B.∷-cong P.refl (fwd xs ys)
fwd []       ys = fwd' ys
  where
    fwd' : (xs {ys} : List A) {w : A} →
           xs ++ w ∷ ys ∼[ bag ] w ∷ xs ++ ys
    fwd' []       = id
    fwd' (x ∷ xs) = bbl [] ∘ B.∷-cong P.refl (fwd' xs)

bwd : (xs ys {zs} : List A) {w : A} →
      xs ++ w ∷ ys ++ zs ∼[ bag ] xs ++ ys ++ w ∷ zs
bwd xs ys = sym (fwd xs ys)

-- List all possible ways to split a list xs into two lists xs₁ and xs₂.
allSplit : (xs : List A) → List (Σ[ xs₁ ∈ List A ] Σ[ xs₂ ∈ List A ] xs ≡ xs₁ ++ xs₂)
allSplit []       = L.[ [] , [] , P.refl ]
allSplit (x ∷ xs) = now ∷ later
  where
    now   = ([] , x ∷ xs , P.refl)
    later = flip map (allSplit xs) $
      λ{(xs₁ , xs₂ , p) → (x ∷ xs₁ , xs₂ , P.cong (x ∷_) p)}

-- Test if allSplit does as advertised.
{-
private
  module _ where

    postulate x y z w : A

    test-allSplit :
      allSplit (x ∷ y ∷ z ∷ w ∷ []) ≡
      ( ( []                    , (x ∷ y ∷ z ∷ w ∷ []) , P.refl )
      ∷ ( (x ∷ [])              ,     (y ∷ z ∷ w ∷ []) , P.refl )
      ∷ ( (x ∷ y ∷ [])          ,         (z ∷ w ∷ []) , P.refl )
      ∷ ( (x ∷ y ∷ z ∷ [])      ,             (w ∷ []) , P.refl )
      ∷ ( (x ∷ y ∷ z ∷ w ∷ [] ) ,                  []  , P.refl )
      ∷ [] )
    test-allSplit = P.refl
-}

-- It is possible to list all environments Δ for which there
-- exists a bijection between indices into the environment Γ
-- and the environment Δ.
all : (xs : List A) → List (Σ[ ys ∈ List A ] xs ∼[ bag ] ys)
all [] = ([] , id) ∷ []
all (x ∷ xs) = concatMap insAll (all xs)
  where
    insAll : Σ[ ys ∈ List A ] xs ∼[ bag ] ys
           → List (Σ[ ys ∈ List A ] x ∷ xs ∼[ bag ] ys)
    insAll (ys , b) = map insOne (allSplit ys)
      where
        insOne : Σ[ ys₁ ∈ List A ] Σ[ ys₂ ∈ List A ] ys ≡ ys₁ ++ ys₂
               → Σ[ zs ∈ List A ] x ∷ xs ∼[ bag ] zs
        insOne (ys₁ , ys₂ , p) = ys₁ ++ x ∷ ys₂ ,
          bwd [] ys₁ {ys₂} {x} ∘ B.∷-cong P.refl (P.subst (ys ∼[ bag ]_) p id ∘ b)

-- Any element which is contained in a list created using replicate
-- is equal to the replicated element.
∈-replicate : {x y : A} (n : ℕ) → x ∈ y ∷ replicate n y → x ≡ y
∈-replicate zero    (here px) = px
∈-replicate zero    (there ())
∈-replicate (suc n) (here px) = px
∈-replicate (suc n) (there m) = ∈-replicate n m

-- Any bag which is equivalent to the bag created using replicate,
-- is equal to the bag created using replicate.
all-replicate : {xs : List A} {y : A} (n : ℕ) →

  xs ∼[ bag ] replicate n y → xs ≡ replicate n y

all-replicate {[]}     {y} zero    b = P.refl
all-replicate {[]}     {y} (suc n) b with from b ⟨$⟩ here P.refl; ... | ()
all-replicate {x ∷ xs} {y} zero    b with to   b ⟨$⟩ here P.refl; ... | ()
all-replicate {x ∷ xs} {y} (suc n) b = P.cong₂ _∷_ x=y (all-replicate n b')
  where
    x=y : x ≡ y
    x=y = ∈-replicate n (to b ⟨$⟩ here P.refl)
    b'  : xs ∼[ bag ] replicate n y
    b'  = B.drop-cons (P.subst (λ x → x ∷ xs ∼[ bag ] y ∷ replicate n y) x=y b)

-- The same lemma holds for replicate⁺.
all-replicate⁺ : {xs : List A} {y : A} (n : ℕ⁺) →

  xs ∼[ bag ] replicate⁺ n y → xs ≡ replicate⁺ n y

all-replicate⁺ {[]}     {y} (suc n) b with from b ⟨$⟩ here P.refl; ... | ()
all-replicate⁺ {x ∷ xs} {y} (suc n) b = P.cong₂ _∷_ x=y (all-replicate n b')
  where
    x=y : x ≡ y
    x=y = ∈-replicate n (to b ⟨$⟩ here P.refl)
    b'  : xs ∼[ bag ] replicate n y
    b'  = B.drop-cons (P.subst (λ x → x ∷ xs ∼[ bag ] y ∷ replicate n y) x=y b)

-- There is a bijection between indices into the environment
-- ΓΣΔΠ and the environment ΓΔΣΠ.
swp₄ : (xs ys zs {ws} : List A) →
      xs ++ zs ++ ys ++ ws ∼[ bag ] xs ++ ys ++ zs ++ ws
swp₄ xs []       zs = id
swp₄ xs (y ∷ ys) zs =
  ( P.subst₂ _∼[ bag ]_ (++.assoc xs [ y ] _) (++.assoc xs [ y ] _)
  $ swp₄ (xs ++ [ y ]) ys zs
  ) ∘ fwd xs zs

-- Alias for swp₄.
swp = swp₄

-- There is a bijection between indices into the environment
-- ΓΣΔ and the environment ΓΔΣ. This is mostly a convenience
-- function because of the annoyance of using ++.identity
-- in the logic proofs.
swp₃ : (xs ys {zs} : List A) →
       xs ++ zs ++ ys ∼[ bag ] xs ++ ys ++ zs
swp₃ xs ys {zs} =
  ( P.subst₂ (λ ys' zs' → xs ++ zs ++ ys' ∼[ bag ] xs ++ ys ++ zs')
             (proj₂ ++.identity ys)
             (proj₂ ++.identity zs)
  $ swp₄ xs ys zs
  )

-- There is a bijection between indices into the environment
-- ΓΣΔ and the environment ΓΔΣ. This is mostly a convenience
-- function because of the annoyance of using ++.identity
-- in the logic proofs.
swp₂ : (xs {ys} : List A) →
       ys ++ xs ∼[ bag ] xs ++ ys
swp₂ = swp₃ []

_-_ : (xs : List A) {x : A} (i : x ∈ xs) → List A
(x ∷ xs) - (here  _) = xs
(x ∷ xs) - (there i) = x ∷ xs - i

del-[] : {x y : A} (i : y ∈ x ∷ []) → (x ∷ []) - i ≡ []
del-[] (here px) = P.refl
del-[] (there ())

-- Given a proof of membership x ∈ xs, we can be sure that
-- there are two lists xs₁ and xs₂ s.t.
--
--   (1) xs = xs₁ ++ x ∷ xs₂; and
--   (2) xs - i = xs₁ ++ xs₂.
--
-- That is to say, that we can break the list xs into a prefix,
-- the element x, and a suffix, and that if we delete that occurrence
-- of x, we are left with the prefix and the suffix.
∈→++ : {xs : List A} {x : A} (i : x ∈ xs) →
      ∃₂ λ xs₁ xs₂ → xs ≡ xs₁ ++ x ∷ xs₂ × xs - i ≡ xs₁ ++ xs₂
∈→++ {x ∷ xs} (here P.refl) = ([] , xs , P.refl , P.refl)
∈→++ {x ∷ xs} (there i) with ∈→++ {xs} i
... | (xs₁ , xs₂ , p₁ , p₂) = (x ∷ xs₁ , xs₂ , P.cong (x ∷_) p₁ , P.cong (x ∷_) p₂)

-- Given two lists which are bag-equal, we can prove that if we delete
-- the same element from both lists, the resulting lists are also bag-equal.
del-to : {xs ys : List A} {x : A} →
         (eq : xs ∼[ bag ] ys) (i : x ∈ xs) →
         xs - i ∼[ bag ] ys - (to eq ⟨$⟩ i)
del-to {xs} {ys} {x} eq i
  with ∈→++ {xs} i
... | (xs₁ , xs₂ , p₁ , p₂) rewrite p₁ | p₂
  with ∈→++ {ys} (to eq ⟨$⟩ i)
... | (ys₁ , ys₂ , q₁ , q₂) rewrite q₁ | q₂
    = B.drop-cons (fwd [] ys₁ ∘ eq ∘ sym (fwd [] xs₁))

del-from : {xs ys : List A} {x : A} →
           (eq : ys ∼[ bag ] xs) (i : x ∈ xs) →
           ys - (from eq ⟨$⟩ i) ∼[ bag ] xs - i
del-from {xs} {ys} {x} eq i
  with ∈→++ {xs} i
... | (xs₁ , xs₂ , p₁ , p₂) rewrite p₁ | p₂
  with ∈→++ {ys} (from eq ⟨$⟩ i)
... | (ys₁ , ys₂ , q₁ , q₂) rewrite q₁ | q₂
    = B.drop-cons (fwd [] xs₁ ∘ eq ∘ sym (fwd [] ys₁))

-- Split a environment based on a proof of membership (used as index).
split : ∀ (xs {ys} : List A) {x : A} →
        (i : x ∈ xs ++ ys) →
        Σ[ j ∈ x ∈ xs ] ((xs ++ ys) - i ≡ xs - j ++ ys) ⊎
        Σ[ j ∈ x ∈ ys ] ((xs ++ ys) - i ≡ xs ++ ys - j)
split []       i         = inj₂ (i , P.refl)
split (_ ∷ xs) (here px) = inj₁ (here px , P.refl)
split (_ ∷ xs) (there i) with split xs i
... | inj₁ (j , p) = inj₁ (there j , P.cong (_ ∷_) p)
... | inj₂ (j , p) = inj₂ (j , P.cong (_ ∷_) p)

-- -}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
module x06-747Connectives-hc where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)

------------------------------------------------------------------------------
-- BEGIN : Copied from 747Isomorphism.

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  constructor mk-≃  -- This has been added, not in PLFA
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_

-- You may copy over the various reasoning modules if you wish.

-- END : Copied from 747Isomorphism.
------------------------------------------------------------------------------

------------------------------------------------------------------------------
-- logical AND is Cartesian product.

data _×_ (A : Set) (B : Set) : Set where

  ⟨_,_⟩ :
      A
    → B
      -----
    → A × B

-- destructors (aka eliminators) for ×.

proj₁ : ∀ {A B : Set}
  → A × B
    -----
  → A

proj₁ ⟨ a , _ ⟩ = a

proj₂ : ∀ {A B : Set}
  → A × B
    -----
  →     B

proj₂ ⟨ _ , b ⟩ = b

-- equivalent construction using records
record _×′_ (A B : Set) : Set where
  field
    proj₁′ : A
    proj₂′ : B
open _×′_

-- eta-equivalence relates constructors and destructors
η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ a , b ⟩ = refl

-- type with two members
infixr 2 _×_
data Bool : Set where
  true  : Bool
  false : Bool

-- type with three members (used in examples)
data Tri : Set where
  aa : Tri
  bb : Tri
  cc : Tri

-- Bool × Tri has six members
×-count : Bool × Tri → ℕ
×-count ⟨ true  , aa ⟩  =  1
×-count ⟨ true  , bb ⟩  =  2
×-count ⟨ true  , cc ⟩  =  3
×-count ⟨ false , aa ⟩  =  4
×-count ⟨ false , bb ⟩  =  5
×-count ⟨ false , cc ⟩  =  6

-- Cartesian product is commutative and associative up to isomorphism.

swap : ∀ {A B : Set} → A × B → B × A
swap ⟨ a , b ⟩ = ⟨ b , a ⟩

×-comm : ∀ {A B : Set} → A × B ≃ B × A
to      ×-comm = swap
from    ×-comm = swap
from∘to ×-comm ⟨ _ , _ ⟩ = refl
to∘from ×-comm ⟨ _ , _ ⟩ = refl

×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
to      ×-assoc ⟨ ⟨ a ,   b ⟩ , c ⟩   = ⟨   a , ⟨ b ,   c ⟩ ⟩
from    ×-assoc ⟨   a , ⟨ b ,   c ⟩ ⟩ = ⟨ ⟨ a ,   b ⟩ , c ⟩
from∘to ×-assoc ⟨ ⟨ _ ,   _ ⟩ , _ ⟩   = refl
to∘from ×-assoc ⟨   _ , ⟨ _ ,   _ ⟩ ⟩ = refl

-- A ⇔ B is isomorphic to (A → B) × (B → A)
iff-iso-if-onlyif : ∀ {A B : Set} → A ⇔ B ≃ (A → B) × (B → A)
_≃_.to         iff-iso-if-onlyif record { to = to ; from = from } = ⟨ to , from ⟩
to   (_≃_.from iff-iso-if-onlyif            ⟨ A→B , B→A ⟩)        = A→B
from (_≃_.from iff-iso-if-onlyif            ⟨ A→B , B→A ⟩)        = B→A
from∘to        iff-iso-if-onlyif record { to = to ; from = from } = refl
to∘from        iff-iso-if-onlyif            ⟨ A→B , B→A ⟩         = refl

------------------------------------------------------------------------------
-- logical True is a type with one member (unit)
data ⊤ : Set where
  tt :
    --
    ⊤

η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ tt = refl

⊤-count : ⊤ → ℕ
⊤-count tt = 1

-- Unit is the left and right identity of product.

⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
to      ⊤-identityˡ ⟨ ⊤  , a ⟩ =        a
from    ⊤-identityˡ        a   = ⟨ tt , a ⟩
from∘to ⊤-identityˡ ⟨ tt , a ⟩ = refl
to∘from ⊤-identityˡ        a   = refl

⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
to      ⊤-identityʳ ⟨ a , ⊤  ⟩ =   a
from    ⊤-identityʳ   a        = ⟨ a , tt ⟩
from∘to ⊤-identityʳ ⟨ a , tt ⟩ = refl
to∘from ⊤-identityʳ   a        = refl

------------------------------------------------------------------------------
-- logical OR (disjunction) is sum (disjoint union)

data _⊎_ : Set → Set → Set where

  inj₁ : ∀ {A B : Set}
    → A
      -----
    → A ⊎ B

  inj₂ : ∀ {A B : Set}
    →     B
      -----
    → A ⊎ B

-- a way to eliminate a sum (but easier to use pattern-matching to eliminate sums)
case-⊎ : ∀ {A B C : Set}
  → (A → C)
  → (B → C)
  →  A ⊎ B
    -----------
  →      C
case-⊎ f g (inj₁ x) = f x
case-⊎ f g (inj₂ x) = g x

-- eta equivalence for sums
η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
η-⊎ (inj₁ _) = refl
η-⊎ (inj₂ _) = refl

-- generalization
uniq-⊎ : ∀ {A B C : Set}
       → (h : A ⊎ B → C) → (w : A ⊎ B)
       → case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
uniq-⊎ h (inj₁ _) = refl
uniq-⊎ h (inj₂ _) = refl

infix 1 _⊎_

-- Bool ⊎ Tri has five members
⊎-count : Bool ⊎ Tri → ℕ
⊎-count (inj₁ true)   =  1
⊎-count (inj₁ false)  =  2
⊎-count (inj₂ aa)     =  3
⊎-count (inj₂ bb)     =  4
⊎-count (inj₂ cc)     =  5

-- Sum is commutative up to isomorphism.
⊎-comm : ∀ {A B : Set} → A ⊎ B ≃ B ⊎ A
to      ⊎-comm (inj₁ a) = inj₂ a
to      ⊎-comm (inj₂ b) = inj₁ b
from    ⊎-comm (inj₁ b) = inj₂ b
from    ⊎-comm (inj₂ a) = inj₁ a
from∘to ⊎-comm (inj₁ _) = refl
from∘to ⊎-comm (inj₂ _) = refl
to∘from ⊎-comm (inj₁ _) = refl
to∘from ⊎-comm (inj₂ _) = refl

-- Sum is associative up to isomorphism.
⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
to      ⊎-assoc (inj₁ (inj₁ a)) = inj₁ a
to      ⊎-assoc (inj₁ (inj₂ b)) = inj₂ (inj₁ b)
to      ⊎-assoc (inj₂ c)        = inj₂ (inj₂ c)
from    ⊎-assoc (inj₁ a)        = inj₁ (inj₁ a)
from    ⊎-assoc (inj₂ (inj₁ b)) = inj₁ (inj₂ b)
from    ⊎-assoc (inj₂ (inj₂ c)) = inj₂ c
from∘to ⊎-assoc (inj₁ (inj₁ _)) = refl
from∘to ⊎-assoc (inj₁ (inj₂ _)) = refl
from∘to ⊎-assoc (inj₂ _)        = refl
to∘from ⊎-assoc (inj₁ _)        = refl
to∘from ⊎-assoc (inj₂ (inj₁ _)) = refl
to∘from ⊎-assoc (inj₂ (inj₂ _)) = refl

------------------------------------------------------------------------------
-- logical False is the empty type ("bottom", "empty")

data ⊥ : Set where
  -- no clauses

-- Ex falso quodlibet "from falsehood, anything follows".
⊥-elim : ∀ {A : Set}
  → ⊥
    --
  → A

⊥-elim ()

uniq-⊥ : ∀ {C : Set}
       → (h : ⊥ → C) → (w : ⊥)
       → ⊥-elim w ≡ h w
uniq-⊥ h ()

⊥-count : ⊥ → ℕ
⊥-count ()

-- Empty is the left unit of sum up to isomorphism.
⊎-identityˡ : ∀ {A : Set} → ⊥ ⊎ A ≃ A
to      ⊎-identityˡ (inj₂ a) = a
from    ⊎-identityˡ       a  = inj₂ a
from∘to ⊎-identityˡ (inj₂ _) = refl
to∘from ⊎-identityˡ       _  = refl

-- Empty is the right unit of sum up to isomorphism.
⊎-identityʳ : ∀ {A : Set} → A ⊎ ⊥ ≃ A
to      ⊎-identityʳ (inj₁ a) = a
from    ⊎-identityʳ       a  = inj₁ a
from∘to ⊎-identityʳ (inj₁ _) = refl
to∘from ⊎-identityʳ       _  = refl

------------------------------------------------------------------------------
-- logical implication (if-then) is the function TYPE constructor.
-- Eliminating an if-then (modus ponens) is function application.

→-elim : ∀ {A B : Set}
  → (A → B)
  →  A
    -------
  →      B

→-elim L M = L M

-- →-elim works because eta-reduction for → is built in

η-→ : ∀ {A B : Set}
    → (f : A → B)
    → (λ (x : A) → f x) ≡ f
η-→ f = refl

-- The function space A → B is called the exponential Bᴬ.
-- Bool → Tri has 3² (9) members.
→-count : (Bool → Tri) → ℕ
→-count f with f true | f false
...          | aa     | aa      =   1
...          | aa     | bb      =   2
...          | aa     | cc      =   3
...          | bb     | aa      =   4
...          | bb     | bb      =   5
...          | bb     | cc      =   6
...          | cc     | aa      =   7
...          | cc     | bb      =   8
...          | cc     | cc      =   9

------------------------------------------------------------------------------
-- "currying" : functions of multiple parameters
-- math  : (p ^ n) ^ m = p ^ (n * m)
-- types : (A ^ B) ^ C ≃ A ^ (B × C)
currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
to      currying f = λ { ⟨ a , b ⟩ → f a b }
from    currying f = λ a b →  f ⟨ a , b ⟩
from∘to currying _ = refl
to∘from currying f = extensionality λ { ⟨ x , y ⟩ → refl }

-- math, : p ^ (n + m) =  (p ^ n) * (p ^ m)
-- types : (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
to      →-distrib-⊎ f             = ⟨ (λ a → f (inj₁ a)) , (λ b → f (inj₂ b)) ⟩
from    →-distrib-⊎ ⟨ A→C , B→C ⟩ = λ { (inj₁ a) → A→C a ; (inj₂ b) → B→C b }
from∘to →-distrib-⊎ _             = extensionality λ { (inj₁ x) → refl ; (inj₂ x) → refl }
to∘from →-distrib-⊎               = λ{ ⟨ g , h ⟩ → refl }

-- math  : (p * n) ^ m = (p ^ m) * (n ^ m)
-- types : (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
to      →-distrib-× f = ⟨ (λ a → proj₁ (f a)) , (λ a → proj₂ (f a)) ⟩
from    →-distrib-× f = λ a → ⟨ proj₁ f a , proj₂ f a ⟩
from∘to →-distrib-×   = λ a→b×c → extensionality λ a → η-× (a→b×c a)
to∘from →-distrib-×   = λ { ⟨ _ , _ ⟩ → refl }

×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
to      ×-distrib-⊎ ⟨ inj₁ a , c ⟩   = inj₁ ⟨ a , c ⟩
to      ×-distrib-⊎ ⟨ inj₂ b , c ⟩   = inj₂ ⟨ b , c ⟩
from    ×-distrib-⊎ (inj₁ ⟨ a , c ⟩) = ⟨ inj₁ a , c ⟩
from    ×-distrib-⊎ (inj₂ ⟨ b , c ⟩) = ⟨ inj₂ b , c ⟩
from∘to ×-distrib-⊎                  = λ { ⟨ inj₁   a , c ⟩  → refl ; ⟨ inj₂   b , c ⟩  → refl }
to∘from ×-distrib-⊎                  = λ { ( inj₁ ⟨ a , c ⟩) → refl ; ( inj₂ ⟨ b , c ⟩) → refl }

-- Think of a counterexample to show this is not an isomorphism. TODO
⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
to      ⊎-distrib-× (inj₁ ⟨ a , b ⟩)    = ⟨ inj₁ a , inj₁ b ⟩
to      ⊎-distrib-× (inj₂ c)            = ⟨ inj₂ c , inj₂ c ⟩
from    ⊎-distrib-× ⟨ inj₁ a , inj₁ b ⟩ = inj₁ ⟨ a , b ⟩
from    ⊎-distrib-× ⟨ inj₁ a , inj₂ c ⟩ = inj₂ c
from    ⊎-distrib-× ⟨ inj₂ c , inj₁ b ⟩ = inj₂ c
from    ⊎-distrib-× ⟨ inj₂ c , inj₂ C ⟩ = inj₂ c -- inj₂ C also valid (loses info)
from∘to ⊎-distrib-×                     = λ { (inj₁ ⟨ a , b ⟩) → refl ; (inj₂ c) → refl }

×-distrib-→ : ∀ {A B C : Set} → (C → (A × B)) ≃ (C → A) × (C → B)
to      ×-distrib-→ f = ⟨ (λ c →   proj₁ (f c)) , (λ c → proj₂ (f c)) ⟩
from    ×-distrib-→ f =    λ c → ⟨ proj₁  f c   ,        proj₂  f c   ⟩
from∘to ×-distrib-→   =    λ { c→a×b → extensionality λ c → η-× (c→a×b c) }
to∘from ×-distrib-→   =    λ { ⟨ c→a , c→b ⟩ → refl }

⊎-distrib-→ : ∀ {A B C : Set} → ((A ⊎ B) → C) ≃ (A → C) × (B → C)
to      ⊎-distrib-→ f = ⟨ (λ a →  f (inj₁ a)) , (λ b → f (inj₂ b)) ⟩
from    ⊎-distrib-→ f = λ { (inj₁ a) → (proj₁ f a) ; (inj₂ b) → (proj₂ f b) }
--from∘to ⊎-distrib-→ f = extensionality λ a⊎b → {!!} -- TODO
from∘to ⊎-distrib-→   = λ { a⊎b→c → extensionality λ { (inj₁ a) → refl ; (inj₂ b) → refl } }
to∘from ⊎-distrib-→   = λ { ⟨ a→c , b→c ⟩ → refl }

-- PLFA exercise: a weak distributive law.
⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
⊎-weak-× ⟨ inj₁ a , c ⟩ = inj₁ a
⊎-weak-× ⟨ inj₂ b , c ⟩ = inj₂ ⟨ b , c ⟩
-- State and prove the strong law, and explain the relationship. TODO

-- SumOfProdImpProdOfSum : disjunct of conjuncts implies a conjunct of disjuncts.
⊎×-implies-×⊎ : ∀ {A B C D : Set}
              → (A × B) ⊎ (C × D)
              → (A ⊎ C) × (B ⊎ D)
⊎×-implies-×⊎ (inj₁ ⟨ a , b ⟩) = ⟨ inj₁ a , inj₁ b ⟩
⊎×-implies-×⊎ (inj₂ ⟨ c , d ⟩) = ⟨ inj₂ c , inj₂ d ⟩

-- the converse is NOT true
×⊎-implies-⊎×-not : ∀ {A B C D : Set}
                  → (A ⊎ C) × (B ⊎ D)
                  → (A × B) ⊎ (C × D)
×⊎-implies-⊎×-not ⟨ inj₁ a , inj₁ b ⟩ = inj₁ ⟨ a , b ⟩
×⊎-implies-⊎×-not ⟨ inj₁ a , inj₂ d ⟩ = {!!} -- A × B ⊎ C × D -- not possible
×⊎-implies-⊎×-not ⟨ inj₂ c , inj₁ b ⟩ = {!!} -- A × B ⊎ C × D -- not possible
×⊎-implies-⊎×-not ⟨ inj₂ c , inj₂ d ⟩ = inj₂ ⟨ c , d ⟩

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

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

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