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

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

open import Vehicle
open import Vehicle.Data.Tensor
open import Data.Product
open import Data.Sum
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℝ using () renaming (ℚ to ℝ)
open import Data.Fin as Fin using (#_)
open import Data.List

module property6-output where

private
  VEHICLE_PROJECT_FILE = "TODO_projectFile"

pi : ℝ
pi = ℤ.+ 392699 ℝ./ 125000

InputVector : Set
InputVector = Tensor ℝ (5 ∷ [])

OutputVector : Set
OutputVector = Tensor ℝ (5 ∷ [])

acasXu : InputVector → OutputVector
acasXu = evaluate record
  { projectFile = VEHICLE_PROJECT_FILE
  ; networkUUID = "TODO_networkUUID"
  }

distanceToIntruder : InputVector → ℝ
distanceToIntruder x = x (# 0)

angleToIntruder : InputVector → ℝ
angleToIntruder x = x (# 1)

intruderHeading : InputVector → ℝ
intruderHeading x = x (# 2)

speed : InputVector → ℝ
speed x = x (# 3)

intruderSpeed : InputVector → ℝ
intruderSpeed x = x (# 4)

clearOfConflictScore : InputVector → ℝ
clearOfConflictScore x = acasXu x (# 0)

IntruderFarAway : InputVector → Set
IntruderFarAway x = (ℝ.- pi ℝ.≤ angleToIntruder x × angleToIntruder x ℝ.≤ ℝ.- (ℤ.+ 7 ℝ./ 10) ⊎ ℤ.+ 7 ℝ./ 10 ℝ.≤ angleToIntruder x × angleToIntruder x ℝ.≤ pi) × ((ℤ.+ 12000 ℝ./ 1 ℝ.≤ distanceToIntruder x × distanceToIntruder x ℝ.≤ ℤ.+ 62000 ℝ./ 1) × ((ℝ.- pi ℝ.≤ intruderHeading x × intruderHeading x ℝ.≤ ℝ.- pi ℝ.+ ℤ.+ 1 ℝ./ 200) × ((ℤ.+ 100 ℝ./ 1 ℝ.≤ speed x × speed x ℝ.≤ ℤ.+ 1200 ℝ./ 1) × (ℤ.+ 0 ℝ./ 1 ℝ.≤ intruderSpeed x × intruderSpeed x ℝ.≤ ℤ.+ 1200 ℝ./ 1))))

AdvisesClearOfConflict : InputVector → Set
AdvisesClearOfConflict x = let y = acasXu x in y (# 0) ℝ.> y (# 1) × (y (# 0) ℝ.> y (# 2) × (y (# 0) ℝ.> y (# 3) × y (# 0) ℝ.> y (# 4)))

abstract
  property6 : ∀ (x : Tensor ℝ (5 ∷ [])) → IntruderFarAway x → AdvisesClearOfConflict x
  property6 = checkProperty record
    { projectFile  = VEHICLE_PROJECT_FILE
    ; propertyUUID = "TODO_propertyUUID"
    }

max_stars_repo_name: wenkokke/vehicle

max_issues_repo_name: wenkokke/vehicle

max_forks_repo_name: wenkokke/vehicle


text:
module JamesChapman where

infixr 50 _⟶_

data Ty : Set where
   ι : Ty
   _⟶_ : Ty -> Ty -> Ty

data Tm : Ty -> Set where
   _$_ : {σ τ : Ty} -> Tm (σ ⟶ τ) -> Tm σ -> Tm τ

data Nf : Ty -> Set where

data _↓_ : {σ : Ty} -> Tm σ -> Nf σ -> Set where
   r$ : {σ τ : Ty} -> {t : Tm (σ ⟶ τ)} -> {f : Nf (σ ⟶ τ)} -> t ↓ f ->
     {u : Tm σ} -> {a : Nf σ} -> u ↓ a -> {v : Nf τ} ->
     t $ u ↓ v

nf* : {σ : Ty} -> (t : Tm σ) -> {n : Nf σ} -> t ↓ n -> Set
nf* .{τ} (_$_ {σ} {τ} t u) {v} (r$ {f = f} p q) with nf* {σ ⟶ τ} t {f} p
nf* (t $ u) (r$ p q)  |   _ = Ty

ext: agda

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --without-K #-}
module sets.vec where

open import sets.vec.core public
open import sets.vec.properties public
open import sets.vec.dependent public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 06-universes where

import 05-identity-types
open 05-identity-types public

-- Section 4.1 Type theoretic universes

{- Because of Agda's design we already had to introduce universes in the very
   first file. What is left to do here is to formalize the examples of
   structured types. -}

-- Pointed types
UU-pt : (i : Level) → UU (lsuc i)
UU-pt i = Σ (UU i) (λ X → X)

-- Graphs
Gph : (i : Level) → UU (lsuc i)
Gph i = Σ (UU i) (λ X → (X → X → (UU i)))

-- Reflexive graphs
rGph : (i : Level) →  UU (lsuc i)
rGph i = Σ (UU i) (λ X → Σ (X → X → (UU i)) (λ R → (x : X) → R x x))

-- Section 4.2 Defining families and relations using a universe

-- Finite sets
Fin : ℕ → UU lzero
Fin zero-ℕ = empty
Fin (succ-ℕ n) = coprod (Fin n) unit

-- Observational equality on the natural numbers
Eq-ℕ : ℕ → (ℕ → UU lzero)
Eq-ℕ zero-ℕ zero-ℕ = 𝟙
Eq-ℕ zero-ℕ (succ-ℕ n) = 𝟘
Eq-ℕ (succ-ℕ m) zero-ℕ = 𝟘
Eq-ℕ (succ-ℕ m) (succ-ℕ n) = Eq-ℕ m n

-- Exercises

-- Exercise 3.1

{- In this exercise we were asked to show that (A + ¬A) implies (¬¬A → A). In
   other words, we get double negation elimination for the types that are
   decidable. -}

is-decidable : {l : Level} (A : UU l) → UU l
is-decidable A = coprod A (¬ A)

double-negation-elim-is-decidable :
  {i : Level} (A : UU i) → is-decidable A → (¬ (¬ A) → A)
double-negation-elim-is-decidable A (inl x) p = x
double-negation-elim-is-decidable A (inr x) p = ind-empty (p x)

-- Exercise 3.3

{- In this exercise we were asked to show that the observational equality on ℕ
   is an equivalence relation. -}

refl-Eq-ℕ : (n : ℕ) → Eq-ℕ n n
refl-Eq-ℕ zero-ℕ = star
refl-Eq-ℕ (succ-ℕ n) = refl-Eq-ℕ n

symmetric-Eq-ℕ : (m n : ℕ) → Eq-ℕ m n → Eq-ℕ n m
symmetric-Eq-ℕ zero-ℕ zero-ℕ t = t
symmetric-Eq-ℕ zero-ℕ (succ-ℕ n) t = t
symmetric-Eq-ℕ (succ-ℕ n) zero-ℕ t = t
symmetric-Eq-ℕ (succ-ℕ m) (succ-ℕ n) t = symmetric-Eq-ℕ m n t

transitive-Eq-ℕ : (l m n : ℕ) → Eq-ℕ l m → Eq-ℕ m n → Eq-ℕ l n
transitive-Eq-ℕ zero-ℕ zero-ℕ zero-ℕ s t = star
transitive-Eq-ℕ (succ-ℕ n) zero-ℕ zero-ℕ s t = ind-empty s
transitive-Eq-ℕ zero-ℕ (succ-ℕ n) zero-ℕ s t = ind-empty s
transitive-Eq-ℕ zero-ℕ zero-ℕ (succ-ℕ n) s t = ind-empty t
transitive-Eq-ℕ (succ-ℕ l) (succ-ℕ m) zero-ℕ s t = ind-empty t
transitive-Eq-ℕ (succ-ℕ l) zero-ℕ (succ-ℕ n) s t = ind-empty s
transitive-Eq-ℕ zero-ℕ (succ-ℕ m) (succ-ℕ n) s t = ind-empty s
transitive-Eq-ℕ (succ-ℕ l) (succ-ℕ m) (succ-ℕ n) s t = transitive-Eq-ℕ l m n s t

-- Exercise 3.4

{- In this exercise we were asked to show that observational equality on the
   natural numbers is the least reflexive relation, in the sense that it
   implies all other reflexive relation. As we will see once we introduce the
   identity type, it follows that observationally equal natural numbers can be
   identified. -}

succ-relation-ℕ :
  {i : Level} (R : ℕ → ℕ → UU i) → ℕ → ℕ → UU i
succ-relation-ℕ R m n = R (succ-ℕ m) (succ-ℕ n)

succ-reflexivity-ℕ :
  {i : Level} (R : ℕ → ℕ → UU i) (ρ : (n : ℕ) → R n n) →
  (n : ℕ) → succ-relation-ℕ R n n
succ-reflexivity-ℕ R ρ n = ρ (succ-ℕ n)

{- In the book we suggest that first the order of the variables should be
   swapped, in order to make the inductive hypothesis stronger. Agda's pattern
   matching mechanism allows us to bypass this step and give a more direct
   construction. -}

least-reflexive-Eq-ℕ :
  {i : Level} (R : ℕ → ℕ → UU i) (ρ : (n : ℕ) → R n n) →
  (m n : ℕ) → Eq-ℕ m n → R m n
least-reflexive-Eq-ℕ R ρ zero-ℕ zero-ℕ star = ρ zero-ℕ
least-reflexive-Eq-ℕ R ρ zero-ℕ (succ-ℕ n) ()
least-reflexive-Eq-ℕ R ρ (succ-ℕ m) zero-ℕ ()
least-reflexive-Eq-ℕ R ρ (succ-ℕ m) (succ-ℕ n) e =
  least-reflexive-Eq-ℕ (succ-relation-ℕ R) (succ-reflexivity-ℕ R ρ) m n e

-- Exercise 3.5

{- In this exercise we were asked to show that any function on the natural
   numbers preserves observational equality. The quick solution uses the fact
   that observational equality is the least reflexive relation. -}

preserve_Eq-ℕ : (f : ℕ → ℕ) (n m : ℕ) → (Eq-ℕ n m) → (Eq-ℕ (f n) (f m))
preserve_Eq-ℕ f =
  least-reflexive-Eq-ℕ
    ( λ x y → Eq-ℕ (f x) (f y))
    ( λ x → refl-Eq-ℕ (f x))

-- Exercise 3.6

{- In this exercise we were asked to construct the relations ≤ and < on the
   natural numbers, and show basic properties about them. -}

-- The definition of ≤

leq-ℕ : ℕ → ℕ → UU lzero
leq-ℕ zero-ℕ m = unit
leq-ℕ (succ-ℕ n) zero-ℕ = empty
leq-ℕ (succ-ℕ n) (succ-ℕ m) = leq-ℕ n m

_≤_ = leq-ℕ

leq-zero-ℕ :
  (n : ℕ) → leq-ℕ zero-ℕ n
leq-zero-ℕ zero-ℕ = star
leq-zero-ℕ (succ-ℕ n) = star

-- The definition of <

le-ℕ : ℕ → ℕ → UU lzero
le-ℕ m zero-ℕ = empty
le-ℕ zero-ℕ (succ-ℕ m) = unit
le-ℕ (succ-ℕ n) (succ-ℕ m) = le-ℕ n m

_<_ = le-ℕ

reflexive-leq-ℕ : (n : ℕ) → n ≤ n
reflexive-leq-ℕ zero-ℕ = star
reflexive-leq-ℕ (succ-ℕ n) = reflexive-leq-ℕ n

anti-reflexive-le-ℕ : (n : ℕ) → ¬ (n < n)
anti-reflexive-le-ℕ zero-ℕ = ind-empty
anti-reflexive-le-ℕ (succ-ℕ n) = anti-reflexive-le-ℕ n

transitive-leq-ℕ :
  (n m l : ℕ) → (n ≤ m) → (m ≤ l) → (n ≤ l)
transitive-leq-ℕ zero-ℕ m l p q = star
transitive-leq-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
  transitive-leq-ℕ n m l p q

transitive-le-ℕ : (n m l : ℕ) → (le-ℕ n m) → (le-ℕ m l) → (le-ℕ n l)
transitive-le-ℕ zero-ℕ (succ-ℕ m) (succ-ℕ l) p q = star
transitive-le-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
  transitive-le-ℕ n m l p q

succ-le-ℕ : (n : ℕ) → le-ℕ n (succ-ℕ n)
succ-le-ℕ zero-ℕ = star
succ-le-ℕ (succ-ℕ n) = succ-le-ℕ n

-- Exercise 3.7

{- With the construction of the divisibility relation we open the door to basic
   number theory. -}

divides : (d n : ℕ) → UU lzero
divides d n = Σ ℕ (λ m → Eq-ℕ (mul-ℕ d m) n)

-- Exercise 3.8

{- In this exercise we were asked to construct observational equality on the
   booleans. This construction is analogous to, but simpler than, the
   construction of observational equality on the natural numbers. -}

Eq-𝟚 : bool → bool → UU lzero
Eq-𝟚 true true = unit
Eq-𝟚 true false = empty
Eq-𝟚 false true = empty
Eq-𝟚 false false = unit

reflexive-Eq-𝟚 : (x : bool) → Eq-𝟚 x x
reflexive-Eq-𝟚 true = star
reflexive-Eq-𝟚 false = star

least-reflexive-Eq-𝟚 : {i : Level}
  (R : bool → bool → UU i) (ρ : (x : bool) → R x x)
  (x y : bool) → Eq-𝟚 x y → R x y
least-reflexive-Eq-𝟚 R ρ true true p = ρ true
least-reflexive-Eq-𝟚 R ρ true false p = ind-empty p
least-reflexive-Eq-𝟚 R ρ false true p = ind-empty p
least-reflexive-Eq-𝟚 R ρ false false p = ρ false

-- Exercise 3.10

{- In this exercise we were asked to define the relations ≤ and < on the
   integers. As a criterion of correctness, we were then also asked to show
   that the type of all integers l satisfying k ≤ l satisfy the induction
   principle of the natural numbers. -}

is-non-negative-ℤ : ℤ → UU lzero
is-non-negative-ℤ (inl x) = empty
is-non-negative-ℤ (inr k) = unit

diff-ℤ : ℤ → ℤ → ℤ
diff-ℤ k l = add-ℤ (neg-ℤ k) l

leq-ℤ : ℤ → ℤ → UU lzero
leq-ℤ k l = is-non-negative-ℤ (diff-ℤ k l)

reflexive-leq-ℤ : (k : ℤ) → leq-ℤ k k
reflexive-leq-ℤ k =
  tr is-non-negative-ℤ (inv (left-inverse-law-add-ℤ k)) star

is-non-negative-succ-ℤ :
  (k : ℤ) → is-non-negative-ℤ k → is-non-negative-ℤ (succ-ℤ k)
is-non-negative-succ-ℤ (inr (inl star)) p = star
is-non-negative-succ-ℤ (inr (inr x)) p = star

is-non-negative-add-ℤ :
  (k l : ℤ) →
  is-non-negative-ℤ k → is-non-negative-ℤ l → is-non-negative-ℤ (add-ℤ k l)
is-non-negative-add-ℤ (inr (inl star)) (inr (inl star)) p q = star
is-non-negative-add-ℤ (inr (inl star)) (inr (inr n)) p q = star
is-non-negative-add-ℤ (inr (inr zero-ℕ)) (inr (inl star)) p q = star
is-non-negative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inl star)) star star =
  is-non-negative-succ-ℤ
    ( add-ℤ (inr (inr n)) (inr (inl star)))
    ( is-non-negative-add-ℤ (inr (inr n)) (inr (inl star)) star star)
is-non-negative-add-ℤ (inr (inr zero-ℕ)) (inr (inr m)) star star = star
is-non-negative-add-ℤ (inr (inr (succ-ℕ n))) (inr (inr m)) star star =
  is-non-negative-succ-ℤ
    ( add-ℤ (inr (inr n)) (inr (inr m)))
    ( is-non-negative-add-ℤ (inr (inr n)) (inr (inr m)) star star)

triangle-diff-ℤ :
  (k l m : ℤ) → Id (add-ℤ (diff-ℤ k l) (diff-ℤ l m)) (diff-ℤ k m)
triangle-diff-ℤ k l m =
  ( associative-add-ℤ (neg-ℤ k) l (diff-ℤ l m)) ∙
  ( ap
    ( add-ℤ (neg-ℤ k))
    ( ( inv (associative-add-ℤ l (neg-ℤ l) m)) ∙
      ( ( ap (λ x → add-ℤ x m) (right-inverse-law-add-ℤ l)) ∙
        ( left-unit-law-add-ℤ m))))

transitive-leq-ℤ : (k l m : ℤ) → leq-ℤ k l → leq-ℤ l m → leq-ℤ k m
transitive-leq-ℤ k l m p q =
  tr is-non-negative-ℤ
    ( triangle-diff-ℤ k l m)
    ( is-non-negative-add-ℤ
      ( add-ℤ (neg-ℤ k) l)
      ( add-ℤ (neg-ℤ l) m)
      ( p)
      ( q))

succ-leq-ℤ : (k : ℤ) → leq-ℤ k (succ-ℤ k)
succ-leq-ℤ k =
  tr is-non-negative-ℤ
    ( inv
      ( ( right-successor-law-add-ℤ (neg-ℤ k) k) ∙
        ( ap succ-ℤ (left-inverse-law-add-ℤ k))))
    ( star)

leq-ℤ-succ-leq-ℤ : (k l : ℤ) → leq-ℤ k l → leq-ℤ k (succ-ℤ l)
leq-ℤ-succ-leq-ℤ k l p = transitive-leq-ℤ k l (succ-ℤ l) p (succ-leq-ℤ l)

is-positive-ℤ : ℤ → UU lzero
is-positive-ℤ k = is-non-negative-ℤ (pred-ℤ k)

le-ℤ : ℤ → ℤ → UU lzero
le-ℤ (inl zero-ℕ) (inl x) = empty
le-ℤ (inl zero-ℕ) (inr y) = unit
le-ℤ (inl (succ-ℕ x)) (inl zero-ℕ) = unit
le-ℤ (inl (succ-ℕ x)) (inl (succ-ℕ y)) = le-ℤ (inl x) (inl y)
le-ℤ (inl (succ-ℕ x)) (inr y) = unit
le-ℤ (inr x) (inl y) = empty
le-ℤ (inr (inl star)) (inr (inl star)) = empty
le-ℤ (inr (inl star)) (inr (inr x)) = unit
le-ℤ (inr (inr x)) (inr (inl star)) = empty
le-ℤ (inr (inr zero-ℕ)) (inr (inr zero-ℕ)) = empty
le-ℤ (inr (inr zero-ℕ)) (inr (inr (succ-ℕ y))) = unit
le-ℤ (inr (inr (succ-ℕ x))) (inr (inr zero-ℕ)) = empty
le-ℤ (inr (inr (succ-ℕ x))) (inr (inr (succ-ℕ y))) =
  le-ℤ (inr (inr x)) (inr (inr y))

-- We prove that the induction principle for ℕ implies strong induction.

zero-ℕ-leq-ℕ :
  (n : ℕ) → leq-ℕ zero-ℕ n
zero-ℕ-leq-ℕ n = star

fam-strong-ind-ℕ :
  { l : Level} → (ℕ → UU l) → ℕ → UU l
fam-strong-ind-ℕ P n = (m : ℕ) → (leq-ℕ m n) → P m

zero-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) → P zero-ℕ → fam-strong-ind-ℕ P zero-ℕ
zero-strong-ind-ℕ P p0 zero-ℕ t = p0
zero-strong-ind-ℕ P p0 (succ-ℕ m) ()

succ-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( k : ℕ) → (fam-strong-ind-ℕ P k) → (fam-strong-ind-ℕ P (succ-ℕ k))
succ-strong-ind-ℕ P pS k f zero-ℕ t = f zero-ℕ (zero-ℕ-leq-ℕ k)
succ-strong-ind-ℕ P pS k f (succ-ℕ m) t =
  pS m (λ m' t' → f m' (transitive-leq-ℕ m' m k t' t))

conclusion-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( ( n : ℕ) → fam-strong-ind-ℕ P n) → (n : ℕ) → P n
conclusion-strong-ind-ℕ P f n = f n n (reflexive-leq-ℕ n)

induction-strong-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( fam-strong-ind-ℕ P zero-ℕ) →
  ( (k : ℕ) → (fam-strong-ind-ℕ P k) → (fam-strong-ind-ℕ P (succ-ℕ k))) →
  ( n : ℕ) → fam-strong-ind-ℕ P n
induction-strong-ind-ℕ P q0 qS zero-ℕ = q0
induction-strong-ind-ℕ P q0 qS (succ-ℕ n) = qS n
  ( induction-strong-ind-ℕ P q0 qS n)

strong-ind-ℕ :
  { l : Level} → (P : ℕ → UU l) (p0 : P zero-ℕ) →
  ( pS : (k : ℕ) → (fam-strong-ind-ℕ P k) → P (succ-ℕ k)) →
  ( n : ℕ) → P n
strong-ind-ℕ P p0 pS =
  conclusion-strong-ind-ℕ P
    ( induction-strong-ind-ℕ P
      ( zero-strong-ind-ℕ P p0)
      ( succ-strong-ind-ℕ P pS))

-- We show that induction on ℕ implies ordinal induction.

fam-ordinal-ind-ℕ :
  { l : Level} → (ℕ → UU l) → ℕ → UU l
fam-ordinal-ind-ℕ P n = (m : ℕ) → (le-ℕ m n) → P m

le-zero-ℕ :
  (m : ℕ) → (le-ℕ m zero-ℕ) → empty
le-zero-ℕ zero-ℕ ()
le-zero-ℕ (succ-ℕ m) ()

zero-ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) → fam-ordinal-ind-ℕ P zero-ℕ
zero-ordinal-ind-ℕ P m t = ind-empty (le-zero-ℕ m t)

le-one-ℕ :
  (n : ℕ) → le-ℕ (succ-ℕ n) one-ℕ → empty
le-one-ℕ zero-ℕ ()
le-one-ℕ (succ-ℕ n) ()

transitive-le-ℕ' :
  (k l m : ℕ) → (le-ℕ k l) → (le-ℕ l (succ-ℕ m)) → le-ℕ k m
transitive-le-ℕ' zero-ℕ zero-ℕ m () s
transitive-le-ℕ' (succ-ℕ k) zero-ℕ m () s
transitive-le-ℕ' zero-ℕ (succ-ℕ l) zero-ℕ star s = ind-empty (le-one-ℕ l s)
transitive-le-ℕ' (succ-ℕ k) (succ-ℕ l) zero-ℕ t s = ind-empty (le-one-ℕ l s)
transitive-le-ℕ' zero-ℕ (succ-ℕ l) (succ-ℕ m) star s = star
transitive-le-ℕ' (succ-ℕ k) (succ-ℕ l) (succ-ℕ m) t s =
  transitive-le-ℕ' k l m t s

succ-ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( (n : ℕ) → (fam-ordinal-ind-ℕ P n) → P n) →
  ( k : ℕ) → fam-ordinal-ind-ℕ P k → fam-ordinal-ind-ℕ P (succ-ℕ k)
succ-ordinal-ind-ℕ P f k g m t =
  f m (λ m' t' → g m' (transitive-le-ℕ' m' m k t' t))

induction-ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( qS : (k : ℕ) → fam-ordinal-ind-ℕ P k → fam-ordinal-ind-ℕ P (succ-ℕ k))
  ( n : ℕ) → fam-ordinal-ind-ℕ P n
induction-ordinal-ind-ℕ P qS zero-ℕ = zero-ordinal-ind-ℕ P
induction-ordinal-ind-ℕ P qS (succ-ℕ n) =
  qS n (induction-ordinal-ind-ℕ P qS n)

conclusion-ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  (( n : ℕ) → fam-ordinal-ind-ℕ P n) → (n : ℕ) → P n
conclusion-ordinal-ind-ℕ P f n = f (succ-ℕ n) n (succ-le-ℕ n)

ordinal-ind-ℕ :
  { l : Level} (P : ℕ → UU l) →
  ( (n : ℕ) → (fam-ordinal-ind-ℕ P n) → P n) →
  ( n : ℕ) → P n
ordinal-ind-ℕ P f =
  conclusion-ordinal-ind-ℕ P
    ( induction-ordinal-ind-ℕ P (succ-ordinal-ind-ℕ P f))

-- Extra material

-- We show that ℕ is an ordered semi-ring

leq-eq-ℕ : {m m' n n' : ℕ} → Id m m' → Id n n' → leq-ℕ m n → leq-ℕ m' n'
leq-eq-ℕ refl refl = id

right-law-leq-add-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (add-ℕ k m) (add-ℕ k n)
right-law-leq-add-ℕ zero-ℕ m n = id
right-law-leq-add-ℕ (succ-ℕ k) m n H = right-law-leq-add-ℕ k m n H

left-law-leq-add-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (add-ℕ m k) (add-ℕ n k)
left-law-leq-add-ℕ k m n H =
  leq-eq-ℕ
    ( commutative-add-ℕ k m)
    ( commutative-add-ℕ k n)
    ( right-law-leq-add-ℕ k m n H)

preserves-leq-add-ℕ :
  {m m' n n' : ℕ} → leq-ℕ m m' → leq-ℕ n n' → leq-ℕ (add-ℕ m n) (add-ℕ m' n')
preserves-leq-add-ℕ {m} {m'} {n} {n'} H K =
  transitive-leq-ℕ
    ( add-ℕ m n)
    ( add-ℕ m' n)
    ( add-ℕ m' n')
    ( left-law-leq-add-ℕ n m m' H)
    ( right-law-leq-add-ℕ m' n n' K)

right-law-leq-mul-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (mul-ℕ k m) (mul-ℕ k n)
right-law-leq-mul-ℕ zero-ℕ m n H = star
right-law-leq-mul-ℕ (succ-ℕ k) m n H =
  preserves-leq-add-ℕ
    { m = mul-ℕ k m}
    { m' = mul-ℕ k n}
    ( right-law-leq-mul-ℕ k m n H) H

left-law-leq-mul-ℕ : (k m n : ℕ) → leq-ℕ m n → leq-ℕ (mul-ℕ m k) (mul-ℕ n k)
left-law-leq-mul-ℕ k m n H =
  leq-eq-ℕ
    ( commutative-mul-ℕ k m)
    ( commutative-mul-ℕ k n)
    ( right-law-leq-mul-ℕ k m n H)

-- We show that ℤ is an ordered ring

{-
leq-add-ℤ : (m k l : ℤ) → leq-ℤ k l → leq-ℤ (add-ℤ m k) (add-ℤ m l)
leq-add-ℤ (inl zero-ℕ) k l H = {!!}
leq-add-ℤ (inl (succ-ℕ x)) k l H = {!!}
leq-add-ℤ (inr m) k l H = {!!}
-}

-- Section 5.5 Identity systems

succ-fam-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i) →
  (m n : ℕ) → Eq-ℕ m n → UU i
succ-fam-Eq-ℕ R m n e = R (succ-ℕ m) (succ-ℕ n) e

succ-refl-fam-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  (ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  (n : ℕ) → (succ-fam-Eq-ℕ R n n (refl-Eq-ℕ n))
succ-refl-fam-Eq-ℕ R ρ n = ρ (succ-ℕ n)

path-ind-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  ( ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  ( m n : ℕ) (e : Eq-ℕ m n) → R m n e
path-ind-Eq-ℕ R ρ zero-ℕ zero-ℕ star = ρ zero-ℕ
path-ind-Eq-ℕ R ρ zero-ℕ (succ-ℕ n) ()
path-ind-Eq-ℕ R ρ (succ-ℕ m) zero-ℕ ()
path-ind-Eq-ℕ R ρ (succ-ℕ m) (succ-ℕ n) e =
  path-ind-Eq-ℕ (succ-fam-Eq-ℕ R) (succ-refl-fam-Eq-ℕ R ρ) m n e

comp-path-ind-Eq-ℕ :
  {i : Level} (R : (m n : ℕ) → Eq-ℕ m n → UU i)
  ( ρ : (n : ℕ) → R n n (refl-Eq-ℕ n)) →
  ( n : ℕ) → Id (path-ind-Eq-ℕ R ρ n n (refl-Eq-ℕ n)) (ρ n)
comp-path-ind-Eq-ℕ R ρ zero-ℕ = refl
comp-path-ind-Eq-ℕ R ρ (succ-ℕ n) =
  comp-path-ind-Eq-ℕ (succ-fam-Eq-ℕ R) (succ-refl-fam-Eq-ℕ R ρ) n

max_stars_repo_name: tadejpetric/HoTT-Intro

max_issues_repo_name: tadejpetric/HoTT-Intro

max_forks_repo_name: tadejpetric/HoTT-Intro


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

module Cubical.Categories.NaturalTransformation where

open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category
open import Cubical.Categories.Functor

private
  variable
    ℓ𝒞 ℓ𝒞' ℓ𝒟 ℓ𝒟' : Level

module _ {𝒞 : Precategory ℓ𝒞 ℓ𝒞'} {𝒟 : Precategory ℓ𝒟 ℓ𝒟'} where
  record NatTrans (F G : Functor 𝒞 𝒟) : Type (ℓ-max (ℓ-max ℓ𝒞 ℓ𝒞') (ℓ-max ℓ𝒟 ℓ𝒟')) where
    open Precategory
    open Functor

    field
      N-ob : (x : 𝒞 .ob) → 𝒟 .hom (F .F-ob x) (G .F-ob x)
      N-hom : {x y : 𝒞 .ob} (f : 𝒞 .hom x y) → 𝒟 .seq (F .F-hom f) (N-ob y) ≡ 𝒟 .seq (N-ob x) (G .F-hom f)

  open Precategory
  open Functor
  open NatTrans

  id-trans : (F : Functor 𝒞 𝒟) → NatTrans F F
  id-trans F .N-ob x = 𝒟 .idn (F .F-ob x)
  id-trans F .N-hom f =
     𝒟 .seq (F .F-hom f) (id-trans F .N-ob _)
       ≡⟨ 𝒟 .seq-ρ _ ⟩
     F .F-hom f
       ≡⟨ sym (𝒟 .seq-λ _) ⟩
     𝒟 .seq (𝒟 .idn (F .F-ob _)) (F .F-hom f)
       ∎

  seq-trans : {F G H : Functor 𝒞 𝒟} (α : NatTrans F G) (β : NatTrans G H) → NatTrans F H
  seq-trans α β .N-ob x = 𝒟 .seq (α .N-ob x) (β .N-ob x)
  seq-trans {F} {G} {H} α β .N-hom f =
    𝒟 .seq (F .F-hom f) (𝒟 .seq (α .N-ob _) (β .N-ob _))
      ≡⟨ sym (𝒟 .seq-α _ _ _) ⟩
    𝒟 .seq (𝒟 .seq (F .F-hom f) (α .N-ob _)) (β .N-ob _)
      ≡[ i ]⟨ 𝒟 .seq (α .N-hom f i) (β .N-ob _) ⟩
    𝒟 .seq (𝒟 .seq (α .N-ob _) (G .F-hom f)) (β .N-ob _)
      ≡⟨ 𝒟 .seq-α _ _ _ ⟩
    𝒟 .seq (α .N-ob _) (𝒟 .seq (G .F-hom f) (β .N-ob _))
      ≡[ i ]⟨ 𝒟 .seq (α .N-ob _) (β .N-hom f i) ⟩
    𝒟 .seq (α .N-ob _) (𝒟 .seq (β .N-ob _) (H .F-hom f))
      ≡⟨ sym (𝒟 .seq-α _ _ _) ⟩
    𝒟 .seq (𝒟 .seq (α .N-ob _) (β .N-ob _)) (H .F-hom f)
      ∎

  module _  ⦃ 𝒟-category : isCategory 𝒟 ⦄ {F G : Functor 𝒞 𝒟} {α β : NatTrans F G} where
    open Precategory
    open Functor
    open NatTrans

    make-nat-trans-path : α .N-ob ≡ β .N-ob → α ≡ β
    make-nat-trans-path p i .N-ob = p i
    make-nat-trans-path p i .N-hom f = rem i
      where
        rem : PathP (λ i → 𝒟 .seq (F .F-hom f) (p i _) ≡ 𝒟 .seq (p i _) (G .F-hom f)) (α .N-hom f) (β .N-hom f)
        rem = toPathP (𝒟-category .homIsSet _ _ _ _)

module _ (𝒞 : Precategory ℓ𝒞 ℓ𝒞') (𝒟 : Precategory ℓ𝒟 ℓ𝒟') ⦃ _ : isCategory 𝒟 ⦄ where
  open Precategory
  open NatTrans
  open Functor

  FUNCTOR : Precategory (ℓ-max (ℓ-max ℓ𝒞 ℓ𝒞') (ℓ-max ℓ𝒟 ℓ𝒟')) (ℓ-max (ℓ-max ℓ𝒞 ℓ𝒞') (ℓ-max ℓ𝒟 ℓ𝒟'))
  FUNCTOR .ob = Functor 𝒞 𝒟
  FUNCTOR .hom = NatTrans
  FUNCTOR .idn = id-trans
  FUNCTOR .seq = seq-trans
  FUNCTOR .seq-λ α = make-nat-trans-path λ i x → 𝒟 .seq-λ (α .N-ob x) i
  FUNCTOR .seq-ρ α = make-nat-trans-path λ i x → 𝒟 .seq-ρ (α .N-ob x) i
  FUNCTOR .seq-α α β γ = make-nat-trans-path λ i x → 𝒟 .seq-α (α .N-ob x) (β .N-ob x) (γ .N-ob x) i

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
-- {-# OPTIONS -v tc.with:40 #-}

id : (A : Set) → A → A
id A = {!id′!}
 -- C-c C-h produces:       id′ : ∀ {A} → A
 -- when it should produce: id′ : ∀ {A} → A → A

max_stars_repo_name: larrytheliquid/agda


text:
-- Andreas, 2016-01-23, issue 1796
-- Need to run size constraint solver before with-abstraction

open import Common.Size

postulate
  anything : ∀{A : Set} → A

mutual

  record IO i : Set where
    coinductive
    field force : ∀{j : Size< i} → IO' j

  data IO' i : Set where
    cons : IO i → IO' i

mutual

  record All i (s : IO ∞) : Set where
    field force : ∀{j : Size< i} → All' j (IO.force s)

  data All' i : (s : IO' ∞) → Set where
    always  : ∀ e → All' i (cons e)

runIO  : ∀{i} (s : IO ∞) → IO i
IO.force (runIO s) with IO.force s
... | cons e = cons e

-- With abstraction fails when _ in IO.force s {_}
-- has not been solved to ∞.

test : ∀ i s → All i (runIO s)
All.force (test i s) with IO.force s -- works with {∞} added
All.force (test i s) | cons e = always e

-- cons e != IO.force (runIO {∞} s) {∞} | IO.force s of type IO' ∞
-- when checking that the expression always e has type
-- All' .j (IO.force (runIO {∞} s) {∞} | IO.force s)


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

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

open import Functions.Definition

module Sets.EquivalenceRelations where

Reflexive : {a b : _} {A : Set a} (r : Rel {a} {b} A) → Set (a ⊔ b)
Reflexive {A = A} r = {x : A} → r x x

Symmetric : {a b : _} {A : Set a} (r : Rel {a} {b} A) → Set (a ⊔ b)
Symmetric {A = A} r = {x y : A} → r x y → r y x

Transitive : {a b : _} {A : Set a} (r : Rel {a} {b} A) → Set (a ⊔ b)
Transitive {A = A} r = {x y z : A} → r x y → r y z → r x z

record Equivalence {a b : _} {A : Set a} (r : Rel {a} {b} A) : Set (a ⊔ lsuc b) where
  field
    reflexive : Reflexive r
    symmetric : Symmetric r
    transitive : Transitive r
    -- See https://lists.chalmers.se/pipermail/agda/2016/009090.html
  transitive' : {x y z : A} → r y z → r x y → r x z
  transitive' p2 p1 = transitive p1 p2


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

open import LogicalFormulae
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Lists.Lists
open import Numbers.Primes.PrimeNumbers
open import Decidable.Relations
open import Numbers.BinaryNaturals.Definition
open import Numbers.BinaryNaturals.Addition

module ProjectEuler.Problem1 where

numbers<N : (N : ℕ) → List ℕ
numbers<N zero = []
numbers<N (succ N) = N :: numbers<N N

filtered : (N : ℕ) → List ℕ
filtered N = filter' (orDecidable (divisionDecidable 3) (divisionDecidable 5)) (numbers<N N)

ans : ℕ → ℕ
ans n = binNatToN (fold _+B_ (NToBinNat 0) (map NToBinNat (filtered n)))

t : ans 10 ≡ 23
t = refl

--q : ans 1000 ≡ {!233168!} -- takes about 15secs for me to reduce the term that fills this hole
--q = refl


text:
{-# OPTIONS --without-K  #-}
module equality.inspect where

open import level
open import equality.core

data _of_is_ {i j}{A : Set i}{B : A → Set j}
            (f : (x : A) → B x)(x : A)(y : B x) : Set (i ⊔ j) where
  [_] : f x ≡ y → f of x is y

inspect : ∀ {i j}{A : Set i}{B : A → Set j}
        → (f : (x : A)→ B x)(x : A)
        → f of x is f x
inspect f x = [ refl ]

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
------------------------------------------------------------------------
-- Equivalence relations
------------------------------------------------------------------------

module Eq where

infix 4 _≡_

------------------------------------------------------------------------
-- Definition

record Equiv {a : Set} (_≈_ : a -> a -> Set) : Set where
  field
    refl      : forall x       -> x ≈ x
    sym       : forall {x y}   -> x ≈ y -> y ≈ x
    _`trans`_ : forall {x y z} -> x ≈ y -> y ≈ z -> x ≈ z

------------------------------------------------------------------------
-- Propositional equality

data _≡_ {a : Set} (x : a) : a -> Set where
  refl : x ≡ x

subst : forall {a x y} ->
  (P : a -> Set) -> x ≡ y -> P x -> P y
subst _ refl p = p

cong : forall {a b x y} ->
  (f : a -> b) -> x ≡ y -> f x ≡ f y
cong _ refl = refl

Equiv-≡ : forall {a} -> Equiv {a} _≡_
Equiv-≡ {a} =
  record { refl      = \_ -> refl
         ; sym       = sym
         ; _`trans`_ = _`trans`_
         }
  where
  sym : {x y : a} -> x ≡ y -> y ≡ x
  sym refl = refl

  _`trans`_ : {x y z : a} -> x ≡ y -> y ≡ z -> x ≡ z
  refl `trans` refl = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module Explore.Examples where

open import Type
open import Level.NP
open import Data.Maybe.NP
open import Data.List
open import Data.Zero
open import Data.One
open import Data.Two
open import Data.Product
open import Data.Sum.NP
open import HoTT using (UA)
open import Function.NP
open import Function.Extensionality using (FunExt)
open import Relation.Binary.PropositionalEquality hiding ([_])

open import Explore.Core
open import Explore.Explorable
open import Explore.Universe.Type {𝟘}
open import Explore.Universe.Base
open import Explore.Monad {₀} ₀ public renaming (map to map-explore)
open import Explore.Two
open import Explore.Product
open Explore.Product.Operators

module E where
  open FromExplore public

module M {Msg Digest : ★}
         (_==_ : Digest → Digest → 𝟚)
         (H : Msg → Digest)
         (exploreMsg : ∀ {ℓ} → Explore ℓ Msg)
         (d : Digest) where

  module V1 where
    list-H⁻¹ : List Msg
    list-H⁻¹ = exploreMsg [] _++_ (λ m → [0: [] 1: [ m ] ] (H m == d))

  module ExploreMsg = FromExplore {A = Msg} exploreMsg

  module V2 where
    first-H⁻¹ : Maybe Msg
    first-H⁻¹ = ExploreMsg.findKey (λ m → H m == d)

  module V3 where
    explore-H⁻¹ : Explore ₀ Msg
    explore-H⁻¹ ε _⊕_ f = exploreMsg ε _⊕_ (λ m → [0: ε 1: f m ] (H m == d))

  module V4 where
    explore-H⁻¹ : Explore ₀ Msg
    explore-H⁻¹ = exploreMsg >>= λ m → [0: empty-explore 1: point-explore m ] (H m == d)

  module V5 where

    explore-H⁻¹ : ∀ {ℓ} → Explore ℓ Msg
    explore-H⁻¹ = filter-explore (λ m → H m == d) exploreMsg

    list-H⁻¹ : List Msg
    list-H⁻¹ = E.list explore-H⁻¹

    first-H⁻¹ : Maybe Msg
    first-H⁻¹ = E.first explore-H⁻¹

  module V6 where
    explore-H⁻¹ : ∀ {ℓ} → Explore ℓ Msg
    explore-H⁻¹ = explore-endo (filter-explore (λ m → H m == d) exploreMsg)

    list-H⁻¹ : List Msg
    list-H⁻¹ = E.list explore-H⁻¹

    first-H⁻¹ : Maybe Msg
    first-H⁻¹ = E.first explore-H⁻¹

    last-H⁻¹ : Maybe Msg
    last-H⁻¹ = E.last explore-H⁻¹

Msg = 𝟚 × 𝟚
Digest = 𝟚
-- _==_ : Digest → Digest → 𝟚
H : Msg → Digest
H (x , y) = x xor y
Msgᵉ : ∀ {ℓ} → Explore ℓ Msg
Msgᵉ = 𝟚ᵉ ×ᵉ 𝟚ᵉ
module N5 = M.V5 _==_ H Msgᵉ
module N6 = M.V6 _==_ H Msgᵉ
test5 = N5.list-H⁻¹
test6-list : N6.list-H⁻¹ 0₂ ≡ (0₂ , 0₂) ∷ (1₂ , 1₂) ∷ []
test6-list = refl
test6-rev-list : E.list (E.backward (N6.explore-H⁻¹ 0₂)) ≡ (1₂ , 1₂) ∷ (0₂ , 0₂) ∷ []
test6-rev-list = refl
test6-first : N6.first-H⁻¹ 0₂ ≡ just (0₂ , 0₂)
test6-first = refl
test6-last : N6.last-H⁻¹ 0₂ ≡ just (1₂ , 1₂)
test6-last = refl
-- -}

𝟛ᵁ : U
𝟛ᵁ = 𝟙ᵁ ⊎ᵁ 𝟚ᵁ

prop-∧-comm : 𝟚 × 𝟚 → 𝟚
prop-∧-comm (x , y) = x ∧ y == y ∧ x

module _ {{_ : UA}}{{_ : FunExt}} where
  check-∧-comm : ∀ x y → ✓ (x ∧ y == y ∧ x)
  check-∧-comm x y = check! (𝟚ᵁ ×ᵁ 𝟚ᵁ) prop-∧-comm (x , y)

prop-∧-∨-distr : 𝟚 × 𝟚 × 𝟚 → 𝟚
prop-∧-∨-distr (x , y , z) = x ∧ (y ∨ z) == x ∧ y ∨ x ∧ z

module _ {{_ : UA}}{{_ : FunExt}} where
  check-∧-∨-distr : ∀ x y z → ✓ (x ∧ (y ∨ z) == x ∧ y ∨ x ∧ z)
  check-∧-∨-distr x y z =
    check! (𝟚ᵁ ×ᵁ 𝟚ᵁ ×ᵁ 𝟚ᵁ) prop-∧-∨-distr (x , y , z)

list22 = list (𝟚ᵁ →ᵁ 𝟚ᵁ)
list33 = list (𝟛ᵁ →ᵁ 𝟛ᵁ)

{-
module _ {{_ : UA}}{{_ : FunExt}} where
  module _ (fᵁ : El (𝟚ᵁ →ᵁ 𝟚ᵁ)) x where
    f = →ᵁ→→ 𝟚ᵁ 𝟚ᵁ fᵁ
    check22 : ✓ (f x == f (f (f x)))
    check22 = check! ((𝟚ᵁ →ᵁ 𝟚ᵁ) ×ᵁ 𝟚ᵁ) (λ { (f , x) → let f' = →ᵁ→→ 𝟚ᵁ 𝟚ᵁ f in f' x == f' (f' (f' x)) }) {{!!}} ((f 0₂ , f 1₂) , x)
  {-
  check22 : ∀ (f : 𝟚 → 𝟚) x → ✓ (f x == f (f (f x)))
  check22 f x = let k = check! ((𝟚ᵁ →ᵁ 𝟚ᵁ) ×ᵁ 𝟚ᵁ) (λ { (f , x) → let f' = →ᵁ→→ 𝟚ᵁ 𝟚ᵁ f in f' x == f' (f' (f' x)) }) {{!!}} ((f 0₂ , f 1₂) , x) in {!k!}
-- -}
-- -}
-- -}
-- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Esterel.Context.Properties where

open import Esterel.Lang
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open import Data.List
  using (List ; _∷_ ; [] ; map ; _++_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; proj₁ ; proj₂ ; _×_ ; _,′_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; sym ; cong ; subst ; trans)

open _≐_⟦_⟧e
open _≐_⟦_⟧c
open EvaluationContext1
open Context1

plug : ∀{p E q} → E ⟦ q ⟧e ≡ p → p ≐ E ⟦ q ⟧e
plug {E = []}             refl = dehole
plug {E = epar₁ q ∷ E}    refl = depar₁    (plug {E = E} refl)
plug {E = epar₂ p₁ ∷ E}   refl = depar₂    (plug {E = E} refl)
plug {E = eseq q ∷ E}     refl = deseq     (plug {E = E} refl)
plug {E = eloopˢ q ∷ E}   refl = deloopˢ   (plug {E = E} refl)
plug {E = esuspend S ∷ E} refl = desuspend (plug {E = E} refl)
plug {E = etrap ∷ E}      refl = detrap    (plug {E = E} refl)

unplug : ∀{p E q} → p ≐ E ⟦ q ⟧e → E ⟦ q ⟧e ≡ p
unplug dehole                           = refl
unplug (depar₁ eq)    rewrite unplug eq = refl
unplug (depar₂ eq)    rewrite unplug eq = refl
unplug (deseq eq)     rewrite unplug eq = refl
unplug (deloopˢ eq)   rewrite unplug eq = refl
unplug (desuspend eq) rewrite unplug eq = refl
unplug (detrap eq)    rewrite unplug eq = refl

plugc : ∀ {C q p} → C ⟦ q ⟧c ≡ p → p ≐ C ⟦ q ⟧c
plugc {[]}                     refl = dchole
plugc {ceval (epar₁ q) ∷ C}    refl = dcpar₁     (plugc {C} refl)
plugc {ceval (epar₂ p) ∷ C}    refl = dcpar₂     (plugc {C} refl)
plugc {ceval (eseq q) ∷ C}     refl = dcseq₁     (plugc {C} refl)
plugc {ceval (eloopˢ q) ∷ C}   refl = dcloopˢ₁   (plugc {C} refl)
plugc {ceval (esuspend S) ∷ C} refl = dcsuspend  (plugc {C} refl)
plugc {ceval etrap ∷ C}        refl = dctrap     (plugc {C} refl)
plugc {csignl S ∷ C}           refl = dcsignl    (plugc {C} refl)
plugc {cpresent₁ S q ∷ C}      refl = dcpresent₁ (plugc {C} refl)
plugc {cpresent₂ S p ∷ C}      refl = dcpresent₂ (plugc {C} refl)
plugc {cloop ∷ C}              refl = dcloop     (plugc {C} refl)
plugc {cloopˢ₂ p ∷ C}          refl = dcloopˢ₂   (plugc {C} refl)
plugc {cseq₂ p ∷ C}            refl = dcseq₂     (plugc {C} refl)
plugc {cshared s e ∷ C}        refl = dcshared   (plugc {C} refl)
plugc {cvar x e ∷ C}           refl = dcvar      (plugc {C} refl)
plugc {cif₁ x q ∷ C}           refl = dcif₁      (plugc {C} refl)
plugc {cif₂ x p ∷ C}           refl = dcif₂      (plugc {C} refl)
plugc {cenv θ A ∷ C}           refl = dcenv      (plugc {C} refl)

unplugc : ∀{p C q} → p ≐ C ⟦ q ⟧c → C ⟦ q ⟧c ≡ p
unplugc dchole                             = refl
unplugc (dcpar₁ eq)     rewrite unplugc eq = refl
unplugc (dcpar₂ eq)     rewrite unplugc eq = refl
unplugc (dcseq₁ eq)     rewrite unplugc eq = refl
unplugc (dcseq₂ eq)     rewrite unplugc eq = refl
unplugc (dcsuspend eq)  rewrite unplugc eq = refl
unplugc (dctrap eq)     rewrite unplugc eq = refl
unplugc (dcsignl eq)    rewrite unplugc eq = refl
unplugc (dcpresent₁ eq) rewrite unplugc eq = refl
unplugc (dcpresent₂ eq) rewrite unplugc eq = refl
unplugc (dcloop eq)     rewrite unplugc eq = refl
unplugc (dcloopˢ₁ eq)   rewrite unplugc eq = refl
unplugc (dcloopˢ₂ eq)   rewrite unplugc eq = refl
unplugc (dcshared eq)   rewrite unplugc eq = refl
unplugc (dcvar eq)      rewrite unplugc eq = refl
unplugc (dcif₁ eq)      rewrite unplugc eq = refl
unplugc (dcif₂ eq)      rewrite unplugc eq = refl
unplugc (dcenv eq)      rewrite unplugc eq = refl

plug-sym : ∀{E E' p q} → E ⟦ p ⟧e ≐ E' ⟦ q ⟧e → E' ⟦ q ⟧e ≐ E ⟦ p ⟧e
plug-sym eq = plug (sym (unplug eq))

unplug-eq : ∀{p q r E} → p ≐ E ⟦ q ⟧e → p ≐ E ⟦ r ⟧e → q ≡ r
unplug-eq dehole          dehole          = refl
unplug-eq (depar₁ qeq)    (depar₁ req)    = unplug-eq qeq req
unplug-eq (depar₂ qeq)    (depar₂ req)    = unplug-eq qeq req
unplug-eq (deseq qeq)     (deseq req)     = unplug-eq qeq req
unplug-eq (deloopˢ qeq)   (deloopˢ req)   = unplug-eq qeq req
unplug-eq (desuspend qeq) (desuspend req) = unplug-eq qeq req
unplug-eq (detrap qeq)    (detrap req)    = unplug-eq qeq req

plug-eq : ∀{p q r E} → p ≐ E ⟦ r ⟧e → q ≐ E ⟦ r ⟧e → p ≡ q
plug-eq peq qeq = trans (sym (unplug peq)) (unplug qeq)

Erefl : ∀{E p} → E ⟦ p ⟧e ≐ E ⟦ p ⟧e
Erefl = plug refl

Crefl : ∀{C p} → C ⟦ p ⟧c ≐ C ⟦ p ⟧c
Crefl = plugc refl

⟦⟧e-to-⟦⟧c : ∀ {E p q} -> p ≐ E ⟦ q ⟧e -> p ≐ (map ceval E) ⟦ q ⟧c
⟦⟧e-to-⟦⟧c dehole             = dchole
⟦⟧e-to-⟦⟧c (depar₁ decomp)    = dcpar₁    (⟦⟧e-to-⟦⟧c decomp)
⟦⟧e-to-⟦⟧c (depar₂ decomp)    = dcpar₂    (⟦⟧e-to-⟦⟧c decomp)
⟦⟧e-to-⟦⟧c (deseq decomp)     = dcseq₁    (⟦⟧e-to-⟦⟧c decomp)
⟦⟧e-to-⟦⟧c (deloopˢ decomp)   = dcloopˢ₁  (⟦⟧e-to-⟦⟧c decomp)
⟦⟧e-to-⟦⟧c (desuspend decomp) = dcsuspend (⟦⟧e-to-⟦⟧c decomp)
⟦⟧e-to-⟦⟧c (detrap decomp)    = dctrap    (⟦⟧e-to-⟦⟧c decomp)

⟦⟧c-to-⟦⟧e : ∀ {E p q} → p ≐ (map ceval E) ⟦ q ⟧c → p ≐ E ⟦ q ⟧e
⟦⟧c-to-⟦⟧e {[]}    dchole             = dehole
⟦⟧c-to-⟦⟧e {_ ∷ _} (dcpar₁ p≐E⟦q⟧)    = depar₁    (⟦⟧c-to-⟦⟧e p≐E⟦q⟧)
⟦⟧c-to-⟦⟧e {_ ∷ _} (dcpar₂ p≐E⟦q⟧)    = depar₂    (⟦⟧c-to-⟦⟧e p≐E⟦q⟧)
⟦⟧c-to-⟦⟧e {_ ∷ _} (dcseq₁ p≐E⟦q⟧)    = deseq     (⟦⟧c-to-⟦⟧e p≐E⟦q⟧)
⟦⟧c-to-⟦⟧e {_ ∷ _} (dcloopˢ₁ p≐E⟦q⟧)  = deloopˢ   (⟦⟧c-to-⟦⟧e p≐E⟦q⟧)
⟦⟧c-to-⟦⟧e {_ ∷ _} (dcsuspend p≐E⟦q⟧) = desuspend (⟦⟧c-to-⟦⟧e p≐E⟦q⟧)
⟦⟧c-to-⟦⟧e {_ ∷ _} (dctrap p≐E⟦q⟧)    = detrap    (⟦⟧c-to-⟦⟧e p≐E⟦q⟧)

C++ : ∀ {C1 C2 p1 p2 p3} ->
  p1 ≐ C1 ⟦ p2 ⟧c ->
  p2 ≐ C2 ⟦ p3 ⟧c ->
  p1 ≐ C1 ++ C2 ⟦ p3 ⟧c
C++ dchole p2C = p2C
C++ (dcpar₁ p1C) p2C = dcpar₁ (C++ p1C p2C)
C++ (dcpar₂ p1C) p2C = dcpar₂ (C++ p1C p2C)
C++ (dcseq₁ p1C) p2C = dcseq₁ (C++ p1C p2C)
C++ (dcseq₂ p1C) p2C = dcseq₂ (C++ p1C p2C)
C++ (dcsuspend p1C) p2C = dcsuspend (C++ p1C p2C)
C++ (dctrap p1C) p2C = dctrap (C++ p1C p2C)
C++ (dcsignl p1C) p2C = dcsignl (C++ p1C p2C)
C++ (dcpresent₁ p1C) p2C = dcpresent₁ (C++ p1C p2C)
C++ (dcpresent₂ p1C) p2C = dcpresent₂ (C++ p1C p2C)
C++ (dcloop p1C) p2C = dcloop (C++ p1C p2C)
C++ (dcloopˢ₁ p1C) p2C = dcloopˢ₁ (C++ p1C p2C)
C++ (dcloopˢ₂ p1C) p2C = dcloopˢ₂ (C++ p1C p2C)
C++ (dcshared p1C) p2C = dcshared (C++ p1C p2C)
C++ (dcvar p1C) p2C = dcvar (C++ p1C p2C)
C++ (dcif₁ p1C) p2C = dcif₁ (C++ p1C p2C)
C++ (dcif₂ p1C) p2C = dcif₂ (C++ p1C p2C)
C++ (dcenv p1C) p2C = dcenv (C++ p1C p2C)

++-is-nesting : ∀ C′ C q ->
 (C′ ++ C) ⟦ q ⟧c ≐ C′ ⟦ C ⟦ q ⟧c ⟧c
++-is-nesting [] C q = dchole
++-is-nesting (ceval (epar₁ q) ∷ C′) C q₁ = dcpar₁ (++-is-nesting C′ C q₁)
++-is-nesting (ceval (epar₂ p) ∷ C′) C q = dcpar₂ (++-is-nesting C′ C q)
++-is-nesting (ceval (eseq q) ∷ C′) C q₁ = dcseq₁ (++-is-nesting C′ C q₁)
++-is-nesting (ceval (eloopˢ q) ∷ C′) C q₁ = dcloopˢ₁ (++-is-nesting C′ C q₁)
++-is-nesting (ceval (esuspend S) ∷ C′) C q = dcsuspend (++-is-nesting C′ C q)
++-is-nesting (ceval etrap ∷ C′) C q = dctrap (++-is-nesting C′ C q)
++-is-nesting (csignl S ∷ C′) C q = dcsignl (++-is-nesting C′ C q)
++-is-nesting (cpresent₁ S q ∷ C′) C q₁ = dcpresent₁ (++-is-nesting C′ C q₁)
++-is-nesting (cpresent₂ S p ∷ C′) C q = dcpresent₂ (++-is-nesting C′ C q)
++-is-nesting (cloop ∷ C′) C q = dcloop (++-is-nesting C′ C q)
++-is-nesting (cloopˢ₂ p ∷ C′) C q = dcloopˢ₂ (++-is-nesting C′ C q)
++-is-nesting (cseq₂ p ∷ C′) C q = dcseq₂ (++-is-nesting C′ C q)
++-is-nesting (cshared s e ∷ C′) C q = dcshared (++-is-nesting C′ C q)
++-is-nesting (cvar x e ∷ C′) C q = dcvar (++-is-nesting C′ C q)
++-is-nesting (cif₁ x q ∷ C′) C q₁ = dcif₁ (++-is-nesting C′ C q₁)
++-is-nesting (cif₂ x p ∷ C′) C q = dcif₂ (++-is-nesting C′ C q)
++-is-nesting (cenv θ A ∷ C′) C q = dcenv (++-is-nesting C′ C q)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module RMonads.Modules where

open import Library
open import Categories
open import Functors
open import RMonads

record Mod {a}{b}{c}{d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D}
           (RM : RMonad J) : Set (a ⊔ c ⊔ d) where
  constructor mod
  open Cat
  open Fun
  open RMonad RM
  field M       : Obj C → Obj D
        mbind   : ∀ {X Y} → Hom D (OMap J X) (T Y) → Hom D (M X) (M Y)
        laweta  : ∀{X} → mbind (η {X}) ≅ iden D {M X}
        lawbind : ∀{X Y Z}
                  {f : Hom D (OMap J X) (T Y)}{g : Hom D (OMap J Y) (T Z)} →
                  mbind (comp D (bind g) f) ≅ comp D (mbind g) (mbind f)

-- any rel. monad is trivially a module over its J.
ModJ : forall {a}{b}{c}{d}{C : Cat {a}{b}}{D : Cat {c}{d}}
       {J : Fun C D} (RM : RMonad J) -> Mod (trivRM J)
ModJ {D = D}{J = J} RM =
  mod T
      (\ f -> bind (comp η f))
      (trans (cong bind idr) law1)
      (trans (cong bind (trans (trans (sym ass)
                                      (cong (\ g -> comp g _) (sym law2)))
                               ass))
             law3)
  where open Fun J; open RMonad RM; open Cat D

open import Functors.FullyFaithful
open import Isomorphism
-- if J is fully faithful then any suitably typed functor is a module for trivial rel monad given by J
ModF : forall {a}{b}{c}{d}{C : Cat {a}{b}}{D : Cat {c}{d}}
       {J : Fun C D} → Full J → Faithful J → (F : Fun C D) -> Mod (trivRM J)
ModF {C = C}{D = D}{J = J} P Q F = mod
  (OMap F)
  (λ f → HMap F (fst (P f)))
  (trans (cong (HMap F) (Q (trans (snd (P (Cat.iden D))) (sym $ fid J)))) (fid F))
  (trans (cong (HMap F)
               (Q (trans (snd (P _))
                         (trans (cong₂ (Cat.comp D)
                                       (sym $ snd (P _))
                                       (sym $ snd (P _)))
                                (sym $ fcomp J)))))
         (fcomp F)) where open Fun

-- any rel. monad is trivially a module over itself, 'tautalogical module'
ModRM : forall {a}{b}{c}{d}{C : Cat {a}{b}}{D : Cat {c}{d}}
       {J : Fun C D} (RM : RMonad J) -> Mod RM
ModRM RM = mod T bind law1 law3 where open RMonad RM

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

open import results-checks
open import preservation

module finality where
  finality : ∀{Δ Σ' Γ E e r k τ} →
               E env-final →
               Δ , Σ' , Γ ⊢ E →
               Δ , Σ' , Γ ⊢ e :: τ →
               E ⊢ e ⇒ r ⊣ k →
               r final
  finality E-final ctxcons (TAFix _) EFix = FFix E-final
  finality (EF E-fin) ctxcons (TAVar _) (EVar h) = E-fin h
  finality E-final ctxcons (TAApp _ ta-f ta-arg) (EAppFix {Ef = Ef} {f} {x} {ef} {r2 = r2} CF∞ h2 eval-f eval-arg eval-ef)
    rewrite h2 with preservation ctxcons ta-f eval-f
  ... | TAFix ctxcons-Ef (TAFix ta-ef) =
    finality (EF new-Ef+-final) new-ctxcons ta-ef eval-ef
    where
      new-ctxcons =
        EnvInd (EnvInd ctxcons-Ef (preservation ctxcons ta-f eval-f)) (preservation ctxcons ta-arg eval-arg)
      new-Ef-final  : ∀{x' rx'} → (x' , rx') ∈ (Ef ,, (f , [ Ef ]fix f ⦇·λ x => ef ·⦈)) → rx' final
      new-Ef-final  {x'} {rx'} h with ctx-split {Γ = Ef} h
      new-Ef-final  {x'} {rx'} h | Inl (_ , x'∈Ef) with finality E-final ctxcons ta-f eval-f
      ... | FFix (EF Ef-fin) = Ef-fin x'∈Ef
      new-Ef-final  {x'} {rx'} h | Inr (_ , rx'==r2) rewrite rx'==r2 = finality E-final ctxcons ta-f eval-f
      new-Ef+-final : ∀{x' rx'} → (x' , rx') ∈ (Ef ,, (f , [ Ef ]fix f ⦇·λ x => ef ·⦈) ,, (x , r2)) → rx' final
      new-Ef+-final {x'} {rx'} h with ctx-split {Γ = Ef ,, (f , [ Ef ]fix f ⦇·λ x => ef ·⦈)} h
      new-Ef+-final {x'} {rx'} h | Inl (_ , x'∈Ef+) = new-Ef-final x'∈Ef+
      new-Ef+-final {x'} {rx'} h | Inr (_ , rx'==r2) rewrite rx'==r2 = finality E-final ctxcons ta-arg eval-arg
  finality E-final ctxcons (TAApp h ta-f ta-arg) (EAppUnfinished eval-f h2 eval-arg) =
    FAp (finality E-final ctxcons ta-f eval-f) (finality E-final ctxcons ta-arg eval-arg) h2
  finality E-final ctxcons TAUnit EUnit = FUnit
  finality E-final ctxcons (TAPair _ ta1 ta2) (EPair eval1 eval2)
    = FPair (finality E-final ctxcons ta1 eval1) (finality E-final ctxcons ta2 eval2)
  finality E-final ctxcons (TAFst ta) (EFst eval)
    with finality E-final ctxcons ta eval
  ... | FPair fin _ = fin
  finality E-final ctxcons (TAFst ta) (EFstUnfinished eval ne)
    = FFst (finality E-final ctxcons ta eval) ne
  finality E-final ctxcons (TASnd ta) (ESnd eval)
    with finality E-final ctxcons ta eval
  ... | FPair _ fin = fin
  finality E-final ctxcons (TASnd ta) (ESndUnfinished eval ne)
    = FSnd (finality E-final ctxcons ta eval) ne
  finality E-final ctxcons (TACtor h h2 ta) (ECtor eval) = FCon (finality E-final ctxcons ta eval)
  finality {Σ' = Σ'} (EF E-fin) ctxcons (TACase d∈Σ'1 ta h1 h2) (EMatch {E = E} {xc = xc} {r' = r'} CF∞ form eval eval-ec)
    with h2 form
  ...  | _ , _ , _ , c∈cctx1 , ta-ec
    with preservation ctxcons ta eval
  ...  | TACtor {cctx = cctx} d∈Σ' c∈cctx ta-r'
    rewrite ctxunicity {Γ = π1 Σ'} d∈Σ'1 d∈Σ' | ctxunicity {Γ = cctx} c∈cctx1 c∈cctx =
      finality (EF new-E-final) (EnvInd ctxcons ta-r') ta-ec eval-ec
      where
        new-E-final : ∀{x' rx'} → (x' , rx') ∈ (E ,, (xc , r')) → rx' final
        new-E-final {x'} {rx'} x'∈E+ with ctx-split {Γ = E} x'∈E+
        ... | Inl (_ , x'∈E) = E-fin x'∈E
        ... | Inr (_ , rx'==r') rewrite rx'==r' with finality (EF E-fin) ctxcons ta eval
        ... | FCon r'-fin = r'-fin
  finality E-final ctxcons (TACase h ta h2 h3) (EMatchUnfinished eval h4) = FCase (finality E-final ctxcons ta eval) h4 E-final
  finality E-final ctxcons (TAHole _) EHole = FHole E-final
  finality E-final ctxcons (TAAsrt _ _ _) (EAsrt _ _ _) = FUnit

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


text:
{-# OPTIONS --no-positivity-check #-}

-- Formalization of OPLSS: Computational Type Theory (Robert Harper), 2018.

module CTT where

open import Function using (_$_)
open import Level using (Level)
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Product renaming (_×_ to _∧_)

private
  variable
    ℓ : Level

Deterministic : {A B : Set} (_⇒_ : REL A B ℓ) → Set ℓ
Deterministic {A = A} {B = B} _⇒_ = {M : A} {M'₁ M'₂ : B} → M ⇒ M'₁ → M ⇒ M'₂ → M'₁ ≡ M'₂

record Language : Set₁ where
  field
    exp : Set
    _val : exp → Set
    _↦_ : exp → exp → Set

    val-↦-exclusive : {M : exp} → ¬ (M val ∧ ∃ λ M' → M ↦ M')
    ↦-deterministic : Deterministic _↦_

per-refl : {A : Set} {_≈_ : Rel A ℓ} {M M' : A} → IsPartialEquivalence _≈_ → M ≈ M' → M ≈ M
per-refl record { sym = sym ; trans = trans } h = trans h (sym h)

module MultiStep (L : Language) where
  open Language L

  data _↦*_ : exp → exp → Set where
    here : {M : exp} → M ↦* M
    step : {M M' M'' : exp} → M ↦ M' → M' ↦* M'' → M ↦* M''

  ↦*-append : {M M' M'' : exp} → M ↦* M' → M' ↦* M'' → M ↦* M''
  ↦*-append here M↦*M'' = M↦*M''
  ↦*-append (step M↦M''' M'''↦*M') M'↦*M'' = step M↦M''' (↦*-append M'''↦*M' M'↦*M'')

  stepʳ : {M M' M'' : exp} → M ↦* M' → M' ↦ M'' → M ↦* M''
  stepʳ M↦*M' M'↦M'' = ↦*-append M↦*M' (step M'↦M'' here)

  lift-principal : (f : exp → exp) → ({M M' : exp} → M ↦ M' → f M ↦ f M') → {M M' : exp} → M ↦* M' → f M ↦* f M'
  lift-principal f h here = here
  lift-principal f h (step M↦M'' M''↦*M') = step (h M↦M'') (lift-principal f h M''↦*M')

  record _⇓_ (M M' : exp) : Set where
    constructor _and_
    field
      M↦*M' : M ↦* M'
      M'val : M' val

  step⇓ : {M M' M'' : exp} → M ↦ M' → M' ⇓ M'' → M ⇓ M''
  step⇓ M↦*M' (M'↦*M'' and M''val) = step M↦*M' M'↦*M'' and M''val

  step*⇓ : {M M' M'' : exp} → M ↦* M' → M' ⇓ M'' → M ⇓ M''
  step*⇓ M↦*M' (M'↦*M'' and M''val) = ↦*-append M↦*M' M'↦*M'' and M''val

  val⇓ : {M : exp} → M val → M ⇓ M
  val⇓ Mval = here and Mval

  ⇓-deterministic : Deterministic _⇓_
  ⇓-deterministic (M↦*M'₁ and M'₁val) (M↦*M'₂ and M'val₂) = aux M↦*M'₁ M↦*M'₂ M'₁val M'val₂
    where
      aux : {M : exp} {M'₁ M'₂ : exp} → M ↦* M'₁ → M ↦* M'₂ → M'₁ val → M'₂ val → M'₁ ≡ M'₂
      aux here here _ _ = refl
      aux here (step M↦M' _) Mval _ = contradiction (Mval , -, M↦M') val-↦-exclusive
      aux (step M↦M' _) here _ Mval = contradiction (Mval , -, M↦M') val-↦-exclusive
      aux (step M↦M'₁ M'₁↦*M''₁) (step M↦M'₂ M'₂↦*M'') M''₁val M''₂val with ↦-deterministic M↦M'₁ M↦M'₂
      ... | refl = aux M'₁↦*M''₁ M'₂↦*M'' M''₁val M''₂val

  val⇓val : {M M' : exp} → M val → M ⇓ M' → M' ≡ M
  val⇓val Mval M⇓M' with ⇓-deterministic (val⇓ Mval) M⇓M'
  ... | refl = refl

module Example1 where
  -- Language

  data exp : Set where
    Bool : exp
    tt ff : exp
    if : exp → exp → exp → exp
    Nat : exp
    zero : exp
    succ : exp → exp
    rec : exp → (exp → exp → exp) → exp → exp
    _×_ : exp → exp → exp
    ⟨_,_⟩ : exp → exp → exp
    _·1 : exp → exp
    _·2 : exp → exp
    Eq : exp → exp → exp → exp
    refl : exp

  data _val : exp → Set where
    Bool : Bool val
    tt : tt val
    ff : ff val
    Nat : Nat val
    zero : zero val
    succ : {M : exp} → succ M val
    _×_ : {A₁ A₂ : exp} → A₁ val → A₂ val → (A₁ × A₂) val
    ⟨_,_⟩ : {M₁ M₂ : exp} → ⟨ M₁ , M₂ ⟩ val
    Eq : {A M₁ M₂ : exp} → Eq A M₁ M₂ val
    refl : refl val

  infix 3 _↦_
  data _↦_ : exp → exp → Set where
    if/principal : {M M' M₁ M₀ : exp} → M ↦ M' → if M M₁ M₀ ↦ if M' M₁ M₀
    if/tt : {M₁ M₀ : exp} → if tt M₁ M₀ ↦ M₁
    if/ff : {M₁ M₀ : exp} → if ff M₁ M₀ ↦ M₀
    rec/principal : ∀ {M M' M₀ M₁} → M ↦ M' → rec M₀ M₁ M ↦ rec M₀ M₁ M'
    rec/zero : ∀ {M₀ M₁} → rec M₀ M₁ zero ↦ M₀
    rec/succ : ∀ {M M₀ M₁} → rec M₀ M₁ (succ M) ↦ M₁ M (rec M₀ M₁ M)
    _·1/principal : {M M' : exp} → M ↦ M' → M ·1 ↦ M' ·1
    _·1 : {M₁ M₂ : exp} → ⟨ M₁ , M₂ ⟩ ·1 ↦ M₁
    _·2/principal : {M M' : exp} → M ↦ M' → M ·2 ↦ M' ·2
    _·2 : {M₁ M₂ : exp} → ⟨ M₁ , M₂ ⟩ ·2 ↦ M₂

  ↦-deterministic : Deterministic _↦_
  ↦-deterministic (if/principal h) (if/principal h') with ↦-deterministic h h'
  ... | refl = refl
  ↦-deterministic if/tt if/tt = refl
  ↦-deterministic if/ff if/ff = refl
  ↦-deterministic (rec/principal h) (rec/principal h') with ↦-deterministic h h'
  ... | refl = refl
  ↦-deterministic rec/zero rec/zero = refl
  ↦-deterministic rec/succ rec/succ = refl
  ↦-deterministic (h ·1/principal) (h' ·1/principal) with ↦-deterministic h h'
  ... | refl = refl
  ↦-deterministic _·1 _·1 = refl
  ↦-deterministic (h ·2/principal) (h' ·2/principal) with ↦-deterministic h h'
  ... | refl = refl
  ↦-deterministic _·2 _·2 = refl

  val-↦-exclusive : {M : exp} → ¬ ((M val) ∧ ∃ (_↦_ M))
  val-↦-exclusive (Bool , _ , ())
  val-↦-exclusive (tt , _ , ())
  val-↦-exclusive (ff , _ , ())
  val-↦-exclusive (_ × _ , _ , ())
  val-↦-exclusive (⟨_,_⟩ , _ , ())

  open MultiStep
    record
      { exp = exp
      ; _val = _val
      ; _↦_ = _↦_
      ; val-↦-exclusive = val-↦-exclusive
      ; ↦-deterministic = ↦-deterministic
      }

  -- Type Signatures

  data _≐_typeᵒ : exp → exp → Set
  record _≐_type (A A' : exp) : Set

  ≐typeᵒ-sym : Symmetric _≐_typeᵒ
  ≐typeᵒ-trans : Transitive _≐_typeᵒ
  ≐typeᵒ-isPartialEquivalence : IsPartialEquivalence (_≐_typeᵒ)

  ≐type-sym : Symmetric _≐_type
  ≐type-trans : Transitive _≐_type
  ≐type-isPartialEquivalence : IsPartialEquivalence (_≐_type)

  data _∋ᵒ_≐_ : (A : exp) → exp → exp → Set
  record _∋_≐_ (A : exp) (M M' : exp) : Set

  A∋ᵒ≐-sym : {A : exp} → Symmetric (A ∋ᵒ_≐_)
  A∋ᵒ≐-trans : {A : exp} → Transitive (A ∋ᵒ_≐_)
  A∋ᵒ≐-isPartialEquivalence : (A : exp) → IsPartialEquivalence (A ∋ᵒ_≐_)

  A∋≐-sym : {A : exp} → Symmetric (A ∋_≐_)
  A∋≐-trans : {A : exp} → Transitive (A ∋_≐_)
  A∋≐-isPartialEquivalence : (A : exp) → IsPartialEquivalence (A ∋_≐_)

  lemma/moveᵒ : {A A' M₁ M₂ : exp} → A ≐ A' typeᵒ → A' ∋ᵒ M₁ ≐ M₂ → A ∋ᵒ M₁ ≐ M₂
  lemma/move : {A A' M₁ M₂ : exp} → A ≐ A' type → A' ∋ M₁ ≐ M₂ → A ∋ M₁ ≐ M₂

  -- Implementations

  data _≐_typeᵒ where
    Bool : Bool ≐ Bool typeᵒ
    Nat : Nat ≐ Nat typeᵒ
    _×_ : {A₁ A₁' A₂ A₂' : exp} →
      A₁ ≐ A₁' typeᵒ →
      A₂ ≐ A₂' typeᵒ →
      (A₁ × A₂) ≐ (A₁' × A₂') typeᵒ
    Eq : {A A' M₁ M₁' M₂ M₂' : exp} →
      A ≐ A' type →
      A ∋ M₁ ≐ M₁' →
      A ∋ M₂ ≐ M₂' →
      Eq A M₁ M₂ ≐ Eq A' M₁' M₂' typeᵒ

  _typeᵒ : exp → Set
  A typeᵒ = A ≐ A typeᵒ

  record _≐_type A A' where
    constructor ⇓_,⇓_,_
    pattern
    inductive
    field
      {Aᵒ} : exp
      A⇓Aᵒ : A ⇓ Aᵒ
      {A'ᵒ} : exp
      A'⇓A'ᵒ : A' ⇓ A'ᵒ
      Aᵒ≐A'ᵒtypeᵒ : Aᵒ ≐ A'ᵒ typeᵒ

  _type : exp → Set
  A type = A ≐ A type

  ⇓_,⇓-,_ : {A Aᵒ : exp} (A⇓Aᵒ : A ⇓ Aᵒ) (Aᵒtypeᵒ : Aᵒ typeᵒ) → A type
  ⇓ A⇓Aᵒ ,⇓-, Aᵒtypeᵒ = ⇓ A⇓Aᵒ ,⇓ A⇓Aᵒ , Aᵒtypeᵒ

  ≐typeᵒ-sym Bool = Bool
  ≐typeᵒ-sym Nat = Nat
  ≐typeᵒ-sym (h₁ × h₂) = ≐typeᵒ-sym h₁ × ≐typeᵒ-sym h₂
  ≐typeᵒ-sym (Eq h h₁ h₂) = Eq (≐type-sym h) (A∋≐-sym (lemma/move (≐type-sym h) h₁)) (A∋≐-sym (lemma/move (≐type-sym h) h₂))

  ≐typeᵒ-trans Bool Bool = Bool
  ≐typeᵒ-trans Nat Nat = Nat
  ≐typeᵒ-trans (h₁ × h₂) (h₁' × h₂') = ≐typeᵒ-trans h₁ h₁' × ≐typeᵒ-trans h₂ h₂'
  ≐typeᵒ-trans (Eq h h₁ h₂) (Eq h' h₁' h₂') = Eq (≐type-trans h h') (A∋≐-trans h₁ (lemma/move h h₁')) (A∋≐-trans h₂ (lemma/move h h₂'))

  ≐typeᵒ-isPartialEquivalence = record { sym = ≐typeᵒ-sym ; trans = ≐typeᵒ-trans }

  ≐type-sym (⇓ A⇓Aᵒ ,⇓ A'⇓A'ᵒ , Aᵒ≐A'ᵒtypeᵒ) = ⇓ A'⇓A'ᵒ ,⇓ A⇓Aᵒ , (≐typeᵒ-sym Aᵒ≐A'ᵒtypeᵒ)

  ≐type-trans {A₀} {A₁} {A₂} (⇓ A₀⇓ ,⇓ A₁⇓ , Aᵒ≐A'ᵒtypeᵒ) (⇓ A₁⇓' ,⇓ A₂⇓ , Aᵒ₁≐A'ᵒ₁typeᵒ) with ⇓-deterministic A₁⇓ A₁⇓'
  ... | refl = ⇓ A₀⇓ ,⇓ A₂⇓ , ≐typeᵒ-trans Aᵒ≐A'ᵒtypeᵒ Aᵒ₁≐A'ᵒ₁typeᵒ

  ≐type-isPartialEquivalence = record { sym = ≐type-sym ; trans = ≐type-trans }

  typeᵒ-val : {A A' : exp} → A ≐ A' typeᵒ → A val
  typeᵒ-val Bool = Bool
  typeᵒ-val Nat = Nat
  typeᵒ-val (h₁ × h₂) = typeᵒ-val h₁ × typeᵒ-val h₂
  typeᵒ-val (Eq h h₁ h₂) = Eq

  typeᵒ-val' : {A A' : exp} → A ≐ A' typeᵒ → A' val
  typeᵒ-val' Bool = Bool
  typeᵒ-val' Nat = Nat
  typeᵒ-val' (h₁ × h₂) = typeᵒ-val' h₁ × typeᵒ-val' h₂
  typeᵒ-val' (Eq h h₁ h₂) = Eq

  typeᵒ-type : {A A' : exp} → A ≐ A' typeᵒ → A ≐ A' type
  typeᵒ-type A≐A'typeᵒ = ⇓ (val⇓ (typeᵒ-val A≐A'typeᵒ)) ,⇓ (val⇓ (typeᵒ-val' A≐A'typeᵒ)) , A≐A'typeᵒ

  data R/Bool : exp → exp → Set where
    tt : {M M' : exp} → M ⇓ tt → M' ⇓ tt → R/Bool M M'
    ff : {M M' : exp} → M ⇓ ff → M' ⇓ ff → R/Bool M M'

  R/Bool-sym : Symmetric R/Bool
  R/Bool-sym (tt h h') = tt h' h
  R/Bool-sym (ff h h') = ff h' h

  R/Bool-trans : Transitive R/Bool
  R/Bool-trans (tt h _) (tt _ h') = tt h h'
  R/Bool-trans (tt _ h) (ff h' _) with ⇓-deterministic h h'
  ... | ()
  R/Bool-trans (ff _ h) (tt h' _) with ⇓-deterministic h h'
  ... | ()
  R/Bool-trans (ff h _) (ff _ h') = ff h h'

  R/Bool-isPartialEquivalence : IsPartialEquivalence R/Bool
  R/Bool-isPartialEquivalence = record { sym = R/Bool-sym ; trans = R/Bool-trans }

  data R/Nat : exp → exp → Set where
    zero : {M M' : exp} → M ⇓ zero → M' ⇓ zero → R/Nat M M'
    succ : {M M' N N' : exp} → M ⇓ succ N → M' ⇓ succ N' → R/Nat N N' → R/Nat M M'

  R/Nat-sym : Symmetric R/Nat
  R/Nat-sym (zero h h') = zero h' h
  R/Nat-sym (succ h h' r) = succ h' h (R/Nat-sym r)

  R/Nat-trans : Transitive R/Nat
  R/Nat-trans (zero h _) (zero _ h') = zero h h'
  R/Nat-trans (zero _ h₁) (succ h₁' _ _) with ⇓-deterministic h₁ h₁'
  ... | ()
  R/Nat-trans (succ _ h₁ _) (zero h₁' _)  with ⇓-deterministic h₁ h₁'
  ... | ()
  R/Nat-trans (succ h h₁ r) (succ h₁' h' r') with ⇓-deterministic h₁ h₁'
  ... | refl = succ h h' (R/Nat-trans r r')

  R/Nat-isPartialEquivalence : IsPartialEquivalence R/Nat
  R/Nat-isPartialEquivalence = record { sym = R/Nat-sym ; trans = R/Nat-trans }

  data R/Eq : exp → exp → Set where
    refl : {M M' : exp} → M ⇓ refl → M' ⇓ refl → R/Eq M M'

  R/Eq-sym : Symmetric R/Eq
  R/Eq-sym (refl h h') = refl h' h

  R/Eq-trans : Transitive R/Eq
  R/Eq-trans (refl h₁ h₁') (refl h₂ h₂') = refl h₁ h₂'

  R/Eq-isPartialEquivalence : IsPartialEquivalence R/Eq
  R/Eq-isPartialEquivalence = record { sym = R/Eq-sym ; trans = R/Eq-trans }

  data _∋ᵒ_≐_ where
    Bool : {M M' : exp} → R/Bool M M' → Bool ∋ᵒ M ≐ M'
    Nat : {M M' : exp} → R/Nat M M' → Nat ∋ᵒ M ≐ M'
    _×_ : {A₁ A₂ M₁ M₂ M₁' M₂' : exp} →
      A₁ ∋ M₁ ≐ M₁' →
      A₂ ∋ M₂ ≐ M₂' →
      (A₁ × A₂) ∋ᵒ ⟨ M₁ , M₂ ⟩ ≐ ⟨ M₁' , M₂' ⟩
    Eq : {A M₁ M₂ M M' : exp} →
      R/Eq M M' →
      A ∋ M₁ ≐ M₂ →
      Eq A M₁ M₂ ∋ᵒ M ≐ M'

  _∋ᵒ_ : (A : exp) → exp → Set
  A ∋ᵒ M = A ∋ᵒ M ≐ M

  A∋ᵒ≐-sym (Bool h) = Bool (R/Bool-sym h)
  A∋ᵒ≐-sym (Nat h) = Nat (R/Nat-sym h)
  A∋ᵒ≐-sym (h₁ × h₂) = A∋≐-sym h₁ × A∋≐-sym h₂
  A∋ᵒ≐-sym (Eq h h≐) = Eq (R/Eq-sym h) h≐

  A∋ᵒ≐-trans (Bool h) (Bool h') = Bool (R/Bool-trans h h')
  A∋ᵒ≐-trans (Nat h) (Nat h') = Nat (R/Nat-trans h h')
  A∋ᵒ≐-trans (h₁ × h₂) (h₁' × h₂') = A∋≐-trans h₁ h₁' × A∋≐-trans h₂ h₂'
  A∋ᵒ≐-trans (Eq h h≐) (Eq h' h≐') = Eq (R/Eq-trans h h') h≐

  A∋ᵒ≐-isPartialEquivalence A = record { sym = A∋ᵒ≐-sym ; trans = A∋ᵒ≐-trans }

  record _∋_≐_ A M M' where
    constructor ⇓_,⇓_,⇓_,_
    pattern
    inductive
    field
      {Aᵒ} : exp
      A⇓Aᵒ : A ⇓ Aᵒ
      {Mᵒ} : exp
      M⇓Mᵒ : M ⇓ Mᵒ
      {M'ᵒ} : exp
      M'⇓M'ᵒ : M' ⇓ M'ᵒ
      Aᵒ∋ᵒMᵒ≐M'ᵒ : Aᵒ ∋ᵒ Mᵒ ≐ M'ᵒ

  _∋_ : (A : exp) → exp → Set
  A ∋ M = A ∋ M ≐ M

  ⇓_,⇓_,⇓-,_ : {A Aᵒ M Mᵒ : exp} (A⇓Aᵒ : A ⇓ Aᵒ) (M⇓Mᵒ : M ⇓ Mᵒ) (Aᵒ∋ᵒMᵒ : Aᵒ ∋ᵒ Mᵒ) → A ∋ M
  ⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓-, Aᵒ∋ᵒMᵒ = ⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓ M⇓Mᵒ , Aᵒ∋ᵒMᵒ

  A∋≐-sym {A} (⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓ M'⇓M'ᵒ , A∋ᵒMᵒ≐M'ᵒ) = ⇓ A⇓Aᵒ ,⇓ M'⇓M'ᵒ ,⇓ M⇓Mᵒ , A∋ᵒ≐-sym A∋ᵒMᵒ≐M'ᵒ

  A∋≐-trans {A} {M₀} {M₁} {M₂} (⇓ A⇓ ,⇓ M₀⇓ ,⇓ M₁⇓ , A∋ᵒMᵒ≐M'ᵒ₁) (⇓ A⇓' ,⇓ M₁⇓' ,⇓ M₂⇓ , A∋ᵒM'ᵒ₁≐M'ᵒ) with ⇓-deterministic A⇓ A⇓' | ⇓-deterministic M₁⇓ M₁⇓'
  ... | refl | refl = ⇓ A⇓ ,⇓ M₀⇓ ,⇓ M₂⇓ , A∋ᵒ≐-trans A∋ᵒMᵒ≐M'ᵒ₁ A∋ᵒM'ᵒ₁≐M'ᵒ

  A∋≐-isPartialEquivalence A = record { sym = A∋≐-sym ; trans = A∋≐-trans }

  -- Lemmas

  lemma/moveᵒ Bool A'∋ᵒM₁≐M₂ = A'∋ᵒM₁≐M₂
  lemma/moveᵒ Nat A'∋ᵒM₁≐M₂ = A'∋ᵒM₁≐M₂
  lemma/moveᵒ (A₁≐A₁'typeᵒ × A₂≐A₂'typeᵒ) (A₁'∋ᵒM₁≐M₁' × A₂'∋ᵒM₂≐M₂') = lemma/move (typeᵒ-type A₁≐A₁'typeᵒ) A₁'∋ᵒM₁≐M₁' × lemma/move (typeᵒ-type A₂≐A₂'typeᵒ) A₂'∋ᵒM₂≐M₂'
  lemma/moveᵒ (Eq A≐A'type A∋M₁≐M₁' A∋M₂≐M₂') (Eq h h≐) = Eq h (A∋≐-trans A∋M₁≐M₁' (A∋≐-trans (lemma/move A≐A'type h≐) (A∋≐-sym A∋M₂≐M₂')))

  lemma/move (⇓ A⇓Aᵒ ,⇓ A'⇓A'ᵒ₁ , Aᵒ≐A'ᵒtypeᵒ) (⇓ A'⇓A'ᵒ ,⇓ M₁⇓M₁ᵒ ,⇓ M₂⇓M₂ᵒ , A'ᵒ∋ᵒM₁ᵒ≐M₂ᵒ) with ⇓-deterministic A'⇓A'ᵒ₁ A'⇓A'ᵒ
  ... | refl = ⇓ A⇓Aᵒ ,⇓ M₁⇓M₁ᵒ ,⇓ M₂⇓M₂ᵒ , lemma/moveᵒ Aᵒ≐A'ᵒtypeᵒ A'ᵒ∋ᵒM₁ᵒ≐M₂ᵒ

  rev-closure-A : {A A' M₁ M₂ : exp} → A ↦ A' → A' ∋ M₁ ≐ M₂ → A ∋ M₁ ≐ M₂
  rev-closure-A A↦A' (⇓ A⇓Aᵒ ,⇓ M₁⇓M₁ᵒ ,⇓ M₂⇓M₂ᵒ , Aᵒ∋ᵒM₁ᵒ≐M₂ᵒ) = ⇓ step⇓ A↦A' A⇓Aᵒ ,⇓ M₁⇓M₁ᵒ ,⇓ M₂⇓M₂ᵒ , Aᵒ∋ᵒM₁ᵒ≐M₂ᵒ

  rev-closure-A* : {A A' M₁ M₂ : exp} → A ↦* A' → A' ∋ M₁ ≐ M₂ → A ∋ M₁ ≐ M₂
  rev-closure-A* here A'∋M₁≐M₂ = A'∋M₁≐M₂
  rev-closure-A* (step A↦A'' A''↦*A') A'∋M₁≐M₂ = rev-closure-A A↦A'' (rev-closure-A* A''↦*A' A'∋M₁≐M₂)

  rev-closure-M : {A M M' : exp} → M ↦ M' → A ∋ M' → A ∋ M
  rev-closure-M M↦M' (⇓ A⇓Aᵒ ,⇓ M'⇓Mᵒ ,⇓ M'⇓M'ᵒ , A∋ᵒMᵒ≐M'ᵒ) = ⇓ A⇓Aᵒ ,⇓ step⇓ M↦M' M'⇓Mᵒ ,⇓ step⇓ M↦M' M'⇓M'ᵒ , A∋ᵒMᵒ≐M'ᵒ

  rev-closure-M* : {A M M' : exp} → M ↦* M' → A ∋ M' → A ∋ M
  rev-closure-M* here A∋M' = A∋M'
  rev-closure-M* (step M↦M'' M''↦*M') A∋M' = rev-closure-M M↦M'' (rev-closure-M* M''↦*M' A∋M')

  rev-closure-M*₂ : {A M₁ M₁' M₂ M₂' : exp} → M₁ ↦* M₁' → M₂ ↦* M₂' → A ∋ M₁' ≐ M₂' → A ∋ M₁ ≐ M₂
  rev-closure-M*₂ M₁↦*M₁' M₂↦*M₂' (⇓ A⇓Aᵒ ,⇓ M₁'⇓M₁'ᵒ ,⇓ M₂'⇓M₂'ᵒ , Aᵒ∋ᵒMᵒ≐M'ᵒ) =
    ⇓ A⇓Aᵒ ,⇓ ((↦*-append M₁↦*M₁' (_⇓_.M↦*M' M₁'⇓M₁'ᵒ)) and _⇓_.M'val M₁'⇓M₁'ᵒ) ,⇓ ((↦*-append M₂↦*M₂' (_⇓_.M↦*M' M₂'⇓M₂'ᵒ)) and _⇓_.M'val M₂'⇓M₂'ᵒ) , Aᵒ∋ᵒMᵒ≐M'ᵒ

  -- Hypotheticals

  _>>_ : (A : exp) → (exp → exp → Set) → Set
  A >> J = {a a' : exp} → A ∋ a ≐ a' → J a a'

  _>>_≐_type : (A : exp) (B B' : exp → exp) → Set
  A >> B ≐ B' type = A >> λ a a' → B a ≐ B' a' type

  _>>_type : (A : exp) (B : exp → exp) → Set
  A >> B type = A >> B ≐ B type

  _>>_∋_≐_ : (A : exp) (B N N' : exp → exp) → Set
  A >> B ∋ N ≐ N' = A >> λ a a' → B a ∋ N a ≐ N' a'

  _>>_∋_ : (A : exp) (B N : exp → exp) → Set
  A >> B ∋ N = A >> B ∋ N ≐ N

  -- Facts

  fact/if : {A M M₁ M₀ M₁' M₀' : exp} → Bool ∋ M → A ∋ M₁ → A ∋ M₀ → A ∋ if M M₁ M₀
  fact/if {M₁ = M₁} {M₀ = M₀} (⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓ M'⇓M'ᵒ , Aᵒ∋ᵒMᵒ≐M'ᵒ) h₁ h₀ with val⇓val Bool A⇓Aᵒ
  fact/if {M₁ = M₁} {M₀ = M₀} (⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓ M'⇓M'ᵒ , Bool (tt Mᵒ⇓tt _)) h₁ h₀ | refl =
    let step-principal M₁ M₀ = lift-principal (λ M → if M M₁ M₀) if/principal (↦*-append (_⇓_.M↦*M' M⇓Mᵒ) (_⇓_.M↦*M' Mᵒ⇓tt)) in
    rev-closure-M* (stepʳ (step-principal M₁ M₀) if/tt) h₁
  fact/if {M₁ = M₁} {M₀ = M₀} (⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓ M'⇓M'ᵒ , Bool (ff Mᵒ⇓ff _)) h₁ h₀ | refl =
    let step-principal M₁ M₀ = lift-principal (λ M → if M M₁ M₀) if/principal (↦*-append (_⇓_.M↦*M' M⇓Mᵒ) (_⇓_.M↦*M' Mᵒ⇓ff)) in
    rev-closure-M* (stepʳ (step-principal M₁ M₀) if/ff) h₀

  fact/if' : {M A₁ A₀ M₁ M₀ : exp} → Bool ∋ M → A₁ ∋ M₁ → A₀ ∋ M₀ → if M A₁ A₀ ∋ if M M₁ M₀
  fact/if' {A₁ = A₁} {A₀ = A₀} {M₁ = M₁} {M₀ = M₀} (⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓ M'⇓M'ᵒ , Aᵒ∋ᵒMᵒ≐M'ᵒ) h₁ h₀ with val⇓val Bool A⇓Aᵒ
  fact/if' {A₁ = A₁} {A₀ = A₀} {M₁ = M₁} {M₀ = M₀} (⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓ M'⇓M'ᵒ , Bool (tt Mᵒ⇓tt _)) h₁ h₀ | refl =
    let step-principal M₁ M₀ = lift-principal (λ M → if M M₁ M₀) if/principal (↦*-append (_⇓_.M↦*M' M⇓Mᵒ) (_⇓_.M↦*M' Mᵒ⇓tt)) in
    rev-closure-A* (stepʳ (step-principal A₁ A₀) if/tt) $
    rev-closure-M* (stepʳ (step-principal M₁ M₀) if/tt) $
    h₁
  fact/if' {A₁ = A₁} {A₀ = A₀} {M₁ = M₁} {M₀ = M₀} (⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓ M'⇓M'ᵒ , Bool (ff Mᵒ⇓ff _)) h₁ h₀ | refl =
    let step-principal M₁ M₀ = lift-principal (λ M → if M M₁ M₀) if/principal (↦*-append (_⇓_.M↦*M' M⇓Mᵒ) (_⇓_.M↦*M' Mᵒ⇓ff)) in
    rev-closure-A* (stepʳ (step-principal A₁ A₀) if/ff) $
    rev-closure-M* (stepʳ (step-principal M₁ M₀) if/ff) $
    h₀

  R/Nat⇒Nat∋≐ : {N N' : exp} → R/Nat N N' → Nat ∋ N ≐ N'
  R/Nat⇒Nat∋≐ (zero h h') = ⇓ here and Nat ,⇓ h ,⇓ h' , Nat (zero (here and _⇓_.M'val h) (here and _⇓_.M'val h'))
  R/Nat⇒Nat∋≐ (succ h h' r) = ⇓ here and Nat ,⇓ h ,⇓ h' , Nat (succ (here and _⇓_.M'val h) (here and _⇓_.M'val h') r)

  fact/rec : ∀ {B M₀ M₁ M} →
    Nat >> B type →
    B zero ∋ M₀ →
    Nat >> (λ a a' → B a >> λ b b' → B (succ a) ∋ M₁ a b ≐ M₁ a' b') →
    Nat ∋ M → B M ∋ rec M₀ M₁ M
  fact/rec Nat>>Btype h₀ h₁ (⇓ A⇓Aᵒ ,⇓ M⇓Mᵒ ,⇓ M⇓M'ᵒ , Aᵒ∋ᵒMᵒ≐M'ᵒ) with val⇓val Nat A⇓Aᵒ
  fact/rec {B} {M₀} {M₁} Nat>>Btype h₀ h₁ (⇓ A⇓Nat ,⇓ M⇓Mᵒ ,⇓ M⇓M'ᵒ , Nat r) | refl = induction (_⇓_.M↦*M' M⇓Mᵒ) r
    where
      induction : {M Mᵒ M'ᵒ : exp} → M ↦* Mᵒ → R/Nat Mᵒ M'ᵒ → B M ∋ rec M₀ M₁ M
      induction M↦*Mᵒ (zero Mᵒ⇓zero Mᵒ⇓zero') =
        let step-principal  = lift-principal (rec M₀ M₁) rec/principal (↦*-append M↦*Mᵒ (_⇓_.M↦*M' Mᵒ⇓zero)) in
        rev-closure-M* (stepʳ step-principal rec/zero) $
        lemma/move (Nat>>Btype (⇓ A⇓Nat ,⇓ step*⇓ M↦*Mᵒ Mᵒ⇓zero ,⇓ val⇓ zero , Nat (zero (val⇓ zero) (val⇓ zero)))) $
        h₀
      induction M↦*Mᵒ (succ Mᵒ⇓succN Mᵒ⇓succN' r) =
        let step-principal  = lift-principal (rec M₀ M₁) rec/principal (↦*-append M↦*Mᵒ (_⇓_.M↦*M' Mᵒ⇓succN)) in
        rev-closure-M* (stepʳ step-principal rec/succ) $
        lemma/move (Nat>>Btype (⇓ A⇓Nat ,⇓ step*⇓ M↦*Mᵒ Mᵒ⇓succN ,⇓ val⇓ succ , Nat (succ (val⇓ succ) (val⇓ succ) (per-refl R/Nat-isPartialEquivalence r)))) $
        h₁ (per-refl (A∋≐-isPartialEquivalence Nat) (R/Nat⇒Nat∋≐ r)) (induction here r)

  fact/·1 : {A₁ A₂ M : exp} → A₁ val → A₂ val → (A₁ × A₂) ∋ M → A₁ ∋ (M ·1)
  fact/·1 {A₁ = A₁} A₁val A₂val (⇓ A⇓Aᵒ ,⇓ M⇓⟨M₁,M₂⟩ ,⇓ M⇓⟨M₁',M₂'⟩ , Aᵒ∋ᵒMᵒ≐M'ᵒ) with val⇓val (A₁val × A₂val) A⇓Aᵒ
  fact/·1 {A₁ = A₁} A₁val A₂val (⇓ A⇓Aᵒ ,⇓ M⇓⟨M₁,M₂⟩ ,⇓ M⇓⟨M₁',M₂'⟩ , (A₁∋M₁≐M₁' × A₂∋M₂≐M₂')) | refl =
    rev-closure-M* (stepʳ (lift-principal _·1 _·1/principal (_⇓_.M↦*M' M⇓⟨M₁,M₂⟩)) _·1) (per-refl (A∋≐-isPartialEquivalence A₁) A₁∋M₁≐M₁')

  fact/⟨,⟩·1 : {A₁ M₁ M₂ : exp} → A₁ ∋ M₁ → A₁ ∋ ⟨ M₁ , M₂ ⟩ ·1 ≐ M₁
  fact/⟨,⟩·1 (⇓ A⇓Aᵒ ,⇓ M₁⇓Mᵒ ,⇓ M₁⇓M'ᵒ , A₁∋ᵒMᵒ≐M'ᵒ) = ⇓ A⇓Aᵒ ,⇓ step⇓ _·1 M₁⇓Mᵒ ,⇓ M₁⇓M'ᵒ , A₁∋ᵒMᵒ≐M'ᵒ

  fact/eq/inhabited : Eq Nat (succ zero) (succ zero) ∋ refl
  fact/eq/inhabited =
    ⇓ val⇓ Eq ,⇓ val⇓ refl ,⇓-,
      Eq (refl (val⇓ refl) (val⇓ refl)) (
        ⇓ val⇓ Nat ,⇓ val⇓ succ ,⇓-, (
          Nat (succ (val⇓ succ) (val⇓ succ) (zero (val⇓ zero) (val⇓ zero)))
        )
      )

  fact/eq/reflexive : {A M : exp} → A ∋ M → Eq A M M ∋ refl
  fact/eq/reflexive A∋M = ⇓ val⇓ Eq ,⇓ val⇓ refl ,⇓-, Eq (refl (val⇓ refl) (val⇓ refl)) A∋M


text:
-- There was a bug where f (suc n) didn't reduce for neutral n.
module Issue26 where

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

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

f : Nat -> Nat
f 0       = 0
f (suc n) = f n

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

lem : (n : Nat) -> f (suc n) == f n
lem n = refl

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
data D : _ where
D : _

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Automatic solvers for equations over integers
------------------------------------------------------------------------

-- See README.Integer for examples of how to use this solver

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

module Data.Integer.Solver where

import Algebra.Solver.Ring.Simple as Solver
import Algebra.Solver.Ring.AlmostCommutativeRing as ACR
open import Data.Integer using (_≟_)
open import Data.Integer.Properties using (+-*-commutativeRing)

------------------------------------------------------------------------
-- A module for automatically solving propositional equivalences
-- containing _+_ and _*_

-- A module for automatically solving propositional equivalences
module +-*-Solver =
  Solver (ACR.fromCommutativeRing +-*-commutativeRing) _≟_


text:
{-# OPTIONS --allow-unsolved-metas #-}
module Issue107 where

data Bool : Set where
  true : Bool
  false : Bool

data False : Set where
record True : Set where

T : Bool -> Set
T false = False
T _  = True

foo : ((a : Bool) -> T a) -> True
foo f = f _

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


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

open import Cubical.ZCohomology.Base
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.Data.Empty
open import Cubical.Data.Sigma hiding (_×_)
open import Cubical.HITs.Susp
open import Cubical.HITs.Wedge
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to sRec2 ; elim to sElim ; elim2 to sElim2 ; setTruncIsSet to §)
open import Cubical.Data.Int renaming (_+_ to _ℤ+_)
open import Cubical.Data.Nat
open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec ; elim3 to trElim3)
open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Connected
open import Cubical.Homotopy.Freudenthal
open import Cubical.Algebra.Group
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Data.NatMinusOne

open import Cubical.HITs.Pushout
open import Cubical.Data.Sum.Base
open import Cubical.Data.HomotopyGroup

open import Cubical.ZCohomology.KcompPrelims

open Iso renaming (inv to inv')

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

infixr 34 _+ₖ_
infixr 34 _+ₕ_

is2ConnectedKn : (n : ℕ) → isConnected 2 (coHomK (suc n))
is2ConnectedKn zero = ∣ ∣ base ∣ ∣
                    , trElim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _)
                        (trElim (λ _ → isOfHLevelPath 3 (isOfHLevelSuc 2 (isOfHLevelTrunc 2)) _ _)
                          (toPropElim (λ _ → isOfHLevelTrunc 2 _ _) refl))
is2ConnectedKn (suc n) = ∣ ∣ north ∣ ∣
                       , trElim (λ _ → isOfHLevelPath 2 (isOfHLevelTrunc 2) _ _)
                           (trElim (λ _ → isProp→isOfHLevelSuc (3 + n) (isOfHLevelTrunc 2 _ _))
                             (suspToPropElim (ptSn (suc n)) (λ _ → isOfHLevelTrunc 2 _ _) refl))

isConnectedKn : (n : ℕ) → isConnected (2 + n) (coHomK (suc n))
isConnectedKn n = isOfHLevelRetractFromIso 0 (invIso (truncOfTruncIso (2 + n) 1)) (sphereConnected (suc n))

-- Induction principles for cohomology groups
-- If we want to show a proposition about some x : Hⁿ(A), it suffices to show it under the
-- assumption that x = ∣f∣₂ and that f is pointed

coHomPointedElim : {A : Type ℓ} (n : ℕ) (a : A) {B : coHom (suc n) A → Type ℓ'}
                 → ((x : coHom (suc n) A) → isProp (B x))
                 → ((f : A → coHomK (suc n)) → f a ≡ coHom-pt (suc n) → B ∣ f ∣₂)
                 → (x : coHom (suc n) A) → B x
coHomPointedElim {ℓ' = ℓ'} {A = A} n a isprop indp =
  sElim (λ _ → isOfHLevelSuc 1 (isprop _))
         λ f → helper n isprop indp f (f a) refl
  where
  helper :  (n : ℕ) {B : coHom (suc n) A → Type ℓ'}
         → ((x : coHom (suc n) A) → isProp (B x))
         → ((f : A → coHomK (suc n)) → f a ≡ coHom-pt (suc n) → B ∣ f ∣₂)
         → (f : A → coHomK (suc n))
         → (x : coHomK (suc n))
         → f a ≡ x → B ∣ f ∣₂
  -- pattern matching a bit extra to avoid isOfHLevelPlus'
  helper zero isprop ind f =
    trElim (λ _ → isOfHLevelPlus {n = 1} 2 (isPropΠ λ _ → isprop _))
           (toPropElim (λ _ → isPropΠ λ _ → isprop _) (ind f))
  helper (suc zero) isprop ind f =
    trElim (λ _ → isOfHLevelPlus {n = 1} 3 (isPropΠ λ _ → isprop _))
           (suspToPropElim base (λ _ → isPropΠ λ _ → isprop _) (ind f))
  helper (suc (suc zero)) isprop ind f =
    trElim (λ _ → isOfHLevelPlus {n = 1} 4 (isPropΠ λ _ → isprop _))
           (suspToPropElim north (λ _ → isPropΠ λ _ → isprop _) (ind f))
  helper (suc (suc (suc n))) isprop ind f =
    trElim (λ _ → isOfHLevelPlus' {n = 5 + n} 1 (isPropΠ λ _ → isprop _))
           (suspToPropElim north (λ _ → isPropΠ λ _ → isprop _) (ind f))

coHomPointedElim2 : {A : Type ℓ} (n : ℕ) (a : A) {B : coHom (suc n) A → coHom (suc n) A → Type ℓ'}
                 → ((x y : coHom (suc n) A) → isProp (B x y))
                 → ((f g : A → coHomK (suc n)) → f a ≡ coHom-pt (suc n) → g a ≡ coHom-pt (suc n) → B ∣ f ∣₂ ∣ g ∣₂)
                 → (x y : coHom (suc n) A) → B x y
coHomPointedElim2 {ℓ' = ℓ'} {A = A} n a isprop indp = sElim2 (λ _ _ → isOfHLevelSuc 1 (isprop _ _))
                                                   λ f g → helper n a isprop indp f g (f a) (g a) refl refl
  where
  helper : (n : ℕ) (a : A) {B : coHom (suc n) A → coHom (suc n) A → Type ℓ'}
                 → ((x y : coHom (suc n) A) → isProp (B x y))
                 → ((f g : A → coHomK (suc n)) → f a ≡ coHom-pt (suc n) → g a ≡ coHom-pt (suc n) → B ∣ f ∣₂ ∣ g ∣₂)
                 → (f g : A → coHomK (suc n))
                 → (x y : coHomK (suc n))
                 → f a ≡ x → g a ≡ y
                 → B ∣ f ∣₂ ∣ g ∣₂
  helper zero a isprop indp f g =
    elim2 (λ _ _ → isOfHLevelPlus {n = 1} 2 (isPropΠ2 λ _ _ → isprop _ _))
          (toPropElim2 (λ _ _ → isPropΠ2 λ _ _ → isprop _ _) (indp f g))
  helper (suc zero) a isprop indp f g =
    elim2 (λ _ _ → isOfHLevelPlus {n = 1} 3 (isPropΠ2 λ _ _ → isprop _ _))
          (suspToPropElim2 base (λ _ _ → isPropΠ2 λ _ _ → isprop _ _) (indp f g))
  helper (suc (suc zero)) a isprop indp f g =
    elim2 (λ _ _ → isOfHLevelPlus {n = 1} 4 (isPropΠ2 λ _ _ → isprop _ _))
          (suspToPropElim2 north (λ _ _ → isPropΠ2 λ _ _ → isprop _ _) (indp f g))
  helper (suc (suc (suc n))) a isprop indp f g =
    elim2 (λ _ _ → isOfHLevelPlus' {n = 5 + n} 1 (isPropΠ2 λ _ _ → isprop _ _))
          (suspToPropElim2 north (λ _ _ → isPropΠ2 λ _ _ → isprop _ _) (indp f g))

{- Equivalence between cohomology of A and reduced cohomology of (A + 1) -}
coHomRed+1Equiv : (n : ℕ) →
                  (A : Type ℓ) →
                  (coHom n A) ≡ (coHomRed n ((A ⊎ Unit , inr (tt))))
coHomRed+1Equiv zero A i = ∥ helpLemma {C = (Int , pos 0)} i ∥₂
  module coHomRed+1 where
  helpLemma : {C : Pointed ℓ} → ( (A → (typ C)) ≡  ((((A ⊎ Unit) , inr (tt)) →∙ C)))
  helpLemma {C = C} = isoToPath (iso map1
                                     map2
                                     (λ b → linvPf b)
                                     (λ _  → refl))
    where
    map1 : (A → typ C) → ((((A ⊎ Unit) , inr (tt)) →∙ C))
    map1 f = map1' , refl
      module helpmap where
      map1' : A ⊎ Unit → fst C
      map1' (inl x) = f x
      map1' (inr x) = pt C

    map2 : ((((A ⊎ Unit) , inr (tt)) →∙ C)) → (A → typ C)
    map2 (g , pf) x = g (inl x)

    linvPf : (b :((((A ⊎ Unit) , inr (tt)) →∙ C))) →  map1 (map2 b) ≡ b
    linvPf (f , snd) i = (λ x → helper x i)  , λ j → snd ((~ i) ∨ j)
      where
      helper : (x : A ⊎ Unit) → ((helpmap.map1') (map2 (f , snd)) x) ≡ f x
      helper (inl x) = refl
      helper (inr tt) = sym snd
coHomRed+1Equiv (suc zero) A i = ∥ coHomRed+1.helpLemma A i {C = (coHomK 1 , ∣ base ∣)} i ∥₂
coHomRed+1Equiv (suc (suc n)) A i = ∥ coHomRed+1.helpLemma A i {C = (coHomK (2 + n) , ∣ north ∣)} i ∥₂

-----------

Kn→ΩKn+1 : (n : ℕ) → coHomK n → typ (Ω (coHomK-ptd (suc n)))
Kn→ΩKn+1 n = Iso.fun (Iso-Kn-ΩKn+1 n)

ΩKn+1→Kn : (n : ℕ) → typ (Ω (coHomK-ptd (suc n))) → coHomK n
ΩKn+1→Kn n = Iso.inv (Iso-Kn-ΩKn+1 n)

Kn≃ΩKn+1 : {n : ℕ} → coHomK n ≃ typ (Ω (coHomK-ptd (suc n)))
Kn≃ΩKn+1 {n = n} = isoToEquiv (Iso-Kn-ΩKn+1 n)

---------- Algebra/Group stuff --------

0ₖ : (n : ℕ) → coHomK n
0ₖ = coHom-pt

_+ₖ_ : {n : ℕ} → coHomK n → coHomK n → coHomK n
_+ₖ_ {n = n} x y  = ΩKn+1→Kn n (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y)

-ₖ_ : {n : ℕ} →  coHomK n → coHomK n
-ₖ_ {n = n} x = ΩKn+1→Kn n (sym (Kn→ΩKn+1 n x))

-- subtraction as a binary operator
_-ₖ_ : {n : ℕ} → coHomK n → coHomK n → coHomK n
_-ₖ_ {n = n} x y = ΩKn+1→Kn n (Kn→ΩKn+1 n x ∙ sym (Kn→ΩKn+1 n y))

+ₖ-syntax : (n : ℕ) → coHomK n → coHomK n → coHomK n
+ₖ-syntax n = _+ₖ_ {n = n}

-ₖ-syntax : (n : ℕ) → coHomK n → coHomK n
-ₖ-syntax n = -ₖ_ {n = n}

-'ₖ-syntax : (n : ℕ) → coHomK n → coHomK n → coHomK n
-'ₖ-syntax n = _-ₖ_ {n = n}

syntax +ₖ-syntax n x y = x +[ n ]ₖ y
syntax -ₖ-syntax n x = -[ n ]ₖ x
syntax -'ₖ-syntax n x y = x -[ n ]ₖ y

Kn→ΩKn+10ₖ : (n : ℕ) → Kn→ΩKn+1 n (0ₖ n) ≡ refl
Kn→ΩKn+10ₖ zero = sym (rUnit refl)
Kn→ΩKn+10ₖ (suc zero) i j = ∣ (rCancel (merid base) i j) ∣
Kn→ΩKn+10ₖ (suc (suc n)) i j = ∣ (rCancel (merid north) i j) ∣

ΩKn+1→Kn-refl : (n : ℕ) → ΩKn+1→Kn n refl ≡ 0ₖ n
ΩKn+1→Kn-refl zero = refl
ΩKn+1→Kn-refl (suc zero) = refl
ΩKn+1→Kn-refl (suc (suc zero)) = refl
ΩKn+1→Kn-refl (suc (suc (suc zero))) = refl
ΩKn+1→Kn-refl (suc (suc (suc (suc zero)))) = refl
ΩKn+1→Kn-refl (suc (suc (suc (suc (suc n))))) = refl

-0ₖ : {n : ℕ} → -[ n ]ₖ (0ₖ n) ≡ (0ₖ n)
-0ₖ {n = n} = (λ i → ΩKn+1→Kn n (sym (Kn→ΩKn+10ₖ n i)))
           ∙∙ (λ i → ΩKn+1→Kn n (Kn→ΩKn+10ₖ n (~ i)))
           ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 n) (0ₖ n)

+ₖ→∙ : (n : ℕ) (a b : coHomK n) → Kn→ΩKn+1 n (a +[ n ]ₖ b) ≡ Kn→ΩKn+1 n a ∙ Kn→ΩKn+1 n b
+ₖ→∙ n a b = Iso.rightInv (Iso-Kn-ΩKn+1 n) (Kn→ΩKn+1 n a ∙ Kn→ΩKn+1 n b)

lUnitₖ : (n : ℕ) (x : coHomK n) → (0ₖ n) +[ n ]ₖ x ≡ x
lUnitₖ 0 x = Iso.leftInv (Iso-Kn-ΩKn+1 zero) x
lUnitₖ (suc zero) = trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _) λ x → Iso.leftInv (Iso-Kn-ΩKn+1 1) ∣ x ∣
lUnitₖ (suc (suc n)) x =
  (λ i → ΩKn+1→Kn (2 + n) (Kn→ΩKn+10ₖ (2 + n) i ∙ Kn→ΩKn+1 (2 + n) x)) ∙∙
                       (cong (ΩKn+1→Kn (2 + n)) (sym (lUnit (Kn→ΩKn+1 (2 + n) x)))) ∙∙
                       Iso.leftInv (Iso-Kn-ΩKn+1 (2 + n)) x
rUnitₖ : (n : ℕ) (x : coHomK n) → x +[ n ]ₖ (0ₖ n) ≡ x
rUnitₖ 0 x = Iso.leftInv (Iso-Kn-ΩKn+1 zero) x
rUnitₖ (suc zero) = trElim (λ _ → isOfHLevelPath 3 (isOfHLevelTrunc 3) _ _) λ x → Iso.leftInv (Iso-Kn-ΩKn+1 1) ∣ x ∣
rUnitₖ (suc (suc n)) x =
    (λ i → ΩKn+1→Kn (2 + n) (Kn→ΩKn+1 (2 + n) x ∙ Kn→ΩKn+10ₖ (2 + n) i))
  ∙∙ (cong (ΩKn+1→Kn (2 + n)) (sym (rUnit (Kn→ΩKn+1 (2 + n) x))))
  ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 (2 + n)) x

rCancelₖ  : (n : ℕ) (x : coHomK n) → x +[ n ]ₖ (-[ n ]ₖ x) ≡ (0ₖ n)
rCancelₖ zero x = (λ i → ΩKn+1→Kn 0 (Kn→ΩKn+1 zero x ∙ Iso.rightInv (Iso-Kn-ΩKn+1 zero) (sym (Kn→ΩKn+1 zero x)) i)) ∙
                        cong (ΩKn+1→Kn 0) (rCancel (Kn→ΩKn+1 zero x))
rCancelₖ (suc n) x = (λ i → ΩKn+1→Kn (suc n) (Kn→ΩKn+1 (1 + n) x ∙ Iso.rightInv (Iso-Kn-ΩKn+1 (1 + n)) (sym (Kn→ΩKn+1 (1 + n) x)) i)) ∙
                               cong (ΩKn+1→Kn (suc n)) (rCancel (Kn→ΩKn+1 (1 + n) x)) ∙
                               (λ i → ΩKn+1→Kn (suc n) (Kn→ΩKn+10ₖ (suc n) (~ i))) ∙
                               Iso.leftInv (Iso-Kn-ΩKn+1 (suc n)) (0ₖ (suc n))

lCancelₖ : (n : ℕ) (x : coHomK n) → (-[ n ]ₖ x) +[ n ]ₖ x  ≡ (0ₖ n)
lCancelₖ 0 x = (λ i → ΩKn+1→Kn 0 (Iso.rightInv (Iso-Kn-ΩKn+1 zero) (sym (Kn→ΩKn+1 zero x)) i ∙ Kn→ΩKn+1 zero x)) ∙
                        cong (ΩKn+1→Kn 0) (lCancel (Kn→ΩKn+1 zero x))
lCancelₖ (suc n) x = (λ i → ΩKn+1→Kn (suc n) (Iso.rightInv (Iso-Kn-ΩKn+1 (1 + n)) (sym (Kn→ΩKn+1 (1 + n) x)) i ∙ Kn→ΩKn+1 (1 + n) x)) ∙
                               cong (ΩKn+1→Kn (suc n)) (lCancel (Kn→ΩKn+1 (1 + n) x)) ∙
                               (λ i → (ΩKn+1→Kn (suc n)) (Kn→ΩKn+10ₖ (suc n) (~ i))) ∙
                               Iso.leftInv (Iso-Kn-ΩKn+1 (suc n)) (0ₖ (suc n))

assocₖ : (n : ℕ) (x y z : coHomK n) → ((x +[ n ]ₖ y) +[ n ]ₖ z) ≡ (x +[ n ]ₖ (y +[ n ]ₖ z))
assocₖ n x y z = ((λ i → ΩKn+1→Kn n (Kn→ΩKn+1 n (ΩKn+1→Kn n (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y)) ∙ Kn→ΩKn+1 n z)) ∙∙
                          (λ i → ΩKn+1→Kn n (Iso.rightInv (Iso-Kn-ΩKn+1 n) (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y) i ∙ Kn→ΩKn+1 n z)) ∙∙
                          (λ i → ΩKn+1→Kn n (assoc (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) (Kn→ΩKn+1 n z) (~ i)))) ∙
                          (λ i → ΩKn+1→Kn n ((Kn→ΩKn+1 n x) ∙ Iso.rightInv (Iso-Kn-ΩKn+1 n) ((Kn→ΩKn+1 n y ∙ Kn→ΩKn+1 n z)) (~ i)))

cancelₖ : (n : ℕ) (x : coHomK n) → x -[ n ]ₖ x ≡ (0ₖ n)
cancelₖ zero x = cong (ΩKn+1→Kn 0) (rCancel (Kn→ΩKn+1 zero x))
cancelₖ (suc zero) x = cong (ΩKn+1→Kn 1) (rCancel (Kn→ΩKn+1 1 x))
cancelₖ (suc (suc zero)) x = cong (ΩKn+1→Kn 2) (rCancel (Kn→ΩKn+1 2 x))
cancelₖ (suc (suc (suc zero))) x = cong (ΩKn+1→Kn 3) (rCancel (Kn→ΩKn+1 3 x))
cancelₖ (suc (suc (suc (suc zero)))) x = cong (ΩKn+1→Kn 4) (rCancel (Kn→ΩKn+1 4 x))
cancelₖ (suc (suc (suc (suc (suc n))))) x = cong (ΩKn+1→Kn (5 + n)) (rCancel (Kn→ΩKn+1 (5 + n) x))

-rUnitₖ : (n : ℕ) (x : coHomK n) → x -[ n ]ₖ 0ₖ n ≡ x
-rUnitₖ zero x = rUnitₖ zero x
-rUnitₖ (suc n) x = cong (λ y → ΩKn+1→Kn (suc n) (Kn→ΩKn+1 (suc n) x ∙ sym y)) (Kn→ΩKn+10ₖ (suc n))
                 ∙∙ cong (ΩKn+1→Kn (suc n)) (sym (rUnit (Kn→ΩKn+1 (suc n) x)))
                 ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 (suc n)) x

isComm∙ : ∀ {ℓ} (A : Pointed ℓ) → Type ℓ
isComm∙ A = (p q : typ (Ω A)) → p ∙ q ≡ q ∙ p

abstract
  isCommA→isCommTrunc : ∀ {ℓ} {A : Pointed ℓ} (n : ℕ) → isComm∙ A → isOfHLevel (suc n) (typ A) → isComm∙ (∥ typ A ∥ (suc n) , ∣ pt A ∣)
  isCommA→isCommTrunc {A = (A , a)} n comm hlev p q =
      ((λ i j → (Iso.leftInv (truncIdempotentIso (suc n) hlev) ((p ∙ q) j) (~ i)))
   ∙∙ (λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣) (cong (trRec hlev (λ x → x)) (p ∙ q)))
   ∙∙ (λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣) (congFunct {A = ∥ A ∥ (suc n)} {B = A} (trRec hlev (λ x → x)) p q i)))
   ∙ ((λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣) (comm (cong (trRec hlev (λ x → x)) p) (cong (trRec hlev (λ x → x)) q) i))
   ∙∙ (λ i → cong {B = λ _ → ∥ A ∥ (suc n) } (λ x → ∣ x ∣) (congFunct {A = ∥ A ∥ (suc n)} {B = A} (trRec hlev (λ x → x)) q p (~ i)))
   ∙∙ (λ i j → (Iso.leftInv (truncIdempotentIso (suc n) hlev) ((q ∙ p) j) i)))

  isCommΩK1 : (n : ℕ) → isComm∙ ((Ω^ n) (coHomK-ptd 1))
  isCommΩK1 zero = isCommA→isCommTrunc 2 comm-ΩS¹ isGroupoidS¹
  isCommΩK1 (suc n) = Eckmann-Hilton n

  open Iso renaming (inv to inv')
  ptdIso→comm : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Type ℓ'} (e : Iso (typ A) B) → isComm∙ A → isComm∙ (B , Iso.fun e (pt A))
  ptdIso→comm {A = (A , a)} {B = B} e comm p q =
         sym (rightInv (congIso e) (p ∙ q))
      ∙∙ (cong (fun (congIso e)) ((invCongFunct e p q)
                              ∙∙ (comm (inv' (congIso e) p) (inv' (congIso e) q))
                              ∙∙ (sym (invCongFunct e q p))))
      ∙∙ rightInv (congIso e) (q ∙ p)

  isCommΩK : (n : ℕ) → isComm∙ (coHomK-ptd n)
  isCommΩK zero p q = isSetInt _ _ (p ∙ q) (q ∙ p)
  isCommΩK (suc zero) = isCommA→isCommTrunc 2 comm-ΩS¹ isGroupoidS¹
  isCommΩK (suc (suc n)) = subst isComm∙ (λ i → coHomK (2 + n) , ΩKn+1→Kn-refl (2 + n) i) (ptdIso→comm {A = (_ , _)} (invIso (Iso-Kn-ΩKn+1 (2 + n))) (Eckmann-Hilton 0))

commₖ : (n : ℕ) (x y : coHomK n) → (x +[ n ]ₖ y) ≡ (y +[ n ]ₖ x)
commₖ 0 x y i = ΩKn+1→Kn 0 (isCommΩK1 0 (Kn→ΩKn+1 0 x) (Kn→ΩKn+1 0 y) i)
commₖ 1 x y i = ΩKn+1→Kn 1 (ptdIso→comm {A = ((∣ north ∣ ≡ ∣ north ∣) , snd ((Ω^ 1) (coHomK 3 , ∣ north ∣)))}
                                        {B = coHomK 2}
                                        (invIso (Iso-Kn-ΩKn+1 2)) (Eckmann-Hilton 0) (Kn→ΩKn+1 1 x) (Kn→ΩKn+1 1 y) i)
commₖ 2 x y i = ΩKn+1→Kn 2 (ptdIso→comm {A = (∣ north ∣ ≡ ∣ north ∣) , snd ((Ω^ 1) (coHomK 4 , ∣ north ∣))}
                                        {B = coHomK 3}
                                        (invIso (Iso-Kn-ΩKn+1 3)) (Eckmann-Hilton 0) (Kn→ΩKn+1 2 x) (Kn→ΩKn+1 2 y) i)
commₖ 3 x y i = ΩKn+1→Kn 3 (ptdIso→comm {A = (∣ north ∣ ≡ ∣ north ∣) , snd ((Ω^ 1) (coHomK 5 , ∣ north ∣))}
                                        {B = coHomK 4}
                                        (invIso (Iso-Kn-ΩKn+1 4)) (Eckmann-Hilton 0) (Kn→ΩKn+1 3 x) (Kn→ΩKn+1 3 y) i)
commₖ (suc (suc (suc (suc n)))) x y i =
  ΩKn+1→Kn (4 + n) (ptdIso→comm {A = (∣ north ∣ ≡ ∣ north ∣) , snd ((Ω^ 1) (coHomK (6 + n) , ∣ north ∣))}
                                {B = coHomK (5 + n)}
                                (invIso (Iso-Kn-ΩKn+1 (5 + n))) (Eckmann-Hilton 0) (Kn→ΩKn+1 (4 + n) x) (Kn→ΩKn+1 (4 + n) y) i)

rUnitₖ' : (n : ℕ) (x : coHomK n) → x +[ n ]ₖ (0ₖ n) ≡ x
rUnitₖ' n x = commₖ n x (0ₖ n) ∙ lUnitₖ n x

-distrₖ : (n : ℕ) (x y : coHomK n) → -[ n ]ₖ (x +[ n ]ₖ y) ≡ (-[ n ]ₖ x) +[ n ]ₖ (-[ n ]ₖ y)
-distrₖ n x y = ((λ i → ΩKn+1→Kn n (sym (Kn→ΩKn+1 n (ΩKn+1→Kn n (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y))))) ∙∙
                      (λ i → ΩKn+1→Kn n (sym (Iso.rightInv (Iso-Kn-ΩKn+1 n) (Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y) i))) ∙∙
                      (λ i → ΩKn+1→Kn n (symDistr (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) i))) ∙∙
                      (λ i → ΩKn+1→Kn n (Iso.rightInv (Iso-Kn-ΩKn+1 n) (sym (Kn→ΩKn+1 n y)) (~ i) ∙ (Iso.rightInv (Iso-Kn-ΩKn+1 n) (sym (Kn→ΩKn+1 n x)) (~ i)))) ∙∙
                      commₖ n (-[ n ]ₖ y) (-[ n ]ₖ x)

private
  rCancelLem : (n : ℕ) (x : coHomK n) → ΩKn+1→Kn n ((Kn→ΩKn+1 n x) ∙ refl) ≡ ΩKn+1→Kn n (Kn→ΩKn+1 n x)
  rCancelLem zero x = refl
  rCancelLem (suc n) x = cong (ΩKn+1→Kn (suc n)) (sym (rUnit (Kn→ΩKn+1 (suc n) x)))

  lCancelLem : (n : ℕ) (x : coHomK n) → ΩKn+1→Kn n (refl ∙ (Kn→ΩKn+1 n x)) ≡ ΩKn+1→Kn n (Kn→ΩKn+1 n x)
  lCancelLem zero x = refl
  lCancelLem (suc n) x = cong (ΩKn+1→Kn (suc n)) (sym (lUnit (Kn→ΩKn+1 (suc n) x)))

-cancelRₖ : (n : ℕ) (x y : coHomK n) → (y +[ n ]ₖ x) -[ n ]ₖ x ≡ y
-cancelRₖ n x y = (cong (ΩKn+1→Kn n) ((cong (_∙ sym (Kn→ΩKn+1 n x)) (+ₖ→∙ n y x))
                                  ∙∙ sym (assoc _ _ _)
                                  ∙∙ cong (Kn→ΩKn+1 n y ∙_) (rCancel _)))
                   ∙∙ rCancelLem n y
                   ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 n) y

-cancelLₖ : (n : ℕ) (x y : coHomK n) → (x +[ n ]ₖ y) -[ n ]ₖ x ≡ y
-cancelLₖ n x y = cong (λ z → z -[ n ]ₖ x) (commₖ n x y) ∙ -cancelRₖ n x y

-+cancelₖ : (n : ℕ) (x y : coHomK n) → (x -[ n ]ₖ y) +[ n ]ₖ y ≡ x
-+cancelₖ n x y = (cong (ΩKn+1→Kn n) ((cong (_∙ (Kn→ΩKn+1 n y)) (Iso.rightInv (Iso-Kn-ΩKn+1 n) (Kn→ΩKn+1 n x ∙ sym (Kn→ΩKn+1 n y))))
                                  ∙∙ sym (assoc _ _ _)
                                  ∙∙ cong (Kn→ΩKn+1 n x ∙_) (lCancel _)))
                   ∙∙ rCancelLem n x
                   ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 n) x

---- Group structure of cohomology groups ---

_+ₕ_ : {n : ℕ} → coHom n A → coHom n A → coHom n A
_+ₕ_ {n = n} = sRec2 § λ a b → ∣ (λ x → a x +[ n ]ₖ b x) ∣₂

-ₕ_  : {n : ℕ} → coHom n A → coHom n A
-ₕ_  {n = n} = sRec § λ a → ∣ (λ x → -[ n ]ₖ a x) ∣₂

_-ₕ_  : {n : ℕ} → coHom n A → coHom n A → coHom n A
_-ₕ_  {n = n} = sRec2 § λ a b → ∣ (λ x → a x -[ n ]ₖ b x) ∣₂

+ₕ-syntax : (n : ℕ) → coHom n A → coHom n A → coHom n A
+ₕ-syntax n = _+ₕ_ {n = n}

-ₕ-syntax : (n : ℕ) → coHom n A → coHom n A
-ₕ-syntax n = -ₕ_ {n = n}

-ₕ'-syntax : (n : ℕ) → coHom n A → coHom n A → coHom n A
-ₕ'-syntax n = _-ₕ_ {n = n}

syntax +ₕ-syntax n x y = x +[ n ]ₕ y
syntax -ₕ-syntax n x = -[ n ]ₕ x
syntax -ₕ'-syntax n x y = x -[ n ]ₕ y

0ₕ : (n : ℕ) → coHom n A
0ₕ n = ∣ (λ _ → (0ₖ n)) ∣₂

rUnitₕ : (n : ℕ) (x : coHom n A) → x +[ n ]ₕ (0ₕ n) ≡ x
rUnitₕ n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                λ a i → ∣ funExt (λ x → rUnitₖ n (a x)) i ∣₂

lUnitₕ : (n : ℕ) (x : coHom n A) → (0ₕ n) +[ n ]ₕ x ≡ x
lUnitₕ n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                  λ a i → ∣ funExt (λ x → lUnitₖ n (a x)) i ∣₂

rCancelₕ : (n : ℕ) (x : coHom n A) → x +[ n ]ₕ (-[ n ]ₕ x) ≡ 0ₕ n
rCancelₕ n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                 λ a i → ∣ funExt (λ x → rCancelₖ n (a x)) i ∣₂

lCancelₕ : (n : ℕ) (x : coHom n A) → (-[ n ]ₕ x) +[ n ]ₕ x  ≡ 0ₕ n
lCancelₕ n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                 λ a i → ∣ funExt (λ x → lCancelₖ n (a x)) i ∣₂

assocₕ : (n : ℕ) (x y z : coHom n A) → ((x +[ n ]ₕ y) +[ n ]ₕ z) ≡ (x +[ n ]ₕ (y +[ n ]ₕ z))
assocₕ n = elim3 (λ _ _ _ → isOfHLevelPath 1 (§ _ _))
               λ a b c i → ∣ funExt (λ x → assocₖ n (a x) (b x) (c x)) i ∣₂

commₕ : (n : ℕ) (x y : coHom n A) → (x +[ n ]ₕ y) ≡ (y +[ n ]ₕ x)
commₕ n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                        λ a b i → ∣ funExt (λ x → commₖ n (a x) (b x)) i ∣₂

cancelₕ : (n : ℕ) (x : coHom n A) → x -[ n ]ₕ x ≡ 0ₕ n
cancelₕ n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                   λ a i → ∣ funExt (λ x → cancelₖ n (a x)) i ∣₂

-ₖ-ₖ : (n : ℕ) (x : coHomK n) → (-[ n ]ₖ (-[ n ]ₖ x)) ≡ x
-ₖ-ₖ n x = cong ((ΩKn+1→Kn n) ∘ sym) (Iso.rightInv (Iso-Kn-ΩKn+1 n) (sym (Kn→ΩKn+1 n x))) ∙ Iso.leftInv (Iso-Kn-ΩKn+1 n) x

-- Proof that rUnitₖ and lUnitₖ agree on 0ₖ. Needed for Mayer-Vietoris.
private
  rUnitlUnitGen : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {b : B} (e : Iso A (b ≡ b))
                  (0A : A)
                  (0fun : fun e 0A ≡ refl)
                → Path (inv' e (fun e 0A ∙ fun e 0A) ≡ 0A)
                       (cong (inv' e) (cong (_∙ fun e 0A) 0fun) ∙∙ cong (inv' e) (sym (lUnit (fun e 0A))) ∙∙ Iso.leftInv e 0A)
                       (cong (inv' e) (cong (fun e 0A ∙_) 0fun) ∙∙ cong (inv' e) (sym (rUnit (fun e 0A))) ∙∙ Iso.leftInv e 0A)
  rUnitlUnitGen e 0A 0fun =
      (λ i → cong (inv' e) (cong (_∙ fun e 0A) 0fun) ∙∙ rUnit (cong (inv' e) (sym (lUnit (fun e 0A)))) i ∙∙ Iso.leftInv e 0A)
    ∙ ((λ i → (λ j → inv' e (0fun (~ i ∧ j) ∙ 0fun (j ∧ i)))
            ∙∙ ((λ j → inv' e (0fun (~ i ∨ j) ∙ 0fun i))
            ∙∙ cong (inv' e) (sym (lUnit (0fun i)))
            ∙∙ λ j → inv' e (0fun (i ∧ (~ j))))
            ∙∙ Iso.leftInv e 0A)
    ∙∙ (λ i → (λ j → inv' e (fun e 0A ∙ 0fun j))
            ∙∙ (λ j → inv' e (0fun (j ∧ ~ i) ∙ refl))
            ∙∙ cong (inv' e) (sym (rUnit (0fun (~ i))))
            ∙∙ (λ j → inv' e (0fun (~ i ∧ ~ j)))
            ∙∙ Iso.leftInv e 0A)
    ∙∙ λ i → cong (inv' e) (cong (fun e 0A ∙_) 0fun)
           ∙∙ rUnit (cong (inv' e) (sym (rUnit (fun e 0A)))) (~ i)
           ∙∙ Iso.leftInv e 0A)

rUnitlUnit0 : (n : ℕ) → rUnitₖ n (0ₖ n) ≡ lUnitₖ n (0ₖ n)
rUnitlUnit0 0 = refl
rUnitlUnit0 (suc zero) = refl
rUnitlUnit0 (suc (suc n)) = sym (rUnitlUnitGen (Iso-Kn-ΩKn+1 (2 + n)) (0ₖ (2 + n)) (Kn→ΩKn+10ₖ (2 + n)))

-cancelLₕ : (n : ℕ) (x y : coHom n A) → (x +[ n ]ₕ y) -[ n ]ₕ x ≡ y
-cancelLₕ n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                     λ a b i → ∣ (λ x → -cancelLₖ n (a x) (b x) i) ∣₂

-cancelRₕ : (n : ℕ) (x y : coHom n A) → (y +[ n ]ₕ x) -[ n ]ₕ x ≡ y
-cancelRₕ n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                     λ a b i → ∣ (λ x → -cancelRₖ n (a x) (b x) i) ∣₂

-+cancelₕ : (n : ℕ) (x y : coHom n A) → (x -[ n ]ₕ y) +[ n ]ₕ y ≡ x
-+cancelₕ n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                     λ a b i → ∣ (λ x → -+cancelₖ n (a x) (b x) i) ∣₂

-- Group structure of reduced cohomology groups (in progress - might need K to compute properly first) ---

+ₕ∙ : {A : Pointed ℓ} (n : ℕ) → coHomRed n A → coHomRed n A → coHomRed n A
+ₕ∙ zero = sRec2 § λ { (a , pa) (b , pb) → ∣ (λ x → a x +[ zero ]ₖ b x) , (λ i → (pa i +[ zero ]ₖ pb i)) ∣₂ }
+ₕ∙ (suc zero) = sRec2 § λ { (a , pa) (b , pb) → ∣ (λ x → a x +[ 1 ]ₖ b x) , (λ i → pa i +[ 1 ]ₖ pb i) ∙ lUnitₖ 1 (0ₖ 1) ∣₂ }
+ₕ∙ (suc (suc n)) = sRec2 § λ { (a , pa) (b , pb) → ∣ (λ x → a x +[ (2 + n) ]ₖ b x) , (λ i → pa i +[ (2 + n) ]ₖ pb i) ∙ lUnitₖ (2 + n) (0ₖ (2 + n)) ∣₂ }

open IsSemigroup
open IsMonoid
open GroupStr
open GroupHom

coHomGr : ∀ {ℓ} (n : ℕ) (A : Type ℓ) → Group {ℓ}
coHomGr n A = coHom n A , coHomGrnA
  where
  coHomGrnA : GroupStr (coHom n A)
  0g coHomGrnA = 0ₕ n
  GroupStr._+_ coHomGrnA = λ x y → x +[ n ]ₕ y
  - coHomGrnA = λ x → -[ n ]ₕ x
  isGroup coHomGrnA = helper
    where
    abstract
      helper : IsGroup (0ₕ n) (λ x y → x +[ n ]ₕ y) (λ x → -[ n ]ₕ x)
      helper = makeIsGroup § (λ x y z → sym (assocₕ n x y z)) (rUnitₕ n) (lUnitₕ n) (rCancelₕ n) (lCancelₕ n)

×coHomGr : (n : ℕ) (A : Type ℓ) (B : Type ℓ') → Group
×coHomGr n A B = dirProd (coHomGr n A) (coHomGr n B)

coHomFun : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n : ℕ) (f : A → B) → coHom n B → coHom n A
coHomFun n f = sRec § λ β → ∣ β ∘ f ∣₂

-distrLemma : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n m : ℕ) (f : GroupHom (coHomGr n A) (coHomGr m B))
              (x y : coHom n A)
            → fun f (x -[ n ]ₕ y) ≡ fun f x -[ m ]ₕ fun f y
-distrLemma n m f' x y = sym (-cancelRₕ m (f y) (f (x -[ n ]ₕ y)))
                     ∙∙ cong (λ x → x -[ m ]ₕ f y) (sym (isHom f' (x -[ n ]ₕ y) y))
                     ∙∙ cong (λ x → x -[ m ]ₕ f y) ( cong f (-+cancelₕ n _ _))
  where
  f = fun f'

--- the loopspace of Kₙ is commutative regardless of base

addIso : (n : ℕ) (x : coHomK n) → Iso (coHomK n) (coHomK n)
fun (addIso n x) y = y +[ n ]ₖ x
inv' (addIso n x) y = y -[ n ]ₖ x
rightInv (addIso n x) y = -+cancelₖ n y x
leftInv (addIso n x) y = -cancelRₖ n x y

isCommΩK-based : (n : ℕ) (x : coHomK n) → isComm∙ (coHomK n , x)
isCommΩK-based zero x p q = isSetInt _ _ (p ∙ q) (q ∙ p)
isCommΩK-based (suc zero) x =
  subst isComm∙ (λ i → coHomK 1 , lUnitₖ 1 x i)
                (ptdIso→comm {A = (_ , 0ₖ 1)} (addIso 1 x)
                              (isCommΩK 1))
isCommΩK-based (suc (suc n)) x =
  subst isComm∙ (λ i → coHomK (suc (suc n)) , lUnitₖ (suc (suc n)) x i)
                (ptdIso→comm {A = (_ , 0ₖ (suc (suc n)))} (addIso (suc (suc n)) x)
                              (isCommΩK (suc (suc n))))

addLemma : (a b : Int) → a +[ 0 ]ₖ b ≡ (a ℤ+ b)
addLemma a b = (cong (ΩKn+1→Kn 0) (sym (congFunct ∣_∣ (intLoop a) (intLoop b))))
            ∙∙ (λ i → ΩKn+1→Kn 0 (cong ∣_∣ (intLoop-hom a b i)))
            ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 0) (a ℤ+ b)

---
-- hidden versions of cohom stuff using the "lock" hack. The locked versions can be used when proving things.
-- Swapping "key" for "tt*" will then give computing functions.

Unit' : Type₀
Unit' = lockUnit {ℓ-zero}

lock : ∀ {ℓ} {A : Type ℓ} → Unit' → A → A
lock unlock = λ x → x

module lockedCohom (key : Unit') where
  +K : (n : ℕ) → coHomK n → coHomK n → coHomK n
  +K n = lock key (_+ₖ_ {n = n})

  -K : (n : ℕ) → coHomK n → coHomK n
  -K n = lock key (-ₖ_ {n = n})

  -Kbin : (n : ℕ) → coHomK n → coHomK n → coHomK n
  -Kbin n = lock key (_-ₖ_ {n = n})

  rUnitK : (n : ℕ) (x : coHomK n) → +K n x (0ₖ n) ≡ x
  rUnitK n x = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) x (0ₖ n) ≡ x
    pm unlock = rUnitₖ n x

  lUnitK : (n : ℕ) (x : coHomK n) → +K n (0ₖ n) x ≡ x
  lUnitK n x = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) (0ₖ n) x ≡ x
    pm unlock = lUnitₖ n x

  rCancelK : (n : ℕ) (x : coHomK n) → +K n x (-K n x) ≡ 0ₖ n
  rCancelK n x = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) x (lock t (-ₖ_ {n = n}) x) ≡ 0ₖ n
    pm unlock = rCancelₖ n x

  lCancelK : (n : ℕ) (x : coHomK n) → +K n (-K n x) x ≡ 0ₖ n
  lCancelK n x = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) (lock t (-ₖ_ {n = n}) x) x ≡ 0ₖ n
    pm unlock = lCancelₖ n x

  -cancelRK : (n : ℕ) (x y : coHomK n) → -Kbin n (+K n y x) x ≡ y
  -cancelRK n x y = pm key
    where
    pm : (t : Unit') → lock t (_-ₖ_ {n = n}) (lock t (_+ₖ_ {n = n}) y x) x ≡ y
    pm unlock = -cancelRₖ n x y

  -cancelLK : (n : ℕ) (x y : coHomK n) → -Kbin n (+K n x y) x ≡ y
  -cancelLK n x y = pm key
    where
    pm : (t : Unit') → lock t (_-ₖ_ {n = n}) (lock t (_+ₖ_ {n = n}) x y) x ≡ y
    pm unlock = -cancelLₖ n x y

  -+cancelK : (n : ℕ) (x y : coHomK n) → +K n (-Kbin n x y) y ≡ x
  -+cancelK n x y = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) (lock t (_-ₖ_ {n = n}) x y) y ≡ x
    pm unlock = -+cancelₖ n x y

  cancelK : (n : ℕ) (x : coHomK n) → -Kbin n x x ≡ 0ₖ n
  cancelK n x = pm key
    where
    pm : (t : Unit') → (lock t (_-ₖ_ {n = n}) x x) ≡ 0ₖ n
    pm unlock = cancelₖ n x

  assocK : (n : ℕ) (x y z : coHomK n) → +K n (+K n x y) z ≡ +K n x (+K n y z)
  assocK n x y z = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) (lock t (_+ₖ_ {n = n}) x y) z
                     ≡ lock t (_+ₖ_ {n = n}) x (lock t (_+ₖ_ {n = n}) y z)
    pm unlock = assocₖ n x y z

  commK : (n : ℕ) (x y : coHomK n) → +K n x y ≡ +K n y x
  commK n x y = pm key
    where
    pm : (t : Unit') → lock t (_+ₖ_ {n = n}) x y ≡ lock t (_+ₖ_ {n = n}) y x
    pm unlock = commₖ n x y

  -- cohom

  +H : (n : ℕ) (x y : coHom n A) → coHom n A
  +H n = sRec2 § λ a b → ∣ (λ x → +K n (a x) (b x)) ∣₂

  -H : (n : ℕ) (x : coHom n A) → coHom n A
  -H n = sRec § λ a → ∣ (λ x → -K n (a x)) ∣₂

  -Hbin : (n : ℕ) → coHom n A → coHom n A → coHom n A
  -Hbin n = sRec2 § λ a b → ∣ (λ x → -Kbin n (a x) (b x)) ∣₂

  rUnitH : (n : ℕ) (x : coHom n A) → +H n x (0ₕ n) ≡ x
  rUnitH n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                  λ a i → ∣ funExt (λ x → rUnitK n (a x)) i ∣₂

  lUnitH : (n : ℕ) (x : coHom n A) → +H n (0ₕ n) x ≡ x
  lUnitH n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                    λ a i → ∣ funExt (λ x → lUnitK n (a x)) i ∣₂

  rCancelH : (n : ℕ) (x : coHom n A) → +H n x (-H n x) ≡ 0ₕ n
  rCancelH n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                   λ a i → ∣ funExt (λ x → rCancelK n (a x)) i ∣₂

  lCancelH : (n : ℕ) (x : coHom n A) → +H n (-H n x) x  ≡ 0ₕ n
  lCancelH n = sElim (λ _ → isOfHLevelPath 1 (§ _ _))
                   λ a i → ∣ funExt (λ x → lCancelK n (a x)) i ∣₂

  assocH : (n : ℕ) (x y z : coHom n A) → (+H n (+H n x y) z) ≡ (+H n x (+H n y z))
  assocH n = elim3 (λ _ _ _ → isOfHLevelPath 1 (§ _ _))
                 λ a b c i → ∣ funExt (λ x → assocK n (a x) (b x) (c x)) i ∣₂

  commH : (n : ℕ) (x y : coHom n A) → (+H n x y) ≡ (+H n y x)
  commH n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                          λ a b i → ∣ funExt (λ x → commK n (a x) (b x)) i ∣₂

  -cancelRH : (n : ℕ) (x y : coHom n A) → -Hbin n (+H n y x) x ≡ y
  -cancelRH n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                        λ a b i → ∣ (λ x → -cancelRK n (a x) (b x) i) ∣₂

  -cancelLH : (n : ℕ) (x y : coHom n A) → -Hbin n (+H n x y) x ≡ y
  -cancelLH n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                        λ a b i → ∣ (λ x → -cancelLK n (a x) (b x) i) ∣₂

  -+cancelH : (n : ℕ) (x y : coHom n A) → +H n (-Hbin n x y) y ≡ x
  -+cancelH n = sElim2 (λ _ _ → isOfHLevelPath 1 (§ _ _))
                        λ a b i → ∣ (λ x → -+cancelK n (a x) (b x) i) ∣₂

+K→∙ : (key : Unit') (n : ℕ) (a b : coHomK n) → Kn→ΩKn+1 n (lockedCohom.+K key n a b) ≡ Kn→ΩKn+1 n a ∙ Kn→ΩKn+1 n b
+K→∙ unlock = +ₖ→∙

+H≡+ₕ : (key : Unit') (n : ℕ) → lockedCohom.+H key {A = A} n ≡ _+ₕ_ {n = n}
+H≡+ₕ unlock _ = refl

rUnitlUnit0K : (key : Unit') (n : ℕ) → lockedCohom.rUnitK key n (0ₖ n) ≡ lockedCohom.lUnitK key n (0ₖ n)
rUnitlUnit0K unlock = rUnitlUnit0

max_stars_repo_name: ayberkt/cubical

max_issues_repo_name: ayberkt/cubical

max_forks_repo_name: ayberkt/cubical


text:
module FunctorComposition where

open import Functor as F

compose : {F₁ F₂ : Setoid → Setoid} →
          Functor F₁ → Functor F₂ → Functor (λ A → F₁ (F₂ A))
compose {F₁} {F₂} FF₁ FF₂ = record
  { map      = map FF₁ ∘ map FF₂
  ; identity = λ {A} →
      trans (F₁ (F₂ A) ⇨ F₁ (F₂ A))
            {i = map FF₁ ⟨$⟩ (map FF₂ ⟨$⟩ id)}
            {j = map FF₁ ⟨$⟩ id}
            {k = id}
            (cong (map FF₁) (identity FF₂))
            (identity FF₁)
  ; composition = λ {A B C} f g →
      trans (F₁ (F₂ A) ⇨ F₁ (F₂ C))
            {i = map FF₁ ⟨$⟩ (map FF₂ ⟨$⟩ (f ∘ g))}
            {j = map FF₁ ⟨$⟩ ((map FF₂ ⟨$⟩ f) ∘ (map FF₂ ⟨$⟩ g))}
            {k = (map FF₁ ⟨$⟩ (map FF₂ ⟨$⟩ f)) ∘
                 (map FF₁ ⟨$⟩ (map FF₂ ⟨$⟩ g))}
            (cong (map FF₁) (composition FF₂ f g))
            (composition FF₁ (map FF₂ ⟨$⟩ f) (map FF₂ ⟨$⟩ g))
  }
  where
  open Setoid
  open F.Functor

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda