text:
module paper where

open import Data.Bool using (Bool; not; _∨_; _∧_)
open import Data.Nat using (ℕ)
open import Data.Fin using (Fin; suc; zero)
open import Data.List using (List; _++_) renaming (_∷_ to _,_; [] to ∅)
open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

postulate
  Entity   : Set
  _⊃_      : Bool → Bool → Bool
  FORALL   : (Entity → Bool) → Bool
  EXISTS   : (Entity → Bool) → Bool
  PERSON   : Entity → Bool
  FIND     : Entity → Entity → Bool
  UNICORN  : Entity → Bool

data U : Set where S N NP : U

⟦_⟧ᵁ : U → Set
⟦ S   ⟧ᵁ = Bool
⟦ N   ⟧ᵁ = Entity → Bool
⟦ NP  ⟧ᵁ = Entity

import IntuitionisticLogic U ⟦_⟧ᵁ as IL
import LinearLogic U S ⟦_⟧ᵁ as LP
import LambekGrishinCalculus U S ⟦_⟧ᵁ as LG

open LG
open IL.Explicit using (Ctxt; _,_; ∅)
open IL.Explicit.Reify TypeReify

everyone  : ⟦ (el NP + ⇐ el N +) ⊗ el N + ⟧
everyone  = ( (λ{ (A , B) → FORALL (λ x → B x ⊃ A x) }) , PERSON )
finds     : ⟦ (el NP + ⇒ el S -) ⇐ el NP + ⟧
finds     = λ{ ((x , k) , y) → k (FIND y x) }
some      : ⟦ el NP + ⇐ el N + ⟧
some      = λ{ (A , B) → EXISTS (λ x → A x ∧ B x) }
unicorn   : ⟦ el N + ⟧
unicorn   = UNICORN

sent :
  · (el NP + ⇐ el N +) ⊗ el N +         -- everyone
  · ⊗ (· (el NP + ⇒ el S -) ⇐ el NP +  -- finds
  · ⊗ (· el NP + ⇐ el N +               -- some
  · ⊗ · el N + ·                         -- unicorn
  )) ⊢[ el S - ]
sent =
  μ (res₃ (⊗L (res₃ (μ̃* (⇐L (
    μ̃ (res₄ (res₁ (res₁ (res₃ (μ̃* (⇐L (
      μ̃ (res₂ (res₃ (μ̃* (⇐L (⇒L var covar) var))))) var))))))) var)))))

test : ([ sent ] (everyone , finds , some , unicorn , ∅))
     ≡ (λ k → FORALL (λ x₁ → PERSON x₁ ⊃ EXISTS (λ x₂ → k (FIND x₂ x₁) ∧ UNICORN x₂)))
test = refl


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Escape {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.LogicalRelation

open import Tools.Embedding
open import Tools.Product
import Tools.PropositionalEquality as PE

-- Reducible types are well-formed.
escape : ∀ {l Γ A} → Γ ⊩⟨ l ⟩ A → Γ ⊢ A
escape (Uᵣ′ l′ l< ⊢Γ) = Uⱼ ⊢Γ
escape (ℕᵣ [ ⊢A , ⊢B , D ]) = ⊢A
escape (ne′ K [ ⊢A , ⊢B , D ] neK K≡K) = ⊢A
escape (Πᵣ′ F G [ ⊢A , ⊢B , D ] ⊢F ⊢G A≡A [F] [G] G-ext) = ⊢A
escape (emb′ 0<1 [A]) = escape [A]

-- Reducible type equality respect the equality relation.
escapeEq : ∀ {l Γ A B} → ([A] : Γ ⊩⟨ l ⟩ A)
            → Γ ⊩⟨ l ⟩ A ≡ B / [A]
            → Γ ⊢ A ≅ B
escapeEq (Uᵣ′ l' l< ⊢Γ) (U₌ PE.refl) = ≅-Urefl ⊢Γ
escapeEq (ℕᵣ [ ⊢A , ⊢B , D ]) (ιx (ℕ₌ D′)) = ≅-red D D′ ℕₙ ℕₙ (≅-ℕrefl (wf ⊢A))
escapeEq (ne′ K D neK K≡K) (ιx (ne₌ M D′ neM K≡M)) = ≅-red (red D) (red D′) (ne neK) (ne neM) (~-to-≅ K≡M)
escapeEq (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext) (Π₌ F′ G′ D′ A≡B [F≡F′] [G≡G′]) =
  ≅-red (red D) D′ Πₙ Πₙ A≡B
escapeEq (emb′ 0<1 A) (ιx A≡B) = escapeEq A A≡B

-- Reducible terms are well-formed.
escapeTerm : ∀ {l Γ A t} → ([A] : Γ ⊩⟨ l ⟩ A)
              → Γ ⊩⟨ l ⟩ t ∷ A / [A]
              → Γ ⊢ t ∷ A
escapeTerm (Uᵣ′ l′ l< ⊢Γ) (Uₜ A [ ⊢t , ⊢u , d ] typeA A≡A [A]) = ⊢t
escapeTerm (ℕᵣ D) (ιx (ℕₜ n [ ⊢t , ⊢u , d ] t≡t prop)) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (ne′ K D neK K≡K) (ιx (neₜ k [ ⊢t , ⊢u , d ] nf)) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
               (f , [ ⊢t , ⊢u , d ] , funcF , f≡f , [f] , [f]₁) =
  conv ⊢t (sym (subset* (red D)))
escapeTerm (emb′ 0<1 A) (ιx t) = escapeTerm A t

-- Reducible term equality respect the equality relation.
escapeTermEq : ∀ {l Γ A t u} → ([A] : Γ ⊩⟨ l ⟩ A)
                → Γ ⊩⟨ l ⟩ t ≡ u ∷ A / [A]
                → Γ ⊢ t ≅ u ∷ A
escapeTermEq (Uᵣ′ l′ l< ⊢Γ) (Uₜ₌ A B d d′ typeA typeB A≡B [A] [B] [A≡B]) =
  ≅ₜ-red (id (Uⱼ ⊢Γ)) (redₜ d) (redₜ d′) Uₙ (typeWhnf typeA) (typeWhnf typeB) A≡B
escapeTermEq (ℕᵣ D) (ιx (ℕₜ₌ k k′ d d′ k≡k′ prop)) =
  let natK , natK′ = split prop
  in  ≅ₜ-red (red D) (redₜ d) (redₜ d′) ℕₙ
             (naturalWhnf natK) (naturalWhnf natK′) k≡k′
escapeTermEq (ne′ K D neK K≡K)
                 (ιx (neₜ₌ k m d d′ (neNfₜ₌ neT neU t≡u))) =
  ≅ₜ-red (red D) (redₜ d) (redₜ d′) (ne neK) (ne neT) (ne neU)
         (~-to-≅ₜ t≡u)
escapeTermEq (Πᵣ′ F G D ⊢F ⊢G A≡A [F] [G] G-ext)
                 (Πₜ₌ f g d d′ funcF funcG f≡g [f] [g] [f≡g]) =
  ≅ₜ-red (red D) (redₜ d) (redₜ d′) Πₙ (functionWhnf funcF) (functionWhnf funcG) f≡g
escapeTermEq (emb′ 0<1 A) (ιx t≡u) = escapeTermEq A t≡u

ext: agda

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation.Data.Integer where

-- TODO

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
module Categories.Products where

open import Library renaming (_×_ to Pair) hiding ([_])
open import Categories

_×_ : ∀{l l' m m'}(C : Cat {l}{m})(D : Cat {l'}{m'}) -> Cat
C × D = record
          { Obj  = Pair (Obj C) (Obj D)
          ; Hom  = λ {(X , X') (Y , Y') -> Pair (Hom C X Y) (Hom D X' Y')}
          ; iden = iden C , iden D
          ; comp = λ {(f , f') (g , g') -> comp C f g , comp D f' g'}
          ; idl  = cong₂ _,_ (idl C) (idl D)
          ; idr  = cong₂ _,_ (idr C) (idr D)
          ; ass  = cong₂ _,_ (ass C) (ass D)
          } where open Cat

infixr 50 _×_

record Prod {l}{m}(C : Cat {l}{m})(A : Cat.Obj C)(B : Cat.Obj C) : Set (l ⊔ m)
  where
  constructor prod
  open Cat C
  field Pr : Obj
        π₁ : Hom Pr A
        π₂ : Hom Pr B
        [_,_] : ∀{C} → Hom C A → Hom C B → Hom C Pr
        law1 : ∀{C}{f : Hom C A}{g} → comp π₁ [ f , g ] ≅ f
        law2 : ∀{C}{f : Hom C A}{g} → comp π₂ [ f , g ] ≅ g
        law3 : ∀{C}{f : Hom C A}{g : Hom C B}{h : Hom C Pr} →
               comp π₁ h ≅ f → comp π₂ h ≅ g → h ≅ [ f , g ]

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
module Issue59 where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

-- This no longer termination checks with the
-- new rules for with.
bad : Nat → Nat
bad n with n
... | zero  = zero
... | suc m = bad m

-- This shouldn't termination check.
bad₂ : Nat → Nat
bad₂ n with bad₂ n
... | m = m

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Cats.Util.SetoidMorphism.Iso where

open import Data.Product using (_,_ ; proj₁ ; proj₂)
open import Level using (_⊔_)
open import Relation.Binary using (Setoid ; IsEquivalence)

open import Cats.Util.SetoidMorphism as Mor using
  ( _⇒_ ; arr ; resp ; _≈_ ; ≈-intro ; ≈-elim ; ≈-elim′ ; _∘_ ; ∘-resp ; id ; IsInjective
  ; IsSurjective)
open import Cats.Util.SetoidReasoning

private
  module S = Setoid

record IsIso {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
  (f : A ⇒ B) : Set (l ⊔ l≈ ⊔ l′ ⊔ l≈′)
  where
  field
    back : B ⇒ A
    forth-back : f ∘ back ≈ id
    back-forth : back ∘ f ≈ id

open IsIso

record _≅_ {l l≈} (A : Setoid l l≈) {l′ l≈′} (B : Setoid l′ l≈′)
  : Set (l ⊔ l≈ ⊔ l′ ⊔ l≈′)
  where
  field
    forth : A ⇒ B
    back : B ⇒ A
    forth-back : forth ∘ back ≈ id
    back-forth : back ∘ forth ≈ id

open _≅_ public

IsIso→≅ : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′} (f : A ⇒ B)
  → IsIso f → A ≅ B
IsIso→≅ f i = record
    { forth = f
    ; back = back i
    ; forth-back = forth-back i
    ; back-forth = back-forth i
    }

≅→IsIso : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
  → (i : A ≅ B) → IsIso (forth i)
≅→IsIso i = record
    { back = back i
    ; forth-back = forth-back i
    ; back-forth = back-forth i
    }

IsIso-resp : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
  → {f g : A ⇒ B} → f ≈ g → IsIso f → IsIso g
IsIso-resp {A = A} {B = B} {f} {g} f≈g i = record
    { back = back i
    ; forth-back = ≈-intro λ {x} {y} x≈y →
        begin⟨ B ⟩
          arr g (arr (back i) x)
        ≈⟨ B.sym (≈-elim f≈g (resp (back i) (B.sym x≈y))) ⟩
          arr f (arr (back i) y)
        ≈⟨ ≈-elim′ (forth-back i) ⟩
          y
        ∎
    ; back-forth = ≈-intro λ {x} {y} x≈y →
        begin⟨ A ⟩
          arr (back i) (arr g x)
        ≈⟨ resp (back i) (B.sym (≈-elim f≈g (A.sym x≈y))) ⟩
          arr (back i) (arr f y)
        ≈⟨ ≈-elim′ (back-forth i) ⟩
          y
        ∎
    }
  where
    module A = Setoid A
    module B = Setoid B

refl : ∀ {l l≈} {A : Setoid l l≈} → A ≅ A
refl = record
    { forth = id
    ; back = id
    ; forth-back = ≈-intro λ eq → eq
    ; back-forth = ≈-intro λ eq → eq
    }

sym : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
  → A ≅ B → B ≅ A
sym i = record
    { forth = back i
    ; back = forth i
    ; forth-back = back-forth i
    ; back-forth = forth-back i
    }

trans : ∀ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′}
  → ∀ {l″ l≈″} {C : Setoid l″ l≈″}
  → A ≅ B → B ≅ C → A ≅ C
trans {A = A} {C = C} AB BC = record
    { forth = forth BC ∘ forth AB
    ; back = back AB ∘ back BC
    ; forth-back = ≈-intro λ x≈y
        → S.trans C (resp (forth BC) (≈-elim (forth-back AB) (resp (back BC) x≈y)))
            (≈-elim′ (forth-back BC))
    ; back-forth = ≈-intro λ x≈y
        → S.trans A (resp (back AB) (≈-elim (back-forth BC) (resp (forth AB) x≈y)))
            (≈-elim′ (back-forth AB))
    }

module _ {l l≈} {A : Setoid l l≈} {l′ l≈′} {B : Setoid l′ l≈′} where

  Injective∧Surjective→Iso : {f : A ⇒ B}
    → IsInjective f → IsSurjective f → IsIso f
  Injective∧Surjective→Iso {f} inj surj = record
      { back = record
        { arr = λ b → proj₁ (surj b)
        ; resp = λ {b} {c} b≈c → inj
            (S.trans B (S.sym B (proj₂ (surj b))) (S.trans B b≈c (proj₂ (surj c))))
        }
      ; forth-back = ≈-intro λ {x} {y} x≈y → S.trans B (S.sym B (proj₂ (surj x))) x≈y
      ; back-forth = ≈-intro λ {x} {y} x≈y → inj
          (S.trans B (S.sym B (proj₂ (surj _))) (resp f x≈y))
      }

  Injective∧Surjective→≅ : {f : A ⇒ B} → IsInjective f → IsSurjective f → A ≅ B
  Injective∧Surjective→≅ {f} inj surj
      = IsIso→≅ f (Injective∧Surjective→Iso inj surj)

  Iso→Injective : {f : A ⇒ B} → IsIso f → IsInjective f
  Iso→Injective {f} i {a} {b} fa≈fb =
      begin⟨ A ⟩
        a
      ≈⟨ S.sym A (≈-elim′ (back-forth i)) ⟩
        arr (back i) (arr f a)
      ≈⟨ resp (back i) fa≈fb ⟩
        arr (back i) (arr f b)
      ≈⟨ ≈-elim′ (back-forth i) ⟩
        b
      ∎

  ≅-Injective : (i : A ≅ B) → IsInjective (forth i)
  ≅-Injective i = Iso→Injective (≅→IsIso i)

  Iso→Surjective : {f : A ⇒ B} → IsIso f → IsSurjective f
  Iso→Surjective i b = arr (back i) b  , S.sym B (≈-elim′ (forth-back i))

  ≅-Surjective : (i : A ≅ B) → IsSurjective (forth i)
  ≅-Surjective i = Iso→Surjective (≅→IsIso i)

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-
    T R U N C A T I O N   L E V E L S
                 I N
H O M O T O P Y   T Y P E   T H E O R Y

======= ELECTRONIC APPENDIX =======

           NICOLAI KRAUS

           February 2015
-}

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

module INDEX where

-- Chapter 2
open import Preliminaries
-- Parts of Chapter 2 are in a separate file:
open import Pointed

{- Chapter 3,4,5,6 are joint work with
   Martin Escardo,
   Thierry Coquand,
   Thorsten Altenkirch -}

-- Chapter 3
open import Truncation_Level_Criteria

-- Chapter 4
open import Anonymous_Existence_CollSplit
open import Anonymous_Existence_Populatedness
open import Anonymous_Existence_Comparison

-- Chapter 5
open import Weakly_Constant_Functions

-- Chapter 6
open import Judgmental_Computation

{- Chapter 7 (joint work with Christian Sattler)
   has two parts. First, we construct homotopically
   complicated types; this development is distributed
   beween two files. Then, we discuss connectedness,
   which turns out to be very hard to formalise;
   we use in total five files to structure that
   discussion, see below. -}

{- First, we have an auxiliary file which makes precise
   that the 'universe of n-types' behaves like an actual
   universe. We formalise operations for it; this is
   very useful as it allows a more 'principled' development. -}
open import UniverseOfNTypes
{- Now: Sections 1-4 of Chapter 7, where 1,2 are "hidden".
   They are special cases of the more general theorem that
   we prove in 7.4; the special cases are written out only
   for pedagogical reasons and are thus omitted in this
   formalisation. -}
open import HHHUU-ComplicatedTypes

{- Note that Chapter 7.5 is not formalised, even though it
   could have been; we omit it because it is only an
   alternative to the above formalisation, and actually
   leads to a weaker result than the one in
   'HHHUU-ComplicatedTypes'.

   Chapter 7.6 is very hard to formalise (mostly done by
   Christian Sattler). Caveat: The order of the statements
   in the formalisation is different from the order in
   the thesis (it sometimes is more convenient to define
   multiple notions in the same module because they share
   argument to avoid replication of code, without them
   belonging together logically).

   First, we show (in a separate file) that the non-dependent
   universal property and the dependent universal
   property are equivalent.

   Contains: Definition 7.6.2, Lemma 7.6.6 -}
open import Trunc.Universal

-- Definition 7.6.4, Lemma 7.6.7, Corollary 7.6.8
open import Trunc.Basics

-- Lemma 7.6.9, Lemma 7.6.10
-- (actually even a stronger version of Lemma 7.6.10)
open import Trunc.TypeConstructors

{- main part of connectedness:
   (link to 7.6.1,)
   Definition 7.6.13, Definition 7.6.11,
   Lemma 7.6.14, Lemma 7.6.12, Lemma 7.6.15
   and
   Theorem 7.7.1 -}
open import Trunc.Connection

-- Remark 7.6.16
open import Trunc.ConnectednessAlt

{- The main result of Chapter 8 is, unfortunately,
   meta-theoretical. It is plausible that in an
   implementation of a type theory with 'two levels'
   (one semi-internal 'strict' equality and the
   ordinary identity type), the complete Chapter 8
   could be formalised; but at the moment, this is
   merely speculation. -}

-- Chapter 9.2: Semi-Simplicial Types

-- Proposition 9.2.1 (Δ₊ implemented with judgmental categorical laws)
open import Deltaplus

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
{-# OPTIONS --verbose tc.constr.findInScope:20 #-}

module InstanceArgumentsConstraints where

data Bool : Set where
  true false : Bool

postulate A1 A2 B C : Set
          a1 : A1
          a2 : A2
          someF : A1 → C

record Class (R : Bool → Set) : Set where
  field f : (t : Bool) → R t

open Class {{...}}

class1 : Class (λ _ → A1)
class1 = record { f = λ _ → a1 }

class2 : Class (λ _ → A2)
class2 = record { f = λ _ → a2 }

test : C
test = someF (f true)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


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

module Data.Bool where

open import Level
open import Agda.Builtin.Bool using (Bool; true; false) public
open import Data.Unit
open import Data.Empty

bool : ∀ {ℓ} {P : Bool → Type ℓ} (f : P false) (t : P true) → (x : Bool) → P x
bool f t false = f
bool f t true = t

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

infixl 6 _or_
_or_ : Bool → Bool → Bool
false or y = y
true  or y = true

infixl 7 _and_
_and_ : Bool → Bool → Bool
false and y = false
true  and y = y

infixr 0 if_then_else_
if_then_else_ : ∀ {a} {A : Set a} → Bool → A → A → A
if true  then x else _ = x
if false then _ else x = x

T : Bool → Type₀
T true  = ⊤
T false = ⊥

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------
-- Example: Left recursive expression grammar
------------------------------------------------------------------------

module TotalParserCombinators.Examples.Expression where

open import Codata.Musical.Notation
open import Data.Char as Char using (Char)
open import Data.List
open import Data.Nat
open import Data.String as String using (String)
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)

open import TotalParserCombinators.BreadthFirst
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser

open Token Char Char._≟_

------------------------------------------------------------------------
-- An expression grammar

-- t ∷= t '+' f ∣ f
-- f ∷= f '*' a ∣ a
-- a ∷= '(' t ')' ∣ n

-- Applicative implementation of the grammar.

module Applicative where

  mutual

    term   = ♯ (return (λ e₁ _ e₂ → e₁ + e₂) ⊛ term) ⊛ tok '+' ⊛ factor
           ∣ factor

    factor = ♯ (return (λ e₁ _ e₂ → e₁ * e₂) ⊛ factor) ⊛ tok '*' ⊛ atom
           ∣ atom

    atom   = return (λ _ e _ → e) ⊛ tok '(' ⊛ ♯ term ⊛ tok ')'
           ∣ number

-- Monadic implementation of the grammar.

module Monadic where

  mutual

    term   = factor
           ∣ ♯ term            >>= λ e₁ →
             tok '+'           >>= λ _  →
             factor            >>= λ e₂ →
             return (e₁ + e₂)

    factor = atom
           ∣ ♯ factor          >>= λ e₁ →
             tok '*'           >>= λ _  →
             atom              >>= λ e₂ →
             return (e₁ * e₂)

    atom   = number
           ∣ tok '('           >>= λ _  →
             ♯ term            >>= λ e  →
             tok ')'           >>= λ _  →
             return e

------------------------------------------------------------------------
-- Unit tests

module Tests where

  test : ∀ {R xs} → Parser Char R xs → String → List R
  test p = parse p ∘ String.toList

  -- Some examples have been commented out in order to reduce
  -- type-checking times.

  -- ex₁ : test Applicative.term "1*(2+3)" ≡ [ 5 ]
  -- ex₁ = P.refl

  -- ex₂ : test Applicative.term "1*(2+3" ≡ []
  -- ex₂ = P.refl

  ex₃ : test Monadic.term "1+2+3" ≡ [ 6 ]
  ex₃ = P.refl

  ex₄ : test Monadic.term "+32" ≡ []
  ex₄ = P.refl

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module Tactic.Nat.Reflect where

open import Prelude hiding (abs)
open import Control.Monad.State
open import Control.Monad.Transformer

import Agda.Builtin.Nat as Builtin

open import Builtin.Reflection
open import Tactic.Reflection
open import Tactic.Reflection.Quote
open import Tactic.Reflection.Meta
open import Tactic.Deriving.Quotable
open import Tactic.Reflection.Equality

open import Tactic.Nat.Exp

R = StateT (Nat × List (Term × Nat)) TC

fail : ∀ {A} → R A
fail = lift (typeErrorS "reflection error")

liftMaybe : ∀ {A} → Maybe A → R A
liftMaybe = maybe fail pure

runR : ∀ {A} → R A → TC (Maybe (A × List Term))
runR r =
  maybeA (second (reverse ∘ map fst ∘ snd) <$> runStateT r (0 , []))

pattern `Nat = def (quote Nat) []

infixr 1 _`->_
infix  4 _`≡_

pattern _`≡_ x y = def (quote _≡_) (_ ∷ hArg `Nat ∷ vArg x ∷ vArg y ∷ [])
pattern _`->_ a b = pi (vArg a) (abs _ b)

pattern _`+_ x y = def₂ (quote Builtin._+_) x y
pattern _`*_ x y = def₂ (quote Builtin._*_) x y
pattern `0       = con₀ (quote Nat.zero)
pattern `suc n   = con₁ (quote Nat.suc) n

fresh : Term → R (Exp Var)
fresh t =
  get >>= uncurry′ λ i Γ →
   var i <$ put (suc i , (t , i) ∷ Γ)

⟨suc⟩ : ∀ {X} → Exp X → Exp X
⟨suc⟩ (lit n) = lit (suc n)
⟨suc⟩ (lit n ⟨+⟩ e) = lit (suc n) ⟨+⟩ e
⟨suc⟩ e = lit 1 ⟨+⟩ e

private
  forceInstance : Name → Term → R ⊤
  forceInstance i v = lift $ unify v (def₀ i)
  forceSemiring = forceInstance (quote SemiringNat)
  forceNumber   = forceInstance (quote NumberNat)

termToExpR : Term → R (Exp Var)
termToExpR (a `+ b) = ⦇ termToExpR a ⟨+⟩ termToExpR b ⦈
termToExpR (a `* b) = ⦇ termToExpR a ⟨*⟩ termToExpR b ⦈
termToExpR (def (quote Semiring._+_) (_ ∷ _ ∷ vArg i@(meta x _) ∷ vArg a ∷ vArg b ∷ [])) = do
  forceSemiring i
  ⦇ termToExpR a ⟨+⟩ termToExpR b ⦈
termToExpR (def (quote Semiring._*_) (_ ∷ _ ∷ vArg i@(meta x _) ∷ vArg a ∷ vArg b ∷ [])) = do
  lift $ unify i (def₀ (quote SemiringNat))
  ⦇ termToExpR a ⟨*⟩ termToExpR b ⦈
termToExpR (def (quote Semiring.zro) (_ ∷ _ ∷ vArg i@(meta x _) ∷ [])) = do
  forceSemiring i
  pure (lit 0)
termToExpR (def (quote Semiring.one) (_ ∷ _ ∷ vArg i@(meta x _) ∷ [])) = do
  forceSemiring i
  pure (lit 1)
termToExpR (def (quote Number.fromNat) (_ ∷ _ ∷ vArg i@(meta x _) ∷ vArg a ∷ _ ∷ [])) = do
  forceNumber i
  termToExpR a
termToExpR `0       = pure (lit 0)
termToExpR (`suc a) = ⟨suc⟩ <$> termToExpR a
termToExpR (lit (nat n)) = pure (lit n)
termToExpR (meta x _) = lift (blockOnMeta x)
termToExpR unknown  = fail
termToExpR t = do
  lift (ensureNoMetas t)
  just i ← gets (flip lookup t ∘ snd) where nothing → fresh t
  pure (var i)

private
  lower : Nat → Term → R Term
  lower 0 = pure
  lower i = liftMaybe ∘ strengthen i

termToEqR : Term → R (Exp Var × Exp Var)
termToEqR (lhs `≡ rhs) = ⦇ termToExpR lhs , termToExpR rhs ⦈
termToEqR (def (quote _≡_) (_ ∷ hArg (meta x _) ∷ _)) = lift (blockOnMeta x)
termToEqR (meta x _) = lift (blockOnMeta x)
termToEqR _ = fail

termToHypsR′ : Nat → Term → R (List (Exp Var × Exp Var))
termToHypsR′ i (hyp `-> a) = _∷_ <$> (termToEqR =<< lower i hyp) <*> termToHypsR′ (suc i) a
termToHypsR′ _ (meta x _) = lift (blockOnMeta x)
termToHypsR′ i a = [_] <$> (termToEqR =<< lower i a)

termToHypsR : Term → R (List (Exp Var × Exp Var))
termToHypsR = termToHypsR′ 0

termToHyps : Term → TC (Maybe (List (Exp Var × Exp Var) × List Term))
termToHyps t = runR (termToHypsR t)

termToEq : Term → TC (Maybe ((Exp Var × Exp Var) × List Term))
termToEq t = runR (termToEqR t)

buildEnv : List Nat → Env Var
buildEnv []        i      = 0
buildEnv (x ∷ xs)  zero   = x
buildEnv (x ∷ xs) (suc i) = buildEnv xs i

defaultArg : Term → Arg Term
defaultArg = arg (arg-info visible relevant)

data ProofError {a} : Set a → Set (lsuc a) where
  bad-goal : ∀ g → ProofError g

qProofError : Term → Term
qProofError v = con (quote bad-goal) (defaultArg v ∷ [])

implicitArg instanceArg : ∀ {A} → A → Arg A
implicitArg = arg (arg-info hidden relevant)
instanceArg = arg (arg-info instance′ relevant)

unquoteDecl QuotableExp = deriveQuotable QuotableExp (quote Exp)

stripImplicitArg : Arg Term → List (Arg Term)
stripImplicitArgs : List (Arg Term) → List (Arg Term)
stripImplicitAbsTerm : Abs Term → Abs Term
stripImplicitArgTerm : Arg Term → Arg Term

stripImplicit : Term → Term
stripImplicit (var x args) = var x (stripImplicitArgs args)
stripImplicit (con c args) = con c (stripImplicitArgs args)
stripImplicit (def f args) = def f (stripImplicitArgs args)
stripImplicit (meta x args) = meta x (stripImplicitArgs args)
stripImplicit (lam v t) = lam v (stripImplicitAbsTerm t)
stripImplicit (pi t₁ t₂) = pi (stripImplicitArgTerm t₁) (stripImplicitAbsTerm t₂)
stripImplicit (agda-sort x) = agda-sort x
stripImplicit (lit l) = lit l
stripImplicit (pat-lam cs args) = pat-lam cs (stripImplicitArgs args)
stripImplicit unknown = unknown

stripImplicitAbsTerm (abs x v) = abs x (stripImplicit v)

stripImplicitArgs [] = []
stripImplicitArgs (a ∷ as) = stripImplicitArg a ++ stripImplicitArgs as

stripImplicitArgTerm (arg i x) = arg i (stripImplicit x)

stripImplicitArg (arg (arg-info visible r) x) = arg (arg-info visible r) (stripImplicit x) ∷ []
stripImplicitArg (arg (arg-info hidden r) x) = []
stripImplicitArg (arg (arg-info instance′ r) x) = []

quotedEnv : List Term → Term
quotedEnv ts = def (quote buildEnv) $ defaultArg (quoteList $ map stripImplicit ts) ∷ []

QED : ∀ {a} {A : Set a} {x : Maybe A} → Set
QED {x = x} = IsJust x

get-proof : ∀ {a} {A : Set a} (prf : Maybe A) → QED {x = prf} → A
get-proof (just eq) _ = eq
get-proof nothing ()
{-# STATIC get-proof #-}

getProof : Name → Term → Term → Term
getProof err t proof =
  def (quote get-proof)
  $ vArg proof
  ∷ vArg (def err $ vArg (stripImplicit t) ∷ [])
  ∷ []

failedProof : Name → Term → Term
failedProof err t =
  def (quote get-proof)
  $ vArg (con (quote nothing) [])
  ∷ vArg (def err $ vArg (stripImplicit t) ∷ [])
  ∷ []

cantProve : Set → ⊤
cantProve _ = _

invalidGoal : Set → ⊤
invalidGoal _ = _

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Group.Algebra where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphism
open import Cubical.Algebra.Group.MorphismProperties

open import Cubical.HITs.PropositionalTruncation hiding (map)

-- open import Cubical.Data.Group.Base

open Iso
open Group
open GroupHom

private
  variable
    ℓ ℓ₁ ℓ₂ ℓ₃ : Level

------- elementary properties of morphisms --------

-- (- 0) = 0
-0≡0 : ∀ {ℓ} {G : Group {ℓ}} → (- G) (0g G) ≡ (0g G) --  - 0 ≡ 0
-0≡0 {G = G} =  sym (IsGroup.lid (isGroup G) _) ∙ fst (IsGroup.inverse (isGroup G) _)

-- ϕ(0) ≡ 0
morph0→0 : ∀ {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) (f : GroupHom G H)
           → fun f (0g G) ≡ 0g H
morph0→0 G H f =
  (fun f) (0g G)                                        ≡⟨ sym (IsGroup.rid (isGroup H) _) ⟩
  (f' (0g G) H.+ 0g H)                                  ≡⟨ (λ i → f' (0g G) H.+ invr H (f' (0g G)) (~ i)) ⟩
  (f' (0g G) H.+ (f' (0g G) H.+ (H.- f' (0g G))))       ≡⟨ (Group.assoc H (f' (0g G)) (f' (0g G)) (H.- (f' (0g G)))) ⟩
  ((f' (0g G) H.+ f' (0g G)) H.+ (H.- f' (0g G)))       ≡⟨ sym (cong (λ x → x H.+ (H.- f' (0g G))) (sym (cong f' (IsGroup.lid (isGroup G) _)) ∙ isHom f (0g G) (0g G))) ⟩
  (f' (0g G)) H.+ (H.- (f' (0g G)))                     ≡⟨ invr H (f' (0g G)) ⟩
  0g H ∎
  where
  module G = Group G
  module H = Group H
  f' = fun f

-- ϕ(- x) = - ϕ(x)
morphMinus : ∀ {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) → (ϕ : GroupHom G H)
            → (g : ⟨ G ⟩) → fun ϕ ((- G) g) ≡ (- H) (fun ϕ g)
morphMinus G H ϕ g =
  f (G.- g)                             ≡⟨ sym (IsGroup.rid (isGroup H) (f (G.- g))) ⟩
  (f (G.- g) H.+ 0g H)                  ≡⟨ cong (f (G.- g) H.+_) (sym (invr H (f g))) ⟩
  (f (G.- g) H.+ (f g H.+ (H.- f g)))   ≡⟨ Group.assoc H (f (G.- g)) (f g) (H.- f g) ⟩
  ((f (G.- g) H.+ f g) H.+ (H.- f g))   ≡⟨ cong (H._+ (H.- f g)) helper ⟩
  (0g H H.+ (H.- f g))                  ≡⟨ IsGroup.lid (isGroup H) (H.- (f g))⟩
  H.- (f g) ∎
  where
  module G = Group G
  module H = Group H
  f = fun ϕ
  helper : (f (G.- g) H.+ f g) ≡ 0g H
  helper = sym (isHom ϕ (G.- g) g) ∙∙ cong f (invl G g) ∙∙ morph0→0 G H ϕ

-- ----------- Alternative notions of isomorphisms --------------
record GroupIso {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  no-eta-equality
  constructor iso
  field
    map : GroupHom G H
    inv : ⟨ H ⟩ → ⟨ G ⟩
    rightInv : section (GroupHom.fun map) inv
    leftInv : retract (GroupHom.fun map) inv

record BijectionIso {ℓ ℓ'} (A : Group {ℓ}) (B : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where
  constructor bij-iso
  field
    map' : GroupHom A B
    inj : isInjective A B map'
    surj : isSurjective A B map'

-- "Very" short exact sequences
-- i.e. an exact sequence A → B → C → D where A and D are trivial
record vSES {ℓ ℓ' ℓ'' ℓ'''} (A : Group {ℓ}) (B : Group {ℓ'}) (leftGr : Group {ℓ''}) (rightGr : Group {ℓ'''})
           : Type (ℓ-suc (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ'' ℓ''')))) where
  constructor ses
  field
    isTrivialLeft : isProp ⟨ leftGr ⟩
    isTrivialRight : isProp ⟨ rightGr ⟩

    left : GroupHom leftGr A
    right : GroupHom B rightGr
    ϕ : GroupHom A B

    Ker-ϕ⊂Im-left : (x : ⟨ A ⟩)
                  → isInKer A B ϕ x
                  → isInIm leftGr A left x
    Ker-right⊂Im-ϕ : (x : ⟨ B ⟩)
                   → isInKer B rightGr right x
                   → isInIm A B ϕ x

open BijectionIso
open GroupIso
open vSES

compGroupIso : {G : Group {ℓ}} {H : Group {ℓ₁}} {A : Group {ℓ₂}} → GroupIso G H → GroupIso H A → GroupIso G A
map (compGroupIso iso1 iso2) = compGroupHom (map iso1) (map iso2)
inv (compGroupIso iso1 iso2) = inv iso1 ∘ inv iso2
rightInv (compGroupIso iso1 iso2) a = cong (fun (map iso2)) (rightInv iso1 _) ∙ rightInv iso2 a
leftInv (compGroupIso iso1 iso2) a = cong (inv iso1) (leftInv iso2 _) ∙ leftInv iso1 a

isGroupHomInv' : {G : Group {ℓ}} {H : Group {ℓ₁}} (f : GroupIso G H) → isGroupHom H G (inv f)
isGroupHomInv' {G = G} {H = H}  f h h' = isInj-f _ _ (
  f' (g (h ⋆² h')) ≡⟨ (rightInv f) _ ⟩
  (h ⋆² h') ≡⟨ sym (cong₂ _⋆²_ (rightInv f h) (rightInv f h')) ⟩
  (f' (g h) ⋆² f' (g h')) ≡⟨ sym (isHom (map f) _ _) ⟩ -- sym (isHom (hom f) _ _) ⟩
  f' (g h ⋆¹ g h') ∎)
  where
  f' = fun (map f)
  _⋆¹_ = Group._+_ G
  _⋆²_ = Group._+_ H
  g = inv f -- invEq (eq f)

  isInj-f : (x y : ⟨ G ⟩) → f' x ≡ f' y → x ≡ y
  isInj-f x y p = sym (leftInv f _) ∙∙ cong g p ∙∙ leftInv f _

invGroupIso : {G : Group {ℓ}} {H : Group {ℓ₁}} → GroupIso G H → GroupIso H G
fun (map (invGroupIso iso1)) = inv iso1
isHom (map (invGroupIso iso1)) = isGroupHomInv' iso1
inv (invGroupIso iso1) = fun (map iso1)
rightInv (invGroupIso iso1) = leftInv iso1
leftInv (invGroupIso iso1) = rightInv iso1

dirProdGroupIso : {G : Group {ℓ}} {H : Group {ℓ₁}} {A : Group {ℓ₂}} {B : Group {ℓ₃}}
               → GroupIso G H → GroupIso A B → GroupIso (dirProd G A) (dirProd H B)
fun (map (dirProdGroupIso iso1 iso2)) prod = fun (map iso1) (fst prod) , fun (map iso2) (snd prod)
isHom (map (dirProdGroupIso iso1 iso2)) a b = ΣPathP (isHom (map iso1) (fst a) (fst b) , isHom (map iso2) (snd a) (snd b))
inv (dirProdGroupIso iso1 iso2) prod = (inv iso1) (fst prod) , (inv iso2) (snd prod)
rightInv (dirProdGroupIso iso1 iso2) a = ΣPathP (rightInv iso1 (fst a) , (rightInv iso2 (snd a)))
leftInv (dirProdGroupIso iso1 iso2) a = ΣPathP (leftInv iso1 (fst a) , (leftInv iso2 (snd a)))

GrIsoToGrEquiv : {G : Group {ℓ}} {H : Group {ℓ₂}} → GroupIso G H → GroupEquiv G H
GroupEquiv.eq (GrIsoToGrEquiv i) = isoToEquiv (iso (fun (map i)) (inv i) (rightInv i) (leftInv i))
GroupEquiv.isHom (GrIsoToGrEquiv i) = isHom (map i)

--- Proofs that BijectionIso and vSES both induce isomorphisms ---
BijectionIsoToGroupIso : {A : Group {ℓ}} {B : Group {ℓ₂}} → BijectionIso A B → GroupIso A B
BijectionIsoToGroupIso {A = A} {B = B} i = grIso
  where
  module A = Group A
  module B = Group B
  f = fun (map' i)

  helper : (b : _) → isProp (Σ[ a ∈ ⟨ A ⟩ ] f a ≡ b)
  helper _ a b =
    Σ≡Prop (λ _ → isSetCarrier B _ _)
           (fst a ≡⟨ sym (IsGroup.rid (isGroup A) (fst a)) ⟩
           ((fst a) A.+ 0g A) ≡⟨ cong ((fst a) A.+_) (sym (invl A (fst b))) ⟩
           ((fst a) A.+ ((A.- fst b) A.+ fst b)) ≡⟨ Group.assoc A _ _ _ ⟩
           (((fst a) A.+ (A.- fst b)) A.+ fst b) ≡⟨ cong (A._+ fst b) idHelper ⟩
           (0g A A.+ fst b) ≡⟨ IsGroup.lid (isGroup A) (fst b) ⟩
           fst b ∎)
    where
    idHelper : fst a A.+ (A.- fst b) ≡ 0g A
    idHelper =
      inj i _
           (isHom (map' i) (fst a) (A.- (fst b))
         ∙ (cong (f (fst a) B.+_) (morphMinus A B (map' i) (fst b))
         ∙∙ cong (B._+ (B.- f (fst b))) (snd a ∙ sym (snd b))
         ∙∙ invr B (f (fst b))))

  grIso : GroupIso A B
  map grIso = map' i
  inv grIso b = (rec (helper b) (λ a → a) (surj i b)) .fst
  rightInv grIso b = (rec (helper b) (λ a → a) (surj i b)) .snd
  leftInv grIso b j = rec (helper (f b)) (λ a → a) (propTruncIsProp (surj i (f b)) ∣ b , refl ∣ j) .fst

BijectionIsoToGroupEquiv : {A : Group {ℓ}} {B : Group {ℓ₂}} → BijectionIso A B → GroupEquiv A B
BijectionIsoToGroupEquiv i = GrIsoToGrEquiv (BijectionIsoToGroupIso i)

vSES→GroupIso : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Group {ℓ}} {B : Group {ℓ'}} (leftGr : Group {ℓ''}) (rightGr : Group {ℓ'''})
                → vSES A B leftGr rightGr
                → GroupIso A B
vSES→GroupIso {A = A} lGr rGr vses = BijectionIsoToGroupIso theIso
  where
  theIso : BijectionIso _ _
  map' theIso = vSES.ϕ vses
  inj theIso a inker = rec (isSetCarrier A _ _)
                            (λ (a , p) → sym p
                                        ∙∙ cong (fun (left vses)) (isTrivialLeft vses a _)
                                        ∙∙ morph0→0 lGr A (left vses))
                            (Ker-ϕ⊂Im-left vses a inker)
  surj theIso a = Ker-right⊂Im-ϕ vses a (isTrivialRight vses _ _)

vSES→GroupEquiv : {A : Group {ℓ}} {B : Group {ℓ₁}} (leftGr : Group {ℓ₂}) (rightGr : Group {ℓ₃})
        → vSES A B leftGr rightGr
        → GroupEquiv A B
vSES→GroupEquiv {A = A} lGr rGr vses = GrIsoToGrEquiv (vSES→GroupIso lGr rGr vses)

-- The trivial group is a unit.
lUnitGroupIso : ∀ {ℓ} {G : Group {ℓ}} → GroupEquiv (dirProd trivialGroup G) G
lUnitGroupIso =
  GrIsoToGrEquiv
    (iso (grouphom snd (λ a b → refl))
         (λ g → tt , g)
         (λ _ → refl)
         λ _ → refl)

rUnitGroupIso : ∀ {ℓ} {G : Group {ℓ}} → GroupEquiv (dirProd G trivialGroup) G
rUnitGroupIso =
  GrIsoToGrEquiv
    (iso
      (grouphom fst λ _ _ → refl)
      (λ g → g , tt)
      (λ _ → refl)
      λ _ → refl)

contrGroup≅trivialGroup : {G : Group {ℓ}} → isContr ⟨ G ⟩ → GroupEquiv G trivialGroup
GroupEquiv.eq (contrGroup≅trivialGroup contr) = isContr→≃Unit contr
GroupEquiv.isHom (contrGroup≅trivialGroup contr) _ _ = refl

max_stars_repo_name: knrafto/cubical

max_issues_repo_name: knrafto/cubical

max_forks_repo_name: knrafto/cubical


text:
module Relations where

-- Imports

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-comm)

-- Defining relations

data _≤_ : ℕ → ℕ → Set where

  z≤n : ∀ {n : ℕ}
      --------
    → zero ≤ n

  s≤s : ∀ {m n : ℕ}
    → m ≤ n
      -------------
    → suc m ≤ suc n

_ : 2 ≤ 4
_ = s≤s (s≤s z≤n)

-- Implicit arguments

_ : 2 ≤ 4
_ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2}))

_ : 2 ≤ 4
_ = s≤s {m = 1} {n = 3} (s≤s {m = 0} {n = 2} (z≤n {n = 2}))

_ : 2 ≤ 4
_ = s≤s {n = 3} (s≤s {n = 2} z≤n)

-- Precedence

infix 4 _≤_

-- Inversion

inv-s≤s : ∀ {m n : ℕ}
  → suc m ≤ suc n
    -------------
  → m ≤ n
inv-s≤s (s≤s m≤n) = m≤n

inv-z≤n : ∀ {m : ℕ}
  → m ≤ zero
    --------
  → m ≡ zero
inv-z≤n z≤n = refl

-- Reflexivity (反射律)

≤-refl : ∀ {n : ℕ}
    -----
  → n ≤ n
≤-refl {zero}  = z≤n
≤-refl {suc n} = s≤s ≤-refl

-- Transitivity (推移律)

≤-trans : ∀ {m n p : ℕ}
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans z≤n       _         = z≤n
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)

≤-trans′ : ∀ (m n p : ℕ)
  → m ≤ n
  → n ≤ p
    -----
  → m ≤ p
≤-trans′ zero    _       _       z≤n       _         = z≤n
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans′ m n p m≤n n≤p)

-- Anti-symmetry (非対称律)

≤-antisym : ∀ {m n : ℕ}
  → m ≤ n
  → n ≤ m
    -----
  → m ≡ n
≤-antisym z≤n       z≤n       = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)

-- Total (全順序)

data Total (m n : ℕ) : Set where

  forward :
      m ≤ n
      ---------
    → Total m n

  flipped :
      n ≤ m
      ---------
    → Total m n

data Total′ : ℕ → ℕ → Set where

  forward′ : ∀ {m n : ℕ}
    → m ≤ n
      ----------
    → Total′ m n

  flipped′ : ∀ {m n : ℕ}
    → n ≤ m
      ----------
    → Total′ m n

≤-total : ∀ (m n : ℕ) → Total m n
≤-total zero    n                        = forward z≤n
≤-total (suc m) zero                     = flipped z≤n
≤-total (suc m) (suc n) with ≤-total m n
...                        | forward m≤n = forward (s≤s m≤n)
...                        | flipped n≤m = flipped (s≤s n≤m)

≤-total′ : ∀ (m n : ℕ) → Total m n
≤-total′ zero    n       = forward z≤n
≤-total′ (suc m) zero    = flipped z≤n
≤-total′ (suc m) (suc n) = helper (≤-total′ m n)
  where
  helper : Total m n → Total (suc m) (suc n)
  helper (forward m≤n) = forward (s≤s m≤n)
  helper (flipped n≤m) = flipped (s≤s n≤m)

≤-total″ : ∀ (m n : ℕ) → Total m n
≤-total″ m       zero                      = flipped z≤n
≤-total″ zero    (suc n)                   = forward z≤n
≤-total″ (suc m) (suc n) with ≤-total″ m n
...                        | forward m≤n   = forward (s≤s m≤n)
...                        | flipped n≤m   = flipped (s≤s n≤m)

-- Monotonicity (単調性)

+-monoʳ-≤ : ∀ (n p q : ℕ)
  → p ≤ q
    -------------
  → n + p ≤ n + q
+-monoʳ-≤ zero    p q p≤q = p≤q
+-monoʳ-≤ (suc n) p q p≤q = s≤s (+-monoʳ-≤ n p q p≤q)

+-monoˡ-≤ : ∀ (m n p : ℕ)
  → m ≤ n
    -------------
  → m + p ≤ n + p
+-monoˡ-≤ m n p m≤n  rewrite +-comm m p | +-comm n p  = +-monoʳ-≤ p m n m≤n

+-mono-≤ : ∀ (m n p q : ℕ)
  → m ≤ n
  → p ≤ q
    -------------
  → m + p ≤ n + q
+-mono-≤ m n p q m≤n p≤q  =  ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)

-- Strict inequality

infix 4 _<_

data _<_ : ℕ → ℕ → Set where

  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

-- Even and odd

data even : ℕ → Set
data odd  : ℕ → Set

data even where

  zero :
      ---------
      even zero

  suc  : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where

  suc   : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

e+e≡e : ∀ {m n : ℕ}
  → even m
  → even n
    ------------
  → even (m + n)

o+e≡o : ∀ {m n : ℕ}
  → odd m
  → even n
    -----------
  → odd (m + n)

e+e≡e zero     en = en
e+e≡e (suc om) en = suc (o+e≡o om en)

o+e≡o (suc em) en = suc (e+e≡e em en)

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
module Data.Nat.Instance where

open import Agda.Builtin.Nat
open import Class.Equality
open import Class.Monoid
open import Class.Show
open import Data.Char
open import Data.List
open import Data.Nat renaming (_≟_ to _≟ℕ_; _+_ to _+ℕ_)
open import Data.String
open import Function

private

  postulate
    primShowNat : ℕ -> List Char

  {-# COMPILE GHC primShowNat = show #-}

  showNat : ℕ -> String
  showNat = fromList ∘ primShowNat

instance
  Eq-ℕ : Eq ℕ
  Eq-ℕ = record { _≟_ = _≟ℕ_ }

  EqB-ℕ : EqB ℕ
  EqB-ℕ = record { _≣_ = Agda.Builtin.Nat._==_ }

  ℕ-Monoid : Monoid ℕ
  ℕ-Monoid = record { mzero = zero ; _+_ = _+ℕ_ }

  Show-ℕ : Show ℕ
  Show-ℕ = record { show = showNat }

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
open import Data.Product using ( _×_ ; _,_ ; swap )
open import Data.Sum using ( inj₁ ; inj₂ )
open import Relation.Nullary using ( ¬_ ; yes ; no )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox using ( ABox ; ε ; _,_ ; _∼_ ; _∈₁_ ; _∈₂_ )
open import Web.Semantic.DL.ABox.Interp using
  ( Interp ; ⌊_⌋ ; ind ; ind⁻¹ ; Surjective ; surj✓ )
open import Web.Semantic.DL.ABox.Interp.Morphism using
  ( _≲_ ; _≃_ ; _,_ ; ≲⌊_⌋ ; ≲-resp-ind )
open import Web.Semantic.DL.ABox.Interp.Meet using
  ( meet ; meet-lb ; meet-glb ; meet-uniq ; meet-surj )
open import Web.Semantic.DL.ABox.Model using ( _⊨a_ )
open import Web.Semantic.DL.Concept using
  ( Concept ; ⟨_⟩ ; ¬⟨_⟩ ; ⊤ ; ⊥ ; _⊔_ ; _⊓_ ; ∀[_]_ ; ∃⟨_⟩_ ; ≤1 ; >1 ; neg )
open import Web.Semantic.DL.Concept.Model using
  ( _⟦_⟧₁ ; neg-sound ; neg-complete )
open import Web.Semantic.DL.Integrity.Closed using
  ( Mediated₀ ; Initial₀ ; sur_⊨₀_ ; _,_ )
open import Web.Semantic.DL.Integrity.Closed.Alternate using
  ( _⊫_∼_ ; _⊫_∈₁_ ; _⊫_∈₂_ ; _⊫t_ ; _⊫a_ ; _⊫k_
  ; eq ; rel ; rev ; +atom ; -atom ; top ; inj₁ ; inj₂
  ; all ; ex ; uniq ; ¬uniq ; cn ; rl ; dis ; ref ; irr ; tra ; ε ; _,_ )
open import Web.Semantic.DL.KB using ( KB ; tbox ; abox )
open import Web.Semantic.DL.KB.Model using ( _⊨_ ; Interps ; ⊨-resp-≃ )
open import Web.Semantic.DL.Role using ( Role ; ⟨_⟩ ; ⟨_⟩⁻¹ )
open import Web.Semantic.DL.Role.Model using ( _⟦_⟧₂ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using
  ( TBox ; ε ; _,_ ; _⊑₁_ ; _⊑₂_ ; Dis ; Ref ; Irr ; Tra )
open import Web.Semantic.DL.TBox.Interp using ( _⊨_≈_ ; ≈-sym ; ≈-trans )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( ≲-resp-≈ ; iso )
open import Web.Semantic.DL.TBox.Model using ( _⊨t_ )
open import Web.Semantic.Util using
  ( ExclMiddle ; ExclMiddle₁ ; smaller-excl-middle ; is! ; is✓ ; tt ; elim )

module Web.Semantic.DL.Integrity.Closed.Properties
  (excl-middle₁ : ExclMiddle₁) {Σ : Signature} {X : Set} where

-- The two definitions of closed-world integrity coincide for surjective interpretations.
-- Note that this requires excluded middle, as the alternate definition assumes a classical logic,
-- for example interpreting C ⊑ D as (¬ C ⊔ D) being a tautology.

min : KB Σ X → Interp Σ X
min K = meet excl-middle₁ (Interps K)

excl-middle : ExclMiddle
excl-middle = smaller-excl-middle excl-middle₁

sound∼ : ∀ K x y → (K ⊫ x ∼ y) → (⌊ min K ⌋ ⊨ x ≈ y)
sound∼ K x y (eq K⊫x∼y) = is! K⊫x∼y

complete∼ : ∀ K x y → (⌊ min K ⌋ ⊨ x ≈ y) → (K ⊫ x ∼ y)
complete∼ K x y x≈y = eq (is✓ x≈y)

sound₂ : ∀ K R xy → (K ⊫ xy ∈₂ R) → (xy ∈ ⌊ min K ⌋ ⟦ R ⟧₂)
sound₂ K ⟨ r ⟩   (x , y) (rel K⊫xy∈r) = is! K⊫xy∈r
sound₂ K ⟨ r ⟩⁻¹ (x , y) (rev K⊫yx∈r) = is! K⊫yx∈r

complete₂ : ∀ K R xy → (xy ∈ ⌊ min K ⌋ ⟦ R ⟧₂) → (K ⊫ xy ∈₂ R)
complete₂ K ⟨ r ⟩   (x , y) xy∈⟦r⟧ = rel (is✓ xy∈⟦r⟧)
complete₂ K ⟨ r ⟩⁻¹ (x , y) yx∈⟦r⟧ = rev (is✓ yx∈⟦r⟧)

sound₁ : ∀ K C x → (K ⊫ x ∈₁ C) → (x ∈ ⌊ min K ⌋ ⟦ C ⟧₁)
sound₁ K ⟨ c ⟩ x (+atom K⊨x∈c) =
  is! K⊨x∈c
sound₁ K ¬⟨ c ⟩ x (-atom K⊭x∈c) =
  λ x∈⟦c⟧ → K⊭x∈c (is✓ x∈⟦c⟧)
sound₁ K ⊤ x top = tt
sound₁ K ⊥ x ()
sound₁ K (C ⊓ D) x (K⊫x∈C , K⊫x∈D) =
  (sound₁ K C x K⊫x∈C , sound₁ K D x K⊫x∈D)
sound₁ K (C ⊔ D) x (inj₁ K⊫x∈C) =
  inj₁ (sound₁ K C x K⊫x∈C)
sound₁ K (C ⊔ D) x (inj₂ K⊫x∈D) =
  inj₂ (sound₁ K D x K⊫x∈D)
sound₁ K (∀[ R ] C) x (all K⊫x∈∀RC) =
  λ y xy∈⟦R⟧ → sound₁ K C y (K⊫x∈∀RC y (complete₂ K R _ xy∈⟦R⟧))
sound₁ K (∃⟨ R ⟩ C) x (ex y K⊫xy∈R K⊫y∈C) =
  (y , sound₂ K R _ K⊫xy∈R , sound₁ K C y K⊫y∈C)
sound₁ K (≤1 R) x (uniq K⊫x∈≤1R) =
  λ y z xy∈⟦R⟧ xz∈⟦R⟧ → sound∼ K y z
    (K⊫x∈≤1R y z (complete₂ K R _ xy∈⟦R⟧) (complete₂ K R _ xz∈⟦R⟧))
sound₁ K (>1 R) x (¬uniq y z K⊫xy∈R K⊫xz∈R K⊯y∼z) =
  ( y , z , sound₂ K R _ K⊫xy∈R , sound₂ K R _ K⊫xz∈R
  , λ y≈z → K⊯y∼z (complete∼ K y z y≈z) )

complete₁ : ∀ K C x → (x ∈ ⌊ min K ⌋ ⟦ C ⟧₁) → (K ⊫ x ∈₁ C)
complete₁ K ⟨ c ⟩ x x∈⟦c⟧ =
  +atom (is✓ x∈⟦c⟧)
complete₁ K ¬⟨ c ⟩ x x∉⟦c⟧ =
  -atom (λ K⊫x∈c → x∉⟦c⟧ (is! K⊫x∈c))
complete₁ K ⊤ x x∈⟦C⟧ =
  top
complete₁ K ⊥ x ()
complete₁ K (C ⊓ D) x (x∈⟦C⟧ , x∈⟦D⟧) =
  (complete₁ K C x x∈⟦C⟧ , complete₁ K D x x∈⟦D⟧)
complete₁ K (C ⊔ D) x (inj₁ x∈⟦C⟧) =
  inj₁ (complete₁ K C x x∈⟦C⟧)
complete₁ K (C ⊔ D) x (inj₂ x∈⟦D⟧) =
  inj₂ (complete₁ K D x x∈⟦D⟧)
complete₁ K (∀[ R ] C) x x∈⟦∀RC⟧ =
  all (λ y K⊫xy∈R → complete₁ K C y (x∈⟦∀RC⟧ y (sound₂ K R _ K⊫xy∈R)))
complete₁ K (∃⟨ R ⟩ C) x (y , xy∈⟦R⟧ , y∈⟦C⟧) =
  ex y (complete₂ K R (x , y) xy∈⟦R⟧) (complete₁ K C y y∈⟦C⟧)
complete₁ K (≤1 R) x x∈⟦≤1R⟧ =
  uniq (λ y z K⊫xy∈R K⊫xz∈R → complete∼ K y z
    (x∈⟦≤1R⟧ y z (sound₂ K R _ K⊫xy∈R) (sound₂ K R _ K⊫xz∈R)))
complete₁ K (>1 R) x (y , z , xy∈⟦R⟧ , xz∈⟦R⟧ , y≉z) =
  ¬uniq y z (complete₂ K R _ xy∈⟦R⟧) (complete₂ K R _ xz∈⟦R⟧)
    (λ K⊫y∼z → y≉z (sound∼ K y z K⊫y∼z))

⊫-impl-min⊨ : ∀ K L → (K ⊫k L) → (min K ⊨ L)
⊫-impl-min⊨ K L (K⊫T , K⊫A) = ( J⊨T K⊫T , J⊨A K⊫A ) where

  J : Interp Σ X
  J = min K

  J⊨T : ∀ {T} → (K ⊫t T) → (⌊ J ⌋ ⊨t T)
  J⊨T ε = tt
  J⊨T (K⊫T , K⊫U) = (J⊨T K⊫T , J⊨T K⊫U)
  J⊨T (rl Q R K⊫Q⊑R) =
    λ {xy} xy∈⟦Q⟧ → sound₂ K R xy (K⊫Q⊑R xy (complete₂ K Q xy xy∈⟦Q⟧))
  J⊨T (cn C D K⊫C⊑D) = λ {x} → lemma x (K⊫C⊑D x) where

    lemma : ∀ x → (K ⊫ x ∈₁ (neg C ⊔ D)) →
      (x ∈ ⌊ J ⌋ ⟦ C ⟧₁) → (x ∈ ⌊ J ⌋ ⟦ D ⟧₁)
    lemma x (inj₁ K⊫x∈¬C) x∈⟦C⟧ =
      elim (neg-sound ⌊ J ⌋ {x} C (sound₁ K (neg C) x K⊫x∈¬C) x∈⟦C⟧)
    lemma x (inj₂ K⊫x∈D) x∈⟦C⟧ =
      sound₁ K D x K⊫x∈D

  J⊨T (dis Q R K⊫DisQR) = λ {xy} xy∈⟦Q⟧ xy∈⟦R⟧ →
    K⊫DisQR xy (complete₂ K Q xy xy∈⟦Q⟧) (complete₂ K R xy xy∈⟦R⟧)
  J⊨T (ref R K⊫RefR) = λ x → sound₂ K R (x , x) (K⊫RefR x)
  J⊨T (irr R K⊫IrrR) = λ x xx∈⟦R⟧ → K⊫IrrR x (complete₂ K R (x , x) xx∈⟦R⟧)
  J⊨T (tra R K⊫TraR) = λ {x} {y} {z} xy∈⟦R⟧ yz∈⟦R⟧ →
    sound₂ K R (x , z) (K⊫TraR x y z
      (complete₂ K R (x , y) xy∈⟦R⟧) (complete₂ K R (y , z) yz∈⟦R⟧))

  J⊨A : ∀ {A} → (K ⊫a A) → (J ⊨a A)
  J⊨A ε = tt
  J⊨A (K⊫A , K⊫B) = (J⊨A K⊫A , J⊨A K⊫B)
  J⊨A (eq x y K⊫x∼y) = sound∼ K x y K⊫x∼y
  J⊨A (rl (x , y) r K⊫xy∈r) = sound₂ K ⟨ r ⟩ (x , y) K⊫xy∈r
  J⊨A (cn x c K⊫x∈c) = sound₁ K ⟨ c ⟩ x K⊫x∈c

min⊨-impl-⊫ : ∀ K L → (min K ⊨ L) → (K ⊫k L)
min⊨-impl-⊫ K L (J⊨T , J⊨A) =
  ( K⊫T (tbox L) J⊨T ,  K⊫A (abox L) J⊨A ) where

  J : Interp Σ X
  J = min K

  K⊫T : ∀ T → (⌊ J ⌋ ⊨t T) → (K ⊫t T)
  K⊫T ε J⊨ε = ε
  K⊫T (T , U) (J⊨T , J⊨U) = (K⊫T T J⊨T , K⊫T U J⊨U)
  K⊫T (Q ⊑₂ R) J⊨Q⊑R =
    rl Q R (λ xy K⊫xy∈Q → complete₂ K R xy (J⊨Q⊑R (sound₂ K Q xy K⊫xy∈Q)))
  K⊫T (C ⊑₁ D) J⊨C⊑D = cn C D lemma where

    lemma : ∀ x → (K ⊫ x ∈₁ neg C ⊔ D)
    lemma x with excl-middle (x ∈ ⌊ J ⌋ ⟦ C ⟧₁)
    lemma x | yes x∈⟦C⟧ =
      inj₂ (complete₁ K D x (J⊨C⊑D x∈⟦C⟧))
    lemma x | no  x∉⟦C⟧ =
      inj₁ (complete₁ K (neg C) x (neg-complete excl-middle ⌊ J ⌋ C x∉⟦C⟧))

  K⊫T (Dis Q R) J⊨DisQR =
    dis Q R (λ xy K⊫xy∈Q K⊫xy∈R →
      J⊨DisQR (sound₂ K Q xy K⊫xy∈Q) (sound₂ K R xy K⊫xy∈R))
  K⊫T (Ref R) J⊨RefR =
    ref R (λ x → complete₂ K R (x , x) (J⊨RefR x))
  K⊫T (Irr R) J⊨IrrR =
    irr R (λ x K⊫xx∈R → J⊨IrrR x (sound₂ K R (x , x) K⊫xx∈R))
  K⊫T (Tra R) J⊨TrR =
    tra R (λ x y z K⊫xy∈R K⊫yz∈R →
      complete₂ K R (x , z) (J⊨TrR
        (sound₂ K R (x , y) K⊫xy∈R) (sound₂ K R (y , z) K⊫yz∈R)))

  K⊫A : ∀ A → (J ⊨a A) → (K ⊫a A)
  K⊫A ε J⊨ε = ε
  K⊫A (A , B) (J⊨A , J⊨B) = (K⊫A A J⊨A , K⊫A B J⊨B)
  K⊫A (x ∼ y) x≈y = eq x y (complete∼ K x y x≈y)
  K⊫A (x ∈₁ c) x∈⟦c⟧ = cn x c (complete₁ K ⟨ c ⟩ x x∈⟦c⟧)
  K⊫A ((x , y) ∈₂ r) xy∈⟦r⟧ = rl (x , y) r (complete₂ K ⟨ r ⟩ (x , y) xy∈⟦r⟧)

min-med : ∀ (K : KB Σ X) J → (J ⊨ K) → Mediated₀ (min K) J
min-med K J J⊨K = (meet-lb excl-middle₁ (Interps K) J J⊨K , meet-uniq excl-middle₁ (Interps K) J J⊨K)

min-init : ∀ (K : KB Σ X) → (K ⊫k K) → (min K ∈ Initial₀ K)
min-init K K⊫K = ( ⊫-impl-min⊨ K K K⊫K , min-med K)

min-uniq : ∀ (I : Interp Σ X) (K : KB Σ X) → (I ∈ Surjective) → (I ∈ Initial₀ K) → (I ≃ min K)
min-uniq I K I∈Surj (I⊨K , I-med) =
  ( iso
      ≲⌊ meet-glb excl-middle₁ (Interps K) I I∈Surj lemma₁ ⌋
      ≲⌊ meet-lb excl-middle₁ (Interps K) I I⊨K ⌋
      (λ x → ≈-sym ⌊ I ⌋ (surj✓ I∈Surj x))
      (λ x → is! (lemma₂ x))
  , λ x → is! (lemma₂ x)) where

  lemma₁ : ∀ J J⊨K → I ≲ J
  lemma₁ J J⊨K with I-med J J⊨K
  lemma₁ J J⊨K | (I≲J , I≲J-uniq) = I≲J

  lemma₂ : ∀ x J J⊨K → ⌊ J ⌋ ⊨ ind J (ind⁻¹ I∈Surj (ind I x)) ≈ ind J x
  lemma₂ x J J⊨K =
    ≈-trans ⌊ J ⌋ (≈-sym ⌊ J ⌋ (≲-resp-ind (lemma₁ J J⊨K) (ind⁻¹ I∈Surj (ind I x))))
      (≈-trans ⌊ J ⌋ (≲-resp-≈ ≲⌊ lemma₁ J J⊨K ⌋ (≈-sym ⌊ I ⌋ (surj✓ I∈Surj (ind I x))))
        (≲-resp-ind (lemma₁ J J⊨K) x))

⊫-impl-⊨₀ : ∀ (KB₁ KB₂ : KB Σ X) → (KB₁ ⊫k KB₁) → (KB₁ ⊫k KB₂) → (sur KB₁ ⊨₀ KB₂)
⊫-impl-⊨₀ KB₁ KB₂ KB₁⊫KB₁ KB₁⊫KB₂ =
  ( min KB₁
  , meet-surj excl-middle₁ (Interps KB₁)
  , min-init KB₁ KB₁⊫KB₁
  , ⊫-impl-min⊨ KB₁ KB₂ KB₁⊫KB₂ )

⊨₀-impl-⊫₁ : ∀ (KB₁ KB₂ : KB Σ X) → (sur KB₁ ⊨₀ KB₂) → (KB₁ ⊫k KB₁)
⊨₀-impl-⊫₁ KB₁ KB₂ (I , I∈Surj , (I⊨KB₁ , I-med) , I⊨KB₂) =
  min⊨-impl-⊫ KB₁ KB₁ (⊨-resp-≃ (min-uniq I KB₁ I∈Surj (I⊨KB₁ , I-med)) KB₁ I⊨KB₁)

⊨₀-impl-⊫₂ : ∀ (KB₁ KB₂ : KB Σ X) → (sur KB₁ ⊨₀ KB₂) → (KB₁ ⊫k KB₂)
⊨₀-impl-⊫₂ KB₁ KB₂ (I , I∈Surj , I-init , I⊨KB₂) =
  min⊨-impl-⊫ KB₁ KB₂ (⊨-resp-≃ (min-uniq I KB₁ I∈Surj I-init) KB₂ I⊨KB₂)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


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

module Fragment.Examples.CSemigroup.Types where

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
-- This document shows how to encode GADTs using `IFix`.

{-# OPTIONS --type-in-type #-}

module ScottVec where

-- The kind of church-encoded type-level natural numbers.
Nat = (Set -> Set) -> Set -> Set

zero : Nat
zero = λ f z -> z

suc : Nat -> Nat
suc = λ n f z -> f (n f z)

plus : Nat -> Nat -> Nat
plus = λ n m f z -> n f (m f z)

-- Our old friend.
{-# NO_POSITIVITY_CHECK #-}
record IFix {I : Set} (F : (I -> Set) -> I -> Set) (i : I) : Set where
  constructor wrap
  field unwrap : F (IFix F) i
open IFix

-- Scott-encoded vectors (a vector is a list with statically-known length).

-- As usually the pattern vector of a Scott-encoded data type encodes pattern-matching.
VecF : Set -> (Nat -> Set) -> Nat -> Set
VecF
  = λ A Rec n
  -> (R : Nat -> Set)                  -- The type of the result depends on the vector's length.
  -> (∀ p -> A -> Rec p -> R (suc p))  -- The encoded `cons` constructor.
  -> R zero                            -- The encoded `nil` constructor.
  -> R n

Vec : Set -> Nat -> Set
Vec = λ (A : Set) -> IFix (VecF A)

nil : ∀ A -> Vec A zero
nil = λ A -> wrap λ R f z -> z

cons : ∀ A n -> A -> Vec A n -> Vec A (suc n)
cons = λ A n x xs -> wrap λ R f z -> f n x xs

open import Data.Empty
open import Data.Unit.Base
open import Data.Nat.Base using (ℕ; _+_)

-- Type-safe `head`.
head : ∀ A n -> Vec A (suc n) -> A
head A n xs =
  unwrap
    xs
    (λ p -> p (λ _ -> A) ⊤)  -- `p (λ _ -> A) ⊤` returns `A` when `p` is `suc p'` for some `p'`
                             -- and `⊤` when `p` is `zero`
    (λ p x xs' -> x)         -- In the `cons` case `suc p (λ _ -> A) ⊤` reduces to `A`,
                             -- hence we return the list element of type `A`.
    tt                       -- In the `nil` case `zero (λ _ -> A) ⊤` reduces to `⊤`,
                             -- hence we return the only value of that type.

{- Note [Type-safe `tail`]
It's not obvious if type-safe `tail` can be implemented with this setup. This is because even
though `Vec` is Scott-encoded, the type-level natural are Church-encoded (obviously we could
have Scott-encoded type-level naturals in Agda just as well, but not in Zerepoch Core), which
makes `pred` hard, which makes `tail` non-trivial.

I did try using Scott-encoded naturals in Agda, that makes `tail` even more straightforward
than `head`:

    tail : ∀ A n -> Vec A (suc n) -> Vec A n
    tail A n xs =
      unwrap
        xs
        (λ p -> ((B : ℕ -> Set) -> B (pred p) -> B n) -> Vec A n)
        (λ p x xs' coe -> coe (Vec A) xs')
        (λ coe -> coe (Vec A) (nil A))
        (λ B x -> x)
-}

-- Here we pattern-match on `xs` and if it's non-empty, i.e. of type `Vec ℕ (suc p)` for some `p`,
-- then we also get access to a coercion function that allows us to coerce the second list from
-- `Vec ℕ n` to the same `Vec ℕ (suc p)` and call the type-safe `head` over it.
-- Note that we don't even need to encode the `n ~ suc p` and `n ~ zero` equality constraints in
-- the definition of `vecF` and can recover coercions along those constraints by adding the
-- `Vec ℕ n -> Vec ℕ p` argument to the motive.
sumHeadsOr0 : ∀ n -> Vec ℕ n -> Vec ℕ n -> ℕ
sumHeadsOr0 n xs ys =
  unwrap
    xs
    (λ p -> (Vec ℕ n -> Vec ℕ p) -> ℕ)
    (λ p i _ coe -> i + head ℕ p (coe ys))
    (λ _ -> 0)
    (λ x -> x)

max_stars_repo_name: Quantum-One-DLT/zerepoch

max_issues_repo_name: Quantum-One-DLT/zerepoch

max_forks_repo_name: Quantum-One-DLT/zerepoch


text:
module EqTest where

import Common.Level

open import Common.Maybe
open import Common.Equality

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

_≟_ : (x y : ℕ) -> Maybe (x ≡ y)
suc m  ≟ suc n with m ≟ n
suc .n ≟ suc n |    just refl = just refl
suc m  ≟ suc n |    nothing   = nothing
zero   ≟ suc _ = nothing
suc m  ≟ zero  = nothing
zero   ≟ zero  = just refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2012-09-26 disable projection-likeness for recursive functions
-- {-# OPTIONS -v tc.proj.like:100 #-}
module ProjectionLikeRecursive where

open import Common.Prelude
open import Common.Equality

if_then_else_ : {A : Set} → Bool → A → A → A
if true then t else e = t
if false then t else e = e

infixr 5 _∷_ _∷′_

data Vec (n : Nat) : Set where
  []  : {p : n ≡ 0} → Vec n
  _∷_ : {m : Nat}{p : n ≡ suc m} → Nat → Vec m → Vec n

null : {n : Nat} → Vec n → Bool
null [] = true
null xs = false

-- last is considered projection-like
last : (n : Nat) → Vec n → Nat
-- last 0 xs = zero  --restoring this line removes proj.-likeness and passes the file
last n [] = zero
last n (x ∷ xs) = if (null xs) then x else last _ xs
-- breaks if projection-like translation is not removing the _ in the rec. call

[]′ : Vec zero
[]′ = [] {p = refl}

_∷′_ : {n : Nat} → Nat → Vec n → Vec (suc n)
x ∷′ xs = _∷_ {p = refl} x xs

three = last 3 (1 ∷′ 2 ∷′ 3 ∷′ []′)

test : three ≡ 3
test = refl
-- Error: Incomplete pattern matching
-- when checking that the expression refl has type three ≡ 3

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module HasNegation where

record HasNegation (A : Set) : Set
 where
  field
    ~ : A → A

open HasNegation ⦃ … ⦄ public

{-# DISPLAY HasNegation.~ _ = ~ #-}


text:
{-
Stream transducers have been described in:

  N. Ghani, P. Hancock, and D. Pattinson,
  Continuous functions on final coalgebras.
  In Proc. CMCS 2006, Electr. Notes in Theoret. Comp. Sci., 2006.

They have been modelled by mixed equi-(co)inductive sized types in

  A. Abel,
  Mixed Inductive/Coinductive Types and Strong Normalization.
  In APLAS 2007, LNCS 4807.

Here we model them by mutual data/codata and mixed recursion/corecursion.
Cf. examples/Termination/StreamProc.agda
 -}

module StreamEating where

open import Common.Coinduction

-- Infinite streams.

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

-- A stream processor SP A B consumes elements of A and produces
-- elements of B. It can only consume a finite number of A's before
-- producing a B.

data SP (A B : Set) : Set where
  get : (f : A → SP A B) → SP A B
  put : (b : B) (sp : ∞ (SP A B)) → SP A B

-- eat is defined by (outer) corecursion into Stream B
-- and an inner recursion on SP A B
eat : ∀ {A B} → SP A B → Stream A → Stream B
eat (get f)    (a ∷ as) = eat (f a) (♭ as)
eat (put b sp) as       = b ∷ (♯ eat (♭ sp) as)

_∘_ : ∀ {A B C} → SP B C → SP A B → SP A C
get f₁    ∘ put x sp₂ = f₁ x ∘ ♭ sp₂
put x sp₁ ∘ sp₂       = put x (♯ (♭ sp₁ ∘ sp₂))
sp₁       ∘ get f₂    = get (λ x → sp₁ ∘ f₂ x)


text:
module Properties where

import Properties.Contradiction
import Properties.Dec
import Properties.Equality
import Properties.Step
import Properties.Remember


text:
{-# OPTIONS --enable-prop #-}

data Squash {ℓ} (A : Set ℓ) : Prop ℓ where
  squash : A → Squash A

squash-elim : ∀ {ℓ₁ ℓ₂} (A : Set ℓ₁) (P : Prop ℓ₂)
            → (A → P) → Squash A → P
squash-elim A P f (squash x) = f x

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
-- Some proposition constructors.

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

module Tools.Nullary where

open import Tools.Empty

-- Negation.

infix 3 ¬_

¬_ : Set → Set
¬ P = P → ⊥

-- Decidable propositions.

data Dec (P : Set) : Set where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

-- If A and B are logically equivalent, then so are Dec A and Dec B.

map : ∀ {A B} → (A → B) → (B → A) → Dec A → Dec B
map f g (yes p) = yes (f p)
map f g (no ¬p) = no (λ x → ¬p (g x))

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
------------------------------------------------------------------------
-- Finite maps with indexed keys and values, based on AVL trees
------------------------------------------------------------------------

open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Product as Prod hiding (map)

module Data.AVL.IndexedMap
         {Index : Set} {Key : Index → Set} {_≈_ _<_ : Rel (∃ Key)}
         (isOrderedKeySet : IsStrictTotalOrder _≈_ _<_)
         -- Equal keys must have equal indices.
         (indicesEqual : _≈_ =[ proj₁ ]⇒ _≡_)
         (Value : Index → Set)
         where

import Data.AVL
open import Data.Function
open import Data.Maybe as Maybe
open import Data.Bool
open import Data.List
open import Category.Functor
open RawFunctor Maybe.functor

-- Key/value pairs.

KV : Set
KV = ∃ λ i → Key i × Value i

-- Conversions.

private

  fromKV : KV → Σ (∃ Key) λ ik → Value (proj₁ ik)
  fromKV (i , k , v) = ((i , k) , v)

  toKV : Σ (∃ Key) (λ ik → Value (proj₁ ik)) → KV
  toKV ((i , k) , v) = (i , k , v)

private

  Order : StrictTotalOrder
  Order = record { isStrictTotalOrder = isOrderedKeySet }

-- The map type.

private
  open module AVL = Data.AVL Order (λ ik → Value (proj₁ ik))
    public using () renaming (Tree to Map)

-- Repackaged functions.

empty : Map
empty = AVL.empty

singleton : ∀ {i} → Key i → Value i → Map
singleton k v = AVL.singleton (, k) v

insert : ∀ {i} → Key i → Value i → Map → Map
insert k v = AVL.insert (, k) v

delete : ∀ {i} → Key i → Map → Map
delete k = AVL.delete (, k)

lookup : ∀ {i} → Key i → Map → Maybe (Value i)
lookup k m with AVL.lookup (_ , k) m
... | nothing                    = nothing
... | just ((i′ , k′) , v′ , eq) with indicesEqual eq
...   | refl = just v′

_∈?_ : ∀ {i} → Key i → Map → Bool
_∈?_ k = AVL._∈?_ (, k)

headTail : Map → Maybe (KV × Map)
headTail m = Prod.map toKV id <$> AVL.headTail m

initLast : Map → Maybe (Map × KV)
initLast m = Prod.map id toKV <$> AVL.initLast m

fromList : List KV → Map
fromList = AVL.fromList ∘ map fromKV

toList : Map → List KV
toList = map toKV ∘ AVL.toList

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- A small prelude
------------------------------------------------------------------------

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

-- Note that parts of Agda's standard library make use of the K rule.

module Prelude where

------------------------------------------------------------------------
-- Universes

-- Basic type universes and universe levels.

open import Agda.Primitive public
  renaming (Set to Type)
  using (Prop; Level; _⊔_; lzero; lsuc)

private
  variable
    a b c ℓ p                       : Level
    @0 A A₁ A₂ B B₁ B₂ C D Whatever : Type a
    @0 P Q R                        : A → Type p

-- Lifting.

record ↑ ℓ (A : Type a) : Type (a ⊔ ℓ) where
  constructor lift
  field lower : A

open ↑ public

------------------------------------------------------------------------
-- Strings

open import Agda.Builtin.String public using (String)

------------------------------------------------------------------------
-- The unit type

-- A variant of the unit type with η-equality.

open import Agda.Builtin.Unit public using (⊤; tt)

-- A variant without η-equality.

data Unit : Type where
  unit : Unit

-- Block s is used to block unfolding (for performance reasons). The
-- string can be used to indicate what it is that is blocked.

Block : String → Type
Block _ = Unit

pattern ⊠ = unit

-- A function that can be used to locally block something.

block : (Unit → A) → A
block f = f ⊠

-- A function that can be used to unblock something.

unblock : (b : Unit) (@0 P : Unit → Type p) → P ⊠ → P b
unblock ⊠ _ p = p

------------------------------------------------------------------------
-- The empty type

data ⊥ {ℓ} : Type ℓ where

⊥-elim : ⊥ {ℓ = ℓ} → Whatever
⊥-elim ()

-- A version of the empty type that is not universe-polymorphic.

⊥₀ : Type
⊥₀ = ⊥

-- Negation.

infix 3 ¬_

¬_ : Type ℓ → Type ℓ
¬ P = P → ⊥₀

------------------------------------------------------------------------
-- Natural numbers

open import Agda.Builtin.Nat public
  using (zero; suc; _+_; _*_)
  renaming (Nat to ℕ; _-_ to _∸_)

-- Dependent eliminator.

ℕ-rec : P 0 → (∀ n → P n → P (suc n)) → ∀ n → P n
ℕ-rec z s zero    = z
ℕ-rec z s (suc n) = s n (ℕ-rec z s n)

-- A non-recursive variant of ℕ-rec.

ℕ-case : P 0 → (∀ n → P (suc n)) → ∀ n → P n
ℕ-case z s = ℕ-rec z (λ n _ → s n)

-- Exponentiation.

infixr 8 _^_

_^_ : ℕ → ℕ → ℕ
m ^ zero  = 1
m ^ suc n = m * m ^ n

-- Factorial.

infix 9 _!

_! : ℕ → ℕ
zero  ! = 1
suc n ! = suc n * n !

-- Translation from natural numbers to levels.

# : ℕ → Level
# zero    = lzero
# (suc n) = lsuc (# n)

------------------------------------------------------------------------
-- Combinators defined using only abstraction and application

infixr 9 _∘_
infixl 1 _on_
infixr 0 _$_

-- The identity function.

id : A → A
id x = x

-- Composition.

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

-- "Equational" reasoning combinators.

infix  -1 finally-→
infixr -2 step-→

-- For an explanation of why step-⇔ is defined in this way, see
-- Equality.step-≡.

step-→ : (@0 A : Type a) → (B → C) → (A → B) → A → C
step-→ _ f g = f ∘ g

syntax step-→ A B→C A→B = A →⟨ A→B ⟩ B→C

finally-→ : (@0 A : Type a) (@0 B : Type b) → (A → B) → A → B
finally-→ _ _ A→B = A→B

syntax finally-→ A B A→B = A →⟨ A→B ⟩□ B □

-- Application.

_$_ :
  {@0 B : A → Type b} →
  ((x : A) → B x) → ((x : A) → B x)
f $ x = f x

-- Constant functions.

const : A → (B → A)
const x = λ _ → x

{-# DISPLAY const x y = x #-}

-- Flips the first two arguments.

flip :
  {@0 C : A → B → Type c} →
  ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ x y → f y x

-- Applies the unary function to each argument and combines the
-- results using the binary function.

_on_ :
  {@0 C : B → B → Type c} →
  ((x y : B) → C x y) →
  (f : A → B) →
  ((x y : A) → C (f x) (f y))
_*_ on f = λ x y → f x * f y

-- A term's type.

Type-of : {A : Type a} → A → Type a
Type-of {A = A} _ = A

-- Type signatures.

infix 0 type-signature

type-signature : (@0 A : Type a) → A → A
type-signature _ a = a

syntax type-signature A a = a ⦂ A

-- The it function can be used to instantiate an argument by using
-- instance search.

it : ⦃ _ : A ⦄ → A
it ⦃ x ⦄ = x

-- Case expressions (to be used with pattern-matching lambdas).

infix 0 case_return_of_ case_of_

case_return_of_ :
  (x : A) (@0 B : A → Type b) → ((x : A) → B x) → B x
case x return B of f = f x

case_of_ : A → (A → B) → B
case x of f = case x return _ of f

------------------------------------------------------------------------
-- Σ-types

infixr 4 _,′_
infixr 2 _×_

open import Agda.Builtin.Sigma public
  using (Σ; _,_)
  hiding (module Σ)
  renaming (fst to proj₁; snd to proj₂)

module Σ where

  open Agda.Builtin.Sigma.Σ public
    using ()
    renaming (fst to proj₁; snd to proj₂)

  -- Variants of the projections with erased type arguments.

  proj₁₀ :
    {@0 B : A → Type b} →
    Σ A B → A
  proj₁₀ (x , y) = x

  proj₂₀ :
    {@0 B : A → Type b}
    (p : Σ A B) → B (proj₁ p)
  proj₂₀ (x , y) = y

open Σ public using (proj₁₀; proj₂₀)

-- A variant where the first argument is implicit.

∃ : {A : Type a} → (A → Type b) → Type (a ⊔ b)
∃ = Σ _

-- Binary products.

_×_ : (A : Type a) (B : Type b) → Type (a ⊔ b)
A × B = Σ A (const B)

-- A variant of _,_ that is specialised to _×_. Use of this variant
-- can make type-inference easier.

_,′_ : A → B → A × B
x ,′ y = x , y

-- A map function.

Σ-map :
  (f : A → B) → (∀ {x} → P x → Q (f x)) →
  Σ A P → Σ B Q
Σ-map f g = λ p → (f (proj₁₀ p) , g (proj₂₀ p))

-- Zip.

Σ-zip :
  (f : A → B → C) → (∀ {x y} → P x → Q y → R (f x y)) →
  Σ A P → Σ B Q → Σ C R
Σ-zip f g = λ p q → (f (proj₁₀ p) (proj₁₀ q) , g (proj₂₀ p) (proj₂₀ q))

-- Curry and uncurry.

curry :
  {@0 B : A → Type b} {@0 C : Σ A B → Type c} →
  ((p : Σ A B) → C p) →
  ((x : A) (y : B x) → C (x , y))
curry f x y = f (x , y)

uncurry :
  {@0 B : A → Type b} {@0 C : Σ A B → Type c} →
  ((x : A) (y : B x) → C (x , y)) →
  ((p : Σ A B) → C p)
uncurry f (x , y) = f x y

-- Swaps the two components of the pair.

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

------------------------------------------------------------------------
-- W-types

data W (A : Type a) (B : A → Type b) : Type (a ⊔ b) where
  sup : (x : A) (f : B x → W A B) → W A B

-- Projections.

headᵂ :
  {@0 B : A → Type b} →
  W A B → A
headᵂ (sup x f) = x

tailᵂ :
  {@0 B : A → Type b} →
  (x : W A B) → B (headᵂ x) → W A B
tailᵂ (sup x f) = f

-- If B is always inhabited, then W A B is empty.

abstract

  inhabited⇒W-empty :
    {@0 B : A → Type b} →
    (∀ x → B x) → ¬ W A B
  inhabited⇒W-empty b (sup x f) = inhabited⇒W-empty b (f (b x))

------------------------------------------------------------------------
-- Binary sums

infixr 1 _⊎_

data _⊎_ (A : Type a) (B : Type b) : Type (a ⊔ b) where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

-- Eliminator for binary sums.

[_,_] :
  {@0 C : A ⊎ B → Type c} →
  ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
  ((x : A ⊎ B) → C x)
[ f , g ] (inj₁ x) = f x
[ f , g ] (inj₂ y) = g y

-- A generalisation of if-then-else.

infix 5 if_then_else_

if_then_else_ : A ⊎ B → C → C → C
if x then t else f = [ const t , const f ] x

-- A generalisation of not.

not : A ⊎ B → B ⊎ A
not (inj₁ x) = inj₂ x
not (inj₂ x) = inj₁ x

-- A map function.

⊎-map : (A₁ → A₂) → (B₁ → B₂) → A₁ ⊎ B₁ → A₂ ⊎ B₂
⊎-map f g = [ (λ x → inj₁ (f x)) , (λ x → inj₂ (g x)) ]

-- The function from-⊎ is a safe analogue of fromJust. For an example
-- of how from-⊎ can be used, see
-- Quotient.equivalence-but-not-strong-equivalence.

From-⊎ : {A B : Type ℓ} → A ⊎ B → Type ℓ
From-⊎ {A = A} (inj₁ _) = A
From-⊎ {B = B} (inj₂ _) = B

from-⊎ : (x : A ⊎ B) → From-⊎ x
from-⊎ (inj₁ x) = x
from-⊎ (inj₂ y) = y

-- A special case of binary sums: decided predicates.

Dec : Type p → Type p
Dec P = P ⊎ ¬ P

pattern yes p = inj₁ p
pattern no  p = inj₂ p

-- Decidable relations.

Decidable : {A : Type a} {B : Type b} →
            (A → B → Type ℓ) → Type (a ⊔ b ⊔ ℓ)
Decidable _∼_ = ∀ x y → Dec (x ∼ y)

-- Exclusive or.

infixr 1 _Xor_

_Xor_ : Type a → Type b → Type (a ⊔ b)
A Xor B = (A × ¬ B) ⊎ (¬ A × B)

-- Maybe.

Maybe : Type a → Type a
Maybe A = ⊤ ⊎ A

pattern nothing = inj₁ tt
pattern just x  = inj₂ x

-- The truth predicate T is only inhabited when its argument is
-- inj₁ something.

T : A ⊎ B → Type
T b = if b then ⊤ else ⊥

------------------------------------------------------------------------
-- Booleans

-- Booleans.

Bool : Type
Bool = ⊤ ⊎ ⊤

pattern true  = inj₁ tt
pattern false = inj₂ tt

-- And.

infixr 6 _∧_

_∧_ : Bool → Bool → Bool
b₁ ∧ b₂ = if b₁ then b₂ else false

-- Or.

infixr 5 _∨_

_∨_ : Bool → Bool → Bool
b₁ ∨ b₂ = if b₁ then true else b₂

------------------------------------------------------------------------
-- Lists

open import Agda.Builtin.List public using (List; []; _∷_)

------------------------------------------------------------------------
-- Finite sets

Fin : ℕ → Type
Fin zero    = ⊥
Fin (suc n) = ⊤ ⊎ Fin n

pattern fzero  = inj₁ tt
pattern fsuc i = inj₂ i

------------------------------------------------------------------------
-- Some relation combinators

-- Combines two relations into a relation on functions.

_→-rel_ : {A : Type a} {C : Type c} →
          (A → C → Type ℓ) → (B → D → Type ℓ) →
          (A → B) → (C → D) → Type (a ⊔ c ⊔ ℓ)
(P →-rel Q) f g = ∀ x y → P x y → Q (f x) (g y)

-- Combines two relations into a relation on products.

_×-rel_ : (A → C → Type ℓ) → (B → D → Type ℓ) → A × B → C × D → Type ℓ
(P ×-rel Q) (x , u) (y , v) = P x y × Q u v

-- Combines two relations into a relation on sums.

_⊎-rel_ : (A → C → Type ℓ) → (B → D → Type ℓ) → A ⊎ B → C ⊎ D → Type ℓ
(P ⊎-rel Q) (inj₁ x) (inj₁ y) = P x y
(P ⊎-rel Q) (inj₁ x) (inj₂ v) = ⊥
(P ⊎-rel Q) (inj₂ u) (inj₁ y) = ⊥
(P ⊎-rel Q) (inj₂ u) (inj₂ v) = Q u v

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- Searchable set
------------------------------------------------------------------------

-- http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.127.3062&rep=rep1&type=pdf
-- http://www.cs.bham.ac.uk/~mhe/papers/omniscient-2011-07-06.pdf

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

module Constructive.Searchable where

-- agda-stdlib
open import Data.Bool
open import Data.Empty
open import Data.Product as Prod
open import Data.Sum as Sum
open import Function.Base
open import Relation.Binary.PropositionalEquality
import Function.Equivalence as Eqv -- TOOD use new function bundle

-- agda-misc
open import Constructive.Axiom
open import Constructive.Axiom.Properties.Base
open import Constructive.Axiom.Properties.Bool
open import Constructive.Common
open import Constructive.Combinators

module SearchModule {a} {A : Set a} (searchable : Searchable-Bool A) where
  ε : ((A → Bool) → A)
  ε = proj₁ searchable
  ε-correct : (P : A → Bool) → P (ε P) ≡ true → (x : A) → P x ≡ true
  ε-correct = proj₂ searchable

-- Lemma 2.1
searchable-Bool⇒lpo-Bool-Alt : ∀ {a} {A : Set a} → Searchable-Bool A → LPO-Bool-Alt A
searchable-Bool⇒lpo-Bool-Alt (ε , ε-correct) P with P (ε P) | inspect P (ε P)
... | false | [ P[εP]≡false ] = inj₁ (ε P , P[εP]≡false)
... | true  | [ P[εP]≡true  ] = inj₂ (ε-correct P P[εP]≡true)

searchable-Bool⇒inhabited : ∀ {a} {A : Set a} → Searchable-Bool A → Inhabited A
searchable-Bool⇒inhabited searchable-Bool = (proj₁ searchable-Bool) λ _ → true

-- Inhabited ∧ LPO-Bool-Alt => Searchable-Bool
inhabited∧lpo-Bool-Alt⇒ε : ∀ {a} {A : Set a} → Inhabited A → LPO-Bool-Alt A → (A → Bool) → A
inhabited∧lpo-Bool-Alt⇒ε inhabited lpo-Bool-Alt P with lpo-Bool-Alt P
... | inj₁ (x , _) = x
... | inj₂ _       = inhabited

inhabited∧lpo-Bool-Alt⇒ε-correct :
  ∀ {a} {A : Set a} (i : Inhabited A) (lpo-Bool-Alt : LPO-Bool-Alt A) (P : A → Bool) →
 P ((inhabited∧lpo-Bool-Alt⇒ε i lpo-Bool-Alt) P) ≡ true → (x : A) → P x ≡ true
inhabited∧lpo-Bool-Alt⇒ε-correct inhabited lpo-Bool-Alt P with lpo-Bool-Alt P
... | inj₁ (x , Px≡false) =
  λ Px≡true → ⊥-elim $ false≢true $ trans (sym Px≡false) Px≡true
  where
  false≢true : false ≢ true
  false≢true ()
... | inj₂ ∀x→Px≡true     = λ _ → ∀x→Px≡true

inhabited∧lpo-Bool-Alt⇒searchable-Bool :
  ∀ {a} {A : Set a} → Inhabited A → LPO-Bool-Alt A → Searchable-Bool A
inhabited∧lpo-Bool-Alt⇒searchable-Bool inhabited lpo-Bool-Alt =
  inhabited∧lpo-Bool-Alt⇒ε inhabited lpo-Bool-Alt ,
  inhabited∧lpo-Bool-Alt⇒ε-correct inhabited lpo-Bool-Alt

-- Searchable-Bool <=> Searchable
searchable-Bool⇒searchable : ∀ {a p} {A : Set a} →
                             Searchable-Bool A → Searchable A p
searchable-Bool⇒searchable {a} {p} {A} searchable-Bool =
  inhabited∧lpo⇒searchable inhabited lpo
  where
  inhabited = searchable-Bool⇒inhabited searchable-Bool
  lpo : LPO A p
  lpo = lpo-Bool⇒lpo p $ lpo-Bool-Alt⇒lpo-Bool $
          searchable-Bool⇒lpo-Bool-Alt searchable-Bool

searchable⇒searchable-Bool : ∀ {a p} {A : Set a} →
                             Searchable A p → Searchable-Bool A
searchable⇒searchable-Bool searchable =
  inhabited∧lpo-Bool-Alt⇒searchable-Bool inhabited lpo-Bool-Alt
  where
  inhabited = searchable⇒inhabited searchable
  lpo-Bool-Alt = lpo-Bool⇒lpo-Bool-Alt $ lpo⇒lpo-Bool $ searchable⇒lpo searchable

-- Lemma 2.2
module Lemma2-2 {a} {A : Set a} (searchable-Bool : Searchable-Bool A) where
  open SearchModule searchable-Bool
  module _ {P : A → Bool} where
    ∃x→Px≡false→P[εP]≡false : (∃ λ x → P x ≡ false) → P (ε P) ≡ false
    ∃x→Px≡false→P[εP]≡false e =
      x≢true⇒x≡false $ contraposition (ε-correct P)
                                      (∃¬P→¬∀P (Prod.map₂ x≡false⇒x≢true e))
        where
        x≡false⇒x≢true : ∀ {x} → x ≡ false → x ≢ true
        x≡false⇒x≢true {false} refl ()
        x≢true⇒x≡false : ∀ {x} → x ≢ true → x ≡ false
        x≢true⇒x≡false {false} neq = refl
        x≢true⇒x≡false {true } neq = ⊥-elim $ neq refl

    ∃x→Px≡false⇔P[εP]≡false : (∃ λ x → P x ≡ false) Eqv.⇔ P (ε P) ≡ false
    ∃x→Px≡false⇔P[εP]≡false =
      Eqv.equivalence ∃x→Px≡false→P[εP]≡false λ eq → ε P , eq

  -- E_X
  Exist : (A → Bool) → Bool
  Exist P = P (ε P)

  Exist[P]≡false⇔∃x→Px≡false :
    {P : A → Bool} → Exist P ≡ false Eqv.⇔ (∃ λ x → P x ≡ false)
  Exist[P]≡false⇔∃x→Px≡false = Eqv.sym ∃x→Px≡false⇔P[εP]≡false

open Lemma2-2

Exhaustible : ∀ {a} → Set a → Set a
Exhaustible A = Σ ((A → Bool) → Bool) λ ∀K →
  (P : A → Bool) → ∀K P ≡ true → ∀ x → P x ≡ true


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

open import lib.Base
open import lib.PathGroupoid
open import lib.PathOver

module lib.cubical.Square where

{-
  *--1--*
  |     |
  0     3
  |     |
  *--2--*
-}

data Square {i} {A : Type i} {a₀₀ : A} : {a₀₁ a₁₀ a₁₁ : A}
  → a₀₀ == a₀₁ → a₀₀ == a₁₀ → a₀₁ == a₁₁ → a₁₀ == a₁₁ → Type i
  where
  ids : Square idp idp idp idp

hid-square : ∀ {i} {A : Type i} {a₀₀ a₀₁ : A} {p : a₀₀ == a₀₁}
  → Square p idp idp p
hid-square {p = idp} = ids

vid-square : ∀ {i} {A : Type i} {a₀₀ a₁₀ : A} {p : a₀₀ == a₁₀}
  → Square idp p p idp
vid-square {p = idp} = ids

square-to-disc : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → p₀₋ ∙ p₋₁ == p₋₀ ∙ p₁₋
square-to-disc ids = idp

disc-to-square : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → p₀₋ ∙ p₋₁ == p₋₀ ∙ p₁₋
  → Square p₀₋ p₋₀ p₋₁ p₁₋
disc-to-square {p₀₋ = idp} {p₋₀ = idp} {p₋₁ = idp} {p₁₋ = .idp} idp = ids

square-to-disc-β : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (α : p₀₋ ∙ p₋₁ == p₋₀ ∙ p₁₋)
  → square-to-disc (disc-to-square {p₀₋ = p₀₋} {p₋₀ = p₋₀} α) == α
square-to-disc-β {p₀₋ = idp} {p₋₀ = idp} {p₋₁ = idp} {p₁₋ = .idp} idp = idp

disc-to-square-β : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → disc-to-square (square-to-disc sq) == sq
disc-to-square-β ids = idp

ap-square : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → Square (ap f p₀₋) (ap f p₋₀) (ap f p₋₁) (ap f p₁₋)
ap-square f ids = ids

ap-square-hid : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  {a₀ a₁ : A} {p : a₀ == a₁}
  → ap-square f (hid-square {p = p}) == hid-square
ap-square-hid {p = idp} = idp

ap-square-vid : ∀ {i j} {A : Type i} {B : Type j} {f : A → B}
  {a₀ a₁ : A} {p : a₀ == a₁}
  → ap-square f (vid-square {p = p}) == vid-square
ap-square-vid {p = idp} = idp

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

  horiz-degen-square : {a a' : A} {p q : a == a'}
    → p == q → Square p idp idp q
  horiz-degen-square {p = idp} α = disc-to-square α

  horiz-degen-path : {a a' : A} {p q : a == a'}
    → Square p idp idp q → p == q
  horiz-degen-path {p = idp} sq = square-to-disc sq

  horiz-degen-path-β : {a a' : A} {p q : a == a'} (α : p == q)
    → horiz-degen-path (horiz-degen-square α) == α
  horiz-degen-path-β {p = idp} α = square-to-disc-β α

  horiz-degen-square-β : {a a' : A} {p q : a == a'} (sq : Square p idp idp q)
    → horiz-degen-square (horiz-degen-path sq) == sq
  horiz-degen-square-β {p = idp} sq = disc-to-square-β sq

  vert-degen-square : {a a' : A} {p q : a == a'}
    → p == q → Square idp p q idp
  vert-degen-square {p = idp} α = disc-to-square (! α)

  vert-degen-path : {a a' : A} {p q : a == a'}
    → Square idp p q idp → p == q
  vert-degen-path {p = idp} sq = ! (square-to-disc sq)

  vert-degen-path-β : {a a' : A} {p q : a == a'} (α : p == q)
    → vert-degen-path (vert-degen-square α) == α
  vert-degen-path-β {p = idp} α = ap ! (square-to-disc-β (! α)) ∙ !-! α

  vert-degen-square-β : {a a' : A} {p q : a == a'} (sq : Square idp p q idp)
    → vert-degen-square (vert-degen-path sq) == sq
  vert-degen-square-β {p = idp} sq =
    ap disc-to-square (!-! (square-to-disc sq)) ∙ disc-to-square-β sq

  horiz-degen-square-idp : {a a' : A} {p : a == a'}
    → horiz-degen-square (idp {a = p}) == hid-square
  horiz-degen-square-idp {p = idp} = idp

  vert-degen-square-idp : {a a' : A} {p : a == a'}
    → vert-degen-square (idp {a = p}) == vid-square
  vert-degen-square-idp {p = idp} = idp

{- Flipping squares -}
module _ {i} {A : Type i} where

  square-symmetry : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₋₀ p₀₋ p₁₋ p₋₁
  square-symmetry ids = ids

  square-sym-inv : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → square-symmetry (square-symmetry sq) == sq
  square-sym-inv ids = idp

ap-square-symmetry : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  {a₀₀ a₀₁ a₁₀ a₁₁ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → ap-square f (square-symmetry sq) == square-symmetry (ap-square f sq)
ap-square-symmetry f ids = idp

{- Alternate induction principles -}

square-left-J : ∀ {i j} {A : Type i} {a₀₀ a₀₁ : A} {p₀₋ : a₀₀ == a₀₁}
  (P : {a₁₀ a₁₁ : A} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
       (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
       → Type j)
  (r : P hid-square)
  {a₁₀ a₁₁ : A} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → P sq
square-left-J P r ids = r

square-top-J : ∀ {i j} {A : Type i} {a₀₀ a₁₀ : A} {p₋₀ : a₀₀ == a₁₀}
  (P : {a₀₁ a₁₁ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
       (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
       → Type j)
  (r : P vid-square)
  {a₀₁ a₁₁ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → P sq
square-top-J P r ids = r

square-bot-J : ∀ {i j} {A : Type i} {a₀₁ a₁₁ : A} {p₋₁ : a₀₁ == a₁₁}
  (P : {a₀₀ a₁₀ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₁₋ : a₁₀ == a₁₁}
       (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
       → Type j)
  (r : P vid-square)
  {a₀₀ a₁₀ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₁₋ : a₁₀ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → P sq
square-bot-J P r ids = r

square-right-J : ∀ {i j} {A : Type i} {a₁₀ a₁₁ : A} {p₁₋ : a₁₀ == a₁₁}
  (P : {a₀₀ a₀₁ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁}
       (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
       → Type j)
  (r : P hid-square)
  {a₀₀ a₀₁ : A} {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁}
  (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
  → P sq
square-right-J P r ids = r

module _ where
  private
    lemma : ∀ {i j} {A : Type i} {a₀ : A}
      (P : {a₁ : A} {p q : a₀ == a₁} → p == q → Type j)
      (r : P (idp {a = idp}))
      {a₁ : A} {p q : a₀ == a₁} (α : p == q)
      → P α
    lemma P r {p = idp} idp = r

  horiz-degen-J : ∀ {i j} {A : Type i} {a₀ : A}
    (P : {a₁ : A} {p q : a₀ == a₁} → Square p idp idp q → Type j)
    (r : P ids)
    {a₁ : A} {p q : a₀ == a₁} (sq : Square p idp idp q)
    → P sq
  horiz-degen-J P r sq = transport P
    (horiz-degen-square-β sq)
    (lemma (P ∘ horiz-degen-square) r (horiz-degen-path sq))

  vert-degen-J : ∀ {i j} {A : Type i} {a₀ : A}
    (P : {a₁ : A} {p q : a₀ == a₁} → Square idp p q idp → Type j)
    (r : P ids)
    {a₁ : A} {p q : a₀ == a₁} (sq : Square idp p q idp)
    → P sq
  vert-degen-J P r sq = transport P
    (vert-degen-square-β sq)
    (lemma (P ∘ vert-degen-square) r (vert-degen-path sq))

{- Square filling -}
module _ {i} {A : Type i} where
  fill-square-left : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    (p₋₀ : a₀₀ == a₁₀) (p₋₁ : a₀₁ == a₁₁) (p₁₋ : a₁₀ == a₁₁)
    → Σ (a₀₀ == a₀₁) (λ p₀₋ → Square p₀₋ p₋₀ p₋₁ p₁₋)
  fill-square-left idp idp p = (p , hid-square)

  fill-square-top : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    (p₀₋ : a₀₀ == a₀₁) (p₋₁ : a₀₁ == a₁₁) (p₁₋ : a₁₀ == a₁₁)
    → Σ (a₀₀ == a₁₀) (λ p₋₀ → Square p₀₋ p₋₀ p₋₁ p₁₋)
  fill-square-top idp p idp = (p , vid-square)

  fill-square-bot : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    (p₀₋ : a₀₀ == a₀₁) (p₋₀ : a₀₀ == a₁₀) (p₁₋ : a₁₀ == a₁₁)
    → Σ (a₀₁ == a₁₁) (λ p₋₁ → Square p₀₋ p₋₀ p₋₁ p₁₋)
  fill-square-bot idp p idp = (p , vid-square)

  fill-square-right : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    (p₀₋ : a₀₀ == a₀₁) (p₋₀ : a₀₀ == a₁₀) (p₋₁ : a₀₁ == a₁₁)
    → Σ (a₁₀ == a₁₁) (λ p₁₋ → Square p₀₋ p₋₀ p₋₁ p₁₋)
  fill-square-right p idp idp = (p , hid-square)

module _ {i j} {A : Type i} {B : Type j} {f g : A → B} where

  ↓-='-to-square : {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    → u == v [ (λ z → f z == g z) ↓ p ]
    → Square u (ap f p) (ap g p) v
  ↓-='-to-square {p = idp} α = horiz-degen-square α

  ↓-='-from-square : {x y : A} {p : x == y} {u : f x == g x} {v : f y == g y}
    → Square u (ap f p) (ap g p) v
    → u == v [ (λ z → f z == g z) ↓ p ]
  ↓-='-from-square {p = idp} sq = horiz-degen-path sq

module _  {i j} {A : Type i} {B : Type j} {f : A → B} {b : B} where

  ↓-cst=app-from-square : {x y : A} {p : x == y}
    {u : b == f x} {v : b == f y}
    → Square u idp (ap f p) v
    → u == v [ (λ z → b == f z) ↓ p ]
  ↓-cst=app-from-square {p = idp} sq = horiz-degen-path sq

  ↓-cst=app-to-square : {x y : A} {p : x == y}
    {u : b == f x} {v : b == f y}
    → u == v [ (λ z → b == f z) ↓ p ]
    → Square u idp (ap f p) v
  ↓-cst=app-to-square {p = idp} α = horiz-degen-square α

  ↓-app=cst-from-square : {x y : A} {p : x == y}
    {u : f x == b} {v : f y == b}
    → Square u (ap f p) idp v
    → u == v [ (λ z → f z == b) ↓ p ]
  ↓-app=cst-from-square {p = idp} sq = horiz-degen-path sq

  ↓-app=cst-to-square : {x y : A} {p : x == y}
    {u : f x == b} {v : f y == b}
    → u == v [ (λ z → f z == b) ↓ p ]
    → Square u (ap f p) idp v
  ↓-app=cst-to-square {p = idp} α = horiz-degen-square α

module _  {i} {A : Type i} {f : A → A} where

  ↓-idf=app-from-square : {x y : A} {p : x == y}
    {u : x == f x} {v : y == f y}
    → Square u p (ap f p) v
    → u == v [ (λ z → z == f z) ↓ p ]
  ↓-idf=app-from-square {p = idp} sq = horiz-degen-path sq

  ↓-idf=app-to-square : {x y : A} {p : x == y}
    {u : x == f x} {v : y == f y}
    → u == v [ (λ z → z == f z) ↓ p ]
    → Square u p (ap f p) v
  ↓-idf=app-to-square {p = idp} α = horiz-degen-square α

  ↓-app=idf-from-square : {x y : A} {p : x == y}
    {u : f x == x} {v : f y == y}
    → Square u (ap f p) p v
    → u == v [ (λ z → f z == z) ↓ p ]
  ↓-app=idf-from-square {p = idp} sq = horiz-degen-path sq

  ↓-app=idf-to-square : {x y : A} {p : x == y}
    {u : f x == x} {v : f y == y}
    → u == v [ (λ z → f z == z) ↓ p ]
    → Square u (ap f p) p v
  ↓-app=idf-to-square {p = idp} α = horiz-degen-square α

module _  {i j} {A : Type i} {B : Type j} (g : B → A) (f : A → B) where

  ↓-∘=idf-from-square : {x y : A} {p : x == y}
    {u : g (f x) == x} {v : g (f y) == y}
    → Square u (ap g (ap f p)) p v
    → (u == v [ (λ z → g (f z) == z) ↓ p ])
  ↓-∘=idf-from-square {p = idp} sq = horiz-degen-path sq

  ↓-∘=idf-to-square : {x y : A} {p : x == y}
    {u : g (f x) == x} {v : g (f y) == y}
    → (u == v [ (λ z → g (f z) == z) ↓ p ])
    → Square u (ap g (ap f p)) p v
  ↓-∘=idf-to-square {p = idp} α = horiz-degen-square α

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

  natural-square : {f₁ f₂ : A → B} (p : ∀ a → f₁ a == f₂ a)
    {a₁ a₂ : A} (q : a₁ == a₂)
    → Square (p a₁) (ap f₁ q) (ap f₂ q) (p a₂)
  natural-square p idp = hid-square

  natural-square-idp : {f₁ : A → B} {a₁ a₂ : A} (q : a₁ == a₂)
    → natural-square {f₁ = f₁} (λ _ → idp) q == vid-square
  natural-square-idp idp = idp

  {- Used for getting square equivalents of glue-β terms -}
  natural-square-β : {f₁ f₂ : A → B} (p : (a : A) → f₁ a == f₂ a)
    {x y : A} (q : x == y)
    {sq : Square (p x) (ap f₁ q) (ap f₂ q) (p y)}
    → apd p q == ↓-='-from-square sq
    → natural-square p q == sq
  natural-square-β _ idp α =
    ! horiz-degen-square-idp ∙ ap horiz-degen-square α ∙ horiz-degen-square-β _

_⊡v_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ a₀₂ a₁₂ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {q₀₋ : a₀₁ == a₀₂} {q₋₂ : a₀₂ == a₁₂} {q₁₋ : a₁₁ == a₁₂}
  → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square q₀₋ p₋₁ q₋₂ q₁₋
  → Square (p₀₋ ∙ q₀₋) p₋₀ q₋₂ (p₁₋ ∙ q₁₋)
ids ⊡v sq = sq

_⊡v'_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ a₀₂ a₁₂ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {q₀₋ : a₀₁ == a₀₂} {q₋₂ : a₀₂ == a₁₂} {q₁₋ : a₁₁ == a₁₂}
  → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square q₀₋ p₋₁ q₋₂ q₁₋
  → Square (p₀₋ ∙' q₀₋) p₋₀ q₋₂ (p₁₋ ∙' q₁₋)
sq ⊡v' ids = sq

_∙v⊡_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ p₋₀' : a₀₀ == a₁₀}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → p₋₀ == p₋₀'
  → Square p₀₋ p₋₀' p₋₁ p₁₋
  → Square p₀₋ p₋₀ p₋₁ p₁₋
idp ∙v⊡ sq = sq

_⊡v∙_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₋₀ : a₀₀ == a₁₀} {p₀₋ : a₀₀ == a₀₁}
  {p₋₁ p₋₁' : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → p₋₁ == p₋₁'
  → Square p₀₋ p₋₀ p₋₁' p₁₋
sq ⊡v∙ idp = sq

_⊡h_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ a₂₀ a₂₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {q₋₀ : a₁₀ == a₂₀} {q₋₁ : a₁₁ == a₂₁} {q₂₋ : a₂₀ == a₂₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → Square p₁₋ q₋₀ q₋₁ q₂₋
  → Square p₀₋ (p₋₀ ∙ q₋₀) (p₋₁ ∙ q₋₁) q₂₋
ids ⊡h sq = sq

_⊡h'_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ a₂₀ a₂₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  {q₋₀ : a₁₀ == a₂₀} {q₋₁ : a₁₁ == a₂₁} {q₂₋ : a₂₀ == a₂₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → Square p₁₋ q₋₀ q₋₁ q₂₋
  → Square p₀₋ (p₋₀ ∙' q₋₀) (p₋₁ ∙' q₋₁) q₂₋
sq ⊡h' ids = sq

_∙h⊡_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ p₀₋' : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
  → p₀₋ == p₀₋'
  → Square p₀₋' p₋₀ p₋₁ p₁₋
  → Square p₀₋ p₋₀ p₋₁ p₁₋
idp ∙h⊡ sq = sq

_⊡h∙_ : ∀ {i} {A : Type i} {a₀₀ a₀₁ a₁₀ a₁₁ : A}
  {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
  {p₋₁ : a₀₁ == a₁₁} {p₁₋ p₁₋' : a₁₀ == a₁₁}
  → Square p₀₋ p₋₀ p₋₁ p₁₋
  → p₁₋ == p₁₋'
  → Square p₀₋ p₋₀ p₋₁ p₁₋'
sq ⊡h∙ idp = sq

infixr 80 _⊡v_ _⊡v'_ _⊡h_ _⊡h'_

infixr 80 _∙v⊡_ _∙h⊡_
infixl 85 _⊡v∙_ _⊡h∙_

module _ {i} {A : Type i} where
  !□h : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋
    → Square p₁₋ (! p₋₀) (! p₋₁) p₀₋
  !□h ids = ids

  !□v : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋
    → Square (! p₀₋) p₋₁ p₋₀ (! p₁₋)
  !□v ids = ids

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

  {- TODO rest of these -}

  ⊡h-unit-l : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → hid-square ⊡h sq == sq
  ⊡h-unit-l ids = idp

  ⊡h-unit-r : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → sq ⊡h hid-square == ∙-unit-r _ ∙v⊡ (sq ⊡v∙ ! (∙-unit-r _))
  ⊡h-unit-r ids = idp

  ⊡h'-unit-l : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → hid-square ⊡h' sq == ∙'-unit-l _ ∙v⊡ (sq ⊡v∙ ! (∙'-unit-l _))
  ⊡h'-unit-l ids = idp

  ⊡h-unit-l-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀} {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq' : Square p₀₋ idp idp p₀₋) (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → sq' ⊡h sq == sq
    → sq' == hid-square
  ⊡h-unit-l-unique sq' ids p = ! (⊡h-unit-r sq') ∙ p

module _ {i} {A : Type i} where
  !□h-inv-l : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → (!□h sq) ⊡h sq == !-inv-l p₋₀ ∙v⊡ (hid-square ⊡v∙ ! (!-inv-l p₋₁))
  !□h-inv-l ids = idp

  !□h-inv-r : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → sq ⊡h (!□h sq) == !-inv-r p₋₀ ∙v⊡ (hid-square ⊡v∙ ! (!-inv-r p₋₁))
  !□h-inv-r ids = idp

  !□v-inv-l : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → (!□v sq) ⊡v sq == !-inv-l p₀₋ ∙h⊡ (vid-square ⊡h∙ ! (!-inv-l p₁₋))
  !□v-inv-l ids = idp

  !□v-inv-r : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    (sq : Square p₀₋ p₋₀ p₋₁ p₁₋)
    → sq ⊡v (!□v sq) == !-inv-r p₀₋ ∙h⊡ (vid-square ⊡h∙ ! (!-inv-r p₁₋))
  !□v-inv-r ids = idp

module _ {i} {A : Type i} where
  square-left-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ p₀₋' : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₀₋' p₋₀ p₋₁ p₁₋
    → p₀₋ == p₀₋'
  square-left-unique {p₋₀ = idp} {p₋₁ = idp} sq₁ sq₂ =
    horiz-degen-path (sq₁ ⊡h (!□h sq₂))

  square-top-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ p₋₀' : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₀₋ p₋₀' p₋₁ p₁₋
    → p₋₀ == p₋₀'
  square-top-unique {p₀₋ = idp} {p₁₋ = idp} sq₁ sq₂ =
    vert-degen-path (sq₁ ⊡v (!□v sq₂))

  square-bot-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ p₋₁' : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₀₋ p₋₀ p₋₁' p₁₋
    → p₋₁ == p₋₁'
  square-bot-unique {p₀₋ = idp} {p₁₋ = idp} sq₁ sq₂ =
    vert-degen-path ((!□v sq₁) ⊡v sq₂)

  square-right-unique : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ p₁₋' : a₁₀ == a₁₁}
    → Square p₀₋ p₋₀ p₋₁ p₁₋ → Square p₀₋ p₋₀ p₋₁ p₁₋'
    → p₁₋ == p₁₋'
  square-right-unique {p₋₀ = idp} {p₋₁ = idp} sq₁ sq₂ =
    horiz-degen-path ((!□h sq₁) ⊡h sq₂)

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

  {- XXX naminig -}
  connection : {a₀ a₁ : A} {q : a₀ == a₁}
    → Square idp idp q q
  connection {q = idp} = ids

  {- XXX naminig -}
  connection2 : {a₀ a₁ a₂ : A} {p : a₀ == a₁} {q : a₁ == a₂}
    → Square p p q q
  connection2 {p = idp} {q = idp} = ids

  lb-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square p idp (! p) idp
  lb-square idp = ids

  bl-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square (! p) idp p idp
  bl-square idp = ids

  br-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square idp idp p p
  br-square idp = ids

  rb-square = br-square

  rt-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square idp (! p) idp p
  rt-square idp = ids

  tr-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square idp p idp (! p)
  tr-square idp = ids

  lt-square : {a₀ a₁ : A} (p : a₀ == a₁)
    → Square p p idp idp
  lt-square idp = ids

  tl-square = lt-square

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import HoTT
open import groups.KernelImage
open import groups.KernelImageEmap

module cohomology.ChainComplex where

  record ChainComplex i : Type (lsucc i) where
    field
      head : AbGroup i
      chain : ℕ → AbGroup i
      augment : AbGroup.grp (chain 0) →ᴳ AbGroup.grp head
      boundary : ∀ n → (AbGroup.grp (chain (S n)) →ᴳ AbGroup.grp (chain n))

  record CochainComplex i : Type (lsucc i) where
    field
      head : AbGroup i
      cochain : ℕ → AbGroup i
      augment : AbGroup.grp head →ᴳ AbGroup.grp (cochain 0)
      coboundary : ∀ n → (AbGroup.grp (cochain n) →ᴳ AbGroup.grp (cochain (S n)))

  record CochainComplexEquiv {i₀ i₁}
    (cc₀ : CochainComplex i₀) (cc₁ : CochainComplex i₁) : Type (lmax i₀ i₁) where
    private
      module cc₀ = CochainComplex cc₀
      module cc₁ = CochainComplex cc₁
    field
      head : AbGroup.grp cc₀.head ≃ᴳ AbGroup.grp cc₁.head
      cochain : (n : ℕ) → AbGroup.grp (cc₀.cochain n) ≃ᴳ AbGroup.grp (cc₁.cochain n)
      augment : CommSquareᴳ cc₀.augment cc₁.augment (–>ᴳ head) (–>ᴳ (cochain 0))
      coboundary : ∀ n → CommSquareᴳ (cc₀.coboundary n) (cc₁.coboundary n)
        (–>ᴳ (cochain n)) (–>ᴳ (cochain (S n)))

  homology-group : ∀ {i} → ChainComplex i → (n : ℤ) → Group i
  homology-group cc (pos 0) = Ker/Im cc.augment (cc.boundary 0) (snd (cc.chain 0))
    where module cc = ChainComplex cc
  homology-group cc (pos (S n)) = Ker/Im (cc.boundary n) (cc.boundary (S n)) (snd (cc.chain (S n)))
    where module cc = ChainComplex cc
  homology-group {i} cc (negsucc _) = Lift-group {j = i} Unit-group

  cohomology-group : ∀ {i} → CochainComplex i → (n : ℤ) → Group i
  cohomology-group cc (pos 0) = Ker/Im (cc.coboundary 0) cc.augment (snd (cc.cochain 0))
    where module cc = CochainComplex cc
  cohomology-group cc (pos (S n)) = Ker/Im (cc.coboundary (S n)) (cc.coboundary n) (snd (cc.cochain (S n)))
    where module cc = CochainComplex cc
  cohomology-group {i} cc (negsucc _) = Lift-group {j = i} Unit-group

  cohomology-group-emap : ∀ {i₀ i₁} {cc₀ : CochainComplex i₀} {cc₁ : CochainComplex i₁}
    → CochainComplexEquiv cc₀ cc₁
    → (n : ℤ) → cohomology-group cc₀ n ≃ᴳ cohomology-group cc₁ n
  cohomology-group-emap {cc₀ = cc₀} {cc₁} cc= (pos 0) =
    Ker/Im-emap (snd (cc₀.cochain 0)) (snd (cc₁.cochain 0))
      (cc=.coboundary 0) cc=.augment
      (snd cc=.head) (snd (cc=.cochain 0)) (snd (cc=.cochain 1))
    where module cc₀ = CochainComplex cc₀
          module cc₁ = CochainComplex cc₁
          module cc= = CochainComplexEquiv cc=
  cohomology-group-emap {cc₀ = cc₀} {cc₁} cc= (pos (S n)) =
    Ker/Im-emap (snd (cc₀.cochain (S n))) (snd (cc₁.cochain (S n)))
      (cc=.coboundary (S n)) (cc=.coboundary n)
      (snd (cc=.cochain n)) (snd (cc=.cochain (S n))) (snd (cc=.cochain (S (S n))))
    where module cc₀ = CochainComplex cc₀
          module cc₁ = CochainComplex cc₁
          module cc= = CochainComplexEquiv cc=
  cohomology-group-emap _ (negsucc _) = lift-iso ∘eᴳ lower-iso

  complex-dualize : ∀ {i j} → ChainComplex i → AbGroup j
    →  CochainComplex (lmax i j)
  complex-dualize {i} {j} cc G = record {M} where
    module cc = ChainComplex cc
    module M where
      head : AbGroup (lmax i j)
      head = hom-abgroup (AbGroup.grp cc.head) G

      cochain : ℕ → AbGroup (lmax i j)
      cochain n = hom-abgroup (AbGroup.grp (cc.chain n)) G

      augment : AbGroup.grp head →ᴳ AbGroup.grp (cochain 0)
      augment = pre∘ᴳ-hom G cc.augment

      coboundary : ∀ n → (AbGroup.grp (cochain n) →ᴳ AbGroup.grp (cochain (S n)))
      coboundary n = pre∘ᴳ-hom G (cc.boundary n)


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

open import HoTT

-- Associativity of the join (work in progress)

module experimental.JoinAssoc {i j k} (A : Type i) (B : Type j) (C : Type k) where

  {- First map -}

  to : (A * B) * C → A * (B * C)
  to = To.f  module _ where

    to-left-glue : (ab : A × B) → left (fst ab) == right (left (snd ab)) :> A * (B * C)
    to-left-glue (a , b) = glue (a , left b)

    module ToLeft = PushoutRec left (right ∘ left) to-left-glue

    to-left : A * B → A * (B * C)
    to-left = ToLeft.f

    to-glue-left : (c : C) (a : A) → to-left (left a) == right (right c)
    to-glue-left c a = glue (a , right c)

    to-glue-right : (c : C) (b : B) → to-left (right b) == right (right c)
    to-glue-right c b = ap right (glue (b , c))

    to-glue-glue : (c : C) (ab : A × B) → to-glue-left c (fst ab) == to-glue-right c (snd ab) [ (λ x → to-left x == right (right c)) ↓ glue ab ]
    to-glue-glue c (a , b) = ↓-swap to-left right _ idp
      (ToLeft.glue-β (a , b) ◃ apd (λ x → glue (a , x)) (glue (b , c)))

    module ToGlue (c : C) = PushoutElim (to-glue-left c) (to-glue-right c) (to-glue-glue c)

    to-glue : (ab-c : (A * B) × C) → to-left (fst ab-c) == right (right (snd ab-c))
    to-glue (ab , c) = M.f ab where module M = ToGlue c

    module To = PushoutRec {d = *-span (A * B) C} to-left (right ∘ right) to-glue

  {- Second map -}

  from : A * (B * C) → (A * B) * C
  from = From.f  module MM where

    from-right-glue : (bc : B × C) → left (right (fst bc)) == right (snd bc)
    from-right-glue (b , c) = glue (right b , c)

    module FromRight = PushoutRec (left ∘ right) right from-right-glue

    from-right : B * C → (A * B) * C
    from-right = FromRight.f

    from-glue-left : (a : A) (b : B) → left (left a) == from-right (left b)
    from-glue-left a b = ap left (glue (a , b))

    from-glue-right : (a : A) (c : C) → left (left a) == from-right (right c)
    from-glue-right a c = glue (left a , c)

    from-glue-glue : (a : A) (bc : B × C) → from-glue-left a (fst bc) == from-glue-right a (snd bc) [ (λ x → left (left a) == from-right x) ↓ glue bc ]
    from-glue-glue a (b , c) = ↓-swap! left from-right _ idp
      (apd (λ x → glue (x , c)) (glue (a , b)) ▹! (FromRight.glue-β (b , c)))

    module FromGlue (a : A) = PushoutElim (from-glue-left a) (from-glue-right a) (from-glue-glue a)

    from-glue : (a-bc : A × (B * C)) → left (left (fst a-bc)) == from-right (snd a-bc)
    from-glue (a , bc) = M.f bc where module M = FromGlue a

    module From = PushoutRec {d = *-span A (B * C)} (left ∘ left) from-right from-glue

  open MM public

  {- First composite -}

  to-from-right-glue' : (b : B) (c : C) → ap (to ∘ from-right) (glue (b , c)) =-= ap right (glue (b , c))
  to-from-right-glue' b c =
    ap (λ z → to (from-right z)) (glue (b , c))     =⟪ ap-∘ to from-right (glue (b , c)) ⟫
    ap to (ap from-right (glue (b , c)))            =⟪ FromRight.glue-β (b , c) |in-ctx ap to ⟫
    ap to (glue ((right b , c) :> ((A * B) × C)))   =⟪ To.glue-β (right b , c)⟫
    ap right (glue (b , c)) ∎∎

  to-from-right-glue : (bc : B × C) → idp == idp [ (λ x → to (from (right x)) == right x) ↓ glue bc ]
  to-from-right-glue (b , c) = ↓-='-in (! (↯ to-from-right-glue' b c))

  module ToFromRight = PushoutElim (λ _ → idp) (λ _ → idp) to-from-right-glue

  to-from-right : (bc : B * C) → to (from (right bc)) == right bc
  to-from-right = ToFromRight.f

  to-from-glue-left' : (a : A) (b : B) → ap to (ap from (glue (a , left b))) =-= glue (a , left b)
  to-from-glue-left' a b =
    ap to (ap from (glue (a , left b)))   =⟪ From.glue-β (a , left b) |in-ctx ap to ⟫
    ap to (ap left (glue (a , b)))        =⟪ ∘-ap to left (glue (a , b)) ⟫
    ap to-left (glue (a , b))             =⟪ ToLeft.glue-β (a , b) ⟫
    glue (a , left b) ∎∎

  to-from-glue-left : (a : A) (b : B) → idp == to-from-right (left b) [ (λ x → to (from x) == x) ↓ glue (a , left b) ]
  to-from-glue-left a b = ↓-∘=idf-in to from (↯ to-from-glue-left' a b)

  to-from-glue-right' : (a : A) (c : C) → ap to (ap from (glue (a , right c))) =-= glue (a , right c)
  to-from-glue-right' a c =
    ap to (ap from (glue (a , right c)))   =⟪ From.glue-β (a , right c) |in-ctx ap to ⟫
    ap to (glue (left a , c))              =⟪ To.glue-β (left a , c) ⟫
    glue (a , right c) ∎∎

  to-from-glue-right : (a : A) (c : C) → idp == to-from-right (right c) [ (λ x → to (from x) == x) ↓ glue (a , right c) ]
  to-from-glue-right a c = ↓-∘=idf-in to from (↯ to-from-glue-right' a c)

  postulate  -- Not proved yet. Some of it is being worked on at JoinAssoc2
    *-assoc : ((A * B) * C) ≃ (A * (B * C))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
-- Andreas, 2016-10-08, issue #2243

-- {-# OPTIONS -v tc.cover.cover:100 #-}

open import Agda.Builtin.Char

f : Char → Char
f 'x' = 'x'
f 'x' = 'y'  -- should be marked as unreachable clause
f _ = 's'

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda